intermed. ctxt ..: ctxt correct after Apply_Method in sub-method
this is checked in Minisubpbl/400-start-meth-subpbl.sml
1.1 --- a/src/Tools/isac/Interpret/script.sml Tue May 17 15:02:43 2011 +0200
1.2 +++ b/src/Tools/isac/Interpret/script.sml Tue May 17 17:38:35 2011 +0200
1.3 @@ -183,8 +183,7 @@
1.4 | get_t y (Const ("Script.Letpar",_) $ e1 $ Abs (_,_,e2)) a =
1.5 (case get_t y e1 a of NONE => get_t y e2 a | la => la)
1.6 (*| get_t y (Const ("HOL.Let",_) $ e1 $ Abs (_,_,e2)) a =
1.7 - (tracing("get_t: Let e1= "^(term2str e1)^", e2= "^(term2str e2));
1.8 - case get_t y e1 a of NONE => get_t y e2 a | la => la)
1.9 + (case get_t y e1 a of NONE => get_t y e2 a | la => la)
1.10 | get_t y (Abs (_,_,e)) a = get_t y e a*)
1.11 | get_t y (Const ("HOL.Let",_) $ e1 $ Abs (_,_,e2)) a =
1.12 get_t y e1 a (*don't go deeper without evaluation !*)
1.13 @@ -1653,6 +1652,7 @@
1.14 (id, string_of_thmI thm), f,(e_term,[(*!?!8.6.03*)])),
1.15 (Uistate, ctxt), (e_term, Sundef))) (*next stac*)
1.16 end
1.17 +
1.18 | next_tac thy (ptp as (pt,pos as (p,_)):ptree * pos') (sc as Script (h $ body))
1.19 (ScrState (E,l,a,v,s,b), ctxt) =
1.20 let val ctxt = get_ctxt pt pos
1.21 @@ -1673,11 +1673,12 @@
1.22 | Appy (m', scrst as (_,_,_,v,_,_)) =>
1.23 (m', (ScrState scrst, ctxt), (v, Sundef))) (*next stac*)
1.24 end
1.25 +
1.26 | next_tac _ _ _ (is, _) = error ("next_tac: not impl for " ^ (istate2str is));
1.27
1.28
1.29 (*.create the initial interpreter state from the items of the guard.*)
1.30 -fun init_scrstate thy itms metID =
1.31 +fun init_scrstate thy itms metID =(*FIXME.WN170511: delete ctxt from value*)
1.32 let
1.33 val actuals = itms2args thy metID itms;
1.34 val scr as Script sc = (#scr o get_met) metID;
2.1 --- a/src/Tools/isac/Interpret/solve.sml Tue May 17 15:02:43 2011 +0200
2.2 +++ b/src/Tools/isac/Interpret/solve.sml Tue May 17 17:38:35 2011 +0200
2.3 @@ -143,45 +143,36 @@
2.4 val (("Apply_Method",Apply_Method' (mI,_,_)),pt, pos as (p,_))=(m,pt, pos);
2.5 *)
2.6 fun solve ("Apply_Method", m as Apply_Method' (mI, _, _, _)) (pt:ptree, (pos as (p,_))) =
2.7 - let val {srls, ...} = get_met mI;
2.8 - val PblObj {meth=itms, ...} = get_obj I pt p;
2.9 - val thy' = get_obj g_domID pt p;
2.10 - val thy = assoc_thy thy';
2.11 - val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI;
2.12 - val ini = init_form thy sc env;
2.13 - val p = lev_dn p;
2.14 - in
2.15 - case ini of
2.16 - SOME t => (* val SOME t = ini;
2.17 - *)
2.18 - let val (pos,c,_,pt) =
2.19 - generate1 thy (Apply_Method' (mI, SOME t, is, ctxt))
2.20 - (is, ctxt) (lev_on p, Frm)(*implicit Take*) pt;
2.21 - in ("ok",([(Apply_Method mI, Apply_Method' (mI, SOME t, is, ctxt),
2.22 - ((lev_on p, Frm), (is, ctxt)))], c, (pt,pos)):calcstate')
2.23 - end
2.24 - | NONE => (*execute the first tac in the Script, compare solve m*)
2.25 - let val (m', (is', ctxt'), _) = next_tac (thy', srls) (pt, (p, Res)) sc (is, ctxt);
2.26 - val d = e_rls (*FIXME: get simplifier from domID*);
2.27 - in
2.28 - case locate_gen (thy',srls) m' (pt,(p, Res))(sc,d) (is', ctxt') of
2.29 - Steps (is'', ss as (m'',f',pt',p',c')::_) =>
2.30 -(* val Steps (is'', ss as (m'',f',pt',p',c')::_) =
2.31 - locate_gen (thy',srls) m' (pt,(p,Res)) (sc,d) is';
2.32 - *)
2.33 - ("ok", (map step2taci ss, c', (pt',p')))
2.34 - | NotLocatable =>
2.35 - let val (p,ps,f,pt) =
2.36 - generate_hard (assoc_thy "Isac") m (p,Frm) pt;
2.37 - in ("not-found-in-script",
2.38 - ([(tac_2tac m, m, (pos, (is, ctxt)))], ps, (pt,p))) end
2.39 - (*just-before------------------------------------------------------
2.40 - ("ok",([(Apply_Method mI,Apply_Method'(mI,NONE,e_istate),
2.41 - (pos, is))],
2.42 - [], (update_env pt (fst pos) (SOME is),pos)))
2.43 - -----------------------------------------------------------------*)
2.44 - end
2.45 - end
2.46 + let val {srls, ...} = get_met mI;
2.47 + val PblObj {meth=itms, ctxt, ...} = get_obj I pt p;
2.48 + val thy' = get_obj g_domID pt p;
2.49 + val thy = assoc_thy thy';
2.50 + val (is as ScrState (env,_,_,_,_,_), _, sc) = init_scrstate thy itms mI;
2.51 + val ini = init_form thy sc env;
2.52 + val p = lev_dn p;
2.53 + in
2.54 + case ini of
2.55 + SOME t =>
2.56 + let val (pos,c,_,pt) =
2.57 + generate1 thy (Apply_Method' (mI, SOME t, is, ctxt))
2.58 + (is, ctxt) (lev_on p, Frm)(*implicit Take*) pt;
2.59 + in ("ok",([(Apply_Method mI, Apply_Method' (mI, SOME t, is, ctxt),
2.60 + ((lev_on p, Frm), (is, ctxt)))], c, (pt,pos)):calcstate')
2.61 + end
2.62 + | NONE => (*execute the first tac in the Script, compare solve m*)
2.63 + let
2.64 + val (m', (is', ctxt'), _) = next_tac (thy', srls) (pt, (p, Res)) sc (is, ctxt);
2.65 + val d = e_rls (*FIXME: get simplifier from domID*);
2.66 + in
2.67 + case locate_gen (thy',srls) m' (pt,(p, Res))(sc,d) (is', ctxt') of
2.68 + Steps (is'', ss as (m'',f',pt',p',c')::_) =>
2.69 + ("ok", (map step2taci ss, c', (pt',p')))
2.70 + | NotLocatable =>
2.71 + let val (p,ps,f,pt) =
2.72 + generate_hard (assoc_thy "Isac") m (p,Frm) pt;
2.73 + in ("not-found-in-script", ([(tac_2tac m, m, (pos, (is, ctxt)))], ps, (pt,p))) end
2.74 + end
2.75 + end
2.76
2.77 | solve ("Free_Solve", Free_Solve') (pt,po as (p,_)) =
2.78 let (*val _=tracing"###solve Free_Solve";*)
2.79 @@ -350,28 +341,16 @@
2.80 | nxt_solv (End_Proof'') _ ptp = ([], [], ptp)
2.81
2.82 | nxt_solv tac_ is (pt, pos as (p,p_)) =
2.83 -(* val (pt, pos as (p,p_)) = ptp;
2.84 - *)
2.85 - let val pos = case pos of
2.86 - (p, Met) => ((lev_on o lev_dn) p, Frm)(*begin script*)
2.87 - | (p, Res) => (lev_on p,Res) (*somewhere in script*)
2.88 - | _ => pos (*somewhere in script*)
2.89 - (*val _= tracing"### nxt_solv4 Apply_Method: stored is =";
2.90 - val _= tracing(istate2str is);*)
2.91 - val (pos',c,_,pt) = generate1 (assoc_thy "Isac") tac_ is pos pt;
2.92 - in ([(tac_2tac tac_, tac_, (pos,is))], c, (pt, pos')) end
2.93 + let
2.94 + val pos =
2.95 + case pos of
2.96 + (p, Met) => ((lev_on o lev_dn) p, Frm)(*begin script*)
2.97 + | (p, Res) => (lev_on p,Res) (*somewhere in script*)
2.98 + | _ => pos
2.99 + val (pos',c,_,pt) = generate1 (assoc_thy "Isac") tac_ is pos pt;
2.100 + in ([(tac_2tac tac_, tac_, (pos,is))], c, (pt, pos')) end
2.101
2.102 -
2.103 - (*(p,p_), (([],Res),Uistate,Empty_Tac_), EmptyMout, Empty_Tac, Safe, pt*)
2.104 -
2.105 -
2.106 -(*.find the next tac from the script, nxt_solv will update the ptree.*)
2.107 -(* val (ptp as (pt,pos as (p,p_))) = ptp';
2.108 - val (ptp as (pt, pos as (p,p_))) = ptp'';
2.109 - val (ptp as (pt, pos as (p,p_))) = ptp;
2.110 - val (ptp as (pt, pos as (p,p_))) = (pt,ip);
2.111 - val (ptp as (pt, pos as (p,p_))) = (pt, pos);
2.112 - *)
2.113 +(* find the next tac from the script, nxt_solv will update the ptree *)
2.114 and nxt_solve_ (ptp as (pt, pos as (p,p_))) =
2.115 if e_metID = get_obj g_metID pt (par_pblobj pt p)
2.116 then ([], [], (pt,(p,p_))):calcstate'
3.1 --- a/test/Tools/isac/Interpret/script.sml Tue May 17 15:02:43 2011 +0200
3.2 +++ b/test/Tools/isac/Interpret/script.sml Tue May 17 17:38:35 2011 +0200
3.3 @@ -1,10 +1,6 @@
3.4 -(* tests for ME/script.sml
3.5 - TODO.WN0509 collect typical tests from systest here !!!!!
3.6 - author: Walther Neuper 050908
3.7 +(* Title: test/../script.sml
3.8 + Author: Walther Neuper 050908
3.9 (c) copyright due to lincense terms.
3.10 -
3.11 -use"../smltest/ME/script.sml";
3.12 -use"script.sml";
3.13 *)
3.14 "-----------------------------------------------------------------";
3.15 "table of contents -----------------------------------------------";
3.16 @@ -307,9 +303,8 @@
3.17 val (pt, p) = case locatetac tac (pt,p) of
3.18 ("ok", (_, _, ptp)) => ptp | _ => error "script.sml locatetac";
3.19 "~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
3.20 -val pIopt = get_pblID (pt,ip);
3.21 +val pIopt = get_pblID (pt,ip); (*SOME ["linear", "univariate", "equation", "test"]*)
3.22 tacis; (*= []*)
3.23 -pIopt; (*= SOME ["sqroot-test", "univariate", ...]*)
3.24 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*)
3.25 "~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
3.26 (*WAS stac2tac_ TODO: no match for SubProblem*)
4.1 --- a/test/Tools/isac/Minisubpbl/000-comments.sml Tue May 17 15:02:43 2011 +0200
4.2 +++ b/test/Tools/isac/Minisubpbl/000-comments.sml Tue May 17 17:38:35 2011 +0200
4.3 @@ -15,5 +15,6 @@
4.4 200: start and execute the method of the rootproblem
4.5 300: initialisation of a subproblem from script and specify phase
4.6 400: start and execute the method of the subproblem
4.7 - 500: check postconditions of subproblem and rootproblem
4.8 + 500: shift interpretation from sub-method to root-method
4.9 + 600: check postconditions of subproblem and rootproblem
4.10 *)
5.1 --- a/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Tue May 17 15:02:43 2011 +0200
5.2 +++ b/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Tue May 17 17:38:35 2011 +0200
5.3 @@ -14,25 +14,57 @@
5.4 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.5 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.6 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.7 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "squ-equ-test-subpbl1"]*)
5.8 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.9 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.10 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subp ["linear", "univariate", "equation", "test"]*)
5.11 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.12 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Subproblem"*)
5.13 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.14 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.15 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.16 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.17 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.18 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.19 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.20 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.21 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst isolate_bdv*);
5.22 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*);
5.23 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["linear","univariate", ...]) *);
5.24 -(*-----nxt = ("Empty_Tac", Empty_Tac): tac'_
5.25 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_elementwise "Assumptions *);
5.26 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond["sqroot-test", "univariate", ...]) *);
5.27 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("End_Proof'" *);
5.28 ------*)
5.29 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*)
5.30 +get_ctxt pt p |> is_e_ctxt; (*false... OK: from specify, PblObj{ctxt,...}*)
5.31 +val ctxt = get_ctxt pt p;
5.32 +val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
5.33 +get_loc pt p |> snd |> is_e_ctxt; (*true ... OK: interpreter not yet started*)
5.34 +val (pt'',p'') = (pt, p);
5.35 +"~~~~~ fun me, args:"; val (_,tac) = nxt;
5.36 +"~~~~~ fun locatetac, args:"; val ptp as (pt, p) = (pt, p);
5.37 +val (mI,m) = mk_tac'_ tac;
5.38 +val Appl m = applicable_in p pt m;
5.39 +member op = specsteps mI; (*false*)
5.40 +"~~~~~ fun loc_solve_, args:"; val (m, (pt, pos) ) = ((mI, m), ptp);
5.41 +"~~~~~ fun solve, args:"; val (("Apply_Method", Apply_Method' (mI,_,_,_)), pos as (p,_)) = (m, pos);
5.42 +val {srls, ...} = get_met mI;
5.43 +val PblObj {meth=itms, ctxt, ...} = get_obj I pt p;
5.44 +val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
5.45 +val thy' = get_obj g_domID pt p;
5.46 +val thy = assoc_thy thy';
5.47 +val (is as ScrState (env,_,_,_,_,_), _, sc) = init_scrstate thy itms mI;
5.48 +(*dont take ctxt ^^^ from ^^^^^^^^^^^^^*)
5.49 +(*= the first part vvvvvvvvv works now =======================================*)
5.50 +val (pt, p) = case locatetac tac (pt'',p'') of
5.51 + ("ok", (_, _, ptp)) => ptp | _ => error "script.sml locatetac";
5.52 +val ctxt = get_ctxt pt p;
5.53 +val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
5.54 +(*= the first part ^^^^^^^^^^ works now =======================================*)
5.55 +val (pt'',p'') = (pt, p);
5.56 +"~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
5.57 +val pIopt = get_pblID (pt,ip);
5.58 +tacis; (*= []*)
5.59 +member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*)
5.60 +"~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
5.61 +val thy' = get_obj g_domID pt (par_pblobj pt p);
5.62 +val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
5.63 +"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt,(p,_)):ptree * pos'), (sc as Script (h $ body)),
5.64 + (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
5.65 +val ctxt = get_ctxt pt pos;
5.66 +val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
5.67 +(*= the first part ^^^^^^^^^^ works now =======================================*)
5.68 +l = [];
5.69 +appy thy ptp E [R] body NONE v;
5.70 +val (p,_,f,nxt,_,pt) = me nxt p'' [] pt''; (*nxt = Rewrite_Set_Inst isolate_bdv*);
5.71
5.72 -
6.1 --- a/test/Tools/isac/Test_Isac.thy Tue May 17 15:02:43 2011 +0200
6.2 +++ b/test/Tools/isac/Test_Isac.thy Tue May 17 17:38:35 2011 +0200
6.3 @@ -101,48 +101,6 @@
6.4 use "Minisubpbl/400-start-meth-subpbl.sml"
6.5 use "Minisubpbl/500-met-sub-to-root.sml"
6.6 use "Minisubpbl/600-postcond.sml"
6.7 -
6.8 -ML {*
6.9 -val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
6.10 -val (dI',pI',mI') =
6.11 - ("Test", ["sqroot-test","univariate","equation","test"],
6.12 - ["Test","squ-equ-test-subpbl1"]);
6.13 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.14 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.15 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.16 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.17 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.18 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.19 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.20 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.21 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.22 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.23 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Subproblem"*)
6.24 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.25 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.26 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.27 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.28 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.29 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.30 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.31 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.32 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst isolate_bdv*);
6.33 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*);
6.34 -*}
6.35 -ML {*
6.36 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["linear","univariate", ...]) *);
6.37 -*}
6.38 -ML {*
6.39 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.40 -*}
6.41 -ML {*
6.42 -*}
6.43 -ML {*
6.44 -*}
6.45 -ML {*
6.46 -*}
6.47 -
6.48 -
6.49 ML {*"%%%%%%%%%%%%%%%%% end Minisubpbl %%%%%%%%%%%%%%%%%%%%%%%";*}
6.50 ML {*"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";*}
6.51 use "Interpret/mstools.sml" (*new 2010*)
6.52 @@ -214,17 +172,71 @@
6.53 ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}
6.54
6.55 ML {*
6.56 -val am = [];
6.57 -insert_assumptions am
6.58 -*}
6.59 -ML {*
6.60 -val ctxt = get_ctxt pt p |> insert_assumptions am
6.61 -*}
6.62 -ML {*
6.63 -from_pblobj_or_detail'
6.64 -*}
6.65 -ML {*
6.66 -from_pblobj'
6.67 +(*Minisubpbl/500-met-sub-to-root.sml*)
6.68 +val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
6.69 +val (dI',pI',mI') =
6.70 + ("Test", ["sqroot-test","univariate","equation","test"],
6.71 + ["Test","squ-equ-test-subpbl1"]);
6.72 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.73 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.74 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.75 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.76 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.77 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.78 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.79 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "squ-equ-test-subpbl1"]*)
6.80 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.81 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.82 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subp ["linear", "univariate", "equation", "test"]*)
6.83 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.84 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.85 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.86 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.87 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.88 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.89 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.90 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*)
6.91 +get_ctxt pt p |> is_e_ctxt; (*false... OK: from specify, PblObj{ctxt,...}*)
6.92 +val ctxt = get_ctxt pt p;
6.93 +val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
6.94 +get_loc pt p |> snd |> is_e_ctxt; (*true ... OK: interpreter not yet started*)
6.95 +val (pt'',p'') = (pt, p);
6.96 +"~~~~~ fun me, args:"; val (_,tac) = nxt;
6.97 +"~~~~~ fun locatetac, args:"; val ptp as (pt, p) = (pt, p);
6.98 +val (mI,m) = mk_tac'_ tac;
6.99 +val Appl m = applicable_in p pt m;
6.100 +member op = specsteps mI; (*false*)
6.101 +"~~~~~ fun loc_solve_, args:"; val (m, (pt, pos) ) = ((mI, m), ptp);
6.102 +"~~~~~ fun solve, args:"; val (("Apply_Method", Apply_Method' (mI,_,_,_)), pos as (p,_)) = (m, pos);
6.103 +val {srls, ...} = get_met mI;
6.104 +val PblObj {meth=itms, ctxt, ...} = get_obj I pt p;
6.105 +val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
6.106 +val thy' = get_obj g_domID pt p;
6.107 +val thy = assoc_thy thy';
6.108 +val (is as ScrState (env,_,_,_,_,_), _, sc) = init_scrstate thy itms mI;
6.109 +(*dont take ctxt ^^^ from ^^^^^^^^^^^^^*)
6.110 +(*= the first part vvvvvvvvv works now =======================================*)
6.111 +val (pt, p) = case locatetac tac (pt'',p'') of
6.112 + ("ok", (_, _, ptp)) => ptp | _ => error "script.sml locatetac";
6.113 +val ctxt = get_ctxt pt p;
6.114 +val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
6.115 +(*= the first part ^^^^^^^^^^ works now =======================================*)
6.116 +val (pt'',p'') = (pt, p);
6.117 +"~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
6.118 +val pIopt = get_pblID (pt,ip);
6.119 +tacis; (*= []*)
6.120 +member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*)
6.121 +"~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
6.122 +val thy' = get_obj g_domID pt (par_pblobj pt p);
6.123 +val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
6.124 +"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt,(p,_)):ptree * pos'), (sc as Script (h $ body)),
6.125 + (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
6.126 +val ctxt = get_ctxt pt pos;
6.127 +val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
6.128 +(*= the first part ^^^^^^^^^^ works now =======================================*)
6.129 +l = [];
6.130 +appy thy ptp E [R] body NONE v;
6.131 +val (p,_,f,nxt,_,pt) = me nxt p'' [] pt''; (*nxt = Rewrite_Set_Inst isolate_bdv*);
6.132 *}
6.133 ML {*
6.134 *}
6.135 @@ -236,6 +248,41 @@
6.136 *}
6.137 ML {*
6.138 *}
6.139 +ML {*
6.140 +*}
6.141 +ML {*
6.142 +get_ctxt pt p |> is_e_ctxt; (*true ...?!?*)
6.143 +get_loc pt p |> snd |> is_e_ctxt; (*true ...?!?*)
6.144 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*);
6.145 +*}
6.146 +ML {*
6.147 +get_ctxt pt p |> is_e_ctxt; (*true ...?!?*)
6.148 +get_loc pt p |> snd |> is_e_ctxt; (*true ...?!?*)
6.149 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["linear","univariate", ...]) *);
6.150 +*}
6.151 +ML {*
6.152 +"~~~~~ fun me, args:"; val (_,tac) = nxt;
6.153 +val (pt, p) = case locatetac tac (pt,p) of
6.154 + ("ok", (_, _, ptp)) => ptp | _ => error "script.sml locatetac";
6.155 +show_pt pt; (*...(([3], Res), [x = 1])]... back in root, OK *)
6.156 +"~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
6.157 +val pIopt = get_pblID (pt,ip); (*= SOME ["sqroot-test", "univariate", ...]*)
6.158 +tacis; (*= []*)
6.159 +member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*)
6.160 +"~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
6.161 +val thy' = get_obj g_domID pt (par_pblobj pt p);
6.162 +val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*)
6.163 +"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt,(p,_)):ptree * pos'), (sc as Script (h $ body)),
6.164 + (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
6.165 +l; (*= [R, R, D, L, R]*)
6.166 +"~~~~~ dont like to go into nstep_up...";
6.167 +*}
6.168 +ML {*
6.169 +*}
6.170 +
6.171 +
6.172 +ML {*
6.173 +*}
6.174
6.175 end
6.176