diff --git a/src/checks/init_calculus.mli b/src/checks/init_calculus.mli
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/src/compiler_common.mli b/src/compiler_common.mli
index d0bf81963e1b8898e239bd8dba0f78999fc4c055..28400a5878336e68801ad7b1aa918663b81af023 100644
--- a/src/compiler_common.mli
+++ b/src/compiler_common.mli
@@ -24,3 +24,5 @@ val type_decls: Types.t Env.t -> program_t -> Types.t Env.t
 val clock_decls: Clocks.t Env.t -> program_t -> Clocks.t Env.t
 
 val create_dest_dir: unit -> unit
+
+val track_exception: unit -> unit
diff --git a/src/compiler_stages.mli b/src/compiler_stages.mli
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..a1a2eb553b6602c246abd8cee3cdeb54c08b5aef 100644
--- a/src/compiler_stages.mli
+++ b/src/compiler_stages.mli
@@ -0,0 +1,8 @@
+open Lustre_types
+open Machine_code_types
+
+exception StopPhase1 of program_t
+
+val stage1: Normalization.param_t -> program_t -> string -> string -> string -> program_t * dep_t list
+val stage2: Normalization.param_t -> program_t -> program_t * machine_t list
+val stage3: program_t -> machine_t list -> dep_t list -> string -> string -> unit
diff --git a/src/dune b/src/dune
index accc80f7440631d9c9ebac5c769e805debe7d1f5..4a73229bda2b54f9eca79d3a18eb17f63a98f9b6 100644
--- a/src/dune
+++ b/src/dune
@@ -12,7 +12,6 @@
  (modules
   lustre_types
   utils
-  lustre_utils
   location
   dimension
   env
@@ -136,7 +135,7 @@
 (executable
  (name main_lustre_testgen)
  (public_name lustret)
- (modules main_lustre_testgen mutation mmap pathConditions)
+ (modules main_lustre_testgen mutation pathConditions)
  (libraries lustrec_lib))
 
 (library
diff --git a/src/error.mli b/src/error.mli
index 5adf214a81165b34681b4590f9902f6e13b4cc9b..0d5695aed37c769281fc18705b4f90df8a666e3f 100644
--- a/src/error.mli
+++ b/src/error.mli
@@ -13,6 +13,8 @@ type t =
 
 exception Error of Location.t * t
 
+val return_code: t -> int
+
 val pp: Format.formatter -> t -> unit
 val pp_error: Location.t -> (Format.formatter -> unit) -> unit
 val pp_warning: Location.t -> (Format.formatter -> unit) -> unit
diff --git a/src/expand.mli b/src/expand.mli
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/src/global.mli b/src/global.mli
index e5e0e45e411ad0941509404f5ce8af1235df3b18..49d2f8deb4fb5b7293becb896572639621d663ce 100644
--- a/src/global.mli
+++ b/src/global.mli
@@ -1,3 +1,5 @@
 val type_env: Types.t Env.t ref
 val clock_env: Clocks.t Env.t ref
 val main_node: string ref
+
+val initialize: unit -> unit
diff --git a/src/init_predef.mli b/src/init_predef.mli
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/src/lustre_utils.mli b/src/lustre_utils.mli
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/src/main_lustre_compiler.ml b/src/main_lustre_compiler.ml
index 46192fa69d7989e9997334c2483cb56b7aa056bd..52138e89fe64d77d4b4211c7ad411cc6271cf7d1 100644
--- a/src/main_lustre_compiler.ml
+++ b/src/main_lustre_compiler.ml
@@ -79,7 +79,7 @@ let compile dirname basename extension =
     let all_scopes = Scopes.compute_scopes prog !Options.main_node in
     (* Printing scopes *)
     if !Options.verbose_level >= 1 then Format.printf "Possible scopes are:@   ";
-    Format.printf "@[<v>%a@ @]@ @?" Scopes.print_scopes all_scopes;
+    Format.printf "@[<v>%a@ @]@ @?" Scopes.pp_scopes all_scopes;
     exit 0);
   let machine_code = Plugins.refine_machine_code prog machine_code in
   Log.report ~level:1 (fun fmt -> fprintf fmt "@]@ @ ");
@@ -125,7 +125,7 @@ let _ =
   | Parse.Error | Types.Error (_, _) | Clocks.Error (_, _) ->
     exit 1
   | Error.Error (loc, kind) (*| Task_set.Error _*) ->
-    Error.pp_error loc (fun fmt -> Error.pp_error_msg fmt kind);
+    Error.pp_error loc (fun fmt -> Error.pp fmt kind);
     exit (Error.return_code kind)
   (* | Causality.Error _ -> exit (Error.return_code Error.AlgebraicLoop) *)
   | Sys_error msg ->
diff --git a/src/main_lustre_compiler.mli b/src/main_lustre_compiler.mli
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/src/main_lustre_testgen.ml b/src/main_lustre_testgen.ml
index 27f2de55e73bd301da0c3e40f9d1f1dae77fac3e..a1bbb0a172e71681d806f4eeae8c2a4260b53de2 100644
--- a/src/main_lustre_testgen.ml
+++ b/src/main_lustre_testgen.ml
@@ -11,9 +11,9 @@
 
 (* This module is used for the lustre test generator *)
 
-open Format
 open Log
 open Utils
+open Format
 open Compiler_common
 
 let usage = "Usage: lustret [options] \x1b[4msource file\x1b[0m"
@@ -23,13 +23,12 @@ let extensions = [ ".lus" ]
 let pp_trace trace_filename mutation_list =
   let trace_file = open_out trace_filename in
   let trace_fmt = formatter_of_out_channel trace_file in
-  Format.fprintf trace_fmt "@[<v 2>{@ %a@ }@]"
-    (fprintf_list ~sep:",@ " (fun fmt (mutation, mutation_loc, mutant_name) ->
-         Format.fprintf fmt "\"%s\": { @[<v 0>%a,@ %a@ }@]" mutant_name
-           Mutation.print_directive_json mutation Mutation.print_loc_json
-           mutation_loc))
-    mutation_list;
-  Format.fprintf trace_fmt "@.@?"
+  Format.(fprintf trace_fmt "@[<v 2>{@ %a@ }@]@.@?"
+            (pp_comma_list (fun fmt (mutation, mutation_loc, mutant_name) ->
+                 fprintf fmt "\"%s\": { @[<v 0>%a,@ %a@ }@]" mutant_name
+                   Mutation.pp_directive_json mutation Mutation.pp_loc_json
+                   mutation_loc))
+            mutation_list)
 
 let testgen_source dirname basename extension =
   let source_name = dirname ^ "/" ^ basename ^ extension in
@@ -69,7 +68,7 @@ let testgen_source dirname basename extension =
     Format.fprintf fmt "@.@?";
 
     (* Prog is (1) cleaned from initial equations TODO (2) produced as EMF *)
-    Options.output := "emf";
+    Options.output := Options.OutEMF;
     let params = Backends.get_normalization_params () in
     let prog_mcdc = Normalization.normalize_prog params prog_mcdc in
     let prog_mcdc, machine_code = Compiler_stages.stage2 params prog_mcdc in
@@ -117,7 +116,7 @@ let testgen_source dirname basename extension =
         let mutant_fmt = formatter_of_out_channel mutant_out in
         report ~level:1 (fun fmt ->
             fprintf fmt ".. generating mutant %s: %a@,@?" mutant_filename
-              Mutation.print_directive mutation);
+              Mutation.pp_directive mutation);
         Format.fprintf mutant_fmt "%a@." Printers.pp_prog mutant;
         mutation, mutation_loc, mutant_basename)
       mutants
diff --git a/src/main_lustre_testgen.mli b/src/main_lustre_testgen.mli
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/src/main_lustre_verifier.ml b/src/main_lustre_verifier.ml
index c56081e0e00dbc51911cfee9fb44c1fb5c1d2473..2d2c30ceeeeb0d2073827169a9e9f801768ec25a 100644
--- a/src/main_lustre_verifier.ml
+++ b/src/main_lustre_verifier.ml
@@ -84,7 +84,7 @@ let verify dirname basename extension =
     let all_scopes = Scopes.compute_scopes prog !Options.main_node in
     (* Printing scopes *)
     if !Options.verbose_level >= 1 then Format.printf "Possible scopes are:@   ";
-    Format.printf "@[<v>%a@ @]@ @?" Scopes.print_scopes all_scopes;
+    Format.printf "@[<v>%a@ @]@ @?" Scopes.pp_scopes all_scopes;
     exit 0);
 
   let machine_code = Plugins.refine_machine_code prog machine_code in
@@ -126,7 +126,7 @@ let _ =
   | Parse.Error | Types.Error (_, _) | Clocks.Error (_, _) ->
     exit 1
   | Error.Error (loc, kind) (*| Task_set.Error _*) ->
-    Error.pp_error loc (fun fmt -> Error.pp_error_msg fmt kind);
+    Error.pp_error loc (fun fmt -> Error.pp fmt kind);
     exit (Error.return_code kind)
   (* | Causality.Error _ -> exit (Error.return_code Error.AlgebraicLoop) *)
   | Sys_error msg ->
diff --git a/src/main_lustre_verifier.mli b/src/main_lustre_verifier.mli
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/src/mmap.mli b/src/mmap.mli
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/src/mutation.ml b/src/mutation.ml
index 1cfd464bfcdab82ec93a41b581ae4a1580b0d2a2..b20ab15bf5d4d674141f68f8e6f7ec17e03a0ac5 100644
--- a/src/mutation.ml
+++ b/src/mutation.ml
@@ -5,6 +5,7 @@
    terminating process. The current setting is harder but may miss enumerating
    some cases. To be checked! *)
 
+open Utils
 open Lustre_types
 open Corelang
 open Log
@@ -56,7 +57,7 @@ module IntSet = Set.Make (struct
   let compare = compare
 end)
 
-module OpCount = Mmap.Make (struct
+module OpCount = Map.Make (struct
   type t = string
 
   let compare = compare
@@ -198,7 +199,7 @@ let check_mut e1 e2 =
   in
   if not (eq e1 e2) then Some (e1, e2) else None
 
-let mk_cst_expr c = mkexpr Location.dummy_loc (Expr_const c)
+let mk_cst_expr c = mkexpr Location.dummy (Expr_const c)
 
 let rdm_mutate_int i =
   if Random.int 100 > threshold_inc_int then i + 1
@@ -423,7 +424,7 @@ let set_mutation_loc () =
     assert false
 (* Those global vars should be defined during the visitor pattern execution *)
 
-let print_directive fmt d =
+let pp_directive fmt d =
   match d with
   | Pre n ->
     Format.fprintf fmt "pre %i" n
@@ -438,7 +439,7 @@ let print_directive fmt d =
   | SwitchIntCst (n, m) ->
     Format.fprintf fmt "switch int cst %i -> %i" n m
 
-let print_directive_json fmt d =
+let pp_directive_json fmt d =
   match d with
   | Pre _ ->
     Format.fprintf fmt "\"mutation\": \"pre\""
@@ -454,11 +455,11 @@ let print_directive_json fmt d =
   | SwitchIntCst (_, m) ->
     Format.fprintf fmt "\"mutation\": \"cst_switch\", \"to_cst\": \"%i\"" m
 
-let print_loc_json fmt (n, eqlhs, l) =
-  Format.fprintf fmt
-    "\"node_id\": \"%s\", \"eq_lhs\": [%a], \"loc_line\": \"%i\"" n
-    (Utils.fprintf_list ~sep:", " (fun fmt s -> Format.fprintf fmt "\"%s\"" s))
-    eqlhs (Location.loc_line l)
+let pp_loc_json fmt (n, eqlhs, l) =
+  Format.(fprintf fmt
+            "\"node_id\": \"%s\", \"eq_lhs\": [%a], \"loc_line\": \"%i\"" n
+            (pp_comma_list (fun fmt -> fprintf fmt "\"%s\""))
+            eqlhs (Location.line_of l))
 
 let fold_mutate_int i =
   if Random.int 100 > threshold_inc_int then i + 1
@@ -643,11 +644,11 @@ let create_mutant prog directive =
       mi
     | _ ->
       Format.eprintf "Failed when creating mutant for directive %a@.@?"
-        print_directive directive;
+        pp_directive directive;
       let _ =
         match !target with
         | Some dir' ->
-          Format.eprintf "New directive %a@.@?" print_directive dir'
+          Format.eprintf "New directive %a@.@?" pp_directive dir'
         | _ ->
           ()
       in
diff --git a/src/mutation.mli b/src/mutation.mli
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..fb7ae649d4992295e5c9c4d370243ba3ef7891f8 100644
--- a/src/mutation.mli
+++ b/src/mutation.mli
@@ -0,0 +1,19 @@
+open Utils
+open Format
+open Lustre_types
+
+type mutant_t =
+  | Boolexpr of int
+  | Pre of int
+  | Op of string * int * string
+  | IncrIntCst of int
+  | DecrIntCst of int
+  | SwitchIntCst of int * int
+
+val pp_directive_json: formatter -> mutant_t -> unit
+
+val pp_directive: formatter -> mutant_t -> unit
+
+val pp_loc_json: formatter -> ident * ident list * Location.t -> unit
+
+val mutate: int -> program_t -> (mutant_t * (ident * ident list * Location.t) * program_t) list
diff --git a/src/options_management.ml b/src/options_management.ml
index fd9f1e5e50730c50857046a3152dd8696dbb2d89..2ad047a9d2c66c817bb41c836a27e196c2ca34a3 100644
--- a/src/options_management.ml
+++ b/src/options_management.ml
@@ -10,6 +10,8 @@
 (********************************************************************)
 open Options
 
+type options_spec = (string * Arg.spec * string) list
+
 let print_version () =
   let open Utils.Format in
   printf
diff --git a/src/options_management.mli b/src/options_management.mli
index 625d7fc82e219a5394bcbfe48efcae947caeb5de..23101d0a7679980bf86a61c5ae2994f0450d7dcd 100644
--- a/src/options_management.mli
+++ b/src/options_management.mli
@@ -1,8 +1,18 @@
+type options_spec = (string * Arg.spec * string) list
+
 val core_dependency: string -> string
 val plugin_opt: string * (unit -> unit) * (Format.formatter -> unit) *
-                (string * Arg.spec * string) list -> (string * Arg.spec * string) list
+                options_spec -> options_spec
 
 val name_dependency: ('a * string) -> string -> string
 val get_witness_dir: string -> string
 
-val verifier_opt: string * (unit -> unit) * (string * Arg.spec * string) list -> (string * Arg.spec * string) list
+val verifier_opt: string * (unit -> unit) * options_spec -> options_spec
+
+val lustrec_options: options_spec
+
+val lustrev_options: options_spec
+
+val lustret_options: options_spec
+
+val setup: unit -> unit
diff --git a/src/parsers/lexer_lustre.mll b/src/parsers/lexer_lustre.mll
index 31c8c507a4802f3d196c2e0244ca559135c4d310..e27c5b538049b9715aae197c351d5c61cc28d5de 100644
--- a/src/parsers/lexer_lustre.mll
+++ b/src/parsers/lexer_lustre.mll
@@ -120,13 +120,13 @@ let newline token lexbuf =
 
 let make_annot orig_loc s =
   let lexbuf = Lexing.from_string s in
-  let f = Location.filename_of_loc orig_loc in
+  let f = Location.filename_of orig_loc in
   ANNOT (Parse.parse (module LexerLustreSpec) ~orig_loc f s lexbuf
         Parser_lustre.lustre_annot Parse.Inc.lustre_annot)
 
 let make_spec orig_loc s =
   let lexbuf = Lexing.from_string s in
-  let f = Location.filename_of_loc orig_loc in
+  let f = Location.filename_of orig_loc in
   NODESPEC (Parse.parse (module LexerLustreSpec) ~orig_loc f s lexbuf
         Parser_lustre.lustre_spec Parse.Inc.lustre_spec)
 }
diff --git a/src/parsers/parse.mli b/src/parsers/parse.mli
index 6d55261776a64fab384e9f94c5176af5b66df090..11479a52f9557d6f5cd95513421d7626cd64442a 100644
--- a/src/parsers/parse.mli
+++ b/src/parsers/parse.mli
@@ -1,3 +1,5 @@
+exception Error
+
 type start_symbol = Header | Program
 
 module type LEXER = sig
diff --git a/src/pathConditions.ml b/src/pathConditions.ml
index 6abf681f4ffdc872c95626ddb1f32c47ce73690b..1a53320389be0d095ac44183abfea44842a938c8 100644
--- a/src/pathConditions.ml
+++ b/src/pathConditions.ml
@@ -328,7 +328,7 @@ let mcdc_top_decl td =
                 [ "PROPERTY" ], neg_ee;
                 (* Using negated property to force model-checker to produce a
                    suitable covering trace *)
-                (let loc = Location.dummy_loc in
+                (let loc = Location.dummy in
                  let valid_e =
                    let open Corelang in
                    mkexpr loc (Expr_const (const_of_bool atom_valid))
diff --git a/src/pathConditions.mli b/src/pathConditions.mli
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..75e3ac520baa8b7ef7dc45a8c2c6c7a711d389e6 100644
--- a/src/pathConditions.mli
+++ b/src/pathConditions.mli
@@ -0,0 +1 @@
+val mcdc: Lustre_types.program_t -> Lustre_types.program_t
diff --git a/src/plugins/mpfr/lustrec_mpfr.mli b/src/plugins/mpfr/lustrec_mpfr.mli
index c055cae8c62503094625ddc0733d7e0e8e4f1272..1b1ba89360fc9756f8952465107a8c020d8454c9 100644
--- a/src/plugins/mpfr/lustrec_mpfr.mli
+++ b/src/plugins/mpfr/lustrec_mpfr.mli
@@ -6,6 +6,8 @@ open Machine_code_types
 val unfoldable_value: Machine_code_types.value_t -> bool
 val inject_prog: program_t -> program_t
 
+val mpfr_module: top_decl
+
 val mpfr_t: string
 
 val mpfr_rnd: unit -> string
diff --git a/src/plugins/pluginType.ml b/src/plugins/pluginType.ml
index a4bd750cd6d0f88846d69b54c63f80a69a3931fd..e58bc92f8ff7c233195a9bdd7146831a5ca7d24d 100644
--- a/src/plugins/pluginType.ml
+++ b/src/plugins/pluginType.ml
@@ -5,7 +5,7 @@ module type S = sig
 
   val usage : Format.formatter -> unit
 
-  val options : (string * Arg.spec * string) list
+  val options : Options_management.options_spec
 
   val init : unit -> unit
 
diff --git a/src/plugins/pluginType.mli b/src/plugins/pluginType.mli
index 53c395c5300c5bf16777c4979a6c18cbc2c2666f..402f1b2d6a9654fd9173dad7cd714d565564b990 100644
--- a/src/plugins/pluginType.mli
+++ b/src/plugins/pluginType.mli
@@ -5,7 +5,7 @@ module type S = sig
 
   val usage : Format.formatter -> unit
 
-  val options : (string * Arg.spec * string) list
+  val options : Options_management.options_spec
 
   val init : unit -> unit
 
diff --git a/src/plugins/plugins.mli b/src/plugins/plugins.mli
index 5e9c3d2a33a0ff4c79da984d7c60bbb9d04dac85..964e9ca955f3ee4aa3ee7c130fd24dea934b9c87 100644
--- a/src/plugins/plugins.mli
+++ b/src/plugins/plugins.mli
@@ -1,5 +1,6 @@
 open Utils
 open Lustre_types
+open Machine_code_types
 
 val inline_annots: (ident -> ident) -> expr_annot list -> expr_annot list
 
@@ -7,3 +8,9 @@ val check_force_stateful: unit -> bool
 
 val c_backend_main_loop_body_prefix: string -> string -> Format.formatter -> unit -> unit
 val c_backend_main_loop_body_suffix: Format.formatter -> unit -> unit
+
+val refine_machine_code: program_t -> machine_t list -> machine_t list
+
+val init: unit -> unit
+
+val options: unit -> Options_management.options_spec
diff --git a/src/plugins/scopes/scopes.ml b/src/plugins/scopes/scopes.ml
index 070aa37ce5bf0f7eaf11767e0a9f5f8e8c27bef3..6a79770591b3125af64ae87e7d5d9b167ed46a6f 100644
--- a/src/plugins/scopes/scopes.ml
+++ b/src/plugins/scopes/scopes.ml
@@ -58,7 +58,7 @@ let rec compute_scopes ?(first = true) prog root_node : scope_t list =
     local_scopes @ List.flatten sub_scopes
   with Not_found -> []
 
-let print_scopes =
+let pp_scopes =
   Format.(pp_print_list (fun fmt ((_, v) as s) ->
       fprintf fmt "%a: %a"
         (pp_print_list ~pp_sep:(fun fmt () -> pp_print_string fmt ".") pp_print_string)
@@ -177,13 +177,10 @@ let extract_scopes_defs scopes =
     | _ ->
       assert false
   in
-  let scopes_vars =
-    List.map
-      (fun (sl, scope) ->
-        String.concat "." sl, scope_path_name scope "main_mem.")
-      scopes
-  in
-  scopes_vars
+  List.map
+    (fun (sl, scope) ->
+       String.concat "." sl, scope_path_name scope "main_mem.")
+    scopes
 
 let pp_scopes_files _basename _mname fmt scopes =
   let scopes_vars = extract_scopes_defs scopes in
@@ -202,7 +199,7 @@ let pp_scopes_files _basename _mname fmt scopes =
     scopes_vars;
   Format.fprintf fmt "@]}@ "
 
-let pp_scopes fmt scopes =
+let pp_full_scopes fmt scopes =
   let scopes_vars = extract_scopes_defs scopes in
   List.iteri
     (fun idx (id, (var_path, var)) ->
@@ -433,13 +430,13 @@ end = struct
       let all_scopes = compute_scopes prog !Options.main_node in
       (* Printing scopes *)
       if !Options.verbose_level >= 1 then Format.printf "Possible scopes are:@ ";
-      Format.printf "@[<v 0>%a@ @]@.@?" print_scopes all_scopes;
+      Format.printf "@[<v 0>%a@ @]@.@?" pp_scopes all_scopes;
       exit 0);
     if is_active () then process_scopes !Options.main_node prog machine_code
     else machine_code
 
   let c_backend_main_loop_body_suffix fmt () =
-    if is_active () then Format.fprintf fmt "@ %a" pp_scopes !scopes_map
+    if is_active () then Format.fprintf fmt "@ %a" pp_full_scopes !scopes_map
 
   let c_backend_main_loop_body_prefix basename mname fmt () =
     if is_active () then
diff --git a/src/plugins/scopes/scopes.mli b/src/plugins/scopes/scopes.mli
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..9c9a33329f1e982040052489cdf123959189364a 100644
--- a/src/plugins/scopes/scopes.mli
+++ b/src/plugins/scopes/scopes.mli
@@ -0,0 +1,15 @@
+open Utils
+open Lustre_types
+
+module Plugin : sig
+  include PluginType.S
+
+  val show_scopes : unit -> bool
+end
+
+(* (variable, node name, node instance) *)
+type scope_t = (var_decl * string * string option) list * var_decl
+
+val compute_scopes: ?first:bool -> program_t -> ident -> scope_t list
+
+val pp_scopes: Format.formatter -> scope_t list -> unit
diff --git a/src/printers.mli b/src/printers.mli
index 5328d2c9f6dddf022d531a7a9b95e31261e76700..d852a03beec58284b6f99fb6169b46712f2a2564 100644
--- a/src/printers.mli
+++ b/src/printers.mli
@@ -20,3 +20,5 @@ val pp_typedef: formatter -> typedef_desc -> unit
 val pp_prog: formatter -> program_t -> unit
 val pp_prog_short: formatter -> program_t -> unit
 val pp_quantifiers: formatter -> quantifier_type * var_decl list -> unit
+val pp_node_list: formatter -> top_decl list -> unit
+val pp_lusi_header: formatter -> string -> program_t -> unit
diff --git a/src/tools/importer/main_lustre_importer.mli b/src/tools/importer/main_lustre_importer.mli
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/src/tools/stateflow/common/basetypes.ml b/src/tools/stateflow/common/basetypes.ml
index 3eb1af45eec5a3bbc9eb16d5aa1172242716b8c4..c7c85005535314ee1153f752b7232ee0778a384a 100644
--- a/src/tools/stateflow/common/basetypes.ml
+++ b/src/tools/stateflow/common/basetypes.ml
@@ -96,13 +96,15 @@ module type ActionType = sig
   val pp_act : Format.formatter -> t -> unit
 end
 
+type action_t =
+  | Quote : base_action_t -> action_t
+  | Close : path_t -> action_t
+  | Open : path_t -> action_t
+  | Call : 'c call_t * 'c -> action_t
+  | Nil : action_t
+
 module Action = struct
-  type t =
-    | Quote : base_action_t -> t
-    | Close : path_t -> t
-    | Open : path_t -> t
-    | Call : 'c call_t * 'c -> t
-    | Nil : t
+  type t = action_t
 
   let nil = Nil
 
@@ -163,14 +165,16 @@ module type ConditionType = sig
   val pp_cond : Format.formatter -> t -> unit
 end
 
+type condition_t =
+  | Quote of base_condition_t
+  | Active of path_t
+  | Event of event_base_t
+  | And of condition_t * condition_t
+  | Neg of condition_t
+  | True
+
 module Condition = struct
-  type t =
-    | Quote of base_condition_t
-    | Active of path_t
-    | Event of event_base_t
-    | And of t * t
-    | Neg of t
-    | True
+  type t = condition_t
 
   let cquote cond = Quote cond
 
diff --git a/src/tools/stateflow/common/basetypes.mli b/src/tools/stateflow/common/basetypes.mli
index 286a40b2d46b1013a079c53b7b5cf0cfa6f8b7b4..eecf18a875daf85ff70a18c3e5478ae0c481762b 100644
--- a/src/tools/stateflow/common/basetypes.mli
+++ b/src/tools/stateflow/common/basetypes.mli
@@ -1,3 +1,5 @@
+val sf_level: int
+
 type state_name_t = string
 
 type junction_name_t = string
@@ -25,10 +27,6 @@ type base_condition_t = {
   cvariables : Lustre_types.var_decl list;
 }
 
-val pp_state_name: Format.formatter -> state_name_t -> unit
-val pp_junction_name: Format.formatter -> junction_name_t -> unit
-val pp_path: Format.formatter -> path_t -> unit
-
 type frontier_t = Loose | Strict
 
 type _ call_t =
@@ -36,6 +34,12 @@ type _ call_t =
   | Dcall : path_t call_t
   | Xcall : (path_t * frontier_t) call_t
 
+val pp_state_name: Format.formatter -> state_name_t -> unit
+val pp_junction_name: Format.formatter -> junction_name_t -> unit
+val pp_path: Format.formatter -> path_t -> unit
+val pp_frontier: Format.formatter -> frontier_t -> unit
+val pp_call: Format.formatter -> 'a call_t -> unit
+
 (* Conditions are either (1) simple strings, (2) the active status of a state or
    (3) occurence of an event. They can be combined (conjunction, negation) *)
 module type ConditionType = sig
@@ -56,7 +60,15 @@ module type ConditionType = sig
   val pp_cond : Format.formatter -> t -> unit
 end
 
-module Condition: ConditionType
+type condition_t =
+  | Quote of base_condition_t
+  | Active of path_t
+  | Event of event_base_t
+  | And of condition_t * condition_t
+  | Neg of condition_t
+  | True
+
+module Condition: ConditionType with type t = condition_t
 
 module type ActionType = sig
   type t
@@ -74,4 +86,15 @@ module type ActionType = sig
   val pp_act : Format.formatter -> t -> unit
 end
 
-module Action: ActionType
+type action_t =
+  | Quote : base_action_t -> action_t
+  | Close : path_t -> action_t
+  | Open : path_t -> action_t
+  | Call : 'c call_t * 'c -> action_t
+  | Nil : action_t
+
+module Action: ActionType with type t = action_t
+
+module GlobalVarDef: sig
+  type t = { variable : Lustre_types.var_decl; init_val : Lustre_types.expr }
+end
diff --git a/src/tools/stateflow/common/datatype.mli b/src/tools/stateflow/common/datatype.mli
index 1aa9830e9e13067f6e88572fe96a1b16b85ce67a..e1183053964fda6d62ba06cc8182c3a062d6e26e 100644
--- a/src/tools/stateflow/common/datatype.mli
+++ b/src/tools/stateflow/common/datatype.mli
@@ -51,3 +51,20 @@ module type MODEL_T = sig
 
   val traces : trace_t list
 end
+
+(* Module (S)tate(F)low provides basic constructors for action, condition,
+   events, as well as printer functions *)
+module SF: sig
+  val no_action: action_t
+  val no_condition: condition_t
+  val no_event: event_t
+  val condition: base_condition_t -> condition_t
+  val event: event_base_t -> event_t
+  val state_action: action_t -> action_t -> action_t -> state_actions_t
+  val states: prog_t -> ActiveStates.Vars.t
+  val global_vars: prog_t -> (Lustre_types.var_decl * Lustre_types.expr) list
+  val pp_dest: Format.formatter -> destination_t -> unit
+  val pp_trans: Format.formatter -> trans_t -> unit
+  val pp_transitions: Format.formatter -> trans_t list -> unit
+  val pp_comp: Format.formatter -> composition_t -> unit
+end
diff --git a/src/tools/stateflow/models/model_simple.ml b/src/tools/stateflow/models/model_simple.ml
index 729f8f6262e324be6e837c4e4a7cf8c594f93360..c7ae2c019b14b9521da00a8b711b684305f47a7f 100644
--- a/src/tools/stateflow/models/model_simple.ml
+++ b/src/tools/stateflow/models/model_simple.ml
@@ -8,7 +8,7 @@ let condition _ =
   condition
     {
       expr =
-        Corelang.mkexpr Location.dummy_loc
+        Corelang.mkexpr Location.dummy
           (Lustre_types.Expr_const (Corelang.const_of_bool true));
       cinputs = [];
       coutputs = [];
diff --git a/src/tools/stateflow/models/model_stopwatch.ml b/src/tools/stateflow/models/model_stopwatch.ml
index 098cf377c232f88a205c5fdb3969805fa481c5a6..437953afbae5de71875b37f1adaa7391a9955b50 100644
--- a/src/tools/stateflow/models/model_stopwatch.ml
+++ b/src/tools/stateflow/models/model_stopwatch.ml
@@ -16,7 +16,7 @@ let condition _ =
   condition
     {
       expr =
-        Corelang.mkexpr Location.dummy_loc
+        Corelang.mkexpr Location.dummy
           (Lustre_types.Expr_const (Corelang.const_of_bool true));
       cinputs = [];
       coutputs = [];
@@ -289,10 +289,10 @@ let model =
     ]
   in
   let globals =
-    let int_typ = Corelang.mktyp Location.dummy_loc Lustre_types.Tydec_int in
+    let int_typ = Corelang.mktyp Location.dummy Lustre_types.Tydec_int in
     List.map
       (fun k ->
-        ( Corelang.mkvar_decl Location.dummy_loc
+        ( Corelang.mkvar_decl Location.dummy
             ( k,
               (* name *)
               int_typ,
@@ -305,7 +305,7 @@ let model =
               (* no default value *)
               None (* no parent known *) ),
           (* Default value is zero *)
-          Corelang.mkexpr Location.dummy_loc
+          Corelang.mkexpr Location.dummy
             (Lustre_types.Expr_const (Lustre_types.Const_int 0)) ))
       [ "cent"; "sec"; "min"; "cont" ]
   in
diff --git a/src/tools/stateflow/semantics/cPS.mli b/src/tools/stateflow/semantics/cPS.mli
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..dd4e7e5fe9e3b1fc53d033321ef106dc38c5bc7d 100644
--- a/src/tools/stateflow/semantics/cPS.mli
+++ b/src/tools/stateflow/semantics/cPS.mli
@@ -0,0 +1,3 @@
+module Semantics (T : CPS_transformer.TransformerType) (M : Datatype.MODEL_T) : sig
+  val code_gen: bool * bool * bool -> Lustre_types.program_t
+end
diff --git a/src/tools/stateflow/semantics/cPS_ccode_generator.mli b/src/tools/stateflow/semantics/cPS_ccode_generator.mli
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..f72f057bed40acdce8965ef44fd672b1d607ed4b 100644
--- a/src/tools/stateflow/semantics/cPS_ccode_generator.mli
+++ b/src/tools/stateflow/semantics/cPS_ccode_generator.mli
@@ -0,0 +1 @@
+module CodeGenerator : CPS_transformer.ComparableTransformerType
diff --git a/src/tools/stateflow/semantics/cPS_interpreter.mli b/src/tools/stateflow/semantics/cPS_interpreter.mli
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..c642299ccb53e8953e46753551a4283cba2ffb82 100644
--- a/src/tools/stateflow/semantics/cPS_interpreter.mli
+++ b/src/tools/stateflow/semantics/cPS_interpreter.mli
@@ -0,0 +1,28 @@
+open Basetypes
+open Datatype
+open CPS_transformer
+open Theta
+
+module Interpreter (Transformer : TransformerType): sig
+
+  (* module KT = KenvTheta (Transformer) *)
+
+  module type ProgType = sig
+    val init : state_name_t
+
+    val defs : prog_t src_components_t list
+  end
+
+  module type EvaluationType = sig
+    module Theta : ThetaType with type t = Transformer.t
+
+    val eval_prog : Transformer.t
+
+    val eval_components : 'c call_t -> ('c * Transformer.t) list
+  end
+
+  module Evaluation
+      (Thetaify : KenvTheta(Transformer).ThetaifyType)
+      (Prog : ProgType) :
+    EvaluationType
+end
diff --git a/src/tools/stateflow/semantics/cPS_lustre_generator.ml b/src/tools/stateflow/semantics/cPS_lustre_generator.ml
index 20c12ed7e868b303b7ba5d273123adb697e121eb..b7a0bfdbeca4b2d65bf155ac08f0e795d6c3beaf 100644
--- a/src/tools/stateflow/semantics/cPS_lustre_generator.ml
+++ b/src/tools/stateflow/semantics/cPS_lustre_generator.ml
@@ -1,3 +1,4 @@
+open Utils
 open Basetypes
 open CPS_transformer
 
@@ -34,8 +35,8 @@ end) : TransformerType = struct
       fun () -> cpt := 0 )
 
   let pp_path prefix fmt path =
-    Format.fprintf fmt "%s%t" prefix (fun fmt ->
-        Utils.fprintf_list ~sep:"_" Format.pp_print_string fmt path)
+    Format.(fprintf fmt "%s%t" prefix (fun fmt ->
+        pp_print_list ~pp_sep:(fun fmt () -> pp_print_string fmt "_") pp_print_string fmt path))
 
   (* let pp_typed_path sin fmt path =
    *   Format.fprintf fmt "%a : bool" (pp_path sin) path *)
@@ -53,7 +54,7 @@ end) : TransformerType = struct
     List.map (fun p -> var_to_ident prefix p) (ActiveStates.Vars.elements vars)
 
   let mkvar name typ =
-    let loc = Location.dummy_loc in
+    let loc = Location.dummy in
     Corelang.mkvar_decl loc
       ( name,
         typ,
@@ -65,7 +66,7 @@ end) : TransformerType = struct
   let var_to_vdecl ?(prefix = "") var typ = mkvar (var_to_ident prefix var) typ
 
   let state_vars_to_vdecl_list ?(prefix = "") vars =
-    let bool_type = Corelang.mktyp Location.dummy_loc Lustre_types.Tydec_bool in
+    let bool_type = Corelang.mktyp Location.dummy Lustre_types.Tydec_bool in
     List.map
       (fun v -> var_to_vdecl ~prefix v bool_type)
       (ActiveStates.Vars.elements vars)
@@ -77,11 +78,11 @@ end) : TransformerType = struct
       locs []
   (* TODO: declare global vars *)
 
-  let mkeq = Corelang.mkeq Location.dummy_loc
+  let mkeq = Corelang.mkeq Location.dummy
 
-  let mkexpr = Corelang.mkexpr Location.dummy_loc
+  let mkexpr = Corelang.mkexpr Location.dummy
 
-  let mkpredef_call = Corelang.mkpredef_call Location.dummy_loc
+  let mkpredef_call = Corelang.mkpredef_call Location.dummy
 
   let expr_of_bool b =
     mkexpr (Lustre_types.Expr_const (Corelang.const_of_bool b))
@@ -104,14 +105,14 @@ end) : TransformerType = struct
       [
         {
           Lustre_types.assert_expr = expr_of_bool false;
-          assert_loc = Location.dummy_loc;
+          assert_loc = Location.dummy;
         };
       ]
     else []
 
   let var_to_expr ?(prefix = "") p =
     let id = var_to_ident prefix p in
-    Corelang.expr_of_ident id Location.dummy_loc
+    Corelang.expr_of_ident id Location.dummy
 
   let vars_to_exprl ?(prefix = "") vars =
     List.map (fun p -> var_to_expr ~prefix p) (ActiveStates.Vars.elements vars)
@@ -128,7 +129,7 @@ end) : TransformerType = struct
   let event_type =
     {
       Lustre_types.ty_dec_desc = Lustre_types.Tydec_const "event_type";
-      Lustre_types.ty_dec_loc = Location.dummy_loc;
+      Lustre_types.ty_dec_loc = Location.dummy;
     }
 
   let event_var = mkvar "event" event_type
@@ -192,15 +193,15 @@ end) : TransformerType = struct
 
   let mkact' action sin sout =
     match action with
-    | Action.Call (c, a) ->
+    | Call (c, a) ->
       mkcall' sin sout c a
-    | Action.Quote a ->
+    | Quote a ->
       (* TODO: check. This seems to be innappropriate *)
       (* let funname = "action_" ^ a.ident in let args = vars_to_exprl
          ~prefix:sin Vars.state_vars in let rhs = mkpredef_call funname args in
          mkstmt_eq ~prefix_lhs:sout Vars.state_vars rhs *)
       { statements = a.defs; assert_false = false }
-    | Action.Open p ->
+    | Open p ->
       let vars' = ActiveStates.Vars.remove p Vars.state_vars in
       (* eq1: sout_p = true *)
       let eq1 = mkeq ([ var_to_ident sout p ], expr_of_bool true) in
@@ -212,7 +213,7 @@ end) : TransformerType = struct
         statements = [ Lustre_types.Eq eq1; Lustre_types.Eq eq2 ];
         assert_false = false;
       }
-    | Action.Close p ->
+    | Close p ->
       let vars' = ActiveStates.Vars.remove p Vars.state_vars in
       (* eq1: sout_p = false *)
       let eq1 = mkeq ([ var_to_ident sout p ], expr_of_bool false) in
@@ -224,7 +225,7 @@ end) : TransformerType = struct
         statements = [ Lustre_types.Eq eq1; Lustre_types.Eq eq2 ];
         assert_false = false;
       }
-    | Action.Nil ->
+    | Nil ->
       let expr_list = vars_to_exprl ~prefix:sin Vars.state_vars in
       let rhs = mkexpr (Lustre_types.Expr_tuple expr_list) in
       mkstmt_eq ~prefix_lhs:sout Vars.state_vars rhs
@@ -237,11 +238,11 @@ end) : TransformerType = struct
   let rec mkcond' sin condition =
     (*Format.printf "----- cond = %a@." Condition.pp_cond condition;*)
     match condition with
-    | Condition.True ->
+    | True ->
       expr_of_bool true
-    | Condition.Active p ->
+    | Active p ->
       var_to_expr ~prefix:sin p
-    | Condition.Event e ->
+    | Event e ->
       mkpredef_call "="
         [
           Corelang.expr_of_vdecl event_var;
@@ -249,17 +250,17 @@ end) : TransformerType = struct
             (Lustre_types.Expr_const
                (Lustre_types.Const_int (get_event_const e)));
         ]
-    | Condition.Neg cond ->
+    | Neg cond ->
       mkpredef_call "not" [ mkcond' sin cond ]
-    | Condition.And (cond1, cond2) ->
+    | And (cond1, cond2) ->
       mkpredef_call "&&" [ mkcond' sin cond1; mkcond' sin cond2 ]
-    | Condition.Quote c ->
+    | Quote c ->
       c.expr
   (* TODO: shall we prefix with sin ? *)
 
   let eval_cond condition (ok : t) ko sin sout =
     let open Lustre_types in
-    let loc = Location.dummy_loc in
+    let loc = Location.dummy in
     (*Format.printf "----- cond = %a@." Condition.pp_cond condition;*)
     let vars1, tr1 = ok sin sout in
     let vars2, tr2 = ko sin sout in
@@ -275,7 +276,7 @@ end) : TransformerType = struct
                  [
                    loc, mkcond' sin condition, true (* restart *), "Cond_" ^ aut;
                    ( loc,
-                     mkcond' sin (Condition.Neg condition),
+                     mkcond' sin (Neg condition),
                      true (* restart *),
                      "NotCond_" ^ aut );
                  ]
@@ -385,7 +386,7 @@ end) : TransformerType = struct
      - elles peuvent/doivent etre dans input et output de ce node thetacallD *)
 
   let mk_main_loop () =
-    (* let loc = Location.dummy_loc in *)
+    (* let loc = Location.dummy in *)
     let call_stmt =
       (* (%t) -> pre (thetaCallD_from_principal (event, %a)) *)
       let init =
diff --git a/src/tools/stateflow/semantics/cPS_lustre_generator.mli b/src/tools/stateflow/semantics/cPS_lustre_generator.mli
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..68bec7ace8c8caa10cf0921953eef7c2a9466850 100644
--- a/src/tools/stateflow/semantics/cPS_lustre_generator.mli
+++ b/src/tools/stateflow/semantics/cPS_lustre_generator.mli
@@ -0,0 +1,8 @@
+open Basetypes
+open CPS_transformer
+
+module LustrePrinter (Vars : sig
+  val state_vars : ActiveStates.Vars.t
+
+  val global_vars : GlobalVarDef.t list
+end) : TransformerType
diff --git a/src/tools/stateflow/semantics/cPS_transformer.mli b/src/tools/stateflow/semantics/cPS_transformer.mli
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..ce7c8ada2588b19c5b847c4889c7bf26f01cdfda 100644
--- a/src/tools/stateflow/semantics/cPS_transformer.mli
+++ b/src/tools/stateflow/semantics/cPS_transformer.mli
@@ -0,0 +1,70 @@
+open Basetypes
+
+type mode_t = Outer | Inner | Enter
+
+type 't success_t = path_t -> 't
+
+type 't fail_t = { local : 't; global : 't }
+
+type 't wrapper_t = path_t -> 't -> 't
+
+type ('a, 'b, 't) tag_t =
+  | E : (path_t, path_t -> frontier_t -> 't, 't) tag_t
+  | D : (path_t, 't, 't) tag_t
+  | X : (path_t, frontier_t -> 't, 't) tag_t
+  | J
+      : ( junction_name_t,
+          't wrapper_t -> 't success_t -> 't fail_t -> 't,
+          't )
+        tag_t
+
+type ('a, 'b, 't) theta_t = ('a, 'b, 't) tag_t -> 'a -> 'b
+
+module type ThetaType = sig
+  type t
+
+  val theta : ('a, 'b, t) theta_t
+end
+
+val pp_mode: Format.formatter -> mode_t -> unit
+val pp_tag: Format.formatter -> ('a, 'b, 't) tag_t -> unit
+
+module type TransformerType = sig
+  type act_t = Action.t
+
+  type cond_t = Condition.t
+
+  type t
+
+  include ActionType with type t := act_t
+
+  include ConditionType with type t := cond_t
+
+  val null : t
+
+  val bot : t
+
+  val ( >> ) : t -> t -> t
+
+  val eval_act : (module ThetaType with type t = t) -> act_t -> t
+
+  val eval_cond : cond_t -> t -> t -> t
+
+  (* val mktransformer : t -> unit *)
+  val mkprincipal : t -> Lustre_types.program_t
+
+  val mkcomponent : 'c call_t -> 'c -> t -> Lustre_types.program_t
+end
+
+module type ComparableTransformerType = sig
+  include TransformerType
+
+  val ( == ) : t -> t -> bool
+end
+
+module TransformerStub: sig
+  type act_t = Action.t
+  type cond_t = Condition.t
+  include ConditionType with type t := cond_t
+  include ActionType with type t := act_t
+end
diff --git a/src/tools/stateflow/semantics/theta.mli b/src/tools/stateflow/semantics/theta.mli
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..ed4b71c0f6de7180fb4af84852fa53774f3d01b6 100644
--- a/src/tools/stateflow/semantics/theta.mli
+++ b/src/tools/stateflow/semantics/theta.mli
@@ -0,0 +1,42 @@
+open Basetypes
+open CPS_transformer
+
+module KenvTheta (T : TransformerType) : sig
+  type kenv_t = {
+    cont_node :
+      (path_t
+      * ((kenv_t -> path_t -> frontier_t -> T.t)
+        * (kenv_t -> T.t)
+        * (kenv_t -> frontier_t -> T.t)))
+      list;
+    cont_junc :
+      (junction_name_t
+      * (kenv_t -> T.t wrapper_t -> T.t success_t -> T.t fail_t -> T.t))
+      list;
+  }
+
+  module type KenvType = sig
+    val kenv : kenv_t
+  end
+
+  module type MemoThetaTablesType = sig
+    val tables : 'c call_t -> ('c, T.t) Memo.t
+  end
+
+  module type MemoThetaType = sig
+    include ThetaType with type t = T.t
+
+    val components : 'c call_t -> ('c * t) list
+  end
+
+  module type ModularType = sig
+    val modular : (path_t, 'b, bool) tag_t -> path_t -> 'b
+  end
+
+  module type ThetaifyType = functor (Kenv : KenvType) -> MemoThetaType
+
+  module MemoThetaTables () : MemoThetaTablesType
+
+  module ModularThetaify (Tables : MemoThetaTablesType) (Mod : ModularType) :
+    ThetaifyType
+end
diff --git a/src/utils/location.ml b/src/utils/location.ml
index 4461b78cdddd49ed49ed412b657562f385509708..f1c0ae358ab01df41bc83e0f44a1ab00d7c378b1 100644
--- a/src/utils/location.ml
+++ b/src/utils/location.ml
@@ -29,7 +29,7 @@ let set_input, get_input, get_module =
 
 let curr lexbuf = lexbuf.lex_start_p, lexbuf.lex_curr_p
 
-let filename_of_loc (s, _) = s.pos_fname
+let filename_of (s, _) = s.pos_fname
 
 let filename_of_lexbuf lexbuf = lexbuf.lex_start_p.pos_fname
 
@@ -49,7 +49,7 @@ let shift_pos pos1 pos2 =
          then pos1.pos_cnum + pos2.pos_cnum else pos2.pos_cnum *);
   }
 
-let loc_line (s, _e) = s.pos_lnum
+let line_of (s, _e) = s.pos_lnum
 
 let pp fmt loc =
   if loc = dummy then () else Format.fprintf fmt "%s" (Lex.range loc)
diff --git a/src/utils/location.mli b/src/utils/location.mli
index e461dd88a23244244cdf0b52e736b206307f9c9a..266d7204b6275dcc4bbe74011699724837bc35f9 100644
--- a/src/utils/location.mli
+++ b/src/utils/location.mli
@@ -8,4 +8,5 @@ val get_module: unit -> filename
 val curr: Lexing.lexbuf -> t
 val shift: t -> t -> t
 val set_input: filename -> unit
-val filename_of_loc: t -> filename
+val filename_of: t -> filename
+val line_of: t -> int
diff --git a/src/verifierType.ml b/src/verifierType.ml
index f442ed3ea232ee2cab49f2baead28aa8633e3fc7..836a9c31909650463a29c54e4b0f789f54f3195c 100644
--- a/src/verifierType.ml
+++ b/src/verifierType.ml
@@ -5,7 +5,7 @@ module type S = sig
 
   val is_active : unit -> bool
 
-  val options : (string * Arg.spec * string) list
+  val options : Options_management.options_spec
 
   val get_normalization_params : unit -> Normalization.param_t
 
diff --git a/src/verifierType.mli b/src/verifierType.mli
index 5bfdeab920f2ff3a1f372f3235060652e50060c9..e8907cd2df9ee1adc1ac2e34de04acee1dc3b445 100644
--- a/src/verifierType.mli
+++ b/src/verifierType.mli
@@ -5,7 +5,7 @@ module type S = sig
 
   val is_active : unit -> bool
 
-  val options : (string * Arg.spec * string) list
+  val options : Options_management.options_spec
 
   val get_normalization_params : unit -> Normalization.param_t
 
diff --git a/src/verifiers.mli b/src/verifiers.mli
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..915ae8c141eacee563866ffebb70a4dd506071a5 100644
--- a/src/verifiers.mli
+++ b/src/verifiers.mli
@@ -0,0 +1,2 @@
+val get_active: unit -> (module VerifierType.S)
+val options: unit -> Options_management.options_spec
diff --git a/src/version.mli b/src/version.mli
index e8e24e73cf53990a155e583794249ef1e2eafc31..d721a4b327a14ba003d3cc10adfcd2f7d215a8fe 100644
--- a/src/version.mli
+++ b/src/version.mli
@@ -1,3 +1,4 @@
 val number: string
 val codename: string
 val include_path: string
+val testgen_path: string
diff --git a/src/checks/init_calculus.ml b/unused/checks/init_calculus.ml
similarity index 100%
rename from src/checks/init_calculus.ml
rename to unused/checks/init_calculus.ml
diff --git a/src/expand.ml b/unused/expand.ml
similarity index 100%
rename from src/expand.ml
rename to unused/expand.ml
diff --git a/src/init_predef.ml b/unused/init_predef.ml
similarity index 100%
rename from src/init_predef.ml
rename to unused/init_predef.ml
diff --git a/src/lustre_utils.ml b/unused/lustre_utils.ml
similarity index 100%
rename from src/lustre_utils.ml
rename to unused/lustre_utils.ml
diff --git a/src/mmap.ml b/unused/mmap.ml
similarity index 100%
rename from src/mmap.ml
rename to unused/mmap.ml