194 (Program.Expr (subst_atomic (case a of SOME a => Env.update E (a,v) | NONE => E) t), a); |
194 (Program.Expr (subst_atomic (case a of SOME a => Env.update E (a,v) | NONE => E) t), a); |
195 |
195 |
196 |
196 |
197 (* check if a term is a Prog_Tac *) |
197 (* check if a term is a Prog_Tac *) |
198 |
198 |
199 val Calculate = TermC.parse @{context} "Calculate"; |
199 val SOME Calculate = ParseC.term_opt @{context} "Calculate"; |
200 val Rewrite = TermC.parse @{context} "Rewrite"; |
200 val SOME Rewrite = ParseC.term_opt @{context} "Rewrite"; |
201 val Rewrite_Inst = TermC.parse @{context} "Rewrite'_Inst"; |
201 val SOME Rewrite_Inst = ParseC.term_opt @{context} "Rewrite'_Inst"; |
202 val Rewrite_Set = TermC.parse @{context} "Rewrite'_Set"; |
202 val SOME Rewrite_Set = ParseC.term_opt @{context} "Rewrite'_Set"; |
203 val Rewrite_Set_Inst = TermC.parse @{context} "Rewrite'_Set'_Inst"; |
203 val SOME Rewrite_Set_Inst = ParseC.term_opt @{context} "Rewrite'_Set'_Inst"; |
204 val Or_to_List = TermC.parse @{context} "Or'_to'_List"; |
204 val SOME Or_to_List = ParseC.term_opt @{context} "Or'_to'_List"; |
205 val SubProblem = TermC.parse @{context} "SubProblem"; |
205 val SOME SubProblem = ParseC.term_opt @{context} "SubProblem"; |
206 val Substitute = TermC.parse @{context} "Substitute"; |
206 val SOME Substitute = ParseC.term_opt @{context} "Substitute"; |
207 val Take = TermC.parse @{context} "Take"; |
207 val SOME Take = ParseC.term_opt @{context} "Take"; |
208 val Check_elementwise = TermC.parse @{context} "Check'_elementwise"; |
208 val SOME Check_elementwise = ParseC.term_opt @{context} "Check'_elementwise"; |
209 val Assumptions = TermC.parse @{context} "Assumptions"; |
209 val SOME Assumptions = ParseC.term_opt @{context} "Assumptions"; |
210 |
210 |
211 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, |
212 SubProblem, Substitute, Take, Check_elementwise, Assumptions] |
212 SubProblem, Substitute, Take, Check_elementwise, Assumptions] |
213 |
213 |
214 fun is t = TermC.contains_Const_typeless all_Consts t |
214 fun is t = TermC.contains_Const_typeless all_Consts t |
222 i.e. formal arguments require \<open>adapt_to_type\<close> for \<open>Calc.T\<close>. |
222 i.e. formal arguments require \<open>adapt_to_type\<close> for \<open>Calc.T\<close>. |
223 |
223 |
224 Remarkably this appears not necessary for \<open>Rewrite_Inst\<close> and \<open>Rewrite_Set_Inst\<close>; |
224 Remarkably this appears not necessary for \<open>Rewrite_Inst\<close> and \<open>Rewrite_Set_Inst\<close>; |
225 for these, hoewever, \<open>adapt_to_type\<close> is required for conversion from \<open>Tac.subst_input\<close>. |
225 for these, hoewever, \<open>adapt_to_type\<close> is required for conversion from \<open>Tac.subst_input\<close>. |
226 *) |
226 *) |
227 (* TermC.parse ctxt fails with "c_2 = 0" \<longrightarrow> \<open>c_2 = (0 :: 'a)\<close> and thus requires adapt_to_type *) |
227 (* ParseC.term_opt ctxt fails with "c_2 = 0" \<longrightarrow> \<open>c_2 = (0 :: 'a)\<close> and thus requires adapt_to_type *) |
228 fun Take_adapt_to_type ctxt arg = arg |
228 fun Take_adapt_to_type ctxt arg = arg |
229 |> TermC.parse ctxt |
229 |> ParseC.term_opt ctxt |
|
230 |> the |
230 |> ParseC.adapt_term_to_type ctxt |
231 |> ParseC.adapt_term_to_type ctxt |
231 |
232 |
232 fun Substitute_adapt_to_type thy isasub = |
233 fun Substitute_adapt_to_type thy isasub = |
233 isasub |
234 isasub |
234 |> ParseC.adapt_term_to_type (Proof_Context.init_global thy) |
235 |> ParseC.adapt_term_to_type (Proof_Context.init_global thy) |
235 |> TermC.isalist2list |
236 |> TermC.isalist2list |
236 |> Subst.eqs_to_input; |
237 |> Subst.eqs_to_input; |
237 |
238 |
238 (* TermC.parse ctxt fails with "c_2 = 0" \<longrightarrow> \<open>c_2 = (0 :: 'a)\<close> and thus requires adapt_to_type *) |
239 (* TermC.parse ctxt fails with "c_2 = 0" \<longrightarrow> \<open>c_2 = (0 :: 'a)\<close> and thus requires adapt_to_type *) |
239 fun Substitute_adapt_to_type' ctxt strs = strs |
240 fun Substitute_adapt_to_type' ctxt strs = strs |
240 |> map (TermC.parse ctxt) |
241 |> map (ParseC.term_opt ctxt) |
|
242 |> map the |
241 |> map (ParseC.adapt_term_to_type ctxt) |
243 |> map (ParseC.adapt_term_to_type ctxt) |
242 |
244 |
243 (**)end(*struct*) |
245 (**)end(*struct*) |
244 \<close> ML \<open> |
246 \<close> ML \<open> |
245 \<close> |
247 \<close> |