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_::real) (q__::real) (v_::real) (b_::real=>real) \
27 \(rb_::bool list) (rm_::bool list) = \
28 \ (let q___ = Take (M_b v_v = q__); \
29 \ (M1__::bool) = ((Substitute [v_ = 0])) q___ \
31 (*========== inhibit exn 110721 ================================================
32 val sc' = ((inst_abs thy) o term_of o the o (parse thy)) str;
33 (========= inhibit exn 110721 ================================================*)
36 "Script BiegelinieScript \
37 \(l_::real) (q__::real) (v_::real) (b_::real=>real) \
38 \(rb_::bool list) (rm_::bool list) = \
39 \ (let q___ = Take (q_ v_v = q__); \
40 \ (M1__::bool) = ((Substitute [v_ = 0]) @@ \
41 \ (Substitute [M_b 0 = 0])) q___ \
42 \ in True)";(*..doesnt find Substitute with ..@@ !!!!!!!!!!!!!!!!!!!!!*)
45 "Script BiegelinieScript \
46 \(l_::real) (q__::real) (v_::real) (b_::real=>real) \
47 \(rb_::bool list) (rm_::bool list) = \
48 \ (let q___ = Take (q_ v_v = q__); \
49 \ (M1__::bool) = Substitute [v_ = 0] q___ ; \
50 \ M1__ = Substitute [M_b 0 = 0] M1__ \
54 "Script BiegelinieScript \
55 \(l_::real) (q__::real) (v_::real) (b_::real=>real) \
56 \(rb_::bool list) (rm_::bool list) = \
57 \ (let q___ = Take (q_ v_v = q__); \
58 \ (M1__::bool) = Substitute [v_ = 0] q___ ; \
59 \ M1__ = Substitute [v_ = 1] q___ ; \
60 \ M1__ = Substitute [v_ = 2] q___ ; \
61 \ M1__ = Substitute [v_ = 3] q___ ; \
62 \ M1__ = Substitute [M_b 0 = 0] M1__ \
66 "Script BiegelinieScript \
67 \(l_::real) (q__::real) (v_::real) (b_::real=>real) \
68 \(rb_::bool list) (rm_::bool list) = \
69 \ (let q___ = Take (M_b v_v = q__); \
70 \ (M1__::bool) = Substitute [v_ = 0] q___ ; \
71 \ M2__ = Take q___ ; \
72 \ M2__ = Substitute [v_ = 2] 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";
110 (*========== inhibit exn 110721 ================================================
111 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
112 (* *** generate1: not impl.for Substitute' !!!!!!!!!!(*#1#*)!!!!!!!!!!!*)
113 (* val nxt = ("Check_Postcond",.. !!!!!!!!!!!!!!!!!!!(*#2#*)!!!!!!!!!!!*)
115 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
116 (* *** generate1: not impl.for Empty_Tac_ !!!!!!!!!!(*#3#*)!!!!!!!!!!!*)
117 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
118 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
119 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
120 (*---------------------------------------------------------------------*)
122 case nxt of (_, End_Proof') => ()
123 | _ => error "script.sml, doesnt find Substitute #3";
124 (*---------------------------------------------------------------------*)
125 (*the reason, that next_tac didnt find the 2nd Substitute, was that
126 the Take inbetween was missing, and thus the 2nd Substitute was applied
127 the last formula in ctree, and not to argument from script*)
128 ========== inhibit exn 110721 ================================================*)
132 "----------- WN0509 Substitute 2nd part --------------------------";
133 "----------- WN0509 Substitute 2nd part --------------------------";
134 "----------- WN0509 Substitute 2nd part --------------------------";
135 (*replace met 'IntegrierenUndKonstanteBestimmen' with this script...*)
136 val str = (*Substitute ; Substitute works*)
137 "Script BiegelinieScript \
138 \(l_::real) (q__::real) (v_::real) (b_::real=>real) \
139 \(rb_::bool list) (rm_::bool list) = "^
140 (*begin after the 2nd integrate*)
141 " (let M__ = Take (M_b v_v = q__); \
142 \ e1__ = nth_ 1 rm_ ; \
143 \ (x1__::real) = argument_in (lhs e1__); \
144 \ (M1__::bool) = Substitute [v_ = x1__] M__; \
145 \ M1__ = Substitute [e1__] M1__ \
148 (*========== inhibit exn 110721 ================================================
149 (*---^^^-OK-----------------------------------------------------------------*)
150 val sc' = ((inst_abs thy) o term_of o the o (parse thy)) str;
152 (*---vvv-NOT ok-------------------------------------------------------------*)
153 ========== inhibit exn 110721 ================================================*)
155 val str = (*Substitute @@ Substitute does NOT work???*)
156 "Script BiegelinieScript \
157 \(l_::real) (q__::real) (v_::real) (b_::real=>real) \
158 \(rb_::bool list) (rm_::bool list) = "^
159 (*begin after the 2nd integrate*)
160 " (let M__ = Take (M_b v_v = q__); \
161 \ e1__ = nth_ 1 rm_ ; \
162 \ (x1__::real) = argument_in (lhs e1__); \
163 \ (M1__::bool) = ((Substitute [v_ = x1__]) @@ \
164 \ (Substitute [e1__])) M__ \
168 val {scr=Script sc,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
169 (*---------------------------------------------------------------------
170 if sc = sc' then () else error"script.sml, doesnt find Substitute #1";
171 ---------------------------------------------------------------------*)
172 val fmz = ["Traegerlaenge L",
173 "Streckenlast (- q_0 * x^^^2 / 2 + x * c + c_2)",
175 "RandbedingungenBiegung [y 0 = 0, y L = 0]",
176 "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
177 "FunktionsVariable x"];
179 ("Biegelinie",["MomentBestimmte","Biegelinien"],
180 ["IntegrierenUndKonstanteBestimmen"]);
181 val p = e_pos'; val c = [];
182 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
183 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
184 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
185 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
186 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
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;
189 val (p,_,f,nxt,_,pt) = me nxt p c pt;
190 case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()
191 | _ => error "script.sml, doesnt find Substitute #2";
193 (*========== inhibit exn 110721 ================================================
195 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f(*------------------------*);
196 trace_rewrite:=false;
197 (*Exception TYPE raised:
198 Illegal type for constant "HOL.eq" :: "[real, bool] => bool"
199 Atools.argument'_in (Tools.lhs (ListG.nth_ (1 + -1 + -1) [])) =
200 ListG.nth_ (1 + -1 + -1) []
203 ("Illegal type for constant \"op =\" :: \"[real, bool] => bool\"",
205 [Const ("HOL.Trueprop", "bool => prop") $
206 (Const ("HOL.eq", "[RealDef.real, bool] => bool") $ ... $ ...)])
208 ... this was because eval_argument_in took "argument_in (lhs (M_b 0 = 0))"
209 ie. the argument had not been simplified before ^^^^^^^^^^^^^^^
210 thus corrected eval_argument_in OK*)
211 ========== inhibit exn 110721 ================================================*)
213 val {srls,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
214 val e1__ = str2term "nth_nth 1 [M_b 0 = 0, M_b L = 0]";
215 (*========== inhibit exn 110721 ================================================
216 val e1__ = eval_listexpr_ Biegelinie.thy srls e1__; term2str e1__;
218 if term2str e1__ = "M_b 0 = 0" then () else
219 error"script.sml diff.beh. eval_listexpr_ nth_nth 1 [...";
220 ========== inhibit exn 110721 ================================================*)
222 (*TODO.WN050913 ??? doesnt eval_listexpr_ go into subterms ???...
223 val x1__ = str2term"argument_in (lhs (M_b 0 = 0))";
224 val x1__ = eval_listexpr_ Biegelinie.thy srls x1__; term2str x1__;
226 calculate_ Biegelinie.thy ("Tools.lhs", eval_rhs"eval_lhs_") x1__;
227 val SOME (str, t) = eval_lhs 0 "Tools.lhs" (str2term"lhs (M_b 0 = 0)") 0;*)
229 val l__ = str2term"lhs (M_b 0 = 0)";
230 (*========== inhibit exn 110721 ================================================
231 val l__ = eval_listexpr_ Biegelinie.thy srls l__; term2str l__;
232 val SOME (str, t) = eval_lhs 0 "Tools.lhs" (str2term"lhs (M_b 0 = 0)") 0;
236 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f(*------------------------*);
237 trace_rewrite:=false;
238 ========== inhibit exn 110721 ================================================*)
242 "----------- fun sel_appl_atomic_tacs ----------------------------";
243 "----------- fun sel_appl_atomic_tacs ----------------------------";
244 "----------- fun sel_appl_atomic_tacs ----------------------------";
247 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
248 ("Test", ["sqroot-test","univariate","equation","test"],
249 ["Test","squ-equ-test-subpbl1"]))];
252 autoCalculate 1 CompleteCalcHead;
253 autoCalculate 1 (Step 1);
254 autoCalculate 1 (Step 1);
255 val ((pt, p), _) = get_calc 1; show_pt pt;
256 val appltacs = sel_appl_atomic_tacs pt p;
259 (*These SHOULD be the same*)
262 [Rewrite ("radd_commute", "?m + ?n = ?n + ?m"),
263 Rewrite ("radd_assoc", "?m + ?n + ?k = ?m + (?n + ?k)"),
264 Calculate "times"];*)
266 (*========== inhibit exn 110721 ================================================
268 [Rewrite ("radd_commute", "?m + ?n = ?n + ?m"),
269 Rewrite ("radd_assoc", "?m + ?n + ?k = ?m + (?n + ?k)"),
270 Calculate "times"] then ()
271 else error "script.sml fun sel_appl_atomic_tacs diff.behav.";
272 ========== inhibit exn 110721 ================================================*)
274 trace_script := true;
275 trace_script := false;
276 applyTactic 1 p (hd appltacs);
277 val ((pt, p), _) = get_calc 1; show_pt pt;
278 val appltacs = sel_appl_atomic_tacs pt p;
280 (*========== inhibit exn 110721 ================================================
281 "----- WN080102 these vvv do not work, because locatetac starts the search\
283 (* ERROR: assy: call by ([3], Pbl) *)
284 applyTactic 1 p (hd appltacs);
285 autoCalculate 1 CompleteCalc;
286 ============ inhibit exn 110721 ==============================================*)
288 "----------- fun init_form, fun get_stac -------------------------";
289 "----------- fun init_form, fun get_stac -------------------------";
290 "----------- fun init_form, fun get_stac -------------------------";
291 val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
292 val (dI',pI',mI') = ("Test",["sqroot-test","univariate","equation","test"],
293 ["Test","squ-equ-test-subpbl1"]);
294 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
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 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
299 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
300 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
301 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
302 "~~~~~ fun me, args:"; val (_,tac) = nxt;
303 "~~~~~ fun locatetac, args:"; val ptp as (pt, p) = (pt, p);
304 val (mI,m) = mk_tac'_ tac;
305 val Appl m = applicable_in p pt m;
306 member op = specsteps mI; (*false*)
307 "~~~~~ fun loc_solve_, args:"; val (m, (pt, pos) ) = ((mI, m), ptp);
308 "~~~~~ fun solve, args:"; val (("Apply_Method", Apply_Method' (mI,_,_,_)), pos as (p,_)) = (m, pos);
309 val {srls, ...} = get_met mI;
310 val PblObj {meth=itms, ...} = get_obj I pt p;
311 val thy' = get_obj g_domID pt p;
312 val thy = assoc_thy thy';
313 val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI;
314 val ini = init_form thy sc env;
315 "----- fun init_form, args:"; val (Script sc) = sc;
316 "----- fun get_stac, args:"; val (y, h $ body) = (thy, sc);
317 case get_stac thy sc of SOME (Free ("e_e", _)) => ()
318 | _ => error "script: Const (?, ?) in script (as term) changed";;
321 "----------- x+1=2 start SubProblem 'stac2tac_ TODO: no match for ";
322 "----------- x+1=2 start SubProblem 'stac2tac_ TODO: no match for ";
323 "----------- x+1=2 start SubProblem 'stac2tac_ TODO: no match for ";
324 val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
326 ("Test", ["sqroot-test","univariate","equation","test"],
327 ["Test","squ-equ-test-subpbl1"]);
328 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
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;
335 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
336 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
337 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
338 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt; WAS: Empty_Tac, helpless*)
340 "~~~~~ fun me, args:"; val (_,tac) = nxt;
341 val (pt, p) = case locatetac tac (pt,p) of
342 ("ok", (_, _, ptp)) => ptp | _ => error "script.sml locatetac";
343 "~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
344 val pIopt = get_pblID (pt,ip); (*SOME ["linear", "univariate", "equation", "test"]*)
346 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*)
347 "~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
348 (*WAS stac2tac_ TODO: no match for SubProblem*)
349 val thy' = get_obj g_domID pt (par_pblobj pt p);
350 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
351 "~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt,(p,_)):ptree * pos'), (sc as Script (h $ body)),
352 (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
353 l; (*= [R, L, R, L, R, R]*)
354 val Appy (m', scrst as (_,_,_,v,_,_)) = nstep_up thy ptp sc E l Skip_ a v;
355 "~~~~~ dont like to go into nstep_up...";
356 val t = str2term ("SubProblem" ^
357 "(Test', [linear, univariate, equation, test], [Test, solve_linear])" ^
358 "[BOOL (-1 + x = 0), REAL x]");
359 val (tac, tac_) = stac2tac_ pt @{theory "Isac"} t; (*WAS stac2tac_ TODO: no match for SubProblem*)
362 | _ => error "script.sml x+1=2 start SubProblem from script";
365 "----------- x+1=2 set ctxt in Subproblem ------------------------";
366 "----------- x+1=2 set ctxt in Subproblem ------------------------";
367 "----------- x+1=2 set ctxt in Subproblem ------------------------";