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 "----------- x+1=2 set ctxt in Subproblem ------------------------";
14 "-----------------------------------------------------------------";
15 "-----------------------------------------------------------------";
16 "-----------------------------------------------------------------";
18 val thy= @{theory Isac};
19 "----------- WN0509 why does next_tac doesnt find Substitute -----";
20 "----------- WN0509 why does next_tac doesnt find Substitute -----";
21 "----------- WN0509 why does next_tac doesnt find Substitute -----";
23 (*replace met 'IntegrierenUndKonstanteBestimmen' with this script...*)
25 "Script BiegelinieScript " ^
26 "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
27 "(rb_rb::bool list) (rm_rm::bool list) = " ^
28 " (let q___q = Take (M_b v_v = q__q); " ^
29 " (M1__M1::bool) = ((Substitute [v_v = 0])) q___q " ^
32 val sc' = ((inst_abs thy) o term_of o the o (parse thy)) str;
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 " (M1__M1::bool) = ((Substitute [v_v = 0]) @@ " ^
39 " in True)";(*..doesnt find Substitute with ..@@ !!!!!!!!!!!!!!!!!!!!!*)
42 "Script BiegelinieScript " ^
43 "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
44 "(rb_rb::bool list) (rm_rm::bool list) = " ^
45 " (let q___q = Take (q_q v_v = q__q); " ^
46 " (M1__M1::bool) = Substitute [v_v = 0] q___q ; " ^
47 " M1__m1 = Substitute [M_b 0 = 0] M1__M1 " ^
51 "Script BiegelinieScript " ^
52 "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
53 "(rb_rb::bool list) (rm_rm::bool list) = " ^
54 " (let q___q = Take (q_q v_v = q__q); " ^
55 " (M1__M1::bool) = Substitute [v_v = 0] q___q ; " ^
56 " M1__M1 = Substitute [v_v = 1] q___q ; " ^
57 " M1__M1 = Substitute [v_v = 2] q___q ; " ^
58 " M1__M1 = Substitute [v_v = 3] q___q ; " ^
59 " M1__M1 = Substitute [M_b 0 = 0] M1__M1 " ^
63 "Script BiegelinieScript " ^
64 "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
65 "(rb_rb::bool list) (rm_rm::bool list) = " ^
66 " (let q___q = Take (M_b v_v = q__q); " ^
67 " (M1__M1::bool) = Substitute [v_v = 0] q___q ; " ^
68 " M2__M2 = Take q___q ; " ^
69 " M2__M2 = Substitute [v_v = 2] q___q " ^
73 val sc' = ((inst_abs thy) o term_of o the o (parse thy)) str;
76 val {scr = Script sc,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
77 (*---------------------------------------------------------------------
78 if sc = sc' then () else error"script.sml, doesnt find Substitute #1";
79 ---------------------------------------------------------------------*)
81 val fmz = ["Traegerlaenge L",
82 "Streckenlast (- q_0 * x^^^2 / 2 + x * c + c_2)",
84 "RandbedingungenBiegung [y 0 = 0, y L = 0]",
85 "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
86 "FunktionsVariable x"];
89 ("Biegelinie",["MomentBestimmte","Biegelinien"],
90 ["IntegrierenUndKonstanteBestimmen"]);
92 val p = e_pos'; val c = [];
94 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
95 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
96 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
97 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
98 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
99 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
100 val (p,_,f,nxt,_,pt) = me nxt p c pt;
101 val (p,_,f,nxt,_,pt) = me nxt p c pt;
103 case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()
104 | _ => error "script.sml, doesnt find Substitute #2";
106 (*========== inhibit exn AK110721 ================================================
108 (* AK110722 f2str f is NOT working anywhere - deprecated?????*)
110 (*(* val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
111 (* ERROR: exception PTREE "get_obj: pos = [0] does not exist" raised
112 (line 908 of "src/Tools/isac/Interpret/ctree.sml")*)*)
114 (* ERROR: exception Match raised (line 416 of "src/Tools/isac/Interpret/mathengine.sml")*)*)
115 (* "~~~~~ fun f2str, args:"; val ((Form' (FormKF (_, _, _, _, cterm')))) = (f);
116 (* ERROR: exception Bind raised *)*)
121 (* *** generate1: not impl.for Substitute' !!!!!!!!!!(*#1#*)!!!!!!!!!!!*)
122 (* val nxt = ("Check_Postcond",.. !!!!!!!!!!!!!!!!!!!(*#2#*)!!!!!!!!!!!*)
124 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
125 (* *** generate1: not impl.for Empty_Tac_ !!!!!!!!!!(*#3#*)!!!!!!!!!!!*)
126 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
127 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
128 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
129 (*---------------------------------------------------------------------*)
131 case nxt of (_, End_Proof') => ()
132 | _ => error "script.sml, doesnt find Substitute #3";
133 (*---------------------------------------------------------------------*)
134 (*the reason, that next_tac didnt find the 2nd Substitute, was that
135 the Take inbetween was missing, and thus the 2nd Substitute was applied
136 the last formula in ctree, and not to argument from script*)
137 ========== inhibit exn AK110721 ================================================*)
140 "----------- WN0509 Substitute 2nd part --------------------------";
141 "----------- WN0509 Substitute 2nd part --------------------------";
142 "----------- WN0509 Substitute 2nd part --------------------------";
143 (*replace met 'IntegrierenUndKonstanteBestimmen' with this script...*)
144 val str = (*Substitute ; Substitute works*)
145 "Script BiegelinieScript " ^
146 "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
147 "(rb_rb::bool list) (rm_rm::bool list) = "^
148 (*begin after the 2nd integrate*)
149 " (let M__M = Take (M_b v_v = q__q); " ^
150 " e1__e1 = nth_nth 1 rm_rm ; " ^
151 " (x1__x1::real) = argument_in (lhs e1__e1); " ^
152 " (M1__M1::bool) = Substitute [v_v = x1__x1] M__M; " ^
153 " M1__M1 = Substitute [e1__e1] M1__M1 " ^
156 val sc' = ((inst_abs thy) o term_of o the o (parse thy)) str;
159 val str = (*Substitute @@ Substitute does NOT work???*)
160 "Script BiegelinieScript " ^
161 "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
162 "(rb_rb::bool list) (rm_rm::bool list) = "^
163 (*begin after the 2nd integrate*)
164 " (let M__M = Take (M_b v_v = q__q); " ^
165 " e1__e1 = nth_nth 1 rm_rm ; " ^
166 " (x1__x1::real) = argument_in (lhs e1__e1); " ^
167 " (M1__M1::bool) = ((Substitute [v_v = x1__x1]) @@ " ^
168 " (Substitute [e1__e1])) M__M " ^
172 val {scr = Script sc,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
173 (*---------------------------------------------------------------------
174 if sc = sc' then () else error "script.sml, doesnt find Substitute #1";
175 ---------------------------------------------------------------------*)
176 val fmz = ["Traegerlaenge L",
177 "Streckenlast (- q_0 * x^^^2 / 2 + x * c + c_2)",
179 "RandbedingungenBiegung [y 0 = 0, y L = 0]",
180 "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
181 "FunktionsVariable x"];
183 ("Biegelinie",["MomentBestimmte","Biegelinien"],
184 ["IntegrierenUndKonstanteBestimmen"]);
185 val p = e_pos'; val c = [];
186 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
187 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
188 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
189 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
190 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
191 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
192 val (p,_,f,nxt,_,pt) = me nxt p c pt;
193 val (p,_,f,nxt,_,pt) = me nxt p c pt;
194 case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()
195 | _ => error "script.sml, doesnt find Substitute #2";
197 (*========== inhibit exn AK110721 ================================================
198 (* ERROR: caused by f2str f *)
200 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f(*------------------------*);
201 trace_rewrite:=false;
202 (*Exception TYPE raised:
203 Illegal type for constant "HOL.eq" :: "[real, bool] => bool"
204 Atools.argument'_in (Tools.lhs (ListG.nth_ (1 + -1 + -1) [])) =
205 ListG.nth_ (1 + -1 + -1) []
208 ("Illegal type for constant \"op =\" :: \"[real, bool] => bool\"",
210 [Const ("HOL.Trueprop", "bool => prop") $
211 (Const ("HOL.eq", "[RealDef.real, bool] => bool") $ ... $ ...)])
213 ... this was because eval_argument_in took "argument_in (lhs (M_b 0 = 0))"
214 ie. the argument had not been simplified before ^^^^^^^^^^^^^^^
215 thus corrected eval_argument_in OK*)
216 ========== inhibit exn AK110721 ================================================*)
218 val {srls,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
219 val e1__e1 = str2term "nth_nth 1 [M_b 0 = 0, M_b L = 0]";
220 val e1__e1 = eval_listexpr_ @{theory Biegelinie} srls e1__e1; term2str e1__e1;
222 (*========== inhibit exn 110721 ================================================
224 TRIAL: Should be the same
225 term2str e1__e1 = "M_b 0 = 0";
228 if term2str e1__e1 = "M_b 0 = 0"
230 else error"script.sml diff.beh. eval_listexpr_ nth_nth 1 [...";
231 ========== inhibit exn 110721 ================================================*)
233 (*TODO.WN050913 ??? doesnt eval_listexpr_ go into subterms ???...
234 val x1__ = str2term"argument_in (lhs (M_b 0 = 0))";
235 val x1__ = eval_listexpr_ Biegelinie.thy srls x1__; term2str x1__;
237 calculate_ Biegelinie.thy ("Tools.lhs", eval_rhs"eval_lhs_") x1__;
238 val SOME (str, t) = eval_lhs 0 "Tools.lhs" (str2term"lhs (M_b 0 = 0)") 0;*)
240 val l__l = str2term "lhs (M_b 0 = 0)";
241 (*AK110722 eval_listexpr_ is prob. without _ ????*)
242 val l__l = eval_listexpr_ @{theory Biegelinie} srls l__l; term2str l__l;
243 val SOME (str, t) = eval_lhs 0 "Tools.lhs" (str2term "lhs (M_b 0 = 0)") 0;
244 (*========== inhibit exn 110721 ================================================
246 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f (*------------------------*);
247 trace_rewrite:=false;
248 ========== inhibit exn 110721 ================================================*)
252 "----------- fun sel_appl_atomic_tacs ----------------------------";
253 "----------- fun sel_appl_atomic_tacs ----------------------------";
254 "----------- fun sel_appl_atomic_tacs ----------------------------";
257 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
258 ("Test", ["sqroot-test","univariate","equation","test"],
259 ["Test","squ-equ-test-subpbl1"]))];
262 autoCalculate 1 CompleteCalcHead;
263 autoCalculate 1 (Step 1);
264 autoCalculate 1 (Step 1);
265 val ((pt, p), _) = get_calc 1; show_pt pt;
266 val appltacs = sel_appl_atomic_tacs pt p;
268 (*========== inhibit exn AK110721 ================================================
269 (*(*These SHOULD be the same*)
272 [Rewrite ("radd_commute", "?m + ?n = ?n + ?m"),
273 Rewrite ("radd_assoc", "?m + ?n + ?k = ?m + (?n + ?k)"),
274 Calculate "TIMES"];*)
277 [Rewrite ("radd_commute", "?m + ?n = ?n + ?m"),
278 Rewrite ("radd_assoc", "?m + ?n + ?k = ?m + (?n + ?k)"),
279 Calculate "TIMES"] then ()
280 else error "script.sml fun sel_appl_atomic_tacs diff.behav.";
281 ========== inhibit exn AK110721 ================================================*)
283 trace_script := true;
284 trace_script := false;
285 applyTactic 1 p (hd appltacs);
286 val ((pt, p), _) = get_calc 1; show_pt pt;
287 val appltacs = sel_appl_atomic_tacs pt p;
289 (*(* AK110722 Debugging start*)
290 (*applyTactic 1 p (hd appltacs); WAS assy: call by ([3], Pbl)*)
291 "~~~~~ fun applyTactic, args:"; val ((cI:calcID), ip, tac) = (1, p, (hd appltacs));
292 val ((pt, _), _) = get_calc cI;
293 val p = get_pos cI 1;
299 (*locatetac tac (pt, ip); (*WAS assy: call by ([3], Pbl)*)*)
300 "~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, ip));
301 val (mI,m) = mk_tac'_ tac;
303 applicable_in p pt m ; (*Appl*)
305 member op = specsteps mI; (*false*)
307 (*loc_solve_ (mI,m) ptp; (*Argument: (mI, m) : string * tac Reason: Can't unify tac_ with tac*)*)
308 loc_solve_; (*without _ ??? result is -> lOc writing error ???*)
309 (*val it = fn: string * tac_ -> ptree * (pos * pos_) -> lOc_*)
310 (mI,m); (*string * tac*)
311 ptp (*ptree * pos'*);
313 "~~~~~ fun loc_solve_, args:"; val (m ,(pt,pos)) = ((mI,m), ptp);
314 (*val (msg, cs') = solve m (pt, pos);
315 (*Argument: m : string * tac Reason: Can't unify tac_ with tac (Different type constructors)*)*)
320 "~~~~~ fun solve, args:"; val ((mI,m), (pt, po as (p,p_))) = (m, (pt, pos));
321 (*solve has still p_!!!!!!!!!!!!!!!!!!!!!!!!!*)
323 e_metID = get_obj g_metID pt (par_pblobj pt p); (*false*)
324 val ctxt = get_ctxt pt po;
326 (*generate1 (assoc_thy (get_obj g_domID pt (par_pblobj pt p))) m (e_istate, ctxt) (p,p_) pt;
327 (*Argument: m : tac Reason: Can't unify tac_ with tac (Different type constructors)*)*)
328 (assoc_thy (get_obj g_domID pt (par_pblobj pt p)));
331 (*not finished - error continues in fun generate1*)
332 (* AK110722 Debugging end*)*)
333 (*========== inhibit exn AK110721 ================================================
334 "----- WN080102 these vvv do not work, because locatetac starts the search" ^
336 (* AK110722 ERROR: assy: call by ([3], Pbl) *)
337 applyTactic 1 p (hd appltacs);
338 ============ inhibit exn AK110721 ==============================================*)
340 autoCalculate 1 CompleteCalc;
342 "----------- fun init_form, fun get_stac -------------------------";
343 "----------- fun init_form, fun get_stac -------------------------";
344 "----------- fun init_form, fun get_stac -------------------------";
345 val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
346 val (dI',pI',mI') = ("Test",["sqroot-test","univariate","equation","test"],
347 ["Test","squ-equ-test-subpbl1"]);
348 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
349 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
350 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
351 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
352 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
353 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
354 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
355 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
356 "~~~~~ fun me, args:"; val (_,tac) = nxt;
357 "~~~~~ fun locatetac, args:"; val ptp as (pt, p) = (pt, p);
358 val (mI,m) = mk_tac'_ tac;
359 val Appl m = applicable_in p pt m;
360 member op = specsteps mI; (*false*)
361 "~~~~~ fun loc_solve_, args:"; val (m, (pt, pos) ) = ((mI, m), ptp);
362 "~~~~~ fun solve, args:"; val (("Apply_Method", Apply_Method' (mI,_,_,_)), pos as (p,_)) = (m, pos);
363 val {srls, ...} = get_met mI;
364 val PblObj {meth=itms, ...} = get_obj I pt p;
365 val thy' = get_obj g_domID pt p;
366 val thy = assoc_thy thy';
367 val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI;
368 val ini = init_form thy sc env;
369 "----- fun init_form, args:"; val (Script sc) = sc;
370 "----- fun get_stac, args:"; val (y, h $ body) = (thy, sc);
371 case get_stac thy sc of SOME (Free ("e_e", _)) => ()
372 | _ => error "script: Const (?, ?) in script (as term) changed";;
375 "----------- x+1=2 start SubProblem 'stac2tac_ TODO: no match for ";
376 "----------- x+1=2 start SubProblem 'stac2tac_ TODO: no match for ";
377 "----------- x+1=2 start SubProblem 'stac2tac_ TODO: no match for ";
378 val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
380 ("Test", ["sqroot-test","univariate","equation","test"],
381 ["Test","squ-equ-test-subpbl1"]);
382 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
383 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
384 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
385 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
386 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
387 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
388 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
389 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
390 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
391 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
392 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt; WAS: Empty_Tac, helpless*)
394 "~~~~~ fun me, args:"; val (_,tac) = nxt;
395 val (pt, p) = case locatetac tac (pt,p) of
396 ("ok", (_, _, ptp)) => ptp | _ => error "script.sml locatetac";
397 "~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
398 val pIopt = get_pblID (pt,ip); (*SOME ["linear", "univariate", "equation", "test"]*)
400 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*)
401 "~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
402 (*WAS stac2tac_ TODO: no match for SubProblem*)
403 val thy' = get_obj g_domID pt (par_pblobj pt p);
404 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
405 "~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt,(p,_)):ptree * pos'), (sc as Script (h $ body)),
406 (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
407 l; (*= [R, L, R, L, R, R]*)
408 val Appy (m', scrst as (_,_,_,v,_,_)) = nstep_up thy ptp sc E l Skip_ a v;
409 "~~~~~ dont like to go into nstep_up...";
410 val t = str2term ("SubProblem" ^
411 "(Test', [linear, univariate, equation, test], [Test, solve_linear])" ^
412 "[BOOL (-1 + x = 0), REAL x]");
413 val (tac, tac_) = stac2tac_ pt @{theory "Isac"} t; (*WAS stac2tac_ TODO: no match for SubProblem*)
416 | _ => error "script.sml x+1=2 start SubProblem from script";
419 "----------- x+1=2 set ctxt in Subproblem ------------------------";
420 "----------- x+1=2 set ctxt in Subproblem ------------------------";
421 "----------- x+1=2 set ctxt in Subproblem ------------------------";