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