(* Title:  "Minisubpbl/200-start-method-NEXT_STEP.sml"

   Author: Walther Neuper 1105

   (c) copyright due to lincense terms.

*)

"----------- Minisubplb/200-start-method-NEXT_STEP.sml ---------------------------------------";

"----------- Minisubplb/200-start-method-NEXT_STEP.sml ---------------------------------------";

"----------- Minisubplb/200-start-method-NEXT_STEP.sml ---------------------------------------";

val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];

val (dI',pI',mI') =

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

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

val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Model_Problem*)

(*rewrite__set_ called with 'Rule_Set.Empty' for 'precond_rootpbl x'*)

(*[], Pbl*)val (_, ([(tac''''', _, _)], _, (pt''''', p'''''))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Theory*)

(*/--------- step into Specify_Theory --------------------------------------------------------\*)

"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, e_pos'), []));

    val pIopt = Ctree.get_pblID (pt, ip);

    (*if*) ip = ([], Pos.Res) (*else*);

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

      val SOME _ = (*case*) pIopt (*of*);

(*rewrite__set_ called with 'Rule_Set.Empty' for 'precond_rootpbl x'*)

           switch_specify_solve p_ (pt, ip);

"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));

      (*if*) member op = [Pos.Pbl, Pos.Met] state_pos (*then*);

(*rewrite__set_ called with 'Rule_Set.Empty' for 'precond_rootpbl x'*)

           specify_do_next (pt, input_pos);

"~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);

(*rewrite__set_ called with 'Rule_Set.Empty' for 'precond_rootpbl x'*)

    val (_, (_, _)) =

Specify.find_next_step ptp;

"~~~~~ fun find_next_step , args:"; val (pt, (p, p_)) = ptp;

    val (pblobj, met, origin, oris, dI', pI', mI', pbl, dI, pI, mI) = 

  	  case Ctree.get_obj I pt p of

  	    pblobj as (Ctree.PblObj {meth, origin = origin as (oris, (dI', pI', mI'), _),

  		  probl, spec = (dI, pI, mI), ...}) => (pblobj, meth, origin, oris, dI', pI', mI', probl, dI, pI, mI)

      | Ctree.PrfObj _ => error "nxt_specify_: not on PrfObj";

    (*if*) Ctree.just_created_ pblobj (*by Subproblem*) andalso origin <> Ctree.e_origin (*else*);

        val cpI = if pI = Problem.id_empty then pI' else pI;

  	    val cmI = if mI = Method.id_empty then mI' else mI;

  	    val {ppc = pbt, prls, where_, ...} = Problem.from_store cpI;

(*+* )------- in f3cac3053e7b (Rule_Set.empty just renamed, NOT deleted) we had

(*+*)  prls =

(*+*)    Rule_Set.Repeat {calc = [], erls = Rule_Set.Empty, errpatts = [], id = "empty", preconds = [], rew_ord =

(*+*)      ("dummy_ord", fn), rules = [], scr = Empty_Prog, srls = Rule_Set.Empty}:

(*+*).. THIS IS Rule_Set.empty, BUT IT DID not CAUSE ANY ERROR !

(*+*)------- WITH Rule_Set.empty REMOVED (based on f3cac3053e7b) we had

(*+*)val Empty = prls (* <---ERROR: rewrite__set_ called with 'Rule_Set.Empty' for 'precond_rootpbl x' *)

( *+*)val ["sqroot-test", "univariate", "equation", "test"] = cpI

(*\--------- step into Specify_Theory --------------------------------------------------------/*)

(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p''''' ((pt''''', e_pos'), []);(*Specify_Problem ["sqroot-test", "univariate", "equation", "test"*)

(*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Method ["Test", "squ-equ-test-subpbl1"]*)

(*[1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Apply_Method ["Test", "squ-equ-test-subpbl1"]*)

(*[1], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Rewrite_Set "norm_equation"*)

(*[2], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Rewrite_Set "Test_simplify"*)

(*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(* Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*)

(*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Model_Problem*)

(*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Theory "Test"*)

(*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Problem ["LINEAR", "univariate", "equation", "test"]*)

(*[3], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Method ["Test", "solve_linear"]*)

(*[3, 1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Apply_Method ["Test", "solve_linear"]*)

(*[3, 1], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv")*)

val  Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv") = tac;

if p = ([3, 1], Res) andalso (get_obj g_res pt (fst p) |> UnparseC.term) = "x = 0 + -1 * -1"

then case tac of Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv") => ()

  | _ => error "Minisubplb/200-start-method-NEXT_STEP.sml CHANGED 1"

else error "Minisubplb/200-start-method-NEXT_STEP.sml CHANGED 2"