diff --git a/src/socExecEvalPredef.ml b/src/socExecEvalPredef.ml
index 39bc5652314f6d993e0fee3b592d8fb853de0e51..6d67de26d45090b2ed2798e95c0a48cb0c5add2d 100644
--- a/src/socExecEvalPredef.ml
+++ b/src/socExecEvalPredef.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 19/03/2013 (at 14:40) by Erwan Jahier> *)
+(* Time-stamp: <modified the 20/03/2013 (at 17:25) by Erwan Jahier> *)
 
 open SocExecValue
 open Soc
@@ -7,59 +7,59 @@ open Soc
 
 let (lustre_plus : ctx -> ctx) =
   fun ctx -> 
-    let ns = 
+    let (vn,vv) =
       match [get_val "x" ctx; get_val "y" ctx] with
         | [I x1; I x2] -> "z"::ctx.cpath,I(x1+x2)
         | [F i1; F i2] -> "z"::ctx.cpath,F(i1+.i2)
         | [U; _] | [_;U] -> "z"::ctx.cpath,U
         |  _  -> assert false
     in
-    { ctx with s = sadd ctx.s ns }
+    { ctx with s = sadd ctx.s vn vv }
 
 let lustre_times ctx =
-  let ns = 
+  let (vn,vv) = 
     match ([get_val "x" ctx; get_val "y" ctx]) with
       | [I x1; I x2] -> "z"::ctx.cpath,I(x1 * x2)
       | [F x1; F x2] -> "z"::ctx.cpath,F(x1 *. x2)
       | [U; _] | [_;U] -> "z"::ctx.cpath,U
       | _  -> assert false
   in
-  { ctx with s = sadd ctx.s ns }
+  { ctx with s = sadd ctx.s vn vv }
 
 
 let lustre_div ctx =
-  let ns = 
+  let (vn,vv) = 
     match ([get_val "x" ctx; get_val "y" ctx]) with
       | [I x1; I x2] -> "z"::ctx.cpath,I(x1 / x2)
       | [F x1; F x2] -> "z"::ctx.cpath,F(x1 /. x2)
       | [U; _] | [_;U] -> "z"::ctx.cpath,U
       | _  -> assert false
   in
-  { ctx with s = sadd ctx.s ns }
+  { ctx with s = sadd ctx.s vn vv }
 
 
 let lustre_minus ctx =
-  let ns = 
+  let (vn,vv) = 
     match ([get_val "x" ctx; get_val "y" ctx]) with
       | [I x1; I x2] -> "z"::ctx.cpath,I(x1 - x2)
       | [F x1; F x2] -> "z"::ctx.cpath,F(x1 -. x2)
       | [U; _] | [_;U] -> "z"::ctx.cpath,U
       | _  -> assert false
   in
-  { ctx with s = sadd ctx.s ns }
+  { ctx with s = sadd ctx.s vn vv }
 
 let lustre_mod ctx =
-  let ns = 
+  let (vn,vv) = 
     match ([get_val "x" ctx; get_val "y" ctx]) with
       | [I x1; I x2] -> "z"::ctx.cpath,I(x1 mod x2)
       | [U; _] | [_;U] -> "z"::ctx.cpath,U
       | _  -> assert false
   in
-  { ctx with s = sadd ctx.s ns }
+  { ctx with s = sadd ctx.s vn vv }
 
 
 let lustre_eq ctx =
-  let ns = 
+  let (vn,vv) = 
     match ([get_val "x" ctx; get_val "y" ctx]) with
       | [I x1; I x2] -> "z"::ctx.cpath,B(x1 = x2)
       | [F x1; F x2] -> "z"::ctx.cpath,B(x1 = x2)
@@ -67,129 +67,129 @@ let lustre_eq ctx =
       | [U; _] | [_;U] -> "z"::ctx.cpath,U
       | _  -> assert false
   in
-  { ctx with s = sadd ctx.s ns }
+  { ctx with s = sadd ctx.s vn vv }
 
 let lustre_uminus ctx =
-  let ns = 
+  let (vn,vv) = 
     match ([get_val "x" ctx]) with
       | [I x1] -> "z"::ctx.cpath,I(- x1)
       | [F x1] -> "z"::ctx.cpath,F(-. x1)
       | [U; _] | [_;U] -> "z"::ctx.cpath,U
       | _  -> assert false
   in
-  { ctx with s = sadd ctx.s ns }
+  { ctx with s = sadd ctx.s vn vv }
 
 let lustre_real2int ctx =
-  let ns = 
+  let (vn,vv) = 
     match ([get_val "x" ctx]) with
       | [F x1] -> "z"::ctx.cpath,I(int_of_float x1)
       | [U] -> "z"::ctx.cpath,U
       | _  -> assert false
   in
-  { ctx with s = sadd ctx.s ns }
+  { ctx with s = sadd ctx.s vn vv }
 
 
 let lustre_int2real ctx =
-  let ns = 
+  let (vn,vv) = 
     match ([get_val "x" ctx]) with
       | [I x1] -> "z"::ctx.cpath,F(float_of_int x1)
       | [U] -> "z"::ctx.cpath,U
       | _  -> assert false
   in
-  { ctx with s = sadd ctx.s ns }
+  { ctx with s = sadd ctx.s vn vv }
 
 
 let lustre_not ctx =
-  let ns = 
+  let (vn,vv) = 
     match ([get_val "x" ctx]) with
       | [B x1] -> "z"::ctx.cpath,B(not x1)
       | [U] -> "z"::ctx.cpath,U
       | _  -> assert false
   in
-  { ctx with s = sadd ctx.s ns }
+  { ctx with s = sadd ctx.s vn vv }
 
 
 let lustre_lt ctx =
-  let ns = 
+  let (vn,vv) = 
     match ([get_val "x" ctx; get_val "y" ctx]) with
       | [I x1; I x2] -> "z"::ctx.cpath,B(x1 < x2)
       | [F x1; F x2] -> "z"::ctx.cpath,B(x1 < x2)
       | [U; _] | [_;U] -> "z"::ctx.cpath,U
       | _  -> assert false
   in
-  { ctx with s = sadd ctx.s ns }
+  { ctx with s = sadd ctx.s vn vv }
  
 let lustre_gt ctx =
-  let ns = 
+  let (vn,vv) = 
     match ([get_val "x" ctx; get_val "y" ctx]) with
       | [I x1; I x2] -> "z"::ctx.cpath,B(x1 > x2)
       | [F x1; F x2] -> "z"::ctx.cpath,B(x1 > x2)
       | [U; _] | [_;U] -> "z"::ctx.cpath,U
       | _  -> assert false
   in
-  { ctx with s = sadd ctx.s ns }
+  { ctx with s = sadd ctx.s vn vv }
 
 let lustre_lte ctx =
-  let ns = 
+  let (vn,vv) = 
     match ([get_val "x" ctx; get_val "y" ctx]) with
       | [I x1; I x2] -> "z"::ctx.cpath,B(x1 <= x2)
       | [F x1; F x2] -> "z"::ctx.cpath,B(x1 <= x2)
       | [U; _] | [_;U] -> "z"::ctx.cpath,U
       | _  -> assert false
   in
-  { ctx with s = sadd ctx.s ns }
+  { ctx with s = sadd ctx.s vn vv }
 
 let lustre_gte ctx =
-  let ns = 
+  let (vn,vv) = 
     match ([get_val "x" ctx; get_val "y" ctx]) with
       | [I x1; I x2] -> "z"::ctx.cpath,B(x1 >= x2)
       | [F x1; F x2] -> "z"::ctx.cpath,B(x1 >= x2)
       | [U; _] | [_;U] -> "z"::ctx.cpath,U
       | _  -> assert false
   in
-  { ctx with s = sadd ctx.s ns }
+  { ctx with s = sadd ctx.s vn vv }
 
 let lustre_and ctx =
-  let ns = 
+  let (vn,vv) = 
     match ([get_val "x" ctx; get_val "y" ctx]) with
       | [B x1; B x2] -> "z"::ctx.cpath,B(x1 && x2)
       | [U; _] | [_;U] -> "z"::ctx.cpath,U
       | _  -> assert false
   in
-  { ctx with s = sadd ctx.s ns }
+  { ctx with s = sadd ctx.s vn vv }
 
 
 let lustre_neq  ctx =
-  let ns = 
+  let (vn,vv) = 
     match ([get_val "x" ctx; get_val "y" ctx]) with
       | [B x1; B x2] -> "z"::ctx.cpath,B(x1 <> x2)
       | [U; _] | [_;U] -> "z"::ctx.cpath,U
       | _  -> assert false
   in
-  { ctx with s = sadd ctx.s ns }
+  { ctx with s = sadd ctx.s vn vv }
 
 
 let lustre_or  ctx =
-  let ns = 
+  let (vn,vv) = 
     match ([get_val "x" ctx; get_val "y" ctx]) with
       | [B x1; B x2] -> "z"::ctx.cpath,B(x1 || x2)
       | [U; _] | [_;U] -> "z"::ctx.cpath,U
       | _  -> assert false
   in
-  { ctx with s = sadd ctx.s ns }
+  { ctx with s = sadd ctx.s vn vv }
 
 
 let lustre_impl ctx =
-  let ns = 
+  let (vn,vv) = 
     match ([get_val "x" ctx; get_val "y" ctx]) with
       | [B x1; B x2] -> "z"::ctx.cpath,B(not x1 or x2)
       | [U; _] | [_;U] -> "z"::ctx.cpath,U
       | _  -> assert false
   in
-  { ctx with s = sadd ctx.s ns }
+  { ctx with s = sadd ctx.s vn vv }
 
 let lustre_if ctx =
-  let ns = 
+  let (vn,vv) = 
     match ([get_val "c" ctx; get_val "xt" ctx; get_val "xe" ctx]) with
       | [B c; I x1; I x2]  -> "z"::ctx.cpath,I(if c then x1 else x2)
       | [B c; F x1; F x2]  -> "z"::ctx.cpath,F(if c then x1 else x2)
@@ -203,14 +203,14 @@ let lustre_if ctx =
       | [U;_; _] | [_;U;U] -> "z"::ctx.cpath,U
       | _  -> assert false
   in
-  { ctx with s = sadd ctx.s ns }
+  { ctx with s = sadd ctx.s vn vv }
  
 let lustre_hat tl ctx =
   let i = match tl with
     | [_;Soc.Array(_,i)] -> i
     | _ -> assert false
   in
-  let ns = 
+  let (vn,vv) = 
     match ([get_val "x" ctx]) with
       | [B x]  -> "z"::ctx.cpath,A(Array.make i (B x))
       | [I x]  -> "z"::ctx.cpath,A(Array.make i (I x))
@@ -219,12 +219,12 @@ let lustre_hat tl ctx =
       | [U]  -> "z"::ctx.cpath,U
       | _  -> assert false
   in
-  { ctx with s = sadd ctx.s ns }
+  { ctx with s = sadd ctx.s vn vv }
  
 (* That one is different *)
 let lustre_xor ctx = assert false
 let lustre_diese ctx = assert false
-(*   let ns =  *)
+(*   let (vn,vv) =  *)
 (*     let values = [get_val "x" ctx; get_val "y" ctx] in *)
 (*     let l = List.filter (fun x -> x=B true) values in *)
 (*     "z"::ctx.cpath,B(List.length l = 1) *)
diff --git a/src/socExecValue.ml b/src/socExecValue.ml
index 7b7858d10dbf4fb21557e647cdd488ad11143028..d5874415351925737325a8133ea09fd221e597cf 100644
--- a/src/socExecValue.ml
+++ b/src/socExecValue.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 19/03/2013 (at 18:03) by Erwan Jahier> *)
+(* Time-stamp: <modified the 20/03/2013 (at 17:27) by Erwan Jahier> *)
 
 open Soc
 
@@ -15,6 +15,14 @@ let (path_to_string: ident list -> string) =
 
 type subst = (path * t)
 
+(* soc environnement holding memory values.
+
+   Each soc have a list of memories, which is actually a list of soc
+   instances (in the licc terminology). 
+
+   Hence we need a kind of mapping from instance list (the path in the
+   call tree) to values.
+*)
 (* type substs = subst list *)
 type substs =
   | Node of (ident * substs) list
@@ -25,12 +33,90 @@ type ctx = {
   s:substs;
 }
 
+(**************************************************************************)
+
+let rec (get_top_var_type : Soc.var_expr -> Soc.var_type) =
+  fun ve -> 
+    match ve with
+      | Var(_,vt)  -> vt
+      | Index(ve,_,_)  
+      | Field(ve, _)  -> get_top_var_type ve
+      | Const(id,_) -> assert false
+
+type access = Idx of int | Fld of ident
+
+let rec (get_access : Soc.var_expr -> access list) =
+  fun ve -> 
+    match ve with
+      | Var(id,_)  -> []
+      | Index(ve,i,_)  -> (Idx i)::(get_access ve)
+      | Field(ve, (n,_))  -> (Fld n)::(get_access ve)
+      | Const(id,_) -> assert false
+
+let rec (update_val : t -> t -> access list -> t) =
+  fun pre_v v access -> 
+(* Replace access(pre_v) by v in pre_v *)
+    match pre_v,access with
+      | _,[] -> v
+      | A a, (Idx i)::access -> 
+        let a_i = update_val a.(i) v access in
+        a.(i) <- a_i;
+        A a
+      | _,_ -> assert false (* finish me (field struct) *)
+
+let (update_leaf : var_expr -> t -> t -> substs) =
+  fun ve v pre_v -> 
+    let access = get_access ve in
+    let new_v = update_val pre_v v access in
+    Leaf(new_v)
+
+let rec (create_val : Soc.var_type -> t ->  access list -> t) =
+  fun vt v access ->
+(* The same as update in the case where no previous value exists *)
+    match vt,access with
+      | _,[] -> v
+      | Array(vt,size), (Idx i)::access -> 
+        let a = Array.make size U in
+        let a_i = create_val vt v access in
+        a.(i) <- a_i;
+        A a
+      | _,_ -> assert false (* finish me (field struct) *)
+
+let (create_leaf : var_expr -> t -> substs) =
+  fun ve v -> 
+    let access = get_access ve in
+    let top_vt = get_top_var_type ve in
+    let new_v = create_val top_vt v access in
+    Leaf(new_v)
+
+(* should be able to replace sadd actually *)
+let (sadd_partial : substs  -> var_expr -> path -> t -> substs) =
+  fun ct ve x v ->
+(* update ct by associating x::ve to v in ct ;  *)
+    let rec aux ct (x,v) =
+    match ct,x with
+      | Leaf(pre_v),[] -> update_leaf ve v pre_v
+      | Node(l),n::t -> (
+        try 
+          let s = aux (List.assoc n l) (t,v) in
+          Node((n,s)::(List.remove_assoc n l))
+        with Not_found -> 
+          if t = [] then Node((n, create_leaf ve v)::l)
+          else
+          let new_substs = aux (Node []) (t,v) in
+          Node((n,new_substs)::l)
+      )
+      | _,[] -> assert false
+      | Leaf(_),_ -> assert false
+    in
+    aux ct (List.rev x,v)
+
 (* let rec (sadd : substs -> subst -> substs) =  *)
 (*   fun ct (x,v) -> *)
 (*     (x,v)::(List.remove_assoc x ct) *)
 
-let  (sadd : substs -> subst -> substs) = 
-  fun ct (x,v) ->
+let (sadd : substs -> path -> t -> substs) = 
+  fun ct  x v ->
     let rec aux ct (x,v) =
     match ct,x with
       | Leaf(_),[] -> Leaf(v)
@@ -49,6 +135,10 @@ let  (sadd : substs -> subst -> substs) =
     in
     aux ct (List.rev x,v)
 
+
+(**************************************************************************)
+
+
 (* let filter_top_subst s = *)
 (*   List.fold_left *)
 (*     (fun acc (idl,v) ->  *)
@@ -219,7 +309,7 @@ let (substitute_args_and_params : var_expr list -> var list -> ctx -> substs) =
     assert (List.length args = List.length params);
     let arg_ctx = { ctx with cpath = List.tl ctx.cpath } in
     let s = List.map2 (fun arg (pn,_) -> pn::ctx.cpath, get_value arg_ctx arg) args params in
-    let s = List.fold_left sadd ctx.s s in 
+    let s = List.fold_left (fun acc (vn,vv) -> sadd acc vn vv) ctx.s s in 
     s     
 
 let (substitute_params_and_args : var list -> var_expr list -> ctx -> substs) = 
@@ -233,7 +323,7 @@ let (substitute_params_and_args : var list -> var_expr list -> ctx -> substs) =
       )
       args params
     in
-    let s = List.fold_left sadd ctx.s s in 
+    let s = List.fold_left (fun acc (vn,vv) -> sadd acc vn vv) ctx.s s in 
     s
 
 let empty_ctx: ctx = {
@@ -251,11 +341,11 @@ let rec (create_ctx : Soc.tbl -> Soc.t -> ctx) =
             | Some(vt, Some(value)) -> 
               let name = (SocPredef.get_mem_name soc.key vt)::cpath in
               let value = get_value empty_ctx value in
-              sadd mem (name,value)
+              sadd mem name value
             | Some(vt, None) -> 
               let name = (SocPredef.get_mem_name soc.key vt)::cpath in
               let value = U in 
-              sadd mem (name,value) 
+              sadd mem name value
             | None -> mem
         in 
         List.fold_left (init_instances cpath) mem soc.instances
diff --git a/src/socExecValue.mli b/src/socExecValue.mli
index acddabb49842a240d3a00d7274ccf4ff58178d9c..c540ba4560d5426e5862d8a4e88a18e342b5a818 100644
--- a/src/socExecValue.mli
+++ b/src/socExecValue.mli
@@ -1,17 +1,25 @@
-(* Time-stamp: <modified the 19/03/2013 (at 16:16) by Erwan Jahier> *)
+(* Time-stamp: <modified the 20/03/2013 (at 17:23) by Erwan Jahier> *)
 
 (** Manipulating data in the Soc interpreter  *)
 
 type t = | I of int | F of float | B of bool | E of Soc.ident | A of t array 
          | U (* to set uninitialized mem *)
-type subst = (Soc.ident list * t)
 
+type path = Soc.ident list
+type subst = (path * t)
+
+(* Not really a good name anymore. Memory ? *)
 type substs 
-(* = *)
-(*   | Node of (Soc.ident * substs) list *)
-(*   | Leaf of t *)
 
-val sadd : substs -> subst -> substs
+
+(* update the memory. The path correspond to a path in the call tree,
+   except the last ident that is the variable name we want to
+   associate a value to.
+*)
+val sadd : substs -> path -> t -> substs
+
+(* ditto, but in the case of a partial assignment (e.g., a[i] = something).  *)
+val sadd_partial : substs  -> Soc.var_expr -> path -> t -> substs
 
 
 type ctx = {