From 3e9d5fa10b37f9b3c355d32c65f506ef39e27e08 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?L=C3=A9lio=20Brun?= <lelio.brun@isae-supaero.fr>
Date: Thu, 12 May 2022 13:04:46 +0200
Subject: [PATCH] fix dune build
---
src/dune | 265 ++++++++----------
src/plugins/pluginType.ml | 4 +-
src/plugins/pluginType.mli | 4 +-
src/plugins/salsa/dune | 2 +-
src/plugins/scopes/dune | 2 +-
.../json-parser/main_parse_json_file.ml | 60 ++--
6 files changed, 158 insertions(+), 179 deletions(-)
diff --git a/src/dune b/src/dune
index 39d94634..5d1d188b 100644
--- a/src/dune
+++ b/src/dune
@@ -5,192 +5,167 @@
(include_subdirs unqualified)
+; use of the "sites" features of dune
+
+(generate_sites_module
+ (module sites)
+ (plugins
+ (lustrec plugins)
+ (lustrec verifiers)))
+
+; a common library for various executables and plugins
+
(library
- (name lustrec_core)
+ (name lustrec_common)
(package lustrec)
- (modules_without_implementation scheduling_type machine_code_types)
+ (wrapped false)
(modules
- lustre_types
utils
location
- dimension
env
+ dimension
real
- types
options
+ types
clocks
delay
- log
- corelang
- machine_code_types
+ lustre_types
spec_types
scheduling_type
- printers
- basic_library
- version
+ machine_code_types
type_predef
annotations
+ corelang
clock_predef
error
global
- compiler_common
- parse
+ basic_library
+ sites
+ sites_paths
+ backends
+ options_management
+ arrow
+ log
+ stateless
+ typing
+ machine_code_common
+ printers
+ version
+ ocaml_utils
+ lustrec_mpfr
+ machine_types
+ c_backend_common
+ automata
parser_lustre
parser_lustre_table
parser_lustre_messages
- lexer_lustre
+ parse
lexerLustreSpec
- automata
- stateless
- typing
+ lexer_lustre
clock_calculus
- backends
- normalization
- machine_types
- splitting)
- (wrapped false)
- (libraries ocamlgraph menhirLib zarith unix))
+ compiler_common
+ splitting
+ normalization)
+ (modules_without_implementation machine_code_types scheduling_type)
+ (libraries ocamlgraph menhirLib zarith dune-site dune-site.plugins str unix))
-(library
- (name lustrec_interface)
- (package lustrec)
- (modules
- lustre_utils
- spec_common
- lustre_live
- delay_predef
- machine_code_common
- arrow
- sites_paths
- options_management
- c_backend_common
- ocaml_utils
- lustrec_mpfr
- arrow_taint)
- (wrapped false)
- (libraries lustrec_core sites str))
+; a library for plugin registration
(library
(name plugin_register)
(package lustrec)
(wrapped false)
(modules pluginList pluginType)
- (libraries lustrec_interface))
-
-(generate_sites_module
- (module sites)
- (plugins
- (lustrec plugins)
- (lustrec verifiers)))
+ (libraries lustrec_common))
-(library
- (name sites)
- (package lustrec)
- (modules sites)
- (libraries dune-site dune-site.plugins))
-
-(library
- (name lustrec_lib)
- (package lustrec)
- (modules
- lusic
- c_backend_header
- c_backend_spec
- c_backend_makefile
- c_backend_mauve
- c_backend_src
- ada_backend
- ada_printer
- ada_backend_common
- ada_backend_ads
- ada_backend_adb
- ada_backend_wrapper
- horn_backend
- horn_backend_common
- horn_backend_printers
- Horn_backend_collecting_sem
- horn_backend_traces
- EMF_backend
- EMF_common
- EMF_library_calls
- misc_lustre_function
- misc_printer
- machine_code
- machine_code_dep
- causality
- scheduling
- liveness
- compiler_stages
- modules
- sortProg
- inliner
- access
- algebraicLoop
- optimize_prog
- optimize_machine
- spec
- c_backend
- c_backend_main
- plugins)
- (wrapped false)
- (libraries lustrec_interface plugin_register))
-
-(executable
- (name main_lustre_compiler)
- (public_name lustrec)
- (modules main_lustre_compiler)
- (package lustrec)
- (libraries lustrec_lib lustrec.scopes))
-
-(executable
- (name main_lustre_testgen)
- (public_name lustret)
- (modules main_lustre_testgen mutation pathConditions)
- (libraries lustrec_core lustrec_lib))
+; a library for verifier registration
(library
(name verifier_register)
(package lustrec)
(wrapped false)
(modules verifierList verifierType)
- (libraries lustrec_interface))
+ (libraries lustrec_common))
-(executable
- (name main_lustre_verifier)
- (public_name lustrev)
- (modules main_lustre_verifier verifiers)
- (libraries lustrec_lib verifier_register lustrec.scopes))
+; executables
-(executable
- (name main_lustre_importer)
- (public_name lustrei)
- (modules main_lustre_importer vhdl_deriving_yojson vhdl_json_lib)
- (libraries yojson ppx_deriving_yojson.runtime)
+(executables
+ (package lustrec)
+ (names
+ main_lustre_compiler
+ main_lustre_verifier
+ main_lustre_testgen
+ main_lustre_importer
+ sf_sem)
+ (public_names lustrec lustrev lustret lustrei lustresf)
+ (modules
+ (:standard
+ \
+ pluginType
+ pluginList
+ verifierType
+ verifierList
+ lustre_types
+ utils
+ location
+ dimension
+ env
+ real
+ types
+ options
+ clocks
+ delay
+ machine_code_types
+ spec_types
+ scheduling_type
+ corelang
+ machine_code_common
+ printers
+ type_predef
+ basic_library
+ c_backend_common
+ version
+ clock_predef
+ annotations
+ arrow
+ compiler_common
+ options_management
+ ocaml_utils
+ error
+ stateless
+ lustrec_mpfr
+ global
+ log
+ typing
+ machine_types
+ parse
+ normalization
+ splitting
+ parser_lustre
+ parser_lustre_table
+ automata
+ parser_lustre_messages
+ lexer_lustre
+ lexerLustreSpec
+ clock_calculus
+ sites_paths
+ sites
+ backends))
+ (libraries
+ plugin_register
+ verifier_register
+ lustrec.scopes
+ yojson
+ ppx_deriving_yojson.runtime)
(preprocess
(pps ppx_deriving_yojson)))
-(library
- (name tools_lib)
- (package lustrec)
- (wrapped false)
- (modules basetypes datatype activeStates)
- (libraries lustrec_lib))
-
-(executable
- (name sf_sem)
- (public_name lustresf)
- (modules
- sf_sem
- model_simple
- model_stopwatch
- CPS_ccode_generator
- CPS_transformer
- CPS_interpreter
- CPS_lustre_generator
- CPS
- theta
- memo)
- (libraries tools_lib))
+; (library
+; (name tools_lib)
+; (package lustrec)
+; (wrapped false)
+; (modules basetypes datatype activeStates)
+; (libraries lustrec_lib))
; (executable
; (name main_parse_json_file)
diff --git a/src/plugins/pluginType.ml b/src/plugins/pluginType.ml
index c9a083ec..5b3557b6 100644
--- a/src/plugins/pluginType.ml
+++ b/src/plugins/pluginType.ml
@@ -1,8 +1,10 @@
+type options_spec = (string * Arg.spec * string) list
+
module type S = sig
val name : string
val activate : unit -> unit
val usage : Format.formatter -> unit
- val options : Options_management.options_spec
+ val options : options_spec
val init : unit -> unit
val check_force_stateful : unit -> bool
diff --git a/src/plugins/pluginType.mli b/src/plugins/pluginType.mli
index 8ec31572..891d32ff 100644
--- a/src/plugins/pluginType.mli
+++ b/src/plugins/pluginType.mli
@@ -1,8 +1,10 @@
+type options_spec = (string * Arg.spec * string) list
+
module type S = sig
val name : string
val activate : unit -> unit
val usage : Format.formatter -> unit
- val options : Options_management.options_spec
+ val options : options_spec
val init : unit -> unit
val check_force_stateful : unit -> bool
diff --git a/src/plugins/salsa/dune b/src/plugins/salsa/dune
index cdec3fbf..247ec7f6 100644
--- a/src/plugins/salsa/dune
+++ b/src/plugins/salsa/dune
@@ -3,7 +3,7 @@
(library
(name salsa_plugin)
(public_name lustrec.salsa_plugin)
- (libraries lustrec_interface plugin_register salsa)
+ (libraries lustrec_common plugin_register salsa)
(optional))
(plugin
diff --git a/src/plugins/scopes/dune b/src/plugins/scopes/dune
index aaed4e67..efa809a0 100644
--- a/src/plugins/scopes/dune
+++ b/src/plugins/scopes/dune
@@ -3,7 +3,7 @@
(library
(name scopes)
(public_name lustrec.scopes)
- (libraries lustrec_interface plugin_register))
+ (libraries lustrec_common plugin_register))
(plugin
(name scopes_plugin)
diff --git a/src/tools/stateflow/json-parser/main_parse_json_file.ml b/src/tools/stateflow/json-parser/main_parse_json_file.ml
index 1af3c9ae..49f16b31 100644
--- a/src/tools/stateflow/json-parser/main_parse_json_file.ml
+++ b/src/tools/stateflow/json-parser/main_parse_json_file.ml
@@ -39,43 +39,44 @@ module ParseExt = struct
let protect funname default parse_fun embed_fun json =
(* Logs.debug (fun m -> m "protect %s" (Y.to_string json)); *)
try
- (* TODO: project the declared env onto the variables used in the actions or conditions
- let vars = get_vars json in *)
+ (* TODO: project the declared env onto the variables used in the actions
+ or conditions let vars = get_vars json in *)
let vars = [], [], [] in
let actions = json |> (*Util.member "actions" |> *) to_string in
let actions = remove_quotes actions in
- if actions = "[]" || actions = "" then default (* should not happen *) else (
- Format.eprintf "Parsing string: %s@." actions;
- let lexbuf = Lexing.from_string actions in
- try
- let content = parse_fun Lexer_lustre.token lexbuf in
- Parsing.clear_parser ();
- embed_fun content vars
- with Parsing.Parse_error ->
- let loc = Location.dummy_loc in
- raise (Parse.Error (loc, Parse.String_Syntax_error actions))
- )
- with Util.Type_error _ -> (
+ if actions = "[]" || actions = "" then default (* should not happen *)
+ else (
+ Format.eprintf "Parsing string: %s@." actions;
+ let lexbuf = Lexing.from_string actions in
+ try
+ let content = parse_fun Lexer_lustre.token lexbuf in
+ Parsing.clear_parser ();
+ embed_fun content vars
+ with Parsing.Parse_error ->
+ let loc = Location.dummy_loc in
+ raise (Parse.Error (loc, Parse.String_Syntax_error actions)))
+ with Util.Type_error _ ->
Format.eprintf
- "Unable to explore json subtree in %s: empty string %s@." funname (Yojson.Basic.to_string json);
+ "Unable to explore json subtree in %s: empty string %s@."
+ funname
+ (Yojson.Basic.to_string json);
default
let parse_condition =
- protect "condition"
+ protect
+ "condition"
Condition.tru
Parser_lustre.expr
- (fun e (in_,out_,locals_) ->
- (* let vars = Corelang.get_expr_vars e in *)
- Condition.cquote {
- expr = e;
- cinputs = in_;
- coutputs = out_;
- cvariables = locals_;
-
- })
-
+ (fun e (in_, out_, locals_) ->
+ (* let vars = Corelang.get_expr_vars e in *)
+ Condition.cquote
+ { expr = e; cinputs = in_; coutputs = out_; cvariables = locals_ })
+
let parse_action =
- protect "action" Action.nil Parser_lustre.stmt_list
+ protect
+ "action"
+ Action.nil
+ Parser_lustre.stmt_list
(fun (stmts, asserts, annots) (in_, out_, locals_) ->
if asserts != [] || annots != [] then assert false
(* Stateflow equations should not use asserts nor define
@@ -111,7 +112,6 @@ let json_parse _ file pp =
let module Model = struct
let model = prog
-
let name = "toto"
(* TODO find a meaningful name *)
@@ -132,7 +132,6 @@ let json_parse _ file pp =
let module T = CPS_lustre_generator.LustrePrinter (struct
let state_vars = state_vars
-
let global_vars = global_vars
end) in
let module Sem = CPS.Semantics (T) (Model) in
@@ -155,7 +154,8 @@ let json_parse _ file pp =
let auto_out = open_out auto_file in
let auto_fmt = Format.formatter_of_out_channel auto_out in
Format.fprintf auto_fmt "%a@." Printers.pp_prog prog;
- Format.eprintf "Print initial lustre model with automaton in sf_gen_test_auto.lus@.";
+ Format.eprintf
+ "Print initial lustre model with automaton in sf_gen_test_auto.lus@.";
let params = Backends.get_normalization_params () in
let prog, deps = Compiler_stages.stage1 params prog "" "" "lus" in
--
GitLab