diff --git a/src/annotations.ml b/src/annotations.ml
new file mode 100644
index 0000000000000000000000000000000000000000..ef7ca11e1fea3640de7dd2322d4e552aa366e72a
--- /dev/null
+++ b/src/annotations.ml
@@ -0,0 +1,22 @@
+(********************************************************************)
+(* *)
+(* The LustreC compiler toolset / The LustreC Development Team *)
+(* Copyright 2012 - -- ONERA - CNRS - INPT *)
+(* *)
+(* LustreC is free software, distributed WITHOUT ANY WARRANTY *)
+(* under the terms of the GNU Lesser General Public License *)
+(* version 2.1. *)
+(* *)
+(********************************************************************)
+
+open LustreSpec
+
+
+(* Associate to each annotation key the pair (node, expr tag) *)
+let expr_annotations : (string list, ident * tag) Hashtbl.t= Hashtbl.create 13
+let node_annotations : (string list, ident) Hashtbl.t= Hashtbl.create 13
+
+let add_expr_ann node_id expr_tag key = Hashtbl.add expr_annotations key (node_id, expr_tag)
+let add_node_ann node_id key = Hashtbl.add node_annotations key node_id
+
+let get_expr_annotations key = Hashtbl.find_all expr_annotations key
diff --git a/src/corelang.ml b/src/corelang.ml
index 603873d491dd324870e86da2b3ce7f0f11ffb427..799f09a227bb3e8bda2d5e0bb8082a80e2e48192 100755
--- a/src/corelang.ml
+++ b/src/corelang.ml
@@ -167,7 +167,10 @@ let merge_expr_annot ann1 ann2 =
annot_loc = ann1.annot_loc
}
-let update_expr_annot e annot =
+let update_expr_annot node_id e annot =
+ List.iter (fun (key, _) ->
+ Annotations.add_expr_ann node_id e.expr_tag key
+ ) annot.annots;
{ e with expr_annot = merge_expr_annot e.expr_annot (Some annot) }
diff --git a/src/corelang.mli b/src/corelang.mli
index 4215eb70b45a61538937f16bf0f8ff98ef94fe4b..ef7603e78b515a83c98e8c71a027f9a5e7064ad5 100755
--- a/src/corelang.mli
+++ b/src/corelang.mli
@@ -116,7 +116,6 @@ val eq_replace_rhs_var: (ident -> bool) -> (ident -> ident) -> eq -> eq
(** rename_prog f_node f_var f_const prog *)
val rename_prog: (ident -> ident) -> (ident -> ident) -> (ident -> ident) -> program -> program
-val update_expr_annot: expr -> LustreSpec.expr_annot -> expr
val substitute_expr: var_decl list -> eq list -> expr -> expr
@@ -124,7 +123,7 @@ val substitute_expr: var_decl list -> eq list -> expr -> expr
val mkeexpr: Location.t -> expr -> eexpr
val merge_node_annot: node_annot -> node_annot -> node_annot
val extend_eexpr: (quantifier_type * var_decl list) list -> eexpr -> eexpr
-val update_expr_annot: expr -> expr_annot -> expr
+val update_expr_annot: ident -> expr -> LustreSpec.expr_annot -> expr
(* val mkpredef_call: Location.t -> ident -> eexpr list -> eexpr*)
(* Local Variables: *)
diff --git a/src/inliner.ml b/src/inliner.ml
index f948549ead30a9fdbe7ed5cd43ff843b342b55d0..0756ee85ac9358f5a84039be706a2509abed124b 100644
--- a/src/inliner.ml
+++ b/src/inliner.ml
@@ -11,6 +11,16 @@
open LustreSpec
open Corelang
+open Utils
+
+(* Local annotations are declared with the following key /inlining/: true *)
+let keyword = ["inlining"]
+
+let is_inline_expr expr =
+match expr.expr_annot with
+| Some ann ->
+ List.exists (fun (key, value) -> key = keyword) ann.annots
+| None -> false
let check_node_name id = (fun t ->
match t.top_decl_desc with
@@ -90,7 +100,9 @@ let inline_call orig_expr args reset locals node =
variables and the code of called node instance added to new_eqs
*)
-let rec inline_expr expr locals nodes =
+let rec inline_expr ?(selection_on_annotation=false) expr locals nodes =
+ let inline_expr = inline_expr ~selection_on_annotation:selection_on_annotation in
+ let inline_node = inline_node ~selection_on_annotation:selection_on_annotation in
let inline_tuple el =
List.fold_right (fun e (el_tail, locals, eqs, asserts) ->
let e', locals', eqs', asserts' = inline_expr e locals nodes in
@@ -109,13 +121,17 @@ let rec inline_expr expr locals nodes =
| [e1'; e2'; e3'] -> e1', e2', e3', l', eqs', asserts'
| _ -> assert false
in
-
+
match expr.expr_desc with
| Expr_appl (id, args, reset) ->
let args', locals', eqs', asserts' = inline_expr args locals nodes in
- if List.exists (check_node_name id) nodes then
+ if List.exists (check_node_name id) nodes && (* the current node call is provided
+ as arguments nodes *)
+ (not selection_on_annotation || is_inline_expr expr) (* and if selection on annotation is activated,
+ it is explicitely inlined here *)
+ then
(* The node should be inlined *)
- (* let _ = Format.eprintf "Inlining call to %s@." id in *)
+ let _ = Format.eprintf "Inlining call to %s@." id in
let node = try List.find (check_node_name id) nodes
with Not_found -> (assert false) in
let node = node_of_top node in
@@ -164,7 +180,8 @@ let rec inline_expr expr locals nodes =
let el, l', eqs', asserts' = inline_tuple (List.map snd branches) in
let branches' = List.map2 (fun (label, _) v -> label, v) branches el in
{ expr with expr_desc = Expr_merge (id, branches') }, l', eqs', asserts'
-and inline_node nd nodes =
+and inline_node ?(selection_on_annotation=false) nd nodes =
+ let inline_expr = inline_expr ~selection_on_annotation:selection_on_annotation in
let new_locals, eqs, asserts =
List.fold_left (fun (locals, eqs, asserts) eq ->
let eq_rhs', locals', new_eqs', asserts' =
@@ -319,6 +336,23 @@ let global_inline basename prog type_env clock_env =
);
res
+let local_inline basename prog type_env clock_env =
+ let local_anns = Annotations.get_expr_annotations keyword in
+ if local_anns != [] then (
+ let nodes_with_anns = List.fold_left (fun accu (k, _) -> ISet.add k accu) ISet.empty local_anns in
+ ISet.iter (fun node_id -> Format.eprintf "Node %s has local expression annotations@." node_id) nodes_with_anns;
+ List.fold_right (fun top accu ->
+ ( match top.top_decl_desc with
+ | Node nd when ISet.mem nd.node_id nodes_with_anns ->
+ { top with top_decl_desc = Node (inline_node ~selection_on_annotation:true nd prog) }
+ | _ -> top
+ )::accu) prog []
+
+)
+ else
+ prog
+
+
(* Local Variables: *)
(* compile-command:"make -C .." *)
(* End: *)
diff --git a/src/main_lustre_compiler.ml b/src/main_lustre_compiler.ml
index 72416348418445bafbc58202e010dd58f92dca57..6332d662f959dc9724681e635242857c5d15cc9f 100644
--- a/src/main_lustre_compiler.ml
+++ b/src/main_lustre_compiler.ml
@@ -127,12 +127,12 @@ let rec compile_source dirname basename extension =
if !Options.global_inline &&
(match !Options.main_node with | "" -> false | _ -> true) then
Inliner.global_inline basename prog type_env clock_env
- else
- prog
+ else (* if !Option.has_local_inline *)
+ Inliner.local_inline basename prog type_env clock_env
in
(* Delay calculus *)
- (*
+ (* TO BE DONE LATER (Xavier)
if(!Options.delay_calculus)
then
begin
@@ -146,18 +146,7 @@ let rec compile_source dirname basename extension =
raise exc
end;
*)
- (*
- eprintf "Causality analysis@.@?";
- (* Causality analysis *)
- begin
- try
- Causality.check_causal_prog prog
- with (Causality.Cycle v) as exc ->
- Causality.pp_error err_formatter v;
- raise exc
- end;
- *)
-
+
(* Creating destination directory if needed *)
create_dest_dir ();
diff --git a/src/parserLustreSpec.mly b/src/parserLustreSpec.mly
index 17fb13120b88b9b53c0b07784ac8095de20294ac..9b798551cb78bf46ce537d2ec598550909cc5687 100644
--- a/src/parserLustreSpec.mly
+++ b/src/parserLustreSpec.mly
@@ -73,7 +73,7 @@
%nonassoc UMINUS
%start lustre_annot
-%type <LustreSpec.expr_annot> lustre_annot
+%type <LustreSpec.ident -> LustreSpec.expr_annot> lustre_annot
%start lustre_spec
%type <LustreSpec.node_annot> lustre_spec
@@ -287,7 +287,7 @@ const:
| STRING {Const_string $1}
lustre_annot:
-lustre_annot_list EOF { $1 }
+lustre_annot_list EOF { fun node_id -> $1 }
lustre_annot_list:
{ [] }
diff --git a/src/parser_lustre.mly b/src/parser_lustre.mly
index 69af04db6187ba8c47cfc41d0fd83a1ae7bf08e0..314e9c889043bac1c747d26b39c248fae8d1f25e 100755
--- a/src/parser_lustre.mly
+++ b/src/parser_lustre.mly
@@ -37,6 +37,12 @@ let mkdim_ite i t e = mkdim_ite (get_loc ()) i t e
let mkannots annots = { annots = annots; annot_loc = get_loc () }
+let node_stack : ident list ref = ref []
+let debug_calls () = Format.eprintf "call stack: %a@.@?" (Utils.fprintf_list ~sep:", " Format.pp_print_string) !node_stack
+let push_node nd = node_stack:= nd :: !node_stack
+let pop_node () = try node_stack := List.tl !node_stack with _ -> assert false
+let get_current_node () = try List.hd !node_stack with _ -> assert false
+
%}
%token <int> INT
@@ -118,6 +124,9 @@ node_ident:
UIDENT { $1 }
| IDENT { $1 }
+node_ident_decl:
+ node_ident { push_node $1; $1 }
+
vdecl_ident:
UIDENT { $1 }
| IDENT { $1 }
@@ -176,6 +185,7 @@ top_decl_header:
nodei_prototype = $13;
nodei_in_lib = $14;})
in
+ pop_node ();
(*add_imported_node $3 nd;*) [nd] }
prototype_opt:
@@ -188,27 +198,35 @@ in_lib_opt:
top_decl:
| CONST cdecl_list { List.rev ($2 false) }
-| nodespec_list state_annot node_ident LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt locals LET stmt_list TEL
- {let stmts, asserts, annots = $16 in
- let nd = mktop_decl false (Node
- {node_id = $3;
- node_type = Types.new_var ();
- node_clock = Clocks.new_var true;
- node_inputs = List.rev $5;
- node_outputs = List.rev $10;
- node_locals = List.rev $14;
- node_gencalls = [];
- node_checks = [];
- node_asserts = asserts;
- node_stmts = stmts;
- node_dec_stateless = $2;
- node_stateless = None;
- node_spec = $1;
- node_annot = annots})
- in
+| nodespec_list state_annot node_ident_decl LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt locals LET stmt_list TEL
+ {
+ let stmts, asserts, annots = $16 in
+ (* Declaring eqs annots *)
+ List.iter (fun ann ->
+ List.iter (fun (key, _) ->
+ Annotations.add_node_ann $3 key
+ ) ann.annots
+ ) annots;
+ (* Building the node *)
+ let nd = mktop_decl false (Node
+ {node_id = $3;
+ node_type = Types.new_var ();
+ node_clock = Clocks.new_var true;
+ node_inputs = List.rev $5;
+ node_outputs = List.rev $10;
+ node_locals = List.rev $14;
+ node_gencalls = [];
+ node_checks = [];
+ node_asserts = asserts;
+ node_stmts = stmts;
+ node_dec_stateless = $2;
+ node_stateless = None;
+ node_spec = $1;
+ node_annot = annots})
+ in
(*add_node $3 nd;*) [nd] }
-
-nodespec_list:
+
+ nodespec_list:
{ None }
| NODESPEC nodespec_list {
(function
@@ -350,7 +368,7 @@ expr:
| IDENT { mkexpr (Expr_ident $1) }
| tag_ident { mkexpr (Expr_ident $1) (*(Expr_const (Const_tag $1))*) }
| LPAR ANNOT expr RPAR
- {update_expr_annot $3 $2}
+ {update_expr_annot (get_current_node ()) $3 $2}
| LPAR expr RPAR
{$2}
| LPAR tuple_expr RPAR