(* Title:  "Minisubplb/400-start-meth-subpbl.sml"

   Author: Walther Neuper 1105

   (c) copyright due to lincense terms.

*)

"----------- Minisubpbl/400-start-meth-subpbl.sml ----------------";

"----------- Minisubpbl/400-start-meth-subpbl.sml ----------------";

"----------- Minisubpbl/400-start-meth-subpbl.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'))];

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 = Apply_Method ["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; (*nxt = Subp ["LINEAR", "univariate", "equation", "test"]*)

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 = Apply_Method ["Test", "solve_linear"]*)

(*//--1 begin step into relevant call ---------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^-------\\

      1 relevant for all Apply_Method                                                           *)

(*+*)if get_ctxt pt p |> is_e_ctxt then error "ctxt no initialised by specify, PblObj{ctxt,...}" else ();

(*+*)if get_ctxt pt p |> is_e_ctxt then error "ctxt NOT initialised by Subproblem'}" else ();

(*+*)val SOME t = parseNEW (get_ctxt pt p) "Check_elementwise [x = 1] {(v_v::real). Assumptions}";

"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt''', p''', [], pt''');

  val ("ok", (_, _, (pt'''', p''''))) = (*case*)

       Step.by_tactic tac (pt, p) (*of*);

"~~~~~ fun Step.by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));

   val Appl m = (*case*) applicable_in p pt tac (*of*);

  (*if*) Tactic.for_specify' m; (*false*)

           loc_solve_ m ptp;

"~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos) ) = (m, ptp);

           Step_Solve.by_tactic m (pt, pos);

"~~~~~ fun Step_Solve.by_tactic , args:"; val (m as Tactic.Apply_Method' (mI, _, _, ctxt), (pt, (pos as (p, _))))

  = (m, (pt, pos));

      val itms = case get_obj I pt p of

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

      | _ => error "Step_Solve.by_tactic Apply_Method: uncovered case get_obj"

      val thy' = get_obj g_domID pt p;

      val thy = Celem.assoc_thy thy';

      val srls = LItool.get_simplifier (pt, pos)

      val (is, env, ctxt, sc) = case LItool.init_pstate srls ctxt itms mI of

        (is as Istate.Pstate {env, ...}, ctxt, sc) =>  (is, env, ctxt, sc)

      | _ => error "Step_Solve.by_tactic Apply_Method: uncovered case init_pstate"

(*+*)val (pt, p) = case Step.by_tactic tac (pt, pos) of

	("ok", (_, _, ptp))  => ptp | _ => error "script.sml Step.by_tactic";

(*+*)val SOME t = parseNEW (get_ctxt pt p) "Check_elementwise [x = 1] {(v_v::real). Assumptions}";

"~~~~~ from Step_Solve.by_tactic to..to me return"; val (pt, p) = (pt'''', p'''');

  val ("ok", ([(Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv"), _, (_, (Pstate _, _)))], _, _)) = (*case*)

           Step.do_next p ((pt, e_pos'), []) (*of*);

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

val pIopt = get_pblID (pt,ip);

tacis; (*= []*)

member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*)

"~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);

val thy' = get_obj g_domID pt (par_pblobj pt p);

val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;

"~~~~~ fun find_next_step , args:"; val ((thy, _), (ptp as (pt, (p, _))), sc, (Istate.Pstate ist, _(*ctxt*)))

  = ((thy',srls), (pt,pos), sc, is);

(*+*)val SOME t = parseNEW (get_ctxt pt pos) "Check_elementwise [x = 1] {(v_v::real). Assumptions}";

(*\\--1 end step into relevant call ----------------------------------------------------------//*)

val (p,_,f,nxt,_,pt) = me nxt''' p''' [] pt'''; (*nxt = Rewrite_Set_Inst isolate_bdv*);

if p = ([3, 1], Frm) andalso f2str f = "-1 + x = 0" andalso

  tac2str nxt = "Rewrite_Set_Inst ([(''bdv'', x)], \"isolate_bdv\")"

then () else error "Minisubpbl/400-start-meth-subpbl changed";