1.1 --- a/src/Tools/isac/Interpret/inform.sml Sun Oct 27 12:10:57 2019 +0100
1.2 +++ b/src/Tools/isac/Interpret/inform.sml Wed Oct 30 11:02:41 2019 +0100
1.3 @@ -437,7 +437,7 @@
1.4 {errpats, scr = Rule.Prog prog, ...} => (errpats, prog)
1.5 | _ => error "find_fillpatterns: uncovered case of get_met"
1.6 val env = case Ctree.get_istate pt pos of
1.7 - Istate.Pstate (env, _, _, _, _, _) => env
1.8 + Istate.Pstate pst => Istate.get_env pst
1.9 | _ => error "find_fillpatterns: uncovered case of get_istate"
1.10 val subst = Rtools.get_bdv_subst prog env
1.11 val errpatthms = errpats
2.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Sun Oct 27 12:10:57 2019 +0100
2.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Wed Oct 30 11:02:41 2019 +0100
2.3 @@ -255,11 +255,11 @@
2.4 in
2.5 case m of (*TODO?: make applicable_in..Subproblem analogous to other tacs ?refine problem?*)
2.6 Tactic.Subproblem _ => Appy (m', (
2.7 - get_env ist, get_path ist, a', Lucin.tac_2res m', Istate.AppUndef_, false))
2.8 + get_env ist, get_path ist, get_rls ist, a', Lucin.tac_2res m', Istate.AppUndef_, false))
2.9 | _ =>
2.10 (case Applicable.applicable_in p pt m of
2.11 Chead.Appl m' => (Appy (m', (
2.12 - get_env ist, get_path ist, a', Lucin.tac_2res m', Istate.AppUndef_, false)))
2.13 + get_env ist, get_path ist, get_rls ist, a', Lucin.tac_2res m', Istate.AppUndef_, false)))
2.14 | _ => Napp (get_env ist))
2.15 end
2.16 (*end*)
2.17 @@ -479,10 +479,10 @@
2.18 | nstep_up _ _ _ ist _ = error ("nstep_up: uncovered fun-def at " ^ Celem.loc_2str (get_path ist))
2.19 (*end*)
2.20
2.21 -fun execute_progr_1 thy ptp (sc as Rule.Prog prog) (Istate.Pstate (E, l, a, v, _, _)) =
2.22 +fun execute_progr_1 thy ptp (sc as Rule.Prog prog) (Istate.Pstate (E, l, rls, a, v, _, _)) =
2.23 if l = []
2.24 - then appy thy ptp (E, [R], NONE, v, AppUndef_, false) (Program.body_of prog)
2.25 - else nstep_up thy ptp sc (E, l, a, v, AppUndef_, false) Skip_
2.26 + then appy thy ptp (E, [R], rls, NONE, v, AppUndef_, false) (Program.body_of prog)
2.27 + else nstep_up thy ptp sc (E, l, rls, a, v, AppUndef_, false) Skip_
2.28 | execute_progr_1 _ _ _ _ = raise ERROR "execute_progr_1: uncovered pattern";
2.29
2.30 (* decide for the next applicable stac in the program;
2.31 @@ -502,8 +502,8 @@
2.32 (Istate.Uistate, ctxt), (Rule.e_term, Istate.Sundef)) (*next stac*)
2.33 | _ => error "determine_next_tactic: uncovered case next_rule")
2.34 -----*)
2.35 -fun determine_next_tactic thy (ptp as (pt, (p, _))) sc (Istate.Pstate (E,l,a,v,s,_), ctxt) =
2.36 - (case execute_progr_1 thy ptp sc (Istate.Pstate (E,l,a,v,s,false)) of
2.37 +fun determine_next_tactic thy (ptp as (pt, (p, _))) sc (Istate.Pstate (E,l,rls,a,v,s,_), ctxt) =
2.38 + (case execute_progr_1 thy ptp sc (Istate.Pstate (E,l,rls,a,v,s,false)) of
2.39 Skip (v, _) => (* program finished *)
2.40 (case par_pbl_det pt p of
2.41 (true, p', _) =>
2.42 @@ -517,7 +517,7 @@
2.43 (Tactic.End_Detail' (Rule.e_term,[])(*8.6.03*), (Istate.e_istate, ctxt), (v, Telem.Safe)))
2.44 | Napp _ =>
2.45 (Tactic.Empty_Tac_, (Istate.e_istate, ctxt), (Rule.e_term, Telem.Helpless_))(* helpless *)
2.46 - | Appy (m', scrst as (_,_,_,v,_,_)) =>
2.47 + | Appy (m', scrst as (_,_,_,_,v,_,_)) =>
2.48 (m', (Istate.Pstate scrst, ctxt), (v, Telem.Safe))) (* found next tac *)
2.49 | determine_next_tactic _ _ _ (is, _) =
2.50 error ("determine_next_tactic: not impl for " ^ (Istate.istate2str is));
2.51 @@ -597,10 +597,10 @@
2.52 then assy ya ((E, l @ [R], a,v,S,b),ss) e
2.53 else NasNap (v, E)
2.54 ( *NEW..*)
2.55 - | assy (ya as (_, srls, _, _)) ((E,l,a,v,S,b),ss) (Const ("Tactical.While"(*2*),_) $ c $ e) =
2.56 - if Rewrite.eval_true_ "Isac_Knowledge" srls (subst_atomic (Env.upd_env_opt E (a,v)) c)
2.57 - then assy ya ((E, l @ [Celem.R], a,v,S,b),ss) e
2.58 - else NasNap (v, E)
2.59 + | assy (ya as (_, srls, _, _)) (ist, ss) (Const ("Tactical.While"(*2*),_) $ c $ e) =
2.60 + if Rewrite.eval_true_ "Isac_Knowledge" srls (subst_atomic (Env.upd_env_opt' (get_subst ist)) c)
2.61 + then assy ya (ist |> path_down [R], ss) e
2.62 + else NasNap (ist |> get_act_env)
2.63 (*4* )
2.64 | assy ya ((E,l,_,v,S,b),ss) (Const ("Tactical.Try"(*1*),_) $ e $ a) =
2.65 (case assy ya ((E, l @ [L, R], SOME a,v,S,b),ss) e of ay => ay)
2.66 @@ -763,14 +763,14 @@
2.67 | NasNap (v, E) => astep_up ys (ist |> path_up |> upd_act_env (v, E), ss)
2.68 end
2.69 (*2*)
2.70 - | ass_up ys iss (Abs(*2*) (_,_,_)) = astep_up ys iss
2.71 + | ass_up ys iss (Abs(*2*) (_, _, _)) = astep_up ys iss
2.72 (*3*)
2.73 | ass_up ys iss (Const ("HOL.Let"(*3*),_) $ _ $ (Abs _)) = astep_up ys iss
2.74 (*4*)
2.75 - | ass_up ysa iss (Const ("Tactical.Seq"(*1*),_) $ _ $ _ $ _) =
2.76 + | ass_up ysa iss (Const ("Tactical.Seq"(*1*), _) $ _ $ _ $ _) =
2.77 astep_up ysa iss (*all has been done in (*2*) below*)
2.78 (*5*)
2.79 - | ass_up ysa iss (Const ("Tactical.Seq"(*2*),_) $ _ $ _) =
2.80 + | ass_up ysa iss (Const ("Tactical.Seq"(*2*), _) $ _ $ _) =
2.81 astep_up ysa iss (*2*: comes from e2*)
2.82 (*6* )
2.83 | ass_up (ysa as (ctxt,s,Rule.Prog sc, cstate)) ((E,l,a,v,S,b),ss)
2.84 @@ -897,10 +897,10 @@
2.85 | astep_up _ (ist, _) = error ("astep_up: uncovered fun-def with " ^ Celem.loc_2str (get_path ist))
2.86 (*end*)
2.87
2.88 -fun execute_progr_2 srls m (pt, p) (scr as Rule.Prog sc, _) (Istate.Pstate (E,l,a,v,S,b), ctxt) =
2.89 - if l = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res)
2.90 - then assy (ctxt,srls, (pt, p), Aundef) ((E,[R],a,v,S,b), m) (Program.body_of sc)
2.91 - else astep_up (ctxt,srls,scr, (pt, p)) ((E,l,a,v,S,b), m)
2.92 +fun execute_progr_2 srls m (pt, p) (scr as Rule.Prog sc, _) (Istate.Pstate ist, ctxt) =
2.93 + if get_path ist = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res)
2.94 + then assy (ctxt,srls, (pt, p), Aundef) (ist |> upd_path [R], m) (Program.body_of sc)
2.95 + else astep_up (ctxt,srls,scr, (pt, p)) (ist, m)
2.96 | execute_progr_2 _ _ _ _ _ = raise ERROR "execute_progr_2: uncovered pattern in fun.def"
2.97
2.98 fun locate_input_tactic (progr as Rule.Prog _) cstate istate ctxt tac =
2.99 @@ -908,7 +908,7 @@
2.100 val srls = Lucin.get_simplifier cstate (*TODO: shift into Istate.T*)
2.101 in
2.102 (case execute_progr_2 srls tac cstate (progr, Rule.e_rls) (istate, ctxt) of
2.103 - Assoc (is as (_,_,_,_,_,strong_ass), ctxt, tac') =>
2.104 + Assoc (is as (_,_,_,_,_,_,strong_ass), ctxt, tac') =>
2.105 if strong_ass
2.106 then Safe_Step (Istate.Pstate is, ctxt, tac')
2.107 else Unsafe_Step (Istate.Pstate is, ctxt, tac')
2.108 @@ -950,7 +950,7 @@
2.109 else itms
2.110 (*\\----------- hack for funpack: generalise handling of meths which extend problem items -----//*)
2.111 val (is, env, ctxt, scr) = case Lucin.init_pstate ctxt itms mI of
2.112 - (is as Istate.Pstate (env,_,_,_,_,_), ctxt, scr) => (is, env, ctxt, scr)
2.113 + (is as Istate.Pstate pst, ctxt, scr) => (is, Istate.get_env pst, ctxt, scr)
2.114 | _ => error "begin_end_prog Apply_Method': uncovered case init_pstate"
2.115 val ini = Lucin.init_form thy scr env;
2.116 in
2.117 @@ -979,18 +979,19 @@
2.118 | _ => get_assumptions_ pt (p, p_))
2.119 val metID = get_obj g_metID pt pp;
2.120 val {srls = srls, scr = sc, ...} = Specify.get_met metID;
2.121 - val (loc, E, l, a, b, ctxt) = case get_loc pt (p, p_) of
2.122 - loc as (Istate.Pstate (E,l,a,_,_,b), ctxt) => (loc, E, l, a, b, ctxt)
2.123 + val (loc, pst, ctxt) = case get_loc pt (p, p_) of
2.124 + loc as (Istate.Pstate pst, ctxt) => (loc, pst, ctxt)
2.125 | _ => error "begin_end_prog Check_Postcond': uncovered case get_loc"
2.126 val thy' = get_obj g_domID pt pp;
2.127 val thy = Celem.assoc_thy thy';
2.128 - val (_, _, (scval, scsaf)) = determine_next_tactic (thy', srls) (pt, (p, p_)) sc loc;
2.129 + val (_, _, (scval, _(*scsaf*))) = determine_next_tactic (thy', srls) (pt, (p, p_)) sc loc;
2.130 (* Telem.safe should go on to Check_Postcond' vvvvv *)
2.131 in
2.132 if pp = []
2.133 then
2.134 let
2.135 - val is = Istate.Pstate (E, l, a, scval, Istate.Skip_, b)
2.136 + (*val is = Istate.Pstate (E, l, Rule.e_rls, a, scval, Istate.Skip_, b)*)
2.137 + val is = Istate.Pstate (pst |> Istate.upd_act scval |> Istate.upd_appy Istate.Skip_)
2.138 val tac_ = Tactic.Check_Postcond' (pI, (scval, asm))
2.139 (*extend Tactic.Check_Postcond' (pI, (scval, asm), scsaf) ^^^^^ *)
2.140 val ((p, p_), ps, _, pt) = Generate.generate1 thy tac_ (is, ctxt) (pp, Res) pt;
2.141 @@ -1000,12 +1001,13 @@
2.142 val ppp = par_pblobj pt (lev_up p);
2.143 val thy' = get_obj g_domID pt ppp;
2.144 val thy = Celem.assoc_thy thy';
2.145 - val (E, l, a, b, ctxt') = case get_loc pt (pp, Frm) of
2.146 - (Istate.Pstate (E,l,a,_,_,b), ctxt') => (E, l, a, b, ctxt')
2.147 +
2.148 + val (pst', ctxt') = case get_loc pt (pp, Frm) of
2.149 + (Istate.Pstate pst', ctxt') => (pst', ctxt')
2.150 | _ => error "begin_end_prog Check_Postcond' script of parpbl: uncovered case get_loc"
2.151 val ctxt'' = ContextC.from_subpbl_to_caller ctxt scval ctxt'
2.152 val tac_ = Tactic.Check_Postcond' (pI, (scval, asm))
2.153 - val is = Istate.Pstate (E,l,a,scval,Istate.Skip_,b)
2.154 + val is = Istate.Pstate (pst' |> Istate.upd_act scval |> Istate.upd_appy Istate.Skip_)
2.155 val ((p, p_), ps, _, pt) = Generate.generate1 thy tac_ (is, ctxt'') (pp, Res) pt;
2.156 in ([(Tactic.Check_Postcond pI, tac_, ((pp, Res), (is, ctxt'')))], ps, (pt, (p, p_))) end
2.157 end
3.1 --- a/src/Tools/isac/Interpret/rewtools.sml Sun Oct 27 12:10:57 2019 +0100
3.2 +++ b/src/Tools/isac/Interpret/rewtools.sml Wed Oct 30 11:02:41 2019 +0100
3.3 @@ -573,7 +573,7 @@
3.4 # otherwise []
3.5 WN060617 hack assuming that all scripts use only one bound variable
3.6 and use 'v_' as the formal argument for this bound variable*)
3.7 -fun subs_from (Istate.Pstate (env, _, _, _, _, _)) _ guh =
3.8 +fun subs_from (Istate.Pstate pst) _ guh =
3.9 let
3.10 val (_, _, thyID, sect, xstr) = case guh2theID guh of
3.11 theID as [isa, thyID, sect, xstr] => (theID, isa, thyID, sect, xstr)
3.12 @@ -586,8 +586,8 @@
3.13 if Auto_Prog.contains_bdv thm
3.14 then
3.15 let
3.16 - val formal_arg = TermC.str2term "v_"
3.17 - val value = subst_atomic env formal_arg
3.18 + val formal_arg = TermC.str2term "v_"
3.19 + val value = subst_atomic (Istate.get_env pst) formal_arg
3.20 in ["(''bdv''," ^ Rule.term2str value ^ ")"] : Selem.subs end
3.21 else []
3.22 end
3.23 @@ -599,7 +599,7 @@
3.24 then
3.25 let
3.26 val formal_arg = TermC.str2term "v_"
3.27 - val value = subst_atomic env formal_arg
3.28 + val value = subst_atomic (Istate.get_env pst) formal_arg
3.29 in ["(''bdv''," ^ Rule.term2str value ^ ")"] : Selem.subs end
3.30 else []
3.31 end
4.1 --- a/src/Tools/isac/Interpret/script.sml Sun Oct 27 12:10:57 2019 +0100
4.2 +++ b/src/Tools/isac/Interpret/script.sml Wed Oct 30 11:02:41 2019 +0100
4.3 @@ -546,12 +546,12 @@
4.4 else
4.5 let val (f, a) = assoc_by_type f aas
4.6 in relate_args (env @ [(f, a)]) ff (remove op = a aas) end
4.7 - val env = relate_args [] formals actuals;
4.8 - val _ = trace_istate env;
4.9 val {pre, prls, ...} = Specify.get_met metID;
4.10 val pres = Stool.check_preconds (Proof_Context.theory_of ctxt) prls pre itms |> map snd;
4.11 val ctxt = ctxt |> ContextC.insert_assumptions pres;
4.12 - in (Istate.Pstate (env, [], NONE, Rule.e_term, Istate.AppUndef_, true), ctxt, scr) end;
4.13 + in
4.14 + (Istate.Pstate (Istate.e_scrstate |> Istate.upd_env_true (relate_args [] formals actuals)), ctxt, scr)
4.15 + end;
4.16 end (*local*)
4.17
4.18 fun get_simplifier (pt, (p, _)) =
4.19 @@ -666,8 +666,8 @@
4.20 val metID' = if metID = Celem.e_metID then (thd3 o snd3) (get_obj g_origin pt pp) else metID
4.21 val (sc, srls) = (case Specify.get_met metID' of
4.22 {scr = Rule.Prog sc, srls, ...} => (sc, srls) | _ => error "sel_rules 1")
4.23 - val (env, a, v) = (case get_istate pt (p, p_) of
4.24 - Istate.Pstate (env, _, a, v, _, _) => (env, a, v) | _ => error "sel_rules 2")
4.25 + val (env, (a, v)) = (case get_istate pt (p, p_) of
4.26 + Istate.Pstate pst => (Istate.get_subst pst) | _ => error "sel_rules 2")
4.27 in map ((stac2tac pt thy) o Celem.rep_stacexpr o #2 o
4.28 (handle_leaf "selrul" thy' srls (env, (a, v)))) (Auto_Prog.stacpbls sc)
4.29 end;
4.30 @@ -692,8 +692,8 @@
4.31 val (sc, srls, erls, ro) = (case Specify.get_met metID' of
4.32 {scr = Rule.Prog sc, srls, erls, rew_ord' = ro, ...} => (sc, srls, erls, ro)
4.33 | _ => error "sel_appl_atomic_tacs 1")
4.34 - val (env, a, v) = (case get_istate pt (p, p_) of
4.35 - Istate.Pstate (env, _, a, v, _, _) => (env, a, v) | _ => error "sel_appl_atomic_tacs 2")
4.36 + val (env, (a, v)) = (case get_istate pt (p, p_) of
4.37 + Istate.Pstate pst => (Istate.get_subst pst) | _ => error "sel_appl_atomic_tacs 2")
4.38 val alltacs = (*we expect at least 1 stac in a script*)
4.39 map ((stac2tac pt thy) o Celem.rep_stacexpr o #2 o
4.40 (handle_leaf "selrul" thy' srls (env, (a, v)))) (Auto_Prog.stacpbls sc)
5.1 --- a/src/Tools/isac/MathEngBasic/ctree-basic.sml Sun Oct 27 12:10:57 2019 +0100
5.2 +++ b/src/Tools/isac/MathEngBasic/ctree-basic.sml Wed Oct 30 11:02:41 2019 +0100
5.3 @@ -211,8 +211,8 @@
5.4 (*val e_iist = (e_istate, e_istate); --- sinnlos f"ur NICHT-equality-type*)
5.5
5.6
5.7 -fun new_val v (Istate.Pstate (env, loc_, topt, _, safe, bool)) =
5.8 - (Istate.Pstate (env, loc_, topt, v, safe, bool))
5.9 +fun new_val v (Istate.Pstate pst) =
5.10 + (Istate.Pstate (Istate.upd_act v pst))
5.11 | new_val _ _ = error "new_val: only for Pstate";
5.12
5.13 datatype con = land | lor;
6.1 --- a/src/Tools/isac/MathEngBasic/istate.sml Sun Oct 27 12:10:57 2019 +0100
6.2 +++ b/src/Tools/isac/MathEngBasic/istate.sml Wed Oct 30 11:02:41 2019 +0100
6.3 @@ -8,7 +8,7 @@
6.4 datatype appy_ = AppUndef_ | Napp_ | Skip_
6.5 type pstate
6.6 val e_scrstate: pstate
6.7 - val scrstate2str: Rule.subst * Celem.loc_ * term option * term * appy_ * bool -> string
6.8 + val scrstate2str: Rule.subst * Celem.loc_ * Rule.rls * term option * term * appy_ * bool -> string
6.9
6.10 datatype T = RrlsState of Rule.rrlsstate | Pstate of pstate | Uistate
6.11 val istate2str: T -> string
6.12 @@ -18,6 +18,7 @@
6.13 val get_path: pstate -> Celem.loc_
6.14 val get_path_up: pstate -> Celem.loc_
6.15 val get_act: pstate -> term
6.16 + val get_rls: pstate -> Rule.rls
6.17 val get_env: pstate -> Env.T
6.18 val get_act_env: pstate -> (term * Env.T)
6.19 (*val get_form_env: pstate -> (term option * Env.T)*)
6.20 @@ -32,8 +33,12 @@
6.21 val path_up: pstate -> pstate
6.22 val path_up_down: Celem.loc_ -> pstate -> pstate
6.23
6.24 - val upd_form: term -> pstate -> pstate
6.25 + val upd_form: term -> pstate -> pstate
6.26 + val upd_path: Celem.loc_ -> pstate -> pstate
6.27 + val upd_act: term -> pstate -> pstate
6.28 + val upd_appy: appy_ -> pstate -> pstate
6.29 val upd_env: Env.T -> pstate -> pstate
6.30 + val upd_env_true: Env.T -> pstate -> pstate
6.31 val upd_env': term -> pstate -> pstate
6.32 val upd_env'': Env.T * (term * term) -> pstate -> pstate
6.33 val upd_form_env: (term * Env.T) -> pstate -> pstate
6.34 @@ -64,6 +69,7 @@
6.35 Env.T(*stack*) (* used to instantiate tac for checking associate
6.36 12.03.noticed: e_ not updated during execution ?!? *)
6.37 * Celem.loc_ (* location of tac in script *)
6.38 + * Rule.rls (* for evaluating Prog_Expr *)
6.39 * term option (*id FORMal ARGument of curried functions *)
6.40 * term (*vl ACTual ARGument (value) for execution of Tactic.T
6.41 updated also after a derivation by 'new_val' *)
6.42 @@ -71,26 +77,24 @@
6.43 * bool; (* true = strongly .., false = weakly associated:
6.44 only used during ass_dn/up *)
6.45 val e_scrstate =
6.46 - ([]: Env.T, []:Celem.loc_, SOME Rule.e_term, Rule.e_term, AppUndef_, false) : pstate
6.47 + ([]: Env.T, []:Celem.loc_, Rule.e_rls, NONE, Rule.e_term, AppUndef_, false) : pstate
6.48 fun topt2str NONE = "NONE"
6.49 | topt2str (SOME t) = "SOME" ^ Rule.term2str t;
6.50 -fun scrstate2str (env, loc_, topt, t, safe, bool) = (* for tests only *)
6.51 - "(" ^ Env.env2str env ^ ", " ^ Celem.loc_2str loc_ ^ ", " ^ topt2str topt ^ ", \n" ^
6.52 - Rule.term2str t ^ ", " ^ appy_2str safe ^ ", " ^ bool2str bool ^ ")";
6.53 +fun scrstate2str (env, loc_, rls, topt, t, safe, bool) = (* for tests only *)
6.54 + "(" ^ Env.env2str env ^ ", " ^ Celem.loc_2str loc_ ^ ", " ^ Rule.id_rls rls ^ ", " ^
6.55 + topt2str topt ^ ", \n" ^ Rule.term2str t ^ ", " ^ appy_2str safe ^ ", " ^ bool2str bool ^ ")";
6.56
6.57 (* for handling type T see fun from_pblobj_or_detail', +? *)
6.58 datatype T = (*interpreter state*)
6.59 Uistate (*undefined in modspec, in '_deriv'ation*)
6.60 | Pstate of pstate (*for script interpreter*)
6.61 | RrlsState of Rule.rrlsstate; (*for reverse rewriting*)
6.62 -val e_istate = (Pstate ([], [], NONE, Rule.e_term, AppUndef_, false));
6.63 +val e_istate = (Pstate ([], [], Rule.e_rls, NONE, Rule.e_term, AppUndef_, false));
6.64
6.65 fun rta2str (r, (t, a)) = "\n(" ^ Rule.rule2str r ^ ",(" ^ Rule.term2str t ^", " ^ Rule.terms2str a ^ "))";
6.66 fun istate2str Uistate = "Uistate"
6.67 - | istate2str (Pstate (e, l, to, t, s, b)) =
6.68 - "Pstate ("^ Env.subst2str e ^ ",\n " ^
6.69 - Celem.loc_2str l ^ ", " ^ Rule.termopt2str to ^ ",\n " ^
6.70 - Rule.term2str t ^ ", " ^ appy_2str s ^ ", " ^ bool2str b ^ ")"
6.71 + | istate2str (Pstate pst) =
6.72 + "Pstate " ^ scrstate2str pst
6.73 | istate2str (RrlsState (t, t1, rss, rtas)) =
6.74 "RrlsState (" ^ Rule.term2str t ^ ", " ^ Rule.term2str t1 ^ ", " ^
6.75 (strs2str o (map (strs2str o (map Rule.rule2str)))) rss ^ ", " ^
6.76 @@ -100,51 +104,59 @@
6.77 | istates2str (SOME ist, NONE) = "(#SOME " ^ istate2str ist ^ ",\n #NONE)"
6.78 | istates2str (SOME i1, SOME i2) = "(#SOME " ^ istate2str i1 ^ ",\n #SOME " ^ istate2str i2 ^ ")";
6.79
6.80 -fun get_path (_, path, _, _, _, _) = path
6.81 -fun get_path_up (ist as (_, path, _, _, _, _)) =
6.82 +fun get_path (_, path, _, _,_, _, _) = path
6.83 +fun get_path_up (ist as (_, path, _, _, _, _, _)) =
6.84 if length path > 1 then drop_last path else raise ERROR ("get_path_up [] with " ^ scrstate2str ist)
6.85 -fun get_act (_, _, _, act_arg, _, _) = act_arg
6.86 -fun get_env (env, _, _, _, _, _) = env
6.87 -fun get_act_env (env, _, _, act_arg, _, _) = (act_arg, env)
6.88 -(*fun get_form_env (env, _, form_arg, _, _, _) = (form_arg, env)*)
6.89 -fun get_assoc (_, _, _, _, _, ass) = ass
6.90 -fun get_subst (env, _, form_arg, act_arg, _, _) = (env, (form_arg, act_arg))
6.91 +fun get_act (_, _, _, _, act_arg, _, _) = act_arg
6.92 +fun get_rls (_, _, rls, _, _, _, _) = rls
6.93 +fun get_env (env, _, _, _, _, _, _) = env
6.94 +fun get_act_env (env, _, _, _, act_arg, _, _) = (act_arg, env)
6.95 +fun get_assoc (_, _, _, _, _, _, ass) = ass
6.96 +fun get_subst (env, _, _, form_arg, act_arg, _, _) = (env, (form_arg, act_arg))
6.97
6.98 -fun trans_ass (_, _, _, _, _, ass) (env, path, form_arg, act_arg, safe, _) =
6.99 - (env, path, form_arg, act_arg, safe, ass)
6.100 -fun trans_env_act (env, _, _, act_arg, _, _) (_, path, form_arg, _, safe, ass) =
6.101 - (env, path, form_arg, act_arg, safe, ass)
6.102 +fun trans_ass (_, _, _, _,_, _, ass) (env, path, rls, form_arg, act_arg, safe, _) =
6.103 + (env, path, rls, form_arg, act_arg, safe, ass)
6.104 +fun trans_env_act (env, _, _, _, act_arg, _, _) (_, path, rls, form_arg, _, safe, ass) =
6.105 + (env, path, rls, form_arg, act_arg, safe, ass)
6.106
6.107 -fun path_down path (env, p, form_arg, act_arg, safe, ass) =
6.108 - (env, p @ path, form_arg, act_arg, safe, ass)
6.109 -fun path_down_form (path, form_arg) (env, p, _, act_arg, safe, ass) =
6.110 - (env, p @ path, SOME form_arg, act_arg, safe, ass)
6.111 -fun path_up (env, path, form_arg, act_arg, safe, ass) =
6.112 - (env, drop_last path, form_arg, act_arg, safe, ass)
6.113 -fun path_up_down path (env, p, form_arg, act_arg, safe, ass) =
6.114 - (env, (drop_last p) @ path, form_arg, act_arg, safe, ass)
6.115 +fun path_down path (env, p, rls, form_arg, act_arg, safe, ass) =
6.116 + (env, p @ path, rls, form_arg, act_arg, safe, ass)
6.117 +fun path_down_form (path, form_arg) (env, p, rls, _, act_arg, safe, ass) =
6.118 + (env, p @ path, rls, SOME form_arg, act_arg, safe, ass)
6.119 +fun path_up (env, path, rls, form_arg, act_arg, safe, ass) =
6.120 + (env, drop_last path, rls, form_arg, act_arg, safe, ass)
6.121 +fun path_up_down path (env, p, rls, form_arg, act_arg, safe, ass) =
6.122 + (env, (drop_last p) @ path, rls, form_arg, act_arg, safe, ass)
6.123
6.124 -fun upd_form form (env, path, _, act_arg, safe, ass) =
6.125 - (env, path, SOME form, act_arg, safe, ass)
6.126 +fun upd_form form (env, path, rls, _, act_arg, safe, ass) =
6.127 + (env, path, rls, SOME form, act_arg, safe, ass)
6.128 +fun upd_path path (env, _, rls, form_arg, act_arg, safe, ass) =
6.129 + (env, path, rls, form_arg, act_arg, safe, ass)
6.130 +fun upd_act act (env, path, rls, form_arg, _, safe, ass) =
6.131 + (env, path, rls, form_arg, act, safe, ass)
6.132 +fun upd_appy app (env, path, rls, form_arg, act_arg, _, ass) =
6.133 + (env, path, rls, form_arg, act_arg, app, ass)
6.134
6.135 -fun upd_env env (_, path, form_arg, act_arg, safe, ass) =
6.136 - (env, path, form_arg, act_arg, safe, ass)
6.137 -fun upd_env' form (env, path, form_arg, act_arg, safe, ass) =
6.138 - (Env.upd_env env (form, act_arg), path, form_arg, act_arg, safe, ass)
6.139 -fun upd_env'' (env, (form, act)) (_, path, _, _, safe, ass) =
6.140 - (Env.upd_env env (form, act), path, SOME form, act, safe, ass)
6.141 +fun upd_env env (_, path, rls, form_arg, act_arg, safe, ass) =
6.142 + (env, path, rls, form_arg, act_arg, safe, ass)
6.143 +fun upd_env_true env (_, path, rls, form_arg, act_arg, safe, _) =
6.144 + (env, path, rls, form_arg, act_arg, safe, true)
6.145 +fun upd_env' form (env, path, rls, form_arg, act_arg, safe, ass) =
6.146 + (Env.upd_env env (form, act_arg), path, rls, form_arg, act_arg, safe, ass)
6.147 +fun upd_env'' (env, (form, act)) (_, path, rls, _, _, safe, ass) =
6.148 + (Env.upd_env env (form, act), path, rls, SOME form, act, safe, ass)
6.149
6.150 -fun upd_form_env (form_arg, env) (_, path, _, act_arg, safe, ass) =
6.151 - (env, path, SOME form_arg, act_arg, safe, ass)
6.152 -fun upd_act_env (act_arg, env) (_, path, form_arg, _, safe, ass) =
6.153 - (env, path, form_arg, act_arg, safe, ass)
6.154 +fun upd_form_env (form_arg, env) (_, path, rls, _, act_arg, safe, ass) =
6.155 + (env, path, rls, SOME form_arg, act_arg, safe, ass)
6.156 +fun upd_act_env (act_arg, env) (_, path, rls, form_arg, _, safe, ass) =
6.157 + (env, path, rls, form_arg, act_arg, safe, ass)
6.158
6.159 -fun upd_subst env (form_arg, act_arg) (_, path, _, _, safe, ass) =
6.160 - (env, path, SOME form_arg, act_arg, safe, ass)
6.161 -fun upd_subst_true (form_arg, act_arg) (env, path, _, _, safe, _) =
6.162 - (env, path, form_arg, act_arg, safe, true)
6.163 -fun upd_subst_false (form_arg, act_arg) (env, path, _, _, safe, _) =
6.164 - (env, path, form_arg, act_arg, safe, false)
6.165 +fun upd_subst env (form_arg, act_arg) (_, path, rls, _, _, safe, ass) =
6.166 + (env, path, rls, SOME form_arg, act_arg, safe, ass)
6.167 +fun upd_subst_true (form_arg, act_arg) (env, path, rls, _, _, safe, _) =
6.168 + (env, path, rls, form_arg, act_arg, safe, true)
6.169 +fun upd_subst_false (form_arg, act_arg) (env, path, rls, _, _, safe, _) =
6.170 + (env, path, rls, form_arg, act_arg, safe, false)
6.171
6.172 (**)end(**)
6.173
7.1 --- a/src/Tools/isac/MathEngine/solve.sml Sun Oct 27 12:10:57 2019 +0100
7.2 +++ b/src/Tools/isac/MathEngine/solve.sml Wed Oct 30 11:02:41 2019 +0100
7.3 @@ -112,7 +112,7 @@
7.4 (*FIXME.WN050821 compare solve ... begin_end_prog:
7.5 WN190811: solve ("Apply_Method",.. used by root-pbl + by locate_input_tactic !!!
7.6 *)
7.7 -fun solve ("Apply_Method", m as Tactic.Apply_Method' (mI, _, _, ctxt)) (pt, (pos as (p, p_))) =
7.8 +fun solve ("Apply_Method", m as Tactic.Apply_Method' (mI, _, _, ctxt)) (pt, (pos as (p, _))) =
7.9 let
7.10 val {srls, ...} = Specify.get_met mI;
7.11 val itms = case get_obj I pt p of
7.12 @@ -121,7 +121,7 @@
7.13 val thy' = get_obj g_domID pt p;
7.14 val thy = Celem.assoc_thy thy';
7.15 val (is, env, ctxt, sc) = case Lucin.init_pstate ctxt itms mI of
7.16 - (is as Istate.Pstate (env,_,_,_,_,_), ctxt, sc) => (is, env, ctxt, sc)
7.17 + (is as Istate.Pstate pst, ctxt, sc) => (is, Istate.get_env pst, ctxt, sc)
7.18 | _ => error "solve Apply_Method: uncovered case init_pstate"
7.19 val ini = Lucin.init_form thy sc env;
7.20 val p = lev_dn p;
7.21 @@ -153,7 +153,7 @@
7.22 (*OLD* ) ("ok", ([(Lucin.tac_2tac tac, tac, (snd cstate, (istate, ctxt)))],
7.23 (*OLD*) [(*ctree NOT cut*)], cstate))
7.24 ( *OLD*)
7.25 - | _ => (* NotLocatable *)
7.26 + | _ => (* NotLocatable, but applicable_in from the beginning *)
7.27 let
7.28 val (p, ps, _, pt) =
7.29 Generate.generate_hard (Celem.assoc_thy "Isac_Knowledge") m (p, Frm) pt;
7.30 @@ -180,18 +180,21 @@
7.31 handle _ => [] (*WN.27.5.03 asms in subpbls not completely clear*)
7.32 val metID = get_obj g_metID pt pp;
7.33 val {srls = srls, scr = sc, ...} = Specify.get_met metID;
7.34 - val (loc, E, l, a, b, ctxt) = case get_loc pt (p, p_) of
7.35 - loc as (Istate.Pstate (E, l, a, _, _, b), ctxt) => (loc, E, l, a, b, ctxt)
7.36 + val (loc, pst, ctxt) = case get_loc pt (p, p_) of
7.37 + loc as (Istate.Pstate pst, ctxt) => (loc, pst, ctxt)
7.38 | _ => error "solve Check_Postcond: uncovered case get_loc"
7.39 +
7.40 val thy' = get_obj g_domID pt pp;
7.41 val thy = Celem.assoc_thy thy';
7.42 - val (_, _, (scval, scsaf)) = LucinNEW.determine_next_tactic (thy', srls) (pt, (p, p_)) sc loc;
7.43 + val (_, _, (scval, _(*scsaf*))) = LucinNEW.determine_next_tactic (thy', srls) (pt, (p, p_)) sc loc;
7.44 + (* Telem.safe should go on to Check_Postcond' vvvvv *)
7.45 in
7.46 if pp = []
7.47 then
7.48 let
7.49 - val is = Istate.Pstate (E,l,a,scval,Istate.Skip_,b)
7.50 + val is = Istate.Pstate (pst |> Istate.upd_act scval |> Istate.upd_appy Istate.Skip_)
7.51 val tac_ = Tactic.Check_Postcond' (pI, (scval, asm))
7.52 + (*extend Tactic.Check_Postcond' (pI, (scval, asm), scsaf) ^^^^^ *)
7.53 val (pos, ps, _, pt) = Generate.generate1 thy tac_ (is, ctxt) (pp, Res) pt;
7.54 in ("ok", ([(Tactic.Check_Postcond pI, tac_, ((pp, Res), (is, ctxt)))], ps, (pt, pos))) end
7.55 else
7.56 @@ -199,14 +202,14 @@
7.57 val ppp = par_pblobj pt (lev_up p);
7.58 val thy' = get_obj g_domID pt ppp;
7.59 val thy = Celem.assoc_thy thy';
7.60 - val (E, l, a, b, ctxt') = case get_loc pt (pp, Frm) of
7.61 - (Istate.Pstate (E, l, a, _, _, b), ctxt') => (E, l, a, b, ctxt')
7.62 + val (pst', ctxt') = case get_loc pt (pp, Frm) of
7.63 + (Istate.Pstate pst', ctxt') => (pst', ctxt')
7.64 | _ => error "solve Check_Postcond resume script of parpbl: uncovered case get_loc"
7.65 val ctxt'' = ContextC.from_subpbl_to_caller ctxt scval ctxt'
7.66 val ((p, p_), ps, _, pt) = Generate.generate1 thy (Tactic.Check_Postcond' (pI, (scval, asm)))
7.67 - (Istate.Pstate (E,l,a,scval,Istate.Skip_,b), ctxt'') (pp,Res) pt;
7.68 + (Istate.Pstate (pst' |> Istate.upd_act scval |> Istate.upd_appy Istate.Skip_), ctxt'') (pp,Res) pt;
7.69 in ("ok", ([(Tactic.Check_Postcond pI, Tactic.Check_Postcond'(pI, (scval, asm)),
7.70 - ((pp, Res), (Istate.Pstate (E, l, a, scval, Istate.Skip_, b), ctxt'')))], ps, (pt, (p, p_)))) end
7.71 + ((pp, Res), (Istate.Pstate (pst' |> Istate.upd_act scval |> Istate.upd_appy Istate.Skip_), ctxt'')))], ps, (pt, (p, p_)))) end
7.72 end
7.73 | solve (_, Tactic.End_Proof'') (pt, (p, p_)) =
7.74 ("end-proof", ([(Tactic.Empty_Tac, Tactic.Empty_Tac_, (([], Res), (Istate.Uistate, ContextC.e_ctxt)))], [], (pt, (p, p_))))
7.75 @@ -216,7 +219,7 @@
7.76 in
7.77 ("ok", ([(Tactic.End_Detail, Tactic.End_Detail' t , ((p, p_), get_loc pt (p, p_)))], [], (pt, pr)))
7.78 end
7.79 - (* ======== general case ======== *)
7.80 + (* ======== general case as fall htrough ======== *)
7.81 | solve (_, m) (pt, po as (p, p_)) =
7.82 if Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (*29.8.02: could be detail, too !!*)
7.83 then
7.84 @@ -413,7 +416,7 @@
7.85 {errpats, nrls, scr = Rule.Prog prog, ...} => (errpats, nrls, prog)
7.86 | _ => error "inform: uncovered case of get_met"
7.87 val env = case Ctree.get_istate pt pos of
7.88 - Istate.Pstate (env, _, _, _, _, _) => env
7.89 + Istate.Pstate pst => Istate.get_env pst
7.90 | _ => error "inform: uncovered case of get_istate"
7.91 in
7.92 case Inform.check_error_patterns (f_pred, f_in) (prog, env) (errpats, nrls) of
8.1 --- a/src/Tools/isac/Specify/generate.sml Sun Oct 27 12:10:57 2019 +0100
8.2 +++ b/src/Tools/isac/Specify/generate.sml Wed Oct 30 11:02:41 2019 +0100
8.3 @@ -51,14 +51,12 @@
8.4 error ("interSteps>..>init_istate: \"" ^ rls ^ "\" has EmptyScr." ^
8.5 "use prep_rls' for storing rule-sets !")
8.6 | Rule.Rls {scr = Rule.Prog s, ...} =>
8.7 - (Istate.Pstate ([(hd (Program.formal_args s), t)], [], NONE, Rule.e_term, Istate.AppUndef_, true))
8.8 + (Istate.Pstate (Istate.e_scrstate |> Istate.upd_env_true [(hd (Program.formal_args s), t)]))
8.9 | Rule.Seq {scr = Rule.EmptyScr,...} =>
8.10 error ("interSteps>..>init_istate: \"" ^ rls ^ "\" has EmptyScr." ^
8.11 " Use prep_rls' for storing rule-sets !")
8.12 | Rule.Seq {scr = Rule.Prog s,...} =>
8.13 -(writeln ("### init_istate: rls = \"" ^ "rls" ^ "\", Prog = \"" ^ Rule.term2str s ^ "\"");
8.14 - (Istate.Pstate ([(hd (Program.formal_args s), t)], [], NONE, Rule.e_term, Istate.AppUndef_, true))
8.15 -)
8.16 + (Istate.Pstate (Istate.e_scrstate |> Istate.upd_env_true [(hd (Program.formal_args s), t)]))
8.17 | _ => error "init_istate Rewrite_Set: uncovered case assoc_rls")
8.18 | init_istate (Tactic.Rewrite_Set_Inst (subs, rls)) t =
8.19 let
8.20 @@ -71,16 +69,12 @@
8.21 error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr." ^
8.22 "use prep_rls' for storing rule-sets !")
8.23 | Rule.Rls {scr = Rule.Prog s, ...} =>
8.24 - let val env = (Program.formal_args s) ~~ [t, v]
8.25 - in (Istate.Pstate (env, [], NONE, Rule.e_term, Istate.AppUndef_, true))
8.26 - end
8.27 + Istate.Pstate (Istate.e_scrstate |> Istate.upd_env_true ((Program.formal_args s) ~~ [t, v]))
8.28 | Rule.Seq {scr = Rule.EmptyScr, ...} =>
8.29 error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr." ^
8.30 "use prep_rls' for storing rule-sets !")
8.31 | Rule.Seq {scr = Rule.Prog s,...} =>
8.32 - let val env = (Program.formal_args s) ~~ [t, v]
8.33 - in (Istate.Pstate (env,[], NONE, Rule.e_term, Istate.AppUndef_,true))
8.34 - end
8.35 + Istate.Pstate (Istate.e_scrstate |> Istate.upd_env_true ((Program.formal_args s) ~~ [t, v]))
8.36 | _ => error "init_istate Rewrite_Set_Inst: uncovered case assoc_rls"
8.37 end
8.38 | init_istate tac _ = error ("init_istate: uncovered definition for " ^ Tactic.tac2str tac)
9.1 --- a/src/Tools/isac/TODO.thy Sun Oct 27 12:10:57 2019 +0100
9.2 +++ b/src/Tools/isac/TODO.thy Wed Oct 30 11:02:41 2019 +0100
9.3 @@ -17,6 +17,16 @@
9.4 \item + test/..
9.5 rename Env.upd_env -> Env.update & Co.
9.6 \item xxx
9.7 + \item finalise changes in istate, appy, assy & Co
9.8 + \begin{itemize}
9.9 + \item remove remaining src/ which opens structure "(E," "(_,"
9.10 + + Test_Isac
9.11 + \item cleanup arguments of appy, assy & Co
9.12 + + Test_Isac/../lucas-interpreter.sml, Minisubpbl/
9.13 + \item draw changes into remaining tests
9.14 + \item xxx
9.15 + \end{itemize}
9.16 + \end{itemize}
9.17 \item xxx
9.18 \item fun handle_leaf: trace_prog .. separate message
9.19 \item xxx
9.20 @@ -255,7 +265,7 @@
9.21 val subpbl: string -> string list -> term unify with ^^^
9.22 \item xxx
9.23 \item Telem.safe is questionable: has it been replaced by Safe_Step, Not_Derivable, Helpless, etc?
9.24 - Note: replacement of Istate.safe by Istate.appy_ didn't care about Telem.safe.
9.25 + Note: replacement of Istate.safe by Istate.appy_ didn't care much about Telem.safe.
9.26 If Telem.safe is kept, consider merge with CTbasic.ostate
9.27 \item xxx
9.28 \item xxx
10.1 --- a/test/Tools/isac/BridgeLibisabelle/use-cases.sml Sun Oct 27 12:10:57 2019 +0100
10.2 +++ b/test/Tools/isac/BridgeLibisabelle/use-cases.sml Wed Oct 30 11:02:41 2019 +0100
10.3 @@ -161,7 +161,7 @@
10.4 val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1; (*<---------------------- orig. test code*)
10.5 (*+isa=REP*) if p = ([1], Frm) andalso term2str (get_obj g_form pt [1]) = "1 + -1 * 2 + x = 0"
10.6 andalso istate2str (get_istate pt p)
10.7 - = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"],\n [], NONE,\n ??.empty, AppUndef_, true)"
10.8 + = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [], e_rls, NONE, \n??.empty, AppUndef_, true)"
10.9 then () else error "refFormula = 1 + -1 * 2 + x = 0 changed";
10.10 (*-------------------------------------------------------------------------*)
10.11
10.12 @@ -181,11 +181,11 @@
10.13 (*//******************* locatetac returns tac_ + istate + cstate *****************************\\*)
10.14 locatetac : Tactic.input -> state -> string * (taci list * pos' list * state);
10.15 if istate2str istate
10.16 - = "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), AppUndef_, true)"
10.17 + = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [R,L,R,L,R,L,R], e_rls, SOMEe_e, \nx = 0 + -1 * (1 + -1 * 2), AppUndef_, true)"
10.18 then () else error "from locatetac return --- changed 1";
10.19
10.20 if istate2str (get_istate (fst cstate) (snd cstate))
10.21 - = "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), AppUndef_, true)"
10.22 + = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [R,L,R,L,R,L,R], e_rls, SOMEe_e, \nx = 0 + -1 * (1 + -1 * 2), AppUndef_, true)"
10.23 then () else error "from locatetac return --- changed 2";
10.24 (*\\******************* locatetac returns tac_ + istate + cstate *****************************//*)
10.25
10.26 @@ -207,7 +207,7 @@
10.27 (*+*)Safe_Step: Istate.T * Proof.context * T -> input_tactic_result;
10.28 (********************* locate_input_tactic returns cstate * istate * Proof.context *************)
10.29 (*+*)if istate2str istate
10.30 -(*+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), AppUndef_, true)"(**)
10.31 +(*+isa*) = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [R,L,R,L,R,L,R], e_rls, SOMEe_e, \nx = 0 + -1 * (1 + -1 * 2), AppUndef_, true)"
10.32 then case m of Rewrite_Set_Inst' _ => ()
10.33 else error "from locate_input_tactic return --- changed";
10.34
10.35 @@ -232,7 +232,7 @@
10.36 (*+isa==REP*)val [(Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv"),
10.37 Rewrite_Set_Inst' _, (pos', (istate, ctxt)))] = tacis;
10.38 (*+*)if pos' = ([1], Res) andalso istate2str istate
10.39 - = "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), AppUndef_, true)"
10.40 + = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [R,L,R,L,R,L,R], e_rls, SOMEe_e, \nx = 0 + -1 * (1 + -1 * 2), AppUndef_, true)"
10.41 then () else error "init. step 1 + -1 * 2 + x = 0 changed";
10.42
10.43 val pIopt = get_pblID (pt,ip);
10.44 @@ -244,7 +244,7 @@
10.45 val ("ok", [], ptp as (pt, p)) = xxxx;
10.46
10.47 if istate2str (get_istate pt p) (* <> <> <> <> ^^^^^^^^^^^^^*)
10.48 -(*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), AppUndef_, true)"
10.49 +(*REP*) = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [R,L,R,L,R,L,R], e_rls, SOMEe_e, \nx = 0 + -1 * (1 + -1 * 2), AppUndef_, true)"
10.50 then () else error "REP autoCalculate on (e_e, 1 + -1 * 2 + x = 0) changed"
10.51
10.52 "~~~~~ from TOPLEVEL to states return:"; upd_calc cI (ptp, []); upd_ipos cI 1 p;
11.1 --- a/test/Tools/isac/Interpret/inform.sml Sun Oct 27 12:10:57 2019 +0100
11.2 +++ b/test/Tools/isac/Interpret/inform.sml Wed Oct 30 11:02:41 2019 +0100
11.3 @@ -1037,7 +1037,7 @@
11.4 (*+*)then () else error "inform with (positive) check_error_patterns broken 3";
11.5
11.6 val env = case Ctree.get_istate pt pos of
11.7 - Istate.Pstate (env, _, _, _, _, _) => env
11.8 + Istate.Pstate (env, _, _, _, _, _, _) => env
11.9 | _ => error "inform: uncovered case of get_istate"
11.10 ;
11.11 (*+*)if term2str f_pred = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso
11.12 @@ -1076,7 +1076,7 @@
11.13 val f_curr = get_curr_formula (pt, pos); (* = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))"*)
11.14 val pp = par_pblobj pt p
11.15 val {errpats, scr = Prog prog, ...} = get_met (get_obj g_metID pt pp)
11.16 - val Pstate (env, _, _, _, _, _) = get_istate pt pos
11.17 + val Pstate (env, _, _, _, _, _, _) = get_istate pt pos
11.18 val subst = get_bdv_subst prog env
11.19 val errpatthms = errpats
11.20 |> filter ((curry op = errpatID) o (#1: errpat -> errpatID))
12.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Sun Oct 27 12:10:57 2019 +0100
12.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Wed Oct 30 11:02:41 2019 +0100
12.3 @@ -46,24 +46,24 @@
12.4 val PblObj {meth=itms, ...} = get_obj I pt p;
12.5 val thy' = get_obj g_domID pt p;
12.6 val thy = assoc_thy thy';
12.7 - val (is as Istate.Pstate (env,_,_,_,_,_), ctxt, sc) = init_pstate ctxt itms mI;
12.8 + val (is as Istate.Pstate (env,_,_,_,_,_,_), ctxt, sc) = init_pstate ctxt itms mI;
12.9 val ini = init_form thy sc env;
12.10 val p = lev_dn p;
12.11 ini = NONE; (*true*)
12.12 val (m', (is', ctxt'), _) = determine_next_tactic (thy', srls) (pt, (p, Res)) sc (is, ctxt);
12.13 val d = e_rls (*FIXME: get simplifier from domID*);
12.14 "~~~~~ fun locate_input_tactic, args:"; val ((ts as (thy',srls)), (m:Tactic.T), ((pt,p):ctree * pos'),
12.15 - (scr as Prog (h $ body),d), (Istate.Pstate (E,l,a,v,S,b), ctxt)) =
12.16 + (scr as Prog (h $ body),d), (Istate.Pstate (E,l,rls,a,v,S,b), ctxt)) =
12.17 ((thy',srls), m', (pt,(p, Res)), (sc,d), (is', ctxt'));
12.18 val thy = assoc_thy thy';
12.19 l = [] orelse ((*init.in solve..Apply_Method...*)
12.20 (last_elem o fst) p = 0 andalso snd p = Res); (*true*)
12.21 -"~~~~~ fun assy, args:"; val (ya, (is as (E,l,a,v,S,b),ss),
12.22 +"~~~~~ fun assy, args:"; val (ya, (is as (E,l,rls,a,v,S,b),ss),
12.23 (Const ("HOL.Let",_) $ e $ (Abs (id,T,body)))) =
12.24 - ((thy',ctxt,srls,d,Aundef), ((E,[R],a,v,S,b), [(m,EmptyMout,pt,p,[])]), body);
12.25 + ((thy',ctxt,srls,d,Aundef), ((E,[R],rls,a,v,S,b), [(m,EmptyMout,pt,p,[])]), body);
12.26 (*check: true*) term2str e = "Take (Integral f_f D v_v)";
12.27 -"~~~~~ fun assy, args:"; val ((thy',ctxt,sr,d,ap), (is as (E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss), t) =
12.28 - (ya, ((E , l@[L,R], a,v,S,b),ss), e);
12.29 +"~~~~~ fun assy, args:"; val ((thy',ctxt,sr,d,ap), (is as (E,l,rls,a,v,S,b), (m,_,pt,(p,p_),c)::ss), t) =
12.30 + (ya, ((E , l@[L,R], rls,a,v,S,b),ss), e);
12.31 val (a', STac stac) = handle_leaf "locate" thy' sr (E, (a, v)) t;
12.32 (* val ctxt = get_ctxt pt (p,p_)
12.33 exception PTREE "get_obj: pos = [0] does not exist" raised
12.34 @@ -114,37 +114,37 @@
12.35
12.36 (** )val Assoc ((is as (_,_,_,_,_,strong_ass), ctxt, ss as((tac', _, ctree, pos', _) :: _))) =( **)
12.37 (*case*) execute_progr_2 srls m cstate (progr, e_rls(*!!!*)) (istate, ctxt)(*of*);
12.38 -"~~~~~ fun execute_progr_2 , args:"; val (srls, m, (pt, p), (scr as Rule.Prog sc, d), (Istate.Pstate (E,l,a,v,S,b), ctxt))
12.39 +"~~~~~ fun execute_progr_2 , args:"; val (srls, m, (pt, p), (scr as Rule.Prog sc, d), (Istate.Pstate (E,l,rls,a,v,S,b), ctxt))
12.40 = (srls, m, cstate, (progr, e_rls(*!!!*)), (istate, ctxt));
12.41 (*if*) l = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*then*);
12.42
12.43 (** )val xxxxx_xx = ( **)
12.44 - assy (ctxt,srls, (pt, p), Aundef) ((E,[Celem.R],a,v,S,b), m) (Program.body_of sc);
12.45 + assy (ctxt,srls, (pt, p), Aundef) ((E,[Celem.R],rls,a,v,S,b), m) (Program.body_of sc);
12.46 "~~~~~ fun assy , args:"; val (ya, ((E,l,a,v,S,b), tac), (Const ("HOL.Let",_) $ e $ (Abs (id,T,body))))
12.47 = ((ctxt,srls, (pt, p), Aundef), ((E,[Celem.R],a,v,S,b), m), (Program.body_of sc));
12.48
12.49 - (*case*) assy ya ((E , l @ [Celem.L, Celem.R], a,v,S,b), tac) e (*of*);
12.50 -"~~~~~ fun xxx , args:"; val (ya, ((E,l,_,v,S,b),ss), (Const ("Tactical.Seq"(*2*),_) $ e1 $ e2 $ a))
12.51 - = (ya, ((E , l @ [Celem.L, Celem.R], a,v,S,b), tac), e);
12.52 + (*case*) assy ya ((E , l @ [Celem.L, Celem.R], rls,a,v,S,b), tac) e (*of*);
12.53 +"~~~~~ fun xxx , args:"; val (ya, ((E,l,rls,_,v,S,b),ss), (Const ("Tactical.Seq"(*2*),_) $ e1 $ e2 $ a))
12.54 + = (ya, ((E , l @ [Celem.L, Celem.R], rls,a,v,S,b), tac), e);
12.55
12.56 - (*case*) assy ya ((E, l @ [Celem.L, Celem.L, Celem.R], SOME a,v,S,b),ss) e1 (*of*);
12.57 -"~~~~~ fun assy , args:"; val (ya, ((E,l,a,v,S,b),ss), (Const ("Tactical.Try"(*1*),_) $ e))
12.58 - = (ya, ((E, l @ [Celem.L, Celem.L, Celem.R], SOME a,v,S,b),ss), e1);
12.59 + (*case*) assy ya ((E, l @ [Celem.L, Celem.L, Celem.R], rls,SOME a,v,S,b),ss) e1 (*of*);
12.60 +"~~~~~ fun assy , args:"; val (ya, ((E,l,rls,a,v,S,b),ss), (Const ("Tactical.Try"(*1*),_) $ e))
12.61 + = (ya, ((E, l @ [Celem.L, Celem.L, Celem.R], rls,SOME a,v,S,b),ss), e1);
12.62
12.63 - (*case*) assy ya ((E, l @ [Celem.R], a,v,S,b),ss) e (*of*);
12.64 + (*case*) assy ya ((E, l @ [Celem.R], rls,a,v,S,b),ss) e (*of*);
12.65 (*======= end of scanning tacticals, a leaf =======*)
12.66 -"~~~~~ fun assy , args:"; val ((ctxt,sr,(pt,p),ap), ((E,l,a,v,S,_), m), t)
12.67 - = (ya, ((E, l @ [Celem.R], a,v,S,b),ss), e);
12.68 +"~~~~~ fun assy , args:"; val ((ctxt,sr,(pt,p),ap), ((E,l,rls,a,v,S,_), m), t)
12.69 + = (ya, ((E, l @ [Celem.R], rls,a,v,S,b),ss), e);
12.70 val (a', Celem.STac stac) = (*case*) Lucin.handle_leaf "locate" "Isac_Knowledge" sr (E, (a, v)) t (*of*);
12.71 val Lucin.Ass (m, v', ctxt) = (*case*) Lucin.associate pt ctxt (m, stac) (*of*);
12.72 (* 1st ContextC.insert_assumptions asms' ctxt *)
12.73
12.74 -(*NEW*) Assoc ((E,l,a',v',S,true), ctxt, m) (*return value*);
12.75 +(*NEW*) Assoc ((E,l,rls,a',v',S,true), ctxt, m) (*return value*);
12.76 "~~~~~ from assy to execute_progr_2 return val:"; val (xxxxx_xx)
12.77 - = (Assoc ((E,l,a',v',S,true), ctxt, m)); (*return value*)
12.78 + = (Assoc ((E,l,rls,a',v',S,true), ctxt, m)); (*return value*)
12.79
12.80 -"~~~~~ from execute_progr_2 to locate_input_tactic return val:"; val Assoc (is as (_,_,_,_,_,strong_ass), ctxt(*NEW*), tac')
12.81 - = (Assoc ((E,l,a',v',S,true), ctxt, m));
12.82 +"~~~~~ from execute_progr_2 to locate_input_tactic return val:"; val Assoc (is as (_,_,_,_,_,_,strong_ass), ctxt(*NEW*), tac')
12.83 + = (Assoc ((E,l,rls,a',v',S,true), ctxt, m));
12.84 (*if*) strong_ass; (*then*)
12.85
12.86 "~~~~~ from locate_input_tactic to solve return:"; val Safe_Step (istate, ctxt, tac)
12.87 @@ -158,7 +158,7 @@
12.88 (*NEW*) val (p'', _, _,pt') =
12.89 (*NEW*) Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") m
12.90 (*NEW*) (* DEL.^^^^^ ContextC.insert_assumptions asms' ctxt 2nd, fst in Lucin.associate *)
12.91 -(*NEW*) (Istate.Pstate (E,l,a',v',S,true), ctxt) (p', p_) pt;
12.92 +(*NEW*) (Istate.Pstate (E,l,rls,a',v',S,true), ctxt) (p', p_) pt;
12.93 (*NEW*) (*in*)
12.94 (*NEW*) ("ok", ([(Lucin.tac_2tac tac, tac, (p'', (istate, ctxt)))],
12.95 (*NEW*) [(*ctree NOT cut*)], (pt', p'')));
12.96 @@ -276,57 +276,57 @@
12.97 val srls = Lucin.get_simplifier cstate (*TODO: shift into Istate.T*);
12.98
12.99 (*case*) execute_progr_2 srls tac cstate (progr, Rule.e_rls) (istate, ctxt) (*of*);
12.100 -"~~~~~ fun execute_progr_2 , args:"; val (srls, m, (pt, p), (scr as Rule.Prog sc, d), (Istate.Pstate (E,l,a,v,S,b), ctxt))
12.101 +"~~~~~ fun execute_progr_2 , args:"; val (srls, m, (pt, p), (scr as Rule.Prog sc, d), (Istate.Pstate (E,l,rls,a,v,S,b), ctxt))
12.102 = (srls, tac, cstate ,(progr, Rule.e_rls), (istate, ctxt));
12.103 (*if*) l = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*else*);
12.104
12.105 - astep_up (ctxt,srls,scr,(pt, p)) ((E,l,a,v,S,b), m);
12.106 + astep_up (ctxt,srls,scr,(pt, p)) ((E,l,rls,a,v,S,b), m);
12.107 "~~~~~ and astep_up , args:"; val ((ys as (_,_,Rule.Prog sc,_)), ((E,l,a,v,S,b),ss))
12.108 = ((ctxt,srls,scr,(pt, p)), ((E,l,a,v,S,b), m));
12.109 (*if*) 1 < length l (*then*);
12.110 val up = drop_last l; (* = [R, L, R, L, R]*)
12.111
12.112 - ass_up ys ((E,up,a,v,S,b),ss) (go up sc);
12.113 + ass_up ys ((E,up,rls,a,v,S,b),ss) (go up sc);
12.114 "~~~~~ fun ass_up , args:"; val (ysa, iss, (Const ("Tactical.Try"(*2*),_) $ _))
12.115 - = (ys, ((E,up,a,v,S,b),ss), (go up sc));
12.116 + = (ys, ((E,up,rls,a,v,S,b),ss), (go up sc));
12.117
12.118 astep_up ysa iss;
12.119 -"~~~~~ fun astep_up , args:"; val (((ys as (_,_,Rule.Prog sc,_)), ((E,l,a,v,S,b),ss)))
12.120 +"~~~~~ fun astep_up , args:"; val (((ys as (_,_,Rule.Prog sc,_)), ((E,l,rls,a,v,S,b),ss)))
12.121 = (ysa, iss);
12.122 (*if*) 1 < length l (*then*);
12.123 val up = drop_last l; (* = [R, L, R, L]*)
12.124
12.125 - ass_up ys ((E,up,a,v,S,b),ss) (go up sc);
12.126 -"~~~~~ fun ass_up , args:"; val ((ysa as (ctxt,s,Rule.Prog sc,d)), ((E,l,a,v,S,b),ss),
12.127 + ass_up ys ((E,up,rls,a,v,S,b),ss) (go up sc);
12.128 +"~~~~~ fun ass_up , args:"; val ((ysa as (ctxt,s,Rule.Prog sc,d)), ((E,l,rls,a,v,S,b),ss),
12.129 (Const ("Tactical.Seq"(*3*),_) $ _ ))
12.130 - = (ys, ((E,up,a,v,S,b),ss), (go up sc));
12.131 + = (ys, ((E,up,rls,a,v,S,b),ss), (go up sc));
12.132 val up = drop_last l;
12.133 val Const ("Tactical.Seq",_) $ _ $ e2 = (*case*) go up sc (*of*);
12.134
12.135 - (*case*) assy ((*y,*)ctxt,s,d,Aundef) ((E, up @ [Celem.R], a,v,S,b),ss) e2 (*of*);
12.136 -"~~~~~ fun assy , args:"; val (ya, ((E,l,a,v,S,b),ss), (Const ("Tactical.Seq"(*2*),_) $e1 $ e2))
12.137 - = (((*y,*)ctxt,s,d,Aundef), ((E, up @ [Celem.R], a,v,S,b),ss), e2);
12.138 - val NasApp ((E,_,_,v,_,_), ctxt(*NEW*), ss) = (*case*) assy ya ((E, l @ [Celem.L, Celem.R], a,v,S,b),ss) e1 (*of*);
12.139 + (*case*) assy ((*y,*)ctxt,s,d,Aundef) ((E, up @ [Celem.R], rls,a,v,S,b),ss) e2 (*of*);
12.140 +"~~~~~ fun assy , args:"; val (ya, ((E,l,rls,a,v,S,b),ss), (Const ("Tactical.Seq"(*2*),_) $e1 $ e2))
12.141 + = (((*y,*)ctxt,s,d,Aundef), ((E, up @ [Celem.R], rls,a,v,S,b),ss), e2);
12.142 + val NasApp ((E,_,_,_,v,_,_), ctxt(*NEW*), ss) = (*case*) assy ya ((E, l @ [Celem.L, Celem.R], rls,a,v,S,b),ss) e1 (*of*);
12.143
12.144 - assy ya ((E, l @ [Celem.R], a,v,S,b),ss) e2;
12.145 -"~~~~~ fun assy , args:"; val (ya, ((E,l,a,v,S,b),ss), (Const ("Tactical.Try"(*2*),_) $ e))
12.146 - = (ya, ((E, l @ [Celem.R], a,v,S,b),ss), e2);
12.147 + assy ya ((E, l @ [Celem.R], rls,a,v,S,b),ss) e2;
12.148 +"~~~~~ fun assy , args:"; val (ya, ((E,l,rls,a,v,S,b),ss), (Const ("Tactical.Try"(*2*),_) $ e))
12.149 + = (ya, ((E, l @ [Celem.R], rls,a,v,S,b),ss), e2);
12.150
12.151 - (*case*) assy ya ((E, l @ [Celem.R], a,v,S,b),ss) e (*of*);
12.152 + (*case*) assy ya ((E, l @ [Celem.R], rls,a,v,S,b),ss) e (*of*);
12.153 (*======= end of scanning tacticals, a leaf =======*)
12.154 -"~~~~~ fun assy , args:"; val ((ctxt,sr,(pt,p),ap), ((E,l,a,v,S,_), m), t)
12.155 - = (ya, ((E, l @ [Celem.R], a,v,S,b),ss), e);
12.156 +"~~~~~ fun assy , args:"; val ((ctxt,sr,(pt,p),ap), ((E,l,rls,a,v,S,_), m), t)
12.157 + = (ya, ((E, l @ [Celem.R], rls,a,v,S,b),ss), e);
12.158 val (a', Celem.STac stac) = (*case*) Lucin.handle_leaf "locate" "Isac_Knowledge" sr (E, (a, v)) t (*of*);
12.159 val Lucin.NotAss = (*case*) Lucin.associate pt ctxt (m, stac) (*of*);
12.160 val Aundef = (*case*) ap (*of*);
12.161 val Appl m' = (*case*) Applicable.applicable_in p pt (Lucin.stac2tac pt (Celem.assoc_thy "Isac_Knowledge") stac) (*of*);
12.162 - val is = (E,l,a',Lucin.tac_2res m',S,false(*FIXXXME.WN0?*));
12.163 + val is = (E,l,rls,a',Lucin.tac_2res m',S,false(*FIXXXME.WN0?*));
12.164 NasApp (is, ctxt, m) (* return value *);
12.165
12.166 val Rewrite' ("PolyMinus", "tless_true", _, _, ("tausche_minus",_ (*"?b ist_monom \<Longrightarrow> ?a kleiner ?b \<Longrightarrow> ?b - ?a = - ?a + ?b"*)),
12.167 t, (res, asm)) = m;
12.168 if scrstate2str is =
12.169 - "([\"\n(t_t, 5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12)\"], [R,L,R,R,R,R], SOMEt_t, \n" ^
12.170 + "([\"\n(t_t, 5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12)\"], [R,L,R,R,R,R], e_rls, SOMEt_t, \n" ^
12.171 "- (8 * g) + (-9 + 12 + 5 * e - 7 * e + (6 - 4) * f) + 10 * g, AppUndef_, false)"
12.172 andalso
12.173 term2str t = "- (8 * g) + (- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f) + 10 * g"
13.1 --- a/test/Tools/isac/Interpret/script.sml Sun Oct 27 12:10:57 2019 +0100
13.2 +++ b/test/Tools/isac/Interpret/script.sml Wed Oct 30 11:02:41 2019 +0100
13.3 @@ -111,7 +111,7 @@
13.4 val PblObj {meth=itms, ...} = get_obj I pt p;
13.5 val thy' = get_obj g_domID pt p;
13.6 val thy = assoc_thy thy';
13.7 -val (is as Pstate (env,_,_,_,_,_), ctxt, sc) = init_pstate ctxt itms mI;
13.8 +val (is as Pstate (env,_,_,_,_,_,_), ctxt, sc) = init_pstate ctxt itms mI;
13.9 val ini = init_form thy sc env;
13.10 "----- fun init_form, args:"; val (Prog sc) = sc;
13.11 "----- fun get_stac, args:"; val (y, h $ body) = (thy, sc);
13.12 @@ -204,7 +204,7 @@
13.13 then (thd3 o snd3) (get_obj g_origin pt pp)
13.14 else metID
13.15 val {scr=Prog sc,srls,erls,rew_ord'=ro,...} = get_met metID'
13.16 - val Pstate (env,_,a,v,_,_) = get_istate pt (p,p_)
13.17 + val Pstate (env,_,_,a,v,_,_) = get_istate pt (p,p_)
13.18 val alltacs = (*we expect at least 1 stac in a script*)
13.19 map ((stac2tac pt thy) o rep_stacexpr o #2 o
13.20 (handle_leaf "selrul" thy' srls (env, (a, v)))) (stacpbls sc)
13.21 @@ -414,7 +414,7 @@
13.22 "~~~~~ fun init_pstate , args:"; val (thy, itms, metID) = (assoc_thy thy, meth, metID);
13.23 val (Pstate st, ctxt, Prog _) = init_pstate ctxt itms metID;
13.24 if scrstate2str st =
13.25 -"([\"\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, AppUndef_, true)"
13.26 +"([\"\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)\"], [], e_rls, NONE, \n??.empty, AppUndef_, true)"
13.27 then () else error "init_pstate changed for Biegelinie";
13.28
13.29 (*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' c pt'''''; (*nxt = Model_Problem*)
14.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml Sun Oct 27 12:10:57 2019 +0100
14.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml Wed Oct 30 11:02:41 2019 +0100
14.3 @@ -211,7 +211,7 @@
14.4 (*locate_input_tactic (thy',srls) m (pt,(p,p_)) (sc,d) is;
14.5 WAS: not-found-in-script: NotLocatable from NasNap (Const ("List...*)
14.6 "~~~~~ fun locate_input_tactic, args:"; val ((ts as (thy',srls)), (m:Tactic.T), ((pt,p):ctree * pos'),
14.7 - (scr as Prog (h $ body),d), (Pstate (E,l,a,v,S,b), ctxt)) =
14.8 + (scr as Prog (h $ body),d), (Pstate (E,l,rls,a,v,S,b), ctxt)) =
14.9 ((thy',srls), m ,(pt,(p,p_)) ,(sc,d) ,is); (* locate_input_tactic 2nd pattern *)
14.10 val thy = assoc_thy thy';
14.11 l = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*false*);
15.1 --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml Sun Oct 27 12:10:57 2019 +0100
15.2 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml Wed Oct 30 11:02:41 2019 +0100
15.3 @@ -616,7 +616,7 @@
15.4 val (tac_,is,(t,_)) = determine_next_tactic (thy',srls) (pt,pos) sc is;
15.5 (*tac_ = Rewrite' (..., ("rnorm_equation_add", "Test.rnorm_equation_add"), ...) !!!!!!!!!!!!!!!!*)
15.6 "~~~~~ fun determine_next_tactic , args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'),
15.7 - (sc as Prog (h $ body)), (Pstate (ist as (E,l,a,v,s,b)), ctxt)) = ((thy',srls), (pt,pos), sc, is);
15.8 + (sc as Prog (h $ body)), (Pstate (ist as (E,l,rls,a,v,s,b)), ctxt)) = ((thy',srls), (pt,pos), sc, is);
15.9 l = [] = false;
15.10 nstep_up thy ptp sc ist Skip_ (*--> Appy (Rewrite' (.., (.., "Test.rnorm_equation_add"), ...)
15.11 BUT WE FIND IN THE CODE ABOVE IN determine_next_tactic:*)
16.1 --- a/test/Tools/isac/Minisubpbl/200-start-method.sml Sun Oct 27 12:10:57 2019 +0100
16.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method.sml Wed Oct 30 11:02:41 2019 +0100
16.3 @@ -58,7 +58,7 @@
16.4 val {srls, pre, prls, ...} = get_met mI;
16.5 val pres = check_preconds thy prls pre meth |> map snd;
16.6 val ctxt = ctxt |> insert_assumptions pres;
16.7 -val (is'''' as Pstate (env'''',_,_,_,_,_), _, sc'''') = init_pstate ctxt meth mI;
16.8 +val (is'''' as Pstate (env'''',_,_,_,_,_,_), _, sc'''') = init_pstate ctxt meth mI;
16.9 "~~~~~ fun init_pstate , args:"; val (thy, itms, metID) = (thy, meth, mI)
16.10 val actuals = itms2args thy metID itms
16.11 val scr as Prog sc = (#scr o get_met) metID
16.12 @@ -131,7 +131,7 @@
16.13 val thy' = get_obj g_domID pt (par_pblobj pt p);
16.14 val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
16.15 "~~~~~ fun determine_next_tactic, args:"; val (thy, (ptp as (pt, (p, _))), (sc as Rule.Prog (_ $ body)),
16.16 - (Istate.Pstate (E,l,a,v,s,_), ctxt)) = ((thy', srls), (pt, pos), sc, is);
16.17 + (Istate.Pstate (E,l,rls,a,v,s,_), ctxt)) = ((thy', srls), (pt, pos), sc, is);
16.18 l = [] (* = true*);
16.19 "~~~~~ fun appy, args:"; val (thy, ptp, E, l, (Const ("HOL.Let",_) $ e $ (Abs (i,T,b))), a, v) =
16.20 (thy, ptp, E, [Celem.R], body, NONE, v);
17.1 --- a/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Sun Oct 27 12:10:57 2019 +0100
17.2 +++ b/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Wed Oct 30 11:02:41 2019 +0100
17.3 @@ -53,26 +53,26 @@
17.4 val srls = get_simplifier cstate;
17.5
17.6 (*case*) execute_progr_2 srls m cstate (progr, e_rls(*!!!*)) (istate, ctxt)(*of*);
17.7 -"~~~~~ 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))
17.8 +"~~~~~ fun execute_progr_2 , args:"; val (((*thy',*) srls), m, (pt, p), (scr as Rule.Prog sc, d), (Istate.Pstate (E,l,rls,a,v,S,b), ctxt))
17.9 = (srls, m, cstate, (progr, e_rls(*!!!*)), (istate, ctxt));
17.10 (*if*)l = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*then*);
17.11
17.12 (*val Assoc (pstate, steps) = in isabisacREP*)
17.13 (*ERROR assy: call by ([3], Pbl) in isabisac*)
17.14 - assy (ctxt,srls, (pt, p), Aundef) ((E,[Celem.R],a,v,S,b), m) (Program.body_of sc);
17.15 + assy (ctxt,srls, (pt, p), Aundef) ((E,[Celem.R],rls,a,v,S,b), m) (Program.body_of sc);
17.16
17.17 (* checked all arguments of assy for equality: isabisac -- isabisacREP *)
17.18 -"~~~~~ fun assy [1], args:"; val (ya, ((E,l,a,v,S,b), tac), (Const ("HOL.Let",_) $ e $ (Abs (id,T,body))))
17.19 - = ((ctxt,srls, (pt, p), Aundef), ((E,[Celem.R],a,v,S,b), m), (Program.body_of sc));
17.20 +"~~~~~ fun assy [1], args:"; val (ya, ((E,l,rls,a,v,S,b), tac), (Const ("HOL.Let",_) $ e $ (Abs (id,T,body))))
17.21 + = ((ctxt,srls, (pt, p), Aundef), ((E,[Celem.R],rls,a,v,S,b), m), (Program.body_of sc));
17.22
17.23 -(*val Assoc (pstate, steps) = in isabisac*) assy ya ((E , l @ [Celem.L, Celem.R], a,v,S,b), tac) e;
17.24 +(*val Assoc (pstate, steps) = in isabisac*) assy ya ((E , l @ [Celem.L, Celem.R], rls,a,v,S,b), tac) e;
17.25 "~~~~~ fun assy, args:"; val (ya, ((E,l,_,v,S,b),ss),
17.26 (Const ("Tactical.Seq"(*1*),_) $e1 $ e2 $ a)) =
17.27 (ya, ((E , l @ [Celem.L, Celem.R], a,v,S,b), tac), e);
17.28
17.29 (*val Assoc (pstate, steps) = in isabisacREP*)
17.30 (*val NasApp ((E,_,_,v,_,_),ss) = in isabisac*)
17.31 - (*case*) assy ya ((E, l @ [Celem.L, Celem.L, Celem.R], SOME a,v,S,b),ss) e1 (*of*);
17.32 + (*case*) assy ya ((E, l @ [Celem.L, Celem.L, Celem.R], rls, SOME a,v,S,b),ss) e1 (*of*);
17.33 "~~~~~ fun assy, args:"; val (ya, ((E,l,a,v,S,b),ss), (Const ("Tactical.Try"(*1*),_) $ e)) =
17.34 ( ya, ((E, l @ [Celem.L, Celem.L, Celem.R], SOME a,v,S,b),ss), e1);
17.35
17.36 @@ -82,7 +82,7 @@
17.37
17.38 (*val Assoc (pstate, steps) = in isabisacREP*)
17.39 (*val NasApp ((E,_,_,v,_,_),ss) = in isabisac*)
17.40 -assy ya ((E, l @ [Celem.R], a,v,S,b),ss) e ;
17.41 +assy ya ((E, l @ [Celem.R], rls,a,v,S,b),ss) e ;
17.42 (*======= end of scanning tacticals, a leaf =======*)
17.43 "~~~~~ fun assy, args:"; val ((ctxt,sr,(pt,p),ap), ((E,l,a,v,S,_), m), t) =
17.44 (ya, ((E, l @ [Celem.R], a,v,S,b),ss), e);
17.45 @@ -114,7 +114,7 @@
17.46 (* isabisac17: val (tac_, is, (t, _)) = determine_next_tactic (thy', srls) (pt, pos) sc is;
17.47 go: no [L,L,R] *)
17.48 "~~~~~ fun determine_next_tactic, args:"; val (thy, (ptp as (pt, (p, _))), (sc as Prog (_ $ body)),
17.49 - (Pstate (E,l,a,v,s,_), ctxt) ) = ((thy', srls), (pt, pos), sc, is);
17.50 + (Pstate (E,l,rls,a,v,s,_), ctxt) ) = ((thy', srls), (pt, pos), sc, is);
17.51 (*if*) l = [] = false;
17.52
17.53 (* isabisac17: nstep_up thy ptp sc E l Skip_ a v ERROR go: no [L,L,R] *)
17.54 @@ -170,12 +170,12 @@
17.55 val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
17.56
17.57 (*val (tac_, is, (t, _)) =*) determine_next_tactic (thy', srls) (pt, pos) sc is;
17.58 -"~~~~~ fun determine_next_tactic , args:"; val (thy, (ptp as (pt, (p, _))), sc, (Istate.Pstate (E,l,a,v,s,_), ctxt))
17.59 +"~~~~~ fun determine_next_tactic , args:"; val (thy, (ptp as (pt, (p, _))), sc, (Istate.Pstate (E,l,rls,a,v,s,_), ctxt))
17.60 = ((thy', srls), (pt, pos), sc, is);
17.61
17.62 - (*case*) execute_progr_1 thy ptp sc (Istate.Pstate (E,l,a,v,s,false)) (*of*);
17.63 -"~~~~~ fun execute_progr_1 , args:"; val (thy, ptp, (sc as Rule.Prog prog), (Istate.Pstate (ist as (E, l, a, v, _, _))))
17.64 - = (thy, ptp, sc, (Istate.Pstate (E,l,a,v,s,false)));
17.65 + (*case*) execute_progr_1 thy ptp sc (Istate.Pstate (E,l,rls,a,v,s,false)) (*of*);
17.66 +"~~~~~ fun execute_progr_1 , args:"; val (thy, ptp, (sc as Rule.Prog prog), (Istate.Pstate (ist as (E, l, rls,a, v, _, _))))
17.67 + = (thy, ptp, sc, (Istate.Pstate (E,l,rls,a,v,s,false)));
17.68 (*if*) l = [] (*else*);
17.69
17.70 nstep_up thy ptp sc ist Skip_;
18.1 --- a/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Sun Oct 27 12:10:57 2019 +0100
18.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Wed Oct 30 11:02:41 2019 +0100
18.3 @@ -43,7 +43,7 @@
18.4 val srls = get_simplifier cstate;
18.5
18.6 (*case*) execute_progr_2 srls m cstate (progr, e_rls(*!!!*)) (istate, ctxt)(*of*);
18.7 -"~~~~~ 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))
18.8 +"~~~~~ fun execute_progr_2 , args:"; val (((*thy',*) srls), m, (pt, p), (scr as Rule.Prog sc, d), (Istate.Pstate (E,l,rls,a,v,S,b), ctxt))
18.9 = (srls, m, cstate, (progr, e_rls(*!!!*)), (istate, ctxt));
18.10 (*if*)l = [] orelse ((*init.in solve..Apply_Method...*)
18.11 (last_elem o fst) p = 0 andalso snd p = Res) (*else*);
18.12 @@ -54,33 +54,33 @@
18.13 (*if*) 1 < length l (*true*);
18.14 val up = drop_last l;
18.15
18.16 - ass_up ys ((E,up,a,v,S,b),ss) (go up sc);
18.17 + ass_up ys ((E,up,rls,a,v,S,b),ss) (go up sc);
18.18 "~~~~~ fun ass_up, args:"; val (ysa, iss, (Const ("Tactical.Try",_) $ e)) =
18.19 - (ys, ((E,up,a,v,S,b),ss), (go up sc));
18.20 + (ys, ((E,up,rls,a,v,S,b),ss), (go up sc));
18.21 astep_up ysa iss;
18.22 -"~~~~~ and astep_up , args:"; val ((ys as (_,_,Rule.Prog sc,_)), ((E,l,a,v,S,b),ss)) = (ysa, iss);
18.23 +"~~~~~ and astep_up , args:"; val ((ys as (_,_,Rule.Prog sc,_)), ((E,l,rls,a,v,S,b),ss)) = (ysa, iss);
18.24 (*if*) 1 < length l; (*then*)
18.25 val up = drop_last l;
18.26
18.27 - ass_up ys ((E,up,a,v,S,b),ss) (go up sc);
18.28 -"~~~~~ fun ass_up , args:"; val (ysa, iss, (Const ("Tactical.Seq",_) $ _ $ _ )) = (ys, ((E,up,a,v,S,b),ss), (go up sc));
18.29 + ass_up ys ((E,up,rls,a,v,S,b),ss) (go up sc);
18.30 +"~~~~~ fun ass_up , args:"; val (ysa, iss, (Const ("Tactical.Seq",_) $ _ $ _ )) = (ys, ((E,up,rls,a,v,S,b),ss), (go up sc));
18.31
18.32 astep_up ysa iss (*2*: comes from e2*);
18.33 -"~~~~~ and astep_up , args:"; val ((ys as (_,_,Rule.Prog sc,_)), ((E,l,a,v,S,b),ss)) = (ysa, iss);
18.34 +"~~~~~ and astep_up , args:"; val ((ys as (_,_,Rule.Prog sc,_)), ((E,l,rls,a,v,S,b),ss)) = (ysa, iss);
18.35 (*if*) 1 < length l; (*then*)
18.36 val up = drop_last l;
18.37
18.38 - ass_up ys ((E,up,a,v,S,b),ss) (go up sc);
18.39 -"~~~~~ fun ass_up , args:"; val (ysa, iss, (Const ("Tactical.Seq",_) $ _ $ _ $ _)) = (ys, ((E,up,a,v,S,b),ss), (go up sc));
18.40 + ass_up ys ((E,up,rls,a,v,S,b),ss) (go up sc);
18.41 +"~~~~~ fun ass_up , args:"; val (ysa, iss, (Const ("Tactical.Seq",_) $ _ $ _ $ _)) = (ys, ((E,up,rls,a,v,S,b),ss), (go up sc));
18.42
18.43 astep_up ysa iss (*all has been done in (*2*) below*);
18.44 -"~~~~~ and astep_up , args:"; val ((ys as (_,_,Rule.Prog sc,_)), ((E,l,a,v,S,b),ss)) = (ysa, iss);
18.45 +"~~~~~ and astep_up , args:"; val ((ys as (_,_,Rule.Prog sc,_)), ((E,l,rls,a,v,S,b),ss)) = (ysa, iss);
18.46 (*if*) 1 < length l; (*then*)
18.47 val up = drop_last l;
18.48
18.49 - ass_up ys ((E,up,a,v,S,b),ss) (go up sc);
18.50 -"~~~~~ fun ass_up , args:"; val ((ys as (ctxt,s,Rule.Prog sc,d)), ((E,l,a,v,S,b),ss), (Const ("HOL.Let",_) $ _))
18.51 - = (ys, ((E,up,a,v,S,b),ss), (go up sc));
18.52 + ass_up ys ((E,up,rls,a,v,S,b),ss) (go up sc);
18.53 +"~~~~~ fun ass_up , args:"; val ((ys as (ctxt,s,Rule.Prog sc,d)), ((E,l,rls,a,v,S,b),ss), (Const ("HOL.Let",_) $ _))
18.54 + = (ys, ((E,up,rls,a,v,S,b),ss), (go up sc));
18.55 val l = drop_last l; (*comes from e, goes to Abs*)
18.56 val (i, T, body) =
18.57 (case go l sc of
18.58 @@ -89,14 +89,14 @@
18.59 val i = TermC.mk_Free (i, T);
18.60 val E = Env.upd_env E (i, v);
18.61
18.62 - (*case*) assy (ctxt,s,d,Aundef) ((E, l @ [Celem.R, Celem.D], a,v,S,b),ss) body (*of*);
18.63 -"~~~~~ fun assy , args:"; val (ya, ((E,l,a,v,S,b),ss), (Const ("HOL.Let",_) $ e $ (Abs (id,T,body))))
18.64 - = ((ctxt,s,d,Aundef), ((E, l @ [Celem.R, Celem.D], a,v,S,b),ss), body);
18.65 + (*case*) assy (ctxt,s,d,Aundef) ((E, l @ [Celem.R, Celem.D], rls,a,v,S,b),ss) body (*of*);
18.66 +"~~~~~ fun assy , args:"; val (ya, ((E,l,rls,a,v,S,b),ss), (Const ("HOL.Let",_) $ e $ (Abs (id,T,body))))
18.67 + = ((ctxt,s,d,Aundef), ((E, l @ [Celem.R, Celem.D], rls,a,v,S,b),ss), body);
18.68
18.69 - (*case*) assy ya ((E , l @ [Celem.L, Celem.R], a,v,S,b), ss) e (*of*);
18.70 + (*case*) assy ya ((E , l @ [Celem.L, Celem.R], rls,a,v,S,b), ss) e (*of*);
18.71 (*======= end of scanning tacticals, a leaf =======*)
18.72 -"~~~~~ fun assy , args:"; val ((ctxt,sr,(pt,p),ap), ((E,l,a,v,S,_), m), t)
18.73 - = (ya, ((E , l @ [Celem.L, Celem.R], a,v,S,b), ss), e);
18.74 +"~~~~~ fun assy , args:"; val ((ctxt,sr,(pt,p),ap), ((E,l,rls,a,v,S,_), m), t)
18.75 + = (ya, ((E , l @ [Celem.L, Celem.R], rls,a,v,S,b), ss), e);
18.76
18.77 (*val (a', STac stac) = ( *case*) Lucin.handle_leaf "locate" "Isac_Knowledge" sr (E, (a, v)) t (*of*);
18.78 "~~~~~ fun handle_leaf , args:"; val (call, thy, srls, (E, (a, v)), t)
19.1 --- a/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Sun Oct 27 12:10:57 2019 +0100
19.2 +++ b/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Wed Oct 30 11:02:41 2019 +0100
19.3 @@ -54,7 +54,7 @@
19.4 val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
19.5 val thy' = get_obj g_domID pt p;
19.6 val thy = assoc_thy thy';
19.7 - val (is as Pstate (env,_,_,_,_,_), ctxt, sc) = init_pstate ctxt itms mI;
19.8 + val (is as Pstate (env,_,_,_,_,_,_), ctxt, sc) = init_pstate ctxt itms mI;
19.9 (*dont take ctxt ^^^ from ^^^^^^^^^^^^^*)
19.10
19.11 (*+*)val (pt, p) = case locatetac tac (pt, pos) of
19.12 @@ -73,7 +73,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,(p,_)):ctree * pos'), (sc as Prog (h $ body)),
19.16 - (Pstate (ist as (E,l,a,v,s,b)), ctxt)) = ((thy',srls), (pt,pos), sc, is);
19.17 + (Pstate (ist as (E,l,rls,a,v,s,b)), ctxt)) = ((thy',srls), (pt,pos), sc, is);
19.18
19.19 (*+*)val SOME t = parseNEW (get_ctxt pt pos) "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
19.20
20.1 --- a/test/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml Sun Oct 27 12:10:57 2019 +0100
20.2 +++ b/test/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml Wed Oct 30 11:02:41 2019 +0100
20.3 @@ -59,7 +59,7 @@
20.4 handle _ => [] (*FIXME.WN030527 asms in subpbls not completely clear*)
20.5 val metID = get_obj g_metID pt pp;
20.6 val {srls=srls,scr=sc,...} = get_met metID;
20.7 - val loc as (Pstate (E,l,a,_,_,b), ctxt) = get_loc pt (p,p_);
20.8 + val loc as (Pstate (E,l,rls,a,_,_,b), ctxt) = get_loc pt (p,p_);
20.9 val thy' = get_obj g_domID pt pp;
20.10 val thy = assoc_thy thy';
20.11 val (_,_,(scval,scsaf)) = determine_next_tactic (thy',srls) (pt,(p,p_)) sc loc;
20.12 @@ -69,10 +69,10 @@
20.13 val thy = assoc_thy thy';
20.14 val metID = get_obj g_metID pt ppp;
20.15 val {scr,...} = get_met metID;
20.16 - val (Pstate (E,l,a,_,_,b), ctxt') = get_loc pt (pp(*!/p/*),Frm)
20.17 + val (Pstate (E,l,rls,a,_,_,b), ctxt') = get_loc pt (pp(*!/p/*),Frm)
20.18 val ctxt'' = from_subpbl_to_caller ctxt scval ctxt'
20.19 val tac_ = Check_Postcond' (pI, (scval, asm))
20.20 - val is = Pstate (E,l,a,scval,Istate.Skip_,b);
20.21 + val is = Pstate (E,l,rls,a,scval,Istate.Skip_,b);
20.22 "~~~~~ fun generate1, args:"; val (thy, (Check_Postcond' (pI, (scval, asm))), l, (p,p_), pt) =
20.23 (thy, tac_, (is, ctxt''), (pp, Res), pt);
20.24 val (pt,c) = append_result pt p l (scval, (*map str2term*) asm) Complete;
21.1 --- a/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Sun Oct 27 12:10:57 2019 +0100
21.2 +++ b/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Wed Oct 30 11:02:41 2019 +0100
21.3 @@ -56,7 +56,7 @@
21.4 val thy' = get_obj g_domID pt (par_pblobj pt p);
21.5 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*)
21.6 "~~~~~ fun determine_next_tactic, args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'), (sc as Prog (h $ body)),
21.7 -(Pstate (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
21.8 +(Pstate (E,l,rls,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
21.9 val ctxt = get_ctxt pt pos
21.10 val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
21.11 l; (*= [R, R, D, L, R]*)
22.1 --- a/test/Tools/isac/Minisubpbl/700-interSteps.sml Sun Oct 27 12:10:57 2019 +0100
22.2 +++ b/test/Tools/isac/Minisubpbl/700-interSteps.sml Wed Oct 30 11:02:41 2019 +0100
22.3 @@ -123,7 +123,7 @@
22.4 (* val (tac_, is, (t, _)) =*) determine_next_tactic (thy', srls) (pt, pos) sc is;
22.5 ;
22.6 "~~~~~ fun determine_next_tactic , args:"; val (thy, (ptp as (pt, (p, _))), (sc as Rule.Prog (_ $ body)),
22.7 - (Istate.Pstate (ist as (E,l,a,v,s,_)), ctxt)) = ((thy', srls), (pt, pos), sc, is);
22.8 + (Istate.Pstate (ist as (E,l,rls,a,v,s,_)), ctxt)) = ((thy', srls), (pt, pos), sc, is);
22.9 (*if*) l = [] (* = true *);
22.10
22.11 appy thy ptp ist body;
23.1 --- a/test/Tools/isac/Test_Isac_Short.thy Sun Oct 27 12:10:57 2019 +0100
23.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Wed Oct 30 11:02:41 2019 +0100
23.3 @@ -54,7 +54,7 @@
23.4 "~~~~~ from xxx to yyy return val:"; val () = ();
23.5 (*if*) (*then*); (*else*); (*case*) (*of*); (*return value*);
23.6 "xx"
23.7 -^ "xxx" (*+*)
23.8 +^ "xxx" (*+*) (*isa*) (*REP*)
23.9 \<close>
23.10 section \<open>Run the tests\<close>
23.11 text \<open>
23.12 @@ -212,7 +212,6 @@
23.13 ML_file "Interpret/script.sml"
23.14 ML_file "Interpret/inform.sml"
23.15 ML_file "Interpret/lucas-interpreter.sml"
23.16 -
23.17 ML_file "MathEngine/solve.sml"
23.18 ML_file "MathEngine/mathengine-stateless.sml" (*!part. WN130804: +check Interpret/me.sml*)
23.19 ML_file "MathEngine/messages.sml"
24.1 --- a/test/Tools/isac/Test_Some.thy Sun Oct 27 12:10:57 2019 +0100
24.2 +++ b/test/Tools/isac/Test_Some.thy Wed Oct 30 11:02:41 2019 +0100
24.3 @@ -45,10 +45,10 @@
24.4 ML \<open>
24.5 "~~~~~ fun xxx , args:"; val () = ();
24.6 "~~~~~ and xxx , args:"; val () = ();
24.7 -"~~~~~ from xxx to yyy return val:"; val () = ();
24.8 +"~~~~~ from xxx -> fun yyy -> fun zzz, return val:"; val () = ();
24.9 (*if*) (*then*); (*else*); (*case*) (*of*); (*return value*);
24.10 "xx"
24.11 -^ "xxx" (*+*)
24.12 +^ "xxx" (*+*) (*!for return!*) (*isa*) (*REP*)
24.13 \<close> ML \<open>
24.14 \<close>
24.15 text \<open>