1 (* Title: "ProgLang/scrtools.sml"
2 tests on tools for scripts
3 Author: Walther Neuper 060605
4 (c) due to copyright terms
6 "-----------------------------------------------------------------";
7 "table of contents -----------------------------------------------";
8 "-----------------------------------------------------------------";
9 "-------- test the same called by interSteps norm_Poly -----------";
10 "-------- test the same called by interSteps norm_Rational -------";
11 "-------- check auto-gen.script for Rewrite_Set_Inst -------------";
12 "-------- distinguish input to Model -----------------------------------------";
13 "-------- fun subpbl, fun pblterm --------------------------------------------";
14 "-------- fun stacpbls, fun subst_stacexpr -----------------------------------";
15 "-------- fun is_calc, fun op_of_calc ----------------------------------------";
16 "-------- fun rule2stac, fun rule2stac_inst ----------------------------------";
17 "-------- fun op @@ ----------------------------------------------------------";
18 "-------- fun get_fun_id -----------------------------------------------------";
19 "-------- fun rules2scr_Rls --------------------------------------------------";
20 "-----------------------------------------------------------------------------";
21 "-----------------------------------------------------------------------------";
22 "-----------------------------------------------------------------------------";
24 "-------- test the same called by interSteps norm_Poly -----------";
25 "-------- test the same called by interSteps norm_Poly -----------";
26 "-------- test the same called by interSteps norm_Poly -----------";
27 val Seq {scr = Prog auto_script,...} = assoc_rls "norm_Poly";
28 writeln(term2str auto_script);
29 (*Script Stepwise t_t =
30 (Try (Rewrite_Set discard_minus False) @@
31 Try (Rewrite_Set expand_poly_ False) @@
32 Try (Repeat (Calculate TIMES)) @@
33 Try (Rewrite_Set order_mult_rls_ False) @@
34 Try (Rewrite_Set simplify_power_ False) @@
35 Try (Rewrite_Set calc_add_mult_pow_ False) @@
36 Try (Rewrite_Set reduce_012_mult_ False) @@
37 Try (Rewrite_Set order_add_rls_ False) @@
38 Try (Rewrite_Set collect_numerals_ False) @@
39 Try (Rewrite_Set reduce_012_ False) @@
40 Try (Rewrite_Set discard_parentheses1 False))
41 ??.empty ..WORKS, NEVERTHELESS *)
44 reset_states (); (*<-- evaluate, if ML-blocks are edited below*)
46 [(["Term (b + a - b)", "normalform N"],
47 ("Poly",["polynomial","simplification"],
48 ["simplification","for_polynomials"]))];
52 autoCalculate 1 CompleteCalc;
53 val ((pt,p),_) = get_calc 1;
56 (([], Frm), Simplify (b + a - b)),
57 (([1], Frm), b + a - b),
61 interSteps 1 ([], Res);
62 val ((pt,p),_) = get_calc 1; show_pt pt;
65 (([], Frm), Simplify (b + a - b)),
66 (([1], Frm), b + a - b),
70 interSteps 1 ([1], Res);(*<SYSERROR><CALCID>1</CALCID><ERROR>error in kernel 8</ERROR></SYSERROR>*)
71 "~~~~~ fun interSteps, args:"; val (cI, ip) = (1, ([1], Res));
72 val ((pt, p), tacis) = get_calc cI;
73 (*if*) (not o is_interpos) ip = false;
74 val ip' = lev_pred' pt ip;
76 (*Math_Engine.detailstep pt ip ..ERROR interSteps>..>init_istate: "norm_Poly" has EmptyScr*)
77 val ("donesteps", ctree_BEFORE_step_into, pos'_BEFORE_step_into) = Math_Engine.detailstep pt ip;
78 "~~~~~ fun detailstep, args:"; val (pt, (pos as (p, _))) = (pt, ip);
79 val nd = Ctree.get_nd pt p
80 val cn = Ctree.children nd;
81 (*if*) null cn = false;
83 "~~~~~ to detailrls return val:";
85 val return_val = ("donesteps", pt, (p @ [length (Ctree.children (Ctree.get_nd pt p))], Ctree.Res));
86 if p @ [length (Ctree.children (Ctree.get_nd pt p))] = [1, 4]
87 then () else error "detailrls: auto-generated norm_Poly doesnt work";
89 val ((pt,p),_) = get_calc 1; show_pt pt;
91 (([], Frm), Simplify (b + a - b)),
92 (([1], Frm), b + a - b),
93 (([1,1], Frm), b + a - b),
94 (([1,1], Res), b + a + -1 * b),
95 (([1,2], Res), a + b + -1 * b),
96 (([1,3], Res), a + 0 * b),
100 if existpt' ([1,4], Res) pt then ()
101 else error "auto-generated norm_Poly doesnt work";
104 "-------- test the same called by interSteps norm_Rational -------";
105 "-------- test the same called by interSteps norm_Rational -------";
106 "-------- test the same called by interSteps norm_Rational -------";
108 val Seq {scr = Prog auto_script,...} = assoc_rls "norm_Rational";
109 writeln(term2str auto_script);
112 *** Const (Script.Stepwise, 'z => 'z => 'z)
114 *** . Const (Script.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
115 *** . . Const (Script.Try, ('a => 'a) => 'a => 'a)
116 *** . . . Const (Script.Rewrite'_Set, ID => bool => 'a => 'a)
117 *** . . . . Free (discard_minus, ID)
118 *** . . . . Const (HOL.False, bool)
119 *** . . Const (Script.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
120 *** . . . Const (Script.Try, ('a => 'a) => 'a => 'a)
121 *** . . . . Const (Script.Rewrite'_Set, ID => bool => 'a => 'a)
122 *** . . . . . Free (rat_mult_poly, ID)
123 *** . . . . . Const (HOL.False, bool)
124 *** . . . Const (Script.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
125 *** . . . . Const (Script.Try, ('a => 'a) => 'a => 'a)
126 *** . . . . . Const (Script.Rewrite'_Set, ID => bool => 'a => 'a)
127 *** . . . . . . Free (make_rat_poly_with_parentheses, ID)
128 *** . . . . . . Const (HOL.False, bool)
129 *** . . . . Const (Script.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
130 *** . . . . . Const (Script.Try, ('a => 'a) => 'a => 'a)
131 *** . . . . . . Const (Script.Rewrite'_Set, ID => bool => 'a => 'a)
132 *** . . . . . . . Free (cancel_p_rls, ID)
133 *** . . . . . . . Const (HOL.False, bool)
134 *** . . . . . Const (Script.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
135 *** . . . . . . Const (Script.Try, ('a => 'a) => 'a => 'a)
136 *** . . . . . . . Const (Script.Rewrite'_Set, ID => bool => 'a => 'a)
137 *** . . . . . . . . Free (norm_Rational_rls, ID)
138 *** . . . . . . . . Const (HOL.False, bool)
139 *** . . . . . . Const (Script.Try, ('a => 'a) => 'a => 'a)
140 *** . . . . . . . Const (Script.Rewrite'_Set, ID => bool => 'a => 'a)
141 *** . . . . . . . . Free (discard_parentheses1, ID)
142 *** . . . . . . . . Const (HOL.False, bool)
143 *** . . Const (empty, 'a)
147 [(["Term (b + a - b)", "normalform N"],
148 ("Poly",["polynomial","simplification"],
149 ["simplification","of_rationals"]))];
152 autoCalculate 1 CompleteCalc;
154 interSteps 1 ([], Res);
155 val ((pt,p),_) = get_calc 1; show_pt pt;
157 interSteps 1 ([1], Res);
158 val ((pt,p),_) = get_calc 1; show_pt pt;
160 (*with "Script SimplifyScript (t_::real) = \
161 \ ((Rewrite_Set norm_Rational False) t_)"
162 val (Form form, SOME tac, asm) = pt_extract (pt, ([1], Res));
164 val (Form form, SOME tac, asm) = pt_extract (pt, ([2], Res));
165 case (term2str form, tac, terms2strs asm) of
166 ("a", Check_Postcond ["polynomial", "simplification"], []) => ()
167 | _ => error "scrtools.sml: auto-generated norm_Rational doesnt work";
169 "-------- check auto-gen.script for Rewrite_Set_Inst -------------";
170 "-------- check auto-gen.script for Rewrite_Set_Inst -------------";
171 "-------- check auto-gen.script for Rewrite_Set_Inst -------------";
172 val rls = assoc_rls "integration";
173 val Seq {scr = Prog auto_script,...} = rls;
174 writeln(term2str auto_script);
176 if contain_bdv (get_rules rls) then ()
177 else error "scrtools.sml: contain_bdv doesnt work for 'integration'";
179 if terms2str (formal_args auto_script) = "[\"t_t\",\"v\"]"
180 then () else error "formal_args of auto-gen.script changed";
181 init_istate (Rewrite_Set_Inst (["(''bdv'', x)"], "integration_rules"))
182 (str2term "someTermWithBdv");
185 "-------- distinguish input to Model -----------------------------------------";
186 "-------- distinguish input to Model -----------------------------------------";
187 "-------- distinguish input to Model -----------------------------------------";
188 "----- fun is_booll_dsc -----";
189 val t as Const ("Descript.relations",
190 Type ("fun", [Type ("List.list", [Type ("HOL.bool",[])]),
191 Type ("Tools.una", [])])) = @{term "relations"};
193 if is_booll_dsc t then () else error "is_booll_dsc changed";
194 "----- fun is_reall_dsc -----";
195 if not (is_reall_dsc t) then () else error "is_reall_dsc changed";
197 "----- fun is_list_dsc -----";
198 val t = @{term "someList"};
199 if is_list_dsc t then () else error "is_list_dsc changed 1";
201 val t = @{term "additionalRels [a=b,c=(d::real)]"};
202 if is_list_dsc t then () else error "is_list_dsc changed 2";
203 if is_list_dsc (head_of t) then () else error "is_list_dsc changed 3";
205 "----- fun is_list_dsc -----";
206 val t = @{term "maximum"};
207 if is_dsc t then () else error "is_dsc changed 1";
209 val t = head_of @{term "maximum A"};
210 if is_dsc t then () else error "is_dsc changed 2";
212 val t = head_of @{term "fixedValues [R=(R::real)]"};
213 if is_dsc t then () else error "is_dsc changed 3";
215 "-------- fun stacpbls, fun subst_stacexpr -----------------------------------";
216 "-------- fun stacpbls, fun subst_stacexpr -----------------------------------";
217 "-------- fun subst_stacexpr, fun stacpbls -----------------------------------";
218 val {scr, ...} = get_met ["Test","sqrt-equ-test"]; val Prog sc = scr; val ts = stacpbls sc;
220 [Const ("Script.Rewrite", _) $ square_equation_left $ Const ("HOL.True", _),
221 Const ("Script.Rewrite'_Set", _) $ Test_simplify $ Const ("HOL.False", _),
222 Const ("Script.Rewrite'_Set", _) $ rearrange_assoc $ Const ("HOL.False", _),
223 Const ("Script.Rewrite'_Set", _) $ isolate_root $ Const ("HOL.False", _),
224 Const ("Script.Rewrite'_Set", _) $ norm_equation $ Const ("HOL.False", _),
225 Const ("Script.Rewrite'_Set'_Inst", _) $
226 (Const ("List.list.Cons", _) $ (Const ("Product_Type.Pair", _) $ bdv $ Free ("v_v", _)) $
227 Const ("List.list.Nil", _)) $
228 isolate_bdv $ Const ("HOL.False", _)] =>
229 if HOLogic.dest_string square_equation_left = "square_equation_left" andalso
230 HOLogic.dest_string Test_simplify = "Test_simplify" andalso
231 HOLogic.dest_string rearrange_assoc = "rearrange_assoc" andalso
232 HOLogic.dest_string isolate_root = "isolate_root" andalso
233 HOLogic.dest_string norm_equation = "norm_equation" andalso
234 HOLogic.dest_string bdv = "bdv" andalso
235 HOLogic.dest_string isolate_bdv = "isolate_bdv"
236 then () else error "stacpbls (Test.Solve_root_equation) changed 2"
237 | _ => error "stacpbls (Test.Solve_root_equation) changed 1";
239 (* inappropriate input is skipped *)
240 val t = @{term "(a::real) = (rhs (NTH 1 sol_a))"};
241 case stacpbls t of [] => () | _ => error "stacpbls rhs (NTH 1 sol_a) changed";
243 @{term "(SubProblem (BiegelinieX,[vonBelastungZu,Biegelinien], [Biegelinien,ausBelastung]) [REAL q__q, REAL v_v])"};
244 case stacpbls t of [] => () | _ => error "stacpbls (SubProblem ...) changed";
246 (* --- fun subst_stacexpr *)
247 case subst_stacexpr [] NONE e_term sc of
248 (NONE, Expr (Const ("HOL.eq", _) $
249 (Const ("Test.solve_root_equ", _) $ Free ("e_e", _) $ Free ("v_v", _)) $
250 (Const ("HOL.Let", _) $
251 (Const ("Script.Seq", _) $
252 (Const ("Script.While", _) $ _ $
256 Abs ("e_e", _, Const ("List.list.Cons", _) $ Free ("e_e", _) $ Const ("List.list.Nil", _)) )
258 | _ => error "subst_stacexpr [] NONE e_term";
260 "-------- fun is_calc, fun op_of_calc ----------------------------------------";
261 "-------- fun is_calc, fun op_of_calc ----------------------------------------";
262 "-------- fun is_calc, fun op_of_calc ----------------------------------------";
263 val rls = prep_rls @{theory} Test_simplify; (* adds the Program *)
264 val Prog sc = (#scr o rep_rls) rls;
265 val stacs = stacpbls sc;
267 val calcs = filter is_calc stacs;
268 val ids = map op_of_calc calcs;
270 ["PLUS", "TIMES", "DIVIDE", "POWER"] => ()
271 | _ => error "op_of_calc";
273 val calcs = ((assoc_calc' @{theory} |> map) o (map LTool.op_of_calc) o
274 (filter LTool.is_calc) o LTool.stacpbls) sc;
276 [("PLUS", ("Groups.plus_class.plus", _)), ("TIMES", ("Groups.times_class.times", _)),
277 ("DIVIDE", ("Rings.divide_class.divide", _)), ("POWER", ("Atools.pow", _))] => ()
278 | _ => error "get_calcs changed"
280 "-------- fun rule2stac, fun rule2stac_inst ----------------------------------";
281 "-------- fun rule2stac, fun rule2stac_inst ----------------------------------";
282 "-------- fun rule2stac, fun rule2stac_inst ----------------------------------";
283 val t = rule2stac @{theory} (Thm ("real_diff_minus", num_str @{thm real_diff_minus}));
284 if term2str t = "Try (Repeat (Rewrite ''real_diff_minus'' False))" then ()
285 else error "rule2stac Thm.. changed";
287 val t = rule2stac @{theory} (Calc ("Groups.plus_class.plus", eval_binop "#add_"));
288 if term2str t = "Try (Repeat (Calculate ''PLUS''))" then ()
289 else error "rule2stac Calc.. changed";
291 val t = rule2stac @{theory} (Rls_ rearrange_assoc);
292 if term2str t = "Try (Rewrite_Set ''rearrange_assoc'' False)" then ()
293 else error "rule2stac Rls_.. changed";
295 val t = rule2stac_inst @{theory} (Thm ("risolate_bdv_add", num_str @{thm risolate_bdv_add}));
296 if term2str t = "Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_add'' False))" then ()
297 else error "rule2stac_inst Thm.. changed";
299 (Const ("Script.Try", _) $
300 (Const ("Script.Repeat", _) $
301 (Const ("Script.Rewrite'_Inst", _) $
302 (Const ("List.list.Cons", _) $
303 (Const ("Product_Type.Pair", _) $
306 Const ("List.list.Nil", _)) $
308 Const ("HOL.False", _)))) =>
309 (if HOLogic.dest_string bdv = "bdv" andalso
310 HOLogic.dest_string risolate_bdv_add = "risolate_bdv_add" then ()
311 else error "rule2stac_inst changed 1")
312 | _ => error "rule2stac_inst changed 2"
314 "-------- fun op @@ ----------------------------------------------------------";
315 "-------- fun op @@ ----------------------------------------------------------";
316 "-------- fun op @@ ----------------------------------------------------------";
317 val rules = (#rules o rep_rls) isolate_root;
318 val rs = map (rule2stac @{theory}) rules;
320 if term2str t = "Try (Repeat (Rewrite ''rroot_to_lhs'' False)) @@\n" ^
321 "Try (Repeat (Rewrite ''rroot_to_lhs_mult'' False)) @@\n" ^
322 "Try (Repeat (Rewrite ''rroot_to_lhs_add_mult'' False)) @@\n" ^
323 "Try (Repeat (Rewrite ''risolate_root_add'' False)) @@\n" ^
324 "Try (Repeat (Rewrite ''risolate_root_mult'' False)) @@\n" ^
325 "Try (Repeat (Rewrite ''risolate_root_div'' False))"
326 then () else error "fun @@ changed"
328 "-------- fun get_fun_id -----------------------------------------------------";
329 "-------- fun get_fun_id -----------------------------------------------------";
330 "-------- fun get_fun_id -----------------------------------------------------";
331 (* fun_id is nested into arguments, compare ... *)
332 val Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $
333 (((((((Const (const_id, const_typ) $ _) $ _) $ _) $ _) $ _) $ _) $ _) $ _) =
334 Thm.prop_of @{thm biegelinie.simps};
336 val Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $
337 (Const (const_id, const_typ) $ _) $ _) =
338 Thm.prop_of @{thm simplify.simps};
340 (* get fun_id out of nesting *)
341 val Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $
343 Thm.prop_of @{thm biegelinie.simps};
344 val (Const ("Biegelinie.biegelinie", _) $
351 Var (("id_abl", 0), _)) = nested;
354 (Const ("Biegelinie.biegelinie", "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool list \<Rightarrow> bool")
356 [Var (("l", 0), "real"), Var (("q", 0), "real"), Var (("v", 0), "real"),
357 Var (("b", 0), "real \<Rightarrow> real"), Var (("s", 0), "bool list")]):
360 case get_fun_id (prep_program @{thm biegelinie.simps}) of
361 ("Biegelinie.biegelinie", _) => ()
362 | _ => error "get_fun_id changed";
363 case get_fun_id (prep_program @{thm simplify.simps}) of
364 ("PolyMinus.simplify", _) => ()
365 | _ => error "get_fun_id changed";
367 "-------- fun rules2scr_Rls --------------------------------------------------";
368 "-------- fun rules2scr_Rls --------------------------------------------------";
369 "-------- fun rules2scr_Rls --------------------------------------------------";
371 val prog = LTool.rules2scr_Rls @{theory} [Rule.Thm ("thm111", @{thm thm111}), Rule.Thm ("refl", @{thm refl})]
373 writeln (t2str @{theory} prog);
374 (*auto_generated t_t =
376 ((Try (Repeat (Rewrite ''thm111'' False)) @@
377 Try (Repeat (Rewrite ''refl'' False)))
380 if t2str @{theory} prog =
381 "auto_generated t_t =\nRepeat\n ((Try (Repeat (Rewrite ''thm111'' False)) @@\n Try (Repeat (Rewrite ''refl'' False)))\n ??.empty)"
382 then () else error "rules2scr_Rls auto_generated changed"