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 = get_rls @{context} "integration";
29 val thy' = @{theory "Integrate"}
30 val ctxt = Proof_Context.init_global thy'
31 val t = @{term "ttt :: real"};
33 Auto_Prog.gen thy' t rls;
34 "~~~~~ fun gen , args:"; val (thy, t, rls) = (thy', t, rls);
35 val prog = case rls of
36 Rule_Set.Repeat {rules, ...} => rules2scr_Rls thy rules
37 | Rule_Set.Sequence {rules, ...} => rules2scr_Seq thy rules
38 val auto_script = subst_typs prog (type_of t) (TermC.guess_bdv_typ t) (*return from generate*);
40 if UnparseC.term auto_script =
41 "auto_generated_inst t_t v =\n" ^
42 "(Try (Rewrite_Set_Inst [(''bdv'', v)] ''integration_rules'') #>\n" ^
43 " Try (Rewrite_Set_Inst [(''bdv'', v)] ''add_new_c'') #>\n" ^
44 " Try (Rewrite_Set_Inst [(''bdv'', v)] ''simplify_Integral''))\n" ^
46 then () else error "Auto_Prog.gen integration CHANGED";
48 if contain_bdv (get_rules rls) then ()
49 else error "scrtools.sml: contain_bdv doesnt work for 'integration'";
51 if UnparseC.terms (formal_args auto_script) = "[\"t_t\", \"v\"]"
52 then () else error "formal_args of auto-gen.script changed";
54 Istate.init_detail (Rewrite_Set_Inst (["(''bdv'', x)"], "integration_rules")) (TermC.parse_test @{context} "someTermWithBdv");
55 "~~~~~ fun init_detail , args:"; val ((Tactic.Rewrite_Set_Inst (subs, rls)), t)
56 = ((Rewrite_Set_Inst (["(''bdv'', x)"], "integration_rules")), TermC.parse_test @{context} "someTermWithBdv");
57 val v = case Subst.T_from_input ctxt subs of
59 (*case*) get_rls ctxt 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 thy' = @{theory "Poly"}
66 val ctxt = Proof_Context.init_global thy'
67 val rls = get_rls ctxt "norm_Poly";
68 val t = @{term "ttt :: real"}
69 val auto_script = Auto_Prog.gen thy' t rls;
71 if UnparseC.term auto_script =
72 "auto_generated t_t =\n" ^
73 "(Try (Rewrite_Set ''discard_minus'') #>\n" ^
74 " Try (Rewrite_Set ''expand_poly_'') #>\n" ^
75 " Try (Repeat (Calculate ''TIMES'')) #>\n" ^
76 " Try (Rewrite_Set ''order_mult_rls_'') #>\n" ^
77 " Try (Rewrite_Set ''simplify_power_'') #>\n" ^
78 " Try (Rewrite_Set ''calc_add_mult_pow_'') #>\n" ^
79 " Try (Rewrite_Set ''reduce_012_mult_'') #>\n" ^
80 " Try (Rewrite_Set ''order_add_rls_'') #>\n" ^
81 " Try (Rewrite_Set ''collect_numerals_'') #>\n" ^
82 " Try (Rewrite_Set ''reduce_012_'') #>\n" ^
83 " Try (Rewrite_Set ''discard_parentheses1''))\n" ^
84 " ??.empty" (* ..WORKS, NEVERTHELESS*)
85 then () else error "Auto_Prog.gen norm_Poly CHANGED";
87 States.reset (); (*<-- evaluate, if ML-blocks are edited below*)
89 [(["Term (b + a - b)", "normalform N"],
90 ("Poly",["polynomial", "simplification"],
91 ["simplification", "for_polynomials"]))];
95 autoCalculate 1 CompleteCalc;
96 val ((pt,p),_) = States.get_calc 1;
99 (([], Frm), Simplify (b + a - b)),
100 (([1], Frm), b + a - b),
104 interSteps 1 ([], Res);
105 val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
106 Test_Tool.show_pt pt;
108 (([], Frm), Simplify (b + a - b)),
109 (([1], Frm), b + a - b),
113 interSteps 1 ([1], Res);(*<SYSERROR><CALCID>1</CALCID><ERROR>error in kernel 8</ERROR></SYSERROR>*)
114 "~~~~~ fun interSteps, args:"; val (cI, ip) = (1, ([1], Res));
115 val ((pt, p), tacis) = States.get_calc cI;
116 (*if*) (not o is_interpos) ip = false;
117 val ip' = lev_pred' pt ip;
119 (*Detail_Step.go pt ip ..ERROR interSteps>..>init_detail: "norm_Poly" has Empty_Prog*)
120 val ("donesteps", ctree_BEFORE_step_into, pos'_BEFORE_step_into) = Detail_Step.go pt ip;
121 "~~~~~ fun go, args:"; val (pt, (pos as (p, _))) = (pt, ip);
122 val nd = Ctree.get_nd pt p
123 val cn = Ctree.children nd;
124 (*if*) null cn = false;
126 "~~~~~ to detailrls return val:";
128 val return_val = ("donesteps", pt, (p @ [length (Ctree.children (Ctree.get_nd pt p))], Pos.Res));
129 if p @ [length (Ctree.children (Ctree.get_nd pt p))] = [1, 4]
130 then () else error "detailrls: auto-generated norm_Poly doesnt work";
132 val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
133 Test_Tool.show_pt pt; (*[
134 (([], Frm), Simplify (b + a - b)),
135 (([1], Frm), b + a - b),
136 (([1,1], Frm), b + a - b),
137 (([1,1], Res), b + a + -1 * b),
138 (([1,2], Res), a + b + -1 * b),
139 (([1,3], Res), a + 0 * b),
143 if existpt' ([1,4], Res) pt then ()
144 else error "auto-generated norm_Poly doesnt work";
147 "-------- test the same called by interSteps norm_Rational -------------------------------------";
148 "-------- test the same called by interSteps norm_Rational -------------------------------------";
149 "-------- test the same called by interSteps norm_Rational -------------------------------------";
150 val thy = @{theory (** )"Poly" ( **) Rational(**) (*required for rls "norm_Rational"*)}
151 val ctxt = Proof_Context.init_global thy
153 Auto_Prog.gen thy @{term "ttt :: real"} (get_rls ctxt "norm_Rational");
154 writeln(UnparseC.term auto_script);
155 TermC.atomty auto_script;
157 *** Const (Program.Stepwise, 'z => 'z => 'z)
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 (discard_minus, 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 (rat_mult_poly, 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 (make_rat_poly_with_parentheses, 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 (cancel_p_rls, ID)
175 *** . . . . . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
176 *** . . . . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
177 *** . . . . . . . Const (Program.Rewrite_Set, ID => 'a => 'a)
178 *** . . . . . . . . Free (norm_Rational_rls, ID)
179 *** . . . . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
180 *** . . . . . . . Const (Program.Rewrite_Set, ID => 'a => 'a)
181 *** . . . . . . . . Free (discard_parentheses1, ID)
182 *** . . Const (empty, 'a)
186 [(["Term (b + a - b)", "normalform N"],
187 ((** )"Poly"( **)"Rational"(**),["polynomial", "simplification"],
188 ["simplification", "of_rationals"]))];
191 autoCalculate 1 CompleteCalc;
193 interSteps 1 ([], Res);
194 val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
196 interSteps 1 ([1], Res);
197 val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
199 (*with "Program SimplifyScript (t_::real) = \
200 \ ((Rewrite_Set norm_Rational) t_)"
201 val (Form form, SOME tac, asm) = ME_Misc.pt_extract (pt, ([1], Res));
203 val (Form form, SOME tac, asm) = ME_Misc.pt_extract (pt, ([2], Res));
204 case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of
205 ("a", Check_Postcond ["polynomial", "simplification"], []) => ()
206 | _ => error "scrtools.sml: auto-generated norm_Rational doesnt work";
209 "-------- fun op #> ----------------------------------------------------------------------------";
210 "-------- fun op #> ----------------------------------------------------------------------------";
211 "-------- fun op #> ----------------------------------------------------------------------------";
212 val rules = (#rules o Rule_Set.rep) isolate_root;
213 val rs = map (rule2stac @{theory}) rules;
215 if UnparseC.term t = "Try (Repeat (Rewrite ''rroot_to_lhs'')) #>\n" ^
216 "Try (Repeat (Rewrite ''rroot_to_lhs_mult'')) #>\n" ^
217 "Try (Repeat (Rewrite ''rroot_to_lhs_add_mult'')) #>\n" ^
218 "Try (Repeat (Rewrite ''risolate_root_add'')) #>\n" ^
219 "Try (Repeat (Rewrite ''risolate_root_mult'')) #>\n" ^
220 "Try (Repeat (Rewrite ''risolate_root_div''))"
221 then () else error "fun #> changed"
224 "-------- fun rules2scr_Rls --------------------------------------------------------------------";
225 "-------- fun rules2scr_Rls --------------------------------------------------------------------";
226 "-------- fun rules2scr_Rls --------------------------------------------------------------------";
227 (*compare Prog_Expr.*)
228 val prog = Auto_Prog.rules2scr_Rls @{theory} [\<^rule_thm>\<open>thm111\<close>, \<^rule_thm>\<open>refl\<close>]
230 writeln (UnparseC.term_in_thy @{theory} prog);
231 (*auto_generated t_t =
233 ((Try (Repeat (Rewrite ''thm111'')) #>
234 Try (Repeat (Rewrite ''refl'')))
237 if UnparseC.term_in_thy @{theory} prog =
238 "auto_generated t_t =\n" ^
240 " ((Try (Repeat (Rewrite ''thm111'')) #> Try (Repeat (Rewrite ''refl'')))\n" ^
242 then () else error "rules2scr_Rls auto_generated changed";
245 "-------- fun rule2stac, fun rule2stac_inst ----------------------------------------------------";
246 "-------- fun rule2stac, fun rule2stac_inst ----------------------------------------------------";
247 "-------- fun rule2stac, fun rule2stac_inst ----------------------------------------------------";
248 val t = rule2stac @{theory} (Thm ("real_diff_minus", @{thm real_diff_minus}));
249 if UnparseC.term t = "Try (Repeat (Rewrite ''real_diff_minus''))" then ()
250 else error "rule2stac Thm.. changed";
252 val t = rule2stac @{theory} (Eval (\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_"));
253 if UnparseC.term t = "Try (Repeat (Calculate ''PLUS''))" then ()
254 else error "rule2stac Eval.. changed";
256 val t = rule2stac @{theory} (Rls_ rearrange_assoc);
257 if UnparseC.term t = "Try (Rewrite_Set ''rearrange_assoc'')" then ()
258 else error "rule2stac Rls_.. changed";
260 val t = rule2stac_inst @{theory} (Thm ("risolate_bdv_add", @{thm risolate_bdv_add}));
261 if UnparseC.term t = "Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_add''))" then ()
262 else error "rule2stac_inst Thm.. changed";
264 (Const (\<^const_name>\<open>Try\<close>, _) $
265 (Const (\<^const_name>\<open>Repeat\<close>, _) $
266 (Const (\<^const_name>\<open>Rewrite_Inst\<close>, _) $
267 (Const (\<^const_name>\<open>Cons\<close>, _) $
268 (Const (\<^const_name>\<open>Pair\<close>, _) $
271 Const (\<^const_name>\<open>Nil\<close>, _)) $
272 risolate_bdv_add))) =>
273 (if HOLogic.dest_string bdv = "bdv" andalso
274 HOLogic.dest_string risolate_bdv_add = "risolate_bdv_add" then ()
275 else error "rule2stac_inst changed 1")
276 | _ => error "rule2stac_inst changed 2";
279 "-------- fun stacpbls, fun eval_leaf -----------------------------------";
280 "-------- fun stacpbls, fun eval_leaf -----------------------------------";
281 "-------- fun stacpbls, fun eval_leaf -----------------------------------";
282 val {scr, ...} = MethodC.from_store ctxt ["Test", "sqrt-equ-test"]; val Prog sc = scr; val ts = stacpbls sc;
284 [Const (\<^const_name>\<open>Rewrite\<close>, _) $ square_equation_left,
285 Const (\<^const_name>\<open>Rewrite_Set\<close>, _) $ Test_simplify,
286 Const (\<^const_name>\<open>Rewrite_Set\<close>, _) $ rearrange_assoc,
287 Const (\<^const_name>\<open>Rewrite_Set\<close>, _) $ isolate_root,
288 Const (\<^const_name>\<open>Rewrite_Set\<close>, _) $ norm_equation,
289 Const (\<^const_name>\<open>Rewrite_Set_Inst\<close>, _) $
290 (Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>Pair\<close>, _) $ bdv $ Free ("v_v", _)) $
291 Const (\<^const_name>\<open>Nil\<close>, _)) $ isolate_bdv] =>
292 if HOLogic.dest_string square_equation_left = "square_equation_left" andalso
293 HOLogic.dest_string Test_simplify = "Test_simplify" andalso
294 HOLogic.dest_string rearrange_assoc = "rearrange_assoc" andalso
295 HOLogic.dest_string isolate_root = "isolate_root" andalso
296 HOLogic.dest_string norm_equation = "norm_equation" andalso
297 HOLogic.dest_string bdv = "bdv" andalso
298 HOLogic.dest_string isolate_bdv = "isolate_bdv"
299 then () else error "stacpbls (Test.Solve_root_equation) changed 2"
300 | _ => error "stacpbls (Test.Solve_root_equation) changed 1";
302 (* inappropriate input is skipped *)
303 val t = @{term "(a::real) = (rhs (NTH 1 sol_a))"};
304 case stacpbls t of [] => () | _ => error "stacpbls rhs (NTH 1 sol_a) changed";
306 @{term "(SubProblem (BiegelinieX,[vonBelastungZu,Biegelinien], [Biegelinien,ausBelastung]) [REAL q__q, REAL v_v])"};
307 case stacpbls t of [] => () | _ => error "stacpbls (SubProblem ...) changed";
310 "-------- fun is_calc, fun op_of_calc ----------------------------------------------------------";
311 "-------- fun is_calc, fun op_of_calc ----------------------------------------------------------";
312 "-------- fun is_calc, fun op_of_calc ----------------------------------------------------------";
313 val rls = prep_rls @{theory} Test_simplify; (* adds the Program *)
314 val sc = Auto_Prog.gen thy' t rls;
315 val stacs = stacpbls sc;
317 val calcs = filter is_calc stacs;
318 val ids = map op_of_calc calcs;
320 ["PLUS", "TIMES", "DIVIDE", "POWER"] => ()
321 | _ => error "op_of_calc";
323 val calcs = ((get_calc (@{theory} |> Proof_Context.init_global) |> map) o (map Auto_Prog.op_of_calc) o
324 (filter Auto_Prog.is_calc) o Auto_Prog.stacpbls) sc;
326 [("PLUS", (\<^const_name>\<open>plus\<close>, _)), ("TIMES", (\<^const_name>\<open>times\<close>, _)),
327 ("DIVIDE", (\<^const_name>\<open>divide\<close>, _)), ("POWER", (\<^const_name>\<open>realpow\<close>, _))] => ()
328 | _ => error "get_calcs changed"
331 "-------- fun subst_typ ------------------------------------------------------------------------";
332 "-------- fun subst_typ ------------------------------------------------------------------------";
333 "-------- fun subst_typ ------------------------------------------------------------------------";
334 val thy = @{theory "Isac_Knowledge"}
335 val ctxt = Proof_Context.init_global thy
336 val prog = Auto_Prog.gen thy t (get_rls ctxt "isolate_bdv");
337 (* UnparseC.term prog |> writeln
338 auto_generated_inst t_t v =
340 ((Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_add'')) #>
341 Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_mult_add'')) #>
342 Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_mult'')) #>
343 Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''mult_square'')) #>
344 Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''constant_square'')) #>
345 Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''constant_mult_square'')))
349 val frees = vars prog; (* = [Free ("t_t", "'z"), Free ("v", "real")]*)
350 if length frees = 2 then () else error "test setup Auto_Prog.subst_typ changed 1";
352 val args = formal_args prog; (* = [Free ("t_t", "'z"), Free ("v", "real")]*)
353 if length args = 2 then () else error "test setup Auto_Prog.subst_typ changed 2";
355 val typ_t = HOLogic.realT
356 val typ_bdv = HOLogic.realT
358 val vars_v = (* = [Free ("v", "real"), Free ("v", "'a")]*)
359 filter (fn t => curry op = (t |> dest_Free |> fst) "v") frees
360 val typs_v = (* = ["real", "'a"]*)
361 map (fn t => (t |> dest_Free |> snd)) vars_v;
363 val subst_ty = subst_typ "v" HOLogic.realT frees; (* = [("real", "real")]*)
364 if length subst_ty = 1 then () else error "Auto_Prog.subst_typ changed";
367 "-------- fun subst_typs -----------------------------------------------------------------------";
368 "-------- fun subst_typs -----------------------------------------------------------------------";
369 "-------- fun subst_typs -----------------------------------------------------------------------";
370 val prog = Auto_Prog.gen thy' t (get_rls ctxt "isolate_bdv");
371 val frees = vars prog; (* = [Free ("t_t", "'z"), Free ("v", "real"), Free ("v", "'a")]*)
372 if length frees = 2 then () else error "test setup Auto_Prog.subst_typs changed 1";
374 val args = formal_args prog; (* = [Free ("t_t", "'z"), Free ("v", "real")]*)
375 if length args = 2 then () else error "test setup Auto_Prog.subst_typs changed 2";
377 val prog' = subst_typs prog HOLogic.realT HOLogic.realT
378 val frees' = vars prog'; (* = [Free ("t_t", "'z"), Free ("v", "real")]*);
379 if length frees' = 2 then () else error "Auto_Prog.subst_typs changed 2"