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