1.1 --- a/test/Tools/isac/Test_Isac.thy Tue May 17 15:02:43 2011 +0200
1.2 +++ b/test/Tools/isac/Test_Isac.thy Tue May 17 17:38:35 2011 +0200
1.3 @@ -101,48 +101,6 @@
1.4 use "Minisubpbl/400-start-meth-subpbl.sml"
1.5 use "Minisubpbl/500-met-sub-to-root.sml"
1.6 use "Minisubpbl/600-postcond.sml"
1.7 -
1.8 -ML {*
1.9 -val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
1.10 -val (dI',pI',mI') =
1.11 - ("Test", ["sqroot-test","univariate","equation","test"],
1.12 - ["Test","squ-equ-test-subpbl1"]);
1.13 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.14 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.15 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.16 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
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 = ("Subproblem"*)
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;
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; (*nxt = Rewrite_Set_Inst isolate_bdv*);
1.33 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*);
1.34 -*}
1.35 -ML {*
1.36 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["linear","univariate", ...]) *);
1.37 -*}
1.38 -ML {*
1.39 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.40 -*}
1.41 -ML {*
1.42 -*}
1.43 -ML {*
1.44 -*}
1.45 -ML {*
1.46 -*}
1.47 -
1.48 -
1.49 ML {*"%%%%%%%%%%%%%%%%% end Minisubpbl %%%%%%%%%%%%%%%%%%%%%%%";*}
1.50 ML {*"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";*}
1.51 use "Interpret/mstools.sml" (*new 2010*)
1.52 @@ -214,17 +172,71 @@
1.53 ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}
1.54
1.55 ML {*
1.56 -val am = [];
1.57 -insert_assumptions am
1.58 -*}
1.59 -ML {*
1.60 -val ctxt = get_ctxt pt p |> insert_assumptions am
1.61 -*}
1.62 -ML {*
1.63 -from_pblobj_or_detail'
1.64 -*}
1.65 -ML {*
1.66 -from_pblobj'
1.67 +(*Minisubpbl/500-met-sub-to-root.sml*)
1.68 +val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
1.69 +val (dI',pI',mI') =
1.70 + ("Test", ["sqroot-test","univariate","equation","test"],
1.71 + ["Test","squ-equ-test-subpbl1"]);
1.72 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.73 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.74 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.75 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.76 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.77 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.78 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.79 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "squ-equ-test-subpbl1"]*)
1.80 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.81 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.82 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subp ["linear", "univariate", "equation", "test"]*)
1.83 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.84 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.85 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.86 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.87 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.88 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.89 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.90 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*)
1.91 +get_ctxt pt p |> is_e_ctxt; (*false... OK: from specify, PblObj{ctxt,...}*)
1.92 +val ctxt = get_ctxt pt p;
1.93 +val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
1.94 +get_loc pt p |> snd |> is_e_ctxt; (*true ... OK: interpreter not yet started*)
1.95 +val (pt'',p'') = (pt, p);
1.96 +"~~~~~ fun me, args:"; val (_,tac) = nxt;
1.97 +"~~~~~ fun locatetac, args:"; val ptp as (pt, p) = (pt, p);
1.98 +val (mI,m) = mk_tac'_ tac;
1.99 +val Appl m = applicable_in p pt m;
1.100 +member op = specsteps mI; (*false*)
1.101 +"~~~~~ fun loc_solve_, args:"; val (m, (pt, pos) ) = ((mI, m), ptp);
1.102 +"~~~~~ fun solve, args:"; val (("Apply_Method", Apply_Method' (mI,_,_,_)), pos as (p,_)) = (m, pos);
1.103 +val {srls, ...} = get_met mI;
1.104 +val PblObj {meth=itms, ctxt, ...} = get_obj I pt p;
1.105 +val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
1.106 +val thy' = get_obj g_domID pt p;
1.107 +val thy = assoc_thy thy';
1.108 +val (is as ScrState (env,_,_,_,_,_), _, sc) = init_scrstate thy itms mI;
1.109 +(*dont take ctxt ^^^ from ^^^^^^^^^^^^^*)
1.110 +(*= the first part vvvvvvvvv works now =======================================*)
1.111 +val (pt, p) = case locatetac tac (pt'',p'') of
1.112 + ("ok", (_, _, ptp)) => ptp | _ => error "script.sml locatetac";
1.113 +val ctxt = get_ctxt pt p;
1.114 +val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
1.115 +(*= the first part ^^^^^^^^^^ works now =======================================*)
1.116 +val (pt'',p'') = (pt, p);
1.117 +"~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
1.118 +val pIopt = get_pblID (pt,ip);
1.119 +tacis; (*= []*)
1.120 +member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*)
1.121 +"~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
1.122 +val thy' = get_obj g_domID pt (par_pblobj pt p);
1.123 +val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
1.124 +"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt,(p,_)):ptree * pos'), (sc as Script (h $ body)),
1.125 + (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
1.126 +val ctxt = get_ctxt pt pos;
1.127 +val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
1.128 +(*= the first part ^^^^^^^^^^ works now =======================================*)
1.129 +l = [];
1.130 +appy thy ptp E [R] body NONE v;
1.131 +val (p,_,f,nxt,_,pt) = me nxt p'' [] pt''; (*nxt = Rewrite_Set_Inst isolate_bdv*);
1.132 *}
1.133 ML {*
1.134 *}
1.135 @@ -236,6 +248,41 @@
1.136 *}
1.137 ML {*
1.138 *}
1.139 +ML {*
1.140 +*}
1.141 +ML {*
1.142 +get_ctxt pt p |> is_e_ctxt; (*true ...?!?*)
1.143 +get_loc pt p |> snd |> is_e_ctxt; (*true ...?!?*)
1.144 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*);
1.145 +*}
1.146 +ML {*
1.147 +get_ctxt pt p |> is_e_ctxt; (*true ...?!?*)
1.148 +get_loc pt p |> snd |> is_e_ctxt; (*true ...?!?*)
1.149 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["linear","univariate", ...]) *);
1.150 +*}
1.151 +ML {*
1.152 +"~~~~~ fun me, args:"; val (_,tac) = nxt;
1.153 +val (pt, p) = case locatetac tac (pt,p) of
1.154 + ("ok", (_, _, ptp)) => ptp | _ => error "script.sml locatetac";
1.155 +show_pt pt; (*...(([3], Res), [x = 1])]... back in root, OK *)
1.156 +"~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
1.157 +val pIopt = get_pblID (pt,ip); (*= SOME ["sqroot-test", "univariate", ...]*)
1.158 +tacis; (*= []*)
1.159 +member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*)
1.160 +"~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
1.161 +val thy' = get_obj g_domID pt (par_pblobj pt p);
1.162 +val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*)
1.163 +"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt,(p,_)):ptree * pos'), (sc as Script (h $ body)),
1.164 + (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
1.165 +l; (*= [R, R, D, L, R]*)
1.166 +"~~~~~ dont like to go into nstep_up...";
1.167 +*}
1.168 +ML {*
1.169 +*}
1.170 +
1.171 +
1.172 +ML {*
1.173 +*}
1.174
1.175 end
1.176