1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Sat May 21 09:40:02 2011 +0200
1.3 @@ -0,0 +1,84 @@
1.4 +(* Title: 530-error-Check_Elementwise.sml
1.5 +Author: Walther Neuper 1105
1.6 +(c) copyright due to lincense terms.
1.7 +*)
1.8 +
1.9 +"----------- Minisubplb/530-error-Check_Elementwise.sml ----------";
1.10 +"----------- Minisubplb/530-error-Check_Elementwise.sml ----------";
1.11 +"----------- Minisubplb/530-error-Check_Elementwise.sml ----------";
1.12 +val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
1.13 +val (dI',pI',mI') =
1.14 +("Test", ["sqroot-test","univariate","equation","test"],
1.15 +["Test","squ-equ-test-subpbl1"]);
1.16 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.17 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.18 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.19 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.20 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.21 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.22 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.23 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "squ-equ-test-subpbl1"]*)
1.24 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.25 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.26 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subp ["linear", "univariate", "equation", "test"]*)
1.27 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.28 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.29 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.30 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.31 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.32 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.33 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.34 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*)
1.35 +val (p,_,f,nxt,_,pt) = me nxt p'' [] pt''; (*nxt = Rewrite_Set_Inst isolate_bdv*);
1.36 +get_ctxt pt p |> is_e_ctxt; (*false*)
1.37 +val ctxt = get_ctxt pt p;
1.38 +val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
1.39 +get_loc pt p |> snd |> is_e_ctxt; (*false*)
1.40 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*);
1.41 +get_ctxt pt p |> is_e_ctxt; (*false*)
1.42 +val ctxt = get_ctxt pt p;
1.43 +val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
1.44 +get_loc pt p |> snd |> is_e_ctxt; (*false*)
1.45 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["linear","univariate", ...]) *);
1.46 +
1.47 +val (pt'''', p'''') = (pt, p);
1.48 +"~~~~~ fun me, args:"; val (_,tac) = nxt;
1.49 +val (pt, p) = case locatetac tac (pt,p) of
1.50 +("ok", (_, _, ptp)) => ptp | _ => error "script.sml locatetac";
1.51 +show_pt pt; (*...(([3], Res), [x = 1])]... back in root, OK *)
1.52 +"~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
1.53 +val pIopt = get_pblID (pt,ip); (*= SOME ["sqroot-test", "univariate", ...]*)
1.54 +tacis; (*= []*)
1.55 +member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*)
1.56 +"~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
1.57 +val thy' = get_obj g_domID pt (par_pblobj pt p);
1.58 +val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*)
1.59 +"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt, pos as (p, _)):ptree * pos'), (sc as Script (h $ body)),
1.60 +(ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
1.61 +val ctxt = get_ctxt pt pos
1.62 +val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
1.63 +l; (*= [R, R, D, L, R]*)
1.64 +"~~~~~ fun nstep_up, args:"; val (thy, ptp, (Script sc), E, l, ay, a, v) =
1.65 +(thy, ptp, sc, E, l, Skip_, a, v);
1.66 +1 < length l; (*true*)
1.67 +val up = drop_last l;
1.68 +go up sc; (* = Const ("HOL.Let", *)
1.69 +"~~~~~ fun nxt_up, args:"; val (thy, ptp, (scr as (Script sc)), E, l, ay,
1.70 +(t as Const ("HOL.Let",_) $ _), a, v) =
1.71 +(thy, ptp, (Script sc), E, up, ay, (go up sc), a, v);
1.72 +ay = Napp_; (*false*)
1.73 +val up = drop_last l;
1.74 +val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go up sc;
1.75 +val i = mk_Free (i, T);
1.76 +val E = upd_env E (i, v);
1.77 +body; (*= Const ("Script.Check'_elementwise"*)
1.78 +"~~~~~ fun appy, args:"; val ((thy as (th,sr)), (pt, p), E, l, t, a, v)=
1.79 +(thy, ptp, E, (up@[R,D]), body, a, v);
1.80 +handle_leaf "next " th sr E a v t; (*= (NONE, STac (Const ("Script.Check'_elementwise"*)
1.81 +val (a', STac stac) = handle_leaf "next " th sr E a v t;
1.82 +"~~~~~ fun stac2tac_, args:"; val (pt, thy, (Const("Script.Check'_elementwise",_) $ _ $
1.83 +(set as Const ("Set.Collect",_) $ Abs (_,_,pred)))) = (pt, (assoc_thy th), stac);
1.84 +(*2011 changed ^^^^^ *)
1.85 +val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*WAS nxt = ("Empty_Tac", Empty_Tac)*)
1.86 +if nxt = ("Check_elementwise", Check_elementwise "Assumptions") then ()
1.87 +else error "Check_elementwise changed; after switch sub-->root-method"
2.1 --- a/test/Tools/isac/Test_Isac.thy Sat May 21 09:30:36 2011 +0200
2.2 +++ b/test/Tools/isac/Test_Isac.thy Sat May 21 09:40:02 2011 +0200
2.3 @@ -165,6 +165,7 @@
2.4 ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}
2.5
2.6 ML {*
2.7 +
2.8 *}
2.9 ML {*
2.10 "----------- Minisubplb/500-met-sub-to-root.sml ------------------";