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 "----------- Apply_Method: exception PTREE get_obj: pos = [0] does";
10 "----------- WN0509 Substitute 2nd part --------------------------";
11 "----------- fun sel_appl_atomic_tacs ----------------------------";
12 "----------- fun init_form, fun get_stac -------------------------";
13 "----------- x+1=2 start SubProblem 'stac2tac_ TODO: no match for ";
14 "----------- x+1=2 set ctxt in Subproblem ------------------------";
15 "-----------------------------------------------------------------";
16 "-----------------------------------------------------------------";
17 "-----------------------------------------------------------------";
19 val thy= @{theory Isac};
21 "----------- WN0509 why does next_tac doesnt find Substitute -----";
22 "----------- WN0509 why does next_tac doesnt find Substitute -----";
23 "----------- WN0509 why does next_tac doesnt find Substitute -----";
25 (*replace met 'IntegrierenUndKonstanteBestimmen' with this script...*)
27 "Script BiegelinieScript " ^
28 "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
29 "(rb_rb::bool list) (rm_rm::bool list) = " ^
30 " (let q___q = Take (M_b v_v = q__q); " ^
31 " (M1__M1::bool) = ((Substitute [v_v = 0])) q___q " ^
34 val sc' = ((inst_abs thy) o term_of o the o (parse thy)) str;
37 "Script BiegelinieScript " ^
38 "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
39 "(rb_rb::bool list) (rm_rm::bool list) = " ^
40 " (M1__M1::bool) = ((Substitute [v_v = 0]) @@ " ^
41 " in True)";(*..doesnt find Substitute with ..@@ !!!!!!!!!!!!!!!!!!!!!*)
44 "Script BiegelinieScript " ^
45 "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
46 "(rb_rb::bool list) (rm_rm::bool list) = " ^
47 " (let q___q = Take (q_q v_v = q__q); " ^
48 " (M1__M1::bool) = Substitute [v_v = 0] q___q ; " ^
49 " M1__m1 = Substitute [M_b 0 = 0] M1__M1 " ^
53 "Script BiegelinieScript " ^
54 "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
55 "(rb_rb::bool list) (rm_rm::bool list) = " ^
56 " (let q___q = Take (q_q v_v = q__q); " ^
57 " (M1__M1::bool) = Substitute [v_v = 0] q___q ; " ^
58 " M1__M1 = Substitute [v_v = 1] q___q ; " ^
59 " M1__M1 = Substitute [v_v = 2] q___q ; " ^
60 " M1__M1 = Substitute [v_v = 3] q___q ; " ^
61 " M1__M1 = Substitute [M_b 0 = 0] M1__M1 " ^
65 "Script BiegelinieScript " ^
66 "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
67 "(rb_rb::bool list) (rm_rm::bool list) = " ^
68 " (let q___q = Take (M_b v_v = q__q); " ^
69 " (M1__M1::bool) = Substitute [v_v = 0] q___q ; " ^
70 " M2__M2 = Take q___q ; " ^
71 " M2__M2 = Substitute [v_v = 2] q___q " ^
75 val sc' = ((inst_abs thy) o term_of o the o (parse thy)) str;
78 val {scr = Script sc,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
79 (*---------------------------------------------------------------------
80 if sc = sc' then () else error"script.sml, doesnt find Substitute #1";
81 ---------------------------------------------------------------------*)
83 "----------- Apply_Method: exception PTREE get_obj: pos = [0] does";
84 "----------- Apply_Method: exception PTREE get_obj: pos = [0] does";
85 "----------- Apply_Method: exception PTREE get_obj: pos = [0] does";
86 (*WN110922 exception PTREE "get_obj: pos = [0] does not exist"*)
87 val fmz = ["Traegerlaenge L",
88 "Streckenlast (- q_0 * x^^^2 / 2 + x * c + c_2)",
90 "RandbedingungenBiegung [y 0 = 0, y L = 0]",
91 "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
92 "FunktionsVariable x"];
94 ("Biegelinie",["MomentBestimmte","Biegelinien"],
95 ["IntegrierenUndKonstanteBestimmen"]);
96 val p = e_pos'; val c = [];
97 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
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; 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;
104 val (p,_,f,nxt,_,pt) = me nxt p c pt;
106 case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()
107 | _ => error "script.sml, doesnt find Substitute #2";
109 (*========== inhibit exn AK110721 ================================================
111 (* AK110722 f2str f is NOT working anywhere - deprecated?????*)
113 (*(* val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
114 (* ERROR: exception PTREE "get_obj: pos = [0] does not exist" raised
115 (line 908 of "src/Tools/isac/Interpret/ctree.sml")*)*)
117 (* ERROR: exception Match raised (line 416 of "src/Tools/isac/Interpret/mathengine.sml")*)*)
118 (* "~~~~~ fun f2str, args:"; val ((Form' (FormKF (_, _, _, _, cterm')))) = (f);
119 (* ERROR: exception Bind raised *)*)
124 (* *** generate1: not impl.for Substitute' !!!!!!!!!!(*#1#*)!!!!!!!!!!!*)
125 (* val nxt = ("Check_Postcond",.. !!!!!!!!!!!!!!!!!!!(*#2#*)!!!!!!!!!!!*)
127 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
128 (* *** generate1: not impl.for Empty_Tac_ !!!!!!!!!!(*#3#*)!!!!!!!!!!!*)
129 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
130 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
131 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
132 (*---------------------------------------------------------------------*)
134 case nxt of (_, End_Proof') => ()
135 | _ => error "script.sml, doesnt find Substitute #3";
136 (*---------------------------------------------------------------------*)
137 (*the reason, that next_tac didnt find the 2nd Substitute, was that
138 the Take inbetween was missing, and thus the 2nd Substitute was applied
139 the last formula in ctree, and not to argument from script*)
140 ========== inhibit exn AK110721 ================================================*)
143 "----------- WN0509 Substitute 2nd part --------------------------";
144 "----------- WN0509 Substitute 2nd part --------------------------";
145 "----------- WN0509 Substitute 2nd part --------------------------";
146 (*replace met 'IntegrierenUndKonstanteBestimmen' with this script...*)
147 val str = (*Substitute ; Substitute works*)
148 "Script BiegelinieScript " ^
149 "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
150 "(rb_rb::bool list) (rm_rm::bool list) = "^
151 (*begin after the 2nd integrate*)
152 " (let M__M = Take (M_b v_v = q__q); " ^
153 " e1__e1 = nth_nth 1 rm_rm ; " ^
154 " (x1__x1::real) = argument_in (lhs e1__e1); " ^
155 " (M1__M1::bool) = Substitute [v_v = x1__x1] M__M; " ^
156 " M1__M1 = Substitute [e1__e1] M1__M1 " ^
159 val sc' = ((inst_abs thy) o term_of o the o (parse thy)) str;
162 val str = (*Substitute @@ Substitute does NOT work???*)
163 "Script BiegelinieScript " ^
164 "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
165 "(rb_rb::bool list) (rm_rm::bool list) = "^
166 (*begin after the 2nd integrate*)
167 " (let M__M = Take (M_b v_v = q__q); " ^
168 " e1__e1 = nth_nth 1 rm_rm ; " ^
169 " (x1__x1::real) = argument_in (lhs e1__e1); " ^
170 " (M1__M1::bool) = ((Substitute [v_v = x1__x1]) @@ " ^
171 " (Substitute [e1__e1])) M__M " ^
175 val {scr = Script sc,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
176 (*---------------------------------------------------------------------
177 if sc = sc' then () else error "script.sml, doesnt find Substitute #1";
178 ---------------------------------------------------------------------*)
179 val fmz = ["Traegerlaenge L",
180 "Streckenlast (- q_0 * x^^^2 / 2 + x * c + c_2)",
182 "RandbedingungenBiegung [y 0 = 0, y L = 0]",
183 "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
184 "FunktionsVariable x"];
186 ("Biegelinie",["MomentBestimmte","Biegelinien"],
187 ["IntegrierenUndKonstanteBestimmen"]);
188 val p = e_pos'; val c = [];
189 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
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; val (p,_,f,nxt,_,pt) = me nxt p c pt;
193 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
194 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
195 val (p,_,f,nxt,_,pt) = me nxt p c pt;
196 val (p,_,f,nxt,_,pt) = me nxt p c pt;
197 case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()
198 | _ => error "script.sml, doesnt find Substitute #2";
200 (*========== inhibit exn AK110721 ================================================
201 (* ERROR: caused by f2str f *)
203 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f(*------------------------*);
204 trace_rewrite:=false;
205 (*Exception TYPE raised:
206 Illegal type for constant "HOL.eq" :: "[real, bool] => bool"
207 Atools.argument'_in (Tools.lhs (ListG.nth_ (1 + -1 + -1) [])) =
208 ListG.nth_ (1 + -1 + -1) []
211 ("Illegal type for constant \"op =\" :: \"[real, bool] => bool\"",
213 [Const ("HOL.Trueprop", "bool => prop") $
214 (Const ("HOL.eq", "[RealDef.real, bool] => bool") $ ... $ ...)])
216 ... this was because eval_argument_in took "argument_in (lhs (M_b 0 = 0))"
217 ie. the argument had not been simplified before ^^^^^^^^^^^^^^^
218 thus corrected eval_argument_in OK*)
219 ========== inhibit exn AK110721 ================================================*)
221 val {srls,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
222 val e1__e1 = str2term "nth_nth 1 [M_b 0 = 0, M_b L = 0]";
223 val e1__e1 = eval_listexpr_ @{theory Biegelinie} srls e1__e1; term2str e1__e1;
225 (*========== inhibit exn 110721 ================================================
227 TRIAL: Should be the same
228 term2str e1__e1 = "M_b 0 = 0";
231 if term2str e1__e1 = "M_b 0 = 0"
233 else error"script.sml diff.beh. eval_listexpr_ nth_nth 1 [...";
234 ========== inhibit exn 110721 ================================================*)
236 (*TODO.WN050913 ??? doesnt eval_listexpr_ go into subterms ???...
237 val x1__ = str2term"argument_in (lhs (M_b 0 = 0))";
238 val x1__ = eval_listexpr_ Biegelinie.thy srls x1__; term2str x1__;
240 calculate_ Biegelinie.thy ("Tools.lhs", eval_rhs"eval_lhs_") x1__;
241 val SOME (str, t) = eval_lhs 0 "Tools.lhs" (str2term"lhs (M_b 0 = 0)") 0;*)
243 val l__l = str2term "lhs (M_b 0 = 0)";
244 (*AK110722 eval_listexpr_ is prob. without _ ????*)
245 val l__l = eval_listexpr_ @{theory Biegelinie} srls l__l; term2str l__l;
246 val SOME (str, t) = eval_lhs 0 "Tools.lhs" (str2term "lhs (M_b 0 = 0)") 0;
247 (*========== inhibit exn 110721 ================================================
249 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f (*------------------------*);
250 trace_rewrite:=false;
251 ========== inhibit exn 110721 ================================================*)
255 "----------- fun sel_appl_atomic_tacs ----------------------------";
256 "----------- fun sel_appl_atomic_tacs ----------------------------";
257 "----------- fun sel_appl_atomic_tacs ----------------------------";
260 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
261 ("Test", ["sqroot-test","univariate","equation","test"],
262 ["Test","squ-equ-test-subpbl1"]))];
265 autoCalculate 1 CompleteCalcHead;
266 autoCalculate 1 (Step 1);
267 autoCalculate 1 (Step 1);
268 val ((pt, p), _) = get_calc 1; show_pt pt;
269 val appltacs = sel_appl_atomic_tacs pt p;
271 (*========== inhibit exn AK110721 ================================================
272 (*(*These SHOULD be the same*)
275 [Rewrite ("radd_commute", "?m + ?n = ?n + ?m"),
276 Rewrite ("radd_assoc", "?m + ?n + ?k = ?m + (?n + ?k)"),
277 Calculate "TIMES"];*)
280 [Rewrite ("radd_commute", "?m + ?n = ?n + ?m"),
281 Rewrite ("radd_assoc", "?m + ?n + ?k = ?m + (?n + ?k)"),
282 Calculate "TIMES"] then ()
283 else error "script.sml fun sel_appl_atomic_tacs diff.behav.";
284 ========== inhibit exn AK110721 ================================================*)
286 trace_script := true;
287 trace_script := false;
288 applyTactic 1 p (hd appltacs);
289 val ((pt, p), _) = get_calc 1; show_pt pt;
290 val appltacs = sel_appl_atomic_tacs pt p;
292 (*(* AK110722 Debugging start*)
293 (*applyTactic 1 p (hd appltacs); WAS assy: call by ([3], Pbl)*)
294 "~~~~~ fun applyTactic, args:"; val ((cI:calcID), ip, tac) = (1, p, (hd appltacs));
295 val ((pt, _), _) = get_calc cI;
296 val p = get_pos cI 1;
302 (*locatetac tac (pt, ip); (*WAS assy: call by ([3], Pbl)*)*)
303 "~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, ip));
304 val (mI,m) = mk_tac'_ tac;
306 applicable_in p pt m ; (*Appl*)
308 member op = specsteps mI; (*false*)
310 (*loc_solve_ (mI,m) ptp; (*Argument: (mI, m) : string * tac Reason: Can't unify tac_ with tac*)*)
311 loc_solve_; (*without _ ??? result is -> lOc writing error ???*)
312 (*val it = fn: string * tac_ -> ptree * (pos * pos_) -> lOc_*)
313 (mI,m); (*string * tac*)
314 ptp (*ptree * pos'*);
316 "~~~~~ fun loc_solve_, args:"; val (m ,(pt,pos)) = ((mI,m), ptp);
317 (*val (msg, cs') = solve m (pt, pos);
318 (*Argument: m : string * tac Reason: Can't unify tac_ with tac (Different type constructors)*)*)
323 "~~~~~ fun solve, args:"; val ((mI,m), (pt, po as (p,p_))) = (m, (pt, pos));
324 (*solve has still p_!!!!!!!!!!!!!!!!!!!!!!!!!*)
326 e_metID = get_obj g_metID pt (par_pblobj pt p); (*false*)
327 val ctxt = get_ctxt pt po;
329 (*generate1 (assoc_thy (get_obj g_domID pt (par_pblobj pt p))) m (e_istate, ctxt) (p,p_) pt;
330 (*Argument: m : tac Reason: Can't unify tac_ with tac (Different type constructors)*)*)
331 (assoc_thy (get_obj g_domID pt (par_pblobj pt p)));
334 (*not finished - error continues in fun generate1*)
335 (* AK110722 Debugging end*)*)
336 (*========== inhibit exn AK110721 ================================================
337 "----- WN080102 these vvv do not work, because locatetac starts the search" ^
339 (* AK110722 ERROR: assy: call by ([3], Pbl) *)
340 applyTactic 1 p (hd appltacs);
341 ============ inhibit exn AK110721 ==============================================*)
343 autoCalculate 1 CompleteCalc;
345 "----------- fun init_form, fun get_stac -------------------------";
346 "----------- fun init_form, fun get_stac -------------------------";
347 "----------- fun init_form, fun get_stac -------------------------";
348 val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
349 val (dI',pI',mI') = ("Test",["sqroot-test","univariate","equation","test"],
350 ["Test","squ-equ-test-subpbl1"]);
351 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
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 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
357 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
358 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
359 "~~~~~ fun me, args:"; val (_,tac) = nxt;
360 "~~~~~ fun locatetac, args:"; val ptp as (pt, p) = (pt, p);
361 val (mI,m) = mk_tac'_ tac;
362 val Appl m = applicable_in p pt m;
363 member op = specsteps mI; (*false*)
364 "~~~~~ fun loc_solve_, args:"; val (m, (pt, pos) ) = ((mI, m), ptp);
365 "~~~~~ fun solve, args:"; val (("Apply_Method", Apply_Method' (mI,_,_,_)), pos as (p,_)) = (m, pos);
366 val {srls, ...} = get_met mI;
367 val PblObj {meth=itms, ...} = get_obj I pt p;
368 val thy' = get_obj g_domID pt p;
369 val thy = assoc_thy thy';
370 val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI;
371 val ini = init_form thy sc env;
372 "----- fun init_form, args:"; val (Script sc) = sc;
373 "----- fun get_stac, args:"; val (y, h $ body) = (thy, sc);
374 case get_stac thy sc of SOME (Free ("e_e", _)) => ()
375 | _ => error "script: Const (?, ?) in script (as term) changed";;
378 "----------- x+1=2 start SubProblem 'stac2tac_ TODO: no match for ";
379 "----------- x+1=2 start SubProblem 'stac2tac_ TODO: no match for ";
380 "----------- x+1=2 start SubProblem 'stac2tac_ TODO: no match for ";
381 val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
383 ("Test", ["sqroot-test","univariate","equation","test"],
384 ["Test","squ-equ-test-subpbl1"]);
385 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
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;
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; WAS: Empty_Tac, helpless*)
397 "~~~~~ fun me, args:"; val (_,tac) = nxt;
398 val (pt, p) = case locatetac tac (pt,p) of
399 ("ok", (_, _, ptp)) => ptp | _ => error "script.sml locatetac";
400 "~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
401 val pIopt = get_pblID (pt,ip); (*SOME ["linear", "univariate", "equation", "test"]*)
403 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*)
404 "~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
405 (*WAS stac2tac_ TODO: no match for SubProblem*)
406 val thy' = get_obj g_domID pt (par_pblobj pt p);
407 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
408 "~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt,(p,_)):ptree * pos'), (sc as Script (h $ body)),
409 (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
410 l; (*= [R, L, R, L, R, R]*)
411 val Appy (m', scrst as (_,_,_,v,_,_)) = nstep_up thy ptp sc E l Skip_ a v;
412 "~~~~~ dont like to go into nstep_up...";
413 val t = str2term ("SubProblem" ^
414 "(Test', [linear, univariate, equation, test], [Test, solve_linear])" ^
415 "[BOOL (-1 + x = 0), REAL x]");
416 val (tac, tac_) = stac2tac_ pt @{theory "Isac"} t; (*WAS stac2tac_ TODO: no match for SubProblem*)
419 | _ => error "script.sml x+1=2 start SubProblem from script";
422 "----------- x+1=2 set ctxt in Subproblem ------------------------";
423 "----------- x+1=2 set ctxt in Subproblem ------------------------";
424 "----------- x+1=2 set ctxt in Subproblem ------------------------";