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 "-----------------------------------------------------------------";
17 "-----------------------------------------------------------------";
18 "-----------------------------------------------------------------";
20 (*========== inhibit exn 110503 ================================================
22 "----------- WN0509 why does next_tac doesnt find Substitute -----";
23 "----------- WN0509 why does next_tac doesnt find Substitute -----";
24 "----------- WN0509 why does next_tac doesnt find Substitute -----";
26 (*replace met 'IntegrierenUndKonstanteBestimmen' with this script...*)
28 "Script BiegelinieScript \
29 \(l_::real) (q__::real) (v_::real) (b_::real=>real) \
30 \(rb_::bool list) (rm_::bool list) = \
31 \ (let q___ = Take (M_b v_v = q__); \
32 \ (M1__::bool) = ((Substitute [v_ = 0])) q___ \
34 val sc' = ((inst_abs thy) o term_of o the o (parse thy)) str;
37 "Script BiegelinieScript \
38 \(l_::real) (q__::real) (v_::real) (b_::real=>real) \
39 \(rb_::bool list) (rm_::bool list) = \
40 \ (let q___ = Take (q_ v_v = q__); \
41 \ (M1__::bool) = ((Substitute [v_ = 0]) @@ \
42 \ (Substitute [M_b 0 = 0])) q___ \
43 \ in True)";(*..doesnt find Substitute with ..@@ !!!!!!!!!!!!!!!!!!!!!*)
46 "Script BiegelinieScript \
47 \(l_::real) (q__::real) (v_::real) (b_::real=>real) \
48 \(rb_::bool list) (rm_::bool list) = \
49 \ (let q___ = Take (q_ v_v = q__); \
50 \ (M1__::bool) = Substitute [v_ = 0] q___ ; \
51 \ M1__ = Substitute [M_b 0 = 0] M1__ \
55 "Script BiegelinieScript \
56 \(l_::real) (q__::real) (v_::real) (b_::real=>real) \
57 \(rb_::bool list) (rm_::bool list) = \
58 \ (let q___ = Take (q_ v_v = q__); \
59 \ (M1__::bool) = Substitute [v_ = 0] q___ ; \
60 \ M1__ = Substitute [v_ = 1] q___ ; \
61 \ M1__ = Substitute [v_ = 2] q___ ; \
62 \ M1__ = Substitute [v_ = 3] q___ ; \
63 \ M1__ = Substitute [M_b 0 = 0] M1__ \
67 "Script BiegelinieScript \
68 \(l_::real) (q__::real) (v_::real) (b_::real=>real) \
69 \(rb_::bool list) (rm_::bool list) = \
70 \ (let q___ = Take (M_b v_v = q__); \
71 \ (M1__::bool) = Substitute [v_ = 0] q___ ; \
72 \ M2__ = Take q___ ; \
73 \ M2__ = Substitute [v_ = 2] q___ \
76 val sc' = ((inst_abs thy) o term_of o the o (parse thy)) str;
78 val {scr=Script sc,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
79 (*---------------------------------------------------------------------
80 if sc = sc' then () else error"script.sml, doesnt find Substitute #1";
81 ---------------------------------------------------------------------*)
83 val fmz = ["Traegerlaenge L",
84 "Streckenlast (- q_0 * x^^^2 / 2 + x * c + c_2)",
86 "RandbedingungenBiegung [y 0 = 0, y L = 0]",
87 "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
88 "FunktionsVariable x"];
90 ("Biegelinie",["MomentBestimmte","Biegelinien"],
91 ["IntegrierenUndKonstanteBestimmen"]);
92 val p = e_pos'; val c = [];
93 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
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;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;
100 val (p,_,f,nxt,_,pt) = me nxt p c pt;
101 case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()
102 | _ => error "script.sml, doesnt find Substitute #2";
103 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
104 (* *** generate1: not impl.for Substitute' !!!!!!!!!!(*#1#*)!!!!!!!!!!!*)
105 (* val nxt = ("Check_Postcond",.. !!!!!!!!!!!!!!!!!!!(*#2#*)!!!!!!!!!!!*)
107 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
108 (* *** generate1: not impl.for Empty_Tac_ !!!!!!!!!!(*#3#*)!!!!!!!!!!!*)
109 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
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 (*---------------------------------------------------------------------*)
113 case nxt of (_, End_Proof') => ()
114 | _ => error "script.sml, doesnt find Substitute #3";
115 (*---------------------------------------------------------------------*)
116 (*the reason, that next_tac didnt find the 2nd Substitute, was that
117 the Take inbetween was missing, and thus the 2nd Substitute was applied
118 the last formula in ctree, and not to argument from script*)
121 "----------- WN0509 Substitute 2nd part --------------------------";
122 "----------- WN0509 Substitute 2nd part --------------------------";
123 "----------- WN0509 Substitute 2nd part --------------------------";
124 (*replace met 'IntegrierenUndKonstanteBestimmen' with this script...*)
125 val str = (*Substitute ; Substitute works*)
126 "Script BiegelinieScript \
127 \(l_::real) (q__::real) (v_::real) (b_::real=>real) \
128 \(rb_::bool list) (rm_::bool list) = "^
129 (*begin after the 2nd integrate*)
130 " (let M__ = Take (M_b v_v = q__); \
131 \ e1__ = nth_ 1 rm_ ; \
132 \ (x1__::real) = argument_in (lhs e1__); \
133 \ (M1__::bool) = Substitute [v_ = x1__] M__; \
134 \ M1__ = Substitute [e1__] M1__ \
137 (*---^^^-OK-----------------------------------------------------------------*)
138 val sc' = ((inst_abs thy) o term_of o the o (parse thy)) str;
140 (*---vvv-NOT ok-------------------------------------------------------------*)
141 val str = (*Substitute @@ Substitute does NOT work???*)
142 "Script BiegelinieScript \
143 \(l_::real) (q__::real) (v_::real) (b_::real=>real) \
144 \(rb_::bool list) (rm_::bool list) = "^
145 (*begin after the 2nd integrate*)
146 " (let M__ = Take (M_b v_v = q__); \
147 \ e1__ = nth_ 1 rm_ ; \
148 \ (x1__::real) = argument_in (lhs e1__); \
149 \ (M1__::bool) = ((Substitute [v_ = x1__]) @@ \
150 \ (Substitute [e1__])) M__ \
154 val {scr=Script sc,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
155 (*---------------------------------------------------------------------
156 if sc = sc' then () else error"script.sml, doesnt find Substitute #1";
157 ---------------------------------------------------------------------*)
158 val fmz = ["Traegerlaenge L",
159 "Streckenlast (- q_0 * x^^^2 / 2 + x * c + c_2)",
161 "RandbedingungenBiegung [y 0 = 0, y L = 0]",
162 "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
163 "FunktionsVariable x"];
165 ("Biegelinie",["MomentBestimmte","Biegelinien"],
166 ["IntegrierenUndKonstanteBestimmen"]);
167 val p = e_pos'; val c = [];
168 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
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;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;
175 val (p,_,f,nxt,_,pt) = me nxt p c pt;
176 case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()
177 | _ => error "script.sml, doesnt find Substitute #2";
179 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f(*------------------------*);
180 trace_rewrite:=false;
181 (*Exception TYPE raised:
182 Illegal type for constant "HOL.eq" :: "[real, bool] => bool"
183 Atools.argument'_in (Tools.lhs (ListG.nth_ (1 + -1 + -1) [])) =
184 ListG.nth_ (1 + -1 + -1) []
187 ("Illegal type for constant \"op =\" :: \"[real, bool] => bool\"",
189 [Const ("HOL.Trueprop", "bool => prop") $
190 (Const ("HOL.eq", "[RealDef.real, bool] => bool") $ ... $ ...)])
192 ... this was because eval_argument_in took "argument_in (lhs (M_b 0 = 0))"
193 ie. the argument had not been simplified before ^^^^^^^^^^^^^^^
194 thus corrected eval_argument_in OK*)
196 val {srls,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
197 val e1__ = str2term"nth_ 1 [M_b 0 = 0, M_b L = 0]";
198 val e1__ = eval_listexpr_ Biegelinie.thy srls e1__; term2str e1__;
199 if term2str e1__ = "M_b 0 = 0" then () else
200 error"script.sml diff.beh. eval_listexpr_ nth_ 1 [...";
202 (*TODO.WN050913 ??? doesnt eval_listexpr_ go into subterms ???...
203 val x1__ = str2term"argument_in (lhs (M_b 0 = 0))";
204 val x1__ = eval_listexpr_ Biegelinie.thy srls x1__; term2str x1__;
206 calculate_ Biegelinie.thy ("Tools.lhs", eval_rhs"eval_lhs_") x1__;
207 val SOME (str, t) = eval_lhs 0 "Tools.lhs" (str2term"lhs (M_b 0 = 0)") 0;*)
209 val l__ = str2term"lhs (M_b 0 = 0)";
210 val l__ = eval_listexpr_ Biegelinie.thy srls l__; term2str l__;
211 val SOME (str, t) = eval_lhs 0 "Tools.lhs" (str2term"lhs (M_b 0 = 0)") 0;
215 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f(*------------------------*);
216 trace_rewrite:=false;
220 "----------- fun sel_appl_atomic_tacs ----------------------------";
221 "----------- fun sel_appl_atomic_tacs ----------------------------";
222 "----------- fun sel_appl_atomic_tacs ----------------------------";
224 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
225 ("Test", ["sqroot-test","univariate","equation","test"],
226 ["Test","squ-equ-test-subpbl1"]))];
229 autoCalculate 1 CompleteCalcHead;
230 autoCalculate 1 (Step 1);
231 autoCalculate 1 (Step 1);
232 val ((pt, p), _) = get_calc 1; show_pt pt;
233 val appltacs = sel_appl_atomic_tacs pt p;
235 [Rewrite ("radd_commute", "?m + ?n = ?n + ?m"),
236 Rewrite ("radd_assoc", "?m + ?n + ?k = ?m + (?n + ?k)"),
237 Calculate "times"] then ()
238 else error "script.sml fun sel_appl_atomic_tacs diff.behav.";
240 trace_script := true;
241 trace_script := false;
242 applyTactic 1 p (hd appltacs);
243 val ((pt, p), _) = get_calc 1; show_pt pt;
244 val appltacs = sel_appl_atomic_tacs pt p;
246 "----- WN080102 these vvv do not work, because locatetac starts the search\
248 applyTactic 1 p (hd appltacs);
249 autoCalculate 1 CompleteCalc;
250 ============ inhibit exn 110503 ==============================================*)
252 "----------- fun init_form, fun get_stac -------------------------";
253 "----------- fun init_form, fun get_stac -------------------------";
254 "----------- fun init_form, fun get_stac -------------------------";
255 val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
256 val (dI',pI',mI') = ("Test",["sqroot-test","univariate","equation","test"],
257 ["Test","squ-equ-test-subpbl1"]);
258 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
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 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
265 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
266 "~~~~~ fun me, args:"; val (_,tac) = nxt;
267 "~~~~~ fun locatetac, args:"; val ptp as (pt, p) = (pt, p);
268 val (mI,m) = mk_tac'_ tac;
269 val Appl m = applicable_in p pt m;
270 member op = specsteps mI; (*false*)
271 "~~~~~ fun loc_solve_, args:"; val (m, (pt, pos) ) = ((mI, m), ptp);
272 "~~~~~ fun solve, args:"; val (("Apply_Method", Apply_Method' (mI,_,_,_)), pos as (p,_)) = (m, pos);
273 val {srls, ...} = get_met mI;
274 val PblObj {meth=itms, ...} = get_obj I pt p;
275 val thy' = get_obj g_domID pt p;
276 val thy = assoc_thy thy';
277 val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI;
278 val ini = init_form thy sc env;
279 "----- fun init_form, args:"; val (Script sc) = sc;
280 "----- fun get_stac, args:"; val (y, h $ body) = (thy, sc);
281 case get_stac thy sc of SOME (Free ("e_e", _)) => ()
282 | _ => error "script: Const (?, ?) in script (as term) changed";;