8 "table of contents -----------------------------------------------------------------------------"; |
8 "table of contents -----------------------------------------------------------------------------"; |
9 "-----------------------------------------------------------------------------------------------"; |
9 "-----------------------------------------------------------------------------------------------"; |
10 "-------- check auto-gen.script for Rewrite_Set_Inst -------------------------------------------"; |
10 "-------- check auto-gen.script for Rewrite_Set_Inst -------------------------------------------"; |
11 "-------- test the same called by interSteps norm_Poly -----------------------------------------"; |
11 "-------- test the same called by interSteps norm_Poly -----------------------------------------"; |
12 "-------- test the same called by interSteps norm_Rational -------------------------------------"; |
12 "-------- test the same called by interSteps norm_Rational -------------------------------------"; |
13 "-------- fun op @@ ----------------------------------------------------------------------------"; |
13 "-------- fun op #> ----------------------------------------------------------------------------"; |
14 "-------- fun rules2scr_Rls --------------------------------------------------------------------"; |
14 "-------- fun rules2scr_Rls --------------------------------------------------------------------"; |
15 "-------- fun rule2stac, fun rule2stac_inst ----------------------------------------------------"; |
15 "-------- fun rule2stac, fun rule2stac_inst ----------------------------------------------------"; |
16 "-------- fun stacpbls -------------------------------------------------------------------------"; |
16 "-------- fun stacpbls -------------------------------------------------------------------------"; |
17 "-------- fun is_calc, fun op_of_calc ----------------------------------------------------------"; |
17 "-------- fun is_calc, fun op_of_calc ----------------------------------------------------------"; |
18 "-------- fun subst_typ ------------------------------------------------------------------------"; |
18 "-------- fun subst_typ ------------------------------------------------------------------------"; |
41 "-------- test the same called by interSteps norm_Poly -----------------------------------------"; |
41 "-------- test the same called by interSteps norm_Poly -----------------------------------------"; |
42 "-------- test the same called by interSteps norm_Poly -----------------------------------------"; |
42 "-------- test the same called by interSteps norm_Poly -----------------------------------------"; |
43 val Seq {scr = Prog auto_script,...} = assoc_rls "norm_Poly"; |
43 val Seq {scr = Prog auto_script,...} = assoc_rls "norm_Poly"; |
44 writeln(term2str auto_script); |
44 writeln(term2str auto_script); |
45 (*Program Stepwise t_t = |
45 (*Program Stepwise t_t = |
46 (Try (Rewrite_Set discard_minus) @@ |
46 (Try (Rewrite_Set discard_minus) #> |
47 Try (Rewrite_Set expand_poly_) @@ |
47 Try (Rewrite_Set expand_poly_) #> |
48 Try (Repeat (Calculate TIMES)) @@ |
48 Try (Repeat (Calculate TIMES)) #> |
49 Try (Rewrite_Set order_mult_rls_) @@ |
49 Try (Rewrite_Set order_mult_rls_) #> |
50 Try (Rewrite_Set simplify_power_) @@ |
50 Try (Rewrite_Set simplify_power_) #> |
51 Try (Rewrite_Set calc_add_mult_pow_) @@ |
51 Try (Rewrite_Set calc_add_mult_pow_) #> |
52 Try (Rewrite_Set reduce_012_mult_) @@ |
52 Try (Rewrite_Set reduce_012_mult_) #> |
53 Try (Rewrite_Set order_add_rls_) @@ |
53 Try (Rewrite_Set order_add_rls_) #> |
54 Try (Rewrite_Set collect_numerals_) @@ |
54 Try (Rewrite_Set collect_numerals_) #> |
55 Try (Rewrite_Set reduce_012_) @@ |
55 Try (Rewrite_Set reduce_012_) #> |
56 Try (Rewrite_Set discard_parentheses1)) |
56 Try (Rewrite_Set discard_parentheses1)) |
57 ??.empty ..WORKS, NEVERTHELESS *) |
57 ??.empty ..WORKS, NEVERTHELESS *) |
58 atomty auto_script; |
58 atomty auto_script; |
59 |
59 |
60 reset_states (); (*<-- evaluate, if ML-blocks are edited below*) |
60 reset_states (); (*<-- evaluate, if ML-blocks are edited below*) |
172 val (Form form, SOME tac, asm) = pt_extract (pt, ([2], Res)); |
172 val (Form form, SOME tac, asm) = pt_extract (pt, ([2], Res)); |
173 case (term2str form, tac, terms2strs asm) of |
173 case (term2str form, tac, terms2strs asm) of |
174 ("a", Check_Postcond ["polynomial", "simplification"], []) => () |
174 ("a", Check_Postcond ["polynomial", "simplification"], []) => () |
175 | _ => error "scrtools.sml: auto-generated norm_Rational doesnt work"; |
175 | _ => error "scrtools.sml: auto-generated norm_Rational doesnt work"; |
176 |
176 |
177 "-------- fun op @@ ----------------------------------------------------------------------------"; |
177 "-------- fun op #> ----------------------------------------------------------------------------"; |
178 "-------- fun op @@ ----------------------------------------------------------------------------"; |
178 "-------- fun op #> ----------------------------------------------------------------------------"; |
179 "-------- fun op @@ ----------------------------------------------------------------------------"; |
179 "-------- fun op #> ----------------------------------------------------------------------------"; |
180 val rules = (#rules o rep_rls) isolate_root; |
180 val rules = (#rules o rep_rls) isolate_root; |
181 val rs = map (rule2stac @{theory}) rules; |
181 val rs = map (rule2stac @{theory}) rules; |
182 val t = @@ rs; |
182 val t = #> rs; |
183 if term2str t = "Try (Repeat (Rewrite ''rroot_to_lhs'')) @@\n" ^ |
183 if term2str t = "Try (Repeat (Rewrite ''rroot_to_lhs'')) #>\n" ^ |
184 "Try (Repeat (Rewrite ''rroot_to_lhs_mult'')) @@\n" ^ |
184 "Try (Repeat (Rewrite ''rroot_to_lhs_mult'')) #>\n" ^ |
185 "Try (Repeat (Rewrite ''rroot_to_lhs_add_mult'')) @@\n" ^ |
185 "Try (Repeat (Rewrite ''rroot_to_lhs_add_mult'')) #>\n" ^ |
186 "Try (Repeat (Rewrite ''risolate_root_add'')) @@\n" ^ |
186 "Try (Repeat (Rewrite ''risolate_root_add'')) #>\n" ^ |
187 "Try (Repeat (Rewrite ''risolate_root_mult'')) @@\n" ^ |
187 "Try (Repeat (Rewrite ''risolate_root_mult'')) #>\n" ^ |
188 "Try (Repeat (Rewrite ''risolate_root_div''))" |
188 "Try (Repeat (Rewrite ''risolate_root_div''))" |
189 then () else error "fun @@ changed" |
189 then () else error "fun #> changed" |
190 |
190 |
191 "-------- fun rules2scr_Rls --------------------------------------------------------------------"; |
191 "-------- fun rules2scr_Rls --------------------------------------------------------------------"; |
192 "-------- fun rules2scr_Rls --------------------------------------------------------------------"; |
192 "-------- fun rules2scr_Rls --------------------------------------------------------------------"; |
193 "-------- fun rules2scr_Rls --------------------------------------------------------------------"; |
193 "-------- fun rules2scr_Rls --------------------------------------------------------------------"; |
194 (*compare Prog_Expr.*) |
194 (*compare Prog_Expr.*) |
195 val prog = Auto_Prog.rules2scr_Rls @{theory} [Rule.Thm ("thm111", @{thm thm111}), Rule.Thm ("refl", @{thm refl})] |
195 val prog = Auto_Prog.rules2scr_Rls @{theory} [Rule.Thm ("thm111", @{thm thm111}), Rule.Thm ("refl", @{thm refl})] |
196 ; |
196 ; |
197 writeln (t2str @{theory} prog); |
197 writeln (t2str @{theory} prog); |
198 (*auto_generated t_t = |
198 (*auto_generated t_t = |
199 Repeat |
199 Repeat |
200 ((Try (Repeat (Rewrite ''thm111'')) @@ |
200 ((Try (Repeat (Rewrite ''thm111'')) #> |
201 Try (Repeat (Rewrite ''refl''))) |
201 Try (Repeat (Rewrite ''refl''))) |
202 ??.empty)*) |
202 ??.empty)*) |
203 ; |
203 ; |
204 if t2str @{theory} prog = |
204 if t2str @{theory} prog = |
205 "auto_generated t_t =\n" ^ |
205 "auto_generated t_t =\n" ^ |
206 "Repeat\n" ^ |
206 "Repeat\n" ^ |
207 " ((Try (Repeat (Rewrite ''thm111'')) @@ Try (Repeat (Rewrite ''refl'')))\n" ^ |
207 " ((Try (Repeat (Rewrite ''thm111'')) #> Try (Repeat (Rewrite ''refl'')))\n" ^ |
208 " ??.empty)" |
208 " ??.empty)" |
209 then () else error "rules2scr_Rls auto_generated changed"; |
209 then () else error "rules2scr_Rls auto_generated changed"; |
210 |
210 |
211 "-------- fun rule2stac, fun rule2stac_inst ----------------------------------------------------"; |
211 "-------- fun rule2stac, fun rule2stac_inst ----------------------------------------------------"; |
212 "-------- fun rule2stac, fun rule2stac_inst ----------------------------------------------------"; |
212 "-------- fun rule2stac, fun rule2stac_inst ----------------------------------------------------"; |
296 "-------- fun subst_typ ------------------------------------------------------------------------"; |
296 "-------- fun subst_typ ------------------------------------------------------------------------"; |
297 val Rule.Rls {scr = Prog prog, ...} = assoc_rls "isolate_bdv"; |
297 val Rule.Rls {scr = Prog prog, ...} = assoc_rls "isolate_bdv"; |
298 (* term2str prog |> writeln |
298 (* term2str prog |> writeln |
299 auto_generated_inst t_t v = |
299 auto_generated_inst t_t v = |
300 Repeat |
300 Repeat |
301 ((Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_add'')) @@ |
301 ((Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_add'')) #> |
302 Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_mult_add'')) @@ |
302 Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_mult_add'')) #> |
303 Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_mult'')) @@ |
303 Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_mult'')) #> |
304 Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''mult_square'')) @@ |
304 Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''mult_square'')) #> |
305 Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''constant_square'')) @@ |
305 Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''constant_square'')) #> |
306 Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''constant_mult_square''))) |
306 Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''constant_mult_square''))) |
307 ??.empty) |
307 ??.empty) |
308 *) |
308 *) |
309 |
309 |
310 val frees = vars prog; (* = [Free ("t_t", "'z"), Free ("v", "real"), Free ("v", "'a")]*) |
310 val frees = vars prog; (* = [Free ("t_t", "'z"), Free ("v", "real"), Free ("v", "'a")]*) |