(* 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' -> Chead.calcstate -> string * Chead.calcstate'

   val by_tactic: Tactic.input -> Calc.T -> string * Chead.calcstate'

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

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

 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)

   (*NONE*)                                                     

 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )

   val specify_do_next: Calc.T -> string * Chead.calcstate'

   val switch_specify_solve: Pos.pos_ -> Calc.T -> string * Chead.calcstate'

 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)

 end

 (**)

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

 struct

 (**)

 (** check a tactic for applicability **)

 fun check tac (ctree, pos) =

   if Pos.on_specification (snd pos)

   then Specify_Step.check tac (ctree, pos)

   else Solve_Step.check tac (ctree, pos)

 (* 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)) = SpecifyNEW.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_'))

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

   end

 fun switch_specify_solve state_pos (pt, input_pos) =

   let

     val result =

       if Library.member op = [Pos.Pbl, Pos.Met] state_pos

   	  then specify_do_next (pt, input_pos)

       else LI.do_next (pt, input_pos)

   in

     case result of

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

     | scs => scs

   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) =

   let

     val pIopt = Ctree.get_pblID (pt, ip);

   in

     if ip = ([], Pos.Res)

     then ("end-of-calculation", (tacis, [], ptp): Chead.calcstate') 

     else

       case tacis of

         (_ :: _) => 

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

           then 

             let val (pt', c', p') = Generate.generate tacis (pt, [], p)

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

           else

             switch_specify_solve p_ (pt, ip)

       | _ => case pIopt of

   	            NONE => ("no-fmz-spec", ([], [], ptp))

   	          | SOME _ => 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): Chead.calcstate')

 	  | Applicable.Yes tac' =>

 	    if Tactic.for_specify' tac'

 	    then Step_Specify.by_tactic tac' ptp

 	    else Step_Solve.by_tactic tac' ptp

 (**)end(**)