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 Format
|
14
|
open Utils
|
15
|
|
16
|
(* Prints [v] as [pp_fun] would do, but adds a backslash at each end of line,
|
17
|
following the C convention for multiple lines macro *)
|
18
|
let pp_as_c_macro pp_fun fmt v =
|
19
|
let formatter_out_funs = pp_get_formatter_out_functions fmt () in
|
20
|
let macro_newline () =
|
21
|
begin
|
22
|
formatter_out_funs.out_string "\\" 0 1;
|
23
|
formatter_out_funs.out_newline ()
|
24
|
end in
|
25
|
begin
|
26
|
pp_set_formatter_out_functions fmt { formatter_out_funs with out_newline = macro_newline };
|
27
|
pp_fun fmt v;
|
28
|
pp_set_formatter_out_functions fmt formatter_out_funs;
|
29
|
end
|
30
|
|
31
|
let rec pp_var_struct_type_field fmt (label, tdesc) =
|
32
|
fprintf fmt "%a : %a;" pp_print_string label pp_var_type_dec_desc tdesc
|
33
|
and pp_var_type_dec_desc fmt tdesc =
|
34
|
match tdesc with
|
35
|
| Tydec_any -> fprintf fmt "<any>"
|
36
|
| Tydec_int -> fprintf fmt "int"
|
37
|
| Tydec_real -> fprintf fmt "real"
|
38
|
(* | Tydec_float -> fprintf fmt "float" *)
|
39
|
| Tydec_bool -> fprintf fmt "bool"
|
40
|
| Tydec_clock t -> fprintf fmt "%a clock" pp_var_type_dec_desc t
|
41
|
| Tydec_const t -> fprintf fmt "%s" t
|
42
|
| Tydec_enum id_list -> fprintf fmt "enum {%a }" (fprintf_list ~sep:", " pp_print_string) id_list
|
43
|
| Tydec_struct f_list -> fprintf fmt "struct {%a }" (fprintf_list ~sep:" " pp_var_struct_type_field) f_list
|
44
|
| Tydec_array (s, t) -> fprintf fmt "%a^%a" pp_var_type_dec_desc t Dimension.pp_dimension s
|
45
|
|
46
|
let pp_var_type_dec fmt ty =
|
47
|
pp_var_type_dec_desc fmt ty.ty_dec_desc
|
48
|
|
49
|
let pp_var_name fmt id = fprintf fmt "%s" id.var_id
|
50
|
let pp_var_type fmt id =
|
51
|
if !Options.print_dec_types then
|
52
|
pp_var_type_dec fmt id.var_dec_type
|
53
|
else
|
54
|
Types.print_node_ty fmt id.var_type
|
55
|
let pp_var_clock fmt id = Clocks.print_ck_suffix fmt id.var_clock
|
56
|
|
57
|
let pp_eq_lhs = fprintf_list ~sep:", " pp_print_string
|
58
|
|
59
|
let pp_var fmt id =
|
60
|
fprintf fmt "%s%s: %a"
|
61
|
(if id.var_dec_const then "const " else "")
|
62
|
id.var_id
|
63
|
pp_var_type id
|
64
|
|
65
|
let pp_quantifiers fmt (q, vars) =
|
66
|
match q with
|
67
|
| Forall -> fprintf fmt "forall %a" (fprintf_list ~sep:"; " pp_var) vars
|
68
|
| Exists -> fprintf fmt "exists %a" (fprintf_list ~sep:"; " pp_var) vars
|
69
|
|
70
|
let rec pp_struct_const_field fmt (label, c) =
|
71
|
fprintf fmt "%a = %a;" pp_print_string label pp_const c
|
72
|
and pp_const fmt c =
|
73
|
match c with
|
74
|
| Const_int i -> pp_print_int fmt i
|
75
|
| Const_real (c, e, s) -> pp_print_string fmt s (*if e = 0 then pp_print_int fmt c else if e < 0 then Format.fprintf fmt "%ie%i" c (-e) else Format.fprintf fmt "%ie-%i" c e *)
|
76
|
(* | Const_float r -> pp_print_float fmt r *)
|
77
|
| Const_tag t -> pp_print_string fmt t
|
78
|
| Const_array ca -> Format.fprintf fmt "[%a]" (Utils.fprintf_list ~sep:"," pp_const) ca
|
79
|
| Const_struct fl -> Format.fprintf fmt "{%a }" (Utils.fprintf_list ~sep:" " pp_struct_const_field) fl
|
80
|
| Const_string s -> pp_print_string fmt ("\"" ^ s ^ "\"")
|
81
|
|
82
|
|
83
|
let pp_annot_key fmt kwds =
|
84
|
match kwds with
|
85
|
| [] -> assert false
|
86
|
| [x] -> Format.pp_print_string fmt x
|
87
|
| _ -> Format.fprintf fmt "/%a/" (fprintf_list ~sep:"/" Format.pp_print_string) kwds
|
88
|
|
89
|
let rec pp_expr fmt expr =
|
90
|
(match expr.expr_annot with
|
91
|
| None -> fprintf fmt "%t"
|
92
|
| Some ann -> fprintf fmt "@[(%a %t)@]" pp_expr_annot ann)
|
93
|
(fun fmt ->
|
94
|
match expr.expr_desc with
|
95
|
| Expr_const c -> pp_const fmt c
|
96
|
| Expr_ident id -> fprintf fmt "%s" id
|
97
|
| Expr_array a -> fprintf fmt "[%a]" pp_tuple a
|
98
|
| Expr_access (a, d) -> fprintf fmt "%a[%a]" pp_expr a Dimension.pp_dimension d
|
99
|
| Expr_power (a, d) -> fprintf fmt "(%a^%a)" pp_expr a Dimension.pp_dimension d
|
100
|
| Expr_tuple el -> fprintf fmt "(%a)" pp_tuple el
|
101
|
| Expr_ite (c, t, e) -> fprintf fmt "@[<hov 1>(if %a then@ @[<hov 2>%a@]@ else@ @[<hov 2>%a@]@])" pp_expr c pp_expr t pp_expr e
|
102
|
| Expr_arrow (e1, e2) -> fprintf fmt "(%a -> %a)" pp_expr e1 pp_expr e2
|
103
|
| Expr_fby (e1, e2) -> fprintf fmt "%a fby %a" pp_expr e1 pp_expr e2
|
104
|
| Expr_pre e -> fprintf fmt "pre %a" pp_expr e
|
105
|
| Expr_when (e, id, l) -> fprintf fmt "%a when %s(%s)" pp_expr e l id
|
106
|
| Expr_merge (id, hl) ->
|
107
|
fprintf fmt "merge %s %a" id pp_handlers hl
|
108
|
| Expr_appl (id, e, r) -> pp_app fmt id e r
|
109
|
)
|
110
|
and pp_tuple fmt el =
|
111
|
fprintf_list ~sep:"," pp_expr fmt el
|
112
|
|
113
|
and pp_handler fmt (t, h) =
|
114
|
fprintf fmt "(%s -> %a)" t pp_expr h
|
115
|
|
116
|
and pp_handlers fmt hl =
|
117
|
fprintf_list ~sep:" " pp_handler fmt hl
|
118
|
|
119
|
and pp_app fmt id e r =
|
120
|
match r with
|
121
|
| None -> pp_call fmt id e
|
122
|
| Some c -> fprintf fmt "%t every (%a)" (fun fmt -> pp_call fmt id e) pp_expr c
|
123
|
|
124
|
and pp_call fmt id e =
|
125
|
match id, e.expr_desc with
|
126
|
| "+", Expr_tuple([e1;e2]) -> fprintf fmt "(%a + %a)" pp_expr e1 pp_expr e2
|
127
|
| "uminus", _ -> fprintf fmt "(- %a)" pp_expr e
|
128
|
| "-", Expr_tuple([e1;e2]) -> fprintf fmt "(%a - %a)" pp_expr e1 pp_expr e2
|
129
|
| "*", Expr_tuple([e1;e2]) -> fprintf fmt "(%a * %a)" pp_expr e1 pp_expr e2
|
130
|
| "/", Expr_tuple([e1;e2]) -> fprintf fmt "(%a / %a)" pp_expr e1 pp_expr e2
|
131
|
| "mod", Expr_tuple([e1;e2]) -> fprintf fmt "(%a mod %a)" pp_expr e1 pp_expr e2
|
132
|
| "&&", Expr_tuple([e1;e2]) -> fprintf fmt "(%a and %a)" pp_expr e1 pp_expr e2
|
133
|
| "||", Expr_tuple([e1;e2]) -> fprintf fmt "(%a or %a)" pp_expr e1 pp_expr e2
|
134
|
| "xor", Expr_tuple([e1;e2]) -> fprintf fmt "(%a xor %a)" pp_expr e1 pp_expr e2
|
135
|
| "impl", Expr_tuple([e1;e2]) -> fprintf fmt "(%a => %a)" pp_expr e1 pp_expr e2
|
136
|
| "<", Expr_tuple([e1;e2]) -> fprintf fmt "(%a < %a)" pp_expr e1 pp_expr e2
|
137
|
| "<=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a <= %a)" pp_expr e1 pp_expr e2
|
138
|
| ">", Expr_tuple([e1;e2]) -> fprintf fmt "(%a > %a)" pp_expr e1 pp_expr e2
|
139
|
| ">=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a >= %a)" pp_expr e1 pp_expr e2
|
140
|
| "!=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a <> %a)" pp_expr e1 pp_expr e2
|
141
|
| "=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a = %a)" pp_expr e1 pp_expr e2
|
142
|
| "not", _ -> fprintf fmt "(not %a)" pp_expr e
|
143
|
| _, Expr_tuple _ -> fprintf fmt "%s %a" id pp_expr e
|
144
|
| _ -> fprintf fmt "%s (%a)" id pp_expr e
|
145
|
|
146
|
and pp_eexpr fmt e =
|
147
|
fprintf fmt "%a%t %a"
|
148
|
(Utils.fprintf_list ~sep:"; " pp_quantifiers) e.eexpr_quantifiers
|
149
|
(fun fmt -> match e.eexpr_quantifiers with [] -> () | _ -> fprintf fmt ";")
|
150
|
pp_expr e.eexpr_qfexpr
|
151
|
|
152
|
and pp_sf_value fmt e =
|
153
|
fprintf fmt "%a"
|
154
|
(* (Utils.fprintf_list ~sep:"; " pp_quantifiers) e.eexpr_quantifiers *)
|
155
|
(* (fun fmt -> match e.eexpr_quantifiers *)
|
156
|
(* with [] -> () *)
|
157
|
(* | _ -> fprintf fmt ";") *)
|
158
|
pp_expr e.eexpr_qfexpr
|
159
|
|
160
|
and pp_s_function fmt expr_ann =
|
161
|
let pp_annot fmt (kwds, ee) =
|
162
|
Format.fprintf fmt " %t : %a"
|
163
|
(fun fmt -> match kwds with
|
164
|
| [] -> assert false
|
165
|
| [x] -> Format.pp_print_string fmt x
|
166
|
| _ -> Format.fprintf fmt "%a" (fprintf_list ~sep:"/" Format.pp_print_string) kwds)
|
167
|
pp_sf_value ee
|
168
|
in
|
169
|
fprintf_list ~sep:"@ " pp_annot fmt expr_ann.annots
|
170
|
|
171
|
and pp_expr_annot fmt expr_ann =
|
172
|
let pp_annot fmt (kwds, ee) =
|
173
|
Format.fprintf fmt "(*! %a: %a; *)"
|
174
|
pp_annot_key kwds
|
175
|
pp_eexpr ee
|
176
|
in
|
177
|
fprintf_list ~sep:"@ " pp_annot fmt expr_ann.annots
|
178
|
|
179
|
|
180
|
let pp_asserts fmt asserts =
|
181
|
match asserts with
|
182
|
| _::_ -> (
|
183
|
fprintf fmt "(* Asserts definitions *)@ ";
|
184
|
fprintf_list ~sep:"@ " (fun fmt assert_ ->
|
185
|
let expr = assert_.assert_expr in
|
186
|
fprintf fmt "assert %a;" pp_expr expr
|
187
|
) fmt asserts
|
188
|
)
|
189
|
| _ -> ()
|
190
|
|
191
|
(*
|
192
|
let pp_node_var fmt id = fprintf fmt "%s%s: %a(%a)%a" (if id.var_dec_const then "const " else "") id.var_id print_dec_ty id.var_dec_type.ty_dec_desc Types.print_ty id.var_type Clocks.print_ck_suffix id.var_clock
|
193
|
*)
|
194
|
let pp_node_var fmt id =
|
195
|
begin
|
196
|
fprintf fmt "%s%s: %a%a"
|
197
|
(if id.var_dec_const then "const " else "")
|
198
|
id.var_id
|
199
|
pp_var_type id
|
200
|
pp_var_clock id;
|
201
|
match id.var_dec_value with
|
202
|
| None -> ()
|
203
|
| Some v -> fprintf fmt " = %a" pp_expr v
|
204
|
end
|
205
|
|
206
|
let pp_node_args = fprintf_list ~sep:";@ " pp_node_var
|
207
|
|
208
|
let pp_node_eq fmt eq =
|
209
|
fprintf fmt "%a = %a;"
|
210
|
pp_eq_lhs eq.eq_lhs
|
211
|
pp_expr eq.eq_rhs
|
212
|
|
213
|
let pp_restart fmt restart =
|
214
|
Format.fprintf fmt "%s" (if restart then "restart" else "resume")
|
215
|
|
216
|
let pp_unless fmt (_, expr, restart, st) =
|
217
|
Format.fprintf fmt "unless %a %a %s"
|
218
|
pp_expr expr
|
219
|
pp_restart restart
|
220
|
st
|
221
|
|
222
|
let pp_until fmt (_, expr, restart, st) =
|
223
|
Format.fprintf fmt "until %a %a %s"
|
224
|
pp_expr expr
|
225
|
pp_restart restart
|
226
|
st
|
227
|
|
228
|
let rec pp_handler fmt handler =
|
229
|
Format.fprintf fmt "state %s:@ @[<v 2> %a%t%alet@,@[<v 2> %a@ %a@ %a@]@,tel@ %a@]"
|
230
|
handler.hand_state
|
231
|
(Utils.fprintf_list ~sep:"@ " pp_unless) handler.hand_unless
|
232
|
(fun fmt -> if not ([] = handler.hand_unless) then fprintf fmt "@ ")
|
233
|
(fun fmt locals ->
|
234
|
match locals with [] -> () | _ ->
|
235
|
Format.fprintf fmt "@[<v 4>var %a@]@ "
|
236
|
(Utils.fprintf_list ~sep:"@ "
|
237
|
(fun fmt v -> Format.fprintf fmt "%a;" pp_node_var v))
|
238
|
locals)
|
239
|
handler.hand_locals
|
240
|
(fprintf_list ~sep:"@ " pp_expr_annot) handler.hand_annots
|
241
|
pp_node_stmts handler.hand_stmts
|
242
|
pp_asserts handler.hand_asserts
|
243
|
(Utils.fprintf_list ~sep:"@," pp_until) handler.hand_until
|
244
|
|
245
|
and pp_node_stmt fmt stmt =
|
246
|
match stmt with
|
247
|
| Eq eq -> pp_node_eq fmt eq
|
248
|
| Aut aut -> pp_node_aut fmt aut
|
249
|
|
250
|
and pp_node_stmts fmt stmts = fprintf_list ~sep:"@ " pp_node_stmt fmt stmts
|
251
|
|
252
|
and pp_node_aut fmt aut =
|
253
|
Format.fprintf fmt "@[<v 0>automaton %s@,%a@]"
|
254
|
aut.aut_id
|
255
|
(Utils.fprintf_list ~sep:"@ " pp_handler) aut.aut_handlers
|
256
|
|
257
|
and pp_node_eqs fmt eqs = fprintf_list ~sep:"@ " pp_node_eq fmt eqs
|
258
|
|
259
|
let pp_typedef fmt ty =
|
260
|
fprintf fmt "type %s = %a;" ty.tydef_id pp_var_type_dec_desc ty.tydef_desc
|
261
|
|
262
|
let pp_typedec fmt ty =
|
263
|
fprintf fmt "type %s;" ty.tydec_id
|
264
|
|
265
|
(* let rec pp_var_type fmt ty = *)
|
266
|
(* fprintf fmt "%a" (match ty.tdesc with *)
|
267
|
(* | Tvar | Tarrow | Tlink | Tunivar -> assert false *)
|
268
|
(* | Tint -> pp_print_string fmt "int" *)
|
269
|
(* | Treal -> pp_print_string fmt "real" *)
|
270
|
(* | Tbool -> pp_print_string fmt "bool" *)
|
271
|
(* | Trat -> pp_print_string fmt "rat" *)
|
272
|
(* | Tclock -> pp_print_string fmt "clock" *)
|
273
|
(* | Ttuple tel -> fprintf_list ~sep:" * " pp_var_type fmt tel *)
|
274
|
(* ) *)
|
275
|
|
276
|
|
277
|
let pp_spec fmt spec =
|
278
|
fprintf fmt "@[<hov 2>(*@@ ";
|
279
|
fprintf_list ~sep:"@,@@ " (fun fmt r -> fprintf fmt "requires %a;" pp_eexpr r) fmt spec.requires;
|
280
|
fprintf_list ~sep:"@,@@ " (fun fmt r -> fprintf fmt "ensures %a; " pp_eexpr r) fmt spec.ensures;
|
281
|
fprintf_list ~sep:"@," (fun fmt (name, assumes, ensures, _) ->
|
282
|
fprintf fmt "behavior %s:@[@ %a@ %a@]"
|
283
|
name
|
284
|
(fprintf_list ~sep:"@ " (fun fmt r -> fprintf fmt "assumes %a;" pp_eexpr r)) assumes
|
285
|
(fprintf_list ~sep:"@ " (fun fmt r -> fprintf fmt "ensures %a;" pp_eexpr r)) ensures
|
286
|
) fmt spec.behaviors;
|
287
|
fprintf fmt "@]*)";
|
288
|
()
|
289
|
|
290
|
|
291
|
let pp_node fmt nd =
|
292
|
fprintf fmt "@[<v 0>%a%t%s @[<hov 0>%s (@[%a)@]@ returns (@[%a)@]@]@ %a%alet@[<h 2> @ @[<v>%a@ %a@ %a@]@]@ tel@]@ "
|
293
|
(fun fmt s -> match s with Some s -> pp_spec fmt s | _ -> ()) nd.node_spec
|
294
|
(fun fmt -> match nd.node_spec with None -> () | Some _ -> Format.fprintf fmt "@ ")
|
295
|
(if nd.node_dec_stateless then "function" else "node")
|
296
|
nd.node_id
|
297
|
pp_node_args nd.node_inputs
|
298
|
pp_node_args nd.node_outputs
|
299
|
(fun fmt locals ->
|
300
|
match locals with [] -> () | _ ->
|
301
|
fprintf fmt "@[<v 4>var %a@]@ "
|
302
|
(fprintf_list ~sep:"@ "
|
303
|
(fun fmt v -> fprintf fmt "%a;" pp_node_var v))
|
304
|
locals
|
305
|
) nd.node_locals
|
306
|
(fun fmt checks ->
|
307
|
match checks with [] -> () | _ ->
|
308
|
fprintf fmt "@[<v 4>check@ %a@]@ "
|
309
|
(fprintf_list ~sep:"@ "
|
310
|
(fun fmt d -> fprintf fmt "%a" Dimension.pp_dimension d))
|
311
|
checks
|
312
|
) nd.node_checks
|
313
|
(fprintf_list ~sep:"@ " pp_expr_annot) nd.node_annot
|
314
|
pp_node_stmts nd.node_stmts
|
315
|
pp_asserts nd.node_asserts
|
316
|
(*fprintf fmt "@ /* Scheduling: %a */ @ " (fprintf_list ~sep:", " pp_print_string) (Scheduling.schedule_node nd)*)
|
317
|
|
318
|
let pp_imported_node fmt ind =
|
319
|
fprintf fmt "@[<v>%s %s (%a) returns (%a)@]"
|
320
|
(if ind.nodei_stateless then "function" else "node")
|
321
|
ind.nodei_id
|
322
|
pp_node_args ind.nodei_inputs
|
323
|
pp_node_args ind.nodei_outputs
|
324
|
|
325
|
let pp_const_decl fmt cdecl =
|
326
|
fprintf fmt "%s = %a;" cdecl.const_id pp_const cdecl.const_value
|
327
|
|
328
|
let pp_const_decl_list fmt clist =
|
329
|
fprintf_list ~sep:"@ " pp_const_decl fmt clist
|
330
|
|
331
|
let pp_decl fmt decl =
|
332
|
match decl.top_decl_desc with
|
333
|
| Node nd -> fprintf fmt "%a" pp_node nd
|
334
|
| ImportedNode ind ->
|
335
|
fprintf fmt "imported %a;" pp_imported_node ind
|
336
|
| Const c -> fprintf fmt "const %a" pp_const_decl c
|
337
|
| Open (local, s) -> if local then fprintf fmt "#open \"%s\"" s else fprintf fmt "#open <%s>" s
|
338
|
| TypeDef tdef -> fprintf fmt "%a" pp_typedef tdef
|
339
|
|
340
|
let pp_prog fmt prog =
|
341
|
(* we first print types: the function SortProg.sort could do the job but ut
|
342
|
introduces a cyclic dependance *)
|
343
|
let type_decl, others =
|
344
|
List.partition (fun decl -> match decl.top_decl_desc with TypeDef _ -> true | _ -> false) prog
|
345
|
in
|
346
|
fprintf fmt "@[<v 0>%a@]" (fprintf_list ~sep:"@ " pp_decl) (type_decl@others)
|
347
|
|
348
|
let pp_short_decl fmt decl =
|
349
|
match decl.top_decl_desc with
|
350
|
| Node nd -> fprintf fmt "node %s@ " nd.node_id
|
351
|
| ImportedNode ind -> fprintf fmt "imported node %s" ind.nodei_id
|
352
|
| Const c -> fprintf fmt "const %a@ " pp_const_decl c
|
353
|
| Open (local, s) -> if local then fprintf fmt "#open \"%s\"@ " s else fprintf fmt "#open <%s>@ " s
|
354
|
| TypeDef tdef -> fprintf fmt "type %s;@ " tdef.tydef_id
|
355
|
|
356
|
let pp_lusi fmt decl =
|
357
|
match decl.top_decl_desc with
|
358
|
| ImportedNode ind -> fprintf fmt "%a;@ " pp_imported_node ind
|
359
|
| Const c -> fprintf fmt "const %a@ " pp_const_decl c
|
360
|
| Open (local, s) -> if local then fprintf fmt "#open \"%s\"@ " s else fprintf fmt "#open <%s>@ " s
|
361
|
| TypeDef tdef -> fprintf fmt "%a@ " pp_typedef tdef
|
362
|
| Node _ -> assert false
|
363
|
|
364
|
let pp_lusi_header fmt basename prog =
|
365
|
fprintf fmt "@[<v 0>";
|
366
|
fprintf fmt "(* Generated Lustre Interface file from %s.lus *)@ " basename;
|
367
|
fprintf fmt "(* by Lustre-C compiler version %s, %a *)@ " Version.number pp_date (Unix.gmtime (Unix.time ()));
|
368
|
fprintf fmt "(* Feel free to mask some of the definitions by removing them from this file. *)@ @ ";
|
369
|
List.iter (fprintf fmt "%a@ " pp_lusi) prog;
|
370
|
fprintf fmt "@]@."
|
371
|
|
372
|
let pp_offset fmt offset =
|
373
|
match offset with
|
374
|
| Index i -> fprintf fmt "[%a]" Dimension.pp_dimension i
|
375
|
| Field f -> fprintf fmt ".%s" f
|
376
|
|
377
|
(* Local Variables: *)
|
378
|
(* compile-command:"make -C .." *)
|
379
|
(* End: *)
|