intermed. ctxt ..: Add_Given doesnt work due to wrong ctxt in Subproblem
cleanup before getting ctxt into Subproblem usable for x+1=2
1 (* tests for ME/script.sml
2 TODO.WN0509 collect typical tests from systest here !!!!!
3 author: Walther Neuper 050908
4 (c) copyright due to lincense terms.
6 use"../smltest/ME/script.sml";
9 "-----------------------------------------------------------------";
10 "table of contents -----------------------------------------------";
11 "-----------------------------------------------------------------";
12 "----------- WN0509 why does next_tac doesnt find Substitute -----";
13 "----------- WN0509 Substitute 2nd part --------------------------";
14 "----------- fun sel_appl_atomic_tacs ----------------------------";
15 "----------- fun init_form, fun get_stac -------------------------";
16 "----------- x+1=2 start SubProblem 'stac2tac_ TODO: no match for ";
17 "----------- x+1=2 set ctxt in Subproblem ------------------------";
18 "-----------------------------------------------------------------";
19 "-----------------------------------------------------------------";
20 "-----------------------------------------------------------------";
22 (*========== inhibit exn 110503 ================================================
24 "----------- WN0509 why does next_tac doesnt find Substitute -----";
25 "----------- WN0509 why does next_tac doesnt find Substitute -----";
26 "----------- WN0509 why does next_tac doesnt find Substitute -----";
28 (*replace met 'IntegrierenUndKonstanteBestimmen' with this script...*)
30 "Script BiegelinieScript \
31 \(l_::real) (q__::real) (v_::real) (b_::real=>real) \
32 \(rb_::bool list) (rm_::bool list) = \
33 \ (let q___ = Take (M_b v_v = q__); \
34 \ (M1__::bool) = ((Substitute [v_ = 0])) q___ \
36 val sc' = ((inst_abs thy) o term_of o the o (parse thy)) str;
39 "Script BiegelinieScript \
40 \(l_::real) (q__::real) (v_::real) (b_::real=>real) \
41 \(rb_::bool list) (rm_::bool list) = \
42 \ (let q___ = Take (q_ v_v = q__); \
43 \ (M1__::bool) = ((Substitute [v_ = 0]) @@ \
44 \ (Substitute [M_b 0 = 0])) q___ \
45 \ in True)";(*..doesnt find Substitute with ..@@ !!!!!!!!!!!!!!!!!!!!!*)
48 "Script BiegelinieScript \
49 \(l_::real) (q__::real) (v_::real) (b_::real=>real) \
50 \(rb_::bool list) (rm_::bool list) = \
51 \ (let q___ = Take (q_ v_v = q__); \
52 \ (M1__::bool) = Substitute [v_ = 0] q___ ; \
53 \ M1__ = Substitute [M_b 0 = 0] M1__ \
57 "Script BiegelinieScript \
58 \(l_::real) (q__::real) (v_::real) (b_::real=>real) \
59 \(rb_::bool list) (rm_::bool list) = \
60 \ (let q___ = Take (q_ v_v = q__); \
61 \ (M1__::bool) = Substitute [v_ = 0] q___ ; \
62 \ M1__ = Substitute [v_ = 1] q___ ; \
63 \ M1__ = Substitute [v_ = 2] q___ ; \
64 \ M1__ = Substitute [v_ = 3] q___ ; \
65 \ M1__ = Substitute [M_b 0 = 0] M1__ \
69 "Script BiegelinieScript \
70 \(l_::real) (q__::real) (v_::real) (b_::real=>real) \
71 \(rb_::bool list) (rm_::bool list) = \
72 \ (let q___ = Take (M_b v_v = q__); \
73 \ (M1__::bool) = Substitute [v_ = 0] q___ ; \
74 \ M2__ = Take q___ ; \
75 \ M2__ = Substitute [v_ = 2] q___ \
78 val sc' = ((inst_abs thy) o term_of o the o (parse thy)) str;
80 val {scr=Script sc,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
81 (*---------------------------------------------------------------------
82 if sc = sc' then () else error"script.sml, doesnt find Substitute #1";
83 ---------------------------------------------------------------------*)
85 val fmz = ["Traegerlaenge L",
86 "Streckenlast (- q_0 * x^^^2 / 2 + x * c + c_2)",
88 "RandbedingungenBiegung [y 0 = 0, y L = 0]",
89 "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
90 "FunktionsVariable x"];
92 ("Biegelinie",["MomentBestimmte","Biegelinien"],
93 ["IntegrierenUndKonstanteBestimmen"]);
94 val p = e_pos'; val c = [];
95 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
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;val (p,_,f,nxt,_,pt) = me nxt p c pt;
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;
102 val (p,_,f,nxt,_,pt) = me nxt p c pt;
103 case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()
104 | _ => error "script.sml, doesnt find Substitute #2";
105 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
106 (* *** generate1: not impl.for Substitute' !!!!!!!!!!(*#1#*)!!!!!!!!!!!*)
107 (* val nxt = ("Check_Postcond",.. !!!!!!!!!!!!!!!!!!!(*#2#*)!!!!!!!!!!!*)
109 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
110 (* *** generate1: not impl.for Empty_Tac_ !!!!!!!!!!(*#3#*)!!!!!!!!!!!*)
111 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
112 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
113 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
114 (*---------------------------------------------------------------------*)
115 case nxt of (_, End_Proof') => ()
116 | _ => error "script.sml, doesnt find Substitute #3";
117 (*---------------------------------------------------------------------*)
118 (*the reason, that next_tac didnt find the 2nd Substitute, was that
119 the Take inbetween was missing, and thus the 2nd Substitute was applied
120 the last formula in ctree, and not to argument from script*)
123 "----------- WN0509 Substitute 2nd part --------------------------";
124 "----------- WN0509 Substitute 2nd part --------------------------";
125 "----------- WN0509 Substitute 2nd part --------------------------";
126 (*replace met 'IntegrierenUndKonstanteBestimmen' with this script...*)
127 val str = (*Substitute ; Substitute works*)
128 "Script BiegelinieScript \
129 \(l_::real) (q__::real) (v_::real) (b_::real=>real) \
130 \(rb_::bool list) (rm_::bool list) = "^
131 (*begin after the 2nd integrate*)
132 " (let M__ = Take (M_b v_v = q__); \
133 \ e1__ = nth_ 1 rm_ ; \
134 \ (x1__::real) = argument_in (lhs e1__); \
135 \ (M1__::bool) = Substitute [v_ = x1__] M__; \
136 \ M1__ = Substitute [e1__] M1__ \
139 (*---^^^-OK-----------------------------------------------------------------*)
140 val sc' = ((inst_abs thy) o term_of o the o (parse thy)) str;
142 (*---vvv-NOT ok-------------------------------------------------------------*)
143 val str = (*Substitute @@ Substitute does NOT work???*)
144 "Script BiegelinieScript \
145 \(l_::real) (q__::real) (v_::real) (b_::real=>real) \
146 \(rb_::bool list) (rm_::bool list) = "^
147 (*begin after the 2nd integrate*)
148 " (let M__ = Take (M_b v_v = q__); \
149 \ e1__ = nth_ 1 rm_ ; \
150 \ (x1__::real) = argument_in (lhs e1__); \
151 \ (M1__::bool) = ((Substitute [v_ = x1__]) @@ \
152 \ (Substitute [e1__])) M__ \
156 val {scr=Script sc,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
157 (*---------------------------------------------------------------------
158 if sc = sc' then () else error"script.sml, doesnt find Substitute #1";
159 ---------------------------------------------------------------------*)
160 val fmz = ["Traegerlaenge L",
161 "Streckenlast (- q_0 * x^^^2 / 2 + x * c + c_2)",
163 "RandbedingungenBiegung [y 0 = 0, y L = 0]",
164 "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
165 "FunktionsVariable x"];
167 ("Biegelinie",["MomentBestimmte","Biegelinien"],
168 ["IntegrierenUndKonstanteBestimmen"]);
169 val p = e_pos'; val c = [];
170 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
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;val (p,_,f,nxt,_,pt) = me nxt p c pt;
173 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
174 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
175 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
176 val (p,_,f,nxt,_,pt) = me nxt p c pt;
177 val (p,_,f,nxt,_,pt) = me nxt p c pt;
178 case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()
179 | _ => error "script.sml, doesnt find Substitute #2";
181 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f(*------------------------*);
182 trace_rewrite:=false;
183 (*Exception TYPE raised:
184 Illegal type for constant "HOL.eq" :: "[real, bool] => bool"
185 Atools.argument'_in (Tools.lhs (ListG.nth_ (1 + -1 + -1) [])) =
186 ListG.nth_ (1 + -1 + -1) []
189 ("Illegal type for constant \"op =\" :: \"[real, bool] => bool\"",
191 [Const ("HOL.Trueprop", "bool => prop") $
192 (Const ("HOL.eq", "[RealDef.real, bool] => bool") $ ... $ ...)])
194 ... this was because eval_argument_in took "argument_in (lhs (M_b 0 = 0))"
195 ie. the argument had not been simplified before ^^^^^^^^^^^^^^^
196 thus corrected eval_argument_in OK*)
198 val {srls,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
199 val e1__ = str2term"nth_ 1 [M_b 0 = 0, M_b L = 0]";
200 val e1__ = eval_listexpr_ Biegelinie.thy srls e1__; term2str e1__;
201 if term2str e1__ = "M_b 0 = 0" then () else
202 error"script.sml diff.beh. eval_listexpr_ nth_ 1 [...";
204 (*TODO.WN050913 ??? doesnt eval_listexpr_ go into subterms ???...
205 val x1__ = str2term"argument_in (lhs (M_b 0 = 0))";
206 val x1__ = eval_listexpr_ Biegelinie.thy srls x1__; term2str x1__;
208 calculate_ Biegelinie.thy ("Tools.lhs", eval_rhs"eval_lhs_") x1__;
209 val SOME (str, t) = eval_lhs 0 "Tools.lhs" (str2term"lhs (M_b 0 = 0)") 0;*)
211 val l__ = str2term"lhs (M_b 0 = 0)";
212 val l__ = eval_listexpr_ Biegelinie.thy srls l__; term2str l__;
213 val SOME (str, t) = eval_lhs 0 "Tools.lhs" (str2term"lhs (M_b 0 = 0)") 0;
217 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f(*------------------------*);
218 trace_rewrite:=false;
222 "----------- fun sel_appl_atomic_tacs ----------------------------";
223 "----------- fun sel_appl_atomic_tacs ----------------------------";
224 "----------- fun sel_appl_atomic_tacs ----------------------------";
226 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
227 ("Test", ["sqroot-test","univariate","equation","test"],
228 ["Test","squ-equ-test-subpbl1"]))];
231 autoCalculate 1 CompleteCalcHead;
232 autoCalculate 1 (Step 1);
233 autoCalculate 1 (Step 1);
234 val ((pt, p), _) = get_calc 1; show_pt pt;
235 val appltacs = sel_appl_atomic_tacs pt p;
237 [Rewrite ("radd_commute", "?m + ?n = ?n + ?m"),
238 Rewrite ("radd_assoc", "?m + ?n + ?k = ?m + (?n + ?k)"),
239 Calculate "times"] then ()
240 else error "script.sml fun sel_appl_atomic_tacs diff.behav.";
242 trace_script := true;
243 trace_script := false;
244 applyTactic 1 p (hd appltacs);
245 val ((pt, p), _) = get_calc 1; show_pt pt;
246 val appltacs = sel_appl_atomic_tacs pt p;
248 "----- WN080102 these vvv do not work, because locatetac starts the search\
250 applyTactic 1 p (hd appltacs);
251 autoCalculate 1 CompleteCalc;
252 ============ inhibit exn 110503 ==============================================*)
254 "----------- fun init_form, fun get_stac -------------------------";
255 "----------- fun init_form, fun get_stac -------------------------";
256 "----------- fun init_form, fun get_stac -------------------------";
257 val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
258 val (dI',pI',mI') = ("Test",["sqroot-test","univariate","equation","test"],
259 ["Test","squ-equ-test-subpbl1"]);
260 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
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 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
265 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
266 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
267 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
268 "~~~~~ fun me, args:"; val (_,tac) = nxt;
269 "~~~~~ fun locatetac, args:"; val ptp as (pt, p) = (pt, p);
270 val (mI,m) = mk_tac'_ tac;
271 val Appl m = applicable_in p pt m;
272 member op = specsteps mI; (*false*)
273 "~~~~~ fun loc_solve_, args:"; val (m, (pt, pos) ) = ((mI, m), ptp);
274 "~~~~~ fun solve, args:"; val (("Apply_Method", Apply_Method' (mI,_,_,_)), pos as (p,_)) = (m, pos);
275 val {srls, ...} = get_met mI;
276 val PblObj {meth=itms, ...} = get_obj I pt p;
277 val thy' = get_obj g_domID pt p;
278 val thy = assoc_thy thy';
279 val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI;
280 val ini = init_form thy sc env;
281 "----- fun init_form, args:"; val (Script sc) = sc;
282 "----- fun get_stac, args:"; val (y, h $ body) = (thy, sc);
283 case get_stac thy sc of SOME (Free ("e_e", _)) => ()
284 | _ => error "script: Const (?, ?) in script (as term) changed";;
287 "----------- x+1=2 start SubProblem 'stac2tac_ TODO: no match for ";
288 "----------- x+1=2 start SubProblem 'stac2tac_ TODO: no match for ";
289 "----------- x+1=2 start SubProblem 'stac2tac_ TODO: no match for ";
290 val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
292 ("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 [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;
301 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
302 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
303 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
304 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt; WAS: Empty_Tac, helpless*)
306 "~~~~~ fun me, args:"; val (_,tac) = nxt;
307 val (pt, p) = case locatetac tac (pt,p) of
308 ("ok", (_, _, ptp)) => ptp | _ => error "script.sml locatetac";
309 "~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
310 val pIopt = get_pblID (pt,ip);
312 pIopt; (*= SOME ["sqroot-test", "univariate", ...]*)
313 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*)
314 "~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
315 (*WAS stac2tac_ TODO: no match for SubProblem*)
316 val thy' = get_obj g_domID pt (par_pblobj pt p);
317 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
318 "~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt,(p,_)):ptree * pos'), (sc as Script (h $ body)),
319 (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
320 l; (*= [R, L, R, L, R, R]*)
321 val Appy (m', scrst as (_,_,_,v,_,_)) = nstep_up thy ptp sc E l Skip_ a v;
322 "~~~~~ dont like to go into nstep_up...";
323 val t = str2term ("SubProblem" ^
324 "(Test', [linear, univariate, equation, test], [Test, solve_linear])" ^
325 "[BOOL (-1 + x = 0), REAL x]");
326 val (tac, tac_) = stac2tac_ pt @{theory "Isac"} t; (*WAS stac2tac_ TODO: no match for SubProblem*)
329 | _ => error "script.sml x+1=2 start SubProblem from script";
332 "----------- x+1=2 set ctxt in Subproblem ------------------------";
333 "----------- x+1=2 set ctxt in Subproblem ------------------------";
334 "----------- x+1=2 set ctxt in Subproblem ------------------------";