1.1 --- a/test/Tools/isac/Minisubpbl/500-met-sub-to-root.sml Tue May 17 17:38:35 2011 +0200
1.2 +++ b/test/Tools/isac/Minisubpbl/500-met-sub-to-root.sml Tue May 17 17:54:58 2011 +0200
1.3 @@ -5,26 +5,47 @@
1.4
1.5 val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
1.6 val (dI',pI',mI') =
1.7 - ("Test", ["sqroot-test","univariate","equation","test"],
1.8 - ["Test","squ-equ-test-subpbl1"]);
1.9 + ("Test", ["sqroot-test","univariate","equation","test"],
1.10 + ["Test","squ-equ-test-subpbl1"]);
1.11 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.12 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.13 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.14 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.15 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.16 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.17 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.18 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.19 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.20 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.21 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Subproblem"*)
1.22 -(*
1.23 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.24 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.25 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.26 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.27 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.28 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.29 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.30 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.31 -*)
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;
1.35 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.36 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.37 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "squ-equ-test-subpbl1"]*)
1.38 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.39 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.40 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subp ["linear", "univariate", "equation", "test"]*)
1.41 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.42 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.43 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.44 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.45 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.46 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.47 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.48 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*)
1.49 +val (p,_,f,nxt,_,pt) = me nxt p'' [] pt''; (*nxt = Rewrite_Set_Inst isolate_bdv*);
1.50 +get_ctxt pt p |> is_e_ctxt; (*true ...?!?*)
1.51 +get_loc pt p |> snd |> is_e_ctxt; (*true ...?!?*)
1.52 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*);
1.53 +get_ctxt pt p |> is_e_ctxt; (*true ...?!?*)
1.54 +get_loc pt p |> snd |> is_e_ctxt; (*true ...?!?*)
1.55 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["linear","univariate", ...]) *);
1.56 +"~~~~~ fun me, args:"; val (_,tac) = nxt;
1.57 +val (pt, p) = case locatetac tac (pt,p) of
1.58 + ("ok", (_, _, ptp)) => ptp | _ => error "script.sml locatetac";
1.59 +show_pt pt; (*...(([3], Res), [x = 1])]... back in root, OK *)
1.60 +"~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
1.61 +val pIopt = get_pblID (pt,ip); (*= SOME ["sqroot-test", "univariate", ...]*)
1.62 +tacis; (*= []*)
1.63 +member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*)
1.64 +"~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
1.65 +val thy' = get_obj g_domID pt (par_pblobj pt p);
1.66 +val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*)
1.67 +"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt,(p,_)):ptree * pos'), (sc as Script (h $ body)),
1.68 + (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
1.69 +l; (*= [R, R, D, L, R]*)
1.70 +"~~~~~ dont like to go into nstep_up...";
1.71 +
2.1 --- a/test/Tools/isac/Test_Isac.thy Tue May 17 17:38:35 2011 +0200
2.2 +++ b/test/Tools/isac/Test_Isac.thy Tue May 17 17:54:58 2011 +0200
2.3 @@ -172,7 +172,7 @@
2.4 ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}
2.5
2.6 ML {*
2.7 -(*Minisubpbl/500-met-sub-to-root.sml*)
2.8 +(*500-met-sub-to-root*)
2.9 val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
2.10 val (dI',pI',mI') =
2.11 ("Test", ["sqroot-test","univariate","equation","test"],
2.12 @@ -196,71 +196,21 @@
2.13 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.14 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.15 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*)
2.16 -get_ctxt pt p |> is_e_ctxt; (*false... OK: from specify, PblObj{ctxt,...}*)
2.17 -val ctxt = get_ctxt pt p;
2.18 +val (p,_,f,nxt,_,pt) = me nxt p'' [] pt''; (*nxt = Rewrite_Set_Inst isolate_bdv*);
2.19 +get_ctxt pt p |> is_e_ctxt; (*false*)
2.20 +val ctxt = get_ctxt pt p;
2.21 val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
2.22 -get_loc pt p |> snd |> is_e_ctxt; (*true ... OK: interpreter not yet started*)
2.23 -val (pt'',p'') = (pt, p);
2.24 -"~~~~~ fun me, args:"; val (_,tac) = nxt;
2.25 -"~~~~~ fun locatetac, args:"; val ptp as (pt, p) = (pt, p);
2.26 -val (mI,m) = mk_tac'_ tac;
2.27 -val Appl m = applicable_in p pt m;
2.28 -member op = specsteps mI; (*false*)
2.29 -"~~~~~ fun loc_solve_, args:"; val (m, (pt, pos) ) = ((mI, m), ptp);
2.30 -"~~~~~ fun solve, args:"; val (("Apply_Method", Apply_Method' (mI,_,_,_)), pos as (p,_)) = (m, pos);
2.31 -val {srls, ...} = get_met mI;
2.32 -val PblObj {meth=itms, ctxt, ...} = get_obj I pt p;
2.33 +get_loc pt p |> snd |> is_e_ctxt; (*false*)
2.34 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*);
2.35 +get_ctxt pt p |> is_e_ctxt; (*false*)
2.36 +val ctxt = get_ctxt pt p;
2.37 val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
2.38 -val thy' = get_obj g_domID pt p;
2.39 -val thy = assoc_thy thy';
2.40 -val (is as ScrState (env,_,_,_,_,_), _, sc) = init_scrstate thy itms mI;
2.41 -(*dont take ctxt ^^^ from ^^^^^^^^^^^^^*)
2.42 -(*= the first part vvvvvvvvv works now =======================================*)
2.43 -val (pt, p) = case locatetac tac (pt'',p'') of
2.44 - ("ok", (_, _, ptp)) => ptp | _ => error "script.sml locatetac";
2.45 -val ctxt = get_ctxt pt p;
2.46 -val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
2.47 -(*= the first part ^^^^^^^^^^ works now =======================================*)
2.48 -val (pt'',p'') = (pt, p);
2.49 -"~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
2.50 -val pIopt = get_pblID (pt,ip);
2.51 -tacis; (*= []*)
2.52 -member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*)
2.53 -"~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
2.54 -val thy' = get_obj g_domID pt (par_pblobj pt p);
2.55 -val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
2.56 -"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt,(p,_)):ptree * pos'), (sc as Script (h $ body)),
2.57 - (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
2.58 -val ctxt = get_ctxt pt pos;
2.59 -val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
2.60 -(*= the first part ^^^^^^^^^^ works now =======================================*)
2.61 -l = [];
2.62 -appy thy ptp E [R] body NONE v;
2.63 -val (p,_,f,nxt,_,pt) = me nxt p'' [] pt''; (*nxt = Rewrite_Set_Inst isolate_bdv*);
2.64 +get_loc pt p |> snd |> is_e_ctxt; (*false*)
2.65 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["linear","univariate", ...]) *);
2.66 +val (pt'', p'') = (pt, p);
2.67 *}
2.68 ML {*
2.69 -*}
2.70 -ML {*
2.71 -*}
2.72 -ML {*
2.73 -*}
2.74 -ML {*
2.75 -*}
2.76 -ML {*
2.77 -*}
2.78 -ML {*
2.79 -*}
2.80 -ML {*
2.81 -get_ctxt pt p |> is_e_ctxt; (*true ...?!?*)
2.82 -get_loc pt p |> snd |> is_e_ctxt; (*true ...?!?*)
2.83 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*);
2.84 -*}
2.85 -ML {*
2.86 -get_ctxt pt p |> is_e_ctxt; (*true ...?!?*)
2.87 -get_loc pt p |> snd |> is_e_ctxt; (*true ...?!?*)
2.88 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["linear","univariate", ...]) *);
2.89 -*}
2.90 -ML {*
2.91 +val (pt'', p'') = (pt, p);
2.92 "~~~~~ fun me, args:"; val (_,tac) = nxt;
2.93 val (pt, p) = case locatetac tac (pt,p) of
2.94 ("ok", (_, _, ptp)) => ptp | _ => error "script.sml locatetac";
2.95 @@ -279,10 +229,19 @@
2.96 *}
2.97 ML {*
2.98 *}
2.99 -
2.100 -
2.101 ML {*
2.102 *}
2.103 +ML {*
2.104 +*}
2.105 +ML {*
2.106 +*}
2.107 +ML {*
2.108 +*}
2.109 +ML {*
2.110 +*}
2.111 +ML {*
2.112 +val (p,_,f,nxt,_,pt) = me nxt p'' [] pt''; (*WAS nxt = ("Empty_Tac", Empty_Tac)*)
2.113 +*}
2.114
2.115 end
2.116