diff --git a/global/ident.ml b/global/ident.ml
index 6982642..157af1d 100644
--- a/global/ident.ml
+++ b/global/ident.ml
@@ -79,3 +79,5 @@ module IdentSet = struct
     Format.fprintf ff "}@]";
 end
 
+
+let print_ident ff id = fprintf ff "%s" (name id)
diff --git a/global/ident.mli b/global/ident.mli
index b691327..3c5ab8f 100644
--- a/global/ident.mli
+++ b/global/ident.mli
@@ -37,3 +37,6 @@ sig
   include (Set.S with type elt = ident)
   val fprint_t : Format.formatter -> t -> unit
 end
+
+
+val print_ident : Format.formatter -> ident -> unit
diff --git a/global/names.ml b/global/names.ml
index 253bd0f..03cc7fc 100644
--- a/global/names.ml
+++ b/global/names.ml
@@ -41,4 +41,30 @@ let mk_longname s =
     Modname { qual = String.sub s 0 ind; id = id; }
   with Not_found -> Name s
 
-let print_longname ff id = Format.fprintf ff "%s" (fullname id)
+(** Are infix
+  [or], [quo], [mod], [land], [lor], [lxor], [lsl], [lsr], [asr]
+  and every names not beginning with 'a' .. 'z' | 'A' .. 'Z' | '_' | '`'*)
+let is_infix s =
+  let module StrSet = Set.Make(String) in
+  let infix_set =
+    List.fold_right StrSet.add
+      ["or"; "quo"; "mod"; "land"; "lor"; "lxor"; "lsl"; "lsr"; "asr"]
+      StrSet.empty in
+  if StrSet.mem s infix_set then true
+  else (match String.get s 0 with
+        | 'a' .. 'z' | 'A' .. 'Z' | '_' | '`' -> false
+        | _ -> true)
+
+let print_name ff n =
+  let n = if is_infix n
+    then "( " ^ (n ^ " )") (* do not remove the space around n, since for example "(*" would create bugs *)
+    else n
+  in Format.fprintf ff "%s" n
+  
+let print_longname ff n =
+  match n with
+  | Name m -> print_name ff m
+  | Modname { qual = "Pervasives"; id = m } -> print_name ff m
+  | Modname { qual = m1; id = m2 } -> (Format.fprintf ff "%s." m1; print_name ff m2)
+
+
diff --git a/global/static.ml b/global/static.ml
index 04da672..8366eb1 100644
--- a/global/static.ml
+++ b/global/static.ml
@@ -130,32 +130,14 @@ let rec print_size_exp ff =
   | SConst i -> fprintf ff "%d" i
   | SVar id -> fprintf ff "%s" id
   | SOp (op, e1, e2) ->
-      (fprintf ff "@[(";
-       print_size_exp ff e1;
-       fprintf ff " %s " (op_to_string op);
-       print_size_exp ff e2;
-       fprintf ff ")@]")
+      fprintf ff "@[(%a %s %a@]"
+        print_size_exp e1 (op_to_string op) print_size_exp e2
   
-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)
-  
-let print_size_constr ff =
-  function
+let print_size_constr ff = function
   | Equal (e1, e2) ->
-      (fprintf ff "@[";
-       print_size_exp ff e1;
-       fprintf ff " = ";
-       print_size_exp ff e2;
-       fprintf ff "@]")
+      fprintf ff "@[%a = %a@]" print_size_exp e1 print_size_exp e2
   | LEqual (e1, e2) ->
-      (fprintf ff "@[";
-       print_size_exp ff e1;
-       fprintf ff " <= ";
-       print_size_exp ff e2;
-       fprintf ff "@]")
+      fprintf ff "@[%a <= %a@]" print_size_exp e1 print_size_exp e2
   | False -> fprintf ff "False"
   
 let psize_constr oc c =
diff --git a/global/types.ml b/global/types.ml
index 952d294..fcceceb 100644
--- a/global/types.ml
+++ b/global/types.ml
@@ -15,3 +15,15 @@ type ty =
 let invalid_type = Tprod []
 
 let const_array_of ty n = Tarray (ty, SConst n)
+
+
+
+open Pp_tools
+open Format
+
+let rec print_type ff = function
+  | Tprod ty_list ->
+      fprintf ff "@[<hov2>%a@]" (print_list_r print_type "(" " *" ")") ty_list
+  | Tid id -> print_longname ff id
+  | Tarray (ty, n) ->
+      fprintf ff "@[<hov2>%a^%a@]" print_type ty print_size_exp n
\ No newline at end of file
diff --git a/minils/minils.ml b/minils/minils.ml
index a86fea8..bc1f1c9 100644
--- a/minils/minils.ml
+++ b/minils/minils.ml
@@ -65,7 +65,7 @@ and array_op =
   | Eupdate of size_exp list * exp * exp (*indices, array, value*)
   | Eselect_slice of size_exp * size_exp * exp (*lower bound, upper bound, array*)
   | Econcat of exp * exp
-  | Eiterator of iterator_name * longname * size_exp list * size_exp * exp list * ident option
+  | Eiterator of iterator_type * longname * size_exp list * size_exp * exp list * ident option
    
 and op_desc = { op_name: longname; op_params: size_exp list; op_kind: op_kind }
 and op_kind = | Eop | Enode
@@ -135,6 +135,8 @@ type program =
       p_nodes  : node_dec list;
       p_consts : const_dec list; }
 
+
+
 (*Helper functions to build the AST*)
 
 
@@ -151,38 +153,35 @@ let rec size_exp_of_exp e =
 	    SOp(sop, size_exp_of_exp e1, size_exp_of_exp e2)
   | _ -> raise Not_static
 
-(*Returns the list of bounds of an array type*)
+(** @return the list of bounds of an array type*)
 let rec bounds_list ty = 
   match ty with
     | Tarray(ty, n) -> n::(bounds_list ty)
     | _ -> []
 
-(** Returns the var_dec object corresponding to the name n
-    in a list of var_dec. *)
+(** @return the [var_dec] object corresponding to the name [n]
+    in a list of [var_dec]. *)
 let rec vd_find n = function
   | [] -> Format.printf "Not found var %s\n" (name n); raise Not_found
   | vd::l -> 
       if vd.v_name = n then vd else vd_find n l
 
-(** Returns whether an object of name n belongs to 
-    a list of var_dec. *)
+(** @return whether an object of name [n] belongs to 
+    a list of [var_dec]. *)
 let rec vd_mem n = function
   | [] -> false
   | vd::l -> vd.v_name = n or (vd_mem n l)
 
-(** [is_record_type ty] returns whether ty corresponds to a record type. *)
-let is_record_type ty =
-  match ty with
-    | Tid n ->
-	(try
-	   ignore (Modules.find_struct n);
-	   true
-	 with 
-	     Not_found -> false
-	)
-    | _ -> false
-
+(** @return whether [ty] corresponds to a record type. *)
+let is_record_type ty = match ty with
+  | Tid n ->
+	    (try
+	       ignore (Modules.find_struct n); true
+	     with 
+	     Not_found -> false)
+  | _ -> false
 
+(*
 module Vars =
 struct
   let rec vars_pat acc = function
@@ -316,7 +315,8 @@ struct
       | Ereset_mem (y, _, _) -> [y]
       | _ -> []
 end
-
+*)
+(*
 (* data-flow dependences. pre-dependences are discarded *)
 module DataFlowDep = Make
   (struct
@@ -338,382 +338,5 @@ module AllDep = Make
      let def = Vars.def
      let antidep eq = false
    end)
+*)
 
-module Printer =
-struct
-  open Format
-
-  let is_infix =
-    let module StrSet = Set.Make(String) in
-    let set_infix = StrSet.singleton "or" in
-    fun s ->
-      if (StrSet.mem s set_infix) then true
-      else begin
-        match (String.get s 0) with
-          | 'a' .. 'z' | 'A' .. 'Z' | '_' | '`' -> false
-          | _ -> true
-      end
-
-  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
-
-  let print_name ff n =
-    let n = if is_infix n then
-      match n with
-        | "*" -> "( * )"
-        | _ -> "(" ^ n ^ ")"
-    else n
-    in fprintf ff "%s" n
-
-  let print_longname ff n =
-    match n 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 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"
-    | Tfloat -> fprintf ff  "float"
-    | Tid(id) -> print_longname ff id
-    | Tarray(ty, n) -> 
-	print_type ff ty;
-	fprintf ff "^";
-	print_size_exp ff n
-
-  let rec print_type ff = function
-    | Tbase(ty) -> print_type ff ty
-    | Tprod(ty_list) ->
-        fprintf ff "@[(";
-        print_list ff print_type " *" ty_list;
-        fprintf ff ")@]"
-
-  let rec print_ck ff = function
-    | Cbase -> fprintf ff "base"
-    | Con(ck, c, n) ->
-        print_ck ff ck; fprintf ff " on ";
-        print_longname ff c; fprintf ff "(";
-        print_ident ff n; fprintf ff ")"
-    | Cvar { contents = Cindex n } -> fprintf ff "base"
-    | Cvar { contents = Clink ck } -> print_ck ff ck
-
-  let rec print_clock ff = function
-    | Ck(ck) -> print_ck ff ck
-    | Cprod(ct_list) ->
-        fprintf ff "@[(";
-        print_list ff print_clock " *" ct_list;
-        fprintf ff ")@]"
-
-  let print_vd ff { v_name = n; v_type = ty; v_clock = ck } =
-    fprintf ff "@[<v>";
-    print_ident ff n;
-    fprintf ff ":";
-    print_type ff ty;
-    fprintf ff " at ";
-    print_ck ff ck;
-    fprintf ff "@]"
-
-  let rec print_c ff = function
-    | Cint i -> fprintf ff "%d" i
-    | Cfloat f -> fprintf ff "%f" f
-    | Cconstr(tag) -> print_longname ff tag
-    | Carray (n, c) ->
-	print_c ff c;
-	fprintf ff "^";
-	print_size_exp ff n
-
-  let print_call_params ff = function
-    | [] -> ()
-    | l -> 
-	fprintf ff "<<";
-	print_list ff print_size_exp "," l;
-	fprintf ff ">>"
-
-  let rec print_exps ff e_list =
-    fprintf ff "@[(";print_list ff print_exp "," e_list; fprintf ff ")@]"
-
-  and print_exp ff e =
-    if !Misc.full_type_info then fprintf ff "(";
-    begin match e.e_desc with
-      | Evar x -> print_ident ff x
-      | Econstvar x -> print_name ff x
-      | Econst c -> print_c ff c
-      | Efby(Some(c), e) ->
-          print_c ff c; fprintf ff " fby "; print_exp ff e
-      | Ereset_mem(y,v,res) ->
-	  fprintf ff "@[reset_mem ";
-	  print_ident ff y;
-	  fprintf ff " = ";
-	  print_c ff v;
-	  fprintf ff " every ";
-	  print_ident ff res;
-	  fprintf ff "@]"
-      | Efby(None, e) ->
-          fprintf ff "pre "; print_exp ff e
-      | Eop((Name(m) | Modname { qual = "Pervasives"; id = m }), params, [e1;e2])
-          when is_infix m ->
-          fprintf ff "(%a %s %a %a)"
-            print_exp e1
-            m
-	    print_call_params params
-            print_exp e2
-      | Eop(op, params, e_list) ->
-          print_longname ff op;
-	  print_call_params ff params;
-          print_exps ff e_list
-      | Eapp({ a_op = f }, params, e_list) ->
-          print_longname ff f;
-	  print_call_params ff params;
-          print_exps ff e_list
-      | Eevery({ a_op = f }, params, e_list, x) ->
-          print_longname ff f;
-	  print_call_params ff params;
-          print_exps ff e_list;
-          fprintf ff " every "; print_ident ff x
-      | Ewhen(e, c, n) ->
-          fprintf ff "(";
-          print_exp ff e;
-          fprintf ff " when ";
-          print_longname ff c; fprintf ff "(";
-          print_ident ff n; fprintf ff ")";
-          fprintf ff ")"
-      | Eifthenelse(e1, e2, e3) ->
-          fprintf ff "@[if ";print_exp ff e1;
-          fprintf ff "@ then ";
-          print_exp ff e2;
-          fprintf ff "@ else ";
-          print_exp ff e3;
-          fprintf ff "@]"
-      | Emerge(x, tag_e_list) ->
-          fprintf ff "@[<hov 2>merge ";print_ident ff x;fprintf ff "@ ";
-          fprintf ff "@[";
-          print_tag_e_list ff tag_e_list;
-          fprintf ff "@]@]"
-      | Etuple(e_list) ->
-          fprintf ff "@[(";
-          print_list ff print_exp "," e_list;
-          fprintf ff ")@]"
-      | Efield(e, field) ->
-          print_exp ff e;
-          fprintf ff ".";
-          print_longname ff field
-      | Estruct(f_e_list) ->
-          fprintf ff "@[<v 1>{";
-          print_list ff
-            (fun ff (field, e) -> print_longname ff field;fprintf ff " = ";
-               print_exp ff e)
-            ";" f_e_list;
-          fprintf ff "}@]"
-    (*Array operators*)
-      | Earray e_list -> 
-	  fprintf ff "@[[";
-          print_list ff print_exp ";" e_list;
-          fprintf ff "]@]"
-      | Erepeat (n,e) -> 
-	  print_exp ff e;
-	  fprintf ff "^";
-          print_size_exp ff n
-      | Eselect (idx,e) -> 
-	  print_exp ff e;
-	  fprintf ff "[";
-          print_list ff print_size_exp "][" idx;
-          fprintf ff "]" 
-      | Eselect_dyn (idx, _, e1, e2) ->
-	  fprintf ff "@[";
-	  print_exp ff e1;
-	  fprintf ff "[";
-          print_list ff print_exp "][" idx;
-	  fprintf ff "] default ";
-	  print_exp ff e2;
-	    fprintf ff "@]"
-      | Eupdate (idx, e1, e2) ->
-	  fprintf ff "@[";
-	  print_exp ff e1;
-          fprintf ff " with [";
-	  print_list ff print_size_exp "][" idx;
-	  fprintf ff "] = ";
-	  print_exp ff e2;
-	  fprintf ff "@]"
-      | Eselect_slice (idx1, idx2, e) -> 
-	  print_exp ff e;
-          fprintf ff "[";
-	  print_size_exp ff idx1;
-	  fprintf ff "..";
-	  print_size_exp ff idx2;
-	  fprintf ff "]"
-      | Econcat (e1, e2) ->
-	  print_exp ff e1;
-	  fprintf ff " @@ ";
-	  print_exp ff e2
-      | Eiterator (it, f, params, n, e_list, reset) -> 
-	  fprintf ff "("; 
-	  fprintf ff "%s" (iterator_to_string it);
-	  fprintf ff " ";
-	  (match params with
-	     | [] -> print_longname ff f
-	     | l -> 
-		 fprintf ff "(";
-		 print_longname ff f;
-		 print_call_params ff params;
-		 fprintf ff ")"
-	  );
-	  fprintf ff " <<";
-	  print_size_exp ff n;
-	  fprintf ff ">>) (@[";
-	  print_list ff print_exp "," e_list;
-	  fprintf ff ")@]";
-	  (match reset with 
-	     | None -> ()
-	     | Some r -> fprintf ff " every %s" (name 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 "@]"
-    end;
-    if !Misc.full_type_info
-    then begin
-      fprintf ff " : %a)" print_type e.e_ty;
-      if e.e_loc = no_location then fprintf ff " (no loc)"
-    end
-  and print_tag_e_list ff tag_e_list =
-    print_list ff
-      (fun ff (tag, e) ->
-         fprintf ff "@[(";
-         print_longname ff tag;
-         fprintf ff " -> ";
-         print_exp ff e;
-         fprintf ff ")@]@,") ""
-      tag_e_list
-
-  let print_eq ff { eq_lhs = p; eq_rhs = e } =
-    fprintf ff "@[<hov 2>";
-    print_pat ff p;
-    (*     (\* DEBUG *\) *)
-    (*     fprintf ff " : "; *)
-    (*     print_ck ff e.e_ck; *)
-    (*     (\* END DEBUG *\) *)
-    fprintf ff " =@ ";
-    print_exp ff e;
-    if !Misc.full_type_info
-    then begin fprintf ff "@ at "; print_ck ff e.e_ck end;
-    fprintf ff ";@]"
-
-  let print_eqs ff l =
-    fprintf ff "@[<v>"; print_list ff print_eq "" l; fprintf ff "@]"
-
-  let print_open_module ff name =
-    fprintf ff "@[open ";
-    print_name ff name;
-    fprintf ff "@.@]"
-
-  let print_type_def ff { t_name = name; t_desc = tdesc } =
-    match tdesc with
-      | 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;
-          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_name ff field;
-               fprintf ff ": ";
-               print_type ff ty) ";" f_ty_list;
-          fprintf ff "}@]@\n@]"
-
-  let print_contract ff {c_local = l;
-                         c_eq = eqs;
-                         c_assume = e_a;
-                         c_enforce = e_g;
-                         c_controllables = cl } =
-    if l <> [] then begin
-      fprintf ff "contract\n";
-      fprintf ff "@[<hov 4>var ";
-      print_list ff print_vd ";" l;
-      fprintf ff ";@]\n"
-    end;
-    if eqs <> [] then begin
-      fprintf ff "@[<v 2>let @,";
-      print_eqs ff eqs;
-      fprintf ff "@]"; fprintf ff "tel\n"
-    end;
-    fprintf ff "assume@ %a@;enforce@ %a with ("
-      print_exp e_a
-      print_exp e_g;
-    print_list ff print_vd ";" cl;
-    fprintf ff ")"
-
-  let print_node_params ff = function
-    | [] -> ()
-    | l -> 
-	fprintf ff "<<";
-	print_list ff print_name "," l;
-	fprintf ff ">>"
-
-  let print_node ff
-      { n_name = n;n_input = ni;n_output = no;
-        n_contract = contract;
-        n_local = nl; n_equs = ne;
-	n_params = params; } =
-    fprintf ff "@[<v 2>node %s" 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 "@])@,";
-    optunit (print_contract ff) contract;
-    if nl <> [] then begin
-      fprintf ff "@[<hov 2>var ";
-      print_list ff print_vd ";" nl;
-      fprintf ff ";@]@,"
-    end;
-    fprintf ff "@[<v 2>let @,";
-    print_eqs ff ne;
-    fprintf ff "@]@;"; fprintf ff "tel";fprintf ff "@.@]"
-
-  let print_exp oc e =
-    let ff = formatter_of_out_channel oc in
-    print_exp ff e;
-    fprintf ff "@."
-
-  let print_type oc ty =
-    let ff = formatter_of_out_channel oc in
-    print_type ff ty;
-    fprintf ff "@?"
-
-  let print_clock oc ct =
-    let ff = formatter_of_out_channel oc in
-    print_clock ff ct;
-    fprintf ff "@?"
-
-  let print oc { p_opened = pm; p_types = pt; p_nodes = pn } =
-    let ff = formatter_of_out_channel oc in
-    List.iter (print_open_module ff) pm;
-    List.iter (print_type_def ff) pt;
-    List.iter (print_node ff) pn;
-    fprintf ff "@?"
-end
diff --git a/minils/minils_printer.ml b/minils/minils_printer.ml
new file mode 100644
index 0000000..92ea09a
--- /dev/null
+++ b/minils/minils_printer.ml
@@ -0,0 +1,268 @@
+open Minils
+open Names
+open Ident
+open Types
+open Static
+open Format
+open Pp_tools
+
+
+let rec print_pat ff = function
+  | Evarpat n -> print_ident ff n
+  | Etuplepat pat_list ->
+      fprintf ff "@[%a@]" (print_list_r print_pat "("","")") pat_list
+
+let rec print_ck ff = function
+  | Cbase -> fprintf ff "base"
+  | Con (ck, c, n) ->
+      fprintf ff "%a on %a(%a)" print_ck ck print_longname c print_ident n
+  | Cvar { contents = Cindex n } -> fprintf ff "base"
+  | Cvar { contents = Clink ck } -> print_ck ff ck
+
+let rec print_clock ff = function
+  | Ck ck -> print_ck ff ck
+  | Cprod ct_list ->
+      fprintf ff "@[%a@]" (print_list_r print_clock "("" *"")") ct_list
+
+let print_vd ff { v_name = n; v_type = ty; v_clock = ck } =
+  fprintf ff "@[<v>%a : %a at %a@]" print_ident n print_type ty print_ck ck
+  
+let rec print_c ff = function
+  | Cint i -> fprintf ff "%d" i
+  | Cfloat f -> fprintf ff "%f" f
+  | Cconstr tag -> print_longname ff tag
+  | Carray (n, c) -> fprintf ff "@[%a^%a@]" print_c c print_size_exp n
+
+let print_params ff = function
+  | [] -> ()
+  | l -> print_list_r print_size_exp "<<"","">>" ff l
+
+let rec print_args ff e_list =
+  fprintf ff "@[%a@]" (print_list_r print_exp "("","")") e_list
+
+and print_op ff op =
+  fprintf ff "%a %a" print_longname op.op_name print_params op.op_params
+  
+and print_exp ff e =
+  (if !Misc.full_type_info then fprintf ff "(" else ();
+    (match e.e_desc with
+      | Evar x -> print_ident ff x
+      | Econstvar x -> print_name ff x
+      | Econst c -> print_c ff c
+      | Efby ((Some c), e) ->
+          (print_c ff c; fprintf ff " fby "; print_exp ff e)
+      | Efby (None, e) -> (fprintf ff "pre "; print_exp ff e)
+      | Ecall (op, args, reset) ->
+          fprintf ff "%a %a every %a" print_op op print_args args print_ident x
+      | Ewhen (e, c, n) ->
+          fprintf ff "@[(%a when %a(%a))@]"
+            print_exp e print_longname c print_ident n
+      | Eifthenelse (e1, e2, e3) ->
+          fprintf ff "@[if %a@ then %a@ else @]"
+            print_exp e1 print_exp e2 print_exp e3
+      | Emerge (x, tag_e_list) ->
+          fprintf ff "@[<hov2>merge %a@ @[%a@]@]"
+            print_ident x print_tag_e_list tag_e_list
+      | Etuple e_list -> (*TODO*)
+          (fprintf ff "@[(";
+            print_list ff print_exp "," e_list;
+            fprintf ff ")@]")
+      | Efield (e, field) ->
+          (print_exp ff e; fprintf ff "."; print_longname ff field)
+      | Estruct f_e_list ->
+          (fprintf ff "@[<v 1>{";
+            print_list ff
+              (fun ff (field, e) ->
+                    (print_longname ff field; fprintf ff " = "; print_exp ff e))
+              ";" f_e_list;
+            fprintf ff "}@]")
+      | (*Array operators*) Earray e_list ->
+          (fprintf ff "@[[";
+            print_list ff print_exp ";" e_list;
+            fprintf ff "]@]")
+      | Erepeat (n, e) -> (print_exp ff e; fprintf ff "^"; print_size_exp ff n)
+      | Eselect (idx, e) ->
+          (print_exp ff e;
+            fprintf ff "[";
+            print_list ff print_size_exp "][" idx;
+            fprintf ff "]")
+      | Eselect_dyn (idx, _, e1, e2) ->
+          (fprintf ff "@[";
+            print_exp ff e1;
+            fprintf ff "[";
+            print_list ff print_exp "][" idx;
+            fprintf ff "] default ";
+            print_exp ff e2;
+            fprintf ff "@]")
+      | Eupdate (idx, e1, e2) ->
+          (fprintf ff "@[";
+            print_exp ff e1;
+            fprintf ff " with [";
+            print_list ff print_size_exp "][" idx;
+            fprintf ff "] = ";
+            print_exp ff e2;
+            fprintf ff "@]")
+      | Eselect_slice (idx1, idx2, e) ->
+          (print_exp ff e;
+            fprintf ff "[";
+            print_size_exp ff idx1;
+            fprintf ff "..";
+            print_size_exp ff idx2;
+            fprintf ff "]")
+      | Econcat (e1, e2) ->
+          (print_exp ff e1; fprintf ff " @@ "; print_exp ff e2)
+      | Eiterator (it, f, params, n, e_list, reset) ->
+          (fprintf ff "(";
+            fprintf ff "%s" (iterator_to_string it);
+            fprintf ff " ";
+            (match params with
+              | [] -> print_longname ff f
+              | l ->
+                  (fprintf ff "(";
+                    print_longname ff f;
+                    print_call_params ff params;
+                    fprintf ff ")"));
+            fprintf ff " <<";
+            print_size_exp ff n;
+            fprintf ff ">>) (@[";
+            print_list ff print_exp "," e_list;
+            fprintf ff ")@]";
+            (match reset with
+              | None -> ()
+              | Some r -> fprintf ff " every %s" (name 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 "@]"));
+    if !Misc.full_type_info
+    then
+      (fprintf ff " : %a)" print_type e.e_ty;
+        if e.e_loc = no_location then fprintf ff " (no loc)" else ())
+    else ())
+
+and print_tag_e_list ff tag_e_list =
+  print_list ff
+    (fun ff (tag, e) ->
+          (fprintf ff "@[(";
+            print_longname ff tag;
+            fprintf ff " -> ";
+            print_exp ff e;
+            fprintf ff ")@]@,"))
+    "" tag_e_list
+
+let print_eq ff { eq_lhs = p; eq_rhs = e } = (*     (\* DEBUG *\) *)
+  (*     fprintf ff " : "; *) (*     print_ck ff e.e_ck; *)
+  (*     (\* END DEBUG *\) *)
+  (fprintf ff "@[<hov 2>";
+    print_pat ff p;
+    fprintf ff " =@ ";
+    print_exp ff e;
+    if !Misc.full_type_info
+    then (fprintf ff "@ at "; print_ck ff e.e_ck)
+    else ();
+    fprintf ff ";@]")
+
+let print_eqs ff l =
+  (fprintf ff "@[<v>"; print_list ff print_eq "" l; fprintf ff "@]")
+
+let print_open_module ff name =
+  (fprintf ff "@[open "; print_name ff name; fprintf ff "@.@]")
+
+let print_type_def ff { t_name = name; t_desc = tdesc } =
+  match tdesc with
+  | 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;
+        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_name ff field; fprintf ff ": "; print_type ff ty))
+          ";" f_ty_list;
+        fprintf ff "}@]@\n@]")
+
+let print_contract ff
+    {
+      c_local = l;
+      c_eq = eqs;
+      c_assume = e_a;
+      c_enforce = e_g;
+      c_controllables = cl
+    } =
+  (if l <> []
+    then
+      (fprintf ff "contract\n";
+        fprintf ff "@[<hov 4>var ";
+        print_list ff print_vd ";" l;
+        fprintf ff ";@]\n")
+    else ();
+    if eqs <> []
+    then
+      (fprintf ff "@[<v 2>let @,";
+        print_eqs ff eqs;
+        fprintf ff "@]";
+        fprintf ff "tel\n")
+    else ();
+    fprintf ff "assume@ %a@;enforce@ %a with (" print_exp e_a print_exp e_g;
+    print_list ff print_vd ";" cl;
+    fprintf ff ")")
+
+let print_node_params ff =
+  function
+  | [] -> ()
+  | l -> (fprintf ff "<<"; print_list ff print_name "," l; fprintf ff ">>")
+
+let print_node ff
+    {
+      n_name = n;
+      n_input = ni;
+      n_output = no;
+      n_contract = contract;
+      n_local = nl;
+      n_equs = ne;
+      n_params = params
+    } =
+  (fprintf ff "@[<v 2>node %s" 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 "@])@,";
+    optunit (print_contract ff) contract;
+    if nl <> []
+    then
+      (fprintf ff "@[<hov 2>var ";
+        print_list ff print_vd ";" nl;
+        fprintf ff ";@]@,")
+    else ();
+    fprintf ff "@[<v 2>let @,";
+    print_eqs ff ne;
+    fprintf ff "@]@;";
+    fprintf ff "tel";
+    fprintf ff "@.@]")
+
+let print_exp oc e =
+  let ff = formatter_of_out_channel oc in (print_exp ff e; fprintf ff "@.")
+
+let print_type oc ty =
+  let ff = formatter_of_out_channel oc in (print_type ff ty; fprintf ff "@?")
+
+let print_clock oc ct =
+  let ff = formatter_of_out_channel oc
+  in (print_clock ff ct; fprintf ff "@?")
+
+let print oc { p_opened = pm; p_types = pt; p_nodes = pn } =
+  let ff = formatter_of_out_channel oc
+  in
+  (List.iter (print_open_module ff) pm;
+    List.iter (print_type_def ff) pt;
+    List.iter (print_node ff) pn;
+    fprintf ff "@?")
diff --git a/utilities/pp_tools.ml b/utilities/pp_tools.ml
new file mode 100644
index 0000000..6681799
--- /dev/null
+++ b/utilities/pp_tools.ml
@@ -0,0 +1,107 @@
+(**************************************************************************)
+(*                                                                        *)
+(*  Lucid Synchrone V4                                                    *)
+(*  Copyright (C) 2008 Marc Pouzet                                        *)
+(*  Organization : LRI, University of Paris-Sud, Orsay                    *)
+(*                                                                        *)
+(**************************************************************************)
+(* useful stuff for printing *)
+(* $Id: pp_tools.ml,v 1.12.4.1 2009-07-12 09:40:19 gerard Exp $ *)
+
+open Format
+
+let rec print_list print ff = function
+  | [] -> ()
+  | x::l ->
+    fprintf ff "@[<hv2>%a@]" print x;
+    List.iter (fprintf ff "@ @[<hv2>%a@]" print) l
+
+(** print the list x1...xn : \@\[[lp][x1][sep] [x2]...[sep] [xn][rp]\]\@
+    and nothing if the list is empty *)
+let rec print_list_r print lp sep rp ff = function
+  | [] -> ()
+  | x :: l ->
+      fprintf ff "@[<hv2>%s%a" lp print x;
+      List.iter (fprintf ff "%s@]@ @[<hv2>%a" sep print) l;
+      fprintf ff "%s@]" rp 
+
+(** print the list x1...xn : \@\[[lp][x1] [sep][x2]... [sep][xn][rp]\]\@
+    and nothing if the list is empty *)
+let rec print_list_l print lp sep rp ff = function
+  | [] -> ()
+  | x :: l ->
+      fprintf ff "@[<hv2>%s%a" lp print x;
+      List.iter (fprintf ff "@]@ @[<hv2>%s%a" sep print) l;
+      fprintf ff "%s@]" rp 
+(*
+let rec print_list_rb print lp sep rp ff = function
+  | [] -> ()
+  | x :: l ->
+      fprintf ff "@[<2>%s%a" lp print x;
+      List.iter (fprintf ff "%s@]@ @[<2>%a" sep print) l;
+      fprintf ff "%s@]" rp 
+
+let rec print_list_lb print lp sep rp ff = function
+  | [] -> ()
+  | x :: l ->
+      fprintf ff "@[<2>%s%a@]" lp print x;
+      List.iter (fprintf ff "@]@ @[<2>%s%a" sep print) l;
+      fprintf ff "%s@]" rp 
+*)
+let print_couple print1 print2 lp sep rp ff (c1, c2) =
+  fprintf ff "%s%a%s@ %a%s" lp print1 c1 sep print2 c2 rp 
+
+let print_couple2 print1 print2 lp sep1 sep2 rp ff (c1, c2) =
+  fprintf ff "%s%a%s@ %s%a%s" lp print1 c1 sep1 sep2 print2 c2 rp 
+
+let print_opt print ff = function
+  | None -> ()
+  | Some(s) -> print ff s
+
+let print_opt_magic print ff = function
+  | None -> pp_print_string ff "Obj.magic ()"
+  | Some(e) -> print ff e
+
+
+let print_opt2 print sep ff = function
+  | None -> ()
+  | Some(s) -> fprintf ff "%s%a" sep print s
+
+let print_record print ff r =
+  fprintf ff "@[<hv2>%a@]" (print_list_r print "{ "";"" }") r
+
+let print_type_params ff pl =
+  print_list_r (fun ff s -> fprintf ff "'%s" s) "("","") " ff pl
+
+
+(* Map and Set redefinition to allow pretty printing
+
+module type P = sig
+        type t
+        val fprint : Format.formatter -> t -> unit
+end
+
+module type ELT = sig
+        type t
+        val compare : t -> t -> int
+        val fprint : Format.formatter -> t -> unit
+end
+
+module SetMake (Elt : ELT) = struct
+        module M = Set.Make(Elt)
+        include M
+        let fprint ff es =
+                Format.fprintf ff "@[<hov>{@ ";
+                iter (fun e -> Format.fprintf ff "%a@ " Elt.fprint e) es;
+                Format.fprintf ff "}@]";
+end
+
+module MapMake (Key : ELT) (Elt : P) = struct
+        module M = Map.Make(Key)
+        include M
+        let fprint prp  eem =
+                Format.fprintf prp  "[@[<hv 2>";
+                iter (fun k m -> Format.fprintf prp  "@ | %a -> %a" Key.fprint k Elt.fprint m) eem;
+                Format.fprintf prp  "@]@ ]";
+end
+*)