intermed. ctxt ..: ctxt correct after Apply_Method in sub-method
this is checked in Minisubpbl/400-start-meth-subpbl.sml
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 (*========== inhibit exn 110503 ================================================
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_::real) (q__::real) (v_::real) (b_::real=>real) \
28 \(rb_::bool list) (rm_::bool list) = \
29 \ (let q___ = Take (M_b v_v = q__); \
30 \ (M1__::bool) = ((Substitute [v_ = 0])) q___ \
32 val sc' = ((inst_abs thy) o term_of o the o (parse thy)) str;
35 "Script BiegelinieScript \
36 \(l_::real) (q__::real) (v_::real) (b_::real=>real) \
37 \(rb_::bool list) (rm_::bool list) = \
38 \ (let q___ = Take (q_ v_v = q__); \
39 \ (M1__::bool) = ((Substitute [v_ = 0]) @@ \
40 \ (Substitute [M_b 0 = 0])) q___ \
41 \ in True)";(*..doesnt find Substitute with ..@@ !!!!!!!!!!!!!!!!!!!!!*)
44 "Script BiegelinieScript \
45 \(l_::real) (q__::real) (v_::real) (b_::real=>real) \
46 \(rb_::bool list) (rm_::bool list) = \
47 \ (let q___ = Take (q_ v_v = q__); \
48 \ (M1__::bool) = Substitute [v_ = 0] q___ ; \
49 \ M1__ = Substitute [M_b 0 = 0] M1__ \
53 "Script BiegelinieScript \
54 \(l_::real) (q__::real) (v_::real) (b_::real=>real) \
55 \(rb_::bool list) (rm_::bool list) = \
56 \ (let q___ = Take (q_ v_v = q__); \
57 \ (M1__::bool) = Substitute [v_ = 0] q___ ; \
58 \ M1__ = Substitute [v_ = 1] q___ ; \
59 \ M1__ = Substitute [v_ = 2] q___ ; \
60 \ M1__ = Substitute [v_ = 3] q___ ; \
61 \ M1__ = Substitute [M_b 0 = 0] M1__ \
65 "Script BiegelinieScript \
66 \(l_::real) (q__::real) (v_::real) (b_::real=>real) \
67 \(rb_::bool list) (rm_::bool list) = \
68 \ (let q___ = Take (M_b v_v = q__); \
69 \ (M1__::bool) = Substitute [v_ = 0] q___ ; \
70 \ M2__ = Take q___ ; \
71 \ M2__ = Substitute [v_ = 2] q___ \
74 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"];
88 ("Biegelinie",["MomentBestimmte","Biegelinien"],
89 ["IntegrierenUndKonstanteBestimmen"]);
90 val p = e_pos'; val c = [];
91 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
92 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
93 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
94 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
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;
98 val (p,_,f,nxt,_,pt) = me nxt p c pt;
99 case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()
100 | _ => error "script.sml, doesnt find Substitute #2";
101 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
102 (* *** generate1: not impl.for Substitute' !!!!!!!!!!(*#1#*)!!!!!!!!!!!*)
103 (* val nxt = ("Check_Postcond",.. !!!!!!!!!!!!!!!!!!!(*#2#*)!!!!!!!!!!!*)
105 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
106 (* *** generate1: not impl.for Empty_Tac_ !!!!!!!!!!(*#3#*)!!!!!!!!!!!*)
107 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
108 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
109 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
110 (*---------------------------------------------------------------------*)
111 case nxt of (_, End_Proof') => ()
112 | _ => error "script.sml, doesnt find Substitute #3";
113 (*---------------------------------------------------------------------*)
114 (*the reason, that next_tac didnt find the 2nd Substitute, was that
115 the Take inbetween was missing, and thus the 2nd Substitute was applied
116 the last formula in ctree, and not to argument from script*)
119 "----------- WN0509 Substitute 2nd part --------------------------";
120 "----------- WN0509 Substitute 2nd part --------------------------";
121 "----------- WN0509 Substitute 2nd part --------------------------";
122 (*replace met 'IntegrierenUndKonstanteBestimmen' with this script...*)
123 val str = (*Substitute ; Substitute works*)
124 "Script BiegelinieScript \
125 \(l_::real) (q__::real) (v_::real) (b_::real=>real) \
126 \(rb_::bool list) (rm_::bool list) = "^
127 (*begin after the 2nd integrate*)
128 " (let M__ = Take (M_b v_v = q__); \
129 \ e1__ = nth_ 1 rm_ ; \
130 \ (x1__::real) = argument_in (lhs e1__); \
131 \ (M1__::bool) = Substitute [v_ = x1__] M__; \
132 \ M1__ = Substitute [e1__] M1__ \
135 (*---^^^-OK-----------------------------------------------------------------*)
136 val sc' = ((inst_abs thy) o term_of o the o (parse thy)) str;
138 (*---vvv-NOT ok-------------------------------------------------------------*)
139 val str = (*Substitute @@ Substitute does NOT work???*)
140 "Script BiegelinieScript \
141 \(l_::real) (q__::real) (v_::real) (b_::real=>real) \
142 \(rb_::bool list) (rm_::bool list) = "^
143 (*begin after the 2nd integrate*)
144 " (let M__ = Take (M_b v_v = q__); \
145 \ e1__ = nth_ 1 rm_ ; \
146 \ (x1__::real) = argument_in (lhs e1__); \
147 \ (M1__::bool) = ((Substitute [v_ = x1__]) @@ \
148 \ (Substitute [e1__])) M__ \
152 val {scr=Script sc,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
153 (*---------------------------------------------------------------------
154 if sc = sc' then () else error"script.sml, doesnt find Substitute #1";
155 ---------------------------------------------------------------------*)
156 val fmz = ["Traegerlaenge L",
157 "Streckenlast (- q_0 * x^^^2 / 2 + x * c + c_2)",
159 "RandbedingungenBiegung [y 0 = 0, y L = 0]",
160 "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
161 "FunktionsVariable x"];
163 ("Biegelinie",["MomentBestimmte","Biegelinien"],
164 ["IntegrierenUndKonstanteBestimmen"]);
165 val p = e_pos'; val c = [];
166 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
167 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
168 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
169 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
170 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
171 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
172 val (p,_,f,nxt,_,pt) = me nxt p c pt;
173 val (p,_,f,nxt,_,pt) = me nxt p c pt;
174 case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()
175 | _ => error "script.sml, doesnt find Substitute #2";
177 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f(*------------------------*);
178 trace_rewrite:=false;
179 (*Exception TYPE raised:
180 Illegal type for constant "HOL.eq" :: "[real, bool] => bool"
181 Atools.argument'_in (Tools.lhs (ListG.nth_ (1 + -1 + -1) [])) =
182 ListG.nth_ (1 + -1 + -1) []
185 ("Illegal type for constant \"op =\" :: \"[real, bool] => bool\"",
187 [Const ("HOL.Trueprop", "bool => prop") $
188 (Const ("HOL.eq", "[RealDef.real, bool] => bool") $ ... $ ...)])
190 ... this was because eval_argument_in took "argument_in (lhs (M_b 0 = 0))"
191 ie. the argument had not been simplified before ^^^^^^^^^^^^^^^
192 thus corrected eval_argument_in OK*)
194 val {srls,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
195 val e1__ = str2term"nth_ 1 [M_b 0 = 0, M_b L = 0]";
196 val e1__ = eval_listexpr_ Biegelinie.thy srls e1__; term2str e1__;
197 if term2str e1__ = "M_b 0 = 0" then () else
198 error"script.sml diff.beh. eval_listexpr_ nth_ 1 [...";
200 (*TODO.WN050913 ??? doesnt eval_listexpr_ go into subterms ???...
201 val x1__ = str2term"argument_in (lhs (M_b 0 = 0))";
202 val x1__ = eval_listexpr_ Biegelinie.thy srls x1__; term2str x1__;
204 calculate_ Biegelinie.thy ("Tools.lhs", eval_rhs"eval_lhs_") x1__;
205 val SOME (str, t) = eval_lhs 0 "Tools.lhs" (str2term"lhs (M_b 0 = 0)") 0;*)
207 val l__ = str2term"lhs (M_b 0 = 0)";
208 val l__ = eval_listexpr_ Biegelinie.thy srls l__; term2str l__;
209 val SOME (str, t) = eval_lhs 0 "Tools.lhs" (str2term"lhs (M_b 0 = 0)") 0;
213 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f(*------------------------*);
214 trace_rewrite:=false;
218 "----------- fun sel_appl_atomic_tacs ----------------------------";
219 "----------- fun sel_appl_atomic_tacs ----------------------------";
220 "----------- fun sel_appl_atomic_tacs ----------------------------";
222 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
223 ("Test", ["sqroot-test","univariate","equation","test"],
224 ["Test","squ-equ-test-subpbl1"]))];
227 autoCalculate 1 CompleteCalcHead;
228 autoCalculate 1 (Step 1);
229 autoCalculate 1 (Step 1);
230 val ((pt, p), _) = get_calc 1; show_pt pt;
231 val appltacs = sel_appl_atomic_tacs pt p;
233 [Rewrite ("radd_commute", "?m + ?n = ?n + ?m"),
234 Rewrite ("radd_assoc", "?m + ?n + ?k = ?m + (?n + ?k)"),
235 Calculate "times"] then ()
236 else error "script.sml fun sel_appl_atomic_tacs diff.behav.";
238 trace_script := true;
239 trace_script := false;
240 applyTactic 1 p (hd appltacs);
241 val ((pt, p), _) = get_calc 1; show_pt pt;
242 val appltacs = sel_appl_atomic_tacs pt p;
244 "----- WN080102 these vvv do not work, because locatetac starts the search\
246 applyTactic 1 p (hd appltacs);
247 autoCalculate 1 CompleteCalc;
248 ============ inhibit exn 110503 ==============================================*)
250 "----------- fun init_form, fun get_stac -------------------------";
251 "----------- fun init_form, fun get_stac -------------------------";
252 "----------- fun init_form, fun get_stac -------------------------";
253 val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
254 val (dI',pI',mI') = ("Test",["sqroot-test","univariate","equation","test"],
255 ["Test","squ-equ-test-subpbl1"]);
256 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
257 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
258 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
259 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
260 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
261 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
262 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
263 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
264 "~~~~~ fun me, args:"; val (_,tac) = nxt;
265 "~~~~~ fun locatetac, args:"; val ptp as (pt, p) = (pt, p);
266 val (mI,m) = mk_tac'_ tac;
267 val Appl m = applicable_in p pt m;
268 member op = specsteps mI; (*false*)
269 "~~~~~ fun loc_solve_, args:"; val (m, (pt, pos) ) = ((mI, m), ptp);
270 "~~~~~ fun solve, args:"; val (("Apply_Method", Apply_Method' (mI,_,_,_)), pos as (p,_)) = (m, pos);
271 val {srls, ...} = get_met mI;
272 val PblObj {meth=itms, ...} = get_obj I pt p;
273 val thy' = get_obj g_domID pt p;
274 val thy = assoc_thy thy';
275 val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI;
276 val ini = init_form thy sc env;
277 "----- fun init_form, args:"; val (Script sc) = sc;
278 "----- fun get_stac, args:"; val (y, h $ body) = (thy, sc);
279 case get_stac thy sc of SOME (Free ("e_e", _)) => ()
280 | _ => error "script: Const (?, ?) in script (as term) changed";;
283 "----------- x+1=2 start SubProblem 'stac2tac_ TODO: no match for ";
284 "----------- x+1=2 start SubProblem 'stac2tac_ TODO: no match for ";
285 "----------- x+1=2 start SubProblem 'stac2tac_ TODO: no match for ";
286 val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
288 ("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 [1] pt;
292 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
293 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
294 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
295 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
296 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
297 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
298 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
299 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
300 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt; WAS: Empty_Tac, helpless*)
302 "~~~~~ fun me, args:"; val (_,tac) = nxt;
303 val (pt, p) = case locatetac tac (pt,p) of
304 ("ok", (_, _, ptp)) => ptp | _ => error "script.sml locatetac";
305 "~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
306 val pIopt = get_pblID (pt,ip); (*SOME ["linear", "univariate", "equation", "test"]*)
308 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*)
309 "~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
310 (*WAS stac2tac_ TODO: no match for SubProblem*)
311 val thy' = get_obj g_domID pt (par_pblobj pt p);
312 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
313 "~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt,(p,_)):ptree * pos'), (sc as Script (h $ body)),
314 (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
315 l; (*= [R, L, R, L, R, R]*)
316 val Appy (m', scrst as (_,_,_,v,_,_)) = nstep_up thy ptp sc E l Skip_ a v;
317 "~~~~~ dont like to go into nstep_up...";
318 val t = str2term ("SubProblem" ^
319 "(Test', [linear, univariate, equation, test], [Test, solve_linear])" ^
320 "[BOOL (-1 + x = 0), REAL x]");
321 val (tac, tac_) = stac2tac_ pt @{theory "Isac"} t; (*WAS stac2tac_ TODO: no match for SubProblem*)
324 | _ => error "script.sml x+1=2 start SubProblem from script";
327 "----------- x+1=2 set ctxt in Subproblem ------------------------";
328 "----------- x+1=2 set ctxt in Subproblem ------------------------";
329 "----------- x+1=2 set ctxt in Subproblem ------------------------";