(* Title:  700-interSteps.sml

   Author: Walther Neuper 1105

   (c) copyright due to lincense terms.

*)

"----------- Minisubplb/700-interSteps.sml -----------------------";

"----------- Minisubplb/700-interSteps.sml -----------------------";

"----------- Minisubplb/700-interSteps.sml -----------------------";

(** adaption from rewtools.sml --- initContext..Thy_, fun context_thm ---,

  *into a functional representation, i.e. we outcomment statements with side-effects:

 ** reset_states ();

 ** CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], 

 **   ("Test", ["sqroot-test","univariate","equation","test"],

 **    ["Test","squ-equ-test-subpbl1"]))];

 ** Iterator 1; moveActiveRoot 1;

 ** autoCalculate 1 CompleteCalc;

 **)

val (p,_,f,nxt,_,pt) = CalcTreeTEST [(["equality (x+1=(2::real))", "solveFor x","solutions L"],

  ("Test", ["sqroot-test","univariate","equation","test"],

   ["Test","squ-equ-test-subpbl1"]))];

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Subproblem"*)

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

(*+*)if p = ([], Res)

(*+*)then case nxt of End_Proof' => ()

(*+*)  | _ => error "calculation not finished correctly 1"

(*+*)else error "calculation not finished correctly 2";

(*+*)show_pt pt; (* 11 lines with subpbl *)

"----- no thy-context at result -----";

(** val p = ([], Res);

 ** initContext 1 Thy_ p

 ***  = <MESSAGE><CALCID>1</CALCID><STRING>no thy-context at result</STRING></MESSAGE>: XML.tree;

 ** val ((pt,_),_) = get_calc 1;  (* 11 lines with subpbl *)

 **

 ** interSteps 1 ([2], Res); (* added [2,1]..[2,6] *)

 **)

"~~~~~ fun interSteps, args:"; val (cI, ip) = (1, ([2], Res));

(** val ((pt, p), tacis) = get_calc cI;*)

val ip' = lev_pred' pt ip;

(*+*)ip = ([2], Res);

(*+*)ip' = ([1], Res);

(*+*)show_pt pt;                  (* 11 lines, as produced by autoCalculate CompleteCalc *)

val ("detailrls", pt''''', _) = (*case*) Detail_Step.go pt ip (*of*);

(*+*)show_pt pt''''';                  (* added [2,1]..[2,6] after ([1], Res)*)

(*//-------------------------- 1. go down along calls to error ------------------------------\\*)

"~~~~~ fun go , args:"; val (pt, (pos as (p, _))) = (pt, ip);

(*+*)p = [2];

(*+*)pos = ([2], Res);

    val nd = Ctree.get_nd pt p

    val cn = Ctree.children nd

;

    (*if*) null cn (*then*);

      (*if*) (Tactic.is_rewset o (Ctree.get_obj Ctree.g_tac nd)) [(*root of nd*)] (*then*);

     Detail_Step.detailrls pt pos;

"~~~~~ fun detailrls , args:"; val (pt, (pos as (p, _))) = (pt, pos);

    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

  val _ = (*case*) rls (*of*);

        val is = Generate.init_istate tac t

(*+*)val Rule_Set.Repeat {scr = EmptyProg, ...} = rls; (*this prog is replaced by Auto_Prog.gen on the fly*)

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

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

	      val thy = ThyC.get_theory "Isac_Knowledge"

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

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

           complete_solve CompleteSubpbl [] (pt', pos');

"~~~~~ fun complete_solve , args:"; val (auto, c, (ptp as (_, p as (_, p_))))

  = (CompleteSubpbl, [], (pt', pos'));

    (*if*) p = ([], Res) (*else*);

      (*if*) member op = [Pbl,Met] p_ (*else*);

   val (_, ([(Rewrite ("radd_commute", _), _, _)], c', ptp')) =

      (*case*) Step_Solve.do_next ptp (*of*);

(*+*)c' = [([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), ([3, 2], Res), ([3], Res), ([4], Res), ([], Res)];

(*+*)show_pt (fst ptp');(*[

(([], Frm), solve (x + 1 = 2, x)),

(([1], Frm), x + 1 = 2),

(([1], Res), x + 1 + -1 * 2 = 0),

(([2,1], Frm), x + 1 + -1 * 2 = 0),

(([2,1], Res), 1 + x + -1 * 2 = 0)]*)

(*+*)val (keep_c', keep_ptp') = (c', ptp');

"~~~~~ and Step_Solve.do_next , args:"; val () = ();

(*+*)(*STOPPED HERE:

  NOTE: prog.xxx found by LItool.resume_prog from  Rule_Set.Repeat {scr = Prog xxx, ...}*)

(*+*)val (c', ptp') = (keep_c', keep_ptp');

	   (** )val (_, c', ptp') =( **)

           complete_solve auto (c @ c') ptp';

"~~~~~ fun complete_solve , args:"; val (auto, c, (ptp as (_, p as (_, p_))))

  = (auto, (c @ c'), ptp');

    (*if*) p = ([], Res) (*else*);

      (*if*) member op = [Pbl,Met] p_ (*else*);

   val (_, ([(Rewrite ("add.assoc", _), _, _)], c', ptp')) = (*case*)Step_Solve.do_next ptp (*of*);

"~~~~~ fun complete_solve , args:"; val (auto, c, (ptp as (_, p as (_, p_))))

  = (auto, (c @ c'), ptp');

    (*if*) p = ([], Res) (*else*);

      (*if*) member op = [Pbl,Met] p_ (*else*);

   val (_, ([(Calculate "TIMES", _, _)], c', ptp')) = (*case*)Step_Solve.do_next ptp (*of*);

show_pt (fst ptp');          (* added  [2,1]..[2,3], more to come *)

(*\\-------------------------- 1. go down along calls to error ------------------------------//*)

(**

 ** interSteps 1 ([3,1], Res);

 **)

"~~~~~ fun interSteps, args:"; val (cI, ip) = (1, ([3,1], Res));

(**val ((pt, p), tacis) = get_calc cI;*)

val ip' = lev_pred' pt ip;

(*+*)ip = ([3, 1], Res);

(*+*)ip' = ([3, 1], Frm);

val ("detailrls", pt, _) = (*case*) Detail_Step.go pt''''' ip (*of*);

show_pt pt;                  (* added ([3,1,1], Frm), ([3,1,1], Res) after ([3,1], Frm)*)

(*---------- final test ----------------------------------------------------------\\*)

if pr_ctree pr_short pt =

  ".    ----- pblobj -----\n1" ^

  ".   x + 1 = 2\n" ^

  "2.   x + 1 + -1 * 2 = 0\n" ^

  "2.1.   x + 1 + -1 * 2 = 0\n" ^

  "2.2.   1 + x + -1 * 2 = 0\n" ^

  "2.3.   1 + (x + -1 * 2) = 0\n" ^

  "2.4.   1 + (x + -2) = 0\n" ^

  "2.5.   1 + (-2 + x) = 0\n" ^

  "2.6.   -2 + (1 + x) = 0\n" ^

  "3.    ----- pblobj -----\n" ^

  "3.1.   -1 + x = 0\n" ^

  "3.1.1.   -1 + x = 0\n" ^

(*([3,1,1], Res), x = 0 + -1 * -1)       only shown by show_pt*)

  "3.2.   x = 0 + -1 * -1\n" ^(* another difference to show_pt*)

  "4.   [x = 1]\n"

(*".  [x = 1]"                           only shown by show_pt*)

then () else error "intermediate steps CHANGED";