lustrec / src / inliner.ml @ 3769b712
History  View  Annotate  Download (20.1 KB)
1 
(********************************************************************) 

2 
(* *) 
3 
(* The LustreC compiler toolset / The LustreC Development Team *) 
4 
(* Copyright 2012   ONERA  CNRS  INPT *) 
5 
(* *) 
6 
(* LustreC is free software, distributed WITHOUT ANY WARRANTY *) 
7 
(* under the terms of the GNU Lesser General Public License *) 
8 
(* version 2.1. *) 
9 
(* *) 
10 
(********************************************************************) 
11 
open Lustrec 
12 
open Lustre_types 
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 
24  
25 
let check_node_name id = (fun t > 
26 
match t.top_decl_desc with 
27 
 Node nd > nd.node_id = id 
28 
 _ > false) 
29  
30 
let is_node_var node v = 
31 
try 
32 
ignore (Corelang.get_node_var v node); true 
33 
with Not_found > false 
34  
35 
(* let rename_expr rename expr = expr_replace_var rename expr *) 
36 
(* 
37 
let rename_eq rename eq = 
38 
{ eq with 
39 
eq_lhs = List.map rename eq.eq_lhs; 
40 
eq_rhs = rename_expr rename eq.eq_rhs 
41 
} 
42 
*) 
43 

44 
let rec add_expr_reset_cond cond expr = 
45 
let aux = add_expr_reset_cond cond in 
46 
let new_desc = 
47 
match expr.expr_desc with 
48 
 Expr_const _ 
49 
 Expr_ident _ > expr.expr_desc 
50 
 Expr_tuple el > Expr_tuple (List.map aux el) 
51 
 Expr_ite (c, t, e) > Expr_ite (aux c, aux t, aux e) 
52 

53 
 Expr_arrow (e1, e2) > 
54 
(* we replace the expression e1 > e2 by e1 > (if cond then e1 else e2) *) 
55 
let e1 = aux e1 and e2 = aux e2 in 
56 
(* inlining is performed before typing. we can leave the fields free *) 
57 
let new_e2 = mkexpr expr.expr_loc (Expr_ite (cond, e1, e2)) in 
58 
Expr_arrow (e1, new_e2) 
59  
60 
 Expr_fby _ > assert false (* TODO: deal with fby. This hasn't been much handled yet *) 
61  
62 
 Expr_array el > Expr_array (List.map aux el) 
63 
 Expr_access (e, dim) > Expr_access (aux e, dim) 
64 
 Expr_power (e, dim) > Expr_power (aux e, dim) 
65 
 Expr_pre e > Expr_pre (aux e) 
66 
 Expr_when (e, id, l) > Expr_when (aux e, id, l) 
67 
 Expr_merge (id, cases) > Expr_merge (id, List.map (fun (l,e) > l, aux e) cases) 
68  
69 
 Expr_appl (id, args, reset_opt) > 
70 
(* we "add" cond to the reset field. *) 
71 
let new_reset = match reset_opt with 
72 
None > cond 
73 
 Some cond' > mkpredef_call cond'.expr_loc "" [cond; cond'] 
74 
in 
75 
Expr_appl (id, args, Some new_reset) 
76 

77  
78 
in 
79 
{ expr with expr_desc = new_desc } 
80  
81 
let add_eq_reset_cond cond eq = 
82 
{ eq with eq_rhs = add_expr_reset_cond cond eq.eq_rhs } 
83 
(* 
84 
let get_static_inputs input_arg_list = 
85 
List.fold_right (fun (vdecl, arg) res > 
86 
if vdecl.var_dec_const 
87 
then (vdecl.var_id, Corelang.dimension_of_expr arg) :: res 
88 
else res) 
89 
input_arg_list [] 
90  
91 
let get_carrier_inputs input_arg_list = 
92 
List.fold_right (fun (vdecl, arg) res > 
93 
if Corelang.is_clock_dec_type vdecl.var_dec_type.ty_dec_desc 
94 
then (vdecl.var_id, ident_of_expr arg) :: res 
95 
else res) 
96 
input_arg_list [] 
97 
*) 
98 
(* 
99 
expr, locals', eqs = inline_call id args' reset locals node nodes 
100  
101 
We select the called node equations and variables. 
102 
renamed_inputs = args 
103 
renamed_eqs 
104  
105 
the resulting expression is tuple_of_renamed_outputs 
106 

107 
TODO: convert the specification/annotation/assert and inject them 
108 
*) 
109 
(** [inline_call node loc uid args reset locals caller] returns a tuple (expr, 
110 
locals, eqs, asserts) 
111 
*) 
112 
let inline_call node loc uid args reset locals caller = 
113 
let rename v = 
114 
if v = tag_true  v = tag_false  not (is_node_var node v) then v else 
115 
Corelang.mk_new_node_name caller (Format.sprintf "%s_%i_%s" node.node_id uid v) 
116 
in 
117 
let eqs, auts = get_node_eqs node in 
118 
let eqs' = List.map (rename_eq (fun x > x) rename) eqs in 
119 
let auts' = List.map (rename_aut (fun x > x) rename) auts in 
120 
let input_arg_list = List.combine node.node_inputs (Corelang.expr_list_of_expr args) in 
121 
let static_inputs, dynamic_inputs = List.partition (fun (vdecl, arg) > vdecl.var_dec_const) input_arg_list in 
122 
let static_inputs = List.map (fun (vdecl, arg) > vdecl, Corelang.dimension_of_expr arg) static_inputs in 
123 
let carrier_inputs, other_inputs = List.partition (fun (vdecl, arg) > Corelang.is_clock_dec_type vdecl.var_dec_type.ty_dec_desc) dynamic_inputs in 
124 
let carrier_inputs = List.map (fun (vdecl, arg) > vdecl, Corelang.ident_of_expr arg) carrier_inputs in 
125 
let rename_static v = 
126 
try 
127 
snd (List.find (fun (vdecl, _) > v = vdecl.var_id) static_inputs) 
128 
with Not_found > Dimension.mkdim_ident loc v in 
129 
let rename_carrier v = 
130 
try 
131 
snd (List.find (fun (vdecl, _) > v = vdecl.var_id) carrier_inputs) 
132 
with Not_found > v in 
133 
let rename_var v = 
134 
let vdecl = 
135 
Corelang.mkvar_decl v.var_loc 
136 
(rename v.var_id, 
137 
{ v.var_dec_type with ty_dec_desc = Corelang.rename_static rename_static v.var_dec_type.ty_dec_desc }, 
138 
{ v.var_dec_clock with ck_dec_desc = Corelang.rename_carrier rename_carrier v.var_dec_clock.ck_dec_desc }, 
139 
v.var_dec_const, 
140 
Utils.option_map (rename_expr (fun x > x) rename) v.var_dec_value, 
141 
v.var_parent_nodeid (* we keep the original parent name *) 
142 
) in 
143 
begin 
144 
(* 
145 
(try 
146 
Format.eprintf "Inliner.inline_call unify %a %a@." Types.print_ty vdecl.var_type Dimension.pp_dimension (List.assoc v.var_id static_inputs); 
147 
Typing.unify vdecl.var_type (Type_predef.type_static (List.assoc v.var_id static_inputs) (Types.new_var ())) 
148 
with Not_found > ()); 
149 
(try 
150 
Clock_calculus.unify vdecl.var_clock (Clock_predef.ck_carrier (List.assoc v.var_id carrier_inputs) (Clocks.new_var true)) 
151 
with Not_found > ()); 
152 
(*Format.eprintf "Inliner.inline_call res=%a@." Printers.pp_var vdecl;*) 
153 
*) 
154 
vdecl 
155 
end 
156 
(*Format.eprintf "Inliner.rename_var %a@." Printers.pp_var v;*) 
157 
in 
158 
let inputs' = List.map (fun (vdecl, _) > rename_var vdecl) dynamic_inputs in 
159 
let outputs' = List.map rename_var node.node_outputs in 
160 
let locals' = 
161 
(List.map (fun (vdecl, arg) > let vdecl' = rename_var vdecl in { vdecl' with var_dec_value = Some (Corelang.expr_of_dimension arg) }) static_inputs) 
162 
@ (List.map rename_var node.node_locals) 
163 
in 
164 
(* checking we are at the appropriate (early) step: node_checks and 
165 
node_gencalls should be empty (not yet assigned) *) 
166 
assert (node.node_checks = []); 
167 
assert (node.node_gencalls = []); 
168  
169 
(* Expressing reset locally in equations *) 
170 
let eqs_r' = 
171 
let all_eqs = (List.map (fun eq > Eq eq) eqs') @ (List.map (fun aut > Aut aut) auts') in 
172 
match reset with 
173 
None > all_eqs 
174 
 Some cond > ( 
175 
assert (auts' = []); (* TODO: we do not handle properly automaton in case of reset call *) 
176 
List.map (fun eq > Eq (add_eq_reset_cond cond eq)) eqs' 
177 
) 
178 
in 
179 
let assign_inputs = Eq (mkeq loc (List.map (fun v > v.var_id) inputs', 
180 
expr_of_expr_list args.expr_loc (List.map snd dynamic_inputs))) in 
181 
let expr = expr_of_expr_list loc (List.map expr_of_vdecl outputs') 
182 
in 
183 
let asserts' = (* We rename variables in assert expressions *) 
184 
List.map 
185 
(fun a > 
186 
{a with assert_expr = 
187 
let expr = a.assert_expr in 
188 
rename_expr (fun x > x) rename expr 
189 
}) 
190 
node.node_asserts 
191 
in 
192 
let annots' = 
193 
Plugins.inline_annots rename node.node_annot 
194 
in 
195 
expr, 
196 
inputs'@outputs'@locals'@locals, 
197 
assign_inputs::eqs_r', 
198 
asserts', 
199 
annots' 
200  
201  
202  
203 
let inline_table = Hashtbl.create 23 
204  
205 
(* 
206 
new_expr, new_locals, new_eqs = inline_expr expr locals node nodes 
207 

208 
Each occurence of a node in nodes in the expr should be replaced by fresh 
209 
variables and the code of called node instance added to new_eqs 
210  
211 
*) 
212 
let rec inline_expr ?(selection_on_annotation=false) expr locals node nodes = 
213 
let inline_expr = inline_expr ~selection_on_annotation:selection_on_annotation in 
214 
let inline_node = inline_node ~selection_on_annotation:selection_on_annotation in 
215 
let inline_tuple el = 
216 
List.fold_right (fun e (el_tail, locals, eqs, asserts, annots) > 
217 
let e', locals', eqs', asserts', annots' = inline_expr e locals node nodes in 
218 
e'::el_tail, locals', eqs'@eqs, asserts@asserts', annots@annots' 
219 
) el ([], locals, [], [], []) 
220 
in 
221 
let inline_pair e1 e2 = 
222 
let el', l', eqs', asserts', annots' = inline_tuple [e1;e2] in 
223 
match el' with 
224 
 [e1'; e2'] > e1', e2', l', eqs', asserts', annots' 
225 
 _ > assert false 
226 
in 
227 
let inline_triple e1 e2 e3 = 
228 
let el', l', eqs', asserts', annots' = inline_tuple [e1;e2;e3] in 
229 
match el' with 
230 
 [e1'; e2'; e3'] > e1', e2', e3', l', eqs', asserts', annots' 
231 
 _ > assert false 
232 
in 
233 

234 
match expr.expr_desc with 
235 
 Expr_appl (id, args, reset) > 
236 
let args', locals', eqs', asserts', annots' = inline_expr args locals node nodes in 
237 
if List.exists (check_node_name id) nodes && (* the current node call is provided 
238 
as arguments nodes *) 
239 
(not selection_on_annotation  is_inline_expr expr) (* and if selection on annotation is activated, 
240 
it is explicitely inlined here *) 
241 
then ( 
242 
(* Format.eprintf "Inlining call to %s in expression %a@." id Printers.pp_expr expr; *) 
243 
(* The node should be inlined *) 
244 
(* let _ = Format.eprintf "Inlining call to %s@." id in *) 
245 
let called = try List.find (check_node_name id) nodes 
246 
with Not_found > (assert false) in 
247 
let called = node_of_top called in 
248 
let called' = inline_node called nodes in 
249 
let expr, locals', eqs'', asserts'', annots'' = 
250 
inline_call called' expr.expr_loc expr.expr_tag args' reset locals' node in 
251 
expr, locals', eqs'@eqs'', asserts'@asserts'', annots'@annots'' 
252 
) 
253 
else 
254 
(* let _ = Format.eprintf "Not inlining call to %s@." id in *) 
255 
{ expr with expr_desc = Expr_appl(id, args', reset)}, 
256 
locals', 
257 
eqs', 
258 
asserts', 
259 
annots' 
260  
261 
(* For other cases, we just keep the structure, but convert subexpressions *) 
262 
 Expr_const _ 
263 
 Expr_ident _ > expr, locals, [], [], [] 
264 
 Expr_tuple el > 
265 
let el', l', eqs', asserts', annots' = inline_tuple el in 
266 
{ expr with expr_desc = Expr_tuple el' }, l', eqs', asserts', annots' 
267 
 Expr_ite (g, t, e) > 
268 
let g', t', e', l', eqs', asserts', annots' = inline_triple g t e in 
269 
{ expr with expr_desc = Expr_ite (g', t', e') }, l', eqs', asserts', annots' 
270 
 Expr_arrow (e1, e2) > 
271 
let e1', e2', l', eqs', asserts', annots' = inline_pair e1 e2 in 
272 
{ expr with expr_desc = Expr_arrow (e1', e2') } , l', eqs', asserts', annots' 
273 
 Expr_fby (e1, e2) > 
274 
let e1', e2', l', eqs', asserts', annots' = inline_pair e1 e2 in 
275 
{ expr with expr_desc = Expr_fby (e1', e2') }, l', eqs', asserts', annots' 
276 
 Expr_array el > 
277 
let el', l', eqs', asserts', annots' = inline_tuple el in 
278 
{ expr with expr_desc = Expr_array el' }, l', eqs', asserts', annots' 
279 
 Expr_access (e, dim) > 
280 
let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in 
281 
{ expr with expr_desc = Expr_access (e', dim) }, l', eqs', asserts', annots' 
282 
 Expr_power (e, dim) > 
283 
let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in 
284 
{ expr with expr_desc = Expr_power (e', dim) }, l', eqs', asserts', annots' 
285 
 Expr_pre e > 
286 
let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in 
287 
{ expr with expr_desc = Expr_pre e' }, l', eqs', asserts', annots' 
288 
 Expr_when (e, id, label) > 
289 
let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in 
290 
{ expr with expr_desc = Expr_when (e', id, label) }, l', eqs', asserts', annots' 
291 
 Expr_merge (id, branches) > 
292 
let el, l', eqs', asserts', annots' = inline_tuple (List.map snd branches) in 
293 
let branches' = List.map2 (fun (label, _) v > label, v) branches el in 
294 
{ expr with expr_desc = Expr_merge (id, branches') }, l', eqs', asserts', annots' 
295  
296 
and inline_node ?(selection_on_annotation=false) node nodes = 
297 
try copy_node (Hashtbl.find inline_table node.node_id) 
298 
with Not_found > 
299 
let inline_expr = inline_expr ~selection_on_annotation:selection_on_annotation in 
300 
let eqs, auts = get_node_eqs node in 
301 
assert (auts = []); (* No inlining of automaton yet. One should visit each 
302 
handler eqs and perform similar computation *) 
303 
let new_locals, stmts, asserts, annots = 
304 
List.fold_left (fun (locals, stmts, asserts, annots) eq > 
305 
let eq_rhs', locals', new_stmts', asserts', annots' = 
306 
inline_expr eq.eq_rhs locals node nodes 
307 
in 
308 
locals', Eq { eq with eq_rhs = eq_rhs' }::new_stmts'@stmts, asserts'@asserts, annots'@annots 
309 
) (node.node_locals, [], node.node_asserts, node.node_annot) eqs 
310 
in 
311 
let inlined = 
312 
{ node with 
313 
node_locals = new_locals; 
314 
node_stmts = stmts; 
315 
node_asserts = asserts; 
316 
node_annot = annots; 
317 
} 
318 
in 
319 
begin 
320 
(*Format.eprintf "inline node:<< %a@.>>@." Printers.pp_node inlined;*) 
321 
Hashtbl.add inline_table node.node_id inlined; 
322 
inlined 
323 
end 
324  
325 
let inline_all_calls node nodes = 
326 
let nd = match node.top_decl_desc with Node nd > nd  _ > assert false in 
327 
{ node with top_decl_desc = Node (inline_node nd nodes) } 
328 

329  
330  
331  
332  
333 
let witness filename main_name orig inlined type_env clock_env = 
334 
let loc = Location.dummy_loc in 
335 
let rename_local_node nodes prefix id = 
336 
if List.exists (check_node_name id) nodes then 
337 
prefix ^ id 
338 
else 
339 
id 
340 
in 
341 
let main_orig_node = match (List.find (check_node_name main_name) orig).top_decl_desc with 
342 
Node nd > nd  _ > assert false in 
343 

344 
let orig_rename = rename_local_node orig "orig_" in 
345 
let inlined_rename = rename_local_node inlined "inlined_" in 
346 
let identity = (fun x > x) in 
347 
let is_node top = match top.top_decl_desc with Node _ > true  _ > false in 
348 
let orig = rename_prog orig_rename (* f_node *) identity (* f_var *) identity (* f_const *) orig in 
349 
let inlined = rename_prog inlined_rename identity identity inlined in 
350 
let nodes_origs, others = List.partition is_node orig in 
351 
let nodes_inlined, _ = List.partition is_node inlined in 
352  
353 
(* One ok_i boolean variable per output var *) 
354 
let nb_outputs = List.length main_orig_node.node_outputs in 
355 
let ok_ident = "OK" in 
356 
let ok_i = List.map (fun id > 
357 
mkvar_decl 
358 
loc 
359 
(Format.sprintf "%s_%i" ok_ident id, 
360 
{ty_dec_desc=Tydec_bool; ty_dec_loc=loc}, 
361 
{ck_dec_desc=Ckdec_any; ck_dec_loc=loc}, 
362 
false, 
363 
None, 
364 
None 
365 
) 
366 
) (Utils.enumerate nb_outputs) 
367 
in 
368  
369 
(* OK = ok_1 and ok_2 and ... ok_n1 *) 
370 
let ok_output = mkvar_decl 
371 
loc 
372 
(ok_ident, 
373 
{ty_dec_desc=Tydec_bool; ty_dec_loc=loc}, 
374 
{ck_dec_desc=Ckdec_any; ck_dec_loc=loc}, 
375 
false, 
376 
None, 
377 
None 
378 
) 
379 
in 
380 
let main_ok_expr = 
381 
let mkv x = mkexpr loc (Expr_ident x) in 
382 
match ok_i with 
383 
 [] > assert false 
384 
 [x] > mkv x.var_id 
385 
 hd::tl > 
386 
List.fold_left (fun accu elem > 
387 
mkpredef_call loc "&&" [mkv elem.var_id; accu] 
388 
) (mkv hd.var_id) tl 
389 
in 
390  
391 
(* Building main node *) 
392  
393 
let ok_i_eq = 
394 
{ eq_loc = loc; 
395 
eq_lhs = List.map (fun v > v.var_id) ok_i; 
396 
eq_rhs = 
397 
let inputs = expr_of_expr_list loc (List.map (fun v > mkexpr loc (Expr_ident v.var_id)) main_orig_node.node_inputs) in 
398 
let call_orig = 
399 
mkexpr loc (Expr_appl ("orig_" ^ main_name, inputs, None)) in 
400 
let call_inlined = 
401 
mkexpr loc (Expr_appl ("inlined_" ^ main_name, inputs, None)) in 
402 
let args = mkexpr loc (Expr_tuple [call_orig; call_inlined]) in 
403 
mkexpr loc (Expr_appl ("=", args, None)) 
404 
} in 
405 
let ok_eq = 
406 
{ eq_loc = loc; 
407 
eq_lhs = [ok_ident]; 
408 
eq_rhs = main_ok_expr; 
409 
} in 
410 
let main_node = { 
411 
node_id = "check"; 
412 
node_type = Types.new_var (); 
413 
node_clock = Clocks.new_var true; 
414 
node_inputs = main_orig_node.node_inputs; 
415 
node_outputs = [ok_output]; 
416 
node_locals = ok_i; 
417 
node_gencalls = []; 
418 
node_checks = []; 
419 
node_asserts = []; 
420 
node_stmts = [Eq ok_i_eq; Eq ok_eq]; 
421 
node_dec_stateless = false; 
422 
node_stateless = None; 
423 
node_spec = Some 
424 
(Contract 
425 
(mk_contract_guarantees 
426 
(mkeexpr loc (mkexpr loc (Expr_ident ok_ident))) 
427 
) 
428 
); 
429 
node_annot = []; 
430 
node_iscontract = true; 
431 
} 
432 
in 
433 
let main = [{ top_decl_desc = Node main_node; top_decl_loc = loc; top_decl_owner = filename; top_decl_itf = false }] in 
434 
let new_prog = others@nodes_origs@nodes_inlined@main in 
435 
(* 
436 
let _ = Typing.type_prog type_env new_prog in 
437 
let _ = Clock_calculus.clock_prog clock_env new_prog in 
438 
*) 
439 

440 
let witness_file = (Options_management.get_witness_dir filename) ^ "/" ^ "inliner_witness.lus" in 
441 
let witness_out = open_out witness_file in 
442 
let witness_fmt = Format.formatter_of_out_channel witness_out in 
443 
begin 
444 
List.iter (fun vdecl > Typing.try_unify Type_predef.type_bool vdecl.var_type vdecl.var_loc) (ok_output::ok_i); 
445 
Format.fprintf witness_fmt 
446 
"(* Generated lustre file to check validity of inlining process *)@."; 
447 
Printers.pp_prog witness_fmt new_prog; 
448 
Format.fprintf witness_fmt "@."; 
449 
() 
450 
end (* xx *) 
451  
452 
let global_inline basename prog (*type_env clock_env*) = 
453 
(* We select the main node desc *) 
454 
let main_node, other_nodes, other_tops = 
455 
List.fold_right 
456 
(fun top (main_opt, nodes, others) > 
457 
match top.top_decl_desc with 
458 
 Node nd when nd.node_id = !Options.main_node > 
459 
Some top, nodes, others 
460 
 Node _ > main_opt, top::nodes, others 
461 
 _ > main_opt, nodes, top::others) 
462 
prog (None, [], []) 
463 
in 
464  
465 
(* Recursively each call of a node in the top node is replaced *) 
466 
let main_node = Utils.desome main_node in 
467 
let main_node' = inline_all_calls main_node other_nodes in 
468 
let res = List.map (fun top > if check_node_name !Options.main_node top then main_node' else top) prog in 
469 
(* Code snippet from unstable branch. May be used when reactivating witnesses. 
470 
let res = main_node'::other_tops in 
471 
if !Options.witnesses then ( 
472 
witness 
473 
basename 
474 
(match main_node.top_decl_desc with Node nd > nd.node_id  _ > assert false) 
475 
prog res type_env clock_env 
476 
); 
477 
*) 
478 
res 
479  
480 
let pp_inline_calls fmt prog = 
481 
let local_anns = Annotations.get_expr_annotations keyword in 
482 
let nodes_with_anns = List.fold_left (fun accu (k, _) > ISet.add k accu) ISet.empty local_anns in 
483 
Format.fprintf fmt "@[<v 0>Inlined expresssions in node (by tags):@ %a@]" 
484 
(fprintf_list ~sep:"" 
485 
(fun fmt top > 
486 
match top.top_decl_desc with 
487 
 Node nd when ISet.mem nd.node_id nodes_with_anns > 
488 
Format.fprintf fmt "%s: {@[<v 0>%a}@]@ " 
489 
nd.node_id 
490 
(fprintf_list ~sep:"@ " (fun fmt tag > Format.fprintf fmt "%i" tag)) 
491 
(List.fold_left 
492 
(fun accu (id, tag) > if id = nd.node_id then tag::accu else accu) 
493 
[] 
494 
local_anns 
495 
) 
496 
(*  Node nd > Format.fprintf fmt "%s: no inline annotations" nd.node_id *) 
497 
 _ > () 
498 
)) 
499 
prog 
500 

501 

502 
let local_inline prog (* type_env clock_env *) = 
503 
Log.report ~level:2 (fun fmt > Format.fprintf fmt ".. @[<v 2>Inlining@,"); 
504 
let local_anns = Annotations.get_expr_annotations keyword in 
505 
let prog = 
506 
if local_anns != [] then ( 
507 
let nodes_with_anns = List.fold_left (fun accu (k, _) > ISet.add k accu) ISet.empty local_anns in 
508 
ISet.iter (fun node_id > Log.report ~level:2 (fun fmt > Format.fprintf fmt "Node %s has local expression annotations@ " node_id)) 
509 
nodes_with_anns; 
510 
List.fold_right (fun top accu > 
511 
( match top.top_decl_desc with 
512 
 Node nd when ISet.mem nd.node_id nodes_with_anns > 
513 
Log.report ~level:2 (fun fmt > Format.fprintf fmt "[local inline] Processing node %s@ " nd.node_id); 
514 
let inlined_node = inline_node ~selection_on_annotation:true nd prog in 
515 
(* Format.eprintf "Before inline@.%a@.After:@.%a@." *) 
516 
(* Printers.pp_node nd *) 
517 
(* Printers.pp_node inlined_node; *) 
518 
{ top with top_decl_desc = Node inlined_node } 
519 

520 
 _ > top 
521 
)::accu) prog [] 
522 

523 
) 
524 
else ( 
525 
Log.report ~level:2 (fun fmt > Format.fprintf fmt "No local inline information!@ "); 
526 
prog 
527 
) 
528 
in 
529 
Log.report ~level:2 (fun fmt > Format.fprintf fmt "@]@,"); 
530 
prog 
531  
532 
(* Local Variables: *) 
533 
(* compilecommand:"make C .." *) 
534 
(* End: *) 