1 (* Title: Specify/solve-step.sml
3 (c) due to copyright terms
5 Code for the solve-phase in analogy to structure Specify_Step for the specify-phase.
10 val check: Tactic.input -> Calc.T -> Applicable.T
11 val add: Tactic.T -> Istate_Def.T * Proof.context -> Calc.T -> Test_Out.T
13 val add_general: Tactic.T -> Istate_Def.T * Proof.context -> Calc.T -> Test_Out.T
14 val s_add_general: State_Steps.T ->
15 Ctree.ctree * Pos.pos' list * Pos.pos' -> Ctree.ctree * Pos.pos' list * Pos.pos'
17 theory -> Tactic.T -> Pos.pos' -> Ctree.ctree -> Test_Out.T
19 val get_ruleset: 'a -> Pos.pos -> Ctree.ctree ->
20 string * ThyC.id * Rule_Def.rew_ord' * Rule_Def.rule_set * bool
21 val get_eval: string -> Pos.pos ->Ctree.ctree ->
22 string * ThyC.id * (string * Rule_Def.eval_fn)
24 val rew_info: Rule_Def.rule_set -> string * Rule_Def.rule_set * Rule_Def.calc list
29 structure Solve_Step(**): SOLVE_STEP(**) =
33 (** get data from Calc.T **)
35 (* the source is the parent node, either a problem or a Rule_Set (with inter_steps) *)
36 fun rew_info (Rule_Def.Repeat {erls, rew_ord = (rew_ord', _), calc = ca, ...}) =
38 | rew_info (Rule_Set.Sequence {erls, rew_ord = (rew_ord', _), calc = ca, ...}) =
40 | rew_info (Rule_Set.Rrls {erls, rew_ord = (rew_ord', _), calc = ca, ...}) =
42 | rew_info rls = raise ERROR ("rew_info called with '" ^ Rule_Set.id rls ^ "'");
44 fun get_ruleset _ p pt =
46 val (pbl, p', rls') = Ctree.parent_node pt p
51 val thy' = Ctree.get_obj Ctree.g_domID pt p'
52 val {rew_ord', erls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt p')
53 in ("OK", thy', rew_ord', erls, false) end
56 val thy' = Ctree.get_obj Ctree.g_domID pt (Ctree.par_pblobj pt p)
57 val (rew_ord', erls, _) = rew_info rls'
58 in ("OK", thy', rew_ord', erls, false) end
61 fun get_eval scrop p pt =
63 val (pbl, p', rls') = Ctree.parent_node pt p
68 val thy' = Ctree.get_obj Ctree.g_domID pt p'
69 val {calc = scr_isa_fns, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt p')
70 val opt = assoc (scr_isa_fns, scrop)
73 SOME isa_fn => ("OK", thy', isa_fn)
74 | NONE => ("applicable_in Calculate: unknown '" ^ scrop ^ "'", "", ("", Eval_Def.e_evalfn))
78 val thy' = Ctree.get_obj Ctree.g_domID pt (Ctree.par_pblobj pt p);
79 val (_, _,(*_,*)scr_isa_fns) = rew_info rls'(*rls*)
81 case assoc (scr_isa_fns, scrop) of
82 SOME isa_fn => ("OK",thy',isa_fn)
83 | NONE => ("applicable_in Calculate: unknown '" ^ scrop ^ "'", "", ("", Eval_Def.e_evalfn))
87 (** Solve_Step.check **)
90 check tactics (input by the user, mostly) for applicability
91 and determine as much of the result of the tactic as possible initially.
93 fun check (Tactic.Apply_Method mI) (pt, (p, _)) =
95 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)
97 | _ => raise ERROR "Specify_Step.check Apply_Method: uncovered case Ctree.get_obj"
98 val {where_, ...} = Problem.from_store pI
99 val pres = map (I_Model.environment probl |> subst_atomic) where_
100 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
104 Applicable.Yes (Tactic.Apply_Method' (mI, NONE, Istate_Def.empty (*filled later*), ctxt))
106 | check (Tactic.Calculate op_) (cs as (pt, (p, _))) =
108 val (msg, thy', isa_fn) = get_eval op_ p pt;
109 val f = Calc.current_formula cs;
113 case Rewrite.calculate_ (ThyC.id_to_ctxt thy') isa_fn f of
115 => Applicable.Yes (Tactic.Calculate' (thy', op_, f, (f', (id, thm))))
116 | NONE => Applicable.No ("'calculate " ^ op_ ^ "' not applicable")
117 else Applicable.No msg
119 | check (Tactic.Check_Postcond pI) (_, _) = (*TODO: only applicable, if evaluating to True*)
120 Applicable.Yes (Tactic.Check_Postcond' (pI, TermC.empty))
121 | check (Tactic.Check_elementwise pred) cs =
123 val f = Calc.current_formula cs;
125 Applicable.Yes (Tactic.Check_elementwise' (f, pred, (f, [])))
127 | check Tactic.Empty_Tac _ = Applicable.No "Empty_Tac is not applicable"
128 | check (Tactic.Free_Solve) _ = Applicable.Yes (Tactic.Free_Solve')
129 | check Tactic.Or_to_List cs =
131 val f = Calc.current_formula cs;
132 val ls = Prog_Expr.or2list f;
134 Applicable.Yes (Tactic.Or_to_List' (f, ls))
136 | check (Tactic.Rewrite thm) (cs as (pt, (p, _))) =
138 val (msg, thy', ro, rls', _) = get_ruleset thm p pt;
139 val thy = ThyC.id_to_ctxt thy';
140 val f = Calc.current_formula cs;
144 case Rewrite.rewrite_ thy (Rewrite_Ord.assoc_rew_ord ro) rls' false (snd thm) f of
145 SOME (f',asm) => Applicable.Yes (Tactic.Rewrite' (thy', ro, rls', false, thm, f, (f', asm)))
146 | NONE => Applicable.No ((thm |> fst |> quote) ^ " not applicable")
147 else Applicable.No msg
149 | check (Tactic.Rewrite_Inst (subs, thm)) (cs as (pt, (p, _))) =
151 val pp = Ctree.par_pblobj pt p;
152 val thy' = Ctree.get_obj Ctree.g_domID pt pp;
153 val thy = ThyC.get_theory thy';
154 val ctxt = Proof_Context.init_global thy;
155 val {rew_ord' = ro', erls = erls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt pp);
156 val f = Calc.current_formula cs;
157 val subst = Subst.T_from_input ctxt subs; (*TODO: input requires parse _: _ -> _ option*)
159 case Rewrite.rewrite_inst_ ctxt (Rewrite_Ord.assoc_rew_ord ro') erls false subst (snd thm) f of
161 Applicable.Yes (Tactic.Rewrite_Inst' (thy', ro', erls, false, subst, thm, f, (f', asm)))
162 | NONE => Applicable.No (fst thm ^ " not applicable")
164 | check (Tactic.Rewrite_Set rls) (cs as (pt, (p, _))) =
166 val pp = Ctree.par_pblobj pt p;
167 val thy' = Ctree.get_obj Ctree.g_domID pt pp;
168 val f = Calc.current_formula cs;
170 case Rewrite.rewrite_set_ (ThyC.id_to_ctxt thy') false (assoc_rls rls) f of
172 => Applicable.Yes (Tactic.Rewrite_Set' (thy', false, assoc_rls rls, f, (f', asm)))
173 | NONE => Applicable.No (rls ^ " not applicable")
175 | check (Tactic.Rewrite_Set_Inst (subs, rls)) (cs as (pt, (p, _))) =
177 val pp = Ctree.par_pblobj pt p;
178 val thy' = Ctree.get_obj Ctree.g_domID pt pp;
179 val thy = ThyC.get_theory thy';
180 val ctxt = Proof_Context.init_global thy;
181 val f = Calc.current_formula cs;
182 val subst = Subst.T_from_input ctxt subs; (*TODO: input requires parse _: _ -> _ option*)
184 case Rewrite.rewrite_set_inst_ ctxt false subst (assoc_rls rls) f of
186 => Applicable.Yes (Tactic.Rewrite_Set_Inst' (thy', false, subst, assoc_rls rls, f, (f', asm)))
187 | NONE => Applicable.No (rls ^ " not applicable")
189 | check (Tactic.Subproblem (domID, pblID)) (_, _) =
190 Applicable.Yes (Tactic.Subproblem' ((domID, pblID, MethodC.id_empty), [],
191 TermC.empty, [], ContextC.empty, Auto_Prog.subpbl domID pblID))
192 | check (Tactic.Substitute sube) (cs as (pt, (p, _))) =
194 val pp = Ctree.par_pblobj pt p
195 val thy = ThyC.get_theory (Ctree.get_obj Ctree.g_domID pt pp)
196 val ctxt = Proof_Context.init_global thy;
197 val f = Calc.current_formula cs;
198 val {rew_ord', erls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt pp)
199 val subte = Subst.input_to_terms sube (*TODO: input requires parse _: _ -> _ option*)
200 val subst = Subst.T_from_string_eqs thy sube
201 val ro = Rewrite_Ord.assoc_rew_ord rew_ord'
203 if foldl and_ (true, map TermC.contains_Var subte)
205 let val f' = subst_atomic subst f
207 then Applicable.No (Subst.string_eqs_to_string sube ^ " not applicable")
208 else Applicable.Yes (Tactic.Substitute' (ro, erls, subte, f, f'))
211 case Rewrite.rewrite_terms_ ctxt ro erls subte f of
212 SOME (f', _) => Applicable.Yes (Tactic.Substitute' (ro, erls, subte, f, f'))
213 | NONE => Applicable.No (Subst.string_eqs_to_string sube ^ " not applicable")
215 | check (Tactic.Tac id) (cs as (pt, (p, _))) =
217 val pp = Ctree.par_pblobj pt p;
218 val thy' = Ctree.get_obj Ctree.g_domID pt pp;
219 val thy = ThyC.get_theory thy';
220 val f = Calc.current_formula cs;
222 Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, UnparseC.term f))
224 | check (Tactic.Take str) _ = Applicable.Yes (Tactic.Take' (TermC.str2term str)) (* always applicable ?*)
225 | check (Tactic.Begin_Trans) cs =
226 Applicable.Yes (Tactic.Begin_Trans' (Calc.current_formula cs))
227 | check (Tactic.End_Trans) (pt, (p, p_)) = (*TODO: check parent branches*)
229 then Applicable.Yes (Tactic.End_Trans' (Ctree.get_obj Ctree.g_result pt p))
230 else Applicable.No "'End_Trans' is not applicable at the beginning of a transitive sequence"
231 | check Tactic.End_Proof' _ = Applicable.Yes Tactic.End_Proof''
232 | check m _ = raise ERROR ("Solve_Step.check called for " ^ Tactic.input_to_string m);
235 (** Solve_Step.add **)
237 fun add (Tactic.Apply_Method' (_, topt, is, _)) (_, ctxt) (pt, pos as (p, _)) =
240 let val (pt, c) = Ctree.cappend_form pt p (is, ctxt) t
241 in (pos, c, Test_Out.EmptyMout, pt) end
242 | NONE => (pos, [], Test_Out.EmptyMout, pt))
243 | add (Tactic.Take' t) l (pt, (p, _)) = (* val (Take' t) = m; *)
246 let val (ps, p') = split_last p (* no connex to prev.ppobj *)
247 in if p' = 0 then ps @ [1] else p end
248 val (pt, c) = Ctree.cappend_form pt p l t
250 ((p, Pos.Frm), c, Test_Out.FormKF (UnparseC.term t), pt)
252 | add (Tactic.Begin_Trans' t) l (pt, (p, Pos.Frm)) =
254 val (pt, c) = Ctree.cappend_form pt p l t
255 val pt = Ctree.update_branch pt p Ctree.TransitiveB (*040312*)
256 (* replace the old PrfOjb ~~~~~ *)
257 val p = (Pos.lev_on o Pos.lev_dn (* starts with [...,0] *)) p
258 val (pt, c') = Ctree.cappend_form pt p l t (*FIXME.0402 same istate ???*)
260 ((p, Pos.Frm), c @ c', Test_Out.FormKF (UnparseC.term t), pt)
262 | add (Tactic.Begin_Trans' t) l (pt, (p, Pos.Res)) =
263 (*append after existing PrfObj vvvvvvvvvvvvv*)
264 add (Tactic.Begin_Trans' t) l (pt, (Pos.lev_on p, Pos.Frm))
265 | add (Tactic.End_Trans' tasm) l (pt, (p, _)) =
267 val p' = Pos.lev_up p
268 val (pt, c) = Ctree.append_result pt p' l tasm Ctree.Complete
270 ((p', Pos.Res), c, Test_Out.FormKF "DUMMY" (*term2str t ..ERROR (t) has not been declared*), pt)
272 | add (Tactic.Rewrite_Inst' (_, _, _, _, subs', thm', f, (f', asm))) (is, ctxt) (pt, (p, _)) =
274 val (pt, c) = Ctree.cappend_atomic pt p (is, ctxt) f
275 (Tactic.Rewrite_Inst (Subst.T_to_input subs', thm')) (f',asm) Ctree.Complete;
276 val pt = Ctree.update_branch pt p Ctree.TransitiveB
278 ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term f'), pt)
280 | add (Tactic.Rewrite' (_, _, _, _, thm', f, (f', asm))) (is, ctxt) (pt, (p, _)) =
282 val (pt, c) = Ctree.cappend_atomic pt p (is, ctxt) f (Tactic.Rewrite thm') (f', asm) Ctree.Complete
283 val pt = Ctree.update_branch pt p Ctree.TransitiveB
285 ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term f'), pt)
287 | add (Tactic.Rewrite_Set_Inst' (_, _, subs', rls', f, (f', asm))) (is, ctxt) (pt, (p, _)) =
289 val (pt, c) = Ctree.cappend_atomic pt p (is, ctxt) f
290 (Tactic.Rewrite_Set_Inst (Subst.T_to_input subs', Rule_Set.id rls')) (f', asm) Ctree.Complete
291 val pt = Ctree.update_branch pt p Ctree.TransitiveB
293 ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term f'), pt)
295 | add (Tactic.Rewrite_Set' (_, _, rls', f, (f', asm))) (is, ctxt) (pt, (p, _)) =
297 val (pt, c) = Ctree.cappend_atomic pt p (is, ctxt) f
298 (Tactic.Rewrite_Set (Rule_Set.id rls')) (f', asm) Ctree.Complete
299 val pt = Ctree.update_branch pt p Ctree.TransitiveB
301 ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term f'), pt)
303 | add (Tactic.Check_Postcond' (_, scval)) l (pt, (p, _)) =
305 val (pt, c) = Ctree.append_result pt p l (scval, []) Ctree.Complete
307 ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term scval), pt)
309 | add (Tactic.Calculate' (_, op_, f, (f', _))) l (pt, (p, _)) =
311 val (pt,c) = Ctree.cappend_atomic pt p l f (Tactic.Calculate op_) (f', []) Ctree.Complete
313 ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term f'), pt)
315 | add (Tactic.Check_elementwise' (consts, pred, (f', asm))) l (pt, (p, _)) =
317 val (pt,c) = Ctree.cappend_atomic pt p l consts (Tactic.Check_elementwise pred) (f', asm) Ctree.Complete
319 ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term f'), pt)
321 | add (Tactic.Or_to_List' (ors, list)) l (pt, (p, _)) =
323 val (pt,c) = Ctree.cappend_atomic pt p l ors Tactic.Or_to_List (list, []) Ctree.Complete
325 ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term list), pt)
327 | add (Tactic.Substitute' (_, _, subte, t, t')) l (pt, (p, _)) =
330 Ctree.cappend_atomic pt p l t (Tactic.Substitute (Subst.eqs_to_input subte)) (t',[]) Ctree.Complete
331 in ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term t'), pt)
333 | add (Tactic.Tac_ (_, f, id, f')) l (pt, (p, _)) =
335 val (pt, c) = Ctree.cappend_atomic pt p l (TermC.str2term f) (Tactic.Tac id) (TermC.str2term f', []) Ctree.Complete
337 ((p,Pos.Res), c, Test_Out.FormKF f', pt)
339 | add (Tactic.Subproblem' ((domID, pblID, metID), oris, hdl, fmz_, ctxt_specify, f))
340 (l as (_, ctxt)) (pt, (p, _)) =
342 val (pt, c) = Ctree.cappend_problem pt p l (fmz_, (domID, pblID, metID))
343 (oris, (domID, pblID, metID), hdl, ctxt_specify)
344 val f = Syntax.string_of_term ctxt f
346 ((p, Pos.Pbl), c, Test_Out.FormKF f, pt)
348 | add m' _ (_, pos) =
349 raise ERROR ("Solve_Step.add: not impl.for " ^ Tactic.string_of m' ^ " at " ^ Pos.pos'2str pos)
351 (* LI switches between solve-phase and specify-phase *)
352 fun add_general tac ic cs =
353 if Tactic.for_specify' tac
354 then Specify_Step.add tac ic cs
357 (* the order of State_Steps is reversed: insert last element first *)
358 fun s_add_general [] ptp = ptp
359 | s_add_general tacis (pt, c, _) =
361 val (tacis', (_, tac_, (p, is))) = split_last tacis
362 val (p', c', _, pt') = add_general tac_ is (pt, p)
364 s_add_general tacis' (pt', c@c', p')
367 (* a still undeveloped concept: do a calculation without LI *)
368 fun add_hard _(*thy*) m' (p, p_) pt =
371 Pos.Frm => p | Pos.Res => Pos.lev_on p
372 | _ => raise ERROR ("generate_hard: call by " ^ Pos.pos'2str (p,p_))
374 add_general m' (Istate_Def.empty, ContextC.empty) (pt, (p, p_))