Revision 6394042a src/inliner.ml
src/inliner.ml | ||
---|---|---|
11 | 11 |
|
12 | 12 |
open LustreSpec |
13 | 13 |
open Corelang |
14 |
open Utils |
|
15 |
|
|
16 |
(* Local annotations are declared with the following key /inlining/: true *) |
|
17 |
let keyword = ["inlining"] |
|
18 |
|
|
19 |
let is_inline_expr expr = |
|
20 |
match expr.expr_annot with |
|
21 |
| Some ann -> |
|
22 |
List.exists (fun (key, value) -> key = keyword) ann.annots |
|
23 |
| None -> false |
|
14 | 24 |
|
15 | 25 |
let check_node_name id = (fun t -> |
16 | 26 |
match t.top_decl_desc with |
... | ... | |
90 | 100 |
variables and the code of called node instance added to new_eqs |
91 | 101 |
|
92 | 102 |
*) |
93 |
let rec inline_expr expr locals nodes = |
|
103 |
let rec inline_expr ?(selection_on_annotation=false) expr locals nodes = |
|
104 |
let inline_expr = inline_expr ~selection_on_annotation:selection_on_annotation in |
|
105 |
let inline_node = inline_node ~selection_on_annotation:selection_on_annotation in |
|
94 | 106 |
let inline_tuple el = |
95 | 107 |
List.fold_right (fun e (el_tail, locals, eqs, asserts) -> |
96 | 108 |
let e', locals', eqs', asserts' = inline_expr e locals nodes in |
... | ... | |
109 | 121 |
| [e1'; e2'; e3'] -> e1', e2', e3', l', eqs', asserts' |
110 | 122 |
| _ -> assert false |
111 | 123 |
in |
112 |
|
|
124 |
|
|
113 | 125 |
match expr.expr_desc with |
114 | 126 |
| Expr_appl (id, args, reset) -> |
115 | 127 |
let args', locals', eqs', asserts' = inline_expr args locals nodes in |
116 |
if List.exists (check_node_name id) nodes then |
|
128 |
if List.exists (check_node_name id) nodes && (* the current node call is provided |
|
129 |
as arguments nodes *) |
|
130 |
(not selection_on_annotation || is_inline_expr expr) (* and if selection on annotation is activated, |
|
131 |
it is explicitely inlined here *) |
|
132 |
then |
|
117 | 133 |
(* The node should be inlined *) |
118 |
(* let _ = Format.eprintf "Inlining call to %s@." id in *)
|
|
134 |
let _ = Format.eprintf "Inlining call to %s@." id in
|
|
119 | 135 |
let node = try List.find (check_node_name id) nodes |
120 | 136 |
with Not_found -> (assert false) in |
121 | 137 |
let node = node_of_top node in |
... | ... | |
164 | 180 |
let el, l', eqs', asserts' = inline_tuple (List.map snd branches) in |
165 | 181 |
let branches' = List.map2 (fun (label, _) v -> label, v) branches el in |
166 | 182 |
{ expr with expr_desc = Expr_merge (id, branches') }, l', eqs', asserts' |
167 |
and inline_node nd nodes = |
|
183 |
and inline_node ?(selection_on_annotation=false) nd nodes = |
|
184 |
let inline_expr = inline_expr ~selection_on_annotation:selection_on_annotation in |
|
168 | 185 |
let new_locals, eqs, asserts = |
169 | 186 |
List.fold_left (fun (locals, eqs, asserts) eq -> |
170 | 187 |
let eq_rhs', locals', new_eqs', asserts' = |
... | ... | |
319 | 336 |
); |
320 | 337 |
res |
321 | 338 |
|
339 |
let local_inline basename prog type_env clock_env = |
|
340 |
let local_anns = Annotations.get_expr_annotations keyword in |
|
341 |
if local_anns != [] then ( |
|
342 |
let nodes_with_anns = List.fold_left (fun accu (k, _) -> ISet.add k accu) ISet.empty local_anns in |
|
343 |
ISet.iter (fun node_id -> Format.eprintf "Node %s has local expression annotations@." node_id) nodes_with_anns; |
|
344 |
List.fold_right (fun top accu -> |
|
345 |
( match top.top_decl_desc with |
|
346 |
| Node nd when ISet.mem nd.node_id nodes_with_anns -> |
|
347 |
{ top with top_decl_desc = Node (inline_node ~selection_on_annotation:true nd prog) } |
|
348 |
| _ -> top |
|
349 |
)::accu) prog [] |
|
350 |
|
|
351 |
) |
|
352 |
else |
|
353 |
prog |
|
354 |
|
|
355 |
|
|
322 | 356 |
(* Local Variables: *) |
323 | 357 |
(* compile-command:"make -C .." *) |
324 | 358 |
(* End: *) |
Also available in: Unified diff