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 "-----------------------------------------------------------------";
15 "-----------------------------------------------------------------";
16 "-----------------------------------------------------------------";
18 val thy= @{theory Isac};
20 "----------- WN0509 why does next_tac doesnt find Substitute -----";
21 "----------- WN0509 why does next_tac doesnt find Substitute -----";
22 "----------- WN0509 why does next_tac doesnt find Substitute -----";
24 (*replace met 'IntegrierenUndKonstanteBestimmen' with this script...*)
26 "Script BiegelinieScript " ^
27 "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
28 "(rb_rb::bool list) (rm_rm::bool list) = " ^
29 " (let q___q = Take (M_b v_v = q__q); " ^
30 " (M1__M1::bool) = ((Substitute [v_v = 0])) q___q " ^
33 val sc' = ((inst_abs thy) o term_of o the o (parse thy)) str;
36 "Script BiegelinieScript " ^
37 "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
38 "(rb_rb::bool list) (rm_rm::bool list) = " ^
39 " (M1__M1::bool) = ((Substitute [v_v = 0]) @@ " ^
40 " in True)";(*..doesnt find Substitute with ..@@ !!!!!!!!!!!!!!!!!!!!!*)
43 "Script BiegelinieScript " ^
44 "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
45 "(rb_rb::bool list) (rm_rm::bool list) = " ^
46 " (let q___q = Take (q_q v_v = q__q); " ^
47 " (M1__M1::bool) = Substitute [v_v = 0] q___q ; " ^
48 " M1__m1 = Substitute [M_b 0 = 0] M1__M1 " ^
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 [v_v = 1] q___q ; " ^
58 " M1__M1 = Substitute [v_v = 2] q___q ; " ^
59 " M1__M1 = Substitute [v_v = 3] q___q ; " ^
60 " M1__M1 = Substitute [M_b 0 = 0] M1__M1 " ^
64 "Script BiegelinieScript " ^
65 "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
66 "(rb_rb::bool list) (rm_rm::bool list) = " ^
67 " (let q___q = Take (M_b v_v = q__q); " ^
68 " (M1__M1::bool) = Substitute [v_v = 0] q___q ; " ^
69 " M2__M2 = Take q___q ; " ^
70 " M2__M2 = Substitute [v_v = 2] q___q " ^
74 val sc' = ((inst_abs thy) o term_of o the o (parse thy)) str;
77 val {scr = Script sc,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
78 (*---------------------------------------------------------------------
79 if sc = sc' then () else error"script.sml, doesnt find Substitute #1";
80 ---------------------------------------------------------------------*)
82 "----------- WN0509 Substitute 2nd part --------------------------";
83 "----------- WN0509 Substitute 2nd part --------------------------";
84 "----------- WN0509 Substitute 2nd part --------------------------";
85 (*replace met 'IntegrierenUndKonstanteBestimmen' with this script...*)
86 val str = (*Substitute ; Substitute works*)
87 "Script BiegelinieScript " ^
88 "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
89 "(rb_rb::bool list) (rm_rm::bool list) = "^
90 (*begin after the 2nd integrate*)
91 " (let M__M = Take (M_b v_v = q__q); " ^
92 " e1__e1 = nth_nth 1 rm_rm ; " ^
93 " (x1__x1::real) = argument_in (lhs e1__e1); " ^
94 " (M1__M1::bool) = Substitute [v_v = x1__x1] M__M; " ^
95 " M1__M1 = Substitute [e1__e1] M1__M1 " ^
98 val sc' = ((inst_abs thy) o term_of o the o (parse thy)) str;
101 val str = (*Substitute @@ Substitute does NOT work???*)
102 "Script BiegelinieScript " ^
103 "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
104 "(rb_rb::bool list) (rm_rm::bool list) = "^
105 (*begin after the 2nd integrate*)
106 " (let M__M = Take (M_b v_v = q__q); " ^
107 " e1__e1 = nth_nth 1 rm_rm ; " ^
108 " (x1__x1::real) = argument_in (lhs e1__e1); " ^
109 " (M1__M1::bool) = ((Substitute [v_v = x1__x1]) @@ " ^
110 " (Substitute [e1__e1])) M__M " ^
114 val {scr = Script sc,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
115 (*---------------------------------------------------------------------
116 if sc = sc' then () else error "script.sml, doesnt find Substitute #1";
117 ---------------------------------------------------------------------*)
118 val fmz = ["Traegerlaenge L",
119 "Streckenlast (- q_0 * x^^^2 / 2 + x * c + c_2)",
121 "RandbedingungenBiegung [y 0 = 0, y L = 0]",
122 "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
123 "FunktionsVariable x"];
125 ("Biegelinie",["MomentBestimmte","Biegelinien"],
126 ["IntegrierenUndKonstanteBestimmen"]);
127 val p = e_pos'; val c = [];
128 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
129 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
130 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
131 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
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;
135 val (p,_,f,nxt,_,pt) = me nxt p c pt;
136 case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()
137 | _ => error "script.sml, doesnt find Substitute #2";
139 (*========== inhibit exn AK110721 ================================================
140 (* ERROR: caused by f2str f *)
142 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f(*------------------------*);
143 trace_rewrite:=false;
144 (*Exception TYPE raised:
145 Illegal type for constant "HOL.eq" :: "[real, bool] => bool"
146 Atools.argument'_in (Tools.lhs (ListG.nth_ (1 + -1 + -1) [])) =
147 ListG.nth_ (1 + -1 + -1) []
150 ("Illegal type for constant \"op =\" :: \"[real, bool] => bool\"",
152 [Const ("HOL.Trueprop", "bool => prop") $
153 (Const ("HOL.eq", "[RealDef.real, bool] => bool") $ ... $ ...)])
155 ... this was because eval_argument_in took "argument_in (lhs (M_b 0 = 0))"
156 ie. the argument had not been simplified before ^^^^^^^^^^^^^^^
157 thus corrected eval_argument_in OK*)
158 ========== inhibit exn AK110721 ================================================*)
160 val {srls,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
161 val e1__e1 = str2term "nth_nth 1 [M_b 0 = 0, M_b L = 0]";
162 val e1__e1 = eval_listexpr_ @{theory Biegelinie} srls e1__e1; term2str e1__e1;
164 (*========== inhibit exn 110721 ================================================
166 TRIAL: Should be the same
167 term2str e1__e1 = "M_b 0 = 0";
170 if term2str e1__e1 = "M_b 0 = 0"
172 else error"script.sml diff.beh. eval_listexpr_ nth_nth 1 [...";
173 ========== inhibit exn 110721 ================================================*)
175 (*TODO.WN050913 ??? doesnt eval_listexpr_ go into subterms ???...
176 val x1__ = str2term"argument_in (lhs (M_b 0 = 0))";
177 val x1__ = eval_listexpr_ Biegelinie.thy srls x1__; term2str x1__;
179 calculate_ Biegelinie.thy ("Tools.lhs", eval_rhs"eval_lhs_") x1__;
180 val SOME (str, t) = eval_lhs 0 "Tools.lhs" (str2term"lhs (M_b 0 = 0)") 0;*)
182 val l__l = str2term "lhs (M_b 0 = 0)";
183 (*AK110722 eval_listexpr_ is prob. without _ ????*)
184 val l__l = eval_listexpr_ @{theory Biegelinie} srls l__l; term2str l__l;
185 val SOME (str, t) = eval_lhs 0 "Tools.lhs" (str2term "lhs (M_b 0 = 0)") 0;
186 (*========== inhibit exn 110721 ================================================
188 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f (*------------------------*);
189 trace_rewrite:=false;
190 ========== inhibit exn 110721 ================================================*)
194 "----------- fun sel_appl_atomic_tacs ----------------------------";
195 "----------- fun sel_appl_atomic_tacs ----------------------------";
196 "----------- fun sel_appl_atomic_tacs ----------------------------";
199 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
200 ("Test", ["sqroot-test","univariate","equation","test"],
201 ["Test","squ-equ-test-subpbl1"]))];
204 autoCalculate 1 CompleteCalcHead;
205 autoCalculate 1 (Step 1);
206 autoCalculate 1 (Step 1);
207 val ((pt, p), _) = get_calc 1; show_pt pt;
208 val appltacs = sel_appl_atomic_tacs pt p;
210 (*========== inhibit exn AK110721 ================================================
211 (*(*These SHOULD be the same*)
214 [Rewrite ("radd_commute", "?m + ?n = ?n + ?m"),
215 Rewrite ("radd_assoc", "?m + ?n + ?k = ?m + (?n + ?k)"),
216 Calculate "TIMES"];*)
219 [Rewrite ("radd_commute", "?m + ?n = ?n + ?m"),
220 Rewrite ("radd_assoc", "?m + ?n + ?k = ?m + (?n + ?k)"),
221 Calculate "TIMES"] then ()
222 else error "script.sml fun sel_appl_atomic_tacs diff.behav.";
223 ========== inhibit exn AK110721 ================================================*)
225 trace_script := true;
226 trace_script := false;
227 applyTactic 1 p (hd appltacs);
228 val ((pt, p), _) = get_calc 1; show_pt pt;
229 val appltacs = sel_appl_atomic_tacs pt p;
231 (*(* AK110722 Debugging start*)
232 (*applyTactic 1 p (hd appltacs); WAS assy: call by ([3], Pbl)*)
233 "~~~~~ fun applyTactic, args:"; val ((cI:calcID), ip, tac) = (1, p, (hd appltacs));
234 val ((pt, _), _) = get_calc cI;
235 val p = get_pos cI 1;
241 (*locatetac tac (pt, ip); (*WAS assy: call by ([3], Pbl)*)*)
242 "~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, ip));
243 val (mI,m) = mk_tac'_ tac;
245 applicable_in p pt m ; (*Appl*)
247 member op = specsteps mI; (*false*)
249 (*loc_solve_ (mI,m) ptp; (*Argument: (mI, m) : string * tac Reason: Can't unify tac_ with tac*)*)
250 loc_solve_; (*without _ ??? result is -> lOc writing error ???*)
251 (*val it = fn: string * tac_ -> ptree * (pos * pos_) -> lOc_*)
252 (mI,m); (*string * tac*)
253 ptp (*ptree * pos'*);
255 "~~~~~ fun loc_solve_, args:"; val (m ,(pt,pos)) = ((mI,m), ptp);
256 (*val (msg, cs') = solve m (pt, pos);
257 (*Argument: m : string * tac Reason: Can't unify tac_ with tac (Different type constructors)*)*)
262 "~~~~~ fun solve, args:"; val ((mI,m), (pt, po as (p,p_))) = (m, (pt, pos));
263 (*solve has still p_!!!!!!!!!!!!!!!!!!!!!!!!!*)
265 e_metID = get_obj g_metID pt (par_pblobj pt p); (*false*)
266 val ctxt = get_ctxt pt po;
268 (*generate1 (assoc_thy (get_obj g_domID pt (par_pblobj pt p))) m (e_istate, ctxt) (p,p_) pt;
269 (*Argument: m : tac Reason: Can't unify tac_ with tac (Different type constructors)*)*)
270 (assoc_thy (get_obj g_domID pt (par_pblobj pt p)));
273 (*not finished - error continues in fun generate1*)
274 (* AK110722 Debugging end*)*)
275 (*========== inhibit exn AK110721 ================================================
276 "----- WN080102 these vvv do not work, because locatetac starts the search" ^
278 (* AK110722 ERROR: assy: call by ([3], Pbl) *)
279 applyTactic 1 p (hd appltacs);
280 ============ inhibit exn AK110721 ==============================================*)
282 autoCalculate 1 CompleteCalc;
284 "----------- fun init_form, fun get_stac -------------------------";
285 "----------- fun init_form, fun get_stac -------------------------";
286 "----------- fun init_form, fun get_stac -------------------------";
287 val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
288 val (dI',pI',mI') = ("Test",["sqroot-test","univariate","equation","test"],
289 ["Test","squ-equ-test-subpbl1"]);
290 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
291 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
292 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
293 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
294 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
295 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
296 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
297 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
298 "~~~~~ fun me, args:"; val (_,tac) = nxt;
299 "~~~~~ fun locatetac, args:"; val ptp as (pt, p) = (pt, p);
300 val (mI,m) = mk_tac'_ tac;
301 val Appl m = applicable_in p pt m;
302 member op = specsteps mI; (*false*)
303 "~~~~~ fun loc_solve_, args:"; val (m, (pt, pos) ) = ((mI, m), ptp);
304 "~~~~~ fun solve, args:"; val (("Apply_Method", Apply_Method' (mI,_,_,_)), pos as (p,_)) = (m, pos);
305 val {srls, ...} = get_met mI;
306 val PblObj {meth=itms, ...} = get_obj I pt p;
307 val thy' = get_obj g_domID pt p;
308 val thy = assoc_thy thy';
309 val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI;
310 val ini = init_form thy sc env;
311 "----- fun init_form, args:"; val (Script sc) = sc;
312 "----- fun get_stac, args:"; val (y, h $ body) = (thy, sc);
313 case get_stac thy sc of SOME (Free ("e_e", _)) => ()
314 | _ => error "script: Const (?, ?) in script (as term) changed";;
317 "----------- x+1=2 start SubProblem 'stac2tac_ TODO: no match for ";
318 "----------- x+1=2 start SubProblem 'stac2tac_ TODO: no match for ";
319 "----------- x+1=2 start SubProblem 'stac2tac_ TODO: no match for ";
320 val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
322 ("Test", ["sqroot-test","univariate","equation","test"],
323 ["Test","squ-equ-test-subpbl1"]);
324 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
325 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
326 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
327 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
328 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
329 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
330 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
331 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
332 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
333 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
334 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt; WAS: Empty_Tac, helpless*)
336 "~~~~~ fun me, args:"; val (_,tac) = nxt;
337 val (pt, p) = case locatetac tac (pt,p) of
338 ("ok", (_, _, ptp)) => ptp | _ => error "script.sml locatetac";
339 "~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
340 val pIopt = get_pblID (pt,ip); (*SOME ["linear", "univariate", "equation", "test"]*)
342 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*)
343 "~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
344 (*WAS stac2tac_ TODO: no match for SubProblem*)
345 val thy' = get_obj g_domID pt (par_pblobj pt p);
346 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
347 "~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt,(p,_)):ptree * pos'), (sc as Script (h $ body)),
348 (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
349 l; (*= [R, L, R, L, R, R]*)
350 val Appy (m', scrst as (_,_,_,v,_,_)) = nstep_up thy ptp sc E l Skip_ a v;
351 "~~~~~ dont like to go into nstep_up...";
352 val t = str2term ("SubProblem" ^
353 "(Test', [linear, univariate, equation, test], [Test, solve_linear])" ^
354 "[BOOL (-1 + x = 0), REAL x]");
355 val (tac, tac_) = stac2tac_ pt @{theory "Isac"} t; (*WAS stac2tac_ TODO: no match for SubProblem*)
358 | _ => error "script.sml x+1=2 start SubProblem from script";
361 "----------- Take as 1st stac in script --------------------------";
362 "----------- Take as 1st stac in script --------------------------";
363 "----------- Take as 1st stac in script --------------------------";
364 val p = e_pos'; val c = [];
365 val (p,_,f,nxt,_,pt) =
367 [(["functionTerm (x^^^2 + 1)", "integrateBy x", "antiDerivative FF"],
368 ("Integrate", ["integrate","function"], ["diff","integration"]))];
369 val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = ("Tac ", ...) --> Add_Given...*)
370 val (p,_,f,nxt,_,pt) = me nxt p c pt;
371 val (p,_,f,nxt,_,pt) = me nxt p c pt;
372 val (p,_,f,nxt,_,pt) = me nxt p c pt;
373 val (p,_,f,nxt,_,pt) = me nxt p c pt;
374 val (p,_,f,nxt,_,pt) = me nxt p c pt;
375 val (p,_,f,nxt,_,pt) = me nxt p c pt;
376 case nxt of (_, Apply_Method ["diff", "integration"]) => ()
377 | _ => error "integrate.sml -- me method [diff,integration] -- spec";
378 "----- step 8: returns nxt = Rewrite_Set_Inst ([\"(bdv, x)\"],\"integration\")";
380 "~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ptree)) = (nxt, p, c, pt);
381 "~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
382 val (mI,m) = mk_tac'_ tac;
383 val Appl m = applicable_in p pt m;
384 member op = specsteps mI (*false*);
385 "~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = ((mI,m), ptp);
386 "~~~~~ fun solve, args:"; val ((_, m as Apply_Method' (mI, _, _, _)), (pt, (pos as (p,_)))) =
388 val {srls, ...} = get_met mI;
389 val PblObj {meth=itms, ...} = get_obj I pt p;
390 val thy' = get_obj g_domID pt p;
391 val thy = assoc_thy thy';
392 val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI;
393 val ini = init_form thy sc env;
396 val (m', (is', ctxt'), _) = next_tac (thy', srls) (pt, (p, Res)) sc (is, ctxt);
397 val d = e_rls (*FIXME: get simplifier from domID*);
398 "~~~~~ fun locate_gen, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ptree * pos'),
399 (scr as Script (h $ body),d), (ScrState (E,l,a,v,S,b), ctxt)) =
400 ((thy',srls), m', (pt,(p, Res)), (sc,d), (is', ctxt'));
401 val thy = assoc_thy thy';
402 l = [] orelse ((*init.in solve..Apply_Method...*)
403 (last_elem o fst) p = 0 andalso snd p = Res); (*true*)
404 "~~~~~ fun assy, args:"; val (ya, (is as (E,l,a,v,S,b),ss),
405 (Const ("HOL.Let",_) $ e $ (Abs (id,T,body)))) =
406 ((thy',ctxt,srls,d,Aundef), ((E,[R],a,v,S,b), [(m,EmptyMout,pt,p,[])]), body);
407 (*check: true*) term2str e = "Take (Integral f_f D v_v)";
408 "~~~~~ fun assy, args:"; val ((thy',ctxt,sr,d,ap), (is as (E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss), t) =
409 (ya, ((E , l@[L,R], a,v,S,b),ss), e);
410 val (a', STac stac) = handle_leaf "locate" thy' sr E a v t;
411 (* val ctxt = get_ctxt pt (p,p_)
412 exception PTREE "get_obj: pos = [0] does not exist" raised
413 (line 908 of "/usr/local/isabisac/src/Tools/isac/Interpret/ctree.sml")*)