61 sig |
61 sig |
62 val dest_spec : term -> References_Def.T |
62 val dest_spec : term -> References_Def.T |
63 val get_first_argument : term -> term option (*TODO rename get_first_argument*) |
63 val get_first_argument : term -> term option (*TODO rename get_first_argument*) |
64 val eval_leaf: Env.T -> term option -> term -> term -> Program.leaf * term option |
64 val eval_leaf: Env.T -> term option -> term -> term -> Program.leaf * term option |
65 val is: term -> bool |
65 val is: term -> bool |
66 end |
66 |
|
67 val Substitute_adapt_to_type: theory -> term -> Subst.as_string_eqs |
|
68 (**)val Rewrite_Inst_adapt_to_type: theory -> term -> TermC.as_string list(**) |
|
69 (**)val Take_adapt_to_type: Proof.context -> TermC.as_string -> term(**) |
|
70 end |
67 \<close> ML \<open> |
71 \<close> ML \<open> |
68 (**) |
72 (**) |
69 structure Prog_Tac(**): PROGAM_TACTIC(**) = |
73 structure Prog_Tac(**): PROGAM_TACTIC(**) = |
70 struct |
74 struct |
71 (**) |
75 (**) |
206 |
210 |
207 val all_Consts = [Calculate, Rewrite, Rewrite_Inst, Rewrite_Set, Rewrite_Set_Inst, Or_to_List, |
211 val all_Consts = [Calculate, Rewrite, Rewrite_Inst, Rewrite_Set, Rewrite_Set_Inst, Or_to_List, |
208 SubProblem, Substitute, Take, Check_elementwise, Assumptions] |
212 SubProblem, Substitute, Take, Check_elementwise, Assumptions] |
209 |
213 |
210 fun is t = TermC.contains_Const_typeless all_Consts t |
214 fun is t = TermC.contains_Const_typeless all_Consts t |
211 (**)end(**) |
215 |
|
216 |
|
217 (** adapt_to_type arguments of specific tactics **) |
|
218 (* |
|
219 Programs are stored as terms typed by the theory they are defined in. |
|
220 Specific Prog_Tac take substitutions as arguments; these substitutions have |
|
221 the variables to be substituted typed with the program; |
|
222 these variables need to be adapt_to_type from the user-context in order to conform |
|
223 with the terms input by the user. |
|
224 *) |
|
225 fun Substitute_adapt_to_type thy isasub = |
|
226 isasub |
|
227 |> Model_Pattern.adapt_term_to_type (Proof_Context.init_global thy) |
|
228 |> TermC.isalist2list |
|
229 |> Subst.eqs_to_input; |
|
230 |
|
231 fun Rewrite_Inst_adapt_to_type thy sub = |
|
232 sub |
|
233 (*|> Model_Pattern.adapt_term_to_type (Proof_Context.init_global thy)*) |
|
234 |> Subst.program_to_input |
|
235 |
|
236 (*eliminated ERROR: c_2 = (0 :: 'a)*) |
|
237 fun Take_adapt_to_type ctxt arg = arg |
|
238 |> TermC.parse ctxt |
|
239 |> Model_Pattern.adapt_term_to_type ctxt |
|
240 |
|
241 (**)end(*struct*) |
212 \<close> ML \<open> |
242 \<close> ML \<open> |
213 \<close> |
243 \<close> |
|
244 |
214 subsection \<open>TODO\<close> |
245 subsection \<open>TODO\<close> |
215 ML \<open> |
246 ML \<open> |
216 \<close> ML \<open> |
247 \<close> ML \<open> |
217 \<close> ML \<open> |
248 \<close> ML \<open> |
218 \<close> |
249 \<close> |