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