(* Title:  Interpret/step-solve.sml

   Author: Walther Neuper 2019

   (c) due to copyright terms

*)

signature STEP_SOLVE =

sig

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

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

  val by_term : Calc.T -> string -> string * Calc.state_post (*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) MethodC.id_empty;

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

    let

      val ctxt = get_ctxt pt po

      val thy = Proof_Context.theory_of ctxt

    in

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

      then

        let val ((p, p_), ps, _, pt) = Solve_Step.add_general 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 (is, sc) = LItool.resume_prog (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') = Solve_Step.add_general tac (istate, ctxt) (pt, (p', p_))

              in

         		    ("ok", ([(Tactic.input_from_T ctxt 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

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

                 val (p'', _, _,pt') = Solve_Step.add_general tac (istate, ctxt) (pt, (p', p_));

              in

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

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

              end

  	      | _ => (* NotLocatable *)

  	        let val (p,ps, _, pt) = Solve_Step.add_hard thy m (p, p_) pt;

  	        in

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

            end

  	    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_Pattern.check_for.

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

*)

(*fun by_term (next_cs as (_, _, (pt, pos as (p, _))): Calc.state_post) istr =*)

(*will come directly from PIDE--vvvvvvvvvvv*)

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

  let

    val f_in = Syntax.read_term (Ctree.get_ctxt pt pos) istr

      handle ERROR msg => error (msg (*^ Position.here pp*))

    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 CAS_Cmd.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 ctxt = Ctree.get_ctxt pt pos

            val met_id = Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p)

        	  val (errpats, rew_rls, prog) = (* after shift to Diff --vvvvvvvvvvvvvvv ctxt should be sufficient*)

        	    case MethodC.from_store' (Know_Store.get_via_last_thy "Build_Thydata") met_id of

        		    {errpats, rew_rls, program = Rule.Prog prog, ...} => (errpats, rew_rls, prog)

        		  | _ => raise ERROR "inform: uncovered case of get_met"

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

        	in

        	  case Error_Pattern.check_for (Ctree.get_ctxt pt pos) (f_pred, f_in) (prog, env) (errpats, rew_rls) of

        	    SOME errpatID => ("error pattern #" ^ errpatID ^ "#", Calc.state_empty_post)

        	  | NONE => ("no derivation found", Calc.state_empty_post)

          end

  end

end