1.1 --- a/src/Tools/isac/Interpret/ctree-basic.sml Thu Aug 22 11:26:14 2019 +0200
1.2 +++ b/src/Tools/isac/Interpret/ctree-basic.sml Thu Aug 22 12:18:58 2019 +0200
1.3 @@ -211,9 +211,9 @@
1.4 (*val e_iist = (e_istate, e_istate); --- sinnlos f"ur NICHT-equality-type*)
1.5
1.6
1.7 -fun new_val v (Istate.ScrState (env, loc_, topt, _, safe, bool)) =
1.8 - (Istate.ScrState (env, loc_, topt, v, safe, bool))
1.9 - | new_val _ _ = error "new_val: only for ScrState";
1.10 +fun new_val v (Istate.Pstate (env, loc_, topt, _, safe, bool)) =
1.11 + (Istate.Pstate (env, loc_, topt, v, safe, bool))
1.12 + | new_val _ _ = error "new_val: only for Pstate";
1.13
1.14 datatype con = land | lor;
1.15
2.1 --- a/src/Tools/isac/Interpret/generate.sml Thu Aug 22 11:26:14 2019 +0200
2.2 +++ b/src/Tools/isac/Interpret/generate.sml Thu Aug 22 12:18:58 2019 +0200
2.3 @@ -50,13 +50,13 @@
2.4 error ("interSteps>..>init_istate: \"" ^ rls ^ "\" has EmptyScr." ^
2.5 "use prep_rls' for storing rule-sets !")
2.6 | Rule.Rls {scr = Rule.Prog s, ...} =>
2.7 - (Istate.ScrState ([(hd (LTool.formal_args s), t)], [], NONE, Rule.e_term, Istate.Sundef, true))
2.8 + (Istate.Pstate ([(hd (LTool.formal_args s), t)], [], NONE, Rule.e_term, Istate.Sundef, true))
2.9 | Rule.Seq {scr = Rule.EmptyScr,...} =>
2.10 error ("interSteps>..>init_istate: \"" ^ rls ^ "\" has EmptyScr." ^
2.11 " Use prep_rls' for storing rule-sets !")
2.12 | Rule.Seq {scr = Rule.Prog s,...} =>
2.13 (writeln ("### init_istate: rls = \"" ^ "rls" ^ "\", Prog = \"" ^ Rule.term2str s ^ "\"");
2.14 - (Istate.ScrState ([(hd (LTool.formal_args s), t)], [], NONE, Rule.e_term, Istate.Sundef, true))
2.15 + (Istate.Pstate ([(hd (LTool.formal_args s), t)], [], NONE, Rule.e_term, Istate.Sundef, true))
2.16 )
2.17 | _ => error "init_istate Rewrite_Set: uncovered case assoc_rls")
2.18 | init_istate (Tactic.Rewrite_Set_Inst (subs, rls)) t =
2.19 @@ -71,14 +71,14 @@
2.20 "use prep_rls' for storing rule-sets !")
2.21 | Rule.Rls {scr = Rule.Prog s, ...} =>
2.22 let val env = (LTool.formal_args s) ~~ [t, v]
2.23 - in (Istate.ScrState (env, [], NONE, Rule.e_term, Istate.Sundef,true))
2.24 + in (Istate.Pstate (env, [], NONE, Rule.e_term, Istate.Sundef,true))
2.25 end
2.26 | Rule.Seq {scr = Rule.EmptyScr, ...} =>
2.27 error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr." ^
2.28 "use prep_rls' for storing rule-sets !")
2.29 | Rule.Seq {scr = Rule.Prog s,...} =>
2.30 let val env = (LTool.formal_args s) ~~ [t, v]
2.31 - in (Istate.ScrState (env,[], NONE, Rule.e_term, Istate.Sundef,true))
2.32 + in (Istate.Pstate (env,[], NONE, Rule.e_term, Istate.Sundef,true))
2.33 end
2.34 | _ => error "init_istate Rewrite_Set_Inst: uncovered case assoc_rls"
2.35 end
3.1 --- a/src/Tools/isac/Interpret/inform.sml Thu Aug 22 11:26:14 2019 +0200
3.2 +++ b/src/Tools/isac/Interpret/inform.sml Thu Aug 22 12:18:58 2019 +0200
3.3 @@ -437,7 +437,7 @@
3.4 {errpats, scr = Rule.Prog prog, ...} => (errpats, prog)
3.5 | _ => error "find_fillpatterns: uncovered case of get_met"
3.6 val env = case Ctree.get_istate pt pos of
3.7 - Istate.ScrState (env, _, _, _, _, _) => env
3.8 + Istate.Pstate (env, _, _, _, _, _) => env
3.9 | _ => error "find_fillpatterns: uncovered case of get_istate"
3.10 val subst = Rtools.get_bdv_subst prog env
3.11 val errpatthms = errpats
4.1 --- a/src/Tools/isac/Interpret/istate.sml Thu Aug 22 11:26:14 2019 +0200
4.2 +++ b/src/Tools/isac/Interpret/istate.sml Thu Aug 22 12:18:58 2019 +0200
4.3 @@ -11,7 +11,7 @@
4.4 val e_scrstate : scrstate
4.5 val scrstate2str : Rule.subst * Celem.loc_ * term option * term * safe * bool -> string
4.6
4.7 - datatype T = RrlsState of Rule.rrlsstate | ScrState of scrstate | Uistate
4.8 + datatype T = RrlsState of Rule.rrlsstate | Pstate of scrstate | Uistate
4.9 val istate2str : T -> string
4.10 val istates2str : T option * T option -> string
4.11 val e_istate : T
4.12 @@ -48,14 +48,14 @@
4.13 (* for handling type T see fun from_pblobj_or_detail', +? *)
4.14 datatype T = (*interpreter state*)
4.15 Uistate (*undefined in modspec, in '_deriv'ation*)
4.16 - | ScrState of scrstate (*for script interpreter*)
4.17 + | Pstate of scrstate (*for script interpreter*)
4.18 | RrlsState of Rule.rrlsstate; (*for reverse rewriting*)
4.19 -val e_istate = (ScrState ([], [], NONE, Rule.e_term, Sundef, false));
4.20 +val e_istate = (Pstate ([], [], NONE, Rule.e_term, Sundef, false));
4.21
4.22 fun rta2str (r, (t, a)) = "\n(" ^ Rule.rule2str r ^ ",(" ^ Rule.term2str t ^", " ^ Rule.terms2str a ^ "))";
4.23 fun istate2str Uistate = "Uistate"
4.24 - | istate2str (ScrState (e, l, to, t, s, b)) =
4.25 - "ScrState ("^ Celem.subst2str e ^ ",\n " ^
4.26 + | istate2str (Pstate (e, l, to, t, s, b)) =
4.27 + "Pstate ("^ Celem.subst2str e ^ ",\n " ^
4.28 Celem.loc_2str l ^ ", " ^ Rule.termopt2str to ^ ",\n " ^
4.29 Rule.term2str t ^ ", " ^ safe2str s ^ ", " ^ bool2str b ^ ")"
4.30 | istate2str (RrlsState (t, t1, rss, rtas)) =
5.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Thu Aug 22 11:26:14 2019 +0200
5.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Thu Aug 22 12:18:58 2019 +0200
5.3 @@ -255,7 +255,7 @@
5.4 if ay = Skip_ then Skip (v, E) else Napp E
5.5 | nstep_up _ _ _ _ l _ _ _ = error ("nstep_up: uncovered fun-def at " ^ Celem.loc_2str l)
5.6
5.7 -fun execute_progr_1 thy ptp (sc as Rule.Prog prog) (Istate.ScrState (E, l, a, v, _, _)) =
5.8 +fun execute_progr_1 thy ptp (sc as Rule.Prog prog) (Istate.Pstate (E, l, a, v, _, _)) =
5.9 if l = []
5.10 then appy thy ptp E [Celem.R] (LTool.body_of prog) NONE v
5.11 else nstep_up thy ptp sc E l Skip_ a v
5.12 @@ -283,8 +283,8 @@
5.13 (Tactic.Rewrite' (thy, "e_rew_ord", Rule.e_rls, false, thm'', f, (Rule.e_term, [(*!?!8.6.03*)])),
5.14 (Istate.Uistate, ctxt), (Rule.e_term, Istate.Sundef)) (*next stac*)
5.15 | _ => error "determine_next_tactic: uncovered case next_rule")
5.16 - | determine_next_tactic thy (ptp as (pt, (p, _))) sc (Istate.ScrState (E,l,a,v,s,_), ctxt) =
5.17 - (case execute_progr_1 thy ptp sc (Istate.ScrState (E,l,a,v,s,false)) of
5.18 + | determine_next_tactic thy (ptp as (pt, (p, _))) sc (Istate.Pstate (E,l,a,v,s,_), ctxt) =
5.19 + (case execute_progr_1 thy ptp sc (Istate.Pstate (E,l,a,v,s,false)) of
5.20 Skip (v, _) => (*finished*)
5.21 (case par_pbl_det pt p of
5.22 (true, p', _) =>
5.23 @@ -296,7 +296,7 @@
5.24 | _ => (Tactic.End_Detail' (Rule.e_term,[])(*8.6.03*), (Istate.e_istate, ctxt), (v,s)))
5.25 | Napp _ => (Tactic.Empty_Tac_, (Istate.e_istate, ctxt), (Rule.e_term, Istate.Sundef)) (*helpless*)
5.26 | Appy (m', scrst as (_,_,_,v,_,_)) =>
5.27 - (m', (Istate.ScrState scrst, ctxt), (v, Istate.Sundef))) (*next stac*)
5.28 + (m', (Istate.Pstate scrst, ctxt), (v, Istate.Sundef))) (*next stac*)
5.29 | determine_next_tactic _ _ _ (is, _) =
5.30 error ("determine_next_tactic: not impl for " ^ (Istate.istate2str is));
5.31
5.32 @@ -418,11 +418,11 @@
5.33 case Lucin.associate pt ctxt m stac of
5.34 Lucin.Ass (m, v', ctxt) =>
5.35 let val (p'',c',f',pt') =
5.36 - Generate.generate1 (Celem.assoc_thy "Isac") m (Istate.ScrState (E,l,a',v',S,true), ctxt) (p',p_) pt;
5.37 + Generate.generate1 (Celem.assoc_thy "Isac") m (Istate.Pstate (E,l,a',v',S,true), ctxt) (p',p_) pt;
5.38 in Assoc ((E,l,a',v',S,true), (m,f',pt',p'',c @ c')::ss) end
5.39 | Lucin.AssWeak (m, v', ctxt) =>
5.40 let val (p'',c',f',pt') =
5.41 - Generate.generate1 (Celem.assoc_thy "Isac") m (Istate.ScrState (E,l,a',v',S,false), ctxt) (p',p_) pt;
5.42 + Generate.generate1 (Celem.assoc_thy "Isac") m (Istate.Pstate (E,l,a',v',S,false), ctxt) (p',p_) pt;
5.43 in Assoc ((E,l,a',v',S,false), (m,f',pt',p'',c @ c')::ss) end
5.44 | Lucin.NotAss =>
5.45 (case ap of (*switch for Or: 1st AssOnly, 2nd AssGen*)
5.46 @@ -433,7 +433,7 @@
5.47 let
5.48 val is = (E,l,a',Lucin.tac_2res m',S,false(*FIXXXME.WN0?*))
5.49 val (p'',c',f',pt') =
5.50 - Generate.generate1 (Celem.assoc_thy "Isac") m' (Istate.ScrState is, ctxt) (p', p_) pt;
5.51 + Generate.generate1 (Celem.assoc_thy "Isac") m' (Istate.Pstate is, ctxt) (p', p_) pt;
5.52 in NasApp (is,(m,f',pt',p'',c @ c')::ss) end
5.53 | Chead.Notappl _ => (NasNap (v, E))
5.54 )
5.55 @@ -533,7 +533,7 @@
5.56 list (* locate_input_tactic may produce intermediate steps *)
5.57 | NotLocatable; (* no (m Ass m') or (m AssWeak m') found *)
5.58
5.59 -fun execute_progr_2 srls m (pt, p) (scr as Rule.Prog sc, d) (Istate.ScrState (E,l,a,v,S,b), ctxt) =
5.60 +fun execute_progr_2 srls m (pt, p) (scr as Rule.Prog sc, d) (Istate.Pstate (E,l,a,v,S,b), ctxt) =
5.61 if l = [] orelse ((*init.in solve..Apply_Method...*)(last_elem o fst) p = 0 andalso snd p = Res)
5.62 then assy (ctxt,srls,d,Aundef) ((E,[Celem.R],a,v,S,b), [(m,Generate.EmptyMout,pt,p,[])])
5.63 (LTool.body_of sc)
5.64 @@ -567,7 +567,7 @@
5.65 [] => NotLocatable
5.66 | rts' => Steps (Lucin.rts2steps [] ((pt,p),(f,f'',rss,rts),("Isac",ro,er,pa)) rts') ) *)
5.67 (*| locate_input_tactic (thy', srls) m (pt, p)
5.68 - (scr as Rule.Prog _, d) (Istate.ScrState (E,l,a,v,S,b), ctxt) = *)
5.69 + (scr as Rule.Prog _, d) (Istate.Pstate (E,l,a,v,S,b), ctxt) = *)
5.70 fun locate_input_tactic (progr as Rule.Prog _) (cstate as (pt, pos)) istate ctxt tac =
5.71 let
5.72 val srls = Lucin.get_simplifier cstate (*TODO: shift to init_istate*)
5.73 @@ -575,18 +575,18 @@
5.74 (case execute_progr_2 srls tac cstate (progr, Rule.e_rls) (istate, ctxt) of
5.75 Assoc ((is as (_,_,_,_,_,strong_ass), ss as((tac', _, ctree, pos', _) :: _))) =>
5.76 if strong_ass
5.77 - then Safe_Step ((ctree, pos'), Istate.ScrState is, get_ctxt ctree pos', tac')
5.78 + then Safe_Step ((ctree, pos'), Istate.Pstate is, get_ctxt ctree pos', tac')
5.79 else (* TODO: shift generate1 below ( + generate1 in assy) to solve *)
5.80 if Lucin.rew_only ss (*andalso 'not strong_ass'= associated weakly*)
5.81 then
5.82 let
5.83 val (po, p_) = pos
5.84 val po' = case p_ of Frm => po | Res => lev_on po | _ => error ("locate_input_tactic " ^ pos_2str p_)
5.85 - val (p'',_,_,pt'') = Generate.generate1 thy tac' (Istate.ScrState is, ctxt) (po', p_) pt
5.86 + val (p'',_,_,pt'') = Generate.generate1 thy tac' (Istate.Pstate is, ctxt) (po', p_) pt
5.87 in
5.88 - Unsafe_Step ((pt'',p''), Istate.ScrState is, get_ctxt ctree pos', tac')
5.89 + Unsafe_Step ((pt'',p''), Istate.Pstate is, get_ctxt ctree pos', tac')
5.90 end
5.91 - else Unsafe_Step ((ctree, pos'), Istate.ScrState is, get_ctxt ctree pos', tac')
5.92 + else Unsafe_Step ((ctree, pos'), Istate.Pstate is, get_ctxt ctree pos', tac')
5.93 | NasApp _ => Not_Locatable (Tactic.tac_2str tac ^ " not locatable")
5.94 | err => raise ERROR ("not-found-in-script: NotLocatable from " ^ @{make_string} err))
5.95 end
5.96 @@ -636,9 +636,9 @@
5.97 [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] )))]
5.98 else itms
5.99 (*\\----------- hack for funpack: generalise handling of meths which extend problem items -----//*)
5.100 - val (is, env, ctxt, scr) = case Lucin.init_scrstate ctxt itms mI of
5.101 - (is as Istate.ScrState (env,_,_,_,_,_), ctxt, scr) => (is, env, ctxt, scr)
5.102 - | _ => error "begin_end_prog Apply_Method': uncovered case init_scrstate"
5.103 + val (is, env, ctxt, scr) = case Lucin.init_pstate ctxt itms mI of
5.104 + (is as Istate.Pstate (env,_,_,_,_,_), ctxt, scr) => (is, env, ctxt, scr)
5.105 + | _ => error "begin_end_prog Apply_Method': uncovered case init_pstate"
5.106 val ini = Lucin.init_form thy scr env;
5.107 in
5.108 case ini of
5.109 @@ -668,7 +668,7 @@
5.110 val metID = get_obj g_metID pt pp;
5.111 val {srls = srls, scr = sc, ...} = Specify.get_met metID;
5.112 val (loc, E, l, a, b, ctxt) = case get_loc pt (p, p_) of
5.113 - loc as (Istate.ScrState (E,l,a,_,_,b), ctxt) => (loc, E, l, a, b, ctxt)
5.114 + loc as (Istate.Pstate (E,l,a,_,_,b), ctxt) => (loc, E, l, a, b, ctxt)
5.115 | _ => error "begin_end_prog Check_Postcond': uncovered case get_loc"
5.116 val thy' = get_obj g_domID pt pp;
5.117 val thy = Celem.assoc_thy thy';
5.118 @@ -677,7 +677,7 @@
5.119 if pp = []
5.120 then
5.121 let
5.122 - val is = Istate.ScrState (E, l, a, scval, scsaf, b)
5.123 + val is = Istate.Pstate (E, l, a, scval, scsaf, b)
5.124 val tac_ = Tactic.Check_Postcond'(pI,(scval, asm))
5.125 val ((p, p_), ps, _, pt) = Generate.generate1 thy tac_ (is, ctxt) (pp, Res) pt;
5.126 in ([(Tactic.Check_Postcond pI, tac_, ((pp, Res), (is, ctxt)))], ps, (pt, (p, p_))) end
5.127 @@ -687,11 +687,11 @@
5.128 val thy' = get_obj g_domID pt ppp;
5.129 val thy = Celem.assoc_thy thy';
5.130 val (E, l, a, b, ctxt') = case get_loc pt (pp, Frm) of
5.131 - (Istate.ScrState (E,l,a,_,_,b), ctxt') => (E, l, a, b, ctxt')
5.132 + (Istate.Pstate (E,l,a,_,_,b), ctxt') => (E, l, a, b, ctxt')
5.133 | _ => error "begin_end_prog Check_Postcond' script of parpbl: uncovered case get_loc"
5.134 val ctxt'' = ContextC.from_subpbl_to_caller ctxt scval ctxt'
5.135 val tac_ = Tactic.Check_Postcond' (pI, (scval, asm))
5.136 - val is = Istate.ScrState (E,l,a,scval,scsaf,b)
5.137 + val is = Istate.Pstate (E,l,a,scval,scsaf,b)
5.138 val ((p, p_), ps, _, pt) = Generate.generate1 thy tac_ (is, ctxt'') (pp, Res) pt;
5.139 in ([(Tactic.Check_Postcond pI, tac_, ((pp, Res), (is, ctxt'')))], ps, (pt, (p, p_))) end
5.140 end
6.1 --- a/src/Tools/isac/Interpret/rewtools.sml Thu Aug 22 11:26:14 2019 +0200
6.2 +++ b/src/Tools/isac/Interpret/rewtools.sml Thu Aug 22 12:18:58 2019 +0200
6.3 @@ -573,7 +573,7 @@
6.4 # otherwise []
6.5 WN060617 hack assuming that all scripts use only one bound variable
6.6 and use 'v_' as the formal argument for this bound variable*)
6.7 -fun subs_from (Istate.ScrState (env, _, _, _, _, _)) _ guh =
6.8 +fun subs_from (Istate.Pstate (env, _, _, _, _, _)) _ guh =
6.9 let
6.10 val (_, _, thyID, sect, xstr) = case guh2theID guh of
6.11 theID as [isa, thyID, sect, xstr] => (theID, isa, thyID, sect, xstr)
7.1 --- a/src/Tools/isac/Interpret/script.sml Thu Aug 22 11:26:14 2019 +0200
7.2 +++ b/src/Tools/isac/Interpret/script.sml Thu Aug 22 12:18:58 2019 +0200
7.3 @@ -17,7 +17,7 @@
7.4 val sel_rules : Ctree.ctree -> Ctree.pos' -> Tactic.input list
7.5 val init_form : 'a -> Rule.program -> (term * term) list -> term option
7.6 val tac_2tac : Tactic.T -> Tactic.input
7.7 - val init_scrstate : Proof.context -> Model.itm list -> Celem.metID -> Istate.T * Proof.context * Rule.program
7.8 + val init_pstate : Proof.context -> Model.itm list -> Celem.metID -> Istate.T * Proof.context * Rule.program
7.9
7.10 val get_simplifier : Ctree.state -> Rule.rls
7.11 (*DEPR ^*)val from_pblobj' : Rule.theory' -> Ctree.pos' -> Ctree.ctree -> Rule.rls * (Istate.T * Proof.context) * Rule.program
7.12 @@ -569,7 +569,7 @@
7.13 then tracing("@@@ istate " ^ Celem.env2str env)
7.14 else ();
7.15 in
7.16 -fun init_scrstate ctxt itms metID =
7.17 +fun init_pstate ctxt itms metID =
7.18 let
7.19 (*//----------- hack for funpack: generalise handling of meths which extend problem items -----\\*)
7.20 val itms =
7.21 @@ -589,7 +589,7 @@
7.22 val _ = if actuals <> [] then () else raise ERROR (errmsg ^ strs2str' metID)
7.23 val (scr, sc) = (case (#scr o Specify.get_met) metID of
7.24 scr as Rule.Prog sc => (trace_init metID; (scr, sc))
7.25 - | _ => raise ERROR ("init_scrstate with " ^ Celem.metID2str metID))
7.26 + | _ => raise ERROR ("init_pstate with " ^ Celem.metID2str metID))
7.27 val formals = LTool.formal_args sc
7.28 fun assoc_by_type f aa =
7.29 case filter (curry (fn (f, a) => type_of f = type_of a) f) aa of
7.30 @@ -609,7 +609,7 @@
7.31 val {pre, prls, ...} = Specify.get_met metID;
7.32 val pres = Stool.check_preconds (Proof_Context.theory_of ctxt) prls pre itms |> map snd;
7.33 val ctxt = ctxt |> ContextC.insert_assumptions pres;
7.34 - in (Istate.ScrState (env, [], NONE, Rule.e_term, Istate.Safe, true), ctxt, scr) end;
7.35 + in (Istate.Pstate (env, [], NONE, Rule.e_term, Istate.Safe, true), ctxt, scr) end;
7.36 end (*local*)
7.37
7.38 fun get_simplifier (pt, (p, _)) =
7.39 @@ -664,12 +664,10 @@
7.40 then
7.41 let
7.42 val ctxt = ContextC.initialise thy' (Model.vars_of itms)
7.43 - val (is, ctxt, scr) = init_scrstate ctxt itms metID
7.44 + val (is, ctxt, scr) = init_pstate ctxt itms metID
7.45 in (srls, (is, ctxt), scr) end
7.46 else (srls, get_loc pt (p,p_), scr)
7.47 end;
7.48 -
7.49 -
7.50
7.51 (*.get the stactics and problems of a script as tacs
7.52 instantiated with the current environment;
7.53 @@ -724,7 +722,7 @@
7.54 val (sc, srls) = (case Specify.get_met metID' of
7.55 {scr = Rule.Prog sc, srls, ...} => (sc, srls) | _ => error "sel_rules 1")
7.56 val (env, a, v) = (case get_istate pt (p, p_) of
7.57 - Istate.ScrState (env, _, a, v, _, _) => (env, a, v) | _ => error "sel_rules 2")
7.58 + Istate.Pstate (env, _, a, v, _, _) => (env, a, v) | _ => error "sel_rules 2")
7.59 in map ((stac2tac pt thy) o LTool.rep_stacexpr o #2 o
7.60 (handle_leaf "selrul" thy' srls env a v)) (LTool.stacpbls sc)
7.61 end;
7.62 @@ -750,7 +748,7 @@
7.63 {scr = Rule.Prog sc, srls, erls, rew_ord' = ro, ...} => (sc, srls, erls, ro)
7.64 | _ => error "sel_appl_atomic_tacs 1")
7.65 val (env, a, v) = (case get_istate pt (p, p_) of
7.66 - Istate.ScrState (env, _, a, v, _, _) => (env, a, v) | _ => error "sel_appl_atomic_tacs 2")
7.67 + Istate.Pstate (env, _, a, v, _, _) => (env, a, v) | _ => error "sel_appl_atomic_tacs 2")
7.68 val alltacs = (*we expect at least 1 stac in a script*)
7.69 map ((stac2tac pt thy) o LTool.rep_stacexpr o #2 o
7.70 (handle_leaf "selrul" thy' srls env a v)) (LTool.stacpbls sc)
8.1 --- a/src/Tools/isac/Interpret/solve.sml Thu Aug 22 11:26:14 2019 +0200
8.2 +++ b/src/Tools/isac/Interpret/solve.sml Thu Aug 22 12:18:58 2019 +0200
8.3 @@ -119,9 +119,9 @@
8.4 | _ => error "solve Apply_Method: uncovered case get_obj"
8.5 val thy' = get_obj g_domID pt p;
8.6 val thy = Celem.assoc_thy thy';
8.7 - val (is, env, ctxt, sc) = case Lucin.init_scrstate ctxt itms mI of
8.8 - (is as Istate.ScrState (env,_,_,_,_,_), ctxt, sc) => (is, env, ctxt, sc)
8.9 - | _ => error "solve Apply_Method: uncovered case init_scrstate"
8.10 + val (is, env, ctxt, sc) = case Lucin.init_pstate ctxt itms mI of
8.11 + (is as Istate.Pstate (env,_,_,_,_,_), ctxt, sc) => (is, env, ctxt, sc)
8.12 + | _ => error "solve Apply_Method: uncovered case init_pstate"
8.13 val ini = Lucin.init_form thy sc env;
8.14 val p = lev_dn p;
8.15 in
8.16 @@ -166,7 +166,7 @@
8.17 val metID = get_obj g_metID pt pp;
8.18 val {srls = srls, scr = sc, ...} = Specify.get_met metID;
8.19 val (loc, E, l, a, b, ctxt) = case get_loc pt (p, p_) of
8.20 - loc as (Istate.ScrState (E, l, a, _, _, b), ctxt) => (loc, E, l, a, b, ctxt)
8.21 + loc as (Istate.Pstate (E, l, a, _, _, b), ctxt) => (loc, E, l, a, b, ctxt)
8.22 | _ => error "solve Check_Postcond: uncovered case get_loc"
8.23 val thy' = get_obj g_domID pt pp;
8.24 val thy = Celem.assoc_thy thy';
8.25 @@ -175,7 +175,7 @@
8.26 if pp = []
8.27 then
8.28 let
8.29 - val is = Istate.ScrState (E,l,a,scval,scsaf,b)
8.30 + val is = Istate.Pstate (E,l,a,scval,scsaf,b)
8.31 val tac_ = Tactic.Check_Postcond' (pI, (scval, asm))
8.32 val (pos, ps, _, pt) = Generate.generate1 thy tac_ (is, ctxt) (pp, Res) pt;
8.33 in ("ok", ([(Tactic.Check_Postcond pI, tac_, ((pp, Res), (is, ctxt)))], ps, (pt, pos))) end
8.34 @@ -185,13 +185,13 @@
8.35 val thy' = get_obj g_domID pt ppp;
8.36 val thy = Celem.assoc_thy thy';
8.37 val (E, l, a, b, ctxt') = case get_loc pt (pp, Frm) of
8.38 - (Istate.ScrState (E, l, a, _, _, b), ctxt') => (E, l, a, b, ctxt')
8.39 + (Istate.Pstate (E, l, a, _, _, b), ctxt') => (E, l, a, b, ctxt')
8.40 | _ => error "solve Check_Postcond resume script of parpbl: uncovered case get_loc"
8.41 val ctxt'' = ContextC.from_subpbl_to_caller ctxt scval ctxt'
8.42 val ((p, p_), ps, _, pt) = Generate.generate1 thy (Tactic.Check_Postcond' (pI, (scval, asm)))
8.43 - (Istate.ScrState (E,l,a,scval,scsaf,b), ctxt'') (pp,Res) pt;
8.44 + (Istate.Pstate (E,l,a,scval,scsaf,b), ctxt'') (pp,Res) pt;
8.45 in ("ok", ([(Tactic.Check_Postcond pI, Tactic.Check_Postcond'(pI, (scval, asm)),
8.46 - ((pp, Res), (Istate.ScrState (E, l, a, scval, scsaf, b), ctxt'')))], ps, (pt, (p, p_)))) end
8.47 + ((pp, Res), (Istate.Pstate (E, l, a, scval, scsaf, b), ctxt'')))], ps, (pt, (p, p_)))) end
8.48 end
8.49 | solve (_, Tactic.End_Proof'') (pt, (p, p_)) =
8.50 ("end-proof", ([(Tactic.Empty_Tac, Tactic.Empty_Tac_, (([], Res), (Istate.Uistate, ContextC.e_ctxt)))], [], (pt, (p, p_))))
8.51 @@ -313,7 +313,7 @@
8.52 | _ =>
8.53 let
8.54 val is = Generate.init_istate tac t
8.55 - (*TODO.WN060602 ScrState (["(t_, Problem (Isac,[equation,univar]))"]
8.56 + (*TODO.WN060602 Pstate (["(t_, Problem (Isac,[equation,univar]))"]
8.57 is wrong for simpl, but working ?!? *)
8.58 val tac_ = Tactic.Apply_Method' (Celem.e_metID(*WN0402: see generate1 !?!*), SOME t, is, ctxt)
8.59 val pos' = ((lev_on o lev_dn) p, Frm)
8.60 @@ -370,7 +370,7 @@
8.61 {errpats, nrls, scr = Rule.Prog prog, ...} => (errpats, nrls, prog)
8.62 | _ => error "inform: uncovered case of get_met"
8.63 val env = case Ctree.get_istate pt pos of
8.64 - Istate.ScrState (env, _, _, _, _, _) => env
8.65 + Istate.Pstate (env, _, _, _, _, _) => env
8.66 | _ => error "inform: uncovered case of get_istate"
8.67 in
8.68 case Inform.check_error_patterns (f_pred, f_in) (prog, env) (errpats, nrls) of
9.1 --- a/src/Tools/isac/ProgLang/contextC.sml Thu Aug 22 11:26:14 2019 +0200
9.2 +++ b/src/Tools/isac/ProgLang/contextC.sml Thu Aug 22 12:18:58 2019 +0200
9.3 @@ -31,7 +31,7 @@
9.4 * solve-phase by Lucas-Interpretation:
9.5 * locate_input_tactic:
9.6 * Tactic.Apply_Method
9.7 - * initialises ctxt (declare_constraints' + insert_assumptions pres) by init_scrstate
9.8 + * initialises ctxt (declare_constraints' + insert_assumptions pres) by init_pstate
9.9 * in solve for root problem
9.10 * in begin_end_prog for subproblem
9.11 * Tactic.Rewrite* create assumptions; respective insert_assumptions is done by associate
9.12 @@ -47,7 +47,7 @@
9.13 * locate_input_formula: follows sig. of determine_next_tactic
9.14 * changing from one method to another (in determine_next_tactic only):
9.15 * from method to sub-program: just add new preconditions of the guard
9.16 - * locate_input_tactic: init_scrstate by begin_end_prog
9.17 + * locate_input_tactic: init_pstate by begin_end_prog
9.18 * determine_next_tactic:
9.19 * from_subpbl_to_caller
9.20 * finishing a method:
9.21 @@ -92,20 +92,20 @@
9.22
9.23 all_solve
9.24 begin_end_prog (Tactic.Apply_Method'
9.25 - init_scrstate
9.26 + init_pstate
9.27 declare_constraints'
9.28 insert_assumptions
9.29
9.30 nxt_specify_
9.31 begin_end_prog (Tactic.Apply_Method'
9.32 - init_scrstate
9.33 + init_pstate
9.34 declare_constraints'
9.35 insert_assumptions
9.36 ------------------------------------------------------------------------------------------------
9.37 LI
9.38 ------------------------------------------------------------------------------------------------
9.39 solve ("Apply_Method" root-program
9.40 - init_scrstate
9.41 + init_pstate
9.42 declare_constraints'
9.43 insert_assumptions
9.44 locate_input_tactic
9.45 @@ -131,7 +131,7 @@
9.46 all_modspec
9.47 declare_constraints'
9.48 begin_end_prog (Tactic.Apply_Method'
9.49 - init_scrstate
9.50 + init_pstate
9.51 declare_constraints'
9.52 insert_assumptions
9.53 ------------------------------------------------------------------------------------------------
9.54 @@ -165,7 +165,7 @@
9.55 declare_constraints
9.56 ??
9.57 from_pblobj'
9.58 - init_scrstate
9.59 + init_pstate
9.60 declare_constraints'
9.61 insert_assumptions
9.62 ??
10.1 --- a/src/Tools/isac/TODO.thy Thu Aug 22 11:26:14 2019 +0200
10.2 +++ b/src/Tools/isac/TODO.thy Thu Aug 22 12:18:58 2019 +0200
10.3 @@ -14,37 +14,13 @@
10.4 text \<open>
10.5 \begin{itemize}
10.6 \item xxx
10.7 - \item clarify initialisation of contexts
10.8 - \begin{itemize}
10.9 - \item xxx
10.10 - \item Lucin.init_scrstate --> Istate.init_program
10.11 - \item xxx
10.12 - \item Tactic.Apply_Method' (mI, _, _, _(*ctxt ?!?*))) .. remove ctxt
10.13 - \item xxx
10.14 - \item Test_Some.all-contxt: wait for deleting Check_Elementwise Assumptions
10.15 - \item xxx
10.16 - \end{itemize}
10.17 \item xxx
10.18 - \item rename ScrState --> Program_State
10.19 - \item locate_input_tactic arg: type istate ((ScrState is))
10.20 - result: type scrstate ((is)) ... unify + readable paper!
10.21 - rename ? ^^^^^^^^ prog_state, pstate
10.22 + \item xxx
10.23 \item script: rename AssWeak --> Ass_Weak
10.24 - \item lucas-intrpreter.assy: Generate.generate1 (Celem.assoc_thy "Isac")
10.25 \item lucas-intrpreter.locate_input_tactic: execute_progr_2 srls tac cstate (progr, Rule.e_rls)
10.26 ^^^^^^^^^^
10.27 \item Lucin.associate: ctree -> Proof.context -> Tactic.T -> term -> Lucin.ass
10.28 -----> : ctree -> Proof.context -> (Tactic.T * term) -> Lucin.ass
10.29 - \item ?delete Check_Postcond' in begin_end_prog (already done in solve?)
10.30 - in case both are needed, unify !
10.31 - \item rm ctxt from Subproblem' (is separated in associate!))
10.32 - \item xxx
10.33 - \item comoplete mstools.sml (* survey on handling contexts:
10.34 - \item collect ctxt to structure ContextC + address all uses of insert_assumptions here
10.35 - \item xxx
10.36 - \item dest_spec (Const ("Product_Type.Pair", _) $ d $ (Const ("Product_Type.Pair", _) FORALL occur.
10.37 - \item xxx
10.38 - \item check Tactic.Subproblem': are 2 terms required?
10.39 \item xxx
10.40 \item xxx
10.41 \end{itemize}
10.42 @@ -52,6 +28,23 @@
10.43 subsection \<open>Postponed from current changeset\<close>
10.44 text \<open>
10.45 \begin{itemize}
10.46 + \item clarify handling of contexts
10.47 + \begin{itemize}
10.48 + \item Check_Elementwise "Assumptions": prerequisite for ^^goal
10.49 + \item xxx
10.50 + \item Tactic.Apply_Method' (mI, _, _, _(*ctxt ?!?*))) .. remove ctxt
10.51 + \item rm ctxt from Subproblem' (is separated in associate!))
10.52 + \item check Tactic.Subproblem': are 2 terms required?
10.53 + \item xxx
10.54 + \item Test_Some.--- rat-equ: remove x = 0 from [x = 0, x = 6 / 5] due to contexts --
10.55 + --: wait for deleting Check_Elementwise Assumptions
10.56 + \item xxx
10.57 + \item lucas-intrpreter.assy: Generate.generate1 (Celem.assoc_thy "Isac")
10.58 + \end{itemize}
10.59 + \item xxx
10.60 + \item complete mstools.sml (* survey on handling contexts:
10.61 + \item xxx
10.62 + \item dest_spec (Const ("Product_Type.Pair", _) $ d $ (Const ("Product_Type.Pair", _) FORALL occur.
10.63 \item introduce simple type names to LUCAS_INTERPRETER <-?-> readable paper
10.64 \item xxx
10.65 \item check in states: length ?? > 1 with tracing these cases
10.66 @@ -62,8 +55,8 @@
10.67 \item xxx
10.68 \item istate
10.69 \begin{itemize}
10.70 - \item rename srcstate --> program_state
10.71 - and after review of Rrls, detail ?--> istate
10.72 + \item DONE rename srcstate --> pstate
10.73 + and after review of Rrls, detail ?-->? istate
10.74 \item locate_input_tactic: get_simplifier cstate (*TODO: shift to init_istate*)
10.75 \item xxx
10.76 \item xxx
10.77 @@ -72,7 +65,7 @@
10.78 \item xxx
10.79 \item ctxt context
10.80 \begin{itemize}
10.81 - \item Rewrite.eval_listexpr_ thy ..: can thy be extracted from ctxt ?
10.82 + \item DONE Rewrite.eval_listexpr_ thy ..: can thy be extracted from ctxt ?
10.83 \item xxx
10.84 \item xxx
10.85 \end{itemize}
10.86 @@ -105,7 +98,7 @@
10.87 \begin{itemize}
10.88 \item rm from "generate1" ("Detail_Set_Inst'", Tactic.Detail_Set' ?)
10.89 \item shift from "applicable_in..Apply_Method" to ? ? ? (is ONLY use-case in appl.sml))
10.90 - \item ?"insert_assumptions" necessary in "init_scrstate" ?+++? in "applicable_in" ?+++? "associate"
10.91 + \item ?"insert_assumptions" necessary in "init_pstate" ?+++? in "applicable_in" ?+++? "associate"
10.92 \item xxx
10.93 \item xxx
10.94 \item DO DELETIONS AFTER analogous concentrations in determine_next_tactic
10.95 @@ -187,6 +180,9 @@
10.96 text \<open>
10.97 unify to calcstate, calcstate'
10.98 \begin{itemize}
10.99 + \item ?delete Check_Postcond' in begin_end_prog (already done in solve?)
10.100 + in case both are needed, unify !
10.101 + \item xxx
10.102 \item ? rename begin_end_prog -> check_switch_prog
10.103 \item adopt the same for specification phase
10.104 \item xxx
10.105 @@ -272,7 +268,7 @@
10.106 but there is Proof_Context.theory_of !!!
10.107 \end{itemize}
10.108 \<close>
10.109 -subsection \<open>Rfuns, Begin_/End_Detail', Rrls\<close>
10.110 +subsection \<open>Rfuns, Begin_/End_Detail', Rrls, Istate\<close>
10.111 text \<open>
10.112 \begin{itemize}
10.113 \item removing from_pblobj_or_detail' causes many strange errors
10.114 @@ -286,7 +282,7 @@
10.115 \item xxx
10.116 \item datatype istate (Istate.T): remove RrlsState, scrstate: use Rrls only for creating results beyond
10.117 rewriting and/or respective intermediate steps (e.g. cancellation of fractions).
10.118 - Thus we get a 1-step-action which does NOT require a state beyond istate(?).
10.119 + Thus we get a 1-step-action which does NOT require a state beyond istate/pstate.
10.120 Thus we drastically reduce complexity, also get rid of "fun from_pblobj_or_detail_calc" , etc.
10.121 \item debug ^^^ related: is there an occurence of Steps with more than 1 element?
10.122 \item xxx
11.1 --- a/test/Tools/isac/Frontend/use-cases.sml Thu Aug 22 11:26:14 2019 +0200
11.2 +++ b/test/Tools/isac/Frontend/use-cases.sml Thu Aug 22 12:18:58 2019 +0200
11.3 @@ -161,7 +161,7 @@
11.4 val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1; (*<---------------------- orig. test code*)
11.5 (*+isa=REP*) if p = ([1], Frm) andalso term2str (get_obj g_form pt [1]) = "1 + -1 * 2 + x = 0"
11.6 andalso istate2str (get_istate pt p)
11.7 - = "ScrState ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"],\n [], NONE,\n ??.empty, Safe, true)"
11.8 + = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"],\n [], NONE,\n ??.empty, Safe, true)"
11.9 then () else error "refFormula = 1 + -1 * 2 + x = 0 changed";
11.10 (*-------------------------------------------------------------------------*)
11.11
11.12 @@ -181,11 +181,11 @@
11.13 (*//******************* locatetac returns tac_ + istate + cstate *****************************\\*)
11.14 locatetac : Tactic.input -> state -> string * (taci list * pos' list * state);
11.15 if istate2str istate
11.16 - = "ScrState ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"],\n [R,L,R,L,R,L,R], (SOME e_e),\n x = 0 + -1 * (1 + -1 * 2), Safe, true)"
11.17 + = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"],\n [R,L,R,L,R,L,R], (SOME e_e),\n x = 0 + -1 * (1 + -1 * 2), Safe, true)"
11.18 then () else error "from locatetac return --- changed 1";
11.19
11.20 if istate2str (get_istate (fst cstate) (snd cstate))
11.21 - = "ScrState ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"],\n [R,L,R,L,R,L,R], (SOME e_e),\n x = 0 + -1 * (1 + -1 * 2), Safe, true)"
11.22 + = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"],\n [R,L,R,L,R,L,R], (SOME e_e),\n x = 0 + -1 * (1 + -1 * 2), Safe, true)"
11.23 then () else error "from locatetac return --- changed 2";
11.24 (*\\******************* locatetac returns tac_ + istate + cstate *****************************//*)
11.25
11.26 @@ -207,7 +207,7 @@
11.27 (*+*)Safe_Step: state * Istate.T * Proof.context * Tactic.T -> input_tactic_result;
11.28 (********************* locate_input_tactic returns cstate * istate * Proof.context *************)
11.29 (*+*)if istate2str istate
11.30 -(*+isa*) = "ScrState ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"],\n [R,L,R,L,R,L,R], (SOME e_e),\n x = 0 + -1 * (1 + -1 * 2), Safe, true)"(**)
11.31 +(*+isa*) = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"],\n [R,L,R,L,R,L,R], (SOME e_e),\n x = 0 + -1 * (1 + -1 * 2), Safe, true)"(**)
11.32 then case m of Rewrite_Set_Inst' _ => ()
11.33 else error "from locate_input_tactic return --- changed";
11.34
11.35 @@ -232,7 +232,7 @@
11.36 (*+isa==REP*)val [(Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv"),
11.37 Rewrite_Set_Inst' _, (pos', (istate, ctxt)))] = tacis;
11.38 (*+*)if pos' = ([1], Res) andalso istate2str istate
11.39 - = "ScrState ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"],\n [R,L,R,L,R,L,R], (SOME e_e),\n x = 0 + -1 * (1 + -1 * 2), Safe, true)"
11.40 + = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"],\n [R,L,R,L,R,L,R], (SOME e_e),\n x = 0 + -1 * (1 + -1 * 2), Safe, true)"
11.41 then () else error "init. step 1 + -1 * 2 + x = 0 changed";
11.42
11.43 val pIopt = get_pblID (pt,ip);
11.44 @@ -244,7 +244,7 @@
11.45 val ("ok", [], ptp as (pt, p)) = xxxx;
11.46
11.47 if istate2str (get_istate pt p) (* <> <> <> <> ^^^^^^^^^^^^^*)
11.48 -(*REP*) = "ScrState ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"],\n [R,L,R,L,R,L,R], (SOME e_e),\n x = 0 + -1 * (1 + -1 * 2), Safe, true)"
11.49 +(*REP*) = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"],\n [R,L,R,L,R,L,R], (SOME e_e),\n x = 0 + -1 * (1 + -1 * 2), Safe, true)"
11.50 then () else error "REP autoCalculate on (e_e, 1 + -1 * 2 + x = 0) changed"
11.51
11.52 "~~~~~ from TOPLEVEL to states return:"; upd_calc cI (ptp, []); upd_ipos cI 1 p;
12.1 --- a/test/Tools/isac/Interpret/calchead.sml Thu Aug 22 11:26:14 2019 +0200
12.2 +++ b/test/Tools/isac/Interpret/calchead.sml Thu Aug 22 12:18:58 2019 +0200
12.3 @@ -700,7 +700,7 @@
12.4 ("Integrate", ["integrate", "function"],
12.5 ["diff", "integration"])),
12.6 loc =
12.7 - (Some (ScrState ([], [], None, Const ("empty", "'a"), Sundef, false)),
12.8 + (Some (Pstate ([], [], None, Const ("empty", "'a"), Sundef, false)),
12.9 None),
12.10 cell = None, meth = [], spec = ("e_domID", ["e_pblID"], ["e_metID"]),
12.11 probl = [], branch = TransitiveB,
12.12 @@ -761,7 +761,7 @@
12.13 ["diff", "integration"])),
12.14 loc =
12.15 (Some
12.16 - (ScrState ([], [], None, Const ("empty", "'a"), Sundef, false)),
12.17 + (Pstate ([], [], None, Const ("empty", "'a"), Sundef, false)),
12.18 None),
12.19 cell = None, meth = [], spec =
12.20 ("e_domID", ["e_pblID"], ["e_metID"]), probl =
13.1 --- a/test/Tools/isac/Interpret/inform.sml Thu Aug 22 11:26:14 2019 +0200
13.2 +++ b/test/Tools/isac/Interpret/inform.sml Thu Aug 22 12:18:58 2019 +0200
13.3 @@ -660,7 +660,7 @@
13.4 val NONE = env;
13.5 val (SOME istate, NONE) = loc;
13.6 (*default_print_depth 5;*) writeln (istate2str (fst istate)); (*default_print_depth 3;*)
13.7 -(*ScrState ([],
13.8 +(*Pstate ([],
13.9 [], NONE,
13.10 ??.empty, Sundef, false)*)
13.11 (*default_print_depth 5;*) spec; (*default_print_depth 3;*)
13.12 @@ -704,7 +704,7 @@
13.13 val NONE = env;
13.14 val (SOME istate, NONE) = loc;
13.15 (*default_print_depth 5;*) writeln (istate2str (fst istate)); (*default_print_depth 3;*)
13.16 -(*ScrState ([],
13.17 +(*Pstate ([],
13.18 [], NONE,
13.19 ??.empty, Sundef, false)*)
13.20 (*default_print_depth 5;*) spec; (*default_print_depth 3;*)
13.21 @@ -1037,7 +1037,7 @@
13.22 (*+*)then () else error "inform with (positive) check_error_patterns broken 3";
13.23
13.24 val env = case Ctree.get_istate pt pos of
13.25 - Istate.ScrState (env, _, _, _, _, _) => env
13.26 + Istate.Pstate (env, _, _, _, _, _) => env
13.27 | _ => error "inform: uncovered case of get_istate"
13.28 ;
13.29 (*+*)if term2str f_pred = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso
13.30 @@ -1076,7 +1076,7 @@
13.31 val f_curr = get_curr_formula (pt, pos); (* = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))"*)
13.32 val pp = par_pblobj pt p
13.33 val {errpats, scr = Prog prog, ...} = get_met (get_obj g_metID pt pp)
13.34 - val ScrState (env, _, _, _, _, _) = get_istate pt pos
13.35 + val Pstate (env, _, _, _, _, _) = get_istate pt pos
13.36 val subst = get_bdv_subst prog env
13.37 val errpatthms = errpats
13.38 |> filter ((curry op = errpatID) o (#1: errpat -> errpatID))
14.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Thu Aug 22 11:26:14 2019 +0200
14.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Thu Aug 22 12:18:58 2019 +0200
14.3 @@ -45,14 +45,14 @@
14.4 val PblObj {meth=itms, ...} = get_obj I pt p;
14.5 val thy' = get_obj g_domID pt p;
14.6 val thy = assoc_thy thy';
14.7 - val (is as Istate.ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate ctxt itms mI;
14.8 + val (is as Istate.Pstate (env,_,_,_,_,_), ctxt, sc) = init_pstate ctxt itms mI;
14.9 val ini = init_form thy sc env;
14.10 val p = lev_dn p;
14.11 ini = NONE; (*true*)
14.12 val (m', (is', ctxt'), _) = determine_next_tactic (thy', srls) (pt, (p, Res)) sc (is, ctxt);
14.13 val d = e_rls (*FIXME: get simplifier from domID*);
14.14 "~~~~~ fun locate_input_tactic, args:"; val ((ts as (thy',srls)), (m:Tactic.T), ((pt,p):ctree * pos'),
14.15 - (scr as Prog (h $ body),d), (Istate.ScrState (E,l,a,v,S,b), ctxt)) =
14.16 + (scr as Prog (h $ body),d), (Istate.Pstate (E,l,a,v,S,b), ctxt)) =
14.17 ((thy',srls), m', (pt,(p, Res)), (sc,d), (is', ctxt'));
14.18 val thy = assoc_thy thy';
14.19 l = [] orelse ((*init.in solve..Apply_Method...*)
14.20 @@ -139,7 +139,7 @@
14.21 {errpats, nrls, scr = Rule.Prog prog, ...} => (errpats, nrls, prog)
14.22 | _ => error "inform: uncovered case of get_met"
14.23 val env = case Ctree.get_istate pt pos of
14.24 - Istate.ScrState (env, _, _, _, _, _) => env
14.25 + Istate.Pstate (env, _, _, _, _, _) => env
14.26 | _ => error "inform: uncovered case of get_istate"
14.27 in
14.28 case Inform.check_error_patterns (f_pred, f_in) (prog, env) (errpats, nrls) of
14.29 @@ -262,9 +262,9 @@
14.30 (*case*) execute_progr_2 srls m cstate (progr, e_rls(*!!!*)) (istate, ctxt)(*of*);
14.31 (*if*) strong_ass; (*then*)
14.32
14.33 - Safe_Step ((ctree, pos'), Istate.ScrState is, get_ctxt ctree pos', tac'); (*return value*)
14.34 + Safe_Step ((ctree, pos'), Istate.Pstate is, get_ctxt ctree pos', tac'); (*return value*)
14.35 "~~~~~ from locate_input_tactic to solve return:"; val Safe_Step (cstate, istate, ctxt, tac)
14.36 - = (*xxxxx_xx*)(**)Safe_Step ((ctree, pos'), Istate.ScrState is, get_ctxt ctree pos', tac')(**);
14.37 + = (*xxxxx_xx*)(**)Safe_Step ((ctree, pos'), Istate.Pstate is, get_ctxt ctree pos', tac')(**);
14.38
14.39 ([(tac_2tac tac, tac, (snd cstate, (istate, ctxt)))], [(*ctree NOT cut*)], cstate); (*return value*)
14.40 "~~~~~ from solve to loc_solve_ return:"; val ((msg, cs' : calcstate'))
15.1 --- a/test/Tools/isac/Interpret/mathengine.sml Thu Aug 22 11:26:14 2019 +0200
15.2 +++ b/test/Tools/isac/Interpret/mathengine.sml Thu Aug 22 12:18:58 2019 +0200
15.3 @@ -69,11 +69,11 @@
15.4 TO loc : (istate * ctxt) option * (istate * ctxt) option,
15.5 e.g.
15.6 FROM val pt = Nd (PblObj
15.7 - {.., loc = (SOME (ScrState ([], [], NONE, Const ("empty", "'a"), Sundef, false)),
15.8 + {.., loc = (SOME (Pstate ([], [], NONE, Const ("empty", "'a"), Sundef, false)),
15.9 NONE),
15.10 TO val pt = Nd (PblObj
15.11 {.., loc =
15.12 - ((SOME (ScrState ([], [], NONE, Const ("empty", "'a"), Sundef, false)), ctxt),
15.13 + ((SOME (Pstate ([], [], NONE, Const ("empty", "'a"), Sundef, false)), ctxt),
15.14 NONE),
15.15 *)
15.16
15.17 @@ -130,7 +130,7 @@
15.18 val PblObj{meth=itms,...} = get_obj I pt p;
15.19 val thy' = get_obj g_domID pt p;
15.20 val thy = assoc_thy thy';
15.21 - val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI;
15.22 + val (is as Pstate (env,_,_,_,_,_), ctxt, sc) = init_pstate thy itms mI;
15.23
15.24 "----- go on in the calculation";
15.25 val (p,_,f,nxt,_,pt) = me nxt pos [1] pt;
15.26 @@ -592,7 +592,7 @@
15.27 val ctxt = get_ctxt pt pos
15.28 (*rls = Rls {calc = [], erls = ...*)
15.29 val is = init_istate tac t
15.30 - (*TODO.WN060602 ScrState (["(t_, Problem (Isac,[equation,univar]))"]
15.31 + (*TODO.WN060602 Pstate (["(t_, Problem (Isac,[equation,univar]))"]
15.32 is wrong for simpl, but working ?!? *)
15.33 val tac_ = Apply_Method' (e_metID(*WN0402: see generate1 !?!*), SOME t, is, ctxt)
15.34 val pos' = ((lev_on o lev_dn) p, Frm)
15.35 @@ -616,7 +616,7 @@
15.36 val (tac_,is,(t,_)) = determine_next_tactic (thy',srls) (pt,pos) sc is;
15.37 (*tac_ = Rewrite' (..., ("rnorm_equation_add", "Test.rnorm_equation_add"), ...) !!!!!!!!!!!!!!!!*)
15.38 "~~~~~ fun determine_next_tactic, args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'),
15.39 - (sc as Prog (h $ body)), (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
15.40 + (sc as Prog (h $ body)), (Pstate (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
15.41 l = [] = false;
15.42 nstep_up thy ptp sc E l Skip_ a v (*--> Appy (Rewrite' (.., (.., "Test.rnorm_equation_add"), ...)
15.43 BUT WE FIND IN THE CODE ABOVE IN determine_next_tactic:*)
16.1 --- a/test/Tools/isac/Interpret/script.sml Thu Aug 22 11:26:14 2019 +0200
16.2 +++ b/test/Tools/isac/Interpret/script.sml Thu Aug 22 12:18:58 2019 +0200
16.3 @@ -15,7 +15,7 @@
16.4 "----------- fun dsc_valT ----------------------------------------";
16.5 "----------- fun itms2args ---------------------------------------";
16.6 "----------- fun rep_tac_ ----------------------------------------";
16.7 -"----------- fun init_scrstate -----------------------------------------------------------------";
16.8 +"----------- fun init_pstate -----------------------------------------------------------------";
16.9 "-----------------------------------------------------------------";
16.10 "-----------------------------------------------------------------";
16.11 "-----------------------------------------------------------------";
16.12 @@ -111,7 +111,7 @@
16.13 val PblObj {meth=itms, ...} = get_obj I pt p;
16.14 val thy' = get_obj g_domID pt p;
16.15 val thy = assoc_thy thy';
16.16 -val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate ctxt itms mI;
16.17 +val (is as Pstate (env,_,_,_,_,_), ctxt, sc) = init_pstate ctxt itms mI;
16.18 val ini = init_form thy sc env;
16.19 "----- fun init_form, args:"; val (Prog sc) = sc;
16.20 "----- fun get_stac, args:"; val (y, h $ body) = (thy, sc);
16.21 @@ -204,7 +204,7 @@
16.22 then (thd3 o snd3) (get_obj g_origin pt pp)
16.23 else metID
16.24 val {scr=Prog sc,srls,erls,rew_ord'=ro,...} = get_met metID'
16.25 - val ScrState (env,_,a,v,_,_) = get_istate pt (p,p_)
16.26 + val Pstate (env,_,a,v,_,_) = get_istate pt (p,p_)
16.27 val alltacs = (*we expect at least 1 stac in a script*)
16.28 map ((stac2tac pt thy) o rep_stacexpr o #2 o
16.29 (handle_leaf "selrul" thy' srls env a v)) (stacpbls sc)
16.30 @@ -386,9 +386,9 @@
16.31 > lhs'=lhs;
16.32 val it = true : bool*)
16.33
16.34 -"----------- fun init_scrstate -----------------------------------------------------------------";
16.35 -"----------- fun init_scrstate -----------------------------------------------------------------";
16.36 -"----------- fun init_scrstate -----------------------------------------------------------------";
16.37 +"----------- fun init_pstate -----------------------------------------------------------------";
16.38 +"----------- fun init_pstate -----------------------------------------------------------------";
16.39 +"----------- fun init_pstate -----------------------------------------------------------------";
16.40 val fmz = ["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
16.41 "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",
16.42 "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
16.43 @@ -412,11 +412,11 @@
16.44
16.45 (*+*)val PblObj {meth, spec = (thy, _ , metID), ...} = get_obj I pt''''' (fst p''''');
16.46 (*+*)val ctxt = get_ctxt pt''''' p''''';
16.47 -"~~~~~ fun init_scrstate , args:"; val (thy, itms, metID) = (assoc_thy thy, meth, metID);
16.48 -val (ScrState st, ctxt, Prog _) = init_scrstate ctxt itms metID;
16.49 +"~~~~~ fun init_pstate , args:"; val (thy, itms, metID) = (assoc_thy thy, meth, metID);
16.50 +val (Pstate st, ctxt, Prog _) = init_pstate ctxt itms metID;
16.51 if scrstate2str st =
16.52 "([\"\n(l, L)\",\"\n(q, q_0)\",\"\n(v, x)\",\"\n(b, dy)\",\"\n(s, [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0])\",\"\n(vs, [c, c_2, c_3, c_4])\",\"\n(id_abl, y)\"], [], NONE, \n??.empty, Safe, true)"
16.53 -then () else error "init_scrstate changed for Biegelinie";
16.54 +then () else error "init_pstate changed for Biegelinie";
16.55
16.56 (*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' c pt'''''; (*nxt = Model_Problem*)
16.57 if p = ([1], Pbl) andalso (fst nxt) = "Model_Problem" then ()
17.1 --- a/test/Tools/isac/Knowledge/biegelinie-3.sml Thu Aug 22 11:26:14 2019 +0200
17.2 +++ b/test/Tools/isac/Knowledge/biegelinie-3.sml Thu Aug 22 12:18:58 2019 +0200
17.3 @@ -99,9 +99,9 @@
17.4 | _ => error "solve Apply_Method: uncovered case get_obj"
17.5 val thy' = get_obj g_domID pt p;
17.6 val thy = Celem.assoc_thy thy';
17.7 - val (is, env, ctxt, sc) = case Lucin.init_scrstate ctxt itms mI of
17.8 - (is as Istate.ScrState (env,_,_,_,_,_), ctxt, sc) => (is, env, ctxt, sc)
17.9 - | _ => error "solve Apply_Method: uncovered case init_scrstate"
17.10 + val (is, env, ctxt, sc) = case Lucin.init_pstate ctxt itms mI of
17.11 + (is as Istate.Pstate (env,_,_,_,_,_), ctxt, sc) => (is, env, ctxt, sc)
17.12 + | _ => error "solve Apply_Method: uncovered case init_pstate"
17.13 val ini = Lucin.init_form thy sc env;
17.14 val p = lev_dn p;
17.15 val NONE = (*case*) ini (*of*);
17.16 @@ -121,7 +121,7 @@
17.17 AbleitungBiegelinie
17.18 *)
17.19 "~~~~~ fun locate_input_tactic , args:"; val ((thy', srls), m, (pt, p),
17.20 - (scr as Rule.Prog sc, d), (Istate.ScrState (E,l,a,v,S,b), ctxt)) =
17.21 + (scr as Rule.Prog sc, d), (Istate.Pstate (E,l,a,v,S,b), ctxt)) =
17.22 ((thy',srls), m', (pt,(p, Res)), (sc,d), (is', ctxt'));
17.23 val thy = Celem.assoc_thy thy';
17.24 (*if*) l = [] orelse (
18.1 --- a/test/Tools/isac/Knowledge/polyeq.sml Thu Aug 22 11:26:14 2019 +0200
18.2 +++ b/test/Tools/isac/Knowledge/polyeq.sml Thu Aug 22 12:18:58 2019 +0200
18.3 @@ -195,7 +195,7 @@
18.4 (*locate_input_tactic (thy',srls) m (pt,(p,p_)) (sc,d) is;
18.5 WAS: not-found-in-script: NotLocatable from NasNap (Const ("List...*)
18.6 "~~~~~ fun locate_input_tactic, args:"; val ((ts as (thy',srls)), (m:Tactic.T), ((pt,p):ctree * pos'),
18.7 - (scr as Prog (h $ body),d), (ScrState (E,l,a,v,S,b), ctxt)) =
18.8 + (scr as Prog (h $ body),d), (Pstate (E,l,a,v,S,b), ctxt)) =
18.9 ((thy',srls), m ,(pt,(p,p_)) ,(sc,d) ,is); (* locate_input_tactic 2nd pattern *)
18.10 val thy = assoc_thy thy';
18.11 l = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*false*);
19.1 --- a/test/Tools/isac/Knowledge/rateq.sml Thu Aug 22 11:26:14 2019 +0200
19.2 +++ b/test/Tools/isac/Knowledge/rateq.sml Thu Aug 22 12:18:58 2019 +0200
19.3 @@ -105,7 +105,7 @@
19.4 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*)
19.5 "~~~~~ fun determine_next_tactic, args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'),
19.6 (sc as Prog (h $ body)),
19.7 -(ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
19.8 +(Pstate (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
19.9 "~~~~~ fun nstep_up, args:"; val (thy, ptp, (Prog sc), E, l, ay, a, v) =
19.10 (thy, ptp, sc, E, l, Skip_, a, v);
19.11 1 < length l; (*true*)
19.12 @@ -281,7 +281,7 @@
19.13 val thy' = get_obj g_domID pt (par_pblobj pt p);
19.14 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
19.15 "~~~~~ fun determine_next_tactic, args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'),
19.16 - (sc as Prog (h $ body)), (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
19.17 + (sc as Prog (h $ body)), (Pstate (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
19.18 l = []; (* = false*)
19.19 "~~~~~ and nstep_up, args:"; val (thy, ptp, (Prog sc), E, l, ay, a, v) =
19.20 (thy, ptp, sc, E, l, Skip_, a, v);
20.1 --- a/test/Tools/isac/Minisubpbl/200-start-method.sml Thu Aug 22 11:26:14 2019 +0200
20.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method.sml Thu Aug 22 12:18:58 2019 +0200
20.3 @@ -58,8 +58,8 @@
20.4 val {srls, pre, prls, ...} = get_met mI;
20.5 val pres = check_preconds thy prls pre meth |> map snd;
20.6 val ctxt = ctxt |> insert_assumptions pres;
20.7 -val (is'''' as ScrState (env'''',_,_,_,_,_), _, sc'''') = init_scrstate ctxt meth mI;
20.8 -"~~~~~ fun init_scrstate , args:"; val (thy, itms, metID) = (thy, meth, mI)
20.9 +val (is'''' as Pstate (env'''',_,_,_,_,_), _, sc'''') = init_pstate ctxt meth mI;
20.10 +"~~~~~ fun init_pstate , args:"; val (thy, itms, metID) = (thy, meth, mI)
20.11 val actuals = itms2args thy metID itms
20.12 val scr as Prog sc = (#scr o get_met) metID
20.13 val formals = formal_args sc
20.14 @@ -131,7 +131,7 @@
20.15 val thy' = get_obj g_domID pt (par_pblobj pt p);
20.16 val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
20.17 "~~~~~ fun determine_next_tactic, args:"; val (thy, (ptp as (pt, (p, _))), (sc as Rule.Prog (_ $ body)),
20.18 - (Istate.ScrState (E,l,a,v,s,_), ctxt)) = ((thy', srls), (pt, pos), sc, is);
20.19 + (Istate.Pstate (E,l,a,v,s,_), ctxt)) = ((thy', srls), (pt, pos), sc, is);
20.20 l = [] (* = true*);
20.21 "~~~~~ fun appy, args:"; val (thy, ptp, E, l, (Const ("HOL.Let",_) $ e $ (Abs (i,T,b))), a, v) =
20.22 (thy, ptp, E, [Celem.R], body, NONE, v);
21.1 --- a/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Thu Aug 22 11:26:14 2019 +0200
21.2 +++ b/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Thu Aug 22 12:18:58 2019 +0200
21.3 @@ -53,7 +53,7 @@
21.4 val srls = get_simplifier cstate;
21.5
21.6 (*case*) execute_progr_2 srls m cstate (progr, e_rls(*!!!*)) (istate, ctxt)(*of*);
21.7 -"~~~~~ fun execute_progr_2 , args:"; val (((*thy',*) srls), m, (pt, p), (scr as Rule.Prog sc, d), (Istate.ScrState (E,l,a,v,S,b), ctxt))
21.8 +"~~~~~ fun execute_progr_2 , args:"; val (((*thy',*) srls), m, (pt, p), (scr as Rule.Prog sc, d), (Istate.Pstate (E,l,a,v,S,b), ctxt))
21.9 = (srls, m, cstate, (progr, e_rls(*!!!*)), (istate, ctxt));
21.10 (*if*)l = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*then*);
21.11
21.12 @@ -118,7 +118,7 @@
21.13 (* isabisac17: val (tac_, is, (t, _)) = determine_next_tactic (thy', srls) (pt, pos) sc is;
21.14 go: no [L,L,R] *)
21.15 "~~~~~ fun determine_next_tactic, args:"; val (thy, (ptp as (pt, (p, _))), (sc as Prog (_ $ body)),
21.16 - (ScrState (E,l,a,v,s,_), ctxt) ) = ((thy', srls), (pt, pos), sc, is);
21.17 + (Pstate (E,l,a,v,s,_), ctxt) ) = ((thy', srls), (pt, pos), sc, is);
21.18 (*if*) l = [] = false;
21.19
21.20 (* isabisac17: nstep_up thy ptp sc E l Skip_ a v ERROR go: no [L,L,R] *)
21.21 @@ -175,12 +175,12 @@
21.22 val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
21.23
21.24 (*val (tac_, is, (t, _)) =*) determine_next_tactic (thy', srls) (pt, pos) sc is;
21.25 -"~~~~~ fun determine_next_tactic , args:"; val (thy, (ptp as (pt, (p, _))), sc, (Istate.ScrState (E,l,a,v,s,_), ctxt))
21.26 +"~~~~~ fun determine_next_tactic , args:"; val (thy, (ptp as (pt, (p, _))), sc, (Istate.Pstate (E,l,a,v,s,_), ctxt))
21.27 = ((thy', srls), (pt, pos), sc, is);
21.28
21.29 - (*case*) execute_progr_1 thy ptp sc (Istate.ScrState (E,l,a,v,s,false)) (*of*);
21.30 -"~~~~~ fun execute_progr_1 , args:"; val (thy, ptp, (sc as Rule.Prog prog), (Istate.ScrState (E, l, a, v, _, _)))
21.31 - = (thy, ptp, sc, (Istate.ScrState (E,l,a,v,s,false)));
21.32 + (*case*) execute_progr_1 thy ptp sc (Istate.Pstate (E,l,a,v,s,false)) (*of*);
21.33 +"~~~~~ fun execute_progr_1 , args:"; val (thy, ptp, (sc as Rule.Prog prog), (Istate.Pstate (E, l, a, v, _, _)))
21.34 + = (thy, ptp, sc, (Istate.Pstate (E,l,a,v,s,false)));
21.35 (*if*) l = [] (*else*);
21.36
21.37 nstep_up thy ptp sc E l Skip_ a v;
22.1 --- a/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Thu Aug 22 11:26:14 2019 +0200
22.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Thu Aug 22 12:18:58 2019 +0200
22.3 @@ -43,7 +43,7 @@
22.4 val srls = get_simplifier cstate;
22.5
22.6 (*case*) execute_progr_2 srls m cstate (progr, e_rls(*!!!*)) (istate, ctxt)(*of*);
22.7 -"~~~~~ fun execute_progr_2 , args:"; val (((*thy',*) srls), m, (pt, p), (scr as Rule.Prog sc, d), (Istate.ScrState (E,l,a,v,S,b), ctxt))
22.8 +"~~~~~ fun execute_progr_2 , args:"; val (((*thy',*) srls), m, (pt, p), (scr as Rule.Prog sc, d), (Istate.Pstate (E,l,a,v,S,b), ctxt))
22.9 = (srls, m, cstate, (progr, e_rls(*!!!*)), (istate, ctxt));
22.10 (*if*)l = [] orelse ((*init.in solve..Apply_Method...*)
22.11 (last_elem o fst) p = 0 andalso snd p = Res) (*else*);
22.12 @@ -121,7 +121,7 @@
22.13 | _ => error ("assy: call by " ^ pos'2str (p,p_));
22.14 (**)val Lucin.Ass (m, v', ctxt) = (*case*) Lucin.associate pt ctxt m stac (*of*);
22.15 val (p'',c',f',pt') =
22.16 - Generate.generate1 (Celem.assoc_thy "Isac") m (Istate.ScrState (E,l,a',v',S,true), ctxt) (p',p_) pt;
22.17 + Generate.generate1 (Celem.assoc_thy "Isac") m (Istate.Pstate (E,l,a',v',S,true), ctxt) (p',p_) pt;
22.18
22.19 (*+*)if is_e_ctxt ctxt then error "ERROR: assy returns e_ctxt" else ();
22.20 (*\\--1 end step into relevant call ----------------------------------------------------------//*)
23.1 --- a/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Thu Aug 22 11:26:14 2019 +0200
23.2 +++ b/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Thu Aug 22 12:18:58 2019 +0200
23.3 @@ -54,7 +54,7 @@
23.4 val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
23.5 val thy' = get_obj g_domID pt p;
23.6 val thy = assoc_thy thy';
23.7 - val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate ctxt itms mI;
23.8 + val (is as Pstate (env,_,_,_,_,_), ctxt, sc) = init_pstate ctxt itms mI;
23.9 (*dont take ctxt ^^^ from ^^^^^^^^^^^^^*)
23.10
23.11 (*+*)val (pt, p) = case locatetac tac (pt, pos) of
23.12 @@ -73,7 +73,7 @@
23.13 val thy' = get_obj g_domID pt (par_pblobj pt p);
23.14 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
23.15 "~~~~~ fun determine_next_tactic, args:"; val (thy, (ptp as (pt,(p,_)):ctree * pos'), (sc as Prog (h $ body)),
23.16 - (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
23.17 + (Pstate (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
23.18
23.19 (*+*)val SOME t = parseNEW (get_ctxt pt pos) "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
23.20
24.1 --- a/test/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml Thu Aug 22 11:26:14 2019 +0200
24.2 +++ b/test/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml Thu Aug 22 12:18:58 2019 +0200
24.3 @@ -59,7 +59,7 @@
24.4 handle _ => [] (*FIXME.WN030527 asms in subpbls not completely clear*)
24.5 val metID = get_obj g_metID pt pp;
24.6 val {srls=srls,scr=sc,...} = get_met metID;
24.7 - val loc as (ScrState (E,l,a,_,_,b), ctxt) = get_loc pt (p,p_);
24.8 + val loc as (Pstate (E,l,a,_,_,b), ctxt) = get_loc pt (p,p_);
24.9 val thy' = get_obj g_domID pt pp;
24.10 val thy = assoc_thy thy';
24.11 val (_,_,(scval,scsaf)) = determine_next_tactic (thy',srls) (pt,(p,p_)) sc loc;
24.12 @@ -69,10 +69,10 @@
24.13 val thy = assoc_thy thy';
24.14 val metID = get_obj g_metID pt ppp;
24.15 val {scr,...} = get_met metID;
24.16 - val (ScrState (E,l,a,_,_,b), ctxt') = get_loc pt (pp(*!/p/*),Frm)
24.17 + val (Pstate (E,l,a,_,_,b), ctxt') = get_loc pt (pp(*!/p/*),Frm)
24.18 val ctxt'' = from_subpbl_to_caller ctxt scval ctxt'
24.19 val tac_ = Check_Postcond' (pI, (scval, asm))
24.20 - val is = ScrState (E,l,a,scval,scsaf,b);
24.21 + val is = Pstate (E,l,a,scval,scsaf,b);
24.22 "~~~~~ fun generate1, args:"; val (thy, (Check_Postcond' (pI, (scval, asm))), l, (p,p_), pt) =
24.23 (thy, tac_, (is, ctxt''), (pp, Res), pt);
24.24 val (pt,c) = append_result pt p l (scval, (*map str2term*) asm) Complete;
25.1 --- a/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Thu Aug 22 11:26:14 2019 +0200
25.2 +++ b/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Thu Aug 22 12:18:58 2019 +0200
25.3 @@ -56,7 +56,7 @@
25.4 val thy' = get_obj g_domID pt (par_pblobj pt p);
25.5 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*)
25.6 "~~~~~ fun determine_next_tactic, args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'), (sc as Prog (h $ body)),
25.7 -(ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
25.8 +(Pstate (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
25.9 val ctxt = get_ctxt pt pos
25.10 val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
25.11 l; (*= [R, R, D, L, R]*)
26.1 --- a/test/Tools/isac/Minisubpbl/700-interSteps.sml Thu Aug 22 11:26:14 2019 +0200
26.2 +++ b/test/Tools/isac/Minisubpbl/700-interSteps.sml Thu Aug 22 12:18:58 2019 +0200
26.3 @@ -113,7 +113,7 @@
26.4 (* val (tac_, is, (t, _)) =*) determine_next_tactic (thy', srls) (pt, pos) sc is;
26.5 ;
26.6 "~~~~~ fun determine_next_tactic, args:"; val (thy, (ptp as (pt, (p, _))), (sc as Rule.Prog (_ $ body)),
26.7 - (Istate.ScrState (E,l,a,v,s,_), ctxt)) = ((thy', srls), (pt, pos), sc, is);
26.8 + (Istate.Pstate (E,l,a,v,s,_), ctxt)) = ((thy', srls), (pt, pos), sc, is);
26.9 (*if*) l = [] (* = true *);
26.10 appy thy ptp E [Celem.R] body NONE v;
26.11
27.1 --- a/test/Tools/isac/Test_Some.thy Thu Aug 22 11:26:14 2019 +0200
27.2 +++ b/test/Tools/isac/Test_Some.thy Thu Aug 22 12:18:58 2019 +0200
27.3 @@ -114,7 +114,7 @@
27.4 (*+*)then () else error "BEFORE 1 changed";
27.5 \<close> ML \<open>
27.6 (*//--1 begin step into relevant call -------------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^---\\
27.7 - 1 relevant for init_scrstate in root-pbl*)
27.8 + 1 relevant for init_pstate in root-pbl*)
27.9 (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt''''';
27.10 (*\\--1 end step into relevant call ----------------------------------------------------------//*)
27.11 \<close> ML \<open>