# HG changeset patch # User Walther Neuper # Date 1584541395 -3600 # Node ID edf1643edde581576f0e3bac8e81ec0b170397d8 # Parent 375177a58baa0e10855f0a47fe74089a60a27863 prep. cleanup LItool.resume_prog diff -r 375177a58baa -r edf1643edde5 src/Tools/isac/Interpret/li-tool.sml --- a/src/Tools/isac/Interpret/li-tool.sml Wed Mar 18 14:51:58 2020 +0100 +++ b/src/Tools/isac/Interpret/li-tool.sml Wed Mar 18 15:23:15 2020 +0100 @@ -17,8 +17,8 @@ val get_simplifier : Calc.T -> Rule.rls (*vvv initialise : Rule.theory'(*?!?*) -> Calc.T -> (Istate.T * Proof.context) * Program.T*) - val from_pblobj_or_detail' : Rule.theory' -> Ctree.pos' -> Ctree.ctree -> - Rule.rls(*..\ ist \ REMOVE*) * (Istate.T * Proof.context) * Program.T + val resume_prog : Rule.theory' -> Ctree.pos' -> Ctree.ctree -> + (Istate.T * Proof.context) * Program.T val tac_from_prog : Ctree.ctree -> theory -> term -> Tactic.input val check_leaf : string -> Proof.context -> Rule.rls -> (Env.T * (term option * term)) -> term -> @@ -346,23 +346,23 @@ val {srls, ...} = Specify.get_met metID in srls end -(* decide, where to get program/istate from: +(* decide, where to get program/istate/ctxt from: (* 1 *) from PblObj: at begin of program if no init_form (* 2 *) from PblObj/PrfObj: if Prog_Tac is in the middle of the program (* 3 *) from PrfOb: in case of Math_Engine.detailstep *) -fun from_pblobj_or_detail' thy (p, p_) pt = +fun resume_prog thy (p, p_) pt = if Pos.on_specification p_ then case get_obj g_env (*!DEPRECATED!*) pt p of (* 1 *) - NONE => error "from_pblobj_or_detail': no istate" + NONE => error "resume_prog: no istate" | SOME (Istate.Pstate pst, ctxt) => let val metID = get_obj g_metID pt p val {srls, ...} = Specify.get_met metID in - (srls, (Istate.Pstate (Istate.set_eval srls pst), ctxt), (#scr o Specify.get_met) metID) + ((Istate.Pstate (Istate.set_eval srls pst), ctxt), (#scr o Specify.get_met) metID) end - | _ => raise ERROR "from_pblobj_or_detail': unexpected result from g_env" + | _ => raise ERROR "resume_prog: unexpected result from g_env" else let val (pbl, p', rls') = par_pbl_det pt p in if pbl @@ -373,11 +373,10 @@ val (is, ctxt) = case get_loc pt (p, p_) of (Istate.Pstate ist, ctxt) => (Istate.Pstate (Istate.set_eval srls ist), ctxt) - | _ => raise ERROR "from_pblobj_or_detail': unexpected result from get_loc" - in (srls, (is, ctxt), (#scr o Specify.get_met) metID) end + | _ => raise ERROR "resume_prog: unexpected result from get_loc" + in ((is, ctxt), (#scr o Specify.get_met) metID) end else (* 3 *) - (Rule.e_rls(*!!!*), - get_loc pt (p, p_), + (get_loc pt (p, p_), Rule.Prog (Auto_Prog.gen (Celem.assoc_thy thy) (get_last_formula (pt, (p, p_))) rls')) end diff -r 375177a58baa -r edf1643edde5 src/Tools/isac/Interpret/lucas-interpreter.sml --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Wed Mar 18 14:51:58 2020 +0100 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Wed Mar 18 15:23:15 2020 +0100 @@ -575,7 +575,7 @@ else let val thy' = get_obj g_domID pt (par_pblobj pt p); - val (_, (ist, ctxt), sc) = LItool.from_pblobj_or_detail' thy' (p,p_) pt; + val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt; in case find_next_step sc (pt, pos) ist ctxt of Next_Step (ist, ctxt, tac) => diff -r 375177a58baa -r edf1643edde5 src/Tools/isac/Interpret/step-solve.sml --- a/src/Tools/isac/Interpret/step-solve.sml Wed Mar 18 14:51:58 2020 +0100 +++ b/src/Tools/isac/Interpret/step-solve.sml Wed Mar 18 15:23:15 2020 +0100 @@ -104,7 +104,7 @@ else let val thy' = get_obj g_domID pt (par_pblobj pt p); - val (_, is, sc) = LItool.from_pblobj_or_detail' thy' (p,p_) pt; + val (is, sc) = LItool.resume_prog thy' (p,p_) pt; in case LI.locate_input_tactic sc (pt, po) (fst is) (snd is) m of LI.Safe_Step (istate, ctxt, tac) => diff -r 375177a58baa -r edf1643edde5 src/Tools/isac/MathEngBasic/istate-def.sml --- a/src/Tools/isac/MathEngBasic/istate-def.sml Wed Mar 18 14:51:58 2020 +0100 +++ b/src/Tools/isac/MathEngBasic/istate-def.sml Wed Mar 18 15:23:15 2020 +0100 @@ -67,7 +67,7 @@ topt2str form_arg ^ ", " ^ Rule.term2str act_arg ^ ", " ^ asap2str or ^ ", " ^ bool2str found_accept ^ ", " ^ bool2str assoc ^ ")"; -(* for handling type T see fun from_pblobj_or_detail', +? *) +(* for handling type T see fun resume_prog, +? *) datatype T = (*interpreter state*) Uistate (*undefined in modspec, in '_deriv'ation*) | Pstate of pstate (*for script interpreter*) diff -r 375177a58baa -r edf1643edde5 src/Tools/isac/ProgLang/Auto_Prog.thy --- a/src/Tools/isac/ProgLang/Auto_Prog.thy Wed Mar 18 14:51:58 2020 +0100 +++ b/src/Tools/isac/ProgLang/Auto_Prog.thy Wed Mar 18 15:23:15 2020 +0100 @@ -195,12 +195,12 @@ fun rules2scr_Rls thy rules = if contain_bdv rules - then FunID_Term_Bdv $ (Repeat $ (((#> o (map (rule2stac_inst thy))) rules) $ Rule.e_term)) - else FunID_Term $ (Repeat $ (((#> o (map (rule2stac thy))) rules) $ Rule.e_term)); + then FunID_Term_Bdv $ (Repeat $ (((op #> o (map (rule2stac_inst thy))) rules) $ Rule.e_term)) + else FunID_Term $ (Repeat $ (((op #> o (map (rule2stac thy))) rules) $ Rule.e_term)); fun rules2scr_Seq thy rules = if contain_bdv rules - then FunID_Term_Bdv $ (((#> o (map (rule2stac_inst thy))) rules) $ Rule.e_term) - else FunID_Term $ (((#> o (map (rule2stac thy))) rules) $ Rule.e_term); + then FunID_Term_Bdv $ (((op #> o (map (rule2stac_inst thy))) rules) $ Rule.e_term) + else FunID_Term $ (((op #> o (map (rule2stac thy))) rules) $ Rule.e_term); (* REPLACED BY Auto_Prog.gen: prepare the input for an rls for use: @@ -230,6 +230,7 @@ (* on the fly generate a Prog from an rls for Math_Engine.detailstep. Types are not precise, but these are not required by LI. + Argument "thy" is only required for lookup in KEStore. *) fun gen thy t rls = let diff -r 375177a58baa -r edf1643edde5 src/Tools/isac/TODO.thy --- a/src/Tools/isac/TODO.thy Wed Mar 18 14:51:58 2020 +0100 +++ b/src/Tools/isac/TODO.thy Wed Mar 18 15:23:15 2020 +0100 @@ -449,7 +449,6 @@ remove Rfuns -> Rule.Prog, Rule.EmptyScr consider separating spec.funs. to ?Inter_Steps? \begin{itemize} - \item removing from_pblobj_or_detail' causes many strange errors \item ^^^+ see from_pblobj_or_detail_thm, from_pblobj_or_detail_calc, ... \item xxx \item probably only "normal_form" seems to be needed diff -r 375177a58baa -r edf1643edde5 test/Tools/isac/BridgeLibisabelle/use-cases.sml --- a/test/Tools/isac/BridgeLibisabelle/use-cases.sml Wed Mar 18 14:51:58 2020 +0100 +++ b/test/Tools/isac/BridgeLibisabelle/use-cases.sml Wed Mar 18 15:23:15 2020 +0100 @@ -197,7 +197,7 @@ "~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, (pt, p)); (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p); (*else*) val thy' = get_obj g_domID pt (par_pblobj pt p); - val (srls, is, sc) = LItool.from_pblobj_or_detail' thy' (p,p_) pt; + val (is, sc) = LItool.resume_prog thy' (p,p_) pt; val Safe_Step (istate, _, tac) = (*case*) LI.locate_input_tactic sc (pt, po) (fst is) (snd is) m (*of*); diff -r 375177a58baa -r edf1643edde5 test/Tools/isac/Interpret/lucas-interpreter.sml --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Wed Mar 18 14:51:58 2020 +0100 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Wed Mar 18 15:23:15 2020 +0100 @@ -119,7 +119,7 @@ (*+*)val (pt'''''_', (p'''''_', p_'''''_')) = (pt, (p, p_)); (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p); (*else*) val thy' = get_obj g_domID pt (par_pblobj pt p); - val (_, is, sc) = LItool.from_pblobj_or_detail' thy' (p,p_) pt; + val (is, sc) = LItool.resume_prog thy' (p,p_) pt; locate_input_tactic sc (pt, po) (fst is) (snd is) m; "~~~~~ fun locate_input_tactic , args:"; val (Prog prog, cstate, istate, ctxt, tac) @@ -273,7 +273,7 @@ "~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, (pt, p)); (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (*else*); val thy' = get_obj g_domID pt (par_pblobj pt p); - val (_, is, sc) = LItool.from_pblobj_or_detail' thy' (p,p_) pt; + val (is, sc) = LItool.resume_prog thy' (p,p_) pt; (*case*) locate_input_tactic sc (pt, po) (fst is) (snd is) m (*of*); "~~~~~ fun locate_input_tactic , args:"; val ((Rule.Prog prog), (cstate as (pt, (*?*)pos(*?*))), istate, ctxt, tac) @@ -369,7 +369,7 @@ "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip); (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (*else*); val thy' = get_obj g_domID pt (par_pblobj pt p); - val (_, (ist, ctxt), sc) = LItool.from_pblobj_or_detail' thy' (p,p_) pt; + val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt; val Next_Step (_, _, Rewrite_Set' ("Poly", _, Seq {id = "norm_Poly", ...}, _, _)) = LI.find_next_step sc (pt, pos) ist ctxt (*of*); @@ -421,7 +421,7 @@ "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip); (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (*else*); val thy' = get_obj g_domID pt (par_pblobj pt p); - val (_, (ist, ctxt), sc) = LItool.from_pblobj_or_detail' thy' (p,p_) pt; + val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt; (** )val End_Program (ist, tac) = ( *case*) LI.find_next_step sc (pt, pos) ist ctxt (*of*); diff -r 375177a58baa -r edf1643edde5 test/Tools/isac/Knowledge/polyeq-1.sml --- a/test/Tools/isac/Knowledge/polyeq-1.sml Wed Mar 18 14:51:58 2020 +0100 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml Wed Mar 18 15:23:15 2020 +0100 @@ -205,7 +205,7 @@ "~~~~~ fun Step_Solve.by_tactic , args:"; val (m, (pt, po as (p,p_))) = (m, (pt, pos)); e_metID = get_obj g_metID pt (par_pblobj pt p) (*false*); val thy' = get_obj g_domID pt (par_pblobj pt p); - val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; + val (is, sc) = resume_prog thy' (p,p_) pt; val d = e_rls; (*locate_input_tactic (thy',srls) m (pt,(p,p_)) (sc,d) is; WAS: not-found-in-script: NotLocatable from Term_Val1 (Const ("List...*) diff -r 375177a58baa -r edf1643edde5 test/Tools/isac/Knowledge/rateq.sml --- a/test/Tools/isac/Knowledge/rateq.sml Wed Mar 18 14:51:58 2020 +0100 +++ b/test/Tools/isac/Knowledge/rateq.sml Wed Mar 18 15:23:15 2020 +0100 @@ -102,7 +102,7 @@ member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*) "~~~~~ fun 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; (*is: which ctxt?*) +val (is, sc) = resume_prog thy' (p,p_) pt; (*is: which ctxt?*) "~~~~~ fun find_next_step, args:"; val () = (); (*----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------\\* ) "~~~~~ fun go_scan_up, args:"; val (thy, ptp, (Prog sc), E, l, ay, a, v) = @@ -288,7 +288,7 @@ "~~~~~ and do_next, args:"; val ((ptp as (pt, pos as (p,p_)))) = ((pt,ip)); e_metID = get_obj g_metID pt (par_pblobj pt p); (* = false*) val thy' = get_obj g_domID pt (par_pblobj pt p); - val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; + val (is, sc) = resume_prog thy' (p,p_) pt; "~~~~~ fun find_next_step, args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'), (sc as Prog (h $ body)), (Pstate (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is); (*----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------\\* ) diff -r 375177a58baa -r edf1643edde5 test/Tools/isac/Knowledge/rootrateq.sml --- a/test/Tools/isac/Knowledge/rootrateq.sml Wed Mar 18 14:51:58 2020 +0100 +++ b/test/Tools/isac/Knowledge/rootrateq.sml Wed Mar 18 15:23:15 2020 +0100 @@ -340,8 +340,8 @@ val thy' = get_obj g_domID pt (par_pblobj pt p); val (_, (ist, ctxt), sc) = - LItool.from_pblobj_or_detail' thy' (p,p_) pt; -"~~~~~ fun from_pblobj_or_detail' , args:"; val (thy, (p, p_), pt) = (thy', (p,p_), pt); + LItool.resume_prog thy' (p,p_) pt; +"~~~~~ fun resume_prog , args:"; val (thy, (p, p_), pt) = (thy', (p,p_), pt); (*if*) Pos.on_specification p_ (*else*); val (pbl, p', rls') = par_pbl_det pt p (*if*) pbl (*then*); diff -r 375177a58baa -r edf1643edde5 test/Tools/isac/MathEngine/mathengine-stateless.sml --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml Wed Mar 18 14:51:58 2020 +0100 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml Wed Mar 18 15:23:15 2020 +0100 @@ -364,7 +364,7 @@ "~~~~~ fun do_next, args:"; val (ptp as (pt, pos as (p,p_))) = (pt,ip); e_metID = get_obj g_metID pt (par_pblobj pt p); (*false*) val thy' = get_obj g_domID pt (par_pblobj pt p); -val (srls, (ist, ctxt), sc) = from_pblobj_or_detail' thy' (p,p_) pt; +val ((ist, ctxt), sc) = resume_prog thy' (p,p_) pt; val Next_Step (istate, ctxt, tac) = LI.find_next_step sc (pt,pos) ist ctxt; (*WAS Empty_Tac_: tac_*) case tac of Or_to_List' _ => () | _ => error "Or_to_List broken ?" @@ -467,7 +467,7 @@ "~~~~~ fun do_next , args:"; val ((ptp as (pt, pos as (p,p_)))) = (ptp); e_metID = get_obj g_metID pt (par_pblobj pt p) = false; val thy' = get_obj g_domID pt (par_pblobj pt p); - val (srls, (ist, ctxt), sc) = from_pblobj_or_detail' thy' (p,p_) pt; + val ((ist, ctxt), sc) = resume_prog thy' (p,p_) pt; val Next_Step (is, ctxt, tac_) = LI.find_next_step sc (pt,pos) ist ctxt; (*tac_ = Rewrite' (..., ("rnorm_equation_add", "Test.rnorm_equation_add"), ...) !!!!!!!!!!!!!!!!*) diff -r 375177a58baa -r edf1643edde5 test/Tools/isac/Minisubpbl/200-start-method.sml --- a/test/Tools/isac/Minisubpbl/200-start-method.sml Wed Mar 18 14:51:58 2020 +0100 +++ b/test/Tools/isac/Minisubpbl/200-start-method.sml Wed Mar 18 15:23:15 2020 +0100 @@ -127,7 +127,7 @@ "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt,ip); Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (* = false*); val thy' = get_obj g_domID pt (par_pblobj pt p); - val (srls, is, sc) = LItool.from_pblobj_or_detail' thy' (p,p_) pt; + val (is, sc) = LItool.resume_prog thy' (p,p_) pt; "~~~~~ fun find_next_step , args:"; val ((ptp as(pt, (p, _))), (Rule.Prog prog), (Istate.Pstate ist, ctxt)) = ((pt, pos), sc, is); (*case*) scan_to_tactic (prog, (ptp, ctxt)) (Istate.Pstate ist) (*of*); diff -r 375177a58baa -r edf1643edde5 test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml --- a/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Wed Mar 18 14:51:58 2020 +0100 +++ b/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Wed Mar 18 15:23:15 2020 +0100 @@ -43,7 +43,7 @@ "~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, (pt, pos)); (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (* = else*); val thy' = get_obj g_domID pt (par_pblobj pt p); - val (_, is, sc) = LItool.from_pblobj_or_detail' thy' (p,p_) pt; + val (is, sc) = LItool.resume_prog thy' (p,p_) pt; val Safe_Step (_, _, Rewrite_Set' (_, _, Rls {id = "norm_equation", ...}, _, _)) = (*case*) locate_input_tactic sc (pt, po) (fst is) (snd is) m (*of*); @@ -99,7 +99,7 @@ e_metID = get_obj g_metID pt (par_pblobj pt p) = false; (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p)(*else*); val thy' = get_obj g_domID pt (par_pblobj pt p); - val (_, (ist, ctxt), sc) = LItool.from_pblobj_or_detail' thy' (p,p_) pt; + val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt; val Next_Step (_, _, _) = (*case*) LI.find_next_step sc (pt, pos) ist ctxt (*of*); @@ -153,7 +153,7 @@ "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip); (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (*else*); val thy' = get_obj g_domID pt (par_pblobj pt p); - val (srls, (ist, ctxt), sc) = LItool.from_pblobj_or_detail' thy' (p,p_) pt; + val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt; val Next_Step (_, _, _) = (*case*) LI.find_next_step sc (pt, pos) ist ctxt (*of*); diff -r 375177a58baa -r edf1643edde5 test/Tools/isac/Minisubpbl/300-init-subpbl.sml --- a/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Wed Mar 18 14:51:58 2020 +0100 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Wed Mar 18 15:23:15 2020 +0100 @@ -39,7 +39,7 @@ "~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p,p_))) = (m, (pt, p)); (*if*) e_metID = get_obj g_metID pt (par_pblobj pt p) (*false*); val thy' = get_obj g_domID pt (par_pblobj pt p); - val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; + val (is, sc) = resume_prog thy' (p,p_) pt; val Safe_Step (Pstate ist''''', ctxt''''', tac'_''''') = locate_input_tactic sc (pt, po) (fst is) (snd is) m; diff -r 375177a58baa -r edf1643edde5 test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml --- a/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Wed Mar 18 14:51:58 2020 +0100 +++ b/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Wed Mar 18 15:23:15 2020 +0100 @@ -71,7 +71,7 @@ "~~~~~ 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; +val (is, sc) = resume_prog 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); diff -r 375177a58baa -r edf1643edde5 test/Tools/isac/Minisubpbl/470-Check_elementwise-NEXT_STEP.sml --- a/test/Tools/isac/Minisubpbl/470-Check_elementwise-NEXT_STEP.sml Wed Mar 18 14:51:58 2020 +0100 +++ b/test/Tools/isac/Minisubpbl/470-Check_elementwise-NEXT_STEP.sml Wed Mar 18 15:23:15 2020 +0100 @@ -54,7 +54,7 @@ "~~~~~ and do_next , args:"; val ((ptp as (pt, pos as (p, p_)))) = ((pt, ip)); (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (*else*); val thy' = get_obj g_domID pt (par_pblobj pt p); - val (srls, (ist, ctxt), sc) = LItool.from_pblobj_or_detail' thy' (p,p_) pt; + val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt; LI.find_next_step sc (pt, pos) ist ctxt; "~~~~~ fun find_next_step , args:"; val (Rule.Prog prog, (ptp as(pt, (p, _))), Istate.Pstate ist, ctxt) diff -r 375177a58baa -r edf1643edde5 test/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml --- a/test/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml Wed Mar 18 14:51:58 2020 +0100 +++ b/test/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml Wed Mar 18 15:23:15 2020 +0100 @@ -46,7 +46,7 @@ "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip); e_metID = get_obj g_metID pt (par_pblobj pt p); (*false*) val thy' = get_obj g_domID pt (par_pblobj pt p); -val (srls, (ist, ctxt), sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*) +val ((ist, ctxt), sc) = resume_prog thy' (p,p_) pt; (*is: which ctxt?*) val End_Program (ist, tac) = LI.find_next_step sc (pt,pos) ist ctxt; (*+*);tac; (* = Check_Postcond' *) @@ -80,6 +80,6 @@ val (pt,c) = append_result pt p l (scval, (*map str2term*) asm) Complete; (*----------------------------------------############### changed*) -val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*nxt = Check_Postcond ["LINEAR","uval (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*)nivariate", ...]) *); +val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*nxt = Check_Postcond ["LINEAR","uval (is, sc) = resume_prog thy' (p,p_) pt; (*is: which ctxt?*)nivariate", ...]) *); case nxt of ( Check_Postcond ["LINEAR", "univariate", "equation", "test"]) => () | _ => error "450-nxt-Check_Postcond broken" diff -r 375177a58baa -r edf1643edde5 test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml --- a/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Wed Mar 18 14:51:58 2020 +0100 +++ b/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Wed Mar 18 15:23:15 2020 +0100 @@ -55,7 +55,7 @@ "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip); (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (*else*); val thy' = get_obj g_domID pt (par_pblobj pt p); - val (srls, (ist, ctxt), sc) = LItool.from_pblobj_or_detail' thy' (p,p_) pt; + val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt; val Next_Step (_, _, Check_elementwise' _) = (*case*) LI.find_next_step sc (pt, pos) ist ctxt (*of*); diff -r 375177a58baa -r edf1643edde5 test/Tools/isac/Minisubpbl/600-postcond-NEXT_STEP.sml --- a/test/Tools/isac/Minisubpbl/600-postcond-NEXT_STEP.sml Wed Mar 18 14:51:58 2020 +0100 +++ b/test/Tools/isac/Minisubpbl/600-postcond-NEXT_STEP.sml Wed Mar 18 15:23:15 2020 +0100 @@ -109,7 +109,7 @@ "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip); (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (*else*); val thy' = get_obj g_domID pt (par_pblobj pt p); - val (_, (ist, ctxt), sc) = LItool.from_pblobj_or_detail' thy' (p,p_) pt; + val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt; (*+*)istate2str ist = "Pstate ([\"\n(e_e, -1 + x = 0)\",\"\n(v_v, x)\",\"\n(L_L, [x = 1])\"], [R,R,D,R,D], e_rls, NONE, \n[x = 1]," diff -r 375177a58baa -r edf1643edde5 test/Tools/isac/Minisubpbl/700-interSteps.sml --- a/test/Tools/isac/Minisubpbl/700-interSteps.sml Wed Mar 18 14:51:58 2020 +0100 +++ b/test/Tools/isac/Minisubpbl/700-interSteps.sml Wed Mar 18 15:23:15 2020 +0100 @@ -117,7 +117,7 @@ (*+*)val (keep_c', keep_ptp') = (c', ptp'); "~~~~~ and Step_Solve.do_next , args:"; val () = (); (*+*)(*STOPPED HERE: - NOTE: prog.xxx found by LItool.from_pblobj_or_detail' from Rls {scr = Prog xxx, ...}*) + NOTE: prog.xxx found by LItool.resume_prog from Rls {scr = Prog xxx, ...}*) (*+*)val (c', ptp') = (keep_c', keep_ptp'); diff -r 375177a58baa -r edf1643edde5 test/Tools/isac/Minisubpbl/800-append-on-Frm.sml --- a/test/Tools/isac/Minisubpbl/800-append-on-Frm.sml Wed Mar 18 14:51:58 2020 +0100 +++ b/test/Tools/isac/Minisubpbl/800-append-on-Frm.sml Wed Mar 18 15:23:15 2020 +0100 @@ -51,7 +51,7 @@ "~~~~~ and do_next , args:"; val ((ptp as (pt, pos as (p, p_)))) = (pt, input_pos); (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (*else*); val thy' = get_obj g_domID pt (par_pblobj pt p); - val (_, (ist, ctxt), sc) = LItool.from_pblobj_or_detail' thy' (p,p_) pt; + val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt; val Next_Step (ist, ctxt, tac) = (*case*) (**..Ctree NOT updated yet**) LI.find_next_step sc (pt, pos) ist ctxt (*of*); diff -r 375177a58baa -r edf1643edde5 test/Tools/isac/Test_Some.thy --- a/test/Tools/isac/Test_Some.thy Wed Mar 18 14:51:58 2020 +0100 +++ b/test/Tools/isac/Test_Some.thy Wed Mar 18 15:23:15 2020 +0100 @@ -189,7 +189,7 @@ (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (*else*); \ ML \ val thy' = get_obj g_domID pt (par_pblobj pt p); - val (_, (ist, ctxt), sc) = LItool.from_pblobj_or_detail' thy' (p,p_) pt; + val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt; \ ML \ (*+*)Proof_Context.theory_of ctxt; (*..,Isac.RatEq}*) \ text \(*Undefined fact: "all_left"*)