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
|
|
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, _) -> key = keyword) ann.annots
|
23
|
| None ->
|
24
|
false
|
25
|
|
26
|
let check_node_name id t =
|
27
|
match t.top_decl_desc with Node nd -> nd.node_id = id | _ -> false
|
28
|
|
29
|
let is_node_var node v =
|
30
|
try
|
31
|
ignore (Corelang.get_node_var v node);
|
32
|
true
|
33
|
with Not_found -> false
|
34
|
|
35
|
(* let rename_expr rename expr = expr_replace_var rename expr *)
|
36
|
(* let rename_eq rename eq = { eq with eq_lhs = List.map rename eq.eq_lhs;
|
37
|
eq_rhs = rename_expr rename eq.eq_rhs } *)
|
38
|
|
39
|
let rec add_expr_reset_cond cond expr =
|
40
|
let aux = add_expr_reset_cond cond in
|
41
|
let new_desc =
|
42
|
match expr.expr_desc with
|
43
|
| Expr_const _ | Expr_ident _ ->
|
44
|
expr.expr_desc
|
45
|
| Expr_tuple el ->
|
46
|
Expr_tuple (List.map aux el)
|
47
|
| Expr_ite (c, t, e) ->
|
48
|
Expr_ite (aux c, aux t, aux e)
|
49
|
| Expr_arrow (e1, e2) ->
|
50
|
(* we replace the expression e1 -> e2 by e1 -> (if cond then e1 else e2) *)
|
51
|
let e1 = aux e1 and e2 = aux e2 in
|
52
|
(* inlining is performed before typing. we can leave the fields free *)
|
53
|
let new_e2 = mkexpr expr.expr_loc (Expr_ite (cond, e1, e2)) in
|
54
|
Expr_arrow (e1, new_e2)
|
55
|
| Expr_fby _ ->
|
56
|
assert false (* TODO: deal with fby. This hasn't been much handled yet *)
|
57
|
| Expr_array el ->
|
58
|
Expr_array (List.map aux el)
|
59
|
| Expr_access (e, dim) ->
|
60
|
Expr_access (aux e, dim)
|
61
|
| Expr_power (e, dim) ->
|
62
|
Expr_power (aux e, dim)
|
63
|
| Expr_pre e ->
|
64
|
Expr_pre (aux e)
|
65
|
| Expr_when (e, id, l) ->
|
66
|
Expr_when (aux e, id, l)
|
67
|
| Expr_merge (id, cases) ->
|
68
|
Expr_merge (id, List.map (fun (l, e) -> l, aux e) cases)
|
69
|
| Expr_appl (id, args, reset_opt) ->
|
70
|
(* we "add" cond to the reset field. *)
|
71
|
let new_reset =
|
72
|
match reset_opt with
|
73
|
| None ->
|
74
|
cond
|
75
|
| Some cond' ->
|
76
|
mkpredef_call cond'.expr_loc "||" [ cond; cond' ]
|
77
|
in
|
78
|
Expr_appl (id, args, Some new_reset)
|
79
|
in
|
80
|
|
81
|
{ expr with expr_desc = new_desc }
|
82
|
|
83
|
let add_eq_reset_cond cond eq =
|
84
|
{ eq with eq_rhs = add_expr_reset_cond cond eq.eq_rhs }
|
85
|
(* let get_static_inputs input_arg_list = List.fold_right (fun (vdecl, arg) res
|
86
|
-> if vdecl.var_dec_const then (vdecl.var_id, Corelang.dimension_of_expr arg)
|
87
|
:: res else res) input_arg_list []
|
88
|
|
89
|
let get_carrier_inputs input_arg_list = List.fold_right (fun (vdecl, arg) res
|
90
|
-> if Corelang.is_clock_dec_type vdecl.var_dec_type.ty_dec_desc then
|
91
|
(vdecl.var_id, ident_of_expr arg) :: res else res) input_arg_list [] *)
|
92
|
(* expr, locals', eqs = inline_call id args' reset locals node nodes
|
93
|
|
94
|
We select the called node equations and variables. renamed_inputs = args
|
95
|
renamed_eqs
|
96
|
|
97
|
the resulting expression is tuple_of_renamed_outputs
|
98
|
|
99
|
TODO: convert the specification/annotation/assert and inject them *)
|
100
|
|
101
|
(** [inline_call node loc uid args reset locals caller] returns a tuple (expr,
|
102
|
locals, eqs, asserts) *)
|
103
|
let inline_call node loc uid args reset locals caller =
|
104
|
let rename v =
|
105
|
if v = tag_true || v = tag_false || not (is_node_var node v) then v
|
106
|
else
|
107
|
Corelang.mk_new_node_name caller
|
108
|
(Format.sprintf "%s_%i_%s" node.node_id uid v)
|
109
|
in
|
110
|
let eqs, auts = get_node_eqs node in
|
111
|
let eqs' = List.map (rename_eq (fun x -> x) rename) eqs in
|
112
|
let auts' = List.map (rename_aut (fun x -> x) rename) auts in
|
113
|
let input_arg_list =
|
114
|
List.combine node.node_inputs (Corelang.expr_list_of_expr args)
|
115
|
in
|
116
|
let static_inputs, dynamic_inputs =
|
117
|
List.partition (fun (vdecl, _) -> vdecl.var_dec_const) input_arg_list
|
118
|
in
|
119
|
let static_inputs =
|
120
|
List.map
|
121
|
(fun (vdecl, arg) -> vdecl, Corelang.dimension_of_expr arg)
|
122
|
static_inputs
|
123
|
in
|
124
|
let carrier_inputs, _ =
|
125
|
List.partition
|
126
|
(fun (vdecl, _) ->
|
127
|
Corelang.is_clock_dec_type vdecl.var_dec_type.ty_dec_desc)
|
128
|
dynamic_inputs
|
129
|
in
|
130
|
let carrier_inputs =
|
131
|
List.map
|
132
|
(fun (vdecl, arg) -> vdecl, Corelang.ident_of_expr arg)
|
133
|
carrier_inputs
|
134
|
in
|
135
|
let rename_static v =
|
136
|
try snd (List.find (fun (vdecl, _) -> v = vdecl.var_id) static_inputs)
|
137
|
with Not_found -> Dimension.mkdim_ident loc v
|
138
|
in
|
139
|
let rename_carrier v =
|
140
|
try snd (List.find (fun (vdecl, _) -> v = vdecl.var_id) carrier_inputs)
|
141
|
with Not_found -> v
|
142
|
in
|
143
|
let rename_var v =
|
144
|
let vdecl =
|
145
|
Corelang.mkvar_decl v.var_loc
|
146
|
( rename v.var_id,
|
147
|
{
|
148
|
v.var_dec_type with
|
149
|
ty_dec_desc =
|
150
|
Corelang.rename_static rename_static v.var_dec_type.ty_dec_desc;
|
151
|
},
|
152
|
{
|
153
|
v.var_dec_clock with
|
154
|
ck_dec_desc =
|
155
|
Corelang.rename_carrier rename_carrier v.var_dec_clock.ck_dec_desc;
|
156
|
},
|
157
|
v.var_dec_const,
|
158
|
Utils.option_map (rename_expr (fun x -> x) rename) v.var_dec_value,
|
159
|
v.var_parent_nodeid (* we keep the original parent name *) )
|
160
|
in
|
161
|
(* (try Format.eprintf "Inliner.inline_call unify %a %a@." Types.print_ty
|
162
|
vdecl.var_type Dimension.pp_dimension (List.assoc v.var_id
|
163
|
static_inputs); Typing.unify vdecl.var_type (Type_predef.type_static
|
164
|
(List.assoc v.var_id static_inputs) (Types.new_var ())) with Not_found ->
|
165
|
()); (try Clock_calculus.unify vdecl.var_clock (Clock_predef.ck_carrier
|
166
|
(List.assoc v.var_id carrier_inputs) (Clocks.new_var true)) with
|
167
|
Not_found -> ()); (*Format.eprintf "Inliner.inline_call res=%a@."
|
168
|
Printers.pp_var vdecl;*) *)
|
169
|
vdecl
|
170
|
(*Format.eprintf "Inliner.rename_var %a@." Printers.pp_var v;*)
|
171
|
in
|
172
|
let inputs' = List.map (fun (vdecl, _) -> rename_var vdecl) dynamic_inputs in
|
173
|
let outputs' = List.map rename_var node.node_outputs in
|
174
|
let locals' =
|
175
|
List.map
|
176
|
(fun (vdecl, arg) ->
|
177
|
let vdecl' = rename_var vdecl in
|
178
|
{ vdecl' with var_dec_value = Some (Corelang.expr_of_dimension arg) })
|
179
|
static_inputs
|
180
|
@ List.map rename_var node.node_locals
|
181
|
in
|
182
|
(* checking we are at the appropriate (early) step: node_checks and
|
183
|
node_gencalls should be empty (not yet assigned) *)
|
184
|
assert (node.node_checks = []);
|
185
|
assert (node.node_gencalls = []);
|
186
|
|
187
|
(* Expressing reset locally in equations *)
|
188
|
let eqs_r' =
|
189
|
let all_eqs =
|
190
|
List.map (fun eq -> Eq eq) eqs' @ List.map (fun aut -> Aut aut) auts'
|
191
|
in
|
192
|
match reset with
|
193
|
| None ->
|
194
|
all_eqs
|
195
|
| Some cond ->
|
196
|
assert (auts' = []);
|
197
|
(* TODO: we do not handle properly automaton in case of reset call *)
|
198
|
List.map (fun eq -> Eq (add_eq_reset_cond cond eq)) eqs'
|
199
|
in
|
200
|
let assign_inputs =
|
201
|
Eq
|
202
|
(mkeq loc
|
203
|
( List.map (fun v -> v.var_id) inputs',
|
204
|
expr_of_expr_list args.expr_loc (List.map snd dynamic_inputs) ))
|
205
|
in
|
206
|
let expr = expr_of_expr_list loc (List.map expr_of_vdecl outputs') in
|
207
|
let asserts' =
|
208
|
(* We rename variables in assert expressions *)
|
209
|
List.map
|
210
|
(fun a ->
|
211
|
{
|
212
|
a with
|
213
|
assert_expr =
|
214
|
(let expr = a.assert_expr in
|
215
|
rename_expr (fun x -> x) rename expr);
|
216
|
})
|
217
|
node.node_asserts
|
218
|
in
|
219
|
let annots' = Plugins.inline_annots rename node.node_annot in
|
220
|
( expr,
|
221
|
inputs' @ outputs' @ locals' @ locals,
|
222
|
assign_inputs :: eqs_r',
|
223
|
asserts',
|
224
|
annots' )
|
225
|
|
226
|
let inline_table = Hashtbl.create 23
|
227
|
|
228
|
(* new_expr, new_locals, new_eqs = inline_expr expr locals node nodes
|
229
|
|
230
|
Each occurence of a node in nodes in the expr should be replaced by fresh
|
231
|
variables and the code of called node instance added to new_eqs *)
|
232
|
let rec inline_expr ?(selection_on_annotation = false) expr locals node nodes =
|
233
|
let inline_expr = inline_expr ~selection_on_annotation in
|
234
|
let inline_node = inline_node ~selection_on_annotation in
|
235
|
let inline_tuple el =
|
236
|
List.fold_right
|
237
|
(fun e (el_tail, locals, eqs, asserts, annots) ->
|
238
|
let e', locals', eqs', asserts', annots' =
|
239
|
inline_expr e locals node nodes
|
240
|
in
|
241
|
e' :: el_tail, locals', eqs' @ eqs, asserts @ asserts', annots @ annots')
|
242
|
el ([], locals, [], [], [])
|
243
|
in
|
244
|
let inline_pair e1 e2 =
|
245
|
let el', l', eqs', asserts', annots' = inline_tuple [ e1; e2 ] in
|
246
|
match el' with
|
247
|
| [ e1'; e2' ] ->
|
248
|
e1', e2', l', eqs', asserts', annots'
|
249
|
| _ ->
|
250
|
assert false
|
251
|
in
|
252
|
let inline_triple e1 e2 e3 =
|
253
|
let el', l', eqs', asserts', annots' = inline_tuple [ e1; e2; e3 ] in
|
254
|
match el' with
|
255
|
| [ e1'; e2'; e3' ] ->
|
256
|
e1', e2', e3', l', eqs', asserts', annots'
|
257
|
| _ ->
|
258
|
assert false
|
259
|
in
|
260
|
|
261
|
match expr.expr_desc with
|
262
|
| Expr_appl (id, args, reset) ->
|
263
|
let args', locals', eqs', asserts', annots' =
|
264
|
inline_expr args locals node nodes
|
265
|
in
|
266
|
if
|
267
|
List.exists (check_node_name id) nodes
|
268
|
&& (* the current node call is provided as arguments nodes *)
|
269
|
((not selection_on_annotation) || is_inline_expr expr)
|
270
|
(* and if selection on annotation is activated, it is explicitely inlined
|
271
|
here *)
|
272
|
then
|
273
|
(* Format.eprintf "Inlining call to %s in expression %a@." id
|
274
|
Printers.pp_expr expr; *)
|
275
|
(* The node should be inlined *)
|
276
|
(* let _ = Format.eprintf "Inlining call to %s@." id in *)
|
277
|
let called =
|
278
|
try List.find (check_node_name id) nodes
|
279
|
with Not_found -> assert false
|
280
|
in
|
281
|
let called = node_of_top called in
|
282
|
let called' = inline_node called nodes in
|
283
|
let expr, locals', eqs'', asserts'', annots'' =
|
284
|
inline_call called' expr.expr_loc expr.expr_tag args' reset locals' node
|
285
|
in
|
286
|
expr, locals', eqs' @ eqs'', asserts' @ asserts'', annots' @ annots''
|
287
|
else
|
288
|
(* let _ = Format.eprintf "Not inlining call to %s@." id in *)
|
289
|
( { expr with expr_desc = Expr_appl (id, args', reset) },
|
290
|
locals',
|
291
|
eqs',
|
292
|
asserts',
|
293
|
annots' )
|
294
|
(* For other cases, we just keep the structure, but convert sub-expressions *)
|
295
|
| Expr_const _ | Expr_ident _ ->
|
296
|
expr, locals, [], [], []
|
297
|
| Expr_tuple el ->
|
298
|
let el', l', eqs', asserts', annots' = inline_tuple el in
|
299
|
{ expr with expr_desc = Expr_tuple el' }, l', eqs', asserts', annots'
|
300
|
| Expr_ite (g, t, e) ->
|
301
|
let g', t', e', l', eqs', asserts', annots' = inline_triple g t e in
|
302
|
{ expr with expr_desc = Expr_ite (g', t', e') }, l', eqs', asserts', annots'
|
303
|
| Expr_arrow (e1, e2) ->
|
304
|
let e1', e2', l', eqs', asserts', annots' = inline_pair e1 e2 in
|
305
|
{ expr with expr_desc = Expr_arrow (e1', e2') }, l', eqs', asserts', annots'
|
306
|
| Expr_fby (e1, e2) ->
|
307
|
let e1', e2', l', eqs', asserts', annots' = inline_pair e1 e2 in
|
308
|
{ expr with expr_desc = Expr_fby (e1', e2') }, l', eqs', asserts', annots'
|
309
|
| Expr_array el ->
|
310
|
let el', l', eqs', asserts', annots' = inline_tuple el in
|
311
|
{ expr with expr_desc = Expr_array el' }, l', eqs', asserts', annots'
|
312
|
| Expr_access (e, dim) ->
|
313
|
let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in
|
314
|
{ expr with expr_desc = Expr_access (e', dim) }, l', eqs', asserts', annots'
|
315
|
| Expr_power (e, dim) ->
|
316
|
let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in
|
317
|
{ expr with expr_desc = Expr_power (e', dim) }, l', eqs', asserts', annots'
|
318
|
| Expr_pre e ->
|
319
|
let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in
|
320
|
{ expr with expr_desc = Expr_pre e' }, l', eqs', asserts', annots'
|
321
|
| Expr_when (e, id, label) ->
|
322
|
let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in
|
323
|
( { expr with expr_desc = Expr_when (e', id, label) },
|
324
|
l',
|
325
|
eqs',
|
326
|
asserts',
|
327
|
annots' )
|
328
|
| Expr_merge (id, branches) ->
|
329
|
let el, l', eqs', asserts', annots' =
|
330
|
inline_tuple (List.map snd branches)
|
331
|
in
|
332
|
let branches' = List.map2 (fun (label, _) v -> label, v) branches el in
|
333
|
( { expr with expr_desc = Expr_merge (id, branches') },
|
334
|
l',
|
335
|
eqs',
|
336
|
asserts',
|
337
|
annots' )
|
338
|
|
339
|
and inline_node ?(selection_on_annotation = false) node nodes =
|
340
|
try copy_node (Hashtbl.find inline_table node.node_id)
|
341
|
with Not_found ->
|
342
|
let inline_expr = inline_expr ~selection_on_annotation in
|
343
|
let eqs, auts = get_node_eqs node in
|
344
|
assert (auts = []);
|
345
|
(* No inlining of automaton yet. One should visit each handler eqs and
|
346
|
perform similar computation *)
|
347
|
let new_locals, stmts, asserts, annots =
|
348
|
List.fold_left
|
349
|
(fun (locals, stmts, asserts, annots) eq ->
|
350
|
let eq_rhs', locals', new_stmts', asserts', annots' =
|
351
|
inline_expr eq.eq_rhs locals node nodes
|
352
|
in
|
353
|
( locals',
|
354
|
Eq { eq with eq_rhs = eq_rhs' } :: new_stmts' @ stmts,
|
355
|
asserts' @ asserts,
|
356
|
annots' @ annots ))
|
357
|
(node.node_locals, [], node.node_asserts, node.node_annot)
|
358
|
eqs
|
359
|
in
|
360
|
let inlined =
|
361
|
{
|
362
|
node with
|
363
|
node_locals = new_locals;
|
364
|
node_stmts = stmts;
|
365
|
node_asserts = asserts;
|
366
|
node_annot = annots;
|
367
|
}
|
368
|
in
|
369
|
(*Format.eprintf "inline node:<< %a@.>>@." Printers.pp_node inlined;*)
|
370
|
Hashtbl.add inline_table node.node_id inlined;
|
371
|
inlined
|
372
|
|
373
|
let inline_all_calls node nodes =
|
374
|
let nd = match node.top_decl_desc with Node nd -> nd | _ -> assert false in
|
375
|
{ node with top_decl_desc = Node (inline_node nd nodes) }
|
376
|
|
377
|
let witness filename main_name orig inlined (* type_env clock_env *) =
|
378
|
let loc = Location.dummy_loc in
|
379
|
let rename_local_node nodes prefix id =
|
380
|
if List.exists (check_node_name id) nodes then prefix ^ id else id
|
381
|
in
|
382
|
let main_orig_node =
|
383
|
match (List.find (check_node_name main_name) orig).top_decl_desc with
|
384
|
| Node nd ->
|
385
|
nd
|
386
|
| _ ->
|
387
|
assert false
|
388
|
in
|
389
|
|
390
|
let orig_rename = rename_local_node orig "orig_" in
|
391
|
let inlined_rename = rename_local_node inlined "inlined_" in
|
392
|
let identity x = x in
|
393
|
let is_node top =
|
394
|
match top.top_decl_desc with Node _ -> true | _ -> false
|
395
|
in
|
396
|
let orig =
|
397
|
rename_prog orig_rename (* f_node *) identity (* f_var *) identity
|
398
|
(* f_const *) orig
|
399
|
in
|
400
|
let inlined = rename_prog inlined_rename identity identity inlined in
|
401
|
let nodes_origs, others = List.partition is_node orig in
|
402
|
let nodes_inlined, _ = List.partition is_node inlined in
|
403
|
|
404
|
(* One ok_i boolean variable per output var *)
|
405
|
let nb_outputs = List.length main_orig_node.node_outputs in
|
406
|
let ok_ident = "OK" in
|
407
|
let ok_i =
|
408
|
List.map
|
409
|
(fun id ->
|
410
|
mkvar_decl loc
|
411
|
( Format.sprintf "%s_%i" ok_ident id,
|
412
|
{ ty_dec_desc = Tydec_bool; ty_dec_loc = loc },
|
413
|
{ ck_dec_desc = Ckdec_any; ck_dec_loc = loc },
|
414
|
false,
|
415
|
None,
|
416
|
None ))
|
417
|
(Utils.enumerate nb_outputs)
|
418
|
in
|
419
|
|
420
|
(* OK = ok_1 and ok_2 and ... ok_n-1 *)
|
421
|
let ok_output =
|
422
|
mkvar_decl loc
|
423
|
( ok_ident,
|
424
|
{ ty_dec_desc = Tydec_bool; ty_dec_loc = loc },
|
425
|
{ ck_dec_desc = Ckdec_any; ck_dec_loc = loc },
|
426
|
false,
|
427
|
None,
|
428
|
None )
|
429
|
in
|
430
|
let main_ok_expr =
|
431
|
let mkv x = mkexpr loc (Expr_ident x) in
|
432
|
match ok_i with
|
433
|
| [] ->
|
434
|
assert false
|
435
|
| [ x ] ->
|
436
|
mkv x.var_id
|
437
|
| hd :: tl ->
|
438
|
List.fold_left
|
439
|
(fun accu elem -> mkpredef_call loc "&&" [ mkv elem.var_id; accu ])
|
440
|
(mkv hd.var_id) tl
|
441
|
in
|
442
|
|
443
|
(* Building main node *)
|
444
|
let ok_i_eq =
|
445
|
{
|
446
|
eq_loc = loc;
|
447
|
eq_lhs = List.map (fun v -> v.var_id) ok_i;
|
448
|
eq_rhs =
|
449
|
(let inputs =
|
450
|
expr_of_expr_list loc
|
451
|
(List.map
|
452
|
(fun v -> mkexpr loc (Expr_ident v.var_id))
|
453
|
main_orig_node.node_inputs)
|
454
|
in
|
455
|
let call_orig =
|
456
|
mkexpr loc (Expr_appl ("orig_" ^ main_name, inputs, None))
|
457
|
in
|
458
|
let call_inlined =
|
459
|
mkexpr loc (Expr_appl ("inlined_" ^ main_name, inputs, None))
|
460
|
in
|
461
|
let args = mkexpr loc (Expr_tuple [ call_orig; call_inlined ]) in
|
462
|
mkexpr loc (Expr_appl ("=", args, None)));
|
463
|
}
|
464
|
in
|
465
|
let ok_eq = { eq_loc = loc; eq_lhs = [ ok_ident ]; eq_rhs = main_ok_expr } in
|
466
|
let main_node =
|
467
|
{
|
468
|
node_id = "check";
|
469
|
node_type = Types.new_var ();
|
470
|
node_clock = Clocks.new_var true;
|
471
|
node_inputs = main_orig_node.node_inputs;
|
472
|
node_outputs = [ ok_output ];
|
473
|
node_locals = ok_i;
|
474
|
node_gencalls = [];
|
475
|
node_checks = [];
|
476
|
node_asserts = [];
|
477
|
node_stmts = [ Eq ok_i_eq; Eq ok_eq ];
|
478
|
node_dec_stateless = false;
|
479
|
node_stateless = None;
|
480
|
node_spec =
|
481
|
Some
|
482
|
(Contract
|
483
|
(mk_contract_guarantees None
|
484
|
(mkeexpr loc (mkexpr loc (Expr_ident ok_ident)))));
|
485
|
node_annot = [];
|
486
|
node_iscontract = true;
|
487
|
}
|
488
|
in
|
489
|
let main =
|
490
|
[
|
491
|
{
|
492
|
top_decl_desc = Node main_node;
|
493
|
top_decl_loc = loc;
|
494
|
top_decl_owner = filename;
|
495
|
top_decl_itf = false;
|
496
|
};
|
497
|
]
|
498
|
in
|
499
|
let new_prog = others @ nodes_origs @ nodes_inlined @ main in
|
500
|
|
501
|
(* let _ = Typing.type_prog type_env new_prog in let _ =
|
502
|
Clock_calculus.clock_prog clock_env new_prog in *)
|
503
|
let witness_file =
|
504
|
Options_management.get_witness_dir filename ^ "/" ^ "inliner_witness.lus"
|
505
|
in
|
506
|
let witness_out = open_out witness_file in
|
507
|
let witness_fmt = Format.formatter_of_out_channel witness_out in
|
508
|
List.iter
|
509
|
(fun vdecl ->
|
510
|
Typing.try_unify Type_predef.type_bool vdecl.var_type vdecl.var_loc)
|
511
|
(ok_output :: ok_i);
|
512
|
Format.fprintf witness_fmt
|
513
|
"(* Generated lustre file to check validity of inlining process *)@.";
|
514
|
Printers.pp_prog witness_fmt new_prog;
|
515
|
Format.fprintf witness_fmt "@.";
|
516
|
()
|
517
|
(* xx *)
|
518
|
|
519
|
let global_inline prog (*type_env clock_env*) =
|
520
|
(* We select the main node desc *)
|
521
|
let main_node, other_nodes, _ =
|
522
|
List.fold_right
|
523
|
(fun top (main_opt, nodes, others) ->
|
524
|
match top.top_decl_desc with
|
525
|
| Node nd when nd.node_id = !Options.main_node ->
|
526
|
Some top, nodes, others
|
527
|
| Node _ ->
|
528
|
main_opt, top :: nodes, others
|
529
|
| _ ->
|
530
|
main_opt, nodes, top :: others)
|
531
|
prog (None, [], [])
|
532
|
in
|
533
|
|
534
|
(* Recursively each call of a node in the top node is replaced *)
|
535
|
let main_node = Utils.desome main_node in
|
536
|
let main_node' = inline_all_calls main_node other_nodes in
|
537
|
let res =
|
538
|
List.map
|
539
|
(fun top ->
|
540
|
if check_node_name !Options.main_node top then main_node' else top)
|
541
|
prog
|
542
|
in
|
543
|
(* Code snippet from unstable branch. May be used when reactivating witnesses.
|
544
|
let res = main_node'::other_tops in if !Options.witnesses then ( witness
|
545
|
basename (match main_node.top_decl_desc with Node nd -> nd.node_id | _ ->
|
546
|
assert false) prog res type_env clock_env ); *)
|
547
|
res
|
548
|
|
549
|
let pp_inline_calls fmt prog =
|
550
|
let local_anns = Annotations.get_expr_annotations keyword in
|
551
|
let nodes_with_anns =
|
552
|
List.fold_left (fun accu (k, _) -> ISet.add k accu) ISet.empty local_anns
|
553
|
in
|
554
|
Format.fprintf fmt "@[<v 0>Inlined expresssions in node (by tags):@ %a@]"
|
555
|
(fprintf_list ~sep:"" (fun fmt top ->
|
556
|
match top.top_decl_desc with
|
557
|
| Node nd when ISet.mem nd.node_id nodes_with_anns ->
|
558
|
Format.fprintf fmt "%s: {@[<v 0>%a}@]@ " nd.node_id
|
559
|
(fprintf_list ~sep:"@ " (fun fmt tag ->
|
560
|
Format.fprintf fmt "%i" tag))
|
561
|
(List.fold_left
|
562
|
(fun accu (id, tag) ->
|
563
|
if id = nd.node_id then tag :: accu else accu)
|
564
|
[] local_anns)
|
565
|
(* | Node nd -> Format.fprintf fmt "%s: no inline annotations"
|
566
|
nd.node_id *)
|
567
|
| _ ->
|
568
|
()))
|
569
|
prog
|
570
|
|
571
|
let local_inline prog (* type_env clock_env *) =
|
572
|
Log.report ~level:2 (fun fmt -> Format.fprintf fmt ".. @[<v 2>Inlining@,");
|
573
|
let local_anns = Annotations.get_expr_annotations keyword in
|
574
|
let prog =
|
575
|
if local_anns != [] then (
|
576
|
let nodes_with_anns =
|
577
|
List.fold_left
|
578
|
(fun accu (k, _) -> ISet.add k accu)
|
579
|
ISet.empty local_anns
|
580
|
in
|
581
|
ISet.iter
|
582
|
(fun node_id ->
|
583
|
Log.report ~level:2 (fun fmt ->
|
584
|
Format.fprintf fmt "Node %s has local expression annotations@ "
|
585
|
node_id))
|
586
|
nodes_with_anns;
|
587
|
List.fold_right
|
588
|
(fun top accu ->
|
589
|
(match top.top_decl_desc with
|
590
|
| Node nd when ISet.mem nd.node_id nodes_with_anns ->
|
591
|
Log.report ~level:2 (fun fmt ->
|
592
|
Format.fprintf fmt "[local inline] Processing node %s@ "
|
593
|
nd.node_id);
|
594
|
let inlined_node =
|
595
|
inline_node ~selection_on_annotation:true nd prog
|
596
|
in
|
597
|
(* Format.eprintf "Before inline@.%a@.After:@.%a@." *)
|
598
|
(* Printers.pp_node nd *)
|
599
|
(* Printers.pp_node inlined_node; *)
|
600
|
{ top with top_decl_desc = Node inlined_node }
|
601
|
| _ ->
|
602
|
top)
|
603
|
:: accu)
|
604
|
prog [])
|
605
|
else (
|
606
|
Log.report ~level:2 (fun fmt ->
|
607
|
Format.fprintf fmt "No local inline information!@ ");
|
608
|
prog)
|
609
|
in
|
610
|
Log.report ~level:2 (fun fmt -> Format.fprintf fmt "@]@,");
|
611
|
prog
|
612
|
|
613
|
(* Local Variables: *)
|
614
|
(* compile-command:"make -C .." *)
|
615
|
(* End: *)
|