diff --git a/heptagon/heptagon.ml b/heptagon/heptagon.ml
index d4c45e0..1b7939f 100644
--- a/heptagon/heptagon.ml
+++ b/heptagon/heptagon.ml
@@ -150,19 +150,38 @@ type interface =
   and interface_desc =
   | Iopen of name | Itypedef of type_dec | Isignature of signature
 
-(* Helper functions to create AST. *) (*TODO refactor en mk_*)
-
+(* Helper functions to create AST. *)
 let mk_exp desc ty =
   { e_desc = desc; e_ty = ty; e_loc = no_location; }
   
 let mk_op op = { a_op = op; }
-  
+
+let mk_op_desc ln params kind =
+  { op_name = ln; op_params = params; op_kind = kind }
+
 let mk_type_dec name desc = 
   { t_name = name; t_desc = desc; t_loc = no_location; }
   
-let mk_equation desc =
-  { eq_desc = desc; eq_statefull = true; eq_loc = no_location; }
-    
+let mk_equation ?(statefull = true) desc =
+  { eq_desc = desc; eq_statefull = statefull; eq_loc = no_location; }
+
+let mk_var_dec ?(last = Var) name ty  =
+  { v_name = name; v_type = ty;
+    v_last = last; v_loc = Location.get_current_location () }
+
+let mk_block defnames eqs =
+  { b_local = []; b_equs = eqs; b_defnames = defnames;
+    b_statefull = true; b_loc = no_location }
+  
+let dfalse = mk_exp (Econst (Cconstr Initial.pfalse)) (Tid Initial.pbool)
+let dtrue = mk_exp (Econst (Cconstr Initial.ptrue)) (Tid Initial.pbool)
+  
+let mk_ifthenelse e1 e2 e3 =
+  { e3 with e_desc = Eapp(mk_op Eifthenelse, [e1; e2; e3]) }
+
+let mk_simple_equation pat e =
+  mk_equation ~statefull:false (Eeq(pat, e))
+
 (*
 let cfalse = Cconstr Initial.pfalse
   
diff --git a/heptagon/transformations/automata.ml b/heptagon/transformations/automata.ml
index 6ae138f..4b39af7 100644
--- a/heptagon/transformations/automata.ml
+++ b/heptagon/transformations/automata.ml
@@ -10,26 +10,30 @@
 
 (* $Id$ *)
 
-open Location
 open Misc
 open Names
 open Ident
 open Heptagon
-open Global
-open Initial
-open Interference_graph
+open Types
 
-let rename_states env g = 
-  let rename_one n =
-    try
-      let olds = List.hd n.g_content in
-      let s = NamesEnv.find olds env in
-	Hashtbl.remove g.g_hash olds;
-	Hashtbl.add g.g_hash s n;
-	n.g_content <- [s]
-    with Not_found -> ()
-  in
-    List.iter rename_one g.g_nodes
+let mk_var_exp n ty =
+  mk_exp (Evar n) ty
+
+let mk_pair e1 e2 =
+  mk_exp (Etuple [e1;e2]) (Tprod [e1.e_ty; e2.e_ty])
+
+let mk_reset_equation eq_list e = 
+  mk_equation (Ereset (eq_list, e))
+
+let mk_switch_equation e l = 
+  mk_equation (Eswitch (e, l))
+
+let mk_exp_fby_false e = 
+  mk_exp (Eapp(mk_op (Epre (Some (Cconstr Initial.pfalse))), [e])) 
+    (Tid Initial.pbool)
+
+let mk_exp_fby_state initial e =
+  { e with e_desc = Eapp(mk_op (Epre (Some (Cconstr initial))), [e]) }
 
 (* the list of enumerated types introduced to represent states *)
 let state_type_dec_list = ref []
@@ -39,8 +43,8 @@ let intro_type states =
   let n = gen_symbol () in
   let state_type = "st" ^ n in
   state_type_dec_list :=
-    (tmake state_type (Type_enum(list states))) :: !state_type_dec_list;
-  Name(state_type)
+    (mk_type_dec state_type (Type_enum (list states))) :: !state_type_dec_list;
+    Name(state_type)
 
 (* an automaton may be a Moore automaton, i.e., with only weak transitions; *)
 (* a Mealy one, i.e., with only strong transition or mixed *)
@@ -49,41 +53,41 @@ let moore_mealy state_handlers =
     (moore or (l1 <> []), mealy or (l2 <> [])) in
   List.fold_left handler (false, false) state_handlers
 
-let rec translate_eq g (v, eq_list) eq =
+let rec translate_eq (v, eq_list) eq =
   match eq.eq_desc with
       Eautomaton(state_handlers) ->
-        translate_automaton g v eq_list state_handlers
+        translate_automaton v eq_list state_handlers
     | Eswitch(e, switch_handlers) ->
         v,
         { eq with eq_desc =
-            Eswitch(e, translate_switch_handlers g switch_handlers) }
+            Eswitch(e, translate_switch_handlers switch_handlers) }
         :: eq_list
     | Epresent(present_handlers, block) ->
         v, { eq with eq_desc =
-            Epresent(translate_present_handlers g present_handlers,
-                     translate_block g block) } :: eq_list
+            Epresent(translate_present_handlers present_handlers,
+                     translate_block block) } :: eq_list
     | Ereset(r_eq_list, e) ->
-        let v, r_eq_list = translate_eqs g v r_eq_list in
+        let v, r_eq_list = translate_eqs v r_eq_list in
         v, { eq with eq_desc = Ereset(r_eq_list, e) } :: eq_list
     | Eeq _ -> v, eq :: eq_list
 
-and translate_eqs g v eq_list = List.fold_left (translate_eq g) (v, []) eq_list
+and translate_eqs v eq_list = List.fold_left translate_eq (v, []) eq_list
 
-and translate_block g ({ b_local = v; b_equs = eq_list } as b) =
-  let v, eq_list = translate_eqs g v eq_list in
+and translate_block ({ b_local = v; b_equs = eq_list } as b) =
+  let v, eq_list = translate_eqs v eq_list in
   { b with b_local = v; b_equs = eq_list }
 
-and translate_switch_handlers g handlers =
+and translate_switch_handlers handlers =
   let translate_switch_handler { w_name = n; w_block = b } =
-    { w_name = n; w_block = translate_block g b } in
+    { w_name = n; w_block = translate_block b } in
   List.map translate_switch_handler handlers
 
-and translate_present_handlers g handlers =
+and translate_present_handlers handlers =
   let translate_present_handler { p_cond = e; p_block = b } =
-    { p_cond = e; p_block = translate_block g b } in
+    { p_cond = e; p_block = translate_block b } in
   List.map translate_present_handler handlers
 
-and translate_automaton g v eq_list handlers =
+and translate_automaton v eq_list handlers =
   let has_until, has_unless = moore_mealy handlers in
   let states =
     let suffix = gen_symbol () in
@@ -92,7 +96,7 @@ and translate_automaton g v eq_list handlers =
       NamesEnv.empty handlers in
 
   let statetype = intro_type states in
-  let tstatetype = Tbase(Tid(statetype)) in
+  let tstatetype = Tid statetype in
   let initial = Name(NamesEnv.find (List.hd handlers).s_state states) in
 
   let statename = Ident.fresh "s" in
@@ -101,84 +105,80 @@ and translate_automaton g v eq_list handlers =
   let next_resetname = Ident.fresh "nr" in
   let pre_next_resetname = Ident.fresh "pnr" in
 
-  (* update the states graph with the suffixed names *)
-  rename_states states g;
-
   let name n = Name(NamesEnv.find n states) in
-  let state n =
-    emake (Econst(Cconstr(name n))) tstatetype in
-  let statevar n = var n tstatetype in
-  let boolvar n = var n tybool in
+  let state n = mk_exp (Econst (Cconstr (name n))) tstatetype in
+  let statevar n = mk_var_exp n tstatetype in
+  let boolvar n = mk_var_exp n (Tid Initial.pbool) in
 
   let escapes n s rcont =
     let escape { e_cond = e; e_reset = r; e_next_state = n } cont =
-      ifthenelse e (pair (state n) (if r then dtrue else dfalse)) cont in
-    List.fold_right escape s (pair (state n) rcont) in
+      mk_ifthenelse e (mk_pair (state n) (if r then dtrue else dfalse)) cont in
+    List.fold_right escape s (mk_pair (state n) rcont) in
   let strong { s_state = n; s_unless = su } =
-    block
+    mk_block
       (Env.add statename tstatetype
-         (Env.add resetname tybool Env.empty))
-      ([reset(
-          [eq (Etuplepat[Evarpat(statename);Evarpat(resetname)])
+         (Env.add resetname (Tid Initial.pbool) Env.empty))
+      ([mk_reset_equation (
+          [mk_simple_equation (Etuplepat[Evarpat(statename);Evarpat(resetname)])
              (escapes n su (boolvar pre_next_resetname))])
           (boolvar pre_next_resetname)]) in
 
   let weak { s_state = n; s_block = b; s_until = su } =
-    let b = translate_block g b in
+    let b = translate_block b in
     { b with b_equs =
-        [reset ((eq (Etuplepat[Evarpat(next_statename);
+        [mk_reset_equation ((mk_simple_equation (Etuplepat[Evarpat(next_statename);
                                Evarpat(next_resetname)])
                    (escapes n su dfalse)) :: b.b_equs)
            (boolvar resetname)];
         (* (or_op (boolvar pre_next_resetname) (boolvar resetname))]; *)
         b_defnames =
         Env.add next_statename tstatetype
-          (Env.add next_resetname tybool
+          (Env.add next_resetname (Tid Initial.pbool)
              b.b_defnames)
     } in
   let v =
-      (param next_statename (Tid(statetype))) ::
-      (param resetname tbool) ::
-      (param next_resetname tbool) ::
-      (param pre_next_resetname tbool) :: v in
+      (mk_var_dec next_statename (Tid(statetype))) ::
+      (mk_var_dec resetname (Tid Initial.pbool)) ::
+      (mk_var_dec next_resetname (Tid Initial.pbool)) ::
+      (mk_var_dec pre_next_resetname (Tid Initial.pbool)) :: v in
   (* we optimise the case of an only strong automaton *)
   (* or only weak automaton *)
   match has_until, has_unless with
     | true, false ->
 	(* a Moore automaton with only weak transitions *)
-	v, (switch (fby_state initial (statevar next_statename))
+	v, (mk_switch_equation (mk_exp_fby_state initial (statevar next_statename))
 	       (List.map
 		   (fun ({ s_state = n } as case) ->
 		     { w_name = name n; w_block = weak case })
 		   handlers)) ::
-	  (eq (Evarpat pre_next_resetname) 
-	      (fby_false (boolvar (next_resetname)))) ::
-	      (eq (Evarpat resetname) (boolvar pre_next_resetname)) :: eq_list
+	  (mk_simple_equation (Evarpat pre_next_resetname) 
+	      (mk_exp_fby_false (boolvar (next_resetname)))) ::
+	      (mk_simple_equation (Evarpat resetname) (boolvar pre_next_resetname)) :: eq_list
     | _ ->
 	(* the general case; two switch to generate,
 	   statename variable used and defined *)
-	(param statename (Tid(statetype))) :: v,
-	(switch (fby_state initial (statevar next_statename))
+	(mk_var_dec statename (Tid statetype)) :: v,
+	(mk_switch_equation (mk_exp_fby_state initial (statevar next_statename))
 	    (List.map
 		(fun ({ s_state = n } as case) ->
 		  { w_name = name n; w_block = strong case })
 		handlers)) ::
-	  (switch (statevar statename)
+	  (mk_switch_equation (statevar statename)
 	      (List.map
 		  (fun ({ s_state = n } as case) ->
 		    { w_name = name n; w_block = weak case })
 		  handlers)) ::
-	  (eq (Evarpat pre_next_resetname) 
-	      (fby_false (boolvar (next_resetname)))) ::
+	  (mk_simple_equation (Evarpat pre_next_resetname) 
+	      (mk_exp_fby_false (boolvar (next_resetname)))) ::
 	  eq_list
 
-let translate_contract g ({ c_local = v; c_eq = eq_list} as c) =
-  let v, eq_list = translate_eqs g v eq_list in
+let translate_contract ({ c_local = v; c_eq = eq_list} as c) =
+  let v, eq_list = translate_eqs v eq_list in
   { c with c_local = v; c_eq = eq_list }
 
-let node ({ n_local = v; n_equs = eq_list; n_contract = contract; n_states_graph = g } as n) =
-  let v, eq_list = translate_eqs g v eq_list in
-  let contract = optional (translate_contract g) contract in
+let node ({ n_local = v; n_equs = eq_list; n_contract = contract } as n) =
+  let v, eq_list = translate_eqs v eq_list in
+  let contract = optional translate_contract contract in
   { n with n_local = v; n_equs = eq_list; n_contract = contract }
 
 let program ({ p_types = pt_list; p_nodes = n_list } as p) =
diff --git a/heptagon/transformations/completion.ml b/heptagon/transformations/completion.ml
index cfdeffa..57220b3 100644
--- a/heptagon/transformations/completion.ml
+++ b/heptagon/transformations/completion.ml
@@ -8,25 +8,19 @@
 (**************************************************************************)
 (* complete partial definitions with [x = last(x)] *)
 
-(* $Id$ *)
-
-open Location
-open Ident
 open Misc
 open Heptagon
-open Global
+open Ident
 
 (* adds an equation [x = last(x)] for every partially defined variable *)
 (* in a control structure *)
 let complete_with_last defined_names local_defined_names eq_list =
-  let last n ty =
-    { e_desc = Elast(n); e_ty = ty; e_linearity = Linearity.NotLinear;
-      e_loc = no_location } in
+  let last n ty = mk_exp (Elast n) ty in
   let equation n ty eq_list =
-    { eq_desc = Eeq(Evarpat(n), last n ty); eq_statefull = false;
-      eq_loc = no_location } :: eq_list in
+    (mk_equation (Eeq(Evarpat n, last n ty)))::eq_list
+  in
   let d = Env.diff defined_names local_defined_names in
-  Env.fold equation d eq_list
+    Env.fold equation d eq_list
 
 let rec translate_eq eq =
   match eq.eq_desc with
diff --git a/heptagon/transformations/every.ml b/heptagon/transformations/every.ml
index c7008e8..7e7ddea 100644
--- a/heptagon/transformations/every.ml
+++ b/heptagon/transformations/every.ml
@@ -15,42 +15,11 @@
    x = (f every r) e'
 *)
 
-(* $Id$ *)
-
-open Location
 open Misc
 open Ident
 open Heptagon
-open Global
-open Initial
 open Reset
 
-let eq pat e =
-  { eq_desc = Eeq(pat, e); eq_statefull = false; eq_loc = no_location }
-let statefulleq = Heptagon.eq
-
-(* add an equation *)
-let equation v acc_eq_list e =
-  let n = Ident.fresh "r" in
-  n,
-  (bool_param n) :: v,
-  { eq_desc = Eeq(Evarpat(n), e); eq_statefull = true; eq_loc = e.e_loc } ::
-    acc_eq_list
-
-let orthen v acc_eq_list res e =
-  match e.e_desc with
-      Evar(n) -> v, acc_eq_list, Rorthen(res, n)
-    | _ ->
-        let n, v, acc_eq_list = equation v acc_eq_list e in
-        v, acc_eq_list, Rorthen(res, n)
-
-let add_locals m n locals =
-  let rec loop locals i n =
-    if i < n then
-      loop ((bool_param m.(i)) :: locals) (i+1) n
-    else locals in
-  loop locals 0 n
-
 (*
 let defnames m n d =
   let rec loop acc k = if k < n then loop (S.add m.(k) acc) (k+1) else acc in
@@ -60,7 +29,7 @@ let defnames m n d =
 let statefull eq_list = List.exists (fun eq -> eq.eq_statefull) eq_list
 
 let is_var = function
-  | { e_desc = Evar(_) } -> true
+  | { e_desc = Evar _ } -> true
   | _ -> false
 
 let rec translate_eq v acc_eq_list eq =
@@ -102,25 +71,27 @@ and translate v acc_eq_list e =
     | Etuple(e_list) ->
         let v, acc_eq_list,e_list = translate_list v acc_eq_list e_list in
         v,acc_eq_list,
-        { e with e_desc = Etuple(e_list) }
-    | Eapp({ a_op = Eevery(f,params) } as op, re :: e_list)
+        { e with e_desc = Etuple e_list }
+    | Eapp ({ a_op = Ecall(op_desc, Some re) } as op, e_list)
         when not (is_var re) ->
         let v, acc_eq_list,re = translate v acc_eq_list re in
         let n, v, acc_eq_list = equation v acc_eq_list re in
         let v, acc_eq_list, e_list = translate_list v acc_eq_list e_list in
-        v,acc_eq_list,
+          v,acc_eq_list,
           { e with e_desc =
-              Eapp({ op with a_op = Eevery(f,params) },
-		  { re with e_desc = Evar(n) } :: e_list) }
-    | Eapp({ a_op = Eiterator(it, f, params, Some re) } as op, e_list) 
-	when not (is_var re) ->
+              Eapp({ op with a_op = Ecall(op_desc, 
+                                          Some { re with e_desc = Evar(n) }) },
+                   e_list) }
+    | Eapp ({ a_op = Earray_op(Eiterator(it, op_desc, Some re)) } as op, e_list)
+	      when not (is_var re) ->
         let v, acc_eq_list,re = translate v acc_eq_list re in
         let n, v, acc_eq_list = equation v acc_eq_list re in
         let v, acc_eq_list, e_list = translate_list v acc_eq_list e_list in
-	let re = { re with e_desc = Evar n } in
-        v,acc_eq_list,
+	      let re = { re with e_desc = Evar n } in
+          v,acc_eq_list,
           { e with e_desc =
-              Eapp({ op with a_op = Eiterator(it, f, params, Some re) },e_list) }	
+              Eapp({ op with a_op = Earray_op(Eiterator(it, op_desc, Some re)) },
+                   e_list) }
     | Eapp(f, e_list) ->
         let v, acc_eq_list, e_list = translate_list v acc_eq_list e_list in
         v, acc_eq_list,
@@ -142,7 +113,6 @@ and translate v acc_eq_list e =
         let v, acc_eq_list,e_list = translate_list v acc_eq_list e_list in
         v,acc_eq_list,
         { e with e_desc = Earray(e_list) }
-    | Ereset_mem _ -> v,acc_eq_list,e
 
 and translate_list v acc_eq_list e_list =
   let v,acc_eq_list,acc_e =
diff --git a/heptagon/transformations/last.ml b/heptagon/transformations/last.ml
index 903e33f..337d607 100644
--- a/heptagon/transformations/last.ml
+++ b/heptagon/transformations/last.ml
@@ -8,13 +8,9 @@
 (**************************************************************************)
 (* removing accessed to shared variables (last x)      *)
 
-(* $Id$ *)
-
-open Location
 open Misc
-open Ident
 open Heptagon
-open Global
+open Ident
 
 (* introduce a fresh equation [last_x = pre(x)] for every *)
 (* variable declared with a last *)
@@ -23,15 +19,13 @@ let last (eq_list, env, v) { v_name = n; v_type = t; v_last = last } =
     | Var -> (eq_list, env, v)
     | Last(default) ->
         let lastn = Ident.fresh ("last" ^ (sourcename n)) in
-        (eqmake (Eeq(Evarpat(lastn),
-                     emake
-                       (Eapp (eop (Epre(default)),
-			     [emake (Evar(n)) (Tbase(t))]))
-                       (Tbase(t)))))
-        :: eq_list,
+        let eq = mk_equation (Eeq (Evarpat lastn,
+                                   mk_exp (Eapp (mk_op (Epre default),
+			                                           [mk_exp (Evar n) t])) t)) in
+          eq:: eq_list,
         Env.add n lastn env,
-        (param lastn t) :: v
-
+        (mk_var_dec lastn t) :: v
+          
 let extend_env env v = List.fold_left last ([], env, []) v
 
 let rec translate_eq env eq =
@@ -71,7 +65,6 @@ and translate env e =
             Estruct(List.map (fun (f, e) -> (f, translate env e)) e_f_list) }
     | Earray(e_list) ->
 	{ e with e_desc = Earray(List.map (translate env) e_list) }
-    | Ereset_mem _ -> assert false
 
 let translate_contract env contract =
   match contract with
diff --git a/heptagon/transformations/reset.ml b/heptagon/transformations/reset.ml
index 2b95d64..def55dc 100644
--- a/heptagon/transformations/reset.ml
+++ b/heptagon/transformations/reset.ml
@@ -10,12 +10,10 @@
 
 (* $Id$ *)
 
-open Location
 open Misc
 open Ident
 open Heptagon
-open Global
-open Initial
+open Types
 
 (* We introduce an initialization variable for each block  *)
 (* Using an asynchronous reset would allow to produce      *)
@@ -43,14 +41,16 @@ open Initial
    e1 -> e2 is translated into if (true fby false) then e1 else e2 
 *)
 
+let mk_bool_var n = 
+  mk_exp (Evar n) (Tid Initial.pbool)
+let mk_bool_param n = 
+  mk_var_dec n (Tid Initial.pbool)
+
+let or_op_call = mk_op ( Ecall(mk_op_desc Initial.por [] Eop, None) )
+
 let pre_true e =
-  { e with e_desc = Eapp(eop (Epre(Some(Cconstr(ptrue)))), [e]) }
+  { e with e_desc = Eapp(mk_op (Epre (Some (Cconstr Initial.ptrue))), [e]) }
 let init e = pre_true { dfalse with e_loc = e.e_loc }
-let ifthenelse e1 e2 e3 =
-  { e3 with e_desc = Eapp(eop Eifthenelse, [e1; e2; e3]) }
-let eq pat e =
-  { eq_desc = Eeq(pat, e); eq_statefull = false; eq_loc = no_location }
-let statefulleq = Heptagon.eq
 
 (* the boolean condition for a structural reset *)
 type reset =
@@ -68,31 +68,30 @@ let rec or_op res e =
   match res with
     | Rfalse -> e
     | Rorthen(res, n) ->
-        or_op res { e with e_desc = Eapp(eop (Eop(por,[])), [bool_var n; e]) }
+        or_op res { e with e_desc = Eapp(or_op_call, [mk_bool_var n; e]) }
 
 let default e =
   match e.e_desc with
-    | Econst c -> Some(c)
+    | Econst c -> Some c
     | _ -> None
 
 let exp_of_res res =
   match res with
     | Rfalse -> dfalse
-    | Rorthen(res, n) -> or_op res (bool_var n)
+    | Rorthen(res, n) -> or_op res (mk_bool_var n)
 
 let ifres res e2 e3 =
   match res with
-    | Rfalse -> ifthenelse (init e3) e2 e3
+    | Rfalse -> mk_ifthenelse (init e3) e2 e3
     | _ -> (* a reset occurs *)
-	ifthenelse (exp_of_res res) e2 e3
+	      mk_ifthenelse (exp_of_res res) e2 e3
 
 (* add an equation *)
 let equation v acc_eq_list e =
   let n = Ident.fresh "r" in
   n,
-  (bool_param n) :: v,
-  { eq_desc = Eeq(Evarpat(n), e); eq_statefull = true; eq_loc = e.e_loc } ::
-    acc_eq_list
+  (mk_bool_param n) :: v,
+  (mk_equation (Eeq(Evarpat n, e))) ::acc_eq_list
 
 let orthen v acc_eq_list res e =
   match e.e_desc with
@@ -104,7 +103,7 @@ let orthen v acc_eq_list res e =
 let add_locals m n locals =
   let rec loop locals i n =
     if i < n then
-      loop ((bool_param m.(i)) :: locals) (i+1) n
+      loop ((mk_bool_param m.(i)) :: locals) (i+1) n
     else locals in
   loop locals 0 n
 
@@ -112,10 +111,10 @@ let add_local_equations i n m lm acc =
   (* [mi = false;...; m1 = l_m1;...; mn = l_mn] *)
   let rec loop acc k =
     if k < n then
-      if k = i then loop ((eq (varpat(m.(k))) dfalse) :: acc) (k+1)
+      if k = i then loop ((mk_simple_equation (Evarpat (m.(k))) dfalse) :: acc) (k+1)
       else
         loop
-          ((eq (varpat(m.(k))) (bool_var lm.(k))) :: acc) (k+1)
+          ((mk_simple_equation (Evarpat (m.(k))) (mk_bool_var lm.(k))) :: acc) (k+1)
     else acc
   in loop acc 0
 
@@ -124,20 +123,20 @@ let add_global_equations n m lm res acc =
      l_mn = if res then true else true fby mn ] *)
   let rec loop acc k =
     if k < n then
-      loop
-        ((statefulleq (varpat(lm.(k)))
-            (match res with
-              | Rfalse -> pre_true (bool_var m.(k))
-              | _ -> ifres res dtrue (pre_true (bool_var m.(k)))
-            )
-         ) :: acc) (k+1)
+      let exp =            
+        (match res with
+           | Rfalse -> pre_true (mk_bool_var m.(k))
+           | _ -> ifres res dtrue (pre_true (mk_bool_var m.(k)))
+        ) in
+        loop
+          ((mk_equation (Eeq (Evarpat (lm.(k)), exp))) :: acc) (k+1)
     else acc in
   loop acc 0
 
 let defnames m n d =
   let rec loop acc k =
     if k < n
-    then loop (Env.add m.(k) tybool acc) (k+1)
+    then loop (Env.add m.(k) (Tid Initial.pbool) acc) (k+1)
     else acc in
   loop d 0
 
@@ -207,37 +206,49 @@ and translate res e =
           match res, e1 with
             | Rfalse, { e_desc = Econst(c) } ->
                 (* no reset *)
-		{ e with e_desc = 
-		    Eapp({ op with a_op = Epre(Some(c)) }, [e2]) }
+		            { e with e_desc = 
+		                Eapp({ op with a_op = Epre(Some c) }, [e2]) }
             | _ ->
                 ifres res e1
                   { e with e_desc = 
-		      Eapp({ op with a_op = Epre(default e1) }, [e2]) }
+		                  Eapp({ op with a_op = Epre(default e1) }, [e2]) }
         end
     | Eapp({ a_op = Earrow }, [e1;e2]) ->
         let e1 = translate res e1 in
         let e2 = translate res e2 in
         ifres res e1 e2
-    | Eapp({ a_op = Enode(f,params) } as op, e_list) ->
-        let e_list = List.map (translate res) e_list in
-        if true_reset res then
-          { e with e_desc = Eapp({ op with a_op = Eevery(f, params) },
-				(exp_of_res res) :: e_list) }
-        else
-          { e with e_desc = Eapp({ op with a_op = Enode(f,params) }, e_list ) }
-    | Eapp( { a_op = Eiterator(it,f, params, _) } as op, e_list) ->
-        let e_list = List.map (translate res) e_list in
-	  if true_reset res then
-	    let r = Some (exp_of_res res) in
-              { e with e_desc = Eapp({ op with a_op = Eiterator(it,f,params,r) },
-				     e_list) }
-          else
-	    { e with e_desc = Eapp(op, e_list) }
-    | Eapp({ a_op = Eevery(f, params) } as op, re :: e_list) ->
+
+    (* add reset to the current reset exp. *)
+    | Eapp({ a_op = Ecall(op_desc, Some re) } as op, e_list) ->
         let re = translate res re in
         let e_list = List.map (translate res) e_list in
-        { e with e_desc = Eapp({ op with a_op = Eevery(f, params)},
-			       (or_op res re) :: e_list) }
+        let op = { op with a_op = Ecall(op_desc, Some (or_op res re))} in
+          { e with e_desc = Eapp(op, e_list) }
+    (* create a new reset exp if necessary *)
+    | Eapp({ a_op = Ecall(op_desc, None) } as op, e_list) ->
+        let e_list = List.map (translate res) e_list in
+        if true_reset res then
+          let op = { op with a_op = Ecall(op_desc, Some (exp_of_res res)) } in
+            { e with e_desc = Eapp(op, e_list) }
+        else
+          { e with e_desc = Eapp(op, e_list ) }
+     (* add reset to the current reset exp. *)
+    | Eapp( { a_op = Earray_op (Eiterator(it, op_desc, Some re)) } as op, e_list) ->
+        let re = translate res re in
+        let e_list = List.map (translate res) e_list in
+	      let r = Some (or_op res re) in
+        let op = { op with a_op = Earray_op (Eiterator(it, op_desc, r)) } in
+          { e with e_desc = Eapp(op, e_list) }
+     (* create a new reset exp if necessary *)
+    | Eapp( { a_op = Earray_op (Eiterator(it, op_desc, None)) } as op, e_list) ->
+        let e_list = List.map (translate res) e_list in
+	        if true_reset res then
+	          let r = Some (exp_of_res res) in
+            let op = { op with a_op = Earray_op (Eiterator(it, op_desc, r)) } in
+              { e with e_desc = Eapp(op, e_list) }
+          else
+	          { e with e_desc = Eapp(op, e_list) }
+ 
     | Eapp(op, e_list) ->
         { e with e_desc = Eapp(op, List.map (translate res) e_list) }
     | Efield(e', field) ->