From 90cc3b8efa5d8172e29ce1e2473970cd019c975f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?L=C3=A9lio=20Brun?= <lelio.brun@isae-supaero.fr>
Date: Fri, 19 Feb 2021 11:19:21 +0100
Subject: [PATCH] some rewriting in C backend pretty-printer

---
 src/backends/C/c_backend.ml        |    8 +-
 src/backends/C/c_backend_common.ml |  731 ++++++-------
 src/backends/C/c_backend_header.ml |  826 ++++++++-------
 src/backends/C/c_backend_lusic.ml  |   23 +-
 src/backends/C/c_backend_main.ml   |  544 ++++++----
 src/backends/C/c_backend_src.ml    | 1561 ++++++++++++++++------------
 src/lusic.ml                       |   28 +-
 src/options_management.ml          |    9 +-
 src/plugins/mpfr/lustrec_mpfr.ml   |   10 +-
 src/utils/utils.ml                 |   81 +-
 10 files changed, 2094 insertions(+), 1727 deletions(-)

diff --git a/src/backends/C/c_backend.ml b/src/backends/C/c_backend.ml
index 12df980e..f964092b 100644
--- a/src/backends/C/c_backend.ml
+++ b/src/backends/C/c_backend.ml
@@ -9,7 +9,7 @@
 (*                                                                  *)
 (********************************************************************)
 
-open Format
+open Utils.Format
 open C_backend_mauve
 (******************************************************************************)
 (*                        Translation function                                *)
@@ -26,12 +26,6 @@ let makefile_opt print basename dependencies makefile_fmt machines =
   )
 *)
 
-let with_out_file file f =
-  let oc = open_out file in
-  let fmt = formatter_of_out_channel oc in
-  f fmt;
-  close_out oc
-
 let c_or_cpp f =
   if !Options.cpp then f ^ ".cpp" else f ^ ".c" (* Could be changed *)
 
diff --git a/src/backends/C/c_backend_common.ml b/src/backends/C/c_backend_common.ml
index d465ceee..0b19d196 100644
--- a/src/backends/C/c_backend_common.ml
+++ b/src/backends/C/c_backend_common.ml
@@ -9,16 +9,21 @@
 (*                                                                  *)
 (********************************************************************)
 
-open Format
+open Utils.Format
 open Lustre_types
 open Corelang
 open Machine_code_types
 (*open Machine_code_common*)
 module Mpfr = Lustrec_mpfr
 
-let print_version fmt =
-  Format.fprintf fmt 
-    "/* @[<v>C code generated by %s@,Version number %s@,Code is %s compliant@,Using %s numbers */@,@]@."
+let pp_print_version fmt () =
+  fprintf fmt
+    "/* @[<v>\
+     C code generated by %s@,\
+     Version number %s@,\
+     Code is %s compliant@,\
+     Using %s numbers */@,\
+     @]"
     (Filename.basename Sys.executable_name) 
     Version.number 
     (if !Options.ansi then "ANSI C90" else "C99")
@@ -32,27 +37,33 @@ let file_to_module_name basename =
   let baseNAME = protect_filename baseNAME in
   baseNAME
 
+let var_is name v =
+  v.var_id = name
+
 (* Generation of a non-clashing name for the self memory variable (for step and reset functions) *)
 let mk_self m =
   let used name =
-       (List.exists (fun v -> v.var_id = name) m.mstep.step_inputs)
-    || (List.exists (fun v -> v.var_id = name) m.mstep.step_outputs)
-    || (List.exists (fun v -> v.var_id = name) m.mstep.step_locals)
-    || (List.exists (fun v -> v.var_id = name) m.mmemory) in
+    let open List in
+    exists (var_is name) m.mstep.step_inputs
+    || exists (var_is name) m.mstep.step_outputs
+    || exists (var_is name) m.mstep.step_locals
+    || exists (var_is name) m.mmemory in
   mk_new_name used "self"
 
 (* Generation of a non-clashing name for the instance variable of static allocation macro *)
 let mk_instance m =
   let used name =
-       (List.exists (fun v -> v.var_id = name) m.mstep.step_inputs)
-    || (List.exists (fun v -> v.var_id = name) m.mmemory) in
+    let open List in
+    exists (var_is name) m.mstep.step_inputs
+    || exists (var_is name) m.mmemory in
   mk_new_name used "inst"
 
 (* Generation of a non-clashing name for the attribute variable of static allocation macro *)
 let mk_attribute m =
   let used name =
-       (List.exists (fun v -> v.var_id = name) m.mstep.step_inputs)
-    || (List.exists (fun v -> v.var_id = name) m.mmemory) in
+    let open List in
+    exists (var_is name) m.mstep.step_inputs
+    || exists (var_is name) m.mmemory in
   mk_new_name used "attr"
 
 let mk_call_var_decl loc id =
@@ -74,11 +85,14 @@ let reset_loop_counter () =
  loop_cpt := -1
 
 let mk_loop_var m () =
-  let vars = m.mstep.step_inputs@m.mstep.step_outputs@m.mstep.step_locals@m.mmemory in
+  let vars = m.mstep.step_inputs
+             @ m.mstep.step_outputs
+             @ m.mstep.step_locals
+             @ m.mmemory in
   let rec aux () =
     incr loop_cpt;
-    let s = Printf.sprintf "__%s_%d" "i" !loop_cpt in
-    if List.exists (fun v -> v.var_id = s) vars then aux () else s
+    let s = sprintf "__%s_%d" "i" !loop_cpt in
+    if List.exists (var_is s) vars then aux () else s
   in aux ()
 (*
 let addr_cpt = ref (-1)
@@ -111,65 +125,80 @@ let pp_machine_step_name fmt id = fprintf fmt "%s_step" id
 let pp_mod pp_val v1 v2 fmt =
   if !Options.integer_div_euclidean then
     (* (a mod_C b) + (a mod_C b < 0 ? abs(b) : 0) *)
-    Format.fprintf fmt "((%a %% %a) + ((%a %% %a) < 0?(abs(%a)):0))"
+    fprintf fmt "((%a %% %a) + ((%a %% %a) < 0?(abs(%a)):0))"
       pp_val v1 pp_val v2
       pp_val v1 pp_val v2
       pp_val v2
   else (* Regular behavior: printing a % *)
-    Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2
+    fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2
 
 let pp_div pp_val v1 v2 fmt =
   if !Options.integer_div_euclidean then
     (* (a - ((a mod_C b) + (a mod_C b < 0 ? abs(b) : 0))) div_C b *)
-    Format.fprintf fmt "(%a - %t) / %a"
+    fprintf fmt "(%a - %t) / %a"
       pp_val v1
       (pp_mod pp_val v1 v2)
       pp_val v2
   else (* Regular behavior: printing a / *)
-    Format.fprintf fmt "(%a / %a)" pp_val v1 pp_val v2
+    fprintf fmt "(%a / %a)" pp_val v1 pp_val v2
   
 let pp_basic_lib_fun is_int i pp_val fmt vl =
   match i, vl with
-  (*  | "ite", [v1; v2; v3] -> Format.fprintf fmt "(%a?(%a):(%a))" pp_val v1 pp_val v2 pp_val v3 *)
-  | "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v
-  | "not", [v] -> Format.fprintf fmt "(!%a)" pp_val v
-  | "impl", [v1; v2] -> Format.fprintf fmt "(!%a || %a)" pp_val v1 pp_val v2
-  | "=", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2
+  (*  | "ite", [v1; v2; v3] -> fprintf fmt "(%a?(%a):(%a))" pp_val v1 pp_val v2 pp_val v3 *)
+  | "uminus", [v] ->
+    fprintf fmt "(- %a)" pp_val v
+  | "not", [v] ->
+    fprintf fmt "(!%a)" pp_val v
+  | "impl", [v1; v2] ->
+    fprintf fmt "(!%a || %a)" pp_val v1 pp_val v2
+  | "=", [v1; v2] ->
+    fprintf fmt "(%a == %a)" pp_val v1 pp_val v2
   | "mod", [v1; v2] ->
      if is_int then
        pp_mod pp_val v1 v2 fmt 
      else
-       Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2
-  | "equi", [v1; v2] -> Format.fprintf fmt "(!%a == !%a)" pp_val v1 pp_val v2
-  | "xor", [v1; v2] -> Format.fprintf fmt "(!%a != !%a)" pp_val v1 pp_val v2
+       fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2
+  | "equi", [v1; v2] ->
+    fprintf fmt "(!%a == !%a)" pp_val v1 pp_val v2
+  | "xor", [v1; v2] ->
+    fprintf fmt "(!%a != !%a)" pp_val v1 pp_val v2
   | "/", [v1; v2] ->
      if is_int then
        pp_div pp_val v1 v2 fmt
      else
-       Format.fprintf fmt "(%a / %a)" pp_val v1 pp_val v2
-  | _, [v1; v2] -> Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2
-  | _ -> (Format.eprintf "internal error: Basic_library.pp_c %s@." i; assert false)
-
+       fprintf fmt "(%a / %a)" pp_val v1 pp_val v2
+  | _, [v1; v2] ->
+    fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2
+  | _ ->
+    (* TODO: raise proper error *)
+    eprintf "internal error: Basic_library.pp_c %s@." i;
+    assert false
 
 let rec pp_c_dimension fmt dim =
-  match dim.Dimension.dim_desc with
-  | Dimension.Dident id       ->
-     fprintf fmt "%s" id
-  | Dimension.Dint i          ->
-     fprintf fmt "%d" i
-  | Dimension.Dbool b         ->
-     fprintf fmt "%B" b
-  | Dimension.Dite (i, t, e)  ->
-     fprintf fmt "((%a)?%a:%a)"
-       pp_c_dimension i pp_c_dimension t pp_c_dimension e
-  | Dimension.Dappl (f, args) ->
-     fprintf fmt "%a" (pp_basic_lib_fun (Basic_library.is_numeric_operator f) f pp_c_dimension) args
-  | Dimension.Dlink dim' -> fprintf fmt "%a" pp_c_dimension dim'
-  | Dimension.Dvar       -> fprintf fmt "_%s" (Utils.name_of_dimension dim.Dimension.dim_id)
-  | Dimension.Dunivar    -> fprintf fmt "'%s" (Utils.name_of_dimension dim.Dimension.dim_id)
+  let open Dimension in
+  match dim.dim_desc with
+  | Dident id ->
+    fprintf fmt "%s" id
+  | Dint i ->
+    fprintf fmt "%d" i
+  | Dbool b ->
+    fprintf fmt "%B" b
+  | Dite (i, t, e) ->
+    fprintf fmt "((%a)?%a:%a)"
+      pp_c_dimension i pp_c_dimension t pp_c_dimension e
+  | Dappl (f, args) ->
+    fprintf fmt "%a"
+      (pp_basic_lib_fun (Basic_library.is_numeric_operator f) f pp_c_dimension)
+      args
+  | Dlink dim' ->
+    fprintf fmt "%a" pp_c_dimension dim'
+  | Dvar ->
+    fprintf fmt "_%s" (Utils.name_of_dimension dim.dim_id)
+  | Dunivar ->
+    fprintf fmt "'%s" (Utils.name_of_dimension dim.dim_id)
 
 let is_basic_c_type t =
-  Types.is_int_type t || Types.is_real_type t || Types.is_bool_type t
+  Types.(is_int_type t || is_real_type t || is_bool_type t)
 
 let pp_c_basic_type_desc t_desc =
   if Types.is_bool_type t_desc then
@@ -191,19 +220,28 @@ let pp_c_type ?(var_opt=None) var_id fmt t =
   let rec aux t pp_suffix =
     if is_basic_c_type  t then
        fprintf fmt "%a %s%a"
-	 (pp_basic_c_type ~var_opt) t
-	 var_id
-	 pp_suffix ()
+         (pp_basic_c_type ~var_opt) t
+         var_id
+         pp_suffix ()
     else
-      match (Types.repr t).Types.tdesc with
-      | Types.Tclock t'       -> aux t' pp_suffix
-      | Types.Tarray (d, t')  ->
-	 let pp_suffix' fmt () = fprintf fmt "%a[%a]" pp_suffix () pp_c_dimension d in
-	 aux t' pp_suffix'
-      | Types.Tstatic (_, t') -> fprintf fmt "const "; aux t' pp_suffix
-      | Types.Tconst ty       -> fprintf fmt "%s %s" ty var_id
-      | Types.Tarrow (_, _)   -> fprintf fmt "void (*%s)()" var_id
-      | _                     -> eprintf "internal error: C_backend_common.pp_c_type %a@." Types.print_ty t; assert false
+      let open Types in
+      match (repr t).tdesc with
+      | Tclock t' ->
+        aux t' pp_suffix
+      | Tarray (d, t')  ->
+        let pp_suffix' fmt () =
+          fprintf fmt "%a[%a]" pp_suffix () pp_c_dimension d in
+        aux t' pp_suffix'
+      | Tstatic (_, t') ->
+        fprintf fmt "const "; aux t' pp_suffix
+      | Tconst ty ->
+        fprintf fmt "%s %s" ty var_id
+      | Tarrow (_, _) ->
+        fprintf fmt "void (*%s)()" var_id
+      | _ ->
+        (* TODO: raise proper error *)
+        eprintf "internal error: C_backend_common.pp_c_type %a@." print_ty t;
+        assert false
   in aux t (fun _ () -> ())
 (*
 let rec pp_c_initialize fmt t = 
@@ -219,19 +257,25 @@ let rec pp_c_initialize fmt t =
   | _ -> assert false
  *)
 let pp_c_tag fmt t =
- pp_print_string fmt (if t = tag_true then "1" else if t = tag_false then "0" else t)
-
+  pp_print_string fmt
+    (if t = tag_true then "1" else if t = tag_false then "0" else t)
 
 (* Prints a constant value *)
 let rec pp_c_const fmt c =
   match c with
-    | Const_int i     -> pp_print_int fmt i
-    | Const_real r -> Real.pp fmt r
-    (* | Const_float r   -> pp_print_float fmt r *)
-    | Const_tag t     -> pp_c_tag fmt t
-    | Const_array ca  -> fprintf fmt "{%a }" (Utils.fprintf_list ~sep:", " pp_c_const) ca
-    | Const_struct fl -> fprintf fmt "{%a }" (Utils.fprintf_list ~sep:", " (fun fmt (_, c) -> pp_c_const fmt c)) fl
-    | Const_string _ | Const_modeid _ -> assert false (* string occurs in annotations not in C *)
+  | Const_int i ->
+    pp_print_int fmt i
+  | Const_real r ->
+    Real.pp fmt r
+  (* | Const_float r   -> pp_print_float fmt r *)
+  | Const_tag t ->
+    pp_c_tag fmt t
+  | Const_array ca ->
+    pp_print_braced pp_c_const fmt ca
+  | Const_struct fl ->
+    pp_print_braced (fun fmt (_, c) -> pp_c_const fmt c) fmt fl
+  | Const_string _
+  | Const_modeid _ -> assert false (* string occurs in annotations not in C *)
 
                   
 (* Prints a value expression [v], with internal function calls only.
@@ -241,21 +285,29 @@ let rec pp_c_const fmt c =
 let rec pp_c_val m self pp_var fmt v =
   let pp_c_val = pp_c_val m self pp_var in
   match v.value_desc with
-  | Cst c         -> pp_c_const fmt c
-  | Array vl      -> fprintf fmt "{%a}" (Utils.fprintf_list ~sep:", " pp_c_val) vl
-  | Access (t, i) -> fprintf fmt "%a[%a]" pp_c_val t pp_c_val i
-  | Power (v, _)  -> (Format.eprintf "internal error: C_backend_common.pp_c_val %a@." (Machine_code_common.pp_val m) v; assert false)
-  | Var v    ->
-     if Machine_code_common.is_memory m v then (
-       (* array memory vars are represented by an indirection to a local var with the right type,
-          in order to avoid casting everywhere. *)
-       if Types.is_array_type v.var_type && not (Types.is_real_type v.var_type && !Options.mpfr)
+  | Cst c ->
+    pp_c_const fmt c
+  | Array vl ->
+    pp_print_braced pp_c_val fmt vl
+  | Access (t, i) ->
+    fprintf fmt "%a[%a]" pp_c_val t pp_c_val i
+  | Power (v, _) ->
+    (* TODO: raise proper error *)
+    eprintf "internal error: C_backend_common.pp_c_val %a@."
+      (Machine_code_common.pp_val m) v;
+    assert false
+  | Var v ->
+     if Machine_code_common.is_memory m v then
+       (* array memory vars are represented by an indirection to a local var
+        *  with the right type, in order to avoid casting everywhere. *)
+       if Types.is_array_type v.var_type
+       && not (Types.is_real_type v.var_type && !Options.mpfr)
        then fprintf fmt "%a" pp_var v
        else fprintf fmt "%s->_reg.%a" self pp_var v
-     )
      else
        pp_var fmt v
-  | Fun (n, vl)   -> pp_basic_lib_fun (Types.is_int_type v.value_type) n pp_c_val fmt vl
+  | Fun (n, vl) ->
+    pp_basic_lib_fun (Types.is_int_type v.value_type) n pp_c_val fmt vl
 
 (* Access to the value of a variable:
    - if it's not a scalar output, then its name is enough
@@ -267,7 +319,8 @@ let pp_c_var_read m fmt id =
   (* mpfr_t is a static array, not treated as general arrays *)
   if Types.is_address_type id.var_type
   then
-    if Machine_code_common.is_memory m id && not (Types.is_real_type id.var_type && !Options.mpfr)
+    if Machine_code_common.is_memory m id
+    && not (Types.is_real_type id.var_type && !Options.mpfr)
     then fprintf fmt "(*%s)" id.var_id
     else fprintf fmt "%s" id.var_id
   else
@@ -298,8 +351,11 @@ let pp_c_var_write m fmt id =
 *)
 let pp_c_decl_input_var fmt id =
   if !Options.ansi && Types.is_address_type id.var_type
-  then pp_c_type ~var_opt:(Some id) (sprintf "(*%s)" id.var_id) fmt (Types.array_base_type id.var_type)
-  else pp_c_type ~var_opt:(Some id) id.var_id fmt id.var_type
+  then
+    pp_c_type ~var_opt:(Some id) (sprintf "(*%s)" id.var_id) fmt
+      (Types.array_base_type id.var_type)
+  else
+    pp_c_type ~var_opt:(Some id) id.var_id fmt id.var_type
 
 (* Declaration of an output variable:
    - if its type is scalar, then pass its address
@@ -309,8 +365,11 @@ let pp_c_decl_input_var fmt id =
 *)
 let pp_c_decl_output_var fmt id =
   if (not !Options.ansi) && Types.is_address_type id.var_type
-  then pp_c_type  ~var_opt:(Some id)                  id.var_id  fmt id.var_type
-  else pp_c_type  ~var_opt:(Some id) (sprintf "(*%s)" id.var_id) fmt (Types.array_base_type id.var_type)
+  then
+    pp_c_type ~var_opt:(Some id) id.var_id fmt id.var_type
+  else
+    pp_c_type ~var_opt:(Some id) (sprintf "(*%s)" id.var_id) fmt
+      (Types.array_base_type id.var_type)
 
 (* Declaration of a local/mem variable:
    - if it's an array/matrix/etc, its size(s) should be
@@ -320,80 +379,74 @@ let pp_c_decl_output_var fmt id =
 let pp_c_decl_local_var m fmt id =
   if id.var_dec_const
   then
-    Format.fprintf fmt "%a = %a"
-      (pp_c_type  ~var_opt:(Some id) id.var_id) id.var_type
-      (pp_c_val m "" (pp_c_var_read m)) (Machine_code_common.get_const_assign m id)
+    fprintf fmt "%a = %a"
+      (pp_c_type ~var_opt:(Some id) id.var_id)
+      id.var_type
+      (pp_c_val m "" (pp_c_var_read m))
+      (Machine_code_common.get_const_assign m id)
   else
-    Format.fprintf fmt "%a"
-      (pp_c_type  ~var_opt:(Some id) id.var_id) id.var_type
-
-let pp_c_decl_array_mem self fmt id =
-  fprintf fmt "%a = (%a) (%s->_reg.%s)"
-    (pp_c_type (sprintf "(*%s)" id.var_id)) id.var_type
-    (pp_c_type "(*)") id.var_type
-    self
-    id.var_id
+    fprintf fmt "%a"
+      (pp_c_type ~var_opt:(Some id) id.var_id) id.var_type
 
 (* Declaration of a struct variable:
    - if it's an array/matrix/etc, we declare it as a pointer
 *)
 let pp_c_decl_struct_var fmt id =
   if Types.is_array_type id.var_type
-  then pp_c_type (sprintf "(*%s)" id.var_id) fmt (Types.array_base_type id.var_type)
-  else pp_c_type                  id.var_id  fmt id.var_type
+  then
+    pp_c_type (sprintf "(*%s)" id.var_id) fmt
+      (Types.array_base_type id.var_type)
+  else
+    pp_c_type id.var_id  fmt id.var_type
 
 let pp_c_decl_instance_var fmt (name, (node, _)) =
   fprintf fmt "%a *%s" pp_machine_memtype_name (node_name node) name
 
-let pp_c_checks self fmt m =
-  Utils.fprintf_list ~sep:"" 
-    (fun fmt (loc, check) -> 
-      fprintf fmt 
-	"@[<v>%a@,assert (%a);@]@," 
-	Location.pp_c_loc loc
-	(pp_c_val m self (pp_c_var_read m)) check
-    ) 
-    fmt 
-    m.mstep.step_checks
+(* let pp_c_checks self fmt m =
+ *   pp_print_list
+ *     (fun fmt (loc, check) ->
+ *        fprintf fmt
+ *          "@[<v>%a@,assert (%a);@]"
+ *          Location.pp_c_loc loc
+ *          (pp_c_val m self (pp_c_var_read m)) check)
+ *     fmt
+ *     m.mstep.step_checks *)
 
 (********************************************************************************************)
 (*                       Struct Printing functions                                          *)
 (********************************************************************************************)
 
-let pp_registers_struct fmt m =
-  if m.mmemory <> []
-  then
-    fprintf fmt "@[%a {@[<v>%a;@ @]}@] _reg; "
-      pp_machine_regtype_name m.mname.node_id
-      (Utils.fprintf_list ~sep:";@ " pp_c_decl_struct_var) m.mmemory
-  else
-    ()
+(* let pp_registers_struct fmt m =
+ *   pp_print_braced
+ *     ~pp_prologue:(fun fmt () ->
+ *         fprintf fmt "@[%a " pp_machine_regtype_name m.mname.node_id)
+ *     ~pp_open_box:pp_open_vbox0
+ *     ~pp_sep:pp_print_semicolon
+ *     ~pp_eol:pp_print_semicolon
+ *     ~pp_epilogue:(fun fmt () -> pp_print_string fmt "@] _reg;")
+ *     pp_c_decl_struct_var
+ *     fmt m.mmemory *)
 
 let print_machine_struct fmt m =
-  if fst (Machine_code_common.get_stateless_status m) then
-    begin
-    end
-  else
-    begin
-      (* Define struct *)
-      fprintf fmt "@[%a {@[<v>%a%t%a%t@]};@]@."
-	pp_machine_memtype_name m.mname.node_id
-	pp_registers_struct m
-	(Utils.pp_final_char_if_non_empty "@ " m.mmemory)
-	(Utils.fprintf_list ~sep:";@ " pp_c_decl_instance_var) m.minstances
-	(Utils.pp_final_char_if_non_empty ";@ " m.minstances)
-    end
-
-let print_machine_struct_from_header fmt inode =
-  if inode.nodei_stateless then
-    begin
-    end
-  else
-    begin
-      (* Declare struct *)
-      fprintf fmt "@[%a;@]@."
-	pp_machine_memtype_name inode.nodei_id
-    end
+  if not (fst (Machine_code_common.get_stateless_status m)) then
+    (* Define struct *)
+    fprintf fmt "@[<v 2>%a {%a%a@]@,};"
+      pp_machine_memtype_name m.mname.node_id
+      (pp_print_list
+         ~pp_open_box:pp_open_vbox0
+         ~pp_prologue:(fun fmt () ->
+             fprintf fmt "@,@[%a {" pp_machine_regtype_name m.mname.node_id)
+         ~pp_sep:pp_print_semicolon
+         ~pp_eol:pp_print_semicolon'
+         ~pp_epilogue:(fun fmt () -> fprintf fmt "}@] _reg;")
+         pp_c_decl_struct_var)
+      m.mmemory
+      (pp_print_list
+         ~pp_prologue:pp_print_cut
+         ~pp_sep:pp_print_semicolon
+         ~pp_eol:pp_print_semicolon'
+         pp_c_decl_instance_var)
+      m.minstances
 
 (********************************************************************************************)
 (*                      Prototype Printing functions                                        *)
@@ -408,10 +461,10 @@ let print_global_clear_prototype fmt baseNAME =
     pp_global_clear_name baseNAME
 
 let print_alloc_prototype fmt (name, static) =
-  fprintf fmt "%a * %a (%a)"
+  fprintf fmt "%a * %a %a"
     pp_machine_memtype_name name
     pp_machine_alloc_name name
-    (Utils.fprintf_list ~sep:",@ " pp_c_decl_input_var) static
+    (pp_print_parenthesized pp_c_decl_input_var) static
 
 let print_dealloc_prototype fmt name =
   fprintf fmt "void %a (%a * _alloc)"
@@ -419,121 +472,68 @@ let print_dealloc_prototype fmt name =
     pp_machine_memtype_name name
     
 let print_reset_prototype self fmt (name, static) =
-  fprintf fmt "void %a (@[<v>%a%t%a *%s@])"
+  fprintf fmt "void %a (%a%a *%s)"
     pp_machine_reset_name name
-    (Utils.fprintf_list ~sep:",@ " pp_c_decl_input_var) static
-    (Utils.pp_final_char_if_non_empty ",@," static) 
+    (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
+       pp_c_decl_input_var) static
     pp_machine_memtype_name name
     self
 
 let print_init_prototype self fmt (name, static) =
-  fprintf fmt "void %a (@[<v>%a%t%a *%s@])"
+  fprintf fmt "void %a (%a%a *%s)"
     pp_machine_init_name name
-    (Utils.fprintf_list ~sep:",@ " pp_c_decl_input_var) static
-    (Utils.pp_final_char_if_non_empty ",@," static) 
+    (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
+       pp_c_decl_input_var) static
     pp_machine_memtype_name name
     self
 
 let print_clear_prototype self fmt (name, static) =
-  fprintf fmt "void %a (@[<v>%a%t%a *%s@])"
+  fprintf fmt "void %a (%a%a *%s)"
     pp_machine_clear_name name
-    (Utils.fprintf_list ~sep:",@ " pp_c_decl_input_var) static
-    (Utils.pp_final_char_if_non_empty ",@," static) 
+    (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
+       pp_c_decl_input_var) static
     pp_machine_memtype_name name
     self
 
 let print_stateless_prototype fmt (name, inputs, outputs) =
-  fprintf fmt "void %a (@[<v>@[%a%t@]@,@[%a@]@,@])"
+  fprintf fmt "void %a (@[<v>%a%a@])"
     pp_machine_step_name name
-    (Utils.fprintf_list ~sep:",@ " pp_c_decl_input_var) inputs
-    (Utils.pp_final_char_if_non_empty ",@ " inputs) 
-    (Utils.fprintf_list ~sep:",@ " pp_c_decl_output_var) outputs
+    (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
+       ~pp_epilogue:pp_print_cut pp_c_decl_input_var) inputs
+    (pp_print_list ~pp_sep:pp_print_comma pp_c_decl_output_var) outputs
 
 let print_step_prototype self fmt (name, inputs, outputs) =
-  fprintf fmt "void %a (@[<v>@[%a%t@]@,@[%a@]%t@[%a *%s@]@])"
+  fprintf fmt "void %a (@[<v>%a%a%a *%s@])"
     pp_machine_step_name name
-    (Utils.fprintf_list ~sep:",@ " pp_c_decl_input_var) inputs
-    (Utils.pp_final_char_if_non_empty ",@ " inputs) 
-    (Utils.fprintf_list ~sep:",@ " pp_c_decl_output_var) outputs
-    (Utils.pp_final_char_if_non_empty ",@," outputs) 
+    (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
+       ~pp_epilogue:pp_print_cut pp_c_decl_input_var) inputs
+    (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
+       ~pp_epilogue:pp_print_cut pp_c_decl_output_var) outputs
     pp_machine_memtype_name name
     self
 
-let print_stateless_C_prototype fmt (name, inputs, outputs) =
-  let output = 
-    match outputs with
-    | [hd] -> hd
-    | _ -> assert false
-  in
-  fprintf fmt "%a %s (@[<v>@[%a@]@,@])"
-    (pp_basic_c_type ~var_opt:None) output.var_type
-    name
-    (Utils.fprintf_list ~sep:",@ " pp_c_decl_input_var) inputs
-    
-let print_import_init fmt dep =
-  if dep.local then
-    let baseNAME = file_to_module_name dep.name in
-    fprintf fmt "%a();" pp_global_init_name baseNAME
-  else ()
-
-let print_import_clear fmt dep =
-  if dep.local then
-    let baseNAME = file_to_module_name dep.name in
-    fprintf fmt "%a();" pp_global_clear_name baseNAME
-  else ()
-
 let print_import_prototype fmt dep =
-  fprintf fmt "#include \"%s.h\"@," dep.name
+  fprintf fmt "#include \"%s.h\"" dep.name
 
 let print_import_alloc_prototype fmt dep =
   if dep.is_stateful then
-    fprintf fmt "#include \"%s_alloc.h\"@," dep.name
-
-let print_extern_alloc_prototypes fmt dep =
-  List.iter (fun decl -> match decl.top_decl_desc with
-  | ImportedNode ind when not ind.nodei_stateless ->
-    let static = List.filter (fun v -> v.var_dec_const) ind.nodei_inputs in
-    begin
-      fprintf fmt "extern %a;@.@." print_alloc_prototype (ind.nodei_id, static);
-      fprintf fmt "extern %a;@.@." print_dealloc_prototype ind.nodei_id;
-    end
-  | _                -> ()
-  ) dep.content
-
-
-let pp_c_main_var_input fmt id =  
-  fprintf fmt "%s" id.var_id
-
-let pp_c_main_var_output fmt id =
-  if Types.is_address_type id.var_type
-  then
-    fprintf fmt "%s" id.var_id
-  else
-    fprintf fmt "&%s" id.var_id
-
-let pp_main_call mname self fmt m (inputs: value_t list) (outputs: var_decl list) =
-  if fst (Machine_code_common.get_stateless_status m)
-  then
-    fprintf fmt "%a (%a%t%a);"
-      pp_machine_step_name mname
-      (Utils.fprintf_list ~sep:", " (pp_c_val m self pp_c_main_var_input)) inputs
-      (Utils.pp_final_char_if_non_empty ", " inputs) 
-      (Utils.fprintf_list ~sep:", " pp_c_main_var_output) outputs
-  else
-    fprintf fmt "%a (%a%t%a%t%s);"
-      pp_machine_step_name mname
-      (Utils.fprintf_list ~sep:", " (pp_c_val m self pp_c_main_var_input)) inputs
-      (Utils.pp_final_char_if_non_empty ", " inputs) 
-      (Utils.fprintf_list ~sep:", " pp_c_main_var_output) outputs
-      (Utils.pp_final_char_if_non_empty ", " outputs)
-      self
+    fprintf fmt "#include \"%s_alloc.h\"" dep.name
 
 let pp_c_var m self pp_var fmt var =
     pp_c_val m self pp_var fmt (Machine_code_common.mk_val (Var var) var.var_type)
-  
 
-let pp_array_suffix fmt loop_vars =
-  Utils.fprintf_list ~sep:"" (fun fmt v -> fprintf fmt "[%s]" v) fmt loop_vars
+let pp_array_suffix =
+  pp_print_list ~pp_sep:pp_print_nothing (fun fmt v -> fprintf fmt "[%s]" v)
+
+let mpfr_vars vars =
+  if !Options.mpfr then
+    List.filter (fun v -> Types.(is_real_type (array_base_type v.var_type))) vars
+  else []
+
+let mpfr_consts consts =
+  if !Options.mpfr then
+    List.filter (fun c -> Types.(is_real_type (array_base_type c.const_type))) consts
+  else []
 
 (* type directed initialization: useless wrt the lustre compilation model,
    except for MPFR injection, where values are dynamically allocated
@@ -545,50 +545,16 @@ let pp_initialize m self pp_var fmt var =
       let dim = Types.array_type_dimension typ in
       let idx = mk_loop_var m () in
       fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"
-	idx idx idx pp_c_dimension dim idx
-	(aux (idx::indices)) (Types.array_element_type typ)
+        idx idx idx pp_c_dimension dim idx
+        (aux (idx::indices)) (Types.array_element_type typ)
     else
       let indices = List.rev indices in
       let pp_var_suffix fmt var =
-	fprintf fmt "%a%a" (pp_c_var m self pp_var) var pp_array_suffix indices in
+        fprintf fmt "%a%a" (pp_c_var m self pp_var) var pp_array_suffix indices in
       Mpfr.pp_inject_init pp_var_suffix fmt var
   in
-  if !Options.mpfr && Types.is_real_type (Types.array_base_type var.var_type)
-  then
-    begin
-      reset_loop_counter ();
-      aux [] fmt var.var_type
-    end
-
-let pp_const_initialize m pp_var fmt const =
-  let var = Machine_code_common.mk_val (Var (Corelang.var_decl_of_const const)) const.const_type in
-  let rec aux indices value fmt typ =
-    if Types.is_array_type typ
-    then
-      let dim = Types.array_type_dimension typ in
-      let szl = Utils.enumerate (Dimension.size_const_dimension dim) in
-      let typ' = Types.array_element_type typ in
-      let value = match value with
-	| Const_array ca -> List.nth ca
-	| _                      -> assert false in
-      fprintf fmt "%a"
-	(Utils.fprintf_list ~sep:"@," (fun fmt i -> aux (string_of_int i::indices) (value i) fmt typ')) szl
-    else
-      let indices = List.rev indices in
-      let pp_var_suffix fmt var =
-	fprintf fmt "%a%a" (pp_c_val m "" pp_var) var pp_array_suffix indices in
-      begin
-	Mpfr.pp_inject_init pp_var_suffix fmt var;
-	fprintf fmt "@,";
-	Mpfr.pp_inject_real pp_var_suffix pp_c_const fmt var value
-      end
-  in
-  if !Options.mpfr && Types.is_real_type (Types.array_base_type const.const_type)
-  then
-    begin
-      reset_loop_counter ();
-      aux [] const.const_value fmt const.const_type
-    end
+  reset_loop_counter ();
+  aux [] fmt var.var_type
 
 (* type directed clear: useless wrt the lustre compilation model,
    except for MPFR injection, where values are dynamically allocated
@@ -600,195 +566,86 @@ let pp_clear m self pp_var fmt var =
       let dim = Types.array_type_dimension typ in
       let idx = mk_loop_var m () in
       fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"
-	idx idx idx pp_c_dimension dim idx
-	(aux (idx::indices)) (Types.array_element_type typ)
+        idx idx idx pp_c_dimension dim idx
+        (aux (idx::indices)) (Types.array_element_type typ)
     else
       let indices = List.rev indices in
       let pp_var_suffix fmt var =
-	fprintf fmt "%a%a" (pp_c_var m self pp_var) var pp_array_suffix indices in
+        fprintf fmt "%a%a" (pp_c_var m self pp_var) var pp_array_suffix indices in
       Mpfr.pp_inject_clear pp_var_suffix fmt var
   in
-  if !Options.mpfr && Types.is_real_type (Types.array_base_type var.var_type)
-  then
-    begin
-      reset_loop_counter ();
-      aux [] fmt var.var_type
-    end
-
-let pp_const_clear pp_var fmt const =
-  let m = Machine_code_common.empty_machine in
-  let var = Corelang.var_decl_of_const const in
-  let rec aux indices fmt typ =
-    if Types.is_array_type typ
-    then
-      let dim = Types.array_type_dimension typ in
-      let idx = mk_loop_var m () in
-      fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"
-	idx idx idx pp_c_dimension dim idx
-	(aux (idx::indices)) (Types.array_element_type typ)
-    else
-      let indices = List.rev indices in
-      let pp_var_suffix fmt var =
-	fprintf fmt "%a%a" (pp_c_var m "" pp_var) var pp_array_suffix indices in
-      Mpfr.pp_inject_clear pp_var_suffix fmt var 
-  in
-  if !Options.mpfr && Types.is_real_type (Types.array_base_type var.var_type)
-  then
-    begin
-      reset_loop_counter ();
-      aux [] fmt var.var_type
-    end
-
-let pp_call m self pp_read pp_write fmt i (inputs: Machine_code_types.value_t list) (outputs: var_decl list) =
- try (* stateful node instance *)
-   let (n,_) = List.assoc i m.minstances in
-   fprintf fmt "%a (%a%t%a%t%s->%s);"
-     pp_machine_step_name (node_name n)
-     (Utils.fprintf_list ~sep:", " (pp_c_val m self pp_read)) inputs
-     (Utils.pp_final_char_if_non_empty ", " inputs) 
-     (Utils.fprintf_list ~sep:", " pp_write) outputs
-     (Utils.pp_final_char_if_non_empty ", " outputs)
-     self
-     i
- with Not_found -> (* stateless node instance *)
-   let (n,_) = List.assoc i m.mcalls in
-   fprintf fmt "%a (%a%t%a);"
-     pp_machine_step_name (node_name n)
-     (Utils.fprintf_list ~sep:", " (pp_c_val m self pp_read)) inputs
-     (Utils.pp_final_char_if_non_empty ", " inputs) 
-     (Utils.fprintf_list ~sep:", " pp_write) outputs 
-
-let pp_basic_instance_call m self fmt i (inputs: Machine_code_types.value_t list) (outputs: var_decl list) =
-  pp_call m self (pp_c_var_read m) (pp_c_var_write m) fmt i inputs outputs
-(*
- try (* stateful node instance *)
-   let (n,_) = List.assoc i m.minstances in
-   fprintf fmt "%a (%a%t%a%t%s->%s);"
-     pp_machine_step_name (node_name n)
-     (Utils.fprintf_list ~sep:", " (pp_c_val m self (pp_c_var_read m))) inputs
-     (Utils.pp_final_char_if_non_empty ", " inputs) 
-     (Utils.fprintf_list ~sep:", " (pp_c_var_write m)) outputs
-     (Utils.pp_final_char_if_non_empty ", " outputs)
-     self
-     i
- with Not_found -> (* stateless node instance *)
-   let (n,_) = List.assoc i m.mcalls in
-   fprintf fmt "%a (%a%t%a);"
-     pp_machine_step_name (node_name n)
-     (Utils.fprintf_list ~sep:", " (pp_c_val m self (pp_c_var_read m))) inputs
-     (Utils.pp_final_char_if_non_empty ", " inputs) 
-     (Utils.fprintf_list ~sep:", " (pp_c_var_write m)) outputs 
-*)
-
-let pp_instance_call m self fmt i (inputs: Machine_code_types.value_t list) (outputs: var_decl list) =
-  let pp_offset pp_var indices fmt var =
-    match indices with
-    | [] -> fprintf fmt "%a" pp_var var
-    | _  -> fprintf fmt "%a[%a]" pp_var var (Utils.fprintf_list ~sep:"][" pp_print_string) indices in
-  let rec aux indices fmt typ =
-    if Types.is_array_type typ
-    then
-      let dim = Types.array_type_dimension typ in
-      let idx = mk_loop_var m () in
-      fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"
-	idx idx idx pp_c_dimension dim idx
-	(aux (idx::indices)) (Types.array_element_type typ)
-    else
-      let pp_read  = pp_offset (pp_c_var_read  m) indices in
-      let pp_write = pp_offset (pp_c_var_write m) indices in
-      pp_call m self pp_read pp_write fmt i inputs outputs
-  in
-  begin
-    reset_loop_counter ();
-    aux [] fmt (List.hd inputs).Machine_code_types.value_type
-  end
+  reset_loop_counter ();
+  aux [] fmt var.var_type
 
   (*** Common functions for main ***)
 
-let pp_print_file file_suffix fmt typ arg =
-  fprintf fmt "@[<v 2>if (traces) {@ ";
-  fprintf fmt "fprintf(f_%s, \"%%%s\\n\", %s);@ " file_suffix typ arg;
-  fprintf fmt "fflush(f_%s);@ " file_suffix;
-  fprintf fmt "@]}@ "
+let pp_print_file file_suffix fmt (typ, arg) =
+  fprintf fmt
+    "@[<v 2>if (traces) {@,\
+     fprintf(f_%s, \"%%%s\\n\", %s);@,\
+     fflush(f_%s);@]@,\
+     }"
+    file_suffix typ arg
+    file_suffix
   
 let print_put_var fmt file_suffix name var_type var_id =
   let pp_file = pp_print_file ("out" ^ file_suffix) in
   let unclocked_t = Types.unclock_type var_type in
-  if Types.is_int_type unclocked_t then (
-    fprintf fmt "_put_int(\"%s\", %s);@ " name var_id;
-    pp_file fmt "d" var_id
-  )
-  else if Types.is_bool_type unclocked_t then (
-    fprintf fmt "_put_bool(\"%s\", %s);@ " name var_id;
-    pp_file fmt "i" var_id
-  )
-  else if Types.is_real_type unclocked_t then
-    
-      if !Options.mpfr then (
-        fprintf fmt "_put_double(\"%s\", mpfr_get_d(%s, %s), %i);@ " name var_id (Mpfr.mpfr_rnd ()) !Options.print_prec_double;
-        pp_file fmt ".*f" ((string_of_int !Options.print_prec_double) ^ ", mpfr_get_d(" ^ var_id ^ ", MPFR_RNDN)")
-      )
-      else (
-        fprintf fmt "_put_double(\"%s\", %s, %i);@ " name var_id !Options.print_prec_double;
-        pp_file fmt ".*f" ((string_of_int !Options.print_prec_double) ^ ", " ^ var_id)
-      )
-    
-  else
-    (Format.eprintf "Impossible to print the _put_xx for type %a@.@?" Types.print_ty var_type; assert false)
-
-      
-let print_get_inputs fmt m =
-  let pi fmt (id, v', v) =
-    let pp_file = pp_print_file ("in" ^ (string_of_int id)) in
-    let unclocked_t = Types.unclock_type v.var_type in
-    if Types.is_int_type unclocked_t then (
-      fprintf fmt "%s = _get_int(\"%s\");@ " v.var_id v'.var_id;
-      pp_file fmt "d" v.var_id
-    )
-    else if Types.is_bool_type unclocked_t then (
-      fprintf fmt "%s = _get_bool(\"%s\");@ " v.var_id v'.var_id;
-      pp_file fmt "i" v.var_id
-    )
-    else if Types.is_real_type unclocked_t then
-        if !Options.mpfr then (
-	  fprintf fmt "double %s_tmp = _get_double(\"%s\");@ " v.var_id v'.var_id;
-          pp_file fmt "f" (v.var_id ^ "_tmp");
-          fprintf fmt "mpfr_set_d(%s, %s_tmp, %i);" v.var_id v.var_id (Mpfr.mpfr_prec ())
-        )
-        else (
-	  fprintf fmt "%s = _get_double(\"%s\");@ " v.var_id v'.var_id;
-          pp_file fmt "f" v.var_id
-        )
-    else
-      begin
-	Global.main_node := !Options.main_node;
-	Format.eprintf "Code generation error: %a%a@."
-	  Error.pp_error_msg Error.Main_wrong_kind
-	  Location.pp_loc v'.var_loc;
-	raise (Error.Error (v'.var_loc, Error.Main_wrong_kind))
-      end
-  in
-  Utils.List.iteri2 (fun idx v' v ->
-    fprintf fmt "@ %a" pi ((idx+1), v', v);
-  ) m.mname.node_inputs m.mstep.step_inputs
-
+  fprintf fmt "@[<v>%a@]"
+    (fun fmt () ->
+       if Types.is_int_type unclocked_t then
+         fprintf fmt "_put_int(\"%s\", %s);@,%a"
+           name var_id
+           pp_file ("d", var_id)
+       else if Types.is_bool_type unclocked_t then
+         fprintf fmt "_put_bool(\"%s\", %s);@,%a"
+           name var_id
+           pp_file ("i", var_id)
+       else if Types.is_real_type unclocked_t then
+         if !Options.mpfr then
+           fprintf fmt "_put_double(\"%s\", mpfr_get_d(%s, %s), %i);@,%a"
+             name var_id (Mpfr.mpfr_rnd ()) !Options.print_prec_double
+             pp_file (".*f",
+                      string_of_int !Options.print_prec_double
+                      ^ ", mpfr_get_d(" ^ var_id ^ ", MPFR_RNDN)")
+         else
+           fprintf fmt "_put_double(\"%s\", %s, %i);@,%a"
+             name var_id !Options.print_prec_double
+             pp_file (".*f",
+                      string_of_int !Options.print_prec_double ^ ", " ^ var_id)
+       else begin
+         eprintf "Impossible to print the _put_xx for type %a@.@?"
+           Types.print_ty var_type;
+         assert false
+       end) ()
 
 let pp_file_decl fmt inout idx =
   let idx = idx + 1 in (* we start from 1: in1, in2, ... *)
-  fprintf fmt "FILE *f_%s%i;@ " inout idx 
+  fprintf fmt "FILE *f_%s%i;" inout idx
 
 let pp_file_open fmt inout idx =
   let idx = idx + 1 in (* we start from 1: in1, in2, ... *)
-  fprintf fmt "const char* cst_char_suffix_%s%i = \"_simu.%s%i\";@ " inout idx inout idx;
-  fprintf fmt "size_t l%s%i = strlen(dir) + strlen(prefix) + strlen(cst_char_suffix_%s%i);@ " inout idx inout idx;
-  fprintf fmt "char* f_%s%i_name = malloc((l%s%i+2) * sizeof(char));@ " inout idx inout idx;
-  fprintf fmt "strcpy (f_%s%i_name, dir);@ " inout idx;
-  fprintf fmt "strcat(f_%s%i_name, \"/\");@ " inout idx;
-  fprintf fmt "strcat(f_%s%i_name, prefix);@ " inout idx;
-  fprintf fmt "strcat(f_%s%i_name, cst_char_suffix_%s%i);@ " inout idx inout idx;
-  fprintf fmt "f_%s%i = fopen(f_%s%i_name, \"w\");@ " inout idx inout idx;
-  fprintf fmt "free(f_%s%i_name);@ " inout idx;
-  "f_" ^ inout ^ (string_of_int idx)
+  fprintf fmt
+    "@[<v>const char* cst_char_suffix_%s%i = \"_simu.%s%i\";@,\
+     size_t l%s%i = strlen(dir) + strlen(prefix) + strlen(cst_char_suffix_%s%i);@,\
+     char* f_%s%i_name = malloc((l%s%i+2) * sizeof(char));@,\
+     strcpy (f_%s%i_name, dir);@,\
+     strcat(f_%s%i_name, \"/\");@,\
+     strcat(f_%s%i_name, prefix);@,\
+     strcat(f_%s%i_name, cst_char_suffix_%s%i);@,\
+     f_%s%i = fopen(f_%s%i_name, \"w\");@,\
+     free(f_%s%i_name);\
+     @]"
+    inout idx inout idx
+    inout idx inout idx
+    inout idx inout idx
+    inout idx
+    inout idx
+    inout idx
+    inout idx inout idx
+    inout idx inout idx
+    inout idx;
+  "f_" ^ inout ^ string_of_int idx
 
 
 (* Local Variables: *)
diff --git a/src/backends/C/c_backend_header.ml b/src/backends/C/c_backend_header.ml
index b853f5e7..986b9c57 100644
--- a/src/backends/C/c_backend_header.ml
+++ b/src/backends/C/c_backend_header.ml
@@ -9,7 +9,7 @@
 (*                                                                  *)
 (********************************************************************)
 
-open Format 
+open Utils.Format
 open Lustre_types
 open Corelang
 open Machine_code_types
@@ -21,413 +21,453 @@ open C_backend_common
 (********************************************************************************************)
 
 
-module type MODIFIERS_HDR =
-sig
+module type MODIFIERS_HDR = sig
   val print_machine_decl_prefix: Format.formatter -> machine_t -> unit
 end
 
-module EmptyMod =
-struct
+module EmptyMod = struct
   let print_machine_decl_prefix = fun _ _ -> ()
 end
 
-module Main = functor (Mod: MODIFIERS_HDR) -> 
-struct
+module Main = functor (Mod: MODIFIERS_HDR) -> struct
 
-let print_import_standard fmt =
-  begin
+  let print_import_standard fmt () =
     (* if Machine_types.has_machine_type () then *)
-    (*   begin *)
-	fprintf fmt "#include <stdint.h>@.";
-      (* end; *)
-    if !Options.mpfr then
-      begin
-	fprintf fmt "#include <mpfr.h>@."
-      end;
-    if !Options.cpp then
-      fprintf fmt "#include \"%s/arrow.hpp\"@.@." (Arrow.arrow_top_decl ()).top_decl_owner
-    else
-      fprintf fmt "#include \"%s/arrow.h\"@.@." (Arrow.arrow_top_decl ()).top_decl_owner
-	
-  end
-
-let rec print_static_val pp_var fmt v =
-  match v.value_desc with
-  | Cst c         -> pp_c_const fmt c
-  | Var v         -> pp_var fmt v
-  | Fun (n, vl)   -> pp_basic_lib_fun (Types.is_int_type v.value_type) n (print_static_val pp_var) fmt vl
-  | _             -> (Format.eprintf "Internal error: C_backend_header.print_static_val"; assert false)
-
-let print_constant_decl (m, attr, inst) pp_var fmt v =
-  Format.fprintf fmt "%s %a = %a"
-    attr
-    (pp_c_type (Format.sprintf "%s ## %s" inst v.var_id)) v.var_type
-    (print_static_val pp_var) (get_const_assign m v)
-
-let print_static_constant_decl (m, attr, inst) fmt const_locals =
-  let pp_var fmt v =
-    if List.mem v const_locals
-    then
-      Format.fprintf fmt "%s ## %s" inst v.var_id
-    else 
-      Format.fprintf fmt "%s" v.var_id in
-  Format.fprintf fmt "%a%t"
-    (Utils.fprintf_list ~sep:";\\@," (print_constant_decl (m, attr, inst) pp_var)) const_locals
-    (Utils.pp_final_char_if_non_empty ";\\@," const_locals)
-
-let print_static_declare_instance (m, attr, inst) const_locals fmt (i, (n, static)) =
-  let pp_var fmt v =
-    if List.mem v const_locals
-    then
-      Format.fprintf fmt "%s ## %s" inst v.var_id
-    else 
-      Format.fprintf fmt "%s" v.var_id in
-  let values = List.map (value_of_dimension m) static in
-  fprintf fmt "%a(%s, %a%t%s)"
-    pp_machine_static_declare_name (node_name n)
-    attr
-    (Utils.fprintf_list ~sep:", " (print_static_val pp_var)) values
-    (Utils.pp_final_char_if_non_empty ", " static)
-    i
-
-let print_static_declare_macro fmt (m, attr, inst) =
-  let const_locals = List.filter (fun vdecl -> vdecl.var_dec_const) m.mstep.step_locals in
-  let array_mem = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
-  fprintf fmt "@[<v 2>#define %a(%s, %a%t%s)\\@,%a%s %a %s;\\@,%a%t%a;@,@]"
-    pp_machine_static_declare_name m.mname.node_id
-    attr
-    (Utils.fprintf_list ~sep:", " (pp_c_var_read m)) m.mstatic
-    (Utils.pp_final_char_if_non_empty ", " m.mstatic)
-    inst
-    (* constants *)
-    (print_static_constant_decl (m, attr, inst)) const_locals
-    attr
-    pp_machine_memtype_name m.mname.node_id
-    inst
-    (Utils.fprintf_list ~sep:";\\@," (pp_c_decl_local_var m)) array_mem
-    (Utils.pp_final_char_if_non_empty ";\\@," array_mem)
-    (Utils.fprintf_list ~sep:";\\@,"
-       (fun fmt (i',m') ->
-	 let path = sprintf "%s ## _%s" inst i' in
-	 fprintf fmt "%a"
-	   (print_static_declare_instance (m, attr, inst) const_locals) (path, m')
-       )) m.minstances
-
-      
-let print_static_link_instance fmt (i, (m, _)) =
- fprintf fmt "%a(%s)" pp_machine_static_link_name (node_name m) i
-
-(* Allocation of a node struct:
-   - if node memory is an array/matrix/etc, we cast it to a pointer (see pp_registers_struct)
-*)
-let print_static_link_macro fmt (m, _, inst) =
-  let array_mem = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
-  fprintf fmt "@[<v>@[<v 2>#define %a(%s) do {\\@,%a%t%a;\\@]@,} while (0)@.@]"
-    pp_machine_static_link_name m.mname.node_id
-    inst
-    (Utils.fprintf_list ~sep:";\\@,"
-       (fun fmt v ->
-	 fprintf fmt "%s._reg.%s = (%a*) &%s"
-	   inst
-	   v.var_id
-           (fun fmt v -> pp_c_type "" fmt (Types.array_base_type v.var_type)) v
-	   v.var_id
-       )) array_mem
-    (Utils.pp_final_char_if_non_empty ";\\@," array_mem)
-    (Utils.fprintf_list ~sep:";\\@,"
-       (fun fmt (i',m') ->
-	 let path = sprintf "%s ## _%s" inst i' in
-	 fprintf fmt "%a;\\@,%s.%s = &%s"
-	   print_static_link_instance (path,m')
-	   inst
-	   i'
-	   path
-       )) m.minstances
-
-let print_static_alloc_macro fmt (m, attr, inst) =
-  fprintf fmt "@[<v>@[<v 2>#define %a(%s, %a%t%s)\\@,%a(%s, %a%t%s);\\@,%a(%s);@]@,@]@."
-    pp_machine_static_alloc_name m.mname.node_id
-    attr
-    (Utils.fprintf_list ~sep:", " (pp_c_var_read m)) m.mstatic
-    (Utils.pp_final_char_if_non_empty ", " m.mstatic)
-    inst
-    pp_machine_static_declare_name m.mname.node_id
-    attr
-    (Utils.fprintf_list ~sep:", " (pp_c_var_read m)) m.mstatic
-    (Utils.pp_final_char_if_non_empty ", " m.mstatic)
-    inst
-    pp_machine_static_link_name m.mname.node_id
-    inst
-
-(* TODO: ACSL
-we do multiple things:
-- provide the semantics of the node as a predicate: function step and reset are associated to ACSL predicate
-- the node is associated to a refinement contract, wrt its ACSL sem
-- if the node is a regular node associated to a contract, print the contract as function contract.
-- do not print anything if this is a contract node
-*)
-let print_machine_alloc_decl fmt m =
-  Mod.print_machine_decl_prefix fmt m;
-  if fst (get_stateless_status m) then
-    begin
-    end
-  else
-    begin
-      if !Options.static_mem
-      then
-	begin
-	  (* Static allocation *)
-	  let inst = mk_instance m in
-	  let attr = mk_attribute m in
-	  fprintf fmt "%a@.%a@.%a@."
-		  print_static_declare_macro (m, attr, inst)
-		  print_static_link_macro (m, attr, inst)
-		  print_static_alloc_macro (m, attr, inst)
-	end
+    fprintf fmt
+      "#include <stdint.h>@,\
+       %a\
+       #include \"%s/arrow.h%s\""
+      (if !Options.mpfr then
+         pp_print_endcut "#include <mpfr.h>"
+       else pp_print_nothing) ()
+      (Arrow.arrow_top_decl ()).top_decl_owner
+      (if !Options.cpp then "pp" else "")
+
+  let rec print_static_val pp_var fmt v =
+    match v.value_desc with
+    | Cst c ->
+      pp_c_const fmt c
+    | Var v ->
+      pp_var fmt v
+    | Fun (n, vl) ->
+      pp_basic_lib_fun (Types.is_int_type v.value_type) n
+        (print_static_val pp_var) fmt vl
+    | _ ->
+      (* TODO: raise proper error *)
+      eprintf "Internal error: C_backend_header.print_static_val";
+      assert false
+
+  let print_constant_decl (m, attr, inst) pp_var fmt v =
+    fprintf fmt "%s %a = %a"
+      attr
+      (pp_c_type (sprintf "%s ## %s" inst v.var_id)) v.var_type
+      (print_static_val pp_var) (get_const_assign m v)
+
+  let pp_var inst const_locals fmt v =
+    if List.mem v const_locals then
+      fprintf fmt "%s ## %s" inst v.var_id
+    else fprintf fmt "%s" v.var_id
+
+  let print_static_constant_decl (_, _, inst as macro) fmt const_locals =
+    pp_print_list ~pp_open_box:pp_open_vbox0
+      ~pp_sep:(pp_print_endcut ";\\")  ~pp_eol:(pp_print_endcut ";\\")
+      (print_constant_decl macro (pp_var inst const_locals))
+      fmt
+      const_locals
+
+  let print_static_declare_instance
+      (m, attr, inst) const_locals fmt (i, (n, static)) =
+    let values = List.map (value_of_dimension m) static in
+    fprintf fmt "%a(%s, %a%s)"
+      pp_machine_static_declare_name (node_name n)
+      attr
+      (pp_print_list ~pp_open_box:pp_open_hbox ~pp_sep:pp_print_comma
+         ~pp_eol:pp_print_comma (print_static_val (pp_var inst const_locals)))
+      values
+      i
+
+  let print_static_declare_macro fmt (m, attr, inst as macro) =
+    let const_locals =
+      List.filter (fun vdecl -> vdecl.var_dec_const) m.mstep.step_locals in
+    let array_mem =
+      List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
+    fprintf fmt
+      "@[<v 2>\
+       #define %a(%s, %a%s)\\@,\
+       %a%s %a %s;\\@,\
+       %a%a;\
+       @]"
+      pp_machine_static_declare_name m.mname.node_id
+      attr
+      (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
+         (pp_c_var_read m)) m.mstatic
+      inst
+      (* constants *)
+      (print_static_constant_decl macro) const_locals
+      attr
+      pp_machine_memtype_name m.mname.node_id
+      inst
+      (pp_print_list ~pp_open_box:pp_open_vbox0
+         ~pp_sep:(pp_print_endcut ";\\") ~pp_eol:(pp_print_endcut ";\\")
+         (pp_c_decl_local_var m)) array_mem
+      (pp_print_list ~pp_open_box:pp_open_vbox0
+         ~pp_sep:(pp_print_endcut ";\\")
+         (fun fmt (i', m') ->
+            let path = sprintf "%s ## _%s" inst i' in
+            fprintf fmt "%a"
+              (print_static_declare_instance macro const_locals)
+              (path, m'))) m.minstances
+
+  let print_static_link_instance fmt (i, (m, _)) =
+    fprintf fmt "%a(%s)" pp_machine_static_link_name (node_name m) i
+
+  (* Allocation of a node struct:
+     - if node memory is an array/matrix/etc, we cast it to a pointer (see pp_registers_struct)
+  *)
+  let print_static_link_macro fmt (m, _, inst) =
+    let array_mem = List.filter (fun v -> Types.is_array_type v.var_type)
+        m.mmemory in
+    fprintf fmt
+      "@[<v>@[<v 2>\
+       #define %a(%s) do {\\@,\
+       %a%a;\\@]@,\
+       } while (0)\
+       @]"
+      pp_machine_static_link_name m.mname.node_id
+      inst
+      (pp_print_list ~pp_open_box:pp_open_vbox0
+         ~pp_sep:(pp_print_endcut ";\\") ~pp_eol:(pp_print_endcut ";\\")
+         (fun fmt v ->
+            fprintf fmt "%s._reg.%s = (%a*) &%s"
+              inst
+              v.var_id
+              (fun fmt v -> pp_c_type "" fmt (Types.array_base_type v.var_type)) v
+              v.var_id)) array_mem
+      (pp_print_list ~pp_open_box:pp_open_vbox0
+         ~pp_sep:(pp_print_endcut ";\\")
+         (fun fmt (i',m') ->
+            let path = sprintf "%s ## _%s" inst i' in
+            fprintf fmt "%a;\\@,%s.%s = &%s"
+              print_static_link_instance (path,m')
+              inst
+              i'
+              path)) m.minstances
+
+  let print_static_alloc_macro fmt (m, attr, inst) =
+    fprintf fmt
+      "@[<v>@[<v 2>\
+       #define %a(%s, %a%s)\\@,\
+       %a(%s, %a%s);\\@,\
+       %a(%s);\
+       @]@]"
+      pp_machine_static_alloc_name m.mname.node_id
+      attr
+      (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
+         (pp_c_var_read m)) m.mstatic
+      inst
+      pp_machine_static_declare_name m.mname.node_id
+      attr
+      (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
+         (pp_c_var_read m)) m.mstatic
+      inst
+      pp_machine_static_link_name m.mname.node_id
+      inst
+
+  (* TODO: ACSL
+     we do multiple things:
+     - provide the semantics of the node as a predicate: function step and reset are associated to ACSL predicate
+     - the node is associated to a refinement contract, wrt its ACSL sem
+     - if the node is a regular node associated to a contract, print the contract as function contract.
+     - do not print anything if this is a contract node
+  *)
+  let print_machine_alloc_decl fmt m =
+    Mod.print_machine_decl_prefix fmt m;
+    if not (fst (get_stateless_status m)) then
+      if !Options.static_mem then
+        (* Static allocation *)
+        let macro = (m, mk_attribute m, mk_instance m) in
+        fprintf fmt "%a@,%a@,%a"
+          print_static_declare_macro macro
+          print_static_link_macro macro
+          print_static_alloc_macro macro
       else
-	begin 
-          (* Dynamic allocation *)
-	  fprintf fmt "extern %a;@.@."
-	    print_alloc_prototype (m.mname.node_id, m.mstatic);
-
-	  fprintf fmt "extern %a;@.@."
-	    print_dealloc_prototype m.mname.node_id
-	end
-    end
-
-let print_machine_decl_from_header fmt inode =
-  (*Mod.print_machine_decl_prefix fmt m;*)
-  if inode.nodei_prototype = Some "C" then
-    if inode.nodei_stateless then
-      begin
-	fprintf fmt "extern %a;@.@."
-	  print_stateless_C_prototype
-	  (inode.nodei_id, inode.nodei_inputs, inode.nodei_outputs)
-      end
-    else (Format.eprintf "internal error: print_machine_decl_from_header"; assert false)
-  else
-    if inode.nodei_stateless then
-    begin
-      fprintf fmt "extern %a;@.@."
-	print_stateless_prototype 
-	(inode.nodei_id, inode.nodei_inputs, inode.nodei_outputs)
-    end
-    else 
-      begin
-	let static_inputs = List.filter (fun v -> v.var_dec_const) inode.nodei_inputs in
-	let used name =
-	  (List.exists (fun v -> v.var_id = name) inode.nodei_inputs)
-	  || (List.exists (fun v -> v.var_id = name) inode.nodei_outputs) in
-	let self = mk_new_name used "self" in
-	fprintf fmt "extern %a;@.@."
-	  (print_reset_prototype self) (inode.nodei_id, static_inputs);
-
-	fprintf fmt "extern %a;@.@."
-	  (print_init_prototype self) (inode.nodei_id, static_inputs);
-
-	fprintf fmt "extern %a;@.@."
-	  (print_clear_prototype self) (inode.nodei_id, static_inputs);
-
-	fprintf fmt "extern %a;@.@."
-	  (print_step_prototype self)
-	  (inode.nodei_id, inode.nodei_inputs, inode.nodei_outputs)
+        (* Dynamic allocation *)
+        fprintf fmt "extern %a;@,extern %a"
+          print_alloc_prototype (m.mname.node_id, m.mstatic)
+          print_dealloc_prototype m.mname.node_id
+
+  let print_machine_struct_top_decl_from_header fmt tdecl =
+    let inode = imported_node_of_top tdecl in
+    if not inode.nodei_stateless then
+      (* Declare struct *)
+      fprintf fmt "%a;"
+        pp_machine_memtype_name inode.nodei_id
+
+  let print_stateless_C_prototype fmt (name, inputs, outputs) =
+    let output =
+      match outputs with
+      | [hd] -> hd
+      | _ -> assert false
+    in
+    fprintf fmt "%a %s %a"
+      (pp_basic_c_type ~var_opt:None) output.var_type
+      name
+      (pp_print_parenthesized pp_c_decl_input_var) inputs
+
+  let print_machine_decl_top_decl_from_header fmt tdecl =
+    let inode = imported_node_of_top tdecl in
+    (*Mod.print_machine_decl_prefix fmt m;*)
+    let prototype = (inode.nodei_id, inode.nodei_inputs, inode.nodei_outputs) in
+    if inode.nodei_prototype = Some "C" then
+      if inode.nodei_stateless then
+        fprintf fmt "extern %a;" print_stateless_C_prototype prototype
+      else begin
+        (* TODO: raise proper error *)
+        Format.eprintf "internal error: print_machine_decl_top_decl_from_header";
+        assert false
       end
+    else if inode.nodei_stateless then
+      fprintf fmt "extern %a;" print_stateless_prototype prototype
+    else
+      let static_inputs = List.filter (fun v -> v.var_dec_const)
+          inode.nodei_inputs in
+      let used name =
+        List.exists (fun v -> v.var_id = name)
+          (inode.nodei_inputs @ inode.nodei_outputs) in
+      let self = mk_new_name used "self" in
+      let static_prototype = (inode.nodei_id, static_inputs) in
+      fprintf fmt
+        "extern %a;@,\
+         extern %a;@,\
+         extern %a;@,\
+         extern %a;"
+        (print_reset_prototype self) static_prototype
+        (print_init_prototype self) static_prototype
+        (print_clear_prototype self) static_prototype
+        (print_step_prototype self) prototype
+
+  let print_const_top_decl fmt tdecl =
+    let cdecl = const_of_top tdecl in
+    fprintf fmt "extern %a;"
+      (pp_c_type cdecl.const_id)
+      (if !Options.mpfr && Types.(is_real_type (array_base_type cdecl.const_type))
+       then Types.dynamic_type cdecl.const_type
+       else cdecl.const_type)
 
-let print_const_decl fmt cdecl =
-  if !Options.mpfr &&  Types.is_real_type (Types.array_base_type cdecl.const_type)
-  then
-    fprintf fmt "extern %a;@." 
-      (pp_c_type cdecl.const_id) (Types.dynamic_type cdecl.const_type) 
-  else
-    fprintf fmt "extern %a;@." 
-      (pp_c_type cdecl.const_id) cdecl.const_type
-
-let rec pp_c_struct_type_field filename cpt fmt (label, tdesc) =
-   fprintf fmt "%a;" (pp_c_type_decl filename cpt label) tdesc
-and pp_c_type_decl filename cpt var fmt tdecl =
-  match tdecl with
-  | Tydec_any           -> assert false
-  | Tydec_int           -> fprintf fmt "int %s" var
-  | Tydec_real when !Options.mpfr
-                        -> fprintf fmt "%s %s" Mpfr.mpfr_t var
-  | Tydec_real          -> fprintf fmt "double %s" var
-  (* | Tydec_float         -> fprintf fmt "float %s" var *)
-  | Tydec_bool          -> fprintf fmt "_Bool %s" var
-  | Tydec_clock ty      -> pp_c_type_decl filename cpt var fmt ty
-  | Tydec_const c       -> fprintf fmt "%s %s" c var
-  | Tydec_array (d, ty) -> fprintf fmt "%a[%a]" (pp_c_type_decl filename cpt var) ty pp_c_dimension d
-  | Tydec_enum tl ->
-    begin
+  let rec pp_c_type_decl filename cpt var fmt tdecl =
+    match tdecl with
+    | Tydec_any ->
+      assert false
+    | Tydec_int ->
+      fprintf fmt "int %s" var
+    | Tydec_real when !Options.mpfr ->
+      fprintf fmt "%s %s" Mpfr.mpfr_t var
+    | Tydec_real ->
+      fprintf fmt "double %s" var
+    (* | Tydec_float         -> fprintf fmt "float %s" var *)
+    | Tydec_bool ->
+      fprintf fmt "_Bool %s" var
+    | Tydec_clock ty ->
+      pp_c_type_decl filename cpt var fmt ty
+    | Tydec_const c ->
+      fprintf fmt "%s %s" c var
+    | Tydec_array (d, ty) ->
+      fprintf fmt "%a[%a]" (pp_c_type_decl filename cpt var) ty pp_c_dimension d
+    | Tydec_enum tl ->
       incr cpt;
-      fprintf fmt "enum _enum_%s_%d { %a } %s" (protect_filename filename) !cpt (Utils.fprintf_list ~sep:", " pp_print_string) tl var
-    end
-  | Tydec_struct fl ->
-    begin
+      fprintf fmt "enum _enum_%s_%d %a %s" (protect_filename filename) !cpt
+        (pp_print_braced pp_print_string) tl var
+    | Tydec_struct fl ->
       incr cpt;
-      fprintf fmt "struct _struct_%s_%d { %a } %s" (protect_filename filename) !cpt (Utils.fprintf_list ~sep:" " (pp_c_struct_type_field filename cpt)) fl var
-    end
-
-let print_type_definitions fmt filename =
-  let cpt_type = ref 0 in
-  Hashtbl.iter (fun typ decl ->
-		match typ with
-		| Tydec_const var ->
-		   (match decl.top_decl_desc with
-		    | TypeDef tdef ->
-		       fprintf fmt "typedef %a;@.@."
-			       (pp_c_type_decl filename cpt_type var) tdef.tydef_desc
-		    | _ -> assert false)
-		| _        -> ()) type_table
-
-let reset_type_definitions, print_type_definition_from_header =
-  let cpt_type = ref 0 in
-  (fun () -> cpt_type := 0),
-  (fun fmt typ filename ->
-     fprintf fmt "typedef %a;@.@."
-	     (pp_c_type_decl filename cpt_type typ.tydef_id) typ.tydef_desc)
+      fprintf fmt "struct _struct_%s_%d %a %s" (protect_filename filename) !cpt
+        (pp_print_braced ~pp_sep:pp_print_semicolon
+           (fun fmt (label, tdesc) -> pp_c_type_decl filename cpt label fmt tdesc))
+        fl var
 
-(********************************************************************************************)
-(*                         MAIN Header Printing functions                                   *)
-(********************************************************************************************)
-(* Seems not used
-
-let print_header header_fmt basename prog machines dependencies =
-  (* Include once: start *)
-  let baseNAME = file_to_module_name basename in
-  begin
-    (* Print the version number and the supported C standard (C90 or C99) *)
-    print_version header_fmt;
-    fprintf header_fmt "#ifndef _%s@.#define _%s@." baseNAME baseNAME;
-    pp_print_newline header_fmt ();
-    fprintf header_fmt "/* Imports standard library */@.";
-    (* imports standard library definitions (arrow) *)
-    print_import_standard header_fmt;
-    pp_print_newline header_fmt ();
-    (* imports dependencies *)
-    fprintf header_fmt "/* Import dependencies */@.";
-    fprintf header_fmt "@[<v>";
-    List.iter (print_import_prototype header_fmt) dependencies;
-    fprintf header_fmt "@]@.";
-    fprintf header_fmt "/* Types definitions */@.";
-    (* Print the type definitions from the type table *)
-    print_type_definitions header_fmt basename;
-    pp_print_newline header_fmt ();
-    (* Print the global constant declarations. *)
-    fprintf header_fmt "/* Global constant (declarations, definitions are in C file) */@.";
-    List.iter (fun c -> print_const_decl header_fmt (const_of_top c)) (get_consts prog);
-    pp_print_newline header_fmt ();
-    if !Options.mpfr then
-      begin
-	fprintf header_fmt "/* Global initialization declaration */@.";
-	fprintf header_fmt "extern %a;@.@."
-	  print_global_init_prototype baseNAME;
-	
-	fprintf header_fmt "/* Global clear declaration */@.";
-	fprintf header_fmt "extern %a;@.@."
-	  print_global_clear_prototype baseNAME;
-      end;
-    (* Print the struct declarations of all machines. *)
-    fprintf header_fmt "/* Structs declarations */@.";
-    List.iter (print_machine_struct machines header_fmt) machines;
-    pp_print_newline header_fmt ();
-    (* Print the prototypes of all machines *)
-    fprintf header_fmt "/* Nodes declarations */@.";
-    List.iter (print_machine_decl header_fmt) machines;
-    pp_print_newline header_fmt ();
-    (* Include once: end *)
-    fprintf header_fmt "#endif@.";
-    pp_print_newline header_fmt ()
-  end
-  *)
-let print_alloc_header header_fmt basename _prog machines dependencies spec =
-  (* Include once: start *)
-  let baseNAME = file_to_module_name basename in
-  begin
-    (* Print the svn version number and the supported C standard (C90 or C99) *)
-    print_version header_fmt;
-    fprintf header_fmt "#ifndef _%s_alloc@.#define _%s_alloc@." baseNAME baseNAME;
-    pp_print_newline header_fmt ();
-    (* Import the header *)
-    fprintf header_fmt "/* Import header from %s */@." basename;
-    fprintf header_fmt "@[<v>";
-    print_import_prototype header_fmt {local=true; name=basename; content=[]; is_stateful=true} (* assuming it is staful *);
-    fprintf header_fmt "@]@.";
-    fprintf header_fmt "/* Import dependencies */@.";
-    fprintf header_fmt "@[<v>";
-    List.iter (print_import_alloc_prototype header_fmt) dependencies;
-    fprintf header_fmt "@]@.";
-    (* Print the struct definitions of all machines. *)
-    fprintf header_fmt "/* Struct definitions */@.";
-    List.iter (print_machine_struct header_fmt) machines;
-    pp_print_newline header_fmt ();
-    fprintf header_fmt "/* Specification */@.%a@." C_backend_spec.pp_acsl_preamble spec;
-    (* Print the prototypes of all machines *)
-    fprintf header_fmt "/* Node allocation function/macro prototypes */@.";
-    List.iter (print_machine_alloc_decl header_fmt) machines;
-    pp_print_newline header_fmt ();
-    (* Include once: end *)
-    fprintf header_fmt "#endif@.";
-    pp_print_newline header_fmt ()
-  end
-
-(* Function called when compiling a lusi file and generating the associated C
-   header. *)
-let print_header_from_header header_fmt basename header =
-  (* Include once: start *)
-  let baseNAME = file_to_module_name basename in
-  let types = get_typedefs header in
-  let consts = get_consts header in
-  let nodes = get_imported_nodes header in
-  let dependencies = get_dependencies header in
-  begin
-    (* Print the version number and the supported C standard (C90 or C99) *)
-    print_version header_fmt;
-    fprintf header_fmt "#ifndef _%s@.#define _%s@." baseNAME baseNAME;
-    pp_print_newline header_fmt ();
-    fprintf header_fmt "/* Imports standard library */@.";
-    (* imports standard library definitions (arrow) *)
-    print_import_standard header_fmt;
-    pp_print_newline header_fmt ();
-    (* imports dependencies *)
-    fprintf header_fmt "/* Import dependencies */@.";
-    fprintf header_fmt "@[<v>";
-    List.iter
-      (fun dep -> 
-	let (local, s) = dependency_of_top dep in 
-	print_import_prototype header_fmt {local=local; name=s; content=[]; is_stateful=true} (* assuming it is stateful *))
-      dependencies;
-    fprintf header_fmt "@]@.";
-    fprintf header_fmt "/* Types definitions */@.";
-    (* Print the type definitions from the type table *)
+  (* let print_type_definitions fmt filename =
+   *   let cpt_type = ref 0 in
+   *   Hashtbl.iter (fun typ decl ->
+   *       match typ with
+   *       | Tydec_const var ->
+   *         begin match decl.top_decl_desc with
+   *           | TypeDef tdef ->
+   *             fprintf fmt "typedef %a;@.@."
+   *               (pp_c_type_decl filename cpt_type var) tdef.tydef_desc
+   *           | _ -> assert false
+   *         end
+   *       | _ -> ()) type_table *)
+
+  let reset_type_definitions, print_type_definition_top_decl_from_header =
+    let cpt_type = ref 0 in
+    (fun () -> cpt_type := 0),
+    (fun filename fmt tdecl ->
+       let typ = typedef_of_top tdecl in
+       fprintf fmt "typedef %a;"
+         (pp_c_type_decl filename cpt_type typ.tydef_id) typ.tydef_desc)
+
+  (********************************************************************************************)
+  (*                         MAIN Header Printing functions                                   *)
+  (********************************************************************************************)
+
+  let print_alloc_header header_fmt basename _prog machines dependencies spec =
+    (* Include once: start *)
+    let baseNAME = file_to_module_name basename in
+    fprintf header_fmt
+      "@[<v>\
+       %a@,\
+       #ifndef _%s_alloc@,\
+       #define _%s_alloc@,\
+       @,\
+       /* Import header from %s */@,\
+       %a@,\
+       @,\
+       %a\
+       %a\
+       %a\
+       %a\
+       #endif\
+       @]"
+
+      (* Print the svn version number and the supported C standard (C90 or C99) *)
+      pp_print_version ()
+
+      baseNAME baseNAME
+
+      (* Import the header *)
+      basename
+      print_import_prototype
+      {
+        local = true;
+        name = basename;
+        content = [];
+        is_stateful = true  (* assuming it is staful *);
+      }
+
+      (* Print dependencies *)
+      (pp_print_list
+         ~pp_open_box:pp_open_vbox0
+         ~pp_prologue:(pp_print_endcut "/* Import dependencies */")
+         print_import_alloc_prototype
+         ~pp_epilogue:pp_print_cutcut) dependencies
+
+      (* Print the struct definitions of all machines. *)
+      (pp_print_list
+         ~pp_open_box:pp_open_vbox0
+         ~pp_prologue:(pp_print_endcut "/* Struct definitions */")
+         ~pp_sep:pp_print_cutcut
+         print_machine_struct
+         ~pp_epilogue:pp_print_cutcut) machines
+
+      (* Print specification *)
+      C_backend_spec.pp_acsl_preamble spec
+
+      (* Print the prototypes of all machines *)
+      (pp_print_list
+         ~pp_open_box:pp_open_vbox0
+         ~pp_prologue:(pp_print_endcut
+                         "/* Node allocation function/macro prototypes */")
+         ~pp_sep:pp_print_cutcut
+         print_machine_alloc_decl
+         ~pp_epilogue:pp_print_cutcut) machines
+  (* Include once: end *)
+
+  (* Function called when compiling a lusi file and generating the associated C
+     header. *)
+  let print_header_from_header header_fmt basename header =
+    (* Include once: start *)
+    let baseNAME = file_to_module_name basename in
+    let types = get_typedefs header in
+    let consts = get_consts header in
+    let nodes = get_imported_nodes header in
+    let dependencies = get_dependencies header in
     reset_type_definitions ();
-    List.iter (fun typ -> print_type_definition_from_header header_fmt (typedef_of_top typ) basename) types;
-    pp_print_newline header_fmt ();
-    (* Print the global constant declarations. *)
-    fprintf header_fmt "/* Global constant (declarations, definitions are in C file) */@.";
-    List.iter (fun c -> print_const_decl header_fmt (const_of_top c)) consts;
-    pp_print_newline header_fmt ();
-    if !Options.mpfr then
-      begin
-	fprintf header_fmt "/* Global initialization declaration */@.";
-	fprintf header_fmt "extern %a;@.@."
-	  print_global_init_prototype baseNAME;
-	
-	fprintf header_fmt "/* Global clear declaration */@.";
-	fprintf header_fmt "extern %a;@.@."
-	  print_global_clear_prototype baseNAME;
-      end;
-    (* Print the struct declarations of all machines. *)
-    fprintf header_fmt "/* Structs declarations */@.";
-    List.iter (fun node -> print_machine_struct_from_header header_fmt (imported_node_of_top node)) nodes;
-    pp_print_newline header_fmt ();
-    (* Print the prototypes of all machines *)
-    fprintf header_fmt "/* Nodes declarations */@.";
-    List.iter (fun node -> print_machine_decl_from_header header_fmt (imported_node_of_top node)) nodes;
-    pp_print_newline header_fmt ();
-    (* Include once: end *)
-    fprintf header_fmt "#endif@.";
-    pp_print_newline header_fmt ()
-  end
+    fprintf header_fmt
+      "@[<v>\
+       %a@,\
+       #ifndef _%s@,\
+       #define _%s@,\
+       @,\
+       /* Import standard library */@,\
+       %a@,\
+       @,\
+       %a\
+       %a\
+       %a\
+       %a\
+       %a\
+       %a\
+       #endif\
+       @]@."
+
+      (* Print the version number and the supported C standard (C90 or C99) *)
+      pp_print_version ()
+
+      baseNAME baseNAME
+
+      (* imports standard library definitions (arrow) *)
+      print_import_standard ()
+
+      (* imports dependencies *)
+      (pp_print_list
+         ~pp_open_box:pp_open_vbox0
+         ~pp_prologue:(pp_print_endcut "/* Import dependencies */")
+         (fun fmt dep ->
+            let local, name = dependency_of_top dep in
+            print_import_prototype fmt
+              {
+                local;
+                name;
+                content = [];
+                is_stateful = true (* assuming it is stateful *)
+              })
+         ~pp_epilogue:pp_print_cutcut)
+      dependencies
+
+      (* Print the type definitions from the type table *)
+      (pp_print_list
+         ~pp_open_box:pp_open_vbox0
+         ~pp_prologue:(pp_print_endcut "/* Types definitions */")
+         (print_type_definition_top_decl_from_header basename)
+         ~pp_epilogue:pp_print_cutcut)
+      types
+
+      (* Print the global constant declarations. *)
+      (pp_print_list
+         ~pp_open_box:pp_open_vbox0
+         ~pp_prologue:
+           (pp_print_endcut
+              "/* Global constants (declarations, definitions are in C file) */")
+         print_const_top_decl
+         ~pp_epilogue:pp_print_cutcut)
+      consts
+
+      (* MPFR *)
+      (if !Options.mpfr then
+         fun fmt () -> fprintf fmt
+             "/* Global initialization declaration */@,\
+              extern %a;@,@,\
+              /* Global clear declaration */@,\
+              extern %a;@,@,"
+             print_global_init_prototype baseNAME
+             print_global_clear_prototype baseNAME
+       else pp_print_nothing) ()
+
+      (* Print the struct declarations of all machines. *)
+      (pp_print_list
+         ~pp_open_box:pp_open_vbox0
+         ~pp_prologue:(pp_print_endcut "/* Struct declarations */")
+         print_machine_struct_top_decl_from_header
+         ~pp_epilogue:pp_print_cutcut)
+      nodes
+
+      (* Print the prototypes of all machines *)
+      (pp_print_list
+         ~pp_open_box:pp_open_vbox0
+         ~pp_prologue:(pp_print_endcut "/* Nodes declarations */")
+         ~pp_sep:pp_print_cutcut
+         print_machine_decl_top_decl_from_header
+         ~pp_epilogue:pp_print_cutcut)
+      nodes
 
 end
 (* Local Variables: *)
diff --git a/src/backends/C/c_backend_lusic.ml b/src/backends/C/c_backend_lusic.ml
index 0088c7f4..a0e037ad 100644
--- a/src/backends/C/c_backend_lusic.ml
+++ b/src/backends/C/c_backend_lusic.ml
@@ -1,18 +1,17 @@
 open Lusic
+open Utils.Format
 
 let print_lusic_to_h basename extension =
-let module HeaderMod = C_backend_header.EmptyMod in
-let module Header = C_backend_header.Main (HeaderMod) in
+  let module HeaderMod = C_backend_header.EmptyMod in
+  let module Header = C_backend_header.Main (HeaderMod) in
   let lusic = read_lusic basename extension in
   let header_name = basename ^ ".h" in
-  let h_out = open_out header_name in
-  let h_fmt = Format.formatter_of_out_channel h_out in
-  begin
-    assert (not lusic.obsolete);
-    (*Format.eprintf "lusic to h: %i items.@." (List.length lusic.contents);*)
-    (* Typing.uneval_prog_generics lusic.contents;
+  with_out_file header_name @@ fun h_fmt ->
+  assert (not lusic.obsolete);
+  (*Format.eprintf "lusic to h: %i items.@." (List.length lusic.contents);*)
+  (* Typing.uneval_prog_generics lusic.contents;
      * Clock_calculus.uneval_prog_generics lusic.contents; *)
-    Header.print_header_from_header h_fmt (Filename.basename basename) lusic.contents;
-    close_out h_out
-  end
-
+  Header.print_header_from_header
+    h_fmt
+    (Filename.basename basename)
+    lusic.contents
diff --git a/src/backends/C/c_backend_main.ml b/src/backends/C/c_backend_main.ml
index 040c68c4..86dacb65 100644
--- a/src/backends/C/c_backend_main.ml
+++ b/src/backends/C/c_backend_main.ml
@@ -12,209 +12,375 @@
 open Lustre_types
 open Machine_code_types
 open Machine_code_common
-open Format
+open Utils.Format
 open C_backend_common
 open Utils
 
-module type MODIFIERS_MAINSRC =
-sig
+module type MODIFIERS_MAINSRC = sig
 end
 
-module EmptyMod =
-struct
+module EmptyMod = struct
 end
 
-module Main = functor (Mod: MODIFIERS_MAINSRC) -> 
-struct
+module Main = functor (Mod: MODIFIERS_MAINSRC) -> struct
 
-(********************************************************************************************)
-(*                         Main related functions                                           *)
-(********************************************************************************************)
+  (********************************************************************************************)
+  (*                         Main related functions                                           *)
+  (********************************************************************************************)
 
+  let pp_c_main_var_input fmt id =
+    fprintf fmt "%s" id.var_id
 
-let print_put_outputs fmt m = 
-  let po fmt (id, o', o) =
-    let suff = string_of_int id in
+  let pp_c_main_var_output fmt id =
+    if Types.is_address_type id.var_type
+    then
+      fprintf fmt "%s" id.var_id
+    else
+      fprintf fmt "&%s" id.var_id
+
+  let print_put_output fmt id o' o =
+    let suff = string_of_int (id + 1) in
     print_put_var fmt suff o'.var_id o.var_type o.var_id
-  in
-  List.iteri2 (fun idx v' v -> fprintf fmt "@ %a;" po ((idx+1), v', v)) m.mname.node_outputs m.mstep.step_outputs
-
-  
-let print_main_inout_declaration m fmt =
-  fprintf fmt "/* Declaration of inputs/outputs variables */@ ";
-  List.iteri (fun idx v ->
-      fprintf fmt "%a;@ " (pp_c_type v.var_id) v.var_type;
-      ignore (pp_file_decl fmt "in" idx) 
-    ) m.mstep.step_inputs;
-  List.iteri (fun idx v ->
-      fprintf fmt "%a;@ " (pp_c_type v.var_id) v.var_type;
-      ignore (pp_file_decl fmt "out" idx)
-    ) m.mstep.step_outputs;
-  fprintf fmt "@[<v 2>if (traces) {@ ";
-  List.iteri (fun idx _ ->
-      ignore (pp_file_open fmt "in" idx) 
-    ) m.mstep.step_inputs;
-  List.iteri (fun idx _ ->
-      ignore (pp_file_open fmt "out" idx)
-    ) m.mstep.step_outputs;
-  fprintf fmt "@]}@ "
-
-  
-let print_main_memory_allocation mname main_mem fmt m =
-  if not (fst (get_stateless_status m)) then
-  begin  
-    fprintf fmt "@ /* Main memory allocation */@ ";
-    if (!Options.static_mem && !Options.main_node <> "")
-    then (fprintf fmt "%a(static,main_mem);@ " pp_machine_static_alloc_name mname)
-    else (fprintf fmt "%a *main_mem = %a();@ " pp_machine_memtype_name mname pp_machine_alloc_name mname);
-    fprintf fmt "@ /* Initialize the main memory */@ ";
-    fprintf fmt "%a(%s);@ " pp_machine_reset_name mname main_mem;
-  end
-
-let print_global_initialize fmt basename =
-  let mNAME = file_to_module_name basename in
-  fprintf fmt "@ /* Initialize global constants */@ %a();@ "
-    pp_global_init_name mNAME
-
-let print_global_clear fmt basename =
-  let mNAME = file_to_module_name basename in
-  fprintf fmt "@ /* Clear global constants */@ %a();@ "
-    pp_global_clear_name mNAME
-
-let print_main_initialize mname main_mem fmt m =
-  if not (fst (get_stateless_status m))
-  then
-    fprintf fmt "@ /* Initialize inputs, outputs and memories */@ %a%t%a%t%a(%s);@ "
-      (Utils.fprintf_list ~sep:"@ " (pp_initialize m main_mem (pp_c_var_read m))) m.mstep.step_inputs
-      (Utils.pp_newline_if_non_empty m.mstep.step_inputs)
-      (Utils.fprintf_list ~sep:"@ " (pp_initialize m main_mem (pp_c_var_read m))) m.mstep.step_outputs
-      (Utils.pp_newline_if_non_empty m.mstep.step_inputs)
-      pp_machine_init_name mname
-      main_mem
-  else
-    fprintf fmt "@ /* Initialize inputs and outputs */@ %a%t%a@ "
-      (Utils.fprintf_list ~sep:"@ " (pp_initialize m main_mem (pp_c_var_read m))) m.mstep.step_inputs
-      (Utils.pp_newline_if_non_empty m.mstep.step_inputs)
-      (Utils.fprintf_list ~sep:"@ " (pp_initialize m main_mem (pp_c_var_read m))) m.mstep.step_outputs
 
-let print_main_clear mname main_mem fmt m =
-  if not (fst (get_stateless_status m))
+  let print_main_inout_declaration fmt m =
+    fprintf fmt
+      "/* Declaration of inputs/outputs variables */@,\
+       %a%a\
+       @[<v 2>if (traces) {@,\
+       %a%a@]@,\
+       }"
+      (pp_print_list_i
+         ~pp_open_box:pp_open_vbox0
+         ~pp_epilogue:pp_print_cut
+         (fun fmt idx v ->
+            fprintf fmt "%a; %a"
+              (pp_c_type v.var_id) v.var_type
+              (fun fmt () -> pp_file_decl fmt "in" idx) ())) m.mstep.step_inputs
+      (pp_print_list_i
+         ~pp_open_box:pp_open_vbox0
+         ~pp_epilogue:pp_print_cut
+         (fun fmt idx v ->
+            fprintf fmt "%a; %a"
+              (pp_c_type v.var_id) v.var_type
+              (fun fmt () -> pp_file_decl fmt "out" idx) ())) m.mstep.step_outputs
+      (pp_print_list_i
+         ~pp_epilogue:pp_print_cut
+         (fun fmt idx _ ->
+            ignore (pp_file_open fmt "in" idx))) m.mstep.step_inputs
+      (pp_print_list_i
+         (fun fmt idx _ ->
+            ignore (pp_file_open fmt "out" idx))) m.mstep.step_outputs
+
+  let print_main_memory_allocation mname main_mem fmt m =
+    if not (fst (get_stateless_status m)) then
+      fprintf fmt
+        "@[<v>/* Main memory allocation */@,\
+         %a@,\
+         @,\
+         /* Initialize the main memory */@,\
+         %a(%s);@]"
+        (fun fmt () ->
+           if !Options.static_mem && !Options.main_node <> "" then
+             fprintf fmt "%a(static,main_mem);"
+               pp_machine_static_alloc_name mname
+           else
+             fprintf fmt "%a *main_mem = %a();"
+               pp_machine_memtype_name mname
+               pp_machine_alloc_name mname) ()
+        pp_machine_reset_name mname
+        main_mem
+
+  let print_global_initialize fmt basename =
+    let mNAME = file_to_module_name basename in
+    fprintf fmt "/* Initialize global constants */@,%a();"
+      pp_global_init_name mNAME
+
+  let print_global_clear fmt basename =
+    let mNAME = file_to_module_name basename in
+    fprintf fmt "/* Clear global constants */@,%a();"
+      pp_global_clear_name mNAME
+
+  let print_main_initialize mname main_mem fmt m =
+    let inputs = mpfr_vars m.mstep.step_inputs in
+    let outputs = mpfr_vars m.mstep.step_outputs in
+    if not (fst (get_stateless_status m))
+    then
+      fprintf fmt
+        "/* Initialize inputs, outputs and memories */@,\
+         %a%a%a(%s);"
+        (pp_print_list
+           ~pp_open_box:pp_open_vbox0
+           ~pp_eol:pp_print_cut
+           (pp_initialize m main_mem (pp_c_var_read m))) inputs
+        (pp_print_list
+           ~pp_open_box:pp_open_vbox0
+           ~pp_eol:pp_print_cut
+           (pp_initialize m main_mem (pp_c_var_read m))) outputs
+        pp_machine_init_name mname
+        main_mem
+    else
+      fprintf fmt
+        "/* Initialize inputs and outputs */@,\
+         %a%a@ "
+        (pp_print_list
+           ~pp_open_box:pp_open_vbox0
+           ~pp_eol:pp_print_cut
+           (pp_initialize m main_mem (pp_c_var_read m))) inputs
+        (pp_print_list
+           ~pp_open_box:pp_open_vbox0
+           (pp_initialize m main_mem (pp_c_var_read m))) outputs
+
+  let print_main_clear mname main_mem fmt m =
+    let inputs = mpfr_vars m.mstep.step_inputs in
+    let outputs = mpfr_vars m.mstep.step_outputs in
+    if not (fst (get_stateless_status m))
+    then
+      fprintf fmt
+        "@[<v>/* Clear inputs, outputs and memories */@,\
+         %a%a%a(%s);@]"
+        (pp_print_list
+           ~pp_open_box:pp_open_vbox0
+           ~pp_eol:pp_print_cut
+           (pp_clear m main_mem (pp_c_var_read m))) inputs
+        (pp_print_list
+           ~pp_open_box:pp_open_vbox0
+           ~pp_eol:pp_print_cut
+           (pp_clear m main_mem (pp_c_var_read m))) outputs
+        pp_machine_clear_name mname
+        main_mem
+    else
+      fprintf fmt
+        "@[<v>/* Clear inputs and outputs */@,\
+         %a%a@]"
+        (pp_print_list
+           ~pp_open_box:pp_open_vbox0
+           ~pp_eol:pp_print_cut
+           (pp_clear m main_mem (pp_c_var_read m))) inputs
+        (pp_print_list
+           ~pp_open_box:pp_open_vbox0
+           (pp_clear m main_mem (pp_c_var_read m))) outputs
+
+let print_get_input fmt id v' v =
+  let pp_file = pp_print_file ("in" ^ string_of_int (id + 1)) in
+  let unclocked_t = Types.unclock_type v.var_type in
+  fprintf fmt "@[<v>%a@]"
+    (fun fmt () ->
+       if Types.is_int_type unclocked_t then
+         fprintf fmt "%s = _get_int(\"%s\");@,%a"
+           v.var_id v'.var_id
+           pp_file ("d", v.var_id)
+       else if Types.is_bool_type unclocked_t then
+         fprintf fmt "%s = _get_bool(\"%s\");@,%a"
+           v.var_id v'.var_id
+           pp_file ("i", v.var_id)
+       else if Types.is_real_type unclocked_t then
+         if !Options.mpfr then
+           fprintf fmt "double %s_tmp = _get_double(\"%s\");@,\
+                        %a@,\
+                        mpfr_set_d(%s, %s_tmp, %i);"
+             v.var_id v'.var_id
+             pp_file ("f", v.var_id ^ "_tmp")
+             v.var_id v.var_id (Mpfr.mpfr_prec ())
+         else
+           fprintf fmt "%s = _get_double(\"%s\");@,%a"
+             v.var_id v'.var_id
+             pp_file ("f", v.var_id)
+       else begin
+         Global.main_node := !Options.main_node;
+         eprintf "Code generation error: %a%a@."
+           Error.pp_error_msg Error.Main_wrong_kind
+           Location.pp_loc v'.var_loc;
+         raise (Error.Error (v'.var_loc, Error.Main_wrong_kind))
+       end) ()
+
+let pp_main_call mname self fmt m (inputs: value_t list) (outputs: var_decl list) =
+  if fst (Machine_code_common.get_stateless_status m)
   then
-    fprintf fmt "@ /* Clear inputs, outputs and memories */@ %a%t%a%t%a(%s);@ "
-      (Utils.fprintf_list ~sep:"@ " (pp_clear m main_mem (pp_c_var_read m))) m.mstep.step_inputs
-      (Utils.pp_newline_if_non_empty m.mstep.step_inputs)
-      (Utils.fprintf_list ~sep:"@ " (pp_clear m main_mem (pp_c_var_read m))) m.mstep.step_outputs
-      (Utils.pp_newline_if_non_empty m.mstep.step_inputs)
-      pp_machine_clear_name mname
-      main_mem
+    fprintf fmt "%a (%a%a);"
+      pp_machine_step_name mname
+      (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
+         (pp_c_val m self pp_c_main_var_input)) inputs
+      (pp_print_list ~pp_sep:pp_print_comma pp_c_main_var_output) outputs
   else
-    fprintf fmt "@ /* Clear inputs and outputs */@ %a%t%a@ "
-      (Utils.fprintf_list ~sep:"@ " (pp_clear m main_mem (pp_c_var_read m))) m.mstep.step_inputs
-      (Utils.pp_newline_if_non_empty m.mstep.step_inputs)
-      (Utils.fprintf_list ~sep:"@ " (pp_clear m main_mem (pp_c_var_read m))) m.mstep.step_outputs
-
-let print_main_loop mname main_mem fmt m =
-  let input_values =
-    List.map (fun v -> mk_val (Var v) v.var_type)
-      m.mstep.step_inputs in
-  begin
-    fprintf fmt "@ ISATTY = isatty(0);@ ";
-    fprintf fmt "@ /* Infinite loop */@ ";
-    fprintf fmt "@[<v 2>while(1){@ ";
-    fprintf fmt  "fflush(stdout);@ ";
-    fprintf fmt "@[<v 2>if (traces) {@ ";
-    List.iteri (fun idx _ -> fprintf fmt "fflush(f_in%i);@ " (idx+1)) m.mstep.step_inputs;
-    List.iteri (fun idx _ -> fprintf fmt "fflush(f_out%i);@ " (idx+1)) m.mstep.step_outputs;
-    fprintf fmt "@]}@ ";
-    fprintf fmt "%a@ %t%a"
-      print_get_inputs m
-      (fun fmt -> pp_main_call mname main_mem fmt m input_values m.mstep.step_outputs)
-      print_put_outputs m
-  end
-
-let print_usage fmt =
-  fprintf fmt "@[<v 2>void usage(char *argv[]) {@ ";
-  fprintf fmt "printf(\"Usage: %%s\\n\", argv[0]);@ ";
-  fprintf fmt "printf(\" -t: produce trace files for input/output flows\\n\");@ ";
-  fprintf fmt "printf(\" -d<dir>: directory containing traces (default: _traces)\\n\");@ ";
-  fprintf fmt "printf(\" -p<prefix>: prefix_simu.scope<id> (default: file_node)\\n\");@ ";
-  fprintf fmt "exit (8);@ ";
-  fprintf fmt "@]}@ "
-
-let print_options fmt name =
-  fprintf fmt "int traces = 0;@ ";
-  fprintf fmt "char* prefix = \"%s\";@ " name;
-  fprintf fmt "char* dir = \".\";@ ";
-  fprintf fmt "@[<v 2>while ((argc > 1) && (argv[1][0] == '-')) {@ ";
-  fprintf fmt "@[<v 2>switch (argv[1][1]) {@ ";
-  fprintf fmt "@[<v 2>case 't':@ ";
-  fprintf fmt "traces = 1;@ ";
-  fprintf fmt "break;@ ";
-  fprintf fmt "@]@ ";
-  fprintf fmt "@[<v 2>case 'd':@ ";
-  fprintf fmt "dir = &argv[1][2];@ ";
-  fprintf fmt "break;@ ";
-  fprintf fmt "@]@ ";
-  fprintf fmt "@[<v 2>case 'p':@ ";
-  fprintf fmt "prefix = &argv[1][2];@ ";
-  fprintf fmt "break;@ ";
-  fprintf fmt "@]@ ";
-  fprintf fmt "@[<v 2>default:@ ";
-  fprintf fmt "printf(\"Wrong Argument: %%s\\n\", argv[1]);@ ";
-  fprintf fmt "usage(argv);@ ";
-  fprintf fmt "@]@ ";
-  fprintf fmt "@]}@ ";
-  fprintf fmt "++argv;@ ";
-  fprintf fmt "--argc;@ ";
-  fprintf fmt "@]}@ "
-  
-let print_main_code fmt basename m =
-  let mname = m.mname.node_id in
-  (* TODO: find a proper way to shorthen long names. This causes segfault in the binary when trying to fprintf in them *)
-  let mname = if String.length mname > 50 then string_of_int (Hashtbl.hash mname) else mname in
-  
-  let main_mem =
-    if (!Options.static_mem && !Options.main_node <> "")
-    then "&main_mem"
-    else "main_mem" in
-  print_usage fmt;
-  
-  fprintf fmt "@[<v 2>int main (int argc, char *argv[]) {@ ";
-  print_options fmt (basename ^ "_" ^ mname);
-  print_main_inout_declaration m fmt;
-  Plugins.c_backend_main_loop_body_prefix basename mname fmt ();
-  print_main_memory_allocation mname main_mem fmt m;
-  if !Options.mpfr then
-    begin
-      print_global_initialize fmt basename;
-      print_main_initialize mname main_mem fmt m;
-    end;
-  print_main_loop mname main_mem fmt m;
-
-  Plugins.c_backend_main_loop_body_suffix fmt ();
-  fprintf fmt "@]@ }@ @ ";
-  if !Options.mpfr then
-    begin
-      print_main_clear mname main_mem fmt m;
-      print_global_clear fmt basename;
-    end;
-  fprintf fmt "@ return 1;";
-  fprintf fmt "@]@ }@."       
-
-let print_main_header fmt =
-  fprintf fmt (if !Options.cpp then "#include <stdio.h>@.#include <unistd.h>@.#include \"%s/io_frontend.hpp\"@." else "#include <stdio.h>@.#include <unistd.h>@.#include <string.h>@.#include \"%s/io_frontend.h\"@.")
-    (Options_management.core_dependency "io_frontend")
-
-let print_main_c main_fmt main_machine basename _prog _machines _dependencies =
-  print_main_header main_fmt;
-  fprintf main_fmt "#include <stdlib.h>@.#include <assert.h>@.";
-  print_import_alloc_prototype main_fmt {local=true; name=basename; content=[]; is_stateful=true} (* assuming it is stateful*) ;
-  pp_print_newline main_fmt ();
-
-  (* Print the svn version number and the supported C standard (C90 or C99) *)
-  print_version main_fmt;
-  print_main_code main_fmt basename main_machine
-end  
+    fprintf fmt "%a (%a%a%s);"
+      pp_machine_step_name mname
+      (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
+         (pp_c_val m self pp_c_main_var_input)) inputs
+      (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
+         pp_c_main_var_output) outputs
+      self
+
+  let print_main_loop mname main_mem fmt m =
+    let input_values = List.map (fun v ->
+        mk_val (Var v) v.var_type) m.mstep.step_inputs in
+    fprintf fmt
+      "ISATTY = isatty(0);@,\
+       @,\
+       /* Infinite loop */@,\
+       @[<v 2>while(1){@,\
+       fflush(stdout);@,\
+       @[<v 2>if (traces) {@,\
+       %a%a\
+       @]@,\
+       }@,\
+       %a%a%a"
+
+      (pp_print_list_i
+        ~pp_open_box:pp_open_vbox0
+        ~pp_epilogue:pp_print_cut
+         (fun fmt idx _ -> fprintf fmt "fflush(f_in%i);" (idx + 1)))
+      m.mstep.step_inputs
+
+      (pp_print_list_i
+        ~pp_open_box:pp_open_vbox0
+         (fun fmt idx _ -> fprintf fmt "fflush(f_out%i);" (idx + 1)))
+      m.mstep.step_outputs
+
+      (pp_print_list_i2
+        ~pp_open_box:pp_open_vbox0
+        ~pp_epilogue:pp_print_cut
+         print_get_input)
+      (m.mname.node_inputs, m.mstep.step_inputs)
+
+      (fun fmt () ->
+         pp_main_call mname main_mem fmt m input_values m.mstep.step_outputs) ()
+
+      (pp_print_list_i2
+         ~pp_open_box:pp_open_vbox0
+         ~pp_prologue:pp_print_cut
+         print_put_output)
+      (m.mname.node_outputs, m.mstep.step_outputs)
+
+  let print_usage fmt () =
+    fprintf fmt
+      "@[<v 2>\
+       void usage(char *argv[]) {@,\
+       printf(\"Usage: %%s\\n\", argv[0]);@,\
+       printf(\" -t: produce trace files for input/output flows\\n\");@,\
+       printf(\" -d<dir>: directory containing traces (default: _traces)\\n\");@,\
+       printf(\" -p<prefix>: prefix_simu.scope<id> (default: file_node)\\n\");@,\
+       exit (8);@]@,\
+       }"
+
+  let print_options fmt name =
+    fprintf fmt
+      "@[<v>int traces = 0;@,\
+       char* prefix = \"%s\";@,\
+       char* dir = \".\";@,\
+       @[<v 2>while ((argc > 1) && (argv[1][0] == '-')) {@,\
+       @[<v 2>switch (argv[1][1]) {@,\
+       @[<v 2>case 't':@,\
+       traces = 1;@,\
+       break;@,\
+       @]@,\
+       @[<v 2>case 'd':@,\
+       dir = &argv[1][2];@,\
+       break;@,\
+       @]@,\
+       @[<v 2>case 'p':@,\
+       prefix = &argv[1][2];@,\
+       break;@,\
+       @]@,\
+       @[<v 2>default:@,\
+       printf(\"Wrong Argument: %%s\\n\", argv[1]);@,\
+       usage(argv);@]@]@,\
+       }@,\
+       ++argv;@,\
+       --argc;@]@,\
+       }@]"
+      name
+
+  let print_main_code fmt (basename, m) =
+    let mname = m.mname.node_id in
+    (* TODO: find a proper way to shorthen long names. This causes segfault in the binary when trying to fprintf in them *)
+    let mname = if String.length mname > 50
+      then string_of_int (Hashtbl.hash mname) else mname in
+    let main_mem =
+      if !Options.static_mem && !Options.main_node <> ""
+      then "&main_mem"
+      else "main_mem" in
+
+    fprintf fmt
+      "@[<v>\
+       %a@,\
+       @,\
+       @[<v 2>int main (int argc, char *argv[]) {@,\
+       %a@,\
+       @,\
+       %a@,\
+       %a@,\
+       %a@,\
+       %a@,\
+       %a@,\
+       %a@]@,\
+       }@,\
+       %areturn 1;@]@,}@]@."
+
+      print_usage ()
+
+      print_options (basename ^ "_" ^ mname)
+
+      print_main_inout_declaration m
+
+      (Plugins.c_backend_main_loop_body_prefix basename mname) ()
+
+      (print_main_memory_allocation mname main_mem) m
+
+      (fun fmt () ->
+         if !Options.mpfr then
+           fprintf fmt "@[<v>%a@,%a@]@,"
+             print_global_initialize basename
+             (print_main_initialize mname main_mem) m) ()
+
+      (print_main_loop mname main_mem) m
+
+      Plugins.c_backend_main_loop_body_suffix ()
+
+      (fun fmt () ->
+         if !Options.mpfr then
+           fprintf fmt "@[<v>%a@,%a@]@,"
+             (print_main_clear mname main_mem) m
+             print_global_clear basename) ()
+
+  let print_main_header fmt () =
+    fprintf fmt
+      "@[<v>#include <stdio.h>@,\
+       #include <unistd.h>@,\
+       %a@]"
+      (fun fmt () -> fprintf fmt
+          (if !Options.cpp then
+             "#include \"%s/io_frontend.hpp\""
+           else
+             "#include <string.h>@,\
+              #include \"%s/io_frontend.h\"")
+          (Options_management.core_dependency "io_frontend")) ()
+
+  let print_main_c main_fmt main_machine basename _prog _machines _dependencies =
+    fprintf main_fmt
+      "@[<v>\
+       %a@,\
+       #include <stdlib.h>@,\
+       #include <assert.h>@,\
+       %a@,\
+       @,\
+       %a@,\
+       %a
+       @]@."
+      print_main_header ()
+      print_import_alloc_prototype
+      {
+        local = true;
+        name = basename;
+        content = [];
+        is_stateful = true (* assuming it is stateful*)
+      }
+
+      (* Print the svn version number and the supported C standard (C90 or C99) *)
+      pp_print_version ()
+
+      print_main_code (basename, main_machine)
+
+end
 
 (* Local Variables: *)
 (* compile-command:"make -C ../../.." *)
diff --git a/src/backends/C/c_backend_src.ml b/src/backends/C/c_backend_src.ml
index 9a26ef3f..74a73c5c 100644
--- a/src/backends/C/c_backend_src.ml
+++ b/src/backends/C/c_backend_src.ml
@@ -9,32 +9,29 @@
 (*                                                                  *)
 (********************************************************************)
 
-open Format
+open Utils.Format
 open Lustre_types
 open Machine_code_types
 open Corelang
 open Machine_code_common
 open C_backend_common
 
-module type MODIFIERS_SRC =
-sig
+module type MODIFIERS_SRC = sig
 end
 
-module EmptyMod =
-struct
+module EmptyMod = struct
 end
 
-module Main = functor (Mod: MODIFIERS_SRC) -> 
-struct
+module Main = functor (Mod: MODIFIERS_SRC) -> struct
 
-(********************************************************************************************)
-(*                    Instruction Printing functions                                        *)
-(********************************************************************************************)
+  (********************************************************************************************)
+  (*                    Instruction Printing functions                                        *)
+  (********************************************************************************************)
 
 
-(* Computes the depth to which multi-dimension array assignments should be expanded.
-   It equals the maximum number of nested static array constructions accessible from root [v].
-*)
+  (* Computes the depth to which multi-dimension array assignments should be expanded.
+     It equals the maximum number of nested static array constructions accessible from root [v].
+  *)
   let rec expansion_depth v =
     match v.value_desc with
     | Cst cst -> expansion_depth_cst cst
@@ -45,40 +42,45 @@ struct
     | Power _  -> 0 (*1 + expansion_depth v*)
   and expansion_depth_cst c = 
     match c with
-      Const_array cl -> 1 + List.fold_right (fun c -> max (expansion_depth_cst c)) cl 0
+    | Const_array cl ->
+      1 + List.fold_right (fun c -> max (expansion_depth_cst c)) cl 0
     | _ -> 0
-  
+
   let rec merge_static_loop_profiles lp1 lp2 =
     match lp1, lp2 with
     | []      , _        -> lp2
     | _       , []       -> lp1
     | p1 :: q1, p2 :: q2 -> (p1 || p2) :: merge_static_loop_profiles q1 q2
 
-(* Returns a list of bool values, indicating whether the indices must be static or not *)
+  (* Returns a list of bool values, indicating whether the indices must be static or not *)
   let rec static_loop_profile v =
     match v.value_desc with
     | Cst cst  -> static_loop_profile_cst cst
     | Var _  -> []
-    | Fun (_, vl) -> List.fold_right (fun v lp -> merge_static_loop_profiles lp (static_loop_profile v)) vl []
-    | Array vl    -> true :: List.fold_right (fun v lp -> merge_static_loop_profiles lp (static_loop_profile v)) vl []
-    | Access (v, _) -> (match (static_loop_profile v) with [] -> [] | _ :: q -> q)
-    | Power (v, _)  -> false :: static_loop_profile v
+    | Fun (_, vl) ->
+      List.fold_right
+        (fun v lp -> merge_static_loop_profiles lp (static_loop_profile v)) vl []
+    | Array vl    ->
+      true :: List.fold_right
+        (fun v lp -> merge_static_loop_profiles lp (static_loop_profile v)) vl []
+    | Access (v, _) ->
+      begin match static_loop_profile v with [] -> [] | _ :: q -> q end
+    | Power (v, _) -> false :: static_loop_profile v
   and static_loop_profile_cst cst =
     match cst with
-      Const_array cl -> List.fold_right 
-	(fun c lp -> merge_static_loop_profiles lp (static_loop_profile_cst c))
-	cl 
-	[]
+      Const_array cl ->
+      List.fold_right
+        (fun c lp -> merge_static_loop_profiles lp (static_loop_profile_cst c))
+        cl []
     | _ -> [] 
-  
-  
-let rec is_const_index v =
-  match v.value_desc with
-  | Cst (Const_int _) -> true
-  | Fun (_, vl)       -> List.for_all is_const_index vl
-  | _                 -> false
-
-type loop_index = LVar of ident | LInt of int ref | LAcc of value_t
+
+  let rec is_const_index v =
+    match v.value_desc with
+    | Cst (Const_int _) -> true
+    | Fun (_, vl)       -> List.for_all is_const_index vl
+    | _                 -> false
+
+  type loop_index = LVar of ident | LInt of int ref | LAcc of value_t
 (*
 let rec value_offsets v offsets =
  match v, offsets with
@@ -90,657 +92,888 @@ let rec value_offsets v offsets =
  | _                        , LInt r :: q -> value_offsets (Access (v, Cst (Const_int !r))) q
  | _                        , LVar i :: q -> value_offsets (Access (v, Var i)) q
 *)
-(* Computes the list of nested loop variables together with their dimension bounds.
-   - LInt r stands for loop expansion (no loop variable, but int loop index)
-   - LVar v stands for loop variable v
-*)
-let rec mk_loop_variables m ty depth =
- match (Types.repr ty).Types.tdesc, depth with
- | Types.Tarray (d, ty'), 0       ->
-   let v = mk_loop_var m () in
-   (d, LVar v) :: mk_loop_variables m ty' 0
- | Types.Tarray (d, ty'), _       ->
-   let r = ref (-1) in
-   (d, LInt r) :: mk_loop_variables m ty' (depth - 1)
- | _                    , 0       -> []
- | _                              -> assert false
-
-let reorder_loop_variables loop_vars =
-  let (int_loops, var_loops) = 
-    List.partition (function (_, LInt _) -> true | _ -> false) loop_vars
-  in
-  var_loops @ int_loops
-
-(* Prints a one loop variable suffix for arrays *)
-let pp_loop_var _ pp_val fmt lv =
- match snd lv with
- | LVar v -> fprintf fmt "[%s]" v
- | LInt r -> fprintf fmt "[%d]" !r
- | LAcc i -> fprintf fmt "[%a]" pp_val i
-
-(* Prints a suffix of loop variables for arrays *)
-let pp_suffix m pp_val fmt loop_vars =
- Utils.fprintf_list ~sep:"" (pp_loop_var m pp_val) fmt loop_vars
-
-(* Prints a value expression [v], with internal function calls only.
-   [pp_var] is a printer for variables (typically [pp_c_var_read]),
-   but an offset suffix may be added for array variables
-*)
-(* Prints a constant value before a suffix (needs casting) *)
-let rec pp_c_const_suffix var_type fmt c =
-  match c with
-    | Const_int i          -> pp_print_int fmt i
-    | Const_real r         -> Real.pp fmt r
-    | Const_tag t          -> pp_c_tag fmt t
-    | Const_array ca       -> let var_type = Types.array_element_type var_type in
-                              fprintf fmt "(%a[]){%a }" (pp_c_type "") var_type (Utils.fprintf_list ~sep:", " (pp_c_const_suffix var_type)) ca
-    | Const_struct fl       -> fprintf fmt "{%a }" (Utils.fprintf_list ~sep:", " (fun fmt (f, c) -> (pp_c_const_suffix (Types.struct_field_type var_type f)) fmt c)) fl
-    | Const_string _
-      | Const_modeid _ -> assert false (* string occurs in annotations not in C *)
+  (* Computes the list of nested loop variables together with their dimension bounds.
+     - LInt r stands for loop expansion (no loop variable, but int loop index)
+     - LVar v stands for loop variable v
+  *)
+  let rec mk_loop_variables m ty depth =
+    match (Types.repr ty).Types.tdesc, depth with
+    | Types.Tarray (d, ty'), 0 ->
+      let v = mk_loop_var m () in
+      (d, LVar v) :: mk_loop_variables m ty' 0
+    | Types.Tarray (d, ty'), _ ->
+      let r = ref (-1) in
+      (d, LInt r) :: mk_loop_variables m ty' (depth - 1)
+    | _, 0 -> []
+    | _ -> assert false
 
+  let reorder_loop_variables loop_vars =
+    let (int_loops, var_loops) =
+      List.partition (function (_, LInt _) -> true | _ -> false) loop_vars
+    in
+    var_loops @ int_loops
+
+  (* Prints a one loop variable suffix for arrays *)
+  let pp_loop_var pp_val fmt lv =
+    match snd lv with
+    | LVar v -> fprintf fmt "[%s]" v
+    | LInt r -> fprintf fmt "[%d]" !r
+    | LAcc i -> fprintf fmt "[%a]" pp_val i
+
+  (* Prints a suffix of loop variables for arrays *)
+  let pp_suffix pp_val =
+    pp_print_list ~pp_sep:pp_print_nothing (pp_loop_var pp_val)
+
+  (* Prints a value expression [v], with internal function calls only.
+     [pp_var] is a printer for variables (typically [pp_c_var_read]),
+     but an offset suffix may be added for array variables
+  *)
+  (* Prints a constant value before a suffix (needs casting) *)
+  let rec pp_c_const_suffix var_type fmt c =
+    match c with
+    | Const_int i ->
+      pp_print_int fmt i
+    | Const_real r ->
+      Real.pp fmt r
+    | Const_tag t ->
+      pp_c_tag fmt t
+    | Const_array ca ->
+      let var_type = Types.array_element_type var_type in
+      fprintf fmt "(%a[])%a"
+        (pp_c_type "") var_type
+        (pp_print_braced (pp_c_const_suffix var_type)) ca
+    | Const_struct fl ->
+      pp_print_braced
+        (fun fmt (f, c) ->
+           (pp_c_const_suffix (Types.struct_field_type var_type f)) fmt c)
+        fmt fl
+    | Const_string _
+    | Const_modeid _ -> assert false (* string occurs in annotations not in C *)
 
-(* Prints a [value] of type [var_type] indexed by the suffix list [loop_vars] *)
-let rec pp_value_suffix m self var_type loop_vars pp_var fmt value =
-  (*Format.eprintf "pp_value_suffix: %a %a %a@." Types.print_ty var_type Machine_code.pp_val value pp_suffix loop_vars;*)
-  let pp_suffix = pp_suffix m (pp_value_suffix m self var_type [] pp_var) in
-  (
+  (* Prints a [value] of type [var_type] indexed by the suffix list [loop_vars] *)
+  let rec pp_value_suffix m self var_type loop_vars pp_var fmt value =
+    (*eprintf "pp_value_suffix: %a %a %a@." Types.print_ty var_type Machine_code.pp_val value pp_suffix loop_vars;*)
+    let pp_suffix = pp_suffix (pp_value_suffix m self var_type [] pp_var) in
     match loop_vars, value.value_desc with
     | (x, LAcc i) :: q, _ when is_const_index i ->
-       let r = ref (Dimension.size_const_dimension (dimension_of_value i)) in
-       pp_value_suffix m self var_type ((x, LInt r)::q) pp_var fmt value
+      let r = ref (Dimension.size_const_dimension (dimension_of_value i)) in
+      pp_value_suffix m self var_type ((x, LInt r)::q) pp_var fmt value
     | (_, LInt r) :: q, Cst (Const_array cl) ->
-       let var_type = Types.array_element_type var_type in
-       pp_value_suffix m self var_type q pp_var fmt (mk_val (Cst (List.nth cl !r)) Type_predef.type_int)
-    | (_, LInt r) :: q, Array vl      ->
-       let var_type = Types.array_element_type var_type in
-       pp_value_suffix m self var_type q pp_var fmt (List.nth vl !r)
-    | loop_var    :: q, Array vl      ->
-       let var_type = Types.array_element_type var_type in
-       Format.fprintf fmt "(%a[]){%a }%a" (pp_c_type "") var_type (Utils.fprintf_list ~sep:", " (pp_value_suffix m self var_type q pp_var)) vl pp_suffix [loop_var]
-    | []              , Array vl      ->
-       let var_type = Types.array_element_type var_type in
-       Format.fprintf fmt "(%a[]){%a }" (pp_c_type "") var_type (Utils.fprintf_list ~sep:", " (pp_value_suffix m self var_type [] pp_var)) vl
-    | _           :: q, Power (v, _)  ->
-       pp_value_suffix m self var_type q pp_var fmt v
-    | _               , Fun (n, vl)   ->
-       pp_basic_lib_fun (Types.is_int_type value.value_type) n (pp_value_suffix m self var_type loop_vars pp_var) fmt vl
-    | _               , Access (v, i) ->
-       let var_type = Type_predef.type_array (Dimension.mkdim_var ()) var_type in
-       pp_value_suffix m self var_type ((Dimension.mkdim_var (), LAcc i) :: loop_vars) pp_var fmt v
-    | _               , Var v    ->
-       if is_memory m v then (
-         (* array memory vars are represented by an indirection to a local var with the right type,
-	    in order to avoid casting everywhere. *)
-         if Types.is_array_type v.var_type
-         then Format.fprintf fmt "%a%a" pp_var v pp_suffix loop_vars
-         else Format.fprintf fmt "%s->_reg.%a%a" self pp_var v pp_suffix loop_vars
-       )
-       else (
-         Format.fprintf fmt "%a%a" pp_var v pp_suffix loop_vars
-       )
-    | _               , Cst cst       -> pp_c_const_suffix var_type fmt cst
-    | _               , _             -> (Format.eprintf "internal error: C_backend_src.pp_value_suffix %a %a %a@." Types.print_ty var_type (pp_val m) value pp_suffix loop_vars; assert false)
-  )
-   
-(* Subsumes C_backend_common.pp_c_val to cope with aggressive substitution
-   which may yield constant arrays in expressions.
-   Type is needed to correctly print constant arrays.
- *)
-let pp_c_val m self pp_var fmt v =
-  pp_value_suffix m self v.value_type [] pp_var fmt v
-
-let pp_basic_assign pp_var fmt typ var_name value =
-  if Types.is_real_type typ && !Options.mpfr
-  then
-    Mpfr.pp_inject_assign pp_var fmt var_name value
-  else
-    fprintf fmt "%a = %a;" 
-      pp_var var_name
-      pp_var value
-
-(* type_directed assignment: array vs. statically sized type
-   - [var_type]: type of variable to be assigned
-   - [var_name]: name of variable to be assigned
-   - [value]: assigned value
-   - [pp_var]: printer for variables
-*)
-let pp_assign m self pp_var fmt var_type var_name value =
-  let depth = expansion_depth value in
-  (*Format.eprintf "pp_assign %a %a %a %d@." Types.print_ty var_type pp_val var_name pp_val value depth;*)
-  let loop_vars = mk_loop_variables m var_type depth in
-  let reordered_loop_vars = reorder_loop_variables loop_vars in
-  let rec aux typ fmt vars =
-    match vars with
-    | [] ->
-       pp_basic_assign (pp_value_suffix m self var_type loop_vars pp_var) fmt typ var_name value
-    | (d, LVar i) :: q ->
-       let typ' = Types.array_element_type typ in
-      (*eprintf "pp_aux %a %s@." Dimension.pp_dimension d i;*)
-      fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"
-	i i i pp_c_dimension d i
-	(aux typ') q
-    | (d, LInt r) :: q ->
-       (*eprintf "pp_aux %a %d@." Dimension.pp_dimension d (!r);*)
-       let typ' = Types.array_element_type typ in
-       let szl = Utils.enumerate (Dimension.size_const_dimension d) in
-       fprintf fmt "@[<v 2>{@,%a@]@,}"
-	       (Utils.fprintf_list ~sep:"@," (fun fmt i -> r := i; aux typ' fmt q)) szl
-    | _ -> assert false
-  in
-  begin
+      let var_type = Types.array_element_type var_type in
+      pp_value_suffix m self var_type q pp_var fmt
+        (mk_val (Cst (List.nth cl !r)) Type_predef.type_int)
+    | (_, LInt r) :: q, Array vl ->
+      let var_type = Types.array_element_type var_type in
+      pp_value_suffix m self var_type q pp_var fmt (List.nth vl !r)
+    | loop_var :: q, Array vl      ->
+      let var_type = Types.array_element_type var_type in
+      fprintf fmt "(%a[])%a%a"
+        (pp_c_type "") var_type
+        (pp_print_braced (pp_value_suffix m self var_type q pp_var)) vl
+        pp_suffix [loop_var]
+    | [], Array vl      ->
+      let var_type = Types.array_element_type var_type in
+      fprintf fmt "(%a[])%a"
+        (pp_c_type "") var_type
+        (pp_print_braced (pp_value_suffix m self var_type [] pp_var)) vl
+    | _ :: q, Power (v, _)  ->
+      pp_value_suffix m self var_type q pp_var fmt v
+    | _, Fun (n, vl)   ->
+      pp_basic_lib_fun (Types.is_int_type value.value_type) n
+        (pp_value_suffix m self var_type loop_vars pp_var) fmt vl
+    | _, Access (v, i) ->
+      let var_type = Type_predef.type_array (Dimension.mkdim_var ()) var_type in
+      pp_value_suffix m self var_type
+        ((Dimension.mkdim_var (), LAcc i) :: loop_vars) pp_var fmt v
+    | _, Var v ->
+      if is_memory m v then
+        (* array memory vars are represented by an indirection to a local var with the right type,
+           in order to avoid casting everywhere. *)
+        if Types.is_array_type v.var_type
+        then fprintf fmt "%a%a" pp_var v pp_suffix loop_vars
+        else fprintf fmt "%s->_reg.%a%a" self pp_var v pp_suffix loop_vars
+      else
+        fprintf fmt "%a%a" pp_var v pp_suffix loop_vars
+    | _, Cst cst ->
+      pp_c_const_suffix var_type fmt cst
+    | _, _ ->
+      eprintf "internal error: C_backend_src.pp_value_suffix %a %a %a@."
+        Types.print_ty var_type (pp_val m) value pp_suffix loop_vars;
+      assert false
+
+  (* Subsumes C_backend_common.pp_c_val to cope with aggressive substitution
+     which may yield constant arrays in expressions.
+     Type is needed to correctly print constant arrays.
+  *)
+  let pp_c_val m self pp_var fmt v =
+    pp_value_suffix m self v.value_type [] pp_var fmt v
+
+  let pp_basic_assign pp_var fmt typ var_name value =
+    if Types.is_real_type typ && !Options.mpfr
+    then
+      Mpfr.pp_inject_assign pp_var fmt (var_name, value)
+    else
+      fprintf fmt "%a = %a;"
+        pp_var var_name
+        pp_var value
+
+  (* type_directed assignment: array vs. statically sized type
+     - [var_type]: type of variable to be assigned
+     - [var_name]: name of variable to be assigned
+     - [value]: assigned value
+     - [pp_var]: printer for variables
+  *)
+  let pp_assign m self pp_var fmt var_type var_name value =
+    let depth = expansion_depth value in
+    (*eprintf "pp_assign %a %a %a %d@." Types.print_ty var_type pp_val var_name pp_val value depth;*)
+    let loop_vars = mk_loop_variables m var_type depth in
+    let reordered_loop_vars = reorder_loop_variables loop_vars in
+    let rec aux typ fmt vars =
+      match vars with
+      | [] ->
+        pp_basic_assign (pp_value_suffix m self var_type loop_vars pp_var)
+          fmt typ var_name value
+      | (d, LVar i) :: q ->
+        let typ' = Types.array_element_type typ in
+        (*eprintf "pp_aux %a %s@." Dimension.pp_dimension d i;*)
+        fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"
+          i i i pp_c_dimension d i
+          (aux typ') q
+      | (d, LInt r) :: q ->
+        (*eprintf "pp_aux %a %d@." Dimension.pp_dimension d (!r);*)
+        let typ' = Types.array_element_type typ in
+        let szl = Utils.enumerate (Dimension.size_const_dimension d) in
+        fprintf fmt "@[<v 2>{@,%a@]@,}"
+          (pp_print_list (fun fmt i -> r := i; aux typ' fmt q)) szl
+      | _ -> assert false
+    in
+    begin
+      reset_loop_counter ();
+      (*reset_addr_counter ();*)
+      aux var_type fmt reordered_loop_vars;
+      (*eprintf "end pp_assign@.";*)
+    end
+
+  let pp_machine_ pp_machine_name fn_name m self fmt inst =
+    let (node, static) = try List.assoc inst m.minstances with Not_found ->
+      eprintf "internal error: %s %s %s %s:@." fn_name m.mname.node_id self inst;
+      raise Not_found
+    in
+    fprintf fmt "%a(%a%s->%s);"
+      pp_machine_name (node_name node)
+      (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
+         Dimension.pp_dimension) static
+      self inst
+
+  let pp_machine_reset =
+    pp_machine_ pp_machine_reset_name "pp_machine_reset"
+
+  let pp_machine_init =
+    pp_machine_ pp_machine_init_name "pp_machine_init"
+
+  let pp_machine_clear =
+    pp_machine_ pp_machine_clear_name "pp_machine_clear"
+
+  let has_c_prototype funname dependencies =
+    (* We select the last imported node with the name funname.
+       The order of evaluation of dependencies should be
+       compatible with overloading. (Not checked yet) *)
+    let imported_node_opt =
+      List.fold_left
+        (fun res dep ->
+           match res with
+           | Some _ -> res
+           | None ->
+             let decls = dep.content in
+             let matched = fun t -> match t.top_decl_desc with
+               | ImportedNode nd -> nd.nodei_id = funname
+               | _ -> false
+             in
+             if List.exists matched decls then
+               match (List.find matched decls).top_decl_desc with
+               | ImportedNode nd -> Some nd
+               | _ -> assert false
+             else
+               None) None dependencies in
+    match imported_node_opt with
+    | None -> false
+    | Some nd -> (match nd.nodei_prototype with Some "C" -> true | _ -> false)
+
+  let pp_call m self pp_read pp_write fmt i
+      (inputs: Machine_code_types.value_t list) (outputs: var_decl list) =
+    try (* stateful node instance *)
+      let n, _ = List.assoc i m.minstances in
+      fprintf fmt "%a (%a%a%s->%s);"
+        pp_machine_step_name (node_name n)
+        (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
+           (pp_c_val m self pp_read)) inputs
+        (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
+           pp_write) outputs
+        self
+        i
+    with Not_found -> (* stateless node instance *)
+      let n, _ = List.assoc i m.mcalls in
+      fprintf fmt "%a (%a%a);"
+        pp_machine_step_name (node_name n)
+        (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
+           (pp_c_val m self pp_read)) inputs
+        (pp_print_list ~pp_sep:pp_print_comma pp_write) outputs
+
+  let pp_basic_instance_call m self =
+    pp_call m self (pp_c_var_read m) (pp_c_var_write m)
+
+  let pp_instance_call m self fmt i (inputs: Machine_code_types.value_t list) (outputs: var_decl list) =
+    let pp_offset pp_var indices fmt var =
+      fprintf fmt "%a%a"
+        pp_var var
+        (pp_print_list ~pp_sep:pp_print_nothing (fun fmt -> fprintf fmt "[%s]"))
+        indices
+    in
+    let rec aux indices fmt typ =
+      if Types.is_array_type typ
+      then
+        let dim = Types.array_type_dimension typ in
+        let idx = mk_loop_var m () in
+        fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"
+          idx idx idx pp_c_dimension dim idx
+          (aux (idx::indices)) (Types.array_element_type typ)
+      else
+        let pp_read  = pp_offset (pp_c_var_read  m) indices in
+        let pp_write = pp_offset (pp_c_var_write m) indices in
+        pp_call m self pp_read pp_write fmt i inputs outputs
+    in
     reset_loop_counter ();
-    (*reset_addr_counter ();*)
-    aux var_type fmt reordered_loop_vars;
-    (*Format.eprintf "end pp_assign@.";*)
-  end
-
-let pp_machine_reset (m: machine_t) self fmt inst =
-  let (node, static) =
-    try
-      List.assoc inst m.minstances
-    with Not_found -> (Format.eprintf "internal error: pp_machine_reset %s %s %s:@." m.mname.node_id self inst; raise Not_found) in
-  fprintf fmt "%a(%a%t%s->%s);"
-    pp_machine_reset_name (node_name node)
-    (Utils.fprintf_list ~sep:", " Dimension.pp_dimension) static
-    (Utils.pp_final_char_if_non_empty ", " static)
-    self inst
-
-let pp_machine_init (m: machine_t) self fmt inst =
-  let (node, static) =
-    try
-      List.assoc inst m.minstances
-    with Not_found -> (Format.eprintf "internal error: pp_machine_init %s %s %s@." m.mname.node_id self inst; raise Not_found) in
-  fprintf fmt "%a(%a%t%s->%s);"
-    pp_machine_init_name (node_name node)
-    (Utils.fprintf_list ~sep:", " Dimension.pp_dimension) static
-    (Utils.pp_final_char_if_non_empty ", " static)
-    self inst
-
-let pp_machine_clear (m: machine_t) self fmt inst =
-  let (node, static) =
-    try
-      List.assoc inst m.minstances
-    with Not_found -> (Format.eprintf "internal error: pp_machine_clear %s %s %s@." m.mname.node_id self inst; raise Not_found) in
-  fprintf fmt "%a(%a%t%s->%s);"
-    pp_machine_clear_name (node_name node)
-    (Utils.fprintf_list ~sep:", " Dimension.pp_dimension) static
-    (Utils.pp_final_char_if_non_empty ", " static)
-    self inst
-
-let has_c_prototype funname dependencies =
-  let imported_node_opt = (* We select the last imported node with the name funname.
-			       The order of evaluation of dependencies should be
-			       compatible with overloading. (Not checked yet) *) 
-    List.fold_left
-      (fun res dep -> 
-	match res with
-	| Some _ -> res
-	| None ->
-           let decls = dep.content in
-	   let matched = fun t -> match t.top_decl_desc with 
-	                          | ImportedNode nd -> nd.nodei_id = funname 
-	                          | _ -> false
-	   in
-	   if List.exists matched decls then (
-	     match (List.find matched decls).top_decl_desc with
-	     | ImportedNode nd -> Some nd
-	     | _ -> assert false
-	   )
-	   else
-	     None
-      ) None dependencies in
-  match imported_node_opt with
-  | None -> false
-  | Some nd -> (match nd.nodei_prototype with Some "C" -> true | _ -> false)
-(*
-let pp_instance_call dependencies m self fmt i (inputs: value_t list) (outputs: var_decl list) =
-  try (* stateful node instance *)
-    let (n,_) = List.assoc i m.minstances in
-    let (input_types, _) = Typing.get_type_of_call n in
-    let inputs = List.combine input_types inputs in
-    fprintf fmt "%a (%a%t%a%t%s->%s);"
-      pp_machine_step_name (node_name n)
-      (Utils.fprintf_list ~sep:", " (pp_c_val self (pp_c_var_read m))) inputs
-      (Utils.pp_final_char_if_non_empty ", " inputs) 
-      (Utils.fprintf_list ~sep:", " (pp_c_var_write m)) outputs
-      (Utils.pp_final_char_if_non_empty ", " outputs)
-      self
-      i
-  with Not_found -> (* stateless node instance *)
-    let (n,_) = List.assoc i m.mcalls in
-    let (input_types, output_types) = Typing.get_type_of_call n in
-    let inputs = List.combine input_types inputs in
-    if has_c_prototype i dependencies
-    then (* external C function *)
-      let outputs = List.map2 (fun t v -> t, Var v) output_types outputs in
-      fprintf fmt "%a = %s(%a);"
-	(Utils.fprintf_list ~sep:", " (pp_c_val self (pp_c_var_read m))) outputs
-	i
-	(Utils.fprintf_list ~sep:", " (pp_c_val self (pp_c_var_read m))) inputs
+    aux [] fmt (List.hd inputs).Machine_code_types.value_type
+
+  let rec pp_conditional dependencies (m: machine_t) self fmt c tl el =
+    fprintf fmt "@[<v 2>if (%a) {%a@]@,@[<v 2>} else {%a@]@,}"
+      (pp_c_val m self (pp_c_var_read m)) c
+      (pp_print_list ~pp_prologue:pp_print_cut
+         (pp_machine_instr dependencies m self)) tl
+      (pp_print_list ~pp_prologue:pp_print_cut
+         (pp_machine_instr dependencies m self)) el
+
+  and pp_machine_instr dependencies (m: machine_t) self fmt instr =
+    match get_instr_desc instr with
+    | MNoReset _ -> ()
+    | MReset i ->
+      pp_machine_reset m self fmt i
+    | MLocalAssign (i,v) ->
+      pp_assign
+        m self (pp_c_var_read m) fmt
+        i.var_type (mk_val (Var i) i.var_type) v
+    | MStateAssign (i,v) ->
+      pp_assign
+        m self (pp_c_var_read m) fmt
+        i.var_type (mk_val (Var i) i.var_type) v
+    | MStep ([i0], i, vl) when Basic_library.is_value_internal_fun (mk_val (Fun (i, vl)) i0.var_type)  ->
+      pp_machine_instr dependencies m self fmt
+        (update_instr_desc instr (MLocalAssign (i0, mk_val (Fun (i, vl)) i0.var_type)))
+    | MStep (il, i, vl) when !Options.mpfr && Mpfr.is_homomorphic_fun i ->
+      pp_instance_call m self fmt i vl il
+    | MStep ([i0], i, vl) when has_c_prototype i dependencies ->
+      fprintf fmt "%a = %s%a;"
+        (pp_c_val m self (pp_c_var_read m)) (mk_val (Var i0) i0.var_type)
+        i
+        (pp_print_parenthesized (pp_c_val m self (pp_c_var_read m))) vl
+    | MStep (il, i, vl) ->
+      pp_basic_instance_call m self fmt i vl il
+    | MBranch (_, []) ->
+      eprintf "internal error: C_backend_src.pp_machine_instr %a@."
+        (pp_instr m) instr;
+      assert false
+    | MBranch (g, hl) ->
+      if let t = fst (List.hd hl) in t = tag_true || t = tag_false
+      then (* boolean case, needs special treatment in C because truth value is not unique *)
+        (* may disappear if we optimize code by replacing last branch test with default *)
+        let tl = try List.assoc tag_true  hl with Not_found -> [] in
+        let el = try List.assoc tag_false hl with Not_found -> [] in
+        pp_conditional dependencies m self fmt g tl el
+      else (* enum type case *)
+        (*let g_typ = Typing.type_const Location.dummy_loc (Const_tag (fst (List.hd hl))) in*)
+        fprintf fmt "@[<v 2>switch(%a) {@,%a@,}@]"
+          (pp_c_val m self (pp_c_var_read m)) g
+          (pp_print_list ~pp_open_box:pp_open_vbox0
+             (pp_machine_branch dependencies m self)) hl
+    | MSpec s ->
+      fprintf fmt "@[/*@@ %s */@]@ " s
+    | MComment s  ->
+      fprintf fmt "/*%s*/@ " s
+
+  and pp_machine_branch dependencies m self fmt (t, h) =
+    fprintf fmt "@[<v 2>case %a:@,%a@,break;@]"
+      pp_c_tag t
+      (pp_print_list ~pp_open_box:pp_open_vbox0
+         (pp_machine_instr dependencies m self)) h
+
+
+  (********************************************************************************************)
+  (*                         C file Printing functions                                        *)
+  (********************************************************************************************)
+
+  let print_const_def fmt tdecl =
+    let cdecl = const_of_top tdecl in
+    if !Options.mpfr && Types.(is_real_type (array_base_type cdecl.const_type))
+    then
+      fprintf fmt "%a;"
+        (pp_c_type cdecl.const_id) (Types.dynamic_type cdecl.const_type)
     else
-      fprintf fmt "%a (%a%t%a);"
-	pp_machine_step_name (node_name n)
-	(Utils.fprintf_list ~sep:", " (pp_c_val self (pp_c_var_read m))) inputs
-	(Utils.pp_final_char_if_non_empty ", " inputs) 
-	(Utils.fprintf_list ~sep:", " (pp_c_var_write m)) outputs 
-*)
-let rec pp_conditional dependencies (m: machine_t) self fmt c tl el =
-  fprintf fmt "@[<v 2>if (%a) {%t%a@]@,@[<v 2>} else {%t%a@]@,}"
-    (pp_c_val m self (pp_c_var_read m)) c
-    (Utils.pp_newline_if_non_empty tl)
-    (Utils.fprintf_list ~sep:"@," (pp_machine_instr dependencies m self)) tl
-    (Utils.pp_newline_if_non_empty el)
-    (Utils.fprintf_list ~sep:"@," (pp_machine_instr dependencies m self)) el
-
-and pp_machine_instr dependencies (m: machine_t) self fmt instr =
-  match get_instr_desc instr with 
-  | MNoReset _ -> ()
-  | MReset i ->
-    pp_machine_reset m self fmt i
-  | MLocalAssign (i,v) ->
-    pp_assign
-      m self (pp_c_var_read m) fmt
-      i.var_type (mk_val (Var i) i.var_type) v
-  | MStateAssign (i,v) ->
-    pp_assign
-      m self (pp_c_var_read m) fmt
-      i.var_type (mk_val (Var i) i.var_type) v
-  | MStep ([i0], i, vl) when Basic_library.is_value_internal_fun (mk_val (Fun (i, vl)) i0.var_type)  ->
-    pp_machine_instr dependencies m self fmt 
-      (update_instr_desc instr (MLocalAssign (i0, mk_val (Fun (i, vl)) i0.var_type)))
-  | MStep (il, i, vl) when !Options.mpfr && Mpfr.is_homomorphic_fun i ->
-     pp_instance_call m self fmt i vl il
-  | MStep ([i0], i, vl) when has_c_prototype i dependencies -> 
-    fprintf fmt "%a = %s(%a);" 
-      (pp_c_val m self (pp_c_var_read m)) (mk_val (Var i0) i0.var_type)
+      fprintf fmt "%a = %a;"
+        (pp_c_type cdecl.const_id) cdecl.const_type
+        pp_c_const cdecl.const_value
+
+  let print_alloc_instance fmt (i, (m, static)) =
+    fprintf fmt "_alloc->%s = %a %a;"
       i
-      (Utils.fprintf_list ~sep:", " (pp_c_val m self (pp_c_var_read m))) vl
-  | MStep (il, i, vl) ->
-    pp_basic_instance_call m self fmt i vl il
-  | MBranch (_, []) -> (Format.eprintf "internal error: C_backend_src.pp_machine_instr %a@." (pp_instr m) instr; assert false)
-  | MBranch (g, hl) ->
-    if let t = fst (List.hd hl) in t = tag_true || t = tag_false
-    then (* boolean case, needs special treatment in C because truth value is not unique *)
-	 (* may disappear if we optimize code by replacing last branch test with default *)
-      let tl = try List.assoc tag_true  hl with Not_found -> [] in
-      let el = try List.assoc tag_false hl with Not_found -> [] in
-      pp_conditional dependencies m self fmt g tl el
-    else (* enum type case *)
-      (*let g_typ = Typing.type_const Location.dummy_loc (Const_tag (fst (List.hd hl))) in*)
-      fprintf fmt "@[<v 2>switch(%a) {@,%a@,}@]"
-	(pp_c_val m self (pp_c_var_read m)) g
-	(Utils.fprintf_list ~sep:"@," (pp_machine_branch dependencies m self)) hl
-  | MSpec s -> fprintf fmt "@[/*@@ %s */@]@ " s
-  | MComment s  -> 
-      fprintf fmt "/*%s*/@ " s
+      pp_machine_alloc_name (node_name m)
+      (pp_print_parenthesized Dimension.pp_dimension) static
 
+  let print_dealloc_instance fmt (i, (m, _)) =
+    fprintf fmt "%a (_alloc->%s);"
+      pp_machine_dealloc_name (node_name m)
+      i
 
-and pp_machine_branch dependencies m self fmt (t, h) =
-  fprintf fmt "@[<v 2>case %a:@,%a@,break;@]"
-    pp_c_tag t
-    (Utils.fprintf_list ~sep:"@," (pp_machine_instr dependencies m self)) h
-
-
-(********************************************************************************************)
-(*                         C file Printing functions                                        *)
-(********************************************************************************************)
-
-let print_const_def fmt cdecl =
-  if !Options.mpfr && Types.is_real_type (Types.array_base_type cdecl.const_type)
-  then
-    fprintf fmt "%a;@." 
-      (pp_c_type cdecl.const_id) (Types.dynamic_type cdecl.const_type) 
-  else
-    fprintf fmt "%a = %a;@." 
-      (pp_c_type cdecl.const_id) cdecl.const_type
-      pp_c_const cdecl.const_value 
-
-
-let print_alloc_instance fmt (i, (m, static)) =
-  fprintf fmt "_alloc->%s = %a (%a);@,"
-    i
-    pp_machine_alloc_name (node_name m)
-    (Utils.fprintf_list ~sep:", " Dimension.pp_dimension) static
-
-let print_dealloc_instance fmt (i, (m, _)) =
-  fprintf fmt "%a (_alloc->%s);@,"
-    pp_machine_dealloc_name (node_name m)
-    i
-
-let print_alloc_const fmt m =
-  let const_locals = List.filter (fun vdecl -> vdecl.var_dec_const) m.mstep.step_locals in
-  fprintf fmt "%a%t"
-    (Utils.fprintf_list ~sep:";@," (pp_c_decl_local_var m)) const_locals
-    (Utils.pp_final_char_if_non_empty ";@," const_locals)
-
-let print_alloc_array fmt vdecl =
-  let base_type = Types.array_base_type vdecl.var_type in
-  let size_types = Types.array_type_multi_dimension vdecl.var_type in
-  let size_type = Dimension.multi_dimension_product vdecl.var_loc size_types in
-  fprintf fmt "_alloc->_reg.%s = (%a*) malloc((%a)*sizeof(%a));@,assert(_alloc->%s);@,"
-    vdecl.var_id
-    (pp_c_type "") base_type
-    Dimension.pp_dimension size_type
-    (pp_c_type "") base_type
-    vdecl.var_id
-
-let print_dealloc_array fmt vdecl =
-  fprintf fmt "free (_alloc->_reg.%s);@,"
-    vdecl.var_id
-
-let print_alloc_code fmt m =
-  let array_mem = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
-  fprintf fmt "%a *_alloc;@,_alloc = (%a *) malloc(sizeof(%a));@,assert(_alloc);@,%a%areturn _alloc;"
-    pp_machine_memtype_name m.mname.node_id
-    pp_machine_memtype_name m.mname.node_id
-    pp_machine_memtype_name m.mname.node_id
-    (Utils.fprintf_list ~sep:"" print_alloc_array) array_mem
-    (Utils.fprintf_list ~sep:"" print_alloc_instance) m.minstances
-
-let print_dealloc_code fmt m =
-  let array_mem = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
-  fprintf fmt "%a%afree (_alloc);@,return;"
-    (Utils.fprintf_list ~sep:"" print_dealloc_array) array_mem
-    (Utils.fprintf_list ~sep:"" print_dealloc_instance) m.minstances
-
-(* let print_stateless_init_code fmt m self =
- *   let minit = List.map (fun i -> match get_instr_desc i with MReset i -> i | _ -> assert false) m.minit in
- *   let array_mems = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
- *   fprintf fmt "@[<v 2>%a {@,%a%t%a%t%a%treturn;@]@,}@.@."
- *     (print_init_prototype self) (m.mname.node_id, m.mstatic)
- *     (\* array mems *\)
- *     (Utils.fprintf_list ~sep:";@," (pp_c_decl_array_mem self)) array_mems
- *     (Utils.pp_final_char_if_non_empty ";@," array_mems)
- *     (\* memory initialization *\)
- *     (Utils.fprintf_list ~sep:"@," (pp_initialize m self (pp_c_var_read m))) m.mmemory
- *     (Utils.pp_newline_if_non_empty m.mmemory)
- *     (\* sub-machines initialization *\)
- *     (Utils.fprintf_list ~sep:"@," (pp_machine_init m self)) minit
- *     (Utils.pp_newline_if_non_empty m.minit)
- *
- * let print_stateless_clear_code fmt m self =
- *   let minit = List.map (fun i -> match get_instr_desc i with MReset i -> i | _ -> assert false) m.minit in
- *   let array_mems = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
- *   fprintf fmt "@[<v 2>%a {@,%a%t%a%t%a%treturn;@]@,}@.@."
- *     (print_clear_prototype self) (m.mname.node_id, m.mstatic)
- *     (\* array mems *\)
- *     (Utils.fprintf_list ~sep:";@," (pp_c_decl_array_mem self)) array_mems
- *     (Utils.pp_final_char_if_non_empty ";@," array_mems)
- *     (\* memory clear *\)
- *     (Utils.fprintf_list ~sep:"@," (pp_clear m self (pp_c_var_read m))) m.mmemory
- *     (Utils.pp_newline_if_non_empty m.mmemory)
- *     (\* sub-machines clear*\)
- *     (Utils.fprintf_list ~sep:"@," (pp_machine_clear m self)) minit
- *     (Utils.pp_newline_if_non_empty m.minit) *)
-
-let print_stateless_code dependencies fmt m =
-  let self = "__ERROR__" in
-  if not (!Options.ansi && is_generic_node { top_decl_desc = Node m.mname; top_decl_loc = Location.dummy_loc; top_decl_owner = ""; top_decl_itf = false })
-  then
-    (* C99 code *)
-    fprintf fmt "@[<v 2>%a {@,%a%t%a%t@,%a%a%t%a%t%t@]@,}@.@."
-      print_stateless_prototype (m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs)
-      (* locals *)
-      (Utils.fprintf_list ~sep:";@," (pp_c_decl_local_var m)) m.mstep.step_locals
-      (Utils.pp_final_char_if_non_empty ";@," m.mstep.step_locals)
-      (* locals initialization *)
-      (Utils.fprintf_list ~sep:"@," (pp_initialize m self (pp_c_var_read m))) m.mstep.step_locals
-      (Utils.pp_newline_if_non_empty m.mstep.step_locals)
-      (* check assertions *)
-      (pp_c_checks self) m
-      (* instrs *)
-      (Utils.fprintf_list ~sep:"@," (pp_machine_instr dependencies m self)) m.mstep.step_instrs
-      (Utils.pp_newline_if_non_empty m.mstep.step_instrs)
-      (* locals clear *)
-      (Utils.fprintf_list ~sep:"@," (pp_clear m self (pp_c_var_read m))) m.mstep.step_locals
-      (Utils.pp_newline_if_non_empty m.mstep.step_locals)
-      (fun fmt -> fprintf fmt "return;")
-  else
-    (* C90 code *)
-    let (gen_locals, base_locals) = List.partition (fun v -> Types.is_generic_type v.var_type) m.mstep.step_locals in
-    let gen_calls = List.map (fun e -> let (id, _, _) = call_of_expr e in mk_call_var_decl e.expr_loc id) m.mname.node_gencalls in
-    fprintf fmt "@[<v 2>%a {@,%a%t%a%t@,%a%a%t%a%t%t@]@,}@.@."
-      print_stateless_prototype (m.mname.node_id, (m.mstep.step_inputs@gen_locals@gen_calls), m.mstep.step_outputs)
-      (* locals *)
-      (Utils.fprintf_list ~sep:";@," (pp_c_decl_local_var m)) base_locals
-      (Utils.pp_final_char_if_non_empty ";" base_locals)
-      (* locals initialization *)
-      (Utils.fprintf_list ~sep:"@," (pp_initialize m self (pp_c_var_read m))) m.mstep.step_locals
-      (Utils.pp_newline_if_non_empty m.mstep.step_locals)
-      (* check assertions *)
-      (pp_c_checks self) m
-      (* instrs *)
-      (Utils.fprintf_list ~sep:"@," (pp_machine_instr dependencies m self)) m.mstep.step_instrs
-      (Utils.pp_newline_if_non_empty m.mstep.step_instrs)
-      (* locals clear *)
-      (Utils.fprintf_list ~sep:"@," (pp_clear m self (pp_c_var_read m))) m.mstep.step_locals
-      (Utils.pp_newline_if_non_empty m.mstep.step_locals)
-      (fun fmt -> fprintf fmt "return;")
-
-let print_reset_code dependencies fmt m self =
-  let const_locals = List.filter (fun vdecl -> vdecl.var_dec_const) m.mstep.step_locals in
-  fprintf fmt "@[<v 2>%a {@,%a%t@,%a%treturn;@]@,}@.@."
-    (print_reset_prototype self) (m.mname.node_id, m.mstatic)
-    (* constant locals decl *)
-    (Utils.fprintf_list ~sep:";@," (pp_c_decl_local_var m)) const_locals
-    (Utils.pp_final_char_if_non_empty ";" const_locals)
-    (* instrs *)
-    (Utils.fprintf_list ~sep:"@," (pp_machine_instr dependencies m self)) m.minit
-    (Utils.pp_newline_if_non_empty m.minit)
-
-let print_init_code fmt m self =
-  let minit = List.map (fun i -> match get_instr_desc i with MReset i -> i | _ -> assert false) m.minit in
-  let array_mems = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
-  fprintf fmt "@[<v 2>%a {@,%a%t%a%t%a%treturn;@]@,}@.@."
-    (print_init_prototype self) (m.mname.node_id, m.mstatic)
-    (* array mems *) 
-    (Utils.fprintf_list ~sep:";@," (pp_c_decl_array_mem self)) array_mems
-    (Utils.pp_final_char_if_non_empty ";@," array_mems)
-    (* memory initialization *)
-    (Utils.fprintf_list ~sep:"@," (pp_initialize m self (pp_c_var_read m))) m.mmemory
-    (Utils.pp_newline_if_non_empty m.mmemory)
-    (* sub-machines initialization *)
-    (Utils.fprintf_list ~sep:"@," (pp_machine_init m self)) minit
-    (Utils.pp_newline_if_non_empty m.minit)
-
-let print_clear_code fmt m self =
-  let minit = List.map (fun i -> match get_instr_desc i with MReset i -> i | _ -> assert false) m.minit in
-  let array_mems = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
-  fprintf fmt "@[<v 2>%a {@,%a%t%a%t%a%treturn;@]@,}@.@."
-    (print_clear_prototype self) (m.mname.node_id, m.mstatic)
-    (* array mems *)
-    (Utils.fprintf_list ~sep:";@," (pp_c_decl_array_mem self)) array_mems
-    (Utils.pp_final_char_if_non_empty ";@," array_mems)
-    (* memory clear *)
-    (Utils.fprintf_list ~sep:"@," (pp_clear m self (pp_c_var_read m))) m.mmemory
-    (Utils.pp_newline_if_non_empty m.mmemory)
-    (* sub-machines clear*)
-    (Utils.fprintf_list ~sep:"@," (pp_machine_clear m self)) minit
-    (Utils.pp_newline_if_non_empty m.minit)
-
-let print_step_code dependencies fmt m self =
-  if not (!Options.ansi && is_generic_node { top_decl_desc = Node m.mname; top_decl_loc = Location.dummy_loc; top_decl_owner = ""; top_decl_itf = false })
-  then
-    (* C99 code *)
-    let array_mems = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
-    fprintf fmt "@[<v 2>%a {@,%a%t%a%t%a%t@,%a%a%t%a%t%t@]@,}@.@."
-      (print_step_prototype self) (m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs)
+  let const_locals m =
+    List.filter (fun vdecl -> vdecl.var_dec_const) m.mstep.step_locals
+
+  let pp_c_decl_array_mem self fmt id =
+    fprintf fmt "%a = (%a) (%s->_reg.%s)"
+      (pp_c_type (sprintf "(*%s)" id.var_id)) id.var_type
+      (pp_c_type "(*)") id.var_type
+      self
+      id.var_id
+
+  let print_alloc_const fmt m =
+    pp_print_list
+      ~pp_sep:(pp_print_endcut ";") ~pp_eol:(pp_print_endcut ";")
+      (pp_c_decl_local_var m) fmt (const_locals m)
+
+  let print_alloc_array fmt vdecl =
+    let base_type = Types.array_base_type vdecl.var_type in
+    let size_types = Types.array_type_multi_dimension vdecl.var_type in
+    let size_type = Dimension.multi_dimension_product vdecl.var_loc size_types in
+    fprintf fmt
+      "_alloc->_reg.%s = (%a*) malloc((%a)*sizeof(%a));@,\
+       assert(_alloc->%s);"
+      vdecl.var_id
+      (pp_c_type "") base_type
+      Dimension.pp_dimension size_type
+      (pp_c_type "") base_type
+      vdecl.var_id
+
+  let print_dealloc_array fmt vdecl =
+    fprintf fmt "free (_alloc->_reg.%s);"
+      vdecl.var_id
+
+  let array_mems m =
+    List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory
+
+  let print_alloc_code fmt m =
+    fprintf fmt
+      "%a *_alloc;@,\
+       _alloc = (%a *) malloc(sizeof(%a));@,\
+       assert(_alloc);@,\
+       %a%areturn _alloc;"
+      pp_machine_memtype_name m.mname.node_id
+      pp_machine_memtype_name m.mname.node_id
+      pp_machine_memtype_name m.mname.node_id
+      (pp_print_list ~pp_sep:pp_print_nothing print_alloc_array) (array_mems m)
+      (pp_print_list ~pp_sep:pp_print_nothing print_alloc_instance) m.minstances
+
+  let print_dealloc_code fmt m =
+    fprintf fmt
+      "%a%afree (_alloc);@,\
+       return;"
+      (pp_print_list ~pp_sep:pp_print_nothing print_dealloc_array) (array_mems m)
+      (pp_print_list ~pp_sep:pp_print_nothing print_dealloc_instance) m.minstances
+
+  (* let print_stateless_init_code fmt m self =
+   *   let minit = List.map (fun i -> match get_instr_desc i with MReset i -> i | _ -> assert false) m.minit in
+   *   let array_mems = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
+   *   fprintf fmt "@[<v 2>%a {@,%a%t%a%t%a%treturn;@]@,}@.@."
+   *     (print_init_prototype self) (m.mname.node_id, m.mstatic)
+   *     (\* array mems *\)
+   *     (Utils.fprintf_list ~sep:";@," (pp_c_decl_array_mem self)) array_mems
+   *     (Utils.pp_final_char_if_non_empty ";@," array_mems)
+   *     (\* memory initialization *\)
+   *     (Utils.fprintf_list ~sep:"@," (pp_initialize m self (pp_c_var_read m))) m.mmemory
+   *     (Utils.pp_newline_if_non_empty m.mmemory)
+   *     (\* sub-machines initialization *\)
+   *     (Utils.fprintf_list ~sep:"@," (pp_machine_init m self)) minit
+   *     (Utils.pp_newline_if_non_empty m.minit)
+   *
+   * let print_stateless_clear_code fmt m self =
+   *   let minit = List.map (fun i -> match get_instr_desc i with MReset i -> i | _ -> assert false) m.minit in
+   *   let array_mems = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
+   *   fprintf fmt "@[<v 2>%a {@,%a%t%a%t%a%treturn;@]@,}@.@."
+   *     (print_clear_prototype self) (m.mname.node_id, m.mstatic)
+   *     (\* array mems *\)
+   *     (Utils.fprintf_list ~sep:";@," (pp_c_decl_array_mem self)) array_mems
+   *     (Utils.pp_final_char_if_non_empty ";@," array_mems)
+   *     (\* memory clear *\)
+   *     (Utils.fprintf_list ~sep:"@," (pp_clear m self (pp_c_var_read m))) m.mmemory
+   *     (Utils.pp_newline_if_non_empty m.mmemory)
+   *     (\* sub-machines clear*\)
+   *     (Utils.fprintf_list ~sep:"@," (pp_machine_clear m self)) minit
+   *     (Utils.pp_newline_if_non_empty m.minit) *)
+
+  let pp_c_check m self fmt (loc, check) =
+    fprintf fmt "@[<v>%a@,assert (%a);@]"
+      Location.pp_c_loc loc
+      (pp_c_val m self (pp_c_var_read m)) check
+
+  let pp_print_function
+      ~pp_prototype ~prototype
+      ?(pp_local=pp_print_nothing) ?(base_locals=[])
+      ?(pp_array_mem=pp_print_nothing) ?(array_mems=[])
+      ?(pp_init_mpfr_local=pp_print_nothing)
+      ?(pp_clear_mpfr_local=pp_print_nothing)
+      ?(mpfr_locals=[])
+      ?(pp_check=pp_print_nothing) ?(checks=[])
+      ?(pp_extra=pp_print_nothing)
+      ?(pp_instr=pp_print_nothing) ?(instrs=[])
+      fmt =
+    fprintf fmt
+      "@[<v 2>%a {@,\
+       %a%a\
+       %a%a%a%a%areturn;@]@,\
+       }"
+      pp_prototype prototype
       (* locals *)
-      (Utils.fprintf_list ~sep:";@," (pp_c_decl_local_var m)) m.mstep.step_locals
-      (Utils.pp_final_char_if_non_empty ";@," m.mstep.step_locals)
+      (pp_print_list
+         ~pp_open_box:pp_open_vbox0
+         ~pp_sep:pp_print_semicolon
+         ~pp_eol:pp_print_semicolon
+         pp_local)
+      base_locals
       (* array mems *)
-      (Utils.fprintf_list ~sep:";@," (pp_c_decl_array_mem self)) array_mems
-      (Utils.pp_final_char_if_non_empty ";@," array_mems)
-      (* locals initialization *)
-      (Utils.fprintf_list ~sep:"@," (pp_initialize m self (pp_c_var_read m))) m.mstep.step_locals
-      (Utils.pp_newline_if_non_empty m.mstep.step_locals)
-      (* check assertions *)
-      (pp_c_checks self) m
-      (* instrs *)
-      (Utils.fprintf_list ~sep:"@," (pp_machine_instr dependencies m self)) m.mstep.step_instrs
-      (Utils.pp_newline_if_non_empty m.mstep.step_instrs)
-      (* locals clear *)
-      (Utils.fprintf_list ~sep:"@," (pp_clear m self (pp_c_var_read m))) m.mstep.step_locals
-      (Utils.pp_newline_if_non_empty m.mstep.step_locals)
-      (fun fmt -> fprintf fmt "return;")
-  else
-    (* C90 code *)
-    let (gen_locals, base_locals) = List.partition (fun v -> Types.is_generic_type v.var_type) m.mstep.step_locals in
-    let gen_calls = List.map (fun e -> let (id, _, _) = call_of_expr e in mk_call_var_decl e.expr_loc id) m.mname.node_gencalls in
-    fprintf fmt "@[<v 2>%a {@,%a%t%a%t@,%a%a%t%a%t%t@]@,}@.@."
-      (print_step_prototype self) (m.mname.node_id, (m.mstep.step_inputs@gen_locals@gen_calls), m.mstep.step_outputs)
-      (* locals *)
-      (Utils.fprintf_list ~sep:";@," (pp_c_decl_local_var m)) base_locals
-      (Utils.pp_final_char_if_non_empty ";" base_locals)
+      (pp_print_list
+         ~pp_open_box:pp_open_vbox0
+         ~pp_sep:pp_print_semicolon
+         ~pp_eol:pp_print_semicolon
+         pp_array_mem)
+      array_mems
       (* locals initialization *)
-      (Utils.fprintf_list ~sep:"@," (pp_initialize m self (pp_c_var_read m))) m.mstep.step_locals
-      (Utils.pp_newline_if_non_empty m.mstep.step_locals)
+      (pp_print_list
+         ~pp_epilogue:pp_print_cut
+         pp_init_mpfr_local) (mpfr_vars mpfr_locals)
       (* check assertions *)
-      (pp_c_checks self) m
+      (pp_print_list pp_check) checks
       (* instrs *)
-      (Utils.fprintf_list ~sep:"@," (pp_machine_instr dependencies m self)) m.mstep.step_instrs
-      (Utils.pp_newline_if_non_empty m.mstep.step_instrs)
+      (pp_print_list
+         ~pp_open_box:pp_open_vbox0
+         ~pp_epilogue:pp_print_cut
+         pp_instr) instrs
       (* locals clear *)
-      (Utils.fprintf_list ~sep:"@," (pp_clear m self (pp_c_var_read m))) m.mstep.step_locals
-      (Utils.pp_newline_if_non_empty m.mstep.step_locals)
-      (fun fmt -> fprintf fmt "return;")
-
-
-(********************************************************************************************)
-(*                     MAIN C file Printing functions                                       *)
-(********************************************************************************************)
-
-let print_global_init_code fmt basename prog dependencies =
-  let baseNAME = file_to_module_name basename in
-  let constants = List.map const_of_top (get_consts prog) in
-  fprintf fmt "@[<v 2>%a {@,static %s init = 0;@,@[<v 2>if (!init) { @,init = 1;@,%a%t%a@]@,}@,return;@]@,}@.@."
-    print_global_init_prototype baseNAME
-    (pp_c_basic_type_desc Type_predef.type_bool)
-    (* constants *) 
-    (Utils.fprintf_list ~sep:"@," (pp_const_initialize empty_machine (pp_c_var_read empty_machine))) constants
-    (Utils.pp_final_char_if_non_empty "@," dependencies)
-    (* dependencies initialization *)
-    (Utils.fprintf_list ~sep:"@," print_import_init) dependencies
-
-let print_global_clear_code  fmt basename prog dependencies =
-  let baseNAME = file_to_module_name basename in
-  let constants = List.map const_of_top (get_consts prog) in
-  fprintf fmt "@[<v 2>%a {@,static %s clear = 0;@,@[<v 2>if (!clear) { @,clear = 1;@,%a%t%a@]@,}@,return;@]@,}@.@."
-    print_global_clear_prototype baseNAME
-    (pp_c_basic_type_desc Type_predef.type_bool)
-    (* constants *) 
-    (Utils.fprintf_list ~sep:"@," (pp_const_clear (pp_c_var_read empty_machine))) constants
-    (Utils.pp_final_char_if_non_empty "@," dependencies)
-    (* dependencies initialization *)
-    (Utils.fprintf_list ~sep:"@," print_import_clear) dependencies
-
-(* TODO: ACSL 
-- a contract machine shall not be directly printed in the C source
-- but a regular machine associated to a contract machine shall integrate the associated statements, updating its memories, at the end of the function body.
-- last one may print intermediate comment/acsl if/when they are present in the sequence of instruction
-*)
-let print_machine dependencies fmt m =
-  if fst (get_stateless_status m) then
-    begin
+      (pp_print_list
+         ~pp_epilogue:pp_print_cut
+         pp_clear_mpfr_local) (mpfr_vars mpfr_locals)
+      (* extra *)
+      pp_extra ()
+
+  let node_of_machine m = {
+    top_decl_desc = Node m.mname;
+    top_decl_loc = Location.dummy_loc;
+    top_decl_owner = "";
+    top_decl_itf = false
+  }
+
+  let print_stateless_code dependencies fmt m =
+    let self = "__ERROR__" in
+    if not (!Options.ansi && is_generic_node (node_of_machine m))
+    then
+      (* C99 code *)
+      pp_print_function
+        ~pp_prototype:print_stateless_prototype
+        ~prototype:(m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs)
+        ~pp_local:(pp_c_decl_local_var m)
+        ~base_locals:m.mstep.step_locals
+        ~pp_init_mpfr_local:(pp_initialize m self (pp_c_var_read m))
+        ~pp_clear_mpfr_local:(pp_clear m self (pp_c_var_read m))
+        ~mpfr_locals:m.mstep.step_locals
+        ~pp_check:(pp_c_check m self)
+        ~checks:m.mstep.step_checks
+        ~pp_instr:(pp_machine_instr dependencies m self)
+        ~instrs:m.mstep.step_instrs
+        fmt
+    else
+      (* C90 code *)
+      let gen_locals, base_locals = List.partition (fun v ->
+          Types.is_generic_type v.var_type) m.mstep.step_locals in
+      let gen_calls = List.map (fun e ->
+          let (id, _, _) = call_of_expr e
+          in mk_call_var_decl e.expr_loc id) m.mname.node_gencalls in
+      pp_print_function
+        ~pp_prototype:print_stateless_prototype
+        ~prototype:(m.mname.node_id,
+                    m.mstep.step_inputs @ gen_locals @ gen_calls,
+                    m.mstep.step_outputs)
+        ~pp_local:(pp_c_decl_local_var m)
+        ~base_locals
+        ~pp_init_mpfr_local:(pp_initialize m self (pp_c_var_read m))
+        ~pp_clear_mpfr_local:(pp_clear m self (pp_c_var_read m))
+        ~mpfr_locals:m.mstep.step_locals
+        ~pp_check:(pp_c_check m self)
+        ~checks:m.mstep.step_checks
+        ~pp_instr:(pp_machine_instr dependencies m self)
+        ~instrs:m.mstep.step_instrs
+        fmt
+
+  let print_reset_code dependencies self fmt m =
+    pp_print_function
+      ~pp_prototype:(print_reset_prototype self)
+      ~prototype:(m.mname.node_id, m.mstatic)
+      ~pp_local:(pp_c_decl_local_var m)
+      ~base_locals:(const_locals m)
+      ~pp_instr:(pp_machine_instr dependencies m self)
+      ~instrs:m.minit
+      fmt
+
+  let print_init_code self fmt m =
+    let minit = List.map (fun i ->
+        match get_instr_desc i with MReset i -> i | _ -> assert false) m.minit in
+    pp_print_function
+      ~pp_prototype:(print_init_prototype self)
+      ~prototype:(m.mname.node_id, m.mstatic)
+      ~pp_array_mem:(pp_c_decl_array_mem self)
+      ~array_mems:(array_mems m)
+      ~pp_init_mpfr_local:(pp_initialize m self (pp_c_var_read m))
+      ~mpfr_locals:m.mmemory
+      ~pp_extra:(fun fmt () ->
+          pp_print_list
+            ~pp_open_box:pp_open_vbox0
+            ~pp_epilogue:pp_print_cut
+            (pp_machine_init m self)
+            fmt minit)
+      fmt
+
+  let print_clear_code self fmt m =
+    let minit = List.map (fun i ->
+        match get_instr_desc i with MReset i -> i | _ -> assert false) m.minit in
+    pp_print_function
+      ~pp_prototype:(print_clear_prototype self)
+      ~prototype:(m.mname.node_id, m.mstatic)
+      ~pp_array_mem:(pp_c_decl_array_mem self)
+      ~array_mems:(array_mems m)
+      ~pp_clear_mpfr_local:(pp_clear m self (pp_c_var_read m))
+      ~mpfr_locals:m.mmemory
+      ~pp_extra:(fun fmt () ->
+          pp_print_list
+            ~pp_open_box:pp_open_vbox0
+            ~pp_epilogue:pp_print_cut
+            (pp_machine_clear m self)
+            fmt minit)
+      fmt
+
+  let print_step_code dependencies self fmt m =
+    if not (!Options.ansi && is_generic_node (node_of_machine m))
+    then
+      (* C99 code *)
+      pp_print_function
+        ~pp_prototype:(print_step_prototype self)
+        ~prototype:(m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs)
+        ~pp_local:(pp_c_decl_local_var m)
+        ~base_locals:m.mstep.step_locals
+        ~pp_array_mem:(pp_c_decl_array_mem self)
+        ~array_mems:(array_mems m)
+        ~pp_init_mpfr_local:(pp_initialize m self (pp_c_var_read m))
+        ~pp_clear_mpfr_local:(pp_clear m self (pp_c_var_read m))
+        ~mpfr_locals:m.mstep.step_locals
+        ~pp_check:(pp_c_check m self)
+        ~checks:m.mstep.step_checks
+        ~pp_instr:(pp_machine_instr dependencies m self)
+        ~instrs:m.mstep.step_instrs
+        fmt
+    else
+      (* C90 code *)
+      let gen_locals, base_locals = List.partition (fun v ->
+          Types.is_generic_type v.var_type) m.mstep.step_locals in
+      let gen_calls = List.map (fun e ->
+          let id, _, _ = call_of_expr e in
+          mk_call_var_decl e.expr_loc id) m.mname.node_gencalls in
+      pp_print_function
+        ~pp_prototype:(print_step_prototype self)
+        ~prototype:(m.mname.node_id,
+                    m.mstep.step_inputs @ gen_locals @ gen_calls,
+                    m.mstep.step_outputs)
+        ~pp_local:(pp_c_decl_local_var m)
+        ~base_locals
+        ~pp_init_mpfr_local:(pp_initialize m self (pp_c_var_read m))
+        ~pp_clear_mpfr_local:(pp_clear m self (pp_c_var_read m))
+        ~mpfr_locals:m.mstep.step_locals
+        ~pp_check:(pp_c_check m self)
+        ~checks:m.mstep.step_checks
+        ~pp_instr:(pp_machine_instr dependencies m self)
+        ~instrs:m.mstep.step_instrs
+        fmt
+
+  (********************************************************************************************)
+  (*                     MAIN C file Printing functions                                       *)
+  (********************************************************************************************)
+
+  let pp_const_initialize m pp_var fmt const =
+    let var = Machine_code_common.mk_val
+        (Var (Corelang.var_decl_of_const const)) const.const_type in
+    let rec aux indices value fmt typ =
+      if Types.is_array_type typ
+      then
+        let dim = Types.array_type_dimension typ in
+        let szl = Utils.enumerate (Dimension.size_const_dimension dim) in
+        let typ' = Types.array_element_type typ in
+        let value = match value with
+          | Const_array ca -> List.nth ca
+          | _ -> assert false in
+        pp_print_list
+          (fun fmt i -> aux (string_of_int i :: indices) (value i) fmt typ') fmt szl
+      else
+        let indices = List.rev indices in
+        let pp_var_suffix fmt var =
+          fprintf fmt "%a%a" (pp_c_val m "" pp_var) var pp_array_suffix indices in
+        fprintf fmt "%a@,%a"
+          (Mpfr.pp_inject_init pp_var_suffix) var
+          (Mpfr.pp_inject_real pp_var_suffix pp_c_const) (var, value)
+    in
+    reset_loop_counter ();
+    aux [] const.const_value fmt const.const_type
+
+  let pp_const_clear pp_var fmt const =
+    let m = Machine_code_common.empty_machine in
+    let var = Corelang.var_decl_of_const const in
+    let rec aux indices fmt typ =
+      if Types.is_array_type typ
+      then
+        let dim = Types.array_type_dimension typ in
+        let idx = mk_loop_var m () in
+        fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"
+          idx idx idx pp_c_dimension dim idx
+          (aux (idx::indices)) (Types.array_element_type typ)
+      else
+        let indices = List.rev indices in
+        let pp_var_suffix fmt var =
+          fprintf fmt "%a%a" (pp_c_var m "" pp_var) var pp_array_suffix indices in
+        Mpfr.pp_inject_clear pp_var_suffix fmt var
+    in
+    reset_loop_counter ();
+    aux [] fmt var.var_type
+
+  let print_import_init fmt dep =
+    let baseNAME = file_to_module_name dep.name in
+    fprintf fmt "%a();" pp_global_init_name baseNAME
+
+  let print_import_clear fmt dep =
+    let baseNAME = file_to_module_name dep.name in
+    fprintf fmt "%a();" pp_global_clear_name baseNAME
+
+  let print_global_init_code fmt (basename, prog, dependencies) =
+    let baseNAME = file_to_module_name basename in
+    let constants = List.map const_of_top (get_consts prog) in
+    fprintf fmt
+      "@[<v 2>%a {@,\
+       static %s init = 0;@,\
+       @[<v 2>if (!init) { @,\
+       init = 1;%a%a@]@,\
+       }@,\
+       return;@]@,\
+       }"
+      print_global_init_prototype baseNAME
+      (pp_c_basic_type_desc Type_predef.type_bool)
+      (* constants *)
+      (pp_print_list
+         ~pp_prologue:pp_print_cut
+         (pp_const_initialize empty_machine (pp_c_var_read empty_machine)))
+      (mpfr_consts constants)
+      (* dependencies initialization *)
+      (pp_print_list
+         ~pp_prologue:pp_print_cut
+         print_import_init) (List.filter (fun dep -> dep.local) dependencies)
+
+  let print_global_clear_code fmt (basename, prog, dependencies) =
+    let baseNAME = file_to_module_name basename in
+    let constants = List.map const_of_top (get_consts prog) in
+    fprintf fmt
+      "@[<v 2>%a {@,\
+       static %s clear = 0;@,\
+       @[<v 2>if (!clear) { @,\
+       clear = 1;%a%a@]@,\
+       }@,\
+       return;@]@,\
+       }"
+      print_global_clear_prototype baseNAME
+      (pp_c_basic_type_desc Type_predef.type_bool)
+      (* constants *)
+      (pp_print_list
+         ~pp_prologue:pp_print_cut
+         (pp_const_clear (pp_c_var_read empty_machine))) (mpfr_consts constants)
+      (* dependencies initialization *)
+      (pp_print_list
+         ~pp_prologue:pp_print_cut
+         print_import_clear) (List.filter (fun dep -> dep.local) dependencies)
+
+  let print_alloc_function fmt m =
+    if (not !Options.static_mem) then
+      (* Alloc functions, only if non static mode *)
+      fprintf fmt
+        "@[<v 2>%a {@,\
+         %a%a@]@,\
+         }@,\
+         @[<v 2>%a {@,\
+         %a%a@]@,\
+         @,"
+        print_alloc_prototype (m.mname.node_id, m.mstatic)
+        print_alloc_const m
+        print_alloc_code m
+        print_dealloc_prototype m.mname.node_id
+        print_alloc_const m
+        print_dealloc_code m
+
+  let print_mpfr_code self fmt m =
+    if !Options.mpfr then
+      fprintf fmt "@,@[<v>%a@,%a@]"
+        (* Init function *)
+        (print_init_code self) m
+        (* Clear function *)
+        (print_clear_code self) m
+
+
+  (* TODO: ACSL
+     - a contract machine shall not be directly printed in the C source
+     - but a regular machine associated to a contract machine shall integrate
+       the associated statements, updating its memories, at the end of the
+       function body.
+     - last one may print intermediate comment/acsl if/when they are present in
+       the sequence of instruction
+  *)
+  let print_machine dependencies fmt m =
+    if fst (get_stateless_status m) then
       (* Step function *)
       print_stateless_code dependencies fmt m
-    end
-  else
-    begin
-      (* Alloc functions, only if non static mode *)
-      if (not !Options.static_mem) then  
-	begin
-	  fprintf fmt "@[<v 2>%a {@,%a%a@]@,}@.@."
-	    print_alloc_prototype (m.mname.node_id, m.mstatic)
-	    print_alloc_const m
-	    print_alloc_code m;
-
-	  fprintf fmt "@[<v 2>%a {@,%a%a@]@,}@.@."
-	    print_dealloc_prototype m.mname.node_id
-	    print_alloc_const m
-	    print_dealloc_code m;
-	end;
+    else
       let self = mk_self m in
-      (* Reset function *)
-      print_reset_code dependencies fmt m self;
-      (* Step function *)
-      print_step_code dependencies fmt m self;
-      
-      if !Options.mpfr then
-	begin
-          (* Init function *)
-	  print_init_code fmt m self;
-          (* Clear function *)
-	  print_clear_code fmt m self;
-	end
-    end
+      fprintf fmt "@[<v>%a%a@,%a%a@]"
+        print_alloc_function m
+        (* Reset function *)
+        (print_reset_code dependencies self) m
+        (* Step function *)
+        (print_step_code dependencies self) m
+        (print_mpfr_code self) m
+
+  let print_import_standard source_fmt () =
+    fprintf source_fmt
+      "@[<v>#include <assert.h>@,%a%a%a@]"
+      (if Machine_types.has_machine_type ()
+       then pp_print_endcut "#include <stdint.h>"
+       else pp_print_nothing) ()
+      (if not !Options.static_mem
+       then pp_print_endcut "#include <stdlib.h>"
+       else pp_print_nothing) ()
+      (if !Options.mpfr
+       then pp_print_endcut "#include <mpfr.h>"
+       else pp_print_nothing) ()
+
+  let print_extern_alloc_prototype fmt ind =
+    let static = List.filter (fun v -> v.var_dec_const) ind.nodei_inputs in
+    fprintf fmt "extern %a;@,extern %a;"
+      print_alloc_prototype (ind.nodei_id, static)
+      print_dealloc_prototype ind.nodei_id
+
+  let print_lib_c source_fmt basename prog machines dependencies =
+    fprintf source_fmt
+      "@[<v>\
+       %a\
+       %a@,\
+       @,\
+       %a@,\
+       %a\
+       %a\
+       %a\
+       %a\
+       %a\
+       %a\
+       @]@."
+      print_import_standard ()
+      print_import_prototype
+      {
+        local = true;
+        name = basename;
+        content = [];
+        is_stateful=true (* assuming it is stateful *);
+      }
+
+      (* Print the svn version number and the supported C standard (C90 or C99) *)
+      pp_print_version ()
+
+      (* Print dependencies *)
+      (pp_print_list
+         ~pp_open_box:pp_open_vbox0
+         ~pp_prologue:(pp_print_endcut "/* Import dependencies */")
+         print_import_prototype
+         ~pp_epilogue:pp_print_cutcut) dependencies
+
+      (* Print consts *)
+      (pp_print_list
+         ~pp_open_box:pp_open_vbox0
+         ~pp_prologue:(pp_print_endcut "/* Global constants (definitions) */")
+         print_const_def
+         ~pp_epilogue:pp_print_cutcut) (get_consts prog)
+
+      (* MPFR *)
+      (if !Options.mpfr then
+         fun fmt () ->
+           fprintf fmt
+             "@[<v>/* Global constants initialization */@,\
+              %a@,\
+              @,\
+              /* Global constants clearing */@,\
+              %a@]@,@,"
+             print_global_init_code (basename, prog, dependencies)
+             print_global_clear_code (basename, prog, dependencies)
+       else pp_print_nothing) ()
+
+      (if not !Options.static_mem then
+         fun fmt () ->
+           fprintf fmt
+             "@[<v>%a%a@]@,@,"
+             (pp_print_list
+                ~pp_open_box:pp_open_vbox0
+                ~pp_epilogue:pp_print_cut
+                ~pp_prologue:(pp_print_endcut
+                                "/* External allocation function prototypes */")
+                (fun fmt dep ->
+                   pp_print_list
+                     ~pp_open_box:pp_open_vbox0
+                     ~pp_epilogue:pp_print_cut
+                     print_extern_alloc_prototype
+                     fmt
+                     (List.filter_map (fun decl -> match decl.top_decl_desc with
+                          | ImportedNode ind when not ind.nodei_stateless ->
+                            Some ind
+                          | _ -> None) dep.content))) dependencies
+             (pp_print_list
+                ~pp_open_box:pp_open_vbox0
+                ~pp_prologue:(pp_print_endcut
+                                "/* Node allocation function prototypes */")
+                ~pp_sep:pp_print_cutcut
+                (fun fmt m ->
+                   fprintf fmt "%a;@,%a;"
+                     print_alloc_prototype (m.mname.node_id, m.mstatic)
+                     print_dealloc_prototype m.mname.node_id)) machines
+       else pp_print_nothing) ()
+
+      (* Print the struct definitions of all machines. *)
+      (pp_print_list
+         ~pp_open_box:pp_open_vbox0
+         ~pp_prologue:(pp_print_endcut "/* Struct definitions */")
+         ~pp_sep:pp_print_cutcut
+         print_machine_struct
+         ~pp_epilogue:pp_print_cutcut) machines
+
+      (* Print nodes one by one (in the previous order) *)
+      (pp_print_list
+         ~pp_open_box:pp_open_vbox0
+         ~pp_sep:pp_print_cutcut
+         (print_machine dependencies)) machines
 
-let print_import_standard source_fmt =
-  begin
-    fprintf source_fmt "#include <assert.h>@.";
-    if Machine_types.has_machine_type () then
-      begin
-	fprintf source_fmt "#include <stdint.h>@."
-      end;
-    if not !Options.static_mem then
-      begin
-	fprintf source_fmt "#include <stdlib.h>@.";
-      end;
-    if !Options.mpfr then
-      begin
-	fprintf source_fmt "#include <mpfr.h>@.";
-      end
-  end
-
-let print_lib_c source_fmt basename prog machines dependencies =
-  print_import_standard source_fmt;
-  print_import_prototype source_fmt {local=true; name=basename; content=[]; is_stateful=true} (* assuming it is stateful *);
-  pp_print_newline source_fmt ();
-  (* Print the svn version number and the supported C standard (C90 or C99) *)
-  print_version source_fmt;
-  (* Print the prototype of imported nodes *)
-  fprintf source_fmt "/* Import dependencies */@.";
-  fprintf source_fmt "@[<v>";
-  List.iter (print_import_prototype source_fmt) dependencies;
-  fprintf source_fmt "@]@.";
-  (* Print consts *)
-  fprintf source_fmt "/* Global constants (definitions) */@.";
-  fprintf source_fmt "@[<v>";
-  List.iter (fun c -> print_const_def source_fmt (const_of_top c)) (get_consts prog);
-  fprintf source_fmt "@]@.";
-  if !Options.mpfr then
-    begin
-      fprintf source_fmt "/* Global constants initialization */@.";
-      print_global_init_code source_fmt basename prog dependencies;
-      fprintf source_fmt "/* Global constants clearing */@.";
-      print_global_clear_code source_fmt basename prog dependencies;
-    end;
-  if not !Options.static_mem then
-    begin
-      fprintf source_fmt "/* External allocation function prototypes */@.";
-      fprintf source_fmt "@[<v>";
-      List.iter (print_extern_alloc_prototypes source_fmt) dependencies;
-      fprintf source_fmt "@]@.";
-      fprintf source_fmt "/* Node allocation function prototypes */@.";
-      fprintf source_fmt "@[<v>";
-      List.iter
-	(fun m -> fprintf source_fmt "%a;@.@.%a;@.@."
-	  print_alloc_prototype (m.mname.node_id, m.mstatic)
-	  print_dealloc_prototype m.mname.node_id
-	)
-	machines;
-      fprintf source_fmt "@]@.";
-    end;
-
-  (* Print the struct definitions of all machines. *)
-  fprintf source_fmt "/* Struct definitions */@.";
-  fprintf source_fmt "@[<v>";
-  List.iter (print_machine_struct source_fmt) machines;
-  fprintf source_fmt "@]@.";
-  pp_print_newline source_fmt ();
-  (* Print nodes one by one (in the previous order) *)
-  List.iter (print_machine dependencies source_fmt) machines;
- end
+end
 
 (* Local Variables: *)
 (* compile-command:"make -C ../../.." *)
diff --git a/src/lusic.ml b/src/lusic.ml
index 1cd5dd8a..1124aca9 100644
--- a/src/lusic.ml
+++ b/src/lusic.ml
@@ -84,18 +84,16 @@ let read_lusic basename extension =
       }
     end
 
-let print_lusic_to_h basename extension =
-  let lusic = read_lusic basename extension in
-  let header_name = basename ^ ".h" in
-  let h_out = open_out header_name in
-  let h_fmt = formatter_of_out_channel h_out in
-  begin
-    assert (not lusic.obsolete);
-    (*Format.eprintf "lusic to h: %i items.@." (List.length lusic.contents);*)
-    Typing.uneval_prog_generics lusic.contents;
-    Clock_calculus.uneval_prog_generics lusic.contents;
-    Header.print_header_from_header h_fmt (Filename.basename basename) lusic.contents;
-    close_out h_out
-  end
-
-
+(* let print_lusic_to_h basename extension =
+ *   let lusic = read_lusic basename extension in
+ *   let header_name = basename ^ ".h" in
+ *   let h_out = open_out header_name in
+ *   let h_fmt = formatter_of_out_channel h_out in
+ *   begin
+ *     assert (not lusic.obsolete);
+ *     (\*Format.eprintf "lusic to h: %i items.@." (List.length lusic.contents);*\)
+ *     Typing.uneval_prog_generics lusic.contents;
+ *     Clock_calculus.uneval_prog_generics lusic.contents;
+ *     Header.print_header_from_header h_fmt (Filename.basename basename) lusic.contents;
+ *     close_out h_out
+ *   end *)
diff --git a/src/options_management.ml b/src/options_management.ml
index 87f90368..b0941726 100644
--- a/src/options_management.ml
+++ b/src/options_management.ml
@@ -11,15 +11,16 @@
 open Options
 
 let print_version () =
-  Format.printf
+  let open Utils.Format in
+  printf
     "@[<v>\
-     Lustrec compiler, version %s (%s)@;\
-     Standard lib: %s@;\
+     Lustrec compiler, version %s (%s)@,\
+     Standard lib: %s@,\
      User provided include directory: @[<h>%a@]\
      @]@."
     version codename
     Version.include_path
-    (Utils.fprintf_list ~sep:"@ " Format.pp_print_string) !include_dirs
+    (pp_print_list ~pp_sep:pp_print_space pp_print_string) !include_dirs
 
 let add_include_dir dir =
   let removed_slash_suffix =
diff --git a/src/plugins/mpfr/lustrec_mpfr.ml b/src/plugins/mpfr/lustrec_mpfr.ml
index cffcb0fd..ee728114 100644
--- a/src/plugins/mpfr/lustrec_mpfr.ml
+++ b/src/plugins/mpfr/lustrec_mpfr.ml
@@ -47,7 +47,7 @@ let inject_id_id expr =
     expr_clock = expr.expr_clock;
   }
 
-let pp_inject_real pp_var pp_val fmt var value =
+let pp_inject_real pp_var pp_val fmt (var, value) =
   Format.fprintf fmt "%s(%a, %a, %s);"
     inject_real_id
     pp_var var
@@ -61,19 +61,19 @@ let inject_assign expr =
     expr_clock = expr.expr_clock;
   }
 
-let pp_inject_copy pp_var fmt var value =
+let pp_inject_copy pp_var fmt (var, value) =
   Format.fprintf fmt "%s(%a, %a, %s);"
     inject_copy_id
     pp_var var
     pp_var value
     (mpfr_rnd ())
 
-let pp_inject_assign pp_var fmt var value =
+let pp_inject_assign pp_var fmt (_, value as vv) =
   if is_const_value value
   then
-    pp_inject_real pp_var pp_var fmt var value
+    pp_inject_real pp_var pp_var fmt vv
   else
-    pp_inject_copy pp_var fmt var value
+    pp_inject_copy pp_var fmt vv
 
 let pp_inject_init pp_var fmt var =
   Format.fprintf fmt "%s(%a, %i);"
diff --git a/src/utils/utils.ml b/src/utils/utils.ml
index 4d12064f..f26f11d7 100644
--- a/src/utils/utils.ml
+++ b/src/utils/utils.ml
@@ -67,7 +67,7 @@ let position pred l =
 
 (* TODO: Lélio: why n+1? cf former def below *)
 (* if n < 0 then [] else x :: duplicate x (n - 1) *)
-let duplicate x n = List.init (n+1) (fun i -> x)
+let duplicate x n = List.init (n+1) (fun _ -> x)
 
 let enumerate n = List.init n (fun i -> i)
 
@@ -251,12 +251,91 @@ let print_rat fmt (a,b) =
 
 (* Generic pretty printing *)
 
+
 let pp_final_char_if_non_empty c l =
   (fun fmt -> match l with [] -> () | _ -> Format.fprintf fmt "%(%)" c)
 
 let pp_newline_if_non_empty l =
   (fun fmt -> match l with [] -> () | _ -> Format.fprintf fmt "@,")
 
+module Format = struct
+  include Format
+  open Format
+
+  let with_out_file file f =
+    let oc = open_out file in
+    let fmt = formatter_of_out_channel oc in
+    f fmt;
+    close_out oc
+
+  let pp_print_nothing _fmt _ = ()
+
+  let pp_print_cutcut fmt () = fprintf fmt "@,@,"
+
+  let pp_print_endcut s fmt () = fprintf fmt "%s@," s
+
+  let pp_print_opar fmt () = pp_print_string fmt "("
+  let pp_print_cpar fmt () = pp_print_string fmt ")"
+  let pp_print_obrace fmt () = pp_print_string fmt "{"
+  let pp_print_cbrace fmt () = pp_print_string fmt "}"
+
+  let pp_print_comma fmt () = fprintf fmt ",@ "
+  let pp_print_semicolon fmt () = fprintf fmt ";@ "
+  let pp_print_comma' fmt () = fprintf fmt ","
+  let pp_print_semicolon' fmt () = fprintf fmt ";"
+
+  let pp_open_vbox0 fmt () = pp_open_vbox fmt 0
+
+  let pp_print_list
+      ?(pp_prologue=pp_print_nothing) ?(pp_epilogue=pp_print_nothing)
+      ?(pp_op=pp_print_nothing) ?(pp_cl=pp_print_nothing)
+      ?(pp_open_box=fun fmt () -> pp_open_box fmt 0)
+      ?(pp_eol=pp_print_nothing) ?pp_sep pp_v fmt l =
+    fprintf fmt "%a%a%a%a%a@]%a%a"
+      (fun fmt l -> if l <> [] then pp_prologue fmt ()) l
+      pp_op ()
+      pp_open_box ()
+      (pp_print_list ?pp_sep pp_v) l
+      (fun fmt l -> if l <> [] then pp_eol fmt ()) l
+      pp_cl ()
+      (fun fmt l -> if l <> [] then pp_epilogue fmt ()) l
+
+  let pp_print_list_i
+      ?pp_prologue ?pp_epilogue ?pp_op ?pp_cl ?pp_open_box ?pp_eol ?pp_sep
+      pp_v =
+    let i = ref 0 in
+    pp_print_list
+      ?pp_prologue ?pp_epilogue ?pp_op ?pp_cl ?pp_open_box ?pp_eol ?pp_sep
+      (fun fmt x -> pp_v fmt !i x; incr i)
+
+  let pp_print_list2
+      ?pp_prologue ?pp_epilogue ?pp_op ?pp_cl ?pp_open_box ?pp_eol ?pp_sep
+      pp_v fmt (l1, l2) =
+    pp_print_list
+      ?pp_prologue ?pp_epilogue ?pp_op ?pp_cl ?pp_open_box ?pp_eol ?pp_sep
+      pp_v fmt (List.combine l1 l2)
+
+  let pp_print_list_i2
+      ?pp_prologue ?pp_epilogue ?pp_op ?pp_cl ?pp_open_box ?pp_eol ?pp_sep
+      pp_v fmt (l1, l2) =
+    pp_print_list_i
+      ?pp_prologue ?pp_epilogue ?pp_op ?pp_cl ?pp_open_box ?pp_eol ?pp_sep
+      (fun fmt i (x1, x2) -> pp_v fmt i x1 x2) fmt (List.combine l1 l2)
+
+  let pp_print_parenthesized ?(pp_sep=pp_print_comma) =
+    pp_print_list
+      ~pp_op:pp_print_opar
+      ~pp_cl:pp_print_cpar
+      ~pp_sep
+
+  let pp_print_braced ?(pp_sep=pp_print_comma) =
+    pp_print_list
+      ~pp_op:pp_print_obrace
+      ~pp_cl:pp_print_cbrace
+      ~pp_sep
+
+end
+
 let fprintf_list ?(eol:('a, formatter, unit) format = "") ~sep:sep f fmt l =
   Format.(pp_print_list ~pp_sep:(fun fmt () -> fprintf fmt "%(%)" sep) f fmt l);
   if l <> [] then Format.fprintf fmt "%(%)" eol
-- 
GitLab