diff --git a/Makefile b/Makefile
index 0cfcfb33..857795ba 100644
--- a/Makefile
+++ b/Makefile
@@ -1,8 +1,5 @@
 ## Build the compiler and libraries
-all: zwrite.exe zeluc.exe
-
-zwrite.exe:
-	(cd src; dune build -- zwrite.exe)
+all: zeluc.exe
 
 zeluc.exe:
 	(cd src; dune build -- zeluc.exe)
@@ -11,7 +8,6 @@ tests:
 	(cd tests; dune test)
 
 debug:
-	(cd src; dune build --debug-backtraces --debug-dependency-path -- zwrite.bc)
 	(cd src; dune build --debug-backtraces --debug-dependency-path -- zeluc.bc)
 
 clean:
diff --git a/src/Makefile b/src/Makefile
index 9af1b8f1..5914f4fa 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -1,10 +1,8 @@
 all:
-	dune build -- zwrite.exe
 	dune build -- zeluc.exe
 	dune build lib
 
 debug:
-	dune build --debug-backtraces --debug-dependency-path -- zwrite.bc
 	dune build --debug-backtraces --debug-dependency-path -- zeluc.bc
 
 clean:
diff --git a/src/compiler/main/compiler.ml b/src/compiler/main/compiler.ml
index 92c2c03d..bd00e2dc 100644
--- a/src/compiler/main/compiler.ml
+++ b/src/compiler/main/compiler.ml
@@ -139,12 +139,28 @@ let compile modname filename =
               (Typing.program info_ff true) p in
     let p = do_optional_step !Misc.no_causality "Causality done. See below:"
               Debug.print_program (Causality.program info_ff) p in
-    let _ = do_optional_step
+    let p = do_optional_step
               !Misc.no_initialization "Initialization done. See below:"
               Debug.print_program (Initialization.program info_ff) p in
     (* Write the symbol table into the interface file *)
     let itc = open_out_bin obj_interf_name in
+    apply_with_close_out Modules.write itc;
     if !Misc.typeonly then raise Stop;
-    apply_with_close_out Modules.write itc
+
+    (* Mark functions calls to be inlined. This step uses type informations *)
+    (* computed during the causality analysis *)
+    let _ = do_step "Mark functions calls to be inlined. See below:"
+	      Debug.print_program Markfunctions.program p in
+
+    (* source-to-source transformations *)
+
+    (* defines the initial global environment for values *)
+    let genv0 = Genv.initialize modname [] in
+    (* Add Stdlib *)
+    let genv0 = Genv.add_module genv0 (Primitives.stdlib_env ()) in
+
+    let _ = Rewrite.main print_message genv0 p !Misc.n_steps in
+
+    ()
   with
   | Stop -> ()
diff --git a/src/compiler/main/zeluc.ml b/src/compiler/main/zeluc.ml
index 761051e9..3c44517a 100644
--- a/src/compiler/main/zeluc.ml
+++ b/src/compiler/main/zeluc.ml
@@ -56,23 +56,38 @@ and doc_simulation =
    \t\t   where <out> is equal to the argument of -o if the flag\n\
    \t\t   has been set, or <node> otherwise"
 and doc_sampling = "<p> \t Sets the sampling period to p (float <= 1.0)"
-and doc_check = "<n> \t Check that the simulated node returns true for n steps"
 and doc_use_gtk = "\t Use lablgtk2 interface."
 and doc_inlining_level = "<n> \t Level of inlining"
 and doc_inline_all = "\t Inline all function calls"
 and doc_dzero = "\t Turn on discrete zero-crossing detection"
 and doc_nocausality = "\t (undocumented)"
-and doc_no_deadcode = "\t (undocumented)"
 and doc_no_initialization = "\t (undocumented)"
 and doc_nosimplify = "\t (undocumented)"
-and doc_noreduce = "\t (undocumented)"
-and doc_lmm = "<n>\t Translate the node into Lustre--"
-and doc_red_name = "\t Static reduction for"
+and doc_no_deadcode = "\t (undocumented)"
 and doc_zsign = "\t Use the sign function for the zero-crossing argument"
 and doc_with_copy = "\t Add of a copy method for the state"
-and doc_rif = "\t Use RIF format over stdin and stdout to communicate I/O to the node being simulated"
 and doc_no_opt = "\t (undocumented)"
 and doc_no_warning = "\t Turn off warnings"
+and doc_check = "<n> \t Check equivalence for that amount of steps"
+and doc_set_steps = "\t Option to control source-to-source rewriting steps\n\
+    \t\t +<s> turn on step s\n\
+    \t\t -<s> turn off step s\n\
+    \t\t s can be: +a: takes all; -a: takes none\n\
+    \t\t static: static reduction \n\
+    \t\t inline: inlining \n\
+    \t\t der: normalize derivative \n\
+    \t\t copylast: add copy equations [lx = last* x] for lasts \n\
+    \t\t lastinpatterns: add copies for lasts that are inputs or outputs \n\
+    \t\t auto: remove automata statements \n\
+    \t\t present: remove present statements \n\
+    \t\t pre: remove pre/fby \n\
+    \t\t reset: normalise resets; remove initialization (->) \n\
+    \t\t complete: complete branches \n\
+    \t\t encore: add an extra step when a zero-crossing \n\
+    \t\t\t change a discrete-time state variable \n\
+    \t\t letin: fuse blocks \n\
+    \t\t schedule: static scheduling \n\
+    \t\t Example: -step -a+step+inline+static. Default is +a."
 let errmsg = "Options are:"
 
 let set_verbose () =
@@ -116,7 +131,10 @@ let main () =
           "-inlineall", Arg.Set inline_all, doc_inline_all;
           "-zsign", Arg.Set zsign, doc_zsign;
           "-copy", Arg.Set with_copy, doc_with_copy;
-          "-rif", Arg.Set use_rif, doc_rif;
+          "-check", Arg.Int set_check_equivalence_for_n_steps, doc_check;
+          "-inline", Arg.Int Misc.set_inlining_level, doc_inlining_level;
+          "-inlineall", Arg.Set inline_all, doc_inline_all;
+          "-step", Arg.String Rewrite.set_steps, doc_set_steps;
       ])
       compile
       errmsg;
diff --git a/src/compiler/main/zwrite.ml b/src/compiler/main/zwrite.ml
deleted file mode 100644
index 52e868b9..00000000
--- a/src/compiler/main/zwrite.ml
+++ /dev/null
@@ -1,100 +0,0 @@
-(***********************************************************************)
-(*                                                                     *)
-(*                                                                     *)
-(*                        The ZRun Interpreter                         *)
-(*                                                                     *)
-(*                             Marc Pouzet                             *)
-(*                                                                     *)
-(*  (c) 2020-2024 Inria Paris                                          *)
-(*                                                                     *)
-(*  Copyright Institut National de Recherche en Informatique et en     *)
-(*  Automatique. All rights reserved. This file is distributed under   *)
-(*  the terms of the INRIA Non-Commercial License Agreement (see the   *)
-(*  LICENSE file).                                                     *)
-(*                                                                     *)
-(* *********************************************************************)
-
-
-(* the main *)
-open Misc
-   
-let main file =
-  if Filename.check_suffix file ".zls"
-  then 
-    let filename = Filename.chop_extension file in
-    let modname = String.capitalize_ascii (Filename.basename filename) in
-    let n_steps = !equivalence_checking in
-    Rewrite.main modname filename n_steps 
-  else raise (Arg.Bad "Expected *.zls file.")
-
-let doc_main = "\tThe main node to evaluate"
-let doc_all = "\tEvaluate all nodes"
-let doc_number_of_steps = "\tThe number of steps"
-let doc_verbose = "\tVerbose mode"
-let doc_vverbose = "\t Set even more verbose mode"
-let doc_debug = "\t Set debug mode"
-let doc_no_assert = "\tNo check of assertions"
-let doc_nocausality = "\tTurn off the check that all variables are non bottom"
-let doc_print_values = "\tPrint values"
-let doc_number_of_fixpoint_iterations =
-  "\tPrint the number of steps for fixpoints"
-let doc_esterel =
-  "\tSets the interpretation of if/then/else to be constructive"
-let doc_lustre =
-  "\tSets the interpretation of if/then/else to be strict \n\
-   \t\t(that of Lustre)"
-let doc_static_reduction =
-  "\tReduce static (compile-time) expressions"
-let doc_check =
-  "<n> \t Check equivalence for that amount of steps"
-and doc_inlining_level = "<n> \t Level of inlining"
-and doc_inline_all = "\t Inline all function calls"
-and doc_set_steps = "\t Option to control source-to-source rewriting steps\n\
-    \t\t +<s> turn on step s\n\
-    \t\t -<s> turn off step s\n\
-    \t\t s can be: +a: takes all; -a: takes none\n\
-    \t\t static: static reduction \n\
-    \t\t inline: inlining \n\
-    \t\t der: normalize derivative \n\
-    \t\t copylast: add copy equations [lx = last* x] for lasts \n\
-    \t\t lastinpatterns: add copies for lasts that are inputs or outputs \n\
-    \t\t auto: remove automata statements \n\
-    \t\t present: remove present statements \n\
-    \t\t pre: remove pre/fby \n\
-    \t\t reset: normalise resets; remove initialization (->) \n\
-    \t\t complete: complete branches \n\
-    \t\t encore: add an extra step when a zero-crossing \n\
-    \t\t\t change a discrete-time state variable \n\
-    \t\t letin: fuse blocks \n\
-    \t\t schedule: static scheduling \n\
-    \t\t Example: -step -a+step+inline+static. Default is +a."
-let errmsg = "Options are:"
-
-
-let main () =
-  try
-    Arg.parse
-      (Arg.align
-         [ "-v", Arg.Unit Misc.set_verbose, doc_verbose;
-           "-vv", Arg.Unit Misc.set_vverbose, doc_vverbose;
-           "-debug", Arg.Unit Misc.set_debug, doc_debug;
-           "-print", Arg.Set Misc.print_values, doc_print_values;
-           "-noassert", Arg.Set Misc.no_assert, doc_no_assert;
-           "-nocausality", Arg.Set Misc.no_causality, doc_nocausality;
-           "-fix", Arg.Set Misc.print_number_of_fixpoint_iterations,
-           doc_number_of_fixpoint_iterations;
-           "-esterel", Arg.Set Misc.esterel, doc_esterel;
-           "-lustre", Arg.Set Misc.lustre, doc_lustre;
-           "-check", Arg.Int set_equivalence_checking, doc_check;
-           "-inline", Arg.Int Misc.set_inlining_level, doc_inlining_level;
-           "-inlineall", Arg.Set inline_all, doc_inline_all;
-           "-step", Arg.String Rewrite.set_steps, doc_set_steps;
-      ])
-      main
-      errmsg
-  with
-  | Misc.Error -> exit 2
-                 
-let _ = main ()
-let _ = exit 0
-            
diff --git a/src/compiler/rewrite/markfunctions.ml b/src/compiler/rewrite/markfunctions.ml
index 48fd23f3..2cd982c2 100644
--- a/src/compiler/rewrite/markfunctions.ml
+++ b/src/compiler/rewrite/markfunctions.ml
@@ -3,7 +3,7 @@
 (*                                                                     *)
 (*          Zelus, a synchronous language for hybrid systems           *)
 (*                                                                     *)
-(*  (c) 2020 Inria Paris (see the AUTHORS file)                        *)
+(*  (c) 2024 Inria Paris (see the AUTHORS file)                        *)
 (*                                                                     *)
 (*  Copyright Institut National de Recherche en Informatique et en     *)
 (*  Automatique. All rights reserved. This file is distributed under   *)
@@ -18,7 +18,7 @@
 
 open Zelus
 
-type info =
+type io_table =
   { inputs: Causal.S.t; (* the causality tags of inputs of the function *)
     outputs: Causal.S.t; (* the causality tags of outputs *)
     o_table: Causal.S.t Causal.M.t; (* outputs of a causality tag *)
@@ -48,122 +48,44 @@ type info =
  *- on all of its inputs *)
 
 (* compute the set of causality tags that appear as input/outputs *)
-(* of function applications *)
-let funexp_info { f_args = p_list; f_body = ({ e_caus = tc } as e) } =
-  let rec exp c_set { e_desc = desc; e_caus = tc } =
-    match desc with
-    | Elocal _ | Eglobal _ | Econst _
-    | Econstr0 _ | Elast _ -> c_set
-    | Eapp(_, op, arg_list) ->
-        let c_set = List.fold_left exp (exp c_set op) arg_list in
-        (* compute the set of causality tags *)
-        let tc_list = List.map (fun { e_caus = tc } -> tc) (op :: arg_list) in
-        List.fold_left Causal.vars (Causal.vars c_set tc) tc_list
-    | Eop(_, e_list) | Etuple(e_list)
-    | Econstr1(_, e_list) -> List.fold_left exp c_set e_list
-    | Erecord_access(e, _) | Etypeconstraint(e, _) -> exp c_set e
-    | Erecord(m_e_list) ->
-        List.fold_left (fun acc (_, e) -> exp acc e) c_set m_e_list
-    | Erecord_with(e_record, m_e_list) ->
-       List.fold_left (fun acc (_, e) -> exp acc e)
-		      (exp c_set e_record) m_e_list
-    | Epresent(p_h_list, e_opt) ->
-        let c_set =
-          List.fold_left
-            (fun acc { p_body = e } -> exp acc e) c_set p_h_list in
-        Zmisc.optional exp c_set e_opt
-    | Ematch(_, e, m_h_list) ->
-        List.fold_left
-          (fun acc { m_body = e } -> exp acc e) (exp c_set e) m_h_list
-    | Elet(l, e) -> exp (local c_set l) e
-    | Eblock(b, e) ->  exp (block_eq_list c_set b) e
-    | Eseq(e1, e2) -> exp (exp c_set e1) e2
-    | Eperiod  { p_phase = p1; p_period = p2 }  ->
-       let c_set = Zmisc.optional exp c_set p1 in
-       exp c_set p2
-
-  and local c_set { l_eq = eq_list } = List.fold_left equation c_set eq_list
-      
-  and equation c_set { eq_desc = desc } =
-    match desc with
-    | EQeq(_, e) | EQpluseq(_, e) | EQinit(_, e) -> exp c_set e
-    | EQder(_, e, e_opt, p_h_list) ->
-        let c_set = Zmisc.optional exp (exp c_set e) e_opt in
-        List.fold_left (fun acc { p_body = e } -> exp acc e) c_set p_h_list
-    | EQnext(n, e, e_opt) ->
-        Zmisc.optional exp (exp c_set e) e_opt
-    | EQautomaton(_, s_h_list, se_opt) ->
-        let c_set =
-          List.fold_left
-            (fun acc { s_body = b_eq_list; s_trans = s_trans } ->
-               let acc = block_eq_list acc b_eq_list in
-               List.fold_left
-                 (fun acc
-                   { e_cond = scpat; e_block = b_opt; e_next_state = se } ->
-                   let c_set = scondpat acc scpat in
-                   let c_set = Zmisc.optional block_eq_list c_set b_opt in
-                   state c_set se)
-                 acc s_trans)
-            c_set s_h_list in
-        Zmisc.optional state c_set se_opt
-    | EQpresent(p_h_list, b_opt) ->
-        let c_set =
-          List.fold_left
-            (fun acc { p_cond = scpat; p_body = b_eq_list } ->
-               let acc = scondpat acc scpat in
-               block_eq_list acc b_eq_list) c_set p_h_list in
-        Zmisc.optional block_eq_list c_set b_opt
-    | EQmatch(_, e, m_h_list) ->
-        List.fold_left
-          (fun acc { m_body = b_eq_list } -> block_eq_list acc b_eq_list)
-          (exp c_set e) m_h_list
-    | EQreset(res_eq_list, e) ->
-        List.fold_left equation (exp c_set e) res_eq_list
-    | EQand(eq_list) | EQbefore(eq_list) ->
-        List.fold_left equation c_set eq_list
-    | EQemit(_, e_opt) -> Zmisc.optional exp c_set e_opt
-    | EQblock(b) -> block_eq_list c_set b
-    | EQforall({ for_index = i_list; for_init = init_list;
-	         for_body = b_eq_list }) ->
-        let index c_set { desc = desc } =
-	  match desc with
-          | Einput(_, e) -> exp c_set e
-          | Eindex(_, e1, e2) -> exp (exp c_set e1) e2
-          | Eoutput _ -> c_set in
-        let init c_set { desc = desc } =
-	  match desc with
-          | Einit_last(_, e) -> exp c_set e in
-        let c_set = List.fold_left index c_set i_list in
-        let c_set = List.fold_left init c_set init_list in
-        block_eq_list c_set b_eq_list
-        
-  and scondpat c_set { desc = desc } =
-    match desc with
-    | Econdand(sc1, sc2) | Econdor(sc1, sc2) ->
-        scondpat (scondpat c_set sc1) sc2
-    | Econdexp(e) | Econdpat(e, _) -> exp c_set e
-    | Econdon(sc, e) -> scondpat (exp c_set e) sc
-			  
-  and state c_set { desc = desc } =
-    match desc with
-    | Estate0 _ -> c_set
-    | Estate1(_, e_list) -> List.fold_left exp c_set e_list
-                              
-  and block_eq_list c_set { b_locals = l_list; b_body = eq_list } =
-    let c_set = List.fold_left local c_set l_list in
-    List.fold_left equation c_set eq_list in
-
-  (* First: compute the inputs/outputs of the main function *)
-  let tc_list = List.map (fun { p_caus = tc } -> tc) p_list in
+(* of function applications inside the body of the function *)
+let funexp_build_io_table { f_args; f_body = ({ r_info } as r) } =
+  (* traverses the body *)
+  let result c_set r =
+    let expression funs c_set ({ e_desc; e_info } as e) =
+      match e_desc with
+      | Eapp { f; arg_list } ->
+         let _, c_set = Util.mapfold (Mapfold.expression_it funs) c_set arg_list in
+         (* compute the set of causality tags *)
+         let tc_list =
+           List.map (fun { e_info } -> Typinfo.get_caus e_info) (arg_list) in
+         let tc = Typinfo.get_caus f.e_info in
+         let c_set =
+           List.fold_left Causal.vars (Causal.vars c_set tc) tc_list in
+         e, c_set
+      | _ -> Mapfold.expression_it funs c_set e in
+    let global_funs = Mapfold.default_global_funs in
+    let funs =  { Mapfold.defaults with expression; global_funs } in
+    let _, c_set = Mapfold.result_it funs c_set r in
+    c_set in
 
+  (* Compute the inputs/outputs of the main function *)
+  let tc_list =
+    let arg acc a =
+      List.fold_left
+        (fun acc { var_info } -> Typinfo.get_caus var_info :: acc) acc a in
+    List.fold_left arg [] f_args in
+  
+  let tc = Typinfo.get_caus r_info in
+  
   (* mark inputs/outputs *)
   List.iter (Causal.mark_and_polarity false) tc_list;
   Causal.mark_and_polarity true tc;
   let c_set =
     Causal.vars (List.fold_left Causal.vars Causal.S.empty tc_list) tc in
   let inputs, outputs = Causal.ins_and_outs c_set in
-  (* computes the set of causality tags that appear in [e] *)
-  let c_set = exp c_set e in
+  (* computes the set of causality tags that appear in [f_body] *)
+  let c_set = result c_set r in
 
   (* compute the table of outputs for all the variables *)
   let o_table = Causal.build_o_table c_set Causal.M.empty in
@@ -175,9 +97,9 @@ let funexp_info { f_args = p_list; f_body = ({ e_caus = tc } as e) } =
     io_table = io_table;
     o_table = o_table }
   
-(* The function which decides whether or not a function call *)
+(* [to_inline] The function which decides whether or not a function call *)
 (* [f(arg1,...,argn) must be inlined *)
-let to_inline { io_table = io_table; o_table = o_table } tc_arg_list tc_res =
+let to_inline { io_table; o_table } tc_arg_list tc_res =
   let _, out_of_inputs =
     List.fold_left
       (Causal.ins_and_outs_of_a_type true) (Causal.S.empty, Causal.S.empty)
@@ -217,138 +139,42 @@ let to_inline { io_table = io_table; o_table = o_table } tc_arg_list tc_res =
   | Causal.Clash _ -> assert false
  
 (* Mark function calls to be inlined *)
-let funexp_mark_to_inline info ({ f_body = e } as funexp) =
-  (* generic translation for match handlers *)
-  let match_handler body ({ m_body = b } as m_h) =
-    { m_h with m_body = body b } in
-  
-  (* generic translation function for present handlers *)
-  let present_handler scondpat body ({ p_cond = sc; p_body = b } as p_h) =
-    { p_h with p_cond = scondpat sc; p_body = body b } in
-
+let funexp_apply_io_table io_table ({ f_body } as f) =
   (* expressions *)
-  let rec exp ({ e_desc = desc; e_caus = tc } as e) =
-    let desc = match desc with
-      | Elocal _ | Eglobal _ | Econst _
-      | Econstr0 _ | Elast _ | Eperiod _ -> desc
-      | Eop(op, e_list) -> Eop(op, List.map exp e_list)
-      | Eapp({ app_inline = i } as app, op, arg_list) ->
-          (* only fully applied functions can be inlined *)
-	  let op = exp op in
-          let arg_list = List.map exp arg_list in
-          let i =
-            if i then true
-            else let tc_arg_list =
-                   List.map (fun { e_caus = tc } -> tc) (op :: arg_list) in
-                 to_inline info tc_arg_list tc in
-          Eapp({ app with app_inline = i }, op, arg_list)
-      | Etuple(e_list) -> Etuple(List.map exp e_list)
-      | Econstr1(c, e_list) -> Econstr1(c, List.map exp e_list)
-      | Erecord_access(e_record, m) -> Erecord_access(exp e_record, m)
-      | Erecord(m_e_list) ->
-	 Erecord(List.map (fun (m, e) -> (m, exp e)) m_e_list)
-      | Erecord_with(e_record, m_e_list) ->
-	 Erecord_with(exp e_record,
-		      List.map (fun (m, e) -> (m, exp e)) m_e_list)
-      | Etypeconstraint(e, ty) -> Etypeconstraint(exp e, ty)
-      | Epresent(p_h_list, e_opt) ->
-	  Epresent(List.map (present_handler scondpat exp) p_h_list,
-	           Zmisc.optional_map exp e_opt)
-      | Ematch(total, e, m_h_list) ->
-	 Ematch(total, exp e, List.map (match_handler exp) m_h_list)
-      | Elet(l, e) -> Elet(local l, exp e)
-      | Eblock(b, e) -> Eblock(block_eq_list b, exp e)
-      | Eseq(e1, e2) -> Eseq(exp e1, exp e2) in
-    { e with e_desc = desc }
+  let expression funs acc ({ e_desc; e_info } as e) =
+    match e_desc with
+    | Eapp { is_inline; f; arg_list } ->
+       (* only fully applied functions can be inlined *)
+       let op, _ = Mapfold.expression_it funs acc f in
+       let arg_list, _ =
+         Util.mapfold (Mapfold.expression_it funs) acc arg_list in
+       let is_inline =
+         if is_inline then true
+         else
+           let tc_res = Typinfo.get_caus e_info in
+           let tc_arg_list =
+             List.map
+               (fun { e_info } -> Typinfo.get_caus e_info) (op :: arg_list) in
+           to_inline io_table tc_arg_list tc_res in
+       { e with e_desc = Eapp({ is_inline; f; arg_list }) }, acc
+    | _ -> Mapfold.expression_it funs acc e in
+  let global_funs = Mapfold.default_global_funs in
+  let funs =  { Mapfold.defaults with expression; global_funs } in
+  let f_body, _= Mapfold.result_it funs () f_body in
+  { f with f_body }, io_table
 
-  and local ({ l_eq = eq_list } as l) =
-  { l with l_eq = List.map equation eq_list }
+let funexp funs _ f =
+  let io_table = funexp_build_io_table f in
+  let f, _ = funexp_apply_io_table io_table f in
+  f, ()
 
-  and equation ({ eq_desc = desc } as eq) =
-    let desc = match desc with
-      | EQeq(p, e) -> EQeq(p, exp e)
-      | EQpluseq(n, e) -> EQpluseq(n, exp e)
-      | EQder(n, e, e_opt, p_h_list) ->
-          EQder(n, exp e, Zmisc.optional_map exp e_opt,
-	        List.map (present_handler scondpat exp) p_h_list)
-      | EQinit(n, e) -> EQinit(n, exp e)
-      | EQnext(n, e, e_opt) ->
-          EQnext(n, exp e, Zmisc.optional_map exp e_opt)
-      | EQautomaton(is_weak, s_h_list, se_opt) ->
-          EQautomaton(is_weak, List.map state_handler s_h_list,
-		      Zmisc.optional_map state se_opt)
-      | EQpresent(p_h_list, b_opt) ->
-          EQpresent(List.map (present_handler scondpat block_eq_list) p_h_list,
-		    Zmisc.optional_map block_eq_list b_opt)
-      | EQmatch(total, e, m_h_list) ->
-          EQmatch(total, exp e,
-	          List.map (match_handler block_eq_list) m_h_list)
-      | EQreset(res_eq_list, e) ->
-          EQreset(List.map equation res_eq_list, exp e)
-      | EQand(and_eq_list) ->
-          EQand(List.map equation and_eq_list)
-      | EQbefore(before_eq_list) ->
-          EQbefore(List.map equation before_eq_list)
-      | EQemit(n, e_opt) ->
-          EQemit(n, Zmisc.optional_map exp e_opt)
-      | EQblock(b) -> EQblock(block_eq_list b)
-      | EQforall({ for_index = i_list; for_init = init_list;
-		   for_body = b_eq_list } as body) ->
-          let index ({ desc = desc } as ind) =
-	    let desc = match desc with
-                | Einput(x, e) -> Einput(x, exp e)
-	        | Eindex(x, e1, e2) ->
-                     Eindex(x, exp e1, exp e2)
-	        | Eoutput _ -> desc in
-            { ind with desc = desc } in
-          let init ({ desc = desc } as ini) =
-	    let desc = match desc with
-	        | Einit_last(x, e) -> Einit_last(x, exp e) in
-            { ini with desc = desc } in
-          let i_list = List.map index i_list in
-          let init_list = List.map init init_list in
-          let b_eq_list = block_eq_list b_eq_list in
-          EQforall { body with for_index = i_list; for_init = init_list;
-			       for_body = b_eq_list } in
-    { eq with eq_desc = desc }
+let program p =
+  let global_funs = Mapfold.default_global_funs in
+  let funs =
+    { Mapfold.defaults with funexp; global_funs } in
+  let { p_impl_list } as p, _ =
+    Mapfold.program_it funs () p in
+  { p with p_impl_list = p_impl_list }
 
-  and scondpat ({ desc = desc } as sc) =
-    let desc = match desc with
-      | Econdand(sc1, sc2) -> Econdand(scondpat sc1, scondpat sc2)
-      | Econdor(sc1, sc2) -> Econdor(scondpat sc1, scondpat sc2)
-      | Econdexp(e) -> Econdexp(exp e)
-      | Econdpat(e, p) -> Econdpat(exp e, p)
-      | Econdon(sc, e) -> Econdon(scondpat sc, exp e) in
-    { sc with desc = desc }     
-    
-  and state_handler ({ s_body = b; s_trans = trans } as sh) =
-    { sh with s_body = block_eq_list b; s_trans = List.map escape trans }
-    
-  and state ({ desc = desc } as se) =
-    let desc = match desc with
-      | Estate0 _ -> desc
-      | Estate1(id, e_list) ->
-          Estate1(id, List.map exp e_list) in
-    { se with desc = desc }
-    
-  and block_eq_list ({ b_locals = l_list; b_body = eq_list } as b) =
-    { b with b_locals = List.map local l_list;
-	     b_body = List.map equation eq_list }
-    
-  and escape ({ e_cond = sc; e_block = b_opt; e_next_state = se } as esc) =
-    { esc with e_cond = scondpat sc;
-	       e_block = Zmisc.optional_map block_eq_list b_opt;
-	       e_next_state = state se } in
 
-  { funexp with f_body = exp e }
     
-let implementation impl =
-  match impl.desc with
-  | Eopen _ | Etypedecl _ | Econstdecl _ -> impl
-  | Efundecl(n, funexp) ->
-      let info = funexp_info funexp in
-      let funexp = funexp_mark_to_inline info funexp in
-      { impl with desc = Efundecl(n, funexp) }
-
-let implementation_list impl_list =
-  Zmisc.iter implementation impl_list
diff --git a/src/compiler/main/rewrite.ml b/src/compiler/rewrite/rewrite.ml
similarity index 55%
rename from src/compiler/main/rewrite.ml
rename to src/compiler/rewrite/rewrite.ml
index 510537cd..15841b12 100644
--- a/src/compiler/main/rewrite.ml
+++ b/src/compiler/rewrite/rewrite.ml
@@ -12,66 +12,37 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-(* the main functions *)
+(* the sequence of source-to-source transformations applied to the input program *)
 open Misc
 open Location
                
-exception Stop
-
-let lexical_error err loc =
-  Format.eprintf "%aIllegal character.@." output_location loc;
-  raise Error
-
-let syntax_error loc =
-  Format.eprintf "%aSyntax error.@." output_location loc;
-  raise Error
-
-let parse parsing_fun lexing_fun source_name =
-  let ic = open_in source_name in
-  let lexbuf = Lexing.from_channel ic in
-  lexbuf.Lexing.lex_curr_p <-
-    { lexbuf.Lexing.lex_curr_p with Lexing.pos_fname = source_name };
-  try
-    parsing_fun lexing_fun lexbuf
-  with
-  | Lexer.Lexical_error(err, loc) ->
-     close_in ic; lexical_error err loc
-  | Parser.Error ->
-     close_in ic;
-     syntax_error
-       (Loc(Lexing.lexeme_start lexbuf, Lexing.lexeme_end lexbuf))
-     
-let parse_implementation_file source_name =
-  parse Parser.implementation_file Lexer.main source_name
-               
-let apply_with_close_out f o =
-  try
-    f o;
-    close_out o
-  with x -> close_out o; raise x
-
-let print_message comment =
-  if !verbose then
-    Format.fprintf Format.err_formatter
-      "@[------------------------------------------------------------------\n\
-       %s\n\
-       --------------------------------------------------------------------@]@."
-      comment
+let hybrid_list =
+  ["der", "Remove handlers in definitions of derivatives. See below:",
+   Der.program;
+   "period", "Translation of periods done. See below:",
+   Period.program;
+   "disc", "Translation of disc done. See below:",
+   Disc.program]
 
-let do_step comment output step input = 
-  print_message comment;
-  let o = step input in
-  output o;
-  o
+(*
+let optim_list =
+  ["horizon",
+   "Gather all horizons into a single one per function. See below:",
+   Horizon.program;
+   "aform", "A-normal form. See below:",
+   Aform.program;
+   "deadcode", "Dead-code removal. See below:",
+   Deadcode.program;
+   "copy", "Remove of copy variables. See below:",
+   Copy.program]
+*)
 
 let default_list =
   ["static", "Static reduction done. See below:",
    Static.program;
    "inline", "Inlining done. See below:",
-   Inline.program;
-   "der", "Remove handlers in definitions of derivatives. See below:",
-   Der.program;
-   "auto", "Translation of automata. See below:",
+   Inline.program] @ hybrid_list @ [
+   "automata", "Translation of automata. See below:",
    Automata.program;
    "present", "Translation of present. See below:",
    Present.program;
@@ -119,7 +90,7 @@ let set_steps w =
   List.iter
     (fun l -> set true (List.hd l); List.iter (fun s -> set false s) (List.tl l))
     l_l
-let rewrite_list () =
+let rewrite_list =
   List.filter (fun (w, _, _) -> S.mem w !s_set) default_list
 
 let compare name n_steps genv0 p p' =
@@ -131,43 +102,14 @@ let compare name n_steps genv0 p p' =
   Coiteration.check n_steps genv genv'; p'
     
 (* Apply a sequence of source-to-source transformation *)
-(* do equivalence checking for every step if the flag is turned on *)
-let main modname filename n_steps =
-  let transform_and_compare genv p (name, comment, transform) =
-    let p' = transform genv p in
+(* do equivalence checking for every step if [n_steps <> 0] *)
+let main print_message genv0 p n_steps =
+  let rewrite_and_compare genv p (name, comment, rewrite) =
+    let p' = rewrite genv p in
     print_message comment;
     Debug.print_program p';
     if n_steps = 0 then p' else compare name n_steps genv p p' in
     
-  let iter genv p l = List.fold_left (transform_and_compare genv) p l in
-  
-  let _ = Format.std_formatter in
-  
-  (* output file in which values are stored *)
-  let obj_name = filename ^ ".zlo" in
-  let otc = open_out_bin obj_name in
-  let source_name = filename ^ ".zls" in
-  (* set the current opened module *)
-  Location.initialize source_name;
-
-  (* Parsing *)
-  let p = parse_implementation_file source_name in
-  Debug.print_message "Parsing done";
-
-  (* defines the initial global environment for values *)
-  let genv0 = Genv.initialize modname [] in
-  (* Add Stdlib *)
-  let genv0 = Genv.add_module genv0 (Primitives.stdlib_env ()) in
+  let iter genv p l = List.fold_left (rewrite_and_compare genv) p l in
   
-  (* Associate unique index to variables *)
-  let module Scoping = Scoping.Make(Typinfo) in
-  let p = do_step "Scoping done. See below:" Debug.print_program
-            Scoping.program p in
-  (* Write defined variables for equations *)
-  let module Write = Write.Make(Typinfo) in
-  let p = do_step "Write done. See below: "
-      Debug.print_program Write.program p in
-  (* Source-to-source transformations start here *)
-  let _ = iter genv0 p (rewrite_list ()) in
-
-  apply_with_close_out (fun _ -> ()) otc
+  iter genv0 p rewrite_list
diff --git a/src/compiler/typing/typing.ml b/src/compiler/typing/typing.ml
index 53e75a09..9d2be6a7 100644
--- a/src/compiler/typing/typing.ml
+++ b/src/compiler/typing/typing.ml
@@ -1236,7 +1236,7 @@ let implementation ff is_first { desc; loc } =
     | Eopen(modname) ->
        if is_first then Modules.open_module modname
     | Eletdecl { d_leq } ->
-       let new_h, actual_k = leq (Tfun(Tconst)) Env.empty d_leq in
+       let new_h, actual_k = leq (Tfun(Tany)) Env.empty d_leq in
        (* check that there is no unbounded size variables *)
        check_no_unbounded_size_name loc new_h;
        (* update the global environment *)
diff --git a/src/ctests/good/1.zci b/src/ctests/good/1.zci
new file mode 100644
index 00000000..aab538cc
Binary files /dev/null and b/src/ctests/good/1.zci differ
diff --git a/src/ctests/good/2.zci b/src/ctests/good/2.zci
new file mode 100644
index 00000000..66c71bae
Binary files /dev/null and b/src/ctests/good/2.zci differ
diff --git a/src/ctests/good/3.zci b/src/ctests/good/3.zci
index 4125ee47..8165b3c2 100644
Binary files a/src/ctests/good/3.zci and b/src/ctests/good/3.zci differ
diff --git a/src/ctests/good/3.zls b/src/ctests/good/3.zls
index 3f97dfa8..bfd7b858 100644
--- a/src/ctests/good/3.zls
+++ b/src/ctests/good/3.zls
@@ -1,11 +1,10 @@
 let node f1 () returns (o)
   if true then o = 1 else o = 2
 
-(*
 let node f2 () returns (o)
   automaton
   | A -> do o = 1 until true then B
   | B -> do o = 2 until false then A
   init
     if true then B else A
-  end *)
+  end
\ No newline at end of file
diff --git a/src/dune b/src/dune
index 8535af5b..dc70f906 100644
--- a/src/dune
+++ b/src/dune
@@ -116,15 +116,26 @@
   (libraries zelus.global_lib zelus.typdefs_lib)
 )
 
-; causality and initialisation analyses
+; causality analysis
  (library
-  (name analyses_lib)
-  (public_name zelus.analyses_lib)
+  (name causality_lib)
+  (public_name zelus.causality_lib)
   (wrapped false)
   (modules
     causal ; type manipulation and unification between types for causality
-    init ;  type manipulation and unification between types for initialisation
     causality ; causality inference
+    )
+  (libraries zelus.global_lib zelus.typdefs_lib zelus.common_lib
+   zelus.typing_lib)
+)
+
+; initialisation analysis
+ (library
+  (name initialization_lib)
+  (public_name zelus.initialization_lib)
+  (wrapped false)
+  (modules
+    init ;  type manipulation and unification between types for initialisation
     initialization ; initialization inference
     )
   (libraries zelus.global_lib zelus.typdefs_lib zelus.common_lib
@@ -141,6 +152,7 @@
     cost ; a cost function used to decide which function call to inline
     mapfold ; generic mapfold
     aux ; auxiliary functions for building terms
+    markfunctions ; mark function calls to be inlined
     static ; static reduction
     inline ; inlining of function calls
     der ; remove the initialization and handler part of a derivative equation
@@ -164,7 +176,8 @@
     schedule ; static scheduling
     rewrite ; compose rewriting steps
   )
-  (libraries zelus.global_lib zelus.typdefs_lib zelus.common_lib zelus.zrun_lib)
+  (libraries zelus.global_lib zelus.typdefs_lib zelus.common_lib
+   zelus.causality_lib zelus.zrun_lib)
 )
 
 ;sequential code generation
@@ -181,16 +194,6 @@
   (libraries zelus.global_lib zelus.typdefs_lib)
 )
 
-; Source-to-source transformations
-(executable
- (name zwrite)
-  (modes (byte exe))
-  (modules
-	zwrite; the main function
-  )
-  (libraries zelus.parser_lib zelus.global_lib zelus.zrun_lib zelus.rewrite_lib)
-  (promote (until-clean) (into ..)))
-
 ; The compiler
 (executable
  (name zeluc)
@@ -201,7 +204,7 @@
 	zeluc; the main function
   )
   (libraries zelus.parser_lib zelus.global_lib zelus.zrun_lib
-  zelus.typing_lib zelus.analyses_lib zelus.rewrite_lib)
+  zelus.typing_lib zelus.causality_lib zelus.initialization_lib zelus.rewrite_lib)
   (promote (until-clean) (into ..)))
 
 (install
diff --git a/src/global/misc.ml b/src/global/misc.ml
index 21599945..7c6a289c 100644
--- a/src/global/misc.ml
+++ b/src/global/misc.ml
@@ -141,8 +141,8 @@ let lustre = ref false
 let static_reduction = ref false
 
 (* check equivalence *)
-let equivalence_checking = ref 0
-let set_equivalence_checking n = equivalence_checking := n
+let n_steps = ref 0
+let set_check_equivalence_for_n_steps n = n_steps := n
 
 (* sets the inline flags *)
 let inlining_level = ref 10
diff --git a/src/typdefs/typinfo.ml b/src/typdefs/typinfo.ml
index 813fdd93..6c4cfba0 100644
--- a/src/typdefs/typinfo.ml
+++ b/src/typdefs/typinfo.ml
@@ -39,3 +39,4 @@ let set_caus typinfo tc = { typinfo with t_caus = tc }
 let set_init typinfo ti = { typinfo with t_init = ti }
 
 let get_type { t_typ } = t_typ
+let get_caus { t_caus } = t_caus