1 (* Title: ProgLang/auto_prog.sml
2 Author: Walther Neuper 190922
3 (c) due to copyright terms
6 "-----------------------------------------------------------------------------------------------";
7 "-----------------------------------------------------------------------------------------------";
8 "table of contents -----------------------------------------------------------------------------";
9 "-----------------------------------------------------------------------------------------------";
10 "-------- check auto-gen.script for Rewrite_Set_Inst -------------------------------------------";
11 "-------- test the same called by interSteps norm_Poly -----------------------------------------";
12 "-------- test the same called by interSteps norm_Rational -------------------------------------";
13 "-------- fun op #> ----------------------------------------------------------------------------";
14 "-------- fun rules2scr_Rls --------------------------------------------------------------------";
15 "-------- fun rule2stac, fun rule2stac_inst ----------------------------------------------------";
16 "-------- fun stacpbls, fun eval_leaf -----------------------------------";
17 "-------- fun is_calc, fun op_of_calc ----------------------------------------------------------";
18 "-------- fun subst_typ ------------------------------------------------------------------------";
19 "-------- fun subst_typs -----------------------------------------------------------------------";
20 "-----------------------------------------------------------------------------------------------";
21 "-----------------------------------------------------------------------------------------------";
22 "-----------------------------------------------------------------------------------------------";
25 "-------- check auto-gen.script for Rewrite_Set_Inst -------------------------------------------";
26 "-------- check auto-gen.script for Rewrite_Set_Inst -------------------------------------------";
27 "-------- check auto-gen.script for Rewrite_Set_Inst -------------------------------------------";
28 val rls = assoc_rls "integration";
29 val thy' = @{theory "Integrate"}
30 val t = @{term "ttt :: real"};
32 Auto_Prog.gen thy' t rls;
33 "~~~~~ fun generate , args:"; val (thy, t, rls) = (thy', t, rls);
34 val prog = case rls of
35 Rule.Rls {rules, ...} => rules2scr_Rls thy rules
36 | Rule.Seq {rules, ...} => rules2scr_Seq thy rules
37 val auto_script = subst_typs prog (type_of t) (TermC.guess_bdv_typ t) (*return from generate*);
39 if term2str auto_script =
40 "auto_generated_inst t_t v =\n" ^
41 "(Try (Rewrite_Set_Inst [(''bdv'', v)] ''integration_rules'') #>\n" ^
42 " Try (Rewrite_Set_Inst [(''bdv'', v)] ''add_new_c'') #>\n" ^
43 " Try (Rewrite_Set_Inst [(''bdv'', v)] ''simplify_Integral''))\n" ^
45 then () else error "Auto_Prog.gen integration CHANGED";
47 if contain_bdv (get_rules rls) then ()
48 else error "scrtools.sml: contain_bdv doesnt work for 'integration'";
50 if terms2str (formal_args auto_script) = "[\"t_t\",\"v\"]"
51 then () else error "formal_args of auto-gen.script changed";
53 init_istate (Rewrite_Set_Inst (["(''bdv'', x)"], "integration_rules"))
54 (str2term "someTermWithBdv");
55 "~~~~~ fun init_istate , args:"; val ((Tactic.Rewrite_Set_Inst (subs, rls)), t)
56 = ((Rewrite_Set_Inst (["(''bdv'', x)"], "integration_rules")), str2term "someTermWithBdv");
57 val v = case Selem.subs2subst (Celem.assoc_thy "Isac_Knowledge") subs of
59 (*case*) assoc_rls rls (*of*);
62 "-------- test the same called by interSteps norm_Poly -----------------------------------------";
63 "-------- test the same called by interSteps norm_Poly -----------------------------------------";
64 "-------- test the same called by interSteps norm_Poly -----------------------------------------";
65 val rls = assoc_rls "norm_Poly";
66 val thy' = @{theory "Poly"}
67 val t = @{term "ttt :: real"}
68 val auto_script = Auto_Prog.gen thy' t rls;
70 if term2str auto_script =
71 "auto_generated t_t =\n" ^
72 "(Try (Rewrite_Set ''discard_minus'') #>\n" ^
73 " Try (Rewrite_Set ''expand_poly_'') #>\n" ^
74 " Try (Repeat (Calculate ''TIMES'')) #>\n" ^
75 " Try (Rewrite_Set ''order_mult_rls_'') #>\n" ^
76 " Try (Rewrite_Set ''simplify_power_'') #>\n" ^
77 " Try (Rewrite_Set ''calc_add_mult_pow_'') #>\n" ^
78 " Try (Rewrite_Set ''reduce_012_mult_'') #>\n" ^
79 " Try (Rewrite_Set ''order_add_rls_'') #>\n" ^
80 " Try (Rewrite_Set ''collect_numerals_'') #>\n" ^
81 " Try (Rewrite_Set ''reduce_012_'') #>\n" ^
82 " Try (Rewrite_Set ''discard_parentheses1''))\n" ^
83 " ??.empty" (* ..WORKS, NEVERTHELESS*)
84 then () else error "Auto_Prog.gen norm_Poly CHANGED";
86 reset_states (); (*<-- evaluate, if ML-blocks are edited below*)
88 [(["Term (b + a - b)", "normalform N"],
89 ("Poly",["polynomial","simplification"],
90 ["simplification","for_polynomials"]))];
94 autoCalculate 1 CompleteCalc;
95 val ((pt,p),_) = get_calc 1;
98 (([], Frm), Simplify (b + a - b)),
99 (([1], Frm), b + a - b),
103 interSteps 1 ([], Res);
104 val ((pt,p),_) = get_calc 1; show_pt pt;
107 (([], Frm), Simplify (b + a - b)),
108 (([1], Frm), b + a - b),
112 interSteps 1 ([1], Res);(*<SYSERROR><CALCID>1</CALCID><ERROR>error in kernel 8</ERROR></SYSERROR>*)
113 "~~~~~ fun interSteps, args:"; val (cI, ip) = (1, ([1], Res));
114 val ((pt, p), tacis) = get_calc cI;
115 (*if*) (not o is_interpos) ip = false;
116 val ip' = lev_pred' pt ip;
118 (*Detail_Step.go pt ip ..ERROR interSteps>..>init_istate: "norm_Poly" has EmptyScr*)
119 val ("donesteps", ctree_BEFORE_step_into, pos'_BEFORE_step_into) = Detail_Step.go pt ip;
120 "~~~~~ fun go, args:"; val (pt, (pos as (p, _))) = (pt, ip);
121 val nd = Ctree.get_nd pt p
122 val cn = Ctree.children nd;
123 (*if*) null cn = false;
125 "~~~~~ to detailrls return val:";
127 val return_val = ("donesteps", pt, (p @ [length (Ctree.children (Ctree.get_nd pt p))], Pos.Res));
128 if p @ [length (Ctree.children (Ctree.get_nd pt p))] = [1, 4]
129 then () else error "detailrls: auto-generated norm_Poly doesnt work";
131 val ((pt,p),_) = get_calc 1; show_pt pt;
133 (([], Frm), Simplify (b + a - b)),
134 (([1], Frm), b + a - b),
135 (([1,1], Frm), b + a - b),
136 (([1,1], Res), b + a + -1 * b),
137 (([1,2], Res), a + b + -1 * b),
138 (([1,3], Res), a + 0 * b),
142 if existpt' ([1,4], Res) pt then ()
143 else error "auto-generated norm_Poly doesnt work";
146 "-------- test the same called by interSteps norm_Rational -------------------------------------";
147 "-------- test the same called by interSteps norm_Rational -------------------------------------";
148 "-------- test the same called by interSteps norm_Rational -------------------------------------";
150 Auto_Prog.gen @{theory "Poly"} @{term "ttt :: real"} (assoc_rls "norm_Rational");
151 writeln(term2str auto_script);
154 *** Const (Program.Stepwise, 'z => 'z => 'z)
156 *** . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
157 *** . . Const (Program.Try, ('a => 'a) => 'a => 'a)
158 *** . . . Const (Program.Rewrite'_Set, ID => 'a => 'a)
159 *** . . . . Free (discard_minus, ID)
160 *** . . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
161 *** . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
162 *** . . . . Const (Program.Rewrite'_Set, ID => 'a => 'a)
163 *** . . . . . Free (rat_mult_poly, ID)
164 *** . . . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
165 *** . . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
166 *** . . . . . Const (Program.Rewrite'_Set, ID => 'a => 'a)
167 *** . . . . . . Free (make_rat_poly_with_parentheses, ID)
168 *** . . . . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
169 *** . . . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
170 *** . . . . . . Const (Program.Rewrite'_Set, ID => 'a => 'a)
171 *** . . . . . . . Free (cancel_p_rls, ID)
172 *** . . . . . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
173 *** . . . . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
174 *** . . . . . . . Const (Program.Rewrite'_Set, ID => 'a => 'a)
175 *** . . . . . . . . Free (norm_Rational_rls, ID)
176 *** . . . . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
177 *** . . . . . . . Const (Program.Rewrite'_Set, ID => 'a => 'a)
178 *** . . . . . . . . Free (discard_parentheses1, ID)
179 *** . . Const (empty, 'a)
183 [(["Term (b + a - b)", "normalform N"],
184 ("Poly",["polynomial","simplification"],
185 ["simplification","of_rationals"]))];
188 autoCalculate 1 CompleteCalc;
190 interSteps 1 ([], Res);
191 val ((pt,p),_) = get_calc 1; show_pt pt;
193 interSteps 1 ([1], Res);
194 val ((pt,p),_) = get_calc 1; show_pt pt;
196 (*with "Program SimplifyScript (t_::real) = \
197 \ ((Rewrite_Set norm_Rational) t_)"
198 val (Form form, SOME tac, asm) = pt_extract (pt, ([1], Res));
200 val (Form form, SOME tac, asm) = pt_extract (pt, ([2], Res));
201 case (term2str form, tac, terms2strs asm) of
202 ("a", Check_Postcond ["polynomial", "simplification"], []) => ()
203 | _ => error "scrtools.sml: auto-generated norm_Rational doesnt work";
206 "-------- fun op #> ----------------------------------------------------------------------------";
207 "-------- fun op #> ----------------------------------------------------------------------------";
208 "-------- fun op #> ----------------------------------------------------------------------------";
209 val rules = (#rules o rep_rls) isolate_root;
210 val rs = map (rule2stac @{theory}) rules;
212 if term2str t = "Try (Repeat (Rewrite ''rroot_to_lhs'')) #>\n" ^
213 "Try (Repeat (Rewrite ''rroot_to_lhs_mult'')) #>\n" ^
214 "Try (Repeat (Rewrite ''rroot_to_lhs_add_mult'')) #>\n" ^
215 "Try (Repeat (Rewrite ''risolate_root_add'')) #>\n" ^
216 "Try (Repeat (Rewrite ''risolate_root_mult'')) #>\n" ^
217 "Try (Repeat (Rewrite ''risolate_root_div''))"
218 then () else error "fun #> changed"
221 "-------- fun rules2scr_Rls --------------------------------------------------------------------";
222 "-------- fun rules2scr_Rls --------------------------------------------------------------------";
223 "-------- fun rules2scr_Rls --------------------------------------------------------------------";
224 (*compare Prog_Expr.*)
225 val prog = Auto_Prog.rules2scr_Rls @{theory} [Rule.Thm ("thm111", @{thm thm111}), Rule.Thm ("refl", @{thm refl})]
227 writeln (t2str @{theory} prog);
228 (*auto_generated t_t =
230 ((Try (Repeat (Rewrite ''thm111'')) #>
231 Try (Repeat (Rewrite ''refl'')))
234 if t2str @{theory} prog =
235 "auto_generated t_t =\n" ^
237 " ((Try (Repeat (Rewrite ''thm111'')) #> Try (Repeat (Rewrite ''refl'')))\n" ^
239 then () else error "rules2scr_Rls auto_generated changed";
242 "-------- fun rule2stac, fun rule2stac_inst ----------------------------------------------------";
243 "-------- fun rule2stac, fun rule2stac_inst ----------------------------------------------------";
244 "-------- fun rule2stac, fun rule2stac_inst ----------------------------------------------------";
245 val t = rule2stac @{theory} (Thm ("real_diff_minus", num_str @{thm real_diff_minus}));
246 if term2str t = "Try (Repeat (Rewrite ''real_diff_minus''))" then ()
247 else error "rule2stac Thm.. changed";
249 val t = rule2stac @{theory} (Num_Calc ("Groups.plus_class.plus", eval_binop "#add_"));
250 if term2str t = "Try (Repeat (Calculate ''PLUS''))" then ()
251 else error "rule2stac Num_Calc.. changed";
253 val t = rule2stac @{theory} (Rls_ rearrange_assoc);
254 if term2str t = "Try (Rewrite_Set ''rearrange_assoc'')" then ()
255 else error "rule2stac Rls_.. changed";
257 val t = rule2stac_inst @{theory} (Thm ("risolate_bdv_add", num_str @{thm risolate_bdv_add}));
258 if term2str t = "Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_add''))" then ()
259 else error "rule2stac_inst Thm.. changed";
261 (Const ("Tactical.Try", _) $
262 (Const ("Tactical.Repeat", _) $
263 (Const ("Prog_Tac.Rewrite'_Inst", _) $
264 (Const ("List.list.Cons", _) $
265 (Const ("Product_Type.Pair", _) $
268 Const ("List.list.Nil", _)) $
269 risolate_bdv_add))) =>
270 (if HOLogic.dest_string bdv = "bdv" andalso
271 HOLogic.dest_string risolate_bdv_add = "risolate_bdv_add" then ()
272 else error "rule2stac_inst changed 1")
273 | _ => error "rule2stac_inst changed 2";
276 "-------- fun stacpbls, fun eval_leaf -----------------------------------";
277 "-------- fun stacpbls, fun eval_leaf -----------------------------------";
278 "-------- fun stacpbls, fun eval_leaf -----------------------------------";
279 val {scr, ...} = get_met ["Test","sqrt-equ-test"]; val Prog sc = scr; val ts = stacpbls sc;
281 [Const ("Prog_Tac.Rewrite", _) $ square_equation_left,
282 Const ("Prog_Tac.Rewrite'_Set", _) $ Test_simplify,
283 Const ("Prog_Tac.Rewrite'_Set", _) $ rearrange_assoc,
284 Const ("Prog_Tac.Rewrite'_Set", _) $ isolate_root,
285 Const ("Prog_Tac.Rewrite'_Set", _) $ norm_equation,
286 Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $
287 (Const ("List.list.Cons", _) $ (Const ("Product_Type.Pair", _) $ bdv $ Free ("v_v", _)) $
288 Const ("List.list.Nil", _)) $ isolate_bdv] =>
289 if HOLogic.dest_string square_equation_left = "square_equation_left" andalso
290 HOLogic.dest_string Test_simplify = "Test_simplify" andalso
291 HOLogic.dest_string rearrange_assoc = "rearrange_assoc" andalso
292 HOLogic.dest_string isolate_root = "isolate_root" andalso
293 HOLogic.dest_string norm_equation = "norm_equation" andalso
294 HOLogic.dest_string bdv = "bdv" andalso
295 HOLogic.dest_string isolate_bdv = "isolate_bdv"
296 then () else error "stacpbls (Test.Solve_root_equation) changed 2"
297 | _ => error "stacpbls (Test.Solve_root_equation) changed 1";
299 (* inappropriate input is skipped *)
300 val t = @{term "(a::real) = (rhs (NTH 1 sol_a))"};
301 case stacpbls t of [] => () | _ => error "stacpbls rhs (NTH 1 sol_a) changed";
303 @{term "(SubProblem (BiegelinieX,[vonBelastungZu,Biegelinien], [Biegelinien,ausBelastung]) [REAL q__q, REAL v_v])"};
304 case stacpbls t of [] => () | _ => error "stacpbls (SubProblem ...) changed";
307 "-------- fun is_calc, fun op_of_calc ----------------------------------------------------------";
308 "-------- fun is_calc, fun op_of_calc ----------------------------------------------------------";
309 "-------- fun is_calc, fun op_of_calc ----------------------------------------------------------";
310 val rls = prep_rls @{theory} Test_simplify; (* adds the Program *)
311 val sc = Auto_Prog.gen thy' t rls;
312 val stacs = stacpbls sc;
314 val calcs = filter is_calc stacs;
315 val ids = map op_of_calc calcs;
317 ["PLUS", "TIMES", "DIVIDE", "POWER"] => ()
318 | _ => error "op_of_calc";
320 val calcs = ((assoc_calc' @{theory} |> map) o (map Auto_Prog.op_of_calc) o
321 (filter Auto_Prog.is_calc) o Auto_Prog.stacpbls) sc;
323 [("PLUS", ("Groups.plus_class.plus", _)), ("TIMES", ("Groups.times_class.times", _)),
324 ("DIVIDE", ("Rings.divide_class.divide", _)), ("POWER", ("Prog_Expr.pow", _))] => ()
325 | _ => error "get_calcs changed"
328 "-------- fun subst_typ ------------------------------------------------------------------------";
329 "-------- fun subst_typ ------------------------------------------------------------------------";
330 "-------- fun subst_typ ------------------------------------------------------------------------";
331 val prog = Auto_Prog.gen @{theory Isac_Knowledge} t (assoc_rls "isolate_bdv");
332 (* term2str prog |> writeln
333 auto_generated_inst t_t v =
335 ((Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_add'')) #>
336 Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_mult_add'')) #>
337 Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_mult'')) #>
338 Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''mult_square'')) #>
339 Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''constant_square'')) #>
340 Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''constant_mult_square'')))
344 val frees = vars prog; (* = [Free ("t_t", "'z"), Free ("v", "real")]*)
345 if length frees = 2 then () else error "test setup Auto_Prog.subst_typ changed 1";
347 val args = formal_args prog; (* = [Free ("t_t", "'z"), Free ("v", "real")]*)
348 if length args = 2 then () else error "test setup Auto_Prog.subst_typ changed 2";
350 val typ_t = HOLogic.realT
351 val typ_bdv = HOLogic.realT
353 val vars_v = (* = [Free ("v", "real"), Free ("v", "'a")]*)
354 filter (fn t => curry op = (t |> dest_Free |> fst) "v") frees
355 val typs_v = (* = ["real", "'a"]*)
356 map (fn t => (t |> dest_Free |> snd)) vars_v;
358 val subst_ty = subst_typ "v" HOLogic.realT frees; (* = [("real", "real")]*)
359 if length subst_ty = 1 then () else error "Auto_Prog.subst_typ changed";
362 "-------- fun subst_typs -----------------------------------------------------------------------";
363 "-------- fun subst_typs -----------------------------------------------------------------------";
364 "-------- fun subst_typs -----------------------------------------------------------------------";
365 val prog = Auto_Prog.gen thy' t (assoc_rls "isolate_bdv");
366 val frees = vars prog; (* = [Free ("t_t", "'z"), Free ("v", "real"), Free ("v", "'a")]*)
367 if length frees = 2 then () else error "test setup Auto_Prog.subst_typs changed 1";
369 val args = formal_args prog; (* = [Free ("t_t", "'z"), Free ("v", "real")]*)
370 if length args = 2 then () else error "test setup Auto_Prog.subst_typs changed 2";
372 val prog' = subst_typs prog HOLogic.realT HOLogic.realT
373 val frees' = vars prog'; (* = [Free ("t_t", "'z"), Free ("v", "real")]*);
374 if length frees' = 2 then () else error "Auto_Prog.subst_typs changed 2"