1.1 --- a/src/Tools/isac/Specify/istate.sml	Thu Oct 17 13:17:48 2019 +0200
     1.2 +++ b/src/Tools/isac/Specify/istate.sml	Fri Oct 18 16:18:14 2019 +0200
     1.3 @@ -16,11 +16,25 @@
     1.4    val istates2str : T option * T option -> string
     1.5    val e_istate : T
     1.6  
     1.7 -(*val get_env : scrstate -> Env.T *)
     1.8 -  val get_res_env : scrstate -> (term * Env.T)
     1.9 +  val get_act_env : scrstate -> (term * Env.T)
    1.10 +  val get_subst : scrstate -> (Env.T * (term option * term))
    1.11 +  val get_assoc : scrstate -> bool
    1.12 +
    1.13 +  val trans_ass: scrstate -> scrstate -> scrstate
    1.14 +  val trans_env_act: scrstate -> scrstate -> scrstate
    1.15  
    1.16    val append_path : Celem.loc_ -> scrstate -> scrstate
    1.17 +  val append_path_form: (Celem.loc_ * term) -> scrstate -> scrstate
    1.18 +
    1.19 +  val upd_form : term  -> scrstate -> scrstate
    1.20    val upd_curr : term option -> scrstate -> scrstate
    1.21 +  val upd_env: Env.T -> scrstate -> scrstate
    1.22 +  val upd_env': term -> scrstate -> scrstate
    1.23 +  val upd_form_env: (term * Env.T) -> scrstate -> scrstate
    1.24 +(*val upd_act_env: (term * Env.T) -> scrstate -> scrstate*)
    1.25 +  val upd_subst: Env.T -> (term * term) -> scrstate -> scrstate
    1.26 +  val upd_subst_true: (term option * term) -> scrstate -> scrstate
    1.27 +  val upd_subst_false: (term option * term) -> scrstate -> scrstate
    1.28  
    1.29  end
    1.30  
    1.31 @@ -39,8 +53,8 @@
    1.32  	 Env.T(*stack*)  (* used to instantiate tac for checking associate
    1.33  		                12.03.noticed: e_ not updated during execution ?!? *)
    1.34  	 * Celem.loc_  (* location of tac in script                          *)
    1.35 -	 * term option (* argument of curried functions                      *)
    1.36 -	 * term        (* result value obtained by execution of Tactic.T
    1.37 +	 * term option (* FORMal ARGument of curried functions               *)
    1.38 +	 * term        (* ACTual ARGument (value) for execution of Tactic.T
    1.39  		                updated also after a derivation by 'new_val'       *)
    1.40  	 * safe        (* estimation of how result will be obtained          *)
    1.41  	 * bool;       (* true = strongly .., false = weakly associated: 
    1.42 @@ -75,14 +89,38 @@
    1.43    | istates2str (SOME ist, NONE) = "(#SOME " ^ istate2str ist ^ ",\n #NONE)"
    1.44    | istates2str (SOME i1, SOME i2) = "(#SOME " ^ istate2str i1 ^ ",\n #SOME " ^ istate2str i2 ^ ")";
    1.45  
    1.46 -fun get_res_env (env, _, _, res, _, _) = (res, env)
    1.47 -fun get_env (env, _, _, _, _, _) = env
    1.48 +fun get_act_env (env, _, _, act_arg, _, _) = (act_arg, env)
    1.49 +fun get_assoc (_, _, _, _, _, ass) = ass
    1.50 +fun get_subst (env, _, form_arg, act_arg, _, _) = (env, (form_arg, act_arg))
    1.51  
    1.52 -fun append_path path (env, p, curr, res, safe, assweak) =
    1.53 -  (env, p @ path, curr, res, safe, assweak)
    1.54 -fun upd_curr curr (env, path, _, res, safe, assweak) =
    1.55 -  (env, path, curr, res, safe, assweak)
    1.56 +fun trans_ass (_, _, _, _, _, ass) (env, path, form_arg, act_arg, safe, _) = 
    1.57 +  (env, path, form_arg, act_arg, safe, ass)
    1.58 +fun trans_env_act (env, _, _, act_arg, _, _) (_, path, form_arg, _, safe, ass) = 
    1.59 +  (env, path, form_arg, act_arg, safe, ass)
    1.60  
    1.61 +fun append_path path (env, p, form_arg, act_arg, safe, ass) =
    1.62 +  (env, p @ path, form_arg, act_arg, safe, ass)
    1.63 +fun append_path_form (path, form_arg) (env, p, _, act_arg, safe, ass) =
    1.64 +  (env, p @ path, SOME form_arg, act_arg, safe, ass)
    1.65 +
    1.66 +fun upd_form form (env, path, _, act_arg, safe, ass) =
    1.67 +  (env, path, SOME form, act_arg, safe, ass)
    1.68 +fun upd_curr form_arg (env, path, _, res, safe, ass) =
    1.69 +  (env, path, form_arg, res, safe, ass)
    1.70 +fun upd_env env (_, path, form_arg, act_arg, safe, ass) =
    1.71 +  (env, path, form_arg, act_arg, safe, ass)
    1.72 +fun upd_env' form (env, path, form_arg, act_arg, safe, ass) =
    1.73 +    (Env.upd_env env (form, act_arg), path, form_arg, act_arg, safe, ass)
    1.74 +fun upd_form_env (form_arg, env) (_, path, _, act_arg, safe, ass) =
    1.75 +  (env, path, SOME form_arg, act_arg, safe, ass)
    1.76 +(*fun upd_act_env (act_arg, env) (_, path, form_arg, _, safe, ass) =
    1.77 +  (env, path, form_arg, act_arg, safe, ass)*)
    1.78 +fun upd_subst env (form_arg, act_arg) (_, path, _, _, safe, ass) =
    1.79 +  (env, path, SOME form_arg, act_arg, safe, ass)
    1.80 +fun upd_subst_true (form_arg, act_arg) (env, path, _, _, safe, _) =
    1.81 +  (env, path, form_arg, act_arg, safe, true)
    1.82 +fun upd_subst_false (form_arg, act_arg) (env, path, _, _, safe, _) =
    1.83 +  (env, path, form_arg, act_arg, safe, false)
    1.84  
    1.85  end
    1.86