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 "-----------------------------------------------------------------";
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 (*========== inhibit exn 110721 ================================================
33 (* ERROR: parse thy Can't unify theory to domID * rls*)
34 val sc' = ((inst_abs thy) o term_of o the o (parse thy)) str;
35 ========= inhibit exn 110721 ================================================*)
38 "Script BiegelinieScript " ^
39 "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
40 "(rb_rb::bool list) (rm_rm::bool list) = " ^
41 " (M1__M1::bool) = ((Substitute [v_v = 0]) @@ " ^
42 " in True)";(*..doesnt find Substitute with ..@@ !!!!!!!!!!!!!!!!!!!!!*)
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 " (let q___q = Take (q_q v_v = q__q); " ^
49 " (M1__M1::bool) = Substitute [v_v = 0] q___q ; " ^
50 " M1__m1 = Substitute [M_b 0 = 0] M1__M1 " ^
54 "Script BiegelinieScript " ^
55 "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
56 "(rb_rb::bool list) (rm_rm::bool list) = " ^
57 " (let q___q = Take (q_q v_v = q__q); " ^
58 " (M1__M1::bool) = Substitute [v_v = 0] q___q ; " ^
59 " M1__M1 = Substitute [v_v = 1] q___q ; " ^
60 " M1__M1 = Substitute [v_v = 2] q___q ; " ^
61 " M1__M1 = Substitute [v_v = 3] q___q ; " ^
62 " M1__M1 = Substitute [M_b 0 = 0] M1__M1 " ^
66 "Script BiegelinieScript " ^
67 "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
68 "(rb_rb::bool list) (rm_rm::bool list) = " ^
69 " (let q___q = Take (M_b v_v = q__q); " ^
70 " (M1__M1::bool) = Substitute [v_v = 0] q___q ; " ^
71 " M2__M2 = Take q___q ; " ^
72 " M2__M2 = Substitute [v_v = 2] q___q " ^
76 (*========== inhibit exn 110721 ================================================
77 val sc' = ((inst_abs thy) o term_of o the o (parse thy)) str;
79 ========== inhibit exn 110721 ================================================*)
81 val {scr = Script sc,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
82 (*---------------------------------------------------------------------
83 if sc = sc' then () else error"script.sml, doesnt find Substitute #1";
84 ---------------------------------------------------------------------*)
86 val fmz = ["Traegerlaenge L",
87 "Streckenlast (- q_0 * x^^^2 / 2 + x * c + c_2)",
89 "RandbedingungenBiegung [y 0 = 0, y L = 0]",
90 "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
91 "FunktionsVariable x"];
94 ("Biegelinie",["MomentBestimmte","Biegelinien"],
95 ["IntegrierenUndKonstanteBestimmen"]);
97 val p = e_pos'; val c = [];
99 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
100 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
101 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
102 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
103 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
104 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
105 val (p,_,f,nxt,_,pt) = me nxt p c pt;
106 val (p,_,f,nxt,_,pt) = me nxt p c pt;
108 case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()
109 | _ => error "script.sml, doesnt find Substitute #2";
111 (*========== inhibit exn AK110721 ================================================
113 (* AK110722 f2str f is NOT working anywhere - deprecated?????*)
115 (*(* val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
116 (* ERROR: exception PTREE "get_obj: pos = [0] does not exist" raised
117 (line 908 of "src/Tools/isac/Interpret/ctree.sml")*)*)
119 (* ERROR: exception Match raised (line 416 of "src/Tools/isac/Interpret/mathengine.sml")*)*)
120 (* "~~~~~ fun f2str, args:"; val ((Form' (FormKF (_, _, _, _, cterm')))) = (f);
121 (* ERROR: exception Bind raised *)*)
126 (* *** generate1: not impl.for Substitute' !!!!!!!!!!(*#1#*)!!!!!!!!!!!*)
127 (* val nxt = ("Check_Postcond",.. !!!!!!!!!!!!!!!!!!!(*#2#*)!!!!!!!!!!!*)
129 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
130 (* *** generate1: not impl.for Empty_Tac_ !!!!!!!!!!(*#3#*)!!!!!!!!!!!*)
131 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
132 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
133 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
134 (*---------------------------------------------------------------------*)
136 case nxt of (_, End_Proof') => ()
137 | _ => error "script.sml, doesnt find Substitute #3";
138 (*---------------------------------------------------------------------*)
139 (*the reason, that next_tac didnt find the 2nd Substitute, was that
140 the Take inbetween was missing, and thus the 2nd Substitute was applied
141 the last formula in ctree, and not to argument from script*)
142 ========== inhibit exn AK110721 ================================================*)
145 "----------- WN0509 Substitute 2nd part --------------------------";
146 "----------- WN0509 Substitute 2nd part --------------------------";
147 "----------- WN0509 Substitute 2nd part --------------------------";
148 (*replace met 'IntegrierenUndKonstanteBestimmen' with this script...*)
149 val str = (*Substitute ; Substitute works*)
150 "Script BiegelinieScript " ^
151 "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
152 "(rb_rb::bool list) (rm_rm::bool list) = "^
153 (*begin after the 2nd integrate*)
154 " (let M__M = Take (M_b v_v = q__q); " ^
155 " e1__e1 = nth_nth 1 rm_rm ; " ^
156 " (x1__x1::real) = argument_in (lhs e1__e1); " ^
157 " (M1__M1::bool) = Substitute [v_v = x1__x1] M__M; " ^
158 " M1__M1 = Substitute [e1__e1] M1__M1 " ^
161 (*========== inhibit exn 110721 ================================================
162 (*---^^^-OK-----------------------------------------------------------------*)
163 val sc' = ((inst_abs thy) o term_of o the o (parse thy)) str;
165 (*---vvv-NOT ok-------------------------------------------------------------*)
166 ========== inhibit exn 110721 ================================================*)
168 val str = (*Substitute @@ Substitute does NOT work???*)
169 "Script BiegelinieScript " ^
170 "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
171 "(rb_rb::bool list) (rm_rm::bool list) = "^
172 (*begin after the 2nd integrate*)
173 " (let M__M = Take (M_b v_v = q__q); " ^
174 " e1__e1 = nth_nth 1 rm_rm ; " ^
175 " (x1__x1::real) = argument_in (lhs e1__e1); " ^
176 " (M1__M1::bool) = ((Substitute [v_v = x1__x1]) @@ " ^
177 " (Substitute [e1__e1])) M__M " ^
181 val {scr = Script sc,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
182 (*---------------------------------------------------------------------
183 if sc = sc' then () else error "script.sml, doesnt find Substitute #1";
184 ---------------------------------------------------------------------*)
185 val fmz = ["Traegerlaenge L",
186 "Streckenlast (- q_0 * x^^^2 / 2 + x * c + c_2)",
188 "RandbedingungenBiegung [y 0 = 0, y L = 0]",
189 "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
190 "FunktionsVariable x"];
192 ("Biegelinie",["MomentBestimmte","Biegelinien"],
193 ["IntegrierenUndKonstanteBestimmen"]);
194 val p = e_pos'; val c = [];
195 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
196 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
197 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
198 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
199 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
200 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
201 val (p,_,f,nxt,_,pt) = me nxt p c pt;
202 val (p,_,f,nxt,_,pt) = me nxt p c pt;
203 case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()
204 | _ => error "script.sml, doesnt find Substitute #2";
206 (*========== inhibit exn AK110721 ================================================
207 (* ERROR: caused by f2str f *)
209 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f(*------------------------*);
210 trace_rewrite:=false;
211 (*Exception TYPE raised:
212 Illegal type for constant "HOL.eq" :: "[real, bool] => bool"
213 Atools.argument'_in (Tools.lhs (ListG.nth_ (1 + -1 + -1) [])) =
214 ListG.nth_ (1 + -1 + -1) []
217 ("Illegal type for constant \"op =\" :: \"[real, bool] => bool\"",
219 [Const ("HOL.Trueprop", "bool => prop") $
220 (Const ("HOL.eq", "[RealDef.real, bool] => bool") $ ... $ ...)])
222 ... this was because eval_argument_in took "argument_in (lhs (M_b 0 = 0))"
223 ie. the argument had not been simplified before ^^^^^^^^^^^^^^^
224 thus corrected eval_argument_in OK*)
225 ========== inhibit exn AK110721 ================================================*)
227 val {srls,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
228 val e1__e1 = str2term "nth_nth 1 [M_b 0 = 0, M_b L = 0]";
229 val e1__e1 = eval_listexpr_ @{theory Biegelinie} srls e1__e1; term2str e1__e1;
231 (*========== inhibit exn 110721 ================================================
233 TRIAL: Should be the same
234 term2str e1__e1 = "M_b 0 = 0";
237 if term2str e1__e1 = "M_b 0 = 0"
239 else error"script.sml diff.beh. eval_listexpr_ nth_nth 1 [...";
240 ========== inhibit exn 110721 ================================================*)
242 (*TODO.WN050913 ??? doesnt eval_listexpr_ go into subterms ???...
243 val x1__ = str2term"argument_in (lhs (M_b 0 = 0))";
244 val x1__ = eval_listexpr_ Biegelinie.thy srls x1__; term2str x1__;
246 calculate_ Biegelinie.thy ("Tools.lhs", eval_rhs"eval_lhs_") x1__;
247 val SOME (str, t) = eval_lhs 0 "Tools.lhs" (str2term"lhs (M_b 0 = 0)") 0;*)
249 val l__l = str2term "lhs (M_b 0 = 0)";
250 (*AK110722 eval_listexpr_ is prob. without _ ????*)
251 val l__l = eval_listexpr_ @{theory Biegelinie} srls l__l; term2str l__l;
252 val SOME (str, t) = eval_lhs 0 "Tools.lhs" (str2term "lhs (M_b 0 = 0)") 0;
253 (*========== inhibit exn 110721 ================================================
255 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f (*------------------------*);
256 trace_rewrite:=false;
257 ========== inhibit exn 110721 ================================================*)
261 "----------- fun sel_appl_atomic_tacs ----------------------------";
262 "----------- fun sel_appl_atomic_tacs ----------------------------";
263 "----------- fun sel_appl_atomic_tacs ----------------------------";
266 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
267 ("Test", ["sqroot-test","univariate","equation","test"],
268 ["Test","squ-equ-test-subpbl1"]))];
271 autoCalculate 1 CompleteCalcHead;
272 autoCalculate 1 (Step 1);
273 autoCalculate 1 (Step 1);
274 val ((pt, p), _) = get_calc 1; show_pt pt;
275 val appltacs = sel_appl_atomic_tacs pt p;
277 (*========== inhibit exn AK110721 ================================================
278 (*(*These SHOULD be the same*)
281 [Rewrite ("radd_commute", "?m + ?n = ?n + ?m"),
282 Rewrite ("radd_assoc", "?m + ?n + ?k = ?m + (?n + ?k)"),
283 Calculate "TIMES"];*)
286 [Rewrite ("radd_commute", "?m + ?n = ?n + ?m"),
287 Rewrite ("radd_assoc", "?m + ?n + ?k = ?m + (?n + ?k)"),
288 Calculate "TIMES"] then ()
289 else error "script.sml fun sel_appl_atomic_tacs diff.behav.";
290 ========== inhibit exn AK110721 ================================================*)
292 trace_script := true;
293 trace_script := false;
294 applyTactic 1 p (hd appltacs);
295 val ((pt, p), _) = get_calc 1; show_pt pt;
296 val appltacs = sel_appl_atomic_tacs pt p;
298 (*(* AK110722 Debugging start*)
299 (*applyTactic 1 p (hd appltacs); WAS assy: call by ([3], Pbl)*)
300 "~~~~~ fun applyTactic, args:"; val ((cI:calcID), ip, tac) = (1, p, (hd appltacs));
301 val ((pt, _), _) = get_calc cI;
302 val p = get_pos cI 1;
308 (*locatetac tac (pt, ip); (*WAS assy: call by ([3], Pbl)*)*)
309 "~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, ip));
310 val (mI,m) = mk_tac'_ tac;
312 applicable_in p pt m ; (*Appl*)
314 member op = specsteps mI; (*false*)
316 (*loc_solve_ (mI,m) ptp; (*Argument: (mI, m) : string * tac Reason: Can't unify tac_ with tac*)*)
317 loc_solve_; (*without _ ??? result is -> lOc writing error ???*)
318 (*val it = fn: string * tac_ -> ptree * (pos * pos_) -> lOc_*)
319 (mI,m); (*string * tac*)
320 ptp (*ptree * pos'*);
322 "~~~~~ fun loc_solve_, args:"; val (m ,(pt,pos)) = ((mI,m), ptp);
323 (*val (msg, cs') = solve m (pt, pos);
324 (*Argument: m : string * tac Reason: Can't unify tac_ with tac (Different type constructors)*)*)
329 "~~~~~ fun solve, args:"; val ((mI,m), (pt, po as (p,p_))) = (m, (pt, pos));
330 (*solve has still p_!!!!!!!!!!!!!!!!!!!!!!!!!*)
332 e_metID = get_obj g_metID pt (par_pblobj pt p); (*false*)
333 val ctxt = get_ctxt pt po;
335 (*generate1 (assoc_thy (get_obj g_domID pt (par_pblobj pt p))) m (e_istate, ctxt) (p,p_) pt;
336 (*Argument: m : tac Reason: Can't unify tac_ with tac (Different type constructors)*)*)
337 (assoc_thy (get_obj g_domID pt (par_pblobj pt p)));
340 (*not finished - error continues in fun generate1*)
341 (* AK110722 Debugging end*)*)
342 (*========== inhibit exn AK110721 ================================================
343 "----- WN080102 these vvv do not work, because locatetac starts the search" ^
345 (* AK110722 ERROR: assy: call by ([3], Pbl) *)
346 applyTactic 1 p (hd appltacs);
347 ============ inhibit exn AK110721 ==============================================*)
349 autoCalculate 1 CompleteCalc;
351 "----------- fun init_form, fun get_stac -------------------------";
352 "----------- fun init_form, fun get_stac -------------------------";
353 "----------- fun init_form, fun get_stac -------------------------";
354 val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
355 val (dI',pI',mI') = ("Test",["sqroot-test","univariate","equation","test"],
356 ["Test","squ-equ-test-subpbl1"]);
357 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
358 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
359 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
360 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
361 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
362 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
363 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
364 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
365 "~~~~~ fun me, args:"; val (_,tac) = nxt;
366 "~~~~~ fun locatetac, args:"; val ptp as (pt, p) = (pt, p);
367 val (mI,m) = mk_tac'_ tac;
368 val Appl m = applicable_in p pt m;
369 member op = specsteps mI; (*false*)
370 "~~~~~ fun loc_solve_, args:"; val (m, (pt, pos) ) = ((mI, m), ptp);
371 "~~~~~ fun solve, args:"; val (("Apply_Method", Apply_Method' (mI,_,_,_)), pos as (p,_)) = (m, pos);
372 val {srls, ...} = get_met mI;
373 val PblObj {meth=itms, ...} = get_obj I pt p;
374 val thy' = get_obj g_domID pt p;
375 val thy = assoc_thy thy';
376 val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI;
377 val ini = init_form thy sc env;
378 "----- fun init_form, args:"; val (Script sc) = sc;
379 "----- fun get_stac, args:"; val (y, h $ body) = (thy, sc);
380 case get_stac thy sc of SOME (Free ("e_e", _)) => ()
381 | _ => error "script: Const (?, ?) in script (as term) changed";;
384 "----------- x+1=2 start SubProblem 'stac2tac_ TODO: no match for ";
385 "----------- x+1=2 start SubProblem 'stac2tac_ TODO: no match for ";
386 "----------- x+1=2 start SubProblem 'stac2tac_ TODO: no match for ";
387 val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
389 ("Test", ["sqroot-test","univariate","equation","test"],
390 ["Test","squ-equ-test-subpbl1"]);
391 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
392 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
393 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
394 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
395 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
396 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
397 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
398 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
399 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
400 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
401 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt; WAS: Empty_Tac, helpless*)
403 "~~~~~ fun me, args:"; val (_,tac) = nxt;
404 val (pt, p) = case locatetac tac (pt,p) of
405 ("ok", (_, _, ptp)) => ptp | _ => error "script.sml locatetac";
406 "~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
407 val pIopt = get_pblID (pt,ip); (*SOME ["linear", "univariate", "equation", "test"]*)
409 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*)
410 "~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
411 (*WAS stac2tac_ TODO: no match for SubProblem*)
412 val thy' = get_obj g_domID pt (par_pblobj pt p);
413 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
414 "~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt,(p,_)):ptree * pos'), (sc as Script (h $ body)),
415 (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
416 l; (*= [R, L, R, L, R, R]*)
417 val Appy (m', scrst as (_,_,_,v,_,_)) = nstep_up thy ptp sc E l Skip_ a v;
418 "~~~~~ dont like to go into nstep_up...";
419 val t = str2term ("SubProblem" ^
420 "(Test', [linear, univariate, equation, test], [Test, solve_linear])" ^
421 "[BOOL (-1 + x = 0), REAL x]");
422 val (tac, tac_) = stac2tac_ pt @{theory "Isac"} t; (*WAS stac2tac_ TODO: no match for SubProblem*)
425 | _ => error "script.sml x+1=2 start SubProblem from script";
428 "----------- x+1=2 set ctxt in Subproblem ------------------------";
429 "----------- x+1=2 set ctxt in Subproblem ------------------------";
430 "----------- x+1=2 set ctxt in Subproblem ------------------------";