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