1.1 --- a/src/Tools/isac/CalcElements/environment.sml	Thu Oct 17 13:17:48 2019 +0200
     1.2 +++ b/src/Tools/isac/CalcElements/environment.sml	Fri Oct 18 16:18:14 2019 +0200
     1.3 @@ -12,6 +12,8 @@
     1.4    val upd_env: T -> term * term -> T
     1.5    val upd_env': term -> term * T -> T
     1.6    val upd_env_opt: T -> term option * term -> T
     1.7 +  val upd_env_opt': T * (term option * term) -> T
     1.8 +  val upd_env_opt'': ((term * T) * term option) -> T
     1.9  
    1.10  end
    1.11  
    1.12 @@ -21,6 +23,16 @@
    1.13  (**)
    1.14  type T = (term * term) list;
    1.15  
    1.16 +fun subst2str s =
    1.17 +    (strs2str o
    1.18 +      (map (
    1.19 +        Celem.linefeed o pair2str o (apsnd Rule.term2str) o (apfst Rule.term2str)))) s;
    1.20 +fun subst2str' s =
    1.21 +    (strs2str' o
    1.22 +     (map (
    1.23 +       pair2str o (apsnd Rule.term2str) o (apfst Rule.term2str)))) s;
    1.24 +val env2str = subst2str;
    1.25 +
    1.26  (* update environment; t <> empty if coming from listexpr *)
    1.27  fun upd_env env (v,t) =
    1.28    let val env' = if t = Rule.e_term then env else overwrite (env,(v,t));
    1.29 @@ -32,17 +44,10 @@
    1.30    curried Rewrite) for CURRENT value (which may be different from PREVIOUS);
    1.31    thus "NONE" must be set at the end of currying (ill designed anyway)*)
    1.32  fun upd_env_opt env (SOME a, v) = upd_env env (a, v)
    1.33 -  | upd_env_opt env (NONE, _) = 
    1.34 -      ((*tracing ("*** upd_env_opt: (NONE," ^ term2str v ^ ")");*) env);
    1.35 +  | upd_env_opt env (NONE, v) =
    1.36 +    ((**)tracing ("*** upd_env_opt: (NONE," ^ Rule.term2str v ^ ")");(**) env);
    1.37 +fun upd_env_opt' (env, (id, v)) = upd_env_opt env (id, v)
    1.38 +fun upd_env_opt'' ((v, env), id) = upd_env_opt env (id, v)
    1.39  
    1.40 -fun subst2str s =
    1.41 -    (strs2str o
    1.42 -      (map (
    1.43 -        Celem.linefeed o pair2str o (apsnd Rule.term2str) o (apfst Rule.term2str)))) s;
    1.44 -fun subst2str' s =
    1.45 -    (strs2str' o
    1.46 -     (map (
    1.47 -       pair2str o (apsnd Rule.term2str) o (apfst Rule.term2str)))) s;
    1.48 -val env2str = subst2str;
    1.49  
    1.50  (**)end(**)

     2.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml	Thu Oct 17 13:17:48 2019 +0200
     2.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml	Fri Oct 18 16:18:14 2019 +0200
     2.3 @@ -352,9 +352,9 @@
     2.4  
     2.5    | assy (ya as (_, srls, _, _)) (ist, ss) (Const ("Tactical.While"(*1*),_) $ c $ e $ a) =
     2.6      if Rewrite.eval_true_ "Isac_Knowledge" srls
     2.7 -      (subst_atomic (ist |> Istate.get_res_env |> Env.upd_env' a) c)
     2.8 +      (subst_atomic (ist |> Istate.get_act_env |> Env.upd_env' a) c)
     2.9      then assy ya (ist |> Istate.append_path [L, R] |> Istate.upd_curr (SOME a), ss) e
    2.10 -    else NasNap (Istate.get_res_env ist)
    2.11 +    else NasNap (Istate.get_act_env ist)
    2.12    | assy (ya as (_, srls, _, _)) (ist as (E,l,a,v,S,b),ss) (Const ("Tactical.While"(*2*),_) $ c $ e) =
    2.13      if Rewrite.eval_true_ "Isac_Knowledge" srls (subst_atomic (Env.upd_env_opt E (a,v)) c) 
    2.14      then assy ya ((E, l @ [Celem.R], a,v,S,b),ss) e

     3.1 --- a/src/Tools/isac/Specify/istate.sml	Thu Oct 17 13:17:48 2019 +0200
     3.2 +++ b/src/Tools/isac/Specify/istate.sml	Fri Oct 18 16:18:14 2019 +0200
     3.3 @@ -16,11 +16,25 @@
     3.4    val istates2str : T option * T option -> string
     3.5    val e_istate : T
     3.6  
     3.7 -(*val get_env : scrstate -> Env.T *)
     3.8 -  val get_res_env : scrstate -> (term * Env.T)
     3.9 +  val get_act_env : scrstate -> (term * Env.T)
    3.10 +  val get_subst : scrstate -> (Env.T * (term option * term))
    3.11 +  val get_assoc : scrstate -> bool
    3.12 +
    3.13 +  val trans_ass: scrstate -> scrstate -> scrstate
    3.14 +  val trans_env_act: scrstate -> scrstate -> scrstate
    3.15  
    3.16    val append_path : Celem.loc_ -> scrstate -> scrstate
    3.17 +  val append_path_form: (Celem.loc_ * term) -> scrstate -> scrstate
    3.18 +
    3.19 +  val upd_form : term  -> scrstate -> scrstate
    3.20    val upd_curr : term option -> scrstate -> scrstate
    3.21 +  val upd_env: Env.T -> scrstate -> scrstate
    3.22 +  val upd_env': term -> scrstate -> scrstate
    3.23 +  val upd_form_env: (term * Env.T) -> scrstate -> scrstate
    3.24 +(*val upd_act_env: (term * Env.T) -> scrstate -> scrstate*)
    3.25 +  val upd_subst: Env.T -> (term * term) -> scrstate -> scrstate
    3.26 +  val upd_subst_true: (term option * term) -> scrstate -> scrstate
    3.27 +  val upd_subst_false: (term option * term) -> scrstate -> scrstate
    3.28  
    3.29  end
    3.30  
    3.31 @@ -39,8 +53,8 @@
    3.32  	 Env.T(*stack*)  (* used to instantiate tac for checking associate
    3.33  		                12.03.noticed: e_ not updated during execution ?!? *)
    3.34  	 * Celem.loc_  (* location of tac in script                          *)
    3.35 -	 * term option (* argument of curried functions                      *)
    3.36 -	 * term        (* result value obtained by execution of Tactic.T
    3.37 +	 * term option (* FORMal ARGument of curried functions               *)
    3.38 +	 * term        (* ACTual ARGument (value) for execution of Tactic.T
    3.39  		                updated also after a derivation by 'new_val'       *)
    3.40  	 * safe        (* estimation of how result will be obtained          *)
    3.41  	 * bool;       (* true = strongly .., false = weakly associated: 
    3.42 @@ -75,14 +89,38 @@
    3.43    | istates2str (SOME ist, NONE) = "(#SOME " ^ istate2str ist ^ ",\n #NONE)"
    3.44    | istates2str (SOME i1, SOME i2) = "(#SOME " ^ istate2str i1 ^ ",\n #SOME " ^ istate2str i2 ^ ")";
    3.45  
    3.46 -fun get_res_env (env, _, _, res, _, _) = (res, env)
    3.47 -fun get_env (env, _, _, _, _, _) = env
    3.48 +fun get_act_env (env, _, _, act_arg, _, _) = (act_arg, env)
    3.49 +fun get_assoc (_, _, _, _, _, ass) = ass
    3.50 +fun get_subst (env, _, form_arg, act_arg, _, _) = (env, (form_arg, act_arg))
    3.51  
    3.52 -fun append_path path (env, p, curr, res, safe, assweak) =
    3.53 -  (env, p @ path, curr, res, safe, assweak)
    3.54 -fun upd_curr curr (env, path, _, res, safe, assweak) =
    3.55 -  (env, path, curr, res, safe, assweak)
    3.56 +fun trans_ass (_, _, _, _, _, ass) (env, path, form_arg, act_arg, safe, _) = 
    3.57 +  (env, path, form_arg, act_arg, safe, ass)
    3.58 +fun trans_env_act (env, _, _, act_arg, _, _) (_, path, form_arg, _, safe, ass) = 
    3.59 +  (env, path, form_arg, act_arg, safe, ass)
    3.60  
    3.61 +fun append_path path (env, p, form_arg, act_arg, safe, ass) =
    3.62 +  (env, p @ path, form_arg, act_arg, safe, ass)
    3.63 +fun append_path_form (path, form_arg) (env, p, _, act_arg, safe, ass) =
    3.64 +  (env, p @ path, SOME form_arg, act_arg, safe, ass)
    3.65 +
    3.66 +fun upd_form form (env, path, _, act_arg, safe, ass) =
    3.67 +  (env, path, SOME form, act_arg, safe, ass)
    3.68 +fun upd_curr form_arg (env, path, _, res, safe, ass) =
    3.69 +  (env, path, form_arg, res, safe, ass)
    3.70 +fun upd_env env (_, path, form_arg, act_arg, safe, ass) =
    3.71 +  (env, path, form_arg, act_arg, safe, ass)
    3.72 +fun upd_env' form (env, path, form_arg, act_arg, safe, ass) =
    3.73 +    (Env.upd_env env (form, act_arg), path, form_arg, act_arg, safe, ass)
    3.74 +fun upd_form_env (form_arg, env) (_, path, _, act_arg, safe, ass) =
    3.75 +  (env, path, SOME form_arg, act_arg, safe, ass)
    3.76 +(*fun upd_act_env (act_arg, env) (_, path, form_arg, _, safe, ass) =
    3.77 +  (env, path, form_arg, act_arg, safe, ass)*)
    3.78 +fun upd_subst env (form_arg, act_arg) (_, path, _, _, safe, ass) =
    3.79 +  (env, path, SOME form_arg, act_arg, safe, ass)
    3.80 +fun upd_subst_true (form_arg, act_arg) (env, path, _, _, safe, _) =
    3.81 +  (env, path, form_arg, act_arg, safe, true)
    3.82 +fun upd_subst_false (form_arg, act_arg) (env, path, _, _, safe, _) =
    3.83 +  (env, path, form_arg, act_arg, safe, false)
    3.84  
    3.85  end
    3.86  

     4.1 --- a/src/Tools/isac/TODO.thy	Thu Oct 17 13:17:48 2019 +0200
     4.2 +++ b/src/Tools/isac/TODO.thy	Fri Oct 18 16:18:14 2019 +0200
     4.3 @@ -48,9 +48,6 @@
     4.4      \item lucas-interpreter.sml         ----- vvvvvvvvv etc.
     4.5        val (p'',_,_,pt'') = Generate.generate1 @ {theory} tac' (Istate.Pstate is, ctxt) (po', p_) pt
     4.6    \item xxx
     4.7 -  \item fun fun eval_* //thy//
     4.8 -        collect into Prog_Expr.thy imports ???
     4.9 -        separate Prog_Tac.thy imports Complex_Main
    4.10    \item rm Float
    4.11    \item xxx
    4.12      \item signature LIBRARY_C
    4.13 @@ -373,6 +370,9 @@
    4.14  subsection \<open>replace theory/thy by context/ctxt\<close>
    4.15  text \<open>
    4.16    \begin{itemize}
    4.17 +  \item xxx
    4.18 +  \item ??? can theory be retrieved from ctxt ???
    4.19 +  \item xxx
    4.20    \item cleaup the many conversions string -- theory
    4.21    \item make dest_spec --> (theory, pblID, metID) ?+ common_subthy ?
    4.22    \item 1. Rewrite.eval_true_, then

     5.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml	Thu Oct 17 13:17:48 2019 +0200
     5.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml	Fri Oct 18 16:18:14 2019 +0200
     5.3 @@ -230,7 +230,7 @@
     5.4        val l = drop_last l; (*comes from e, goes to Abs*)
     5.5        val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go l sc;
     5.6        val i = mk_Free (i, T);
     5.7 -      val E = upd_env E (i, v);
     5.8 +      val E = Env.upd_env E (i, v);
     5.9  (*Type error ...: Can't unify _a to pos * pos_ (Incompatible types)*)
    5.10  val [(tac_, mout, ctree, pos', xxx)] = ss;
    5.11  val ss = [(tac_, mout, ctree, pos', []:(pos * pos_) list)];

     6.1 --- a/test/Tools/isac/Knowledge/rateq.sml	Thu Oct 17 13:17:48 2019 +0200
     6.2 +++ b/test/Tools/isac/Knowledge/rateq.sml	Fri Oct 18 16:18:14 2019 +0200
     6.3 @@ -117,7 +117,7 @@
     6.4  val up = drop_last l;
     6.5  val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go up sc; (*Const ("Prog_Tac.SubProblem",..*)
     6.6  val i = mk_Free (i, T);
     6.7 -val E = upd_env E (i, v);
     6.8 +val E = Env.upd_env E (i, v);
     6.9  "~~~~~ fun appy, args:"; val ((thy as (th,sr)), (pt, p), E, l, t, a, v) =
    6.10    (thy, ptp, E, (up@[R,D]), body, a, v);
    6.11  "~~~~~ fun handle_leaf, args:"; val (call, thy, srls, E, a, v, t) = ("next ", th, sr, E, a, v, t);

     7.1 --- a/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml	Thu Oct 17 13:17:48 2019 +0200
     7.2 +++ b/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml	Fri Oct 18 16:18:14 2019 +0200
     7.3 @@ -224,7 +224,7 @@
     7.4               Const ("HOL.Let",_) $ _ $ (Abs aa) => aa
     7.5             | t => error ("nxt_up..HOL.Let $ _ with " ^ Rule.term2str t))
     7.6          val i = TermC.mk_Free (i, T)
     7.7 -        val E = upd_env E (i, v);
     7.8 +        val E = Env.upd_env E (i, v);
     7.9  
    7.10    (*case*) appy thy ptp E (up @ [Celem.R, Celem.D]) body a v (*of*);
    7.11  "~~~~~ fun appy , args:"; val (thy, ptp, E, l, (Const ("HOL.Let",_) $ e $ (Abs (i,T,b))), a, v)

     8.1 --- a/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml	Thu Oct 17 13:17:48 2019 +0200
     8.2 +++ b/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml	Fri Oct 18 16:18:14 2019 +0200
     8.3 @@ -72,7 +72,7 @@
     8.4  val up = drop_last l;
     8.5  val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go up sc;
     8.6  val i = mk_Free (i, T);
     8.7 -val E = upd_env E (i, v);
     8.8 +val E = Env.upd_env E (i, v);
     8.9  body; (*= Const ("Prog_Tac.Check'_elementwise"*)
    8.10  "~~~~~ fun appy, args:"; val ((thy as (th,sr)), (pt, p), E, l, t, a, v)=
    8.11  (thy, ptp, E, (up@[R,D]), body, a, v);