1.1 --- a/src/Tools/isac/CalcElements/environment.sml Wed Nov 13 12:06:40 2019 +0100
1.2 +++ b/src/Tools/isac/CalcElements/environment.sml Wed Nov 13 15:27:17 2019 +0100
1.3 @@ -9,11 +9,11 @@
1.4 val env2str: Rule.subst -> string
1.5 val subst2str: Rule.subst -> string
1.6 val subst2str': Rule.subst -> string
1.7 - val upd_env: T -> term * term -> T
1.8 - val upd_env': term -> term * T -> T
1.9 - val upd_env_opt: T -> term option * term -> T
1.10 - val upd_env_opt': T * (term option * term) -> T
1.11 - val upd_env_opt'': ((term * T) * term option) -> T
1.12 + val update: T -> term * term -> T
1.13 + val update': term -> term * T -> T
1.14 + val update_opt: T -> term option * term -> T
1.15 + val update_opt': T * (term option * term) -> T
1.16 + val update_opt'': ((term * T) * term option) -> T
1.17
1.18 end
1.19
1.20 @@ -34,20 +34,20 @@
1.21 val env2str = subst2str;
1.22
1.23 (* update environment; t <> empty if coming from listexpr *)
1.24 -fun upd_env env (id, vl) =
1.25 +fun update env (id, vl) =
1.26 let val env' = if vl = Rule.e_term then env else overwrite (env, (id, vl));
1.27 in env' end;
1.28 -fun upd_env' id (vl, env) = upd_env env (id, vl)
1.29 +fun update' id (vl, env) = update env (id, vl)
1.30
1.31 (*WN020526: not clear, when a is available in scan_up1 for eval_true*)
1.32 (*WN060906: in "fun handle_leaf" eg. uses "SOME M__"(from some PREVIOUS
1.33 curried Rewrite) for CURRENT value (which may be different from PREVIOUS);
1.34 thus "NONE" must be set at the end of currying (ill designed anyway)*)
1.35 -fun upd_env_opt env (SOME id, vl) = upd_env env (id, vl)
1.36 - | upd_env_opt env (NONE, vl) =
1.37 - ((**)tracing ("*** upd_env_opt: (NONE," ^ Rule.term2str vl ^ ")");(**) env);
1.38 -fun upd_env_opt' (env, (id, vl)) = upd_env_opt env (id, vl)
1.39 -fun upd_env_opt'' ((vl, env), id) = upd_env_opt env (id, vl)
1.40 +fun update_opt env (SOME id, vl) = update env (id, vl)
1.41 + | update_opt env (NONE, vl) =
1.42 + ((**)tracing ("*** update_opt: (NONE," ^ Rule.term2str vl ^ ")");(**) env);
1.43 +fun update_opt' (env, (id, vl)) = update_opt env (id, vl)
1.44 +fun update_opt'' ((vl, env), id) = update_opt env (id, vl)
1.45
1.46
1.47 (**)end(**)
2.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Wed Nov 13 12:06:40 2019 +0100
2.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Wed Nov 13 15:27:17 2019 +0100
2.3 @@ -140,16 +140,16 @@
2.4 NasApp (ist', _, _) =>
2.5 scan_dn1 xxx (ist' |> path_down [R, D] |> upd_env' (TermC.mk_Free (id, T)) |> trans_ass ist) b
2.6 | NasNap (v, E) =>
2.7 - scan_dn1 xxx (ist |> path_down [R, D] |> upd_env (Env.upd_env E (TermC.mk_Free (id, T), v))) b
2.8 + scan_dn1 xxx (ist |> path_down [R, D] |> upd_env (Env.update E (TermC.mk_Free (id, T), v))) b
2.9 | ay => ay)
2.10
2.11 | scan_dn1 xxx (ist as {eval, ...}) (Const ("Tactical.While"(*1*), _) $ c $ e $ a) =
2.12 if Rewrite.eval_true_ "Isac_Knowledge" eval
2.13 - (subst_atomic (ist |> get_act_env |> Env.upd_env' a) c)
2.14 + (subst_atomic (ist |> get_act_env |> Env.update' a) c)
2.15 then scan_dn1 xxx (ist |> path_down [L, R] |> upd_form a) e
2.16 else NasNap (ist |> get_act_env)
2.17 | scan_dn1 xxx (ist as {eval, ...}) (Const ("Tactical.While"(*2*),_) $ c $ e) =
2.18 - if Rewrite.eval_true_ "Isac_Knowledge" eval (subst_atomic (Env.upd_env_opt' (get_subst ist)) c)
2.19 + if Rewrite.eval_true_ "Isac_Knowledge" eval (subst_atomic (Env.update_opt' (get_subst ist)) c)
2.20 then scan_dn1 xxx (ist |> path_down [R]) e
2.21 else NasNap (ist |> get_act_env)
2.22
2.23 @@ -171,7 +171,7 @@
2.24 | ay => (ay))
2.25
2.26 | scan_dn1 xxx (ist as {eval, ...}) (Const ("Tactical.If", _) $ c $ e1 $ e2) =
2.27 - if Rewrite.eval_true_ "Isac_Knowledge" eval (subst_atomic (Env.upd_env_opt' (get_subst ist)) c)
2.28 + if Rewrite.eval_true_ "Isac_Knowledge" eval (subst_atomic (Env.update_opt' (get_subst ist)) c)
2.29 then scan_dn1 xxx (ist |> path_down [L, R]) e1
2.30 else scan_dn1 xxx (ist |> path_down [R]) e2
2.31
2.32 @@ -180,7 +180,7 @@
2.33 (case Lucin.handle_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t of
2.34 (a', Celem.Expr _) =>
2.35 (NasNap (Rewrite.eval_listexpr_ (Celem.assoc_thy "Isac_Knowledge") eval
2.36 - (subst_atomic (Env.upd_env_opt'' (get_act_env ist, a')) t), env))
2.37 + (subst_atomic (Env.update_opt'' (get_act_env ist, a')) t), env))
2.38 | (a', Celem.STac stac) =>
2.39 (case Lucin.associate pt ctxt (tac, stac) of
2.40 (* HERE ----------------vvvv ContextC.insert_assumptions asm ctxt DONE *)
2.41 @@ -236,7 +236,7 @@
2.42 | scan_up1 yyy ist (Const ("HOL.Let"(*3*), _) $ _ $ (Abs _)) = go_scan_up1 yyy ist
2.43
2.44 | scan_up1 (yyy as (prog, xxx as (cstate, _, _))) (ist as {eval, ...}) (t as Const ("Tactical.While"(*1*),_) $ c $ e $ a) =
2.45 - if Rewrite.eval_true_ "Isac_Knowledge" eval (subst_atomic (Env.upd_env' a (get_act_env ist)) c)
2.46 + if Rewrite.eval_true_ "Isac_Knowledge" eval (subst_atomic (Env.update' a (get_act_env ist)) c)
2.47 then
2.48 case scan_dn1 xxx (ist |> path_down_form ([L, R], a) |> upd_or Aundef) e of
2.49 NasNap (v, E') => go_scan_up1 yyy (ist |> upd_act_env (v, E') |> upd_form a)
2.50 @@ -245,7 +245,7 @@
2.51 | ay => ay
2.52 else go_scan_up1 yyy (ist |> upd_form a)
2.53 | scan_up1 (yyy as (prog, xxx as (cstate, _, _))) (ist as {eval, ...}) (t as Const ("Tactical.While"(*2*), _) $ c $ e) =
2.54 - if Rewrite.eval_true_ "Isac_Knowledge" eval (subst_atomic (Env.upd_env_opt' (get_subst ist)) c)
2.55 + if Rewrite.eval_true_ "Isac_Knowledge" eval (subst_atomic (Env.update_opt' (get_subst ist)) c)
2.56 then
2.57 case scan_dn1 xxx (ist |> path_down [R] |> upd_or Aundef) e of
2.58 NasNap (v, E') => go_scan_up1 yyy (ist |> upd_act_env (v, E'))
2.59 @@ -340,11 +340,11 @@
2.60 | rrr => rrr)
2.61
2.62 | scan_dn2 (xxx as (_, ctxt)) (ist as {eval, ...}) (Const ("Tactical.While"(*1*), _) $ c $ e $ a) =
2.63 - if Rewrite.eval_true_ ctxt eval (subst_atomic (ist |> get_act_env |> Env.upd_env' a) c)
2.64 + if Rewrite.eval_true_ ctxt eval (subst_atomic (ist |> get_act_env |> Env.update' a) c)
2.65 then scan_dn2 xxx (ist |> path_down_form ([L, R], a)) e
2.66 else Skip (get_act_env ist)
2.67 | scan_dn2 (xxx as (_, ctxt)) (ist as {eval, ...}) (Const ("Tactical.While"(*2*), _) $ c $ e) =
2.68 - if Rewrite.eval_true_ ctxt eval (subst_atomic (Env.upd_env_opt' (get_subst ist)) c)
2.69 + if Rewrite.eval_true_ ctxt eval (subst_atomic (Env.update_opt' (get_subst ist)) c)
2.70 then scan_dn2 xxx (ist |> path_down [R]) e
2.71 else Skip (get_act_env ist)
2.72
2.73 @@ -358,7 +358,7 @@
2.74 | _ => scan_dn2 xxx (ist |> path_down [R]) e2)
2.75
2.76 | scan_dn2 (xxx as (_, ctxt)) (ist as {eval, ...}) (Const ("Tactical.If"(*1*), _) $ c $ e1 $ e2) =
2.77 - if Rewrite.eval_true_ ctxt eval (subst_atomic (Env.upd_env_opt' (get_subst ist)) c)
2.78 + if Rewrite.eval_true_ ctxt eval (subst_atomic (Env.update_opt' (get_subst ist)) c)
2.79 then scan_dn2 xxx (ist |> path_down [L, R]) e1
2.80 else scan_dn2 xxx (ist |> path_down [R]) e2
2.81
2.82 @@ -427,7 +427,7 @@
2.83
2.84 (* no appy_: never causes Napp -> Helpless *)
2.85 | scan_up2 (yyy as (_, xxx as (_, ctxt))) (ist as {eval, ...}) (Const ("Tactical.While"(*1*), _) $ c $ e $ _) =
2.86 - if Rewrite.eval_true_ ctxt eval (subst_atomic (Env.upd_env_opt' (get_subst ist)) c)
2.87 + if Rewrite.eval_true_ ctxt eval (subst_atomic (Env.update_opt' (get_subst ist)) c)
2.88 then
2.89 case scan_dn2 xxx (ist |> path_down [L, R]) e of
2.90 Appy lr => Appy lr
2.91 @@ -437,7 +437,7 @@
2.92 go_scan_up2 yyy (ist |> upd_appy Skip_)
2.93 (* no appy_: never causes Napp - Helpless *)
2.94 | scan_up2 (yyy as (_, xxx as (_, ctxt))) (ist as {eval, ...}) (Const ("Tactical.While"(*2*), _) $ c $ e) =
2.95 - if Rewrite.eval_true_ ctxt eval (subst_atomic (Env.upd_env_opt' (get_subst ist)) c)
2.96 + if Rewrite.eval_true_ ctxt eval (subst_atomic (Env.update_opt' (get_subst ist)) c)
2.97 then
2.98 case scan_dn2 xxx (ist |> path_down [R]) e of
2.99 Appy lr => Appy lr
3.1 --- a/src/Tools/isac/Interpret/script.sml Wed Nov 13 12:06:40 2019 +0100
3.2 +++ b/src/Tools/isac/Interpret/script.sml Wed Nov 13 15:27:17 2019 +0100
3.3 @@ -87,13 +87,13 @@
3.4 | rew_only _ = false;
3.5
3.6 (* functions for the environment stack: NOT YET IMPLEMENTED
3.7 -fun accessenv id es = the (assoc ((top es) : Env.upd_env, id))
3.8 - handle _ => error ("accessenv: " ^ free2str id ^ " not in Env.upd_env");
3.9 -fun updateenv id vl (es : Env.upd_env stack) =
3.10 - (push (overwrite(top es, (id, vl))) (pop es)) : Env.upd_env stack;
3.11 -fun pushenv id vl (es : Env.upd_env stack) =
3.12 - (push (overwrite(top es, (id, vl))) es) : Env.upd_env stack;
3.13 -val popenv = pop : Env.upd_env stack -> Env.upd_env stack;
3.14 +fun accessenv id es = the (assoc ((top es) : Env.update, id))
3.15 + handle _ => error ("accessenv: " ^ free2str id ^ " not in Env.update");
3.16 +fun updateenv id vl (es : Env.update stack) =
3.17 + (push (overwrite(top es, (id, vl))) (pop es)) : Env.update stack;
3.18 +fun pushenv id vl (es : Env.update stack) =
3.19 + (push (overwrite(top es, (id, vl))) es) : Env.update stack;
3.20 +val popenv = pop : Env.update stack -> Env.update stack;
3.21 *)
3.22
3.23 fun de_esc_underscore str =
3.24 @@ -127,7 +127,7 @@
3.25 NONE => raise ERROR (errmsg2 d itms)
3.26 | SOME (_, _, _, _, itm_) => Model.penvval_in itm_
3.27 (*| SOME (_,_,_,_,itm_) => mk_arg thy (Model.d_in itm_) (ts_in itm_);
3.28 - penv postponed; presently penv holds already Env.upd_env for script*)
3.29 + penv postponed; presently penv holds already Env.update for script*)
3.30 val pats = (#ppc o Specify.get_met) mI
3.31 val _ = if pats = [] then raise ERROR errmsg else ()
3.32 in (flat o (map (itm2arg itms))) pats end;
3.33 @@ -567,7 +567,7 @@
3.34 in srls end
3.35
3.36 (* decide, where to get program/istate from:
3.37 - (* 1 *) from PblObj.Env.upd_env: at begin of program if no init_form
3.38 + (* 1 *) from PblObj.Env.update: at begin of program if no init_form
3.39 (* 2 *) from PblObj/PrfObj: if Prog_Tac is in the middle of the program
3.40 (* 3 *) from rls/PrfObj: in case of Math_Engine.detailstep *)
3.41 fun from_pblobj_or_detail' _ (p, p_) pt =
3.42 @@ -637,7 +637,7 @@
3.43 a leaf is either a tactic or an 'expr' in "let v = expr"
3.44 where "expr" does not contain a tactic.
3.45 Handling a leaf comprises
3.46 - (1) 'subst_stacexpr' substitute Env.upd_env and complete curried tactic
3.47 + (1) 'subst_stacexpr' substitute Env.update and complete curried tactic
3.48 (2) rewrite the leaf by 'srls'
3.49 *)
3.50 fun handle_leaf call thy srls (E, (a, v)) t =
3.51 @@ -645,7 +645,7 @@
3.52 case Prog_Tac.subst_stacexpr E a v t of
3.53 (a', Celem.STac stac) => (* Prog_Tac *)
3.54 let val stac' =
3.55 - Rewrite.eval_listexpr_ (Celem.assoc_thy thy) srls (subst_atomic (Env.upd_env_opt E (a,v)) stac)
3.56 + Rewrite.eval_listexpr_ (Celem.assoc_thy thy) srls (subst_atomic (Env.update_opt E (a,v)) stac)
3.57 in
3.58 (if (! trace_script)
3.59 then tracing ("@@@ "^call^" leaf '" ^ Rule.term2str t ^ "' ---> STac '" ^ Rule.term2str stac ^ "'")
3.60 @@ -654,7 +654,7 @@
3.61 end
3.62 | (a', Celem.Expr lexpr) => (* Prog_Expr *)
3.63 let val lexpr' =
3.64 - Rewrite.eval_listexpr_ (Celem.assoc_thy thy) srls (subst_atomic (Env.upd_env_opt E (a,v)) lexpr)
3.65 + Rewrite.eval_listexpr_ (Celem.assoc_thy thy) srls (subst_atomic (Env.update_opt E (a,v)) lexpr)
3.66 in
3.67 (if (! trace_script)
3.68 then tracing("@@@ "^call^" leaf '" ^ Rule.term2str t ^ "' ---> Expr '" ^ Rule.term2str lexpr' ^ "'")
4.1 --- a/src/Tools/isac/MathEngBasic/istate.sml Wed Nov 13 12:06:40 2019 +0100
4.2 +++ b/src/Tools/isac/MathEngBasic/istate.sml Wed Nov 13 15:27:17 2019 +0100
4.3 @@ -178,10 +178,10 @@
4.4 or = or, finish = finish, assoc = true}
4.5
4.6 fun upd_env' form {env, path, eval, form_arg, act_arg, or, finish, assoc} =
4.7 - {env = Env.upd_env env (form, act_arg), path = path, eval = eval, form_arg = form_arg,
4.8 + {env = Env.update env (form, act_arg), path = path, eval = eval, form_arg = form_arg,
4.9 act_arg = act_arg, or = or, finish = finish, assoc = assoc}
4.10 fun upd_env'' (env, (form, act)) {path, eval, or, finish, assoc, ...} =
4.11 - {env = Env.upd_env env (form, act), path = path, eval = eval, form_arg = SOME form, act_arg = act,
4.12 + {env = Env.update env (form, act), path = path, eval = eval, form_arg = SOME form, act_arg = act,
4.13 or = or, finish = finish, assoc = assoc}
4.14
4.15
5.1 --- a/src/Tools/isac/ProgLang/Prog_Tac.thy Wed Nov 13 12:06:40 2019 +0100
5.2 +++ b/src/Tools/isac/ProgLang/Prog_Tac.thy Wed Nov 13 15:27:17 2019 +0100
5.3 @@ -178,7 +178,7 @@
5.4 | NONE => ((subst_atomic E t) $ v)))
5.5 (*now all tactics are matched out and this leaf must be without a tactic*)
5.6 | subst_stacexpr E a v t =
5.7 - (a, Celem.Expr (subst_atomic (case a of SOME a => Env.upd_env E (a,v) | NONE => E) t));
5.8 + (a, Celem.Expr (subst_atomic (case a of SOME a => Env.update E (a,v) | NONE => E) t));
5.9
5.10 (**)end(**)
5.11 \<close> ML \<open>
6.1 --- a/src/Tools/isac/TODO.thy Wed Nov 13 12:06:40 2019 +0100
6.2 +++ b/src/Tools/isac/TODO.thy Wed Nov 13 15:27:17 2019 +0100
6.3 @@ -15,7 +15,7 @@
6.4 \begin{itemize}
6.5 \item xxx
6.6 \item + test/..
6.7 - rename Env.upd_env -> Env.update & Co.
6.8 + rename Env.update -> Env.update & Co.
6.9 \item xxx
6.10 \item finalise changes in istate, scan_dn2, scan_dn1 & Co
6.11 \begin{itemize}
7.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Wed Nov 13 12:06:40 2019 +0100
7.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Wed Nov 13 15:27:17 2019 +0100
7.3 @@ -52,7 +52,7 @@
7.4 val srls = Lucin.get_simplifier (pt, pos)
7.5 val (is, env, ctxt, sc) = case Lucin.init_pstate srls ctxt itms mI of
7.6 (is as Istate.Pstate {env, ...}, ctxt, sc) => (is, env, ctxt, sc)
7.7 - | _ => error "solve Apply_Method: uncovered case init_pstate"
7.8 + | _ => error "solve Apply_Method: uncovered case init_pstate";
7.9 (*+*)scrstate2str (the_pstate is) = "([\"\n(f_f, x ^^^ 2 + 1)\",\"\n(v_v, x)\"], [], e_rls, NONE, \n??.empty, Aundef, AppUndef_, true)";
7.10 val ini = Lucin.init_form thy sc env;
7.11 val p = lev_dn p;
8.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml Wed Nov 13 12:06:40 2019 +0100
8.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml Wed Nov 13 15:27:17 2019 +0100
8.3 @@ -228,7 +228,7 @@
8.4 val l = drop_last l; (*comes from e, goes to Abs*)
8.5 val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go l sc;
8.6 val i = mk_Free (i, T);
8.7 - val E = Env.upd_env E (i, v);
8.8 + val E = Env.update E (i, v);
8.9 (*Type error ...: Can't unify _a to pos * pos_ (Incompatible types)*)
8.10 val [(tac_, mout, ctree, pos', xxx)] = ss;
8.11 val ss = [(tac_, mout, ctree, pos', []:(pos * pos_) list)];
9.1 --- a/test/Tools/isac/Knowledge/rateq.sml Wed Nov 13 12:06:40 2019 +0100
9.2 +++ b/test/Tools/isac/Knowledge/rateq.sml Wed Nov 13 15:27:17 2019 +0100
9.3 @@ -116,7 +116,7 @@
9.4 val up = drop_last l;
9.5 val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go up sc; (*Const ("Prog_Tac.SubProblem",..*)
9.6 val i = mk_Free (i, T);
9.7 -val E = Env.upd_env E (i, v);
9.8 +val E = Env.update E (i, v);
9.9 "~~~~~ fun scan_dn2, args:"; val ((thy as (th,sr)), (pt, p), E, l, t, a, v) =
9.10 (thy, ptp, E, (up@[R,D]), body, a, v);
9.11 "~~~~~ fun handle_leaf, args:"; val (call, thy, srls, (E, (a, v)), t) = ("next ", th, sr, (E, (a, v)), t);
10.1 --- a/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Wed Nov 13 12:06:40 2019 +0100
10.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Wed Nov 13 15:27:17 2019 +0100
10.3 @@ -107,7 +107,7 @@
10.4 "~~~~~ from subst_stacexpr to handle_leaf return val:"; val ((a', STac stac))
10.5 = ((NONE : term option, STac (subst_atomic E t)));
10.6 val stac' =
10.7 - Rewrite.eval_listexpr_ (Celem.assoc_thy thy) srls (subst_atomic (upd_env_opt E (a,v)) stac);
10.8 + Rewrite.eval_listexpr_ (Celem.assoc_thy thy) srls (subst_atomic (update_opt E (a,v)) stac);
10.9
10.10 (*return value*) (a', STac stac');
10.11 "~~~~~ from handle_leaf to scan_dn1 return val:"; val (a', STac stac)
11.1 --- a/test/Tools/isac/Minisubpbl/700-interSteps.sml Wed Nov 13 12:06:40 2019 +0100
11.2 +++ b/test/Tools/isac/Minisubpbl/700-interSteps.sml Wed Nov 13 15:27:17 2019 +0100
11.3 @@ -187,7 +187,7 @@
11.4
11.5 "~~~~~ from subst_stacexpr to handle_leaf return val:"; val (a', Celem.STac stac) =
11.6 ((a, Celem.STac (subst_atomic E (t $ a'))));
11.7 - val stac' = Rewrite.eval_listexpr_ (Celem.assoc_thy thy) srls (subst_atomic (upd_env_opt E (a,v)) stac)
11.8 + val stac' = Rewrite.eval_listexpr_ (Celem.assoc_thy thy) srls (subst_atomic (update_opt E (a,v)) stac)
11.9 (*------------------------------------------- HERE IS A SECOND subst_atomic ?!?*)
11.10 ;
11.11 "~~~~~ from handle_leaf to scan_dn2 return val:"; val (a', Celem.STac stac) = (a', Celem.STac stac);