diff --git a/src/lustre_utils.mli b/src/lustre_utils.mli new file mode 100644 index 0000000000000000000000000000000000000000..c1ff4951881a1afeaa61cd8c6b88313a128e7762 --- /dev/null +++ b/src/lustre_utils.mli @@ -0,0 +1 @@ +val check_eq: Lustre_types.node_desc -> Lustre_types.node_desc -> Lustre_types.node_desc diff --git a/src/verifierType.ml b/src/verifierType.ml new file mode 100644 index 0000000000000000000000000000000000000000..9ed16beadef01bc98021569d842460027e070a0d --- /dev/null +++ b/src/verifierType.ml @@ -0,0 +1,20 @@ +module type S = +sig + val name: string + val activate: unit -> unit + val is_active: unit -> bool + val options: (string * Arg.spec * string) list + val get_normalization_params: unit -> Normalization.param_t + val run: basename:string -> Lustre_types.program_t -> Machine_code_types.machine_t list -> unit +end + +module Default = + struct + + let get_normalization_params () = { + Normalization.unfold_arrow_active = true; + force_alias_ite = false; + force_alias_internal_fun = false; + } + + end