(* 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 | Steps of int

   val autoord : auto -> int

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

   (*NONE*)

 (*/-------------------------------------------------------- ! 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;

 open Pos

 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"];

 (* tell 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 = 

   Steps 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 (Steps _ ) = 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.by_tactic (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, ContextC.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 Pstate (["(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_Knowledge"

 	      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 inform (next_cs as (_, _, (pt, pos as (p, _))): Chead.calcstate') istr =

   case TermC.parse (Celem.assoc_thy "Isac_Knowledge") 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, Pos.Met))))

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

           let

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

             val {scr = prog, ...} = Specify.get_met metID

             val istate = get_istate pt pos

             val ctxt = get_ctxt pt pos

           in

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

               LucinNEW.Found_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, ...} = Ctree.get_istate pt pos |> Istate.the_pstate

           		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