31 |
31 |
32 Auto_Prog.gen thy' t rls; |
32 Auto_Prog.gen thy' t rls; |
33 "~~~~~ fun generate , args:"; val (thy, t, rls) = (thy', t, rls); |
33 "~~~~~ fun generate , args:"; val (thy, t, rls) = (thy', t, rls); |
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.Sequence {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.term 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" ^ |
113 "~~~~~ fun interSteps, args:"; val (cI, ip) = (1, ([1], Res)); |
113 "~~~~~ fun interSteps, args:"; val (cI, ip) = (1, ([1], Res)); |
114 val ((pt, p), tacis) = get_calc cI; |
114 val ((pt, p), tacis) = get_calc cI; |
115 (*if*) (not o is_interpos) ip = false; |
115 (*if*) (not o is_interpos) ip = false; |
116 val ip' = lev_pred' pt ip; |
116 val ip' = lev_pred' pt ip; |
117 |
117 |
118 (*Detail_Step.go pt ip ..ERROR interSteps>..>init_istate: "norm_Poly" has EmptyScr*) |
118 (*Detail_Step.go pt ip ..ERROR interSteps>..>init_istate: "norm_Poly" has Empty_Prog*) |
119 val ("donesteps", ctree_BEFORE_step_into, pos'_BEFORE_step_into) = Detail_Step.go pt ip; |
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); |
120 "~~~~~ fun go, args:"; val (pt, (pos as (p, _))) = (pt, ip); |
121 val nd = Ctree.get_nd pt p |
121 val nd = Ctree.get_nd pt p |
122 val cn = Ctree.children nd; |
122 val cn = Ctree.children nd; |
123 (*if*) null cn = false; |
123 (*if*) null cn = false; |
244 "-------- fun rule2stac, fun rule2stac_inst ----------------------------------------------------"; |
244 "-------- fun rule2stac, fun rule2stac_inst ----------------------------------------------------"; |
245 val t = rule2stac @{theory} (Thm ("real_diff_minus", ThmC.numerals_to_Free @{thm real_diff_minus})); |
245 val t = rule2stac @{theory} (Thm ("real_diff_minus", ThmC.numerals_to_Free @{thm real_diff_minus})); |
246 if UnparseC.term 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} (Eval ("Groups.plus_class.plus", eval_binop "#add_")); |
250 if UnparseC.term 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 Eval.. changed"; |
252 |
252 |
253 val t = rule2stac @{theory} (Rls_ rearrange_assoc); |
253 val t = rule2stac @{theory} (Rls_ rearrange_assoc); |
254 if UnparseC.term 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 |