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 * Rewrite_Ord.id * Rule_Def.rule_set * bool
21 val get_eval: string -> Pos.pos' -> Ctree.ctree -> string * ThyC.id * Eval.ml
24 val rew_info: Rule_Def.rule_set -> string * Rule_Def.rule_set * Eval.ml_from_prog 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 {asm_rls, rew_ord = (rew_ord, _), calc = ca, ...}) =
37 (rew_ord, asm_rls, ca)
38 | rew_info (Rule_Set.Sequence {asm_rls, rew_ord = (rew_ord, _), calc = ca, ...}) =
39 (rew_ord, asm_rls, ca)
40 | rew_info (Rule_Set.Rrls {asm_rls, rew_ord = (rew_ord, _), calc = ca, ...}) =
41 (rew_ord, asm_rls, ca)
42 | rew_info rls = raise ERROR ("rew_info called with '" ^ Rule_Set.id rls ^ "'");
44 fun get_ruleset _ (pos as (p, _)) pt =
46 val (pbl, p', rls', ctxt) = LItool.parent_node pt pos
51 val thy' = Ctree.get_obj Ctree.g_domID pt p'
52 val {rew_ord, asm_rls, ...} = MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt p')
53 in ("OK", thy', rew_ord, asm_rls, false) end
56 val thy' = Ctree.get_obj Ctree.g_domID pt (Ctree.par_pblobj pt p)
57 val (rew_ord, asm_rls, _) = rew_info rls'
58 in ("OK", thy', rew_ord, asm_rls, false) end
61 fun get_eval scrop (pos as (p, _)) pt =
63 val (pbl, p', rls', ctxt) = LItool.parent_node pt pos
68 val thy' = Ctree.get_obj Ctree.g_domID pt p'
69 val {calc = scr_isa_fns, ...} = MethodC.from_store ctxt (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.ml_fun_empty))
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.ml_fun_empty))
87 (** get context reliably at switch_specify_solve **)
89 fun at_begin_program (is, Pos.Res) = last_elem is = 0
90 | at_begin_program _ = false;
92 (* strange special case at Apply_Method *)
93 fun get_ctxt_from_PblObj pt (p_, Pos.Res) =
95 val pp = Ctree.par_pblobj pt p_ (*drops the "0"*)
96 val {ctxt, ...} = Ctree.get_obj I pt pp |> Ctree.rep_specify_data
98 | get_ctxt_from_PblObj _ _ = raise ERROR "get_ctxt_from_PblObj called by PrfObj or EmptyPtree";
100 fun get_ctxt pt (p_, Pos.Pbl) =
102 val pp = Ctree.par_pblobj pt p_ (*drops the "0"*)
103 val {ctxt, ...} = Ctree.get_obj I pt pp |> Ctree.rep_specify_data
106 if at_begin_program pos
107 then get_ctxt_from_PblObj pt pos
108 else Ctree.get_ctxt pt pos
112 (** Solve_Step.check **)
115 check tactics (input by the user, mostly) for applicability
116 and determine of the result as much as possible initially of the tactic.
118 fun check (Tactic.Apply_Method mI) (pt, (p, _)) =
120 val (dI, pI, probl, ctxt) = case Ctree.get_obj I pt p of
121 Ctree.PblObj {origin = (_, (dI, pI, _), _), probl, ctxt, ...} => (dI, pI, probl, ctxt)
122 | _ => raise ERROR "Solve_Step.check Apply_Method: uncovered case Ctree.get_obj"
123 val {model, where_rls, where_, ...} = Problem.from_store ctxt pI
124 val checked = Pre_Conds.check ctxt where_rls where_ (model, probl)
125 val true_only = checked
127 |> map (fn (true, prec) => [prec] | (false, _) => [])
129 val ctxt = if ContextC.is_empty ctxt (*only in case of input by user*)
131 |> Know_Store.get_via_last_thy
132 |> Proof_Context.init_global
133 |> ContextC.insert_assumptions true_only
136 Applicable.Yes (Tactic.Apply_Method' (mI, NONE, Istate_Def.empty (*filled later*), ctxt))
138 | check (Tactic.Calculate op_) (cs as (pt, pos)) =
140 val (msg, thy', isa_fn) = get_eval op_ pos pt;
141 val ctxt = Ctree.get_ctxt pt pos
142 val f = Calc.current_formula cs;
146 case Rewrite.calculate_ ctxt isa_fn f of
148 => Applicable.Yes (Tactic.Calculate' (thy', op_, f, (f', (id, thm))))
149 | NONE => Applicable.No ("'calculate " ^ op_ ^ "' not applicable")
150 else Applicable.No msg
152 | check (Tactic.Check_Postcond pI) (_, _) = (*TODO: only applicable, if evaluating to True*)
153 Applicable.Yes (Tactic.Check_Postcond' (pI, TermC.empty))
154 | check (Tactic.Check_elementwise pred) cs =
156 val f = Calc.current_formula cs;
158 Applicable.Yes (Tactic.Check_elementwise' (f, pred, (f, [])))
160 | check Tactic.Empty_Tac _ = Applicable.No "Empty_Tac is not applicable"
161 | check (Tactic.Free_Solve) _ = Applicable.Yes (Tactic.Free_Solve')
162 | check Tactic.Or_to_List cs =
164 val f = Calc.current_formula cs;
165 val ls = Prog_Expr.or2list f;
167 Applicable.Yes (Tactic.Or_to_List' (f, ls))
169 | check (Tactic.Rewrite thm) (cs as (pt, pos)) =
171 val (msg, _, ro, rls', _) = get_ruleset thm pos pt;
172 val ctxt = Ctree.get_ctxt pt pos
173 val thy = ctxt |> Proof_Context.theory_of
174 val f = Calc.current_formula cs;
178 case Rewrite.rewrite_ ctxt (get_rew_ord ctxt ro) rls' false (snd thm) f of
180 Applicable.Yes (Tactic.Rewrite' (ThyC.id_of thy, ro, rls', false, thm, f, (f', asm)))
181 | NONE => Applicable.No ((thm |> fst |> quote) ^ " not applicable")
182 else Applicable.No msg
184 | check (Tactic.Rewrite_Inst (subs, thm)) (cs as (pt, pos as (p, _))) =
186 val pp = Ctree.par_pblobj pt p;
187 val ctxt = Ctree.get_loc pt pos |> snd
188 val thy = Proof_Context.theory_of ctxt
189 val {rew_ord = ro', asm_rls = asm_rls, ...} = MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt pp);
190 val f = Calc.current_formula cs;
191 val subst = Tactic.subst_adapt_to_type ctxt subs;
193 case Rewrite.rewrite_inst_ ctxt (get_rew_ord ctxt ro') asm_rls false subst (snd thm) f of
195 Applicable.Yes (Tactic.Rewrite_Inst'
196 (Context.theory_name thy, ro', asm_rls, false, subst, thm, f, (f', asm)))
197 | NONE => Applicable.No (fst thm ^ " not applicable")
199 | check (Tactic.Rewrite_Set rls) (cs as (pt, pos)) =
201 val ctxt = Ctree.get_loc pt pos |> snd
202 val thy' = ctxt |> Proof_Context.theory_of |> Context.theory_name
203 val f = Calc.current_formula cs;
205 case Rewrite.rewrite_set_ ctxt false (get_rls ctxt rls) f of
207 => Applicable.Yes (Tactic.Rewrite_Set' (thy', false, get_rls ctxt rls, f, (f', asm)))
208 | NONE => Applicable.No (rls ^ " not applicable")
210 | check (Tactic.Rewrite_Set_Inst (subs, rls)) (cs as (pt, pos)) =
212 val ctxt = Ctree.get_loc pt pos |> snd
213 val thy' = ctxt |> Proof_Context.theory_of |> Context.theory_name
214 val f = Calc.current_formula cs;
215 val subst = Tactic.subst_adapt_to_type ctxt subs;
217 case Rewrite.rewrite_set_inst_ ctxt false subst (get_rls ctxt rls) f of
220 (Tactic.Rewrite_Set_Inst' (thy', false, subst, get_rls ctxt rls, f, (f', asm)))
221 | NONE => Applicable.No (rls ^ " not applicable")
223 | check (Tactic.Subproblem (domID, pblID)) (_, _) =
224 Applicable.Yes (Tactic.Subproblem' ((domID, pblID, MethodC.id_empty), [],
225 TermC.empty, [], ContextC.empty, Auto_Prog.subpbl domID pblID))
226 | check (Tactic.Substitute sube) (cs as (pt, pos as (p, _))) =
228 val pp = Ctree.par_pblobj pt p
229 val ctxt = Ctree.get_loc pt pos |> snd
230 val f = Calc.current_formula cs;
231 val {rew_ord, asm_rls, ...} = MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt pp)
232 val subte = Prog_Tac.Substitute_adapt_to_type' ctxt sube
233 val ro = get_rew_ord ctxt rew_ord
235 if foldl and_ (true, map TermC.contains_Var subte)
237 let val f' = subst_atomic (Subst.T_from_string_eqs ctxt sube) f
239 then Applicable.No (Subst.string_eqs_to_string sube ^ " not applicable")
240 else Applicable.Yes (Tactic.Substitute' (ro, asm_rls, subte, f, f'))
243 case Rewrite.rewrite_terms_ ctxt ro asm_rls subte f of
244 SOME (f', _) => Applicable.Yes (Tactic.Substitute' (ro, asm_rls, subte, f, f'))
245 | NONE => Applicable.No (Subst.string_eqs_to_string sube ^ " not applicable")
247 | check (Tactic.Tac id) (cs as (pt, pos)) =
249 val ctxt = Ctree.get_ctxt pt pos
250 val thy = ctxt |> Proof_Context.theory_of
251 val f = Calc.current_formula cs;
252 val f' = UnparseC.term ctxt f
254 Applicable.Yes (Tactic.Tac_ (thy, f', id, f'))
256 | check (Tactic.Take str) (pt, pos) =
258 val ctxt = (*Solve_Step.*)get_ctxt pt pos
259 val t = Prog_Tac.Take_adapt_to_type ctxt str
260 in Applicable.Yes (Tactic.Take' t) end
261 | check (Tactic.Begin_Trans) cs =
262 Applicable.Yes (Tactic.Begin_Trans' (Calc.current_formula cs))
263 | check (Tactic.End_Trans) (pt, (p, p_)) = (*TODO: check parent branches*)
265 then Applicable.Yes (Tactic.End_Trans' (Ctree.get_obj Ctree.g_result pt p))
266 else Applicable.No "Tactic.End_Trans not applicable at the beginning of a transitive sequence"
267 | check Tactic.End_Proof' _ =
268 Applicable.Yes Tactic.End_Proof'' (*TODO! check Post_Cond first !*)
269 | check m (pt, pos) =
271 val ctxt = (*Solve_Step.*)get_ctxt pt pos
273 raise ERROR ("Solve_Step.check called for " ^ Tactic.input_to_string ctxt m)
277 (** Solve_Step.add **)
279 fun add (Tactic.Apply_Method' (_, topt, is, _)) (_, ctxt) (pt, pos as (p, _)) =
282 let val (pt, c) = Ctree.cappend_form pt p (is, ctxt) t
283 in (pos, c, Test_Out.EmptyMout, pt) end
284 | NONE => (pos, [], Test_Out.EmptyMout, pt))
285 | add (Tactic.Take' t) (l as (_, ctxt)) (pt, (p, _)) = (* val (Take' t) = m; *)
288 let val (ps, p') = split_last p (* no connex to prev.ppobj *)
289 in if p' = 0 then ps @ [1] else p end
290 val (pt, c) = Ctree.cappend_form pt p l t
292 ((p, Pos.Frm), c, Test_Out.FormKF (UnparseC.term ctxt t), pt)
294 | add (Tactic.Begin_Trans' t) (l as (_, ctxt)) (pt, (p, Pos.Frm)) =
296 val (pt, c) = Ctree.cappend_form pt p l t
297 val pt = Ctree.update_branch pt p Ctree.TransitiveB (*040312*)
298 (* replace the old PrfOjb ~~~~~ *)
299 val p = (Pos.lev_on o Pos.lev_dn (* starts with [...,0] *)) p
300 val (pt, c') = Ctree.cappend_form pt p l t (*FIXME.0402 same istate ???*)
302 ((p, Pos.Frm), c @ c', Test_Out.FormKF (UnparseC.term ctxt t), pt)
304 | add (Tactic.Begin_Trans' t) l (pt, (p, Pos.Res)) =
305 (*append after existing PrfObj vvvvvvvvvvvvv*)
306 add (Tactic.Begin_Trans' t) l (pt, (Pos.lev_on p, Pos.Frm))
307 | add (Tactic.End_Trans' tasm) (l as (_, _(*ctxt*))) (pt, (p, _)) =
309 val p' = Pos.lev_up p
310 val (pt, c) = Ctree.append_result pt p' l tasm Ctree.Complete
312 ((p', Pos.Res), c, Test_Out.FormKF "DUMMY" (*UnparseC.term ctxt t*), pt)
314 | add (Tactic.Rewrite_Inst' (_, _, _, _, subs', thm', f, (f', asm))) (is, ctxt) (pt, (p, _)) =
316 val (pt, c) = Ctree.cappend_atomic pt p (is, ctxt) f
317 (Tactic.Rewrite_Inst (Subst.T_to_input ctxt subs', thm')) (f',asm) Ctree.Complete;
318 val pt = Ctree.update_branch pt p Ctree.TransitiveB
320 ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term ctxt f'), pt)
322 | add (Tactic.Rewrite' (_, _, _, _, thm', f, (f', asm))) (is, ctxt) (pt, (p, _)) =
324 val (pt, c) = Ctree.cappend_atomic pt p (is, ctxt) f (Tactic.Rewrite thm') (f', asm) Ctree.Complete
325 val pt = Ctree.update_branch pt p Ctree.TransitiveB
327 ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term ctxt f'), pt)
329 | add (Tactic.Rewrite_Set_Inst' (_, _, subs', rls', f, (f', asm))) (is, ctxt) (pt, (p, _)) =
331 val (pt, c) = Ctree.cappend_atomic pt p (is, ctxt) f
332 (Tactic.Rewrite_Set_Inst (Subst.T_to_input ctxt subs', Rule_Set.id rls')) (f', asm) Ctree.Complete
333 val pt = Ctree.update_branch pt p Ctree.TransitiveB
335 ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term ctxt f'), pt)
337 | add (Tactic.Rewrite_Set' (_, _, rls', f, (f', asm))) (is, ctxt) (pt, (p, _)) =
339 val (pt, c) = Ctree.cappend_atomic pt p (is, ctxt) f
340 (Tactic.Rewrite_Set (Rule_Set.id rls')) (f', asm) Ctree.Complete
341 val pt = Ctree.update_branch pt p Ctree.TransitiveB
343 ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term ctxt f'), pt)
345 | add (Tactic.Check_Postcond' (_, scval)) (l as (_, ctxt)) (pt, (p, _)) =
347 val (pt, c) = Ctree.append_result pt p l (scval, []) Ctree.Complete
349 ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term ctxt scval), pt)
351 | add (Tactic.Calculate' (_, op_, f, (f', _))) (l as (_, ctxt)) (pt, (p, _)) =
353 val (pt,c) = Ctree.cappend_atomic pt p l f (Tactic.Calculate op_) (f', []) Ctree.Complete
355 ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term ctxt f'), pt)
357 | add (Tactic.Check_elementwise' (consts, pred, (f', asm))) (l as (_, ctxt)) (pt, (p, _)) =
359 val (pt,c) = Ctree.cappend_atomic pt p l consts (Tactic.Check_elementwise pred) (f', asm) Ctree.Complete
361 ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term ctxt f'), pt)
363 | add (Tactic.Or_to_List' (ors, list)) (l as (_, ctxt)) (pt, (p, _)) =
365 val (pt,c) = Ctree.cappend_atomic pt p l ors Tactic.Or_to_List (list, []) Ctree.Complete
367 ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term ctxt list), pt)
369 | add (Tactic.Substitute' (_, _, subte, t, t')) (l as (_, ctxt)) (pt, (p, _)) =
372 Ctree.cappend_atomic pt p l t
373 (Tactic.Substitute (Subst.eqs_to_input ctxt subte)) (t',[]) Ctree.Complete
374 in ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term ctxt t'), pt)
376 | add (Tactic.Tac_ (_, f, id, f')) l (pt, pos as (p, _)) =
378 val ctxt = Ctree.get_ctxt pt pos
379 val (pt, c) = Ctree.cappend_atomic pt p l
380 (ParseC.term_opt ctxt f |> the) (Tactic.Tac id) (ParseC.term_opt ctxt f' |> the, [])
383 ((p,Pos.Res), c, Test_Out.FormKF f', pt)
385 | add (Tactic.Subproblem' ((domID, pblID, metID), oris, hdl, fmz_, ctxt_specify, f))
386 (l as (_, ctxt)) (pt, (p, _)) =
388 val (pt, c) = Ctree.cappend_problem pt p l (fmz_, (domID, pblID, metID))
389 (oris, (domID, pblID, metID), hdl, ctxt_specify)
390 val f = Syntax.string_of_term ctxt f
392 ((p, Pos.Pbl), c, Test_Out.FormKF f, pt)
394 | add m' (_, ctxt) (_, pos) =
395 raise ERROR ("Solve_Step.add: not impl.for " ^ Tactic.string_of ctxt m' ^ " at " ^ Pos.pos'2str pos)
397 (* LI switches between solve-phase and specify-phase *)
398 fun add_general tac ic cs =
399 if Tactic.for_specify' tac
400 then Specify_Step.add tac ic cs
403 (* the order of State_Steps is reversed: insert last element first *)
404 fun s_add_general [] ptp = ptp
405 | s_add_general tacis (pt, c, _) =
407 val (tacis', (_, tac_, (p, is))) = split_last tacis
408 val (p', c', _, pt') = add_general tac_ is (pt, p)
410 s_add_general tacis' (pt', c@c', p')
413 (* a still undeveloped concept: do a calculation without LI *)
414 fun add_hard _(*thy*) m' (p, p_) pt =
417 Pos.Frm => p | Pos.Res => Pos.lev_on p
418 | _ => raise ERROR ("generate_hard: call by " ^ Pos.pos'2str (p,p_))
420 add_general m' (Istate_Def.empty, ContextC.empty) (pt, (p, p_))