From a7062da6157cf76d63b01c85732f3ba1a8d1d49e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?L=C3=A9lio=20Brun?= <lelio.brun@isae-supaero.fr>
Date: Mon, 28 Jun 2021 21:52:46 +0200
Subject: [PATCH] another step towards refactoring
---
src/annotations.mli | 2 +
src/backends/Ada/ada_backend.ml | 28 +-
src/backends/Ada/ada_backend.mli | 5 +
src/backends/Ada/ada_backend_adb.ml | 364 +++++++--------
src/backends/Ada/ada_backend_adb.mli | 12 +
src/backends/Ada/ada_backend_ads.ml | 424 +++++++++---------
src/backends/Ada/ada_backend_ads.mli | 12 +
src/backends/Ada/ada_backend_common.ml | 111 ++---
src/backends/Ada/ada_backend_common.mli | 8 +-
src/backends/Ada/ada_backend_wrapper.ml | 356 +++++++--------
src/backends/Ada/ada_backend_wrapper.mli | 26 ++
src/backends/Ada/ada_printer.ml | 43 +-
src/backends/Ada/misc_lustre_function.mli | 41 ++
src/backends/Ada/misc_printer.mli | 11 +-
src/backends/C/c_backend.ml | 34 +-
src/backends/C/c_backend.mli | 6 +
src/backends/C/c_backend_common.ml | 37 +-
src/backends/C/c_backend_common.mli | 147 +++++-
src/backends/C/c_backend_header.ml | 20 +-
src/backends/C/c_backend_header.mli | 17 +
src/backends/C/c_backend_main.ml | 12 +-
src/backends/C/c_backend_main.mli | 11 +
src/backends/C/c_backend_makefile.ml | 16 +-
src/backends/C/c_backend_makefile.mli | 17 +
src/backends/C/c_backend_mauve.ml | 2 +-
src/backends/C/c_backend_mauve.mli | 7 +
src/backends/C/c_backend_spec.ml | 9 +-
src/backends/C/c_backend_src.ml | 41 +-
src/backends/C/c_backend_src.mli | 29 ++
src/backends/EMF/EMF_backend.ml | 27 +-
src/backends/EMF/EMF_backend.mli | 1 +
src/backends/EMF/EMF_common.ml | 29 +-
src/backends/EMF/EMF_common.mli | 24 +
src/backends/EMF/EMF_library_calls.ml | 4 +-
src/backends/EMF/EMF_library_calls.mli | 2 +
src/backends/Horn/horn_backend.ml | 2 +-
src/backends/Horn/horn_backend.mli | 1 +
.../Horn/horn_backend_collecting_sem.ml | 41 +-
.../Horn/horn_backend_collecting_sem.mli | 7 +
src/backends/Horn/horn_backend_common.ml | 3 +-
src/backends/Horn/horn_backend_common.mli | 37 ++
src/backends/Horn/horn_backend_printers.ml | 88 ++--
src/backends/Horn/horn_backend_printers.mli | 8 +
src/backends/Horn/horn_backend_traces.ml | 65 ++-
src/backends/Horn/horn_backend_traces.mli | 1 +
src/backends/backends.mli | 1 +
src/basic_library.mli | 1 +
src/causality.ml | 18 +-
src/causality.mli | 14 +
src/checks/access.ml | 4 +-
src/checks/access.mli | 1 +
src/checks/algebraicLoop.ml | 29 +-
src/checks/algebraicLoop.mli | 4 +
src/clock_calculus.mli | 2 +
src/clocks.mli | 6 +
src/compiler_common.mli | 13 +
src/compiler_stages.ml | 23 +-
src/inliner.mli | 7 +
src/machine_code_common.mli | 2 +
src/optimize_machine.mli | 16 +
src/optimize_prog.mli | 3 +
src/options.ml | 2 +
src/options.mli | 5 +
src/options_management.mli | 2 +
src/plugins/mpfr/lustrec_mpfr.mli | 18 +
src/plugins/plugins.mli | 5 +
src/printers.mli | 5 +
src/scheduling.mli | 7 +
src/spec.mli | 3 +
src/tools/stateflow/common/activeStates.ml | 13 +-
src/tools/stateflow/common/activeStates.mli | 7 +
src/tools/stateflow/common/basetypes.ml | 3 +-
src/tools/stateflow/common/basetypes.mli | 77 ++++
src/tools/stateflow/common/datatype.ml | 43 +-
src/tools/stateflow/common/datatype.mli | 53 +++
.../stateflow/json-parser/json_parser.mli | 0
.../json-parser/main_parse_json_file.mli | 0
.../test_json_parser_variables.mli | 0
src/tools/stateflow/models/model_medium.mli | 0
src/tools/stateflow/models/model_simple.mli | 7 +
.../stateflow/models/model_stopwatch.mli | 7 +
src/tools/stateflow/semantics/cPS.mli | 0
.../semantics/cPS_ccode_generator.mli | 0
.../stateflow/semantics/cPS_evaluator.mli | 0
.../stateflow/semantics/cPS_interpreter.mli | 0
.../semantics/cPS_lustre_generator.mli | 0
.../stateflow/semantics/cPS_transformer.mli | 0
src/tools/stateflow/semantics/theta.mli | 0
src/type_predef.mli | 2 +
src/typing.mli | 6 +
src/utils/dimension.ml | 6 +-
src/utils/dimension.mli | 5 +
src/utils/location.ml | 2 +-
src/utils/location.mli | 1 +
src/utils/utils.ml | 12 +-
src/utils/utils.mli | 60 +++
src/verifierList.mli | 1 +
97 files changed, 1723 insertions(+), 961 deletions(-)
create mode 100644 src/tools/stateflow/common/activeStates.mli
create mode 100644 src/tools/stateflow/common/basetypes.mli
create mode 100644 src/tools/stateflow/common/datatype.mli
create mode 100644 src/tools/stateflow/json-parser/json_parser.mli
create mode 100644 src/tools/stateflow/json-parser/main_parse_json_file.mli
create mode 100644 src/tools/stateflow/json-parser/test_json_parser_variables.mli
create mode 100644 src/tools/stateflow/models/model_medium.mli
create mode 100644 src/tools/stateflow/models/model_simple.mli
create mode 100644 src/tools/stateflow/models/model_stopwatch.mli
create mode 100644 src/tools/stateflow/semantics/cPS.mli
create mode 100644 src/tools/stateflow/semantics/cPS_ccode_generator.mli
create mode 100644 src/tools/stateflow/semantics/cPS_evaluator.mli
create mode 100644 src/tools/stateflow/semantics/cPS_interpreter.mli
create mode 100644 src/tools/stateflow/semantics/cPS_lustre_generator.mli
create mode 100644 src/tools/stateflow/semantics/cPS_transformer.mli
create mode 100644 src/tools/stateflow/semantics/theta.mli
diff --git a/src/annotations.mli b/src/annotations.mli
index 9fe9f3fa..98dea773 100644
--- a/src/annotations.mli
+++ b/src/annotations.mli
@@ -1,5 +1,7 @@
open Utils
+val expr_annotations: (string list, ident * tag) Hashtbl.t
+
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/backends/Ada/ada_backend.ml b/src/backends/Ada/ada_backend.ml
index 62dfbc88..246f9e46 100644
--- a/src/backends/Ada/ada_backend.ml
+++ b/src/backends/Ada/ada_backend.ml
@@ -114,9 +114,9 @@ let extract_contract machines m =
@param basename name of the lustre file @param prog list of machines to
translate **)
let translate_to_ada basename machines =
- let module Ads = Ada_backend_ads.Main in
- let module Adb = Ada_backend_adb.Main in
- let module Wrapper = Ada_backend_wrapper.Main in
+ (* let module Ads = Ada_backend_ads.Main in
+ * let module Adb = Ada_backend_adb.Main in
+ * let module Wrapper = Ada_backend_wrapper.Main in *)
let is_real_machine m =
match m.mspec.mnode_spec with Some (Contract _) -> false | _ -> true
in
@@ -145,9 +145,9 @@ let translate_to_ada basename machines =
| main_node -> (
match Machine_code_common.get_machine_opt filtered_machines main_node with
| None ->
- Format.eprintf "Ada Code generation error: %a@." Error.pp_error_msg
+ Format.eprintf "Ada Code generation error: %a@." Error.pp
Error.Main_not_found;
- raise (Error.Error (Location.dummy_loc, Error.Main_not_found))
+ raise (Error.Error (Location.dummy, Error.Main_not_found))
| Some m ->
Some m)
in
@@ -158,10 +158,10 @@ let translate_to_ada basename machines =
List.iter check machines;
log_str_level_two 1 "Generating ads";
- List.iter (write_file destname (_pp_filename "ads") Ads.pp_file) _machines;
+ List.iter (write_file destname (_pp_filename "ads") Ada_backend_ads.pp_file) _machines;
log_str_level_two 1 "Generating adb";
- List.iter (write_file destname (_pp_filename "adb") Adb.pp_file) _machines;
+ List.iter (write_file destname (_pp_filename "adb") Ada_backend_adb.pp_file) _machines;
(* If a main node is given we generate a main adb file and a project file *)
log_str_level_two 1 "Generating wrapper files";
@@ -169,19 +169,19 @@ let translate_to_ada basename machines =
| None ->
()
| Some machine ->
- write_file destname pp_main_filename Wrapper.pp_main_adb
+ write_file destname pp_main_filename Ada_backend_wrapper.pp_main_adb
(*get_typed_submachines filtered_machines machine*)
machine;
write_file destname
- (fun fmt _ -> Wrapper.pp_project_name (basename ^ "_exe") fmt)
- (Wrapper.pp_project_file filtered_machines basename)
+ (fun fmt _ -> Ada_backend_wrapper.pp_project_name (basename ^ "_exe") fmt)
+ (Ada_backend_wrapper.pp_project_file filtered_machines basename)
main_machine);
- write_file destname Wrapper.pp_project_configuration_name
- (fun fmt _ -> Wrapper.pp_project_configuration_file fmt)
+ write_file destname Ada_backend_wrapper.pp_project_configuration_name
+ (fun fmt _ -> Ada_backend_wrapper.pp_project_configuration_file fmt)
basename;
write_file destname
- (fun fmt _ -> Wrapper.pp_project_name (basename ^ "_lib") fmt)
- (Wrapper.pp_project_file filtered_machines basename)
+ (fun fmt _ -> Ada_backend_wrapper.pp_project_name (basename ^ "_lib") fmt)
+ (Ada_backend_wrapper.pp_project_file filtered_machines basename)
None
(* Local Variables: *)
diff --git a/src/backends/Ada/ada_backend.mli b/src/backends/Ada/ada_backend.mli
index e69de29b..8de317ed 100644
--- a/src/backends/Ada/ada_backend.mli
+++ b/src/backends/Ada/ada_backend.mli
@@ -0,0 +1,5 @@
+(** Main function of the Ada backend. It calls all the subfunction creating all
+ the file and fill them with Ada code representing the machines list given.
+ @param basename name of the lustre file @param prog list of machines to
+ translate **)
+val translate_to_ada: string -> Machine_code_types.machine_t list -> unit
diff --git a/src/backends/Ada/ada_backend_adb.ml b/src/backends/Ada/ada_backend_adb.ml
index 2d3c3a35..7c9e6aaf 100644
--- a/src/backends/Ada/ada_backend_adb.ml
+++ b/src/backends/Ada/ada_backend_adb.ml
@@ -9,6 +9,7 @@
(* *)
(********************************************************************)
+open Utils
open Format
open Machine_code_types
open Lustre_types
@@ -20,200 +21,201 @@ open Ada_printer
open Ada_backend_common
(** Main module for generating packages bodies **)
-module Main = struct
- (** Printing function for basic assignement [var := value].
- @param fmt the formater to print on @param var_name the name of the
- variable @param value the value to be assigned **)
- let pp_assign env fmt var value =
- fprintf fmt "%a := %a" (pp_var env) var (pp_value env) value
+(** Printing function for basic assignement [var := value].
- (** Printing function for instruction. See {!type:Machine_code_types.instr_t}
- for more details on machine types.
+ @param fmt the formater to print on @param var_name the name of the
+ variable @param value the value to be assigned **)
+let pp_assign env fmt var value =
+ fprintf fmt "%a := %a" (pp_var env) var (pp_value env) value
- @param typed_submachines list of all typed machine instances of this
- machine @param machine the current machine @param fmt the formater to
- print on @param instr the instruction to print **)
- let rec pp_machine_instr typed_submachines env instr fmt =
- let pp_instr = pp_machine_instr typed_submachines env in
- (* Print args for a step call *)
- let pp_state i fmt = fprintf fmt "%t.%s" pp_state_name i in
- (* Print a when branch of a case *)
- let pp_when (cond, instrs) fmt =
- fprintf fmt "when %s =>@,%a" cond pp_block (List.map pp_instr instrs)
- in
- (* Print a case *)
- let pp_case fmt (g, hl) =
- fprintf fmt "case %a is@,%aend case" (pp_value env) g pp_block
- (List.map pp_when hl)
- in
- (* Print a if *)
- (* If neg is true the we must test for the negation of the condition. It
- first check that we don't have a negation and a else case, if so it
- inverses the two branch and remove the negation doing a recursive call. *)
- let pp_if fmt (neg, g, instrs1, instrs2) =
- let pp_cond =
- if neg then fun fmt x -> fprintf fmt "! (%a)" (pp_value env) x
- else pp_value env
- in
- let pp_else =
- match instrs2 with
- | None ->
- fun fmt -> fprintf fmt ""
- | Some i2 ->
- fun fmt -> fprintf fmt "else@,%a" pp_block (List.map pp_instr i2)
- in
- fprintf fmt "if %a then@,%a%tend if" pp_cond g pp_block
- (List.map pp_instr instrs1)
- pp_else
- in
- match get_instr_desc instr with
- (* no reset *)
- | MNoReset _ ->
- ()
- (* TODO: handle clear_reset *)
- | MClearReset ->
- ()
- (* reset *)
- | MSetReset i when List.mem_assoc i typed_submachines ->
- let substitution, submachine = get_instance i typed_submachines in
- let pp_package =
- pp_package_name_with_polymorphic substitution submachine
- in
- let args =
- if is_machine_statefull submachine then [ [ pp_state i ] ] else []
- in
- pp_call fmt (pp_package_access (pp_package, pp_reset_procedure_name), args)
- | MLocalAssign (ident, value) ->
- pp_assign env fmt ident value
- | MStateAssign (ident, value) ->
- pp_assign env fmt ident value
- | MStep ([ i0 ], i, vl) when is_builtin_fun i ->
- let value = mk_val (Fun (i, vl)) i0.var_type in
- pp_assign env fmt i0 value
- | MStep (il, i, vl) when List.mem_assoc i typed_submachines ->
- let substitution, submachine = get_instance i typed_submachines in
- let pp_package =
- pp_package_name_with_polymorphic substitution submachine
- in
- let input = List.map (fun x fmt -> pp_value env fmt x) vl in
- let output = List.map pp_var_name il in
- let args =
- (if is_machine_statefull submachine then [ [ pp_state i ] ] else [])
- @ (if input != [] then [ input ] else [])
- @ if output != [] then [ output ] else []
- in
- pp_call fmt (pp_package_access (pp_package, pp_step_procedure_name), args)
- | MBranch (_, []) ->
- assert false
- | MBranch (g, (c1, i1) :: tl) when c1 = tag_false || c1 = tag_true ->
- pp_if fmt (build_if g c1 i1 tl)
- | MBranch (g, hl) ->
- pp_case fmt (g, hl)
- | MComment s ->
- let lines = String.split_on_char '\n' s in
- fprintf fmt "%a" (Utils.fprintf_list ~sep:"" pp_oneline_comment) lines
- | _ ->
- assert false
+(** Printing function for instruction. See {!type:Machine_code_types.instr_t}
+ for more details on machine types.
- (** Print the definition of the step procedure from a machine.
-
- @param typed_submachines list of all typed machine instances of this
- machine @param fmt the formater to print on @param machine the machine **)
- let pp_step_definition env typed_submachines fmt (m, m_spec_opt, guarantees) =
- let transform_local_to_state_assign instr =
- match instr.instr_desc with
- | MLocalAssign (ident, value) ->
- { instr with instr_desc = MStateAssign (ident, value) }
- | _ ->
- instr
+ @param typed_submachines list of all typed machine instances of this
+ machine @param machine the current machine @param fmt the formater to
+ print on @param instr the instruction to print **)
+let rec pp_machine_instr typed_submachines env instr fmt =
+ let pp_instr = pp_machine_instr typed_submachines env in
+ (* Print args for a step call *)
+ let pp_state i fmt = fprintf fmt "%t.%s" pp_state_name i in
+ (* Print a when branch of a case *)
+ let pp_when (cond, instrs) fmt =
+ fprintf fmt "when %s =>@,%a" cond pp_block (List.map pp_instr instrs)
+ in
+ (* Print a case *)
+ let pp_case fmt (g, hl) =
+ fprintf fmt "case %a is@,%aend case" (pp_value env) g pp_block
+ (List.map pp_when hl)
+ in
+ (* Print a if *)
+ (* If neg is true the we must test for the negation of the condition. It
+ first check that we don't have a negation and a else case, if so it
+ inverses the two branch and remove the negation doing a recursive call. *)
+ let pp_if fmt (neg, g, instrs1, instrs2) =
+ let pp_cond =
+ if neg then fun fmt x -> fprintf fmt "! (%a)" (pp_value env) x
+ else pp_value env
in
- let pp_local_ghost_list, spec_instrs =
- match m_spec_opt with
+ let pp_else =
+ match instrs2 with
| None ->
- [], []
- | Some m_spec ->
- ( List.map
- (build_pp_var_decl_local (Some (true, false, [], [])))
- (List.filter
- (fun x -> not (List.mem x.var_id guarantees))
- m_spec.mstep.step_locals),
- List.map transform_local_to_state_assign m_spec.mstep.step_instrs )
+ fun fmt -> fprintf fmt ""
+ | Some i2 ->
+ fun fmt -> fprintf fmt "else@,%a" pp_block (List.map pp_instr i2)
+ in
+ fprintf fmt "if %a then@,%a%tend if" pp_cond g pp_block
+ (List.map pp_instr instrs1)
+ pp_else
+ in
+ match get_instr_desc instr with
+ (* no reset *)
+ | MNoReset _ ->
+ ()
+ (* TODO: handle clear_reset *)
+ | MClearReset ->
+ ()
+ (* reset *)
+ | MSetReset i when List.mem_assoc i typed_submachines ->
+ let substitution, submachine = get_instance i typed_submachines in
+ let pp_package =
+ pp_package_name_with_polymorphic substitution submachine
in
- let pp_local_list =
- List.map (build_pp_var_decl_local None) m.mstep.step_locals
+ let args =
+ if is_machine_statefull submachine then [ [ pp_state i ] ] else []
in
- let pp_instr_list =
- List.map
- (pp_machine_instr typed_submachines env)
- (m.mstep.step_instrs @ spec_instrs)
+ pp_call fmt (pp_package_access (pp_package, pp_reset_procedure_name), args)
+ | MLocalAssign (ident, value) ->
+ pp_assign env fmt ident value
+ | MStateAssign (ident, value) ->
+ pp_assign env fmt ident value
+ | MStep ([ i0 ], i, vl) when is_builtin_fun i ->
+ let value = mk_val (Fun (i, vl)) i0.var_type in
+ pp_assign env fmt i0 value
+ | MStep (il, i, vl) when List.mem_assoc i typed_submachines ->
+ let substitution, submachine = get_instance i typed_submachines in
+ let pp_package =
+ pp_package_name_with_polymorphic substitution submachine
in
- let content =
- AdaProcedureContent
- ( ((if pp_local_ghost_list = [] then [] else [ pp_local_ghost_list ])
- @ if pp_local_list = [] then [] else [ pp_local_list ]),
- pp_instr_list )
+ let input = List.map (fun x fmt -> pp_value env fmt x) vl in
+ let output = List.map pp_var_name il in
+ let args =
+ (if is_machine_statefull submachine then [ [ pp_state i ] ] else [])
+ @ (if input != [] then [ input ] else [])
+ @ if output != [] then [ output ] else []
in
- pp_procedure pp_step_procedure_name (build_pp_arg_step m) None fmt content
+ pp_call fmt (pp_package_access (pp_package, pp_step_procedure_name), args)
+ | MBranch (_, []) ->
+ assert false
+ | MBranch (g, (c1, i1) :: tl) when c1 = tag_false || c1 = tag_true ->
+ pp_if fmt (build_if g c1 i1 tl)
+ | MBranch (g, hl) ->
+ pp_case fmt (g, hl)
+ | MComment s ->
+ let lines = String.split_on_char '\n' s in
+ fprintf fmt "%a" (pp_print_list ~pp_sep:pp_print_nothing pp_oneline_comment) lines
+ | _ ->
+ assert false
- (** Print the definition of the reset procedure from a machine.
+(** Print the definition of the step procedure from a machine.
- @param typed_submachines list of all typed machine instances of this
- machine @param fmt the formater to print on @param machine the machine **)
- let pp_reset_definition env typed_submachines fmt (m, m_spec_opt) =
- let build_assign = function
- | var ->
- mkinstr (MStateAssign (var, mk_default_value var.var_type))
- in
- let env, memory =
- match m_spec_opt with None -> env, m.mmemory | Some _ -> env, m.mmemory
- in
- let assigns = List.map build_assign memory in
- let pp_instr_list =
- List.map (pp_machine_instr typed_submachines env) (assigns @ m.minit)
- in
- pp_procedure pp_reset_procedure_name (build_pp_arg_reset m) None fmt
- (AdaProcedureContent ([], pp_instr_list))
+ @param typed_submachines list of all typed machine instances of this
+ machine @param fmt the formater to print on @param machine the machine **)
+let pp_step_definition env typed_submachines fmt (m, m_spec_opt, guarantees) =
+ let transform_local_to_state_assign instr =
+ match instr.instr_desc with
+ | MLocalAssign (ident, value) ->
+ { instr with instr_desc = MStateAssign (ident, value) }
+ | _ ->
+ instr
+ in
+ let pp_local_ghost_list, spec_instrs =
+ match m_spec_opt with
+ | None ->
+ [], []
+ | Some m_spec ->
+ ( List.map
+ (build_pp_var_decl_local (Some (true, false, [], [])))
+ (List.filter
+ (fun x -> not (List.mem x.var_id guarantees))
+ m_spec.mstep.step_locals),
+ List.map transform_local_to_state_assign m_spec.mstep.step_instrs )
+ in
+ let pp_local_list =
+ List.map (build_pp_var_decl_local None) m.mstep.step_locals
+ in
+ let pp_instr_list =
+ List.map
+ (pp_machine_instr typed_submachines env)
+ (m.mstep.step_instrs @ spec_instrs)
+ in
+ let content =
+ AdaProcedureContent
+ ( ((if pp_local_ghost_list = [] then [] else [ pp_local_ghost_list ])
+ @ if pp_local_list = [] then [] else [ pp_local_list ]),
+ pp_instr_list )
+ in
+ pp_procedure pp_step_procedure_name (build_pp_arg_step m) None fmt content
- (** Print the package definition(ads) of a machine. It requires the list of
- all typed instance. A typed submachine instance is (ident, type_machine)
- with ident the instance name and typed_machine is (substitution, machine)
- with machine the machine associated to the instance and substitution the
- instanciation of all its polymorphic types. @param fmt the formater to
- print on @param typed_submachines list of all typed machine instances of
- this machine @param m the machine **)
- let pp_file fmt (typed_submachines, ((opt_spec_machine, guarantees), machine))
- =
- let env = List.map (fun x -> x.var_id, pp_state_name) machine.mmemory in
- let pp_reset fmt =
- if is_machine_statefull machine then
- fprintf fmt "%a;@,@,"
- (pp_reset_definition env typed_submachines)
- (machine, opt_spec_machine)
- else fprintf fmt ""
- in
- let aux pkgs (id, _) =
- try
- let pkg, _ = List.assoc id ada_supported_funs in
- if List.mem pkg pkgs then pkgs else pkg :: pkgs
- with Not_found -> pkgs
- in
- let packages = List.map pp_str (List.fold_left aux [] machine.mcalls) in
- let pp_content fmt =
- fprintf fmt "%t%a" (*Define the reset procedure*) pp_reset
- (*Define the step procedure*)
- (pp_step_definition env typed_submachines)
- (machine, opt_spec_machine, guarantees)
- in
- fprintf fmt "%a%t%a;@."
- (* Include all the required packages*)
- (Utils.fprintf_list ~sep:";@," (pp_with AdaPrivate))
- packages
- (Utils.pp_final_char_if_non_empty ";@,@," packages)
- (*Print package*)
- (pp_package (pp_package_name machine) [] true)
- pp_content
-end
+(** Print the definition of the reset procedure from a machine.
+
+ @param typed_submachines list of all typed machine instances of this
+ machine @param fmt the formater to print on @param machine the machine **)
+let pp_reset_definition env typed_submachines fmt (m, m_spec_opt) =
+ let build_assign = function
+ | var ->
+ mkinstr (MStateAssign (var, mk_default_value var.var_type))
+ in
+ let env, memory =
+ match m_spec_opt with None -> env, m.mmemory | Some _ -> env, m.mmemory
+ in
+ let assigns = List.map build_assign memory in
+ let pp_instr_list =
+ List.map (pp_machine_instr typed_submachines env) (assigns @ m.minit)
+ in
+ pp_procedure pp_reset_procedure_name (build_pp_arg_reset m) None fmt
+ (AdaProcedureContent ([], pp_instr_list))
+
+(** Print the package definition(ads) of a machine. It requires the list of
+ all typed instance. A typed submachine instance is (ident, type_machine)
+ with ident the instance name and typed_machine is (substitution, machine)
+ with machine the machine associated to the instance and substitution the
+ instanciation of all its polymorphic types. @param fmt the formater to
+ print on @param typed_submachines list of all typed machine instances of
+ this machine @param m the machine **)
+let pp_file fmt (typed_submachines, ((opt_spec_machine, guarantees), machine))
+ =
+ let env = List.map (fun x -> x.var_id, pp_state_name) machine.mmemory in
+ let pp_reset fmt =
+ if is_machine_statefull machine then
+ fprintf fmt "%a;@,@,"
+ (pp_reset_definition env typed_submachines)
+ (machine, opt_spec_machine)
+ else fprintf fmt ""
+ in
+ let aux pkgs (id, _) =
+ try
+ let pkg, _ = List.assoc id ada_supported_funs in
+ if List.mem pkg pkgs then pkgs else pkg :: pkgs
+ with Not_found -> pkgs
+ in
+ let packages = List.map pp_str (List.fold_left aux [] machine.mcalls) in
+ let pp_content fmt =
+ fprintf fmt "%t%a" (*Define the reset procedure*) pp_reset
+ (*Define the step procedure*)
+ (pp_step_definition env typed_submachines)
+ (machine, opt_spec_machine, guarantees)
+ in
+ fprintf fmt "%a%a;@."
+ (* Include all the required packages*)
+ (pp_print_list
+ ~pp_sep:pp_print_semicolon
+ ~pp_epilogue:(fun fmt () -> fprintf fmt ";@,@,")
+ (pp_with AdaPrivate))
+ packages
+ (*Print package*)
+ (pp_package (pp_package_name machine) [] true)
+ pp_content
(* Local Variables: *)
(* compile-command: "make -C ../../.." *)
diff --git a/src/backends/Ada/ada_backend_adb.mli b/src/backends/Ada/ada_backend_adb.mli
index e69de29b..e52d73d4 100644
--- a/src/backends/Ada/ada_backend_adb.mli
+++ b/src/backends/Ada/ada_backend_adb.mli
@@ -0,0 +1,12 @@
+open Utils
+open Machine_code_types
+
+(** Print the package definition(ads) of a machine. It requires the list of
+ all typed instance. A typed submachine instance is (ident, type_machine)
+ with ident the instance name and typed_machine is (substitution, machine)
+ with machine the machine associated to the instance and substitution the
+ instanciation of all its polymorphic types. @param fmt the formater to
+ print on @param typed_submachines list of all typed machine instances of
+ this machine @param m the machine **)
+val pp_file: Format.formatter -> (ident * ((tag * Types.t) list * machine_t)) list
+ * ((machine_t option * ident list) * machine_t) -> unit
diff --git a/src/backends/Ada/ada_backend_ads.ml b/src/backends/Ada/ada_backend_ads.ml
index 4a45191f..3b74f2bc 100644
--- a/src/backends/Ada/ada_backend_ads.ml
+++ b/src/backends/Ada/ada_backend_ads.ml
@@ -9,6 +9,7 @@
(* *)
(********************************************************************)
+open Utils
open Format
open Machine_code_types
open Lustre_types
@@ -17,241 +18,248 @@ open Ada_printer
open Ada_backend_common
(** Functions printing the .ads file **)
-module Main = struct
- let rec init f = function i when i < 0 -> [] | i -> f i :: init f (i - 1)
- (*should be replaced by the init of list from ocaml std lib*)
- let suffixOld = "_old"
+let rec init f = function i when i < 0 -> [] | i -> f i :: init f (i - 1)
+(*should be replaced by the init of list from ocaml std lib*)
- let suffixNew = "_new"
+let suffixOld = "_old"
- let pp_invariant_name fmt = fprintf fmt "inv"
+let suffixNew = "_new"
- let pp_transition_name fmt = fprintf fmt "transition"
+let pp_invariant_name fmt = fprintf fmt "inv"
- let pp_init_name fmt = fprintf fmt "init"
+let pp_transition_name fmt = fprintf fmt "transition"
- let pp_state_name_predicate suffix fmt =
- fprintf fmt "%t%s" pp_state_name suffix
+let pp_init_name fmt = fprintf fmt "init"
- let pp_axiomatize_package_name fmt = fprintf fmt "axiomatize"
+let pp_state_name_predicate suffix fmt =
+ fprintf fmt "%t%s" pp_state_name suffix
- (** Print the expression function representing the transition predicate.
- @param fmt the formater to print on **)
- let pp_init_predicate fmt () =
- let new_state =
- AdaIn, pp_state_name_predicate suffixNew, pp_state_type, None
- in
- pp_predicate pp_init_name [ [ new_state ] ] true fmt None
+let pp_axiomatize_package_name fmt = fprintf fmt "axiomatize"
- (** Print the expression function representing the transition predicate.
- @param fmt the formater to print on @param machine the machine **)
- let pp_transition_predicate fmt (_, m) =
- let old_state =
- AdaIn, pp_state_name_predicate suffixOld, pp_state_type, None
- in
- let new_state =
- AdaIn, pp_state_name_predicate suffixNew, pp_state_type, None
- in
- let inputs = build_pp_var_decl_step_input AdaIn None m in
- let outputs = build_pp_var_decl_step_output AdaIn None m in
- pp_predicate pp_transition_name
- ([ [ old_state; new_state ] ] @ inputs @ outputs)
- true fmt None
+(** Print the expression function representing the transition predicate.
+ @param fmt the formater to print on **)
+let pp_init_predicate fmt () =
+ let new_state =
+ AdaIn, pp_state_name_predicate suffixNew, pp_state_type, None
+ in
+ pp_predicate pp_init_name [ [ new_state ] ] true fmt None
- let pp_invariant_predicate fmt () =
- pp_predicate pp_invariant_name
- [ [ build_pp_state_decl AdaIn None ] ]
- true fmt None
+(** Print the expression function representing the transition predicate.
+ @param fmt the formater to print on @param machine the machine **)
+let pp_transition_predicate fmt (_, m) =
+ let old_state =
+ AdaIn, pp_state_name_predicate suffixOld, pp_state_type, None
+ in
+ let new_state =
+ AdaIn, pp_state_name_predicate suffixNew, pp_state_type, None
+ in
+ let inputs = build_pp_var_decl_step_input AdaIn None m in
+ let outputs = build_pp_var_decl_step_output AdaIn None m in
+ pp_predicate pp_transition_name
+ ([ [ old_state; new_state ] ] @ inputs @ outputs)
+ true fmt None
- (** Print a new statement instantiating a generic package. @param fmt the
- formater to print on @param substitutions the instanciation substitution
- @param machine the machine to instanciate **)
- let pp_new_package fmt (substitutions, machine) =
- let pp_name = pp_package_name machine in
- let pp_new_name = pp_package_name_with_polymorphic substitutions machine in
- let instanciations =
- List.map
- (fun (id, typ) -> pp_polymorphic_type id, fun fmt -> pp_type fmt typ)
- substitutions
- in
- pp_package_instanciation pp_new_name pp_name fmt instanciations
+let pp_invariant_predicate fmt () =
+ pp_predicate pp_invariant_name
+ [ [ build_pp_state_decl AdaIn None ] ]
+ true fmt None
- (** Remove duplicates from a list according to a given predicate. @param eq
- the predicate defining equality @param l the list to parse **)
- let remove_duplicates eq l =
- let aux l x = if List.exists (eq x) l then l else x :: l in
- List.fold_left aux [] l
+(** Print a new statement instantiating a generic package. @param fmt the
+ formater to print on @param substitutions the instanciation substitution
+ @param machine the machine to instanciate **)
+let pp_new_package fmt (substitutions, machine) =
+ let pp_name = pp_package_name machine in
+ let pp_new_name = pp_package_name_with_polymorphic substitutions machine in
+ let instanciations =
+ List.map
+ (fun (id, typ) -> pp_polymorphic_type id, fun fmt -> pp_type fmt typ)
+ substitutions
+ in
+ pp_package_instanciation pp_new_name pp_name fmt instanciations
- (** Compare two typed machines. **)
- let eq_typed_machine (subst1, machine1) (subst2, machine2) =
- String.equal machine1.mname.node_id machine2.mname.node_id
- && List.for_all2 (fun a b -> pp_eq_type (snd a) (snd b)) subst1 subst2
+(** Remove duplicates from a list according to a given predicate. @param eq
+ the predicate defining equality @param l the list to parse **)
+let remove_duplicates eq l =
+ let aux l x = if List.exists (eq x) l then l else x :: l in
+ List.fold_left aux [] l
- (** Print the package declaration(ads) of a machine. It requires the list of
- all typed instance. A typed submachine is a (ident, typed_machine) with -
- ident: the name - typed_machine: a (substitution, machine) with - machine:
- the submachine struct - substitution the instanciation of all its
- polymorphic types. @param fmt the formater to print on @param
- typed_submachines list of all typed submachines of this machine @param m
- the machine **)
- let pp_file fmt (typed_submachines, ((m_spec_opt, guarantees), m)) =
- let typed_machines = snd (List.split typed_submachines) in
- let typed_machines_set =
- remove_duplicates eq_typed_machine typed_machines
- in
+(** Compare two typed machines. **)
+let eq_typed_machine (subst1, machine1) (subst2, machine2) =
+ String.equal machine1.mname.node_id machine2.mname.node_id
+ && List.for_all2 (fun a b -> pp_eq_type (snd a) (snd b)) subst1 subst2
- let machines_to_import =
- List.map pp_package_name (snd (List.split typed_machines_set))
- in
+(** Print the package declaration(ads) of a machine. It requires the list of
+ all typed instance. A typed submachine is a (ident, typed_machine) with -
+ ident: the name - typed_machine: a (substitution, machine) with - machine:
+ the submachine struct - substitution the instanciation of all its
+ polymorphic types. @param fmt the formater to print on @param
+ typed_submachines list of all typed submachines of this machine @param m
+ the machine **)
+let pp_file fmt (typed_submachines, ((m_spec_opt, guarantees), m)) =
+ let typed_machines = snd (List.split typed_submachines) in
+ let typed_machines_set =
+ remove_duplicates eq_typed_machine typed_machines
+ in
- let polymorphic_types = find_all_polymorphic_type m in
+ let machines_to_import =
+ List.map pp_package_name (snd (List.split typed_machines_set))
+ in
- let typed_machines_to_instanciate =
- List.filter (fun (l, _) -> l != []) typed_machines_set
- in
+ let polymorphic_types = find_all_polymorphic_type m in
- let typed_instances =
- List.filter is_submachine_statefull typed_submachines
- in
+ let typed_machines_to_instanciate =
+ List.filter (fun (l, _) -> l != []) typed_machines_set
+ in
- let memories =
- match m_spec_opt with
- | None ->
- []
- | Some m ->
- List.map
- (fun x ->
- pp_var_decl
- (build_pp_var_decl AdaNoMode (Some (true, false, [], [])) x))
- m.mmemory
- in
- let ghost_private = memories in
- (* Commented since not used. Could be reinjected in the code let vars_spec =
- match m_spec_opt with | None -> [] | Some m_spec -> List.map
- (build_pp_var_decl AdaNoMode (Some (true, false, [], [])))
- (m_spec.mmemory) in *)
- let vars = List.map (build_pp_var_decl AdaNoMode None) m.mmemory in
- let states =
+ let typed_instances =
+ List.filter is_submachine_statefull typed_submachines
+ in
+
+ let memories =
+ match m_spec_opt with
+ | None ->
+ []
+ | Some m ->
List.map
- (build_pp_state_decl_from_subinstance AdaNoMode None)
- typed_instances
- in
- let var_lists =
- (if states = [] then [] else [ states ])
- @ if vars = [] then [] else [ vars ]
- in
+ (fun x ->
+ pp_var_decl
+ (build_pp_var_decl AdaNoMode (Some (true, false, [], [])) x))
+ m.mmemory
+ in
+ let ghost_private = memories in
+ (* Commented since not used. Could be reinjected in the code let vars_spec =
+ match m_spec_opt with | None -> [] | Some m_spec -> List.map
+ (build_pp_var_decl AdaNoMode (Some (true, false, [], [])))
+ (m_spec.mmemory) in *)
+ let vars = List.map (build_pp_var_decl AdaNoMode None) m.mmemory in
+ let states =
+ List.map
+ (build_pp_state_decl_from_subinstance AdaNoMode None)
+ typed_instances
+ in
+ let var_lists =
+ (if states = [] then [] else [ states ])
+ @ if vars = [] then [] else [ vars ]
+ in
- let pp_ifstatefull fmt pp =
- if is_machine_statefull m then fprintf fmt "%t" pp else fprintf fmt ""
- in
+ let pp_ifstatefull fmt pp =
+ if is_machine_statefull m then fprintf fmt "%t" pp else fprintf fmt ""
+ in
- let pp_state_decl_and_reset fmt =
- let init fmt =
- pp_call fmt
- ( pp_access pp_axiomatize_package_name pp_init_name,
- [ [ pp_state_name ] ] )
- in
- let contract = Some (false, false, [], [ init ]) in
- fprintf fmt "%t;@,@,%a;@,@,"
- (*Declare the state type*)
- (pp_type_decl pp_state_type AdaPrivate)
- (*Declare the reset procedure*)
- (pp_procedure pp_reset_procedure_name (build_pp_arg_reset m) contract)
- AdaNoContent
+ let pp_state_decl_and_reset fmt =
+ let init fmt =
+ pp_call fmt
+ ( pp_access pp_axiomatize_package_name pp_init_name,
+ [ [ pp_state_name ] ] )
in
+ let contract = Some (false, false, [], [ init ]) in
+ fprintf fmt "%t;@,@,%a;@,@,"
+ (*Declare the state type*)
+ (pp_type_decl pp_state_type AdaPrivate)
+ (*Declare the reset procedure*)
+ (pp_procedure pp_reset_procedure_name (build_pp_arg_reset m) contract)
+ AdaNoContent
+ in
- let pp_private_section fmt =
- fprintf fmt "@,private@,@,%a%t%a%t%a"
- (*Instantiate the polymorphic type that need to be instantiated*)
- (Utils.fprintf_list ~sep:";@," pp_new_package)
- typed_machines_to_instanciate
- (Utils.pp_final_char_if_non_empty ";@,@," typed_machines_to_instanciate)
- (*Define the state type*)
- pp_ifstatefull
- (fun fmt -> pp_record pp_state_type fmt var_lists)
- (Utils.pp_final_char_if_non_empty ";@,@," ghost_private)
- (Utils.fprintf_list ~sep:";@," (fun fmt pp -> pp fmt))
- ghost_private
- in
+ let pp_private_section fmt =
+ fprintf fmt "@,private@,@,%a%a%a"
+ (*Instantiate the polymorphic type that need to be instantiated*)
+ (pp_print_list
+ ~pp_sep:pp_print_semicolon
+ ~pp_epilogue:(fun fmt () -> fprintf fmt ";@,@,")
+ pp_new_package)
+ typed_machines_to_instanciate
+ (*Define the state type*)
+ pp_ifstatefull
+ (fun fmt -> pp_record pp_state_type fmt var_lists)
+ (pp_print_list
+ ~pp_sep:pp_print_semicolon
+ ~pp_prologue:(fun fmt () -> fprintf fmt ";@,@,")
+ (fun fmt pp -> pp fmt))
+ ghost_private
+ in
- let pp_content fmt =
- let pp_contract_opt =
- let pp_var x fmt = pp_clean_ada_identifier fmt x in
- let guarantee_post_conditions = List.map pp_var guarantees in
- let state_pre_conditions, state_post_conditions =
- if is_machine_statefull m then
- let input = List.map pp_var_name m.mstep.step_inputs in
- let output = List.map pp_var_name m.mstep.step_outputs in
- let args =
- [ [ pp_old pp_state_name; pp_state_name ] ]
- @ (if input != [] then [ input ] else [])
- @ if output != [] then [ output ] else []
- in
- let transition fmt =
- pp_call fmt
- (pp_access pp_axiomatize_package_name pp_transition_name, args)
- in
- let invariant fmt =
- pp_call fmt
- ( pp_access pp_axiomatize_package_name pp_invariant_name,
- [ [ pp_state_name ] ] )
- in
- [ invariant ], [ transition; invariant ]
- else [], []
- in
- let post_conditions =
- state_post_conditions @ guarantee_post_conditions
- in
- let pre_conditions = state_pre_conditions in
- if post_conditions = [] && pre_conditions = [] then None
- else Some (false, false, pre_conditions, post_conditions)
+ let pp_content fmt =
+ let pp_contract_opt =
+ let pp_var x fmt = pp_clean_ada_identifier fmt x in
+ let guarantee_post_conditions = List.map pp_var guarantees in
+ let state_pre_conditions, state_post_conditions =
+ if is_machine_statefull m then
+ let input = List.map pp_var_name m.mstep.step_inputs in
+ let output = List.map pp_var_name m.mstep.step_outputs in
+ let args =
+ [ [ pp_old pp_state_name; pp_state_name ] ]
+ @ (if input != [] then [ input ] else [])
+ @ if output != [] then [ output ] else []
+ in
+ let transition fmt =
+ pp_call fmt
+ (pp_access pp_axiomatize_package_name pp_transition_name, args)
+ in
+ let invariant fmt =
+ pp_call fmt
+ ( pp_access pp_axiomatize_package_name pp_invariant_name,
+ [ [ pp_state_name ] ] )
+ in
+ [ invariant ], [ transition; invariant ]
+ else [], []
in
- let pp_guarantee name =
- pp_var_decl
- ( AdaNoMode,
- (fun fmt -> pp_clean_ada_identifier fmt name),
- pp_boolean_type,
- Some (true, false, [], []) )
+ let post_conditions =
+ state_post_conditions @ guarantee_post_conditions
in
- let ghost_public = List.map pp_guarantee guarantees in
- fprintf fmt "@,%a%t%a%a%a@,@,%a;@,@,%t"
- (Utils.fprintf_list ~sep:";@," (fun fmt pp -> pp fmt))
- ghost_public
- (Utils.pp_final_char_if_non_empty ";@,@," ghost_public)
- pp_ifstatefull pp_state_decl_and_reset
- (*Declare the step procedure*)
- (pp_procedure pp_step_procedure_name (build_pp_arg_step m)
- pp_contract_opt)
- AdaNoContent pp_ifstatefull
- (fun fmt -> fprintf fmt ";@,")
- (pp_package pp_axiomatize_package_name [] false)
- (fun fmt ->
- fprintf fmt
- "pragma Annotate (GNATProve, External_Axiomatization);@,\
- @,\
- %a;@,\
- %a;@,\
- %a"
- (*Declare the init predicate*)
- pp_init_predicate ()
- (*Declare the transition predicate*)
- pp_transition_predicate (m_spec_opt, m)
- (*Declare the invariant predicate*)
- pp_invariant_predicate ())
- (*Print the private section*)
- pp_private_section
+ let pre_conditions = state_pre_conditions in
+ if post_conditions = [] && pre_conditions = [] then None
+ else Some (false, false, pre_conditions, post_conditions)
+ in
+ let pp_guarantee name =
+ pp_var_decl
+ ( AdaNoMode,
+ (fun fmt -> pp_clean_ada_identifier fmt name),
+ pp_boolean_type,
+ Some (true, false, [], []) )
in
+ let ghost_public = List.map pp_guarantee guarantees in
+ fprintf fmt "@,%a%a%a%a@,@,%a;@,@,%t"
+ (pp_print_list
+ ~pp_sep:pp_print_semicolon
+ ~pp_epilogue:(fun fmt () -> fprintf fmt ";@,@,")
+ (fun fmt pp -> pp fmt))
+ ghost_public
+ pp_ifstatefull pp_state_decl_and_reset
+ (*Declare the step procedure*)
+ (pp_procedure pp_step_procedure_name (build_pp_arg_step m)
+ pp_contract_opt)
+ AdaNoContent pp_ifstatefull
+ (fun fmt -> fprintf fmt ";@,")
+ (pp_package pp_axiomatize_package_name [] false)
+ (fun fmt ->
+ fprintf fmt
+ "pragma Annotate (GNATProve, External_Axiomatization);@,\
+ @,\
+ %a;@,\
+ %a;@,\
+ %a"
+ (*Declare the init predicate*)
+ pp_init_predicate ()
+ (*Declare the transition predicate*)
+ pp_transition_predicate (m_spec_opt, m)
+ (*Declare the invariant predicate*)
+ pp_invariant_predicate ())
+ (*Print the private section*)
+ pp_private_section
+ in
- let pp_poly_type id = pp_type_decl (pp_polymorphic_type id) AdaPrivate in
- let pp_generics = List.map pp_poly_type polymorphic_types in
+ let pp_poly_type id = pp_type_decl (pp_polymorphic_type id) AdaPrivate in
+ let pp_generics = List.map pp_poly_type polymorphic_types in
- fprintf fmt "@[<v>%a%t%a;@]@."
- (* Include all the subinstance package*)
- (Utils.fprintf_list ~sep:";@," (pp_with AdaNoVisibility))
- machines_to_import
- (Utils.pp_final_char_if_non_empty ";@,@," machines_to_import)
- (*Begin the package*)
- (pp_package (pp_package_name m) pp_generics false)
- pp_content
-end
+ fprintf fmt "@[<v>%a%a;@]@."
+ (* Include all the subinstance package*)
+ (pp_print_list
+ ~pp_sep:pp_print_semicolon
+ ~pp_epilogue:(fun fmt () -> fprintf fmt ";@,@,")
+ (pp_with AdaNoVisibility))
+ machines_to_import
+ (*Begin the package*)
+ (pp_package (pp_package_name m) pp_generics false)
+ pp_content
diff --git a/src/backends/Ada/ada_backend_ads.mli b/src/backends/Ada/ada_backend_ads.mli
index e69de29b..90b11e4a 100644
--- a/src/backends/Ada/ada_backend_ads.mli
+++ b/src/backends/Ada/ada_backend_ads.mli
@@ -0,0 +1,12 @@
+open Utils
+open Machine_code_types
+
+(** Print the package declaration(ads) of a machine. It requires the list of
+ all typed instance. A typed submachine is a (ident, typed_machine) with -
+ ident: the name - typed_machine: a (substitution, machine) with - machine:
+ the submachine struct - substitution the instanciation of all its
+ polymorphic types. @param fmt the formater to print on @param
+ typed_submachines list of all typed submachines of this machine @param m
+ the machine **)
+val pp_file: Format.formatter -> (ident * ((tag * Types.t) list * machine_t)) list
+ * ((machine_t option * ident list) * machine_t) -> unit
diff --git a/src/backends/Ada/ada_backend_common.ml b/src/backends/Ada/ada_backend_common.ml
index fa2f1b88..daff6d65 100644
--- a/src/backends/Ada/ada_backend_common.ml
+++ b/src/backends/Ada/ada_backend_common.ml
@@ -1,3 +1,4 @@
+open Utils
open Format
open Machine_code_types
open Lustre_types
@@ -73,68 +74,71 @@ let pp_package_name machine fmt =
(** Print a type. @param fmt the formater to print on @param type the type **)
let pp_type fmt typ =
- match (Types.repr typ).Types.tdesc with
- | Types.Tbasic Types.Basic.Tint ->
+ let open Types in
+ let t = repr typ in
+ if is_bool_type t then
+ pp_boolean_type fmt
+ else if is_int_type t then
pp_integer_type fmt
- | Types.Tbasic Types.Basic.Treal ->
+ else if is_real_type t then
pp_float_type fmt
- | Types.Tbasic Types.Basic.Tbool ->
- pp_boolean_type fmt
- | Types.Tunivar ->
- pp_polymorphic_type typ.Types.tid fmt
- | Types.Tbasic _ ->
- eprintf "Tbasic@.";
- assert false (*TODO*)
- | Types.Tconst _ ->
- eprintf "Tconst@.";
- assert false (*TODO*)
- | Types.Tclock _ ->
- eprintf "Tclock@.";
- assert false (*TODO*)
- | Types.Tarrow _ ->
- eprintf "Tarrow@.";
- assert false (*TODO*)
- | Types.Ttuple l ->
- eprintf "Ttuple %a @." (Utils.fprintf_list ~sep:" " Types.print_ty) l;
- assert false (*TODO*)
- | Types.Tenum _ ->
- eprintf "Tenum@.";
- assert false (*TODO*)
- | Types.Tstruct _ ->
- eprintf "Tstruct@.";
- assert false (*TODO*)
- | Types.Tarray _ ->
- eprintf "Tarray@.";
- assert false (*TODO*)
- | Types.Tstatic _ ->
- eprintf "Tstatic@.";
- assert false (*TODO*)
- | Types.Tlink _ ->
- eprintf "Tlink@.";
- assert false (*TODO*)
- | Types.Tvar ->
- eprintf "Tvar@.";
- assert false
+ else match t.tdesc with
+ | Tunivar ->
+ pp_polymorphic_type typ.tid fmt
+ | Tbasic _ ->
+ eprintf "Tbasic@.";
+ assert false (*TODO*)
+ | Tconst _ ->
+ eprintf "Tconst@.";
+ assert false (*TODO*)
+ | Tclock _ ->
+ eprintf "Tclock@.";
+ assert false (*TODO*)
+ | Tarrow _ ->
+ eprintf "Tarrow@.";
+ assert false (*TODO*)
+ | Ttuple l ->
+ eprintf "Ttuple %a @." (pp_print_list print_ty) l;
+ assert false (*TODO*)
+ | Tenum _ ->
+ eprintf "Tenum@.";
+ assert false (*TODO*)
+ | Tstruct _ ->
+ eprintf "Tstruct@.";
+ assert false (*TODO*)
+ | Tarray _ ->
+ eprintf "Tarray@.";
+ assert false (*TODO*)
+ | Tstatic _ ->
+ eprintf "Tstatic@.";
+ assert false (*TODO*)
+ | Tlink _ ->
+ eprintf "Tlink@.";
+ assert false (*TODO*)
+ | Tvar ->
+ eprintf "Tvar@.";
+ assert false
(*TODO*)
(*| _ -> eprintf "Type error : %a@." Types.print_ty typ; assert false *)
(** Return a default ada constant for a given type. @param cst_typ the constant
type **)
-let default_ada_cst cst_typ =
- match cst_typ with
- | Types.Basic.Tint ->
+let default_ada_cst t =
+ let open Types in
+ if is_bool_type t then
+ Const_tag tag_false
+ else if is_int_type t then
Const_int 0
- | Types.Basic.Treal ->
+ else if is_real_type t then
Const_real Real.zero
- | Types.Basic.Tbool ->
- Const_tag tag_false
- | _ ->
+ else
assert false
(** Make a default value from a given type. @param typ the type **)
let mk_default_value typ =
- match (Types.repr typ).Types.tdesc with
- | Types.Tbasic t ->
+ let t = Types.repr typ in
+ match t.Types.tdesc with
+ | Types.Tbasic _ ->
mk_val (Cst (default_ada_cst t)) typ
| _ ->
assert false
@@ -156,9 +160,12 @@ let pp_package_name_with_polymorphic substitution machine fmt =
(fun poly1 (poly2, _) -> poly1 = poly2)
polymorphic_types substituion);
let instantiated_types = snd (List.split substitution) in
- fprintf fmt "%t%t%a" (pp_package_name machine)
- (Utils.pp_final_char_if_non_empty "_" instantiated_types)
- (Utils.fprintf_list ~sep:"_" pp_type)
+ fprintf fmt "%t%a"
+ (pp_package_name machine)
+ (pp_print_list
+ ~pp_prologue:(fun fmt () -> pp_print_string fmt "_")
+ ~pp_sep:(fun fmt () -> pp_print_string fmt "_")
+ pp_type)
instantiated_types
(** Print the name of a variable. @param fmt the formater to print on @param id
diff --git a/src/backends/Ada/ada_backend_common.mli b/src/backends/Ada/ada_backend_common.mli
index 426b3e48..a193ba56 100644
--- a/src/backends/Ada/ada_backend_common.mli
+++ b/src/backends/Ada/ada_backend_common.mli
@@ -29,16 +29,16 @@ val pp_var : (string * printer) list -> formatter -> var_decl -> unit
val pp_value : (string * printer) list -> formatter -> value_t -> unit
-val pp_type : formatter -> type_expr -> unit
+val pp_type : formatter -> Types.t -> unit
val pp_var_type : formatter -> var_decl -> unit
val pp_package_name : machine_t -> printer
val pp_package_name_with_polymorphic :
- (int * Types.type_expr) list -> machine_t -> printer
+ (int * Types.t) list -> machine_t -> printer
-val mk_default_value : type_expr -> value_t
+val mk_default_value : Types.t -> value_t
val build_pp_var_decl : parameter_mode -> ada_with -> var_decl -> ada_var_decl
@@ -57,7 +57,7 @@ val build_pp_arg_reset : machine_t -> ada_var_decl list list
val build_pp_state_decl_from_subinstance :
parameter_mode ->
ada_with ->
- string * ((int * Types.type_expr) list * Machine_code_types.machine_t) ->
+ string * ((int * Types.t) list * Machine_code_types.machine_t) ->
ada_var_decl
val build_pp_state_decl : parameter_mode -> ada_with -> ada_var_decl
diff --git a/src/backends/Ada/ada_backend_wrapper.ml b/src/backends/Ada/ada_backend_wrapper.ml
index 0caa505d..3194e73f 100644
--- a/src/backends/Ada/ada_backend_wrapper.ml
+++ b/src/backends/Ada/ada_backend_wrapper.ml
@@ -9,6 +9,7 @@
(* *)
(********************************************************************)
+open Utils
open Format
open Machine_code_types
open Lustre_types
@@ -17,33 +18,32 @@ open Misc_lustre_function
open Ada_printer
open Ada_backend_common
-module Main = struct
- let build_text_io_package_local typ =
- AdaLocalPackage
- ( (fun fmt -> fprintf fmt "%s_IO" typ),
- (fun fmt -> fprintf fmt "Ada.Text_IO.%s_IO" typ),
- [ ((fun fmt -> fprintf fmt "Num"), fun fmt -> fprintf fmt "%s" typ) ] )
+let build_text_io_package_local typ =
+ AdaLocalPackage
+ ( (fun fmt -> fprintf fmt "%s_IO" typ),
+ (fun fmt -> fprintf fmt "Ada.Text_IO.%s_IO" typ),
+ [ ((fun fmt -> fprintf fmt "Num"), fun fmt -> fprintf fmt "%s" typ) ] )
- (** Print the main file calling in a loop the step function of the main
- machine. @param fmt the formater to print on @param machine the main
- machine **)
- let pp_main_adb fmt machine =
- let statefull = is_machine_statefull machine in
+(** Print the main file calling in a loop the step function of the main
+ machine. @param fmt the formater to print on @param machine the main
+ machine **)
+let pp_main_adb fmt machine =
+ let statefull = is_machine_statefull machine in
- let pp_package = pp_package_name_with_polymorphic [] machine in
+ let pp_package = pp_package_name_with_polymorphic [] machine in
- (* Dependances *)
- let text_io = "Ada.Text_IO" in
+ (* Dependances *)
+ let text_io = "Ada.Text_IO" in
- (* Locals *)
- let locals =
+ (* Locals *)
+ let locals =
+ [
[
- [
- build_text_io_package_local "Integer";
- build_text_io_package_local "Float";
- ];
- ]
- @ (if statefull then
+ build_text_io_package_local "Integer";
+ build_text_io_package_local "Float";
+ ];
+ ]
+ @ (if statefull then
[
[
AdaLocalVar
@@ -51,171 +51,163 @@ module Main = struct
(asprintf "%t" pp_state_name, ([], machine)));
];
]
- else [])
- @ (if machine.mstep.step_inputs != [] then
+ else [])
+ @ (if machine.mstep.step_inputs != [] then
[ List.map (build_pp_var_decl_local None) machine.mstep.step_inputs ]
- else [])
- @
- if machine.mstep.step_outputs != [] then
- [ List.map (build_pp_var_decl_local None) machine.mstep.step_outputs ]
- else []
- in
-
- (* Stream instructions *)
- let get_basic var =
- match (Types.repr var.var_type).Types.tdesc with
- | Types.Tbasic x ->
- x
- | _ ->
- assert false
- in
- let pp_read fmt var =
- match get_basic var with
- | Types.Basic.Tbool ->
- fprintf fmt "%t := Integer'Value(Ada.Text_IO.Get_Line) /= 0"
- (pp_var_name var)
- | _ ->
- fprintf fmt "%t := %a'Value(Ada.Text_IO.Get_Line)" (pp_var_name var)
- pp_var_type var
- in
- let pp_write fmt var =
- match get_basic var with
- | Types.Basic.Tbool ->
- fprintf fmt
- "Ada.Text_IO.Put_Line(\"'%t': '\" & (if %t then \"1\" else \"0\") & \
- \"' \")"
- (pp_var_name var) (pp_var_name var)
- | Types.Basic.Tint ->
- fprintf fmt
- "Ada.Text_IO.Put(\"'%t': '\");@,\
- Integer_IO.Put(%t);@,\
- Ada.Text_IO.Put_Line(\"' \")" (pp_var_name var) (pp_var_name var)
- | Types.Basic.Treal ->
- fprintf fmt
- "Ada.Text_IO.Put(\"'%t': '\");@,\
- Float_IO.Put(%t, Fore=>0, Aft=> 15, Exp => 0);@,\
- Ada.Text_IO.Put_Line(\"' \")" (pp_var_name var) (pp_var_name var)
- | Types.Basic.Tstring | Types.Basic.Trat ->
- assert false
- (* Could not be the top level inputs *)
- in
-
- (* Loop instructions *)
- let pp_loop fmt =
- let args =
- pp_state_name
- ::
- List.map pp_var_name
- (machine.mstep.step_inputs @ machine.mstep.step_outputs)
- in
+ else [])
+ @
+ if machine.mstep.step_outputs != [] then
+ [ List.map (build_pp_var_decl_local None) machine.mstep.step_outputs ]
+ else []
+ in
+
+ (* Stream instructions *)
+ let get_type var = Types.repr var.var_type in
+ let pp_read fmt var =
+ if Types.is_bool_type (get_type var) then
+ fprintf fmt "%t := Integer'Value(Ada.Text_IO.Get_Line) /= 0"
+ (pp_var_name var)
+ else
+ fprintf fmt "%t := %a'Value(Ada.Text_IO.Get_Line)" (pp_var_name var)
+ pp_var_type var
+ in
+ let pp_write fmt var =
+ let t = get_type var in
+ if Types.is_bool_type t then
+ fprintf fmt
+ "Ada.Text_IO.Put_Line(\"'%t': '\" & (if %t then \"1\" else \"0\") & \
+ \"' \")"
+ (pp_var_name var) (pp_var_name var)
+ else if Types.is_int_type t then
fprintf fmt
- "while not Ada.Text_IO.End_Of_File loop@,\
- \ @[<v>%a;@,\
- %a;@,\
- %a;@]@,\
- end loop"
- (Utils.fprintf_list ~sep:";@," pp_read)
- machine.mstep.step_inputs pp_call
- (pp_package_access (pp_package, pp_step_procedure_name), [ args ])
- (Utils.fprintf_list ~sep:";@," pp_write)
- machine.mstep.step_outputs
+ "Ada.Text_IO.Put(\"'%t': '\");@,\
+ Integer_IO.Put(%t);@,\
+ Ada.Text_IO.Put_Line(\"' \")" (pp_var_name var) (pp_var_name var)
+ else if Types.is_real_type t then
+ fprintf fmt
+ "Ada.Text_IO.Put(\"'%t': '\");@,\
+ Float_IO.Put(%t, Fore=>0, Aft=> 15, Exp => 0);@,\
+ Ada.Text_IO.Put_Line(\"' \")" (pp_var_name var) (pp_var_name var)
+ else
+ assert false
+ (* Could not be the top level inputs *)
+ in
+
+ (* Loop instructions *)
+ let pp_loop fmt =
+ let args =
+ pp_state_name
+ ::
+ List.map pp_var_name
+ (machine.mstep.step_inputs @ machine.mstep.step_outputs)
in
-
- (* Print the file *)
- let instrs =
- (if statefull then
+ fprintf fmt
+ "while not Ada.Text_IO.End_Of_File loop@,\
+ \ @[<v>%a;@,\
+ %a;@,\
+ %a;@]@,\
+ end loop"
+ (pp_print_list ~pp_sep:pp_print_semicolon pp_read)
+ machine.mstep.step_inputs pp_call
+ (pp_package_access (pp_package, pp_step_procedure_name), [ args ])
+ (pp_print_list ~pp_sep:pp_print_semicolon pp_write)
+ machine.mstep.step_outputs
+ in
+
+ (* Print the file *)
+ let instrs =
+ (if statefull then
[
(fun fmt ->
- pp_call fmt
- ( pp_package_access (pp_package, pp_reset_procedure_name),
- [ [ pp_state_name ] ] ));
+ pp_call fmt
+ ( pp_package_access (pp_package, pp_reset_procedure_name),
+ [ [ pp_state_name ] ] ));
]
- else [])
- @ [ pp_loop ]
- in
- fprintf fmt "@[<v>%a;@,%a;@,@,%a;@]" (pp_with AdaPrivate) (pp_str text_io)
- (pp_with AdaPrivate) (pp_package_name machine)
- (pp_procedure pp_main_procedure_name [] None)
- (AdaProcedureContent (locals, instrs))
-
- (** Print the name of the ada project configuration file. @param fmt the
- formater to print on @param main_machine the machine associated to the
- main node **)
- let pp_project_configuration_name fmt basename = fprintf fmt "%s.adc" basename
-
- (** Print the project configuration file. @param fmt the formater to print on
- **)
- let pp_project_configuration_file fmt = fprintf fmt "pragma SPARK_Mode (On);"
-
- (** Print the name of the ada project file. @param base_name name of the
- lustre file @param fmt the formater to print on **)
- let pp_project_name basename fmt = fprintf fmt "%s.gpr" basename
-
- let pp_for_single name arg fmt = fprintf fmt "for %s use \"%s\"" name arg
-
- let pp_for name args fmt =
- fprintf fmt "for %s use (@[%a@])" name
- (Utils.fprintf_list ~sep:",@ " (fun fmt arg -> fprintf fmt "\"%s\"" arg))
- args
-
- let pp_content fmt lines =
- fprintf fmt " @[<v>%a%t@]"
- (Utils.fprintf_list ~sep:";@," (fun fmt pp -> fprintf fmt "%t" pp))
- lines
- (Utils.pp_final_char_if_non_empty ";" lines)
-
- let pp_package name lines fmt =
- fprintf fmt "package %s is@,%a@,end %s" name pp_content lines name
-
- (** Print the gpr project file, if there is a machine in machine_opt then an
- executable project is made else it is a library. @param fmt the formater
- to print on @param machine_opt the main machine option **)
- let pp_project_file machines basename fmt machine_opt =
- let adbs =
- List.map (asprintf "%a" (pp_machine_filename "adb")) machines
- @
- match machine_opt with
- | None ->
- []
- | Some m ->
- [ asprintf "%a" pp_main_filename m ]
- in
- let project_name =
- basename ^ if machine_opt = None then "_lib" else "_exe"
- in
- fprintf fmt "%sproject %s is@,%a@,end %s;"
- (if machine_opt = None then "library " else "")
- project_name pp_content
- ((match machine_opt with
- | None ->
+ else [])
+ @ [ pp_loop ]
+ in
+ fprintf fmt "@[<v>%a;@,%a;@,@,%a;@]" (pp_with AdaPrivate) (pp_str text_io)
+ (pp_with AdaPrivate) (pp_package_name machine)
+ (pp_procedure pp_main_procedure_name [] None)
+ (AdaProcedureContent (locals, instrs))
+
+(** Print the name of the ada project configuration file. @param fmt the
+ formater to print on @param main_machine the machine associated to the
+ main node **)
+let pp_project_configuration_name fmt basename = fprintf fmt "%s.adc" basename
+
+(** Print the project configuration file. @param fmt the formater to print on
+ **)
+let pp_project_configuration_file fmt = fprintf fmt "pragma SPARK_Mode (On);"
+
+(** Print the name of the ada project file. @param base_name name of the
+ lustre file @param fmt the formater to print on **)
+let pp_project_name basename fmt = fprintf fmt "%s.gpr" basename
+
+let pp_for_single name arg fmt = fprintf fmt "for %s use \"%s\"" name arg
+
+let pp_for name args fmt =
+ fprintf fmt "for %s use (@[%a@])" name
+ (pp_comma_list (fun fmt arg -> fprintf fmt "\"%s\"" arg))
+ args
+
+let pp_content fmt lines =
+ fprintf fmt " @[<v>%a%a@]"
+ (pp_print_list ~pp_sep:pp_print_semicolon (fun fmt pp -> fprintf fmt "%t" pp))
+ lines
+ (if lines = [] then pp_print_nothing else pp_print_semicolon) ()
+
+let pp_package name lines fmt =
+ fprintf fmt "package %s is@,%a@,end %s" name pp_content lines name
+
+(** Print the gpr project file, if there is a machine in machine_opt then an
+ executable project is made else it is a library. @param fmt the formater
+ to print on @param machine_opt the main machine option **)
+let pp_project_file machines basename fmt machine_opt =
+ let adbs =
+ List.map (asprintf "%a" (pp_machine_filename "adb")) machines
+ @
+ match machine_opt with
+ | None ->
+ []
+ | Some m ->
+ [ asprintf "%a" pp_main_filename m ]
+ in
+ let project_name =
+ basename ^ if machine_opt = None then "_lib" else "_exe"
+ in
+ fprintf fmt "%sproject %s is@,%a@,end %s;"
+ (if machine_opt = None then "library " else "")
+ project_name pp_content
+ ((match machine_opt with
+ | None ->
+ [
+ pp_for_single "Library_Name" basename;
+ pp_for_single "Library_Dir" "lib";
+ ]
+ | Some _ ->
+ [
+ pp_for "Main" [ asprintf "%t" pp_main_procedure_name ];
+ pp_for_single "Exec_Dir" "bin";
+ ])
+ @ [
+ pp_for_single "Object_Dir" "obj";
+ pp_for "Source_Files" adbs;
+ pp_package "Builder"
[
- pp_for_single "Library_Name" basename;
- pp_for_single "Library_Dir" "lib";
- ]
- | Some _ ->
+ pp_for_single "Global_Configuration_Pragmas"
+ (asprintf "%a" pp_project_configuration_name basename);
+ ];
+ pp_package "Prove"
[
- pp_for "Main" [ asprintf "%t" pp_main_procedure_name ];
- pp_for_single "Exec_Dir" "bin";
- ])
- @ [
- pp_for_single "Object_Dir" "obj";
- pp_for "Source_Files" adbs;
- pp_package "Builder"
- [
- pp_for_single "Global_Configuration_Pragmas"
- (asprintf "%a" pp_project_configuration_name basename);
- ];
- pp_package "Prove"
- [
- pp_for "Switches"
- [
- "--mode=prove";
- "--report=statistics";
- "--proof=per_check";
- "--warnings=continue";
- ];
- pp_for_single "Proof_Dir" (asprintf "proof");
- ];
- ])
- project_name
-end
+ pp_for "Switches"
+ [
+ "--mode=prove";
+ "--report=statistics";
+ "--proof=per_check";
+ "--warnings=continue";
+ ];
+ pp_for_single "Proof_Dir" (asprintf "proof");
+ ];
+ ])
+ project_name
diff --git a/src/backends/Ada/ada_backend_wrapper.mli b/src/backends/Ada/ada_backend_wrapper.mli
index e69de29b..db8a9481 100644
--- a/src/backends/Ada/ada_backend_wrapper.mli
+++ b/src/backends/Ada/ada_backend_wrapper.mli
@@ -0,0 +1,26 @@
+open Utils
+open Format
+open Machine_code_types
+
+(** Print the main file calling in a loop the step function of the main
+ machine. @param fmt the formater to print on @param machine the main
+ machine **)
+val pp_main_adb: formatter -> machine_t -> unit
+
+(** Print the name of the ada project file. @param base_name name of the
+ lustre file @param fmt the formater to print on **)
+val pp_project_name: string -> formatter -> unit
+
+(** Print the gpr project file, if there is a machine in machine_opt then an
+ executable project is made else it is a library. @param fmt the formater
+ to print on @param machine_opt the main machine option **)
+val pp_project_file: machine_t list -> string -> formatter -> machine_t option -> unit
+
+(** Print the name of the ada project configuration file. @param fmt the
+ formater to print on @param main_machine the machine associated to the
+ main node **)
+val pp_project_configuration_name: formatter -> string -> unit
+
+(** Print the project configuration file. @param fmt the formater to print on
+ **)
+val pp_project_configuration_file: formatter -> unit
diff --git a/src/backends/Ada/ada_printer.ml b/src/backends/Ada/ada_printer.ml
index b6f40235..3443fa9f 100644
--- a/src/backends/Ada/ada_printer.ml
+++ b/src/backends/Ada/ada_printer.ml
@@ -1,3 +1,4 @@
+open Utils
open Format
(** Represent the possible mode for a type of a procedure parameter **)
@@ -78,28 +79,32 @@ let pp_float_type fmt = fprintf fmt "Float"
(** Print the boolean type name. @param fmt the formater to print on **)
let pp_boolean_type fmt = fprintf fmt "Boolean"
-let pp_group ~sep pp_list fmt =
+let pp_group ~pp_sep pp_list fmt =
assert (pp_list != []);
- fprintf fmt "@[%a@]" (Utils.fprintf_list ~sep (fun fmt pp -> pp fmt)) pp_list
+ fprintf fmt "@[%a@]" (pp_print_list ~pp_sep (fun fmt pp -> pp fmt)) pp_list
-let pp_args ~sep fmt = function
+let pp_args ~pp_sep fmt = function
| [] ->
fprintf fmt ""
| args ->
fprintf fmt " (@[<v>%a)@]"
- (Utils.fprintf_list ~sep (fun fmt pp -> pp fmt))
+ (pp_print_list ~pp_sep (fun fmt pp -> pp fmt))
args
let pp_block fmt pp_item_list =
- fprintf fmt "%t@[<v>%a@]%t"
- (Utils.pp_final_char_if_non_empty " " pp_item_list)
- (Utils.fprintf_list ~sep:";@," (fun fmt pp -> pp fmt))
+ pp_print_list
+ ~pp_open_box:pp_open_vbox0
+ ~pp_prologue:(fun fmt () -> pp_print_string fmt " ")
+ ~pp_epilogue:pp_print_semicolon
+ ~pp_sep:pp_print_semicolon (fun fmt pp -> pp fmt)
+ fmt
pp_item_list
- (Utils.pp_final_char_if_non_empty ";@," pp_item_list)
-let pp_and l fmt = fprintf fmt "(%t)" (pp_group ~sep:"@ and then " l)
+let pp_and l fmt =
+ fprintf fmt "(%t)" (pp_group ~pp_sep:(fun fmt () -> fprintf fmt "@ and then ") l)
-let pp_or l fmt = fprintf fmt "(%t)" (pp_group ~sep:"@ or " l)
+let pp_or l fmt =
+ fprintf fmt "(%t)" (pp_group ~pp_sep:(fun fmt () -> fprintf fmt "@ or ") l)
let pp_ada_with fmt = function
| None ->
@@ -117,8 +122,8 @@ let pp_ada_with fmt = function
let pp_import fmt =
if not import then fprintf fmt ""
else
- fprintf fmt " Import%t"
- (Utils.pp_final_char_if_non_empty ",@," contract)
+ fprintf fmt " Import%a"
+ (if contract = [] then pp_print_nothing else pp_print_comma) ()
in
let pp_aspect aspect fmt pps =
if pps = [] then fprintf fmt ""
@@ -184,23 +189,23 @@ and pp_content pp_name fmt = function
fprintf fmt " is@, @[<v 2>(%t)@]" pp_content
| AdaProcedureContent (local_list, pp_instr_list) ->
fprintf fmt " is@,%abegin@,%aend %t" pp_block
- (List.map (fun l -> pp_group ~sep:";@;" (List.map pp_local l)) local_list)
+ (List.map (fun l -> pp_group ~pp_sep:pp_print_semicolon (List.map pp_local l)) local_list)
pp_block pp_instr_list pp_name
| AdaRecord var_list ->
assert (var_list != []);
let pp_lists = apply_var_decl_lists var_list in
fprintf fmt " is@, @[<v>record@, @[<v>%a@]@,end record@]" pp_block
- (List.map (pp_group ~sep:";@;") pp_lists)
+ (List.map (pp_group ~pp_sep:pp_print_semicolon) pp_lists)
| AdaPackageInstanciation (pp_name, instanciations) ->
- fprintf fmt " is new %t%a" pp_name (pp_args ~sep:",@,")
+ fprintf fmt " is new %t%a" pp_name (pp_args ~pp_sep:pp_print_comma)
(List.map pp_generic_instanciation instanciations)
and pp_def fmt
(pp_generics, kind_def, pp_name, args, pp_type_opt, content, pp_with_opt) =
let pp_arg_lists = apply_var_decl_lists args in
fprintf fmt "%a%a %t%a%a%a%a" pp_generic pp_generics pp_kind_def kind_def
- pp_name (pp_args ~sep:";@,")
- (List.map (pp_group ~sep:";@,") pp_arg_lists)
+ pp_name (pp_args ~pp_sep:pp_print_semicolon)
+ (List.map (pp_group ~pp_sep:pp_print_semicolon) pp_arg_lists)
(pp_opt "return") pp_type_opt (pp_content pp_name) content pp_ada_with
pp_with_opt
@@ -387,8 +392,8 @@ let pp_oneline_comment fmt s =
fprintf fmt "-- %s@," s
let pp_call fmt (pp_name, args) =
- fprintf fmt "%t%a" pp_name (pp_args ~sep:",@ ")
- (List.map (pp_group ~sep:",@,") args)
+ fprintf fmt "%t%a" pp_name (pp_args ~pp_sep:pp_print_comma)
+ (List.map (pp_group ~pp_sep:pp_print_comma) args)
(** Print the complete name of variable. @param m the machine to check if it is
memory @param fmt the formater to print on @param var the variable **)
diff --git a/src/backends/Ada/misc_lustre_function.mli b/src/backends/Ada/misc_lustre_function.mli
index e69de29b..74a4f7df 100644
--- a/src/backends/Ada/misc_lustre_function.mli
+++ b/src/backends/Ada/misc_lustre_function.mli
@@ -0,0 +1,41 @@
+open Utils
+open Machine_code_types
+
+val is_machine_statefull: machine_t -> bool
+val is_arrow: machine_t -> bool
+
+(** Find all polymorphic type : Types.Tunivar in a machine. @param machine the
+ machine @return a list of id corresponding to polymorphic type **)
+val find_all_polymorphic_type: machine_t -> int list
+
+(** Test if two types are the same. @param typ1 the first type @param typ2 the
+ second type **)
+val pp_eq_type: Types.t -> Types.t -> bool
+
+(** Check if a submachine is statefull. @param submachine a submachine @return
+ true if the submachine is statefull **)
+val is_submachine_statefull: 'a * ('b * machine_t) -> bool
+
+(** Extract from a machine the instance corresponding to the identifier, assume
+ that the identifier exists in the instances of the machine.
+
+ @param identifier the instance identifier @param machine a machine @return
+ the instance of machine.minstances corresponding to identifier **)
+val get_instance: 'a -> ('a * 'b) list -> 'b
+
+val build_if: 'a -> ident -> 'b -> ('c * 'b) list -> bool * 'a * 'b * 'b option
+
+(** Extract from a machine list the one corresponding to the given instance.
+ assume that the machine is in the list. @param machines list of all machines
+ @param instance instance of a machine @return the machine corresponding to
+ hte given instance **)
+val get_machine: machine_t list -> 'a * (Lustre_types.top_decl * 'b) -> machine_t
+
+(** Extract from a subinstance that can have polymorphic type the instantiation
+ of all its polymorphic type instanciation for a given machine. It searches
+ the step calls and extract a substitution for all polymorphic type from it.
+ @param machine the machine which instantiate the subinstance @param ident
+ the identifier of the instance which permits to find the step call @param
+ submachine the machine corresponding to the subinstance @return the
+ correspondance between polymorphic type id and their instantiation **)
+val get_substitution: machine_t -> ident -> machine_t -> (int * Types.t) list
diff --git a/src/backends/Ada/misc_printer.mli b/src/backends/Ada/misc_printer.mli
index df403db0..1fc5de74 100644
--- a/src/backends/Ada/misc_printer.mli
+++ b/src/backends/Ada/misc_printer.mli
@@ -1 +1,10 @@
-type printer = Format.formatter -> unit
+open Format
+
+type printer = formatter -> unit
+
+val pp_str: string -> printer
+
+(** Print a filename by lowercasing the base and appending an extension. @param
+ extension the extension to append to the package name @param fmt the
+ formatter @param pp_name the file base name printer **)
+val pp_filename: string -> formatter -> printer -> unit
diff --git a/src/backends/C/c_backend.ml b/src/backends/C/c_backend.ml
index f3008056..622d69c7 100644
--- a/src/backends/C/c_backend.ml
+++ b/src/backends/C/c_backend.ml
@@ -32,8 +32,8 @@ let with_main_node machines node f =
| None ->
let open Error in
Global.main_node := node;
- Format.eprintf "Code generation error: %a@." pp_error_msg Main_not_found;
- raise (Error (Location.dummy_loc, Main_not_found))
+ Format.eprintf "Code generation error: %a@." pp Main_not_found;
+ raise (Error (Location.dummy, Main_not_found))
| Some m ->
f m
@@ -100,19 +100,18 @@ let gen_files
(* close_out makefile_out *)
let print_c_header basename =
+ let open Options in
let header_m =
- match !Options.spec with
- | "no" ->
- C_backend_header.((module EmptyMod : MODIFIERS_HDR))
- | "acsl" ->
- C_backend_header.((module C_backend_spec.HdrMod : MODIFIERS_HDR))
- | "c" ->
+ match !spec with
+ | SpecNo ->
+ C_backend_header.(module EmptyMod : MODIFIERS_HDR)
+ | SpecACSL ->
+ C_backend_header.(module C_backend_spec.HdrMod : MODIFIERS_HDR)
+ | SpecC ->
assert false (* not implemented yet *)
- | _ ->
- assert false
in
- let module Header = C_backend_header.Main ((val header_m)) in
- let destname = !Options.dest_dir ^ "/" ^ basename in
+ let module Header = C_backend_header.Main (val header_m) in
+ let destname = !dest_dir ^ "/" ^ basename in
(* Generating H file *)
let lusic = Lusic.read_lusic destname ".lusic" in
let header_file = destname ^ ".h" in
@@ -122,22 +121,21 @@ let print_c_header basename =
let translate_to_c generate_c_header basename prog machines dependencies =
let header_m, source_m, source_main_m, makefile_m =
- match !Options.spec with
- | "no" ->
+ let open Options in
+ match !spec with
+ | SpecNo ->
( C_backend_header.((module EmptyMod : MODIFIERS_HDR)),
C_backend_src.((module EmptyMod : MODIFIERS_SRC)),
C_backend_main.((module EmptyMod : MODIFIERS_MAINSRC)),
C_backend_makefile.((module EmptyMod : MODIFIERS_MKF)) )
- | "acsl" ->
+ | SpecACSL ->
let open C_backend_spec in
( C_backend_header.((module HdrMod : MODIFIERS_HDR)),
C_backend_src.((module SrcMod : MODIFIERS_SRC)),
C_backend_main.((module EmptyMod : MODIFIERS_MAINSRC)),
C_backend_makefile.((module MakefileMod : MODIFIERS_MKF)) )
- | "c" ->
+ | SpecC ->
assert false (* not implemented yet *)
- | _ ->
- assert false
in
let module Header = C_backend_header.Main ((val header_m)) in
let module Source = C_backend_src.Main ((val source_m)) in
diff --git a/src/backends/C/c_backend.mli b/src/backends/C/c_backend.mli
index e69de29b..b358eb0e 100644
--- a/src/backends/C/c_backend.mli
+++ b/src/backends/C/c_backend.mli
@@ -0,0 +1,6 @@
+open Lustre_types
+open Machine_code_types
+
+val translate_to_c: bool -> string -> program_t -> machine_t list -> dep_t list -> unit
+
+val print_c_header: string -> unit
diff --git a/src/backends/C/c_backend_common.ml b/src/backends/C/c_backend_common.ml
index 454f2bff..b6d782e8 100644
--- a/src/backends/C/c_backend_common.ml
+++ b/src/backends/C/c_backend_common.ml
@@ -9,7 +9,8 @@
(* *)
(********************************************************************)
-open Utils.Format
+open Utils
+open Format
open Lustre_types
open Corelang
open Machine_code_types
@@ -88,8 +89,8 @@ let mk_call_var_decl loc id =
{
var_id = id;
var_orig = false;
- var_dec_type = mktyp Location.dummy_loc Tydec_any;
- var_dec_clock = mkclock Location.dummy_loc Ckdec_any;
+ var_dec_type = mktyp Location.dummy Tydec_any;
+ var_dec_clock = mkclock Location.dummy Ckdec_any;
var_dec_const = false;
var_dec_value = None;
var_parent_nodeid = None;
@@ -237,7 +238,7 @@ let pp_c_basic_type_desc t_desc =
(* Not a basic C type. Do not handle arrays or pointers *)
let pp_basic_c_type ?(pp_c_basic_type_desc = pp_c_basic_type_desc)
- ?(var_opt = None) fmt t =
+ ?var_opt fmt t =
match var_opt with
| Some v when Machine_types.is_exportable v ->
Machine_types.pp_c_var_type fmt v
@@ -248,7 +249,7 @@ let pp_c_type ?pp_c_basic_type_desc ?var_opt var_id fmt t =
let rec aux t pp_suffix =
if is_basic_c_type t then
fprintf fmt "%a %s%a"
- (pp_basic_c_type ?pp_c_basic_type_desc ~var_opt)
+ (pp_basic_c_type ?pp_c_basic_type_desc ?var_opt)
t var_id pp_suffix ()
else
let open Types in
@@ -512,8 +513,10 @@ type loop_index = LVar of ident | LInt of int ref | LAcc of value_t
(Access (v, Cst (Const_int !r))) q | _ , LVar i :: q -> value_offsets (Access
(v, Var i)) q *)
(* Computes the list of nested loop variables together with their dimension
- bounds. - LInt r stands for loop expansion (no loop variable, but int loop
- index) - LVar v stands for loop variable v *)
+ bounds.
+ * - LInt r stands for loop expansion (no loop variable, but int loop
+ index)
+ * - LVar v stands for loop variable v *)
let rec mk_loop_variables m ty depth =
match (Types.repr ty).Types.tdesc, depth with
| Types.Tarray (d, ty'), 0 ->
@@ -592,7 +595,7 @@ let rec pp_value_suffix ?(indirect = true) m self var_type loop_vars pp_var fmt
in
match loop_vars, value.value_desc with
| (x, LAcc i) :: q, _ when is_const_index i ->
- let r = ref (Dimension.size_const_dimension (dimension_of_value i)) in
+ let r = ref (Dimension.size_const (dimension_of_value i)) in
pp_value_suffix ~indirect m self var_type ((x, LInt r) :: q) pp_var fmt
value
| (_, LInt r) :: q, Cst (Const_array cl) ->
@@ -664,7 +667,7 @@ let rec pp_value_suffix ?(indirect = true) m self var_type loop_vars pp_var fmt
* pp_c_decl_struct_var
* fmt m.mmemory *)
-let print_machine_struct ?(ghost = false) fmt m =
+let pp_machine_struct ?(ghost = false) fmt m =
if not (fst (Machine_code_common.get_stateless_status m)) then
(* Define struct *)
fprintf fmt "@[<v 2>%a {@,_Bool _reset;%a%a@]@,};"
@@ -693,20 +696,20 @@ let print_machine_struct ?(ghost = false) fmt m =
(* Prototype Printing functions *)
(********************************************************************************************)
-let print_global_init_prototype fmt baseNAME =
+let pp_global_init_prototype fmt baseNAME =
fprintf fmt "void %a ()" pp_global_init_name baseNAME
-let print_global_clear_prototype fmt baseNAME =
+let pp_global_clear_prototype fmt baseNAME =
fprintf fmt "void %a ()" pp_global_clear_name baseNAME
-let print_alloc_prototype fmt (name, static) =
+let pp_alloc_prototype fmt (name, static) =
fprintf fmt "%a * %a %a"
(pp_machine_memtype_name ~ghost:false)
name pp_machine_alloc_name name
(pp_print_parenthesized pp_c_decl_input_var)
static
-let print_dealloc_prototype fmt name =
+let pp_dealloc_prototype fmt name =
fprintf fmt "void %a (%a * _alloc)" pp_machine_dealloc_name name
(pp_machine_memtype_name ~ghost:false)
name
@@ -783,9 +786,9 @@ module Protos (Mod : MODIFIERS_GHOST_PROTO) = struct
outputs
end
-let print_import_prototype fmt dep = fprintf fmt "#include \"%s.h\"" dep.name
+let pp_import_prototype fmt dep = fprintf fmt "#include \"%s.h\"" dep.name
-let print_import_alloc_prototype fmt dep =
+let pp_import_alloc_prototype fmt dep =
if dep.is_stateful then fprintf fmt "#include \"%s_alloc.h\"" dep.name
let pp_c_var m self pp_var fmt var =
@@ -858,7 +861,7 @@ let pp_file file_suffix fmt (typ, arg) =
file_suffix typ arg file_suffix
let pp_put_var fmt file_suffix name var_type var_id =
- let pp_file = pp_print_file ("out" ^ file_suffix) in
+ let pp_file = pp_file ("out" ^ file_suffix) in
let unclocked_t = Types.unclock_type var_type in
fprintf fmt "@[<v>%a@]"
(fun fmt () ->
@@ -937,7 +940,7 @@ let pp_assign m self pp_var fmt (var, value) =
| (d, LInt r) :: q ->
(*eprintf "pp_aux %a %d@." Dimension.pp_dimension d (!r);*)
let typ' = Types.array_element_type typ in
- let szl = Utils.enumerate (Dimension.size_const_dimension d) in
+ let szl = Utils.enumerate (Dimension.size_const d) in
fprintf fmt "@[<v 2>{@,%a@]@,}"
(pp_print_list (fun fmt i ->
r := i;
diff --git a/src/backends/C/c_backend_common.mli b/src/backends/C/c_backend_common.mli
index 98fb6dc2..bd7c9abc 100644
--- a/src/backends/C/c_backend_common.mli
+++ b/src/backends/C/c_backend_common.mli
@@ -1,5 +1,146 @@
open Utils
+open Format
+open Lustre_types
+open Machine_code_types
-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
+val pp_file_decl: formatter -> ident -> int -> unit
+val pp_file_open: formatter -> ident -> int -> string
+val pp_put_var: formatter -> string -> ident -> Types.t -> ident -> unit
+val pp_ptr: formatter -> ident -> unit
+val pp_machine_set_reset_name: formatter -> ident -> unit
+val pp_machine_clear_reset_name: formatter -> ident -> unit
+val pp_machine_init_name: formatter -> ident -> unit
+val pp_machine_clear_name: formatter -> ident -> unit
+val pp_machine_step_name: formatter -> ident -> unit
+val pp_machine_alloc_name: formatter -> ident -> unit
+val pp_machine_static_alloc_name: formatter -> ident -> unit
+val pp_machine_dealloc_name: formatter -> ident -> unit
+val pp_global_init_name: formatter -> ident -> unit
+val pp_global_clear_name: formatter -> ident -> unit
+val pp_machine_static_declare_name: formatter -> ident -> unit
+val pp_machine_static_link_name: formatter -> ident -> unit
+val pp_global_init_prototype: formatter -> ident -> unit
+val pp_global_clear_prototype: formatter -> ident -> unit
+val pp_alloc_prototype: formatter -> ident * var_decl list -> unit
+val pp_dealloc_prototype: formatter -> ident -> unit
+val pp_import_prototype: formatter -> dep_t -> unit
+val pp_import_alloc_prototype: formatter -> dep_t -> unit
+val pp_c_var_read: ?test_output:bool -> machine_t -> formatter -> var_decl -> unit
+val pp_c_var_write: machine_t -> formatter -> var_decl -> unit
+val pp_c_var: machine_t -> ident -> (formatter -> var_decl -> unit) -> formatter -> var_decl -> unit
+val pp_c_dimension: formatter -> Dimension.t -> unit
+val pp_label: formatter -> label -> unit
+val pp_c_tag: formatter -> label -> unit
+val pp_reset_assign: ident -> formatter -> bool -> unit
+val pp_assign: machine_t -> ident -> (formatter -> var_decl -> unit) -> formatter -> var_decl * value_t -> unit
+val pp_c_type: ?pp_c_basic_type_desc:(Types.t -> string) -> ?var_opt:var_decl ->
+ ident -> formatter -> Types.t -> unit
+val pp_basic_c_type: ?pp_c_basic_type_desc:(Types.t -> string) -> ?var_opt:var_decl -> formatter -> Types.t -> unit
+val pp_machine_memtype_name: ?ghost:bool -> formatter -> ident -> unit
+val pp_array_suffix: formatter -> ident list -> unit
+val pp_print_version: formatter -> unit -> unit
+val pp_machine_struct: ?ghost:bool -> formatter -> machine_t -> unit
+val pp_reset_flag: ?indirect:bool -> (formatter -> 'a -> unit) -> formatter -> 'a -> unit
+val pp_reset_flag': ?indirect:bool -> formatter -> ident -> unit
+val pp_machine_decl: ?ghost:bool -> (formatter -> 'a -> unit) -> formatter -> ident * 'a -> unit
+val pp_machine_decl': ?ghost:bool -> formatter -> ident * ident -> unit
+val pp_file: ident -> formatter -> ident * ident -> unit
+val pp_basic_lib_fun: bool -> ident -> (formatter -> 'a -> unit) -> formatter -> 'a list -> unit
+val pp_c_decl_input_var: formatter -> var_decl -> unit
+
+(* Prints a value expression [v], with internal function calls only. [pp_var] is
+ a printer for variables (typically [pp_c_var_read]), but an offset suffix may
+ be added for array variables *)
+val pp_c_val: machine_t -> ident -> (formatter -> var_decl -> unit) -> formatter -> value_t -> unit
+
+ (* Prints a constant value *)
+val pp_c_const: formatter -> constant -> unit
+
+(* Declaration of a local/mem variable: - if it's an array/matrix/etc, its
+ size(s) should be known in order to statically allocate memory, so we print
+ the full type *)
+val pp_c_decl_local_var: ?pp_c_basic_type_desc:(Types.t -> string) -> machine_t -> formatter -> var_decl -> unit
+
+(* type directed initialization: useless wrt the lustre compilation model,
+ except for MPFR injection, where values are dynamically allocated *)
+val pp_initialize: machine_t -> ident -> (formatter -> var_decl -> unit) -> formatter -> var_decl -> unit
+
+(* type directed clear: useless wrt the lustre compilation model, except for
+ MPFR injection, where values are dynamically allocated *)
+val pp_clear: machine_t -> ident -> (formatter -> var_decl -> unit) -> formatter -> var_decl -> unit
+
+val mk_call_var_decl: Location.t -> ident -> var_decl
+
+val pp_c_basic_type_desc: Types.t -> string
+
+val has_c_prototype: ident -> dep_t list -> bool
+
+val reset_label: label
+
+type loop_index = LVar of ident | LInt of int ref | LAcc of value_t
+
+val mk_loop_var: machine_t -> unit -> ident
+
+(* Computes the list of nested loop variables together with their dimension
+ bounds.
+ * - LInt r stands for loop expansion (no loop variable, but int loop
+ index)
+ * - LVar v stands for loop variable v *)
+val mk_loop_variables: machine_t -> Types.t -> int -> (Dimension.t * loop_index) list
+
+val reset_loop_counter: unit -> unit
+
+val reorder_loop_variables: (Dimension.t * loop_index) list -> (Dimension.t * loop_index) list
+
+ (* Prints a [value] of type [var_type] indexed by the suffix list [loop_vars] *)
+val pp_value_suffix: ?indirect:bool -> machine_t -> ident -> Types.t ->
+ (Dimension.t * loop_index) list -> (formatter -> var_decl -> unit) -> formatter -> value_t -> unit
+
+(* Generation of a non-clashing name for the self memory variable (for step and
+ reset functions) *)
+val mk_self: machine_t -> ident
+val mk_mem: machine_t -> ident
+val mk_mem_in: machine_t -> ident
+val mk_mem_out: machine_t -> ident
+val mk_mem_reset: machine_t -> ident
+
+(* Generation of a non-clashing name for the attribute variable of static
+ allocation macro *)
+val mk_attribute: machine_t -> ident
+
+(* Generation of a non-clashing name for the instance variable of static
+ allocation macro *)
+val mk_instance: machine_t -> ident
+
+val mpfr_vars: var_decl list -> var_decl list
+val mpfr_consts: const_desc list -> const_desc list
+
+val reset_flag_name: string
+
+val file_to_module_name: string -> string
+
+val protect_filename: string -> string
+
+(* Computes the depth to which multi-dimension array assignments should be
+ expanded. It equals the maximum number of nested static array constructions
+ accessible from root [v]. *)
+val expansion_depth: value_t -> int
+
+module type MODIFIERS_GHOST_PROTO = sig
+ val pp_ghost_parameters :
+ ?cut:bool ->
+ formatter ->
+ (string * (formatter -> string -> unit)) list ->
+ unit
+end
+
+module EmptyGhostProto : MODIFIERS_GHOST_PROTO
+
+module Protos (Mod : MODIFIERS_GHOST_PROTO): sig
+ val print_stateless_prototype: formatter -> ident * var_decl list * var_decl list -> unit
+ val print_clear_reset_prototype: ident -> ident -> formatter -> ident * var_decl list -> unit
+ val print_set_reset_prototype: ident -> ident -> formatter -> ident * var_decl list -> unit
+ val print_step_prototype: ident -> ident -> formatter -> ident * var_decl list * var_decl list -> unit
+ val print_init_prototype: ident -> formatter -> ident * var_decl list -> unit
+ val print_clear_prototype: ident -> formatter -> ident * var_decl list -> unit
+end
diff --git a/src/backends/C/c_backend_header.ml b/src/backends/C/c_backend_header.ml
index 6343c0aa..64255452 100644
--- a/src/backends/C/c_backend_header.ml
+++ b/src/backends/C/c_backend_header.ml
@@ -16,6 +16,8 @@ open Machine_code_types
open Machine_code_common
open C_backend_common
+module Mpfr = Lustrec_mpfr
+
(********************************************************************************************)
(* Header Printing functions *)
(********************************************************************************************)
@@ -23,7 +25,7 @@ open C_backend_common
module type MODIFIERS_HDR = sig
module GhostProto : MODIFIERS_GHOST_PROTO
- val print_machine_decl_prefix : Format.formatter -> machine_t -> unit
+ val print_machine_decl_prefix : formatter -> machine_t -> unit
val pp_import_arrow : formatter -> unit -> unit
end
@@ -174,9 +176,9 @@ functor
print_static_link_macro macro print_static_alloc_macro macro
else
(* Dynamic allocation *)
- fprintf fmt "extern %a;@,extern %a" print_alloc_prototype
+ fprintf fmt "extern %a;@,extern %a" pp_alloc_prototype
(m.mname.node_id, m.mstatic)
- print_dealloc_prototype m.mname.node_id
+ pp_dealloc_prototype m.mname.node_id
let print_machine_struct_top_decl_from_header fmt tdecl =
let inode = imported_node_of_top tdecl in
@@ -187,7 +189,7 @@ functor
let print_stateless_C_prototype fmt (name, inputs, outputs) =
let output = match outputs with [ hd ] -> hd | _ -> assert false in
fprintf fmt "%a %s %a"
- (pp_basic_c_type ~pp_c_basic_type_desc ~var_opt:None)
+ (fun x -> pp_basic_c_type ~pp_c_basic_type_desc x)
output.var_type name
(pp_print_parenthesized pp_c_decl_input_var)
inputs
@@ -317,7 +319,7 @@ functor
(* Print the svn version number and the supported C standard (C90 or
C99) *)
pp_print_version () baseNAME baseNAME (* Import the header *) basename
- print_import_prototype
+ pp_import_prototype
{
local = true;
name = basename;
@@ -327,12 +329,12 @@ functor
(* Print dependencies *)
(pp_print_list ~pp_open_box:pp_open_vbox0
~pp_prologue:(pp_print_endcut "/* Import dependencies */")
- print_import_alloc_prototype ~pp_epilogue:pp_print_cutcut)
+ pp_import_alloc_prototype ~pp_epilogue:pp_print_cutcut)
dependencies
(* Print the struct definitions of all machines. *)
(pp_print_list ~pp_open_box:pp_open_vbox0
~pp_prologue:(pp_print_endcut "/* Struct definitions */")
- ~pp_sep:pp_print_cutcut print_machine_struct
+ ~pp_sep:pp_print_cutcut pp_machine_struct
~pp_epilogue:pp_print_cutcut)
machines
(* Print the prototypes of all machines *)
@@ -372,7 +374,7 @@ functor
~pp_prologue:(pp_print_endcut "/* Import dependencies */")
(fun fmt dep ->
let local, name = dependency_of_top dep in
- print_import_prototype fmt
+ pp_import_prototype fmt
{
local;
name;
@@ -404,7 +406,7 @@ functor
/* Global clear declaration */@,\
extern %a;@,\
@,"
- print_global_init_prototype baseNAME print_global_clear_prototype
+ pp_global_init_prototype baseNAME pp_global_clear_prototype
baseNAME
else pp_print_nothing)
()
diff --git a/src/backends/C/c_backend_header.mli b/src/backends/C/c_backend_header.mli
index e69de29b..fb1395fe 100644
--- a/src/backends/C/c_backend_header.mli
+++ b/src/backends/C/c_backend_header.mli
@@ -0,0 +1,17 @@
+open Format
+open Lustre_types
+open Machine_code_types
+open C_backend_common
+
+module type MODIFIERS_HDR = sig
+ module GhostProto : MODIFIERS_GHOST_PROTO
+ val print_machine_decl_prefix: formatter -> machine_t -> unit
+ val pp_import_arrow: formatter -> unit -> unit
+end
+
+module EmptyMod : MODIFIERS_HDR
+
+module Main (Mod : MODIFIERS_HDR) : sig
+ val print_header_from_header: formatter -> string -> top_decl list -> unit
+ val print_alloc_header: formatter -> string -> machine_t list -> dep_t list -> unit
+end
diff --git a/src/backends/C/c_backend_main.ml b/src/backends/C/c_backend_main.ml
index c0fd5904..b9ad438a 100644
--- a/src/backends/C/c_backend_main.ml
+++ b/src/backends/C/c_backend_main.ml
@@ -16,6 +16,8 @@ open Utils.Format
open C_backend_common
open Utils
+module Mpfr = Lustrec_mpfr
+
module type MODIFIERS_MAINSRC = sig end
module EmptyMod = struct end
@@ -37,7 +39,7 @@ functor
let print_put_output fmt id o' o =
let suff = string_of_int (id + 1) in
- print_put_var fmt suff o'.var_id o.var_type o.var_id
+ pp_put_var fmt suff o'.var_id o.var_type o.var_id
let print_main_inout_declaration fmt m =
fprintf fmt
@@ -133,7 +135,7 @@ functor
outputs
let print_get_input fmt id v' v =
- let pp_file = pp_print_file ("in" ^ string_of_int (id + 1)) in
+ let pp_file = pp_file ("in" ^ string_of_int (id + 1)) in
let unclocked_t = Types.unclock_type v.var_type in
fprintf fmt "@[<v>%a@]"
(fun fmt () ->
@@ -156,8 +158,8 @@ functor
pp_file ("f", v.var_id)
else (
Global.main_node := !Options.main_node;
- eprintf "Code generation error: %a%a@." Error.pp_error_msg
- Error.Main_wrong_kind Location.pp_loc v'.var_loc;
+ eprintf "Code generation error: %a%a@." Error.pp
+ Error.Main_wrong_kind Location.pp v'.var_loc;
raise (Error.Error (v'.var_loc, Error.Main_wrong_kind))))
()
@@ -318,7 +320,7 @@ functor
@,\
%a@,\
%a\n\
- \ @]@." print_main_header () print_import_alloc_prototype
+ \ @]@." print_main_header () pp_import_alloc_prototype
{
local = true;
name = basename;
diff --git a/src/backends/C/c_backend_main.mli b/src/backends/C/c_backend_main.mli
index e69de29b..82313865 100644
--- a/src/backends/C/c_backend_main.mli
+++ b/src/backends/C/c_backend_main.mli
@@ -0,0 +1,11 @@
+open Format
+open Lustre_types
+open Machine_code_types
+
+module type MODIFIERS_MAINSRC = sig end
+
+module EmptyMod: MODIFIERS_MAINSRC
+
+module Main (Mod : MODIFIERS_MAINSRC) : sig
+ val print_main_c: formatter -> machine_t -> string -> program_t -> machine_t list -> dep_t list -> unit
+end
diff --git a/src/backends/C/c_backend_makefile.ml b/src/backends/C/c_backend_makefile.ml
index 717d686b..1235e7b3 100644
--- a/src/backends/C/c_backend_makefile.ml
+++ b/src/backends/C/c_backend_makefile.ml
@@ -9,15 +9,16 @@
(* *)
(********************************************************************)
+open Utils
open Format
open Lustre_types
let pp_dep fmt dep =
- Format.fprintf fmt "%b, %s, {%a}, %b" dep.local dep.name Printers.pp_prog
+ fprintf fmt "%b, %s, {%a}, %b" dep.local dep.name Printers.pp_prog
dep.content dep.is_stateful
let pp_deps fmt deps =
- Format.fprintf fmt "@[<v 0>%a@ @]" (Utils.fprintf_list ~sep:"@ ," pp_dep) deps
+ fprintf fmt "@[<v 0>%a@ @]" (pp_comma_list pp_dep) deps
let header_has_code header =
List.exists
@@ -50,10 +51,10 @@ let lib_dependencies deps =
[] deps
let fprintf_dependencies fmt (deps : dep_t list) =
- (* Format.eprintf "Deps: %a@." pp_deps dep; *)
+ (* eprintf "Deps: %a@." pp_deps dep; *)
let compiled_deps = compiled_dependencies deps in
- (* Format.eprintf "Compiled Deps: %a@." pp_deps compiled_dep; *)
+ (* eprintf "Compiled Deps: %a@." pp_deps compiled_dep; *)
List.iter
(fun s ->
Log.report ~level:1 (fun fmt -> fprintf fmt "Adding dependency: %s@." s);
@@ -69,7 +70,7 @@ let fprintf_dependencies fmt (deps : dep_t list) =
module type MODIFIERS_MKF = sig
(* dep was (bool * ident * top_decl list) *)
- val other_targets : Format.formatter -> string -> string -> dep_t list -> unit
+ val other_targets : formatter -> string -> string -> dep_t list -> unit
end
module EmptyMod : MODIFIERS_MKF = struct
@@ -118,12 +119,11 @@ functor
fprintf fmt "\t${GCC} -I${INC} -I. -c %s_main.c@." basename;
fprintf_dependencies fmt dependencies;
fprintf fmt "\t${GCC} -o ${BINNAME} io_frontend.o %a %s.o %s_main.o %a@."
- (Utils.fprintf_list ~sep:" " (fun fmt dep ->
- Format.fprintf fmt "%s.o" dep.name))
+ (pp_print_list (fun fmt dep -> fprintf fmt "%s.o" dep.name))
(compiled_dependencies dependencies)
basename (* library .o *) basename
(* main function . o *)
- (Utils.fprintf_list ~sep:" " (fun fmt lib -> fprintf fmt "-l%s" lib))
+ (pp_print_list (fun fmt lib -> fprintf fmt "-l%s" lib))
(lib_dependencies dependencies);
fprintf fmt "@.";
fprintf fmt "clean:@.";
diff --git a/src/backends/C/c_backend_makefile.mli b/src/backends/C/c_backend_makefile.mli
index e69de29b..a178afd8 100644
--- a/src/backends/C/c_backend_makefile.mli
+++ b/src/backends/C/c_backend_makefile.mli
@@ -0,0 +1,17 @@
+open Utils
+open Format
+open Lustre_types
+
+module type MODIFIERS_MKF = sig
+ val other_targets : formatter -> string -> string -> dep_t list -> unit
+end
+
+module EmptyMod : MODIFIERS_MKF
+
+module Main (Mod : MODIFIERS_MKF) : sig
+ val print_makefile: string -> string -> dep_t list -> formatter -> unit
+end
+
+val fprintf_dependencies: formatter -> dep_t list -> unit
+val compiled_dependencies: dep_t list -> dep_t list
+val lib_dependencies: dep_t list -> ident list
diff --git a/src/backends/C/c_backend_mauve.ml b/src/backends/C/c_backend_mauve.ml
index 860a6c07..b6e4829e 100644
--- a/src/backends/C/c_backend_mauve.ml
+++ b/src/backends/C/c_backend_mauve.ml
@@ -26,7 +26,7 @@ let fsm_name node = node ^ "FSM"
let print_mauve_header fmt basename =
fprintf fmt "#include \"mauve/runtime.hpp\"@.";
- print_import_alloc_prototype fmt
+ pp_import_alloc_prototype fmt
{ local = true; name = basename; content = []; is_stateful = true }
(* assuming it is stateful*);
pp_print_newline fmt ();
diff --git a/src/backends/C/c_backend_mauve.mli b/src/backends/C/c_backend_mauve.mli
index e69de29b..7680b24f 100644
--- a/src/backends/C/c_backend_mauve.mli
+++ b/src/backends/C/c_backend_mauve.mli
@@ -0,0 +1,7 @@
+open Format
+open Machine_code_types
+
+val print_mauve_header: formatter -> string -> unit
+val print_mauve_shell: formatter -> machine_t -> unit
+val print_mauve_core: formatter -> machine_t -> unit
+val print_mauve_fsm: formatter -> machine_t -> unit
diff --git a/src/backends/C/c_backend_spec.ml b/src/backends/C/c_backend_spec.ml
index 8143ff47..9d55cbd7 100644
--- a/src/backends/C/c_backend_spec.ml
+++ b/src/backends/C/c_backend_spec.ml
@@ -17,6 +17,8 @@ open Corelang
open Spec_types
open Machine_code_common
+module Mpfr = Lustrec_mpfr
+
(**************************************************************************)
(* Printing spec for c *)
@@ -508,7 +510,7 @@ let pp_memory_pack_def m fmt mp =
((mp, (name, mem), (name, self)), mp.mpformula)
let print_machine_ghost_struct fmt m =
- pp_acsl (pp_ghost (print_machine_struct ~ghost:true)) fmt m
+ pp_acsl (pp_ghost (pp_machine_struct ~ghost:true)) fmt m
let pp_memory_pack_defs fmt m =
if not (fst (get_stateless_status m)) then
@@ -900,14 +902,13 @@ module MakefileMod = struct
"\t${GCC} -Wno-attributes -o %s_main_eacsl io_frontend.o %a %s \
%s_main_eacsl.o %a@."
basename
- (Utils.fprintf_list ~sep:" " (fun fmt dep ->
- Format.fprintf fmt "%s.o" dep.name))
+ (pp_print_list (fun fmt dep -> fprintf fmt "%s.o" dep.name))
(C_backend_makefile.compiled_dependencies dependencies)
("${FRAMACEACSL}/e_acsl.c "
^ "${FRAMACEACSL}/memory_model/e_acsl_bittree.c "
^ "${FRAMACEACSL}/memory_model/e_acsl_mmodel.c")
basename
- (Utils.fprintf_list ~sep:" " (fun fmt lib -> fprintf fmt "-l%s" lib))
+ (pp_print_list (fun fmt lib -> fprintf fmt "-l%s" lib))
(C_backend_makefile.lib_dependencies dependencies);
fprintf fmt "@."
end
diff --git a/src/backends/C/c_backend_src.ml b/src/backends/C/c_backend_src.ml
index 8e9fa4f0..091eb15b 100644
--- a/src/backends/C/c_backend_src.ml
+++ b/src/backends/C/c_backend_src.ml
@@ -9,13 +9,16 @@
(* *)
(********************************************************************)
-open Utils.Format
+open Utils
+open Format
open Lustre_types
open Machine_code_types
open Corelang
open Machine_code_common
open C_backend_common
+module Mpfr = Lustrec_mpfr
+
module type MODIFIERS_SRC = sig
module GhostProto : MODIFIERS_GHOST_PROTO
@@ -129,7 +132,7 @@ functor
(if is_arrow_reset then fun fmt -> fprintf fmt "%s_reset"
else pp_machine_name)
name
- (pp_comma_list ~pp_eol:pp_print_comma Dimension.pp_dimension)
+ (pp_comma_list ~pp_eol:pp_print_comma Dimension.pp)
static self
(pp_print_option (fun fmt -> fprintf fmt "->%s"))
inst
@@ -328,7 +331,7 @@ functor
let print_alloc_instance fmt (i, (m, static)) =
fprintf fmt "_alloc->%s = %a %a;" i pp_machine_alloc_name (node_name m)
- (pp_print_parenthesized Dimension.pp_dimension)
+ (pp_print_parenthesized Dimension.pp)
static
let print_dealloc_instance fmt (i, (m, _)) =
@@ -350,11 +353,11 @@ functor
let base_type = Types.array_base_type vdecl.var_type in
let size_types = Types.array_type_multi_dimension vdecl.var_type in
let size_type =
- Dimension.multi_dimension_product vdecl.var_loc size_types
+ Dimension.multi_product vdecl.var_loc size_types
in
fprintf fmt
"_alloc->_reg.%s = (%a*) malloc((%a)*sizeof(%a));@,assert(_alloc->%s);"
- vdecl.var_id (pp_c_type "") base_type Dimension.pp_dimension size_type
+ vdecl.var_id (pp_c_type "") base_type Dimension.pp size_type
(pp_c_type "") base_type vdecl.var_id
let print_dealloc_array fmt vdecl =
@@ -418,7 +421,7 @@ functor
* (Utils.pp_newline_if_non_empty m.minit) *)
let pp_c_check m self fmt (loc, check) =
- fprintf fmt "@[<v>%a@,assert (%a);@]" Location.pp_c_loc loc
+ fprintf fmt "@[<v>%a@,assert (%a);@]" Location.pp_c loc
(pp_c_val m self (pp_c_var_read m))
check
@@ -458,7 +461,7 @@ functor
let node_of_machine m =
{
top_decl_desc = Node m.mname;
- top_decl_loc = Location.dummy_loc;
+ top_decl_loc = Location.dummy;
top_decl_owner = "";
top_decl_itf = false;
}
@@ -624,7 +627,7 @@ functor
let rec aux indices value fmt typ =
if Types.is_array_type typ then
let dim = Types.array_type_dimension typ in
- let szl = Utils.enumerate (Dimension.size_const_dimension dim) in
+ let szl = Utils.enumerate (Dimension.size_const dim) in
let typ' = Types.array_element_type typ in
let value =
match value with Const_array ca -> List.nth ca | _ -> assert false
@@ -688,7 +691,7 @@ functor
}@,\
return;@]@,\
}"
- print_global_init_prototype baseNAME
+ pp_global_init_prototype baseNAME
(pp_c_basic_type_desc Type_predef.type_bool)
(* constants *)
(pp_print_list ~pp_prologue:pp_print_cut
@@ -709,7 +712,7 @@ functor
}@,\
return;@]@,\
}"
- print_global_clear_prototype baseNAME
+ pp_global_clear_prototype baseNAME
(pp_c_basic_type_desc Type_predef.type_bool)
(* constants *)
(pp_print_list ~pp_prologue:pp_print_cut
@@ -723,9 +726,9 @@ functor
if not !Options.static_mem then
(* Alloc functions, only if non static mode *)
fprintf fmt "@[<v 2>%a {@,%a%a@]@,}@,@[<v 2>%a {@,%a%a@]@,@,"
- print_alloc_prototype
+ pp_alloc_prototype
(m.mname.node_id, m.mstatic)
- print_alloc_const m print_alloc_code m print_dealloc_prototype
+ print_alloc_const m print_alloc_code m pp_dealloc_prototype
m.mname.node_id print_alloc_const m print_dealloc_code m
let print_mpfr_code self fmt m =
@@ -775,12 +778,12 @@ functor
let print_extern_alloc_prototype fmt ind =
let static = List.filter (fun v -> v.var_dec_const) ind.nodei_inputs in
- fprintf fmt "extern %a;@,extern %a;" print_alloc_prototype
- (ind.nodei_id, static) print_dealloc_prototype ind.nodei_id
+ fprintf fmt "extern %a;@,extern %a;" pp_alloc_prototype
+ (ind.nodei_id, static) pp_dealloc_prototype ind.nodei_id
let print_lib_c source_fmt basename prog machines dependencies =
fprintf source_fmt "@[<v>%a%a@,@,%a@,%a%a%a%a%a%a%a@]@."
- print_import_standard () print_import_prototype
+ print_import_standard () pp_import_prototype
{
local = true;
name = basename;
@@ -793,7 +796,7 @@ functor
(* Print dependencies *)
(pp_print_list ~pp_open_box:pp_open_vbox0
~pp_prologue:(pp_print_endcut "/* Import dependencies */")
- print_import_prototype ~pp_epilogue:pp_print_cutcut)
+ pp_import_prototype ~pp_epilogue:pp_print_cutcut)
dependencies
(* Print consts *)
(pp_print_list ~pp_open_box:pp_open_vbox0
@@ -836,16 +839,16 @@ functor
~pp_prologue:
(pp_print_endcut "/* Node allocation function prototypes */")
~pp_sep:pp_print_cutcut (fun fmt m ->
- fprintf fmt "%a;@,%a;" print_alloc_prototype
+ fprintf fmt "%a;@,%a;" pp_alloc_prototype
(m.mname.node_id, m.mstatic)
- print_dealloc_prototype m.mname.node_id))
+ pp_dealloc_prototype m.mname.node_id))
machines
else pp_print_nothing)
()
(* Print the struct definitions of all machines. *)
(pp_print_list ~pp_open_box:pp_open_vbox0
~pp_prologue:(pp_print_endcut "/* Struct definitions */")
- ~pp_sep:pp_print_cutcut print_machine_struct
+ ~pp_sep:pp_print_cutcut pp_machine_struct
~pp_epilogue:pp_print_cutcut)
machines (* Print the spec predicates *) Mod.pp_predicates machines
(* Print nodes one by one (in the previous order) *)
diff --git a/src/backends/C/c_backend_src.mli b/src/backends/C/c_backend_src.mli
index e69de29b..93cfc84c 100644
--- a/src/backends/C/c_backend_src.mli
+++ b/src/backends/C/c_backend_src.mli
@@ -0,0 +1,29 @@
+open Utils
+open Format
+open Lustre_types
+open Machine_code_types
+open C_backend_common
+
+module type MODIFIERS_SRC = sig
+ module GhostProto : MODIFIERS_GHOST_PROTO
+
+ val pp_predicates : formatter -> machine_t list -> unit
+
+ val pp_set_reset_spec : formatter -> ident -> ident -> machine_t -> unit
+
+ val pp_clear_reset_spec : formatter -> ident -> ident -> machine_t -> unit
+
+ val pp_step_spec :
+ formatter -> machine_t list -> ident -> ident -> machine_t -> unit
+
+ val pp_step_instr_spec :
+ machine_t -> ident -> ident -> formatter -> instr_t -> unit
+
+ val pp_ghost_parameter : ident -> formatter -> ident option -> unit
+end
+
+module EmptyMod : MODIFIERS_SRC
+
+module Main (Mod : MODIFIERS_SRC) : sig
+ val print_lib_c: formatter -> string -> program_t -> machine_t list -> dep_t list -> unit
+end
diff --git a/src/backends/EMF/EMF_backend.ml b/src/backends/EMF/EMF_backend.ml
index 27440e16..64513a81 100644
--- a/src/backends/EMF/EMF_backend.ml
+++ b/src/backends/EMF/EMF_backend.ml
@@ -98,7 +98,9 @@
*)
+open Utils
open Lustre_types
+open Corelang
open Machine_code_types
open Machine_code_common
open Format
@@ -108,8 +110,6 @@ exception Unhandled of string
module ISet = Utils.ISet
-let fprintf_list = Utils.fprintf_list
-
(**********************************************)
(* Utility functions: arrow and lustre expr *)
(**********************************************)
@@ -170,7 +170,8 @@ let get_instr_id fmt i =
fprintf fmt "branch_%i" !branch_cpt
| MStep (outs, id, _) ->
print_protect fmt (fun fmt ->
- fprintf fmt "%a_%s" (fprintf_list ~sep:"_" pp_var_name) outs id)
+ fprintf fmt "%a_%s" (pp_print_list ~pp_sep:(fun fmt () -> pp_print_string fmt "_")
+ pp_var_name) outs id)
| _ -> ()
(* No name *)
@@ -212,7 +213,7 @@ and branch_instr_vars m i =
lhs,
if is_stateful && is_resetable_fun i.lustre_eq then
let reset_var =
- let loc = Location.dummy_loc in
+ let loc = Location.dummy in
Corelang.mkvar_decl loc
( reset_name f,
Corelang.mktyp loc Tydec_bool,
@@ -334,7 +335,7 @@ let rec pp_emf_instr m fmt i =
fprintf fmt "\"guard\": %a,@ " (pp_emf_cst_or_var m) g;
(* it has to be a variable or a constant *)
fprintf fmt "\"outputs\": [%a],@ "
- (fprintf_list ~sep:", " pp_var_string)
+ (pp_comma_list pp_var_string)
(ISet.elements outputs);
fprintf fmt "\"inputs\": [%a],@ " pp_emf_vars_decl
(*
@@ -343,7 +344,7 @@ let rec pp_emf_instr m fmt i =
remove guard's variable from inputs *)
(VSet.elements inputs);
fprintf fmt "@[<v 2>\"branches\": {@ @[<v 0>%a@]@]@ }"
- (fprintf_list ~sep:",@ " (fun fmt (tag, instrs_tag) ->
+ (pp_comma_list (fun fmt (tag, instrs_tag) ->
let branch_all_lhs, _, branch_inputs =
branch_block_vars m instrs_tag
in
@@ -377,7 +378,7 @@ let rec pp_emf_instr m fmt i =
(fun fmt -> pp_print_string fmt node_f.node_id)
f;
fprintf fmt "\"lhs\": [@[%a@]],@ \"args\": [@[%a@]]"
- (fprintf_list ~sep:",@ " (fun fmt v ->
+ (pp_comma_list (fun fmt v ->
fprintf fmt "\"%a\"" pp_var_name v))
outputs (pp_emf_cst_or_var_list m) inputs;
if is_stateful then
@@ -398,12 +399,12 @@ let rec pp_emf_instr m fmt i =
fprintf fmt "@]@]@ }"
and pp_emf_instrs m fmt instrs =
- fprintf_list ~sep:",@ " (pp_emf_instr m) fmt instrs
+ pp_comma_list (pp_emf_instr m) fmt instrs
let pp_emf_annot cpt fmt (key, ee) =
let _ =
fprintf fmt "\"ann%i\": { @[<hov 0>\"key\": [%a],@ \"eexpr\": %a@] }" !cpt
- (fprintf_list ~sep:"," (fun fmt s -> fprintf fmt "\"%s\"" s))
+ (pp_comma_list (fun fmt s -> fprintf fmt "\"%s\"" s))
key pp_emf_eexpr ee
in
incr cpt
@@ -442,10 +443,10 @@ let pp_emf_spec fmt spec =
fprintf fmt "@] }"
let pp_emf_annots cpt fmt annots =
- fprintf_list ~sep:",@ " (pp_emf_annot cpt) fmt annots.annots
+ pp_comma_list (pp_emf_annot cpt) fmt annots.annots
let pp_emf_annots_list cpt fmt annots_list =
- fprintf_list ~sep:",@ " (pp_emf_annots cpt) fmt annots_list
+ pp_comma_list (pp_emf_annots cpt) fmt annots_list
(* let pp_emf_contract fmt nd =
* let c = Printers.node_as_contract nd in
@@ -523,7 +524,7 @@ let pp_emf_imported_node fmt top =
(****************************************************)
let pp_meta fmt basename =
fprintf fmt "\"meta\": @[<v 0>{@ ";
- Utils.fprintf_list ~sep:",@ "
+ Format.pp_comma_list
(fun fmt (k, v) -> fprintf fmt "\"%s\": \"%s\"" k v)
fmt
[
@@ -550,7 +551,7 @@ let translate fmt basename prog machines =
fprintf fmt "}@],@ ";
fprintf fmt "\"nodes\": @[<v 0>{@ ";
(* Previous alternative: mapping normalized lustre to EMF:
- fprintf_list ~sep:",@ " pp_decl fmt prog; *)
+ pp_comma_list pp_decl fmt prog; *)
pp_emf_list pp_machine fmt machines;
fprintf fmt "}@]@ }";
fprintf fmt "@]@ }"
diff --git a/src/backends/EMF/EMF_backend.mli b/src/backends/EMF/EMF_backend.mli
index e69de29b..f1c2927b 100644
--- a/src/backends/EMF/EMF_backend.mli
+++ b/src/backends/EMF/EMF_backend.mli
@@ -0,0 +1 @@
+val translate: Format.formatter -> string -> Lustre_types.program_t -> Machine_code_types.machine_t list -> unit
diff --git a/src/backends/EMF/EMF_common.ml b/src/backends/EMF/EMF_common.ml
index c820d6b2..33ce3c76 100644
--- a/src/backends/EMF/EMF_common.ml
+++ b/src/backends/EMF/EMF_common.ml
@@ -1,6 +1,7 @@
+open Utils
open Lustre_types
+open Corelang
open Machine_code_types
-module VSet = Corelang.VSet
open Format
open Machine_code_common
@@ -92,8 +93,7 @@ let rec pp_emf_dim fmt dim_expr =
fprintf fmt "\"kind\": \"ident\",@ \"value\": \"%s\"" s
| Dappl (f, args) ->
fprintf fmt "\"kind\": \"fun\",@ \"id\": \"%s\",@ \"args\": [@[%a@]]" f
- (Utils.fprintf_list ~sep:",@ " pp_emf_dim)
- args
+ (pp_comma_list pp_emf_dim) args
| Dite (i, t, e) ->
fprintf fmt
"\"kind\": \"ite\",@ \"guard\": \"%a\",@ \"then\": %a,@ \"else\": %a"
@@ -137,13 +137,13 @@ let rec pp_concrete_type dec_t infered_t fmt =
prefix of the lustre file. They shall not be associated to variables *)
| Tydec_array (dim, e) ->
let inf_base =
- match infered_t.Typing.tdesc with
- | Typing.Tarray (_, t) ->
+ match infered_t.Types.tdesc with
+ | Types.Tarray (_, t) ->
t
| _ ->
(* returing something useless, hoping that the concrete datatype will
return something usefull *)
- Typing.new_var ()
+ Types.new_var ()
in
fprintf fmt "{ \"kind\": \"array\", \"base_type\": %t, \"dim\": %a }"
(pp_concrete_type e inf_base)
@@ -232,7 +232,7 @@ let pp_emf_list ?(eol : ('a, formatter, unit) Stdlib.format = "") pp fmt l =
()
| _ ->
fprintf fmt "@[";
- Utils.fprintf_list ~sep:",@ " pp fmt l;
+ pp_comma_list pp fmt l;
fprintf fmt "@]%(%)" eol
(* Print the variable declaration *)
@@ -330,7 +330,7 @@ let rec pp_emf_cst_or_var m fmt v =
assert false
and pp_emf_cst_or_var_list m =
- Utils.fprintf_list ~sep:",@ " (pp_emf_cst_or_var m)
+ pp_comma_list (pp_emf_cst_or_var m)
(* Printer lustre expr and eexpr *)
@@ -349,7 +349,7 @@ let rec pp_emf_expr fmt e =
fprintf fmt "@]}"
| Expr_tuple el ->
fprintf fmt "[@[<hov 0>%a@ @]]"
- (Utils.fprintf_list ~sep:",@ " pp_emf_expr)
+ (pp_comma_list pp_emf_expr)
el
(* Missing these | 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 *
@@ -394,7 +394,7 @@ let pp_emf_eexpr fmt ee =
()
| Some name ->
Format.fprintf fmt "\"name\": \"%s\",@ " name)
- (Utils.fprintf_list ~sep:"; " Printers.pp_quantifiers)
+ (pp_print_list ~pp_sep:pp_print_semicolon Printers.pp_quantifiers)
ee.eexpr_quantifiers pp_emf_expr ee.eexpr_qfexpr
let pp_emf_eexprs = pp_emf_list pp_emf_eexpr
@@ -411,10 +411,10 @@ let pp_emf_stmt fmt stmt =
assert false
| Eq eq ->
fprintf fmt "@[ @[<v 2>\"%a\": {@ "
- (Utils.fprintf_list ~sep:"_" pp_print_string)
+ (pp_print_list ~pp_sep:(fun fmt () -> pp_print_string fmt "_") pp_print_string)
eq.eq_lhs;
fprintf fmt "\"lhs\": [%a],@ "
- (Utils.fprintf_list ~sep:", " (fun fmt vid -> fprintf fmt "\"%s\"" vid))
+ (pp_comma_list (fun fmt vid -> fprintf fmt "\"%s\"" vid))
eq.eq_lhs;
fprintf fmt "\"rhs\": %a,@ " pp_emf_expr eq.eq_rhs;
fprintf fmt "@]@]@ }"
@@ -439,11 +439,10 @@ let rec pp_emf_typ_dec fmt tydef_dec =
fprintf fmt "\"kind\": \"alias\",@ \"value\": \"%s\"" c
| Tydec_enum el ->
fprintf fmt "\"kind\": \"enum\",@ \"elements\": [%a]"
- (Utils.fprintf_list ~sep:", " (fun fmt e -> fprintf fmt "\"%s\"" e))
- el
+ (pp_comma_list (fun fmt e -> fprintf fmt "\"%s\"" e)) el
| Tydec_struct s ->
fprintf fmt "\"kind\": \"struct\",@ \"fields\": [%a]"
- (Utils.fprintf_list ~sep:", " (fun fmt (id, typ) ->
+ (pp_comma_list (fun fmt (id, typ) ->
fprintf fmt "\"%s\": %a" id pp_emf_typ_dec typ))
s
| Tydec_array (dim, typ) ->
diff --git a/src/backends/EMF/EMF_common.mli b/src/backends/EMF/EMF_common.mli
index e69de29b..15779482 100644
--- a/src/backends/EMF/EMF_common.mli
+++ b/src/backends/EMF/EMF_common.mli
@@ -0,0 +1,24 @@
+open Utils
+open Lustre_types
+open Machine_code_types
+open Format
+
+val pp_emf_cst_or_var_list: machine_t -> formatter -> value_t list -> unit
+val pp_emf_cst_or_var: machine_t -> formatter -> value_t -> unit
+val pp_var_name: formatter -> var_decl -> unit
+val print_protect: formatter -> (formatter -> unit) -> unit
+val pp_var_string: formatter -> ident -> unit
+val pp_emf_vars_decl: formatter -> var_decl list -> unit
+val pp_tag_id: formatter -> ident -> unit
+val pp_emf_expr: formatter -> expr -> unit
+val pp_emf_eexpr: formatter -> eexpr -> unit
+val pp_emf_eexprs: formatter -> eexpr list -> unit
+val pp_emf_list: ?eol:(unit, formatter, unit) Stdlib.format -> (formatter -> 'a -> unit) -> formatter -> 'a list -> unit
+val pp_emf_typedef: formatter -> Lustre_types.top_decl -> unit
+val pp_emf_top_const: formatter -> Lustre_types.top_decl -> unit
+
+val reset_name: ident -> ident
+
+val get_expr_vars: value_t -> Corelang.VSet.t
+
+val is_imported_node: ident -> machine_t -> bool
diff --git a/src/backends/EMF/EMF_library_calls.ml b/src/backends/EMF/EMF_library_calls.ml
index 788f4553..4e765698 100644
--- a/src/backends/EMF/EMF_library_calls.ml
+++ b/src/backends/EMF/EMF_library_calls.ml
@@ -3,6 +3,7 @@
moment, modular compilation of multiple lustre sources as one output JSON is
not considered. *)
+open Utils
open Lustre_types
open Machine_code_types
open Format
@@ -18,8 +19,7 @@ let pp_call fmt m f outputs inputs =
"\"kind\": \"functioncall\",@ \"name\": \"%s\",@ \"library\": \"%s\",@ "
name lib;
fprintf fmt "\"lhs\": [@[%a@]],@ \"args\": [@[%a@]]"
- (Utils.fprintf_list ~sep:",@ " (fun fmt v ->
- fprintf fmt "\"%a\"" Printers.pp_var_name v))
+ (pp_comma_list (fun fmt v -> fprintf fmt "\"%a\"" Printers.pp_var_name v))
outputs (pp_emf_cst_or_var_list m) inputs
| _ ->
Format.eprintf "Calls to function %s in library %s are not handled yet.@."
diff --git a/src/backends/EMF/EMF_library_calls.mli b/src/backends/EMF/EMF_library_calls.mli
index e69de29b..f5d0b3c4 100644
--- a/src/backends/EMF/EMF_library_calls.mli
+++ b/src/backends/EMF/EMF_library_calls.mli
@@ -0,0 +1,2 @@
+val pp_call: Format.formatter -> Machine_code_types.machine_t -> Utils.ident ->
+ Lustre_types.var_decl list -> Machine_code_types.value_t list -> unit
diff --git a/src/backends/Horn/horn_backend.ml b/src/backends/Horn/horn_backend.ml
index 50625633..d596f801 100644
--- a/src/backends/Horn/horn_backend.ml
+++ b/src/backends/Horn/horn_backend.ml
@@ -59,7 +59,7 @@ let print_type_definitions fmt =
| Tydec_enum tl ->
incr cpt_type;
fprintf fmt "(declare-datatypes () ((%s %a)));@.@." var
- (Utils.fprintf_list ~sep:" " pp_print_string)
+ (pp_print_list pp_print_string)
tl
| _ ->
assert false)
diff --git a/src/backends/Horn/horn_backend.mli b/src/backends/Horn/horn_backend.mli
index e69de29b..b1788f5e 100644
--- a/src/backends/Horn/horn_backend.mli
+++ b/src/backends/Horn/horn_backend.mli
@@ -0,0 +1 @@
+val translate: Format.formatter -> Lustre_types.program_t -> Machine_code_types.machine_t list -> unit
diff --git a/src/backends/Horn/horn_backend_collecting_sem.ml b/src/backends/Horn/horn_backend_collecting_sem.ml
index 059c0ae4..fae985b1 100644
--- a/src/backends/Horn/horn_backend_collecting_sem.ml
+++ b/src/backends/Horn/horn_backend_collecting_sem.ml
@@ -14,6 +14,7 @@
This is a modified version that handle reset *)
+open Utils
open Format
open Lustre_types
open Machine_code_types
@@ -45,7 +46,7 @@ let collecting_semantics machines fmt node machine =
in
fprintf fmt "(declare-rel MAIN (%a))@."
- (Utils.fprintf_list ~sep:" " pp_type)
+ (pp_print_list pp_type)
(List.map (fun v -> v.var_type) main_memory_next);
(* Init case *)
@@ -59,11 +60,11 @@ let collecting_semantics machines fmt node machine =
fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>";
fprintf fmt "INIT_STATE@ ";
fprintf fmt "(@[<v 0>%a %a@])" step_name node
- (Utils.fprintf_list ~sep:" " (pp_horn_var machine))
+ (pp_print_list (pp_horn_var machine))
(step_vars_m_x machines machine);
fprintf fmt "@]@ )@ ";
fprintf fmt "(MAIN %a)@]@.))@.@."
- (Utils.fprintf_list ~sep:" " (pp_horn_var machine))
+ (pp_print_list (pp_horn_var machine))
main_memory_next)
else
let reset_name, step_name = pp_machine_reset_name, pp_machine_step_name in
@@ -73,15 +74,15 @@ let collecting_semantics machines fmt node machine =
fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>";
fprintf fmt "INIT_STATE@ ";
fprintf fmt "(@[<v 0>%a %a@])@ " reset_name node
- (Utils.fprintf_list ~sep:" " (pp_horn_var machine))
+ (pp_print_list (pp_horn_var machine))
(reset_vars machines machine);
fprintf fmt "(@[<v 0>%a %a@])" step_name node
- (Utils.fprintf_list ~sep:" " (pp_horn_var machine))
+ (pp_print_list (pp_horn_var machine))
(step_vars_m_x machines machine);
fprintf fmt "@]@ )@ ";
fprintf fmt "(MAIN %a)@]@.))@.@."
- (Utils.fprintf_list ~sep:" " (pp_horn_var machine))
+ (pp_print_list (pp_horn_var machine))
main_memory_next
in
@@ -91,16 +92,16 @@ let collecting_semantics machines fmt node machine =
in
fprintf fmt "; Inductive def@.";
- (Utils.fprintf_list ~sep:" " (fun fmt v -> fprintf fmt "%a@." pp_decl_var v))
+ (pp_print_list (fun fmt v -> fprintf fmt "%a@." pp_decl_var v))
fmt main_output_dummy;
fprintf fmt
"@[<v 2>(rule (=> @ (and @[<v 0>(MAIN %a)@ (@[<v 0>%a %a@])@]@ )@ (MAIN \
%a)@]@.))@.@."
- (Utils.fprintf_list ~sep:" " (pp_horn_var machine))
+ (pp_print_list (pp_horn_var machine))
main_memory_current step_name node
- (Utils.fprintf_list ~sep:" " (pp_horn_var machine))
+ (pp_print_list (pp_horn_var machine))
(step_vars machines machine)
- (Utils.fprintf_list ~sep:" " (pp_horn_var machine))
+ (pp_print_list (pp_horn_var machine))
main_memory_next
let check_prop machines fmt machine =
@@ -115,7 +116,7 @@ let check_prop machines fmt machine =
fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (MAIN %a)@])@ ERR))@."
(pp_conj (pp_horn_var machine))
main_output
- (Utils.fprintf_list ~sep:" " (pp_horn_var machine))
+ (pp_print_list (pp_horn_var machine))
main_memory_next;
if !Options.horn_query then fprintf fmt "(query ERR)@."
@@ -157,7 +158,7 @@ let cex_computation machines fmt node machine =
in
fprintf fmt "(declare-rel CEX (Int %a))@.@."
- (Utils.fprintf_list ~sep:" " pp_type)
+ (pp_print_list pp_type)
(List.map (fun v -> v.var_type) cex_memory_next);
fprintf fmt "; Initial set: Reset(c,m) + One Step(m,x) @.";
@@ -166,31 +167,31 @@ let cex_computation machines fmt node machine =
fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>";
fprintf fmt "INIT_STATE_CEX@ ";
fprintf fmt "(@[<v 0>%a %a@])@ " reset_name node
- (Utils.fprintf_list ~sep:" " (pp_horn_var machine))
+ (pp_print_list (pp_horn_var machine))
(reset_vars machines machine);
fprintf fmt "(@[<v 0>%a %a@])" step_name node
- (Utils.fprintf_list ~sep:" " (pp_horn_var machine))
+ (pp_print_list (pp_horn_var machine))
(step_vars_m_x machines machine);
fprintf fmt "@]@ )@ ";
fprintf fmt "(CEX 0 %a)@]@.))@.@."
- (Utils.fprintf_list ~sep:" " (pp_horn_var machine))
+ (pp_print_list (pp_horn_var machine))
cex_memory_next;
fprintf fmt "; Inductive def@.";
(* Declare dummy inputs. Outputs should have been declared previously with
collecting sem *)
- (Utils.fprintf_list ~sep:" " (fun fmt v -> fprintf fmt "%a@." pp_decl_var v))
+ (pp_print_list (fun fmt v -> fprintf fmt "%a@." pp_decl_var v))
fmt cex_input_dummy;
fprintf fmt "(declare-var cexcpt Int)@.";
fprintf fmt
"@[<v 2>(rule (=> @ (and @[<v 0>(CEX cexcpt %a)@ (@[<v 0>%a %a@])@]@ )@ \
(CEX (+ 1 cexcpt) %a)@]@.))@.@."
- (Utils.fprintf_list ~sep:" " (pp_horn_var machine))
+ (pp_print_list (pp_horn_var machine))
cex_memory_current step_name node
- (Utils.fprintf_list ~sep:" " (pp_horn_var machine))
+ (pp_print_list (pp_horn_var machine))
(step_vars machines machine)
- (Utils.fprintf_list ~sep:" " (pp_horn_var machine))
+ (pp_print_list (pp_horn_var machine))
cex_memory_next
let get_cex machines fmt machine =
@@ -211,7 +212,7 @@ let get_cex machines fmt machine =
"@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (CEX cexcpt %a)@])@ CEXTRACE))@."
(pp_conj (pp_horn_var machine))
cex_output
- (Utils.fprintf_list ~sep:" " (pp_horn_var machine))
+ (pp_print_list (pp_horn_var machine))
cex_memory_next;
fprintf fmt "(query CEXTRACE)@."
diff --git a/src/backends/Horn/horn_backend_collecting_sem.mli b/src/backends/Horn/horn_backend_collecting_sem.mli
index e69de29b..7d975275 100644
--- a/src/backends/Horn/horn_backend_collecting_sem.mli
+++ b/src/backends/Horn/horn_backend_collecting_sem.mli
@@ -0,0 +1,7 @@
+open Utils
+open Machine_code_types
+
+val cex_computation: machine_t list -> Format.formatter -> ident -> machine_t -> unit
+val get_cex: machine_t list -> Format.formatter -> machine_t -> unit
+val collecting_semantics: machine_t list -> Format.formatter -> ident -> machine_t -> unit
+val check_prop: machine_t list -> Format.formatter -> machine_t -> unit
diff --git a/src/backends/Horn/horn_backend_common.ml b/src/backends/Horn/horn_backend_common.ml
index 60efc7c2..3e0ff669 100644
--- a/src/backends/Horn/horn_backend_common.ml
+++ b/src/backends/Horn/horn_backend_common.ml
@@ -9,6 +9,7 @@
(* *)
(********************************************************************)
+open Utils
open Format
open Lustre_types
open Machine_code_types
@@ -60,7 +61,7 @@ let pp_conj pp fmt l =
| [ x ] ->
pp fmt x
| _ ->
- fprintf fmt "(and @[<v 0>%a@]@ )" (Utils.fprintf_list ~sep:"@ " pp) l
+ fprintf fmt "(and @[<v 0>%a@]@ )" (pp_print_list pp) l
(********************************************************************************************)
(* Workaround to prevent the use of declared keywords as node name *)
diff --git a/src/backends/Horn/horn_backend_common.mli b/src/backends/Horn/horn_backend_common.mli
index e69de29b..268b2841 100644
--- a/src/backends/Horn/horn_backend_common.mli
+++ b/src/backends/Horn/horn_backend_common.mli
@@ -0,0 +1,37 @@
+open Utils
+open Format
+open Lustre_types
+open Machine_code_types
+
+val rename_machine_list: ident -> var_decl list -> var_decl list
+val get_machine: machine_t list -> ident -> machine_t
+
+val full_memory_vars: ?without_arrow:bool -> machine_t list -> machine_t -> var_decl list
+
+val rename_machine: ident -> var_decl -> var_decl
+val rename_current: var_decl -> var_decl
+val rename_mid: var_decl -> var_decl
+val rename_next: var_decl -> var_decl
+val rename_current_list: var_decl list -> var_decl list
+val rename_mid_list: var_decl list -> var_decl list
+val rename_next_list: var_decl list -> var_decl list
+
+val concat: string -> ident -> ident
+
+val arrow_vars: machine_t list -> machine_t -> var_decl list
+val reset_vars: machine_t list -> machine_t -> var_decl list
+val step_vars: machine_t list -> machine_t -> var_decl list
+val step_vars_m_x: machine_t list -> machine_t -> var_decl list
+val local_memory_vars: machine_t -> var_decl list
+val inout_vars: machine_t -> var_decl list
+
+val pp_type: formatter -> Types.t -> unit
+val pp_machine_reset_name: formatter -> ident -> unit
+val pp_machine_step_name: formatter -> ident -> unit
+val pp_machine_stateless_name: formatter -> ident -> unit
+val pp_conj: (formatter -> 'a -> unit) -> formatter -> 'a list -> unit
+val pp_decl_var: formatter -> var_decl -> unit
+
+val registered_keywords: ident list
+
+val protect_kwd: ident -> ident
diff --git a/src/backends/Horn/horn_backend_printers.ml b/src/backends/Horn/horn_backend_printers.ml
index 1e06099f..7a98efce 100644
--- a/src/backends/Horn/horn_backend_printers.ml
+++ b/src/backends/Horn/horn_backend_printers.ml
@@ -14,6 +14,7 @@
This is a modified version that handle reset *)
+open Utils
open Format
open Lustre_types
open Machine_code_types
@@ -218,7 +219,7 @@ let pp_instance_reset machines m fmt i =
in
fprintf fmt "(%a @[<v 0>%a)@]" pp_machine_reset_name (node_name n)
- (Utils.fprintf_list ~sep:"@ " (pp_horn_var m))
+ (pp_print_list (pp_horn_var m))
(rename_machine_list (concat m.mname.node_id i)
(rename_current_list (full_memory_vars machines target_machine))
@ rename_machine_list (concat m.mname.node_id i)
@@ -261,23 +262,20 @@ let pp_instance_call machines reset_instances m fmt i inputs outputs =
fprintf fmt "(= %a false)" (pp_horn_var m) mem_x;
fprintf fmt ")@]"
| _ ->
- fprintf fmt "(%a @[<v 0>%a%t%a%t%a)@]" pp_machine_step_name (node_name n)
- (Utils.fprintf_list ~sep:"@ " (pp_horn_val m self (pp_horn_var m)))
- inputs
- (Utils.pp_final_char_if_non_empty "@ " inputs)
- (Utils.fprintf_list ~sep:"@ " (pp_horn_val m self (pp_horn_var m)))
+ fprintf fmt "(%a @[<v 0>%a%a%a)@]" pp_machine_step_name (node_name n)
+ (pp_print_list ~pp_epilogue:pp_print_cut
+ (pp_horn_val m self (pp_horn_var m))) inputs
+ (pp_print_list ~pp_epilogue:pp_print_cut
+ (pp_horn_val m self (pp_horn_var m)))
(List.map (fun v -> mk_val (Var v) v.var_type) outputs)
- (Utils.pp_final_char_if_non_empty "@ " outputs)
- (Utils.fprintf_list ~sep:"@ " (pp_horn_var m))
- (mid_mems @ next_mems)
+ (pp_print_list (pp_horn_var m)) (mid_mems @ next_mems)
with Not_found ->
(* stateless node instance *)
let n, _ = List.assoc i m.mcalls in
- fprintf fmt "(%a @[<v 0>%a%t%a)@]" pp_machine_stateless_name (node_name n)
- (Utils.fprintf_list ~sep:"@ " (pp_horn_val m self (pp_horn_var m)))
- inputs
- (Utils.pp_final_char_if_non_empty "@ " inputs)
- (Utils.fprintf_list ~sep:"@ " (pp_horn_val m self (pp_horn_var m)))
+ fprintf fmt "(%a @[<v 0>%a%a)@]" pp_machine_stateless_name (node_name n)
+ (pp_print_list ~pp_epilogue:pp_print_cut
+ (pp_horn_val m self (pp_horn_var m))) inputs
+ (pp_print_list (pp_horn_val m self (pp_horn_var m)))
(List.map (fun v -> mk_val (Var v) v.var_type) outputs)
(* Print the instruction and update the set of reset instances *)
@@ -370,7 +368,7 @@ let pp_machine_reset machines fmt m =
fprintf fmt "@[<v 5>(and @ ";
(* print "x_m = x_c" for each local memory *)
- (Utils.fprintf_list ~sep:"@ " (fun fmt v ->
+ (pp_print_list (fun fmt v ->
fprintf fmt "(= %a %a)" (pp_horn_var m) (rename_mid v) (pp_horn_var m)
(rename_current v)))
fmt locals;
@@ -378,14 +376,14 @@ let pp_machine_reset machines fmt m =
(* print "child_reset ( associated vars _ {c,m} )" for each subnode. Special
treatment for _arrow: _first = true *)
- (Utils.fprintf_list ~sep:"@ " (fun fmt (id, (n, _)) ->
+ (pp_print_list (fun fmt (id, (n, _)) ->
let name = node_name n in
if name = "_arrow" then
fprintf fmt "(= %s._arrow._first_m true)" (concat m.mname.node_id id)
else
let machine_n = get_machine machines name in
fprintf fmt "(%s_reset @[<hov 0>%a@])" name
- (Utils.fprintf_list ~sep:"@ " (pp_horn_var m))
+ (pp_print_list (pp_horn_var m))
(rename_machine_list
(concat m.mname.node_id id)
(reset_vars machines machine_n))))
@@ -405,7 +403,7 @@ let print_machine machines fmt m =
fprintf fmt "; %s@." m.mname.node_id;
(* Printing variables *)
- Utils.fprintf_list ~sep:"@." pp_decl_var fmt
+ pp_print_list ~pp_open_box:pp_open_vbox0 pp_decl_var fmt
(inout_vars m
@ rename_current_list (full_memory_vars machines m)
@ rename_mid_list (full_memory_vars machines m)
@@ -417,7 +415,7 @@ let print_machine machines fmt m =
(* Declaring single predicate *)
fprintf fmt "(declare-rel %a (%a))@." pp_machine_stateless_name
m.mname.node_id
- (Utils.fprintf_list ~sep:" " pp_type)
+ (pp_print_list pp_type)
(List.map (fun v -> v.var_type) (inout_vars m));
match m.mstep.step_asserts with
@@ -430,7 +428,7 @@ let print_machine machines fmt m =
(* No reset info for stateless nodes *) m fmt m.mstep.step_instrs);
fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@." pp_machine_stateless_name
m.mname.node_id
- (Utils.fprintf_list ~sep:" " (pp_horn_var m))
+ (pp_print_list (pp_horn_var m))
(inout_vars m)
| assertsl ->
let pp_val =
@@ -443,17 +441,17 @@ let print_machine machines fmt m =
ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
fprintf fmt "@. %a)@ (%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val)
assertsl pp_machine_stateless_name m.mname.node_id
- (Utils.fprintf_list ~sep:" " (pp_horn_var m))
+ (pp_print_list (pp_horn_var m))
(step_vars machines m))
else (
(* Declaring predicate *)
fprintf fmt "(declare-rel %a (%a))@." pp_machine_reset_name
m.mname.node_id
- (Utils.fprintf_list ~sep:" " pp_type)
+ (pp_print_list pp_type)
(List.map (fun v -> v.var_type) (reset_vars machines m));
fprintf fmt "(declare-rel %a (%a))@." pp_machine_step_name m.mname.node_id
- (Utils.fprintf_list ~sep:" " pp_type)
+ (pp_print_list pp_type)
(List.map (fun v -> v.var_type) (step_vars machines m));
pp_print_newline fmt ();
@@ -462,7 +460,7 @@ let print_machine machines fmt m =
fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a @[<v 0>%a)@]@]@.))@.@."
(pp_machine_reset machines)
m pp_machine_reset_name m.mname.node_id
- (Utils.fprintf_list ~sep:"@ " (pp_horn_var m))
+ (pp_print_list (pp_horn_var m))
(reset_vars machines m);
match m.mstep.step_asserts with
@@ -473,7 +471,7 @@ let print_machine machines fmt m =
ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@." pp_machine_step_name
m.mname.node_id
- (Utils.fprintf_list ~sep:"@ " (pp_horn_var m))
+ (pp_print_list (pp_horn_var m))
(step_vars machines m)
| assertsl ->
let pp_val =
@@ -487,7 +485,7 @@ let print_machine machines fmt m =
ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
fprintf fmt "@. %a)@ (%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val)
assertsl pp_machine_step_name m.mname.node_id
- (Utils.fprintf_list ~sep:" " (pp_horn_var m))
+ (pp_print_list (pp_horn_var m))
(step_vars machines m)))
let mk_flags arity =
@@ -527,11 +525,11 @@ let print_sfunction machines fmt m =
(* Check if there is annotation for s-function *)
if m.mannot != [] then
Format.fprintf fmt "; @[%a@]@]@\n"
- (Utils.fprintf_list ~sep:"@ " Printers.pp_s_function)
+ (pp_print_list Printers.pp_s_function)
m.mannot;
(* Printing variables *)
- Utils.fprintf_list ~sep:"@." pp_decl_var fmt
+ pp_print_list ~pp_open_box:pp_open_vbox0 pp_decl_var fmt
(step_vars machines m
@ rename_machine_list m.mname.node_id m.mstep.step_locals);
Format.pp_print_newline fmt ();
@@ -541,27 +539,27 @@ let print_sfunction machines fmt m =
(* Declaring single predicate *)
Format.fprintf fmt "(declare-rel %a (%a))@." pp_machine_stateless_name
m.mname.node_id
- (Utils.fprintf_list ~sep:" " pp_type)
+ (pp_print_list pp_type)
(List.map (fun v -> v.var_type) (reset_vars machines m));
Format.pp_print_newline fmt ();
(* Rule for single predicate *)
let str_flags = sf_name ^ " " ^ mk_flags (int_of_string flags) in
Format.fprintf fmt "@[<v 2>(rule (=> @ (%s %a) (%a %a)@]@.))@.@."
str_flags
- (Utils.fprintf_list ~sep:" " (pp_horn_var m))
+ (pp_print_list (pp_horn_var m))
(reset_vars machines m) pp_machine_stateless_name m.mname.node_id
- (Utils.fprintf_list ~sep:" " (pp_horn_var m))
+ (pp_print_list (pp_horn_var m))
(reset_vars machines m))
else (
(* Declaring predicate *)
Format.fprintf fmt "(declare-rel %a (%a))@." pp_machine_reset_name
m.mname.node_id
- (Utils.fprintf_list ~sep:" " pp_type)
+ (pp_print_list pp_type)
(List.map (fun v -> v.var_type) (inout_vars m));
Format.fprintf fmt "(declare-rel %a (%a))@." pp_machine_step_name
m.mname.node_id
- (Utils.fprintf_list ~sep:" " pp_type)
+ (pp_print_list pp_type)
(List.map (fun v -> v.var_type) (step_vars machines m));
Format.pp_print_newline fmt ();
@@ -573,7 +571,7 @@ let print_sfunction machines fmt m =
ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@." pp_machine_step_name
m.mname.node_id
- (Utils.fprintf_list ~sep:"@ " (pp_horn_var m))
+ (pp_print_list (pp_horn_var m))
(step_vars machines m)
| assertsl ->
let pp_val =
@@ -587,7 +585,7 @@ let print_sfunction machines fmt m =
ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
fprintf fmt "@. %a)(%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl
pp_machine_step_name m.mname.node_id
- (Utils.fprintf_list ~sep:" " (pp_horn_var m))
+ (pp_print_list (pp_horn_var m))
(step_vars machines m)))
(**************** XML printing functions *************)
@@ -606,9 +604,9 @@ let rec pp_xml_expr fmt expr =
| Expr_array a ->
fprintf fmt "[%a]" pp_xml_tuple a
| Expr_access (a, d) ->
- fprintf fmt "%a[%a]" pp_xml_expr a Dimension.pp_dimension d
+ fprintf fmt "%a[%a]" pp_xml_expr a Dimension.pp d
| Expr_power (a, d) ->
- fprintf fmt "(%a^%a)" pp_xml_expr a Dimension.pp_dimension d
+ fprintf fmt "(%a^%a)" pp_xml_expr a Dimension.pp d
| Expr_tuple el ->
fprintf fmt "(%a)" pp_xml_tuple el
| Expr_ite (c, t, e) ->
@@ -628,11 +626,11 @@ let rec pp_xml_expr fmt expr =
| Expr_appl (id, e, r) ->
pp_xml_app fmt id e r)
-and pp_xml_tuple fmt el = Utils.fprintf_list ~sep:"," pp_xml_expr fmt el
+and pp_xml_tuple fmt el = pp_comma_list pp_xml_expr fmt el
and pp_xml_handler fmt (t, h) = fprintf fmt "(%s -> %a)" t pp_xml_expr h
-and pp_xml_handlers fmt hl = Utils.fprintf_list ~sep:" " pp_xml_handler fmt hl
+and pp_xml_handlers fmt hl = pp_print_list pp_xml_handler fmt hl
and pp_xml_app fmt id e r =
match r with
@@ -684,7 +682,7 @@ and pp_xml_call fmt id e =
and pp_xml_eexpr fmt e =
fprintf fmt "%a%t %a"
- (Utils.fprintf_list ~sep:"; " Printers.pp_quantifiers)
+ (pp_print_list ~pp_sep:pp_print_semicolon Printers.pp_quantifiers)
e.eexpr_quantifiers
(fun fmt ->
match e.eexpr_quantifiers with [] -> () | _ -> fprintf fmt ";")
@@ -709,11 +707,12 @@ and pp_xml_s_function fmt expr_ann =
Format.pp_print_string fmt x
| _ ->
Format.fprintf fmt "%a"
- (Utils.fprintf_list ~sep:"/" Format.pp_print_string)
+ (pp_print_list ~pp_sep:(fun fmt () -> pp_print_string fmt "/")
+ pp_print_string)
kwds)
pp_xml_sf_value ee
in
- Utils.fprintf_list ~sep:"@ " pp_xml_annot fmt expr_ann.annots
+ pp_print_list pp_xml_annot fmt expr_ann.annots
and pp_xml_expr_annot fmt expr_ann =
let pp_xml_annot fmt (kwds, ee) =
@@ -726,11 +725,12 @@ and pp_xml_expr_annot fmt expr_ann =
Format.pp_print_string fmt x
| _ ->
Format.fprintf fmt "/%a/"
- (Utils.fprintf_list ~sep:"/" Format.pp_print_string)
+ (pp_print_list ~pp_sep:(fun fmt () -> pp_print_string fmt "/")
+ pp_print_string)
kwds)
pp_xml_eexpr ee
in
- Utils.fprintf_list ~sep:"@ " pp_xml_annot fmt expr_ann.annots
+ pp_print_list pp_xml_annot fmt expr_ann.annots
(* Local Variables: *)
(* compile-command:"make -C ../../.." *)
diff --git a/src/backends/Horn/horn_backend_printers.mli b/src/backends/Horn/horn_backend_printers.mli
index e69de29b..cefca734 100644
--- a/src/backends/Horn/horn_backend_printers.mli
+++ b/src/backends/Horn/horn_backend_printers.mli
@@ -0,0 +1,8 @@
+open Format
+open Lustre_types
+open Machine_code_types
+
+val pp_horn_var: machine_t -> formatter -> var_decl -> unit
+val pp_xml_expr: formatter -> expr -> unit
+val print_sfunction: machine_t list -> formatter -> machine_t -> unit
+val print_machine: machine_t list -> formatter -> machine_t -> unit
diff --git a/src/backends/Horn/horn_backend_traces.ml b/src/backends/Horn/horn_backend_traces.ml
index 6c26620b..c2c606b2 100644
--- a/src/backends/Horn/horn_backend_traces.ml
+++ b/src/backends/Horn/horn_backend_traces.ml
@@ -14,6 +14,7 @@
This is a modified version that handle reset *)
+open Utils
open Format
open Lustre_types
open Corelang
@@ -22,8 +23,7 @@ open Horn_backend_common
open Horn_backend_printers
let pp_traces =
- Utils.fprintf_list ~sep:", " (fun fmt (v, e) ->
- Format.fprintf fmt "%s -> %a" v Printers.pp_expr e)
+ pp_comma_list (fun fmt (v, e) -> fprintf fmt "%s -> %a" v Printers.pp_expr e)
(* Compute memories associated to each machine *)
let compute_mems machines m =
@@ -51,7 +51,7 @@ let machines_traces machines =
let filtered =
List.filter (fun (kwds, _) -> kwds = [ "traceability" ]) all_annots
in
- (* List.iter (Format.eprintf "Annots: %a@." Printers.pp_expr_annot)
+ (* List.iter (eprintf "Annots: %a@." Printers.pp_expr_annot)
(m.mannot); *)
let content = List.map snd filtered in
(* Elements are supposed to be a pair (tuple): variable, expression *)
@@ -68,7 +68,7 @@ let machines_traces machines =
assert false)
content
in
- (* Format.eprintf "Build traces: %a@." pp_traces traces; *)
+ (* eprintf "Build traces: %a@." pp_traces traces; *)
m, traces)
machines
@@ -90,7 +90,7 @@ let memories_old machines m =
(* eprintf "Unable to found variable %a in traces (%a)@."
Printers.pp_var v * pp_traces traces; *)
p,
- mkexpr Location.dummy_loc (Expr_ident v.var_id) ))
+ mkexpr Location.dummy (Expr_ident v.var_id) ))
(compute_mems machines m)
let memories_next machines m =
@@ -117,10 +117,10 @@ let memories_next machines m =
false)
m.mname.node_stmts
with _ ->
- Format.eprintf
+ eprintf
"Unable to find definition of %s in stmts %a@.prefix=%a@.@?"
var_id Printers.pp_node_stmts m.mname.node_stmts
- (Utils.fprintf_list ~sep:"," (fun fmt (id, n) ->
+ (pp_comma_list (fun fmt (id, n) ->
fprintf fmt "(%s,%s)" id n.mname.node_id))
(List.rev prefix);
@@ -140,23 +140,24 @@ let memories_next machines m =
prefix, def
| _ ->
eprintf "Mem Failure: (prefix: %a, eexpr: %a)@.@?"
- (Utils.fprintf_list ~sep:"," (fun fmt (id, n) ->
+ (pp_comma_list (fun fmt (id, n) ->
fprintf fmt "(%s,%s)" id n.mname.node_id))
(List.rev prefix) Printers.pp_expr ee;
assert false)
(memories_old machines m)
let pp_prefix_rev fmt prefix =
- Utils.fprintf_list ~sep:"."
+ pp_print_list ~pp_sep:(fun fmt () -> pp_print_string fmt ".")
(fun fmt (id, n) -> fprintf fmt "(%s,%s)" id n.mname.node_id)
fmt (List.rev prefix)
let traces_file fmt machines =
+ let pp_l = pp_print_list ~pp_sep:(fun fmt () -> pp_print_string fmt " | ") in
fprintf fmt "<?xml version=\"1.0\"?>@.";
fprintf fmt
"<Traces xmlns:xsi=\"http://www.w3.org/2001/XMLSchema-instance\">@.";
fprintf fmt "@[<v 5>@ %a@ @]@."
- (Utils.fprintf_list ~sep:"@ " (fun fmt m ->
+ (pp_print_list (fun fmt m ->
let pp_var = pp_horn_var m in
let memories_old = memories_old machines m in
let memories_next = memories_next machines m in
@@ -171,61 +172,45 @@ let traces_file fmt machines =
rename_machine_list m.mname.node_id m.mstep.step_outputs
in
fprintf fmt "<input name=\"%a\" type=\"%a\">%a</input>@ "
- (Utils.fprintf_list ~sep:" | " (pp_horn_var m))
- input_vars
- (Utils.fprintf_list ~sep:" | " (fun fmt id ->
- pp_type fmt id.var_type))
- input_vars
- (Utils.fprintf_list ~sep:" | " (pp_horn_var m))
- m.mstep.step_inputs;
+ (pp_l (pp_horn_var m)) input_vars
+ (pp_l (fun fmt id -> pp_type fmt id.var_type)) input_vars
+ (pp_l (pp_horn_var m)) m.mstep.step_inputs;
fprintf fmt "<output name=\"%a\" type=\"%a\">%a</output>@ "
- (Utils.fprintf_list ~sep:" | " pp_var)
- output_vars
- (Utils.fprintf_list ~sep:" | " (fun fmt id ->
- pp_type fmt id.var_type))
- output_vars
- (Utils.fprintf_list ~sep:" | " pp_var)
- m.mstep.step_outputs;
+ (pp_l pp_var) output_vars
+ (pp_l (fun fmt id -> pp_type fmt id.var_type)) output_vars
+ (pp_l pp_var) m.mstep.step_outputs;
let local_vars =
try full_memory_vars ~without_arrow:true machines m
with Not_found ->
- Format.eprintf "machine %s@.@?" m.mname.node_id;
+ eprintf "machine %s@.@?" m.mname.node_id;
assert false
in
let init_local_vars = rename_next_list local_vars in
let step_local_vars = rename_current_list local_vars in
fprintf fmt "<localInit name=\"%a\" type=\"%a\">%t%a</localInit>@ "
- (Utils.fprintf_list ~sep:" | " pp_var)
- init_local_vars
- (Utils.fprintf_list ~sep:" | " (fun fmt id ->
- pp_type fmt id.var_type))
+ (pp_l pp_var)
init_local_vars
+ (pp_l (fun fmt id -> pp_type fmt id.var_type)) init_local_vars
(fun fmt ->
match memories_next with [] -> () | _ -> fprintf fmt "")
- (Utils.fprintf_list ~sep:" | " (fun fmt (_, ee) ->
- fprintf fmt "%a" pp_xml_expr ee))
+ (pp_l (fun fmt (_, ee) -> fprintf fmt "%a" pp_xml_expr ee))
memories_next;
fprintf fmt "<localStep name=\"%a\" type=\"%a\">%t%a</localStep>@ "
- (Utils.fprintf_list ~sep:" | " pp_var)
- step_local_vars
- (Utils.fprintf_list ~sep:" | " (fun fmt id ->
- pp_type fmt id.var_type))
- step_local_vars
+ (pp_l pp_var) step_local_vars
+ (pp_l (fun fmt id -> pp_type fmt id.var_type)) step_local_vars
(fun fmt -> match memories_old with [] -> () | _ -> fprintf fmt "")
- (Utils.fprintf_list ~sep:" | " (fun fmt (_, ee) ->
- fprintf fmt "(%a)" pp_xml_expr ee))
+ (pp_l (fun fmt (_, ee) -> fprintf fmt "(%a)" pp_xml_expr ee))
memories_old;
let arrow_vars = arrow_vars machines m in
let arrow_vars_curr = rename_current_list arrow_vars
and arrow_vars_mid = rename_mid_list arrow_vars
and arrow_vars_next = rename_next_list arrow_vars in
- Utils.fprintf_list ~sep:"@ "
- (fun fmt v -> fprintf fmt "<reset name=\"%a\"/>" pp_var v)
+ pp_print_list (fun fmt v -> fprintf fmt "<reset name=\"%a\"/>" pp_var v)
fmt
(arrow_vars_curr @ arrow_vars_mid @ arrow_vars_next);
fprintf fmt "@]@ </Node>"))
diff --git a/src/backends/Horn/horn_backend_traces.mli b/src/backends/Horn/horn_backend_traces.mli
index e69de29b..d17ec562 100644
--- a/src/backends/Horn/horn_backend_traces.mli
+++ b/src/backends/Horn/horn_backend_traces.mli
@@ -0,0 +1 @@
+val traces_file: Format.formatter -> Machine_code_types.machine_t list -> unit
diff --git a/src/backends/backends.mli b/src/backends/backends.mli
index 80fcce8c..ec0b6e10 100644
--- a/src/backends/backends.mli
+++ b/src/backends/backends.mli
@@ -1,3 +1,4 @@
val setup: unit -> unit
val is_functional: unit -> bool
val join_guards: bool ref
+val get_normalization_params: unit -> Normalization.param_t
diff --git a/src/basic_library.mli b/src/basic_library.mli
index 2727025c..f5fd8f4e 100644
--- a/src/basic_library.mli
+++ b/src/basic_library.mli
@@ -10,6 +10,7 @@ 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 is_numeric_operator: ident -> bool
val type_env: Types.t Env.t
val clock_env: Clocks.t Env.t
diff --git a/src/causality.ml b/src/causality.ml
index 643f4fc4..a23f9800 100644
--- a/src/causality.ml
+++ b/src/causality.ml
@@ -692,17 +692,15 @@ let pp_dep_graph fmt g =
let pp_error fmt err =
match err with
| NodeCycle trace ->
- Format.fprintf fmt "Causality error, cyclic node calls:@ @[<v 0>%a@]@ "
- (fprintf_list ~sep:",@ " Format.pp_print_string)
- trace
+ Format.(fprintf fmt "Causality error, cyclic node calls:@ @[<v 0>%a@]@ "
+ (pp_comma_list Format.pp_print_string) trace)
| DataCycle traces ->
- Format.fprintf fmt
- "Causality error, cyclic data dependencies:@ @[<v 0>%a@]@ "
- (fprintf_list ~sep:";@ " (fun fmt trace ->
- Format.fprintf fmt "@[<v 0>{%a}@]"
- (fprintf_list ~sep:",@ " Format.pp_print_string)
- trace))
- traces
+ Format.(fprintf fmt
+ "Causality error, cyclic data dependencies:@ @[<v 0>%a@]@ "
+ (pp_print_list ~pp_sep:pp_print_semicolon (fun fmt trace ->
+ fprintf fmt "@[<v 0>{%a}@]"
+ (pp_comma_list Format.pp_print_string) trace))
+ traces)
(* Merges elements of graph [g2] into graph [g1] *)
let merge_with g1 g2 =
diff --git a/src/causality.mli b/src/causality.mli
index cebaffce..a520a169 100644
--- a/src/causality.mli
+++ b/src/causality.mli
@@ -10,9 +10,14 @@ exception Error of error
val pp_error: Format.formatter -> error -> unit
+val world: ident
+
module NodeDep: sig
val dependence_graph: program_t -> IdentDepGraph.t
val filter_static_inputs: var_decl list -> expr list -> Dimension.t list
+ val compute_generic_calls: program_t -> unit
+ val get_callee: expr -> (ident * expr list) option
+ val get_calls: (ident -> bool) -> node_desc -> expr list
end
(* Look for cycles in a dependency graph *)
@@ -32,9 +37,14 @@ module ExprDep: sig
val mk_instance_var: ident -> ident
val is_instance_var: ident -> bool
val is_ghost_var: ident -> bool
+ val is_read_var: ident -> bool
val undo_instance_var: ident -> ident
+ val undo_read_var: ident -> ident
val node_eq_equiv: node_desc -> (ident, ident) Hashtbl.t
val node_input_variables: node_desc -> ISet.t
+ val node_local_variables: node_desc -> ISet.t
+ val node_output_variables: node_desc -> ISet.t
+ val node_memory_variables: node_desc -> ISet.t
end
(* Module used to compute static disjunction of variables based upon their
@@ -46,7 +56,11 @@ module Disjunction: sig
order, maybe removing shorter branches *)
type disjoint_map = (ident, CISet.t) Hashtbl.t
+ val pp_ciset: Format.formatter -> CISet.t -> unit
+
val clock_disjoint_map: var_decl list -> disjoint_map
+
+ val pp_disjoint_map: Format.formatter -> disjoint_map -> unit
end
(* Tests whether [v] is a root of graph [g], i.e. a source *)
diff --git a/src/checks/access.ml b/src/checks/access.ml
index f0b58fa9..36fa1e0c 100644
--- a/src/checks/access.ml
+++ b/src/checks/access.ml
@@ -28,9 +28,9 @@ open Corelang
module ConstraintModule = struct
(* bool dimension module *)
- type t = Dimension.dim_expr
+ type t = Dimension.t
- let equal d1 d2 = Dimension.is_eq_dimension d1 d2
+ let equal d1 d2 = Dimension.equal d1 d2
let compare d1 d2 =
if equal d1 d2 then 0 else compare d1.Dimension.dim_id d2.Dimension.dim_id
diff --git a/src/checks/access.mli b/src/checks/access.mli
index e69de29b..b17b3877 100644
--- a/src/checks/access.mli
+++ b/src/checks/access.mli
@@ -0,0 +1 @@
+val check_prog: Lustre_types.program_t -> unit
diff --git a/src/checks/algebraicLoop.ml b/src/checks/algebraicLoop.ml
index 2a7dd242..07de6846 100644
--- a/src/checks/algebraicLoop.ml
+++ b/src/checks/algebraicLoop.ml
@@ -77,10 +77,10 @@ end
resolution*)
let pp_resolution fmt resolution =
- fprintf_list ~sep:"@ "
- (fun fmt (eq, _) ->
- Format.fprintf fmt "inlining: %a" Printers.pp_node_eq eq)
- fmt resolution
+ Format.(pp_print_list
+ (fun fmt (eq, _) ->
+ fprintf fmt "inlining: %a" Printers.pp_node_eq eq)
+ fmt resolution)
let al_is_solved (_, als) = List.for_all (fun (_, _, status) -> status) als
@@ -132,11 +132,11 @@ let is_expr_inlined nd expr =
assert false)
let pp_calls nd fmt calls =
- Format.fprintf fmt "@[<v 0>%a@]"
- (fprintf_list ~sep:"@ " (fun fmt (funid, expr, _) ->
- Format.fprintf fmt "%s: %i (inlined:%b)" funid expr.expr_tag
- (is_expr_inlined nd expr)))
- calls
+ Format.(fprintf fmt "@[<v 0>%a@]"
+ (pp_print_list (fun fmt (funid, expr, _) ->
+ fprintf fmt "%s: %i (inlined:%b)" funid expr.expr_tag
+ (is_expr_inlined nd expr)))
+ calls)
(* Inline the provided expression *)
let inline_expr node expr =
@@ -354,10 +354,10 @@ let pp_al nd fmt (partition, calls, _) =
let open Format in
fprintf fmt "@[<v 0>";
fprintf fmt "variables in the alg. loop: @[<hov 0>%a@]@ "
- (fprintf_list ~sep:",@ " pp_print_string)
+ (pp_comma_list pp_print_string)
partition;
fprintf fmt "@ involved node calls: @[<v 0>%a@]@ "
- (fprintf_list ~sep:",@ " (fun fmt ((funid, expr, _), status) ->
+ (pp_comma_list (fun fmt ((funid, expr, _), status) ->
fprintf fmt "%s" funid;
if status && is_expr_inlined nd expr then
fprintf fmt " (inlining it solves the alg. loop)"))
@@ -372,7 +372,7 @@ let pp_al nd fmt (partition, calls, _) =
let pp_report fmt report =
let open Format in
- fprintf_list ~sep:"@."
+ pp_print_list ~pp_open_box:pp_open_vbox0
(fun _ (nd, als) ->
let top = Corelang.node_from_name nd.node_id in
let pp =
@@ -385,8 +385,7 @@ let pp_report fmt report =
in
pp top.top_decl_loc (fun fmt ->
fprintf fmt "algebraic loop in node %s: {@[<v 0>%a@]}" nd.node_id
- (fprintf_list ~sep:"@ " (pp_al nd))
- als))
+ (pp_print_list (pp_al nd)) als))
fmt report;
fprintf fmt "@."
@@ -406,7 +405,7 @@ let analyze cpt prog =
(* TODO create a report *)
(* Printing the report on stderr *)
Format.eprintf "%a" pp_report report;
- raise (Error.Error (Location.dummy_loc, Error.AlgebraicLoop)))
+ raise (Error.Error (Location.dummy, Error.AlgebraicLoop)))
in
(* Printing the report on stderr *)
Format.eprintf "%a" pp_report report;
diff --git a/src/checks/algebraicLoop.mli b/src/checks/algebraicLoop.mli
index e69de29b..ea154812 100644
--- a/src/checks/algebraicLoop.mli
+++ b/src/checks/algebraicLoop.mli
@@ -0,0 +1,4 @@
+open Utils
+open Lustre_types
+
+val analyze: program_t -> program_t * Scheduling_type.schedule_report IMap.t
diff --git a/src/clock_calculus.mli b/src/clock_calculus.mli
index 2a57b425..130c0735 100644
--- a/src/clock_calculus.mli
+++ b/src/clock_calculus.mli
@@ -7,3 +7,5 @@ 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
+
+val uneval_prog_generics: program_t -> unit
diff --git a/src/clocks.mli b/src/clocks.mli
index 63f8688a..d7a19be6 100644
--- a/src/clocks.mli
+++ b/src/clocks.mli
@@ -45,7 +45,10 @@ type error =
| Carrier_extrusion of t * carrier_expr
| Clock_extrusion of t * t
+(* Nice pretty-printing. Simplifies expressions before printing them. Non-linear
+ complexity. *)
val pp: Format.formatter -> t -> unit
+
val pp_suffix: Format.formatter -> t -> unit
val new_var: bool -> t
@@ -86,6 +89,9 @@ val get_carrier_name: t -> carrier_expr option
val equal: t -> t -> bool
+(* Disjunction relation between variables based upon their static clocks. *)
+val disjoint: t -> t -> bool
+
val const_of_carrier: carrier_expr -> ident
val pp_error: Format.formatter -> error -> unit
diff --git a/src/compiler_common.mli b/src/compiler_common.mli
index 89d9d3d0..d0bf8196 100644
--- a/src/compiler_common.mli
+++ b/src/compiler_common.mli
@@ -11,3 +11,16 @@ val check_compatibility: program_t * Types.t Env.t * Clocks.t Env.t ->
val update_vdecl_parents_prog: program_t -> unit
val expand_automata: program_t -> program_t
+
+(* Process each node/imported node and introduce the associated contract node *)
+val resolve_contracts: program_t -> program_t
+
+val force_stateful_decls: program_t -> unit
+
+val check_stateless_decls: program_t -> unit
+
+val type_decls: Types.t Env.t -> program_t -> Types.t Env.t
+
+val clock_decls: Clocks.t Env.t -> program_t -> Clocks.t Env.t
+
+val create_dest_dir: unit -> unit
diff --git a/src/compiler_stages.ml b/src/compiler_stages.ml
index b3bb823b..93092726 100644
--- a/src/compiler_stages.ml
+++ b/src/compiler_stages.ml
@@ -93,9 +93,9 @@ let stage1 params prog dirname basename extension =
Global.main_node := main_node;
try ignore (Corelang.node_from_name main_node)
with Not_found ->
- Format.eprintf "Code generation error: %a@." Error.pp_error_msg
+ Format.eprintf "Code generation error: %a@." Error.pp
Error.Main_not_found;
- raise (Error.Error (Location.dummy_loc, Error.Main_not_found)))
+ raise (Error.Error (Location.dummy, Error.Main_not_found)))
in
(* Perform inlining before any analysis *)
@@ -249,9 +249,10 @@ let stage2 params prog =
(* printing code *)
let stage3 prog machine_code dependencies basename extension =
+ let open Options in
let basename = Filename.basename basename in
- match !Options.output, extension with
- | "C", ".lus" ->
+ match !output, extension with
+ | OutC, ".lus" ->
Log.report ~level:1 (fun fmt -> fprintf fmt ".. C code generation@,");
C_backend.translate_to_c !generate_c_header
(* alloc_header_file source_lib_file source_main_file makefile_file *)
@@ -260,11 +261,11 @@ let stage3 prog machine_code dependencies basename extension =
ACSL annotations generation@,"); ACSL_backend.translate_to_acsl (*
alloc_header_file source_lib_file source_main_file makefile_file *)
basename prog machine_code dependencies end *)
- | "C", _ ->
+ | OutC, _ ->
C_backend.print_c_header basename;
Log.report ~level:1 (fun fmt ->
fprintf fmt ".. no C code generation for lusi@,")
- | "java", _ ->
+ | OutJava, _ ->
Format.eprintf "internal error: sorry, but not yet supported !";
assert false
(*let source_file = basename ^ ".java" in Log.report ~level:1 (fun fmt ->
@@ -273,11 +274,11 @@ let stage3 prog machine_code dependencies basename extension =
Log.report ~level:1 (fun fmt -> fprintf fmt ".. java code generation@,@?");
Java_backend.translate_to_java source_fmt basename normalized_prog
machine_code;*)
- | "Ada", _ ->
+ | OutAda, _ ->
Log.report ~level:1 (fun fmt -> fprintf fmt ".. Ada code generation@.");
Ada_backend.translate_to_ada basename
(Machine_code_common.arrow_machine :: machine_code)
- | "horn", _ ->
+ | OutHorn, _ ->
let destname = !Options.dest_dir ^ "/" ^ basename in
let source_file = destname ^ ".smt2" in
(* Could be changed *)
@@ -294,7 +295,7 @@ let stage3 prog machine_code dependencies basename extension =
let fmt = formatter_of_out_channel traces_out in
Log.report ~level:1 (fun fmt -> fprintf fmt ".. tracing info@,");
Horn_backend_traces.traces_file fmt machine_code)
- | "lustre", _ ->
+ | OutLustre, _ ->
let destname = !Options.dest_dir ^ "/" ^ basename in
let source_file = destname ^ ".lustrec" ^ extension in
(* Could be changed *)
@@ -306,7 +307,7 @@ let stage3 prog machine_code dependencies basename extension =
Format.fprintf fmt "@.@?";
(* Lustre_backend.translate fmt basename normalized_prog machine_code *)
()
- | "emf", _ ->
+ | OutEMF, _ ->
let destname = !Options.dest_dir ^ "/" ^ basename in
let source_file = destname ^ ".json" in
(* Could be changed *)
@@ -314,5 +315,3 @@ let stage3 prog machine_code dependencies basename extension =
let fmt = formatter_of_out_channel source_out in
EMF_backend.translate fmt basename prog machine_code;
()
- | _ ->
- assert false
diff --git a/src/inliner.mli b/src/inliner.mli
index e69de29b..53902b18 100644
--- a/src/inliner.mli
+++ b/src/inliner.mli
@@ -0,0 +1,7 @@
+open Utils
+open Lustre_types
+
+val global_inline: program_t -> program_t
+val local_inline: program_t -> program_t
+
+val keyword: ident list
diff --git a/src/machine_code_common.mli b/src/machine_code_common.mli
index ae2ba454..2434f8e1 100644
--- a/src/machine_code_common.mli
+++ b/src/machine_code_common.mli
@@ -111,6 +111,8 @@ val join_guards_list :
val machine_vars : machine_t -> var_decl list
+val get_machine: machine_t list -> ident -> machine_t
+
module PrintSpec : sig
val pp_spec :
machine_t ->
diff --git a/src/optimize_machine.mli b/src/optimize_machine.mli
index e69de29b..4f02cf59 100644
--- a/src/optimize_machine.mli
+++ b/src/optimize_machine.mli
@@ -0,0 +1,16 @@
+open Utils
+open Lustre_types
+open Machine_code_types
+
+(* This functions produces an optimzed prog * machines It 1- eliminates common
+ sub-expressions (TODO how is this different from normalization?) 2- inline
+ constants and eliminate duplicated variables 3- try to reuse variables
+ whenever possible
+
+ When item (2) identified eliminated variables, the initial prog is modified,
+ its normalized recomputed, as well as its scheduling, before regenerating the
+ machines.
+
+ The function returns both the (possibly updated) prog as well as the machines *)
+val optimize: Normalization.param_t -> program_t -> Scheduling_type.schedule_report IMap.t ->
+ machine_t list -> program_t * machine_t list
diff --git a/src/optimize_prog.mli b/src/optimize_prog.mli
index e69de29b..3b481a78 100644
--- a/src/optimize_prog.mli
+++ b/src/optimize_prog.mli
@@ -0,0 +1,3 @@
+open Lustre_types
+
+val prog_unfold_consts: program_t -> program_t
diff --git a/src/options.ml b/src/options.ml
index e19289a8..7b96237e 100644
--- a/src/options.ml
+++ b/src/options.ml
@@ -37,6 +37,7 @@ let spec = ref SpecNo
type option_output =
| OutC
| OutAda
+ | OutJava
| OutEMF
| OutHorn
| OutLustre
@@ -47,6 +48,7 @@ let pp_output fmt =
Format.pp_print_string fmt (match !output with
| OutC -> "C"
| OutAda -> "Ada"
+ | OutJava -> "Java"
| OutEMF -> "EMF"
| OutHorn -> "Horn"
| OutLustre -> "Lustre")
diff --git a/src/options.mli b/src/options.mli
index 9a9d5206..80d63d3b 100644
--- a/src/options.mli
+++ b/src/options.mli
@@ -16,6 +16,7 @@ val spec: option_spec ref
type option_output =
| OutC
| OutAda
+ | OutJava
| OutEMF
| OutHorn
| OutLustre
@@ -76,3 +77,7 @@ val nb_mutants: int ref
val gen_mcdc: bool ref
val no_mutation_suffix: bool ref
+
+val compile_header: bool ref
+
+val track_exceptions: bool ref
diff --git a/src/options_management.mli b/src/options_management.mli
index 9447f369..625d7fc8 100644
--- a/src/options_management.mli
+++ b/src/options_management.mli
@@ -4,3 +4,5 @@ val plugin_opt: string * (unit -> unit) * (Format.formatter -> unit) *
val name_dependency: ('a * string) -> string -> string
val get_witness_dir: string -> string
+
+val verifier_opt: string * (unit -> unit) * (string * Arg.spec * string) list -> (string * Arg.spec * string) list
diff --git a/src/plugins/mpfr/lustrec_mpfr.mli b/src/plugins/mpfr/lustrec_mpfr.mli
index 60f43087..c055cae8 100644
--- a/src/plugins/mpfr/lustrec_mpfr.mli
+++ b/src/plugins/mpfr/lustrec_mpfr.mli
@@ -1 +1,19 @@
+open Utils
+open Format
+open Lustre_types
+open Machine_code_types
+
val unfoldable_value: Machine_code_types.value_t -> bool
+val inject_prog: program_t -> program_t
+
+val mpfr_t: string
+
+val mpfr_rnd: unit -> string
+val mpfr_prec: unit -> int
+
+val is_homomorphic_fun: ident -> bool
+
+val pp_inject_init: (formatter -> 'a -> unit) -> formatter -> 'a -> unit
+val pp_inject_clear: (formatter -> 'a -> unit) -> formatter -> 'a -> unit
+val pp_inject_assign: (formatter -> value_t -> unit) -> formatter -> value_t * value_t -> unit
+val pp_inject_real: (formatter -> 'a -> unit) -> (formatter -> 'b -> unit) -> formatter -> 'a * 'b -> unit
diff --git a/src/plugins/plugins.mli b/src/plugins/plugins.mli
index 093db4ae..5e9c3d2a 100644
--- a/src/plugins/plugins.mli
+++ b/src/plugins/plugins.mli
@@ -2,3 +2,8 @@ open Utils
open Lustre_types
val inline_annots: (ident -> ident) -> expr_annot list -> expr_annot list
+
+val check_force_stateful: unit -> bool
+
+val c_backend_main_loop_body_prefix: string -> string -> Format.formatter -> unit -> unit
+val c_backend_main_loop_body_suffix: Format.formatter -> unit -> unit
diff --git a/src/printers.mli b/src/printers.mli
index 6d4f55c4..5328d2c9 100644
--- a/src/printers.mli
+++ b/src/printers.mli
@@ -6,12 +6,17 @@ 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_var_name: formatter -> var_decl -> unit
val pp_node_eq: formatter -> eq -> unit
val pp_node_eqs: formatter -> eq list -> unit
+val pp_node_stmts: formatter -> statement list -> unit
val pp_spec: formatter -> contract_desc -> unit
val pp_expr_annot: formatter -> expr_annot -> unit
+val pp_s_function: 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
+val pp_prog_short: formatter -> program_t -> unit
+val pp_quantifiers: formatter -> quantifier_type * var_decl list -> unit
diff --git a/src/scheduling.mli b/src/scheduling.mli
index 8d7a6128..998bd942 100644
--- a/src/scheduling.mli
+++ b/src/scheduling.mli
@@ -1,9 +1,16 @@
open Utils
+open Format
open Lustre_types
open Scheduling_type
+val schedule_node: node_desc -> schedule_report
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
+
+val pp_warning_unused: formatter -> schedule_report IMap.t -> unit
+val pp_schedule: formatter -> schedule_report IMap.t -> unit
+val pp_fanin_table: formatter -> schedule_report IMap.t -> unit
+val pp_dep_graph: formatter -> schedule_report IMap.t -> unit
diff --git a/src/spec.mli b/src/spec.mli
index e69de29b..ed915864 100644
--- a/src/spec.mli
+++ b/src/spec.mli
@@ -0,0 +1,3 @@
+open Lustre_types
+
+val enforce_spec_prog: program_t -> program_t
diff --git a/src/tools/stateflow/common/activeStates.ml b/src/tools/stateflow/common/activeStates.ml
index 48fb21b2..5a27430b 100644
--- a/src/tools/stateflow/common/activeStates.ml
+++ b/src/tools/stateflow/common/activeStates.ml
@@ -1,3 +1,4 @@
+open Utils
open Basetypes
(* Module to manipulate set of active states.
@@ -13,10 +14,7 @@ module Vars = struct
end)
let pp_set fmt rho =
- Format.fprintf fmt "@[<v 0>%a@ @]"
- (Utils.fprintf_list ~sep:"@ " (fun fmt p ->
- Format.fprintf fmt "%a" pp_path p))
- (elements rho)
+ Format.(fprintf fmt "@[<v 0>%a@ @]" (pp_print_list pp_path) (elements rho))
end
module Env = struct
@@ -37,8 +35,7 @@ module Env = struct
let keys a = fold (fun key _ -> Vars.add key) a Vars.empty
let pp_env fmt rho =
- Format.fprintf fmt "@[<v 0>%a@ @]"
- (Utils.fprintf_list ~sep:"@ " (fun fmt (p, b) ->
- Format.fprintf fmt "%a -> %b" pp_path p b))
- (bindings rho)
+ Format.(fprintf fmt "@[<v 0>%a@ @]"
+ (pp_print_list (fun fmt (p, b) -> fprintf fmt "%a -> %b" pp_path p b))
+ (bindings rho))
end
diff --git a/src/tools/stateflow/common/activeStates.mli b/src/tools/stateflow/common/activeStates.mli
new file mode 100644
index 00000000..e5b95131
--- /dev/null
+++ b/src/tools/stateflow/common/activeStates.mli
@@ -0,0 +1,7 @@
+module Vars: Set.S with type elt = Basetypes.path_t
+
+module Env: sig
+ include Map.S with type key = Basetypes.path_t
+
+ val from_set: Vars.t -> 'a -> 'a t
+end
diff --git a/src/tools/stateflow/common/basetypes.ml b/src/tools/stateflow/common/basetypes.ml
index 3f082709..3eb1af45 100644
--- a/src/tools/stateflow/common/basetypes.ml
+++ b/src/tools/stateflow/common/basetypes.ml
@@ -33,7 +33,8 @@ let pp_state_name = Format.pp_print_string
let pp_junction_name = Format.pp_print_string
-let pp_path fmt p = Utils.fprintf_list ~sep:"." pp_state_name fmt p
+let pp_path fmt p =
+ Utils.Format.pp_print_list ~pp_sep:(fun fmt () -> Format.pp_print_string fmt ".") pp_state_name fmt p
let pp_event fmt e =
match e with
diff --git a/src/tools/stateflow/common/basetypes.mli b/src/tools/stateflow/common/basetypes.mli
new file mode 100644
index 00000000..286a40b2
--- /dev/null
+++ b/src/tools/stateflow/common/basetypes.mli
@@ -0,0 +1,77 @@
+type state_name_t = string
+
+type junction_name_t = string
+
+type path_t = state_name_t list
+
+type event_base_t = string
+
+type event_t = event_base_t option
+
+type user_variable_name_t = string
+
+(* Connected to lustrec types *)
+type base_action_t = {
+ defs : Lustre_types.statement list;
+ ainputs : Lustre_types.var_decl list;
+ aoutputs : Lustre_types.var_decl list;
+ avariables : Lustre_types.var_decl list; (* ident: string; *)
+}
+
+type base_condition_t = {
+ expr : Lustre_types.expr;
+ cinputs : Lustre_types.var_decl list;
+ coutputs : Lustre_types.var_decl list;
+ cvariables : Lustre_types.var_decl list;
+}
+
+val pp_state_name: Format.formatter -> state_name_t -> unit
+val pp_junction_name: Format.formatter -> junction_name_t -> unit
+val pp_path: Format.formatter -> path_t -> unit
+
+type frontier_t = Loose | Strict
+
+type _ call_t =
+ | Ecall : (path_t * path_t * frontier_t) call_t
+ | Dcall : path_t call_t
+ | Xcall : (path_t * frontier_t) call_t
+
+(* Conditions are either (1) simple strings, (2) the active status of a state or
+ (3) occurence of an event. They can be combined (conjunction, negation) *)
+module type ConditionType = sig
+ type t
+
+ val cquote : base_condition_t -> t
+
+ val tru : t
+
+ val active : path_t -> t
+
+ val event : event_t -> t
+
+ val ( && ) : t -> t -> t
+
+ val neg : t -> t
+
+ val pp_cond : Format.formatter -> t -> unit
+end
+
+module Condition: ConditionType
+
+module type ActionType = sig
+ type t
+
+ val nil : t
+
+ val aquote : base_action_t -> t
+
+ val open_path : path_t -> t
+
+ val close_path : path_t -> t
+
+ val call : 'c call_t -> 'c -> t
+
+ val pp_act : Format.formatter -> t -> unit
+end
+
+module Action: ActionType
diff --git a/src/tools/stateflow/common/datatype.ml b/src/tools/stateflow/common/datatype.ml
index 458702ee..8d730162 100644
--- a/src/tools/stateflow/common/datatype.ml
+++ b/src/tools/stateflow/common/datatype.ml
@@ -1,3 +1,4 @@
+open Utils
open Basetypes
(* open ActiveEnv *)
@@ -119,20 +120,20 @@ module SF = struct
t.condition_act Action.pp_act t.transition_act pp_dest t.dest
let pp_transitions fmt l =
- Format.fprintf fmt "@[<hov 0>[@[<hov 0>%a@]@ ]@]"
- (Utils.fprintf_list ~sep:";@ " pp_trans)
- l
+ Format.(fprintf fmt "@[<hov 0>[@[<hov 0>%a@]@ ]@]"
+ (pp_print_list ~pp_sep:pp_print_semicolon pp_trans)
+ l)
let pp_comp fmt c =
match c with
| Or (_T, _S) ->
- Format.fprintf fmt "Or(%a, {%a})" pp_transitions _T
- (Utils.fprintf_list ~sep:"; " pp_state_name)
- _S
+ Format.(fprintf fmt "Or(%a, {%a})" pp_transitions _T
+ (pp_print_list ~pp_sep:pp_print_semicolon pp_state_name)
+ _S)
| And _S ->
- Format.fprintf fmt "And({%a})"
- (Utils.fprintf_list ~sep:"; " pp_state_name)
- _S
+ Format.(fprintf fmt "And({%a})"
+ (pp_print_list ~pp_sep:pp_print_semicolon pp_state_name)
+ _S)
let pp_state_actions fmt sa =
Format.fprintf fmt "@[<hov 0>(%a,@ %a,@ %a)@]" Action.pp_act sa.entry_act
@@ -144,25 +145,23 @@ module SF = struct
pp_transitions s.inner_trans pp_comp s.internal_composition
let pp_src pp_sffunction fmt src =
- Format.fprintf fmt "@[<v>%a@ @]"
- (Utils.fprintf_list ~sep:"@ @ " (fun fmt src ->
- match src with
- | State (p, def) ->
- Format.fprintf fmt "%a: %a" pp_path p pp_state def
- | Junction (s, tl) ->
- Format.fprintf fmt "%a: %a" pp_state_name s pp_transitions tl
- | SFFunction p ->
- pp_sffunction fmt p))
- src
+ Format.(fprintf fmt "@[<v>%a@ @]"
+ (pp_print_list ~pp_sep:pp_print_cutcut (fun fmt src ->
+ match src with
+ | State (p, def) ->
+ Format.fprintf fmt "%a: %a" pp_path p pp_state def
+ | Junction (s, tl) ->
+ Format.fprintf fmt "%a: %a" pp_state_name s pp_transitions tl
+ | SFFunction p ->
+ pp_sffunction fmt p))
+ src)
let rec pp_sffunction fmt (Program (name, component_list, _)) =
Format.fprintf fmt "SFFunction name: %s@ %a@ " name (pp_src pp_sffunction)
component_list
let pp_vars fmt src =
- Format.fprintf fmt "@[<v>%a@ @]"
- (Utils.fprintf_list ~sep:"@ " Printers.pp_var)
- src
+ Format.(fprintf fmt "@[<v>%a@ @]" (pp_print_list Printers.pp_var) src)
let pp_prog fmt (Program (name, component_list, vars)) =
Format.fprintf fmt "Main node name: %s@ %a@ %a@" name (pp_src pp_sffunction)
diff --git a/src/tools/stateflow/common/datatype.mli b/src/tools/stateflow/common/datatype.mli
new file mode 100644
index 00000000..1aa9830e
--- /dev/null
+++ b/src/tools/stateflow/common/datatype.mli
@@ -0,0 +1,53 @@
+open Basetypes
+
+(* Type definitions of a model *)
+
+type destination_t = DPath of path_t | DJunction of junction_name_t
+
+type trans_t = {
+ event : event_t;
+ condition : Condition.t;
+ condition_act : Action.t;
+ transition_act : Action.t;
+ dest : destination_t;
+}
+
+type transitions_t = trans_t list
+
+type composition_t =
+ | Or of transitions_t * state_name_t list
+ | And of state_name_t list
+
+type state_actions_t = {
+ entry_act : Action.t;
+ during_act : Action.t;
+ exit_act : Action.t;
+}
+
+type state_def_t = {
+ state_actions : state_actions_t;
+ outer_trans : transitions_t;
+ inner_trans : transitions_t;
+ internal_composition : composition_t;
+}
+
+type 'prog_t src_components_t =
+ | State of path_t * state_def_t
+ | Junction of junction_name_t * transitions_t
+ | SFFunction of 'prog_t
+
+type prog_t =
+ | Program of
+ state_name_t
+ * prog_t src_components_t list
+ * (Lustre_types.var_decl * Lustre_types.expr) list
+
+type trace_t = event_t list
+
+module type MODEL_T = sig
+ val name : string
+
+ val model : prog_t
+
+ val traces : trace_t list
+end
diff --git a/src/tools/stateflow/json-parser/json_parser.mli b/src/tools/stateflow/json-parser/json_parser.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/tools/stateflow/json-parser/main_parse_json_file.mli b/src/tools/stateflow/json-parser/main_parse_json_file.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/tools/stateflow/json-parser/test_json_parser_variables.mli b/src/tools/stateflow/json-parser/test_json_parser_variables.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/tools/stateflow/models/model_medium.mli b/src/tools/stateflow/models/model_medium.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/tools/stateflow/models/model_simple.mli b/src/tools/stateflow/models/model_simple.mli
new file mode 100644
index 00000000..62e4c0f5
--- /dev/null
+++ b/src/tools/stateflow/models/model_simple.mli
@@ -0,0 +1,7 @@
+open Datatype
+
+val name : string
+
+val model : prog_t
+
+val traces : trace_t list
diff --git a/src/tools/stateflow/models/model_stopwatch.mli b/src/tools/stateflow/models/model_stopwatch.mli
new file mode 100644
index 00000000..62e4c0f5
--- /dev/null
+++ b/src/tools/stateflow/models/model_stopwatch.mli
@@ -0,0 +1,7 @@
+open Datatype
+
+val name : string
+
+val model : prog_t
+
+val traces : trace_t list
diff --git a/src/tools/stateflow/semantics/cPS.mli b/src/tools/stateflow/semantics/cPS.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/tools/stateflow/semantics/cPS_ccode_generator.mli b/src/tools/stateflow/semantics/cPS_ccode_generator.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/tools/stateflow/semantics/cPS_evaluator.mli b/src/tools/stateflow/semantics/cPS_evaluator.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/tools/stateflow/semantics/cPS_interpreter.mli b/src/tools/stateflow/semantics/cPS_interpreter.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/tools/stateflow/semantics/cPS_lustre_generator.mli b/src/tools/stateflow/semantics/cPS_lustre_generator.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/tools/stateflow/semantics/cPS_transformer.mli b/src/tools/stateflow/semantics/cPS_transformer.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/tools/stateflow/semantics/theta.mli b/src/tools/stateflow/semantics/theta.mli
new file mode 100644
index 00000000..e69de29b
diff --git a/src/type_predef.mli b/src/type_predef.mli
index a8d57a57..23f8c8aa 100644
--- a/src/type_predef.mli
+++ b/src/type_predef.mli
@@ -30,3 +30,5 @@ 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
+val type_arrow: Types.t -> Types.t -> Types.t
+val type_array: Dimension.t -> Types.t -> Types.t
diff --git a/src/typing.mli b/src/typing.mli
index d0b2a9aa..f9201a10 100644
--- a/src/typing.mli
+++ b/src/typing.mli
@@ -26,3 +26,9 @@ 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
+
+val uneval_prog_generics: program_t -> unit
+
+(* Equality on ground types only *)
+(* Should be used between local variables which must have a ground type *)
+val eq_ground: Types.t -> Types.t -> bool
diff --git a/src/utils/dimension.ml b/src/utils/dimension.ml
index ceed2413..2a65b415 100644
--- a/src/utils/dimension.ml
+++ b/src/utils/dimension.ml
@@ -86,14 +86,14 @@ let rec pp fmt dim =
| Dunivar ->
fprintf fmt "'%s" (Utils.name_of_dimension dim.dim_id)
-let rec multi_dimension_product loc dim_list =
+let rec multi_product loc dim_list =
match dim_list with
| [] ->
mkdim_int loc 1
| [ d ] ->
d
| d :: q ->
- mkdim_appl loc "*" [ d; multi_dimension_product loc q ]
+ mkdim_appl loc "*" [ d; multi_product loc q ]
(* Builds a dimension expr representing 0<=d *)
let check_bound loc d = mkdim_appl loc "<=" [ mkdim_int loc 0; d ]
@@ -136,7 +136,7 @@ let size_const dim =
| Dbool b ->
if b then 1 else 0
| _ ->
- Format.eprintf "internal error: size_const_dimension %a@." pp dim;
+ Format.eprintf "internal error: size_const %a@." pp dim;
assert false
let rec is_polymorphic dim =
diff --git a/src/utils/dimension.mli b/src/utils/dimension.mli
index e99526ad..45c9fda4 100644
--- a/src/utils/dimension.mli
+++ b/src/utils/dimension.mli
@@ -44,3 +44,8 @@ val expr_replace_expr: (ident -> t) -> t -> t
val rename: (ident -> ident) -> (ident -> ident) -> t -> t
val size_const: t -> int
+
+val check_bound: Location.t -> t -> t
+val check_access: Location.t -> t -> t -> t
+
+val multi_product: Location.t -> t list -> t
diff --git a/src/utils/location.ml b/src/utils/location.ml
index b3ed097c..4461b78c 100644
--- a/src/utils/location.ml
+++ b/src/utils/location.ml
@@ -54,7 +54,7 @@ let loc_line (s, _e) = s.pos_lnum
let pp fmt loc =
if loc = dummy then () else Format.fprintf fmt "%s" (Lex.range loc)
-let pp_c_loc fmt (s, _e) =
+let pp_c fmt (s, _e) =
let filename = s.pos_fname in
let line = s.pos_lnum in
Format.fprintf fmt "#line %i \"%s\"" line filename
diff --git a/src/utils/location.mli b/src/utils/location.mli
index c2857c00..e461dd88 100644
--- a/src/utils/location.mli
+++ b/src/utils/location.mli
@@ -3,6 +3,7 @@ type filename = string
val dummy: t
val pp: Format.formatter -> t -> unit
+val pp_c: Format.formatter -> t -> unit
val get_module: unit -> filename
val curr: Lexing.lexbuf -> t
val shift: t -> t -> t
diff --git a/src/utils/utils.ml b/src/utils/utils.ml
index 5713cb22..d87a776b 100644
--- a/src/utils/utils.ml
+++ b/src/utils/utils.ml
@@ -357,22 +357,22 @@ module Format = struct
let pp_comma_list = pp_print_list ~pp_sep:pp_print_comma
let pp_print_list_i ?pp_prologue ?pp_epilogue ?pp_op ?pp_cl ?pp_open_box
- ?pp_eol ?pp_sep pp_v =
+ ?pp_eol ?pp_nil ?pp_sep pp_v =
let i = ref 0 in
pp_print_list ?pp_prologue ?pp_epilogue ?pp_op ?pp_cl ?pp_open_box ?pp_eol
- ?pp_sep (fun fmt x ->
+ ?pp_nil ?pp_sep (fun fmt x ->
pp_v fmt !i x;
incr i)
let pp_print_list2 ?pp_prologue ?pp_epilogue ?pp_op ?pp_cl ?pp_open_box
- ?pp_eol ?pp_sep pp_v fmt (l1, l2) =
+ ?pp_eol ?pp_nil ?pp_sep pp_v fmt (l1, l2) =
pp_print_list ?pp_prologue ?pp_epilogue ?pp_op ?pp_cl ?pp_open_box ?pp_eol
- ?pp_sep pp_v fmt (List.combine l1 l2)
+ ?pp_nil ?pp_sep pp_v fmt (List.combine l1 l2)
let pp_print_list_i2 ?pp_prologue ?pp_epilogue ?pp_op ?pp_cl ?pp_open_box
- ?pp_eol ?pp_sep pp_v fmt (l1, l2) =
+ ?pp_eol ?pp_nil ?pp_sep pp_v fmt (l1, l2) =
pp_print_list_i ?pp_prologue ?pp_epilogue ?pp_op ?pp_cl ?pp_open_box ?pp_eol
- ?pp_sep
+ ?pp_nil ?pp_sep
(fun fmt i (x1, x2) -> pp_v fmt i x1 x2)
fmt (List.combine l1 l2)
diff --git a/src/utils/utils.mli b/src/utils/utils.mli
index d738d586..b7a8c729 100644
--- a/src/utils/utils.mli
+++ b/src/utils/utils.mli
@@ -4,6 +4,8 @@ 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
+ val diff: 'a t -> 'a t -> 'a t
+ val of_list: (key * 'a) list -> 'a t
end
module ISet: sig
@@ -13,10 +15,16 @@ end
module Format: sig
include module type of Format
+ val with_out_file: string -> (formatter -> unit) -> unit
+ val pp_print_comma: formatter -> unit -> unit
+ val pp_print_comma': formatter -> unit -> unit
val pp_print_semicolon: formatter -> unit -> unit
+ val pp_print_semicolon': formatter -> unit -> unit
+ val pp_print_cpar: 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_endcut: string -> formatter -> unit -> unit
val pp_print_list:
?pp_prologue:(formatter -> unit -> unit) ->
?pp_epilogue:(formatter -> unit -> unit) ->
@@ -27,6 +35,26 @@ module Format: sig
?pp_nil:(formatter -> unit -> unit) ->
?pp_sep:(formatter -> unit -> unit) ->
(formatter -> 'a -> unit) -> formatter -> 'a list -> unit
+ val pp_print_list_i:
+ ?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 -> int -> 'a -> unit) -> formatter -> 'a list -> unit
+ val pp_print_list_i2:
+ ?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 -> int -> 'a -> 'b -> unit) -> formatter -> 'a list * 'b list -> unit
val pp_comma_list:
?pp_prologue:(formatter -> unit -> unit) ->
?pp_epilogue:(formatter -> unit -> unit) ->
@@ -52,6 +80,22 @@ module Format: sig
?pp_eol:(formatter -> unit -> unit) ->
?pp_nil:(formatter -> unit -> unit) ->
(formatter -> 'a -> unit) -> formatter -> 'a list -> unit
+ val pp_print_braced:
+ ?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_braced':
+ ?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
@@ -59,6 +103,18 @@ module TopologicalDepGraph: sig
val fold : (ident -> 'a -> 'a) -> IdentDepGraph.t -> 'a -> 'a
val iter : (ident -> unit) -> IdentDepGraph.t -> unit
end
+module Bfs: sig
+ (* val iter : (ident -> unit) -> IdentDepGraph.t -> unit *)
+ val iter_component : (ident -> unit) -> IdentDepGraph.t -> ident -> unit
+
+ (* val fold : (G.V.t -> 'a -> 'a) -> 'a -> G.t -> 'a
+ * val fold_component : (G.V.t -> 'a -> 'a) -> 'a -> G.t -> G.V.t -> 'a
+ *
+ * type iterator
+ * val start : G.t -> iterator
+ * val step : iterator -> iterator
+ * val get : iterator -> G.V.t *)
+end
val name_of_dimension: tag -> ident
@@ -91,3 +147,7 @@ val repeat: int -> ('a -> 'a) -> 'a -> 'a
val add_cons: 'a -> 'a list -> 'a list
val enumerate: int -> int list
+
+val duplicate: 'a -> int -> 'a list
+
+val list_union: 'a list -> 'a list -> 'a list
diff --git a/src/verifierList.mli b/src/verifierList.mli
index e69de29b..483bc7b1 100644
--- a/src/verifierList.mli
+++ b/src/verifierList.mli
@@ -0,0 +1 @@
+val verifiers: unit -> (module VerifierType.S) list
--
GitLab