145 case Rewrite.rewrite_ ctxt (assoc_rew_ord thy ro) rls' false (snd thm) f of |
145 case Rewrite.rewrite_ ctxt (assoc_rew_ord thy ro) rls' false (snd thm) f of |
146 SOME (f',asm) => Applicable.Yes (Tactic.Rewrite' (thy', ro, rls', false, thm, f, (f', asm))) |
146 SOME (f',asm) => Applicable.Yes (Tactic.Rewrite' (thy', ro, rls', false, thm, f, (f', asm))) |
147 | NONE => Applicable.No ((thm |> fst |> quote) ^ " not applicable") |
147 | NONE => Applicable.No ((thm |> fst |> quote) ^ " not applicable") |
148 else Applicable.No msg |
148 else Applicable.No msg |
149 end |
149 end |
150 | check (Tactic.Rewrite_Inst (subs, thm)) (cs as (pt, (p, _))) = |
150 | check (Tactic.Rewrite_Inst (subs, thm)) (cs as (pt, pos as (p, _))) = |
151 let |
151 let |
152 val pp = Ctree.par_pblobj pt p; |
152 val pp = Ctree.par_pblobj pt p; |
|
153 (*ctxt*) |
153 val thy' = Ctree.get_obj Ctree.g_domID pt pp; |
154 val thy' = Ctree.get_obj Ctree.g_domID pt pp; |
154 val thy = ThyC.get_theory thy'; |
155 val thy = ThyC.get_theory thy'; |
155 val ctxt = Proof_Context.init_global thy; |
156 val ctxt = Proof_Context.init_global thy; |
|
157 (*ctxt* ) |
|
158 val ctxt = Ctree.get_loc pt pos |> snd |
|
159 val thy = Proof_Context.theory_of ctxt |
|
160 val thy' = Context.theory_name thy |
|
161 ( *ctxt*) |
156 val {rew_ord' = ro', erls = erls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt pp); |
162 val {rew_ord' = ro', erls = erls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt pp); |
157 val f = Calc.current_formula cs; |
163 val f = Calc.current_formula cs; |
158 val subst = Subst.T_from_input ctxt subs; (*TODO: input requires parse _: _ -> _ option*) |
164 val subst = Subst.T_from_input ctxt subs; (*TODO: input requires parse _: _ -> _ option*) |
159 in |
165 in |
160 case Rewrite.rewrite_inst_ ctxt (assoc_rew_ord thy ro') erls false subst (snd thm) f of |
166 case Rewrite.rewrite_inst_ ctxt (assoc_rew_ord thy ro') erls false subst (snd thm) f of |
161 SOME (f', asm) => |
167 SOME (f', asm) => |
162 Applicable.Yes (Tactic.Rewrite_Inst' (thy', ro', erls, false, subst, thm, f, (f', asm))) |
168 Applicable.Yes (Tactic.Rewrite_Inst' (thy', ro', erls, false, subst, thm, f, (f', asm))) |
163 | NONE => Applicable.No (fst thm ^ " not applicable") |
169 | NONE => Applicable.No (fst thm ^ " not applicable") |
164 end |
170 end |
165 | check (Tactic.Rewrite_Set rls) (cs as (pt, (p, _))) = |
171 | check (Tactic.Rewrite_Set rls) (cs as (pt, pos as (p, _))) = |
166 let |
172 let |
|
173 (*ctxt*) |
167 val pp = Ctree.par_pblobj pt p; |
174 val pp = Ctree.par_pblobj pt p; |
168 val thy' = Ctree.get_obj Ctree.g_domID pt pp; |
175 val thy' = Ctree.get_obj Ctree.g_domID pt pp; |
|
176 (*ctxt* ) |
|
177 val ctxt = Ctree.get_loc pt pos |> snd |
|
178 val thy = Proof_Context.theory_of ctxt |
|
179 val thy' = Context.theory_name thy |
|
180 ( *ctxt*) |
169 val f = Calc.current_formula cs; |
181 val f = Calc.current_formula cs; |
170 in |
182 in |
171 case Rewrite.rewrite_set_ (ThyC.id_to_ctxt thy') false (assoc_rls rls) f of |
183 case Rewrite.rewrite_set_ (ThyC.id_to_ctxt thy') false (assoc_rls rls) f of |
172 SOME (f', asm) |
184 SOME (f', asm) |
173 => Applicable.Yes (Tactic.Rewrite_Set' (thy', false, assoc_rls rls, f, (f', asm))) |
185 => Applicable.Yes (Tactic.Rewrite_Set' (thy', false, assoc_rls rls, f, (f', asm))) |
174 | NONE => Applicable.No (rls ^ " not applicable") |
186 | NONE => Applicable.No (rls ^ " not applicable") |
175 end |
187 end |
176 | check (Tactic.Rewrite_Set_Inst (subs, rls)) (cs as (pt, (p, _))) = |
188 | check (Tactic.Rewrite_Set_Inst (subs, rls)) (cs as (pt, pos as (p, _))) = |
177 let |
189 let |
|
190 (*ctxt*) |
178 val pp = Ctree.par_pblobj pt p; |
191 val pp = Ctree.par_pblobj pt p; |
179 val thy' = Ctree.get_obj Ctree.g_domID pt pp; |
192 val thy' = Ctree.get_obj Ctree.g_domID pt pp; |
180 val thy = ThyC.get_theory thy'; |
193 val thy = ThyC.get_theory thy'; |
181 val ctxt = Proof_Context.init_global thy; |
194 val ctxt = Proof_Context.init_global thy; |
|
195 (*ctxt* ) |
|
196 val ctxt = Ctree.get_loc pt pos |> snd |
|
197 val thy = Proof_Context.theory_of ctxt |
|
198 val thy' = Context.theory_name thy |
|
199 ( *ctxt*) |
182 val f = Calc.current_formula cs; |
200 val f = Calc.current_formula cs; |
183 val subst = Subst.T_from_input ctxt subs; (*TODO: input requires parse _: _ -> _ option*) |
201 val subst = Subst.T_from_input ctxt subs; (*TODO: input requires parse _: _ -> _ option*) |
184 in |
202 in |
185 case Rewrite.rewrite_set_inst_ ctxt false subst (assoc_rls rls) f of |
203 case Rewrite.rewrite_set_inst_ ctxt false subst (assoc_rls rls) f of |
186 SOME (f', asm) |
204 SOME (f', asm) |
188 | NONE => Applicable.No (rls ^ " not applicable") |
206 | NONE => Applicable.No (rls ^ " not applicable") |
189 end |
207 end |
190 | check (Tactic.Subproblem (domID, pblID)) (_, _) = |
208 | check (Tactic.Subproblem (domID, pblID)) (_, _) = |
191 Applicable.Yes (Tactic.Subproblem' ((domID, pblID, MethodC.id_empty), [], |
209 Applicable.Yes (Tactic.Subproblem' ((domID, pblID, MethodC.id_empty), [], |
192 TermC.empty, [], ContextC.empty, Auto_Prog.subpbl domID pblID)) |
210 TermC.empty, [], ContextC.empty, Auto_Prog.subpbl domID pblID)) |
193 | check (Tactic.Substitute sube) (cs as (pt, (p, _))) = |
211 | check (Tactic.Substitute sube) (cs as (pt, pos as (p, _))) = |
194 let |
212 let |
195 val pp = Ctree.par_pblobj pt p |
213 val pp = Ctree.par_pblobj pt p |
|
214 (*ctxt*) |
196 val thy = ThyC.get_theory (Ctree.get_obj Ctree.g_domID pt pp) |
215 val thy = ThyC.get_theory (Ctree.get_obj Ctree.g_domID pt pp) |
197 val ctxt = Proof_Context.init_global thy; |
216 val ctxt = Proof_Context.init_global thy; |
|
217 (*ctxt* ) |
|
218 val ctxt = Ctree.get_loc pt pos |> snd |
|
219 val thy = Proof_Context.theory_of ctxt |
|
220 val thy' = Context.theory_name thy |
|
221 ( *ctxt*) |
198 val f = Calc.current_formula cs; |
222 val f = Calc.current_formula cs; |
199 val {rew_ord', erls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt pp) |
223 val {rew_ord', erls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt pp) |
200 val subte = Subst.input_to_terms sube (*TODO: input requires parse _: _ -> _ option*) |
224 val subte = Subst.input_to_terms sube (*TODO: input requires parse _: _ -> _ option*) |
201 val subst = Subst.T_from_string_eqs thy sube |
225 val subst = Subst.T_from_string_eqs thy sube |
202 val ro = assoc_rew_ord thy rew_ord' |
226 val ro = assoc_rew_ord thy rew_ord' |
213 SOME (f', _) => Applicable.Yes (Tactic.Substitute' (ro, erls, subte, f, f')) |
237 SOME (f', _) => Applicable.Yes (Tactic.Substitute' (ro, erls, subte, f, f')) |
214 | NONE => Applicable.No (Subst.string_eqs_to_string sube ^ " not applicable") |
238 | NONE => Applicable.No (Subst.string_eqs_to_string sube ^ " not applicable") |
215 end |
239 end |
216 | check (Tactic.Tac id) (cs as (pt, (p, _))) = |
240 | check (Tactic.Tac id) (cs as (pt, (p, _))) = |
217 let |
241 let |
|
242 (*ctxt*) |
218 val pp = Ctree.par_pblobj pt p; |
243 val pp = Ctree.par_pblobj pt p; |
219 val thy' = Ctree.get_obj Ctree.g_domID pt pp; |
244 val thy' = Ctree.get_obj Ctree.g_domID pt pp; |
220 val thy = ThyC.get_theory thy'; |
245 val thy = ThyC.get_theory thy'; |
|
246 (*ctxt* ) |
|
247 val ctxt = Ctree.get_loc pt pos |> snd |
|
248 val thy = Proof_Context.theory_of ctxt |
|
249 val thy' = Context.theory_name thy |
|
250 ( *ctxt*) |
221 val f = Calc.current_formula cs; |
251 val f = Calc.current_formula cs; |
222 in |
252 in |
223 Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, UnparseC.term f)) |
253 Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, UnparseC.term f)) |
224 end |
254 end |
225 | check (Tactic.Take str) _ = Applicable.Yes (Tactic.Take' (TermC.str2term str)) (* always applicable ?*) |
255 | check (Tactic.Take str) _ = Applicable.Yes (Tactic.Take' (TermC.str2term str)) (* always applicable ?*) |