(* Title:  MathEngine/step.sml

    Author: Walther Neuper 2019

    (c) due to copyright terms

 *)

 (* 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"

  *)

 signature STEP =

 sig

   val do_next: Ctree.pos' -> Chead.calcstate -> string * Chead.calcstate'

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

 (*

   val by_tactic = Step_Solve.by_tactic

                 = Step_Specify.by_tactic ? depending on PIDE, see TODO.thy

   val by_term   = Step_Solve.by_term: Calc.T -> term -> string * Chead.calcstate'

 TODO --------------------------------------"----------> ??????   Calc.T 

                 = Step_Specify.by_tactic ? depending on PIDE, see TODO.thy

 *)

 (* ---- 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'

   datatype lOc_ = ERror of string | UNsafe of Chead.calcstate' | Updated of Chead.calcstate'

   val loc_solve_ : Tactic.T -> Calc.T -> lOc_

   val loc_specify_ : Tactic.T -> Calc.T -> lOc_

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

 end

 (**)

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

 struct

 (**)

 (** 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.e_istate, ContextC.e_ctxt))

   	      ist_ctxt (pt, (p, p_'))

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

   end

 fun switch_specify_solve state_pos (pt, input_pos) =

   let

     val result =

       if 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 **)

 datatype lOc_ = ERror of string | UNsafe of Chead.calcstate' | Updated of Chead.calcstate'

 (*  loc_specify_ : Tactic.T -> Calc.T -> lOc_*)

 fun loc_specify_ m (pt, pos) =

   let

     val (p, _, f, _, _, pt) = Chead.specify m pos [] pt;

   in

     case f of (Generate.Error' e) => ERror e | _ => Updated ([], [], (pt,p))

   end

 (*  loc_solve_ : Tactic.T -> Calc.T -> lOc_*)

 fun loc_solve_ m (pt, pos) =

   let

     val (msg, cs') = Step_Solve.by_tactic m (pt, pos); (*..sig.OK*)

   in

     case msg of "ok" => Updated cs' | msg => ERror msg 

   end

 (* locate a tactic in a program and apply it if possible;

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

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

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

     case Applicable.applicable_in p pt m of

 	    Applicable.Notappl _ => ("not-applicable", ([],[],  ptp): Chead.calcstate')

 	  | Applicable.Appl m =>

 	    let 

         val x = if Tactic.for_specify' m

 		      then loc_specify_ m ptp else loc_solve_ m ptp

 	    in 

 	      case x of 

 		      ERror _ => ("failure", ([], [], ptp))

 		      (*FIXXXXXME: loc_specify_, loc_solve_ TOGETHER with dropping meOLD+detail.sml*)

 		    | UNsafe cs' => ("unsafe-ok", cs')

 		    | Updated (cs' as (_, _, (_, p'))) => (*ev.SEVER.tacs like Begin_Trans*)

 		      (if p' = ([], Pos.Res) then "end-of-calculation" else "ok", cs')

           (*for SEVER.tacs user to ask ? *)

 	    end

 (**)end(**)