(* Title:  solve an example by interpreting a method's script

   Author: Walther Neuper 1999

   (c) copyright due to lincense terms.

*)

signature SOLVE_PHASE =

sig

  datatype auto = CompleteCalc | CompleteCalcHead | CompleteModel | CompleteSubpbl 

  | CompleteToSubpbl | Step of int

  val autoord : auto -> int

  type tac'_

  val mk_tac'_ : Tactic.input -> string * Tactic.input

  val specsteps : string list

  val all_solve : auto -> Ctree.pos' list -> Ctree.state ->

    string * Ctree.pos' list * (Ctree.ctree * (int list * Ctree.pos_))

  val complete_solve :

     auto -> Ctree.pos' list -> Ctree.state -> string * Ctree.pos' list * Ctree.state

  val solve : string * Tactic.T -> Ctree.state -> string * Chead.calcstate'

  val inform : Chead.calcstate' -> string -> string * Chead.calcstate'

  val detailrls : Ctree.ctree -> Ctree.pos' -> string * Ctree.ctree * Ctree.pos'

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

  val get_form : tac'_ -> Ctree.pos' -> Ctree.ctree -> Generate.mout

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

  (*NONE*)

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

(*----- unused code, kept as hints to design ideas ---------------------------------------------*)

  (* NONE *)

end

(**)

structure Solve(**): SOLVE_PHASE(**) =

struct

(**)

open Ctree;

type mstID = string;

type tac'_ = mstID * Tactic.input; (*DG <-> ME*)

fun mk_tac'_   m = case m of (* scr not cleaned -- will disappear eventually *)

  Tactic.Init_Proof (ppc, spec)    => ("Init_Proof", Tactic.Init_Proof (ppc, spec )) 

| Tactic.Model_Problem             => ("Model_Problem", Tactic.Model_Problem)

| Tactic.Refine_Tacitly pblID      => ("Refine_Tacitly", Tactic.Refine_Tacitly pblID)

| Tactic.Refine_Problem pblID      => ("Refine_Problem", Tactic.Refine_Problem pblID)

| Tactic.Add_Given cterm'          => ("Add_Given", Tactic.Add_Given cterm') 

| Tactic.Del_Given cterm'          => ("Del_Given", Tactic.Del_Given cterm') 

| Tactic.Add_Find cterm'           => ("Add_Find", Tactic.Add_Find cterm') 

| Tactic.Del_Find cterm'           => ("Del_Find", Tactic.Del_Find cterm') 

| Tactic.Add_Relation cterm'       => ("Add_Relation", Tactic.Add_Relation cterm') 

| Tactic.Del_Relation cterm'       => ("Del_Relation", Tactic.Del_Relation cterm') 

| Tactic.Specify_Theory domID	    => ("Specify_Theory", Tactic.Specify_Theory domID) 

| Tactic.Specify_Problem pblID     => ("Specify_Problem", Tactic.Specify_Problem pblID)

| Tactic.Specify_Method metID	    => ("Specify_Method", Tactic.Specify_Method metID) 

| Tactic.Apply_Method metID	    => ("Apply_Method", Tactic.Apply_Method metID) 

| Tactic.Check_Postcond pblID	    => ("Check_Postcond", Tactic.Check_Postcond pblID)

| Tactic.Free_Solve                => ("Free_Solve", Tactic.Free_Solve)

| Tactic.Rewrite_Inst (subs, thm') => ("Rewrite_Inst", Tactic.Rewrite_Inst (subs, thm')) 

| Tactic.Rewrite thm'		    => ("Rewrite", Tactic.Rewrite thm') 

| Tactic.Rewrite_Asm thm'	    => ("Rewrite_Asm", Tactic.Rewrite_Asm thm') 

| Tactic.Rewrite_Set_Inst (subs, rls')

               => ("Rewrite_Set_Inst", Tactic.Rewrite_Set_Inst (subs, rls')) 

| Tactic.Rewrite_Set rls'          => ("Rewrite_Set", Tactic.Rewrite_Set rls') 

| Tactic.End_Ruleset		    => ("End_Ruleset", Tactic.End_Ruleset)

| Tactic.End_Detail                => ("End_Detail", Tactic.End_Detail)

| Tactic.Detail_Set rls'           => ("Detail_Set", Tactic.Detail_Set rls')

| Tactic.Detail_Set_Inst (s, rls') => ("Detail_Set_Inst", Tactic.Detail_Set_Inst (s, rls'))

| Tactic.Calculate op_             => ("Calculate", Tactic.Calculate op_)

| Tactic.Substitute sube           => ("Substitute", Tactic.Substitute sube) 

| Tactic.Apply_Assumption cts'	    => ("Apply_Assumption", Tactic.Apply_Assumption cts')

| Tactic.Take cterm'               => ("Take", Tactic.Take cterm') 

| Tactic.Take_Inst cterm'          => ("Take_Inst", Tactic.Take_Inst cterm') 

| Tactic.Subproblem (domID, pblID) => ("Subproblem", Tactic.Subproblem (domID, pblID)) 

(*

| Tactic.Subproblem_Full(spec,cts')=> ("Subproblem_Full", Tactic.Subproblem_Full(spec,cts')) 

*)

| Tactic.End_Subproblem            => ("End_Subproblem", Tactic.End_Subproblem)

| Tactic.CAScmd cterm'		    => ("CAScmd", Tactic.CAScmd cterm')

| Tactic.Split_And                 => ("Split_And", Tactic.Split_And) 

| Tactic.Conclude_And		    => ("Conclude_And", Tactic.Conclude_And) 

| Tactic.Split_Or                  => ("Split_Or", Tactic.Split_Or) 

| Tactic.Conclude_Or		    => ("Conclude_Or", Tactic.Conclude_Or) 

| Tactic.Begin_Trans               => ("Begin_Trans", Tactic.Begin_Trans) 

| Tactic.End_Trans		    => ("End_Trans", Tactic.End_Trans) 

| Tactic.Begin_Sequ                => ("Begin_Sequ", Tactic.Begin_Sequ) 

| Tactic.End_Sequ                  => ("End_Sequ", Tactic.Begin_Sequ) 

| Tactic.Split_Intersect           => ("Split_Intersect", Tactic.Split_Intersect) 

| Tactic.End_Intersect		    => ("End_Intersect", Tactic.End_Intersect) 

| Tactic.Check_elementwise cterm'  => ("Check_elementwise", Tactic.Check_elementwise cterm')

| Tactic.Or_to_List                => ("Or_to_List", Tactic.Or_to_List) 

| Tactic.Collect_Trues	            => ("Collect_Results", Tactic.Collect_Trues) 

| Tactic.Empty_Tac               => ("Empty_Tac", Tactic.Empty_Tac)

| Tactic.Tac string              => ("Tac", Tactic.Tac string)

| Tactic.End_Proof'                => ("End_Proof'", Tactic.End_Proof')

| _ => error "mk_tac'_: uncovered case"; 

type squ = ctree; (* TODO: safe etc. *)

val specsteps = ["Init_Proof", "Refine_Tacitly", "Refine_Problem", "Model_Problem",

  "Add_Given", "Del_Given", "Add_Find", "Del_Find", "Add_Relation", "Del_Relation",

  "Specify_Theory", "Specify_Problem", "Specify_Method"];

(*FIXME.WN050821 compare solve    ...   begin_end_prog:

        WN190811: solve ("Apply_Method",.. used by root-pbl + by locate_input_tactic !!!

*)

fun solve ("Apply_Method", m as Tactic.Apply_Method' (mI, _, _, _)) (pt, (pos as (p, _))) =

    let val {srls, ...} = Specify.get_met mI;

      val itms = case get_obj I pt p of

        PblObj {meth=itms, ...} => itms

      | _ => error "solve Apply_Method: uncovered case get_obj"

      val thy' = get_obj g_domID pt p;

      val thy = Celem.assoc_thy thy';

      val (is, env, ctxt, sc) = case Lucin.init_scrstate thy itms mI of

        (is as Istate.ScrState (env,_,_,_,_,_), ctxt, sc) =>  (is, env, ctxt, sc)

      | _ => error "solve Apply_Method: uncovered case init_scrstate"

      val ini = Lucin.init_form thy sc env;

      val p = lev_dn p;

    in 

      case ini of

	      SOME t =>

          let val (pos,c,_, pt) = 

		        Generate.generate1 thy (Tactic.Apply_Method' (mI, SOME t, is, ctxt))

		        (is, ctxt) (lev_on p, Frm)(*implicit Take*) pt;

	        in ("ok",([(Tactic.Apply_Method mI, Tactic.Apply_Method' (mI, SOME t, is, ctxt), 

		        ((lev_on p, Frm), (is, ctxt)))], c, (pt, pos))) 

	        end	      

	    | NONE => (*execute the first tac in the Script, compare solve m*)

	        let

            val (m', (is', ctxt'), _) = LucinNEW.determine_next_tactic (thy', srls) (pt, (p, Res)) sc (is, ctxt);

	        in 

            case LucinNEW.locate_input_tactic sc (pt, (p, Res)) is' ctxt' m' of

              LucinNEW.Safe_Step (cstate, istate, ctxt, tac) =>

		            ("ok", ([(Lucin.tac_2tac tac, tac, (snd cstate, (istate, ctxt)))], [(*ctree NOT cut*)], cstate))

		        | _ => (* NotLocatable *)

		            let val (p, ps, _, pt) = Generate.generate_hard (Celem.assoc_thy "Isac") m (p, Frm) pt;

		            in 

		              ("not-found-in-script",([(Lucin.tac_2tac m, m, (pos, (is, ctxt)))], ps, (pt, p))) 

		            end

	        end

    end

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

    let

      val p' = lev_dn_ (p, Res);

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

    in

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

    end

  | solve ("Check_Postcond", Tactic.Check_Postcond' (pI, _)) (pt, (p, p_)) =

    let

      val pp = par_pblobj pt p

      val asm = 

        (case get_obj g_tac pt p of

		       Tactic.Check_elementwise _ => (*collects and instantiates asms*)

		         (snd o (get_obj g_result pt)) p

		     | _ => get_assumptions_ pt (p,p_))

	      handle _ => [] (*WN.27.5.03 asms in subpbls not completely clear*)

      val metID = get_obj g_metID pt pp;

      val {srls = srls, scr = sc, ...} = Specify.get_met metID;

      val (loc, E, l, a, b, ctxt) = case get_loc pt (p, p_) of

        loc as (Istate.ScrState (E, l, a, _, _, b), ctxt) => (loc, E, l, a, b, ctxt)

      | _ => error "solve Check_Postcond: uncovered case get_loc"

      val thy' = get_obj g_domID pt pp;

      val thy = Celem.assoc_thy thy';

      val (_, _, (scval, scsaf)) = LucinNEW.determine_next_tactic (thy', srls) (pt, (p, p_)) sc loc;

    in 

      if pp = [] 

      then

	      let 

          val is = Istate.ScrState (E,l,a,scval,scsaf,b)

	        val tac_ = Tactic.Check_Postcond' (pI, (scval, asm))

	        val (pos, ps, _, pt) = Generate.generate1 thy tac_ (is, ctxt) (pp, Res) pt;

	      in ("ok", ([(Tactic.Check_Postcond pI, tac_, ((pp, Res), (is, ctxt)))], ps, (pt, pos))) end

      else

        let (*resume script of parpbl, transfer value of subpbl-script*)

          val ppp = par_pblobj pt (lev_up p);

	        val thy' = get_obj g_domID pt ppp;

          val thy = Celem.assoc_thy thy';

          val (E, l, a, b, ctxt') = case get_loc pt (pp, Frm) of

            (Istate.ScrState (E, l, a, _, _, b), ctxt') => (E, l, a, b, ctxt')

          | _ => error "solve Check_Postcond resume script of parpbl: uncovered case get_loc"

	        val ctxt'' = ContextC.from_subpbl_to_caller ctxt scval ctxt'

          val ((p, p_), ps, _, pt) = Generate.generate1 thy (Tactic.Check_Postcond' (pI, (scval, asm)))

		        (Istate.ScrState (E,l,a,scval,scsaf,b), ctxt'') (pp,Res) pt;

       in ("ok", ([(Tactic.Check_Postcond pI, Tactic.Check_Postcond'(pI, (scval, asm)),

  	      ((pp, Res), (Istate.ScrState (E, l, a, scval, scsaf, b), ctxt'')))], ps, (pt, (p, p_)))) end

     end

  | solve (_, Tactic.End_Proof'') (pt, (p, p_)) =

    ("end-proof", ([(Tactic.Empty_Tac, Tactic.Empty_Tac_, (([], Res), (Istate.Uistate, Selem.e_ctxt)))], [], (pt, (p, p_))))

  | solve (_, 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

    (* ======= general case ======= *)

  | solve (_, m) (pt, po as (p, p_)) =

    if Celem.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 (Celem.assoc_thy (get_obj g_domID pt (par_pblobj pt p))) 

		      m (Istate.e_istate, ctxt) (p, p_) pt;

	    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) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;

	    in

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

	        LucinNEW.Safe_Step (cstate, istate, ctxt, tac) =>

		        ("ok", ([(Lucin.tac_2tac tac, tac, (snd cstate, (istate, ctxt)))], [(*ctree NOT cut*)], cstate))

	      | LucinNEW.Unsafe_Step (cstate, istate, ctxt, tac) =>

		        ("ok", ([(Lucin.tac_2tac tac, tac, (snd cstate, (istate, ctxt)))], [(*ctree NOT cut*)], cstate))

	      | _ => (* NotLocatable *)

	        let 

	          val (p,ps, _, pt) = Generate.generate_hard (Celem.assoc_thy "Isac") m (p, p_) pt;

	        in

	          ("not-found-in-script", ([(Lucin.tac_2tac m, m, (po, is))], ps, (pt, p)))

          end

	    end;

(* says how may steps of a calculation should be done by "fun autocalc"

   FIXXXME040624: does NOT match interfaces/ITOCalc.java

   TODO.WN0512 redesign togehter with autocalc ?                     *)

datatype auto = 

  Step of int      (*1 do #int steps (may stop in model/specify)

                       IS VERY INEFFICIENT IN MODEL/SPECIY                    *)

| CompleteModel    (*2 complete modeling

                       if model complete, finish specifying                   *)

| CompleteCalcHead (*3 complete model/specify in one go                       *)

| CompleteToSubpbl (*4 stop at the next begin of a subproblem,

                       if none, complete the actual (sub)problem              *)

| CompleteSubpbl   (*5 complete the actual (sub)problem (incl.ev.subproblems) *)

| CompleteCalc;    (*6 complete the calculation as a whole                    *)

fun autoord (Step _ ) = 1

  | autoord CompleteModel = 2

  | autoord CompleteCalcHead = 3

  | autoord CompleteToSubpbl = 4

  | autoord CompleteSubpbl = 5

  | autoord CompleteCalc = 6;

fun complete_solve auto c (ptp as (_, p as (_, p_))) =

    if p = ([], Res)

    then ("end-of-calculation", [], ptp)

    else

      if member op = [Pbl,Met] p_

      then

        let

          val ptp = Chead.all_modspec ptp

	        val (_, c', ptp) = all_solve auto c ptp

	      in complete_solve auto (c @ c') ptp end

      else

        case LucinNEW.do_solve_step ptp of

	        ((Tactic.Subproblem _, _, _) :: _, c', ptp') =>

	          if autoord auto < 5

            then ("ok", c @ c', ptp)

	          else

              let

                val ptp = Chead.all_modspec ptp'

	             val (_, c'', ptp) = all_solve auto (c @ c') ptp

	           in complete_solve auto (c @ c'@ c'') ptp end

	      | ((Tactic.Check_Postcond _, _, _) :: _, c', ptp' as (_, p')) =>

	        if autoord auto < 6 orelse p' = ([], Res)

          then ("ok", c @ c', ptp')

	        else complete_solve auto (c @ c') ptp'

	      | ((Tactic.End_Detail, _, _) :: _, c', ptp') => 

	        if autoord auto < 6

          then ("ok", c @ c', ptp')

	        else complete_solve auto (c @ c') ptp'

	      | (_, c', ptp') => complete_solve auto (c @ c') ptp'

and all_solve auto c (ptp as (pt, pos as (p,_)): ctree * pos') = 

    let

      val (_, _, mI) = get_obj g_spec pt p

      val ctxt = get_ctxt pt pos

      val (_, c', ptp) = LucinNEW.begin_end_prog (Tactic.Apply_Method' (mI, NONE, Istate.e_istate, ctxt)) (Istate.e_istate, ctxt) ptp

    in

      complete_solve auto (c @ c') ptp

    end;

(* aux.fun for detailrls with Rrls, reverse rewriting *)

fun rul_terms_2nds _ nds _ [] = nds

  | rul_terms_2nds thy nds t ((rule, res as (t', _)) :: rts) =

    (append_atomic [] (Istate.e_istate, Selem.e_ctxt) t (Tactic.rule2tac thy [] rule) res Complete EmptyPtree) ::

      (rul_terms_2nds thy nds t' rts);

(* detail steps done internally by Rewrite_Set* into ctree by use of a script *)

fun detailrls pt (pos as (p, _)) = 

  let

    val t = get_obj g_form pt p

	  val tac = get_obj g_tac pt p

	  val rls = (assoc_rls o Tactic.rls_of) tac

    val ctxt = get_ctxt pt pos

  in

    case rls of

	    Rule.Rrls {scr = Rule.Rfuns {init_state, ...}, ...} => 

	    let

        val (_, _, _, rul_terms) = init_state t

	      val newnds = rul_terms_2nds (Proof_Context.theory_of ctxt) [] t rul_terms

	      val pt''' = ins_chn newnds pt p 

	    in ("detailrls", pt''', (p @ [length newnds], Res)) end

	  | _ =>

	    let

        val is = Generate.init_istate tac t

	      (*TODO.WN060602 ScrState (["(t_, Problem (Isac,[equation,univar]))"]

			    is wrong for simpl, but working ?!? *)

	      val tac_ = Tactic.Apply_Method' (Celem.e_metID(*WN0402: see generate1 !?!*), SOME t, is, ctxt)

	      val pos' = ((lev_on o lev_dn) p, Frm)

	      val thy = Celem.assoc_thy "Isac"

	      val (_, _, _, pt') = Generate.generate1 thy tac_ (is, ctxt) pos' pt (* implicit Take *)

	      val (_,_, (pt'', _)) = complete_solve CompleteSubpbl [] (pt', pos')

	      val newnds = children (get_nd pt'' p)

	      val pt''' = ins_chn newnds pt p (*complete_solve cuts branches after*)

	    in ("detailrls", pt''', (p @ [length newnds], Res)) end

  end;

fun get_form (mI, m) (p,p_) pt = 

  case Applicable.applicable_in (p, p_) pt m of

    Chead.Notappl e => Generate.Error' e

  | Chead.Appl m => 

      if member op = specsteps mI

      then

        let val (_, _, f, _, _, _) = Chead.specify m (p, p_) [] pt

        in f end

      else Generate.EmptyMout;

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

  let

    val ctxt = get_ctxt pt pos (*see TODO.thy*)

  in

    case TermC.parse (Celem.assoc_thy "Isac") istr of

      NONE => ("syntax error in '" ^ istr ^ "'", Chead.e_calcstate' (*TODO: previous cs'*))

    | 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", next_cs) (* ctree not cut with replaceFormula *)

        else

          case Inform.cas_input f_in of

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

			    | NONE => (*/-------------------------------------- NEW fun locate_input_formula------*)

            let

       (*NEW*)val (_, _, metID) = get_obj g_spec pt (par_pblobj pt p)

       (*NEW*)val {scr = prog, ...} = Specify.get_met metID

       (*NEW*)val istate = get_istate pt pos

       (*NEW*)val ctxt = get_ctxt pt pos

            in

              case LucinNEW.locate_input_formula prog (pt, pos) istate ctxt f_in of

                LucinNEW.Step (cstate, _(*istate*), _(*ctxt*)) =>

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

              | LucinNEW.Not_Derivable calcstate' =>

                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 = case Ctree.get_istate pt pos of

              		    Istate.ScrState (env, _, _, _, _, _) => env

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

            		in

            		  case Inform.check_error_patterns (f_pred, f_in) (prog, env) (errpats, nrls) of

            		    SOME errpatID => ("error pattern #" ^ errpatID ^ "#", calcstate')

            		  | NONE => ("no derivation found", calcstate')

                end

            end

      end

  end

end