(* Title:  MathEngine/step.sml

   Author: Walther Neuper 2019

   (c) due to copyright terms

Unify function of structure Step_Specify and structure Step_Solve

as well as of structure Specify_Step and structure Solve_Step.

*)

signature STEP =

sig

  val do_next: Pos.pos' -> Calc.state_pre -> string * Calc.state_post

  val by_tactic: Tactic.input -> Calc.T -> string * Calc.state_post

(*val by_term  = Step_Solve.by_term: Calc.T -> term -> string * Calc.state_post NOT for specify*)

  val check: Tactic.input -> Calc.T -> Applicable.T

  val add: Tactic.T -> Istate_Def.T * Proof.context -> Calc.T -> Test_Out.T

  val inconsistent: Subst.input option * ThmC.T -> term -> Istate_Def.T * Proof.context ->

    Pos.pos' -> Ctree.ctree -> Calc.T

\<^isac_test>\<open>

  val specify_do_next: Calc.T -> string * Calc.state_post

  val switch_specify_solve: Pos.pos_ -> Calc.T -> string * Calc.state_post

\<close>

end

(**)

structure Step(**): STEP(**) =

struct

(**)

(** check a tactic for applicability **)

fun check tac (ctree, pos) =

  if Tactic.for_specify tac

  then Specify_Step.check tac (ctree, pos)

  else Solve_Step.check tac (ctree, pos);

(** add a step to a calculation **)

val add = Solve_Step.add_general;

(* survey on results of by_tactic, find_next, by_term:

   * Step_Specify

     * by_tactic "ok", "ok", 

   * Step_Solve              

     * locate_input_tactic  : "ok", "unsafe-ok", "not-applicable", "end-of-calculation"

     * locate_input_term : "ok", "syntax error", "same-formula", "no derivation found",

        "error pattern #" ^ errpatID (the latter doesn't fit into the pattern of fixed string)

     * find_next_formula    : "ok", "helpless", "no-fmz-spec"(=helpless), "end-of-calculation"

 *)

(** do a next step **)

fun specify_do_next (ptp as (pt, (p, p_))) =

  let

    val (_, (p_', tac)) = Specify.find_next_step ptp

    val ist_ctxt =  Ctree.get_loc pt (p, p_)

  in

    case tac of

  	  Tactic.Apply_Method mI =>

  	    (*vvvvvvvvvv-------------------------------------------------------------- solve-phase *)

  	    LI.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty))

  	      ist_ctxt (pt, (p, p_'))

    | _ => Step_Specify.by_tactic_input  tac (pt, (p, p_'))

  end

fun switch_specify_solve state_pos (pt, input_pos) =

  let

    val result =

      if Pos.on_specification ([], state_pos)

  	  then specify_do_next (pt, input_pos)

      else LI.do_next (pt, input_pos)

  in

    case result of

    (*unclean alternatives*)

      scs as ("ok", _) => scs

    | (_, cs as ([], _, _)) => ("helpless", cs)

    | _ => raise ERROR "switch_specify_solve: uncovered case in fun.def."

  end

(* does a step forward; returns tactic used, ctree updated (i.e. with NEW term/calchead) *)

fun do_next (ip as (_, p_)) (ptp as (pt, p), tacis) =

  if Pos.on_calc_end ip then

    ("end-of-calculation", (tacis, [], ptp): Calc.state_post) 

  else

    let

      val (_, probl_id, _) = Calc.references (pt, p);

    in

      case tacis of

        (_ :: _) => 

          if ip = p (*the request is done where ptp waits for*) then                 

            let     (*spurious -------------vvvvvvvvvvvvvv*)

              val (pt', c', p') = Solve_Step.s_add_general tacis (pt, [], p)

            in

             ("ok", (tacis, c', (pt', p')))

            end

         else

            switch_specify_solve p_ (pt, ip)

      | _ =>

        if probl_id = Problem.id_empty then

           ("no-fmz-spec", ([], [], ptp))

        else switch_specify_solve p_ (pt, ip)

    end;

(** locate an input tactic **)

(* LEGACY: report of tacs' applicability in tacis; pt is dropped in setNextTactic*)

fun by_tactic _ (ptp as (_, ([], Pos.Res))) = ("end-of-calculation", ([], [], ptp))

  | by_tactic tac (ptp as (pt, p)) =

    case check tac (pt, p) of

	    Applicable.No _ => ("not-applicable", ([],[],  ptp): Calc.state_post)

	  | Applicable.Yes tac' =>

	    if Tactic.for_specify' tac'

	    then Step_Specify.by_tactic tac' ptp

	    else Step_Solve.by_tactic tac' ptp

(** add an inconsisten step **)

fun inconsistent (subs_opt, thm') f' (is, ctxt) (pos as (p,_)) pt =

  let

    val f = Ctree.get_curr_formula (pt, pos)

    val pos' as (p', _) = (Pos.lev_on p, Pos.Res)

    val (pt, _) = case subs_opt of

      NONE => Ctree.cappend_atomic pt p' (is, ctxt) f

        (Tactic.Rewrite thm') (f', []) Ctree.Inconsistent

    | SOME subs => Ctree.cappend_atomic pt p' (is, ctxt) f

        (Tactic.Rewrite_Inst (subs, thm')) (f', []) Ctree.Inconsistent

    val pt = Ctree.update_branch pt p' Ctree.TransitiveB

  in (pt, pos') end

(**)end(**)