neuper@41985: (* Title:  400-start-meth-subpbl.sml
neuper@41985:    Author: Walther Neuper 1105
neuper@41985:    (c) copyright due to lincense terms.
neuper@41985: *)
neuper@41985: 
neuper@42020: "----------- Minisubplb/400-start-meth-subpbl.sml ----------------";
neuper@42020: "----------- Minisubplb/400-start-meth-subpbl.sml ----------------";
neuper@42020: "----------- Minisubplb/400-start-meth-subpbl.sml ----------------";
neuper@41985: val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
neuper@41985: val (dI',pI',mI') =
neuper@41990:    ("Test", ["sqroot-test","univariate","equation","test"],
neuper@41990:     ["Test","squ-equ-test-subpbl1"]);
neuper@41985: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@41985: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@41990: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@41990: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@41990: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@41990: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@41990: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@41999: val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "squ-equ-test-subpbl1"]*)
neuper@41990: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@41990: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@55279: val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subp ["LINEAR", "univariate", "equation", "test"]*)
neuper@41990: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@41990: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@41990: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@41990: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@41990: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@41990: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@41990: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@41999: val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*)
neuper@41999: get_ctxt pt p |> is_e_ctxt;       (*false... OK: from specify, PblObj{ctxt,...}*)
neuper@41999: val ctxt = get_ctxt pt p;
neuper@41999: val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
neuper@41999: get_loc pt p |> snd |> is_e_ctxt; (*true ... OK: interpreter not yet started*)
neuper@42020: 
neuper@41999: val (pt'',p'') = (pt, p);
neuper@41999: "~~~~~ fun me, args:"; val (_,tac) = nxt;
neuper@41999: "~~~~~ fun locatetac, args:"; val ptp as (pt, p) = (pt, p);
neuper@41999: val (mI,m) = mk_tac'_ tac;
neuper@41999: val Appl m = applicable_in p pt m;
neuper@41999: member op = specsteps mI; (*false*)
neuper@41999: "~~~~~ fun loc_solve_, args:"; val (m, (pt, pos) ) = ((mI, m), ptp);
neuper@41999: "~~~~~ fun solve, args:"; val (("Apply_Method", Apply_Method' (mI,_,_,_)), pos as (p,_)) = (m, pos);
neuper@41999: val {srls, ...} = get_met mI;
neuper@42019: val PblObj {meth=itms, ...} = get_obj I pt p;
neuper@41999: val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
neuper@41999: val thy' = get_obj g_domID pt p;
neuper@41999: val thy = assoc_thy thy';
neuper@42019: val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI;
neuper@41999: (*dont take ctxt                   ^^^ from   ^^^^^^^^^^^^^*)
neuper@41999: (*= the first part vvvvvvvvv works now =======================================*)
neuper@41999: val (pt, p) = case locatetac tac (pt'',p'') of
neuper@41999: 	("ok", (_, _, ptp))  => ptp | _ => error "script.sml locatetac";
neuper@41999: val ctxt = get_ctxt pt p;
neuper@41999: val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
neuper@41999: (*= the first part ^^^^^^^^^^ works now =======================================*)
neuper@42020: 
neuper@41999: val (pt'',p'') = (pt, p);
neuper@41999: "~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
neuper@41999: val pIopt = get_pblID (pt,ip);
neuper@41999: tacis; (*= []*)
neuper@41999: member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*)
neuper@41999: "~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
neuper@41999: val thy' = get_obj g_domID pt (par_pblobj pt p);
neuper@41999: val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
wneuper@59279: "~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt,(p,_)):ctree * pos'), (sc as Prog (h $ body)), 
neuper@41999: 	                               (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
neuper@41999: val ctxt = get_ctxt pt pos;
neuper@41999: val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
neuper@41999: (*= the first part ^^^^^^^^^^ works now =======================================*)
neuper@41999: l = [];
neuper@41999: appy thy ptp E [R] body NONE v;
neuper@41999: val (p,_,f,nxt,_,pt) = me nxt p'' [] pt''; (*nxt = Rewrite_Set_Inst isolate_bdv*);
neuper@41990: