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 gen , args:"; val (thy, t, rls) = (thy', t, rls);
34 val prog = case rls of
35 Rule_Set.Repeat {rules, ...} => rules2scr_Rls thy rules
36 | Rule_Set.Sequence {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 UnparseC.term 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 UnparseC.terms (formal_args auto_script) = "[\"t_t\", \"v\"]"
51 then () else error "formal_args of auto-gen.script changed";
53 Istate.init_detail (Rewrite_Set_Inst (["(''bdv'', x)"], "integration_rules")) (TermC.str2term "someTermWithBdv");
54 "~~~~~ fun init_detail , args:"; val ((Tactic.Rewrite_Set_Inst (subs, rls)), t)
55 = ((Rewrite_Set_Inst (["(''bdv'', x)"], "integration_rules")), TermC.str2term "someTermWithBdv");
56 val v = case Subst.T_from_input (ThyC.get_theory "Isac_Knowledge") subs of
58 (*case*) assoc_rls rls (*of*);
61 "-------- test the same called by interSteps norm_Poly -----------------------------------------";
62 "-------- test the same called by interSteps norm_Poly -----------------------------------------";
63 "-------- test the same called by interSteps norm_Poly -----------------------------------------";
64 val rls = assoc_rls "norm_Poly";
65 val thy' = @{theory "Poly"}
66 val t = @{term "ttt :: real"}
67 val auto_script = Auto_Prog.gen thy' t rls;
69 if UnparseC.term auto_script =
70 "auto_generated t_t =\n" ^
71 "(Try (Rewrite_Set ''discard_minus'') #>\n" ^
72 " Try (Rewrite_Set ''expand_poly_'') #>\n" ^
73 " Try (Repeat (Calculate ''TIMES'')) #>\n" ^
74 " Try (Rewrite_Set ''order_mult_rls_'') #>\n" ^
75 " Try (Rewrite_Set ''simplify_power_'') #>\n" ^
76 " Try (Rewrite_Set ''calc_add_mult_pow_'') #>\n" ^
77 " Try (Rewrite_Set ''reduce_012_mult_'') #>\n" ^
78 " Try (Rewrite_Set ''order_add_rls_'') #>\n" ^
79 " Try (Rewrite_Set ''collect_numerals_'') #>\n" ^
80 " Try (Rewrite_Set ''reduce_012_'') #>\n" ^
81 " Try (Rewrite_Set ''discard_parentheses1''))\n" ^
82 " ??.empty" (* ..WORKS, NEVERTHELESS*)
83 then () else error "Auto_Prog.gen norm_Poly CHANGED";
85 reset_states (); (*<-- evaluate, if ML-blocks are edited below*)
87 [(["Term (b + a - b)", "normalform N"],
88 ("Poly",["polynomial", "simplification"],
89 ["simplification", "for_polynomials"]))];
93 autoCalculate 1 CompleteCalc;
94 val ((pt,p),_) = get_calc 1;
97 (([], Frm), Simplify (b + a - b)),
98 (([1], Frm), b + a - b),
102 interSteps 1 ([], Res);
103 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
104 Test_Tool.show_pt pt;
106 (([], Frm), Simplify (b + a - b)),
107 (([1], Frm), b + a - b),
111 interSteps 1 ([1], Res);(*<SYSERROR><CALCID>1</CALCID><ERROR>error in kernel 8</ERROR></SYSERROR>*)
112 "~~~~~ fun interSteps, args:"; val (cI, ip) = (1, ([1], Res));
113 val ((pt, p), tacis) = get_calc cI;
114 (*if*) (not o is_interpos) ip = false;
115 val ip' = lev_pred' pt ip;
117 (*Detail_Step.go pt ip ..ERROR interSteps>..>init_detail: "norm_Poly" has Empty_Prog*)
118 val ("donesteps", ctree_BEFORE_step_into, pos'_BEFORE_step_into) = Detail_Step.go pt ip;
119 "~~~~~ fun go, args:"; val (pt, (pos as (p, _))) = (pt, ip);
120 val nd = Ctree.get_nd pt p
121 val cn = Ctree.children nd;
122 (*if*) null cn = false;
124 "~~~~~ to detailrls return val:";
126 val return_val = ("donesteps", pt, (p @ [length (Ctree.children (Ctree.get_nd pt p))], Pos.Res));
127 if p @ [length (Ctree.children (Ctree.get_nd pt p))] = [1, 4]
128 then () else error "detailrls: auto-generated norm_Poly doesnt work";
130 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
131 Test_Tool.show_pt pt; (*[
132 (([], Frm), Simplify (b + a - b)),
133 (([1], Frm), b + a - b),
134 (([1,1], Frm), b + a - b),
135 (([1,1], Res), b + a + -1 * b),
136 (([1,2], Res), a + b + -1 * b),
137 (([1,3], Res), a + 0 * b),
141 if existpt' ([1,4], Res) pt then ()
142 else error "auto-generated norm_Poly doesnt work";
145 "-------- test the same called by interSteps norm_Rational -------------------------------------";
146 "-------- test the same called by interSteps norm_Rational -------------------------------------";
147 "-------- test the same called by interSteps norm_Rational -------------------------------------";
149 Auto_Prog.gen @{theory "Poly"} @{term "ttt :: real"} (assoc_rls "norm_Rational");
150 writeln(UnparseC.term auto_script);
151 TermC.atomty auto_script;
153 *** Const (Program.Stepwise, 'z => 'z => 'z)
155 *** . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
156 *** . . Const (Program.Try, ('a => 'a) => 'a => 'a)
157 *** . . . Const (Program.Rewrite_Set, ID => 'a => 'a)
158 *** . . . . Free (discard_minus, ID)
159 *** . . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
160 *** . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
161 *** . . . . Const (Program.Rewrite_Set, ID => 'a => 'a)
162 *** . . . . . Free (rat_mult_poly, ID)
163 *** . . . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
164 *** . . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
165 *** . . . . . Const (Program.Rewrite_Set, ID => 'a => 'a)
166 *** . . . . . . Free (make_rat_poly_with_parentheses, ID)
167 *** . . . . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
168 *** . . . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
169 *** . . . . . . Const (Program.Rewrite_Set, ID => 'a => 'a)
170 *** . . . . . . . Free (cancel_p_rls, ID)
171 *** . . . . . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
172 *** . . . . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
173 *** . . . . . . . Const (Program.Rewrite_Set, ID => 'a => 'a)
174 *** . . . . . . . . Free (norm_Rational_rls, ID)
175 *** . . . . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
176 *** . . . . . . . Const (Program.Rewrite_Set, ID => 'a => 'a)
177 *** . . . . . . . . Free (discard_parentheses1, ID)
178 *** . . Const (empty, 'a)
182 [(["Term (b + a - b)", "normalform N"],
183 ("Poly",["polynomial", "simplification"],
184 ["simplification", "of_rationals"]))];
187 autoCalculate 1 CompleteCalc;
189 interSteps 1 ([], Res);
190 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
192 interSteps 1 ([1], Res);
193 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
195 (*with "Program SimplifyScript (t_::real) = \
196 \ ((Rewrite_Set norm_Rational) t_)"
197 val (Form form, SOME tac, asm) = ME_Misc.pt_extract (pt, ([1], Res));
199 val (Form form, SOME tac, asm) = ME_Misc.pt_extract (pt, ([2], Res));
200 case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of
201 ("a", Check_Postcond ["polynomial", "simplification"], []) => ()
202 | _ => error "scrtools.sml: auto-generated norm_Rational doesnt work";
205 "-------- fun op #> ----------------------------------------------------------------------------";
206 "-------- fun op #> ----------------------------------------------------------------------------";
207 "-------- fun op #> ----------------------------------------------------------------------------";
208 val rules = (#rules o Rule_Set.rep) isolate_root;
209 val rs = map (rule2stac @{theory}) rules;
211 if UnparseC.term t = "Try (Repeat (Rewrite ''rroot_to_lhs'')) #>\n" ^
212 "Try (Repeat (Rewrite ''rroot_to_lhs_mult'')) #>\n" ^
213 "Try (Repeat (Rewrite ''rroot_to_lhs_add_mult'')) #>\n" ^
214 "Try (Repeat (Rewrite ''risolate_root_add'')) #>\n" ^
215 "Try (Repeat (Rewrite ''risolate_root_mult'')) #>\n" ^
216 "Try (Repeat (Rewrite ''risolate_root_div''))"
217 then () else error "fun #> changed"
220 "-------- fun rules2scr_Rls --------------------------------------------------------------------";
221 "-------- fun rules2scr_Rls --------------------------------------------------------------------";
222 "-------- fun rules2scr_Rls --------------------------------------------------------------------";
223 (*compare Prog_Expr.*)
224 val prog = Auto_Prog.rules2scr_Rls @{theory} [\<^rule_thm>\<open>thm111\<close>, \<^rule_thm>\<open>refl\<close>]
226 writeln (UnparseC.term_in_thy @{theory} prog);
227 (*auto_generated t_t =
229 ((Try (Repeat (Rewrite ''thm111'')) #>
230 Try (Repeat (Rewrite ''refl'')))
233 if UnparseC.term_in_thy @{theory} prog =
234 "auto_generated t_t =\n" ^
236 " ((Try (Repeat (Rewrite ''thm111'')) #> Try (Repeat (Rewrite ''refl'')))\n" ^
238 then () else error "rules2scr_Rls auto_generated changed";
241 "-------- fun rule2stac, fun rule2stac_inst ----------------------------------------------------";
242 "-------- fun rule2stac, fun rule2stac_inst ----------------------------------------------------";
243 "-------- fun rule2stac, fun rule2stac_inst ----------------------------------------------------";
244 val t = rule2stac @{theory} (Thm ("real_diff_minus", ThmC.numerals_to_Free @{thm real_diff_minus}));
245 if UnparseC.term t = "Try (Repeat (Rewrite ''real_diff_minus''))" then ()
246 else error "rule2stac Thm.. changed";
248 val t = rule2stac @{theory} (Eval ("Groups.plus_class.plus", eval_binop "#add_"));
249 if UnparseC.term t = "Try (Repeat (Calculate ''PLUS''))" then ()
250 else error "rule2stac Eval.. changed";
252 val t = rule2stac @{theory} (Rls_ rearrange_assoc);
253 if UnparseC.term t = "Try (Rewrite_Set ''rearrange_assoc'')" then ()
254 else error "rule2stac Rls_.. changed";
256 val t = rule2stac_inst @{theory} (Thm ("risolate_bdv_add", ThmC.numerals_to_Free @{thm risolate_bdv_add}));
257 if UnparseC.term t = "Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_add''))" then ()
258 else error "rule2stac_inst Thm.. changed";
260 (Const ("Tactical.Try", _) $
261 (Const ("Tactical.Repeat", _) $
262 (Const ("Prog_Tac.Rewrite_Inst", _) $
263 (Const ("List.list.Cons", _) $
264 (Const ("Product_Type.Pair", _) $
267 Const ("List.list.Nil", _)) $
268 risolate_bdv_add))) =>
269 (if HOLogic.dest_string bdv = "bdv" andalso
270 HOLogic.dest_string risolate_bdv_add = "risolate_bdv_add" then ()
271 else error "rule2stac_inst changed 1")
272 | _ => error "rule2stac_inst changed 2";
275 "-------- fun stacpbls, fun eval_leaf -----------------------------------";
276 "-------- fun stacpbls, fun eval_leaf -----------------------------------";
277 "-------- fun stacpbls, fun eval_leaf -----------------------------------";
278 val {scr, ...} = MethodC.from_store ["Test", "sqrt-equ-test"]; val Prog sc = scr; val ts = stacpbls sc;
280 [Const ("Prog_Tac.Rewrite", _) $ square_equation_left,
281 Const ("Prog_Tac.Rewrite_Set", _) $ Test_simplify,
282 Const ("Prog_Tac.Rewrite_Set", _) $ rearrange_assoc,
283 Const ("Prog_Tac.Rewrite_Set", _) $ isolate_root,
284 Const ("Prog_Tac.Rewrite_Set", _) $ norm_equation,
285 Const ("Prog_Tac.Rewrite_Set_Inst", _) $
286 (Const ("List.list.Cons", _) $ (Const ("Product_Type.Pair", _) $ bdv $ Free ("v_v", _)) $
287 Const ("List.list.Nil", _)) $ isolate_bdv] =>
288 if HOLogic.dest_string square_equation_left = "square_equation_left" andalso
289 HOLogic.dest_string Test_simplify = "Test_simplify" andalso
290 HOLogic.dest_string rearrange_assoc = "rearrange_assoc" andalso
291 HOLogic.dest_string isolate_root = "isolate_root" andalso
292 HOLogic.dest_string norm_equation = "norm_equation" andalso
293 HOLogic.dest_string bdv = "bdv" andalso
294 HOLogic.dest_string isolate_bdv = "isolate_bdv"
295 then () else error "stacpbls (Test.Solve_root_equation) changed 2"
296 | _ => error "stacpbls (Test.Solve_root_equation) changed 1";
298 (* inappropriate input is skipped *)
299 val t = @{term "(a::real) = (rhs (NTH 1 sol_a))"};
300 case stacpbls t of [] => () | _ => error "stacpbls rhs (NTH 1 sol_a) changed";
302 @{term "(SubProblem (BiegelinieX,[vonBelastungZu,Biegelinien], [Biegelinien,ausBelastung]) [REAL q__q, REAL v_v])"};
303 case stacpbls t of [] => () | _ => error "stacpbls (SubProblem ...) changed";
306 "-------- fun is_calc, fun op_of_calc ----------------------------------------------------------";
307 "-------- fun is_calc, fun op_of_calc ----------------------------------------------------------";
308 "-------- fun is_calc, fun op_of_calc ----------------------------------------------------------";
309 val rls = prep_rls @{theory} Test_simplify; (* adds the Program *)
310 val sc = Auto_Prog.gen thy' t rls;
311 val stacs = stacpbls sc;
313 val calcs = filter is_calc stacs;
314 val ids = map op_of_calc calcs;
316 ["PLUS", "TIMES", "DIVIDE", "POWER"] => ()
317 | _ => error "op_of_calc";
319 val calcs = ((assoc_calc' @{theory} |> map) o (map Auto_Prog.op_of_calc) o
320 (filter Auto_Prog.is_calc) o Auto_Prog.stacpbls) sc;
322 [("PLUS", ("Groups.plus_class.plus", _)), ("TIMES", ("Groups.times_class.times", _)),
323 ("DIVIDE", ("Rings.divide_class.divide", _)), ("POWER", ("Transcendental.powr", _))] => ()
324 | _ => error "get_calcs changed"
327 "-------- fun subst_typ ------------------------------------------------------------------------";
328 "-------- fun subst_typ ------------------------------------------------------------------------";
329 "-------- fun subst_typ ------------------------------------------------------------------------";
330 val prog = Auto_Prog.gen @{theory Isac_Knowledge} t (assoc_rls "isolate_bdv");
331 (* UnparseC.term prog |> writeln
332 auto_generated_inst t_t v =
334 ((Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_add'')) #>
335 Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_mult_add'')) #>
336 Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_mult'')) #>
337 Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''mult_square'')) #>
338 Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''constant_square'')) #>
339 Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''constant_mult_square'')))
343 val frees = vars prog; (* = [Free ("t_t", "'z"), Free ("v", "real")]*)
344 if length frees = 2 then () else error "test setup Auto_Prog.subst_typ changed 1";
346 val args = formal_args prog; (* = [Free ("t_t", "'z"), Free ("v", "real")]*)
347 if length args = 2 then () else error "test setup Auto_Prog.subst_typ changed 2";
349 val typ_t = HOLogic.realT
350 val typ_bdv = HOLogic.realT
352 val vars_v = (* = [Free ("v", "real"), Free ("v", "'a")]*)
353 filter (fn t => curry op = (t |> dest_Free |> fst) "v") frees
354 val typs_v = (* = ["real", "'a"]*)
355 map (fn t => (t |> dest_Free |> snd)) vars_v;
357 val subst_ty = subst_typ "v" HOLogic.realT frees; (* = [("real", "real")]*)
358 if length subst_ty = 1 then () else error "Auto_Prog.subst_typ changed";
361 "-------- fun subst_typs -----------------------------------------------------------------------";
362 "-------- fun subst_typs -----------------------------------------------------------------------";
363 "-------- fun subst_typs -----------------------------------------------------------------------";
364 val prog = Auto_Prog.gen thy' t (assoc_rls "isolate_bdv");
365 val frees = vars prog; (* = [Free ("t_t", "'z"), Free ("v", "real"), Free ("v", "'a")]*)
366 if length frees = 2 then () else error "test setup Auto_Prog.subst_typs changed 1";
368 val args = formal_args prog; (* = [Free ("t_t", "'z"), Free ("v", "real")]*)
369 if length args = 2 then () else error "test setup Auto_Prog.subst_typs changed 2";
371 val prog' = subst_typs prog HOLogic.realT HOLogic.realT
372 val frees' = vars prog'; (* = [Free ("t_t", "'z"), Free ("v", "real")]*);
373 if length frees' = 2 then () else error "Auto_Prog.subst_typs changed 2"