From 50a8778acf2c7e82b1adc702c3f75135dbf9aa85 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?L=C3=A9lio=20Brun?= <lelio.brun@isae-supaero.fr>
Date: Fri, 25 Jun 2021 12:35:52 +0200
Subject: [PATCH] refactoring first step
---
src/annotations.ml | 2 +-
src/annotations.mli | 5 +
src/arrow.ml | 2 +-
src/automata.ml | 21 +-
src/automata.mli | 14 +
src/backends/Ada/ada_backend.mli | 0
src/backends/Ada/ada_backend_adb.mli | 0
src/backends/Ada/ada_backend_ads.mli | 0
src/backends/Ada/ada_backend_wrapper.mli | 0
src/backends/Ada/misc_lustre_function.ml | 28 +-
src/backends/Ada/misc_lustre_function.mli | 0
src/backends/Ada/misc_printer.mli | 1 +
src/backends/C/c_backend.mli | 0
src/backends/C/c_backend_cmake.mli | 0
src/backends/C/c_backend_common.ml | 4 +-
src/backends/C/c_backend_common.mli | 5 +
src/backends/C/c_backend_header.mli | 0
src/backends/C/c_backend_main.mli | 0
src/backends/C/c_backend_makefile.mli | 0
src/backends/C/c_backend_mauve.mli | 0
src/backends/C/c_backend_spec.ml | 33 +-
src/backends/C/c_backend_spec.mli | 3 +
src/backends/C/c_backend_src.mli | 0
src/backends/EMF/EMF_backend.mli | 0
src/backends/EMF/EMF_common.mli | 0
src/backends/EMF/EMF_library_calls.mli | 0
src/backends/Horn/horn_backend.mli | 0
.../Horn/horn_backend_collecting_sem.mli | 0
src/backends/Horn/horn_backend_common.mli | 0
src/backends/Horn/horn_backend_printers.mli | 0
src/backends/Horn/horn_backend_traces.mli | 0
src/backends/Java/java_backend.mli | 0
src/backends/VHDL/vhdl_ast.mli | 0
src/backends/VHDL/vhdl_test.mli | 0
src/backends/backends.ml | 13 +-
src/backends/backends.mli | 3 +
src/basic_library.mli | 17 +
src/causality.mli | 62 ++++
src/checks/access.mli | 0
src/checks/algebraicLoop.mli | 0
src/checks/init_calculus.mli | 0
src/checks/liveness.ml | 2 +
src/checks/liveness.mli | 18 +
src/checks/stateless.ml | 1 +
src/checks/stateless.mli | 16 +
src/clock_calculus.ml | 10 +-
src/clock_calculus.mli | 9 +
src/clock_predef.mli | 4 +
src/clocks.ml | 71 ++--
src/clocks.mli | 97 ++++++
src/compiler_common.ml | 22 +-
src/compiler_common.mli | 13 +
src/compiler_stages.ml | 5 +-
src/compiler_stages.mli | 0
src/corelang.ml | 29 +-
src/corelang.mli | 20 +-
src/delay.ml | 27 +-
src/delay.mli | 17 +
src/delay_predef.mli | 4 +
src/dune | 3 +-
src/error.ml | 13 +-
src/error.mli | 18 +
src/expand.mli | 0
src/features/machine_types/machine_types.ml | 6 +-
src/global.ml | 8 +-
src/global.mli | 3 +
src/init_predef.mli | 0
src/inliner.ml | 13 +-
src/inliner.mli | 0
src/log.ml | 4 +-
src/log.mli | 1 +
src/lusic.ml | 4 +-
src/lusic.mli | 14 +
src/lustre_live.ml | 2 +-
src/lustre_live.mli | 6 +
src/lustre_types.ml | 42 +--
src/lustre_types.mli | 229 +++++++++++++
src/lustre_utils.ml | 2 +-
src/lustre_utils.mli | 0
src/machine_code.ml | 8 +-
src/machine_code_common.ml | 40 ++-
src/machine_code_common.mli | 116 ++++---
...e_code_types.ml => machine_code_types.mli} | 5 +-
src/main_lustre_compiler.mli | 0
src/main_lustre_testgen.mli | 0
src/main_lustre_verifier.mli | 0
src/mmap.mli | 0
src/modules.ml | 2 +-
src/modules.mli | 4 +-
src/mutation.mli | 0
src/normalization.ml | 12 +-
src/normalization.mli | 1 +
src/optimize_machine.ml | 26 +-
src/optimize_machine.mli | 0
src/optimize_prog.mli | 0
src/options.ml | 30 +-
src/options.mli | 78 +++++
src/options_management.ml | 24 +-
src/options_management.mli | 6 +
src/parsers/lexerLustreSpec.mll | 4 +-
src/parsers/lexer_lustre.mll | 4 +-
src/parsers/parse.ml | 4 +-
src/parsers/parse.mli | 20 ++
src/pathConditions.mli | 0
src/plugins/mpfr/lustrec_mpfr.mli | 1 +
src/plugins/pluginList.ml | 2 +-
src/plugins/pluginList.mli | 2 +
src/plugins/pluginType.ml | 6 +
src/plugins/pluginType.mli | 25 ++
src/plugins/plugins.mli | 4 +
src/plugins/salsa/machine_salsa_opt.mli | 0
src/plugins/salsa/salsaDatatypes.mli | 0
src/plugins/salsa/salsa_plugin.mli | 0
src/plugins/scopes/scopes.ml | 21 +-
src/plugins/scopes/scopes.mli | 0
src/printers.ml | 87 ++---
src/printers.mli | 17 +
src/scheduling.ml | 8 +-
src/scheduling.mli | 9 +
...scheduling_type.ml => scheduling_type.mli} | 0
src/sortProg.ml | 11 +-
src/sortProg.mli | 4 +
src/spec.mli | 0
src/spec_common.mli | 19 +
src/spec_types.ml | 3 +-
src/spec_types.mli | 66 ++++
src/splitting.mli | 5 +
src/tools/importer/main_lustre_importer.mli | 0
src/tools/importer/vhdl_deriving_yojson.mli | 294 ++++++++++++++++
src/tools/importer/vhdl_json_lib.mli | 8 +
src/tools/seal/seal_export.mli | 0
src/tools/seal/seal_extract.mli | 0
src/tools/seal/seal_slice.mli | 0
src/tools/seal/seal_utils.mli | 0
src/tools/seal/seal_verifier.mli | 0
src/tools/stateflow/sf_sem.mli | 0
src/tools/tiny/tiny_utils.mli | 0
src/tools/tiny/tiny_verifier.mli | 0
src/tools/zustre/zustre_analyze.mli | 0
src/tools/zustre/zustre_cex.mli | 0
src/tools/zustre/zustre_common.mli | 0
src/tools/zustre/zustre_data.mli | 0
src/tools/zustre/zustre_test.mli | 0
src/tools/zustre/zustre_verifier.mli | 0
src/type_predef.ml | 8 +-
src/type_predef.mli | 32 ++
src/types.ml | 324 ++++++++----------
src/types.mli | 161 +++++++++
src/typing.ml | 32 +-
src/typing.mli | 28 ++
src/utils/dimension.ml | 42 +--
src/utils/dimension.mli | 46 +++
src/utils/env.ml | 4 +-
src/utils/env.mli | 12 +
src/utils/location.ml | 35 +-
src/utils/location.mli | 10 +
src/utils/utils.ml | 26 +-
src/utils/utils.mli | 93 +++++
src/verifierList.mli | 0
src/verifierType.mli | 17 +
src/verifiers.mli | 0
src/version.mli | 3 +
162 files changed, 2141 insertions(+), 654 deletions(-)
create mode 100644 src/annotations.mli
create mode 100644 src/automata.mli
create mode 100644 src/backends/Ada/ada_backend.mli
create mode 100644 src/backends/Ada/ada_backend_adb.mli
create mode 100644 src/backends/Ada/ada_backend_ads.mli
create mode 100644 src/backends/Ada/ada_backend_wrapper.mli
create mode 100644 src/backends/Ada/misc_lustre_function.mli
create mode 100644 src/backends/Ada/misc_printer.mli
create mode 100644 src/backends/C/c_backend.mli
create mode 100644 src/backends/C/c_backend_cmake.mli
create mode 100644 src/backends/C/c_backend_common.mli
create mode 100644 src/backends/C/c_backend_header.mli
create mode 100644 src/backends/C/c_backend_main.mli
create mode 100644 src/backends/C/c_backend_makefile.mli
create mode 100644 src/backends/C/c_backend_mauve.mli
create mode 100644 src/backends/C/c_backend_spec.mli
create mode 100644 src/backends/C/c_backend_src.mli
create mode 100644 src/backends/EMF/EMF_backend.mli
create mode 100644 src/backends/EMF/EMF_common.mli
create mode 100644 src/backends/EMF/EMF_library_calls.mli
create mode 100644 src/backends/Horn/horn_backend.mli
create mode 100644 src/backends/Horn/horn_backend_collecting_sem.mli
create mode 100644 src/backends/Horn/horn_backend_common.mli
create mode 100644 src/backends/Horn/horn_backend_printers.mli
create mode 100644 src/backends/Horn/horn_backend_traces.mli
create mode 100644 src/backends/Java/java_backend.mli
create mode 100644 src/backends/VHDL/vhdl_ast.mli
create mode 100644 src/backends/VHDL/vhdl_test.mli
create mode 100644 src/backends/backends.mli
create mode 100644 src/basic_library.mli
create mode 100644 src/causality.mli
create mode 100644 src/checks/access.mli
create mode 100644 src/checks/algebraicLoop.mli
create mode 100644 src/checks/init_calculus.mli
create mode 100644 src/checks/liveness.mli
create mode 100644 src/checks/stateless.mli
create mode 100644 src/clock_calculus.mli
create mode 100644 src/clock_predef.mli
create mode 100644 src/clocks.mli
create mode 100644 src/compiler_common.mli
create mode 100644 src/compiler_stages.mli
create mode 100644 src/delay.mli
create mode 100644 src/delay_predef.mli
create mode 100644 src/error.mli
create mode 100644 src/expand.mli
create mode 100644 src/global.mli
create mode 100644 src/init_predef.mli
create mode 100644 src/inliner.mli
create mode 100644 src/log.mli
create mode 100644 src/lusic.mli
create mode 100644 src/lustre_live.mli
create mode 100644 src/lustre_types.mli
create mode 100644 src/lustre_utils.mli
rename src/{machine_code_types.ml => machine_code_types.mli} (95%)
create mode 100644 src/main_lustre_compiler.mli
create mode 100644 src/main_lustre_testgen.mli
create mode 100644 src/main_lustre_verifier.mli
create mode 100644 src/mmap.mli
create mode 100644 src/mutation.mli
create mode 100644 src/optimize_machine.mli
create mode 100644 src/optimize_prog.mli
create mode 100644 src/options.mli
create mode 100644 src/options_management.mli
create mode 100644 src/parsers/parse.mli
create mode 100644 src/pathConditions.mli
create mode 100644 src/plugins/mpfr/lustrec_mpfr.mli
create mode 100644 src/plugins/pluginList.mli
create mode 100644 src/plugins/pluginType.mli
create mode 100644 src/plugins/plugins.mli
create mode 100644 src/plugins/salsa/machine_salsa_opt.mli
create mode 100644 src/plugins/salsa/salsaDatatypes.mli
create mode 100644 src/plugins/salsa/salsa_plugin.mli
create mode 100644 src/plugins/scopes/scopes.mli
create mode 100644 src/printers.mli
create mode 100644 src/scheduling.mli
rename src/{scheduling_type.ml => scheduling_type.mli} (100%)
create mode 100644 src/sortProg.mli
create mode 100644 src/spec.mli
create mode 100644 src/spec_common.mli
create mode 100644 src/spec_types.mli
create mode 100644 src/splitting.mli
create mode 100644 src/tools/importer/main_lustre_importer.mli
create mode 100644 src/tools/importer/vhdl_deriving_yojson.mli
create mode 100644 src/tools/importer/vhdl_json_lib.mli
create mode 100644 src/tools/seal/seal_export.mli
create mode 100644 src/tools/seal/seal_extract.mli
create mode 100644 src/tools/seal/seal_slice.mli
create mode 100644 src/tools/seal/seal_utils.mli
create mode 100644 src/tools/seal/seal_verifier.mli
create mode 100644 src/tools/stateflow/sf_sem.mli
create mode 100644 src/tools/tiny/tiny_utils.mli
create mode 100644 src/tools/tiny/tiny_verifier.mli
create mode 100644 src/tools/zustre/zustre_analyze.mli
create mode 100644 src/tools/zustre/zustre_cex.mli
create mode 100644 src/tools/zustre/zustre_common.mli
create mode 100644 src/tools/zustre/zustre_data.mli
create mode 100644 src/tools/zustre/zustre_test.mli
create mode 100644 src/tools/zustre/zustre_verifier.mli
create mode 100644 src/type_predef.mli
create mode 100644 src/types.mli
create mode 100644 src/typing.mli
create mode 100644 src/utils/dimension.mli
create mode 100644 src/utils/env.mli
create mode 100644 src/utils/location.mli
create mode 100644 src/utils/utils.mli
create mode 100644 src/verifierList.mli
create mode 100644 src/verifierType.mli
create mode 100644 src/verifiers.mli
create mode 100644 src/version.mli
diff --git a/src/annotations.ml b/src/annotations.ml
index 7da8dfb6..a82bf185 100644
--- a/src/annotations.ml
+++ b/src/annotations.ml
@@ -9,7 +9,7 @@
(* *)
(********************************************************************)
-open Lustre_types
+open Utils
(* Associate to each annotation key the pair (node, expr tag) *)
let expr_annotations : (string list, ident * tag) Hashtbl.t = Hashtbl.create 13
diff --git a/src/annotations.mli b/src/annotations.mli
new file mode 100644
index 00000000..9fe9f3fa
--- /dev/null
+++ b/src/annotations.mli
@@ -0,0 +1,5 @@
+open Utils
+
+val add_node_ann: ident -> string list -> unit
+val add_expr_ann: ident -> tag -> string list -> unit
+val get_expr_annotations: ident list -> (ident * tag) list
diff --git a/src/arrow.ml b/src/arrow.ml
index f2e933df..a5b57e96 100644
--- a/src/arrow.ml
+++ b/src/arrow.ml
@@ -32,7 +32,7 @@ let arrow_top_decl () =
top_decl_desc = Node arrow_desc;
top_decl_owner = Options_management.core_dependency "arrow";
top_decl_itf = false;
- top_decl_loc = Location.dummy_loc;
+ top_decl_loc = Location.dummy;
}
let td_is_arrow td = Corelang.node_name td = arrow_id
diff --git a/src/automata.ml b/src/automata.ml
index d75a4d58..04c8f6f0 100644
--- a/src/automata.ml
+++ b/src/automata.ml
@@ -53,16 +53,17 @@ let add_branch (loc, expr, restart, st) cont =
mkexpr loc (Expr_tuple [ mkbool loc restart; mkident loc st ]),
cont ))
-let mkhandler loc st unless until locals (stmts, asserts, annots) =
+let mkhandler hand_loc hand_state hand_unless hand_until hand_locals
+ (hand_stmts, hand_asserts, hand_annots) =
{
- hand_state = st;
- hand_unless = unless;
- hand_until = until;
- hand_locals = locals;
- hand_stmts = stmts;
- hand_asserts = asserts;
- hand_annots = annots;
- hand_loc = loc;
+ hand_state;
+ hand_unless;
+ hand_until;
+ hand_locals;
+ hand_stmts;
+ hand_asserts;
+ hand_annots;
+ hand_loc;
}
let mkautomata loc id handlers =
@@ -297,7 +298,7 @@ let node_of_assign_until nused used node aut_id aut_state handler =
in
let new_var_locals = node_vars_of_idents node writes in
let var_outputs =
- List.sort IdentModule.compare (node_vars_of_idents node writes)
+ List.sort VDeclModule.compare (node_vars_of_idents node writes)
in
let new_var_outputs =
List.map
diff --git a/src/automata.mli b/src/automata.mli
new file mode 100644
index 00000000..1e478988
--- /dev/null
+++ b/src/automata.mli
@@ -0,0 +1,14 @@
+open Utils
+open Lustre_types
+
+val mkhandler: Location.t -> ident -> (Location.t * expr * bool * ident) list
+ -> (Location.t * expr * bool * ident) list
+ -> var_decl list
+ -> statement list * assert_t list * expr_annot list -> handler_desc
+
+val mkautomata: Location.t -> ident -> handler_desc list -> automata_desc
+
+val expand_decls: program_t -> program_t
+
+(* val expand_automata: (ident -> bool) -> (ident -> bool) -> ident -> typedef_desc -> node_desc ->
+ * automata_desc -> top_decl list * var_decl list * statement list *)
diff --git a/src/backends/Ada/ada_backend.mli b/src/backends/Ada/ada_backend.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/backends/Ada/ada_backend_adb.mli b/src/backends/Ada/ada_backend_adb.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/backends/Ada/ada_backend_ads.mli b/src/backends/Ada/ada_backend_ads.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/backends/Ada/ada_backend_wrapper.mli b/src/backends/Ada/ada_backend_wrapper.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/backends/Ada/misc_lustre_function.ml b/src/backends/Ada/misc_lustre_function.ml
index 1647ba77..794ab385 100644
--- a/src/backends/Ada/misc_lustre_function.ml
+++ b/src/backends/Ada/misc_lustre_function.ml
@@ -77,12 +77,14 @@ let rec find_submachine_step_call ident instr_list =
let pp_eq_type typ1 typ2 =
let get_basic typ =
match (Types.repr typ).Types.tdesc with
- | Types.Tbasic Types.Basic.Tint ->
- Types.Basic.Tint
- | Types.Tbasic Types.Basic.Treal ->
- Types.Basic.Treal
- | Types.Tbasic Types.Basic.Tbool ->
- Types.Basic.Tbool
+ | Types.Tbasic t ->
+ t
+ (* | Types.Tbasic Types.Basic.Tint ->
+ * Types.Basic.Tint
+ * | Types.Tbasic Types.Basic.Treal ->
+ * Types.Basic.Treal
+ * | Types.Tbasic Types.Basic.Tbool ->
+ * Types.Basic.Tbool *)
| _ ->
assert false
(*TODO*)
@@ -91,7 +93,7 @@ let pp_eq_type typ1 typ2 =
(** Check that two types are the same. @param t1 a type @param t2 an other type
@param return true if the two types are Tbasic or Tunivar and equal **)
-let rec check_type_equal (t1 : Types.type_expr) (t2 : Types.type_expr) =
+let rec check_type_equal (t1 : Types.t) (t2 : Types.t) =
match (Types.repr t1).Types.tdesc, (Types.repr t2).Types.tdesc with
| Types.Tbasic x, Types.Tbasic y ->
x = y
@@ -114,8 +116,8 @@ let rec check_type_equal (t1 : Types.type_expr) (t2 : Types.type_expr) =
be polymorphic. @param subsitution the base substitution @param type_poly
the type which can be polymorphic @param typ the type to match type_poly
with **)
-let unification (substituion : (int * Types.type_expr) list)
- ((type_poly : Types.type_expr), (typ : Types.type_expr)) =
+let unification (substituion : (int * Types.t) list)
+ ((type_poly : Types.t), (typ : Types.t)) =
assert (not (is_Tunivar typ));
(* If type_poly is polymorphic *)
if is_Tunivar type_poly then
@@ -205,12 +207,8 @@ let get_instance identifier typed_submachines =
(*Usefull for debug*)
let pp_type_debug fmt typ =
match (Types.repr typ).Types.tdesc with
- | Types.Tbasic Types.Basic.Tint ->
- Format.fprintf fmt "INTEGER"
- | Types.Tbasic Types.Basic.Treal ->
- Format.fprintf fmt "FLOAT"
- | Types.Tbasic Types.Basic.Tbool ->
- Format.fprintf fmt "BOOLEAN"
+ | Types.Tbasic t ->
+ Types.BasicT.pp fmt t
| Types.Tunivar ->
Format.fprintf fmt "POLY(%i)" typ.Types.tid
| _ ->
diff --git a/src/backends/Ada/misc_lustre_function.mli b/src/backends/Ada/misc_lustre_function.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/backends/Ada/misc_printer.mli b/src/backends/Ada/misc_printer.mli
new file mode 100644
index 00000000..df403db0
--- /dev/null
+++ b/src/backends/Ada/misc_printer.mli
@@ -0,0 +1 @@
+type printer = Format.formatter -> unit
diff --git a/src/backends/C/c_backend.mli b/src/backends/C/c_backend.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/backends/C/c_backend_cmake.mli b/src/backends/C/c_backend_cmake.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/backends/C/c_backend_common.ml b/src/backends/C/c_backend_common.ml
index 4abd0122..454f2bff 100644
--- a/src/backends/C/c_backend_common.ml
+++ b/src/backends/C/c_backend_common.ml
@@ -852,12 +852,12 @@ let pp_clear m self pp_var fmt var =
(*** Common functions for main ***)
-let pp_print_file file_suffix fmt (typ, arg) =
+let pp_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_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
fprintf fmt "@[<v>%a@]"
diff --git a/src/backends/C/c_backend_common.mli b/src/backends/C/c_backend_common.mli
new file mode 100644
index 00000000..98fb6dc2
--- /dev/null
+++ b/src/backends/C/c_backend_common.mli
@@ -0,0 +1,5 @@
+open Utils
+
+val pp_file_decl: Format.formatter -> ident -> int -> unit
+val pp_file_open: Format.formatter -> ident -> int -> string
+val pp_put_var: Format.formatter -> string -> ident -> Types.t -> ident -> unit
diff --git a/src/backends/C/c_backend_header.mli b/src/backends/C/c_backend_header.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/backends/C/c_backend_main.mli b/src/backends/C/c_backend_main.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/backends/C/c_backend_makefile.mli b/src/backends/C/c_backend_makefile.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/backends/C/c_backend_mauve.mli b/src/backends/C/c_backend_mauve.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/backends/C/c_backend_spec.ml b/src/backends/C/c_backend_spec.ml
index 2c355abe..8143ff47 100644
--- a/src/backends/C/c_backend_spec.ml
+++ b/src/backends/C/c_backend_spec.ml
@@ -42,8 +42,6 @@ let pp_acsl_line pp fmt = fprintf fmt "//%@ @[<h>%a@]" pp
let pp_acsl_line' pp fmt = fprintf fmt "/*%@ @[<h>%a@] */" pp
-let pp_acsl_line_cut pp fmt = fprintf fmt "%a@," (pp_acsl_line pp)
-
let pp_requires pp_req fmt = fprintf fmt "requires %a;" pp_req
let pp_ensures pp_ens fmt = fprintf fmt "ensures %a;" pp_ens
@@ -152,8 +150,6 @@ let pp_separated' =
~pp_prologue:(fun fmt () -> pp_print_string fmt "\\separated(")
~pp_epilogue:pp_print_cpar pp_var_decl
-let pp_par pp fmt = fprintf fmt "(%a)" pp
-
let pp_forall pp_l pp_r fmt (l, r) =
fprintf fmt "@[<v 2>\\forall %a;@,%a@]" pp_l l pp_r r
@@ -162,8 +158,6 @@ let pp_exists pp_l pp_r fmt (l, r) =
let pp_equal pp_l pp_r fmt (l, r) = fprintf fmt "%a == %a" pp_l l pp_r r
-let pp_different pp_l pp_r fmt (l, r) = fprintf fmt "%a != %a" pp_l l pp_r r
-
let pp_implies pp_l pp_r fmt (l, r) =
fprintf fmt "@[<v>%a ==>@ %a@]" pp_l l pp_r r
@@ -174,8 +168,6 @@ let pp_and_l pp_v fmt =
~pp_sep:(fun fmt () -> fprintf fmt "@,&& ")
pp_v fmt
-let pp_or pp_l pp_r fmt (l, r) = fprintf fmt "@[<v>%a @ || %a@]" pp_l l pp_r r
-
let pp_or_l pp_v fmt =
pp_print_list ~pp_open_box:pp_open_vbox0
~pp_sep:(fun fmt () -> fprintf fmt "@,|| ")
@@ -242,8 +234,6 @@ let pp_assign_spec m self_l pp_var_l indirect_l self_r pp_var_r indirect_r fmt
reset_loop_counter ();
aux var_type fmt reordered_loop_vars
-let pp_nothing fmt () = pp_print_string fmt "\\nothing"
-
let pp_memory_pack_aux ?i pp_mem pp_self fmt (name, mem, self) =
fprintf fmt "%s_pack%a(@[<hov>%a,@ %a@])" name
(pp_print_option pp_print_int)
@@ -253,11 +243,6 @@ let pp_memory_pack pp_mem pp_self fmt (mp, mem, self) =
pp_memory_pack_aux ?i:mp.mpindex pp_mem pp_self fmt
(mp.mpname.node_id, mem, self)
-let pp_memory_pack_aux' ?i fmt =
- pp_memory_pack_aux ?i pp_print_string pp_print_string fmt
-
-let pp_memory_pack' fmt = pp_memory_pack pp_print_string pp_print_string fmt
-
let pp_transition_aux ?i m pp_mem_in pp_mem_out pp_var fmt
(name, vars, mem_in, mem_out) =
let stateless = fst (get_stateless_status m) in
@@ -276,15 +261,9 @@ let pp_transition m pp_mem_in pp_mem_out pp_var fmt (t, mem_in, mem_out) =
(t.tname.node_id, t.tvars, mem_in, mem_out)
let pp_transition_aux' ?i m =
- pp_transition_aux ?i m pp_print_string pp_print_string pp_var_decl
-
-let pp_transition_aux'' ?i m =
pp_transition_aux ?i m pp_print_string pp_print_string (fun fmt v ->
(if is_output m v then pp_ptr_decl else pp_var_decl) fmt v)
-let pp_transition' m =
- pp_transition m pp_print_string pp_print_string pp_var_decl
-
let pp_reset_cleared pp_mem_in pp_mem_out fmt (name, mem_in, mem_out) =
fprintf fmt "%s_reset_cleared(@[<hov>%a,@ %a@])" name pp_mem_in mem_in
pp_mem_out mem_out
@@ -455,7 +434,7 @@ module PrintSpec = struct
| Or fs ->
pp_or_l pp_spec' fmt fs
| Imply (a, b) ->
- pp_par (pp_implies pp_spec' pp_spec') fmt (a, b)
+ pp_paren (pp_implies pp_spec' pp_spec') fmt (a, b)
| Exists (xs, a) ->
pp_exists (pp_locals m) pp_spec' fmt (xs, a)
| Forall (xs, a) ->
@@ -475,7 +454,7 @@ module PrintSpec = struct
| StateVarPack (StateVar v) ->
let v' = vdecl_to_val v in
let inst = find_arrow m in
- pp_par
+ pp_paren
(pp_implies
(pp_not (pp_initialization pp_access'))
(pp_assign_spec m mem_out
@@ -650,12 +629,6 @@ let pp_reset_cleared_def fmt m =
( (name, (name, mem_in), (name, mem_out)),
(mem_in, ((mem_out, 0), (name, mem_out)), (mem_out, mem_in)) )
-let pp_at pp_p fmt (p, l) = fprintf fmt "\\at(%a, %s)" pp_p p l
-
-let label_pre = "Pre"
-
-let pp_at_pre pp_p fmt p = pp_at pp_p fmt (p, label_pre)
-
let pp_register_chain ?(indirect = true) ptr =
pp_print_list
~pp_prologue:(fun fmt () -> fprintf fmt "%s->" ptr)
@@ -812,7 +785,7 @@ module SrcMod = struct
outputs
(pp_requires pp_separated')
outputs (pp_assigns pp_ptr_decl) outputs
- (pp_ensures (pp_transition_aux'' m))
+ (pp_ensures (pp_transition_aux' m))
(name, inputs @ outputs, "", "")
else
fprintf fmt
diff --git a/src/backends/C/c_backend_spec.mli b/src/backends/C/c_backend_spec.mli
new file mode 100644
index 00000000..8a982275
--- /dev/null
+++ b/src/backends/C/c_backend_spec.mli
@@ -0,0 +1,3 @@
+module HdrMod: C_backend_header.MODIFIERS_HDR
+module SrcMod: C_backend_src.MODIFIERS_SRC
+module MakefileMod: C_backend_makefile.MODIFIERS_MKF
diff --git a/src/backends/C/c_backend_src.mli b/src/backends/C/c_backend_src.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/backends/EMF/EMF_backend.mli b/src/backends/EMF/EMF_backend.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/backends/EMF/EMF_common.mli b/src/backends/EMF/EMF_common.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/backends/EMF/EMF_library_calls.mli b/src/backends/EMF/EMF_library_calls.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/backends/Horn/horn_backend.mli b/src/backends/Horn/horn_backend.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/backends/Horn/horn_backend_collecting_sem.mli b/src/backends/Horn/horn_backend_collecting_sem.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/backends/Horn/horn_backend_common.mli b/src/backends/Horn/horn_backend_common.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/backends/Horn/horn_backend_printers.mli b/src/backends/Horn/horn_backend_printers.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/backends/Horn/horn_backend_traces.mli b/src/backends/Horn/horn_backend_traces.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/backends/Java/java_backend.mli b/src/backends/Java/java_backend.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/backends/VHDL/vhdl_ast.mli b/src/backends/VHDL/vhdl_ast.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/backends/VHDL/vhdl_test.mli b/src/backends/VHDL/vhdl_test.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/backends/backends.ml b/src/backends/backends.ml
index 22da34e0..0f37e533 100644
--- a/src/backends/backends.ml
+++ b/src/backends/backends.ml
@@ -2,7 +2,7 @@
let join_guards = ref true
let setup () =
- if !Options.output = "emf" then (
+ if !Options.output = Options.OutEMF then (
(* Not merging branches *)
join_guards := false;
(* In case of a default "int" type, substitute it with the legal int32 value *)
@@ -10,21 +10,22 @@ let setup () =
if !Options.optimization < 0 then join_guards := false
let is_functional () =
- match !Options.output with
- | "horn" | "lustre" | "acsl" | "emf" ->
+ let open Options in
+ match !output with
+ | OutHorn | OutLustre | OutEMF ->
true
| _ ->
false
(* Special treatment of arrows in lustre backend. We want to keep them *)
-let unfold_arrow () = match !Options.output with "lustre" -> false | _ -> true
+let unfold_arrow () = match !Options.output with Options.OutLustre -> false | _ -> true
(* Forcing ite normalization *)
-let alias_ite () = match !Options.output with "emf" -> true | _ -> false
+let alias_ite () = match !Options.output with Options.OutEMF -> true | _ -> false
(* Forcing basic functions normalization *)
let alias_internal_fun () =
- match !Options.output with "emf" -> true | _ -> false
+ match !Options.output with Options.OutEMF -> true | _ -> false
let get_normalization_params () =
{
diff --git a/src/backends/backends.mli b/src/backends/backends.mli
new file mode 100644
index 00000000..80fcce8c
--- /dev/null
+++ b/src/backends/backends.mli
@@ -0,0 +1,3 @@
+val setup: unit -> unit
+val is_functional: unit -> bool
+val join_guards: bool ref
diff --git a/src/basic_library.mli b/src/basic_library.mli
new file mode 100644
index 00000000..2727025c
--- /dev/null
+++ b/src/basic_library.mli
@@ -0,0 +1,17 @@
+open Utils
+
+val internal_funs: ident list
+val arith_funs: ident list
+val bool_funs: ident list
+val rel_funs: ident list
+val eval_dim_env: (Dimension.dim_desc list -> Dimension.dim_desc) Env.t
+val is_homomorphic_fun: ident -> bool
+val is_internal_fun: ident -> Types.t list -> bool
+val is_expr_internal_fun: Lustre_types.expr -> bool
+val is_value_internal_fun: Machine_code_types.value_t -> bool
+val is_stateless_fun: ident -> bool
+
+val type_env: Types.t Env.t
+val clock_env: Clocks.t Env.t
+
+val partial_eval: ident -> Lustre_types.expr -> Lustre_types.expr option -> Lustre_types.expr_desc
diff --git a/src/causality.mli b/src/causality.mli
new file mode 100644
index 00000000..cebaffce
--- /dev/null
+++ b/src/causality.mli
@@ -0,0 +1,62 @@
+open Utils
+open Lustre_types
+
+type error =
+ | DataCycle of ident list list
+ (* multiple failed partitions at once *)
+ | NodeCycle of ident list
+
+exception Error of error
+
+val pp_error: Format.formatter -> error -> unit
+
+module NodeDep: sig
+ val dependence_graph: program_t -> IdentDepGraph.t
+ val filter_static_inputs: var_decl list -> expr list -> Dimension.t list
+end
+
+(* Look for cycles in a dependency graph *)
+module CycleDetection: sig
+ val check_cycles: IdentDepGraph.t -> unit
+end
+
+(* A module to sort dependencies among local variables when relying on clocked
+ declarations *)
+module VarClockDep: sig
+ val sort: var_decl list -> var_decl list
+end
+
+module ExprDep: sig
+ (* instance vars represent node instance calls, they are not part of the
+ program/schedule, but used to simplify causality analysis *)
+ val mk_instance_var: ident -> ident
+ val is_instance_var: ident -> bool
+ val is_ghost_var: ident -> bool
+ val undo_instance_var: ident -> ident
+ val node_eq_equiv: node_desc -> (ident, ident) Hashtbl.t
+ val node_input_variables: node_desc -> ISet.t
+end
+
+(* Module used to compute static disjunction of variables based upon their
+ clocks. *)
+module Disjunction: sig
+ module CISet: Set.S with type elt = var_decl
+
+ (* map: var |-> list of disjoint vars, sorted in increasing branch length
+ order, maybe removing shorter branches *)
+ type disjoint_map = (ident, CISet.t) Hashtbl.t
+
+ val clock_disjoint_map: var_decl list -> disjoint_map
+end
+
+(* Tests whether [v] is a root of graph [g], i.e. a source *)
+val is_graph_root: ident -> IdentDepGraph.t -> bool
+
+(* Computes the set of graph roots, i.e. the sources of acyclic graph [g] *)
+val graph_roots: IdentDepGraph.t -> ident list
+
+(* Takes a node and return a pair (node', graph) where node' is node rebuilt
+ with the equations enriched with new ones introduced to "break cycles" *)
+val global_dependency: node_desc -> node_desc * IdentDepGraph.t
+
+val pp_dep_graph: Format.formatter -> IdentDepGraph.t -> unit
diff --git a/src/checks/access.mli b/src/checks/access.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/checks/algebraicLoop.mli b/src/checks/algebraicLoop.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/checks/init_calculus.mli b/src/checks/init_calculus.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/checks/liveness.ml b/src/checks/liveness.ml
index 3db48059..dea8fd0c 100644
--- a/src/checks/liveness.ml
+++ b/src/checks/liveness.ml
@@ -21,6 +21,8 @@ type context = {
policy : (ident, var_decl) Hashtbl.t;
}
+type fanin = (ident, tag) Hashtbl.t
+
(* computes the in-degree for each local variable of node [n], according to dep
graph [g]. *)
let compute_fanin n g =
diff --git a/src/checks/liveness.mli b/src/checks/liveness.mli
new file mode 100644
index 00000000..e6078ad6
--- /dev/null
+++ b/src/checks/liveness.mli
@@ -0,0 +1,18 @@
+open Utils
+open Lustre_types
+
+val compute_unused_variables: node_desc -> IdentDepGraph.t -> ISet.t
+
+type fanin = (ident, tag) Hashtbl.t
+
+ (* computes the in-degree for each local variable of node [n], according to dep
+ graph [g]. *)
+val compute_fanin: node_desc -> IdentDepGraph.t -> fanin
+
+val pp_fanin: Format.formatter -> fanin -> unit
+
+val compute_reuse_policy: node_desc -> ident list list ->
+ Causality.Disjunction.disjoint_map -> IdentDepGraph.t -> (ident, var_decl) Hashtbl.t
+
+(* replace variable [v] by [v'] in graph [g]. [v'] is a dead variable *)
+val replace_in_dep_graph: ident -> ident -> IdentDepGraph.t -> unit
diff --git a/src/checks/stateless.ml b/src/checks/stateless.ml
index 3d4cc7b3..32c67717 100644
--- a/src/checks/stateless.ml
+++ b/src/checks/stateless.ml
@@ -9,6 +9,7 @@
(* *)
(********************************************************************)
+open Utils
open Lustre_types
open Corelang
diff --git a/src/checks/stateless.mli b/src/checks/stateless.mli
new file mode 100644
index 00000000..33f466d3
--- /dev/null
+++ b/src/checks/stateless.mli
@@ -0,0 +1,16 @@
+open Utils
+open Lustre_types
+
+type error =
+ | Stateful_kwd of ident
+ | Stateful_imp of ident
+ | Stateful_ext_C of ident
+
+exception Error of Location.t * error
+
+val check_node: top_decl -> bool
+val check_prog: program_t -> unit
+val force_prog: program_t -> unit
+val check_compat: top_decl list -> unit
+
+val pp_error: Format.formatter -> error -> unit
diff --git a/src/clock_calculus.ml b/src/clock_calculus.ml
index 9cb97068..05b45a75 100644
--- a/src/clock_calculus.ml
+++ b/src/clock_calculus.ml
@@ -596,7 +596,7 @@ and clock_expr env expr =
in
Log.report ~level:4 (fun fmt ->
Format.fprintf fmt "Clock of expr %a: %a@ " Printers.pp_expr expr
- Clocks.print_ck resulting_ck);
+ Clocks.pp resulting_ck);
resulting_ck
let clock_of_vlist vars =
@@ -684,7 +684,7 @@ let clock_node env loc nd =
let ck_node = new_ck (Carrow (ck_ins, ck_outs)) false in
unify_imported_clock None ck_node loc;
Log.report ~level:3 (fun fmt ->
- Format.fprintf fmt "Clock of %s: %a@ " nd.node_id print_ck ck_node);
+ Format.fprintf fmt "Clock of %s: %a@ " nd.node_id Clocks.pp ck_node);
(* Local variables may contain first-order carrier variables that should be
generalized. That's not the case for types. *)
try_generalize ck_node loc;
@@ -697,7 +697,7 @@ let clock_node env loc nd =
(* if (is_main && is_polymorphic ck_node) then raise (Error
(loc,(Cannot_be_polymorphic ck_node))); *)
Log.report ~level:3 (fun fmt ->
- Format.fprintf fmt "Generalized clock of %s: %a@ @ " nd.node_id print_ck
+ Format.fprintf fmt "Generalized clock of %s: %a@ @ " nd.node_id Clocks.pp
ck_node);
nd.node_clock <- ck_node;
Env.add_value env nd.node_id ck_node
@@ -776,7 +776,7 @@ let uneval_vdecl_generics vdecl =
if Types.get_clock_base_type vdecl.var_type <> None then
match get_carrier_name vdecl.var_clock with
| None ->
- Format.eprintf "internal error: %a@." print_ck vdecl.var_clock;
+ Format.eprintf "internal error: %a@." Clocks.pp vdecl.var_clock;
assert false
| Some cr ->
Clocks.uneval vdecl.var_id cr
@@ -803,7 +803,7 @@ let check_env_compat header declared computed =
let computed_c =
instantiate (ref []) (ref []) (Env.lookup_value computed k)
in
- try_semi_unify decl_clock_k computed_c Location.dummy_loc
+ try_semi_unify decl_clock_k computed_c Location.dummy
with Not_found ->
(* If the lookup failed then either an actual required element should
have been declared and is missing but typing should have catch it, or
diff --git a/src/clock_calculus.mli b/src/clock_calculus.mli
new file mode 100644
index 00000000..2a57b425
--- /dev/null
+++ b/src/clock_calculus.mli
@@ -0,0 +1,9 @@
+open Lustre_types
+
+val clock_node: Clocks.t Env.t -> Location.t -> node_desc -> Clocks.t Env.t
+
+val compute_root_clock: Clocks.t -> Clocks.t
+
+val clock_prog: Clocks.t Env.t -> program_t -> Clocks.t Env.t
+
+val check_env_compat: top_decl list -> Clocks.t Env.t -> Clocks.t Env.t -> unit
diff --git a/src/clock_predef.mli b/src/clock_predef.mli
new file mode 100644
index 00000000..5558c9fa
--- /dev/null
+++ b/src/clock_predef.mli
@@ -0,0 +1,4 @@
+val ck_nullary_univ: Clocks.t
+val ck_unary_univ: Clocks.t
+val ck_bin_univ: Clocks.t
+val ck_tuple: Clocks.t list -> Clocks.t
diff --git a/src/clocks.ml b/src/clocks.ml
index 5290af2b..046693f8 100644
--- a/src/clocks.ml
+++ b/src/clocks.ml
@@ -36,7 +36,7 @@ and carrier_expr = {
carrier_id : int;
}
-type clock_expr = {
+type t = {
mutable cdesc : clock_desc;
mutable cscoped : bool;
cid : int;
@@ -44,41 +44,41 @@ type clock_expr = {
(* pck stands for periodic clock. Easier not to separate pck from other clocks *)
and clock_desc =
- | Carrow of clock_expr * clock_expr
- | Ctuple of clock_expr list
- | Con of clock_expr * carrier_expr * ident
- (* | Pck_up of clock_expr * int *)
- (* | Pck_down of clock_expr * int *)
- (* | Pck_phase of clock_expr * rat *)
+ | Carrow of t * t
+ | Ctuple of t list
+ | Con of t * carrier_expr * ident
+ (* | Pck_up of t * int *)
+ (* | Pck_down of t * int *)
+ (* | Pck_phase of t * rat *)
(* | Pck_const of int * rat *)
| Cvar (* of clock_set *)
(* Monomorphic clock variable *)
| Cunivar
(* of clock_set *)
(* Polymorphic clock variable *)
- | Clink of clock_expr
+ | Clink of t
(* During unification, make links instead of substitutions *)
- | Ccarrying of carrier_expr * clock_expr
+ | Ccarrying of carrier_expr * t
type error =
- | Clock_clash of clock_expr * clock_expr
+ | Clock_clash of t * t
(* | Not_pck *)
- (* | Clock_set_mismatch of clock_expr * clock_set *)
- | Cannot_be_polymorphic of clock_expr
- | Invalid_imported_clock of clock_expr
- | Invalid_const of clock_expr
+ (* | Clock_set_mismatch of t * clock_set *)
+ | Cannot_be_polymorphic of t
+ | Invalid_imported_clock of t
+ | Invalid_const of t
| Factor_zero
| Carrier_mismatch of carrier_expr * carrier_expr
- | Carrier_extrusion of clock_expr * carrier_expr
- | Clock_extrusion of clock_expr * clock_expr
+ | Carrier_extrusion of t * carrier_expr
+ | Clock_extrusion of t * t
-exception Unify of clock_expr * clock_expr
+exception Unify of t * t
exception Mismatch of carrier_expr * carrier_expr
exception Scope_carrier of carrier_expr
-exception Scope_clock of clock_expr
+exception Scope_clock of t
exception Error of Location.t * error
@@ -102,7 +102,8 @@ let rec print_ck_long fmt ck =
| Carrow (ck1, ck2) ->
fprintf fmt "%a -> %a" print_ck_long ck1 print_ck_long ck2
| Ctuple cklist ->
- fprintf fmt "(%a)" (fprintf_list ~sep:" * " print_ck_long) cklist
+ fprintf fmt "(%a)" (pp_print_list ~pp_sep:(fun fmt () -> pp_print_string fmt " * ")
+ print_ck_long) cklist
| Con (ck, c, l) ->
fprintf fmt "%a on %s(%a)" print_ck_long ck l print_carrier c
| Cvar ->
@@ -283,7 +284,7 @@ let eq_carrier cr1 cr2 =
| _ ->
cr1.carrier_id = cr2.carrier_id
-let eq_clock ck1 ck2 = (repr ck1).cid = (repr ck2).cid
+let equal ck1 ck2 = (repr ck1).cid = (repr ck2).cid
(* Returns the clock root of a clock *)
let rec root ck =
@@ -335,7 +336,7 @@ let rec disjoint_branches br1 br2 =
(* Disjunction relation between variables based upon their static clocks. *)
let disjoint ck1 ck2 =
- eq_clock (root ck1) (root ck2) && disjoint_branches (branch ck1) (branch ck2)
+ equal (root ck1) (root ck2) && disjoint_branches (branch ck1) (branch ck2)
let print_cvar fmt cvar =
match cvar.cdesc with
@@ -350,13 +351,13 @@ let print_cvar fmt cvar =
(* Nice pretty-printing. Simplifies expressions before printing them. Non-linear
complexity. *)
-let print_ck fmt ck =
+let pp fmt ck =
let rec aux fmt ck =
match ck.cdesc with
| Carrow (ck1, ck2) ->
fprintf fmt "%a -> %a" aux ck1 aux ck2
| Ctuple cklist ->
- fprintf fmt "(%a)" (fprintf_list ~sep:" * " aux) cklist
+ fprintf fmt "(%a)" (pp_print_list ~pp_sep:(fun fmt () -> pp_print_string fmt " * ") aux) cklist
| Con (ck, c, l) ->
fprintf fmt "%a on %s(%a)" aux ck l print_carrier c
| Cvar ->
@@ -373,50 +374,50 @@ let print_ck fmt ck =
let cvars = constrained_vars_of_clock ck in
aux fmt ck;
if cvars <> [] then
- fprintf fmt " (where %a)" (fprintf_list ~sep:", " print_cvar) cvars
+ fprintf fmt " (where %a)" (pp_comma_list print_cvar) cvars
(* prints only the Con components of a clock, useful for printing nodes *)
-let rec print_ck_suffix fmt ck =
+let rec pp_suffix fmt ck =
match ck.cdesc with
| Carrow _ | Ctuple _ | Cvar | Cunivar ->
()
| Con (ck, c, l) ->
- if !Options.kind2_print then print_ck_suffix fmt ck
- else fprintf fmt "%a when %s(%a)" print_ck_suffix ck l print_carrier c
+ if !Options.kind2_print then pp_suffix fmt ck
+ else fprintf fmt "%a when %s(%a)" pp_suffix ck l print_carrier c
| Clink ck' ->
- print_ck_suffix fmt ck'
+ pp_suffix fmt ck'
| Ccarrying (_, ck') ->
- fprintf fmt "%a" print_ck_suffix ck'
+ fprintf fmt "%a" pp_suffix ck'
let pp_error fmt = function
| Clock_clash (ck1, ck2) ->
reset_names ();
- fprintf fmt "Expected clock %a, got clock %a@." print_ck ck1 print_ck ck2
+ fprintf fmt "Expected clock %a, got clock %a@." pp ck1 pp ck2
| Carrier_mismatch (cr1, cr2) ->
fprintf fmt "Name clash. Expected clock %a, got clock %a@." print_carrier
cr1 print_carrier cr2
| Cannot_be_polymorphic ck ->
reset_names ();
- fprintf fmt "The main node cannot have a polymorphic clock: %a@." print_ck
+ fprintf fmt "The main node cannot have a polymorphic clock: %a@." pp
ck
| Invalid_imported_clock ck ->
reset_names ();
- fprintf fmt "Not a valid imported node clock: %a@." print_ck ck
+ fprintf fmt "Not a valid imported node clock: %a@." pp ck
| Invalid_const ck ->
reset_names ();
- fprintf fmt "Clock %a is not a valid periodic clock@." print_ck ck
+ fprintf fmt "Clock %a is not a valid periodic clock@." pp ck
| Factor_zero ->
fprintf fmt "Cannot apply clock transformation with factor 0@."
| Carrier_extrusion (ck, cr) ->
fprintf fmt
"This node has clock@.%a@.It is invalid as the carrier %a escapes its \
scope@."
- print_ck ck print_carrier cr
+ pp ck print_carrier cr
| Clock_extrusion (ck_node, ck) ->
fprintf fmt
"This node has clock@.%a@.It is invalid as the clock %a escapes its \
scope@."
- print_ck ck_node print_ck ck
+ pp ck_node pp ck
let const_of_carrier cr =
match (carrier_repr cr).carrier_desc with
diff --git a/src/clocks.mli b/src/clocks.mli
new file mode 100644
index 00000000..63f8688a
--- /dev/null
+++ b/src/clocks.mli
@@ -0,0 +1,97 @@
+open Utils
+
+(* Clock carriers basically correspond to the "c" in "x when c" *)
+type carrier_desc =
+ | Carry_const of ident
+ | Carry_name
+ | Carry_var
+ | Carry_link of carrier_expr
+
+(* Carriers are scoped, to detect clock extrusion. In other words, we check the
+ scope of a clock carrier before generalizing it. *)
+and carrier_expr = {
+ mutable carrier_desc : carrier_desc;
+ mutable carrier_scoped : bool;
+ carrier_id : int;
+}
+
+type t = {
+ mutable cdesc : clock_desc;
+ mutable cscoped : bool;
+ cid : int;
+}
+
+(* pck stands for periodic clock. Easier not to separate pck from other clocks *)
+and clock_desc =
+ | Carrow of t * t
+ | Ctuple of t list
+ | Con of t * carrier_expr * ident
+ | Cvar (* of clock_set *)
+ (* Monomorphic clock variable *)
+ | Cunivar
+ (* of clock_set *)
+ (* Polymorphic clock variable *)
+ | Clink of t
+ (* During unification, make links instead of substitutions *)
+ | Ccarrying of carrier_expr * t
+
+type error =
+ | Clock_clash of t * t
+ | Cannot_be_polymorphic of t
+ | Invalid_imported_clock of t
+ | Invalid_const of t
+ | Factor_zero
+ | Carrier_mismatch of carrier_expr * carrier_expr
+ | Carrier_extrusion of t * carrier_expr
+ | Clock_extrusion of t * t
+
+val pp: Format.formatter -> t -> unit
+val pp_suffix: Format.formatter -> t -> unit
+
+val new_var: bool -> t
+
+val new_univar: unit -> t
+
+val new_ck: clock_desc -> bool -> t
+
+val new_carrier: carrier_desc -> bool -> carrier_expr
+
+val bottom: t
+
+val repr: t -> t
+val carrier_repr: carrier_expr -> carrier_expr
+
+val simplify: t -> t
+
+val clock_on: t -> carrier_expr -> ident -> t
+
+val clock_of_clock_list: t list -> t
+val clock_list_of_clock: t -> t list
+
+val root: t -> t
+
+val branch: t -> (carrier_expr * ident) list
+
+val common_prefix: (carrier_expr * ident) list -> (carrier_expr * ident) list -> (carrier_expr * ident) list
+
+val clock_of_root_branch: t -> (carrier_expr * ident) list -> t
+
+val split_arrow: t -> t * t
+
+val clock_current: t -> t
+
+val uneval: ident -> carrier_expr -> unit
+
+val get_carrier_name: t -> carrier_expr option
+
+val equal: t -> t -> bool
+
+val const_of_carrier: carrier_expr -> ident
+
+val pp_error: Format.formatter -> error -> unit
+
+exception Unify of t * t
+exception Scope_carrier of carrier_expr
+exception Scope_clock of t
+exception Error of Location.t * error
+exception Mismatch of carrier_expr * carrier_expr
diff --git a/src/compiler_common.ml b/src/compiler_common.ml
index 8a0e6521..60269c47 100644
--- a/src/compiler_common.ml
+++ b/src/compiler_common.ml
@@ -16,9 +16,9 @@ open Corelang
let check_main () =
if !Options.main_node = "" then (
- eprintf "Code generation error: %a@." Error.pp_error_msg
+ eprintf "Code generation error: %a@." Error.pp
Error.No_main_specified;
- raise (Error.Error (Location.dummy_loc, Error.No_main_specified)))
+ raise (Error.Error (Location.dummy, Error.No_main_specified)))
let create_dest_dir () =
if not (Sys.file_exists !Options.dest_dir) then (
@@ -58,7 +58,7 @@ let parse filename extension =
* Parse.report_error err;
* raise exc *)
| Error.Error (loc, err) as exc ->
- eprintf "Parsing error: %a%a@." Error.pp_error_msg err Location.pp_loc loc;
+ eprintf "Parsing error: %a%a@." Error.pp err Location.pp loc;
raise exc
in
(* close_in f_in; *)
@@ -68,7 +68,7 @@ let expand_automata decls =
Log.report ~level:1 (fun fmt -> fprintf fmt "@ .. expanding automata@ ");
try Automata.expand_decls decls
with Error.Error (loc, err) as exc ->
- eprintf "Automata error: %a%a@." Error.pp_error_msg err Location.pp_loc loc;
+ eprintf "Automata error: %a%a@." Error.pp err Location.pp loc;
raise exc
let check_stateless_decls decls =
@@ -77,7 +77,7 @@ let check_stateless_decls decls =
try Stateless.check_prog decls
with Stateless.Error (loc, err) as exc ->
eprintf "Stateless status error: %a%a@." Stateless.pp_error err
- Location.pp_loc loc;
+ Location.pp loc;
raise exc
let force_stateful_decls decls =
@@ -85,7 +85,7 @@ let force_stateful_decls decls =
try Stateless.force_prog decls
with Stateless.Error (loc, err) as exc ->
eprintf "Stateless status error: %a%a@." Stateless.pp_error err
- Location.pp_loc loc;
+ Location.pp loc;
raise exc
let type_decls env decls =
@@ -93,7 +93,7 @@ let type_decls env decls =
let new_env =
try Typing.type_prog env decls
with Types.Error (loc, err) as exc ->
- eprintf "Typing error: %a%a@." Types.pp_error err Location.pp_loc loc;
+ eprintf "Typing error: %a%a@." Types.pp_error err Location.pp loc;
raise exc
in
Log.report ~level:1 (fun fmt -> fprintf fmt "@]");
@@ -107,7 +107,7 @@ let clock_decls env decls =
let new_env =
try Clock_calculus.clock_prog env decls
with Clocks.Error (loc, err) as exc ->
- eprintf "Clock calculus error: %a%a@." Clocks.pp_error err Location.pp_loc
+ eprintf "Clock calculus error: %a%a@." Clocks.pp_error err Location.pp
loc;
raise exc
in
@@ -154,19 +154,19 @@ let check_compatibility (_, computed_types_env, computed_clocks_env)
eprintf
"Type mismatch between computed type and declared type in lustre \
interface file: %a%a@."
- Types.pp_error err Location.pp_loc loc;
+ Types.pp_error err Location.pp loc;
raise exc
| Clocks.Error (loc, err) as exc ->
eprintf
"Clock mismatch between computed clock and declared clock in lustre \
interface file: %a%a@."
- Clocks.pp_error err Location.pp_loc loc;
+ Clocks.pp_error err Location.pp loc;
raise exc
| Stateless.Error (loc, err) as exc ->
eprintf
"Stateless status mismatch between defined status and declared status in \
lustre interface file: %a%a@."
- Stateless.pp_error err Location.pp_loc loc;
+ Stateless.pp_error err Location.pp loc;
raise exc
(* Process each node/imported node and introduce the associated contract node *)
diff --git a/src/compiler_common.mli b/src/compiler_common.mli
new file mode 100644
index 00000000..89d9d3d0
--- /dev/null
+++ b/src/compiler_common.mli
@@ -0,0 +1,13 @@
+open Lustre_types
+
+val check_main: unit -> unit
+
+(* Loading Lus/Lusi file and filling type tables with parsed functions/nodes *)
+val parse: string -> string -> program_t
+
+val check_compatibility: program_t * Types.t Env.t * Clocks.t Env.t ->
+ top_decl list * Types.t Env.t * Clocks.t Env.t -> unit
+
+val update_vdecl_parents_prog: program_t -> unit
+
+val expand_automata: program_t -> program_t
diff --git a/src/compiler_stages.ml b/src/compiler_stages.ml
index 7ce0503b..b3bb823b 100644
--- a/src/compiler_stages.ml
+++ b/src/compiler_stages.ml
@@ -6,7 +6,8 @@ module Mpfr = Lustrec_mpfr
exception StopPhase1 of program_t
let dynamic_checks () =
- match !Options.output, !Options.spec with "C", "C" -> true | _ -> false
+ let open Options in
+ match !output, !spec with OutC, SpecC -> true | _ -> false
let generate_c_header = ref false
@@ -36,7 +37,7 @@ let compile_source_to_header prog computed_types_env computed_clocks_env dirname
(* is it a lusi file ? *)
(if from_lusi then prog else Lusic.extract_header dirname basename prog)
destname lusic_ext;
- generate_c_header := !Options.output = "C")
+ generate_c_header := !Options.output = Options.OutC)
else (
(* Lusic exists and is usable. Checking compatibility *)
Log.report ~level:1 (fun fmt ->
diff --git a/src/compiler_stages.mli b/src/compiler_stages.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/corelang.ml b/src/corelang.ml
index fabbe47f..2c8097f2 100644
--- a/src/corelang.ml
+++ b/src/corelang.ml
@@ -9,6 +9,7 @@
(* *)
(********************************************************************)
+open Utils
open Format
open Lustre_types
open Machine_code_types
@@ -35,7 +36,7 @@ with type elt = var_decl = struct
let pp fmt s =
Format.fprintf fmt "{@[%a}@]"
- (Utils.fprintf_list ~sep:",@ " Printers.pp_var)
+ (pp_comma_list Printers.pp_var)
(elements s)
(* Strangley the find_first function of Set.Make is incorrect (at the current
@@ -44,10 +45,10 @@ with type elt = var_decl = struct
end
let dummy_type_dec =
- { ty_dec_desc = Tydec_any; ty_dec_loc = Location.dummy_loc }
+ { ty_dec_desc = Tydec_any; ty_dec_loc = Location.dummy }
let dummy_clock_dec =
- { ck_dec_desc = Ckdec_any; ck_dec_loc = Location.dummy_loc }
+ { ck_dec_desc = Ckdec_any; ck_dec_loc = Location.dummy }
(************************************************************)
(* *)
@@ -83,7 +84,7 @@ let dummy_var_decl name typ =
var_parent_nodeid = None;
var_type = typ;
var_clock = Clocks.new_ck Clocks.Cvar true;
- var_loc = Location.dummy_loc;
+ var_loc = Location.dummy;
}
let mkexpr loc d =
@@ -192,7 +193,7 @@ let empty_contract =
guarantees = [];
modes = [];
imports = [];
- spec_loc = Location.dummy_loc;
+ spec_loc = Location.dummy;
}
(* For const declaration we do as for regular lustre node. But for local flows
@@ -373,7 +374,7 @@ let is_contract td =
(* alias and type definition table *)
-let mktop = mktop_decl Location.dummy_loc !Options.dest_dir false
+let mktop = mktop_decl Location.dummy !Options.dest_dir false
let top_int_type = mktop (TypeDef { tydef_id = "int"; tydef_desc = Tydec_int })
@@ -440,7 +441,7 @@ let rec coretype_equal ty1 ty2 =
| Tydec_clock ty1, Tydec_clock ty2 ->
coretype_equal ty1 ty2
| Tydec_array (d1, ty1), Tydec_array (d2, ty2) ->
- Dimension.is_eq_dimension d1 d2 && coretype_equal ty1 ty2
+ Dimension.equal d1 d2 && coretype_equal ty1 ty2
| Tydec_enum tl1, Tydec_enum tl2 ->
List.sort compare tl1 = List.sort compare tl2
| Tydec_struct fl1, Tydec_struct fl2 ->
@@ -628,7 +629,7 @@ let rec expr_of_dimension dim =
expr_of_dimension dim'
| Dvar | Dunivar ->
Format.eprintf "internal error: Corelang.expr_of_dimension %a@."
- Dimension.pp_dimension dim;
+ Dimension.pp dim;
assert false
in
{ expr with expr_type = Types.new_ty Types.type_int }
@@ -1195,19 +1196,19 @@ let pp_decl_clock fmt cdecl =
| Node nd ->
fprintf fmt "%s: " nd.node_id;
Utils.reset_names ();
- fprintf fmt "%a@ " Clocks.print_ck nd.node_clock
+ fprintf fmt "%a@ " Clocks.pp nd.node_clock
| ImportedNode ind ->
fprintf fmt "%s: " ind.nodei_id;
Utils.reset_names ();
- fprintf fmt "%a@ " Clocks.print_ck ind.nodei_clock
+ fprintf fmt "%a@ " Clocks.pp ind.nodei_clock
| Const _ | Include _ | Open _ | TypeDef _ ->
()
-let pp_prog_clock fmt prog = Utils.fprintf_list ~sep:"" pp_decl_clock fmt prog
+let pp_prog_clock fmt prog = pp_print_list ~pp_sep:pp_print_nothing pp_decl_clock fmt prog
(* filling node table with internal functions *)
let vdecls_of_typ_ck cpt ty =
- let loc = Location.dummy_loc in
+ let loc = Location.dummy in
List.map
(fun _ ->
incr cpt;
@@ -1399,7 +1400,7 @@ let get_expr_vars e =
let rec get_expr_vars vars e = get_expr_desc_vars vars e.expr_desc
and get_expr_desc_vars vars expr_desc =
(*Format.eprintf "get_expr_desc_vars expr=%a@." Printers.pp_expr (mkexpr
- Location.dummy_loc expr_desc);*)
+ Location.dummy expr_desc);*)
match expr_desc with
| Expr_const _ ->
vars
@@ -1512,7 +1513,7 @@ let find_eq xl eqs =
match eqs with
| [] ->
Format.eprintf "Looking for variables %a in the following equations@.%a@."
- (Utils.fprintf_list ~sep:" , " (fun fmt v -> Format.fprintf fmt "%s" v))
+ (pp_comma_list (fun fmt v -> Format.fprintf fmt "%s" v))
xl Printers.pp_node_eqs eqs;
assert false
| hd :: tl ->
diff --git a/src/corelang.mli b/src/corelang.mli
index 8dea180d..43bc642c 100644
--- a/src/corelang.mli
+++ b/src/corelang.mli
@@ -8,7 +8,7 @@
(* version 2.1. *)
(* *)
(********************************************************************)
-
+open Utils
open Lustre_types
module VDeclModule : sig
@@ -16,7 +16,7 @@ module VDeclModule : sig
val compare : t -> t -> int
end
-with type t = Lustre_types.var_decl
+with type t = var_decl
module VSet : sig
include Set.S
@@ -25,7 +25,7 @@ module VSet : sig
val get : ident -> t -> elt
end
-with type elt = Lustre_types.var_decl
+with type elt = var_decl
val dummy_type_dec : type_dec
@@ -48,7 +48,7 @@ val mkvar_decl :
(* parent id *) ->
var_decl
-val dummy_var_decl : ident -> Types.type_expr -> var_decl
+val dummy_var_decl : ident -> Types.t -> var_decl
val var_decl_of_const : ?parentid:ident option -> const_desc -> var_decl
@@ -182,11 +182,11 @@ val expr_of_expr_list : Location.t -> expr list -> expr
val call_of_expr : expr -> ident * expr list * expr option
-val expr_of_dimension : Dimension.dim_expr -> expr
+val expr_of_dimension : Dimension.t -> expr
-val dimension_of_expr : expr -> Dimension.dim_expr
+val dimension_of_expr : expr -> Dimension.t
-val dimension_of_const : Location.t -> constant -> Dimension.dim_expr
+val dimension_of_const : Location.t -> constant -> Dimension.t
val expr_to_eexpr : expr -> eexpr
(* REMOVED, pushed in utils.ml val new_tag : unit -> tag *)
@@ -222,7 +222,7 @@ val get_node : ident -> program_t -> node_desc
(** Returns the node named ident in the provided program. Raise Not_found *)
val rename_static :
- (ident -> Dimension.dim_expr) -> type_dec_desc -> type_dec_desc
+ (ident -> Dimension.t) -> type_dec_desc -> type_dec_desc
val rename_carrier : (ident -> ident) -> clock_dec_desc -> clock_dec_desc
@@ -296,8 +296,8 @@ val reset_cpt_fresh : unit -> unit
val mk_fresh_var :
ident * var_decl list ->
Location.t ->
- Types.type_expr ->
- Clocks.clock_expr ->
+ Types.t ->
+ Clocks.t ->
var_decl
val find_eq : ident list -> eq list -> eq * eq list
diff --git a/src/delay.ml b/src/delay.ml
index 2e238256..bd257c6b 100644
--- a/src/delay.ml
+++ b/src/delay.ml
@@ -13,21 +13,21 @@ open Utils
(** Types definitions and a few utility functions on delay types. Delay analysis
by type polymorphism instead of constraints *)
-type delay_expr = { mutable ddesc : delay_desc; did : int }
+type t = { mutable ddesc : delay_desc; did : int }
and delay_desc =
| Dvar (* Monomorphic type variable *)
| Dundef
- | Darrow of delay_expr * delay_expr
- | Dtuple of delay_expr list
- | Dlink of delay_expr
+ | Darrow of t * t
+ | Dtuple of t list
+ | Dlink of t
(* During unification, make links instead of substitutions *)
| Dunivar
(* Polymorphic type variable *)
-type error = Delay_clash of delay_expr * delay_expr
+type error = Delay_clash of t * t
-exception Unify of delay_expr * delay_expr
+exception Unify of t * t
exception Error of Location.t * error
@@ -55,7 +55,7 @@ let split_arrow de =
failwith "Internal error: not an arrow type"
(** Returns the type corresponding to a type list. *)
-let delay_of_delay_list de =
+let of_delay_list de =
if List.length de > 1 then new_delay (Dtuple de) else List.hd de
(** [is_polymorphic de] returns true if [de] is polymorphic. *)
@@ -75,25 +75,26 @@ let rec is_polymorphic de =
true
(* Pretty-print*)
-open Format
+open Utils.Format
-let rec print_delay fmt de =
+let rec pp fmt de =
match de.ddesc with
| Dvar ->
fprintf fmt "'_%s" (name_of_type de.did)
| Dundef ->
fprintf fmt "1"
| Darrow (de1, de2) ->
- fprintf fmt "%a->%a" print_delay de1 print_delay de2
+ fprintf fmt "%a->%a" pp de1 pp de2
| Dtuple delist ->
- fprintf fmt "(%a)" (Utils.fprintf_list ~sep:"*" print_delay) delist
+ fprintf fmt "(%a)" (pp_print_list ~pp_sep:(fun fmt () -> pp_print_string fmt "*")
+ pp) delist
| Dlink de ->
- print_delay fmt de
+ pp fmt de
| Dunivar ->
fprintf fmt "'%s" (name_of_delay de.did)
let pp_error fmt = function
| Delay_clash (de1, de2) ->
Utils.reset_names ();
- fprintf fmt "Expected delay %a, got delay %a@." print_delay de1 print_delay
+ fprintf fmt "Expected delay %a, got delay %a@." pp de1 pp
de2
diff --git a/src/delay.mli b/src/delay.mli
new file mode 100644
index 00000000..d5132c7a
--- /dev/null
+++ b/src/delay.mli
@@ -0,0 +1,17 @@
+type t = { mutable ddesc : delay_desc; did : int }
+
+and delay_desc =
+ | Dvar (* Monomorphic type variable *)
+ | Dundef
+ | Darrow of t * t
+ | Dtuple of t list
+ | Dlink of t
+ (* During unification, make links instead of substitutions *)
+ | Dunivar
+(* Polymorphic type variable *)
+
+val new_var: unit -> t
+
+val new_univar: unit -> t
+
+val new_delay: delay_desc -> t
diff --git a/src/delay_predef.mli b/src/delay_predef.mli
new file mode 100644
index 00000000..8f323305
--- /dev/null
+++ b/src/delay_predef.mli
@@ -0,0 +1,4 @@
+val delay_nullary_poly_op: Delay.t
+val delay_unary_poly_op: Delay.t
+val delay_binary_poly_op: Delay.t
+val delay_ternary_poly_op: Delay.t
diff --git a/src/dune b/src/dune
index 10452d91..accc80f7 100644
--- a/src/dune
+++ b/src/dune
@@ -8,6 +8,7 @@
(library
(name lustrec_interface)
(package lustrec)
+ (modules_without_implementation scheduling_type machine_code_types)
(modules
lustre_types
utils
@@ -21,11 +22,11 @@
version
clocks
delay
+ scheduling_type
machine_code_types
spec_types
spec_common
lustre_live
- scheduling_type
log
printers
corelang
diff --git a/src/error.ml b/src/error.ml
index 657b616a..fd35e33a 100644
--- a/src/error.ml
+++ b/src/error.ml
@@ -1,8 +1,7 @@
+open Utils
open Format
-type ident = Lustre_types.ident
-
-type error_kind =
+type t =
| Main_not_found
| Main_wrong_kind
| No_main_specified
@@ -13,7 +12,7 @@ type error_kind =
| AlgebraicLoop
| LoadError of string
-exception Error of Location.t * error_kind
+exception Error of Location.t * t
let return_code kind =
match kind with
@@ -36,7 +35,7 @@ let return_code kind =
| LoadError _ ->
10
-let pp_error_msg fmt = function
+let pp fmt = function
| Main_not_found ->
fprintf fmt "Could not find the definition of main node %s.@."
!Global.main_node
@@ -66,7 +65,7 @@ let pp_error_msg fmt = function
fprintf fmt "Load error: %s.@." l
let pp_warning loc pp_msg =
- Format.eprintf "%a@.Warning: %t@." Location.pp_loc loc pp_msg
+ Format.eprintf "%a@.Warning: %t@." Location.pp loc pp_msg
let pp_error loc pp_msg =
- Format.eprintf "@.%a@.Error: @[<v 0>%t@]@.@?" Location.pp_loc loc pp_msg
+ Format.eprintf "@.%a@.Error: @[<v 0>%t@]@.@?" Location.pp loc pp_msg
diff --git a/src/error.mli b/src/error.mli
new file mode 100644
index 00000000..5adf214a
--- /dev/null
+++ b/src/error.mli
@@ -0,0 +1,18 @@
+open Utils
+
+type t =
+ | Main_not_found
+ | Main_wrong_kind
+ | No_main_specified
+ | Unbound_symbol of ident
+ | Already_bound_symbol of ident
+ | Unknown_library of ident
+ | Wrong_number of ident
+ | AlgebraicLoop
+ | LoadError of string
+
+exception Error of Location.t * t
+
+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
new file mode 100644
index 00000000..e69de29b
diff --git a/src/features/machine_types/machine_types.ml b/src/features/machine_types/machine_types.ml
index c7e6d538..25d82ca4 100644
--- a/src/features/machine_types/machine_types.ml
+++ b/src/features/machine_types/machine_types.ml
@@ -177,7 +177,7 @@ let type_int32 = MTypes.new_ty (MTypes.Tbasic (MT.MTint (Some MT.Tint32_t)))
let type_int64 = MTypes.new_ty (MTypes.Tbasic (MT.MTint (Some MT.Tint64_t)))
module ConvTypes = struct
- type type_expr = MTypes.type_expr
+ type type_expr = MTypes.t
let map_type_basic f_basic =
let rec map_type_basic e =
@@ -281,7 +281,7 @@ end
module Typing = Typing.Make (MTypes) (ConvTypes)
(* Associate to each (node_id, var_id) its machine type *)
-let machine_type_table : (var_decl, MTypes.type_expr) Hashtbl.t =
+let machine_type_table : (var_decl, MTypes.t) Hashtbl.t =
Hashtbl.create 13
(* Store the node signatures, with machine types when available *)
@@ -336,7 +336,7 @@ let pp_c_var_type fmt v =
let erroneous_annotation loc =
Format.eprintf "Invalid annotation for machine_type at loc %a@."
- Location.pp_loc loc;
+ Location.pp loc;
assert false
let valid_subtype subtype typ =
diff --git a/src/global.ml b/src/global.ml
index 95cc5a64..d9c43e37 100644
--- a/src/global.ml
+++ b/src/global.ml
@@ -1,9 +1,7 @@
-module Types = Types.Main
-
-let type_env : Types.type_expr Env.t ref = ref Env.initial
+let type_env : Types.t Env.t ref = ref Env.initial
(* Basic_library.type_env *)
-let clock_env : Clocks.clock_expr Env.t ref = ref Env.initial
+let clock_env : Clocks.t Env.t ref = ref Env.initial
(*Basic_library.clock_env *)
let basename = ref ""
@@ -17,7 +15,7 @@ module TypeEnv = struct
let iter f = Env.iter !type_env f
- let pp pp_fun fmt () = Env.pp_env pp_fun fmt !type_env
+ let pp pp_fun fmt () = Env.pp pp_fun fmt !type_env
end
let initialize () = main_node := !Options.main_node
diff --git a/src/global.mli b/src/global.mli
new file mode 100644
index 00000000..e5e0e45e
--- /dev/null
+++ b/src/global.mli
@@ -0,0 +1,3 @@
+val type_env: Types.t Env.t ref
+val clock_env: Clocks.t Env.t ref
+val main_node: string ref
diff --git a/src/init_predef.mli b/src/init_predef.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/inliner.ml b/src/inliner.ml
index fb31a3de..bfa3507d 100644
--- a/src/inliner.ml
+++ b/src/inliner.ml
@@ -375,7 +375,7 @@ let inline_all_calls node nodes =
{ node with top_decl_desc = Node (inline_node nd nodes) }
let witness filename main_name orig inlined (* type_env clock_env *) =
- let loc = Location.dummy_loc in
+ let loc = Location.dummy in
let rename_local_node nodes prefix id =
if List.exists (check_node_name id) nodes then prefix ^ id else id
in
@@ -551,13 +551,12 @@ let pp_inline_calls fmt prog =
let nodes_with_anns =
List.fold_left (fun accu (k, _) -> ISet.add k accu) ISet.empty local_anns
in
- Format.fprintf fmt "@[<v 0>Inlined expresssions in node (by tags):@ %a@]"
- (fprintf_list ~sep:"" (fun fmt top ->
+ Format.(fprintf fmt "@[<v 0>Inlined expresssions in node (by tags):@ %a@]"
+ (pp_print_list ~pp_sep:pp_print_nothing (fun fmt top ->
match top.top_decl_desc with
| Node nd when ISet.mem nd.node_id nodes_with_anns ->
- Format.fprintf fmt "%s: {@[<v 0>%a}@]@ " nd.node_id
- (fprintf_list ~sep:"@ " (fun fmt tag ->
- Format.fprintf fmt "%i" tag))
+ fprintf fmt "%s: {@[<v 0>%a}@]@ " nd.node_id
+ (pp_print_list pp_print_int)
(List.fold_left
(fun accu (id, tag) ->
if id = nd.node_id then tag :: accu else accu)
@@ -565,7 +564,7 @@ let pp_inline_calls fmt prog =
(* | Node nd -> Format.fprintf fmt "%s: no inline annotations"
nd.node_id *)
| _ ->
- ()))
+ ())))
prog
let local_inline prog (* type_env clock_env *) =
diff --git a/src/inliner.mli b/src/inliner.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/log.ml b/src/log.ml
index 8a651f30..8acc242a 100644
--- a/src/log.ml
+++ b/src/log.ml
@@ -9,9 +9,9 @@
(* *)
(********************************************************************)
-let report ?plugin:(modulename = "") ?(verbose_level = Options.verbose_level)
+let report ?plugin:(modulename = "") ?(verbose_level = (fun () -> !Options.verbose_level) ())
~level p =
- if !verbose_level >= level then
+ if verbose_level >= level then
if modulename = "" then Format.eprintf "%t" p
else Format.eprintf "[%s] @[%t@]" modulename p
diff --git a/src/log.mli b/src/log.mli
new file mode 100644
index 00000000..3a728392
--- /dev/null
+++ b/src/log.mli
@@ -0,0 +1 @@
+val report: ?plugin:string -> ?verbose_level:int -> level:int -> (Format.formatter -> unit) -> unit
diff --git a/src/lusic.ml b/src/lusic.ml
index 0ecdc255..0cf9d661 100644
--- a/src/lusic.ml
+++ b/src/lusic.ml
@@ -15,7 +15,7 @@ open Lustre_types
(* Lusic to/from Header Printing functions *)
(********************************************************************************************)
-type lusic = { obsolete : bool; from_lusi : bool; contents : top_decl list }
+type t = { obsolete : bool; from_lusi : bool; contents : program_t }
(* extracts a header from a program representing module owner = dirname/basename *)
let extract_header dirname basename prog =
@@ -41,7 +41,7 @@ let extract_header dirname basename prog =
let check_obsolete lusic basename =
if lusic.obsolete then
- raise (Error.Error (Location.dummy_loc, Error.Wrong_number basename))
+ raise (Error.Error (Location.dummy, Error.Wrong_number basename))
(* encode and write a header in a file *)
let write_lusic lusi (header : top_decl list) basename extension =
diff --git a/src/lusic.mli b/src/lusic.mli
new file mode 100644
index 00000000..e2068d98
--- /dev/null
+++ b/src/lusic.mli
@@ -0,0 +1,14 @@
+open Lustre_types
+
+type t = { obsolete : bool; from_lusi : bool; contents : program_t }
+
+(* extracts a header from a program representing module owner = dirname/basename *)
+val extract_header: string -> string -> program_t -> top_decl list
+
+(* read and decode a header from a file *)
+val read_lusic: string -> string -> t
+
+(* encode and write a header in a file *)
+val write_lusic: bool -> program_t -> string -> string -> unit
+
+val check_obsolete: t -> string -> unit
diff --git a/src/lustre_live.ml b/src/lustre_live.ml
index 6e66609a..913ab994 100644
--- a/src/lustre_live.ml
+++ b/src/lustre_live.ml
@@ -85,7 +85,7 @@ let set_live_of nid outputs locals sorted_eqs =
Format.(
fprintf fmt "Live variables of %s: %a@;@;" nid
(pp_print_list ~pp_open_box:pp_open_vbox0 (fun fmt (i, l) ->
- fprintf fmt "%i: %a" i pp_iset l))
+ fprintf fmt "%i: %a" i ISet.pp l))
(Live.bindings l)));
Hashtbl.add live nid l
diff --git a/src/lustre_live.mli b/src/lustre_live.mli
new file mode 100644
index 00000000..ae457e82
--- /dev/null
+++ b/src/lustre_live.mli
@@ -0,0 +1,6 @@
+open Utils
+open Lustre_types
+
+val inter_live_i_with: ident -> int -> var_decl list -> var_decl list
+val set_live_of: ident -> var_decl list -> var_decl list -> eq list -> unit
+val existential_vars: ident -> int -> eq -> var_decl list -> var_decl list
diff --git a/src/lustre_types.ml b/src/lustre_types.ml
index 19538aaf..824193cc 100644
--- a/src/lustre_types.ml
+++ b/src/lustre_types.ml
@@ -9,13 +9,9 @@
(* *)
(********************************************************************)
-type ident = Utils.ident
+open Utils
-type rat = Utils.rat
-
-type tag = Utils.tag
-
-type label = Utils.ident
+type label = ident
type type_dec = { ty_dec_desc : type_dec_desc; ty_dec_loc : Location.t }
@@ -29,7 +25,7 @@ and type_dec_desc =
| Tydec_const of ident
| Tydec_enum of ident list
| Tydec_struct of (ident * type_dec_desc) list
- | Tydec_array of Dimension.dim_expr * type_dec_desc
+ | Tydec_array of Dimension.t * type_dec_desc
type typedec_desc = { tydec_id : ident }
@@ -60,8 +56,8 @@ type var_decl = {
var_dec_const : bool;
var_dec_value : expr option;
mutable var_parent_nodeid : ident option;
- mutable var_type : Types.type_expr;
- mutable var_clock : Clocks.clock_expr;
+ mutable var_type : Types.t;
+ mutable var_clock : Clocks.t;
var_loc : Location.t;
}
(* The tag of an expression is a unique identifier used to distinguish different
@@ -75,9 +71,9 @@ type var_decl = {
and expr = {
expr_tag : tag;
expr_desc : expr_desc;
- mutable expr_type : Types.type_expr;
- mutable expr_clock : Clocks.clock_expr;
- mutable expr_delay : Delay.delay_expr;
+ mutable expr_type : Types.t;
+ mutable expr_clock : Clocks.t;
+ mutable expr_delay : Delay.t;
mutable expr_annot : expr_annot option;
expr_loc : Location.t;
}
@@ -90,8 +86,8 @@ and expr_desc =
| Expr_arrow of expr * expr
| Expr_fby of expr * expr
| Expr_array of expr list
- | Expr_access of expr * Dimension.dim_expr
- | Expr_power of expr * Dimension.dim_expr
+ | Expr_access of expr * Dimension.t
+ | Expr_power of expr * Dimension.t
| Expr_pre of expr
| Expr_when of expr * ident * label
| Expr_merge of ident * (label * expr) list
@@ -109,8 +105,8 @@ and eexpr = {
eexpr_qfexpr : expr;
eexpr_quantifiers : (quantifier_type * var_decl list) list;
eexpr_name : string option;
- mutable eexpr_type : Types.type_expr;
- mutable eexpr_clock : Clocks.clock_expr;
+ mutable eexpr_type : Types.t;
+ mutable eexpr_clock : Clocks.t;
(* mutable eexpr_normalized: (var_decl * eq list * var_decl list) option; *)
eexpr_loc : Location.t;
}
@@ -131,7 +127,7 @@ type contract_import = {
import_loc : Location.t;
}
-type offset = Index of Dimension.dim_expr | Field of label
+type offset = Index of Dimension.t | Field of label
type assert_t = { assert_expr : expr; assert_loc : Location.t }
@@ -169,13 +165,13 @@ type node_spec_t = Contract of contract_desc | NodeSpec of ident
type node_desc = {
node_id : ident;
- mutable node_type : Types.type_expr;
- mutable node_clock : Clocks.clock_expr;
+ mutable node_type : Types.t;
+ mutable node_clock : Clocks.t;
node_inputs : var_decl list;
node_outputs : var_decl list;
node_locals : var_decl list;
mutable node_gencalls : expr list;
- mutable node_checks : Dimension.dim_expr list;
+ mutable node_checks : Dimension.t list;
node_asserts : assert_t list;
node_stmts : statement list;
mutable node_dec_stateless : bool;
@@ -187,8 +183,8 @@ type node_desc = {
type imported_node_desc = {
nodei_id : ident;
- mutable nodei_type : Types.type_expr;
- mutable nodei_clock : Clocks.clock_expr;
+ mutable nodei_type : Types.t;
+ mutable nodei_clock : Clocks.t;
nodei_inputs : var_decl list;
nodei_outputs : var_decl list;
nodei_stateless : bool;
@@ -202,7 +198,7 @@ type const_desc = {
const_id : ident;
const_loc : Location.t;
const_value : constant;
- mutable const_type : Types.type_expr;
+ mutable const_type : Types.t;
}
type top_decl_desc =
diff --git a/src/lustre_types.mli b/src/lustre_types.mli
new file mode 100644
index 00000000..438158e6
--- /dev/null
+++ b/src/lustre_types.mli
@@ -0,0 +1,229 @@
+open Utils
+
+type label = ident
+
+type type_dec = { ty_dec_desc : type_dec_desc; ty_dec_loc : Location.t }
+
+and type_dec_desc =
+ | Tydec_any
+ | Tydec_int
+ | Tydec_real
+ (* | Tydec_float *)
+ | Tydec_bool
+ | Tydec_clock of type_dec_desc
+ | Tydec_const of ident
+ | Tydec_enum of ident list
+ | Tydec_struct of (ident * type_dec_desc) list
+ | Tydec_array of Dimension.t * type_dec_desc
+
+type typedec_desc = { tydec_id : ident }
+
+type typedef_desc = { tydef_id : ident; tydef_desc : type_dec_desc }
+
+type clock_dec = { ck_dec_desc : clock_dec_desc; ck_dec_loc : Location.t }
+
+and clock_dec_desc = Ckdec_any | Ckdec_bool of (ident * ident) list
+
+type constant =
+ | Const_int of int
+ | Const_real of Real.t
+ | Const_array of constant list
+ | Const_tag of label
+ | Const_string of string
+ (* used only for annotations *)
+ | Const_modeid of string
+ (* used only for annotations *)
+ | Const_struct of (label * constant) list
+
+type quantifier_type = Exists | Forall
+
+type var_decl = {
+ var_id : ident;
+ var_orig : bool;
+ var_dec_type : type_dec;
+ var_dec_clock : clock_dec;
+ var_dec_const : bool;
+ var_dec_value : expr option;
+ mutable var_parent_nodeid : ident option;
+ mutable var_type : Types.t;
+ mutable var_clock : Clocks.t;
+ var_loc : Location.t;
+}
+(* The tag of an expression is a unique identifier used to distinguish different
+ instances of the same node *)
+
+(** The core language and its ast. Every element of the ast contains its
+ location in the program text. The type and clock of an ast element is
+ mutable (and initialized to dummy values). This avoids to have to duplicate
+ ast structures (e.g. ast, typed_ast, clocked_ast). *)
+
+and expr = {
+ expr_tag : tag;
+ expr_desc : expr_desc;
+ mutable expr_type : Types.t;
+ mutable expr_clock : Clocks.t;
+ mutable expr_delay : Delay.t;
+ mutable expr_annot : expr_annot option;
+ expr_loc : Location.t;
+}
+
+and expr_desc =
+ | Expr_const of constant
+ | Expr_ident of ident
+ | Expr_tuple of expr list
+ | Expr_ite of expr * expr * expr
+ | Expr_arrow of expr * expr
+ | Expr_fby of expr * expr
+ | Expr_array of expr list
+ | Expr_access of expr * Dimension.t
+ | Expr_power of expr * Dimension.t
+ | Expr_pre of expr
+ | Expr_when of expr * ident * label
+ | Expr_merge of ident * (label * expr) list
+ | Expr_appl of call_t
+
+and call_t = ident * expr * expr option
+(* The third part denotes the boolean condition for resetting *)
+
+and eq = { eq_lhs : ident list; eq_rhs : expr; eq_loc : Location.t }
+
+(* The tag of an expression is a unique identifier used to distinguish different
+ instances of the same node *)
+and eexpr = {
+ eexpr_tag : tag;
+ eexpr_qfexpr : expr;
+ eexpr_quantifiers : (quantifier_type * var_decl list) list;
+ eexpr_name : string option;
+ mutable eexpr_type : Types.t;
+ mutable eexpr_clock : Clocks.t;
+ (* mutable eexpr_normalized: (var_decl * eq list * var_decl list) option; *)
+ eexpr_loc : Location.t;
+}
+
+and expr_annot = { annots : (string list * eexpr) list; annot_loc : Location.t }
+
+type contract_mode = {
+ mode_id : ident;
+ require : eexpr list;
+ ensure : eexpr list;
+ mode_loc : Location.t;
+}
+
+type contract_import = {
+ import_nodeid : ident;
+ inputs : expr;
+ outputs : expr;
+ import_loc : Location.t;
+}
+
+type offset = Index of Dimension.t | Field of label
+
+type assert_t = { assert_expr : expr; assert_loc : Location.t }
+
+type statement = Eq of eq | Aut of automata_desc
+
+and automata_desc = {
+ aut_id : ident;
+ aut_handlers : handler_desc list;
+ aut_loc : Location.t;
+}
+
+and handler_desc = {
+ hand_state : ident;
+ hand_unless : (Location.t * expr * bool * ident) list;
+ hand_until : (Location.t * expr * bool * ident) list;
+ hand_locals : var_decl list;
+ hand_stmts : statement list;
+ hand_asserts : assert_t list;
+ hand_annots : expr_annot list;
+ hand_loc : Location.t;
+}
+
+type contract_desc = {
+ consts : var_decl list;
+ locals : var_decl list;
+ stmts : statement list;
+ assume : eexpr list;
+ guarantees : eexpr list;
+ modes : contract_mode list;
+ imports : contract_import list;
+ spec_loc : Location.t;
+}
+
+type node_spec_t = Contract of contract_desc | NodeSpec of ident
+
+type node_desc = {
+ node_id : ident;
+ mutable node_type : Types.t;
+ mutable node_clock : Clocks.t;
+ node_inputs : var_decl list;
+ node_outputs : var_decl list;
+ node_locals : var_decl list;
+ mutable node_gencalls : expr list;
+ mutable node_checks : Dimension.t list;
+ node_asserts : assert_t list;
+ node_stmts : statement list;
+ mutable node_dec_stateless : bool;
+ mutable node_stateless : bool option;
+ node_spec : node_spec_t option;
+ node_annot : expr_annot list;
+ node_iscontract : bool;
+}
+
+type imported_node_desc = {
+ nodei_id : ident;
+ mutable nodei_type : Types.t;
+ mutable nodei_clock : Clocks.t;
+ nodei_inputs : var_decl list;
+ nodei_outputs : var_decl list;
+ nodei_stateless : bool;
+ nodei_spec : node_spec_t option;
+ (* nodei_annot: expr_annot list; *)
+ nodei_prototype : string option;
+ nodei_in_lib : string list;
+}
+
+type const_desc = {
+ const_id : ident;
+ const_loc : Location.t;
+ const_value : constant;
+ mutable const_type : Types.t;
+}
+
+type top_decl_desc =
+ | Node of node_desc
+ | Const of const_desc
+ | ImportedNode of imported_node_desc
+ | Open of bool * string
+ (* the boolean set to true denotes a local lusi vs a lusi installed at system
+ level *)
+ | Include of string
+ (* the boolean set to true denotes a local lus vs a lus installed at system
+ level *)
+ | TypeDef of typedef_desc
+
+type top_decl = {
+ top_decl_desc : top_decl_desc;
+ (* description of the symbol *)
+ top_decl_owner : Location.filename;
+ (* the module where it is defined *)
+ top_decl_itf : bool;
+ (* header or source file ? *)
+ top_decl_loc : Location.t;
+}
+
+type program_t = top_decl list
+
+type dep_t = {
+ local : bool;
+ name : ident;
+ content : program_t;
+ is_stateful : bool;
+}
+
+type spec_types =
+ | LocalContract of contract_desc
+ | TopContract of top_decl list
+
+val tag_true: label
+val tag_false: label
diff --git a/src/lustre_utils.ml b/src/lustre_utils.ml
index 92b19db8..932c5ecb 100644
--- a/src/lustre_utils.ml
+++ b/src/lustre_utils.ml
@@ -9,7 +9,7 @@ let check_eq nd1 nd2 =
(* TODO: check that nd1 and nd2 have the same signature *)
let check_nd = Corelang.copy_node nd1 in
(* to keep the type info *)
- let loc = Location.dummy_loc in
+ let loc = Location.dummy in
let ok_var =
Corelang.mkvar_decl loc ~orig:false
( "__OK",
diff --git a/src/lustre_utils.mli b/src/lustre_utils.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/machine_code.ml b/src/machine_code.ml
index d550720e..1400cbe8 100644
--- a/src/machine_code.ml
+++ b/src/machine_code.ml
@@ -92,7 +92,7 @@ let specialize_to_c expr =
expr
let specialize_op expr =
- match !Options.output with "C" -> specialize_to_c expr | _ -> expr
+ match !Options.output with Options.OutC -> specialize_to_c expr | _ -> expr
let rec translate_expr env expr =
let expr = specialize_op expr in
@@ -120,7 +120,7 @@ let rec translate_expr env expr =
removed for C or Java backends. *)
Fun ("ite", [ translate_expr g; translate_expr t; translate_expr e ])
| _ ->
- Format.eprintf "Normalization error for backend %s: %a@." !Options.output
+ Format.eprintf "Normalization error for backend %t: %a@." Options.pp_output
Printers.pp_expr expr;
raise NormalizationError
in
@@ -138,7 +138,7 @@ let rec translate_act env (y, expr) =
let translate_act = translate_act env in
let translate_guard = translate_guard env in
let translate_expr = translate_expr env in
- let lustre_eq = Corelang.mkeq Location.dummy_loc ([ y.var_id ], expr) in
+ let lustre_eq = Corelang.mkeq Location.dummy ([ y.var_id ], expr) in
match expr.expr_desc with
| Expr_ite (c, t, e) ->
let c = translate_guard c in
@@ -178,7 +178,7 @@ type machine_ctx = {
(* Reset instructions *)
si : instr_t list;
(* Instances *)
- j : (Lustre_types.top_decl * Dimension.dim_expr list) IMap.t;
+ j : (Lustre_types.top_decl * Dimension.t list) IMap.t;
(* Step instructions *)
s : instr_t list;
(* Memory pack spec *)
diff --git a/src/machine_code_common.ml b/src/machine_code_common.ml
index d8361c02..a904c679 100644
--- a/src/machine_code_common.ml
+++ b/src/machine_code_common.ml
@@ -2,7 +2,8 @@ open Lustre_types
open Machine_code_types
open Spec_types
open Corelang
-open Utils.Format
+open Utils
+open Format
let print_statelocaltag = true
@@ -130,10 +131,12 @@ module PrintSpec = struct
end
let pp_spec m =
- if !Options.spec <> "no" then
+ match !Options.spec with
+ | Options.SpecNo ->
+ pp_print_nothing
+ | _ ->
pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_prologue:pp_print_cut
(fun fmt -> fprintf fmt "@[<h>--%@ %a@]" (PrintSpec.pp_spec m))
- else pp_print_nothing
let rec pp_instr m fmt i =
let pp_val = pp_val m in
@@ -217,7 +220,7 @@ let pp_step m fmt s =
let pp_static_call fmt (node, args) =
fprintf fmt "%s<%a>" (node_name node)
- (pp_comma_list Dimension.pp_dimension)
+ (pp_comma_list Dimension.pp)
args
let pp_instance fmt (o1, o2) = fprintf fmt "(%s, %a)" o1 pp_static_call o2
@@ -229,9 +232,11 @@ let pp_memory_pack m fmt mp =
mp.mpindex (PrintSpec.pp_spec m) mp.mpformula
let pp_memory_packs m fmt =
- if !Options.spec <> "no" then
+ match !Options.spec with
+ | Options.SpecNo ->
+ pp_print_nothing fmt
+ | _ ->
fprintf fmt "@[<v 2>memory_packs:@ %a@]" (pp_print_list (pp_memory_pack m))
- else pp_print_nothing fmt
let pp_transition m fmt t =
fprintf fmt "@[<v 2>Transition_%a<SELF>%a%a =@ %a@]" pp_print_string
@@ -242,9 +247,11 @@ let pp_transition m fmt t =
t.tvars (PrintSpec.pp_spec m) t.tformula
let pp_transitions m fmt =
- if !Options.spec <> "no" then
+ match !Options.spec with
+ | Options.SpecNo ->
+ pp_print_nothing fmt
+ | _ ->
fprintf fmt "@[<v 2>transitions:@ %a@]" (pp_print_list (pp_transition m))
- else pp_print_nothing fmt
let pp_machine fmt m =
fprintf fmt
@@ -444,11 +451,10 @@ let get_machine_opt machines name =
None machines
let get_machine machines node_name =
- try Utils.desome (get_machine_opt machines node_name)
- with Utils.DeSome ->
+ try desome (get_machine_opt machines node_name)
+ with DeSome ->
eprintf "Unable to find machine %s in machines %a@.@?" node_name
- (Utils.fprintf_list ~sep:", " (fun fmt m ->
- pp_print_string fmt m.mname.node_id))
+ (pp_comma_list (fun fmt m -> pp_print_string fmt m.mname.node_id))
machines;
assert false
@@ -526,15 +532,15 @@ let rec value_of_dimension m dim =
let rec dimension_of_value value =
match value.value_desc with
| Cst (Const_tag t) when t = tag_true ->
- Dimension.mkdim_bool Location.dummy_loc true
+ Dimension.mkdim_bool Location.dummy true
| Cst (Const_tag t) when t = tag_false ->
- Dimension.mkdim_bool Location.dummy_loc false
+ Dimension.mkdim_bool Location.dummy false
| Cst (Const_int i) ->
- Dimension.mkdim_int Location.dummy_loc i
+ Dimension.mkdim_int Location.dummy i
| Var v ->
- Dimension.mkdim_ident Location.dummy_loc v.var_id
+ Dimension.mkdim_ident Location.dummy v.var_id
| Fun (f, args) ->
- Dimension.mkdim_appl Location.dummy_loc f (List.map dimension_of_value args)
+ Dimension.mkdim_appl Location.dummy f (List.map dimension_of_value args)
| _ ->
assert false
diff --git a/src/machine_code_common.mli b/src/machine_code_common.mli
index 254ccd55..ae2ba454 100644
--- a/src/machine_code_common.mli
+++ b/src/machine_code_common.mli
@@ -1,116 +1,120 @@
+open Utils
+open Lustre_types
+open Machine_code_types
+
val pp_val :
- Machine_code_types.machine_t ->
+ machine_t ->
Format.formatter ->
- Machine_code_types.value_t ->
+ value_t ->
unit
-val is_memory : Machine_code_types.machine_t -> Lustre_types.var_decl -> bool
+val is_memory : machine_t -> var_decl -> bool
-val is_reset_flag : Lustre_types.var_decl -> bool
+val is_reset_flag : var_decl -> bool
-val is_output : Machine_code_types.machine_t -> Lustre_types.var_decl -> bool
+val is_output : machine_t -> var_decl -> bool
-val is_const_value : Machine_code_types.value_t -> bool
+val is_const_value : value_t -> bool
val get_const_assign :
- Machine_code_types.machine_t ->
- Lustre_types.var_decl ->
- Machine_code_types.value_t
+ machine_t ->
+ var_decl ->
+ value_t
-val get_stateless_status_node : Lustre_types.node_desc -> bool * bool
+val get_stateless_status_node : node_desc -> bool * bool
-val get_stateless_status : Machine_code_types.machine_t -> bool * bool
+val get_stateless_status : machine_t -> bool * bool
-val get_stateless_status_top_decl : Lustre_types.top_decl -> bool * bool
+val get_stateless_status_top_decl : top_decl -> bool * bool
-val is_stateless : Machine_code_types.machine_t -> bool
+val is_stateless : machine_t -> bool
val mk_val :
- Machine_code_types.value_t_desc ->
- Types.type_expr ->
- Machine_code_types.value_t
+ value_t_desc ->
+ Types.t ->
+ value_t
-val vdecl_to_val : Lustre_types.var_decl -> Machine_code_types.value_t
+val vdecl_to_val : var_decl -> value_t
val vdecls_to_vals :
- Lustre_types.var_decl list -> Machine_code_types.value_t list
+ var_decl list -> value_t list
-val id_to_tag : Lustre_types.ident -> Machine_code_types.value_t
+val id_to_tag : ident -> value_t
val mk_conditional :
- ?lustre_eq:Lustre_types.eq ->
- Machine_code_types.value_t ->
- Machine_code_types.instr_t list ->
- Machine_code_types.instr_t list ->
- Machine_code_types.instr_t
+ ?lustre_eq:eq ->
+ value_t ->
+ instr_t list ->
+ instr_t list ->
+ instr_t
val mk_branch :
- ?lustre_eq:Lustre_types.eq ->
- Machine_code_types.value_t ->
- (Lustre_types.label * Machine_code_types.instr_t list) list ->
- Machine_code_types.instr_t
+ ?lustre_eq:eq ->
+ value_t ->
+ (label * instr_t list) list ->
+ instr_t
val mk_branch' :
- ?lustre_eq:Lustre_types.eq ->
- Lustre_types.var_decl ->
- (Lustre_types.label * Machine_code_types.instr_t list) list ->
- Machine_code_types.instr_t
+ ?lustre_eq:eq ->
+ var_decl ->
+ (label * instr_t list) list ->
+ instr_t
val mk_assign :
- ?lustre_eq:Lustre_types.eq ->
- Lustre_types.var_decl ->
- Machine_code_types.value_t ->
- Machine_code_types.instr_t
+ ?lustre_eq:eq ->
+ var_decl ->
+ value_t ->
+ instr_t
-val empty_machine : Machine_code_types.machine_t
+val empty_machine : machine_t
-val arrow_machine : Machine_code_types.machine_t
+val arrow_machine : machine_t
val new_instance :
- Lustre_types.top_decl -> Lustre_types.tag -> Lustre_types.ident
+ top_decl -> tag -> ident
val value_of_dimension :
- Machine_code_types.machine_t ->
- Dimension.dim_expr ->
- Machine_code_types.value_t
+ machine_t ->
+ Dimension.t ->
+ value_t
-val dimension_of_value : Machine_code_types.value_t -> Dimension.dim_expr
+val dimension_of_value : value_t -> Dimension.t
val pp_instr :
- Machine_code_types.machine_t ->
+ machine_t ->
Format.formatter ->
- Machine_code_types.instr_t ->
+ instr_t ->
unit
val pp_instrs :
- Machine_code_types.machine_t ->
+ machine_t ->
Format.formatter ->
- Machine_code_types.instr_t list ->
+ instr_t list ->
unit
-val pp_machines : Format.formatter -> Machine_code_types.machine_t list -> unit
+val pp_machines : Format.formatter -> machine_t list -> unit
val get_machine_opt :
- Machine_code_types.machine_t list ->
+ machine_t list ->
string ->
- Machine_code_types.machine_t option
+ machine_t option
(* Same function but fails if no such a machine exists *)
val get_machine :
- Machine_code_types.machine_t list -> string -> Machine_code_types.machine_t
+ machine_t list -> string -> machine_t
val get_node_def :
- string -> Machine_code_types.machine_t -> Lustre_types.node_desc
+ string -> machine_t -> node_desc
val join_guards_list :
- Machine_code_types.instr_t list -> Machine_code_types.instr_t list
+ instr_t list -> instr_t list
-val machine_vars : Machine_code_types.machine_t -> Lustre_types.var_decl list
+val machine_vars : machine_t -> var_decl list
module PrintSpec : sig
val pp_spec :
- Machine_code_types.machine_t ->
+ machine_t ->
Format.formatter ->
- Machine_code_types.value_t Spec_types.formula_t ->
+ value_t Spec_types.formula_t ->
unit
end
diff --git a/src/machine_code_types.ml b/src/machine_code_types.mli
similarity index 95%
rename from src/machine_code_types.ml
rename to src/machine_code_types.mli
index 7bd08add..7f2ecfaa 100644
--- a/src/machine_code_types.ml
+++ b/src/machine_code_types.mli
@@ -1,10 +1,11 @@
(************ Machine code types *************)
+open Utils
open Lustre_types
open Spec_types
type value_t = {
value_desc : value_t_desc;
- value_type : Types.type_expr;
+ value_type : Types.t;
value_annot : expr_annot option;
}
@@ -50,7 +51,7 @@ type step_t = {
step_asserts : value_t list;
}
-type static_call = top_decl * Dimension.dim_expr list
+type static_call = top_decl * Dimension.t list
type mc_transition_t = value_t transition_t
diff --git a/src/main_lustre_compiler.mli b/src/main_lustre_compiler.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/main_lustre_testgen.mli b/src/main_lustre_testgen.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/main_lustre_verifier.mli b/src/main_lustre_verifier.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/mmap.mli b/src/mmap.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/modules.ml b/src/modules.ml
index 084cdf2a..8ef27827 100644
--- a/src/modules.ml
+++ b/src/modules.ml
@@ -340,5 +340,5 @@ let load ~is_header program =
(* Format.eprintf "Import error: %a%a@."
* Error.pp_error_msg err
* Location.pp_loc loc; *)
- Format.eprintf "Import error: %a@." Error.pp_error_msg err;
+ Format.eprintf "Import error: %a@." Error.pp err;
raise exc
diff --git a/src/modules.mli b/src/modules.mli
index 4aa08751..cb792261 100644
--- a/src/modules.mli
+++ b/src/modules.mli
@@ -14,8 +14,8 @@ open Lustre_types
val load :
is_header:bool ->
program_t ->
- program_t * dep_t list * (Typing.type_expr Env.t * Clocks.clock_expr Env.t)
+ program_t * dep_t list * (Types.t Env.t * Clocks.t Env.t)
(* Returns an updated env with the type/clock declaration of the program *)
val get_envs_from_top_decls :
- program_t -> Typing.type_expr Env.t * Clocks.clock_expr Env.t
+ program_t -> Types.t Env.t * Clocks.t Env.t
diff --git a/src/mutation.mli b/src/mutation.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/normalization.ml b/src/normalization.ml
index c9fe1d47..6b5a86b7 100644
--- a/src/normalization.ml
+++ b/src/normalization.ml
@@ -86,7 +86,7 @@ let expr_once loc ck =
}
let is_expr_once =
- let dummy_expr_once = expr_once Location.dummy_loc (Clocks.new_var true) in
+ let dummy_expr_once = expr_once Location.dummy (Clocks.new_var true) in
fun expr -> Corelang.is_eq_expr expr dummy_expr_once
let unfold_arrow expr =
@@ -103,7 +103,7 @@ let get_expr_alias defs expr =
Some
(List.find
(fun eq ->
- Clocks.eq_clock expr.expr_clock eq.eq_rhs.expr_clock
+ Clocks.equal expr.expr_clock eq.eq_rhs.expr_clock
&& is_eq_expr eq.eq_rhs expr)
defs)
with Not_found -> None
@@ -151,7 +151,7 @@ let mk_expr_alias_opt opt norm_ctx (defs, vars) expr =
if !debug then
Log.report ~plugin:"normalization" ~level:2 (fun fmt ->
Format.fprintf fmt "mk_expr_alias_opt %B %a %a %a@." opt
- Printers.pp_expr expr Types.print_ty expr.expr_type Clocks.print_ck
+ Printers.pp_expr expr Types.print_ty expr.expr_type Clocks.pp
expr.expr_clock);
match expr.expr_desc with
| Expr_ident _ -> (defs, vars), expr
@@ -579,8 +579,8 @@ let normalize_pred_eexpr norm_ctx (def, vars) ee =
with Types.Error (loc, err) as exc ->
eprintf "Typing error for eexpr %a: %a%a%a@." Printers.pp_eexpr ee
Types.pp_error err
- (Utils.fprintf_list ~sep:", " Printers.pp_node_eq)
- defs Location.pp_loc loc;
+ (pp_comma_list Printers.pp_node_eq)
+ defs Location.pp loc;
raise exc
@@ -834,7 +834,7 @@ let normalize_node node =
[ "traceability" ];
[ "traceability" ], pair)
diff_vars;
- annot_loc = Location.dummy_loc;
+ annot_loc = Location.dummy;
}
in
norm_traceability :: node.node_annot
diff --git a/src/normalization.mli b/src/normalization.mli
index 51027651..80503773 100644
--- a/src/normalization.mli
+++ b/src/normalization.mli
@@ -1,3 +1,4 @@
+open Utils
open Lustre_types
type param_t = {
diff --git a/src/optimize_machine.ml b/src/optimize_machine.ml
index 2f9d14ac..2e25139d 100644
--- a/src/optimize_machine.ml
+++ b/src/optimize_machine.ml
@@ -20,7 +20,7 @@ open Dimension
module Mpfr = Lustrec_mpfr
let pp_elim m fmt elim =
- pp_imap ~comment:"/* elim table: */" (pp_val m) fmt elim
+ IMap.pp ~comment:"/* elim table: */" (pp_val m) fmt elim
(* Format.fprintf fmt "@[<hv 0>@[<hv 2>{ /* elim table: */";
* IMap.iter (fun v expr -> Format.fprintf fmt "@ %s |-> %a," v (pp_val m) expr) elim;
* Format.fprintf fmt "@]@ }@]" *)
@@ -96,10 +96,10 @@ let rec simplify_cst_expr m offset typ cst =
match offset, cst with
| [], _ ->
mk_val (Cst cst) typ
- | Index i :: q, Const_array cl when Dimension.is_dimension_const i ->
+ | Index i :: q, Const_array cl when Dimension.is_const i ->
let elt_typ = Types.array_element_type typ in
simplify_cst_expr m q elt_typ
- (List.nth cl (Dimension.size_const_dimension i))
+ (List.nth cl (Dimension.size_const i))
| Index i :: q, Const_array cl ->
let elt_typ = Types.array_element_type typ in
unfold_expr_offset m [ Index i ]
@@ -131,8 +131,8 @@ let simplify_expr_offset m expr =
expr
| Index _ :: q, Power (expr, _) ->
simplify q expr
- | Index i :: q, Array vl when Dimension.is_dimension_const i ->
- simplify q (List.nth vl (Dimension.size_const_dimension i))
+ | Index i :: q, Array vl when Dimension.is_const i ->
+ simplify q (List.nth vl (Dimension.size_const i))
| Index i :: q, Array vl ->
unfold_expr_offset m [ Index i ]
(mk_val (Array (List.map (simplify q) vl)) expr.value_type)
@@ -182,8 +182,8 @@ let is_unfoldable_expr fanin expr =
unfold_const q (List.assoc f fl)
| [], Const_struct _ ->
false
- | Index i :: q, Const_array cl when Dimension.is_dimension_const i ->
- unfold_const q (List.nth cl (Dimension.size_const_dimension i))
+ | Index i :: q, Const_array cl when Dimension.is_const i ->
+ unfold_const q (List.nth cl (Dimension.size_const i))
| _, Const_array _ ->
false
| _ ->
@@ -199,8 +199,8 @@ let is_unfoldable_expr fanin expr =
false
| Index _ :: q, Power (v, _) ->
unfold q v
- | Index i :: q, Array vl when Dimension.is_dimension_const i ->
- unfold q (List.nth vl (Dimension.size_const_dimension i))
+ | Index i :: q, Array vl when Dimension.is_const i ->
+ unfold q (List.nth vl (Dimension.size_const i))
| _, Array _ ->
false
| _, Access (v, i) ->
@@ -298,7 +298,7 @@ and instr_unfold m fanin instrs (elim : (value_t * eq) IMap.t) instr =
let static_call_unfold elim (inst, (n, args)) =
let replace v =
try dimension_of_value (IMap.find v elim)
- with Not_found -> Dimension.mkdim_ident Location.dummy_loc v
+ with Not_found -> Dimension.mkdim_ident Location.dummy v
in
inst, (n, List.map (Dimension.expr_replace_expr replace) args)
@@ -351,7 +351,7 @@ let instr_of_const top_const =
let vdecl =
mkvar_decl loc
( id,
- mktyp Location.dummy_loc Tydec_any,
+ mktyp Location.dummy Tydec_any,
mkclock loc Ckdec_any,
true,
None,
@@ -880,7 +880,7 @@ let optimize params prog node_schs machine_code =
(* Optimize machine code *)
let prog, machine_code, removed_table =
if
- !Options.optimization >= 2 && !Options.output <> "emf"
+ !Options.optimization >= 2 && !Options.output <> Options.OutEMF
(*&& !Options.output <> "horn"*)
then (
Log.report ~level:1 (fun fmt ->
@@ -892,7 +892,7 @@ let optimize params prog node_schs machine_code =
in
Log.report ~level:3 (fun fmt ->
Format.fprintf fmt "@ Eliminated flows: %a@ "
- (pp_imap (fun fmt m -> pp_elim empty_machine fmt (IMap.map fst m)))
+ (IMap.pp (fun fmt m -> pp_elim empty_machine fmt (IMap.map fst m)))
removed_table);
Log.report ~level:3 (fun fmt ->
Format.fprintf fmt
diff --git a/src/optimize_machine.mli b/src/optimize_machine.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/optimize_prog.mli b/src/optimize_prog.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/options.ml b/src/options.ml
index 7a481a4d..e19289a8 100644
--- a/src/options.ml
+++ b/src/options.ml
@@ -9,10 +9,6 @@
(* *)
(********************************************************************)
-let version = Version.number
-
-let codename = Version.codename
-
let include_dirs = ref [ "." ]
let main_node = ref ""
@@ -31,9 +27,29 @@ let ansi = ref false
let check = ref false
-let spec = ref "no"
-
-let output = ref "C"
+type option_spec =
+ | SpecNo
+ | SpecACSL
+ | SpecC
+
+let spec = ref SpecNo
+
+type option_output =
+ | OutC
+ | OutAda
+ | OutEMF
+ | OutHorn
+ | OutLustre
+
+let output = ref OutC
+
+let pp_output fmt =
+ Format.pp_print_string fmt (match !output with
+ | OutC -> "C"
+ | OutAda -> "Ada"
+ | OutEMF -> "EMF"
+ | OutHorn -> "Horn"
+ | OutLustre -> "Lustre")
let dest_dir = ref "."
diff --git a/src/options.mli b/src/options.mli
new file mode 100644
index 00000000..9a9d5206
--- /dev/null
+++ b/src/options.mli
@@ -0,0 +1,78 @@
+val kind2_print: bool ref
+val mpfr: bool ref
+val print_dec_types: bool ref
+val verbose_level: int ref
+val main_node: string ref
+val global_inline: bool ref
+val mpfr_prec: int ref
+
+type option_spec =
+ | SpecNo
+ | SpecACSL
+ | SpecC
+
+val spec: option_spec ref
+
+type option_output =
+ | OutC
+ | OutAda
+ | OutEMF
+ | OutHorn
+ | OutLustre
+ (* | OutACSL *)
+
+val output: option_output ref
+
+val pp_output: Format.formatter -> unit
+
+val ansi: bool ref
+
+val int_type: string ref
+val real_type: string ref
+
+val optimization: int ref
+
+val include_dirs: string list ref
+
+val dest_dir: string ref
+
+val print_types: bool ref
+val print_clocks: bool ref
+val print_nodes: bool ref
+val print_prec_double: int ref
+
+val solve_al: bool ref
+val al_nb_max: int ref
+
+val delay_calculus: bool ref
+
+val static_mem: bool ref
+
+val check: bool ref
+
+val lusi: bool ref
+
+val traces: bool ref
+
+val horn_cex: bool ref
+val horn_query: bool ref
+
+val sfunction: string ref
+
+val print_reuse: bool ref
+
+val const_unfold: bool ref
+
+val witnesses: bool ref
+
+val cpp: bool ref
+
+val integer_div_euclidean: bool ref
+
+val mauve: string ref
+
+val nb_mutants: int ref
+
+val gen_mcdc: bool ref
+
+val no_mutation_suffix: bool ref
diff --git a/src/options_management.ml b/src/options_management.ml
index fa950c51..fd9f1e5e 100644
--- a/src/options_management.ml
+++ b/src/options_management.ml
@@ -15,7 +15,7 @@ let print_version () =
printf
"@[<v>Lustrec compiler, version %s (%s)@,\
Standard lib: %s@,\
- User provided include directory: @[<h>%a@]@]@." version codename
+ User provided include directory: @[<h>%a@]@]@." Version.number Version.codename
Version.include_path
(pp_print_list ~pp_sep:pp_print_space pp_print_string)
!include_dirs
@@ -50,7 +50,7 @@ let search_lib_path (local, full_file_name) =
match name with
| None ->
Format.eprintf "Unable to find library %s in paths %a@.@?" full_file_name
- (Utils.fprintf_list ~sep:", " Format.pp_print_string)
+ (Utils.Format.pp_comma_list Format.pp_print_string)
paths;
raise Not_found
| Some s ->
@@ -130,40 +130,40 @@ let lustrec_options =
"only generates a .lusi interface source file from a Lustre source \
<default: no generation>" );
( "-no-spec",
- Arg.Unit (fun () -> spec := "no"),
+ Arg.Unit (fun () -> spec := SpecNo),
"do not generate any specification" );
( "-acsl-spec",
- Arg.Unit (fun () -> spec := "acsl"),
+ Arg.Unit (fun () -> spec := SpecACSL),
"generates an ACSL encoding of the specification. Only meaningful for \
the C backend <default>" );
( "-c-spec",
- Arg.Unit (fun () -> spec := "c"),
+ Arg.Unit (fun () -> spec := SpecC),
"generates a C encoding of the specification instead of ACSL contracts \
and annotations. Only meaningful for the C backend" );
(* "-java", Arg.Unit (fun () -> output := "java"), "generates Java output
instead of C"; *)
( "-ada",
- Arg.Unit (fun () -> set_backend "Ada"),
+ Arg.Unit (fun () -> set_backend OutAda),
"generates Ada encoding output instead of C" );
( "-horn",
- Arg.Unit (fun () -> set_backend "horn"),
+ Arg.Unit (fun () -> set_backend OutHorn),
"generates Horn clauses encoding output instead of C" );
( "-horn-traces",
Arg.Unit
(fun () ->
- set_backend "horn";
+ set_backend OutHorn;
traces := true),
"produce traceability file for Horn backend. Enable the horn backend." );
( "-horn-cex",
Arg.Unit
(fun () ->
- set_backend "horn";
+ set_backend OutHorn;
horn_cex := true),
"generate cex enumeration. Enable the horn backend (work in progress)" );
( "-horn-query",
Arg.Unit
(fun () ->
- set_backend "horn";
+ set_backend OutHorn;
horn_query := true),
"generate queries in generated Horn file. Enable the horn backend \
(work in progress)" );
@@ -172,10 +172,10 @@ let lustrec_options =
"Gets the endpoint predicate of the \x1b[4msfunction\x1b[0m" );
"-print-reuse", Arg.Set print_reuse, "prints variable reuse policy";
( "-lustre",
- Arg.Unit (fun () -> output := "lustre"),
+ Arg.Unit (fun () -> set_backend OutLustre),
"generates Lustre output, performing all active optimizations" );
( "-emf",
- Arg.Unit (fun () -> set_backend "emf"),
+ Arg.Unit (fun () -> set_backend OutEMF),
"generates EMF output, to be used by CocoSim" );
( "-inline",
Arg.Unit
diff --git a/src/options_management.mli b/src/options_management.mli
new file mode 100644
index 00000000..9447f369
--- /dev/null
+++ b/src/options_management.mli
@@ -0,0 +1,6 @@
+val core_dependency: string -> string
+val plugin_opt: string * (unit -> unit) * (Format.formatter -> unit) *
+ (string * Arg.spec * string) list -> (string * Arg.spec * string) list
+
+val name_dependency: ('a * string) -> string -> string
+val get_witness_dir: string -> string
diff --git a/src/parsers/lexerLustreSpec.mll b/src/parsers/lexerLustreSpec.mll
index b725e36c..795e32fd 100644
--- a/src/parsers/lexerLustreSpec.mll
+++ b/src/parsers/lexerLustreSpec.mll
@@ -15,6 +15,8 @@
open Parser_lustre
open Utils
+ module Lex = MenhirLib.LexerUtil
+
let str_buf = Buffer.create 1024
type error =
@@ -38,7 +40,7 @@ let error lexbuf err =
raise (Error (Location.curr lexbuf, err))
let newline token lexbuf =
- Location.Lex.newline lexbuf;
+ Lex.newline lexbuf;
token lexbuf
(* As advised by Caml documentation. This way a single lexer rule is
diff --git a/src/parsers/lexer_lustre.mll b/src/parsers/lexer_lustre.mll
index f31fe8ff..31c8c507 100644
--- a/src/parsers/lexer_lustre.mll
+++ b/src/parsers/lexer_lustre.mll
@@ -13,6 +13,8 @@
open Parser_lustre
open Utils
+module Lex = MenhirLib.LexerUtil
+
(* As advised by Caml documentation. This way a single lexer rule is
used to handle all the possible keywords. *)
let keyword_table =
@@ -113,7 +115,7 @@ let error lexbuf =
error_with (Location.curr lexbuf)
let newline token lexbuf =
- Location.Lex.newline lexbuf;
+ Lex.newline lexbuf;
token lexbuf
let make_annot orig_loc s =
diff --git a/src/parsers/parse.ml b/src/parsers/parse.ml
index faa1b25b..eadffe6e 100644
--- a/src/parsers/parse.ml
+++ b/src/parsers/parse.ml
@@ -96,7 +96,7 @@ let reparse (module Lexer : LEXER) ?orig_loc filename start src =
(* Expand away the $i keywords that might appear in the message. *)
(* let message = E.expand (get src checkpoint) message in *)
(* Show these three components. *)
- eprintf "@[<v>%aSyntax error %s.@,%s@]@." Location.pp_loc loc indication
+ eprintf "@[<v>%aSyntax error %s.@,%s@]@." Location.pp loc indication
message;
raise Error
in
@@ -113,7 +113,7 @@ let parse (module Lexer : LEXER) ?orig_loc filename src lexbuf start_mono
let loc =
match orig_loc with Some loc' -> Location.shift loc' loc | _ -> loc
in
- eprintf "@[<v>%aSyntax error.@,%a@]@." Location.pp_loc loc Lexer.pp_error
+ eprintf "@[<v>%aSyntax error.@,%a@]@." Location.pp loc Lexer.pp_error
err;
raise Error
| Parser_lustre.Error ->
diff --git a/src/parsers/parse.mli b/src/parsers/parse.mli
new file mode 100644
index 00000000..6d552617
--- /dev/null
+++ b/src/parsers/parse.mli
@@ -0,0 +1,20 @@
+type start_symbol = Header | Program
+
+module type LEXER = sig
+ val token : Lexing.lexbuf -> Parser_lustre.token
+
+ type error
+
+ exception Error of Location.t * error
+
+ val pp_error : Format.formatter -> error -> unit
+end
+
+module Inc: module type of Parser_lustre_table.Incremental
+
+val parse: (module LEXER) -> ?orig_loc:Location.t -> Location.filename -> string ->
+ Lexing.lexbuf ->
+ ((Lexing.lexbuf -> Parser_lustre.token) -> Lexing.lexbuf -> 'a) ->
+ (Lexing.position -> 'b Parser_lustre_table.MenhirInterpreter.checkpoint) -> 'a
+
+val parse_filename: (module LEXER) -> Location.filename -> start_symbol -> Lustre_types.program_t
diff --git a/src/pathConditions.mli b/src/pathConditions.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/plugins/mpfr/lustrec_mpfr.mli b/src/plugins/mpfr/lustrec_mpfr.mli
new file mode 100644
index 00000000..60f43087
--- /dev/null
+++ b/src/plugins/mpfr/lustrec_mpfr.mli
@@ -0,0 +1 @@
+val unfoldable_value: Machine_code_types.value_t -> bool
diff --git a/src/plugins/pluginList.ml b/src/plugins/pluginList.ml
index ad10f547..06d8de15 100644
--- a/src/plugins/pluginList.ml
+++ b/src/plugins/pluginList.ml
@@ -1,3 +1,3 @@
-let registered : (module PluginType.S) list ref = ref []
+let registered = ref []
let plugins () = !registered
diff --git a/src/plugins/pluginList.mli b/src/plugins/pluginList.mli
new file mode 100644
index 00000000..ed6f294e
--- /dev/null
+++ b/src/plugins/pluginList.mli
@@ -0,0 +1,2 @@
+val registered: (module PluginType.S) list ref
+val plugins: unit -> (module PluginType.S) list
diff --git a/src/plugins/pluginType.ml b/src/plugins/pluginType.ml
index 4de83163..a4bd750c 100644
--- a/src/plugins/pluginType.ml
+++ b/src/plugins/pluginType.ml
@@ -23,8 +23,14 @@ module type S = sig
end
module Default = struct
+ let name = "default"
+
+ let activate () = ()
+
let usage fmt = Format.fprintf fmt "No specific help."
+ let options = []
+
let init () = ()
let check_force_stateful () = false
diff --git a/src/plugins/pluginType.mli b/src/plugins/pluginType.mli
new file mode 100644
index 00000000..53c395c5
--- /dev/null
+++ b/src/plugins/pluginType.mli
@@ -0,0 +1,25 @@
+module type S = sig
+ val name : string
+
+ val activate : unit -> unit
+
+ val usage : Format.formatter -> unit
+
+ val options : (string * Arg.spec * string) list
+
+ val init : unit -> unit
+
+ val check_force_stateful : unit -> bool
+
+ val refine_machine_code :
+ Lustre_types.top_decl list ->
+ Machine_code_types.machine_t list ->
+ Machine_code_types.machine_t list
+
+ val c_backend_main_loop_body_prefix :
+ string -> string -> Format.formatter -> unit -> unit
+
+ val c_backend_main_loop_body_suffix : Format.formatter -> unit -> unit
+end
+
+module Default: S
diff --git a/src/plugins/plugins.mli b/src/plugins/plugins.mli
new file mode 100644
index 00000000..093db4ae
--- /dev/null
+++ b/src/plugins/plugins.mli
@@ -0,0 +1,4 @@
+open Utils
+open Lustre_types
+
+val inline_annots: (ident -> ident) -> expr_annot list -> expr_annot list
diff --git a/src/plugins/salsa/machine_salsa_opt.mli b/src/plugins/salsa/machine_salsa_opt.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/plugins/salsa/salsaDatatypes.mli b/src/plugins/salsa/salsaDatatypes.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/plugins/salsa/salsa_plugin.mli b/src/plugins/salsa/salsa_plugin.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/plugins/scopes/scopes.ml b/src/plugins/scopes/scopes.ml
index 9274265c..070aa37c 100644
--- a/src/plugins/scopes/scopes.ml
+++ b/src/plugins/scopes/scopes.ml
@@ -1,3 +1,4 @@
+open Utils
open Lustre_types
open Corelang
open Machine_code_types
@@ -37,7 +38,7 @@ let rec compute_scopes ?(first = true) prog root_node : scope_t list =
(nodeid, vid) :: res
with Not_found ->
Format.eprintf "eq=%a@.local_vars=%a@." Printers.pp_node_eq eq
- (Utils.fprintf_list ~sep:"," Printers.pp_var)
+ (Format.pp_comma_list Printers.pp_var)
local_vars;
assert false)
| Eq _ ->
@@ -58,10 +59,10 @@ let rec compute_scopes ?(first = true) prog root_node : scope_t list =
with Not_found -> []
let print_scopes =
- Utils.fprintf_list ~sep:"@ " (fun fmt ((_, v) as s) ->
- Format.fprintf fmt "%a: %a"
- (Utils.fprintf_list ~sep:"." Format.pp_print_string)
- (scope_to_sl s) Types.print_ty v.var_type)
+ 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)
+ (scope_to_sl s) Types.print_ty v.var_type))
(* let print_path fmt p = *)
(* Utils.fprintf_list ~sep:"." (fun fmt (id, _) -> Format.pp_print_string fmt
@@ -206,7 +207,7 @@ let pp_scopes fmt scopes =
List.iteri
(fun idx (id, (var_path, var)) ->
Format.fprintf fmt "@ %t;" (fun fmt ->
- C_backend_common.print_put_var fmt
+ C_backend_common.pp_put_var fmt
("_scopes" ^ string_of_int (idx + 1))
id (*var*) var.var_type var_path))
scopes_vars
@@ -307,7 +308,7 @@ let option_all_scopes = ref false
(* let option_mems_scopes = ref false
* let option_input_scopes = ref false *)
-let scopes_map : (Lustre_types.ident list * scope_t) list ref = ref []
+let scopes_map : (ident list * scope_t) list ref = ref []
let process_scopes main_node prog machines =
let all_scopes = compute_scopes prog !Options.main_node in
@@ -322,9 +323,9 @@ let process_scopes main_node prog machines =
(fun sl ->
let res = is_valid_path sl main_node prog machines in
if not res then
- Format.eprintf "Scope %a is cancelled due to variable removal@."
- (Utils.fprintf_list ~sep:"." Format.pp_print_string)
- sl;
+ Format.(eprintf "Scope %a is cancelled due to variable removal@."
+ (pp_print_list ~pp_sep:(fun fmt () -> pp_print_string fmt ".") pp_print_string)
+ sl);
res)
selected_scopes
in
diff --git a/src/plugins/scopes/scopes.mli b/src/plugins/scopes/scopes.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/printers.ml b/src/printers.ml
index 09e4f8b3..9cb24356 100644
--- a/src/printers.ml
+++ b/src/printers.ml
@@ -50,13 +50,13 @@ and pp_var_type_dec_desc fmt tdesc =
| Tydec_const t ->
fprintf fmt "%s" t
| Tydec_enum id_list ->
- fprintf fmt "enum {%a }" (fprintf_list ~sep:", " pp_print_string) id_list
+ fprintf fmt "enum {%a }" (pp_comma_list pp_print_string) id_list
| Tydec_struct f_list ->
fprintf fmt "struct {%a }"
- (fprintf_list ~sep:" " pp_var_struct_type_field)
+ (pp_print_list pp_var_struct_type_field)
f_list
| Tydec_array (s, t) ->
- fprintf fmt "%a^%a" pp_var_type_dec_desc t Dimension.pp_dimension s
+ fprintf fmt "%a^%a" pp_var_type_dec_desc t Dimension.pp s
let pp_var_type_dec fmt ty = pp_var_type_dec_desc fmt ty.ty_dec_desc
@@ -68,9 +68,9 @@ let pp_var_type fmt id =
if !Options.print_dec_types then pp_var_type_dec fmt id.var_dec_type
else Types.print_node_ty fmt id.var_type
-let pp_var_clock fmt id = Clocks.print_ck_suffix fmt id.var_clock
+let pp_var_clock fmt id = Clocks.pp_suffix fmt id.var_clock
-let pp_eq_lhs = fprintf_list ~sep:", " pp_print_string
+let pp_eq_lhs = pp_comma_list pp_print_string
let pp_var fmt id =
fprintf fmt "%s%s: %a"
@@ -78,7 +78,7 @@ let pp_var fmt id =
(if !Options.kind2_print then kind2_protect id.var_id else id.var_id)
pp_var_type id
-let pp_vars fmt vars = fprintf_list ~sep:"; " pp_var fmt vars
+let pp_vars fmt vars = pp_print_list ~pp_sep:pp_print_semicolon pp_var fmt vars
let pp_quantifiers fmt (q, vars) =
match q with
@@ -102,9 +102,10 @@ and pp_const fmt c =
| Const_tag t ->
pp_print_string fmt t
| Const_array ca ->
- fprintf fmt "[%a]" (Utils.fprintf_list ~sep:"," pp_const) ca
+ fprintf fmt "[%a]" (pp_print_list ~pp_sep:(fun fmt () -> pp_print_string fmt ",")
+ pp_const) ca
| Const_struct fl ->
- fprintf fmt "{%a }" (Utils.fprintf_list ~sep:" " pp_struct_const_field) fl
+ fprintf fmt "{%a }" (pp_print_list pp_struct_const_field) fl
(* used only for annotations *)
| Const_string s ->
pp_print_string fmt ("\"" ^ s ^ "\"")
@@ -118,7 +119,8 @@ let pp_annot_key fmt kwds =
| [ x ] ->
pp_print_string fmt x
| _ ->
- fprintf fmt "/%a/" (fprintf_list ~sep:"/" pp_print_string) kwds
+ fprintf fmt "/%a/" (pp_print_list ~pp_sep:(fun fmt () -> pp_print_string fmt "/")
+ pp_print_string) kwds
let pp_kind2_when fmt (id, l) =
if l = "true" then fprintf fmt "%s" id
@@ -141,9 +143,9 @@ let rec pp_expr fmt expr =
| Expr_array a ->
fprintf fmt "[%a]" pp_tuple a
| Expr_access (a, d) ->
- fprintf fmt "%a[%a]" pp_expr a Dimension.pp_dimension d
+ fprintf fmt "%a[%a]" pp_expr a Dimension.pp d
| Expr_power (a, d) ->
- fprintf fmt "(%a^%a)" pp_expr a Dimension.pp_dimension d
+ fprintf fmt "(%a^%a)" pp_expr a Dimension.pp d
| Expr_tuple el ->
fprintf fmt "(%a)" pp_tuple el
| Expr_ite (c, t, e) ->
@@ -169,11 +171,12 @@ let rec pp_expr fmt expr =
Format.fprintf fmt "%t: %a" pp Types.print_ty expr.expr_type
else pp fmt)
-and pp_tuple fmt el = fprintf_list ~sep:"," pp_expr fmt el
+and pp_tuple fmt el = pp_print_list ~pp_sep:(fun fmt () -> pp_print_string fmt ",")
+ pp_expr fmt el
and pp_handler fmt (t, h) = fprintf fmt "(%s -> %a)" t pp_expr h
-and pp_handlers fmt hl = fprintf_list ~sep:" " pp_handler fmt hl
+and pp_handlers fmt hl = pp_print_list pp_handler fmt hl
and pp_app fmt id e r =
if !Options.kind2_print && not (List.mem id Basic_library.internal_funs) then
@@ -273,7 +276,7 @@ and pp_call fmt id e =
and pp_eexpr fmt e =
fprintf fmt "%a%t %a"
- (Utils.fprintf_list ~sep:"; " pp_quantifiers)
+ (pp_print_list ~pp_sep:pp_print_semicolon pp_quantifiers)
e.eexpr_quantifiers
(fun fmt ->
match e.eexpr_quantifiers with [] -> () | _ -> fprintf fmt ";")
@@ -297,22 +300,23 @@ and pp_s_function fmt expr_ann =
| [ x ] ->
pp_print_string fmt x
| _ ->
- fprintf fmt "%a" (fprintf_list ~sep:"/" pp_print_string) kwds)
+ fprintf fmt "%a" (pp_print_list ~pp_sep:(fun fmt () -> pp_print_string fmt "/")
+ pp_print_string) kwds)
pp_sf_value ee
in
- fprintf_list ~sep:"@ " pp_annot fmt expr_ann.annots
+ pp_print_list pp_annot fmt expr_ann.annots
and pp_expr_annot fmt expr_ann =
let pp_annot fmt (kwds, ee) =
fprintf fmt "(*!%a: %a; *)" pp_annot_key kwds pp_eexpr ee
in
- fprintf_list ~sep:"@ " pp_annot fmt expr_ann.annots
+ pp_print_list pp_annot fmt expr_ann.annots
let pp_asserts fmt asserts =
match asserts with
| _ :: _ ->
fprintf fmt "(* Asserts definitions *)@ ";
- fprintf_list ~sep:"@ "
+ pp_print_list
(fun fmt assert_ ->
let expr = assert_.assert_expr in
fprintf fmt "assert %a;" pp_expr expr)
@@ -334,7 +338,7 @@ let pp_node_var fmt id =
| Some v ->
fprintf fmt " = %a" pp_expr v
-let pp_node_args = fprintf_list ~sep:";@ " pp_node_var
+let pp_node_args = pp_print_list ~pp_sep:pp_print_semicolon pp_node_var
let pp_node_eq fmt eq =
fprintf fmt "%a = %a;" pp_eq_lhs eq.eq_lhs pp_expr eq.eq_rhs
@@ -351,7 +355,7 @@ let pp_until fmt (_, expr, restart, st) =
let rec pp_handler fmt handler =
fprintf fmt "state %s:@ @[<v 2> %a%t%alet@,@[<v 2> %a@ %a@ %a@]@,tel@ %a@]"
handler.hand_state
- (Utils.fprintf_list ~sep:"@ " pp_unless)
+ (pp_print_list pp_unless)
handler.hand_unless
(fun fmt -> if not ([] = handler.hand_unless) then fprintf fmt "@ ")
(fun fmt locals ->
@@ -360,14 +364,13 @@ let rec pp_handler fmt handler =
()
| _ ->
fprintf fmt "@[<v 4>var %a@]@ "
- (Utils.fprintf_list ~sep:"@ " (fun fmt v ->
- fprintf fmt "%a;" pp_node_var v))
+ (pp_print_list ~pp_sep:pp_print_semicolon pp_node_var)
locals)
handler.hand_locals
- (fprintf_list ~sep:"@ " pp_expr_annot)
+ (pp_print_list pp_expr_annot)
handler.hand_annots pp_node_stmts handler.hand_stmts pp_asserts
handler.hand_asserts
- (Utils.fprintf_list ~sep:"@," pp_until)
+ (pp_print_list pp_until)
handler.hand_until
and pp_node_stmt fmt stmt =
@@ -379,10 +382,10 @@ and pp_node_stmts fmt stmts =
and pp_node_aut fmt aut =
fprintf fmt "@[<v 0>automaton %s@,%a@]" aut.aut_id
- (Utils.fprintf_list ~sep:"@ " pp_handler)
+ (pp_print_list pp_handler)
aut.aut_handlers
-and pp_node_eqs fmt eqs = fprintf_list ~sep:"@ " pp_node_eq fmt eqs
+and pp_node_eqs fmt eqs = pp_print_list pp_node_eq fmt eqs
let pp_typedef fmt ty =
fprintf fmt "type %s = %a;" ty.tydef_id pp_var_type_dec_desc ty.tydef_desc
@@ -420,7 +423,7 @@ let pp_spec_stmt fmt stmt =
let pp_spec fmt spec =
(* const are prefixed with const in pp_var and with nothing for regular
variables. We adapt the call to produce the appropriate output. *)
- fprintf_list ~eol:"@, " ~sep:"@, "
+ pp_print_list
(fun fmt v ->
fprintf fmt "%a = %t;" pp_var v (fun fmt ->
match v.var_dec_value with
@@ -430,26 +433,26 @@ let pp_spec fmt spec =
pp_expr fmt e))
fmt spec.consts;
- fprintf_list ~eol:"@, " ~sep:"@, "
+ pp_print_list
(fun fmt s -> pp_spec_stmt fmt s)
fmt spec.stmts;
- fprintf_list ~eol:"@, " ~sep:"@, "
+ pp_print_list
(fun fmt r -> fprintf fmt "assume %a;" pp_eexpr r)
fmt spec.assume;
- fprintf_list ~eol:"@, " ~sep:"@, "
+ pp_print_list
(fun fmt r -> fprintf fmt "guarantee %a;" pp_eexpr r)
fmt spec.guarantees;
- fprintf_list ~eol:"@, " ~sep:"@, "
+ pp_print_list
(fun fmt mode ->
fprintf fmt "mode %s (@[<v 0>%a@ %a@]);" mode.mode_id
- (fprintf_list ~eol:"" ~sep:"@ " (fun fmt r ->
+ (pp_print_list (fun fmt r ->
fprintf fmt "require %a;" pp_eexpr r))
mode.require
- (fprintf_list ~eol:"" ~sep:"@ " (fun fmt r ->
+ (pp_print_list (fun fmt r ->
fprintf fmt "ensure %a;" pp_eexpr r))
mode.ensure)
fmt spec.modes;
- fprintf_list ~eol:"@, " ~sep:"@, "
+ pp_print_list
(fun fmt import ->
fprintf fmt "import %s (%a) returns (%a);" import.import_nodeid pp_expr
import.inputs pp_expr import.outputs)
@@ -495,7 +498,7 @@ let pp_spec_as_comment fmt (inl, outl, spec) =
| NodeSpec name ->
(* Pushing stmts in contract. We update the original information with the
computed one in nd. *)
- let pp_l = fprintf_list ~sep:"," pp_var_name in
+ let pp_l = pp_comma_list pp_var_name in
fprintf fmt "@[<hov 2>(*@contract import %s(%a) returns (%a); @]*)@ " name
pp_l inl pp_l outl
@@ -526,7 +529,7 @@ let pp_node fmt nd =
()
| _ ->
fprintf fmt "@[<v 4>var %a@]@ "
- (fprintf_list ~sep:"@ " (fun fmt v -> fprintf fmt "%a;" pp_node_var v))
+ (pp_print_list (fun fmt v -> fprintf fmt "%a;" pp_node_var v))
locals)
nd.node_locals;
(* Checks *)
@@ -537,14 +540,14 @@ let pp_node fmt nd =
()
| _ ->
fprintf fmt "@[<v 4>check@ %a@]@ "
- (fprintf_list ~sep:"@ " (fun fmt d ->
- fprintf fmt "%a" Dimension.pp_dimension d))
+ (pp_print_list (fun fmt d ->
+ fprintf fmt "%a" Dimension.pp d))
checks)
nd.node_checks;
(* Body *)
fprintf fmt "@[<v 2>let@ ";
(* Annotations *)
- fprintf fmt "%a" (fprintf_list ~sep:"@ " pp_expr_annot) nd.node_annot;
+ fprintf fmt "%a" (pp_print_list pp_expr_annot) nd.node_annot;
(* Statements *)
fprintf fmt "%a" pp_node_stmts nd.node_stmts;
(* Asserts *)
@@ -589,7 +592,7 @@ let pp_const_decl fmt cdecl =
fprintf fmt "%s = %a;" cdecl.const_id pp_const cdecl.const_value
let pp_const_decl_list fmt clist =
- fprintf_list ~sep:"@ " pp_const_decl fmt clist
+ pp_print_list pp_const_decl fmt clist
let pp_decl fmt decl =
match decl.top_decl_desc with
@@ -676,13 +679,13 @@ let pp_lusi_header fmt basename prog =
let pp_offset fmt offset =
match offset with
| Index i ->
- fprintf fmt "[%a]" Dimension.pp_dimension i
+ fprintf fmt "[%a]" Dimension.pp i
| Field f ->
fprintf fmt ".%s" f
let pp_node_list fmt prog =
Format.fprintf fmt "@[<h 2>%a@]"
- (fprintf_list ~sep:"@ " (fun fmt decl ->
+ (pp_print_list (fun fmt decl ->
match decl.top_decl_desc with
| Node nd ->
Format.fprintf fmt "%s" nd.node_id
diff --git a/src/printers.mli b/src/printers.mli
new file mode 100644
index 00000000..6d4f55c4
--- /dev/null
+++ b/src/printers.mli
@@ -0,0 +1,17 @@
+open Format
+open Lustre_types
+
+val pp_expr: formatter -> expr -> unit
+val pp_eexpr: formatter -> eexpr -> unit
+val pp_node: formatter -> node_desc -> unit
+val pp_const: formatter -> constant -> unit
+val pp_var: formatter -> var_decl -> unit
+val pp_node_eq: formatter -> eq -> unit
+val pp_node_eqs: formatter -> eq list -> unit
+val pp_spec: formatter -> contract_desc -> unit
+val pp_expr_annot: formatter -> expr_annot -> unit
+val pp_short_decl: formatter -> top_decl -> unit
+val pp_const_decl: formatter -> const_desc -> unit
+val pp_var_type_dec_desc: formatter -> type_dec_desc -> unit
+val pp_typedef: formatter -> typedef_desc -> unit
+val pp_prog: formatter -> program_t -> unit
diff --git a/src/scheduling.ml b/src/scheduling.ml
index ef862735..7fd6ed10 100644
--- a/src/scheduling.ml
+++ b/src/scheduling.ml
@@ -177,10 +177,10 @@ let pp_eq_schedule fmt vl =
| [] ->
assert false
| [ v ] ->
- Format.fprintf fmt "%s" v
+ Format.pp_print_string fmt v
| _ ->
Format.fprintf fmt "(%a)"
- (fprintf_list ~sep:" , " (fun fmt v -> Format.fprintf fmt "%s" v))
+ (Format.pp_comma_list Format.pp_print_string)
vl
let pp_schedule fmt node_schs =
@@ -223,7 +223,7 @@ let pp_warning_unused fmt node_schs =
if vu.var_orig then
Format.fprintf fmt
" Warning: variable '%s' seems unused@, %a@,@," u
- Location.pp_loc vu.var_loc)
+ Location.pp vu.var_loc)
unused)
node_schs
@@ -266,7 +266,7 @@ let sort_equations_from_schedule eqs sch =
in
Log.report ~level:1 (fun fmt ->
Format.fprintf fmt "[Warning] Unused variables: %a@ "
- (fprintf_list ~sep:", " Format.pp_print_string)
+ (Format.pp_comma_list Format.pp_print_string)
vars);
vars)
else []
diff --git a/src/scheduling.mli b/src/scheduling.mli
new file mode 100644
index 00000000..8d7a6128
--- /dev/null
+++ b/src/scheduling.mli
@@ -0,0 +1,9 @@
+open Utils
+open Lustre_types
+open Scheduling_type
+
+val schedule_prog: program_t -> program_t * schedule_report IMap.t
+val remove_prog_inlined_locals: 'a IMap.t IMap.t -> schedule_report IMap.t -> schedule_report IMap.t
+val compute_prog_reuse_table: schedule_report IMap.t -> (ident, var_decl) Hashtbl.t IMap.t
+
+val sort_equations_from_schedule: eq list -> ident list list -> eq list * ident list
diff --git a/src/scheduling_type.ml b/src/scheduling_type.mli
similarity index 100%
rename from src/scheduling_type.ml
rename to src/scheduling_type.mli
diff --git a/src/sortProg.ml b/src/sortProg.ml
index f46e793a..29f8ad94 100644
--- a/src/sortProg.ml
+++ b/src/sortProg.ml
@@ -50,19 +50,18 @@ let sort prog =
Log.report ~level:3 (fun fmt ->
Format.fprintf fmt "@ @[<v 2>.. ordered list of declarations:@ %a@]@ "
- (Utils.fprintf_list ~sep:"@ " Printers.pp_short_decl)
- sorted);
+ (Format.pp_print_list Printers.pp_short_decl) sorted);
not_nodes @ sorted
-let sort_node_locals nd =
- { nd with node_locals = Causality.VarClockDep.sort nd.node_locals }
-
let sort_nodes_locals prog =
List.map
(fun top ->
match top.top_decl_desc with
| Node nd ->
- { top with top_decl_desc = Node (sort_node_locals nd) }
+ { top with
+ top_decl_desc = Node
+ { nd with
+ node_locals = Causality.VarClockDep.sort nd.node_locals }}
| _ ->
top)
prog
diff --git a/src/sortProg.mli b/src/sortProg.mli
new file mode 100644
index 00000000..0e614642
--- /dev/null
+++ b/src/sortProg.mli
@@ -0,0 +1,4 @@
+open Lustre_types
+
+val sort_nodes_locals: program_t -> program_t
+val sort: program_t -> program_t
diff --git a/src/spec.mli b/src/spec.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/spec_common.mli b/src/spec_common.mli
new file mode 100644
index 00000000..5d285ca5
--- /dev/null
+++ b/src/spec_common.mli
@@ -0,0 +1,19 @@
+open Utils
+open Lustre_types
+open Spec_types
+
+val mk_conditional_tr: 'a -> 'a formula_t -> 'a formula_t -> 'a formula_t
+
+val mk_branch_tr: var_decl -> (ident * 'a formula_t) list -> 'a formula_t
+
+val mk_assign_tr: var_decl -> 'a -> 'a formula_t
+
+val mk_memory_pack: ?i:int -> ?inst:ident -> ident -> 'a formula_t
+
+val mk_transition: ?mems:ISet.t -> ?insts:ident IMap.t -> ?r:'a -> ?i:int -> ?inst:ident -> ident -> 'a list -> 'a formula_t
+
+val mk_state_variable_pack: var_decl -> 'a formula_t
+
+val mk_state_assign_tr: var_decl -> 'a -> 'a formula_t
+
+val red: 'a formula_t -> 'a formula_t
diff --git a/src/spec_types.ml b/src/spec_types.ml
index fc3dfeed..4980309b 100644
--- a/src/spec_types.ml
+++ b/src/spec_types.ml
@@ -1,3 +1,4 @@
+open Utils
open Lustre_types
type register_t = ResetFlag | StateVar of var_decl
@@ -13,7 +14,7 @@ type ('a, _) expression_t =
| Memory : register_t -> ('a, left_v) expression_t
(** TODO: why moving this elsewhere makes the exhaustiveness check fail? *)
-let type_of_l_value : type a. (a, left_v) expression_t -> Types.type_expr =
+let type_of_l_value : type a. (a, left_v) expression_t -> Types.t =
function
| Var v ->
v.var_type
diff --git a/src/spec_types.mli b/src/spec_types.mli
new file mode 100644
index 00000000..8301141d
--- /dev/null
+++ b/src/spec_types.mli
@@ -0,0 +1,66 @@
+open Utils
+open Lustre_types
+
+type register_t = ResetFlag | StateVar of var_decl
+
+type left_v
+
+type right_v
+
+type ('a, _) expression_t =
+ | Val : 'a -> ('a, right_v) expression_t
+ | Tag : ident -> ('a, right_v) expression_t
+ | Var : var_decl -> ('a, left_v) expression_t
+ | Memory : register_t -> ('a, left_v) expression_t
+
+val type_of_l_value: ('a, left_v) expression_t -> Types.t
+
+type 'a predicate_t =
+ | Transition :
+ ident (* node name *)
+ * ident option
+ (* instance *)
+ * int option
+ (* transition index *)
+ * ('a, 'b) expression_t list
+ (* variables *)
+ * bool (* reset *)
+ * Utils.ISet.t (* memory footprint *)
+ * ident Utils.IMap.t
+ (* memory instances footprint *)
+ -> 'a predicate_t
+ | Reset of ident * ident * 'a
+ | MemoryPack of ident * ident option * int option
+ | Initialization
+ | ResetCleared of ident
+
+type 'a formula_t =
+ | True
+ | False
+ | Equal : ('a, left_v) expression_t * ('a, 'b) expression_t -> 'a formula_t
+ | And of 'a formula_t list
+ | Or of 'a formula_t list
+ | Imply of 'a formula_t * 'a formula_t
+ | Exists of var_decl list * 'a formula_t
+ | Forall of var_decl list * 'a formula_t
+ | Ternary :
+ ('a, 'b) expression_t * 'a formula_t * 'a formula_t
+ -> 'a formula_t
+ | Predicate : 'a predicate_t -> 'a formula_t
+ | StateVarPack of register_t
+ | ExistsMem of ident * 'a formula_t * 'a formula_t
+
+type 'a transition_t = {
+ tname : node_desc;
+ tindex : int option;
+ tvars : var_decl list;
+ tformula : 'a formula_t;
+ tmem_footprint : Utils.ISet.t;
+ tinst_footprint : ident Utils.IMap.t;
+}
+
+type 'a memory_pack_t = {
+ mpname : node_desc;
+ mpindex : int option;
+ mpformula : 'a formula_t;
+}
diff --git a/src/splitting.mli b/src/splitting.mli
new file mode 100644
index 00000000..96c139b4
--- /dev/null
+++ b/src/splitting.mli
@@ -0,0 +1,5 @@
+open Lustre_types
+
+val tuple_split_eq: eq -> eq list
+
+val tuple_split_eq_list: eq list -> eq list
diff --git a/src/tools/importer/main_lustre_importer.mli b/src/tools/importer/main_lustre_importer.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/tools/importer/vhdl_deriving_yojson.mli b/src/tools/importer/vhdl_deriving_yojson.mli
new file mode 100644
index 00000000..7825694d
--- /dev/null
+++ b/src/tools/importer/vhdl_deriving_yojson.mli
@@ -0,0 +1,294 @@
+type vhdl_type_t =
+ | Base of string
+ | Range of string option * int * int [@name "RANGE_WITH_DIRECTION"]
+ | Bit_vector of int * int
+ | Array of int * int * vhdl_type_t
+ | Enumerated of string list
+ | Void
+[@@deriving yojson]
+
+(************************************************************************************)
+(* Constants *)
+(************************************************************************************)
+
+(* TODO: do we need more constructors ? *)
+type cst_val_t =
+ | CstInt of int
+ | CstStdLogic of string
+ | CstLiteral of string [@name "CST_LITERAL"]
+[@@deriving yojson { strict = false }]
+
+type vhdl_subtype_indication_t = {
+ name : string;
+ definition : vhdl_type_t option; [@default Some Void]
+}
+[@@deriving yojson { strict = false }]
+
+(* TODO ? Shall we merge definition / declaration *)
+type vhdl_definition_t =
+ | Type of { name : string; definition : vhdl_type_t }
+ [@name "TYPE_DECLARATION"]
+ | Subtype of { name : string; typ : vhdl_subtype_indication_t }
+ [@name "SUBTYPE_DECLARATION"]
+[@@deriving yojson { strict = false }]
+
+type vhdl_declaration_t =
+ | VarDecl of {
+ names : string list;
+ typ : vhdl_subtype_indication_t;
+ init_val : cst_val_t option; [@default Some (CstInt 0)]
+ } [@name "VARIABLE_DECLARATION"]
+ | CstDecl of {
+ names : string list;
+ typ : vhdl_subtype_indication_t;
+ init_val : cst_val_t;
+ } [@name "CONSTANT_DECLARATION"]
+ | SigDecl of {
+ names : string list;
+ typ : vhdl_subtype_indication_t;
+ init_val : cst_val_t option; [@default Some (CstInt 0)]
+ } [@name "SIGNAL_DECLARATION"]
+[@@deriving yojson { strict = false }]
+
+(************************************************************************************)
+(* Attributes for types, arrays, signals and strings *)
+(************************************************************************************)
+
+type 'basetype vhdl_type_attributes_t =
+ | TAttNoArg of { id : string }
+ | TAttIntArg of { id : string; arg : int }
+ | TAttValArg of { id : string; arg : 'basetype }
+ | TAttStringArg of { id : string; arg : string }
+[@@deriving yojson { strict = false }]
+
+type vhdl_array_attributes_t =
+ | AAttInt of { id : string; arg : int }
+ | AAttAscending
+[@@deriving yojson { strict = false }]
+
+type vhdl_signal_attributes_t = SigAtt of string
+[@@deriving yojson { strict = false }]
+
+type vhdl_string_attributes_t = StringAtt of string
+[@@deriving yojson { strict = false }]
+
+(************************************************************************************)
+(* Expressions / Statements *)
+(************************************************************************************)
+type suffix_selection_t = Idx of int | Range of int * int
+[@@deriving yojson { strict = false }]
+
+type vhdl_expr_t =
+ | Call of vhdl_name_t [@name "CALL"]
+ | Cst of cst_val_t [@name "CONSTANT_VALUE"]
+ | Op of { id : string; [@default ""] args : vhdl_expr_t list [@default []] }
+ [@name "EXPRESSION"]
+ | IsNull [@name "IsNull"]
+ | Time of { value : int; phy_unit : string [@default ""] }
+ | Sig of { name : string; att : vhdl_signal_attributes_t option }
+ | SuffixMod of { expr : vhdl_expr_t; selection : suffix_selection_t }
+[@@deriving yojson { strict = false }]
+
+and vhdl_name_t =
+ | Simple of string [@name "SIMPLE_NAME"]
+ | Selected of vhdl_name_t list [@name "SELECTED_NAME"]
+ | Index of { id : vhdl_name_t; exprs : vhdl_expr_t list }
+ [@name "INDEXED_NAME"]
+ | Slice of { id : vhdl_name_t; range : vhdl_type_t } [@name "SLICE_NAME"]
+ | Attribute of {
+ id : vhdl_name_t;
+ designator : vhdl_name_t;
+ expr : vhdl_expr_t; [@default IsNull]
+ } [@name "ATTRIBUTE_NAME"]
+ | Function of { id : vhdl_name_t; assoc_list : vhdl_assoc_element_t list }
+ [@name "FUNCTION_CALL"]
+ | NoName
+[@@deriving yojson { strict = false }]
+
+and vhdl_assoc_element_t = {
+ formal_name : vhdl_name_t option; [@default Some NoName]
+ formal_arg : vhdl_name_t option; [@default Some NoName]
+ actual_name : vhdl_name_t option; [@default Some NoName]
+ actual_designator : vhdl_name_t option; [@default Some NoName]
+ actual_expr : vhdl_expr_t option; [@default Some IsNull]
+}
+[@@deriving yojson { strict = false }]
+
+type vhdl_sequential_stmt_t =
+ | VarAssign of { lhs : vhdl_name_t; rhs : vhdl_expr_t }
+ | SigSeqAssign of {
+ label : string; [@default ""]
+ lhs : vhdl_name_t;
+ rhs : vhdl_expr_t list;
+ } [@name "SIGNAL_ASSIGNMENT_STATEMENT"]
+ | If of {
+ label : string; [@default ""]
+ if_cases : vhdl_if_case_t list;
+ default : vhdl_sequential_stmt_t list; [@default []]
+ } [@name "IF_STATEMENT"]
+ | Case of { guard : vhdl_expr_t; branches : vhdl_case_item_t list }
+ [@name "CASE_STATEMENT_TREE"]
+ | Exit of {
+ label : string; [@default ""]
+ loop_label : string option; [@default Some ""]
+ condition : vhdl_expr_t option; [@default Some IsNull]
+ } [@name "EXIT_STATEMENT"]
+ | Assert of {
+ label : string; [@default ""]
+ cond : vhdl_expr_t;
+ report : vhdl_expr_t; [@default IsNull]
+ severity : vhdl_expr_t; [@default IsNull]
+ } [@name "ASSERTION_STATEMENT"]
+ | Wait [@name "WAIT_STATEMENT"]
+ | Null of { label : string [@default ""] } [@name "NULL_STATEMENT"]
+
+and vhdl_if_case_t = {
+ if_cond : vhdl_expr_t;
+ if_block : vhdl_sequential_stmt_t list;
+}
+
+and vhdl_case_item_t = {
+ when_cond : vhdl_expr_t list;
+ when_stmt : vhdl_sequential_stmt_t list;
+}
+[@@deriving yojson { strict = false }]
+
+type signal_condition_t = {
+ expr : vhdl_expr_t list;
+ (* when expression *)
+ cond : vhdl_expr_t; [@default IsNull]
+ (* optional else case expression. If None, could be a latch *)
+}
+[@@deriving yojson { strict = false }]
+
+type signal_selection_t = {
+ expr : vhdl_expr_t;
+ when_sel : vhdl_expr_t list; [@default []]
+}
+[@@deriving yojson { strict = false }]
+
+type conditional_signal_t = {
+ postponed : bool; [@default false]
+ label : string option; [@default Some ""]
+ lhs : vhdl_name_t;
+ (* assigned signal = target*)
+ rhs : signal_condition_t list;
+ (* expression *)
+ cond : vhdl_expr_t; [@default IsNull]
+ delay : vhdl_expr_t; [@default IsNull]
+}
+[@@deriving yojson { strict = false }]
+
+type process_t = {
+ id : string option; [@default Some ""]
+ declarations : vhdl_declaration_t list option;
+ [@key "PROCESS_DECLARATIVE_PART"] [@default Some []]
+ active_sigs : vhdl_name_t list; [@default []]
+ body : vhdl_sequential_stmt_t list;
+ [@key "PROCESS_STATEMENT_PART"] [@default []]
+}
+[@@deriving yojson { strict = false }]
+
+type selected_signal_t = {
+ postponed : bool; [@default false]
+ label : string option; [@default Some ""]
+ lhs : vhdl_name_t;
+ (* assigned signal = target *)
+ sel : vhdl_expr_t;
+ branches : signal_selection_t list; [@default []]
+ delay : vhdl_expr_t option;
+}
+[@@deriving yojson { strict = false }]
+
+type vhdl_concurrent_stmt_t =
+ | SigAssign of conditional_signal_t [@name "CONDITIONAL_SIGNAL_ASSIGNMENT"]
+ | Process of process_t [@name "PROCESS_STATEMENT"]
+ | SelectedSig of selected_signal_t [@name "SELECTED_SIGNAL_ASSIGNMENT"]
+[@@deriving yojson { strict = false }]
+
+(* type vhdl_statement_t =
+
+ (* | DeclarationStmt of declaration_stmt_t *) | ConcurrentStmt of
+ vhdl_concurrent_stmt_t | SequentialStmt of vhdl_sequential_stmt_t *)
+
+(************************************************************************************)
+(* Entities *)
+(************************************************************************************)
+
+(* TODO? Seems to appear optionally in entities *)
+type vhdl_generic_t = unit [@@deriving yojson { strict = false }]
+
+type vhdl_port_kind_t =
+ | InPort [@name "in"]
+ | OutPort [@name "out"]
+ | InoutPort [@name "inout"]
+ | BufferPort [@name "buffer"]
+[@@deriving yojson]
+
+type vhdl_port_t = {
+ names : string list; [@default []]
+ kind : vhdl_port_kind_t;
+ typ : string; (* typ: vhdl_type_t; *)
+}
+[@@deriving yojson { strict = false }]
+
+type vhdl_entity_t = {
+ name : string; [@default ""]
+ generics : vhdl_generic_t list option;
+ [@key "GENERIC_CLAUSE"] [@default Some []]
+ ports : vhdl_port_t list; [@key "PORT_CLAUSE"] [@default []]
+}
+[@@deriving yojson { strict = false }]
+
+(************************************************************************************)
+(* Packages / Library loading *)
+(************************************************************************************)
+
+(* Optional. Describes shared definitions *)
+type vhdl_package_t = {
+ name : string; [@default ""]
+ shared_defs : vhdl_definition_t list; [@default []]
+}
+[@@deriving yojson { strict = false }]
+
+type vhdl_load_t =
+ | Library of string list [@name "LIBRARY_CLAUSE"] [@default ""]
+ | Use of string list [@name "USE_CLAUSE"] [@default []]
+[@@deriving yojson]
+
+(************************************************************************************)
+(* Architecture / VHDL Design *)
+(************************************************************************************)
+
+type vhdl_architecture_t = {
+ name : string; [@default ""]
+ entity : string; [@default ""]
+ declarations : vhdl_declaration_t list option;
+ [@key "ARCHITECTURE_DECLARATIVE_PART"] [@default Some []]
+ body : vhdl_concurrent_stmt_t list option;
+ [@key "ARCHITECTURE_STATEMENT_PART"] [@default Some []]
+}
+[@@deriving yojson { strict = false }]
+
+(* TODO. Configuration is optional *)
+type vhdl_configuration_t = unit [@@deriving yojson { strict = false }]
+
+type vhdl_design_t = {
+ packages : vhdl_package_t list; [@key "PACKAGE_DECLARATION"] [@default []]
+ libraries : vhdl_load_t list option;
+ [@key "CONTEXT_CLAUSE"] [@default Some []]
+ entities : vhdl_entity_t list; [@key "ENTITY_DECLARATION"] [@default []]
+ architectures : vhdl_architecture_t list;
+ [@key "ARCHITECTURE_BODY"] [@default []]
+ configuration : vhdl_configuration_t option;
+ [@key "CONFIGURATION_DECLARATION"] [@default Some ()]
+}
+[@@deriving yojson { strict = false }]
+
+type vhdl_design_file_t = {
+ design_unit : vhdl_design_t list; [@key "DESIGN_UNIT"] [@default []]
+}
+[@@deriving yojson { strict = false }]
+
+type vhdl_file_t = { design_file : vhdl_design_file_t [@key "DESIGN_FILE"] }
+[@@deriving yojson]
diff --git a/src/tools/importer/vhdl_json_lib.mli b/src/tools/importer/vhdl_json_lib.mli
new file mode 100644
index 00000000..f5f59f9a
--- /dev/null
+++ b/src/tools/importer/vhdl_json_lib.mli
@@ -0,0 +1,8 @@
+open Yojson.Safe
+
+val prune_str: string -> t -> t
+val prune_null_assoc: t -> t
+val to_list_content_str: string -> t -> t
+val flatten_ivd: t -> t
+val flatten_numeric_literal: t -> t
+val to_list_str: string -> t -> t
diff --git a/src/tools/seal/seal_export.mli b/src/tools/seal/seal_export.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/tools/seal/seal_extract.mli b/src/tools/seal/seal_extract.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/tools/seal/seal_slice.mli b/src/tools/seal/seal_slice.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/tools/seal/seal_utils.mli b/src/tools/seal/seal_utils.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/tools/seal/seal_verifier.mli b/src/tools/seal/seal_verifier.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/tools/stateflow/sf_sem.mli b/src/tools/stateflow/sf_sem.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/tools/tiny/tiny_utils.mli b/src/tools/tiny/tiny_utils.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/tools/tiny/tiny_verifier.mli b/src/tools/tiny/tiny_verifier.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/tools/zustre/zustre_analyze.mli b/src/tools/zustre/zustre_analyze.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/tools/zustre/zustre_cex.mli b/src/tools/zustre/zustre_cex.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/tools/zustre/zustre_common.mli b/src/tools/zustre/zustre_common.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/tools/zustre/zustre_data.mli b/src/tools/zustre/zustre_data.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/tools/zustre/zustre_test.mli b/src/tools/zustre/zustre_test.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/tools/zustre/zustre_verifier.mli b/src/tools/zustre/zustre_verifier.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/type_predef.ml b/src/type_predef.ml
index c550c963..9cb281ba 100644
--- a/src/type_predef.ml
+++ b/src/type_predef.ml
@@ -74,13 +74,13 @@ module Make (T : Types.S) = struct
type_arrow (type_tuple [ type_bool; univ; univ ]) univ
let type_access =
- let d = Dimension.mkdim Location.dummy_loc Dimension.Dunivar in
- let d' = Dimension.mkdim Location.dummy_loc Dimension.Dunivar in
+ let d = Dimension.mkdim Location.dummy Dimension.Dunivar in
+ let d' = Dimension.mkdim Location.dummy Dimension.Dunivar in
let univ = new_univar () in
type_arrow (type_tuple [ type_array d univ; type_static d' type_int ]) univ
let type_power =
- let d = Dimension.mkdim Location.dummy_loc Dimension.Dunivar in
+ let d = Dimension.mkdim Location.dummy Dimension.Dunivar in
let univ = new_univar () in
type_arrow (type_tuple [ univ; type_static d type_int ]) (type_array d univ)
end
@@ -93,7 +93,7 @@ end
(* let type_string_builder = Tbasic Basic.Tstring *)
(* end *)
-module Main = Make (Types.Main)
+module Main = Make (Types)
include Main
(* Local Variables: *)
diff --git a/src/type_predef.mli b/src/type_predef.mli
new file mode 100644
index 00000000..a8d57a57
--- /dev/null
+++ b/src/type_predef.mli
@@ -0,0 +1,32 @@
+open Utils
+(* open Types *)
+
+module Make(T: Types.S) : sig
+ (* see https://stackoverflow.com/a/37307124 *)
+ include module type of struct include T end
+ val type_int: t
+ val type_real: t
+ val type_bool: t
+ val type_string: t
+ val type_clock: t -> t
+ val type_const: ident -> t
+ val type_enum: ident list -> t
+ val type_struct: (ident * t) list -> t
+ val type_arrow: t -> t -> t
+ val type_array: Dimension.t -> t -> t
+ val type_static: Dimension.t -> t -> t
+end
+
+(* include Types.S *)
+val type_int: Types.t
+val type_bool: Types.t
+val type_real: Types.t
+val type_const: ident -> Types.t
+val type_static: Dimension.t -> Types.t -> Types.t
+val type_bin_poly_op: Types.t
+val type_unary_poly_op: Types.t
+val type_bin_int_op: Types.t
+val type_bin_bool_op: Types.t
+val type_bin_comp_op: Types.t
+val type_unary_bool_op: Types.t
+val type_tuple: Types.t list -> Types.t
diff --git a/src/types.ml b/src/types.ml
index f9582629..558b68e6 100644
--- a/src/types.ml
+++ b/src/types.ml
@@ -14,8 +14,6 @@
open Utils
(** Types definitions and a few utility functions on types. *)
-open Dimension
-
module type BASIC_TYPES = sig
type t
@@ -48,7 +46,127 @@ module type BASIC_TYPES = sig
val is_unifiable : t -> t -> bool
end
-module Basic = struct
+module type S = sig
+ module BasicT : BASIC_TYPES
+
+ type basic_type = BasicT.t
+
+ type t = { mutable tdesc: type_desc; tid: int }
+
+ and type_desc =
+ | Tconst of ident
+ (* type constant *)
+ | Tbasic of basic_type
+ | Tclock of t
+ (* A type expression explicitely tagged as carrying a clock *)
+ | Tarrow of t * t
+ | Ttuple of t list
+ | Tenum of ident list
+ | Tstruct of (ident * t) list
+ | Tarray of Dimension.t * t
+ | Tstatic of Dimension.t * t
+ (* a type carried by a dimension expression *)
+ | Tlink of t
+ (* During unification, make links instead of substitutions *)
+ | Tvar
+ (* Monomorphic type variable *)
+ | Tunivar
+ (* Polymorphic type variable *)
+
+ type error =
+ | Unbound_value of ident
+ | Already_bound of ident
+ | Already_defined of ident
+ | Undefined_var of ISet.t
+ | Declared_but_undefined of ident
+ | Unbound_type of ident
+ | Not_a_dimension
+ | Not_a_constant
+ | Assigned_constant of ident
+ | WrongArity of int * int
+ | WrongMorphism of int * int
+ | Type_mismatch of ident
+ | Type_clash of t * t
+ | Poly_imported_node of ident
+
+ exception Unify of t * t
+
+ exception Error of Location.t * error
+
+ val is_real_type : t -> bool
+
+ val is_int_type : t -> bool
+
+ val is_bool_type : t -> bool
+
+ val is_const_type : t -> ident -> bool
+
+ val is_static_type : t -> bool
+
+ val is_array_type : t -> bool
+
+ val is_dimension_type : t -> bool
+
+ val is_address_type : t -> bool
+
+ val is_generic_type : t -> bool
+
+ val print_ty : Format.formatter -> t -> unit
+
+ val repr : t -> t
+
+ val dynamic_type : t -> t
+
+ val type_desc : t -> type_desc
+
+ val new_var : unit -> t
+
+ val new_univar : unit -> t
+
+ val new_ty : type_desc -> t
+
+ val type_int : type_desc
+
+ val type_real : type_desc
+
+ val type_bool : type_desc
+
+ val type_string : type_desc
+
+ val array_element_type : t -> t
+
+ val type_list_of_type : t -> t list
+
+ val print_node_ty : Format.formatter -> t -> unit
+
+ val get_clock_base_type : t -> t option
+
+ val get_static_value : t -> Dimension.t option
+
+ val is_tuple_type : t -> bool
+
+ val type_of_type_list : t list -> t
+
+ val split_arrow : t -> t * t
+
+ val unclock_type : t -> t
+
+ val bottom : t
+
+ val map_tuple_type : (t -> t) -> t -> t
+
+ val array_base_type : t -> t
+
+ val array_type_dimension : t -> Dimension.t
+
+ val pp_error : Format.formatter -> error -> unit
+
+ val struct_field_type : t -> ident -> t
+
+ val array_type_multi_dimension : t -> Dimension.t list
+end
+
+module Basic: BASIC_TYPES = struct
type t = Tstring | Tint | Treal | Tbool | Trat
(* Actually unused for now. Only place where it can appear is in a clock
declaration *)
@@ -101,47 +219,27 @@ module Make (BasicT : BASIC_TYPES) = struct
type basic_type = BasicT.t
- type type_expr = { mutable tdesc : type_desc; tid : int }
+ type t = { mutable tdesc: type_desc; tid: int }
and type_desc =
| Tconst of ident
(* type constant *)
| Tbasic of basic_type
- | Tclock of type_expr
+ | Tclock of t
(* A type expression explicitely tagged as carrying a clock *)
- | Tarrow of type_expr * type_expr
- | Ttuple of type_expr list
+ | Tarrow of t * t
+ | Ttuple of t list
| Tenum of ident list
- | Tstruct of (ident * type_expr) list
- | Tarray of dim_expr * type_expr
- | Tstatic of dim_expr * type_expr
+ | Tstruct of (ident * t) list
+ | Tarray of Dimension.t * t
+ | Tstatic of Dimension.t * t
(* a type carried by a dimension expression *)
- | Tlink of type_expr
+ | Tlink of t
(* During unification, make links instead of substitutions *)
| Tvar
(* Monomorphic type variable *)
| Tunivar
- (* Polymorphic type variable *)
-
- (* {mutable tdesc: type_desc; *)
- (* tid: int} *)
-
- (* and type_desc = *)
- (* | Tconst of ident (\* type constant *\) *)
- (* | Tbasic of BasicT.t *)
- (* | Tclock of type_expr (\* A type expression explicitely tagged as carrying
- a clock *\) *)
- (* | Tarrow of type_expr * type_expr *)
- (* | Ttuple of type_expr list *)
- (* | Tenum of ident list *)
- (* | Tstruct of (ident * type_expr) list *)
- (* | Tarray of dim_expr * type_expr *)
- (* | Tstatic of dim_expr * type_expr (\* a type carried by a dimension
- expression *\) *)
- (* | Tlink of type_expr (\* During unification, make links instead of
- substitutions *\) *)
- (* | Tvar (\* Monomorphic type variable *\) *)
- (* | Tunivar (\* Polymorphic type variable *\) *)
+ (* Polymorphic type variable *)
type error =
| Unbound_value of ident
@@ -156,10 +254,10 @@ module Make (BasicT : BASIC_TYPES) = struct
| WrongArity of int * int
| WrongMorphism of int * int
| Type_mismatch of ident
- | Type_clash of type_expr * type_expr
+ | Type_clash of t * t
| Poly_imported_node of ident
- exception Unify of type_expr * type_expr
+ exception Unify of t * t
exception Error of Location.t * error
@@ -189,17 +287,20 @@ module Make (BasicT : BASIC_TYPES) = struct
| Tarrow (ty1, ty2) ->
fprintf fmt "%a -> %a" print_ty ty1 print_ty ty2
| Ttuple tylist ->
- fprintf fmt "(%a)" (Utils.fprintf_list ~sep:" * " print_ty) tylist
+ fprintf fmt "(%a)"
+ (pp_print_list
+ ~pp_sep:(fun fmt () -> pp_print_string fmt " * ") print_ty) tylist
| Tenum taglist ->
fprintf fmt "enum {%a }"
- (Utils.fprintf_list ~sep:", " pp_print_string)
+ (pp_comma_list pp_print_string)
taglist
| Tstruct fieldlist ->
fprintf fmt "struct {%a }"
- (Utils.fprintf_list ~sep:"; " (print_struct_ty_field pp_basic))
+ (pp_print_list ~pp_sep:pp_print_semicolon
+ (print_struct_ty_field pp_basic))
fieldlist
| Tarray (e, ty) ->
- fprintf fmt "%a^%a" print_ty ty Dimension.pp_dimension e
+ fprintf fmt "%a^%a" print_ty ty Dimension.pp e
| Tlink ty ->
print_ty fmt ty
| Tunivar ->
@@ -227,17 +328,18 @@ module Make (BasicT : BASIC_TYPES) = struct
| Tarrow (ty1, ty2) ->
fprintf fmt "%a -> %a" print_node_ty ty1 print_node_ty ty2
| Ttuple tylist ->
- fprintf fmt "(%a)" (Utils.fprintf_list ~sep:"*" print_node_ty) tylist
+ fprintf fmt "(%a)" (pp_print_list
+ ~pp_sep:(fun fmt () -> pp_print_string fmt "") print_node_ty) tylist
| Tenum taglist ->
fprintf fmt "enum {%a }"
- (Utils.fprintf_list ~sep:", " pp_print_string)
+ (pp_comma_list pp_print_string)
taglist
| Tstruct fieldlist ->
fprintf fmt "struct {%a }"
- (Utils.fprintf_list ~sep:"; " print_node_struct_ty_field)
+ (pp_print_list ~pp_sep:pp_print_semicolon print_node_struct_ty_field)
fieldlist
| Tarray (e, ty) ->
- fprintf fmt "%a^%a" print_node_ty ty Dimension.pp_dimension e
+ fprintf fmt "%a^%a" print_node_ty ty Dimension.pp e
| Tlink ty ->
print_node_ty fmt ty
| Tunivar ->
@@ -267,7 +369,7 @@ module Make (BasicT : BASIC_TYPES) = struct
fprintf fmt "Definition and declaration of type %s don't agree@." id
| Undefined_var vset ->
fprintf fmt "No definition provided for variable(s): %a@."
- (Utils.fprintf_list ~sep:"," pp_print_string)
+ (pp_comma_list pp_print_string)
(ISet.elements vset)
| Declared_but_undefined id ->
fprintf fmt "%s is declared but not defined@." id
@@ -279,7 +381,7 @@ module Make (BasicT : BASIC_TYPES) = struct
let new_id = ref (-1)
- let rec bottom = { tdesc = Tlink bottom; tid = -666 }
+ let rec bottom: t = { tdesc = Tlink bottom; tid = -666 }
let new_ty desc =
incr new_id;
@@ -419,7 +521,7 @@ module Make (BasicT : BASIC_TYPES) = struct
| Tarray (d, _) ->
d
| _ ->
- Format.eprintf "internal error: Types.array_type_dimension %a@." print_ty
+ eprintf "internal error: Types.array_type_dimension %a@." print_ty
ty;
assert false
@@ -435,7 +537,7 @@ module Make (BasicT : BASIC_TYPES) = struct
| Tarray (_, ty') ->
ty'
| _ ->
- Format.eprintf "internal error: Types.array_element_type %a@." print_ty ty;
+ eprintf "internal error: Types.array_element_type %a@." print_ty ty;
assert false
let rec array_base_type ty =
@@ -452,7 +554,7 @@ module Make (BasicT : BASIC_TYPES) = struct
let rec is_generic_type ty =
match (dynamic_type ty).tdesc with
| Tarray (d, ty') ->
- (not (Dimension.is_dimension_const d)) || is_generic_type ty'
+ (not (Dimension.is_const d)) || is_generic_type ty'
| _ ->
false
@@ -467,7 +569,7 @@ module Make (BasicT : BASIC_TYPES) = struct
(* Functions are not first order, I don't think the var case needs to be
considered here *)
| _ ->
- Format.eprintf "type %a is not a map@.Unable to split@.@?" print_ty ty;
+ eprintf "type %a is not a map@.Unable to split@.@?" print_ty ty;
assert false
(** Returns the type corresponding to a type list. *)
@@ -518,132 +620,8 @@ module Make (BasicT : BASIC_TYPES) = struct
let type_string = mk_basic BasicT.type_string_builder
end
-module type S = sig
- module BasicT : BASIC_TYPES
-
- type basic_type = BasicT.t
-
- type type_expr = { mutable tdesc : type_desc; tid : int }
-
- and type_desc =
- | Tconst of ident
- (* type constant *)
- | Tbasic of basic_type
- | Tclock of type_expr
- (* A type expression explicitely tagged as carrying a clock *)
- | Tarrow of type_expr * type_expr
- | Ttuple of type_expr list
- | Tenum of ident list
- | Tstruct of (ident * type_expr) list
- | Tarray of dim_expr * type_expr
- | Tstatic of dim_expr * type_expr
- (* a type carried by a dimension expression *)
- | Tlink of type_expr
- (* During unification, make links instead of substitutions *)
- | Tvar
- (* Monomorphic type variable *)
- | Tunivar
- (* Polymorphic type variable *)
-
- type error =
- | Unbound_value of ident
- | Already_bound of ident
- | Already_defined of ident
- | Undefined_var of ISet.t
- | Declared_but_undefined of ident
- | Unbound_type of ident
- | Not_a_dimension
- | Not_a_constant
- | Assigned_constant of ident
- | WrongArity of int * int
- | WrongMorphism of int * int
- | Type_mismatch of ident
- | Type_clash of type_expr * type_expr
- | Poly_imported_node of ident
-
- exception Unify of type_expr * type_expr
-
- exception Error of Location.t * error
-
- val is_real_type : type_expr -> bool
-
- val is_int_type : type_expr -> bool
-
- val is_bool_type : type_expr -> bool
-
- val is_const_type : type_expr -> ident -> bool
-
- val is_static_type : type_expr -> bool
-
- val is_array_type : type_expr -> bool
-
- val is_dimension_type : type_expr -> bool
-
- val is_address_type : type_expr -> bool
-
- val is_generic_type : type_expr -> bool
-
- val print_ty : Format.formatter -> type_expr -> unit
-
- val repr : type_expr -> type_expr
-
- val dynamic_type : type_expr -> type_expr
-
- val type_desc : type_expr -> type_desc
-
- val new_var : unit -> type_expr
-
- val new_univar : unit -> type_expr
-
- val new_ty : type_desc -> type_expr
-
- val type_int : type_desc
-
- val type_real : type_desc
-
- val type_bool : type_desc
-
- val type_string : type_desc
-
- val array_element_type : type_expr -> type_expr
-
- val type_list_of_type : type_expr -> type_expr list
-
- val print_node_ty : Format.formatter -> type_expr -> unit
-
- val get_clock_base_type : type_expr -> type_expr option
-
- val get_static_value : type_expr -> Dimension.dim_expr option
-
- val is_tuple_type : type_expr -> bool
-
- val type_of_type_list : type_expr list -> type_expr
-
- val split_arrow : type_expr -> type_expr * type_expr
-
- val unclock_type : type_expr -> type_expr
-
- val bottom : type_expr
-
- val map_tuple_type : (type_expr -> type_expr) -> type_expr -> type_expr
-
- val array_base_type : type_expr -> type_expr
-
- val array_type_dimension : type_expr -> Dimension.dim_expr
-
- val pp_error : Format.formatter -> error -> unit
-
- val struct_field_type : type_expr -> ident -> type_expr
-
- val array_type_multi_dimension : type_expr -> Dimension.dim_expr list
-end
-(* with type type_expr = BasicT.t type_expr_gen *)
-
-module type Sbasic = S with type BasicT.t = Basic.t
-
-module Main : Sbasic = Make (Basic)
-include Main
+include Make (Basic)
(* Local Variables: *)
(* compile-command:"make -C .." *)
diff --git a/src/types.mli b/src/types.mli
new file mode 100644
index 00000000..8653a9dc
--- /dev/null
+++ b/src/types.mli
@@ -0,0 +1,161 @@
+open Utils
+
+module type BASIC_TYPES = sig
+ type t
+
+ val pp : Format.formatter -> t -> unit
+
+ val pp_c : Format.formatter -> t -> unit
+
+ val is_scalar_type : t -> bool
+
+ val is_numeric_type : t -> bool
+
+ val is_int_type : t -> bool
+
+ val is_real_type : t -> bool
+
+ val is_bool_type : t -> bool
+
+ val is_dimension_type : t -> bool
+
+ val type_int_builder : t
+
+ val type_real_builder : t
+
+ val type_bool_builder : t
+
+ val type_string_builder : t
+
+ val unify : t -> t -> unit
+
+ val is_unifiable : t -> t -> bool
+end
+
+module type S = sig
+ module BasicT : BASIC_TYPES
+
+ type basic_type = BasicT.t
+
+ type t = { mutable tdesc: type_desc; tid: int }
+
+ and type_desc =
+ | Tconst of ident
+ (* type constant *)
+ | Tbasic of basic_type
+ | Tclock of t
+ (* A type expression explicitely tagged as carrying a clock *)
+ | Tarrow of t * t
+ | Ttuple of t list
+ | Tenum of ident list
+ | Tstruct of (ident * t) list
+ | Tarray of Dimension.t * t
+ | Tstatic of Dimension.t * t
+ (* a type carried by a dimension expression *)
+ | Tlink of t
+ (* During unification, make links instead of substitutions *)
+ | Tvar
+ (* Monomorphic type variable *)
+ | Tunivar
+ (* Polymorphic type variable *)
+
+ type error =
+ | Unbound_value of ident
+ | Already_bound of ident
+ | Already_defined of ident
+ | Undefined_var of ISet.t
+ | Declared_but_undefined of ident
+ | Unbound_type of ident
+ | Not_a_dimension
+ | Not_a_constant
+ | Assigned_constant of ident
+ | WrongArity of int * int
+ | WrongMorphism of int * int
+ | Type_mismatch of ident
+ | Type_clash of t * t
+ | Poly_imported_node of ident
+
+ exception Unify of t * t
+
+ exception Error of Location.t * error
+
+ val is_real_type : t -> bool
+
+ val is_int_type : t -> bool
+
+ val is_bool_type : t -> bool
+
+ val is_const_type : t -> ident -> bool
+
+ val is_static_type : t -> bool
+
+ val is_array_type : t -> bool
+
+ val is_dimension_type : t -> bool
+
+ val is_address_type : t -> bool
+
+ val is_generic_type : t -> bool
+
+ val print_ty : Format.formatter -> t -> unit
+
+ val repr : t -> t
+
+ val dynamic_type : t -> t
+
+ val type_desc : t -> type_desc
+
+ val new_var : unit -> t
+
+ val new_univar : unit -> t
+
+ val new_ty : type_desc -> t
+
+ val type_int : type_desc
+
+ val type_real : type_desc
+
+ val type_bool : type_desc
+
+ val type_string : type_desc
+
+ val array_element_type : t -> t
+
+ val type_list_of_type : t -> t list
+
+ val print_node_ty : Format.formatter -> t -> unit
+
+ val get_clock_base_type : t -> t option
+
+ val get_static_value : t -> Dimension.t option
+
+ val is_tuple_type : t -> bool
+
+ val type_of_type_list : t list -> t
+
+ val split_arrow : t -> t * t
+
+ val unclock_type : t -> t
+
+ val bottom : t
+
+ val map_tuple_type : (t -> t) -> t -> t
+
+ val array_base_type : t -> t
+
+ val array_type_dimension : t -> Dimension.t
+
+ val pp_error : Format.formatter -> error -> unit
+
+ val struct_field_type : t -> ident -> t
+
+ val array_type_multi_dimension : t -> Dimension.t list
+end
+
+module Make(BasicT: BASIC_TYPES) : sig
+ include S
+ val print_ty_param: (Format.formatter -> basic_type -> unit) -> Format.formatter -> t -> unit
+end
+with module BasicT = BasicT
+
+include S
diff --git a/src/typing.ml b/src/typing.ml
index 4f5cda9c..762e67e3 100644
--- a/src/typing.ml
+++ b/src/typing.ml
@@ -35,19 +35,20 @@ open Corelang
module type EXPR_TYPE_HUB = sig
type type_expr
- val import : Types.Main.type_expr -> type_expr
+ val import : Types.t -> type_expr
- val export : type_expr -> Types.Main.type_expr
+ val export : type_expr -> Types.t
end
module Make
(T : Types.S)
- (Expr_type_hub : EXPR_TYPE_HUB with type type_expr = T.type_expr) =
+ (Expr_type_hub : EXPR_TYPE_HUB with type type_expr = T.t)
+=
struct
module TP = Type_predef.Make (T)
include TP
- let pp_typing_env fmt env = Env.pp_env print_ty fmt env
+ let pp_typing_env fmt env = Env.pp print_ty fmt env
(****************************************************************)
(* Generic functions: occurs, instantiate and generalize *)
@@ -219,7 +220,7 @@ struct
tdef.tydef_desc
| _ ->
assert false
- with Not_found -> raise (Error (Location.dummy_loc, Unbound_type tname))
+ with Not_found -> raise (Error (Location.dummy, Unbound_type tname))
let get_type_definition tname =
type_coretype (fun _ -> ()) (get_coretype_definition tname)
@@ -252,7 +253,7 @@ struct
eq_ground t1' t2'
| Tstatic (e1, t1'), Tstatic (e2, t2') | Tarray (e1, t1'), Tarray (e2, t2')
->
- Dimension.is_eq_dimension e1 e2 && eq_ground t1' t2'
+ Dimension.equal e1 e2 && eq_ground t1' t2'
| _ ->
false
@@ -312,7 +313,7 @@ struct
| Tarray (e1, t1'), Tarray (e2, t2') ->
let eval_const =
if semi then fun c ->
- Some (Dimension.mkdim_ident Location.dummy_loc c)
+ Some (Dimension.mkdim_ident Location.dummy c)
else fun _ -> None
in
unif t1' t2';
@@ -757,7 +758,7 @@ struct
{
expr_tag = new_tag ();
expr_desc = Expr_when (expr, x, l);
- expr_type = Types.Main.new_var ();
+ expr_type = Types.new_var ();
expr_clock = Clocks.new_var true;
expr_delay = Delay.new_var ();
expr_loc = loc;
@@ -1107,16 +1108,15 @@ struct
let check_typedef_compat header = List.iter check_typedef_top header
end
-include
- Make
- (Types.Main)
- (struct
- type type_expr = Types.Main.type_expr
+module Expr_type_hub: EXPR_TYPE_HUB with type type_expr = Types.t = struct
+ type type_expr = Types.t
- let import x = x
+ let import x = x
+ let export x = x
+end
+
+include Make(Types)(Expr_type_hub)
- let export x = x
- end)
(* Local Variables: *)
(* compile-command:"make -C .." *)
(* End: *)
diff --git a/src/typing.mli b/src/typing.mli
new file mode 100644
index 00000000..d0b2a9aa
--- /dev/null
+++ b/src/typing.mli
@@ -0,0 +1,28 @@
+open Lustre_types
+
+val type_const: ?is_annot:bool -> Location.t -> constant -> Types.t
+val type_node: Types.t Env.t -> node_desc -> Location.t -> Types.t Env.t
+
+
+module type EXPR_TYPE_HUB = sig
+ type type_expr
+
+ val import : Types.t -> type_expr
+
+ val export : type_expr -> Types.t
+end
+
+module Make(T: Types.S) (Expr_type_hub: EXPR_TYPE_HUB with type type_expr = T.t) : sig
+ val type_expr: ?is_annot:bool -> T.t Env.t * 'a -> bool -> bool -> expr -> T.t
+ val generalize: T.t -> unit
+end
+
+val try_unify: ?sub:bool -> ?semi:bool -> Types.t -> Types.t -> Location.t -> unit
+
+val type_var_decl_list: 'a -> Types.t Env.t -> var_decl list -> Types.t Env.t
+
+val type_prog: Types.t Env.t -> program_t -> Types.t Env.t
+
+val check_typedef_compat: top_decl list -> unit
+
+val check_env_compat: top_decl list -> Types.t Env.t -> Types.t Env.t -> unit
diff --git a/src/utils/dimension.ml b/src/utils/dimension.ml
index 635cebf3..ceed2413 100644
--- a/src/utils/dimension.ml
+++ b/src/utils/dimension.ml
@@ -11,7 +11,7 @@
open Format
-type dim_expr = {
+type t = {
mutable dim_desc : dim_desc;
dim_loc : Location.t;
dim_id : int;
@@ -21,13 +21,13 @@ and dim_desc =
| Dbool of bool
| Dint of int
| Dident of Utils.ident
- | Dappl of Utils.ident * dim_expr list
- | Dite of dim_expr * dim_expr * dim_expr
- | Dlink of dim_expr
+ | Dappl of Utils.ident * t list
+ | Dite of t * t * t
+ | Dlink of t
| Dvar
| Dunivar
-exception Unify of dim_expr * dim_expr
+exception Unify of t * t
exception InvalidDimension
@@ -39,7 +39,7 @@ let mkdim loc dim =
let mkdim_var () =
incr new_id;
- { dim_loc = Location.dummy_loc; dim_id = !new_id; dim_desc = Dvar }
+ { dim_loc = Location.dummy; dim_id = !new_id; dim_desc = Dvar }
let mkdim_ident loc id =
incr new_id;
@@ -61,7 +61,7 @@ let mkdim_ite loc i t e =
incr new_id;
{ dim_loc = loc; dim_id = !new_id; dim_desc = Dite (i, t, e) }
-let rec pp_dimension fmt dim =
+let rec pp fmt dim =
(*fprintf fmt "<%d>" (Obj.magic dim: int);*)
match dim.dim_desc with
| Dident id ->
@@ -71,16 +71,16 @@ let rec pp_dimension fmt dim =
| Dbool b ->
fprintf fmt "%B" b
| Dite (i, t, e) ->
- fprintf fmt "if %a then %a else %a" pp_dimension i pp_dimension t
- pp_dimension e
+ fprintf fmt "if %a then %a else %a" pp i pp t
+ pp e
| Dappl (f, [ arg ]) ->
- fprintf fmt "(%s%a)" f pp_dimension arg
+ fprintf fmt "(%s%a)" f pp arg
| Dappl (f, [ arg1; arg2 ]) ->
- fprintf fmt "(%a%s%a)" pp_dimension arg1 f pp_dimension arg2
+ fprintf fmt "(%a%s%a)" pp arg1 f pp arg2
| Dappl (_, _) ->
assert false
| Dlink dim' ->
- fprintf fmt "%a" pp_dimension dim'
+ fprintf fmt "%a" pp dim'
| Dvar ->
fprintf fmt "_%s" (Utils.name_of_dimension dim.dim_id)
| Dunivar ->
@@ -105,7 +105,7 @@ let check_access loc d i =
let rec repr dim = match dim.dim_desc with Dlink dim' -> repr dim' | _ -> dim
-let rec is_eq_dimension d1 d2 =
+let rec equal d1 d2 =
let d1 = repr d1 in
let d2 = repr d2 in
d1.dim_id = d2.dim_id
@@ -114,9 +114,9 @@ let rec is_eq_dimension d1 d2 =
| Dappl (f1, args1), Dappl (f2, args2) ->
f1 = f2
&& List.length args1 = List.length args2
- && List.for_all2 is_eq_dimension args1 args2
+ && List.for_all2 equal args1 args2
| Dite (c1, t1, e1), Dite (c2, t2, e2) ->
- is_eq_dimension c1 c2 && is_eq_dimension t1 t2 && is_eq_dimension e1 e2
+ equal c1 c2 && equal t1 t2 && equal e1 e2
| Dint i1, Dint i2 ->
i1 = i2
| Dbool b1, Dbool b2 ->
@@ -126,17 +126,17 @@ let rec is_eq_dimension d1 d2 =
| _ ->
false
-let is_dimension_const dim =
+let is_const dim =
match (repr dim).dim_desc with Dint _ | Dbool _ -> true | _ -> false
-let size_const_dimension dim =
+let size_const dim =
match (repr dim).dim_desc with
| Dint i ->
i
| Dbool b ->
if b then 1 else 0
| _ ->
- Format.eprintf "internal error: size_const_dimension %a@." pp_dimension dim;
+ Format.eprintf "internal error: size_const_dimension %a@." pp dim;
assert false
let rec is_polymorphic dim =
@@ -176,7 +176,7 @@ let rec factors_constant fs =
let norm_factors fs =
let k = factors_constant fs in
- let nk = List.filter (fun d -> not (is_dimension_const d)) fs in
+ let nk = List.filter (fun d -> not (is_const d)) fs in
k, List.sort compare nk
let rec terms dim =
@@ -229,7 +229,7 @@ let rec eval eval_op eval_const dim =
| Some val_dim ->
dim.dim_desc <- Dlink val_dim
| None ->
- Format.eprintf "invalid %a@." pp_dimension dim;
+ Format.eprintf "invalid %a@." pp dim;
raise InvalidDimension)
| Dite (c, t, e) -> (
eval eval_op eval_const c;
@@ -242,7 +242,7 @@ let rec eval eval_op eval_const dim =
())
| Dappl (id, args) ->
List.iter (eval eval_op eval_const) args;
- if List.for_all is_dimension_const args then
+ if List.for_all is_const args then
dim.dim_desc <-
Env.lookup_value eval_op id (List.map (fun d -> (repr d).dim_desc) args)
| Dlink dim' ->
diff --git a/src/utils/dimension.mli b/src/utils/dimension.mli
new file mode 100644
index 00000000..e99526ad
--- /dev/null
+++ b/src/utils/dimension.mli
@@ -0,0 +1,46 @@
+open Utils
+
+type t = {
+ mutable dim_desc : dim_desc;
+ dim_loc : Location.t;
+ dim_id : int;
+}
+
+and dim_desc =
+ | Dbool of bool
+ | Dint of int
+ | Dident of ident
+ | Dappl of ident * t list
+ | Dite of t * t * t
+ | Dlink of t
+ | Dvar
+ | Dunivar
+
+exception Unify of t * t
+exception InvalidDimension
+
+val mkdim: Location.t -> dim_desc -> t
+val mkdim_ident: Location.t -> ident -> t
+val mkdim_int: Location.t -> int -> t
+val mkdim_bool: Location.t -> bool -> t
+val mkdim_var: unit -> t
+val mkdim_appl: Location.t -> ident -> t list -> t
+val mkdim_ite: Location.t -> t -> t -> t -> t
+
+val pp: Format.formatter -> t -> unit
+
+val is_const: t -> bool
+val is_polymorphic: t -> bool
+val generalize: t -> unit
+val instantiate: (int * t) list ref -> t -> t
+val copy: (int * t) list ref -> t -> t
+val equal: t -> t -> bool
+val eval: (dim_desc list -> dim_desc) Env.t -> (ident -> t option) -> t -> unit
+val unify: ?semi:bool -> t -> t -> unit
+val uneval: ident -> t -> unit
+
+val expr_replace_expr: (ident -> t) -> t -> t
+
+val rename: (ident -> ident) -> (ident -> ident) -> t -> t
+
+val size_const: t -> int
diff --git a/src/utils/env.ml b/src/utils/env.ml
index 8a6c7bca..6e17b948 100644
--- a/src/utils/env.ml
+++ b/src/utils/env.ml
@@ -34,10 +34,10 @@ let overwrite x y =
(fun _ _old _new -> match _new with Some _ -> _new | _ -> _old)
x y
-let pp_env pp_fun fmt env =
+let pp pp_fun fmt env =
let l' = IMap.bindings env in
let pp_fun fmt (id, value) = Format.fprintf fmt "%s |-> %a" id pp_fun value in
- Format.fprintf fmt "{ @[<v 2>%a@] }" (fprintf_list ~sep:"@," pp_fun) l'
+ Format.(fprintf fmt "{ @[<v 2>%a@] }" (pp_print_list pp_fun) l')
(* Local Variables: *)
(* compile-command:"make -C .." *)
diff --git a/src/utils/env.mli b/src/utils/env.mli
new file mode 100644
index 00000000..5da15267
--- /dev/null
+++ b/src/utils/env.mli
@@ -0,0 +1,12 @@
+open Utils
+
+type 'a t
+
+val initial: 'a t
+val add_value: 'a t -> ident -> 'a -> 'a t
+val lookup_value: 'a t -> ident -> 'a
+val exists_value: 'a t -> ident -> bool
+val iter: 'a t -> (ident -> 'a -> unit) -> unit
+val pp: (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a t -> unit
+val overwrite: 'a t -> 'a t -> 'a t
+val fold: (ident -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
diff --git a/src/utils/location.ml b/src/utils/location.ml
index 58069a15..b3ed097c 100644
--- a/src/utils/location.ml
+++ b/src/utils/location.ml
@@ -16,7 +16,7 @@ type t = position * position
type filename = string
-let dummy_loc = dummy_pos, dummy_pos
+let dummy = dummy_pos, dummy_pos
let set_input, get_input, get_module =
let input_name : filename ref = ref "__UNINITIALIZED__" in
@@ -33,14 +33,6 @@ let filename_of_loc (s, _) = s.pos_fname
let filename_of_lexbuf lexbuf = lexbuf.lex_start_p.pos_fname
-(* let init lexbuf fname =
- * lexbuf.Lexing.lex_curr_p <- {
- * Lexing.pos_fname = fname;
- * Lexing.pos_lnum = 1;
- * Lexing.pos_bol = 0;
- * Lexing.pos_cnum = 0;
- * } *)
-
let shift_pos pos1 pos2 =
(* Format.eprintf "Shift pos %s by pos %s@." pos1.Lexing.pos_fname pos2.Lexing.pos_fname;
* assert (pos1.Lexing.pos_fname = pos2.Lexing.pos_fname); *)
@@ -57,31 +49,10 @@ let shift_pos pos1 pos2 =
then pos1.pos_cnum + pos2.pos_cnum else pos2.pos_cnum *);
}
-(* let print loc =
- * let filename = loc.loc_start.pos_fname in
- * let line = loc.loc_start.pos_lnum in
- * let start_char =
- * loc.loc_start.pos_cnum - loc.loc_start.pos_bol
- * in
- * let end_char =
- * loc.loc_end.pos_cnum - loc.loc_start.pos_cnum + start_char
- * in
- * let (start_char, end_char) =
- * if start_char < 0 then (0,1) else (start_char, end_char)
- * in
- * print_string ("File \""^filename^"\", line ");
- * print_int line;
- * print_string ", characters ";
- * print_int start_char;
- * print_string "-";
- * print_int end_char;
- * print_string ":";
- * print_newline () *)
-
let loc_line (s, _e) = s.pos_lnum
-let pp_loc fmt loc =
- if loc == dummy_loc then () else Format.fprintf fmt "%s" (Lex.range loc)
+let pp fmt loc =
+ if loc = dummy then () else Format.fprintf fmt "%s" (Lex.range loc)
let pp_c_loc fmt (s, _e) =
let filename = s.pos_fname in
diff --git a/src/utils/location.mli b/src/utils/location.mli
new file mode 100644
index 00000000..c2857c00
--- /dev/null
+++ b/src/utils/location.mli
@@ -0,0 +1,10 @@
+type t = Lexing.position * Lexing.position
+type filename = string
+
+val dummy: t
+val pp: Format.formatter -> t -> unit
+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
diff --git a/src/utils/utils.ml b/src/utils/utils.ml
index 5283e7aa..5713cb22 100644
--- a/src/utils/utils.ml
+++ b/src/utils/utils.ml
@@ -52,9 +52,23 @@ module IMap = struct
m1 m2
let of_list l = List.fold_left (fun m (x, v) -> add x v m) empty l
+
+ let pp ?(comment = "") pp_val fmt m =
+ Format.fprintf fmt "@[<hv 0>@[<hv 2>{ %s" comment;
+ iter (fun key v -> Format.fprintf fmt "@ %s -> %a" key pp_val v) m;
+ Format.fprintf fmt "@]@ }@]"
+end
+
+module ISet = struct
+ include Set.Make (IdentModule)
+
+ let pp fmt t =
+ let open Format in
+ fprintf fmt "@[<hv 0>@[<hv 2>{";
+ iter (fun s -> fprintf fmt "@ %s" s) t;
+ fprintf fmt "@]@ }@]"
end
-module ISet = Set.Make (IdentModule)
module IdentDepGraph = Imperative.Digraph.ConcreteBidirectional (IdentModule)
module TopologicalDepGraph = Topological.Make (IdentDepGraph)
module ComponentsDepGraph = Components.Make (IdentDepGraph)
@@ -407,16 +421,6 @@ let pp_array a pp_fun beg_str end_str sep_str =
pp_fun a.(n - 1));
if end_str = "\n" then print_newline () else print_string end_str
-let pp_iset fmt t =
- Format.fprintf fmt "@[<hv 0>@[<hv 2>{";
- ISet.iter (fun s -> Format.fprintf fmt "@ %s" s) t;
- Format.fprintf fmt "@]@ }@]"
-
-let pp_imap ?(comment = "") pp_val fmt m =
- Format.fprintf fmt "@[<hv 0>@[<hv 2>{ %s" comment;
- IMap.iter (fun key v -> Format.fprintf fmt "@ %s -> %a" key pp_val v) m;
- Format.fprintf fmt "@]@ }@]"
-
let pp_hashtbl t pp_fun beg_str end_str sep_str =
if beg_str = "\n" then print_newline () else print_string beg_str;
let pp_fun1 k v =
diff --git a/src/utils/utils.mli b/src/utils/utils.mli
new file mode 100644
index 00000000..d738d586
--- /dev/null
+++ b/src/utils/utils.mli
@@ -0,0 +1,93 @@
+type ident = string
+type tag = int
+
+module IMap: sig
+ include Map.S with type key = ident
+ val pp: ?comment:string -> (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a t -> unit
+end
+
+module ISet: sig
+ include Set.S with type elt = ident
+ val pp: Format.formatter -> t -> unit
+end
+
+module Format: sig
+ include module type of Format
+ val pp_print_semicolon: formatter -> unit -> unit
+ val pp_open_vbox0: formatter -> unit -> unit
+ val pp_print_cutcut: formatter -> unit -> unit
+ val pp_print_nothing: formatter -> 'a -> unit
+ val pp_print_list:
+ ?pp_prologue:(formatter -> unit -> unit) ->
+ ?pp_epilogue:(formatter -> unit -> unit) ->
+ ?pp_op:(formatter -> unit -> unit) ->
+ ?pp_cl:(formatter -> unit -> unit) ->
+ ?pp_open_box:(formatter -> unit -> unit) ->
+ ?pp_eol:(formatter -> unit -> unit) ->
+ ?pp_nil:(formatter -> unit -> unit) ->
+ ?pp_sep:(formatter -> unit -> unit) ->
+ (formatter -> 'a -> unit) -> formatter -> 'a list -> unit
+ val pp_comma_list:
+ ?pp_prologue:(formatter -> unit -> unit) ->
+ ?pp_epilogue:(formatter -> unit -> unit) ->
+ ?pp_op:(formatter -> unit -> unit) ->
+ ?pp_cl:(formatter -> unit -> unit) ->
+ ?pp_open_box:(formatter -> unit -> unit) ->
+ ?pp_eol:(formatter -> unit -> unit) ->
+ ?pp_nil:(formatter -> unit -> unit) ->
+ (formatter -> 'a -> unit) -> formatter -> 'a list -> unit
+ val pp_print_parenthesized:
+ ?pp_sep:(formatter -> unit -> unit) ->
+ ?pp_prologue:(formatter -> unit -> unit) ->
+ ?pp_epilogue:(formatter -> unit -> unit) ->
+ ?pp_open_box:(formatter -> unit -> unit) ->
+ ?pp_eol:(formatter -> unit -> unit) ->
+ ?pp_nil:(formatter -> unit -> unit) ->
+ (formatter -> 'a -> unit) -> formatter -> 'a list -> unit
+ val pp_print_bracketed:
+ ?pp_sep:(formatter -> unit -> unit) ->
+ ?pp_prologue:(formatter -> unit -> unit) ->
+ ?pp_epilogue:(formatter -> unit -> unit) ->
+ ?pp_open_box:(formatter -> unit -> unit) ->
+ ?pp_eol:(formatter -> unit -> unit) ->
+ ?pp_nil:(formatter -> unit -> unit) ->
+ (formatter -> 'a -> unit) -> formatter -> 'a list -> unit
+end
+
+module IdentDepGraph: Graph.Sig.I with type V.t = ident
+module TopologicalDepGraph: sig
+ val fold : (ident -> 'a -> 'a) -> IdentDepGraph.t -> 'a -> 'a
+ val iter : (ident -> unit) -> IdentDepGraph.t -> unit
+end
+
+val name_of_dimension: tag -> ident
+
+val name_of_carrier: tag -> ident
+
+val name_of_type: tag -> ident
+
+val name_of_delay: tag -> ident
+
+val reset_names: unit -> unit
+
+val pp_date: Format.formatter -> Unix.tm -> unit
+
+exception TransposeError of int * int
+
+val transpose_list: 'a list list -> 'a list list
+
+val new_tag: unit -> tag
+
+exception DeSome
+
+val desome: 'a option -> 'a
+
+val create_hashtable: int -> ('a * 'b) list -> ('a, 'b) Hashtbl.t
+
+val option_map: ('a -> 'b) -> 'a option -> 'b option
+
+val repeat: int -> ('a -> 'a) -> 'a -> 'a
+
+val add_cons: 'a -> 'a list -> 'a list
+
+val enumerate: int -> int list
diff --git a/src/verifierList.mli b/src/verifierList.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/verifierType.mli b/src/verifierType.mli
new file mode 100644
index 00000000..5bfdeab9
--- /dev/null
+++ b/src/verifierType.mli
@@ -0,0 +1,17 @@
+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
diff --git a/src/verifiers.mli b/src/verifiers.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/version.mli b/src/version.mli
new file mode 100644
index 00000000..e8e24e73
--- /dev/null
+++ b/src/version.mli
@@ -0,0 +1,3 @@
+val number: string
+val codename: string
+val include_path: string
--
GitLab