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 "----------- fun de_esc_underscore -------------------------------";
18 "----------- fun go ----------------------------------------------";
19 "----------- fun formal_args -------------------------------------";
20 "----------- fun dsc_valT ----------------------------------------";
21 "----------- fun itms2args ---------------------------------------";
22 "----------- fun rep_tac_ ----------------------------------------";
23 "-----------------------------------------------------------------";
24 "-----------------------------------------------------------------";
25 "-----------------------------------------------------------------";
27 val thy = @{theory Isac};
29 "----------- WN0509 why does next_tac doesnt find Substitute -----";
30 "----------- WN0509 why does next_tac doesnt find Substitute -----";
31 "----------- WN0509 why does next_tac doesnt find Substitute -----";
33 (*replace met 'IntegrierenUndKonstanteBestimmen' with this script...*)
35 "Script BiegelinieScript " ^
36 "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
37 "(rb_rb::bool list) (rm_rm::bool list) = " ^
38 " (let q___q = Take (M_b v_v = q__q); " ^
39 " (M1__M1::bool) = ((Substitute [v_v = 0])) q___q " ^
42 val sc' = ((inst_abs thy) o Thm.term_of o the o (parse thy)) str;
45 "Script BiegelinieScript " ^
46 "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
47 "(rb_rb::bool list) (rm_rm::bool list) = " ^
48 " (M1__M1::bool) = ((Substitute [v_v = 0]) @@ " ^
49 " in True)";(*..doesnt find Substitute with ..@@ !!!!!!!!!!!!!!!!!!!!!*)
52 "Script BiegelinieScript " ^
53 "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
54 "(rb_rb::bool list) (rm_rm::bool list) = " ^
55 " (let q___q = Take (q_q v_v = q__q); " ^
56 " (M1__M1::bool) = Substitute [v_v = 0] q___q ; " ^
57 " M1__m1 = Substitute [M_b 0 = 0] M1__M1 " ^
61 "Script BiegelinieScript " ^
62 "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
63 "(rb_rb::bool list) (rm_rm::bool list) = " ^
64 " (let q___q = Take (q_q v_v = q__q); " ^
65 " (M1__M1::bool) = Substitute [v_v = 0] q___q ; " ^
66 " M1__M1 = Substitute [v_v = 1] q___q ; " ^
67 " M1__M1 = Substitute [v_v = 2] q___q ; " ^
68 " M1__M1 = Substitute [v_v = 3] q___q ; " ^
69 " M1__M1 = Substitute [M_b 0 = 0] M1__M1 " ^
73 "Script BiegelinieScript " ^
74 "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
75 "(rb_rb::bool list) (rm_rm::bool list) = " ^
76 " (let q___q = Take (M_b v_v = q__q); " ^
77 " (M1__M1::bool) = Substitute [v_v = 0] q___q ; " ^
78 " M2__M2 = Take q___q ; " ^
79 " M2__M2 = Substitute [v_v = 2] q___q " ^
83 val sc' = ((inst_abs thy) o Thm.term_of o the o (parse thy)) str;
86 val {scr = Prog sc,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
87 (*---------------------------------------------------------------------
88 if sc = sc' then () else error"script.sml, doesnt find Substitute #1";
89 ---------------------------------------------------------------------*)
91 "----------- WN0509 Substitute 2nd part --------------------------";
92 "----------- WN0509 Substitute 2nd part --------------------------";
93 "----------- WN0509 Substitute 2nd part --------------------------";
94 (*replace met 'IntegrierenUndKonstanteBestimmen' with this script...*)
95 val str = (*Substitute ; Substitute works*)
96 "Script BiegelinieScript " ^
97 "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
98 "(rb_rb::bool list) (rm_rm::bool list) = "^
99 (*begin after the 2nd integrate*)
100 " (let M__M = Take (M_b v_v = q__q); " ^
101 " e1__e1 = nth_nth 1 rm_rm ; " ^
102 " (x1__x1::real) = argument_in (lhs e1__e1); " ^
103 " (M1__M1::bool) = Substitute [v_v = x1__x1] M__M; " ^
104 " M1__M1 = Substitute [e1__e1] M1__M1 " ^
107 val sc' = ((inst_abs thy) o Thm.term_of o the o (parse thy)) str;
110 val str = (*Substitute @@ Substitute does NOT work???*)
111 "Script BiegelinieScript " ^
112 "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
113 "(rb_rb::bool list) (rm_rm::bool list) = "^
114 (*begin after the 2nd integrate*)
115 " (let M__M = Take (M_b v_v = q__q); " ^
116 " e1__e1 = nth_nth 1 rm_rm ; " ^
117 " (x1__x1::real) = argument_in (lhs e1__e1); " ^
118 " (M1__M1::bool) = ((Substitute [v_v = x1__x1]) @@ " ^
119 " (Substitute [e1__e1])) M__M " ^
123 val {scr = Prog sc,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
124 (*---------------------------------------------------------------------
125 if sc = sc' then () else error "script.sml, doesnt find Substitute #1";
126 ---------------------------------------------------------------------*)
127 val fmz = ["Traegerlaenge L",
128 "Streckenlast (- q_0 * x^^^2 / 2 + x * c + c_2)",
130 "RandbedingungenBiegung [y 0 = 0, y L = 0]",
131 "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
132 "FunktionsVariable x"];
134 ("Biegelinie",["MomentBestimmte","Biegelinien"],
135 ["IntegrierenUndKonstanteBestimmen"]);
136 val p = e_pos'; val c = [];
137 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
138 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
139 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
140 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
141 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
142 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
143 val (p,_,f,nxt,_,pt) = me nxt p c pt;
144 val (p,_,f,nxt,_,pt) = me nxt p c pt;
145 case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()
146 | _ => error "script.sml, doesnt find Substitute #2";
147 (* ERROR: caused by f2str f *)
148 trace_rewrite := false;
150 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f(*------------------------*);
151 trace_rewrite:=false;
152 (*Exception TYPE raised:
153 Illegal type for constant "HOL.eq" :: "[real, bool] => bool"
154 Atools.argument'_in (Tools.lhs (ListG.nth_ (1 + -1 + -1) [])) =
155 ListG.nth_ (1 + -1 + -1) []
158 ("Illegal type for constant \"op =\" :: \"[real, bool] => bool\"",
160 [Const ("HOL.Trueprop", "bool => prop") $
161 (Const ("HOL.eq", "["Real.real, bool] => bool") $ ... $ ...)])
163 ... this was because eval_argument_in took "argument_in (lhs (M_b 0 = 0))"
164 ie. the argument had not been simplified before ^^^^^^^^^^^^^^^
165 thus corrected eval_argument_in OK*)
166 val {srls,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
167 val e1__e1 = str2term "NTH 1 [M_b 0 = 0, M_b L = 0]";
168 val e1__e1 = eval_listexpr_ @{theory Biegelinie} srls e1__e1; term2str e1__e1;
169 if term2str e1__e1 = "M_b 0 = 0"
171 else error"script.sml diff.beh. eval_listexpr_ nth_nth 1 [...";
173 (*TODO.WN050913 ??? doesnt eval_listexpr_ go into subterms ???...
174 val x1__ = str2term"argument_in (lhs (M_b 0 = 0))";
175 val x1__ = eval_listexpr_ Biegelinie.thy srls x1__; term2str x1__;
177 calculate_ Biegelinie.thy ("Tools.lhs", eval_rhs"eval_lhs_") x1__;
178 val SOME (str, t) = eval_lhs 0 "Tools.lhs" (str2term"lhs (M_b 0 = 0)") 0;*)
180 val l__l = str2term "lhs (M_b 0 = 0)";
181 val l__l = eval_listexpr_ @{theory Biegelinie} srls l__l; term2str l__l;
182 val SOME (str, t) = eval_lhs 0 "Tools.lhs" (str2term "lhs (M_b 0 = 0)") 0;
184 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f (*------------------------*);
185 val thm = case nxt of ("Rewrite", Rewrite ("Belastung_Querkraft", thm)) => thm
186 | _ => error "--- WN0509 Substitute 2nd part --- changed 1";
187 if (term2str o Thm.prop_of) thm = "- qq ?x = Q' ?x" then ()
188 else error "--- WN0509 Substitute 2nd part --- changed 2";
191 "----------- fun sel_appl_atomic_tacs ----------------------------";
192 "----------- fun sel_appl_atomic_tacs ----------------------------";
193 "----------- fun sel_appl_atomic_tacs ----------------------------";
196 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
197 ("Test", ["sqroot-test","univariate","equation","test"],
198 ["Test","squ-equ-test-subpbl1"]))];
201 autoCalculate 1 CompleteCalcHead;
202 autoCalculate 1 (Step 1);
203 autoCalculate 1 (Step 1);
204 val ((pt, p), _) = get_calc 1; show_pt pt;
205 val appltacs = sel_appl_atomic_tacs pt p;
207 [Rewrite ("radd_commute", radd_commute),
208 Rewrite ("add_assoc", add_assoc), Calculate "TIMES"]
209 => if (term2str o Thm.prop_of) radd_commute = "?m + ?n = ?n + ?m" andalso
210 (term2str o Thm.prop_of) add_assoc = "?a + ?b + ?c = ?a + (?b + ?c)" then ()
211 else error "script.sml fun sel_appl_atomic_tacs diff.behav. 2"
212 | _ => error "script.sml fun sel_appl_atomic_tacs diff.behav. 1";
214 trace_script := true;
215 trace_script := false;
216 applyTactic 1 p (hd appltacs);
217 val ((pt, p), _) = get_calc 1; show_pt pt;
218 val appltacs = sel_appl_atomic_tacs pt p;
219 (*applyTactic 1 p (hd appltacs); WAS assy: call by ([3], Pbl)*)
221 "~~~~~ fun applyTactic, args:"; val ((cI:calcID), ip, tac) = (1, p, (hd appltacs));
222 val ((pt, _), _) = get_calc cI;
223 val p = get_pos cI 1;
227 (*locatetac tac (pt, ip); (*WAS assy: call by ([3], Pbl)*)*)
228 "~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, ip));
229 val (mI,m) = mk_tac'_ tac;
230 applicable_in p pt m ; (*Appl*)
231 member op = specsteps mI; (*false*)
232 (*loc_solve_ (mI,m) ptp; (*Argument: (mI, m) : string * tac Reason: Can't unify tac_ with tac*)*)
233 loc_solve_; (*without _ ??? result is -> lOc writing error ???*)
234 (*val it = fn: string * tac_ -> ptree * (pos * pos_) -> lOc_*)
235 (mI,m); (*string * tac*)
236 ptp (*ptree * pos'*);
237 "~~~~~ fun loc_solve_, args:"; val (m ,(pt,pos)) = ((mI,m), ptp);
238 (*val (msg, cs') = solve m (pt, pos);
239 (*Argument: m : string * tac Reason: Can't unify tac_ with tac (Different type constructors)*)*)
242 "~~~~~ fun solve, args:"; val ((mI,m), (pt, po as (p,p_))) = (m, (pt, pos));
243 (*solve has still p_!!!!!!!!!!!!!!!!!!!!!!!!!*)
245 e_metID = get_obj g_metID pt (par_pblobj pt p); (*false*)
246 val ctxt = get_ctxt pt po;
248 (*generate1 (assoc_thy (get_obj g_domID pt (par_pblobj pt p))) m (e_istate, ctxt) (p,p_) pt;
249 (*Argument: m : tac Reason: Can't unify tac_ with tac (Different type constructors)*)*)
250 (assoc_thy (get_obj g_domID pt (par_pblobj pt p)));
253 autoCalculate 1 CompleteCalc;
255 "----------- fun init_form, fun get_stac -------------------------";
256 "----------- fun init_form, fun get_stac -------------------------";
257 "----------- fun init_form, fun get_stac -------------------------";
258 val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
259 val (dI',pI',mI') = ("Test",["sqroot-test","univariate","equation","test"],
260 ["Test","squ-equ-test-subpbl1"]);
261 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
262 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
263 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
264 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
265 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
266 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
267 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
268 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
269 "~~~~~ fun me, args:"; val (_,tac) = nxt;
270 "~~~~~ fun locatetac, args:"; val ptp as (pt, p) = (pt, p);
271 val (mI,m) = mk_tac'_ tac;
272 val Appl m = applicable_in p pt m;
273 member op = specsteps mI; (*false*)
274 "~~~~~ fun loc_solve_, args:"; val (m, (pt, pos) ) = ((mI, m), ptp);
275 "~~~~~ fun solve, args:"; val (("Apply_Method", Apply_Method' (mI,_,_,_)), pos as (p,_)) = (m, pos);
276 val {srls, ...} = get_met mI;
277 val PblObj {meth=itms, ...} = get_obj I pt p;
278 val thy' = get_obj g_domID pt p;
279 val thy = assoc_thy thy';
280 val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI;
281 val ini = init_form thy sc env;
282 "----- fun init_form, args:"; val (Prog sc) = sc;
283 "----- fun get_stac, args:"; val (y, h $ body) = (thy, sc);
284 case get_stac thy sc of SOME (Free ("e_e", _)) => ()
285 | _ => error "script: Const (?, ?) in script (as term) changed";;
288 "----------- x+1=2 start SubProblem 'stac2tac_ TODO: no match for ";
289 "----------- x+1=2 start SubProblem 'stac2tac_ TODO: no match for ";
290 "----------- x+1=2 start SubProblem 'stac2tac_ TODO: no match for ";
291 val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
293 ("Test", ["sqroot-test","univariate","equation","test"],
294 ["Test","squ-equ-test-subpbl1"]);
295 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
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;
300 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
301 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
302 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
303 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
304 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
305 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt; WAS: Empty_Tac, helpless*)
307 "~~~~~ fun me, args:"; val (_,tac) = nxt;
308 val (pt, p) = case locatetac tac (pt,p) of
309 ("ok", (_, _, ptp)) => ptp | _ => error "script.sml locatetac";
310 "~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
311 val pIopt = get_pblID (pt,ip); (*SOME ["LINEAR", "univariate", "equation", "test"]*)
313 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*)
314 "~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
315 (*WAS stac2tac_ TODO: no match for SubProblem*)
316 val thy' = get_obj g_domID pt (par_pblobj pt p);
317 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
318 "~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt,(p,_)):ptree * pos'), (sc as Prog (h $ body)),
319 (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
320 l; (*= [R, L, R, L, R, R]*)
321 val Appy (m', scrst as (_,_,_,v,_,_)) = nstep_up thy ptp sc E l Skip_ a v;
322 "~~~~~ dont like to go into nstep_up...";
323 val t = str2term ("SubProblem" ^
324 "(Test', [LINEAR, univariate, equation, test], [Test, solve_linear])" ^
325 "[BOOL (-1 + x = 0), REAL x]");
326 val (tac, tac_) = stac2tac_ pt @{theory "Isac"} t; (*WAS stac2tac_ TODO: no match for SubProblem*)
329 | _ => error "script.sml x+1=2 start SubProblem from script";
332 "----------- Take as 1st stac in script --------------------------";
333 "----------- Take as 1st stac in script --------------------------";
334 "----------- Take as 1st stac in script --------------------------";
335 val p = e_pos'; val c = [];
336 val (p,_,f,nxt,_,pt) =
338 [(["functionTerm (x^^^2 + 1)", "integrateBy x", "antiDerivative FF"],
339 ("Integrate", ["integrate","function"], ["diff","integration"]))];
340 val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = ("Tac ", ...) --> Add_Given...*)
341 val (p,_,f,nxt,_,pt) = me nxt p c pt;
342 val (p,_,f,nxt,_,pt) = me nxt p c pt;
343 val (p,_,f,nxt,_,pt) = me nxt p c pt;
344 val (p,_,f,nxt,_,pt) = me nxt p c pt;
345 val (p,_,f,nxt,_,pt) = me nxt p c pt;
346 val (p,_,f,nxt,_,pt) = me nxt p c pt;
347 case nxt of (_, Apply_Method ["diff", "integration"]) => ()
348 | _ => error "integrate.sml -- me method [diff,integration] -- spec";
349 "----- step 8: returns nxt = Rewrite_Set_Inst ([\"(bdv, x)\"],\"integration\")";
351 "~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ptree)) = (nxt, p, c, pt);
352 "~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
353 val (mI,m) = mk_tac'_ tac;
354 val Appl m = applicable_in p pt m;
355 member op = specsteps mI (*false*);
356 "~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = ((mI,m), ptp);
357 "~~~~~ fun solve, args:"; val ((_, m as Apply_Method' (mI, _, _, _)), (pt, (pos as (p,_)))) =
359 val {srls, ...} = get_met mI;
360 val PblObj {meth=itms, ...} = get_obj I pt p;
361 val thy' = get_obj g_domID pt p;
362 val thy = assoc_thy thy';
363 val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI;
364 val ini = init_form thy sc env;
367 val (m', (is', ctxt'), _) = next_tac (thy', srls) (pt, (p, Res)) sc (is, ctxt);
368 val d = e_rls (*FIXME: get simplifier from domID*);
369 "~~~~~ fun locate_gen, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ptree * pos'),
370 (scr as Prog (h $ body),d), (ScrState (E,l,a,v,S,b), ctxt)) =
371 ((thy',srls), m', (pt,(p, Res)), (sc,d), (is', ctxt'));
372 val thy = assoc_thy thy';
373 l = [] orelse ((*init.in solve..Apply_Method...*)
374 (last_elem o fst) p = 0 andalso snd p = Res); (*true*)
375 "~~~~~ fun assy, args:"; val (ya, (is as (E,l,a,v,S,b),ss),
376 (Const ("HOL.Let",_) $ e $ (Abs (id,T,body)))) =
377 ((thy',ctxt,srls,d,Aundef), ((E,[R],a,v,S,b), [(m,EmptyMout,pt,p,[])]), body);
378 (*check: true*) term2str e = "Take (Integral f_f D v_v)";
379 "~~~~~ fun assy, args:"; val ((thy',ctxt,sr,d,ap), (is as (E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss), t) =
380 (ya, ((E , l@[L,R], a,v,S,b),ss), e);
381 val (a', STac stac) = handle_leaf "locate" thy' sr E a v t;
382 (* val ctxt = get_ctxt pt (p,p_)
383 exception PTREE "get_obj: pos = [0] does not exist" raised
384 (line 908 of "/usr/local/isabisac/src/Tools/isac/Interpret/ctree.sml")*)
387 "----------- 'trace_script' from outside 'fun me '----------------";
388 "----------- 'trace_script' from outside 'fun me '----------------";
389 "----------- 'trace_script' from outside 'fun me '----------------";
390 val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
392 ("Test", ["sqroot-test","univariate","equation","test"],
393 ["Test","squ-equ-test-subpbl1"]);
394 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
395 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
396 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
397 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
398 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
399 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
400 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
401 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "squ-equ-test-subpbl1"]*)
402 (*from_pblobj_or_detail': no istate = from_pblobj_or_detail' "Isac" p pt;*)
404 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*---------------------------------------------------*)
405 val (p'''', pt'''') = (p, pt);
406 f2str f = "x + 1 = 2"; case snd nxt of Rewrite_Set "norm_equation" => () | _ => error "CHANGED";
407 val (p, p_) = p(* = ([1], Frm)*);
408 val (srls, (ScrState scrstate, ctxt), Prog sc) = from_pblobj_or_detail' "Isac" (p, p_) pt;
409 val (env, loc_, curry_arg, res, Safe, true) = scrstate;
410 env2str env = "[\"\n(e_e, x + 1 = 2)\",\"\n(v_v, x)\"]";
413 term2str res = "??.empty"; (* scrstate before starting interpretation *)
414 (*term2str (go loc_ sc) = "Prog Solve_root_equation e_e v_v = ...*)
416 val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*)
417 val (p'''', pt'''') = (p, pt);
418 f2str f = "x + 1 + -1 * 2 = 0";
419 case snd nxt of Rewrite_Set "Test_simplify" => () | _ => error "CHANGED";
420 val (p, p_) = p(* = ([1], Res)*);
421 val (srls, (ScrState scrstate, ctxt), Prog sc) = from_pblobj_or_detail' "Isac" (p, p_) pt;
422 val (env, loc_, curry_arg, res, Safe, true) = scrstate;
423 env2str env = "[\"\n(e_e, x + 1 = 2)\",\"\n(v_v, x)\"]";
424 loc_ = [R, L, R, L, L, R, R];
425 curry_arg = SOME (str2term "e_e::bool");
426 term2str res = "x + 1 + -1 * 2 = 0";(* scrstate after norm_equation, before Test_simplify *)
427 term2str (go loc_ sc) = "Rewrite_Set norm_equation False";
429 val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*)
430 val (p'''', pt'''') = (p, pt);
431 f2str f = "-1 + x = 0";
432 case snd nxt of Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]) => ()
433 | _ => error "CHANGED";
434 val (p, p_) = p(* = ([2], Res)*);
435 val (srls, (ScrState scrstate, ctxt), Prog sc) = from_pblobj_or_detail' "Isac" (p, p_) pt;
436 val (env, loc_, curry_arg, res, Safe, false) = scrstate;
437 env2str env = "[\"\n(e_e, x + 1 = 2)\",\"\n(v_v, x)\"]";
438 loc_ = [R, L, R, L, R, R];
439 curry_arg = SOME (str2term "e_e::bool");
440 term2str res = "-1 + x = 0"; (* scrstate after Test_simplify, before Subproblem *)
441 term2str (go loc_ sc) = "Rewrite_Set Test_simplify False";
443 val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*)
444 val (p'''', pt'''') = (p, pt); (*f2str f = exception Match; ...is a model, not a formula*)
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''''; (*-------------------------------------------*)
452 val (p'''', pt'''') = (p, pt);
453 val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*)
454 val (p'''', pt'''') = (p, pt);
455 val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*)
456 val (p'''', pt'''') = (p, pt);
457 val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*nxt = Apply_Method ["Test", "solve_linear"]*)
458 (*from_pblobj_or_detail': no istate = from_pblobj_or_detail' "Isac" p pt;*)
460 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*---------------------------------------------------*)
461 val (p'''', pt'''') = (p, pt);
462 f2str f = "-1 + x = 0";
463 case snd nxt of Rewrite_Set_Inst (["(bdv, x)"], "isolate_bdv") => () | _ => error "CHANGED";
464 val (p, p_) = p(* = ([3, 1], Frm)*);
465 val (srls, (ScrState scrstate, ctxt), Prog sc) = from_pblobj_or_detail' "Isac" (p, p_) pt;
466 val (env, loc_, curry_arg, res, Safe, true) = scrstate;
467 env2str env = "[\"\n(e_e, -1 + x = 0)\",\"\n(v_v, x)\"]";
470 term2str res = "??.empty"; (* scrstate before starting interpretation *)
471 (*term2str (go loc_ sc) = "Prog Solve_linear e_e v_v = ...*)
473 val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*)
474 val (p'''', pt'''') = (p, pt);
475 f2str f = "x = 0 + -1 * -1";
476 case snd nxt of Rewrite_Set "Test_simplify" => () | _ => error "CHANGED";
477 val (p, p_) = p(* = ([3, 1], Res)*);
478 val (srls, (ScrState scrstate, ctxt), Prog sc) = from_pblobj_or_detail' "Isac" (p, p_) pt;
479 val (env, loc_, curry_arg, res, Safe, true) = scrstate;
480 env2str env = "[\"\n(e_e, -1 + x = 0)\",\"\n(v_v, x)\"]";
481 loc_ = [R, L, R, L, R, L, R];
482 curry_arg = SOME (str2term "e_e::bool");
483 term2str res = "x = 0 + -1 * -1";(* scrstate after isolate_bdv, before Test_simplify *)
484 term2str (go loc_ sc) = "Rewrite_Set_Inst [(bdv, v_v)] isolate_bdv False";
486 "----------- fun sel_rules ---------------------------------------";
487 "----------- fun sel_rules ---------------------------------------";
488 "----------- fun sel_rules ---------------------------------------";
489 (* compare test/../interface.sml
490 "--------- getTactic, fetchApplicableTactics ------------";
493 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
494 ("Test", ["sqroot-test","univariate","equation","test"],
495 ["Test","squ-equ-test-subpbl1"]))];
498 autoCalculate 1 CompleteCalc;
499 val ((pt,_),_) = get_calc 1;
502 (*UC\label{SOLVE:MANUAL:TACTIC:listall} UC 30.3.2.2 p.175*)
503 val tacs = sel_rules pt ([],Pbl);
504 case tacs of [Apply_Method ["Test", "squ-equ-test-subpbl1"]] => ()
505 | _ => error "script.sml: diff.behav. in sel_rules ([],Pbl)";
507 val tacs = sel_rules pt ([1],Res);
508 case tacs of [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",
509 Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]),
510 Check_elementwise "Assumptions"] => ()
511 | _ => error "script.sml: diff.behav. in sel_rules ([1],Res)";
513 val tacs = sel_rules pt ([3],Pbl);
514 case tacs of [Apply_Method ["Test", "solve_linear"]] => ()
515 | _ => error "script.sml: diff.behav. in sel_rules ([3],Pbl)";
517 val tacs = sel_rules pt ([3,1],Res);
518 case tacs of [Rewrite_Set_Inst (["(bdv, x)"], "isolate_bdv"), Rewrite_Set "Test_simplify"] => ()
519 | _ => error "script.sml: diff.behav. in sel_rules ([3,1],Res)";
521 val tacs = sel_rules pt ([3],Res);
522 case tacs of [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",
523 Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]),
524 Check_elementwise "Assumptions"] => ()
525 | _ => error "script.sml: diff.behav. in sel_rules ([3],Res)";
527 val tacs = (sel_rules pt ([],Res)) handle PTREE str => [Tac str];
528 case tacs of [Tac "no tactics applicable at the end of a calculation"] => ()
529 | _ => error "script.sml: diff.behav. in sel_rules ([],Res)";
531 "----------- fun sel_appl_atomic_tacs ----------------------------";
532 "----------- fun sel_appl_atomic_tacs ----------------------------";
533 "----------- fun sel_appl_atomic_tacs ----------------------------";
535 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
536 ("Test", ["sqroot-test","univariate","equation","test"],
537 ["Test","squ-equ-test-subpbl1"]))];
540 autoCalculate 1 CompleteCalc;
542 (*UC\label{SOLVE:MANUAL:TACTIC:listall} UC 30.3.2.2 p.175*)
543 fetchApplicableTactics 1 99999 ([],Pbl);
545 fetchApplicableTactics 1 99999 ([1],Res);
546 "~~~~~ fun fetchApplicableTactics, args:"; val (cI, (scope:int), (p:pos')) = (1, 99999, ([1],Res));
547 val ((pt, _), _) = get_calc cI;
549 case sel_rules pt p of [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",
550 Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]),
551 Check_elementwise "Assumptions"] => ()
552 | _ => error "fetchApplicableTactics ([1],Res) changed";
555 sel_appl_atomic_tacs pt p;
557 ### atomic_appl_tacs: not impl. for tac='Subproblem(Test,["LINEAR","univariate","equation","test"])'
558 ### atomic_appl_tacs: not impl. for tac = 'Check_elementwise "Assumptions"'
561 "~~~~~ fun sel_appl_atomic_tacs, args:"; val (pt, (p,p_)) = (pt, p);
562 is_spec_pos p_ = false;
563 val pp = par_pblobj pt p
564 val thy' = (get_obj g_domID pt pp):theory'
565 val thy = assoc_thy thy'
566 val metID = get_obj g_metID pt pp
569 then (thd3 o snd3) (get_obj g_origin pt pp)
571 val {scr=Prog sc,srls,erls,rew_ord'=ro,...} = get_met metID'
572 val ScrState (env,_,a,v,_,_) = get_istate pt (p,p_)
573 val alltacs = (*we expect at least 1 stac in a script*)
574 map ((stac2tac pt thy) o rep_stacexpr o #2 o
575 (handle_leaf "selrul" thy' srls env a v)) (stacpbls sc)
578 Frm => get_obj g_form pt p
579 | Res => (fst o (get_obj g_result pt)) p;
580 (*WN120611 stopped and took version 1 again for fetchApplicableTactics !
581 (distinct o flat o (map (atomic_appl_tacs thy ro erls f))) alltacs
583 ### atomic_appl_tacs: not impl. for tac='Subproblem(Test,["LINEAR","univariate","equation","test"])'
584 ### atomic_appl_tacs: not impl. for tac = 'Check_elementwise "Assumptions"'
587 "----------- fun de_esc_underscore -------------------------------";
588 "----------- fun de_esc_underscore -------------------------------";
589 "----------- fun de_esc_underscore -------------------------------";
591 > val str = "Rewrite_Set_Inst";
592 > val esc = esc_underscore str;
593 val it = "Rewrite'_Set'_Inst" : string
594 > val des = de_esc_underscore esc;
595 val des = de_esc_underscore esc;*)
597 "----------- fun go ----------------------------------------------";
598 "----------- fun go ----------------------------------------------";
599 "----------- fun go ----------------------------------------------";
601 > val t = (Thm.term_of o the o (parse thy)) "a+b";
602 val it = Const (#,#) $ Free (#,#) $ Free ("b","RealDef.real") : term
603 > val plus_a = go [L] t;
605 > val plus = go [L,L] t;
606 > val a = go [L,R] t;
608 > val t = (Thm.term_of o the o (parse thy)) "a+b+c";
609 val t = Const (#,#) $ (# $ # $ Free #) $ Free ("c","RealDef.real") : term
610 > val pl_pl_a_b = go [L] t;
612 > val a = go [L,R,L,R] t;
613 > val b = go [L,R,R] t;
616 "----------- fun formal_args -------------------------------------";
617 "----------- fun formal_args -------------------------------------";
618 "----------- fun formal_args -------------------------------------";
621 [Free ("f_","RealDef.real"),Free ("v_","RealDef.real"),
622 Free ("eqs_","bool List.list")] : term list
624 "----------- fun dsc_valT ----------------------------------------";
625 "----------- fun dsc_valT ----------------------------------------";
626 "----------- fun dsc_valT ----------------------------------------";
627 (*> val t = (Thm.term_of o the o (parse thy)) "equality";
629 val T = "bool => Tools.una" : typ
630 > val dsc = dsc_valT t;
631 val dsc = "una" : string
633 > val t = (Thm.term_of o the o (parse thy)) "fixedValues";
635 val T = "bool List.list => Tools.nam" : typ
636 > val dsc = dsc_valT t;
637 val dsc = "nam" : string*)
638 "----------- fun itms2args ---------------------------------------";
639 "----------- fun itms2args ---------------------------------------";
640 "----------- fun itms2args ---------------------------------------";
642 > val sc = ... Solve_root_equation ...
643 > val mI = ("Script","sqrt-equ-test");
644 > val PblObj{meth={ppc=itms,...},...} = get_obj I pt [];
645 > val ts = itms2args thy mI itms;
646 > map (term_to_string''' thy) ts;
647 ["sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x)","x","#0"] : string list
649 "----------- fun rep_tac_ ----------------------------------------";
650 "----------- fun rep_tac_ ----------------------------------------";
651 "----------- fun rep_tac_ ----------------------------------------";
652 (***************fun rep_tac_ (Rewrite_Inst' (thy', rod, rls, put, subs, (thmID, _), f, (f', _))) =
654 (a)----- als String zusammensetzen:
656 val it = "d_d x #4 + d_d x (x ^^^ #2 + #3 * x)" : string
658 val it = "#0 + d_d x (x ^^^ #2 + #3 * x)" : string
660 val it = [(Free ("bdv","RealDef.real"),Free ("x","RealDef.real"))] : subst
661 > val tt = (Thm.term_of o the o (parse thy))
662 "(Rewrite_Inst[(bdv,x)]diff_const False(d_d x #4 + d_d x (x ^^^ #2 + #3 * x)))=(#0 + d_d x (x ^^^ #2 + #3 * x))";
664 ML> tracing (term2str tt);
665 (Rewrite_Inst [(bdv,x)] diff_const False d_d x #4 + d_d x (x ^^^ #2 + #3 * x)) =
666 #0 + d_d x (x ^^^ #2 + #3 * x)
668 (b)----- laut rep_tac_:
669 > val ttt=HOLogic.mk_eq (lhs,f');
673 (*Fehlersuche 1-2Monate vor 4.01:*)
674 > val tt = (Thm.term_of o the o (parse thy))
675 "Rewrite_Inst[(bdv,x)]square_equation_left True(x=#1+#2)";
678 > val f = (Thm.term_of o the o (parse thy)) "x=#1+#2";
679 > val f' = (Thm.term_of o the o (parse thy)) "x=#3";
680 > val subs = [((Thm.term_of o the o (parse thy)) "bdv",
681 (Thm.term_of o the o (parse thy)) "x")];
682 > val sT = (type_of o fst o hd) subs;
683 > val subs' = list2isalist (HOLogic.mk_prodT (sT, sT))
684 (map HOLogic.mk_prod subs);
685 > val sT' = type_of subs';
686 > val lhs = Const ("Script.Rewrite'_Inst",[sT',idT,fT,fT] ---> fT)
687 $ subs' $ Free (thmID,idT) $ @{term True} $ f;
690 > rep_tac_ (Rewrite_Inst'
691 ("Script","tless_true","eval_rls",false,subs,
692 ("square_equation_left",""),f,(f',[])));
694 (****************************| rep_tac_ (Rewrite' (thy', _, _, put, (thmID, _), f, (f', _)))=
695 > val tt = (Thm.term_of o the o (parse thy)) (*____ ____..test*)
696 "Rewrite square_equation_left True (x=#1+#2) = (x=#3)";
698 > val f = (Thm.term_of o the o (parse thy)) "x=#1+#2";
699 > val f' = (Thm.term_of o the o (parse thy)) "x=#3";
702 ("Script","tless_true","eval_rls",false,
703 ("square_equation_left",""),f,(f',[])));
704 > val SOME ct = parse thy
705 "Rewrite square_equation_left True (x=#1+#2)";
706 > rewrite_ Script.thy tless_true eval_rls true thm ct;
707 val it = SOME ("x = #3",[]) : (cterm * cterm list) option
709 (**************************************** | rep_tac_ (Rewrite_Set_Inst'
710 WN050824: type error ...
711 let val fT = type_of f;
712 val sT = (type_of o fst o hd) subs;
713 val subs' = list2isalist (HOLogic.mk_prodT (sT, sT))
714 (map HOLogic.mk_prod subs);
715 val sT' = type_of subs';
716 val b = if put then @{term True} else @{term False}
717 val lhs = Const ("Script.Rewrite'_Set'_Inst",
718 [sT',idT,fT,fT] ---> fT)
719 $ subs' $ Free (id_rls rls,idT) $ b $ f;
720 in (((make_rule (assoc_thy thy')) o HOLogic.mk_eq) (lhs,f'),(lhs,f')) end*)
721 (* ... vals from Rewrite_Inst' ...
722 > rep_tac_ (Rewrite_Set_Inst'
723 ("Script",false,subs,
724 "isolate_bdv",f,(f',[])));
726 (* val (Rewrite_Set' (thy',put,rls,f,(f',asm)))=m;
728 (************************************** | rep_tac_ (Rewrite_Set' (thy',put,rls,f,(f',asm)))=
730 val thy = assoc_thy thy';
731 val t = HOLogic.mk_eq (lhs,f');
733 --------------------------------------------------
734 val lll = (Thm.term_of o the o (parse thy))
735 "Rewrite_Set SqRoot_simplify False (d_d x (x ^^^ #2 + #3 * x) + d_d x #4)";
737 --------------------------------------------------
738 > val f = (Thm.term_of o the o (parse thy)) "x=#1+#2";
739 > val f' = (Thm.term_of o the o (parse thy)) "x=#3";
741 rep_tac_ (Rewrite_Set'
742 ("Script",false,"SqRoot_simplify",f,(f',[])));
743 val id = "(Rewrite_Set SqRoot_simplify True x = #1 + #2) = (x = #3)" : string
744 val thm = "(Rewrite_Set SqRoot_simplify True x = #1 + #2) = (x = #3)" : thm
746 (***************************************** | rep_tac_ (Calculate' (thy',op_,f,(f',thm')))=
747 > val lhs'=(Thm.term_of o the o (parse thy))"Calculate plus (#1+#2)";
748 ... test-root-equ.sml: calculate ...
749 > val Appl m'=applicable_in p pt (Calculate "PLUS");
750 > val (lhs,_)=tac_2etac m';
752 val it = true : bool*)