(* Title:  Interpret/step-solve.sml

    Author: Walther Neuper 2019

    (c) due to copyright terms

 *)

 signature STEP_SOLVE =

 sig

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

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

   val by_term : Calc.T -> string -> string * Chead.calcstate' (*TODO: string * Calc.T*)

 end

 (**)

 structure Step_Solve(**): STEP_SOLVE(**) =

 struct

 (**)

 open Ctree;

 open Pos

 fun by_tactic (tac as Tactic.Apply_Method' _) (ptp as (pt, p)) =

     LI.by_tactic tac (get_istate_LI pt p, get_ctxt_LI pt p) ptp

   | by_tactic (tac as Tactic.Check_Postcond' _) (ptp as (pt, p)) =

     LI.by_tactic tac (get_istate_LI pt p, get_ctxt_LI pt p) ptp

   | by_tactic (Tactic.Free_Solve')  (pt, po as (p, _)) =

     let

       val p' = lev_dn_ (p, Res);

       val pt = update_metID pt (par_pblobj pt p) Spec.e_metID;

     in

       ("ok", ([(Tactic.Empty_Tac, Tactic.Empty_Tac_, (po, (Istate.Uistate, ContextC.empty)))], [], (pt,p')))

     end

   | by_tactic (Tactic.End_Proof'') ptp = ("end-proof", ([], [], ptp))

   | by_tactic (Tactic.End_Detail' t) (pt, (p, p_)) = (* could be done by generate1 ?!? *)

     let (*Rewrite_Set* done at Detail_Set*: this result is already in ctree*)

       val pr = (lev_up p, Res)

     in

       ("ok", ([(Tactic.End_Detail, Tactic.End_Detail' t , ((p, p_), get_loc pt (p, p_)))], [], (pt, pr)))

     end

   | by_tactic m (pt, po as (p, p_)) =

     if Spec.e_metID = get_obj g_metID pt (par_pblobj pt p) (*29.8.02: could be detail, too !!*)

     then

       let

         val ctxt = get_ctxt pt po

         val ((p, p_), ps, _, pt) =

           Generate.generate1 m (Istate.empty, ctxt) (pt, (p, p_))

 	    in ("no-method-specified", (*Free_Solve*)

 	      ([(Tactic.Empty_Tac, Tactic.Empty_Tac_, ((p, p_), (Istate.Uistate, ctxt)))], ps, (pt, (p, p_))))

       end

     else

 	    let 

 	      val thy' = get_obj g_domID pt (par_pblobj pt p);

 	      val (is, sc) = LItool.resume_prog thy' (p,p_) pt;

 	    in

         case LI.locate_input_tactic sc (pt, po) (fst is) (snd is) m of

           LI.Safe_Step (istate, ctxt, tac) =>

             let

                val p' = next_in_prog po

                val (p'', _, _,pt') =

                  Generate.generate1 tac (istate, ctxt) (pt, (p', p_))

             in

        		    ("ok", ([(Tactic.input_from_T tac, tac, (p'', (istate, ctxt)))],

                 [(*Ctree NOT cut*)], (pt', p'')))

             end

 	      | LI.Unsafe_Step (istate, ctxt, tac) =>

             let

                val p' = 

                  case p_ of Frm => p 

                  | Res => lev_on p

                  | _ => error ("Step_Solve.by_tactic: call by " ^ pos'2str (p, p_));

                val (p'', _, _,pt') =

                  Generate.generate1 tac (istate, ctxt) (pt, (p', p_));

             in

        		    ("ok", ([(Tactic.input_from_T tac, tac, (p'', (istate, ctxt)))],

                 [(*Ctree NOT cut*)], (pt', p'')))

             end

 	      | _ => (* NotLocatable *)

 	        let 

 	          val (p,ps, _, pt) = Generate.generate_hard (ThyC.get_theory "Isac_Knowledge") m (p, p_) pt;

 	        in

 	          ("not-found-in-program", ([(Tactic.input_from_T m, m, (po, is))], ps, (pt, p)))

           end

 	    end;

 val do_next = LI.do_next

 (*

   Locate a step in a program, which has been determined by input of a term.

   Special case: if the term is a CAS-command, then create a calchead, and do 1 step.

   If "no derivation found" then Error_Fill_Pattern.check_for.

   (Error_Fill_Pattern.check_for *within* compare_step seems too expensive)

 *)

 (*fun by_term (next_cs as (_, _, (pt, pos as (p, _))): Chead.calcstate') istr =*)

 fun by_term (pt, pos as (p, _)) istr =

   case TermC.parse (ThyC.get_theory "Isac_Knowledge") istr of

     NONE => ("syntax error in '" ^ istr ^ "'", Chead.e_calcstate')

   | SOME f_in =>

     let

   	  val f_in = Thm.term_of f_in

       val pos_pred = lev_back(*'*) pos

   	  val f_pred = Ctree.get_curr_formula (pt, pos_pred);

   	  val f_succ = Ctree.get_curr_formula (pt, pos);

     in

       if f_succ = f_in

       then ("same-formula", ([], [], (pt, pos))) (* ctree not cut with replaceFormula *)

       else

         case In_Chead.cas_input f_in of

           SOME (pt, _) => ("ok", ([], [], (pt, (p, Pos.Met))))

 		    | NONE =>

           case LI.locate_input_term (pt, pos) f_in of

             LI.Found_Step cstate =>

             ("ok" , ([], [], cstate (* already contains istate, ctxt *)))

           | LI.Not_Derivable =>

             let

           	  val pp = Ctree.par_pblobj pt p

           	  val (errpats, nrls, prog) = case Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp) of

           		    {errpats, nrls, scr = Rule.Prog prog, ...} => (errpats, nrls, prog)

           		  | _ => error "inform: uncovered case of get_met"

           	  val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate

           	in

           	  case Error_Fill_Pattern.check_for (f_pred, f_in) (prog, env) (errpats, nrls) of

           	    SOME errpatID => ("error pattern #" ^ errpatID ^ "#", Chead.e_calcstate')

           	  | NONE => ("no derivation found", Chead.e_calcstate')

             end

     end

 end