1 (* Title: test/../script.sml
2 Author: Walther Neuper 050908
3 (c) copyright due to lincense terms.
5 "-----------------------------------------------------------------";
6 "table of contents -----------------------------------------------";
7 "-----------------------------------------------------------------";
8 "----------- WN0509 why does next_tac doesnt find Substitute -----";
9 "----------- WN0509 Substitute 2nd part --------------------------";
10 "----------- fun sel_appl_atomic_tacs ----------------------------";
11 "----------- fun init_form, fun get_stac -------------------------";
12 "----------- x+1=2 start SubProblem 'stac2tac_ TODO: no match for ";
13 "----------- Take as 1st stac in script --------------------------";
14 "----------- 'trace_script' from outside 'fun me '----------------";
15 "----------- fun sel_rules ---------------------------------------";
16 "----------- fun sel_appl_atomic_tacs ----------------------------";
17 "-----------------------------------------------------------------";
18 "-----------------------------------------------------------------";
19 "-----------------------------------------------------------------";
21 val thy = @{theory Isac};
23 "----------- WN0509 why does next_tac doesnt find Substitute -----";
24 "----------- WN0509 why does next_tac doesnt find Substitute -----";
25 "----------- WN0509 why does next_tac doesnt find Substitute -----";
27 (*replace met 'IntegrierenUndKonstanteBestimmen' with this script...*)
29 "Script BiegelinieScript " ^
30 "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
31 "(rb_rb::bool list) (rm_rm::bool list) = " ^
32 " (let q___q = Take (M_b v_v = q__q); " ^
33 " (M1__M1::bool) = ((Substitute [v_v = 0])) q___q " ^
36 val sc' = ((inst_abs thy) o Thm.term_of o the o (parse thy)) str;
39 "Script BiegelinieScript " ^
40 "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
41 "(rb_rb::bool list) (rm_rm::bool list) = " ^
42 " (M1__M1::bool) = ((Substitute [v_v = 0]) @@ " ^
43 " in True)";(*..doesnt find Substitute with ..@@ !!!!!!!!!!!!!!!!!!!!!*)
46 "Script BiegelinieScript " ^
47 "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
48 "(rb_rb::bool list) (rm_rm::bool list) = " ^
49 " (let q___q = Take (q_q v_v = q__q); " ^
50 " (M1__M1::bool) = Substitute [v_v = 0] q___q ; " ^
51 " M1__m1 = Substitute [M_b 0 = 0] M1__M1 " ^
55 "Script BiegelinieScript " ^
56 "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
57 "(rb_rb::bool list) (rm_rm::bool list) = " ^
58 " (let q___q = Take (q_q v_v = q__q); " ^
59 " (M1__M1::bool) = Substitute [v_v = 0] q___q ; " ^
60 " M1__M1 = Substitute [v_v = 1] q___q ; " ^
61 " M1__M1 = Substitute [v_v = 2] q___q ; " ^
62 " M1__M1 = Substitute [v_v = 3] q___q ; " ^
63 " M1__M1 = Substitute [M_b 0 = 0] M1__M1 " ^
67 "Script BiegelinieScript " ^
68 "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
69 "(rb_rb::bool list) (rm_rm::bool list) = " ^
70 " (let q___q = Take (M_b v_v = q__q); " ^
71 " (M1__M1::bool) = Substitute [v_v = 0] q___q ; " ^
72 " M2__M2 = Take q___q ; " ^
73 " M2__M2 = Substitute [v_v = 2] q___q " ^
77 val sc' = ((inst_abs thy) o Thm.term_of o the o (parse thy)) str;
80 val {scr = Prog sc,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
81 (*---------------------------------------------------------------------
82 if sc = sc' then () else error"script.sml, doesnt find Substitute #1";
83 ---------------------------------------------------------------------*)
85 "----------- WN0509 Substitute 2nd part --------------------------";
86 "----------- WN0509 Substitute 2nd part --------------------------";
87 "----------- WN0509 Substitute 2nd part --------------------------";
88 (*replace met 'IntegrierenUndKonstanteBestimmen' with this script...*)
89 val str = (*Substitute ; Substitute works*)
90 "Script BiegelinieScript " ^
91 "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
92 "(rb_rb::bool list) (rm_rm::bool list) = "^
93 (*begin after the 2nd integrate*)
94 " (let M__M = Take (M_b v_v = q__q); " ^
95 " e1__e1 = nth_nth 1 rm_rm ; " ^
96 " (x1__x1::real) = argument_in (lhs e1__e1); " ^
97 " (M1__M1::bool) = Substitute [v_v = x1__x1] M__M; " ^
98 " M1__M1 = Substitute [e1__e1] M1__M1 " ^
101 val sc' = ((inst_abs thy) o Thm.term_of o the o (parse thy)) str;
104 val str = (*Substitute @@ Substitute does NOT work???*)
105 "Script BiegelinieScript " ^
106 "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
107 "(rb_rb::bool list) (rm_rm::bool list) = "^
108 (*begin after the 2nd integrate*)
109 " (let M__M = Take (M_b v_v = q__q); " ^
110 " e1__e1 = nth_nth 1 rm_rm ; " ^
111 " (x1__x1::real) = argument_in (lhs e1__e1); " ^
112 " (M1__M1::bool) = ((Substitute [v_v = x1__x1]) @@ " ^
113 " (Substitute [e1__e1])) M__M " ^
117 val {scr = Prog sc,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
118 (*---------------------------------------------------------------------
119 if sc = sc' then () else error "script.sml, doesnt find Substitute #1";
120 ---------------------------------------------------------------------*)
121 val fmz = ["Traegerlaenge L",
122 "Streckenlast (- q_0 * x^^^2 / 2 + x * c + c_2)",
124 "RandbedingungenBiegung [y 0 = 0, y L = 0]",
125 "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
126 "FunktionsVariable x"];
128 ("Biegelinie",["MomentBestimmte","Biegelinien"],
129 ["IntegrierenUndKonstanteBestimmen"]);
130 val p = e_pos'; val c = [];
131 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
132 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
133 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
134 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
135 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
136 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
137 val (p,_,f,nxt,_,pt) = me nxt p c pt;
138 val (p,_,f,nxt,_,pt) = me nxt p c pt;
139 case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()
140 | _ => error "script.sml, doesnt find Substitute #2";
141 (* ERROR: caused by f2str f *)
142 trace_rewrite := false;
144 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f(*------------------------*);
145 trace_rewrite:=false;
146 (*Exception TYPE raised:
147 Illegal type for constant "HOL.eq" :: "[real, bool] => bool"
148 Atools.argument'_in (Tools.lhs (ListG.nth_ (1 + -1 + -1) [])) =
149 ListG.nth_ (1 + -1 + -1) []
152 ("Illegal type for constant \"op =\" :: \"[real, bool] => bool\"",
154 [Const ("HOL.Trueprop", "bool => prop") $
155 (Const ("HOL.eq", "["Real.real, bool] => bool") $ ... $ ...)])
157 ... this was because eval_argument_in took "argument_in (lhs (M_b 0 = 0))"
158 ie. the argument had not been simplified before ^^^^^^^^^^^^^^^
159 thus corrected eval_argument_in OK*)
160 val {srls,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
161 val e1__e1 = str2term "NTH 1 [M_b 0 = 0, M_b L = 0]";
162 val e1__e1 = eval_listexpr_ @{theory Biegelinie} srls e1__e1; term2str e1__e1;
163 if term2str e1__e1 = "M_b 0 = 0"
165 else error"script.sml diff.beh. eval_listexpr_ nth_nth 1 [...";
167 (*TODO.WN050913 ??? doesnt eval_listexpr_ go into subterms ???...
168 val x1__ = str2term"argument_in (lhs (M_b 0 = 0))";
169 val x1__ = eval_listexpr_ Biegelinie.thy srls x1__; term2str x1__;
171 calculate_ Biegelinie.thy ("Tools.lhs", eval_rhs"eval_lhs_") x1__;
172 val SOME (str, t) = eval_lhs 0 "Tools.lhs" (str2term"lhs (M_b 0 = 0)") 0;*)
174 val l__l = str2term "lhs (M_b 0 = 0)";
175 val l__l = eval_listexpr_ @{theory Biegelinie} srls l__l; term2str l__l;
176 val SOME (str, t) = eval_lhs 0 "Tools.lhs" (str2term "lhs (M_b 0 = 0)") 0;
178 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f (*------------------------*);
179 val thm = case nxt of ("Rewrite", Rewrite ("Belastung_Querkraft", thm)) => thm
180 | _ => error "--- WN0509 Substitute 2nd part --- changed 1";
181 if (term2str o Thm.prop_of) thm = "- qq ?x = Q' ?x" then ()
182 else error "--- WN0509 Substitute 2nd part --- changed 2";
185 "----------- fun sel_appl_atomic_tacs ----------------------------";
186 "----------- fun sel_appl_atomic_tacs ----------------------------";
187 "----------- fun sel_appl_atomic_tacs ----------------------------";
190 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
191 ("Test", ["sqroot-test","univariate","equation","test"],
192 ["Test","squ-equ-test-subpbl1"]))];
195 autoCalculate 1 CompleteCalcHead;
196 autoCalculate 1 (Step 1);
197 autoCalculate 1 (Step 1);
198 val ((pt, p), _) = get_calc 1; show_pt pt;
199 val appltacs = sel_appl_atomic_tacs pt p;
201 [Rewrite ("radd_commute", radd_commute),
202 Rewrite ("add_assoc", add_assoc), Calculate "TIMES"]
203 => if (term2str o Thm.prop_of) radd_commute = "?m + ?n = ?n + ?m" andalso
204 (term2str o Thm.prop_of) add_assoc = "?a + ?b + ?c = ?a + (?b + ?c)" then ()
205 else error "script.sml fun sel_appl_atomic_tacs diff.behav. 2"
206 | _ => error "script.sml fun sel_appl_atomic_tacs diff.behav. 1";
208 trace_script := true;
209 trace_script := false;
210 applyTactic 1 p (hd appltacs);
211 val ((pt, p), _) = get_calc 1; show_pt pt;
212 val appltacs = sel_appl_atomic_tacs pt p;
213 (*applyTactic 1 p (hd appltacs); WAS assy: call by ([3], Pbl)*)
215 "~~~~~ fun applyTactic, args:"; val ((cI:calcID), ip, tac) = (1, p, (hd appltacs));
216 val ((pt, _), _) = get_calc cI;
217 val p = get_pos cI 1;
221 (*locatetac tac (pt, ip); (*WAS assy: call by ([3], Pbl)*)*)
222 "~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, ip));
223 val (mI,m) = mk_tac'_ tac;
224 applicable_in p pt m ; (*Appl*)
225 member op = specsteps mI; (*false*)
226 (*loc_solve_ (mI,m) ptp; (*Argument: (mI, m) : string * tac Reason: Can't unify tac_ with tac*)*)
227 loc_solve_; (*without _ ??? result is -> lOc writing error ???*)
228 (*val it = fn: string * tac_ -> ptree * (pos * pos_) -> lOc_*)
229 (mI,m); (*string * tac*)
230 ptp (*ptree * pos'*);
231 "~~~~~ fun loc_solve_, args:"; val (m ,(pt,pos)) = ((mI,m), ptp);
232 (*val (msg, cs') = solve m (pt, pos);
233 (*Argument: m : string * tac Reason: Can't unify tac_ with tac (Different type constructors)*)*)
236 "~~~~~ fun solve, args:"; val ((mI,m), (pt, po as (p,p_))) = (m, (pt, pos));
237 (*solve has still p_!!!!!!!!!!!!!!!!!!!!!!!!!*)
239 e_metID = get_obj g_metID pt (par_pblobj pt p); (*false*)
240 val ctxt = get_ctxt pt po;
242 (*generate1 (assoc_thy (get_obj g_domID pt (par_pblobj pt p))) m (e_istate, ctxt) (p,p_) pt;
243 (*Argument: m : tac Reason: Can't unify tac_ with tac (Different type constructors)*)*)
244 (assoc_thy (get_obj g_domID pt (par_pblobj pt p)));
247 autoCalculate 1 CompleteCalc;
249 "----------- fun init_form, fun get_stac -------------------------";
250 "----------- fun init_form, fun get_stac -------------------------";
251 "----------- fun init_form, fun get_stac -------------------------";
252 val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
253 val (dI',pI',mI') = ("Test",["sqroot-test","univariate","equation","test"],
254 ["Test","squ-equ-test-subpbl1"]);
255 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
256 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
257 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
258 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
259 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
260 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
261 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
262 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
263 "~~~~~ fun me, args:"; val (_,tac) = nxt;
264 "~~~~~ fun locatetac, args:"; val ptp as (pt, p) = (pt, p);
265 val (mI,m) = mk_tac'_ tac;
266 val Appl m = applicable_in p pt m;
267 member op = specsteps mI; (*false*)
268 "~~~~~ fun loc_solve_, args:"; val (m, (pt, pos) ) = ((mI, m), ptp);
269 "~~~~~ fun solve, args:"; val (("Apply_Method", Apply_Method' (mI,_,_,_)), pos as (p,_)) = (m, pos);
270 val {srls, ...} = get_met mI;
271 val PblObj {meth=itms, ...} = get_obj I pt p;
272 val thy' = get_obj g_domID pt p;
273 val thy = assoc_thy thy';
274 val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI;
275 val ini = init_form thy sc env;
276 "----- fun init_form, args:"; val (Prog sc) = sc;
277 "----- fun get_stac, args:"; val (y, h $ body) = (thy, sc);
278 case get_stac thy sc of SOME (Free ("e_e", _)) => ()
279 | _ => error "script: Const (?, ?) in script (as term) changed";;
282 "----------- x+1=2 start SubProblem 'stac2tac_ TODO: no match for ";
283 "----------- x+1=2 start SubProblem 'stac2tac_ TODO: no match for ";
284 "----------- x+1=2 start SubProblem 'stac2tac_ TODO: no match for ";
285 val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
287 ("Test", ["sqroot-test","univariate","equation","test"],
288 ["Test","squ-equ-test-subpbl1"]);
289 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
290 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
291 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
292 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
293 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
294 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
295 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
296 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
297 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
298 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
299 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt; WAS: Empty_Tac, helpless*)
301 "~~~~~ fun me, args:"; val (_,tac) = nxt;
302 val (pt, p) = case locatetac tac (pt,p) of
303 ("ok", (_, _, ptp)) => ptp | _ => error "script.sml locatetac";
304 "~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
305 val pIopt = get_pblID (pt,ip); (*SOME ["LINEAR", "univariate", "equation", "test"]*)
307 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*)
308 "~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
309 (*WAS stac2tac_ TODO: no match for SubProblem*)
310 val thy' = get_obj g_domID pt (par_pblobj pt p);
311 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
312 "~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt,(p,_)):ptree * pos'), (sc as Prog (h $ body)),
313 (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
314 l; (*= [R, L, R, L, R, R]*)
315 val Appy (m', scrst as (_,_,_,v,_,_)) = nstep_up thy ptp sc E l Skip_ a v;
316 "~~~~~ dont like to go into nstep_up...";
317 val t = str2term ("SubProblem" ^
318 "(Test', [LINEAR, univariate, equation, test], [Test, solve_linear])" ^
319 "[BOOL (-1 + x = 0), REAL x]");
320 val (tac, tac_) = stac2tac_ pt @{theory "Isac"} t; (*WAS stac2tac_ TODO: no match for SubProblem*)
323 | _ => error "script.sml x+1=2 start SubProblem from script";
326 "----------- Take as 1st stac in script --------------------------";
327 "----------- Take as 1st stac in script --------------------------";
328 "----------- Take as 1st stac in script --------------------------";
329 val p = e_pos'; val c = [];
330 val (p,_,f,nxt,_,pt) =
332 [(["functionTerm (x^^^2 + 1)", "integrateBy x", "antiDerivative FF"],
333 ("Integrate", ["integrate","function"], ["diff","integration"]))];
334 val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = ("Tac ", ...) --> Add_Given...*)
335 val (p,_,f,nxt,_,pt) = me nxt p c pt;
336 val (p,_,f,nxt,_,pt) = me nxt p c pt;
337 val (p,_,f,nxt,_,pt) = me nxt p c pt;
338 val (p,_,f,nxt,_,pt) = me nxt p c pt;
339 val (p,_,f,nxt,_,pt) = me nxt p c pt;
340 val (p,_,f,nxt,_,pt) = me nxt p c pt;
341 case nxt of (_, Apply_Method ["diff", "integration"]) => ()
342 | _ => error "integrate.sml -- me method [diff,integration] -- spec";
343 "----- step 8: returns nxt = Rewrite_Set_Inst ([\"(bdv, x)\"],\"integration\")";
345 "~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ptree)) = (nxt, p, c, pt);
346 "~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
347 val (mI,m) = mk_tac'_ tac;
348 val Appl m = applicable_in p pt m;
349 member op = specsteps mI (*false*);
350 "~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = ((mI,m), ptp);
351 "~~~~~ fun solve, args:"; val ((_, m as Apply_Method' (mI, _, _, _)), (pt, (pos as (p,_)))) =
353 val {srls, ...} = get_met mI;
354 val PblObj {meth=itms, ...} = get_obj I pt p;
355 val thy' = get_obj g_domID pt p;
356 val thy = assoc_thy thy';
357 val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI;
358 val ini = init_form thy sc env;
361 val (m', (is', ctxt'), _) = next_tac (thy', srls) (pt, (p, Res)) sc (is, ctxt);
362 val d = e_rls (*FIXME: get simplifier from domID*);
363 "~~~~~ fun locate_gen, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ptree * pos'),
364 (scr as Prog (h $ body),d), (ScrState (E,l,a,v,S,b), ctxt)) =
365 ((thy',srls), m', (pt,(p, Res)), (sc,d), (is', ctxt'));
366 val thy = assoc_thy thy';
367 l = [] orelse ((*init.in solve..Apply_Method...*)
368 (last_elem o fst) p = 0 andalso snd p = Res); (*true*)
369 "~~~~~ fun assy, args:"; val (ya, (is as (E,l,a,v,S,b),ss),
370 (Const ("HOL.Let",_) $ e $ (Abs (id,T,body)))) =
371 ((thy',ctxt,srls,d,Aundef), ((E,[R],a,v,S,b), [(m,EmptyMout,pt,p,[])]), body);
372 (*check: true*) term2str e = "Take (Integral f_f D v_v)";
373 "~~~~~ fun assy, args:"; val ((thy',ctxt,sr,d,ap), (is as (E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss), t) =
374 (ya, ((E , l@[L,R], a,v,S,b),ss), e);
375 val (a', STac stac) = handle_leaf "locate" thy' sr E a v t;
376 (* val ctxt = get_ctxt pt (p,p_)
377 exception PTREE "get_obj: pos = [0] does not exist" raised
378 (line 908 of "/usr/local/isabisac/src/Tools/isac/Interpret/ctree.sml")*)
381 "----------- 'trace_script' from outside 'fun me '----------------";
382 "----------- 'trace_script' from outside 'fun me '----------------";
383 "----------- 'trace_script' from outside 'fun me '----------------";
384 val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
386 ("Test", ["sqroot-test","univariate","equation","test"],
387 ["Test","squ-equ-test-subpbl1"]);
388 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
389 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
390 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
391 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
392 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
393 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
394 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
395 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "squ-equ-test-subpbl1"]*)
396 (*from_pblobj_or_detail': no istate = from_pblobj_or_detail' "Isac" p pt;*)
398 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*---------------------------------------------------*)
399 val (p'''', pt'''') = (p, pt);
400 f2str f = "x + 1 = 2"; case snd nxt of Rewrite_Set "norm_equation" => () | _ => error "CHANGED";
401 val (p, p_) = p(* = ([1], Frm)*);
402 val (srls, (ScrState scrstate, ctxt), Prog sc) = from_pblobj_or_detail' "Isac" (p, p_) pt;
403 val (env, loc_, curry_arg, res, Safe, true) = scrstate;
404 env2str env = "[\"\n(e_e, x + 1 = 2)\",\"\n(v_v, x)\"]";
407 term2str res = "??.empty"; (* scrstate before starting interpretation *)
408 (*term2str (go loc_ sc) = "Prog Solve_root_equation e_e v_v = ...*)
410 val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*)
411 val (p'''', pt'''') = (p, pt);
412 f2str f = "x + 1 + -1 * 2 = 0";
413 case snd nxt of Rewrite_Set "Test_simplify" => () | _ => error "CHANGED";
414 val (p, p_) = p(* = ([1], Res)*);
415 val (srls, (ScrState scrstate, ctxt), Prog sc) = from_pblobj_or_detail' "Isac" (p, p_) pt;
416 val (env, loc_, curry_arg, res, Safe, true) = scrstate;
417 env2str env = "[\"\n(e_e, x + 1 = 2)\",\"\n(v_v, x)\"]";
418 loc_ = [R, L, R, L, L, R, R];
419 curry_arg = SOME (str2term "e_e::bool");
420 term2str res = "x + 1 + -1 * 2 = 0";(* scrstate after norm_equation, before Test_simplify *)
421 term2str (go loc_ sc) = "Rewrite_Set norm_equation False";
423 val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*)
424 val (p'''', pt'''') = (p, pt);
425 f2str f = "-1 + x = 0";
426 case snd nxt of Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]) => ()
427 | _ => error "CHANGED";
428 val (p, p_) = p(* = ([2], Res)*);
429 val (srls, (ScrState scrstate, ctxt), Prog sc) = from_pblobj_or_detail' "Isac" (p, p_) pt;
430 val (env, loc_, curry_arg, res, Safe, false) = scrstate;
431 env2str env = "[\"\n(e_e, x + 1 = 2)\",\"\n(v_v, x)\"]";
432 loc_ = [R, L, R, L, R, R];
433 curry_arg = SOME (str2term "e_e::bool");
434 term2str res = "-1 + x = 0"; (* scrstate after Test_simplify, before Subproblem *)
435 term2str (go loc_ sc) = "Rewrite_Set Test_simplify False";
437 val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*)
438 val (p'''', pt'''') = (p, pt); (*f2str f = exception Match; ...is a model, not a formula*)
439 val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*)
440 val (p'''', pt'''') = (p, pt);
441 val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*)
442 val (p'''', pt'''') = (p, pt);
443 val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*)
444 val (p'''', pt'''') = (p, pt);
445 val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*)
446 val (p'''', pt'''') = (p, pt);
447 val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*)
448 val (p'''', pt'''') = (p, pt);
449 val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*)
450 val (p'''', pt'''') = (p, pt);
451 val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*nxt = Apply_Method ["Test", "solve_linear"]*)
452 (*from_pblobj_or_detail': no istate = from_pblobj_or_detail' "Isac" p pt;*)
454 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*---------------------------------------------------*)
455 val (p'''', pt'''') = (p, pt);
456 f2str f = "-1 + x = 0";
457 case snd nxt of Rewrite_Set_Inst (["(bdv, x)"], "isolate_bdv") => () | _ => error "CHANGED";
458 val (p, p_) = p(* = ([3, 1], Frm)*);
459 val (srls, (ScrState scrstate, ctxt), Prog sc) = from_pblobj_or_detail' "Isac" (p, p_) pt;
460 val (env, loc_, curry_arg, res, Safe, true) = scrstate;
461 env2str env = "[\"\n(e_e, -1 + x = 0)\",\"\n(v_v, x)\"]";
464 term2str res = "??.empty"; (* scrstate before starting interpretation *)
465 (*term2str (go loc_ sc) = "Prog Solve_linear e_e v_v = ...*)
467 val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*)
468 val (p'''', pt'''') = (p, pt);
469 f2str f = "x = 0 + -1 * -1";
470 case snd nxt of Rewrite_Set "Test_simplify" => () | _ => error "CHANGED";
471 val (p, p_) = p(* = ([3, 1], Res)*);
472 val (srls, (ScrState scrstate, ctxt), Prog sc) = from_pblobj_or_detail' "Isac" (p, p_) pt;
473 val (env, loc_, curry_arg, res, Safe, true) = scrstate;
474 env2str env = "[\"\n(e_e, -1 + x = 0)\",\"\n(v_v, x)\"]";
475 loc_ = [R, L, R, L, R, L, R];
476 curry_arg = SOME (str2term "e_e::bool");
477 term2str res = "x = 0 + -1 * -1";(* scrstate after isolate_bdv, before Test_simplify *)
478 term2str (go loc_ sc) = "Rewrite_Set_Inst [(bdv, v_v)] isolate_bdv False";
480 "----------- fun sel_rules ---------------------------------------";
481 "----------- fun sel_rules ---------------------------------------";
482 "----------- fun sel_rules ---------------------------------------";
483 (* compare test/../interface.sml
484 "--------- getTactic, fetchApplicableTactics ------------";
487 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
488 ("Test", ["sqroot-test","univariate","equation","test"],
489 ["Test","squ-equ-test-subpbl1"]))];
492 autoCalculate 1 CompleteCalc;
493 val ((pt,_),_) = get_calc 1;
496 (*UC\label{SOLVE:MANUAL:TACTIC:listall} UC 30.3.2.2 p.175*)
497 val tacs = sel_rules pt ([],Pbl);
498 case tacs of [Apply_Method ["Test", "squ-equ-test-subpbl1"]] => ()
499 | _ => error "script.sml: diff.behav. in sel_rules ([],Pbl)";
501 val tacs = sel_rules pt ([1],Res);
502 case tacs of [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",
503 Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]),
504 Check_elementwise "Assumptions"] => ()
505 | _ => error "script.sml: diff.behav. in sel_rules ([1],Res)";
507 val tacs = sel_rules pt ([3],Pbl);
508 case tacs of [Apply_Method ["Test", "solve_linear"]] => ()
509 | _ => error "script.sml: diff.behav. in sel_rules ([3],Pbl)";
511 val tacs = sel_rules pt ([3,1],Res);
512 case tacs of [Rewrite_Set_Inst (["(bdv, x)"], "isolate_bdv"), Rewrite_Set "Test_simplify"] => ()
513 | _ => error "script.sml: diff.behav. in sel_rules ([3,1],Res)";
515 val tacs = sel_rules pt ([3],Res);
516 case tacs of [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",
517 Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]),
518 Check_elementwise "Assumptions"] => ()
519 | _ => error "script.sml: diff.behav. in sel_rules ([3],Res)";
521 val tacs = (sel_rules pt ([],Res)) handle PTREE str => [Tac str];
522 case tacs of [Tac "no tactics applicable at the end of a calculation"] => ()
523 | _ => error "script.sml: diff.behav. in sel_rules ([],Res)";
525 "----------- fun sel_appl_atomic_tacs ----------------------------";
526 "----------- fun sel_appl_atomic_tacs ----------------------------";
527 "----------- fun sel_appl_atomic_tacs ----------------------------";
529 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
530 ("Test", ["sqroot-test","univariate","equation","test"],
531 ["Test","squ-equ-test-subpbl1"]))];
534 autoCalculate 1 CompleteCalc;
536 (*UC\label{SOLVE:MANUAL:TACTIC:listall} UC 30.3.2.2 p.175*)
537 fetchApplicableTactics 1 99999 ([],Pbl);
539 fetchApplicableTactics 1 99999 ([1],Res);
540 "~~~~~ fun fetchApplicableTactics, args:"; val (cI, (scope:int), (p:pos')) = (1, 99999, ([1],Res));
541 val ((pt, _), _) = get_calc cI;
543 case sel_rules pt p of [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",
544 Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]),
545 Check_elementwise "Assumptions"] => ()
546 | _ => error "fetchApplicableTactics ([1],Res) changed";
549 sel_appl_atomic_tacs pt p;
551 ### atomic_appl_tacs: not impl. for tac='Subproblem(Test,["LINEAR","univariate","equation","test"])'
552 ### atomic_appl_tacs: not impl. for tac = 'Check_elementwise "Assumptions"'
555 "~~~~~ fun sel_appl_atomic_tacs, args:"; val (pt, (p,p_)) = (pt, p);
556 is_spec_pos p_ = false;
557 val pp = par_pblobj pt p
558 val thy' = (get_obj g_domID pt pp):theory'
559 val thy = assoc_thy thy'
560 val metID = get_obj g_metID pt pp
563 then (thd3 o snd3) (get_obj g_origin pt pp)
565 val {scr=Prog sc,srls,erls,rew_ord'=ro,...} = get_met metID'
566 val ScrState (env,_,a,v,_,_) = get_istate pt (p,p_)
567 val alltacs = (*we expect at least 1 stac in a script*)
568 map ((stac2tac pt thy) o rep_stacexpr o #2 o
569 (handle_leaf "selrul" thy' srls env a v)) (stacpbls sc)
572 Frm => get_obj g_form pt p
573 | Res => (fst o (get_obj g_result pt)) p
574 (*WN120611 stopped and took version 1 again for fetchApplicableTactics !
575 (distinct o flat o (map (atomic_appl_tacs thy ro erls f))) alltacs
577 ### atomic_appl_tacs: not impl. for tac='Subproblem(Test,["LINEAR","univariate","equation","test"])'
578 ### atomic_appl_tacs: not impl. for tac = 'Check_elementwise "Assumptions"'