34 val prog = case rls of |
34 val prog = case rls of |
35 Rule_Set.Repeat {rules, ...} => rules2scr_Rls thy rules |
35 Rule_Set.Repeat {rules, ...} => rules2scr_Rls thy rules |
36 | Rule_Set.Seqence {rules, ...} => rules2scr_Seq thy rules |
36 | Rule_Set.Seqence {rules, ...} => rules2scr_Seq thy rules |
37 val auto_script = subst_typs prog (type_of t) (TermC.guess_bdv_typ t) (*return from generate*); |
37 val auto_script = subst_typs prog (type_of t) (TermC.guess_bdv_typ t) (*return from generate*); |
38 |
38 |
39 if UnparseC.term2str auto_script = |
39 if UnparseC.term auto_script = |
40 "auto_generated_inst t_t v =\n" ^ |
40 "auto_generated_inst t_t v =\n" ^ |
41 "(Try (Rewrite_Set_Inst [(''bdv'', v)] ''integration_rules'') #>\n" ^ |
41 "(Try (Rewrite_Set_Inst [(''bdv'', v)] ''integration_rules'') #>\n" ^ |
42 " Try (Rewrite_Set_Inst [(''bdv'', v)] ''add_new_c'') #>\n" ^ |
42 " Try (Rewrite_Set_Inst [(''bdv'', v)] ''add_new_c'') #>\n" ^ |
43 " Try (Rewrite_Set_Inst [(''bdv'', v)] ''simplify_Integral''))\n" ^ |
43 " Try (Rewrite_Set_Inst [(''bdv'', v)] ''simplify_Integral''))\n" ^ |
44 " ??.empty" |
44 " ??.empty" |
45 then () else error "Auto_Prog.gen integration CHANGED"; |
45 then () else error "Auto_Prog.gen integration CHANGED"; |
46 |
46 |
47 if contain_bdv (get_rules rls) then () |
47 if contain_bdv (get_rules rls) then () |
48 else error "scrtools.sml: contain_bdv doesnt work for 'integration'"; |
48 else error "scrtools.sml: contain_bdv doesnt work for 'integration'"; |
49 |
49 |
50 if UnparseC.terms2str (formal_args auto_script) = "[\"t_t\",\"v\"]" |
50 if UnparseC.terms (formal_args auto_script) = "[\"t_t\",\"v\"]" |
51 then () else error "formal_args of auto-gen.script changed"; |
51 then () else error "formal_args of auto-gen.script changed"; |
52 |
52 |
53 init_istate (Rewrite_Set_Inst (["(''bdv'', x)"], "integration_rules")) |
53 init_istate (Rewrite_Set_Inst (["(''bdv'', x)"], "integration_rules")) |
54 (str2term "someTermWithBdv"); |
54 (str2term "someTermWithBdv"); |
55 "~~~~~ fun init_istate , args:"; val ((Tactic.Rewrite_Set_Inst (subs, rls)), t) |
55 "~~~~~ fun init_istate , args:"; val ((Tactic.Rewrite_Set_Inst (subs, rls)), t) |
65 val rls = assoc_rls "norm_Poly"; |
65 val rls = assoc_rls "norm_Poly"; |
66 val thy' = @{theory "Poly"} |
66 val thy' = @{theory "Poly"} |
67 val t = @{term "ttt :: real"} |
67 val t = @{term "ttt :: real"} |
68 val auto_script = Auto_Prog.gen thy' t rls; |
68 val auto_script = Auto_Prog.gen thy' t rls; |
69 |
69 |
70 if UnparseC.term2str auto_script = |
70 if UnparseC.term auto_script = |
71 "auto_generated t_t =\n" ^ |
71 "auto_generated t_t =\n" ^ |
72 "(Try (Rewrite_Set ''discard_minus'') #>\n" ^ |
72 "(Try (Rewrite_Set ''discard_minus'') #>\n" ^ |
73 " Try (Rewrite_Set ''expand_poly_'') #>\n" ^ |
73 " Try (Rewrite_Set ''expand_poly_'') #>\n" ^ |
74 " Try (Repeat (Calculate ''TIMES'')) #>\n" ^ |
74 " Try (Repeat (Calculate ''TIMES'')) #>\n" ^ |
75 " Try (Rewrite_Set ''order_mult_rls_'') #>\n" ^ |
75 " Try (Rewrite_Set ''order_mult_rls_'') #>\n" ^ |
146 "-------- 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 -------------------------------------"; |
147 "-------- test the same called by interSteps norm_Rational -------------------------------------"; |
148 "-------- test the same called by interSteps norm_Rational -------------------------------------"; |
148 "-------- test the same called by interSteps norm_Rational -------------------------------------"; |
149 val auto_script = |
149 val auto_script = |
150 Auto_Prog.gen @{theory "Poly"} @{term "ttt :: real"} (assoc_rls "norm_Rational"); |
150 Auto_Prog.gen @{theory "Poly"} @{term "ttt :: real"} (assoc_rls "norm_Rational"); |
151 writeln(UnparseC.term2str auto_script); |
151 writeln(UnparseC.term auto_script); |
152 atomty auto_script; |
152 atomty auto_script; |
153 (*** |
153 (*** |
154 *** Const (Program.Stepwise, 'z => 'z => 'z) |
154 *** Const (Program.Stepwise, 'z => 'z => 'z) |
155 *** . Free (t_t, 'z) |
155 *** . Free (t_t, 'z) |
156 *** . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a) |
156 *** . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a) |
196 (*with "Program SimplifyScript (t_::real) = \ |
196 (*with "Program SimplifyScript (t_::real) = \ |
197 \ ((Rewrite_Set norm_Rational) t_)" |
197 \ ((Rewrite_Set norm_Rational) t_)" |
198 val (Form form, SOME tac, asm) = pt_extract (pt, ([1], Res)); |
198 val (Form form, SOME tac, asm) = pt_extract (pt, ([1], Res)); |
199 *) |
199 *) |
200 val (Form form, SOME tac, asm) = pt_extract (pt, ([2], Res)); |
200 val (Form form, SOME tac, asm) = pt_extract (pt, ([2], Res)); |
201 case (UnparseC.term2str form, tac, UnparseC.terms2strs asm) of |
201 case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of |
202 ("a", Check_Postcond ["polynomial", "simplification"], []) => () |
202 ("a", Check_Postcond ["polynomial", "simplification"], []) => () |
203 | _ => error "scrtools.sml: auto-generated norm_Rational doesnt work"; |
203 | _ => error "scrtools.sml: auto-generated norm_Rational doesnt work"; |
204 |
204 |
205 |
205 |
206 "-------- fun op #> ----------------------------------------------------------------------------"; |
206 "-------- fun op #> ----------------------------------------------------------------------------"; |
207 "-------- fun op #> ----------------------------------------------------------------------------"; |
207 "-------- fun op #> ----------------------------------------------------------------------------"; |
208 "-------- fun op #> ----------------------------------------------------------------------------"; |
208 "-------- fun op #> ----------------------------------------------------------------------------"; |
209 val rules = (#rules o Rule_Set.rep) isolate_root; |
209 val rules = (#rules o Rule_Set.rep) isolate_root; |
210 val rs = map (rule2stac @{theory}) rules; |
210 val rs = map (rule2stac @{theory}) rules; |
211 val t = #> rs; |
211 val t = #> rs; |
212 if UnparseC.term2str t = "Try (Repeat (Rewrite ''rroot_to_lhs'')) #>\n" ^ |
212 if UnparseC.term t = "Try (Repeat (Rewrite ''rroot_to_lhs'')) #>\n" ^ |
213 "Try (Repeat (Rewrite ''rroot_to_lhs_mult'')) #>\n" ^ |
213 "Try (Repeat (Rewrite ''rroot_to_lhs_mult'')) #>\n" ^ |
214 "Try (Repeat (Rewrite ''rroot_to_lhs_add_mult'')) #>\n" ^ |
214 "Try (Repeat (Rewrite ''rroot_to_lhs_add_mult'')) #>\n" ^ |
215 "Try (Repeat (Rewrite ''risolate_root_add'')) #>\n" ^ |
215 "Try (Repeat (Rewrite ''risolate_root_add'')) #>\n" ^ |
216 "Try (Repeat (Rewrite ''risolate_root_mult'')) #>\n" ^ |
216 "Try (Repeat (Rewrite ''risolate_root_mult'')) #>\n" ^ |
217 "Try (Repeat (Rewrite ''risolate_root_div''))" |
217 "Try (Repeat (Rewrite ''risolate_root_div''))" |
222 "-------- fun rules2scr_Rls --------------------------------------------------------------------"; |
222 "-------- fun rules2scr_Rls --------------------------------------------------------------------"; |
223 "-------- fun rules2scr_Rls --------------------------------------------------------------------"; |
223 "-------- fun rules2scr_Rls --------------------------------------------------------------------"; |
224 (*compare Prog_Expr.*) |
224 (*compare Prog_Expr.*) |
225 val prog = Auto_Prog.rules2scr_Rls @{theory} [Rule.Thm ("thm111", @{thm thm111}), Rule.Thm ("refl", @{thm refl})] |
225 val prog = Auto_Prog.rules2scr_Rls @{theory} [Rule.Thm ("thm111", @{thm thm111}), Rule.Thm ("refl", @{thm refl})] |
226 ; |
226 ; |
227 writeln (UnparseC.t2str @{theory} prog); |
227 writeln (UnparseC.term_thy @{theory} prog); |
228 (*auto_generated t_t = |
228 (*auto_generated t_t = |
229 Repeat |
229 Repeat |
230 ((Try (Repeat (Rewrite ''thm111'')) #> |
230 ((Try (Repeat (Rewrite ''thm111'')) #> |
231 Try (Repeat (Rewrite ''refl''))) |
231 Try (Repeat (Rewrite ''refl''))) |
232 ??.empty)*) |
232 ??.empty)*) |
233 ; |
233 ; |
234 if UnparseC.t2str @{theory} prog = |
234 if UnparseC.term_thy @{theory} prog = |
235 "auto_generated t_t =\n" ^ |
235 "auto_generated t_t =\n" ^ |
236 "Repeat\n" ^ |
236 "Repeat\n" ^ |
237 " ((Try (Repeat (Rewrite ''thm111'')) #> Try (Repeat (Rewrite ''refl'')))\n" ^ |
237 " ((Try (Repeat (Rewrite ''thm111'')) #> Try (Repeat (Rewrite ''refl'')))\n" ^ |
238 " ??.empty)" |
238 " ??.empty)" |
239 then () else error "rules2scr_Rls auto_generated changed"; |
239 then () else error "rules2scr_Rls auto_generated changed"; |
241 |
241 |
242 "-------- fun rule2stac, fun rule2stac_inst ----------------------------------------------------"; |
242 "-------- fun rule2stac, fun rule2stac_inst ----------------------------------------------------"; |
243 "-------- fun rule2stac, fun rule2stac_inst ----------------------------------------------------"; |
243 "-------- fun rule2stac, fun rule2stac_inst ----------------------------------------------------"; |
244 "-------- 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})); |
245 val t = rule2stac @{theory} (Thm ("real_diff_minus", num_str @{thm real_diff_minus})); |
246 if UnparseC.term2str t = "Try (Repeat (Rewrite ''real_diff_minus''))" then () |
246 if UnparseC.term t = "Try (Repeat (Rewrite ''real_diff_minus''))" then () |
247 else error "rule2stac Thm.. changed"; |
247 else error "rule2stac Thm.. changed"; |
248 |
248 |
249 val t = rule2stac @{theory} (Num_Calc ("Groups.plus_class.plus", eval_binop "#add_")); |
249 val t = rule2stac @{theory} (Num_Calc ("Groups.plus_class.plus", eval_binop "#add_")); |
250 if UnparseC.term2str t = "Try (Repeat (Calculate ''PLUS''))" then () |
250 if UnparseC.term t = "Try (Repeat (Calculate ''PLUS''))" then () |
251 else error "rule2stac Num_Calc.. changed"; |
251 else error "rule2stac Num_Calc.. changed"; |
252 |
252 |
253 val t = rule2stac @{theory} (Rls_ rearrange_assoc); |
253 val t = rule2stac @{theory} (Rls_ rearrange_assoc); |
254 if UnparseC.term2str t = "Try (Rewrite_Set ''rearrange_assoc'')" then () |
254 if UnparseC.term t = "Try (Rewrite_Set ''rearrange_assoc'')" then () |
255 else error "rule2stac Rls_.. changed"; |
255 else error "rule2stac Rls_.. changed"; |
256 |
256 |
257 val t = rule2stac_inst @{theory} (Thm ("risolate_bdv_add", num_str @{thm risolate_bdv_add})); |
257 val t = rule2stac_inst @{theory} (Thm ("risolate_bdv_add", num_str @{thm risolate_bdv_add})); |
258 if UnparseC.term2str t = "Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_add''))" then () |
258 if UnparseC.term t = "Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_add''))" then () |
259 else error "rule2stac_inst Thm.. changed"; |
259 else error "rule2stac_inst Thm.. changed"; |
260 case t of |
260 case t of |
261 (Const ("Tactical.Try", _) $ |
261 (Const ("Tactical.Try", _) $ |
262 (Const ("Tactical.Repeat", _) $ |
262 (Const ("Tactical.Repeat", _) $ |
263 (Const ("Prog_Tac.Rewrite'_Inst", _) $ |
263 (Const ("Prog_Tac.Rewrite'_Inst", _) $ |
327 |
327 |
328 "-------- fun subst_typ ------------------------------------------------------------------------"; |
328 "-------- fun subst_typ ------------------------------------------------------------------------"; |
329 "-------- fun subst_typ ------------------------------------------------------------------------"; |
329 "-------- fun subst_typ ------------------------------------------------------------------------"; |
330 "-------- fun subst_typ ------------------------------------------------------------------------"; |
330 "-------- fun subst_typ ------------------------------------------------------------------------"; |
331 val prog = Auto_Prog.gen @{theory Isac_Knowledge} t (assoc_rls "isolate_bdv"); |
331 val prog = Auto_Prog.gen @{theory Isac_Knowledge} t (assoc_rls "isolate_bdv"); |
332 (* UnparseC.term2str prog |> writeln |
332 (* UnparseC.term prog |> writeln |
333 auto_generated_inst t_t v = |
333 auto_generated_inst t_t v = |
334 Repeat |
334 Repeat |
335 ((Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_add'')) #> |
335 ((Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_add'')) #> |
336 Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_mult_add'')) #> |
336 Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_mult_add'')) #> |
337 Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_mult'')) #> |
337 Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_mult'')) #> |