82 SOME isa_fn => ("OK",thy',isa_fn) |
83 SOME isa_fn => ("OK",thy',isa_fn) |
83 | NONE => ("applicable_in Calculate: unknown '" ^ scrop ^ "'", "", ("", Eval.ml_fun_empty)) |
84 | NONE => ("applicable_in Calculate: unknown '" ^ scrop ^ "'", "", ("", Eval.ml_fun_empty)) |
84 end |
85 end |
85 end; |
86 end; |
86 |
87 |
|
88 (** get context reliably at switch_specify_solve **) |
|
89 |
|
90 fun at_begin_program (is, Pos.Res) = last_elem is = 0 |
|
91 | at_begin_program _ = false; |
|
92 |
|
93 (* strange special case at Apply_Method *) |
|
94 fun get_ctxt_from_PblObj pt (p_, Pos.Res) = |
|
95 let |
|
96 val pp = Ctree.par_pblobj pt p_ (*drops the "0"*) |
|
97 val {ctxt, ...} = Ctree.get_obj I pt pp |> Ctree.rep_specify_data |
|
98 in ctxt end |
|
99 | get_ctxt_from_PblObj _ _ = raise ERROR "get_ctxt_from_PblObj called by PrfObj or EmptyPtree"; |
|
100 |
|
101 fun get_ctxt pt (p_, Pos.Pbl) = |
|
102 let |
|
103 val pp = Ctree.par_pblobj pt p_ (*drops the "0"*) |
|
104 val {ctxt, ...} = Ctree.get_obj I pt pp |> Ctree.rep_specify_data |
|
105 in ctxt end |
|
106 | get_ctxt pt pos = |
|
107 if at_begin_program pos |
|
108 then get_ctxt_from_PblObj pt pos |
|
109 else Ctree.get_ctxt pt pos |
|
110 |
|
111 |
|
112 |
87 (** Solve_Step.check **) |
113 (** Solve_Step.check **) |
88 |
114 |
89 (* |
115 (* |
90 check tactics (input by the user, mostly) for applicability |
116 check tactics (input by the user, mostly) for applicability |
91 and determine as much of the result of the tactic as possible initially. |
117 and determine as much of the result of the tactic as possible initially. |
92 *) |
118 *) |
93 fun check (Tactic.Apply_Method mI) (pt, (p, _)) = |
119 fun check (Tactic.Apply_Method mI) (pt, (p, _)) = |
94 let |
120 let |
95 val (dI, pI, probl, ctxt) = case Ctree.get_obj I pt p of |
121 val (dI, pI, probl, ctxt) = case Ctree.get_obj I pt p of |
96 Ctree.PblObj {origin = (_, (dI, pI, _), _), probl, ctxt, ...} => (dI, pI, probl, ctxt) |
122 Ctree.PblObj {origin = (_, (dI, pI, _), _), probl, ctxt, ...} => (dI, pI, probl, ctxt) |
97 | _ => raise ERROR "Specify_Step.check Apply_Method: uncovered case Ctree.get_obj" |
123 | _ => raise ERROR "Solve_Step.check Apply_Method: uncovered case Ctree.get_obj" |
98 val {where_, ...} = Problem.from_store ctxt pI |
124 val {where_, ...} = Problem.from_store ctxt pI |
99 val pres = map (I_Model.environment probl |> subst_atomic) where_ |
125 val pres = map (I_Model.environment probl |> subst_atomic) where_ |
100 val ctxt = if ContextC.is_empty ctxt (*vvvvvvvvvvvvvv DO THAT EARLIER?!?*) |
126 val ctxt = if ContextC.is_empty ctxt (*vvvvvvvvvvvvvv DO THAT EARLIER?!?*) |
101 then ThyC.get_theory dI |> Proof_Context.init_global |> ContextC.insert_assumptions pres |
127 then ThyC.get_theory dI |> Proof_Context.init_global |> ContextC.insert_assumptions pres |
102 else ctxt |
128 else ctxt |
194 val pp = Ctree.par_pblobj pt p |
220 val pp = Ctree.par_pblobj pt p |
195 val ctxt = Ctree.get_loc pt pos |> snd |
221 val ctxt = Ctree.get_loc pt pos |> snd |
196 val thy = Proof_Context.theory_of ctxt |
222 val thy = Proof_Context.theory_of ctxt |
197 val f = Calc.current_formula cs; |
223 val f = Calc.current_formula cs; |
198 val {rew_ord', erls, ...} = MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt pp) |
224 val {rew_ord', erls, ...} = MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt pp) |
199 val subte = Subst.input_to_terms sube (*?TODO: input requires parse _: _ -> _ option?*) |
225 val subte = Subst.input_to_terms ctxt sube (*?TODO: input requires parse _: _ -> _ option?*) |
200 val ro = get_rew_ord ctxt rew_ord' |
226 val ro = get_rew_ord ctxt rew_ord' |
201 in |
227 in |
202 if foldl and_ (true, map TermC.contains_Var subte) |
228 if foldl and_ (true, map TermC.contains_Var subte) |
203 then (*1*) |
229 then (*1*) |
204 let val f' = subst_atomic (Subst.T_from_string_eqs thy sube) f |
230 let val f' = subst_atomic (Subst.T_from_string_eqs thy sube) f |
216 val thy = (Ctree.get_loc pt pos |> snd) |> Proof_Context.theory_of |
242 val thy = (Ctree.get_loc pt pos |> snd) |> Proof_Context.theory_of |
217 val f = Calc.current_formula cs; |
243 val f = Calc.current_formula cs; |
218 in |
244 in |
219 Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, UnparseC.term f)) |
245 Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, UnparseC.term f)) |
220 end |
246 end |
221 | check (Tactic.Take str) _ = Applicable.Yes (Tactic.Take' (TermC.str2term str)) (* always applicable ?*) |
247 (*/----------------- updated----------------------------------* ) |
|
248 | check (Tactic.Take str) (pt, pos) = |
|
249 Applicable.Yes (Tactic.Take' |
|
250 (TermC.parse ((*Solve_Step.*)get_ctxt pt pos) str)) (*always applicable*) |
|
251 ( *------------------- updated----------------------------------*) |
|
252 | check (Tactic.Take str) (pt, pos) = |
|
253 let |
|
254 val ctxt = (*Solve_Step.*)get_ctxt pt pos |
|
255 val t = Prog_Tac.Take_adapt_to_type ctxt str |
|
256 in Applicable.Yes (Tactic.Take' t) end |
|
257 (*\----------------- updated----------------------------------*) |
222 | check (Tactic.Begin_Trans) cs = |
258 | check (Tactic.Begin_Trans) cs = |
223 Applicable.Yes (Tactic.Begin_Trans' (Calc.current_formula cs)) |
259 Applicable.Yes (Tactic.Begin_Trans' (Calc.current_formula cs)) |
224 | check (Tactic.End_Trans) (pt, (p, p_)) = (*TODO: check parent branches*) |
260 | check (Tactic.End_Trans) (pt, (p, p_)) = (*TODO: check parent branches*) |
225 if p_ = Pos.Res |
261 if p_ = Pos.Res |
226 then Applicable.Yes (Tactic.End_Trans' (Ctree.get_obj Ctree.g_result pt p)) |
262 then Applicable.Yes (Tactic.End_Trans' (Ctree.get_obj Ctree.g_result pt p)) |
325 let |
361 let |
326 val (pt,c) = |
362 val (pt,c) = |
327 Ctree.cappend_atomic pt p l t (Tactic.Substitute (Subst.eqs_to_input subte)) (t',[]) Ctree.Complete |
363 Ctree.cappend_atomic pt p l t (Tactic.Substitute (Subst.eqs_to_input subte)) (t',[]) Ctree.Complete |
328 in ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term t'), pt) |
364 in ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term t'), pt) |
329 end |
365 end |
330 | add (Tactic.Tac_ (_, f, id, f')) l (pt, (p, _)) = |
366 | add (Tactic.Tac_ (_, f, id, f')) l (pt, pos as (p, _)) = |
331 let |
367 let |
332 val (pt, c) = Ctree.cappend_atomic pt p l (TermC.str2term f) (Tactic.Tac id) (TermC.str2term f', []) Ctree.Complete |
368 val ctxt = Ctree.get_ctxt pt pos |
|
369 val (pt, c) = Ctree.cappend_atomic pt p l |
|
370 (TermC.parse ctxt f) (Tactic.Tac id) (TermC.parse ctxt f', []) Ctree.Complete |
333 in |
371 in |
334 ((p,Pos.Res), c, Test_Out.FormKF f', pt) |
372 ((p,Pos.Res), c, Test_Out.FormKF f', pt) |
335 end |
373 end |
336 | add (Tactic.Subproblem' ((domID, pblID, metID), oris, hdl, fmz_, ctxt_specify, f)) |
374 | add (Tactic.Subproblem' ((domID, pblID, metID), oris, hdl, fmz_, ctxt_specify, f)) |
337 (l as (_, ctxt)) (pt, (p, _)) = |
375 (l as (_, ctxt)) (pt, (p, _)) = |