1 (* Title: MathEngine/step.sml
2 Author: Walther Neuper 2019
3 (c) due to copyright terms
5 Unify function of structure Step_Specify and structure Step_Solve
6 as well as of structure Specify_Step and structure Solve_Step.
11 val do_next: Pos.pos' -> Calc.state_pre -> string * Calc.state_post
12 val by_tactic: Tactic.input -> Calc.T -> string * Calc.state_post
13 (*val by_term = Step_Solve.by_term: Calc.T -> term -> string * Calc.state_post NOT for specify*)
14 val check: Tactic.input -> Calc.T -> Applicable.T
15 val add: Tactic.T -> Istate_Def.T * Proof.context -> Calc.T -> Test_Out.T
17 val inconsistent: Subst.input option * ThmC.T -> term -> Istate_Def.T * Proof.context ->
18 Pos.pos' -> Ctree.ctree -> Calc.T
21 val specify_do_next: Calc.T -> string * Calc.state_post
22 val switch_specify_solve: Pos.pos_ -> Calc.T -> string * Calc.state_post
27 structure Step(**): STEP(**) =
31 (** check a tactic for applicability **)
33 fun check tac (ctree, pos) =
34 if Tactic.for_specify tac
35 then Specify_Step.check tac (ctree, pos)
36 else Solve_Step.check tac (ctree, pos);
39 (** add a step to a calculation **)
41 val add = Solve_Step.add_general;
44 (* survey on results of by_tactic, find_next, by_term:
46 * by_tactic "ok", "ok",
48 * locate_input_tactic : "ok", "unsafe-ok", "not-applicable", "end-of-calculation"
49 * locate_input_term : "ok", "syntax error", "same-formula", "no derivation found",
50 "error pattern #" ^ errpatID (the latter doesn't fit into the pattern of fixed string)
51 * find_next_formula : "ok", "helpless", "no-fmz-spec"(=helpless), "end-of-calculation"
54 (** do a next step **)
56 fun specify_do_next (ptp as (pt, (p, p_))) =
58 val (_, (p_', tac)) = Specify.find_next_step ptp
59 val ist_ctxt = Ctree.get_loc pt (p, p_)
62 Tactic.Apply_Method mI =>
63 (*vvvvvvvvvv-------------------------------------------------------------- solve-phase *)
64 LI.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty))
65 ist_ctxt (pt, (p, p_'))
66 | _ => Step_Specify.by_tactic_input tac (pt, (p, p_'))
69 fun switch_specify_solve state_pos (pt, input_pos) =
72 if Pos.on_specification ([], state_pos)
73 then specify_do_next (pt, input_pos)
74 else LI.do_next (pt, input_pos)
77 (*unclean alternatives*)
78 scs as ("ok", _) => scs
79 | (_, cs as ([], _, _)) => ("helpless", cs)
80 | _ => raise ERROR "switch_specify_solve: uncovered case in fun.def."
83 (* does a step forward; returns tactic used, ctree updated (i.e. with NEW term/calchead) *)
84 fun do_next (ip as (_, p_)) (ptp as (pt, p), tacis) =
85 if Pos.on_calc_end ip then
86 ("end-of-calculation", (tacis, [], ptp): Calc.state_post)
89 val (_, probl_id, _) = Calc.references (pt, p);
93 if ip = p (*the request is done where ptp waits for*) then
94 let (*spurious -------------vvvvvvvvvvvvvv*)
95 val (pt', c', p') = Solve_Step.s_add_general tacis (pt, [], p)
97 ("ok", (tacis, c', (pt', p')))
100 switch_specify_solve p_ (pt, ip)
102 if probl_id = Problem.id_empty then
103 ("no-fmz-spec", ([], [], ptp))
104 else switch_specify_solve p_ (pt, ip)
108 (** locate an input tactic **)
110 (* LEGACY: report of tacs' applicability in tacis; pt is dropped in setNextTactic*)
111 fun by_tactic _ (ptp as (_, ([], Pos.Res))) = ("end-of-calculation", ([], [], ptp))
112 | by_tactic tac (ptp as (pt, p)) =
113 case check tac (pt, p) of
114 Applicable.No _ => ("not-applicable", ([],[], ptp): Calc.state_post)
115 | Applicable.Yes tac' =>
116 if Tactic.for_specify' tac'
117 then Step_Specify.by_tactic tac' ptp
118 else Step_Solve.by_tactic tac' ptp
121 (** add an inconsisten step **)
123 fun inconsistent (subs_opt, thm') f' (is, ctxt) (pos as (p,_)) pt =
125 val f = Ctree.get_curr_formula (pt, pos)
126 val pos' as (p', _) = (Pos.lev_on p, Pos.Res)
127 val (pt, _) = case subs_opt of
128 NONE => Ctree.cappend_atomic pt p' (is, ctxt) f
129 (Tactic.Rewrite thm') (f', []) Ctree.Inconsistent
130 | SOME subs => Ctree.cappend_atomic pt p' (is, ctxt) f
131 (Tactic.Rewrite_Inst (subs, thm')) (f', []) Ctree.Inconsistent
132 val pt = Ctree.update_branch pt p' Ctree.TransitiveB