From 19a1e66bb915087d295401c237cfe1656df0b32e Mon Sep 17 00:00:00 2001
From: ploc <ploc@garoche.net>
Date: Tue, 20 Nov 2018 20:58:59 -0800
Subject: [PATCH] Added include directive that directly inject a lustre source
file in the prog
---
src/backends/Horn/horn_backend.ml | 2 +-
src/clock_calculus.ml | 4 +-
src/corelang.ml | 16 ++++----
src/lusic.ml | 2 +-
src/lustre_types.ml | 2 +
src/modules.ml | 61 ++++++++++++++++---------------
src/normalization.ml | 2 +-
src/options_management.ml | 4 +-
src/parsers/lexer_lustre.mll | 5 ++-
src/parsers/parser_lustre.mly | 18 +++++++--
src/plugins/mpfr/mpfr.ml | 2 +-
src/printers.ml | 3 ++
src/typing.ml | 6 +--
13 files changed, 72 insertions(+), 55 deletions(-)
diff --git a/src/backends/Horn/horn_backend.ml b/src/backends/Horn/horn_backend.ml
index e2501003..e4bbd814 100644
--- a/src/backends/Horn/horn_backend.ml
+++ b/src/backends/Horn/horn_backend.ml
@@ -85,7 +85,7 @@ let print_dep fmt prog =
List.iter
(fun dep ->
let (local, s) = Corelang.dependency_of_top dep in
- let basename = (Options_management.name_dependency (local, s)) ^ ".smt2" in
+ let basename = (Options_management.name_dependency (local, s) ".lusic") ^ ".smt2" in
Log.report ~level:1 (fun fmt -> Format.fprintf fmt "@[<v 0> Horn Library %s@," basename);
let horn = load_file basename in
fprintf fmt "@.%s@." (horn);
diff --git a/src/clock_calculus.ml b/src/clock_calculus.ml
index 78d01a03..cee07933 100644
--- a/src/clock_calculus.ml
+++ b/src/clock_calculus.ml
@@ -754,7 +754,7 @@ let rec clock_top_decl env decl =
| Const c ->
clock_top_const env c
| TypeDef _ -> List.fold_left clock_top_decl env (consts_of_enum_type decl)
- | Open _ -> env
+ | Include _ | Open _ -> env
let clock_prog env decls =
List.fold_left clock_top_decl env decls
@@ -786,7 +786,7 @@ let uneval_top_generics decl =
| ImportedNode nd ->
uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)
| Const _
- | Open _
+ | Include _ | Open _
| TypeDef _ -> ()
let uneval_prog_generics prog =
diff --git a/src/corelang.ml b/src/corelang.ml
index 65a222b2..c7c60511 100644
--- a/src/corelang.ml
+++ b/src/corelang.ml
@@ -642,7 +642,7 @@ let get_nodes prog =
fun nodes decl ->
match decl.top_decl_desc with
| Node _ -> decl::nodes
- | Const _ | ImportedNode _ | Open _ | TypeDef _ -> nodes
+ | Const _ | ImportedNode _ | Include _ | Open _ | TypeDef _ -> nodes
) [] prog
let get_imported_nodes prog =
@@ -650,7 +650,7 @@ let get_imported_nodes prog =
fun nodes decl ->
match decl.top_decl_desc with
| ImportedNode _ -> decl::nodes
- | Const _ | Node _ | Open _ | TypeDef _-> nodes
+ | Const _ | Node _ | Include _ | Open _ | TypeDef _-> nodes
) [] prog
let get_consts prog =
@@ -658,7 +658,7 @@ let get_consts prog =
fun decl consts ->
match decl.top_decl_desc with
| Const _ -> decl::consts
- | Node _ | ImportedNode _ | Open _ | TypeDef _ -> consts
+ | Node _ | ImportedNode _ | Include _ | Open _ | TypeDef _ -> consts
) prog []
let get_typedefs prog =
@@ -666,7 +666,7 @@ let get_typedefs prog =
fun decl types ->
match decl.top_decl_desc with
| TypeDef _ -> decl::types
- | Node _ | ImportedNode _ | Open _ | Const _ -> types
+ | Node _ | ImportedNode _ | Include _ | Open _ | Const _ -> types
) prog []
let get_dependencies prog =
@@ -674,7 +674,7 @@ let get_dependencies prog =
fun decl deps ->
match decl.top_decl_desc with
| Open _ -> decl::deps
- | Node _ | ImportedNode _ | TypeDef _ | Const _ -> deps
+ | Node _ | ImportedNode _ | TypeDef _ | Include _ | Const _ -> deps
) prog []
let get_node_interface nd =
@@ -878,7 +878,7 @@ let rename_prog f_node f_var f_const prog =
| TypeDef tdef ->
{ top with top_decl_desc = TypeDef (rename_typedef f_var tdef) }
| ImportedNode _
- | Open _ -> top)
+ | Include _ | Open _ -> top)
::accu
) [] prog
)
@@ -934,7 +934,7 @@ let pp_decl_type fmt tdecl =
fprintf fmt "%s: " ind.nodei_id;
Utils.reset_names ();
fprintf fmt "%a@ " Types.print_ty ind.nodei_type
- | Const _ | Open _ | TypeDef _ -> ()
+ | Const _ | Include _ | Open _ | TypeDef _ -> ()
let pp_prog_type fmt tdecl_list =
Utils.fprintf_list ~sep:"" pp_decl_type fmt tdecl_list
@@ -949,7 +949,7 @@ let pp_decl_clock fmt cdecl =
fprintf fmt "%s: " ind.nodei_id;
Utils.reset_names ();
fprintf fmt "%a@ " Clocks.print_ck ind.nodei_clock
- | Const _ | Open _ | TypeDef _ -> ()
+ | Const _ | Include _ | Open _ | TypeDef _ -> ()
let pp_prog_clock fmt prog =
Utils.fprintf_list ~sep:"" pp_decl_clock fmt prog
diff --git a/src/lusic.ml b/src/lusic.ml
index 52d6acd3..46a7434d 100644
--- a/src/lusic.ml
+++ b/src/lusic.ml
@@ -40,7 +40,7 @@ let extract_header dirname basename prog =
| ImportedNode _ -> header
| Const _
| TypeDef _
- | Open _ -> decl :: header)
+ | Include _ | Open _ -> decl :: header)
prog []
let check_obsolete lusic basename =
diff --git a/src/lustre_types.ml b/src/lustre_types.ml
index bbd0292a..d3bc43dc 100644
--- a/src/lustre_types.ml
+++ b/src/lustre_types.ml
@@ -218,6 +218,8 @@ type top_decl_desc =
| ImportedNode of imported_node_desc
| Open of bool * string (* the boolean set to true denotes a local
lusi vs a lusi installed at system level *)
+| Include of string (* the boolean set to true denotes a local
+ lus vs a lus installed at system level *)
| TypeDef of typedef_desc
type top_decl =
diff --git a/src/modules.ml b/src/modules.ml
index a97179d4..80cedad9 100644
--- a/src/modules.ml
+++ b/src/modules.ml
@@ -114,34 +114,34 @@ let add_const itf name value =
| _ -> assert false
with Not_found -> Hashtbl.add consts_table name value
-let import_dependency_aux loc (local, dep) =
- let basename = Options_management.name_dependency (local, dep) in
- let extension = ".lusic" in
- try
- let lusic = Lusic.read_lusic basename extension in
- Lusic.check_obsolete lusic basename;
- lusic
- with
- | Sys_error msg ->
- raise (Error (loc, Error.Unknown_library basename))
-
-let import_dependency loc (local, dep) =
- try
- import_dependency_aux loc (local, dep)
- with
- | Corelang.Error (_, err) as exc -> (
- Format.eprintf "Import error: %a%a@."
- Error.pp_error_msg err
- Location.pp_loc loc;
- raise exc
- )
+(* let import_dependency_aux loc (local, dep) =
+ * let basename = Options_management.name_dependency (local, dep) in
+ * let extension = ".lusic" in
+ * try
+ * let lusic = Lusic.read_lusic basename extension in
+ * Lusic.check_obsolete lusic basename;
+ * lusic
+ * with
+ * | Sys_error msg ->
+ * raise (Error (loc, Error.Unknown_library basename))
+ *
+ * let import_dependency loc (local, dep) =
+ * try
+ * import_dependency_aux loc (local, dep)
+ * with
+ * | Corelang.Error (_, err) as exc -> (
+ * Format.eprintf "Import error: %a%a@."
+ * Error.pp_error_msg err
+ * Location.pp_loc loc;
+ * raise exc
+ * ) *)
let get_lusic decl =
match decl.top_decl_desc with
| Open (local, dep) -> (
let loc = decl.top_decl_loc in
- let basename = Options_management.name_dependency (local, dep) in
let extension = ".lusic" in
+ let basename = Options_management.name_dependency (local, dep) extension in
try
let lusic = Lusic.read_lusic basename extension in
Lusic.check_obsolete lusic basename;
@@ -168,7 +168,7 @@ let rec get_envs_from_top_decl (ty_env, ck_env) top_decl =
Env.add_value ck_env ind.nodei_id ind.nodei_clock)
| Const c -> get_envs_from_const c (ty_env, ck_env)
| TypeDef _ -> List.fold_left get_envs_from_top_decl (ty_env, ck_env) (consts_of_enum_type top_decl)
- | Open _ -> (ty_env, ck_env)
+ | Include _ | Open _ -> (ty_env, ck_env)
(* get type and clock environments from a header *)
let get_envs_from_top_decls header =
@@ -187,15 +187,15 @@ let rec load_rec ~is_header accu program =
match decl.top_decl_desc with
| Open (local, dep) ->
(* loading the dep *)
- let basename = Options_management.name_dependency (local, dep) in
+ let basename = Options_management.name_dependency (local, dep) ".lusic" in
if List.exists
- (fun dep -> basename = Options_management.name_dependency (dep.local, dep.name))
+ (fun dep -> basename = Options_management.name_dependency (dep.local, dep.name) ".lusic")
accu_dep
then
(* Library already imported. Just skip *)
accu
else (
- Log.report ~level:1 (fun fmt -> Format.fprintf fmt "@ Library %s@ " basename);
+ Log.report ~level:1 (fun fmt -> Format.fprintf fmt "@ .. Library %s@ " basename);
let lusic = get_lusic decl in
(* Recursive call with accumulator on lusic *)
let (accu_prog, accu_dep, typ_env, clk_env) =
@@ -211,10 +211,11 @@ let rec load_rec ~is_header accu program =
one and the updated envs *)
accu_prog, (new_dep::accu_dep), typ_env, clk_env
)
- (* | Include xxx -> TODO
- load the lus file
- call load_rec ~is_header:false accu on the luscontent
- *)
+ | Include name ->
+ let basename = Options_management.name_dependency (true, name) "" in
+ let include_src = Compiler_common.parse_source basename in
+ load_rec ~is_header:false accu include_src
+
| Node nd ->
if is_header then
diff --git a/src/normalization.ml b/src/normalization.ml
index 13ae553f..c1c5bc46 100644
--- a/src/normalization.ml
+++ b/src/normalization.ml
@@ -630,7 +630,7 @@ let normalize_decl (decls: program_t) (decl: top_decl) : top_decl =
let decl' = {decl with top_decl_desc = Node (normalize_node decls nd)} in
Hashtbl.replace Corelang.node_table nd.node_id decl';
decl'
- | Open _ | ImportedNode _ | Const _ | TypeDef _ -> decl
+ | Include _| Open _ | ImportedNode _ | Const _ | TypeDef _ -> decl
let normalize_prog p decls =
(* Backend specific configurations for normalization *)
diff --git a/src/options_management.ml b/src/options_management.ml
index a4f568bd..9be60388 100644
--- a/src/options_management.ml
+++ b/src/options_management.ml
@@ -58,8 +58,8 @@ let search_lib_path (local, full_file_name) =
let core_dependency lib_name =
search_lib_path (false, lib_name ^ ".h")
-let name_dependency (local, dep) =
- let dir = search_lib_path (false, dep ^ ".lusic") in
+let name_dependency (local, dep) ext =
+ let dir = search_lib_path (false, dep ^ ext) in
dir ^ "/" ^ dep
let set_mpfr prec =
diff --git a/src/parsers/lexer_lustre.mll b/src/parsers/lexer_lustre.mll
index d0fc9823..f9727e9c 100644
--- a/src/parsers/lexer_lustre.mll
+++ b/src/parsers/lexer_lustre.mll
@@ -126,6 +126,7 @@ rule token = parse
| "tel." {TEL}
| "tel;" {TEL}
| "#open" { OPEN }
+| "include" { INCLUDE }
| ['_' 'a'-'z'] [ '_' 'a'-'z' 'A'-'Z' '0'-'9']*
{let s = Lexing.lexeme lexbuf in
try
@@ -137,7 +138,7 @@ rule token = parse
try
Hashtbl.find keyword_table s
with Not_found ->
- UIDENT s}
+ UIDENT s}
| "->" {ARROW}
| "=>" {IMPL}
| "<=" {LTE}
@@ -161,12 +162,12 @@ rule token = parse
| ':' {COL}
| ',' {COMMA}
| '=' {EQ}
-| '/' {DIV}
| "&&" {AMPERAMPER}
| "||" {BARBAR}
| "::" {COLCOL}
| "^" {POWER}
| '"' {QUOTE}
+| '.' {POINT}
| eof { EOF }
| _ { raise (Parse.Error (Location.curr lexbuf, Parse.Undefined_token (Lexing.lexeme lexbuf))) }
diff --git a/src/parsers/parser_lustre.mly b/src/parsers/parser_lustre.mly
index 58e15554..b6597cd6 100644
--- a/src/parsers/parser_lustre.mly
+++ b/src/parsers/parser_lustre.mly
@@ -57,7 +57,7 @@ let rec fby expr n init =
%token <string> STRING
%token AUTOMATON STATE UNTIL UNLESS RESTART RESUME
-%token ASSERT OPEN QUOTE FUNCTION
+%token ASSERT OPEN INCLUDE QUOTE POINT FUNCTION
%token <string> IDENT
%token <string> UIDENT
%token TRUE FALSE
@@ -128,10 +128,21 @@ let rec fby expr n init =
%type <Lustre_types.var_decl list> vdecl_list
%%
+
module_ident:
UIDENT { $1 }
| IDENT { $1 }
+file_ident:
+module_ident { $1 }
+| module_ident POINT file_ident { $1 ^ "." ^ $3 }
+
+path_ident:
+POINT DIV path_ident { "./" ^ $3 }
+| file_ident DIV path_ident { $1 ^ "/" ^ $3 }
+| DIV path_ident { "/" ^ $2 }
+| file_ident { $1 }
+
tag_ident:
UIDENT { $1 }
| TRUE { tag_true }
@@ -172,8 +183,9 @@ open_list:
| open_lusi open_list { $1 :: $2 }
open_lusi:
-| OPEN QUOTE module_ident QUOTE { mktop_decl false (Open (true, $3))}
-| OPEN LT module_ident GT { mktop_decl false (Open (false, $3)) }
+ | OPEN QUOTE path_ident QUOTE { mktop_decl false (Open (true, $3)) }
+ | INCLUDE QUOTE path_ident QUOTE { mktop_decl false (Include ($3)) }
+ | OPEN LT path_ident GT { mktop_decl false (Open (false, $3)) }
top_decl_list:
{[]}
diff --git a/src/plugins/mpfr/mpfr.ml b/src/plugins/mpfr/mpfr.ml
index 3dacceeb..927c6b9a 100644
--- a/src/plugins/mpfr/mpfr.ml
+++ b/src/plugins/mpfr/mpfr.ml
@@ -315,7 +315,7 @@ let inject_decl decl =
match decl.top_decl_desc with
| Node nd ->
{decl with top_decl_desc = Node (inject_node nd)}
- | Open _ | ImportedNode _ | Const _ | TypeDef _ -> decl
+ | Include _ | Open _ | ImportedNode _ | Const _ | TypeDef _ -> decl
let inject_prog decls =
List.map inject_decl decls
diff --git a/src/printers.ml b/src/printers.ml
index 71a82430..1934c9db 100644
--- a/src/printers.ml
+++ b/src/printers.ml
@@ -382,6 +382,7 @@ let pp_decl fmt decl =
fprintf fmt "imported %a;" pp_imported_node ind
| Const c -> fprintf fmt "const %a" pp_const_decl c
| Open (local, s) -> if local then fprintf fmt "#open \"%s\"" s else fprintf fmt "#open <%s>" s
+ | Include s -> fprintf fmt "include \"%s\"" s
| TypeDef tdef -> fprintf fmt "%a" pp_typedef tdef
let pp_prog fmt prog =
@@ -402,6 +403,7 @@ let pp_short_decl fmt decl =
| Node nd -> fprintf fmt "node %s@ " nd.node_id
| ImportedNode ind -> fprintf fmt "imported node %s" ind.nodei_id
| Const c -> fprintf fmt "const %a@ " pp_const_decl c
+ | Include s -> fprintf fmt "include \"%s\"" s
| Open (local, s) -> if local then fprintf fmt "#open \"%s\"@ " s else fprintf fmt "#open <%s>@ " s
| TypeDef tdef -> fprintf fmt "type %s;@ " tdef.tydef_id
@@ -409,6 +411,7 @@ let pp_lusi fmt decl =
match decl.top_decl_desc with
| ImportedNode ind -> fprintf fmt "%a;@ " pp_imported_node ind
| Const c -> fprintf fmt "const %a@ " pp_const_decl c
+ | Include s -> fprintf fmt "include \"%s\"" s
| Open (local, s) -> if local then fprintf fmt "#open \"%s\"@ " s else fprintf fmt "#open <%s>@ " s
| TypeDef tdef -> fprintf fmt "%a@ " pp_typedef tdef
| Node _ -> assert false
diff --git a/src/typing.ml b/src/typing.ml
index 5688eb51..c75ce0ba 100644
--- a/src/typing.ml
+++ b/src/typing.ml
@@ -766,7 +766,7 @@ module Make (T: Types.S) (Expr_type_hub: EXPR_TYPE_HUB with type type_expr = T.t
| Const c ->
type_top_const env c
| TypeDef _ -> List.fold_left type_top_decl env (consts_of_enum_type decl)
- | Open _ -> env
+ | Include _ | Open _ -> env
let get_type_of_call decl =
match decl.top_decl_desc with
@@ -811,9 +811,7 @@ module Make (T: Types.S) (Expr_type_hub: EXPR_TYPE_HUB with type type_expr = T.t
uneval_node_generics (nd.node_inputs @ nd.node_outputs)
| ImportedNode nd ->
uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)
- | Const _
- | TypeDef _
- | Open _
+ | Const _ | TypeDef _ | Open _ | Include _
-> ()
let uneval_prog_generics prog =
--
GitLab