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 "-----------------------------------------------------------------";
18 "-----------------------------------------------------------------";
19 "-----------------------------------------------------------------";
21 (*========== inhibit exn 110503 ================================================
23 "----------- WN0509 why does next_tac doesnt find Substitute -----";
24 "----------- WN0509 why does next_tac doesnt find Substitute -----";
25 "----------- WN0509 why does next_tac doesnt find Substitute -----";
27 (*replace met 'IntegrierenUndKonstanteBestimmen' with this script...*)
29 "Script BiegelinieScript \
30 \(l_::real) (q__::real) (v_::real) (b_::real=>real) \
31 \(rb_::bool list) (rm_::bool list) = \
32 \ (let q___ = Take (M_b v_v = q__); \
33 \ (M1__::bool) = ((Substitute [v_ = 0])) q___ \
35 val sc' = ((inst_abs thy) o term_of o the o (parse thy)) str;
38 "Script BiegelinieScript \
39 \(l_::real) (q__::real) (v_::real) (b_::real=>real) \
40 \(rb_::bool list) (rm_::bool list) = \
41 \ (let q___ = Take (q_ v_v = q__); \
42 \ (M1__::bool) = ((Substitute [v_ = 0]) @@ \
43 \ (Substitute [M_b 0 = 0])) q___ \
44 \ in True)";(*..doesnt find Substitute with ..@@ !!!!!!!!!!!!!!!!!!!!!*)
47 "Script BiegelinieScript \
48 \(l_::real) (q__::real) (v_::real) (b_::real=>real) \
49 \(rb_::bool list) (rm_::bool list) = \
50 \ (let q___ = Take (q_ v_v = q__); \
51 \ (M1__::bool) = Substitute [v_ = 0] q___ ; \
52 \ M1__ = Substitute [M_b 0 = 0] M1__ \
56 "Script BiegelinieScript \
57 \(l_::real) (q__::real) (v_::real) (b_::real=>real) \
58 \(rb_::bool list) (rm_::bool list) = \
59 \ (let q___ = Take (q_ v_v = q__); \
60 \ (M1__::bool) = Substitute [v_ = 0] q___ ; \
61 \ M1__ = Substitute [v_ = 1] q___ ; \
62 \ M1__ = Substitute [v_ = 2] q___ ; \
63 \ M1__ = Substitute [v_ = 3] q___ ; \
64 \ M1__ = Substitute [M_b 0 = 0] M1__ \
68 "Script BiegelinieScript \
69 \(l_::real) (q__::real) (v_::real) (b_::real=>real) \
70 \(rb_::bool list) (rm_::bool list) = \
71 \ (let q___ = Take (M_b v_v = q__); \
72 \ (M1__::bool) = Substitute [v_ = 0] q___ ; \
73 \ M2__ = Take q___ ; \
74 \ M2__ = Substitute [v_ = 2] q___ \
77 val sc' = ((inst_abs thy) o term_of o the o (parse thy)) str;
79 val {scr=Script sc,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
80 (*---------------------------------------------------------------------
81 if sc = sc' then () else error"script.sml, doesnt find Substitute #1";
82 ---------------------------------------------------------------------*)
84 val fmz = ["Traegerlaenge L",
85 "Streckenlast (- q_0 * x^^^2 / 2 + x * c + c_2)",
87 "RandbedingungenBiegung [y 0 = 0, y L = 0]",
88 "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
89 "FunktionsVariable x"];
91 ("Biegelinie",["MomentBestimmte","Biegelinien"],
92 ["IntegrierenUndKonstanteBestimmen"]);
93 val p = e_pos'; val c = [];
94 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
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;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;
101 val (p,_,f,nxt,_,pt) = me nxt p c pt;
102 case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()
103 | _ => error "script.sml, doesnt find Substitute #2";
104 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
105 (* *** generate1: not impl.for Substitute' !!!!!!!!!!(*#1#*)!!!!!!!!!!!*)
106 (* val nxt = ("Check_Postcond",.. !!!!!!!!!!!!!!!!!!!(*#2#*)!!!!!!!!!!!*)
108 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
109 (* *** generate1: not impl.for Empty_Tac_ !!!!!!!!!!(*#3#*)!!!!!!!!!!!*)
110 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
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 (*---------------------------------------------------------------------*)
114 case nxt of (_, End_Proof') => ()
115 | _ => error "script.sml, doesnt find Substitute #3";
116 (*---------------------------------------------------------------------*)
117 (*the reason, that next_tac didnt find the 2nd Substitute, was that
118 the Take inbetween was missing, and thus the 2nd Substitute was applied
119 the last formula in ctree, and not to argument from script*)
122 "----------- WN0509 Substitute 2nd part --------------------------";
123 "----------- WN0509 Substitute 2nd part --------------------------";
124 "----------- WN0509 Substitute 2nd part --------------------------";
125 (*replace met 'IntegrierenUndKonstanteBestimmen' with this script...*)
126 val str = (*Substitute ; Substitute works*)
127 "Script BiegelinieScript \
128 \(l_::real) (q__::real) (v_::real) (b_::real=>real) \
129 \(rb_::bool list) (rm_::bool list) = "^
130 (*begin after the 2nd integrate*)
131 " (let M__ = Take (M_b v_v = q__); \
132 \ e1__ = nth_ 1 rm_ ; \
133 \ (x1__::real) = argument_in (lhs e1__); \
134 \ (M1__::bool) = Substitute [v_ = x1__] M__; \
135 \ M1__ = Substitute [e1__] M1__ \
138 (*---^^^-OK-----------------------------------------------------------------*)
139 val sc' = ((inst_abs thy) o term_of o the o (parse thy)) str;
141 (*---vvv-NOT ok-------------------------------------------------------------*)
142 val str = (*Substitute @@ Substitute does NOT work???*)
143 "Script BiegelinieScript \
144 \(l_::real) (q__::real) (v_::real) (b_::real=>real) \
145 \(rb_::bool list) (rm_::bool list) = "^
146 (*begin after the 2nd integrate*)
147 " (let M__ = Take (M_b v_v = q__); \
148 \ e1__ = nth_ 1 rm_ ; \
149 \ (x1__::real) = argument_in (lhs e1__); \
150 \ (M1__::bool) = ((Substitute [v_ = x1__]) @@ \
151 \ (Substitute [e1__])) M__ \
155 val {scr=Script sc,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
156 (*---------------------------------------------------------------------
157 if sc = sc' then () else error"script.sml, doesnt find Substitute #1";
158 ---------------------------------------------------------------------*)
159 val fmz = ["Traegerlaenge L",
160 "Streckenlast (- q_0 * x^^^2 / 2 + x * c + c_2)",
162 "RandbedingungenBiegung [y 0 = 0, y L = 0]",
163 "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
164 "FunktionsVariable x"];
166 ("Biegelinie",["MomentBestimmte","Biegelinien"],
167 ["IntegrierenUndKonstanteBestimmen"]);
168 val p = e_pos'; val c = [];
169 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
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;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;
176 val (p,_,f,nxt,_,pt) = me nxt p c pt;
177 case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()
178 | _ => error "script.sml, doesnt find Substitute #2";
180 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f(*------------------------*);
181 trace_rewrite:=false;
182 (*Exception TYPE raised:
183 Illegal type for constant "HOL.eq" :: "[real, bool] => bool"
184 Atools.argument'_in (Tools.lhs (ListG.nth_ (1 + -1 + -1) [])) =
185 ListG.nth_ (1 + -1 + -1) []
188 ("Illegal type for constant \"op =\" :: \"[real, bool] => bool\"",
190 [Const ("HOL.Trueprop", "bool => prop") $
191 (Const ("HOL.eq", "[RealDef.real, bool] => bool") $ ... $ ...)])
193 ... this was because eval_argument_in took "argument_in (lhs (M_b 0 = 0))"
194 ie. the argument had not been simplified before ^^^^^^^^^^^^^^^
195 thus corrected eval_argument_in OK*)
197 val {srls,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
198 val e1__ = str2term"nth_ 1 [M_b 0 = 0, M_b L = 0]";
199 val e1__ = eval_listexpr_ Biegelinie.thy srls e1__; term2str e1__;
200 if term2str e1__ = "M_b 0 = 0" then () else
201 error"script.sml diff.beh. eval_listexpr_ nth_ 1 [...";
203 (*TODO.WN050913 ??? doesnt eval_listexpr_ go into subterms ???...
204 val x1__ = str2term"argument_in (lhs (M_b 0 = 0))";
205 val x1__ = eval_listexpr_ Biegelinie.thy srls x1__; term2str x1__;
207 calculate_ Biegelinie.thy ("Tools.lhs", eval_rhs"eval_lhs_") x1__;
208 val SOME (str, t) = eval_lhs 0 "Tools.lhs" (str2term"lhs (M_b 0 = 0)") 0;*)
210 val l__ = str2term"lhs (M_b 0 = 0)";
211 val l__ = eval_listexpr_ Biegelinie.thy srls l__; term2str l__;
212 val SOME (str, t) = eval_lhs 0 "Tools.lhs" (str2term"lhs (M_b 0 = 0)") 0;
216 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f(*------------------------*);
217 trace_rewrite:=false;
221 "----------- fun sel_appl_atomic_tacs ----------------------------";
222 "----------- fun sel_appl_atomic_tacs ----------------------------";
223 "----------- fun sel_appl_atomic_tacs ----------------------------";
225 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
226 ("Test", ["sqroot-test","univariate","equation","test"],
227 ["Test","squ-equ-test-subpbl1"]))];
230 autoCalculate 1 CompleteCalcHead;
231 autoCalculate 1 (Step 1);
232 autoCalculate 1 (Step 1);
233 val ((pt, p), _) = get_calc 1; show_pt pt;
234 val appltacs = sel_appl_atomic_tacs pt p;
236 [Rewrite ("radd_commute", "?m + ?n = ?n + ?m"),
237 Rewrite ("radd_assoc", "?m + ?n + ?k = ?m + (?n + ?k)"),
238 Calculate "times"] then ()
239 else error "script.sml fun sel_appl_atomic_tacs diff.behav.";
241 trace_script := true;
242 trace_script := false;
243 applyTactic 1 p (hd appltacs);
244 val ((pt, p), _) = get_calc 1; show_pt pt;
245 val appltacs = sel_appl_atomic_tacs pt p;
247 "----- WN080102 these vvv do not work, because locatetac starts the search\
249 applyTactic 1 p (hd appltacs);
250 autoCalculate 1 CompleteCalc;
251 ============ inhibit exn 110503 ==============================================*)
253 "----------- fun init_form, fun get_stac -------------------------";
254 "----------- fun init_form, fun get_stac -------------------------";
255 "----------- fun init_form, fun get_stac -------------------------";
256 val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
257 val (dI',pI',mI') = ("Test",["sqroot-test","univariate","equation","test"],
258 ["Test","squ-equ-test-subpbl1"]);
259 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
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 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 "~~~~~ fun me, args:"; val (_,tac) = nxt;
268 "~~~~~ fun locatetac, args:"; val ptp as (pt, p) = (pt, p);
269 val (mI,m) = mk_tac'_ tac;
270 val Appl m = applicable_in p pt m;
271 member op = specsteps mI; (*false*)
272 "~~~~~ fun loc_solve_, args:"; val (m, (pt, pos) ) = ((mI, m), ptp);
273 "~~~~~ fun solve, args:"; val (("Apply_Method", Apply_Method' (mI,_,_,_)), pos as (p,_)) = (m, pos);
274 val {srls, ...} = get_met mI;
275 val PblObj {meth=itms, ...} = get_obj I pt p;
276 val thy' = get_obj g_domID pt p;
277 val thy = assoc_thy thy';
278 val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI;
279 val ini = init_form thy sc env;
280 "----- fun init_form, args:"; val (Script sc) = sc;
281 "----- fun get_stac, args:"; val (y, h $ body) = (thy, sc);
282 case get_stac thy sc of SOME (Free ("e_e", _)) => ()
283 | _ => error "script: Const (?, ?) in script (as term) changed";;
286 "----------- x+1=2 start SubProblem 'stac2tac_ TODO: no match for ";
287 "----------- x+1=2 start SubProblem 'stac2tac_ TODO: no match for ";
288 "----------- x+1=2 start SubProblem 'stac2tac_ TODO: no match for ";
289 val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
291 ("Test", ["sqroot-test","univariate","equation","test"],
292 ["Test","squ-equ-test-subpbl1"]);
293 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
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;
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; WAS: Empty_Tac, helpless*)
305 "~~~~~ fun me, args:"; val (_,tac) = nxt;
306 val (pt, p) = case locatetac tac (pt,p) of
307 ("ok", (_, _, ptp)) => ptp | _ => error "script.sml locatetac";
308 "~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
309 val pIopt = get_pblID (pt,ip);
311 pIopt; (*= SOME ["sqroot-test", "univariate", ...]*)
312 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*)
313 "~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
314 (*WAS stac2tac_ TODO: no match for SubProblem*)
315 val thy' = get_obj g_domID pt (par_pblobj pt p);
316 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
317 "~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt,(p,_)):ptree * pos'), (sc as Script (h $ body)),
318 (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
319 l; (*= [R, L, R, L, R, R]*)
320 val Appy (m', scrst as (_,_,_,v,_,_)) = nstep_up thy ptp sc E l Skip_ a v;
321 "~~~~~ dont like to go into nstep_up...";
322 val t = str2term ("SubProblem" ^
323 "(Test', [linear, univariate, equation, test], [Test, solve_linear])" ^
324 "[BOOL (-1 + x = 0), REAL x]");
325 val (tac, tac_) = stac2tac_ pt @{theory "Isac"} t; (*WAS stac2tac_ TODO: no match for SubProblem*)
328 | _ => error "script.sml x+1=2 start SubProblem from script";