walther@59747: (* Title: MathEngine/step.sml walther@59747: Author: Walther Neuper 2019 walther@59747: (c) due to copyright terms walther@59920: walther@59920: Unify function of structure Step_Specify and structure Step_Solve walther@59920: as well as of structure Specify_Step and structure Solve_Step. walther@59747: *) walther@59747: walther@59747: signature STEP = walther@59747: sig walther@59981: val do_next: Pos.pos' -> Calc.state_pre -> string * Calc.state_post walther@59981: val by_tactic: Tactic.input -> Calc.T -> string * Calc.state_post walther@59981: (*val by_term = Step_Solve.by_term: Calc.T -> term -> string * Calc.state_post NOT for specify*) walther@59921: val check: Tactic.input -> Calc.T -> Applicable.T walther@59959: val add: Tactic.T -> Istate_Def.T * Proof.context -> Calc.T -> Test_Out.T walther@59959: walther@59959: val inconsistent: Subst.input option * ThmC.T -> term -> Istate_Def.T * Proof.context -> walther@59959: Pos.pos' -> Ctree.ctree -> Calc.T Walther@60567: wenzelm@60223: \<^isac_test>\ walther@59981: val specify_do_next: Calc.T -> string * Calc.state_post walther@59981: val switch_specify_solve: Pos.pos_ -> Calc.T -> string * Calc.state_post wenzelm@60223: \ walther@59747: end walther@59747: walther@59747: (**) walther@59747: structure Step(**): STEP(**) = walther@59747: struct walther@59803: (**) walther@59747: walther@59921: (** check a tactic for applicability **) walther@59921: walther@59921: fun check tac (ctree, pos) = walther@59932: if Tactic.for_specify tac walther@59922: then Specify_Step.check tac (ctree, pos) walther@59932: else Solve_Step.check tac (ctree, pos); walther@59932: walther@59932: walther@59932: (** add a step to a calculation **) walther@59932: walther@59932: val add = Solve_Step.add_general; walther@59921: walther@59921: walther@59920: (* survey on results of by_tactic, find_next, by_term: walther@59920: * Step_Specify walther@59920: * by_tactic "ok", "ok", walther@59920: * Step_Solve walther@59920: * locate_input_tactic : "ok", "unsafe-ok", "not-applicable", "end-of-calculation" walther@59920: * locate_input_term : "ok", "syntax error", "same-formula", "no derivation found", walther@59920: "error pattern #" ^ errpatID (the latter doesn't fit into the pattern of fixed string) walther@59920: * find_next_formula : "ok", "helpless", "no-fmz-spec"(=helpless), "end-of-calculation" walther@59920: *) walther@59920: walther@59804: (** do a next step **) walther@59804: walther@59763: fun specify_do_next (ptp as (pt, (p, p_))) = walther@59763: let walther@59976: val (_, (p_', tac)) = Specify.find_next_step ptp walther@59763: val ist_ctxt = Ctree.get_loc pt (p, p_) walther@59763: in walther@59763: case tac of walther@59803: Tactic.Apply_Method mI => walther@59803: (*vvvvvvvvvv-------------------------------------------------------------- solve-phase *) walther@59846: LI.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)) walther@59763: ist_ctxt (pt, (p, p_')) Walther@60556: | _ => Step_Specify.by_tactic_input tac (pt, (p, p_')) walther@59763: end walther@59763: walther@59803: fun switch_specify_solve state_pos (pt, input_pos) = walther@59803: let walther@59803: val result = walther@59932: if Pos.on_specification ([], state_pos) walther@59803: then specify_do_next (pt, input_pos) walther@59803: else LI.do_next (pt, input_pos) walther@59803: in walther@59803: case result of walther@60021: (*unclean alternatives*) walther@60021: scs as ("ok", _) => scs walther@60021: | (_, cs as ([], _, _)) => ("helpless", cs) walther@60269: | _ => raise ERROR "switch_specify_solve: uncovered case in fun.def." walther@59803: end walther@59803: walther@59794: (* does a step forward; returns tactic used, ctree updated (i.e. with NEW term/calchead) *) walther@59781: fun do_next (ip as (_, p_)) (ptp as (pt, p), tacis) = walther@60011: if Pos.on_calc_end ip then walther@60011: ("end-of-calculation", (tacis, [], ptp): Calc.state_post) walther@60011: else walther@60011: let walther@60011: val (_, probl_id, _) = Calc.references (pt, p); walther@60011: in walther@60011: case tacis of walther@60011: (_ :: _) => walther@60021: if ip = p (*the request is done where ptp waits for*) then walther@60021: let (*spurious -------------vvvvvvvvvvvvvv*) walther@60011: val (pt', c', p') = Solve_Step.s_add_general tacis (pt, [], p) walther@60011: in walther@60011: ("ok", (tacis, c', (pt', p'))) walther@60011: end walther@60011: else walther@60011: switch_specify_solve p_ (pt, ip) walther@60011: | _ => walther@60011: if probl_id = Problem.id_empty then walther@60011: ("no-fmz-spec", ([], [], ptp)) walther@60011: else switch_specify_solve p_ (pt, ip) walther@60011: end; walther@60011: walther@59805: walther@59804: (** locate an input tactic **) walther@59804: walther@59806: (* LEGACY: report of tacs' applicability in tacis; pt is dropped in setNextTactic*) walther@59804: fun by_tactic _ (ptp as (_, ([], Pos.Res))) = ("end-of-calculation", ([], [], ptp)) walther@59921: | by_tactic tac (ptp as (pt, p)) = walther@59921: case check tac (pt, p) of walther@59981: Applicable.No _ => ("not-applicable", ([],[], ptp): Calc.state_post) walther@59921: | Applicable.Yes tac' => walther@59921: if Tactic.for_specify' tac' walther@59921: then Step_Specify.by_tactic tac' ptp walther@59921: else Step_Solve.by_tactic tac' ptp walther@59921: walther@59804: walther@59959: (** add an inconsisten step **) walther@59959: walther@59959: fun inconsistent (subs_opt, thm') f' (is, ctxt) (pos as (p,_)) pt = walther@59959: let walther@59959: val f = Ctree.get_curr_formula (pt, pos) walther@59959: val pos' as (p', _) = (Pos.lev_on p, Pos.Res) walther@59959: val (pt, _) = case subs_opt of walther@59959: NONE => Ctree.cappend_atomic pt p' (is, ctxt) f walther@59959: (Tactic.Rewrite thm') (f', []) Ctree.Inconsistent walther@59959: | SOME subs => Ctree.cappend_atomic pt p' (is, ctxt) f walther@59959: (Tactic.Rewrite_Inst (subs, thm')) (f', []) Ctree.Inconsistent walther@59959: val pt = Ctree.update_branch pt p' Ctree.TransitiveB walther@59959: in (pt, pos') end walther@59959: walther@59803: (**)end(**)