From 56f5e434670e0f541c90cf38f152ecddecd61152 Mon Sep 17 00:00:00 2001 From: ploc <ploc@garoche.net> Date: Tue, 12 Apr 2022 11:39:41 +0200 Subject: [PATCH] Missing files --- src/lustre_utils.mli | 1 + src/verifierType.ml | 20 ++++++++++++++++++++ 2 files changed, 21 insertions(+) create mode 100644 src/lustre_utils.mli create mode 100644 src/verifierType.ml diff --git a/src/lustre_utils.mli b/src/lustre_utils.mli new file mode 100644 index 00000000..c1ff4951 --- /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 00000000..9ed16bea --- /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 -- GitLab