Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / inliner.ml @ 37419cf4

History | View | Annotate | Download (17.9 KB)

1 a2d97a3e ploc
(********************************************************************)
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
12 b09a175c ploc
open LustreSpec
13
open Corelang
14 566dbf49 ploc
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 b09a175c ploc
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 fc886259 xthirioux
let is_node_var node v =
31
 try
32
   ignore (Corelang.get_node_var v node); true
33
 with Not_found -> false
34 b09a175c ploc
35 af5af1e8 ploc
let rename_expr rename expr = expr_replace_var rename expr
36 fc886259 xthirioux
37 af5af1e8 ploc
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 45f0f48d xthirioux
43
let rec add_expr_reset_cond cond expr =
44
  let aux = add_expr_reset_cond cond in
45
  let new_desc = 
46
    match expr.expr_desc with
47
    | Expr_const _
48
    | Expr_ident _ -> expr.expr_desc
49
    | Expr_tuple el -> Expr_tuple (List.map aux el)
50
    | Expr_ite (c, t, e) -> Expr_ite (aux c, aux t, aux e)
51
      
52
    | Expr_arrow (e1, e2) -> 
53
      (* we replace the expression e1 -> e2 by e1 -> (if cond then e1 else e2) *)
54
      let e1 = aux e1 and e2 = aux e2 in
55
      (* inlining is performed before typing. we can leave the fields free *)
56
      let new_e2 = mkexpr expr.expr_loc (Expr_ite (cond, e1, e2)) in
57
      Expr_arrow (e1, new_e2) 
58
59
    | Expr_fby _ -> assert false (* TODO: deal with fby. This hasn't been much handled yet *)
60
61
    | Expr_array el -> Expr_array (List.map aux el)
62
    | Expr_access (e, dim) -> Expr_access (aux e, dim)
63
    | Expr_power (e, dim) -> Expr_power (aux e, dim)
64
    | Expr_pre e -> Expr_pre (aux e)
65
    | Expr_when (e, id, l) -> Expr_when (aux e, id, l)
66
    | Expr_merge (id, cases) -> Expr_merge (id, List.map (fun (l,e) -> l, aux e) cases)
67
68
    | Expr_appl (id, args, reset_opt) -> 
69
      (* we "add" cond to the reset field. *)
70
      let new_reset = match reset_opt with
71
	  None -> cond
72
	| Some cond' -> mkpredef_call cond'.expr_loc "||" [cond; cond']
73
      in
74
      Expr_appl (id, args, Some new_reset)
75
      
76
77
  in
78
  { expr with expr_desc = new_desc }
79
80
let add_eq_reset_cond cond eq =
81
  { eq with eq_rhs = add_expr_reset_cond cond eq.eq_rhs }
82 ec433d69 xthirioux
(*
83
let get_static_inputs input_arg_list =
84
 List.fold_right (fun (vdecl, arg) res ->
85
   if vdecl.var_dec_const
86
   then (vdecl.var_id, Corelang.dimension_of_expr arg) :: res
87
   else res)
88
   input_arg_list []
89
90
let get_carrier_inputs input_arg_list =
91
 List.fold_right (fun (vdecl, arg) res ->
92
   if Corelang.is_clock_dec_type vdecl.var_dec_type.ty_dec_desc
93
   then (vdecl.var_id, ident_of_expr arg) :: res
94
   else res)
95
   input_arg_list []
96
*)
97 b09a175c ploc
(* 
98 fc886259 xthirioux
    expr, locals', eqs = inline_call id args' reset locals node nodes
99 b09a175c ploc
100
We select the called node equations and variables.
101
   renamed_inputs = args
102
   renamed_eqs
103
104
the resulting expression is tuple_of_renamed_outputs
105
   
106
TODO: convert the specification/annotation/assert and inject them
107
*)
108 45f0f48d xthirioux
(** [inline_call node loc uid args reset locals caller] returns a tuple (expr,
109
    locals, eqs, asserts)    
110
*)
111
let inline_call node loc uid args reset locals caller =
112 9603460e xthirioux
  let rename v =
113 fc886259 xthirioux
    if v = tag_true || v = tag_false || not (is_node_var node v) then v else
114
      Corelang.mk_new_node_name caller (Format.sprintf "%s_%i_%s" node.node_id uid v)
115 b09a175c ploc
  in
116 ec433d69 xthirioux
  let eqs' = List.map (rename_eq rename) (get_node_eqs node) in
117
  let input_arg_list = List.combine node.node_inputs (Corelang.expr_list_of_expr args) in
118
  let static_inputs, dynamic_inputs = List.partition (fun (vdecl, arg) -> vdecl.var_dec_const) input_arg_list in
119
  let static_inputs = List.map (fun (vdecl, arg) -> vdecl, Corelang.dimension_of_expr arg) static_inputs in
120
  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
121
  let carrier_inputs = List.map (fun (vdecl, arg) -> vdecl, Corelang.ident_of_expr arg) carrier_inputs in
122 fc886259 xthirioux
  let rename_static v =
123
    try
124 ec433d69 xthirioux
      snd (List.find (fun (vdecl, _) -> v = vdecl.var_id) static_inputs)
125
    with Not_found -> Dimension.mkdim_ident loc v in
126 fc886259 xthirioux
  let rename_carrier v =
127
    try
128 ec433d69 xthirioux
      snd (List.find (fun (vdecl, _) -> v = vdecl.var_id) carrier_inputs)
129 fc886259 xthirioux
    with Not_found -> v in
130
  let rename_var v =
131 ec433d69 xthirioux
    let vdecl =
132
      Corelang.mkvar_decl v.var_loc
133
	(rename v.var_id,
134
	 { v.var_dec_type  with ty_dec_desc = Corelang.rename_static rename_static v.var_dec_type.ty_dec_desc },
135
	 { v.var_dec_clock with ck_dec_desc = Corelang.rename_carrier rename_carrier v.var_dec_clock.ck_dec_desc },
136
	 v.var_dec_const,
137
	 Utils.option_map (rename_expr rename) v.var_dec_value) in
138
    begin
139 45f0f48d xthirioux
      (*
140
	(try
141
	Format.eprintf "Inliner.inline_call unify %a %a@." Types.print_ty vdecl.var_type Dimension.pp_dimension (List.assoc v.var_id static_inputs);
142
	Typing.unify vdecl.var_type (Type_predef.type_static (List.assoc v.var_id static_inputs) (Types.new_var ()))
143
	with Not_found -> ());
144
	(try
145
	Clock_calculus.unify vdecl.var_clock (Clock_predef.ck_carrier (List.assoc v.var_id carrier_inputs) (Clocks.new_var true))
146
	with Not_found -> ());
147
      (*Format.eprintf "Inliner.inline_call res=%a@." Printers.pp_var vdecl;*)
148
      *)
149 ec433d69 xthirioux
      vdecl
150
    end
151 01d48bb0 xthirioux
    (*Format.eprintf "Inliner.rename_var %a@." Printers.pp_var v;*)
152 ec433d69 xthirioux
  in
153
  let inputs' = List.map (fun (vdecl, _) -> rename_var vdecl) dynamic_inputs in
154 b09a175c ploc
  let outputs' = List.map rename_var node.node_outputs in
155 ec433d69 xthirioux
  let locals' =
156 01d48bb0 xthirioux
      (List.map (fun (vdecl, arg) -> let vdecl' = rename_var vdecl in { vdecl' with var_dec_value = Some (Corelang.expr_of_dimension arg) }) static_inputs)
157 ec433d69 xthirioux
    @ (List.map rename_var node.node_locals) 
158 01d48bb0 xthirioux
in
159 b09a175c ploc
  (* checking we are at the appropriate (early) step: node_checks and
160
     node_gencalls should be empty (not yet assigned) *)
161
  assert (node.node_checks = []);
162
  assert (node.node_gencalls = []);
163
164 45f0f48d xthirioux
  (* Expressing reset locally in equations *)
165
  let eqs_r' =
166
    match reset with
167
      None -> eqs'
168
    | Some cond -> List.map (add_eq_reset_cond cond) eqs'
169
  in
170
  let assign_inputs = mkeq loc (List.map (fun v -> v.var_id) inputs',
171
                                expr_of_expr_list args.expr_loc (List.map snd dynamic_inputs)) in
172 fc886259 xthirioux
  let expr = expr_of_expr_list loc (List.map expr_of_vdecl outputs')
173 b09a175c ploc
  in
174 af5af1e8 ploc
  let asserts' = (* We rename variables in assert expressions *)
175
    List.map 
176
      (fun a -> 
177
	{a with assert_expr = 
178
	    let expr = a.assert_expr in
179
	    rename_expr rename expr
180 45f0f48d xthirioux
	})
181 af5af1e8 ploc
      node.node_asserts 
182
  in
183 04a63d25 xthirioux
  let annots' =
184
    Plugins.inline_annots rename node.node_annot
185
  in
186 af5af1e8 ploc
  expr, 
187
  inputs'@outputs'@locals'@locals, 
188 45f0f48d xthirioux
  assign_inputs::eqs_r',
189 04a63d25 xthirioux
  asserts',
190
  annots'
191 b09a175c ploc
192
193
194 fc886259 xthirioux
let inline_table = Hashtbl.create 23
195 b09a175c ploc
196
(* 
197 fc886259 xthirioux
   new_expr, new_locals, new_eqs = inline_expr expr locals node nodes
198 b09a175c ploc
   
199
   Each occurence of a node in nodes in the expr should be replaced by fresh
200
   variables and the code of called node instance added to new_eqs
201
202
*)
203 fc886259 xthirioux
let rec inline_expr ?(selection_on_annotation=false) expr locals node nodes =
204 566dbf49 ploc
  let inline_expr = inline_expr ~selection_on_annotation:selection_on_annotation in
205
  let inline_node = inline_node ~selection_on_annotation:selection_on_annotation in
206 b09a175c ploc
  let inline_tuple el = 
207 04a63d25 xthirioux
    List.fold_right (fun e (el_tail, locals, eqs, asserts, annots) -> 
208
      let e', locals', eqs', asserts', annots' = inline_expr e locals node nodes in
209
      e'::el_tail, locals', eqs'@eqs, asserts@asserts', annots@annots'
210
    ) el ([], locals, [], [], [])
211 b09a175c ploc
  in
212
  let inline_pair e1 e2 = 
213 04a63d25 xthirioux
    let el', l', eqs', asserts', annots' = inline_tuple [e1;e2] in
214 b09a175c ploc
    match el' with
215 d2d9d4cb ploc
    | [e1'; e2'] -> e1', e2', l', eqs', asserts', annots'
216 b09a175c ploc
    | _ -> assert false
217
  in
218
  let inline_triple e1 e2 e3 = 
219 04a63d25 xthirioux
    let el', l', eqs', asserts', annots' = inline_tuple [e1;e2;e3] in
220 b09a175c ploc
    match el' with
221 04a63d25 xthirioux
    | [e1'; e2'; e3'] -> e1', e2', e3', l', eqs', asserts', annots'
222 b09a175c ploc
    | _ -> assert false
223
  in
224 566dbf49 ploc
  
225 b09a175c ploc
  match expr.expr_desc with
226
  | Expr_appl (id, args, reset) ->
227 04a63d25 xthirioux
    let args', locals', eqs', asserts', annots' = inline_expr args locals node nodes in 
228 566dbf49 ploc
    if List.exists (check_node_name id) nodes && (* the current node call is provided
229
						    as arguments nodes *)
230
      (not selection_on_annotation || is_inline_expr expr) (* and if selection on annotation is activated, 
231
							      it is explicitely inlined here *)
232
    then 
233 b09a175c ploc
      (* The node should be inlined *)
234 fc886259 xthirioux
      (* let _ =     Format.eprintf "Inlining call to %s@." id in *)
235
      let called = try List.find (check_node_name id) nodes 
236 b09a175c ploc
	with Not_found -> (assert false) in
237 fc886259 xthirioux
      let called = node_of_top called in
238
      let called' = inline_node called nodes in
239 04a63d25 xthirioux
      let expr, locals', eqs'', asserts'', annots'' = 
240 45f0f48d xthirioux
	inline_call called' expr.expr_loc expr.expr_tag args' reset locals' node in
241 04a63d25 xthirioux
      expr, locals', eqs'@eqs'', asserts'@asserts'', annots'@annots''
242 b09a175c ploc
    else 
243
      (* let _ =     Format.eprintf "Not inlining call to %s@." id in *)
244 af5af1e8 ploc
      { expr with expr_desc = Expr_appl(id, args', reset)}, 
245
      locals', 
246
      eqs', 
247 04a63d25 xthirioux
      asserts',
248
      annots'
249 b09a175c ploc
250
  (* For other cases, we just keep the structure, but convert sub-expressions *)
251
  | Expr_const _ 
252 04a63d25 xthirioux
  | Expr_ident _ -> expr, locals, [], [], []
253 b09a175c ploc
  | Expr_tuple el -> 
254 04a63d25 xthirioux
    let el', l', eqs', asserts', annots' = inline_tuple el in
255
    { expr with expr_desc = Expr_tuple el' }, l', eqs', asserts', annots'
256 b09a175c ploc
  | Expr_ite (g, t, e) ->
257 04a63d25 xthirioux
    let g', t', e', l', eqs', asserts', annots' = inline_triple g t e in
258
    { expr with expr_desc = Expr_ite (g', t', e') }, l', eqs', asserts', annots'
259 b09a175c ploc
  | Expr_arrow (e1, e2) ->
260 04a63d25 xthirioux
    let e1', e2', l', eqs', asserts', annots' = inline_pair e1 e2 in
261
    { expr with expr_desc = Expr_arrow (e1', e2') } , l', eqs', asserts', annots'
262 b09a175c ploc
  | Expr_fby (e1, e2) ->
263 04a63d25 xthirioux
    let e1', e2', l', eqs', asserts', annots' = inline_pair e1 e2 in
264
    { expr with expr_desc = Expr_fby (e1', e2') }, l', eqs', asserts', annots'
265 b09a175c ploc
  | Expr_array el ->
266 04a63d25 xthirioux
    let el', l', eqs', asserts', annots' = inline_tuple el in
267
    { expr with expr_desc = Expr_array el' }, l', eqs', asserts', annots'
268 b09a175c ploc
  | Expr_access (e, dim) ->
269 04a63d25 xthirioux
    let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in 
270
    { expr with expr_desc = Expr_access (e', dim) }, l', eqs', asserts', annots'
271 b09a175c ploc
  | Expr_power (e, dim) ->
272 04a63d25 xthirioux
    let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in 
273
    { expr with expr_desc = Expr_power (e', dim) }, l', eqs', asserts', annots'
274 b09a175c ploc
  | Expr_pre e ->
275 04a63d25 xthirioux
    let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in 
276
    { expr with expr_desc = Expr_pre e' }, l', eqs', asserts', annots'
277 b09a175c ploc
  | Expr_when (e, id, label) ->
278 04a63d25 xthirioux
    let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in 
279
    { expr with expr_desc = Expr_when (e', id, label) }, l', eqs', asserts', annots'
280 b09a175c ploc
  | Expr_merge (id, branches) ->
281 04a63d25 xthirioux
    let el, l', eqs', asserts', annots' = inline_tuple (List.map snd branches) in
282 b09a175c ploc
    let branches' = List.map2 (fun (label, _) v -> label, v) branches el in
283 04a63d25 xthirioux
    { expr with expr_desc = Expr_merge (id, branches') }, l', eqs', asserts', annots'
284 fc886259 xthirioux
285
and inline_node ?(selection_on_annotation=false) node nodes =
286 ec433d69 xthirioux
  try copy_node (Hashtbl.find inline_table node.node_id)
287 fc886259 xthirioux
  with Not_found ->
288 566dbf49 ploc
  let inline_expr = inline_expr ~selection_on_annotation:selection_on_annotation in
289 04a63d25 xthirioux
  let new_locals, eqs, asserts, annots = 
290
    List.fold_left (fun (locals, eqs, asserts, annots) eq ->
291
      let eq_rhs', locals', new_eqs', asserts', annots' = 
292 fc886259 xthirioux
	inline_expr eq.eq_rhs locals node nodes 
293 b09a175c ploc
      in
294 04a63d25 xthirioux
      locals', { eq with eq_rhs = eq_rhs' }::new_eqs'@eqs, asserts'@asserts, annots'@annots
295
    ) (node.node_locals, [], node.node_asserts, node.node_annot) (get_node_eqs node)
296 b09a175c ploc
  in
297 fc886259 xthirioux
  let inlined = 
298
  { node with
299 b09a175c ploc
    node_locals = new_locals;
300 b08ffca7 xthirioux
    node_stmts = List.map (fun eq -> Eq eq) eqs;
301 af5af1e8 ploc
    node_asserts = asserts;
302 04a63d25 xthirioux
    node_annot = annots;
303 b09a175c ploc
  }
304 fc886259 xthirioux
  in
305
  begin
306
    (*Format.eprintf "inline node:<< %a@.>>@." Printers.pp_node inlined;*)
307
    Hashtbl.add inline_table node.node_id inlined;
308
    inlined
309
  end
310 b09a175c ploc
311
let inline_all_calls node nodes =
312
  let nd = match node.top_decl_desc with Node nd -> nd | _ -> assert false in
313
  { node with top_decl_desc = Node (inline_node nd nodes) }
314
    
315
316
317
318
319 592f508c ploc
let witness filename main_name orig inlined type_env clock_env =
320 b09a175c ploc
  let loc = Location.dummy_loc in
321
  let rename_local_node nodes prefix id =
322
    if List.exists (check_node_name id) nodes then
323
      prefix ^ id 
324
    else
325
      id
326
  in
327
  let main_orig_node = match (List.find (check_node_name main_name) orig).top_decl_desc with
328
  Node nd -> nd | _ -> assert false in
329
  
330
  let orig_rename = rename_local_node orig "orig_" in
331
  let inlined_rename = rename_local_node inlined "inlined_" in
332
  let identity = (fun x -> x) in
333
  let is_node top = match top.top_decl_desc with Node _ -> true | _ -> false in
334
  let orig = rename_prog orig_rename identity identity orig in
335
  let inlined = rename_prog inlined_rename identity identity inlined in
336
  let nodes_origs, others = List.partition is_node orig in
337
  let nodes_inlined, _ = List.partition is_node inlined in
338
339 b50c665d ploc
  (* One ok_i boolean variable  per output var *)
340
  let nb_outputs = List.length main_orig_node.node_outputs in
341 ec433d69 xthirioux
  let ok_ident = "OK" in
342 b50c665d ploc
  let ok_i = List.map (fun id ->
343
    mkvar_decl 
344
      loc 
345 ec433d69 xthirioux
      (Format.sprintf "%s_%i" ok_ident id,
346 b50c665d ploc
       {ty_dec_desc=Tydec_bool; ty_dec_loc=loc},
347
       {ck_dec_desc=Ckdec_any; ck_dec_loc=loc},
348 ec433d69 xthirioux
       false,
349
       None)
350 b50c665d ploc
  ) (Utils.enumerate nb_outputs) 
351
  in
352
353
  (* OK = ok_1 and ok_2 and ... ok_n-1 *)
354 b09a175c ploc
  let ok_output = mkvar_decl 
355
    loc 
356
    (ok_ident,
357
     {ty_dec_desc=Tydec_bool; ty_dec_loc=loc},
358
     {ck_dec_desc=Ckdec_any; ck_dec_loc=loc},
359 ec433d69 xthirioux
     false,
360
     None)
361 b09a175c ploc
  in
362 b50c665d ploc
  let main_ok_expr =
363
    let mkv x = mkexpr loc (Expr_ident x) in
364
    match ok_i with
365
    | [] -> assert false
366
    | [x] -> mkv x.var_id 
367
    | hd::tl -> 
368
      List.fold_left (fun accu elem -> 
369
	mkpredef_call loc "&&" [mkv elem.var_id; accu]
370
      ) (mkv hd.var_id) tl
371
  in
372
373
  (* Building main node *)
374
375 b08ffca7 xthirioux
  let ok_i_eq =
376
    { eq_loc = loc;
377
      eq_lhs = List.map (fun v -> v.var_id) ok_i;
378
      eq_rhs = 
379
	let inputs = expr_of_expr_list  loc (List.map (fun v -> mkexpr loc (Expr_ident v.var_id)) main_orig_node.node_inputs) in
380
	let call_orig = 
381
	  mkexpr loc (Expr_appl ("orig_" ^ main_name, inputs, None)) in
382
	let call_inlined = 
383
	  mkexpr loc (Expr_appl ("inlined_" ^ main_name, inputs, None)) in
384
	let args = mkexpr loc (Expr_tuple [call_orig; call_inlined]) in 
385
	mkexpr loc (Expr_appl ("=", args, None))
386
    } in
387
  let ok_eq =
388
    { eq_loc = loc;
389
      eq_lhs = [ok_ident];
390
      eq_rhs = main_ok_expr;
391
    } in
392 b09a175c ploc
  let main_node = {
393
    node_id = "check";
394
    node_type = Types.new_var ();
395
    node_clock = Clocks.new_var true;
396
    node_inputs = main_orig_node.node_inputs;
397
    node_outputs = [ok_output];
398 9603460e xthirioux
    node_locals = ok_i;
399 b09a175c ploc
    node_gencalls = [];
400
    node_checks = [];
401
    node_asserts = [];
402 b08ffca7 xthirioux
    node_stmts = [Eq ok_i_eq; Eq ok_eq];
403 3ab5748b ploc
    node_dec_stateless = false;
404 52cfee34 xthirioux
    node_stateless = None;
405 b09a175c ploc
    node_spec = Some 
406
      {requires = []; 
407 01c7d5e1 ploc
       ensures = [mkeexpr loc (mkexpr loc (Expr_ident ok_ident))];
408
       behaviors = [];
409
       spec_loc = loc
410 b09a175c ploc
      };
411 01c7d5e1 ploc
    node_annot = [];
412 b09a175c ploc
  }
413
  in
414 ef34b4ae xthirioux
  let main = [{ top_decl_desc = Node main_node; top_decl_loc = loc; top_decl_owner = filename; top_decl_itf = false }] in
415 b09a175c ploc
  let new_prog = others@nodes_origs@nodes_inlined@main in
416 04a63d25 xthirioux
(*
417
  let _ = Typing.type_prog type_env new_prog in
418
  let _ = Clock_calculus.clock_prog clock_env new_prog in
419
*)
420
   
421 592f508c ploc
  let witness_file = (Options.get_witness_dir filename) ^ "/" ^ "inliner_witness.lus" in
422 b09a175c ploc
  let witness_out = open_out witness_file in
423
  let witness_fmt = Format.formatter_of_out_channel witness_out in
424 ec433d69 xthirioux
  begin
425
    List.iter (fun vdecl -> Typing.try_unify Type_predef.type_bool vdecl.var_type vdecl.var_loc) (ok_output::ok_i);
426
    Format.fprintf witness_fmt
427
      "(* Generated lustre file to check validity of inlining process *)@.";
428
    Printers.pp_prog witness_fmt new_prog;
429
    Format.fprintf witness_fmt "@.";
430
    ()
431
  end (* xx *)
432 b09a175c ploc
433 592f508c ploc
let global_inline basename prog type_env clock_env =
434 b09a175c ploc
  (* We select the main node desc *)
435
  let main_node, other_nodes, other_tops = 
436 ec433d69 xthirioux
    List.fold_right
437
      (fun top (main_opt, nodes, others) -> 
438 b09a175c ploc
	match top.top_decl_desc with 
439
	| Node nd when nd.node_id = !Options.main_node -> 
440
	  Some top, nodes, others
441
	| Node _ -> main_opt, top::nodes, others
442
	| _ -> main_opt, nodes, top::others) 
443 ec433d69 xthirioux
      prog (None, [], []) 
444 b09a175c ploc
  in
445 85da3a4b ploc
446 b09a175c ploc
  (* Recursively each call of a node in the top node is replaced *)
447
  let main_node = Utils.desome main_node in
448
  let main_node' = inline_all_calls main_node other_nodes in
449 ec433d69 xthirioux
  let res = List.map (fun top -> if check_node_name !Options.main_node top then main_node' else top) prog in
450 85da3a4b ploc
 (* Code snippet from unstable branch. May be used when reactivating witnesses. 
451
 let res = main_node'::other_tops in
452 53206908 xthirioux
  if !Options.witnesses then (
453
    witness 
454
      basename
455
      (match main_node.top_decl_desc  with Node nd -> nd.node_id | _ -> assert false) 
456
      prog res type_env clock_env
457
  );
458 85da3a4b ploc
*)
459 b09a175c ploc
  res
460 b50c665d ploc
461 566dbf49 ploc
let local_inline basename prog type_env clock_env =
462
  let local_anns = Annotations.get_expr_annotations keyword in
463
  if local_anns != [] then (
464
    let nodes_with_anns = List.fold_left (fun accu (k, _) -> ISet.add k accu) ISet.empty local_anns in
465
    ISet.iter (fun node_id -> Format.eprintf "Node %s has local expression annotations@." node_id) nodes_with_anns;
466
    List.fold_right (fun top accu -> 
467
      ( match top.top_decl_desc with
468
      | Node nd when ISet.mem nd.node_id nodes_with_anns ->
469
	{ top with top_decl_desc = Node (inline_node ~selection_on_annotation:true nd prog) }
470
      | _ -> top
471
      )::accu) prog []
472
    
473
)
474
 else
475
  prog
476
477
478 b50c665d ploc
(* Local Variables: *)
479
(* compile-command:"make -C .." *)
480
(* End: *)