diff --git a/global/modules.ml b/global/modules.ml
index fff3085..3564559 100644
--- a/global/modules.ml
+++ b/global/modules.ml
@@ -26,7 +26,7 @@ type env =
       mutable types: type_def NamesEnv.t;
       mutable constr: ty NamesEnv.t;
       mutable structs : structure NamesEnv.t;
-      mutable fields: name NamesEnv.t;
+      mutable fields : name NamesEnv.t;
       format_version : string;
     }
 
@@ -132,11 +132,15 @@ let add_constr f ty_res =
 let add_struct f fields =
   if NamesEnv.mem f current.structs then raise Already_defined;
   current.structs <- NamesEnv.add f fields current.structs
+let add_field f n =
+  if NamesEnv.mem f current.fields then raise Already_defined;
+  current.fields <- NamesEnv.add f n current.fields
 
 let find_value = find (fun ident m -> NamesEnv.find ident m.values)
 let find_type = find (fun ident m -> NamesEnv.find ident m.types)
 let find_constr = find (fun ident m -> NamesEnv.find ident m.constr)
 let find_struct = find (fun ident m -> NamesEnv.find ident m.structs)
+let find_field = find (fun ident m -> NamesEnv.find ident m.fields)
 
 let replace_value f signature =
   current.values <- NamesEnv.remove f current.values;
diff --git a/global/signature.ml b/global/signature.ml
index e42d727..4e9a41a 100644
--- a/global/signature.ml
+++ b/global/signature.ml
@@ -43,3 +43,13 @@ let mk_arg name ty =
 let mk_param name = 
   { p_name = name }
 
+let mk_field n ty =
+  { f_name = n; f_type = ty }
+
+let rec field_assoc f = function
+  | [] -> raise Not_found
+  | { f_name = n; f_type = ty }::l ->
+      if shortname f = n then
+        ty
+      else
+        field_assoc f l
diff --git a/heptagon/analysis/interface.ml b/heptagon/analysis/interface.ml
index bdd698b..1da5c45 100644
--- a/heptagon/analysis/interface.ml
+++ b/heptagon/analysis/interface.ml
@@ -8,59 +8,33 @@
 (**************************************************************************)
 (* Read an interface *)
 
-(* $Id$ *)
-
-open Misc
 open Ident
 open Names
-open Linearity
 open Heptagon
-open Global
+open Signature
 open Modules
 open Typing
 
-let rec split3 = function
-  | [] -> [], [], []
-  | (a,b,c)::l ->
-      let a_list, b_list, c_list = split3 l in
-	a::a_list, b::b_list, c::c_list
-
-let rec combine3 l1 l2 l3 = match l1, l2, l3 with
-  | [], [], [] -> []
-  | a::a_list, b::b_list, c::c_list ->
-      (a,b,c)::(combine3 a_list b_list c_list)
-
 module Type =
   struct
-    let sigtype { sig_name = name; sig_inputs = i_list; sig_outputs = o_list; 
-		  sig_node = node; sig_safe = safe; sig_params = params } =
-      let arg_dec_of_tuple (n, ty, l) = 
-	{ a_name = n;
-	  a_type = Tbase(check_type ty);
-	  a_linearity = l;
-	  a_pass_by_ref = false } in
-      let i_inputs, t_inputs, l_inputs = split3 i_list in
-      let o_outputs, t_outputs, l_outputs = split3 o_list in
-	name, { inputs = List.map arg_dec_of_tuple i_list;
-		outputs = List.map arg_dec_of_tuple o_list;
-		contract = None;
-		node = node;
-		safe = safe; 
-	        targeting = [];
-		params = params;
-		params_constraints = []; }
+    let sigtype { sig_name = name; sig_inputs = i_list; 
+                  sig_outputs = o_list; sig_params = params } =
+	      name, { node_inputs = i_list;
+		            node_outputs = o_list;
+		            node_params = params;
+		            node_params_constraints = []; }
 	  
     let read { interf_desc = desc; interf_loc = loc } =
       try
-	match desc with
-	  | Iopen(n) -> open_module n
-	  | Itypedef(tydesc) -> deftype NamesEnv.empty tydesc
-	  | Isignature(s) -> 
-	      let name, s = sigtype s in
-		add_value name s
+	      match desc with
+	        | Iopen(n) -> open_module n
+	        | Itypedef(tydesc) -> deftype NamesEnv.empty tydesc
+	        | Isignature(s) -> 
+	            let name, s = sigtype s in
+		            add_value name s
       with
-	  TypingError(error) -> message loc error
-
+	        TypingError(error) -> message loc error
+            
     let main l = 
       List.iter read l
   end
@@ -74,56 +48,53 @@ struct
     match tdesc with
       | Tabstract -> fprintf ff "@[type %s@.@]" name
       | Tenum(tag_name_list) ->
-	  fprintf ff "@[<hov 2>type %s = " name;
-	  print_list ff print_name " |" tag_name_list;
-	  fprintf ff "@.@]"
+	        fprintf ff "@[<hov 2>type %s = " name;
+	        print_list ff print_name " |" tag_name_list;
+	        fprintf ff "@.@]"
       | Tstruct(f_ty_list) ->
-	  fprintf ff "@[<hov 2>type %s = " name;
-	  fprintf ff "@[<hov 1>{";
-	  print_list ff 
-	    (fun ff (field, ty) -> print_name ff field;
-              fprintf ff ": ";
-	      print_type ff ty) ";" f_ty_list;
-	  fprintf ff "}@]@.@]"
+	        fprintf ff "@[<hov 2>type %s = " name;
+	        fprintf ff "@[<hov 1>{";
+	        print_list ff 
+	          (fun ff (field, ty) -> print_name ff field;
+               fprintf ff ": ";
+	             print_type ff ty) ";" f_ty_list;
+	        fprintf ff "}@]@.@]"
 
-  let signature ff name { inputs = inputs;
-			  outputs = outputs;
-			  contract = contract; node = node;
-			  safe = safe; params = params; params_constraints = constr } =
+  let signature ff name { node_inputs = inputs;
+			  node_outputs = outputs;
+			  node_params = params; 
+        node_params_constraints = constr } =
     let print ff arg =
       match arg.a_name with
-	| None -> print_type ff arg.a_type
-	| Some(name) -> 
-	    print_name ff name; fprintf ff ":"; print_type ff arg.a_type;
-	    fprintf ff " "; print_lin ff arg.a_linearity in
+	      | None -> print_type ff arg.a_type
+	      | Some(name) -> 
+	          print_name ff name; fprintf ff ":"; print_type ff arg.a_type
+    in
 
     let print_node_params ff = function
       | [] -> ()
       | l -> 
-	  fprintf ff "<<";
-	  print_list ff print_name "," l;
-	  fprintf ff ">>" in
+	        fprintf ff "<<";
+	        print_list ff print_name "," l;
+	        fprintf ff ">>" in
       
-    fprintf ff "@[<v 2>val ";
-    if safe then fprintf ff "safe ";
-    if node then fprintf ff "node " else fprintf ff "fun ";
-    print_name ff name;
-    print_node_params ff params;
-    fprintf ff "(@[";
-    print_list ff print ";" inputs;
-    fprintf ff "@]) returns (@[";
-    print_list ff print ";" outputs;
-    fprintf ff "@])";
-    (match constr with
-       | [] -> ()
-       | constr -> 
-	   fprintf ff "\n with: @[";
-	   print_list ff Static.print_size_constr "," constr;
-	   fprintf ff "@]"
-    );
-    optunit (print_contract ff) contract;
-    fprintf ff "@.@]"
-	
+      fprintf ff "@[<v 2>val ";
+      print_name ff name;
+      print_node_params ff params;
+      fprintf ff "(@[";
+      print_list ff print ";" inputs;
+      fprintf ff "@]) returns (@[";
+      print_list ff print ";" outputs;
+      fprintf ff "@])";
+      (match constr with
+         | [] -> ()
+         | constr -> 
+	           fprintf ff "\n with: @[";
+	           print_list ff Static.print_size_constr "," constr;
+	           fprintf ff "@]"
+      );
+      fprintf ff "@.@]"
+	      
   let print oc =
     let ff = formatter_of_out_channel oc in
     NamesEnv.iter (fun key typdesc -> deftype ff key typdesc) current.types;
diff --git a/heptagon/analysis/typing.ml b/heptagon/analysis/typing.ml
index 89c51c7..39bdb39 100644
--- a/heptagon/analysis/typing.ml
+++ b/heptagon/analysis/typing.ml
@@ -15,10 +15,11 @@ open Names
 open Ident
 open Location
 open Heptagon
-open Global
+open Signature
 open Modules
 open Initial
 open Static
+open Types
 
 type value = { ty: ty; mutable last: bool }
 
@@ -35,13 +36,16 @@ type error =
     | Enon_exaustive
     | Estate_clash
     | Epartial_switch of name
-    | Etwo_many_outputs
+    | Etoo_many_outputs
     | Esome_fields_are_missing
     | Esubscripted_value_not_an_array of ty
     | Earray_subscript_should_be_const 
     | Eundefined_const of name
     | Econstraint_solve_failed of size_constr
     | Etype_should_be_static of ty
+    | Erecord_type_expected of ty
+    | Eno_such_field of ty * longname
+    | Eempty_record
 
 exception Unify
 exception TypingError of error
@@ -102,7 +106,7 @@ let message loc kind =
 	"%aThe case %s is missing.\n"
 	output_location loc
 	s
- | Etwo_many_outputs ->
+ | Etoo_many_outputs ->
       Printf.eprintf 
 	"%aA function may only returns a basic value.\n"
 	output_location loc
@@ -134,6 +138,21 @@ let message loc kind =
        "%aThis type should be static : %a.\n"
 	output_location loc 
 	Printer.ptype ty
+ | Erecord_type_expected ty ->
+     Printf.eprintf 
+       "%aA record was expected (found %a).\n"
+	     output_location loc 
+	     Printer.ptype ty   
+ | Eno_such_field (ty, f) ->
+     Printf.eprintf 
+       "%aThe record type '%a' does not have a '%s' field.\n"
+	     output_location loc 
+	     Printer.ptype ty    
+       (shortname f)
+ | Eempty_record -> 
+     Printf.eprintf 
+       "%aThe record is empty.\n"
+	     output_location loc      
   end;
   raise Error
 
@@ -143,9 +162,10 @@ let add_type f type_def =
   try add_type f type_def with Already_defined -> error (Ealready_defined f)
 let add_constr f ty_res =
   try add_constr f ty_res with Already_defined -> error (Ealready_defined f)
-let add_field f ty_arg ty_res =
-  try add_field f ty_arg ty_res 
-  with Already_defined -> error (Ealready_defined f)
+let add_struct f fields =
+  try add_struct f fields with Already_defined -> error (Ealready_defined f)
+let add_field f n =
+  try add_field f n with Already_defined -> error (Ealready_defined f)
 
 let find_value f =
   try find_value f with Not_found -> error (Eundefined(fullname f))
@@ -155,6 +175,8 @@ let find_constr c =
   try find_constr c with Not_found -> error (Eundefined(fullname c))
 let find_field c =
   try find_field c with Not_found -> error (Eundefined(fullname c))
+let find_struct c =
+  try find_struct c with Not_found -> error (Eundefined(fullname c))
 
 let (curr_size_constr : size_constr list ref) = ref []
 let add_size_constr c =
@@ -175,33 +197,26 @@ let get_number_of_fields ty =
 
 let element_type ty =
   match ty with
-    | Tbase (Tarray (ty, _)) -> Tbase ty
+    | Tarray (ty, _) -> ty
     | _ -> error (Esubscripted_value_not_an_array ty)
 
 let size_exp ty =
   match ty with
-    | Tbase (Tarray (_, e)) -> e
+    | Tarray (_, e) -> e
     | _ -> error (Esubscripted_value_not_an_array ty)
 
 let rec unify t1 t2 = 
   match t1, t2 with
-    | Tprod(t1_list), Tprod(t2_list) ->
-	begin
-          try List.iter2 unify t1_list t2_list with _ -> raise Unify
-	end
-    | Tbase(b1), Tbase(b2) when b1 = b2 -> ()
-    | Tbase(Tbool), Tbase(Tid name_bool)  
-    | Tbase(Tid name_bool), Tbase(Tbool)
-	when name_bool = pbool -> ()
-    | Tbase(Tint), Tbase(Tid name_int)  
-    | Tbase(Tid name_int), Tbase(Tint)
-	when name_int = pint -> ()
-    | Tbase(Tfloat), Tbase(Tid name_float)  
-    | Tbase(Tid name_float), Tbase(Tfloat)
-	when name_float = pfloat -> ()
-    | Tbase(Tarray (ty1, e1)), Tbase(Tarray (ty2, e2)) ->
-	add_size_constr (Equal(e1,e2));
-	unify (Tbase ty1) (Tbase ty2)
+    | Tprod t1_list, Tprod t2_list ->
+        (try 
+           List.iter2 unify t1_list t2_list 
+         with 
+             _ -> raise Unify
+	      )
+    | b1, b2 when b1 = b2 -> ()
+    | Tarray (ty1, e1), Tarray (ty2, e2) ->
+	      add_size_constr (Equal(e1,e2));
+	      unify ty1 ty2
     | _ -> raise Unify
 
 let unify t1 t2 =
@@ -210,30 +225,26 @@ let unify t1 t2 =
 let less_than statefull = if not statefull then error Estate_clash
 
 let kind f statefull = function
-  | { inputs = ty_list1;
-      outputs = ty_list2;
-      node = n } -> 
-      let ty_of_arg_dec v = v.a_type in
-      if n & not(statefull) then error (Eshould_be_a_node(f)) 
-      else n, List.map ty_of_arg_dec ty_list1, List.map ty_of_arg_dec ty_list2
+  | { node_inputs = ty_list1;
+      node_outputs = ty_list2 } -> 
+      let ty_of_arg v = v.a_type in
+      (*if n & not(statefull) then error (Eshould_be_a_node(f)) *)
+      (*else n,*) List.map ty_of_arg ty_list1, List.map ty_of_arg ty_list2
 	
 let prod = function
   | []      -> assert false
   | [ty]    -> ty
-  | ty_list -> Tprod(ty_list)
+  | ty_list -> Tprod ty_list
 
-let rec typing_const c = 
-  let typed_c, ty = match c with
-    | Cint _     -> c, Tid(pint)
-    | Cfloat _   -> c, Tid(pfloat)
-    | 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(type ty, n)
-  in
-  typed_c, Tbase(ty)
+let rec typing_const c = match c with
+  | Cint _     -> c, Tid(pint)
+  | Cfloat _   -> c, Tid(pfloat)
+  | 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)
 	
 let typ_of_name h x = 
   try 
@@ -260,13 +271,13 @@ let typ_of_last h x =
       Not_found -> error (Eundefined(sourcename x))
     
 let desc_of_ty = function 
-  | Tbase(Tid(ty_name)) -> 
+  | Tid ty_name -> 
       let { info = tydesc } = find_type ty_name in tydesc
-  | Tbase(Tbool) -> Tenum ["true";"false"]
+  | Tid n when n = pbool  -> Tenum ["true";"false"]
   | _  -> Tabstract
 let set_of_constr = function
   | Tabstract | Tstruct _  -> assert false
-  | Tenum(tag_list) -> List.fold_right S.add tag_list S.empty
+  | Tenum tag_list -> List.fold_right S.add tag_list S.empty
 
 let name_mem n env =
   let check_one id _ acc =
@@ -274,40 +285,40 @@ let name_mem n env =
   in
     Env.fold check_one env false
 
-(* [check_type t] checks that t exists *)
+(** [check_type t] checks that t exists *)
 let rec check_type = function
-  | Tint | Tfloat | Tbool as t -> t
   | Tarray(ty, e) -> 
       Tarray(check_type ty, e) 
   | Tid(ty_name) ->
-      try Tid(Modname((find_type ty_name).qualid))
-      with Not_found -> error (Eundefined(fullname 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)
 
 let rec simplify_type const_env = function
-  | Tint | Tfloat | Tbool | Tid _ as t -> t
+  | Tid _ as t -> t
   | Tarray(ty, e) ->
       Tarray(simplify_type const_env ty, simplify const_env e)
+  | Tprod l -> 
+      Tprod (List.map (simplify_type const_env) l)
 
 let simplify_type loc const_env ty = 
   try
     simplify_type const_env ty
   with
-    Instanciation_failed -> message loc (Etype_should_be_static (Tbase ty))
+    Instanciation_failed -> message loc (Etype_should_be_static ty)
 
 let rec subst_type_vars m = function
   | Tarray(ty, e) -> Tarray(subst_type_vars m ty, size_exp_subst m e)
-  | t -> t
-
-let rec subst_type_vars m = function
-  | Tbase ty -> Tbase (subst_type_vars m ty)
   | Tprod l -> Tprod (List.map (subst_type_vars m) l)
+  | t -> t
 
 let equal expected_tag_list actual_tag_list =
    if not (List.for_all 
 	     (fun tag -> List.mem tag actual_tag_list) expected_tag_list)
   then error Enon_exaustive
 
-(* add two sets of names provided they are distinct *)
+(** Add two sets of names provided they are distinct *)
 let add env1 env2 =
   Env.fold 
     (fun elt ty env -> 
@@ -315,7 +326,7 @@ let add env1 env2 =
        then Env.add elt ty env
        else error (Ealready_defined(sourcename elt))) env1 env2
 
-(* checks that constructors are included in constructor list from type
+(** Checks that constructors are included in constructor list from type
    def and returns the difference *)
 let included_const s1 s2 =
   S.iter 
@@ -326,8 +337,8 @@ let diff_const defined_names local_names =
   included_const local_names defined_names;
   S.diff defined_names local_names
 
-(* checks that local_names are included in defined_names and returns *)
-(* the difference *)
+(** Checks that local_names are included in defined_names and returns
+    the difference *)
 let included_env s1 s2 =
   Env.iter 
     (fun elt _ -> if not (Env.mem elt s2) then error (Emissing(sourcename elt))) 
@@ -337,8 +348,8 @@ let diff_env defined_names local_names =
   included_env local_names defined_names;
   Env.diff defined_names local_names
 
-(* [merge [set1;...;setn]] returns a set of names defined in every seti *)
-(* and only partially defined names *)
+(** [merge [set1;...;setn]] returns a set of names defined in every seti
+ and only partially defined names *)
 let rec merge local_names_list =
   let two s1 s2 =
     let total, partial = Env.partition (fun elt -> Env.mem elt s2) s1 in
@@ -356,7 +367,7 @@ let rec merge local_names_list =
         let total, partial2 = two s total in
         total, Env.union partial1 partial2
 
-(* checks that every partial name has a last value *)
+(** Checks that every partial name has a last value *)
 let all_last h env =
   Env.iter 
     (fun elt _ ->
@@ -365,6 +376,56 @@ let all_last h env =
 
 let last = function | Var -> false | Last _ -> true
 
+(** Checks that a field is not defined twice in a list
+    of field name, exp.*)
+let check_field_unicity l =
+  let add_field acc (f,e) = 
+    if S.mem (shortname f) acc then 
+      message e.e_loc (Ealready_defined (fullname f))
+    else
+      S.add (shortname f) acc
+  in
+    List.fold_left add_field S.empty l
+
+(** @return the qualified name and list of fields of 
+    the type with name [n].
+    Prints an error message if the type is not a record type.
+    [loc] is the location used for error reporting.*)
+let struct_info_from_name loc n =
+  try
+    let { qualid = q;
+		      info = fields } = find_struct n in
+      q, fields           
+  with 
+      Not_found -> message loc (Erecord_type_expected (Tid n)) 
+
+(** @return the qualified name and list of fields of a record type.
+    Prints an error message if the type is not a record type.
+    [loc] is the location used for error reporting.*)
+let struct_info loc ty = match ty with
+  | Tid n -> struct_info_from_name loc n
+  | _ -> message loc (Erecord_type_expected ty)
+
+(** @return the qualified name and list of fields of the 
+    record type corresponding to the field named [n].
+    Prints an error message if the type is not a record type.
+    [loc] is the location used for error reporting.*)
+let struct_info_from_field loc f = 
+  try 
+    let { qualid = q; info = n } = find_field f in
+      struct_info_from_name loc (Modname { qual = q.qual; id = n })
+  with
+      Not_found -> message loc (Eundefined (fullname 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 =
+  try 
+    check_type (field_assoc f fields)
+  with 
+      Not_found -> message loc (Eno_such_field (t1, f)) 
+
 let rec typing statefull h e =
   try
     let typed_desc,ty = match e.e_desc with
@@ -372,7 +433,7 @@ let rec typing statefull h e =
 	  let typed_c, ty = typing_const c in
 	  Econst(c),
 	  ty
-      | Econstvar(x) -> Econstvar x, Tbase Tint
+      | Econstvar(x) -> Econstvar x, Tid Initial.pint
       | Evar(x) ->
 	  Evar(x),
 	  typ_of_varname h x
@@ -388,52 +449,47 @@ let rec typing statefull h e =
 	  let ty, op, typed_e_list = typing_app statefull h op e_list in
 	  Eapp({ app with a_op = op }, typed_e_list),
 	  ty
-      | Efield(e, field) ->
-	  let { qualid = q;
-		info = { arg = ty_arg; res = ty_res } } = find_field field in
-	  let typed_e = expect statefull h (Tbase(ty_arg)) e in
-	  Efield(typed_e, Modname(q)),
-	  Tbase(ty_res)
+      | Efield(e, f) ->
+	      let typed_e, t1 = typing statefull h e in
+        let q, fields = struct_info e.e_loc t1 in
+        let t2 = field_type f fields t1 e.e_loc in
+          Efield(typed_e, Modname { qual = q.qual; id = shortname f }), t2
+
       | Estruct(l) ->
-	  let { qualid = q;
-		info = { arg = ty_arg } } = find_field (fst (List.hd l)) in
-	  let size = get_number_of_fields ty_arg in
-	  let rec fieldrec acc_l acc = function
-	    | [] -> 
-		List.rev acc_l, 
-		Tbase(ty_arg)
-	    | (field, e) :: l ->
-		if S.mem (shortname field) acc 
-		then error (Ealready_defined(fullname field));
-		let { qualid = q;
-		      info = { arg = ty; res = ty_res } } = find_field field in
-		let typed_e = expect statefull h (Tbase(ty_res)) e in
-		unify (Tbase(ty)) (Tbase(ty_arg));
-		fieldrec 
-		  ((Modname(q),typed_e)::acc_l) 
-		  (S.add (shortname field) acc)
-		  l in
-	  let typed_l, ty = fieldrec [] S.empty l in
-	  (* check that no field is missing *)
-	  if List.length l <> size then error Esome_fields_are_missing;
-	  Estruct(typed_l),
-	  ty
+          (* find the record type using the first field *)
+          let q, fields = 
+            (match l with
+               | [] -> message e.e_loc (Eempty_record)
+               | (f,_)::l -> struct_info_from_field e.e_loc f
+            ) in
+            
+            if List.length l <> List.length fields then 
+              message e.e_loc Esome_fields_are_missing;  
+            check_field_unicity l;
+            let l = List.map (typing_field statefull h fields (Tid (Modname q))) l in
+              Estruct l, Tid (Modname q)
+
       | Earray (exp::e_list) -> 
-	  let typed_exp, t1 = typing statefull h exp in
-	  let typed_e_list = List.map (expect statefull h t1) e_list in
-	    Earray(typed_exp::typed_e_list), 
-	    const_array_of t1 (List.length e_list + 1)
+	        let typed_exp, t1 = typing statefull h exp in
+	        let typed_e_list = List.map (expect statefull h t1) e_list in
+	          Earray(typed_exp::typed_e_list), 
+	        const_array_of t1 (List.length e_list + 1)
+       (* Arity problems *)
       | Earray [] -> 
-	  error (Earity_clash (0, 1))
-      | Ereset_mem _ -> assert false
+	        error (Earity_clash (0, 1))
     in
-      { e with
-	  e_desc = typed_desc;
-	  e_ty = ty; },
-      ty
+      { e with e_desc = typed_desc; e_ty = ty; }, ty
   with
       TypingError(kind) -> message e.e_loc kind
       
+and typing_field statefull h fields t1 (f, e) = 
+  try
+    let ty = check_type (field_assoc f fields) in
+    let typed_e = expect statefull 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
   try 
@@ -458,30 +514,52 @@ and typing_app statefull h op e_list =
 	let typed_e2 = expect statefull h t1 e2 in
 	t1, op, [typed_e1;typed_e2]
     | Eifthenelse, [e1;e2;e3] ->
-	let typed_e1 = expect statefull h (Tbase tbool) e1 in
+	let typed_e1 = expect statefull h (Tid Initial.pbool) e1 in
 	let typed_e2, t1 = typing statefull h e2 in
 	let typed_e3 = expect statefull h t1 e3 in
-	t1, op, [typed_e1; typed_e2; typed_e3]
-    | (Enode(f, params) | Eevery(f, params) | Eop(f, params)), e_list ->
-	let { qualid = q; info = ty_desc } = find_value f in
-	let k, expected_ty_list, result_ty_list = kind f statefull ty_desc in
-	let m = List.combine ty_desc.params params in
-	let expected_ty_list = List.map (subst_type_vars m) expected_ty_list in
-	let typed_e_list = typing_args statefull h expected_ty_list e_list in
-	let size_constrs = instanciate_constr m ty_desc.params_constraints in
-	let result_ty_list = List.map (subst_type_vars m) result_ty_list in
-	  List.iter add_size_constr size_constrs;
-	let f = Modname(q) in
-	(prod result_ty_list,
-	 (if k then Enode(f, params) else Eop(f, params)),
-	 typed_e_list)
+	t1, op, [typed_e1; typed_e2; typed_e3]  
+    | Ecall ( { op_name = f; op_params = params } as op_desc , reset), e_list ->
+	      let { qualid = q; info = ty_desc } = find_value f in
+	      let expected_ty_list, result_ty_list = kind f statefull 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 typed_e_list = typing_args statefull h expected_ty_list e_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
+	        List.iter add_size_constr size_constrs;
+	        (prod result_ty_list,
+	         Ecall ( { op_desc with op_name = Modname(q) }, reset),
+	         typed_e_list)
+    | Earray_op op, e_list -> 
+        let ty, op, e_list = typing_array_op statefull h op e_list in
+          ty, Earray_op op, e_list
+    | Efield_update f, [e1; e2] -> 
+	      let typed_e1, t1 = typing statefull h e1 in
+        let q, fields = struct_info e1.e_loc t1 in
+        let t2 = field_type f fields t1 e1.e_loc in
+        let typed_e2 = expect statefull h t2 e2 in
+          t1, op, [typed_e1; typed_e2]
+
+     (*Arity problems*)
+    | Epre _, _ ->
+	      error (Earity_clash(List.length e_list, 1))
+    | (Efby | Earrow), _ ->
+	error (Earity_clash(List.length e_list, 2))
+    | Eifthenelse, _ ->
+	error (Earity_clash(List.length e_list, 2))
+    | Efield_update field, _ ->
+	error (Earity_clash(List.length e_list, 2))
+
 (*Array operators*)
+and typing_array_op statefull h op e_list = 
+  match op, e_list with
     | Erepeat, [e1; e2] -> 
-	let typed_e2 = expect statefull h (Tbase(Tint)) e2 in
+	let typed_e2 = expect statefull h (Tid Initial.pint) e2 in
 	let e2 = size_exp_of_exp e2 in
 	let typed_e1, t1 = typing statefull h e1 in
 	  add_size_constr (LEqual (SConst 1, e2));
-	  array_of t1 e2, op, [typed_e1; typed_e2]
+	  Tarray (t1, e2), op, [typed_e1; typed_e2]
     | Eselect idx_list, [e1] -> 
 	let typed_e1, t1 = typing statefull h e1 in
 	  typing_array_subscript statefull h idx_list t1, op, [typed_e1]
@@ -496,14 +574,14 @@ and typing_app statefull h op e_list =
 	let typed_e2 = expect statefull h ty e2 in
 	  t1, op, [typed_e1; typed_e2]
     | Eselect_slice, [e; idx1; idx2] ->
-	let typed_idx1 = expect statefull h (Tbase(Tint)) idx1 in
-	let typed_idx2 = expect statefull h (Tbase(Tint)) idx2 in
+	let typed_idx1 = expect statefull h (Tid Initial.pint) idx1 in
+	let typed_idx2 = expect statefull h (Tid Initial.pint) idx2 in
 	let typed_e, t1 = typing statefull h e in
 	  (*Create the expression to compute the size of the array *)
 	let e1 = SOp (SMinus, size_exp_of_exp idx2, size_exp_of_exp idx1) in 
 	let e2 = SOp (SPlus, e1, SConst 1) in
 	  add_size_constr (LEqual (SConst 1, e2));
-	  array_of (element_type t1) e2, op, [typed_e; typed_idx1; typed_idx2]
+	  Tarray (element_type t1, e2), op, [typed_e; typed_idx1; typed_idx2]
     | Econcat, [e1; e2] -> 
 	let typed_e1, t1 = typing statefull h e1 in
 	let typed_e2, t2 = typing statefull h e2 in
@@ -513,52 +591,27 @@ and typing_app statefull h op e_list =
 	      TypingError(kind) -> message e1.e_loc kind 
 	  end;
 	  let n = SOp (SPlus, size_exp t1, size_exp t2) in
-	    array_of (element_type t1) n, op, [typed_e1; typed_e2]
-    | Eiterator (it, f, params, reset), e::e_list ->
-	let { qualid = q; info = ty_desc } = find_value f in
-	let f = Modname(q) in
-	let _, expected_ty_list, result_ty_list = kind f statefull ty_desc in
-	let m = List.combine ty_desc.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.params_constraints in
-	let result_ty_list = List.map (subst_type_vars m) result_ty_list in
-	let typed_e = expect statefull h (Tbase Tint) e in
-	let e = size_exp_of_exp e in
-	let ty, typed_e_list = typing_iterator statefull h it e 
-	  expected_ty_list result_ty_list e_list in 
-	  add_size_constr (LEqual (SConst 1, e));
-	  List.iter add_size_constr size_constrs;
-	  ty, Eiterator(it, f, params, reset), typed_e::typed_e_list
-    | Ecopy, [e] -> 
-	let typed_e, ty = typing statefull h e in
-	  ty, op, [typed_e]
-    | Efield_update field, [e1; e2] -> 
-	  let { qualid = q;
-		info = { arg = ty_arg; res = ty_res } } = find_field field in
-	  let typed_e1 = expect statefull h (Tbase(ty_arg)) e1 in
-	  let typed_e2 = expect statefull h (Tbase(ty_res)) e2 in
-	    Tbase(ty_arg), op, [typed_e1; typed_e2]
-    | Eflatten n, [e] -> 
-	  let { qualid = q;
-		info = { fields = fields } } = find_struct n in	
-	  let typed_e = expect statefull h (Tbase(Tid (Modname q))) e in
-	    prod (List.map (fun (_, ty) -> Tbase (check_type ty)) fields), op, [typed_e]
-    | Emake n, e_list ->
-	  let { qualid = q;
-		info = { fields = fields } } = find_struct n in	
-	    if List.length e_list <> List.length fields then 
-	      error (Earity_clash(List.length e_list, List.length fields));
-	    let typed_e_list = List.map2 
-	      (fun e (_,ty) -> expect statefull h (Tbase (check_type ty)) e) 
-	      e_list fields in
-	      Tbase (Tid (Modname q)), op, typed_e_list
-(*Arity problems*)
-    | Epre _, _ ->
-	error (Earity_clash(List.length e_list, 1))
-    | (Efby | Earrow), _ ->
-	error (Earity_clash(List.length e_list, 2))
-    | Eifthenelse, _ ->
-	error (Earity_clash(List.length e_list, 2))
+	    Tarray (element_type t1, n), op, [typed_e1; typed_e2]
+    | Eiterator (it, ({ op_name = f; op_params = params } as op_desc), reset),
+        e::e_list ->
+	      let { qualid = q; info = ty_desc } = find_value f in
+	      let f = Modname(q) in
+	      let expected_ty_list, result_ty_list = kind f statefull 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 = size_exp_of_exp e in
+	      let ty, typed_e_list = typing_iterator statefull h it e 
+	        expected_ty_list result_ty_list e_list in 
+	        add_size_constr (LEqual (SConst 1, e));
+	        List.iter add_size_constr size_constrs;
+	        ty, Eiterator(it, { op_desc with op_name = f }, reset),
+          typed_e::typed_e_list
+
+    (*Arity problems*)
     | Eiterator _, _ -> 
 	error (Earity_clash(List.length e_list, 1))
     | Econcat, _ ->
@@ -573,49 +626,45 @@ and typing_app statefull h op e_list =
 	error (Earity_clash(List.length e_list, 2))
     | Erepeat _, _ -> 
 	error (Earity_clash(List.length e_list, 2))
-    | Ecopy, _ -> 
-	error (Earity_clash(List.length e_list, 1))
-    | Efield_update field, _ ->
-	error (Earity_clash(List.length e_list, 2))
 		
 and typing_iterator statefull h it n args_ty_list result_ty_list e_list = 
   match it with 
     | Imap ->
-	let args_ty_list = List.map (fun ty -> array_of ty n) args_ty_list in
-	let result_ty_list = List.map (fun ty -> array_of ty n) result_ty_list in
-	let typed_e_list = typing_args statefull h args_ty_list e_list in
-	  prod result_ty_list, typed_e_list
+	      let args_ty_list = List.map (fun ty -> Tarray(ty, n)) args_ty_list in
+	      let result_ty_list = List.map (fun ty -> Tarray(ty, n)) result_ty_list in
+	      let typed_e_list = typing_args statefull h args_ty_list e_list in
+	        prod result_ty_list, typed_e_list
     | Ifold -> 
-	let args_ty_list = incomplete_map (fun ty -> array_of ty n) args_ty_list in
-	let typed_e_list = typing_args statefull h args_ty_list e_list in
-	  (*check accumulator type matches in input and output*)
-	  if List.length result_ty_list > 1 then
-	    error (Etwo_many_outputs);
-	  begin try
-	    unify (last_element args_ty_list) (List.hd result_ty_list)
-	  with 
-	      TypingError(kind) -> message (List.hd e_list).e_loc kind 
-	  end;
-	  (List.hd result_ty_list), typed_e_list
+	      let args_ty_list = incomplete_map (fun ty -> Tarray (ty, n)) args_ty_list in
+	      let typed_e_list = typing_args statefull h args_ty_list e_list in
+	        (*check accumulator type matches in input and output*)
+	        if List.length result_ty_list > 1 then
+	          error (Etoo_many_outputs);
+	        begin try
+	          unify (last_element args_ty_list) (List.hd result_ty_list)
+	        with 
+	            TypingError(kind) -> message (List.hd e_list).e_loc kind 
+	        end;
+	        (List.hd result_ty_list), typed_e_list
     | Imapfold -> 
-	let args_ty_list = incomplete_map (fun ty -> array_of ty n) args_ty_list in
-	let result_ty_list = incomplete_map (fun ty -> array_of ty n) result_ty_list in
-	let typed_e_list = typing_args statefull h args_ty_list e_list in
-	  (*check accumulator type matches in input and output*)
-	   begin try
-	      unify (last_element args_ty_list) (last_element result_ty_list)
-	    with 
-		TypingError(kind) -> message (List.hd e_list).e_loc kind 
-	   end;
-	   prod result_ty_list, typed_e_list
+	      let args_ty_list = incomplete_map (fun ty -> Tarray (ty, n)) args_ty_list in
+	      let result_ty_list = incomplete_map (fun ty -> Tarray (ty, n)) result_ty_list in
+	      let typed_e_list = typing_args statefull h args_ty_list e_list in
+	        (*check accumulator type matches in input and output*)
+	        begin try
+	          unify (last_element args_ty_list) (last_element result_ty_list)
+	        with 
+		          TypingError(kind) -> message (List.hd e_list).e_loc kind 
+	        end;
+	        prod result_ty_list, typed_e_list
 
 and typing_array_subscript statefull h idx_list ty  = 
   match ty, idx_list with
     | ty, [] -> ty 
-    | Tbase(Tarray(ty, exp)), idx::idx_list -> 
-	add_size_constr (LEqual (SConst 0, idx));
-	add_size_constr (LEqual (idx, SOp(SMinus, exp, SConst 1)));
-	typing_array_subscript statefull h idx_list (Tbase ty) 
+    | Tarray(ty, exp), idx::idx_list -> 
+	      add_size_constr (LEqual (SConst 0, idx));
+	      add_size_constr (LEqual (idx, SOp(SMinus, exp, SConst 1)));
+	      typing_array_subscript statefull h idx_list ty 
     | _, _ -> error (Esubscripted_value_not_an_array ty)
 
 (* This function checks that the array dimensions matches
@@ -623,11 +672,11 @@ and typing_array_subscript statefull h idx_list ty  =
 and typing_array_subscript_dyn statefull h idx_list ty = 
   match ty, idx_list with
     | ty, [] -> ty, [] 
-    | Tbase(Tarray(ty, exp)), idx::idx_list -> 
-	let typed_idx = expect statefull h (Tbase(Tint)) idx in 
-	let ty, typed_idx_list = 
-	  typing_array_subscript_dyn statefull h idx_list (Tbase ty) in
-	  ty, typed_idx::typed_idx_list 
+    | Tarray(ty, exp), idx::idx_list -> 
+	      let typed_idx = expect statefull h (Tid Initial.pint) idx in 
+	      let ty, typed_idx_list = 
+	        typing_array_subscript_dyn statefull h idx_list ty in
+	        ty, typed_idx::typed_idx_list 
     | _, _ -> error (Esubscripted_value_not_an_array ty)
 
 and typing_args statefull h expected_ty_list e_list =
@@ -672,7 +721,7 @@ let rec typing_eq statefull h acc eq =
 	Epresent(typed_ph,typed_b),
 	acc
     | Ereset(eq_list, e) ->
-	let typed_e = expect statefull h (Tbase(tbool)) e in
+	let typed_e = expect statefull h (Tid Initial.pbool) e in
 	let typed_eq_list, acc = typing_eq_list statefull h acc eq_list in
 	Ereset(typed_eq_list,typed_e),
 	acc
@@ -706,7 +755,7 @@ and typing_automaton_handlers statefull h acc state_handlers =
     
   let escape statefull h ({ e_cond = e; e_next_state = n } as esc) =
     if not (S.mem n states) then error (Eundefined(n));
-    let typed_e = expect statefull h (Tbase(tbool)) e in
+    let typed_e = expect statefull h (Tid Initial.pbool) e in
     { esc with e_cond = typed_e } in
     
   let handler 
@@ -752,7 +801,7 @@ and typing_switch_handlers statefull h acc ty switch_handlers =
 
 and typing_present_handlers statefull h acc def_names present_handlers =
   let handler ({ p_cond = e; p_block = b }) =
-    let typed_e = expect false h (Tbase(tbool)) e in
+    let typed_e = expect false h (Tid Initial.pbool) e in
     let typed_b, defined_names, _ = typing_block statefull h b in
     { p_cond = typed_e; p_block = typed_b },
     defined_names
@@ -793,8 +842,8 @@ and build h h0 dec =
 	then error (Ealready_defined(sourcename n))
 	else
 	  ({ v with v_type = ty }::acc_dec,
-	   Env.add n (Tbase(ty)) acc_defined, 
-	   Env.add n { ty = Tbase(ty); last = last l } h)
+	   Env.add n ty acc_defined, 
+	   Env.add n { ty = ty; last = last l } h)
       with
 	| TypingError(kind) -> message loc kind)
     ([], Env.empty, h) dec
@@ -803,7 +852,7 @@ 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 = Tbase Tint; last = false } h
+    Env.add param { ty = Tid Initial.pint; last = false } h
   in
     List.fold_left add_one h params
 
@@ -822,9 +871,9 @@ let typing_contract statefull h contract =
       let typed_eq, defined_names = typing_eq_list statefull h' Env.empty eq in
       
       (* assumption *)
-      let typed_e_a = expect statefull h' (Tbase(tbool)) e_a in
+      let typed_e_a = expect statefull h' (Tid Initial.pbool) e_a in
       (* property *)
-      let typed_e_g = expect statefull h' (Tbase(tbool)) e_g in
+      let typed_e_g = expect statefull h' (Tid Initial.pbool) e_g in
       
       included_env local_names defined_names;
       included_env defined_names local_names;
@@ -836,21 +885,14 @@ let typing_contract statefull h contract =
 	     c_enforce = typed_e_g },
       controllable_names, h
 
-let signature const_env statefull params returns contract node_params constraints = 
+let signature const_env inputs returns params constraints = 
   let arg_dec_of_var_dec vd =
-    { a_name = Some (sourcename vd.v_name);
-      a_type = Tbase(check_type vd.v_type);
-      a_linearity = vd.v_linearity;
-      a_pass_by_ref = false; } 
+    mk_arg (Some (name vd.v_name)) (check_type vd.v_type)
   in
-    { inputs = List.map arg_dec_of_var_dec params;
-      outputs = List.map arg_dec_of_var_dec returns;
-      contract = contract;
-      node = statefull;
-      safe = false;
-      targeting = [];
-      params = node_params; 
-      params_constraints = constraints; }
+    { node_inputs = List.map arg_dec_of_var_dec inputs;
+      node_outputs = List.map arg_dec_of_var_dec returns;
+      node_params = List.map mk_param params; 
+      node_params_constraints = constraints; }
 
 let solve loc env cl =
   try 
@@ -858,7 +900,7 @@ 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 node const_env ({ n_name = f; 
 		  n_input = i_list; n_output = o_list;
 		  n_contract = contract;
 		  n_local = l_list; n_equs = eq_list; n_loc = loc;
@@ -868,36 +910,26 @@ let node const_env ({ n_name = f; n_statefull = statefull;
     let typed_o_list, output_names, h = build h h o_list in
     
     (* typing contract *)
-    let typed_contract, controllable_names, h = typing_contract statefull h contract in
+    let typed_contract, controllable_names, h = typing_contract false h contract in
 
     let typed_l_list, local_names, h = build h h l_list in
-    let typed_eq_list, defined_names = typing_eq_list statefull h Env.empty eq_list in
-    if not (statefull) & (List.length o_list <> 1) 
-    then error (Etwo_many_outputs);
+    let typed_eq_list, defined_names = typing_eq_list false 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
     included_env expected_names defined_names;
     included_env defined_names expected_names;
 
     let cl = get_size_constr () in
-    let ff = Format.formatter_of_out_channel stdout in
-      Format.fprintf ff "Gathered constraints before solving for %s: %d\n " f (List.length cl);
-      print_list ff print_size_constr ", " cl; 
-      Format.fprintf ff "\n"; 
-
-      let cl = solve loc const_env cl in
-      Format.fprintf ff "Constraints after solving for %s: %d\n " f (List.length cl);
-      print_list ff print_size_constr ", " cl; 
-      Format.fprintf ff "\n"; 
-      Format.fprintf ff "@?" ;
-
-      add_value f (signature const_env statefull i_list o_list contract node_params cl);
+    let cl = solve loc const_env cl in
+      add_value f (signature const_env i_list o_list node_params cl);
 
       { n with 
-	  n_input = List.rev typed_i_list;
-	  n_output = List.rev typed_o_list;
-	  n_local = typed_l_list;
-	  n_contract = typed_contract;
-	  n_equs = typed_eq_list }
+	        n_input = List.rev typed_i_list;
+	        n_output = List.rev typed_o_list;
+	        n_local = typed_l_list;
+	        n_contract = typed_contract;
+	        n_equs = typed_eq_list }
   with
     | TypingError(error) -> message loc error
 
@@ -906,21 +938,24 @@ let deftype const_env { t_name = n; t_desc = tdesc; t_loc = loc } =
     match tdesc with
       | Type_abs -> add_type n Tabstract
       | Type_enum(tag_name_list) ->
-	  add_type n (Tenum(tag_name_list));
-	  List.iter (fun tag -> add_constr tag (Tid(longname n))) tag_name_list
+	        add_type n (Tenum tag_name_list);
+	        List.iter (fun tag -> add_constr tag (Tid (longname n))) tag_name_list
       | Type_struct(field_ty_list) ->
-	  let field_ty_list = 
-	    List.map (fun (n,ty) -> n, simplify_type loc const_env ty) field_ty_list in
-	  add_type n (Tstruct(field_ty_list));
-	  add_struct n field_ty_list;
-	  List.iter 
-	    (fun (field, ty) -> 
-	      add_field field (Tid(longname n)) (check_type ty)) field_ty_list
+	        let field_ty_list = 
+	          List.map (fun f -> 
+                        mk_field f.f_name 
+                          (simplify_type loc const_env f.f_type)) 
+              field_ty_list in
+	          add_type n (Tstruct field_ty_list);
+	          add_struct n field_ty_list;
+	          List.iter 
+	            (fun f -> add_field f.f_name n) field_ty_list
   with
       TypingError(error) -> message loc error
 
 let build_const_env cd_list =
-  List.fold_left (fun env cd -> NamesEnv.add cd.c_name cd.c_value env) NamesEnv.empty cd_list
+  List.fold_left (fun env cd -> NamesEnv.add cd.c_name cd.c_value env) 
+    NamesEnv.empty cd_list
 
 let program 
     ({ p_opened = opened; p_types = p_type_list;
diff --git a/heptagon/printer.ml b/heptagon/printer.ml
index 8423936..dac38cf 100644
--- a/heptagon/printer.ml
+++ b/heptagon/printer.ml
@@ -18,8 +18,9 @@ open Heptagon
 open Modules
 open Static
 open Format
-
-
+open Pp_tools
+open Types
+open Signature
 
 let iterator_to_string i = 
   match i with 
@@ -27,73 +28,13 @@ let iterator_to_string i =
     | Ifold -> "fold"
     | Imapfold -> "mapfold"
 
-
-let rec print_list ff print sep l =
-  match l with
-    | [] -> ()
-    | [x] -> print ff x
-    | x :: l ->
-        print ff x;
-        fprintf ff "%s@ " sep;
-        print_list ff print sep l
-
-(* Infix chars are surrounded by parenthesis *)
-let is_infix =
-  let module StrSet = Set.Make(String) in
-  let set_infix =
-    List.fold_right
-      StrSet.add
-      ["or"; "quo"; "mod"; "land"; "lor"; "lxor"; "lsl"; "lsr"; "asr"]
-      StrSet.empty in
-  fun s -> StrSet.mem s set_infix
-
-let print_name ff s =
-  let c = String.get s 0 in
-  let s = if is_infix s then "(" ^ s ^ ")"
-  else match c with
-    | 'a' .. 'z' | 'A' .. 'Z' | '_' | '`' -> s
-    | '*' -> "( " ^ s ^ " )"
-    | _ -> if s = "()" then s else "(" ^ s ^ ")" in
-  fprintf ff "%s" s
-
-let print_longname ff ln =
-  let ln = currentname ln in
-  match ln with
-    | Name(m) -> print_name ff m
-    | Modname({ qual = "Pervasives"; id = m }) ->
-        print_name ff m
-    | Modname({ qual = m1; id = m2 }) ->
-        fprintf ff "%s." m1; print_name ff m2
-
-let print_ident ff id =
-  fprintf ff "%s" (name id)
-
 let print_iterator ff it =
   fprintf ff "%s" (iterator_to_string it)
 
 let rec print_pat ff = function
   | Evarpat(n) -> print_ident ff n
   | Etuplepat(pat_list) ->
-      fprintf ff "@[(";
-      print_list ff print_pat "," pat_list;
-      fprintf ff ")@]"
-
-let rec print_type ff = function
-  | Tint -> fprintf ff  "int"
-  | Tbool -> fprintf ff "bool"
-  | Tfloat -> fprintf ff  "float"
-  | Tid(id) -> print_longname ff id
-  | Tarray(ty, e) ->
-      print_type ff ty;
-      fprintf ff "^";
-      print_size_exp ff e;
-
-and print_type ff = function
-  | Tbase(ty) -> print_type ff ty
-  | Tprod(ty_list) ->
-      fprintf ff "@[(";
-      print_list ff print_type " *" ty_list;
-      fprintf ff ")@]"
+      print_list_r print_pat "(" "," ")" ff pat_list
 
 and print_c ff = function
   | Cint i -> fprintf ff "%d" i
@@ -117,7 +58,7 @@ and print_vd ff { v_name = n; v_type = ty; v_last = last } =
   fprintf ff "@]"
 
 and print_exps ff e_list =
-  fprintf ff "@[("; print_list ff print_exp "," e_list; fprintf ff ")@]"
+  print_list_r print_exp "(" "," ")" ff e_list
 
 and print_exp ff e =
   if !Misc.full_type_info then fprintf ff "(";
@@ -127,41 +68,24 @@ and print_exp ff e =
     | Elast x -> fprintf ff "last "; print_ident ff x
     | Econst c -> print_c ff c
     | Eapp({ a_op = op }, e_list) -> print_op ff op e_list
-    | Etuple(e_list) ->
-        fprintf ff "@[(";
-        print_list ff print_exp "," e_list;
-        fprintf ff ")@]"
+    | Etuple(e_list) -> print_exps ff e_list
     | Efield(e, field) ->
         print_exp ff e; fprintf ff ".";
         print_longname ff field
     | Estruct(f_e_list) ->
-        fprintf ff "@[<v 1>{";
-        print_list ff
+        print_list_r
           (fun ff (field, e) -> print_longname ff field;fprintf ff " = ";
              print_exp ff e)
-          ";" f_e_list;
+          "{" ";" "}" ff f_e_list;
         fprintf ff "}@]"
-    | Earray(e_list) ->
-        fprintf ff "@[[";
-        print_list ff print_exp "," e_list;
-        fprintf ff "]@]"
-    | Ereset_mem(y,v,res) ->
-	fprintf ff "@[reset_mem ";
-	print_ident ff y;
-	fprintf ff " = ";
-	print_exp ff v;
-	fprintf ff " every ";
-	print_ident ff res;
-	fprintf ff "@]"
+    | Earray e_list ->
+        print_list_r print_exp "[" "," "]" ff e_list
   end;
   if !Misc.full_type_info then fprintf ff " : %a)" print_type e.e_ty
 
 and print_call_params ff = function
   | [] -> ()
-  | l -> 
-      fprintf ff "<<";
-      print_list ff print_size_exp "," l;
-      fprintf ff ">>"
+  | l -> print_list_r print_size_exp "<<" "," ">>" ff l
 
 and print_op ff op e_list =
   match op, e_list with
@@ -174,105 +98,81 @@ and print_op ff op e_list =
         fprintf ff "@ then@ "; print_exp ff e2;
         fprintf ff "@ else@ "; print_exp ff e3;
         fprintf ff "@]"
-    | Enode(f, params), e_list ->
+    | Ecall({ op_name = f; op_params = params }, reset), e_list ->
         print_longname ff f;
-	print_call_params ff params;
-        fprintf ff "(@["; print_list ff print_exp "," e_list;
-        fprintf ff ")@]"
-    | Eevery(f,params), e_list ->
-        print_longname ff f;
-	print_call_params ff params;
-        fprintf ff "(@["; print_list ff print_exp "," e_list;
-        fprintf ff ")@]"
-    | Eop(f, params), e_list ->
-        print_longname ff f;
-	print_call_params ff params;
-        fprintf ff "(@["; print_list ff print_exp "," e_list;
-        fprintf ff ")@]"
+	      print_call_params ff params;
+        print_exps ff e_list;
+	      (match reset with 
+	         | None -> ()
+	         | Some r -> fprintf ff " every %a" print_exp r
+	      )
+   | Efield_update f, [e1;e2] -> 
+	      fprintf ff "(@[";
+	      print_exp ff e1;
+	      fprintf ff " with .";
+	      print_longname ff f;
+	      fprintf ff " = ";
+	      print_exp ff e2;
+	      fprintf ff ")@]"
+    | Earray_op op, e_list ->
+        print_array_op ff op e_list
+
+and print_array_op ff op e_list = 
+  match op, e_list with
     | Erepeat, [e1; e2] ->
-	print_exp ff e1;
-	fprintf ff "^";
-	print_exp ff e2
+	      print_exp ff e1;
+	      fprintf ff "^";
+	      print_exp ff e2
     | Eselect idx_list, [e] -> 
-	print_exp ff e;
-	fprintf ff "[";
-	print_list ff print_size_exp "][" idx_list;
-	fprintf ff "]"
+	      print_exp ff e;
+	      print_list_r print_size_exp "[" "][" "]" ff idx_list
     | Eselect_dyn, e::defe::idx_list ->
-	fprintf ff "@[(";
-	print_exp ff e;
-	fprintf ff "[";
-	print_list ff print_exp "][" idx_list;
-	fprintf ff "] default ";
-	print_exp ff defe;
-	fprintf ff ")@]"
+	      fprintf ff "@[(";
+	      print_exp ff e;
+	      print_list_r print_exp "[" "][" "] default " ff idx_list;
+	      print_exp ff defe;
+	      fprintf ff ")@]"
     | Eupdate idx_list, [e1;e2] ->
-	fprintf ff "(@[";
-	print_exp ff e1;
-	fprintf ff " with [";
-	print_list ff print_size_exp "][" idx_list;
-	fprintf ff "] = ";
-	print_exp ff e2;
-	fprintf ff ")@]"
+	      fprintf ff "(@[";
+	      print_exp ff e1;
+	      fprintf ff " with ";
+	      print_list_r print_size_exp "[" "][" "]" ff idx_list;
+	      fprintf ff " = ";
+	      print_exp ff e2;
+	      fprintf ff ")@]"
     | Eselect_slice, [e; idx1; idx2] ->
-	print_exp ff e;
-	fprintf ff "[";
-	print_exp ff idx1;
-	fprintf ff "..";
-	print_exp ff idx2;
-	fprintf ff "]"	
-    | Eiterator (it, op, params, reset), e::e_list -> 
-	fprintf ff "("; 
-	print_iterator ff it;
-	fprintf ff " ";
-	(match params with
-	   | [] -> print_longname ff op
-	   | l -> 
-	       fprintf ff "(";
-	       print_longname ff op;
-	       print_call_params ff params;
-	       fprintf ff ")"
-	);
-	fprintf ff " <<";
-	print_exp ff e;
-	fprintf ff ">>) (@[";
-	print_list ff print_exp "," e_list;
-	fprintf ff ")@]";
-	(match reset with 
-	   | None -> ()
-	   | Some r -> fprintf ff " every %a" print_exp r
-	)
+	      print_exp ff e;
+	      fprintf ff "[";
+	      print_exp ff idx1;
+	      fprintf ff "..";
+	      print_exp ff idx2;
+	      fprintf ff "]"	
+    | Eiterator (it, { op_name = op; op_params = params } , reset), e::e_list -> 
+	      fprintf ff "("; 
+	      print_iterator ff it;
+	      fprintf ff " ";
+	      (match params with
+	         | [] -> print_longname ff op
+	         | l -> 
+	             fprintf ff "(";
+	             print_longname ff op;
+	             print_call_params ff params;
+	             fprintf ff ")"
+	      );
+	      fprintf ff " <<";
+	      print_exp ff e;
+	      fprintf ff ">>) ";
+	      print_exps ff e_list;
+	      (match reset with 
+	         | None -> ()
+	         | Some r -> fprintf ff " every %a" print_exp r
+	      )
     | Econcat, [e1;e2] -> 
-	fprintf ff "@[";
-	print_exp ff e1;
-	fprintf ff " @@ ";
-	print_exp ff e2;
-	fprintf ff "@]"
-    | Ecopy, [e] -> 
-	fprintf ff "@[copy (";
-	print_exp ff e;
-	fprintf ff ")@]"
-    | Efield_update f, [e1;e2] -> 
-	fprintf ff "(@[";
-	print_exp ff e1;
-	fprintf ff " with .";
-	print_longname ff f;
-	fprintf ff " = ";
-	print_exp ff e2;
-	fprintf ff ")@]"
-    | Eflatten n, e_list ->
-	fprintf ff "@[(flatten ";
-	print_longname ff n;
-	fprintf ff ")(";
-	print_list ff print_exp "," e_list;
-	fprintf ff ")@]"
-    | Emake n, e_list -> 
-	fprintf ff "@[(make ";
-	print_longname ff n;
-	fprintf ff ")(";
-	print_list ff print_exp "," e_list;
-	fprintf ff ")@]"
-    | _ -> assert false
+	      fprintf ff "@[";
+	      print_exp ff e1;
+	      fprintf ff " @@ ";
+	      print_exp ff e2;
+	      fprintf ff "@]"
 
 let rec print_eq ff eq =
   match eq.eq_desc with
@@ -285,19 +185,19 @@ let rec print_eq ff eq =
     | Eautomaton(state_handler_list) ->
         fprintf ff "@[<v>automaton@,";
         fprintf ff "@[<v>";
-        print_list ff print_state_handler "" state_handler_list;
+        print_list print_state_handler ff state_handler_list;
         fprintf ff "@]@,";
         fprintf ff "end@]"
     | Eswitch(e, switch_handler_list) ->
         fprintf ff "@[<v>switch ";
         print_exp ff e;
         fprintf ff "@,@[<v>";
-        print_list ff print_switch_handler "" switch_handler_list;
+        print_list print_switch_handler ff switch_handler_list;
         fprintf ff "@]@,";
         fprintf ff "end@]"
     | Epresent(present_handler_list, b) ->
         fprintf ff "@[<v>present@,";
-        print_list ff print_present_handler "" present_handler_list;
+        print_list print_present_handler ff present_handler_list;
         if b.b_equs <> [] then begin
           fprintf ff "  @[<v 2>default@,";
           print_block ff b;
@@ -326,13 +226,13 @@ and print_state_handler ff
   if until <> [] then
     begin
       fprintf ff "@,@[<v 2>until ";
-      print_list ff print_escape "" until;
+      print_list print_escape ff until;
       fprintf ff "@]"
     end;
   if unless <> [] then
     begin
       fprintf ff "@,@[<v 2>unless ";
-      print_list ff print_escape " " unless;
+      print_list_r print_escape "" " " "" ff unless;
       fprintf ff "@]"
     end;
   fprintf ff "@]"
@@ -361,7 +261,7 @@ and print_block ff { b_local = v_list; b_equs = eqs; b_defnames = defnames } =
   if v_list <> [] then
     begin
       fprintf ff "@[<v 2>var ";
-      print_list ff print_vd ";" v_list;
+      print_list_r print_vd "" ";" "" ff v_list;
       fprintf ff "@]@,"
     end;
   (*   (\* DEBUG *\) *)
@@ -378,17 +278,16 @@ let print_type_def ff { t_name = name; t_desc = tdesc } =
     | Type_abs -> fprintf ff "@[type %s@\n@]" name
     | Type_enum(tag_name_list) ->
         fprintf ff "@[type %s = " name;
-        print_list ff print_name "| " tag_name_list;
+        print_list_r print_name "" "| " "" ff tag_name_list;
         fprintf ff "@\n@]"
     | Type_struct(f_ty_list) ->
         fprintf ff "@[type %s = " name;
-        fprintf ff "@[<v 1>{";
-        print_list ff
-          (fun ff (field, ty) ->
+        print_list_r
+          (fun ff { f_name = field; f_type = ty } ->
              print_name ff field;
              fprintf ff ": ";
-             print_type ff ty) ";" f_ty_list;
-        fprintf ff "}@]@.@]"
+             print_type ff ty) "{" ";" "}" ff f_ty_list;
+        fprintf ff "@.@]"
 
 let print_const_dec ff c =
   fprintf ff "@[const ";
@@ -407,7 +306,7 @@ let print_contract ff {c_local = l;
   if l <> [] then begin
     fprintf ff "@[<v 2>contract@\n";
     fprintf ff "@[<hov 4>var ";
-    print_list ff print_vd ";" l;
+    print_list_r print_vd "" ";" "" ff l;
     fprintf ff ";@]@\n"
   end;
   if eqs <> [] then begin
@@ -418,32 +317,28 @@ let print_contract ff {c_local = l;
   fprintf ff "assume %a@;enforce %a@;with (@[<hov>"
     print_exp e_a
     print_exp e_g;
-  print_list ff print_vd ";" cl;
+  print_list_r print_vd "" ";" "" ff cl;
   fprintf ff "@])@]@\n"
 
 let print_node_params ff = function
   | [] -> ()
-  | l -> 
-      fprintf ff "<<";
-      print_list ff print_name "," l;
-      fprintf ff ">>"
+  | l -> print_list_r print_name "<<" "," ">>" ff l
 
 let print_node ff
-    { n_name = n; n_statefull = statefull; n_input = ni;
+    { n_name = n; n_input = ni;
       n_local = nl; n_output = no; n_contract = contract; n_equs = ne;
       n_params = params; } =
-  fprintf ff "@[<v 2>%s " (if statefull then "node" else "fun");
+  fprintf ff "@[<v 2>node ";
   print_name ff n; 
   print_node_params ff params;
-  fprintf ff "(@[";
-  print_list ff print_vd ";" ni;
-  fprintf ff "@]) returns (@[";
-  print_list ff print_vd ";" no;
-  fprintf ff "@])@,";
+  print_list_r print_vd "(" ";" ")" ff ni;
+  fprintf ff " returns ";
+  print_list_r print_vd "(" ";" ")" ff no;
+  fprintf ff "@,";
   optunit (print_contract ff) contract;
   if nl <> [] then begin
     fprintf ff "@[<hov 4>var ";
-    print_list ff print_vd ";" nl;
+    print_list_r print_vd "" ";" "" ff nl;
     fprintf ff ";@]@,"
   end;
   fprintf ff "@[<v 2>let @,";
@@ -457,7 +352,7 @@ let print_open_module ff name =
 
 let ptype oc ty =
   let ff = formatter_of_out_channel oc in
-  print_type ff ty; fprintf ff "@?"
+    print_type ff ty; fprintf ff "@?"
 
 let print oc { p_opened = po; p_types = pt; p_nodes = pn; p_consts = pc } =
   let ff = formatter_of_out_channel oc in