diff --git a/compiler/global/static.ml b/compiler/global/static.ml
index 4cb2216..7ca3738 100644
--- a/compiler/global/static.ml
+++ b/compiler/global/static.ml
@@ -22,12 +22,12 @@ type static_exp =
   | Sint of int
   | Sfloat of float
   | Sbool of bool
-  | Sconstructor of
+  | Sconstructor of longname
+  | Stuple of static_exp list
   | Sarray_power of static_exp * static_exp (** power : 0^n : [0,0,0,0,0,..] *)
   | Sarray of static_exp list (** [ e1, e2, e3 ] *)
   | Sop of longname * static_exp list (** defined ops for now in pervasives *)
 
-
 (** Constraints on size expressions. *)
 type size_constraint =
   | Cequal of static_exp * static_exp (* e1 = e2*)
@@ -40,67 +40,70 @@ exception Instanciation_failed
 exception Not_static
 
 (** Returns the op from an operator full name. *)
-let op_from_app_name n =
-  match n with
-    | Modname { qual = "Pervasives"; id = "+" } | Name "+" -> Splus
-    | Modname { qual = "Pervasives"; id = "-" } | Name "-" -> Sminus
-    | Modname { qual = "Pervasives"; id = "*" } | Name "*" -> Stimes
-    | Modname { qual = "Pervasives"; id = "/" } | Name "/" -> Sdiv
+let op_from_app_name ln =
+  match ln with
+    | Modname { qual = "Pervasives" } -> ln
     | _ -> raise Not_static
 
+(** Applies the operator [op] to the two integers [n1] and [n2]
+    and returns the reslt as a static exp. *)
+let apply_int_op op n1 n2 =
+  match op with
+    | Modname { qual = "Pervasives"; id = "+" } -> Sint (n1 + n2)
+    | Modname { qual = "Pervasives"; id = "-" } -> Sint (n1 - n2)
+    | Modname { qual = "Pervasives"; id = "*" } -> Sint (n1 * n2)
+    | Modname { qual = "Pervasives"; id = "/" } ->
+        let n = if n2 = 0 then raise Instanciation_failed else n1 / n2 in
+          Sint n
+    | _ -> (* unknown operator, reconstrcut the op *)
+        Sop (op, Sint n1, Sint n2)
+
 (** [simplify env e] returns e simplified with the
     variables values taken from env (mapping vars to integers).
     Variables are replaced with their values and every operator
     that can be computed is replaced with the value of the result. *)
-let rec simplify env =
-  function
-    | Sconst n -> Sconst n
+let rec simplify env se =
+  match se with
+    | Sint _ | Sfloat _ | Sbool _ | Sconstructor -> se
     | Svar id -> (try simplify env (NamesEnv.find id env) with | _ -> Svar id)
-    | Sop (op, e1, e2) ->
-        let e1 = simplify env e1 in
-        let e2 = simplify env e2
-        in
-        (match (e1, e2) with
-           | (Sconst n1, Sconst n2) ->
-               let n =
-                 (match op with
-                    | Splus -> n1 + n2
-                    | Sminus -> n1 - n2
-                    | Stimes -> n1 * n2
-                    | Sdiv ->
-                        if n2 = 0 then raise Instanciation_failed else n1 / n2)
-               in Sconst n
-           | (_, _) -> Sop (op, e1, e2))
+    | Sop (op, [e1; e2]) ->
+        (match simplify env e1, simplify env e2 with
+           | Sint n1, Sint n2 -> apply_int_op op n1 n2
+           | e1, e2 -> Sop (op, [e1; e2])
+        )
+    | Sop (op, se_list) -> Sop (op, List.map (simplify env) se_list)
+    | Sarray se_list -> Sarray (List.map (simplify env) se_list)
+    | Sarray_power (se, n) -> Sarray_power (simplify env se, simplify env n)
+    | Stuple se_list -> Stuple (List.map (simplify env) se_list)
 
 (** [int_of_static_exp env e] returns the value of the expression
     [e] in the environment [env], mapping vars to integers. Raises
     Instanciation_failed if it cannot be computed (if a var has no value).*)
-let int_of_size_exp env e =
-  match simplify env e with | Sconst n -> n | _ -> raise Instanciation_failed
+let int_of_static_exp env e =
+  match simplify env e with | Sint n -> n | _ -> raise Instanciation_failed
 
 (** [is_true env constr] returns whether the constraint is satisfied
     in the environment (or None if this can be decided)
-
     and a simplified constraint. *)
 let is_true env =
   function
-    | Cequal (e1, e2) when e1 = e2 ->
-        ((Some true), (Cequal (simplify env e1, simplify env e2)))
+    | Cequal e1, e2 when e1 = e2 ->
+        Some true, Cequal (simplify env e1, simplify env e2)
     | Cequal (e1, e2) ->
         let e1 = simplify env e1 in
         let e2 = simplify env e2
         in
-        (match (e1, e2) with
-           | (Sconst n1, Sconst n2) -> ((Some (n1 = n2)), (Cequal (e1, e2)))
-           | (_, _) -> (None, (Cequal (e1, e2))))
+        (match e1, e2 with
+           | SConst n1, SConst n2 -> Some (n1 = n2), Cequal (e1, e2)
+           | (_, _) -> None, Cequal (e1, e2))
     | Clequal (e1, e2) ->
         let e1 = simplify env e1 in
         let e2 = simplify env e2
         in
-        (match (e1, e2) with
-           | (Sconst n1, Sconst n2) -> ((Some (n1 <= n2)), (Clequal (e1, e2)))
-           | (_, _) -> (None, (Clequal (e1, e2))))
-    | Cfalse -> (None, Cfalse)
+        (match e1, e2 with
+           | SConst n1, SConst n2 -> Some (n1 <= n2), Clequal (e1, e2)
+           | _, _ -> None, Clequal (e1, e2))
+    | Cfalse -> None, Cfalse
 
 exception Solve_failed of size_constraint
 
@@ -120,11 +123,14 @@ let rec solve const_env =
 
 (** Substitutes variables in the size exp with their value
     in the map (mapping vars to size exps). *)
-let rec static_exp_subst m =
-  function
-    | Svar n -> (try List.assoc n m with | Not_found -> Svar n)
-    | Sop (op, e1, e2) -> Sop (op, static_exp_subst m e1, static_exp_subst m e2)
-    | s -> s
+let rec static_exp_subst m = function
+  | Svar n -> (try List.assoc n m with | Not_found -> Svar n)
+  | Sop (op, se_list) -> Sop (op, List.map (static_exp_subst m) se_list)
+  | Sarray_power (se, n) -> Sarray_power (static_exp_subst m se,
+                                          static_exp_subst m n)
+  | Sarray se_list -> Sarray (List.map (static_exp_subst env) se_list)
+  | Stuple se_list -> Stuple (List.map (static_exp_subst env) se_list)
+  | s -> s
 
 (** Substitutes variables in the constraint list with their value
     in the map (mapping vars to size exps). *)
@@ -135,16 +141,23 @@ let instanciate_constr m constr =
     | Cfalse -> Cfalse
   in List.map (replace_one m) constr
 
-let op_to_string =
-  function | Splus -> "+" | Sminus -> "-" | Stimes -> "*" | Sdiv -> "/"
+let rec print_static_exp ff = function
+  | Sint i -> fprintf ff "%d" i
+  | Sbool b -> fprintf ff "%b" b
+  | Sfloat f -> fprintf ff "%f" f
+  | Sconstructor ln -> print_longname ff ln
+  | Svar id -> fprintf ff "%s" id
+  | Sop (op, se_list) ->
+      fprintf ff "@[<2>%a@,%a@]"
+        print_longname op  print_static_exp_tuple se_list
+  | Sarray_power (se, n) ->
+      fprintf ff "%a^%a" print_static_exp se  print_static_exp n
+  | Sarray se_list ->
+      fprintf ff "@[<2>%a@]" (print_list_r print_static_exp "["";""]") se_list
+  | Stuple se_list -> print_static_exp_tuple se_list
 
-let rec print_static_exp ff =
-  function
-    | SConst i -> fprintf ff "%d" i
-    | Svar id -> fprintf ff "%s" id
-    | Sop (op, e1, e2) ->
-        fprintf ff "@[(%a %s %a)@]"
-          print_static_exp e1 (op_to_string op) print_static_exp e2
+and print_static_exp_tuple ff l =
+  fprintf ff "@[<2>%a@]" (print_list_r print_static_exp "("","")") l
 
 let print_size_constraint ff = function
   | Cequal (e1, e2) ->
diff --git a/compiler/heptagon/analysis/interface.ml b/compiler/heptagon/analysis/interface.ml
index f574afb..350205f 100644
--- a/compiler/heptagon/analysis/interface.ml
+++ b/compiler/heptagon/analysis/interface.ml
@@ -21,7 +21,8 @@ module Type =
 struct
   let sigtype { sig_name = name; sig_inputs = i_list; sig_statefull = statefull;
                 sig_outputs = o_list; sig_params = params } =
-    let check_arg a = { a with a_type = check_type a.a_type } in
+    let const_env = build_node_params NamesEnv.empty node_params in
+    let check_arg a = { a with a_type = check_type const_env a.a_type } in
     name, { node_inputs = List.map check_arg i_list;
             node_outputs = List.map check_arg o_list;
             node_statefull = statefull;
@@ -32,7 +33,7 @@ struct
     try
       match desc with
         | Iopen(n) -> open_module n
-        | Itypedef(tydesc) -> deftype NamesEnv.empty tydesc
+        | Itypedef(tydesc) -> deftype NamesEnv.empty NamesEnv.empty tydesc
         | Isignature(s) ->
             let name, s = sigtype s in
             add_value name s
diff --git a/compiler/heptagon/analysis/typing.ml b/compiler/heptagon/analysis/typing.ml
index 8a24ebe..339962f 100644
--- a/compiler/heptagon/analysis/typing.ml
+++ b/compiler/heptagon/analysis/typing.ml
@@ -226,7 +226,7 @@ let less_than statefull = if not statefull then error Estate_clash
 
 let rec is_statefull_exp e =
   match e.e_desc with
-    | Econst _ | Econstvar _ | Evar _-> false
+    | Econst _ | Evar _-> false
     | Elast _ -> true
     | Etuple e_list -> List.exists is_statefull_exp e_list
     | Eapp({ a_op = (Efby | Epre _ | Earrow) }, _) -> true
@@ -281,15 +281,41 @@ let prod = function
   | [ty]    -> ty
   | ty_list -> Tprod ty_list
 
-let rec typing_const c = match c with
-  | Cint _     -> c, Tid(pint)
-  | Cfloat _   -> c, Tid(pfloat)
+let typing_static_exp const_env se =
+  match se with
+    | Sint -> Initial.pint
+    | Sbool -> Initial.pbool
+    | Sfloat -> Initial.pfloat
+    | Svar n ->
+        (try
+           NamesEnv.find n const_env
+        with
+            Not_found -> message no_location (Eundefined_const n))
+    | Sconstructor ln ->
   | Cconstr(c) ->
       let { qualid = q; info = ty } = find_constr c in
       Cconstr(Modname q), ty
-  | Carray(n, c) ->
-      let c, ty = typing_const c in
-      Carray(n,c),  Tarray(ty, n)
+    | Sop (op, se_list) ->
+
+    | Sarray_power (se, n) ->
+        expect_static_exp const_env no_location (Tid Initial.pint) n;
+        let ty = typing_static_exp const_env se in
+          Tarray(ty, n)
+    | Sarray [] ->
+        message no_location Eempty_array
+    | Sarray se::se_list ->
+        let ty = typing_static_exp const_env se in
+          List.iter (expect_static_exp const_env ty) se_list;
+          Tarray(ty, Sint ((List.length se_list) + 1))
+    | Stuple se_list ->
+        prod (List.map (typing_static_exp const_env) se_list)
+
+and expect_static_exp const_env loc exp_ty se =
+  try
+    let ty = typing_static_exp const_env se in
+      unify ty exp_ty
+  with
+      Unify -> message loc (Etype_clash(ty, exp_ty))
 
 let typ_of_name h x =
   try
@@ -331,25 +357,26 @@ let name_mem n env =
   Env.fold check_one env false
 
 (** [check_type t] checks that t exists *)
-let rec check_type = function
+let rec check_type const_env = function
   | Tarray(ty, e) ->
-      Tarray(check_type ty, e)
+      expect_static_exp const_env (Tid Initial.pint) e;
+      Tarray(check_type const_env ty, e)
   | Tid(ty_name) ->
       (try Tid(Modname((find_type ty_name).qualid))
        with Not_found -> error (Eundefined(fullname ty_name)))
   | Tprod l ->
-      Tprod (List.map check_type l)
+      Tprod (List.map (check_type const_env) l)
 
-let rec simplify_type const_env = function
+let rec simplify_type const_value_env = function
   | Tid _ as t -> t
   | Tarray(ty, e) ->
-      Tarray(simplify_type const_env ty, simplify const_env e)
+      Tarray(simplify_type const_value_env ty, simplify const_value_env e)
   | Tprod l ->
-      Tprod (List.map (simplify_type const_env) l)
+      Tprod (List.map (simplify_type const_value_env) l)
 
-let simplify_type loc const_env ty =
+let simplify_type loc const_value_env ty =
   try
-    simplify_type const_env ty
+    simplify_type const_value_env ty
   with
       Instanciation_failed -> message loc (Etype_should_be_static ty)
 
@@ -466,9 +493,9 @@ let struct_info_from_field loc f =
 (** @return the type of the field with name [f] in the list
     [fields]. [t1] is the corresponding record type and [loc] is
     the location, both used for error reporting. *)
-let field_type f fields t1 loc =
+let field_type const_env f fields t1 loc =
   try
-    check_type (field_assoc f fields)
+    check_type const_env (field_assoc f fields)
   with
       Not_found -> message loc (Eno_such_field (t1, f))
 
@@ -476,10 +503,9 @@ let rec typing statefull h e =
   try
     let typed_desc,ty = match e.e_desc with
       | Econst(c) ->
-          let typed_c, ty = typing_const c in
+          let typed_c, ty = typing_static_exp const_env c in
           Econst(c),
           ty
-      | Econstvar(x) -> Econstvar x, Tid Initial.pint
       | Evar(x) ->
           Evar(x),
           typ_of_varname h x
@@ -529,30 +555,30 @@ let rec typing statefull h e =
   with
       TypingError(kind) -> message e.e_loc kind
 
-and typing_field statefull h fields t1 (f, e) =
+and typing_field statefull const_env h fields t1 (f, e) =
   try
-    let ty = check_type (field_assoc f fields) in
-    let typed_e = expect statefull h ty e in
+    let ty = check_type const_env (field_assoc f fields) in
+    let typed_e = expect statefull const_env h ty e in
     f, typed_e
   with
       Not_found -> message e.e_loc (Eno_such_field (t1, f))
 
-and expect statefull h expected_ty e =
-  let typed_e, actual_ty = typing statefull h e in
+and expect statefull const_env h expected_ty e =
+  let typed_e, actual_ty = typing statefull const_env h e in
   try
     unify actual_ty expected_ty;
     typed_e
   with TypingError(kind) -> message e.e_loc kind
 
-and typing_app statefull h op e_list =
+and typing_app statefull const_env h op e_list =
   match op, e_list with
     | Epre(None), [e] ->
         less_than statefull;
         let typed_e,ty = typing statefull h e in
         ty,op,[typed_e]
-    | Epre(Some(c)), [e] ->
+    | Epre(Some c), [e] ->
         less_than statefull;
-        let typed_c, t1 = typing_const c in
+        let typed_c, t1 = typing_static_exp const_env c in
         let typed_e = expect statefull h t1 e in
         t1, Epre(Some(typed_c)), [typed_e]
     | (Efby | Earrow), [e1;e2] ->
@@ -603,7 +629,7 @@ and typing_app statefull h op e_list =
 (*Array operators*)
 and typing_array_op statefull h op e_list =
   match op, e_list with
-    | Erepeat, [e1; e2] ->
+    | Earray_fill, [e1; e2] ->
         let typed_e2 = expect statefull h (Tid Initial.pint) e2 in
         let e2 = static_exp_of_exp e2 in
         let typed_e1, t1 = typing statefull h e1 in
@@ -642,24 +668,23 @@ and typing_array_op statefull h op e_list =
         end;
         let n = Sop (SPlus, static_exp t1, static_exp t2) in
         Tarray (element_type t1, n), op, [typed_e1; typed_e2]
-    | Eiterator (it, ({ op_name = f; op_params = params;
-                        op_kind = k } as op_desc), reset),
-        e::e_list ->
+    | Eiterator (it, app, n, e_list, reset),
         let { qualid = q; info = ty_desc } = find_value f in
         let f = Modname(q) in
         let k, expected_ty_list, result_ty_list = kind f statefull k ty_desc in
         let m = List.combine (List.map (fun p -> p.p_name) ty_desc.node_params)
           params in
         let expected_ty_list = List.map (subst_type_vars m) expected_ty_list in
-        let size_constrs =
-          instanciate_constr m ty_desc.node_params_constraints in
         let result_ty_list = List.map (subst_type_vars m) result_ty_list in
         let typed_e = expect statefull h (Tid Initial.pint) e in
-        let e = static_exp_of_exp e in
-        let ty, typed_e_list = typing_iterator statefull h it e
+        let ty, typed_e_list = typing_iterator statefull h it n
           expected_ty_list result_ty_list e_list in
-        add_size_constraint (Clequal (Sconst 1, e));
+          (* add size constraints *)
+        let size_constrs =
+          instanciate_constr m ty_desc.node_params_constraints in
+          add_size_constraint (Clequal (SConst 1, e));
         List.iter add_size_constraint size_constrs;
+        (* return the type *)
         ty, Eiterator(it, { op_desc with op_name = f; op_kind = k }, reset),
           typed_e::typed_e_list
 
@@ -714,12 +739,13 @@ and typing_iterator statefull h it n args_ty_list result_ty_list e_list =
         end;
         prod result_ty_list, typed_e_list
 
-and typing_array_subscript statefull h idx_list ty  =
+and typing_array_subscript statefull const_env h idx_list ty  =
   match ty, idx_list with
     | ty, [] -> ty
     | Tarray(ty, exp), idx::idx_list ->
-        add_size_constraint (Clequal (Sconst 0, idx));
-        add_size_constraint (Clequal (idx, Sop(Sminus, exp, Sconst 1)));
+        expect_static_exp const_env (Tid Initial.pint) exp;
+        add_size_constraint (Clequal (SConst 0, idx));
+        add_size_constraint (Clequal (idx, Sop(SMinus, exp, SConst 1)));
         typing_array_subscript statefull h idx_list ty
     | _, _ -> error (Esubscripted_value_not_an_array ty)
 
@@ -886,12 +912,12 @@ and typing_block statefull h
   with
     | TypingError(kind) -> message loc kind
 
-and build h h0 dec =
+and build const_env h h0 dec =
   List.fold_left
     (fun (acc_dec, acc_defined, h)
        ({ v_ident = n; v_type = btype; v_last = l; v_loc = loc } as v) ->
          try
-           let ty = check_type btype in
+           let ty = check_type const_env btype in
            (* update type longname with module name from check_type *)
            v.v_type <- ty;
            if (Env.mem n h0) or (Env.mem n h)
@@ -904,14 +930,6 @@ and build h h0 dec =
            | TypingError(kind) -> message loc kind)
     ([], Env.empty, h) dec
 
-let build_params h params =
-  let add_one h param =
-    if Env.mem param h then
-      error (Ealready_defined(name param));
-    Env.add param { ty = Tid Initial.pint; last = false } h
-  in
-  List.fold_left add_one h params
-
 let typing_contract statefull h contract =
 
   match contract with
@@ -942,9 +960,9 @@ let typing_contract statefull h contract =
                c_enforce = typed_e_g },
         controllable_names, h
 
-let signature const_env statefull inputs returns params constraints =
+let signature const_value_env statefull inputs returns params constraints =
   let arg_dec_of_var_dec vd =
-    mk_arg (Some (name vd.v_ident)) (check_type vd.v_type)
+    mk_arg (Some (name vd.v_ident)) (simplify_type const_value_env vd.v_type)
   in
   { node_inputs = List.map arg_dec_of_var_dec inputs;
     node_outputs = List.map arg_dec_of_var_dec returns;
@@ -958,22 +976,28 @@ let solve loc env cl =
   with
       Solve_failed c -> message loc (Econstraint_solve_failed c)
 
-let node const_env ({ n_name = f; n_statefull = statefull;
+let build_node_params const_env l =
+  List.fold_left (fun env n -> NamesEnv.add n (Tid Initial.pint) env)
+    const_env l
+
+let node const_env const_value_env ({ n_name = f; n_statefull = statefull;
                       n_input = i_list; n_output = o_list;
                       n_contract = contract;
                       n_local = l_list; n_equs = eq_list; n_loc = loc;
                       n_params = node_params; } as n) =
   try
-    let typed_i_list, input_names, h = build Env.empty Env.empty i_list in
-    let typed_o_list, output_names, h = build h h o_list in
+    let const_env = build_node_params const_env node_params in
+
+    let typed_i_list, input_names, h = build const_env Env.empty Env.empty i_list in
+    let typed_o_list, output_names, h = build const_env h h o_list in
 
     (* typing contract *)
     let typed_contract, controllable_names, h =
       typing_contract statefull h contract in
 
-    let typed_l_list, local_names, h = build h h l_list in
+    let typed_l_list, local_names, h = build const_env h h l_list in
     let typed_eq_list, defined_names =
-      typing_eq_list statefull h Env.empty eq_list in
+      typing_eq_list statefull const_env h Env.empty eq_list in
     (* if not (statefull) & (List.length o_list <> 1)
        then error (Etoo_many_outputs);*)
     let expected_names = add local_names output_names in
@@ -981,8 +1005,8 @@ let node const_env ({ n_name = f; n_statefull = statefull;
     included_env defined_names expected_names;
 
     let cl = get_size_constraint () in
-    let cl = solve loc const_env cl in
-    add_value f (signature const_env statefull i_list o_list node_params cl);
+    let cl = solve loc const_value_env cl in
+    add_value f (signature const_value_env statefull i_list o_list node_params cl);
 
     { n with
         n_input = List.rev typed_i_list;
@@ -993,7 +1017,7 @@ let node const_env ({ n_name = f; n_statefull = statefull;
   with
     | TypingError(error) -> message loc error
 
-let deftype const_env { t_name = n; t_desc = tdesc; t_loc = loc } =
+let deftype const_env const_value_env { t_name = n; t_desc = tdesc; t_loc = loc } =
   try
     match tdesc with
       | Type_abs -> add_type n Tabstract
@@ -1004,7 +1028,8 @@ let deftype const_env { t_name = n; t_desc = tdesc; t_loc = loc } =
           let field_ty_list =
             List.map (fun f ->
                         mk_field f.f_name
-                          (simplify_type loc const_env f.f_type))
+                          (simplify_type loc const_value_env
+                             (check_type const_env f.f_type))
               field_ty_list in
           add_type n (Tstruct field_ty_list);
           add_struct n field_ty_list;
@@ -1013,15 +1038,23 @@ let deftype const_env { t_name = n; t_desc = tdesc; t_loc = loc } =
   with
       TypingError(error) -> message loc error
 
-let build_const_env cd_list =
+let build_const_value_env cd_list =
   List.fold_left (fun env cd -> NamesEnv.add cd.c_name cd.c_value env)
     NamesEnv.empty cd_list
 
+let build_const_env cd_list =
+  let typing_const_dec const_envenv cd =
+    expect_static_exp const_env cd.c_loc cd.c_type cd.c_value;
+     NamesEnv.add cd.c_name cd.c_type env
+  in
+    List.fold_left typing_const_env NamesEnv.empty cd_list
+
 let program
     ({ p_opened = opened; p_types = p_type_list;
        p_nodes = p_node_list; p_consts = p_consts_list } as p) =
   let const_env = build_const_env p_consts_list in
+  let const_value_env = build_const_value_env p_consts_list in
   List.iter open_module opened;
-  List.iter (deftype const_env) p_type_list;
-  let typed_node_list = List.map (node const_env) p_node_list in
+  List.iter (deftype const_env const_value_env) p_type_list;
+  let typed_node_list = List.map (node const_env const_value_env) p_node_list in
   { p with p_nodes = typed_node_list }
diff --git a/compiler/heptagon/heptagon.ml b/compiler/heptagon/heptagon.ml
index d6dd691..b8bdc27 100644
--- a/compiler/heptagon/heptagon.ml
+++ b/compiler/heptagon/heptagon.ml
@@ -182,9 +182,6 @@ let op_from_app app =
 let rec static_exp_of_exp e =
   match e.e_desc with
     | Econst se -> se
-    | Eapp (app, [ e1; e2 ]) ->
-        let op = op_from_app app
-        in Sop (op, static_exp_of_exp e1, static_exp_of_exp e2)
     | _ -> raise Not_static
 
 (** @return the set of variables defined in [pat]. *)
diff --git a/compiler/heptagon/parsing/hept_parser.mly b/compiler/heptagon/parsing/hept_parser.mly
index fe0056e..d03297d 100644
--- a/compiler/heptagon/parsing/hept_parser.mly
+++ b/compiler/heptagon/parsing/hept_parser.mly
@@ -216,7 +216,7 @@ opt_equs:
 ;
 
 opt_assume:
-  | /* empty */ {  mk_exp (Econst (Cconstr Initial.ptrue)) }
+  | /* empty */ {  mk_exp (Econst (Sconstructor Initial.ptrue)) }
   | ASSUME exp { $2 }
 ;
 
@@ -242,7 +242,7 @@ loc_params:
 var_last:
   | ident_list COLON ty_ident
       { List.map (fun id -> mk_var_dec id $3 Var) $1 }
-  | LAST IDENT COLON ty_ident EQUAL const
+  | LAST IDENT COLON ty_ident EQUAL exp
       { [ mk_var_dec $2 $4 (Last(Some($6))) ] }
   | LAST IDENT COLON ty_ident
       { [ mk_var_dec $2 $4 (Last(None)) ] }
@@ -442,7 +442,7 @@ exp:
       { mk_exp (Efield ($1, $3)) }
 /*Array operations*/
   | exp POWER simple_exp
-      { mk_exp (mk_array_op_call Erepeat [$1; $3]) }
+      { mk_exp (mk_call Erepeat [$1; $3]) }
   | simple_exp indexes
       { mk_exp (mk_array_op_call (Eselect $2) [$1]) }
   | simple_exp DOT indexes DEFAULT exp
@@ -483,7 +483,6 @@ indexes:
 constructor:
   | Constructor { Name($1) } %prec prec_ident
   | Constructor DOT Constructor { Modname({qual = $1; id = $3}) }
-  | BOOL { Name(if $1 then "true" else "false") }
 ;
 
 longname:
@@ -492,9 +491,10 @@ longname:
 ;
 
 const:
-  | INT { Cint($1) }
-  | FLOAT { Cfloat($1) }
-  | constructor { Cconstr($1) }
+  | INT { Sint $1 }
+  | FLOAT { Sfloat $1 }
+  | BOOL { Sbool $1 }
+  | constructor { Sconstructor $1 }
 ;
 
 tuple_exp:
diff --git a/compiler/heptagon/parsing/parsetree.ml b/compiler/heptagon/parsing/parsetree.ml
index 06bbf65..a2cc43f 100644
--- a/compiler/heptagon/parsing/parsetree.ml
+++ b/compiler/heptagon/parsing/parsetree.ml
@@ -27,39 +27,31 @@ and exp =
       e_loc: location }
 
 and desc =
-  | Econst of const
+  | Econst of static_exp
   | Evar of name
   | Elast of name
-  | Etuple of exp list
-  | Eapp of app * exp list
+  | Epre of exp option * exp
+  | Efby of exp * exp
   | Efield of exp * longname
   | Estruct of (longname * exp) list
-  | Earray of exp list
+  | Eapp of app * exp list
+  | Eiterator of iterator_type * app * static_exp * exp list
 
-and app =
-    { a_op : op; }
+and app = { a_op: op; a_params: static_exp list; }
 
 and op =
-  | Epre of const option
-  | Efby | Earrow | Eifthenelse
-  | Earray_op of array_op
-  | Efield_update of longname
-  | Ecall of op_desc
-
-and array_op =
-  | Erepeat | Eselect of exp list | Eselect_dyn
-  | Eupdate of exp list
+  | Etuple
+  | Enode of longname
+  | Eifthenelse
+  | Earrow
+  | Efield_update of longname (* field name args would be [record ; value] *)
+  | Earray
+  | Earray_fill
+  | Eselect
+  | Eselect_dyn
   | Eselect_slice
+  | Eupdate
   | Econcat
-  | Eiterator of iterator_type * op_desc
-
-and op_desc = { op_name : longname; op_params: exp list; op_kind: op_kind }
-and op_kind = | Efun | Enode
-
-and const =
-  | Cint of int
-  | Cfloat of float
-  | Cconstr of longname
 
 and pat =
   | Etuplepat of pat list
@@ -106,7 +98,7 @@ and var_dec =
       v_last : last;
       v_loc  : location; }
 
-and last = Var | Last of const option
+and last = Var | Last of exp option
 
 type type_dec =
     { t_name : name;
@@ -174,20 +166,14 @@ and interface_desc =
 let mk_exp desc =
   { e_desc = desc; e_loc = Location.current_loc () }
 
-let mk_app op =
-  { a_op = op; }
+let mk_app op params =
+  { a_op = op; a_params = params }
 
-let mk_op_desc ln params kind =
-  { op_name = ln; op_params = params; op_kind = kind }
+let mk_call ?(params=[]) op exps =
+  Eapp (mk_app op params, exps)
 
-let mk_call desc exps =
-  Eapp (mk_app (Ecall desc), exps)
-
-let mk_op_call s params exps =
-  mk_call (mk_op_desc (Name s) params Efun)  exps
-
-let mk_array_op_call op exps =
-  Eapp (mk_app (Earray_op op), exps)
+let mk_op_call  ?(params=[])s exps =
+  mk_call (Efun (Name s)) params exps
 
 let mk_iterator_call it ln params exps =
   mk_array_op_call (Eiterator (it, mk_op_desc ln params Enode)) exps
diff --git a/compiler/heptagon/parsing/scoping.ml b/compiler/heptagon/parsing/scoping.ml
index 3117407..4b31eac 100644
--- a/compiler/heptagon/parsing/scoping.ml
+++ b/compiler/heptagon/parsing/scoping.ml
@@ -103,46 +103,59 @@ let translate_op_kind = function
   | Efun -> Heptagon.Efun
   | Enode -> Heptagon.Enode
 
-let translate_const = function
-  | Cint i -> Heptagon.Cint i
-  | Cfloat f -> Heptagon.Cfloat f
-  | Cconstr ln -> Heptagon.Cconstr ln
-
 let op_from_app loc app =
   match app.a_op with
     | Ecall { op_name = op; op_kind = Efun } -> op_from_app_name op
     | _ -> Error.message loc Error.Estatic_exp_expected
 
 let check_const_vars = ref true
-let rec translate_static_exp const_env e = match e.e_desc with
+let rec static_exp_of_exp const_env e = match e.e_desc with
   | Evar n ->
       if !check_const_vars & not (NamesEnv.mem n const_env) then
         Error.message e.e_loc (Error.Econst_var n)
       else
         Svar n
-  | Econst (Cint i) -> Sconst i
-  | Eapp(app, [e1;e2]) ->
+  | Econst se -> se
+  | Eapp({ a_op = Earray_fill }, [e;n]) ->
+      Sarray_power (static_exp_of_exp const_env e,
+                    static_exp_of_exp const_env n)
+  | Eapp({ a_op = Earray }, [e;n]) ->
+      Sarray (List.map (static_exp_of_exp const_env) e_list)
+  | Eapp({ a_op = Etuple }, [e;n]) ->
+      Stuple (List.map (static_exp_of_exp const_env) e_list)
+  | Eapp(app, e_list) ->
       let op = op_from_app e.e_loc app in
-      Sop(op, translate_static_exp const_env e1,
-              translate_static_exp const_env e2)
-  | _ -> Error.message e.e_loc Error.Estatic_exp_expected
+      Sop(op, List.map (static_exp_of_exp const_env) e_list)
+  | _ -> raise Not_static
+
+let expect_static_exp const_env e =
+  try
+    static_exp_of_exp const_env e
+  with
+      Not_static -> Error.message e.e_loc Error.Estatic_exp_expected
 
 let rec translate_type const_env = function
   | Tprod ty_list -> Types.Tprod(List.map (translate_type const_env) ty_list)
   | Tid ln -> Types.Tid ln
   | Tarray (ty, e) ->
       let ty = translate_type const_env ty in
-      Types.Tarray (ty, translate_static_exp const_env e)
+      Types.Tarray (ty, expect_static_exp const_env e)
 
 and translate_exp const_env env e =
-  { Heptagon.e_desc = translate_desc e.e_loc const_env env e.e_desc;
+  let desc =
+    try (* try to see if the exp is a constant *)
+      Econst (translate_static_exp const_env e)
+    with
+        Not_static -> translate_desc e.e_loc const_env env e.e_desc in
+  { Heptagon.e_desc = desc;
     Heptagon.e_ty = Types.invalid_type;
     Heptagon.e_loc = e.e_loc }
 
 and translate_app const_env env app =
   let op = match app.a_op with
     | Epre None -> Heptagon.Epre None
-    | Epre (Some c) -> Heptagon.Epre (Some (translate_const c))
+    | Epre (Some e) ->
+        Heptagon.Epre (Some (expect_static_exp const_env e))
     | Efby -> Heptagon.Efby
     | Earrow -> Heptagon.Earrow
     | Eifthenelse -> Heptagon.Eifthenelse
@@ -155,14 +168,14 @@ and translate_app const_env env app =
 and translate_op_desc const_env desc =
   { Heptagon.op_name = desc.op_name;
     Heptagon.op_params =
-      List.map (translate_static_exp const_env) desc.op_params;
+      List.map (expect_static_exp const_env) desc.op_params;
     Heptagon.op_kind = translate_op_kind desc.op_kind }
 
 and translate_array_op const_env env = function
   | Eselect e_list ->
-      Heptagon.Eselect (List.map (translate_static_exp const_env) e_list)
+      Heptagon.Eselect (List.map (expect_static_exp const_env) e_list)
   | Eupdate e_list ->
-      Heptagon.Eupdate (List.map (translate_static_exp const_env) e_list)
+      Heptagon.Eupdate (List.map (expect_static_exp const_env) e_list)
   | Erepeat -> Heptagon.Erepeat
   | Eselect_slice -> Heptagon.Eselect_slice
   | Econcat -> Heptagon.Econcat
@@ -172,7 +185,7 @@ and translate_array_op const_env env = function
                           translate_op_desc const_env desc, None)
 
 and translate_desc loc const_env env = function
-  | Econst c -> Heptagon.Econst (translate_const c)
+  | Econst c -> Heptagon.Econst c
   | Evar x ->
       if Rename.mem x env then (* defined var *)
         Heptagon.Evar (Rename.name loc env x)
@@ -183,13 +196,6 @@ and translate_desc loc const_env env = function
   | Elast x -> Heptagon.Elast (Rename.name loc env x)
   | Etuple e_list ->
       Heptagon.Etuple (List.map (translate_exp const_env env) e_list)
-  | Eapp ({ a_op = (Earray_op Erepeat)} as app, e_list) ->
-      let e_list = List.map (translate_exp const_env env) e_list in
-      (match e_list with
-       | [{ Heptagon.e_desc = Heptagon.Econst c }; e1 ] ->
-           Heptagon.Econst (Heptagon.Carray (Heptagon.static_exp_of_exp e1, c))
-       | _ -> Heptagon.Eapp (translate_app const_env env app, e_list)
-      )
   | Eapp (app, e_list) ->
       let e_list = List.map (translate_exp const_env env) e_list in
       Heptagon.Eapp (translate_app const_env env app, e_list)
@@ -260,16 +266,16 @@ and translate_switch_handler loc const_env env sh =
 and translate_var_dec const_env env vd =
   { Heptagon.v_ident = Rename.name vd.v_loc env vd.v_name;
     Heptagon.v_type = translate_type const_env vd.v_type;
-    Heptagon.v_last = translate_last env vd.v_last;
+    Heptagon.v_last = translate_last const_env env vd.v_last;
     Heptagon.v_loc = vd.v_loc }
 
 and translate_vd_list const_env env =
   List.map (translate_var_dec const_env env)
 
-and translate_last env = function
+and translate_last const_env env = function
   | Var -> Heptagon.Var
   | Last (None) -> Heptagon.Last None
-  | Last (Some c) -> Heptagon.Last (Some (translate_const c))
+  | Last (Some e) -> Heptagon.Last (Some (expect_static_exp const_env e))
 
 let translate_contract const_env env ct =
   { Heptagon.c_assume = translate_exp const_env env ct.c_assume;
@@ -310,7 +316,7 @@ let translate_typedec const_env ty =
 let translate_const_dec const_env cd =
   { Heptagon.c_name = cd.c_name;
     Heptagon.c_type = translate_type const_env cd.c_type;
-    Heptagon.c_value = translate_static_exp const_env cd.c_value;
+    Heptagon.c_value = expect_static_exp const_env cd.c_value;
     Heptagon.c_loc = cd.c_loc; }
 
 let translate_program p =
diff --git a/compiler/main/hept2mls.ml b/compiler/main/hept2mls.ml
index bf78ad5..9bc8e24 100644
--- a/compiler/main/hept2mls.ml
+++ b/compiler/main/hept2mls.ml
@@ -182,12 +182,6 @@ let switch x ci_eqs_list =
   check ci_eqs_list;
   distribute ci_eqs_list
 
-let rec const = function
-  | Heptagon.Cint i -> Cint i
-  | Heptagon.Cfloat f -> Cfloat f
-  | Heptagon.Cconstr t -> Cconstr t
-  | Heptagon.Carray(n, c) -> Carray(n, const c)
-
 let translate_op_kind = function
   | Heptagon.Efun -> Efun
   | Heptagon.Enode -> Enode
@@ -210,8 +204,8 @@ let translate_iterator_type = function
 let rec application env { Heptagon.a_op = op; } e_list =
   match op, e_list with
     | Heptagon.Epre(None), [e] -> Efby(None, e)
-    | Heptagon.Epre(Some(c)), [e] -> Efby(Some(const c), e)
-    | Heptagon.Efby, [{ e_desc = Econst(c) } ; e] -> Efby(Some(c), e)
+    | Heptagon.Epre(Some c), [e] -> Efby(Some c, e)
+    | Heptagon.Efby, [{ e_desc = Econst c } ; e] -> Efby(Some c, e)
     | Heptagon.Eifthenelse, [e1;e2;e3] -> Eifthenelse(e1, e2, e3)
     | Heptagon.Ecall(op_desc, r), e_list ->
         Ecall(translate_op_desc op_desc, e_list, translate_reset r)
@@ -243,12 +237,10 @@ let rec translate env
     { Heptagon.e_desc = desc; Heptagon.e_ty = ty;
       Heptagon.e_loc = loc } =
   match desc with
-    | Heptagon.Econst(c) ->
+    | Heptagon.Econst c ->
         Env.const env (mk_exp ~loc:loc ~exp_ty:ty (Econst (const c)))
     | Heptagon.Evar x ->
         Env.con env x (mk_exp ~loc:loc ~exp_ty:ty (Evar x))
-    | Heptagon.Econstvar(x) ->
-        Env.const env (mk_exp ~loc:loc ~exp_ty:ty (Econstvar x))
     | Heptagon.Etuple(e_list) ->
         mk_exp ~loc:loc ~exp_ty:ty (Etuple (List.map (translate env) e_list))
     | Heptagon.Eapp(app, e_list) ->
diff --git a/compiler/minils/mls_utils.ml b/compiler/minils/mls_utils.ml
index e71e2c5..d318319 100644
--- a/compiler/minils/mls_utils.ml
+++ b/compiler/minils/mls_utils.ml
@@ -19,11 +19,7 @@ let err_message ?(exp=void) ?(loc=exp.e_loc) = function
 
 let rec static_exp_of_exp e =
   match e.e_desc with
-    | Econstvar n -> Svar n
-    | Econst (Cint i) -> Sconst i
-    | Ecall(op, [e1;e2], _) ->
-        let sop = op_from_app_name op.op_name in
-        Sop(sop, static_exp_of_exp e1, static_exp_of_exp e2)
+    | Econst se -> se
     | _ -> err_message ~exp:e Enot_static_exp
 
 (** @return the list of bounds of an array type*)
diff --git a/compiler/minils/sequential/mls2obc.ml b/compiler/minils/sequential/mls2obc.ml
index 1d4a04c..84bcb8f 100644
--- a/compiler/minils/sequential/mls2obc.ml
+++ b/compiler/minils/sequential/mls2obc.ml
@@ -63,11 +63,17 @@ let rec translate_type const_env = function
   | Types.Tprod ty -> assert false
 
 let rec translate_const const_env = function
-  | Minils.Cint v -> Cint v
-  | Minils.Cfloat v -> Cfloat v
-  | Minils.Cconstr c -> Cconstr c
-  | Minils.Carray (n, c) ->
-      Carray (int_of_static_exp const_env n, translate_const const_env c)
+  | Minils.Sint v -> Cint v
+  | Minils.Sbool v -> Cbool v
+  | Minils.Sfloat v -> Cfloat v
+  | Minils.Sconstructor c -> Cconstr c
+  | Minils.Sarray_power (n, c) ->
+      Carray_power (int_of_static_exp const_env n, translate_const const_env c)
+  | Minils.Sarray se_list ->
+      Carray (List.map (translate_const const_env) se_list)
+  | Minils.Stuple se_list ->
+      Ctuple (List.map (translate_const const_env) se_list)
+  | Minils.Svar n -> simplify const_env (SVar n)
 
 let rec translate_pat map = function
   | Minils.Evarpat x -> [ var_from_name map x ]
@@ -81,7 +87,6 @@ let rec translate const_env map (m, si, j, s)
   match desc with
     | Minils.Econst v -> Const (translate_const const_env v)
     | Minils.Evar n -> Lhs (var_from_name map n)
-    | Minils.Econstvar n -> Const (Cint (int_of_static_exp const_env (Svar n)))
     | Minils.Ecall ({ Minils.op_name = n; Minils.op_kind = Minils.Efun },
                     e_list, _) when Mls_utils.is_op n ->
         Op (n, List.map (translate const_env map (m, si, j, s)) e_list)
diff --git a/compiler/minils/sequential/obc.ml b/compiler/minils/sequential/obc.ml
index 6d25f1f..3ecf97d 100644
--- a/compiler/minils/sequential/obc.ml
+++ b/compiler/minils/sequential/obc.ml
@@ -39,9 +39,12 @@ and tdesc =
 
 type const =
   | Cint of int
+  | Cbool of bool
   | Cfloat of float
   | Cconstr of longname
-  | Carray of int * const
+  | Carray_power of int * const
+  | Carray of const list
+  | Ctuple of const list
 
 type lhs =
   | Var of var_name