71 val tid = HOLogic.dest_string thmID |
71 val tid = HOLogic.dest_string thmID |
72 in (Tactic.Rewrite (tid, ThmC.thm_from_thy thy tid)) end |
72 in (Tactic.Rewrite (tid, ThmC.thm_from_thy thy tid)) end |
73 | tac_from_prog _ thy (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Inst\<close>, _) $ sub $ thmID $ _) = |
73 | tac_from_prog _ thy (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Inst\<close>, _) $ sub $ thmID $ _) = |
74 let |
74 let |
75 val tid = HOLogic.dest_string thmID |
75 val tid = HOLogic.dest_string thmID |
76 in (Tactic.Rewrite_Inst (Subst.program_to_input sub, (tid, ThmC.thm_from_thy thy tid))) end |
76 val sub' = (**)Subst.program_to_input(** )Prog_Tac.Rewrite_Inst_adapt_to_type thy( **) sub |
|
77 in (Tactic.Rewrite_Inst (sub', (tid, ThmC.thm_from_thy thy tid))) end |
77 | tac_from_prog _ _ (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set\<close>,_) $ rls $ _) = |
78 | tac_from_prog _ _ (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set\<close>,_) $ rls $ _) = |
78 (Tactic.Rewrite_Set (HOLogic.dest_string rls)) |
79 (Tactic.Rewrite_Set (HOLogic.dest_string rls)) |
79 | tac_from_prog _ _ (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set_Inst\<close>, _) $ sub $ rls $ _) = |
80 | tac_from_prog _ thy (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set_Inst\<close>, _) $ sub $ rls $ _) = |
80 (Tactic.Rewrite_Set_Inst (Subst.program_to_input sub, HOLogic.dest_string rls)) |
81 let |
|
82 val sub' = (**)Subst.program_to_input(** )Prog_Tac.Rewrite_Inst_adapt_to_type thy( **) sub |
|
83 in (Tactic.Rewrite_Set_Inst (sub', HOLogic.dest_string rls)) end |
81 | tac_from_prog _ _ (Const (\<^const_name>\<open>Prog_Tac.Calculate\<close>, _) $ op_ $ _) = |
84 | tac_from_prog _ _ (Const (\<^const_name>\<open>Prog_Tac.Calculate\<close>, _) $ op_ $ _) = |
82 (Tactic.Calculate (HOLogic.dest_string op_)) |
85 (Tactic.Calculate (HOLogic.dest_string op_)) |
83 | tac_from_prog _ _ (Const (\<^const_name>\<open>Prog_Tac.Take\<close>, _) $ t) = (Tactic.Take (UnparseC.term t)) |
86 | tac_from_prog _ _ (Const (\<^const_name>\<open>Prog_Tac.Take\<close>, _) $ t) = (Tactic.Take (UnparseC.term t)) |
84 | tac_from_prog _ _ (Const (\<^const_name>\<open>Prog_Tac.Substitute\<close>, _) $ isasub $ _) = |
87 | tac_from_prog _ thy (Const (\<^const_name>\<open>Prog_Tac.Substitute\<close>, _) $ isasub $ _) = |
85 (Tactic.Substitute ((Subst.eqs_to_input o TermC.isalist2list) isasub)) |
88 Tactic.Substitute (Prog_Tac.Substitute_adapt_to_type thy isasub) |
86 | tac_from_prog _ thy (Const (\<^const_name>\<open>Prog_Tac.Check_elementwise\<close>, _) $ _ $ |
89 | tac_from_prog _ thy (Const (\<^const_name>\<open>Prog_Tac.Check_elementwise\<close>, _) $ _ $ |
87 (Const (\<^const_name>\<open>Collect\<close>, _) $ Abs (_, _, pred))) = |
90 (Const (\<^const_name>\<open>Collect\<close>, _) $ Abs (_, _, pred))) = |
88 (Tactic.Check_elementwise (UnparseC.term_in_thy thy pred)) |
91 (Tactic.Check_elementwise (UnparseC.term_in_thy thy pred)) |
89 | tac_from_prog _ _ (Const (\<^const_name>\<open>Prog_Tac.Or_to_List\<close>, _) $ _ ) = Tactic.Or_to_List |
92 | tac_from_prog _ _ (Const (\<^const_name>\<open>Prog_Tac.Or_to_List\<close>, _) $ _ ) = Tactic.Or_to_List |
90 | tac_from_prog pt _ (ptac as Const (\<^const_name>\<open>Prog_Tac.SubProblem\<close>, _) $ _ $ _) = |
93 | tac_from_prog pt _ (ptac as Const (\<^const_name>\<open>Prog_Tac.SubProblem\<close>, _) $ _ $ _) = |
339 if Config.get ctxt LI_trace then |
342 if Config.get ctxt LI_trace then |
340 tracing("@@@ " ^ call ^ " leaf '" ^ UnparseC.term t ^ "' \<longrightarrow> Expr \"" ^ UnparseC.term lexpr' ^ "\"") |
343 tracing("@@@ " ^ call ^ " leaf '" ^ UnparseC.term t ^ "' \<longrightarrow> Expr \"" ^ UnparseC.term lexpr' ^ "\"") |
341 else (); |
344 else (); |
342 (* |
345 (* |
343 check a leaf at the end of recursive descent; a leaf is either a Prog_Tac or a Prog_Expr. |
346 check a leaf at the end of recursive descent; a leaf is either a Prog_Tac or a Prog_Expr. |
344 snd of return value is the formal arguments in case of currying. |
347 snd of return value are the formal arguments in case of currying. |
345 *) |
348 *) |
346 fun check_leaf call ctxt srls (E, (a, v)) t = |
349 fun check_leaf call ctxt srls (E, (a, v)) t = |
347 case Prog_Tac.eval_leaf E a v t of |
350 case Prog_Tac.eval_leaf E a v t of |
348 (Program.Tac stac, a') => |
351 (Program.Tac stac, a') => |
349 let |
352 let |