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 Utils
|
14
|
open Format
|
15
|
|
16
|
let kind2_language_cst = [ "initial" ]
|
17
|
|
18
|
let kind2_protect id =
|
19
|
if List.mem id kind2_language_cst then "_KIND2_PROTECT_" ^ id else id
|
20
|
|
21
|
(* XXX: UNUSED *)
|
22
|
(* Prints [v] as [pp_fun] would do, but adds a backslash at each end of line,
|
23
|
following the C convention for multiple lines macro *)
|
24
|
(* let pp_as_c_macro pp_fun fmt v =
|
25
|
* let formatter_out_funs = pp_get_formatter_out_functions fmt () in
|
26
|
* let macro_newline () =
|
27
|
* formatter_out_funs.out_string "\\" 0 1;
|
28
|
* formatter_out_funs.out_newline ()
|
29
|
* in
|
30
|
* pp_set_formatter_out_functions fmt
|
31
|
* { formatter_out_funs with out_newline = macro_newline };
|
32
|
* pp_fun fmt v;
|
33
|
* pp_set_formatter_out_functions fmt formatter_out_funs *)
|
34
|
|
35
|
let rec pp_var_struct_type_field fmt (label, tdesc) =
|
36
|
fprintf fmt "%a : %a;" pp_print_string label pp_var_type_dec_desc tdesc
|
37
|
|
38
|
and pp_var_type_dec_desc fmt tdesc =
|
39
|
match tdesc with
|
40
|
| Tydec_any ->
|
41
|
fprintf fmt "<any>"
|
42
|
| Tydec_int ->
|
43
|
fprintf fmt "int"
|
44
|
| Tydec_real ->
|
45
|
fprintf fmt "real"
|
46
|
(* | Tydec_float -> fprintf fmt "float" *)
|
47
|
| Tydec_bool ->
|
48
|
fprintf fmt "bool"
|
49
|
| Tydec_clock t ->
|
50
|
fprintf fmt "%a clock" pp_var_type_dec_desc t
|
51
|
| Tydec_const t ->
|
52
|
fprintf fmt "%s" t
|
53
|
| Tydec_enum id_list ->
|
54
|
fprintf fmt "enum {%a }" (pp_comma_list pp_print_string) id_list
|
55
|
| Tydec_struct f_list ->
|
56
|
fprintf fmt "struct {%a }" (pp_print_list pp_var_struct_type_field) f_list
|
57
|
| Tydec_array (s, t) ->
|
58
|
fprintf fmt "%a^%a" pp_var_type_dec_desc t Dimension.pp s
|
59
|
|
60
|
let pp_var_type_dec fmt ty = pp_var_type_dec_desc fmt ty.ty_dec_desc
|
61
|
|
62
|
let pp_var_name fmt id =
|
63
|
fprintf
|
64
|
fmt
|
65
|
"%s"
|
66
|
(if !Options.kind2_print then kind2_protect id.var_id else id.var_id)
|
67
|
|
68
|
let pp_var_type fmt id =
|
69
|
if !Options.print_dec_types then pp_var_type_dec fmt id.var_dec_type
|
70
|
else Types.pp_node_ty fmt id.var_type
|
71
|
|
72
|
let pp_var_clock fmt id = Clocks.pp_suffix fmt id.var_clock
|
73
|
|
74
|
let pp_eq_lhs = pp_comma_list pp_print_string
|
75
|
|
76
|
let pp_var fmt id =
|
77
|
fprintf
|
78
|
fmt
|
79
|
"%s%s: %a"
|
80
|
(if id.var_dec_const then "const " else "")
|
81
|
(if !Options.kind2_print then kind2_protect id.var_id else id.var_id)
|
82
|
pp_var_type
|
83
|
id
|
84
|
|
85
|
let pp_vars fmt vars = pp_print_list ~pp_sep:pp_print_semicolon pp_var fmt vars
|
86
|
|
87
|
let pp_quantifiers fmt (q, vars) =
|
88
|
match q with
|
89
|
| Forall ->
|
90
|
fprintf fmt "forall %a" pp_vars vars
|
91
|
| Exists ->
|
92
|
fprintf fmt "exists %a" pp_vars vars
|
93
|
|
94
|
let rec pp_struct_const_field fmt (label, c) =
|
95
|
fprintf fmt "%a = %a;" pp_print_string label pp_const c
|
96
|
|
97
|
and pp_const fmt c =
|
98
|
match c with
|
99
|
| Const_int i ->
|
100
|
pp_print_int fmt i
|
101
|
| Const_real r ->
|
102
|
Real.pp fmt r
|
103
|
(*if e = 0 then pp_print_int fmt c else if e < 0 then Format.fprintf fmt
|
104
|
"%ie%i" c (-e) else Format.fprintf fmt "%ie-%i" c e *)
|
105
|
(* | Const_float r -> pp_print_float fmt r *)
|
106
|
| Const_tag t ->
|
107
|
pp_print_string fmt t
|
108
|
| Const_array ca ->
|
109
|
fprintf
|
110
|
fmt
|
111
|
"[%a]"
|
112
|
(pp_print_list ~pp_sep:(fun fmt () -> pp_print_string fmt ",") pp_const)
|
113
|
ca
|
114
|
| Const_struct fl ->
|
115
|
fprintf fmt "{%a }" (pp_print_list pp_struct_const_field) fl
|
116
|
(* used only for annotations *)
|
117
|
| Const_string s ->
|
118
|
pp_print_string fmt ("\"" ^ s ^ "\"")
|
119
|
| Const_modeid s ->
|
120
|
pp_print_string fmt ("\"" ^ s ^ "\"")
|
121
|
|
122
|
let pp_annot_key fmt kwds =
|
123
|
match kwds with
|
124
|
| [] ->
|
125
|
assert false
|
126
|
| [ x ] ->
|
127
|
pp_print_string fmt x
|
128
|
| _ ->
|
129
|
fprintf
|
130
|
fmt
|
131
|
"/%a/"
|
132
|
(pp_print_list
|
133
|
~pp_sep:(fun fmt () -> pp_print_string fmt "/")
|
134
|
pp_print_string)
|
135
|
kwds
|
136
|
|
137
|
let pp_kind2_when fmt (id, l) =
|
138
|
if l = "true" then fprintf fmt "%s" id
|
139
|
else if l = "false" then fprintf fmt "not(%s)" id
|
140
|
else fprintf fmt "(%s=%s)" l id
|
141
|
|
142
|
let rec pp_expr fmt expr =
|
143
|
(match expr.expr_annot with
|
144
|
| None ->
|
145
|
fprintf fmt "%t"
|
146
|
| Some ann ->
|
147
|
fprintf fmt "@[(%a %t)@]" pp_expr_annot ann)
|
148
|
(fun fmt ->
|
149
|
let pp fmt =
|
150
|
match expr.expr_desc with
|
151
|
| Expr_const c ->
|
152
|
pp_const fmt c
|
153
|
| Expr_ident id ->
|
154
|
fprintf
|
155
|
fmt
|
156
|
"%s"
|
157
|
(if !Options.kind2_print then kind2_protect id else id)
|
158
|
| Expr_array a ->
|
159
|
fprintf fmt "[%a]" pp_tuple a
|
160
|
| Expr_access (a, d) ->
|
161
|
fprintf fmt "%a[%a]" pp_expr a Dimension.pp d
|
162
|
| Expr_power (a, d) ->
|
163
|
fprintf fmt "(%a^%a)" pp_expr a Dimension.pp d
|
164
|
| Expr_tuple el ->
|
165
|
fprintf fmt "(%a)" pp_tuple el
|
166
|
| Expr_ite (c, t, e) ->
|
167
|
fprintf
|
168
|
fmt
|
169
|
"@[<hov 1>(if %a then@ @[<hov 2>%a@]@ else@ @[<hov 2>%a@]@])"
|
170
|
pp_expr
|
171
|
c
|
172
|
pp_expr
|
173
|
t
|
174
|
pp_expr
|
175
|
e
|
176
|
| Expr_arrow (e1, e2) ->
|
177
|
fprintf fmt "(%a -> %a)" pp_expr e1 pp_expr e2
|
178
|
| Expr_fby (e1, e2) ->
|
179
|
fprintf fmt "%a fby %a" pp_expr e1 pp_expr e2
|
180
|
| Expr_pre e ->
|
181
|
fprintf fmt "pre %a" pp_expr e
|
182
|
| Expr_when (e, id, l) ->
|
183
|
if !Options.kind2_print then
|
184
|
fprintf fmt "%a when %a" pp_expr e pp_kind2_when (l, id)
|
185
|
else fprintf fmt "%a when %s(%s)" pp_expr e l id
|
186
|
| Expr_merge (id, hl) ->
|
187
|
fprintf fmt "merge %s %a" id pp_handlers hl
|
188
|
| Expr_appl (id, e, r) ->
|
189
|
pp_app fmt id e r
|
190
|
in
|
191
|
if false (* extra debug *) then
|
192
|
Format.fprintf fmt "%t: %a" pp Types.pp expr.expr_type
|
193
|
else pp fmt)
|
194
|
|
195
|
and pp_tuple fmt el =
|
196
|
pp_print_list ~pp_sep:(fun fmt () -> pp_print_string fmt ",") pp_expr fmt el
|
197
|
|
198
|
and pp_handler fmt (t, h) = fprintf fmt "(%s -> %a)" t pp_expr h
|
199
|
|
200
|
and pp_handlers fmt hl = pp_print_list pp_handler fmt hl
|
201
|
|
202
|
and pp_app fmt id e r =
|
203
|
if !Options.kind2_print && not (List.mem id Basic_library.internal_funs) then
|
204
|
(* We only translate calls to nodes in kind2. The other may be rejected by
|
205
|
Kind2 *)
|
206
|
(* Small local function to extract the first layer of when constructs *)
|
207
|
let rec un_when_ed_expr e =
|
208
|
match e.expr_desc with
|
209
|
| Expr_when (e, i, l) ->
|
210
|
Some (i, l), e
|
211
|
| Expr_tuple el -> (
|
212
|
let un_when_ed_el = List.map un_when_ed_expr el in
|
213
|
if List.length un_when_ed_el < 1 then assert false;
|
214
|
(* tuple should have at least one element*)
|
215
|
let init_when = fst (List.hd un_when_ed_el) in
|
216
|
let common_when =
|
217
|
List.fold_left
|
218
|
(fun accu (new_opt, _) ->
|
219
|
match accu, new_opt with
|
220
|
| Some c1, Some c2 ->
|
221
|
if c1 = c2 then Some c1
|
222
|
else assert false (* should not be clocked *)
|
223
|
| None, None ->
|
224
|
None
|
225
|
| _ ->
|
226
|
assert false
|
227
|
(* If this is not even, there should be a clocking problem*))
|
228
|
init_when
|
229
|
(List.tl un_when_ed_el)
|
230
|
in
|
231
|
match common_when with
|
232
|
| None ->
|
233
|
None, e
|
234
|
| Some _ ->
|
235
|
( common_when,
|
236
|
{ e with expr_desc = Expr_tuple (List.map snd un_when_ed_el) } ))
|
237
|
| _ ->
|
238
|
None, e
|
239
|
in
|
240
|
let when_expr, _ = un_when_ed_expr e in
|
241
|
match r, when_expr with
|
242
|
| None, None ->
|
243
|
pp_call fmt id e
|
244
|
| None, Some w ->
|
245
|
fprintf fmt "(activate %s every (%a)) (%a)" id pp_kind2_when w pp_expr e
|
246
|
| Some r, None ->
|
247
|
fprintf fmt "(restart %s every (%a)) (%a)" id pp_expr r pp_expr e
|
248
|
| Some r, Some w ->
|
249
|
fprintf
|
250
|
fmt
|
251
|
"(activate %s every (%a) restart every (%a)) (%a)"
|
252
|
id
|
253
|
pp_kind2_when
|
254
|
w
|
255
|
pp_expr
|
256
|
r
|
257
|
pp_expr
|
258
|
e
|
259
|
else
|
260
|
match r with
|
261
|
| None ->
|
262
|
pp_call fmt id e
|
263
|
| Some c ->
|
264
|
fprintf fmt "%t every (%a)" (fun fmt -> pp_call fmt id e) pp_expr c
|
265
|
|
266
|
and pp_call fmt id e =
|
267
|
match id, e.expr_desc with
|
268
|
| "+", Expr_tuple [ e1; e2 ] ->
|
269
|
fprintf fmt "(%a + %a)" pp_expr e1 pp_expr e2
|
270
|
| "uminus", _ ->
|
271
|
fprintf fmt "(- %a)" pp_expr e
|
272
|
| "-", Expr_tuple [ e1; e2 ] ->
|
273
|
fprintf fmt "(%a - %a)" pp_expr e1 pp_expr e2
|
274
|
| "*", Expr_tuple [ e1; e2 ] ->
|
275
|
fprintf fmt "(%a * %a)" pp_expr e1 pp_expr e2
|
276
|
| "/", Expr_tuple [ e1; e2 ] ->
|
277
|
fprintf fmt "(%a / %a)" pp_expr e1 pp_expr e2
|
278
|
| "mod", Expr_tuple [ e1; e2 ] ->
|
279
|
fprintf fmt "(%a mod %a)" pp_expr e1 pp_expr e2
|
280
|
| "&&", Expr_tuple [ e1; e2 ] ->
|
281
|
fprintf fmt "(%a and %a)" pp_expr e1 pp_expr e2
|
282
|
| "||", Expr_tuple [ e1; e2 ] ->
|
283
|
fprintf fmt "(%a or %a)" pp_expr e1 pp_expr e2
|
284
|
| "xor", Expr_tuple [ e1; e2 ] ->
|
285
|
fprintf fmt "(%a xor %a)" pp_expr e1 pp_expr e2
|
286
|
| "impl", Expr_tuple [ e1; e2 ] ->
|
287
|
fprintf fmt "(%a => %a)" pp_expr e1 pp_expr e2
|
288
|
| "<", Expr_tuple [ e1; e2 ] ->
|
289
|
fprintf fmt "(%a < %a)" pp_expr e1 pp_expr e2
|
290
|
| "<=", Expr_tuple [ e1; e2 ] ->
|
291
|
fprintf fmt "(%a <= %a)" pp_expr e1 pp_expr e2
|
292
|
| ">", Expr_tuple [ e1; e2 ] ->
|
293
|
fprintf fmt "(%a > %a)" pp_expr e1 pp_expr e2
|
294
|
| ">=", Expr_tuple [ e1; e2 ] ->
|
295
|
fprintf fmt "(%a >= %a)" pp_expr e1 pp_expr e2
|
296
|
| "!=", Expr_tuple [ e1; e2 ] ->
|
297
|
fprintf fmt "(%a <> %a)" pp_expr e1 pp_expr e2
|
298
|
| "=", Expr_tuple [ e1; e2 ] ->
|
299
|
fprintf fmt "(%a = %a)" pp_expr e1 pp_expr e2
|
300
|
| "not", _ ->
|
301
|
fprintf fmt "(not %a)" pp_expr e
|
302
|
| _, Expr_tuple _ ->
|
303
|
fprintf fmt "%s %a" id pp_expr e
|
304
|
| _ ->
|
305
|
fprintf fmt "%s (%a)" id pp_expr e
|
306
|
|
307
|
and pp_eexpr fmt e =
|
308
|
fprintf
|
309
|
fmt
|
310
|
"%a%t %a"
|
311
|
(pp_print_list ~pp_sep:pp_print_semicolon pp_quantifiers)
|
312
|
e.eexpr_quantifiers
|
313
|
(fun fmt ->
|
314
|
match e.eexpr_quantifiers with [] -> () | _ -> fprintf fmt ";")
|
315
|
pp_expr
|
316
|
e.eexpr_qfexpr
|
317
|
|
318
|
and pp_sf_value fmt e =
|
319
|
fprintf
|
320
|
fmt
|
321
|
"%a"
|
322
|
(* (Utils.fprintf_list ~sep:"; " pp_quantifiers) e.eexpr_quantifiers *)
|
323
|
(* (fun fmt -> match e.eexpr_quantifiers *)
|
324
|
(* with [] -> () *)
|
325
|
(* | _ -> fprintf fmt ";") *)
|
326
|
pp_expr
|
327
|
e.eexpr_qfexpr
|
328
|
|
329
|
and pp_s_function fmt expr_ann =
|
330
|
let pp_annot fmt (kwds, ee) =
|
331
|
fprintf
|
332
|
fmt
|
333
|
" %t : %a"
|
334
|
(fun fmt ->
|
335
|
match kwds with
|
336
|
| [] ->
|
337
|
assert false
|
338
|
| [ x ] ->
|
339
|
pp_print_string fmt x
|
340
|
| _ ->
|
341
|
fprintf
|
342
|
fmt
|
343
|
"%a"
|
344
|
(pp_print_list
|
345
|
~pp_sep:(fun fmt () -> pp_print_string fmt "/")
|
346
|
pp_print_string)
|
347
|
kwds)
|
348
|
pp_sf_value
|
349
|
ee
|
350
|
in
|
351
|
pp_print_list pp_annot fmt expr_ann.annots
|
352
|
|
353
|
and pp_expr_annot fmt expr_ann =
|
354
|
let pp_annot fmt (kwds, ee) =
|
355
|
fprintf fmt "(*!%a: %a; *)" pp_annot_key kwds pp_eexpr ee
|
356
|
in
|
357
|
pp_print_list pp_annot fmt expr_ann.annots
|
358
|
|
359
|
let pp_asserts fmt asserts =
|
360
|
match asserts with
|
361
|
| _ :: _ ->
|
362
|
fprintf fmt "(* Asserts definitions *)@ ";
|
363
|
pp_print_list
|
364
|
(fun fmt assert_ ->
|
365
|
let expr = assert_.assert_expr in
|
366
|
fprintf fmt "assert %a;" pp_expr expr)
|
367
|
fmt
|
368
|
asserts
|
369
|
| _ ->
|
370
|
()
|
371
|
|
372
|
(* let pp_node_var fmt id = fprintf fmt "%s%s: %a(%a)%a" (if id.var_dec_const
|
373
|
then "const " else "") id.var_id print_dec_ty id.var_dec_type.ty_dec_desc
|
374
|
Types.pp id.var_type Clocks.pp_ck_suffix id.var_clock *)
|
375
|
let pp_node_var fmt id =
|
376
|
fprintf
|
377
|
fmt
|
378
|
"%s%s: %a%a"
|
379
|
(if id.var_dec_const then "const " else "")
|
380
|
(if !Options.kind2_print then kind2_protect id.var_id else id.var_id)
|
381
|
pp_var_type
|
382
|
id
|
383
|
pp_var_clock
|
384
|
id;
|
385
|
match id.var_dec_value with
|
386
|
| None ->
|
387
|
()
|
388
|
| Some v ->
|
389
|
fprintf fmt " = %a" pp_expr v
|
390
|
|
391
|
let pp_node_args = pp_print_list ~pp_sep:pp_print_semicolon pp_node_var
|
392
|
|
393
|
let pp_node_eq fmt eq =
|
394
|
fprintf fmt "%a = %a;" pp_eq_lhs eq.eq_lhs pp_expr eq.eq_rhs
|
395
|
|
396
|
let pp_restart fmt restart =
|
397
|
fprintf fmt "%s" (if restart then "restart" else "resume")
|
398
|
|
399
|
let pp_unless fmt (_, expr, restart, st) =
|
400
|
fprintf fmt "unless %a %a %s" pp_expr expr pp_restart restart st
|
401
|
|
402
|
let pp_until fmt (_, expr, restart, st) =
|
403
|
fprintf fmt "until %a %a %s" pp_expr expr pp_restart restart st
|
404
|
|
405
|
let rec pp_handler fmt handler =
|
406
|
fprintf
|
407
|
fmt
|
408
|
"state %s:@ @[<v 2> %a%t%alet@,@[<v 2> %a@ %a@ %a@]@,tel@ %a@]"
|
409
|
handler.hand_state
|
410
|
(pp_print_list pp_unless)
|
411
|
handler.hand_unless
|
412
|
(fun fmt -> if not ([] = handler.hand_unless) then fprintf fmt "@ ")
|
413
|
(fun fmt locals ->
|
414
|
match locals with
|
415
|
| [] ->
|
416
|
()
|
417
|
| _ ->
|
418
|
fprintf
|
419
|
fmt
|
420
|
"@[<v 4>var %a@]@ "
|
421
|
(pp_print_list ~pp_sep:pp_print_semicolon pp_node_var)
|
422
|
locals)
|
423
|
handler.hand_locals
|
424
|
(pp_print_list pp_expr_annot)
|
425
|
handler.hand_annots
|
426
|
pp_node_stmts
|
427
|
handler.hand_stmts
|
428
|
pp_asserts
|
429
|
handler.hand_asserts
|
430
|
(pp_print_list pp_until)
|
431
|
handler.hand_until
|
432
|
|
433
|
and pp_node_stmt fmt stmt =
|
434
|
match stmt with Eq eq -> pp_node_eq fmt eq | Aut aut -> pp_node_aut fmt aut
|
435
|
|
436
|
and pp_node_stmts fmt stmts =
|
437
|
pp_print_list
|
438
|
~pp_open_box:pp_open_vbox0
|
439
|
~pp_sep:pp_print_cut
|
440
|
pp_node_stmt
|
441
|
fmt
|
442
|
stmts
|
443
|
|
444
|
and pp_node_aut fmt aut =
|
445
|
fprintf
|
446
|
fmt
|
447
|
"@[<v 0>automaton %s@,%a@]"
|
448
|
aut.aut_id
|
449
|
(pp_print_list pp_handler)
|
450
|
aut.aut_handlers
|
451
|
|
452
|
and pp_node_eqs fmt eqs = pp_print_list pp_node_eq fmt eqs
|
453
|
|
454
|
let pp_typedef fmt ty =
|
455
|
fprintf fmt "type %s = %a;" ty.tydef_id pp_var_type_dec_desc ty.tydef_desc
|
456
|
|
457
|
(* XXX: UNUSED *)
|
458
|
(* let pp_typedec fmt ty = fprintf fmt "type %s;" ty.tydec_id *)
|
459
|
|
460
|
(* let rec pp_var_type fmt ty = *)
|
461
|
(* fprintf fmt "%a" (match ty.tdesc with *)
|
462
|
(* | Tvar | Tarrow | Tlink | Tunivar -> assert false *)
|
463
|
(* | Tint -> pp_print_string fmt "int" *)
|
464
|
(* | Treal -> pp_print_string fmt "real" *)
|
465
|
(* | Tbool -> pp_print_string fmt "bool" *)
|
466
|
(* | Trat -> pp_print_string fmt "rat" *)
|
467
|
(* | Tclock -> pp_print_string fmt "clock" *)
|
468
|
(* | Ttuple tel -> fprintf_list ~sep:" * " pp_var_type fmt tel *)
|
469
|
(* ) *)
|
470
|
|
471
|
(* let pp_quantifiers fmt (q, vars) =
|
472
|
* match q with
|
473
|
* | Forall -> fprintf fmt "forall %a" pp_vars vars
|
474
|
* | Exists -> fprintf fmt "exists %a" (fprintf_list ~sep:"; " pp_var) vars *)
|
475
|
|
476
|
(*let pp_eexpr fmt e = fprintf fmt "%a%t %a" (Utils.fprintf_list ~sep:"; "
|
477
|
pp_quantifiers) e.eexpr_quantifiers (fun fmt -> match e.eexpr_quantifiers with
|
478
|
[] -> () | _ -> fprintf fmt ";") pp_expr e.eexpr_qfexpr *)
|
479
|
|
480
|
let pp_spec_eq fmt eq =
|
481
|
fprintf
|
482
|
fmt
|
483
|
"var %a : %a = %a;"
|
484
|
pp_eq_lhs
|
485
|
eq.eq_lhs
|
486
|
Types.pp_node_ty
|
487
|
eq.eq_rhs.expr_type
|
488
|
pp_expr
|
489
|
eq.eq_rhs
|
490
|
|
491
|
let pp_spec_stmt fmt stmt =
|
492
|
match stmt with Eq eq -> pp_spec_eq fmt eq | Aut _ -> assert false
|
493
|
(* Not supported yet *)
|
494
|
|
495
|
let pp_spec fmt spec =
|
496
|
(* const are prefixed with const in pp_var and with nothing for regular
|
497
|
variables. We adapt the call to produce the appropriate output. *)
|
498
|
fprintf fmt "@[<v>%a%a%a%a%a%a@]"
|
499
|
(pp_print_list
|
500
|
(fun fmt v ->
|
501
|
fprintf fmt "%a = %t;" pp_var v (fun fmt ->
|
502
|
match v.var_dec_value with
|
503
|
| None ->
|
504
|
assert false
|
505
|
| Some e ->
|
506
|
pp_expr fmt e)))
|
507
|
spec.consts
|
508
|
|
509
|
(pp_print_list ~pp_prologue:pp_print_cut pp_spec_stmt) spec.stmts
|
510
|
|
511
|
(pp_print_list ~pp_prologue:pp_print_cut (fun fmt -> fprintf fmt "assume %a;" pp_eexpr))
|
512
|
spec.assume
|
513
|
|
514
|
(pp_print_list ~pp_prologue:pp_print_cut (fun fmt -> fprintf fmt "guarantee %a;" pp_eexpr))
|
515
|
spec.guarantees
|
516
|
|
517
|
(pp_print_list ~pp_prologue:pp_print_cut
|
518
|
(fun fmt mode ->
|
519
|
fprintf
|
520
|
fmt
|
521
|
"mode %s (@[<v 0>%a@ %a@]);"
|
522
|
mode.mode_id
|
523
|
(pp_print_list (fun fmt r -> fprintf fmt "require %a;" pp_eexpr r))
|
524
|
mode.require
|
525
|
(pp_print_list (fun fmt r -> fprintf fmt "ensure %a;" pp_eexpr r))
|
526
|
mode.ensure))
|
527
|
spec.modes
|
528
|
|
529
|
(pp_print_list ~pp_prologue:pp_print_cut
|
530
|
(fun fmt import ->
|
531
|
fprintf
|
532
|
fmt
|
533
|
"import %s (%a) returns (%a);"
|
534
|
import.import_nodeid
|
535
|
pp_expr
|
536
|
import.inputs
|
537
|
pp_expr
|
538
|
import.outputs))
|
539
|
spec.imports
|
540
|
|
541
|
(* Project the contract node as a pure contract: local memories are pushed back
|
542
|
in the contract definition. Should mainly be used to print it *)
|
543
|
let node_as_contract nd =
|
544
|
match nd.node_spec with
|
545
|
| None | Some (NodeSpec _) ->
|
546
|
raise (Invalid_argument "Not a contract")
|
547
|
| Some (Contract c) ->
|
548
|
(* While a processed contract shall have no locals, sttms nor consts, an
|
549
|
unprocessed one could. So we conservatively merge elements, to enable
|
550
|
printing unprocessed contracts *)
|
551
|
let consts, locals =
|
552
|
List.partition (fun v -> v.var_dec_const) nd.node_locals
|
553
|
in
|
554
|
{
|
555
|
c with
|
556
|
consts = consts @ c.consts;
|
557
|
locals = locals @ c.locals;
|
558
|
stmts = nd.node_stmts @ c.stmts;
|
559
|
}
|
560
|
|
561
|
(* Printing top contract as comments in regular output and as contract in kind2 *)
|
562
|
let pp_contract fmt nd =
|
563
|
let c = node_as_contract nd in
|
564
|
fprintf
|
565
|
fmt
|
566
|
"@[<v 2>%scontract %s(%a) returns (%a);@ "
|
567
|
(if !Options.kind2_print then "" else "(*@")
|
568
|
nd.node_id
|
569
|
pp_node_args
|
570
|
nd.node_inputs
|
571
|
pp_node_args
|
572
|
nd.node_outputs;
|
573
|
fprintf fmt "@[<v 2>let@ ";
|
574
|
pp_spec fmt c;
|
575
|
fprintf fmt "@]@ tel@ @]%s@ " (if !Options.kind2_print then "" else "*)")
|
576
|
|
577
|
let pp_spec_as_comment fmt (inl, outl, spec) =
|
578
|
match spec with
|
579
|
| Contract c ->
|
580
|
(* should have been processed by now *)
|
581
|
fprintf fmt "@[<hov 2>(*@contract@ ";
|
582
|
pp_spec fmt c;
|
583
|
fprintf fmt "@]*)@ "
|
584
|
| NodeSpec name ->
|
585
|
(* Pushing stmts in contract. We update the original information with the
|
586
|
computed one in nd. *)
|
587
|
let pp_l = pp_comma_list pp_var_name in
|
588
|
fprintf
|
589
|
fmt
|
590
|
"@[<hov 2>(*@contract import %s(%a) returns (%a); @]*)@ "
|
591
|
name
|
592
|
pp_l
|
593
|
inl
|
594
|
pp_l
|
595
|
outl
|
596
|
|
597
|
let pp_node_vs_function fmt nd =
|
598
|
fprintf fmt "%s" (if nd.node_dec_stateless then "function" else "node")
|
599
|
|
600
|
let pp_node fmt nd =
|
601
|
(* Prototype *)
|
602
|
fprintf
|
603
|
fmt
|
604
|
"%a @[<hov 0>%s (@[%a)@]@ returns (@[%a)@]@]@ "
|
605
|
pp_node_vs_function
|
606
|
nd
|
607
|
nd.node_id
|
608
|
pp_node_args
|
609
|
nd.node_inputs
|
610
|
pp_node_args
|
611
|
nd.node_outputs;
|
612
|
(* Contracts *)
|
613
|
fprintf
|
614
|
fmt
|
615
|
"%a"
|
616
|
(fun fmt s ->
|
617
|
match s with
|
618
|
| Some s ->
|
619
|
pp_spec_as_comment fmt (nd.node_inputs, nd.node_outputs, s)
|
620
|
| _ ->
|
621
|
())
|
622
|
nd.node_spec
|
623
|
(* (fun fmt -> match nd.node_spec with None -> () | Some _ -> fprintf fmt "@
|
624
|
") *);
|
625
|
(* Locals *)
|
626
|
fprintf
|
627
|
fmt
|
628
|
"%a"
|
629
|
(fun fmt locals ->
|
630
|
match locals with
|
631
|
| [] ->
|
632
|
()
|
633
|
| _ ->
|
634
|
fprintf
|
635
|
fmt
|
636
|
"@[<v 4>var %a@]@ "
|
637
|
(pp_print_list (fun fmt v -> fprintf fmt "%a;" pp_node_var v))
|
638
|
locals)
|
639
|
nd.node_locals;
|
640
|
(* Checks *)
|
641
|
fprintf
|
642
|
fmt
|
643
|
"%a"
|
644
|
(fun fmt checks ->
|
645
|
match checks with
|
646
|
| [] ->
|
647
|
()
|
648
|
| _ ->
|
649
|
fprintf
|
650
|
fmt
|
651
|
"@[<v 4>check@ %a@]@ "
|
652
|
(pp_print_list (fun fmt d -> fprintf fmt "%a" Dimension.pp d))
|
653
|
checks)
|
654
|
nd.node_checks;
|
655
|
(* Body *)
|
656
|
fprintf fmt "@[<v 2>let@ ";
|
657
|
(* Annotations *)
|
658
|
fprintf fmt "%a" (pp_print_list pp_expr_annot) nd.node_annot;
|
659
|
(* Statements *)
|
660
|
fprintf fmt "%a" pp_node_stmts nd.node_stmts;
|
661
|
(* Asserts *)
|
662
|
fprintf fmt "%a" pp_asserts nd.node_asserts;
|
663
|
(* closing boxes body (2) and node (1) *)
|
664
|
fprintf fmt "@]@ tel"
|
665
|
|
666
|
(*fprintf fmt "@ /* Scheduling: %a */ @ " (fprintf_list ~sep:", "
|
667
|
pp_print_string) (Scheduling.schedule_node nd)*)
|
668
|
|
669
|
let pp_node fmt nd =
|
670
|
match nd.node_spec, nd.node_iscontract with
|
671
|
| None, false | Some (NodeSpec _), false ->
|
672
|
pp_node fmt nd
|
673
|
| Some (Contract _), false ->
|
674
|
pp_node fmt nd (* may happen early in the compil process *)
|
675
|
| Some (Contract _), true ->
|
676
|
pp_contract fmt nd
|
677
|
| _ ->
|
678
|
assert false
|
679
|
|
680
|
let pp_imported_node fmt ind =
|
681
|
fprintf fmt "@[<v 0>";
|
682
|
(* Prototype *)
|
683
|
fprintf
|
684
|
fmt
|
685
|
"%s @[<hov 0>%s (@[%a)@]@ returns (@[%a)@]@]@ "
|
686
|
(if ind.nodei_stateless then "function" else "node")
|
687
|
ind.nodei_id
|
688
|
pp_node_args
|
689
|
ind.nodei_inputs
|
690
|
pp_node_args
|
691
|
ind.nodei_outputs;
|
692
|
(* Contracts *)
|
693
|
fprintf
|
694
|
fmt
|
695
|
"%a%t"
|
696
|
(fun fmt s ->
|
697
|
match s with
|
698
|
| Some s ->
|
699
|
pp_spec_as_comment fmt (ind.nodei_inputs, ind.nodei_outputs, s)
|
700
|
| _ ->
|
701
|
())
|
702
|
ind.nodei_spec
|
703
|
(fun fmt ->
|
704
|
match ind.nodei_spec with None -> () | Some _ -> fprintf fmt "@ ");
|
705
|
fprintf fmt "@]@ "
|
706
|
|
707
|
let pp_const_decl fmt cdecl =
|
708
|
fprintf fmt "%s = %a;" cdecl.const_id pp_const cdecl.const_value
|
709
|
|
710
|
(* XXX: UNUSED *)
|
711
|
(* let pp_const_decl_list fmt clist =
|
712
|
* pp_print_list pp_const_decl fmt clist *)
|
713
|
|
714
|
let pp_decl fmt decl =
|
715
|
match decl.top_decl_desc with
|
716
|
| Node nd ->
|
717
|
fprintf fmt "%a" pp_node nd
|
718
|
| ImportedNode ind ->
|
719
|
(* We do not print imported nodes *)
|
720
|
fprintf fmt "(* imported %a; *)" pp_imported_node ind
|
721
|
| Const c ->
|
722
|
fprintf fmt "const %a" pp_const_decl c
|
723
|
| Open (local, s) ->
|
724
|
if local then fprintf fmt "#open \"%s\"" s else fprintf fmt "#open <%s>" s
|
725
|
| Include s ->
|
726
|
fprintf fmt "include \"%s\"" s
|
727
|
| TypeDef tdef ->
|
728
|
fprintf fmt "%a" pp_typedef tdef
|
729
|
|
730
|
let pp_prog pp_decl fmt prog =
|
731
|
(* we first print types: the function SortProg.sort could do the job but ut
|
732
|
introduces a cyclic dependance *)
|
733
|
let open_decl, prog =
|
734
|
List.partition
|
735
|
(fun decl -> match decl.top_decl_desc with Open _ -> true | _ -> false)
|
736
|
prog
|
737
|
in
|
738
|
let type_decl, prog =
|
739
|
List.partition
|
740
|
(fun decl ->
|
741
|
match decl.top_decl_desc with TypeDef _ -> true | _ -> false)
|
742
|
prog
|
743
|
in
|
744
|
pp_print_list
|
745
|
~pp_open_box:pp_open_vbox0
|
746
|
~pp_sep:pp_print_cutcut
|
747
|
pp_decl
|
748
|
fmt
|
749
|
(open_decl @ type_decl @ prog)
|
750
|
|
751
|
(* Gives a short overview of model content. Do not print all node content *)
|
752
|
let pp_short_decl fmt decl =
|
753
|
match decl.top_decl_desc with
|
754
|
| Node nd ->
|
755
|
fprintf fmt "%a %s" pp_node_vs_function nd nd.node_id
|
756
|
| ImportedNode ind ->
|
757
|
fprintf fmt "imported node %s" ind.nodei_id
|
758
|
| Const c ->
|
759
|
fprintf fmt "const %a" pp_const_decl c
|
760
|
| Include s ->
|
761
|
fprintf fmt "include \"%s\"" s
|
762
|
| Open (local, s) ->
|
763
|
if local then fprintf fmt "#open \"%s\"" s
|
764
|
else fprintf fmt "#open <%s>" s
|
765
|
| TypeDef tdef ->
|
766
|
fprintf fmt "type %s" tdef.tydef_id
|
767
|
|
768
|
let pp_prog_short = pp_prog pp_short_decl
|
769
|
|
770
|
let pp_prog = pp_prog pp_decl
|
771
|
|
772
|
let pp_lusi fmt decl =
|
773
|
match decl.top_decl_desc with
|
774
|
| ImportedNode ind ->
|
775
|
fprintf fmt "%a;@ " pp_imported_node ind
|
776
|
| Const c ->
|
777
|
fprintf fmt "const %a@ " pp_const_decl c
|
778
|
| Include s ->
|
779
|
fprintf fmt "include \"%s\"" s
|
780
|
| Open (local, s) ->
|
781
|
if local then fprintf fmt "#open \"%s\"@ " s
|
782
|
else fprintf fmt "#open <%s>@ " s
|
783
|
| TypeDef tdef ->
|
784
|
fprintf fmt "%a@ " pp_typedef tdef
|
785
|
| Node _ ->
|
786
|
assert false
|
787
|
|
788
|
let pp_lusi_header fmt basename prog =
|
789
|
fprintf fmt "@[<v 0>";
|
790
|
fprintf fmt "(* Generated Lustre Interface file from %s.lus *)@ " basename;
|
791
|
fprintf
|
792
|
fmt
|
793
|
"(* by Lustre-C compiler version %s, %a *)@ "
|
794
|
Version.number
|
795
|
pp_date
|
796
|
(Unix.gmtime (Unix.time ()));
|
797
|
fprintf
|
798
|
fmt
|
799
|
"(* Feel free to mask some of the definitions by removing them from this \
|
800
|
file. *)@ @ ";
|
801
|
List.iter (fprintf fmt "%a@ " pp_lusi) prog;
|
802
|
fprintf fmt "@]@."
|
803
|
|
804
|
(* XXX: UNUSED *)
|
805
|
(* let pp_offset fmt offset =
|
806
|
* match offset with
|
807
|
* | Index i ->
|
808
|
* fprintf fmt "[%a]" Dimension.pp i
|
809
|
* | Field f ->
|
810
|
* fprintf fmt ".%s" f *)
|
811
|
|
812
|
let pp_node_list fmt prog =
|
813
|
Format.fprintf
|
814
|
fmt
|
815
|
"@[<h 2>%a@]"
|
816
|
(pp_print_list (fun fmt decl ->
|
817
|
match decl.top_decl_desc with
|
818
|
| Node nd ->
|
819
|
Format.fprintf fmt "%s" nd.node_id
|
820
|
| _ ->
|
821
|
()))
|
822
|
prog
|
823
|
|
824
|
(* Local Variables: *)
|
825
|
(* compile-command:"make -C .." *)
|
826
|
(* End: *)
|