lustrec / src / printers.ml @ 17abbe95
History | View | Annotate | Download (12.4 KB)
1 |
(* ---------------------------------------------------------------------------- |
---|---|
2 |
* SchedMCore - A MultiCore Scheduling Framework |
3 |
* Copyright (C) 2009-2011, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE |
4 |
* |
5 |
* This file is part of Prelude |
6 |
* |
7 |
* Prelude is free software; you can redistribute it and/or |
8 |
* modify it under the terms of the GNU Lesser General Public License |
9 |
* as published by the Free Software Foundation ; either version 2 of |
10 |
* the License, or (at your option) any later version. |
11 |
* |
12 |
* Prelude is distributed in the hope that it will be useful, but |
13 |
* WITHOUT ANY WARRANTY ; without even the implied warranty of |
14 |
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU |
15 |
* Lesser General Public License for more details. |
16 |
* |
17 |
* You should have received a copy of the GNU Lesser General Public |
18 |
* License along with this program ; if not, write to the Free Software |
19 |
* Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 |
20 |
* USA |
21 |
*---------------------------------------------------------------------------- *) |
22 |
open Corelang |
23 |
open LustreSpec |
24 |
open Format |
25 |
open Utils |
26 |
|
27 |
(* Prints [v] as [pp_fun] would do, but adds a backslash at each end of line, |
28 |
following the C convention for multiple lines macro *) |
29 |
let pp_as_c_macro pp_fun fmt v = |
30 |
let (out, flush, newline, spaces) = pp_get_all_formatter_output_functions fmt () in |
31 |
let macro_newline () = (out "\\" 0 1; newline ()) in |
32 |
begin |
33 |
pp_set_all_formatter_output_functions fmt out flush macro_newline spaces; |
34 |
pp_fun fmt v; |
35 |
pp_set_all_formatter_output_functions fmt out flush newline spaces; |
36 |
end |
37 |
|
38 |
|
39 |
let pp_var_name fmt id = fprintf fmt "%s" id.var_id |
40 |
|
41 |
let pp_eq_lhs = fprintf_list ~sep:", " pp_print_string |
42 |
|
43 |
let rec pp_const fmt c = |
44 |
match c with |
45 |
| Const_int i -> pp_print_int fmt i |
46 |
| Const_real r -> pp_print_string fmt r |
47 |
| Const_float r -> pp_print_float fmt r |
48 |
| Const_tag t -> pp_print_string fmt t |
49 |
| Const_array ca -> Format.fprintf fmt "[%a]" (Utils.fprintf_list ~sep:"," pp_const) ca |
50 |
|
51 |
and pp_var fmt id = fprintf fmt "%s: %a" id.var_id Types.print_ty id.var_type |
52 |
|
53 |
and pp_expr fmt expr = |
54 |
match expr.expr_desc with |
55 |
| Expr_const c -> pp_const fmt c |
56 |
| Expr_ident id -> Format.fprintf fmt "%s" id |
57 |
(* | Expr_cst_array (c, e) -> fprintf fmt "%a^%a" pp_expr e pp_const c *) |
58 |
| Expr_array a -> fprintf fmt "[%a]" pp_tuple a |
59 |
| Expr_access (a, d) -> fprintf fmt "%a[%a]" pp_expr a Dimension.pp_dimension d |
60 |
| Expr_power (a, d) -> fprintf fmt "(%a^%a)" pp_expr a Dimension.pp_dimension d |
61 |
| Expr_tuple el -> fprintf fmt "(%a)" pp_tuple el |
62 |
| Expr_ite (c, t, e) -> fprintf fmt "(if %a then %a else %a)" pp_expr c pp_expr t pp_expr e |
63 |
| Expr_arrow (e1, e2) -> fprintf fmt "%a -> %a" pp_expr e1 pp_expr e2 |
64 |
| Expr_fby (e1, e2) -> fprintf fmt "%a fby %a" pp_expr e1 pp_expr e2 |
65 |
| Expr_pre e -> fprintf fmt "pre %a" pp_expr e |
66 |
| Expr_when (e, id, l) -> fprintf fmt "%a when %s(%s)" pp_expr e l id |
67 |
| Expr_merge (id, hl) -> |
68 |
fprintf fmt "merge %s %a" id pp_handlers hl |
69 |
| Expr_appl (id, e, r) -> pp_app fmt id e r |
70 |
| Expr_uclock _ |
71 |
| Expr_dclock _ |
72 |
| Expr_phclock _ -> assert false |
73 |
|
74 |
and pp_tuple fmt el = |
75 |
fprintf_list ~sep:"," pp_expr fmt el |
76 |
|
77 |
and pp_handler fmt (t, h) = |
78 |
fprintf fmt "(%s -> %a)" t pp_expr h |
79 |
|
80 |
and pp_handlers fmt hl = |
81 |
fprintf_list ~sep:" " pp_handler fmt hl |
82 |
|
83 |
and pp_app fmt id e r = |
84 |
match r with |
85 |
| None -> |
86 |
(match id, e.expr_desc with |
87 |
| "+", Expr_tuple([e1;e2]) -> fprintf fmt "(%a + %a)" pp_expr e1 pp_expr e2 |
88 |
| "uminus", _ -> fprintf fmt "(- %a)" pp_expr e |
89 |
| "-", Expr_tuple([e1;e2]) -> fprintf fmt "(%a - %a)" pp_expr e1 pp_expr e2 |
90 |
| "*", Expr_tuple([e1;e2]) -> fprintf fmt "(%a * %a)" pp_expr e1 pp_expr e2 |
91 |
| "/", Expr_tuple([e1;e2]) -> fprintf fmt "(%a / %a)" pp_expr e1 pp_expr e2 |
92 |
| "mod", Expr_tuple([e1;e2]) -> fprintf fmt "(%a mod %a)" pp_expr e1 pp_expr e2 |
93 |
| "&&", Expr_tuple([e1;e2]) -> fprintf fmt "(%a and %a)" pp_expr e1 pp_expr e2 |
94 |
| "||", Expr_tuple([e1;e2]) -> fprintf fmt "(%a or %a)" pp_expr e1 pp_expr e2 |
95 |
| "xor", Expr_tuple([e1;e2]) -> fprintf fmt "(%a xor %a)" pp_expr e1 pp_expr e2 |
96 |
| "impl", 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 |
| "<=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a <= %a)" pp_expr e1 pp_expr e2 |
99 |
| ">", Expr_tuple([e1;e2]) -> fprintf fmt "(%a > %a)" pp_expr e1 pp_expr e2 |
100 |
| ">=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a >= %a)" pp_expr e1 pp_expr e2 |
101 |
| "!=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a != %a)" pp_expr e1 pp_expr e2 |
102 |
| "=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a = %a)" pp_expr e1 pp_expr e2 |
103 |
| "not", _ -> fprintf fmt "(not %a)" pp_expr e |
104 |
| _ -> fprintf fmt "%s (%a)" id pp_expr e) |
105 |
| Some (x, l) -> fprintf fmt "%s (%a) every %s(%s)" id pp_expr e l x |
106 |
|
107 |
let pp_node_eq fmt eq = |
108 |
fprintf fmt "%a = %a;" |
109 |
pp_eq_lhs eq.eq_lhs |
110 |
pp_expr eq.eq_rhs |
111 |
|
112 |
let pp_node_eqs = fprintf_list ~sep:"@ " pp_node_eq |
113 |
|
114 |
let pp_node_args = fprintf_list ~sep:"; " pp_var |
115 |
|
116 |
let pp_var_type_dec fmt ty = |
117 |
let rec pp_var_type_dec_desc fmt tdesc = |
118 |
match tdesc with |
119 |
| Tydec_any -> fprintf fmt "<any>" |
120 |
| Tydec_int -> fprintf fmt "int" |
121 |
| Tydec_real -> fprintf fmt "real" |
122 |
| Tydec_float -> fprintf fmt "float" |
123 |
| Tydec_bool -> fprintf fmt "bool" |
124 |
| Tydec_clock t -> fprintf fmt "%a clock" pp_var_type_dec_desc t |
125 |
| Tydec_const t -> fprintf fmt "%s" t |
126 |
| Tydec_enum id_list -> fprintf fmt "enum {%a }" (fprintf_list ~sep:", " pp_print_string) id_list |
127 |
| Tydec_array (s, t) -> fprintf fmt "%a^%a" pp_var_type_dec_desc t Dimension.pp_dimension s |
128 |
in pp_var_type_dec_desc fmt ty.ty_dec_desc |
129 |
|
130 |
(* let rec pp_var_type fmt ty = *) |
131 |
(* fprintf fmt "%a" (match ty.tdesc with *) |
132 |
(* | Tvar | Tarrow | Tlink | Tunivar -> assert false *) |
133 |
(* | Tint -> pp_print_string fmt "int" *) |
134 |
(* | Treal -> pp_print_string fmt "real" *) |
135 |
(* | Tbool -> pp_print_string fmt "bool" *) |
136 |
(* | Trat -> pp_print_string fmt "rat" *) |
137 |
(* | Tclock -> pp_print_string fmt "clock" *) |
138 |
(* | Ttuple tel -> fprintf_list ~sep:" * " pp_var_type fmt tel *) |
139 |
(* ) *) |
140 |
|
141 |
let pp_node fmt nd = |
142 |
fprintf fmt "@[<v>node %s (%a) returns (%a)@ %a%alet@ @[<h 2> @ @[%a@]@ @]@ tel@]@ " |
143 |
nd.node_id |
144 |
pp_node_args nd.node_inputs |
145 |
pp_node_args nd.node_outputs |
146 |
(fun fmt locals -> |
147 |
match locals with [] -> () | _ -> |
148 |
fprintf fmt "@[<v 4>var %a@]@ " |
149 |
(fprintf_list ~sep:"@ " |
150 |
(fun fmt v -> fprintf fmt "%a;" pp_var v)) |
151 |
locals |
152 |
) nd.node_locals |
153 |
(fun fmt checks -> |
154 |
match checks with [] -> () | _ -> |
155 |
fprintf fmt "@[<v 4>check@ %a@]@ " |
156 |
(fprintf_list ~sep:"@ " |
157 |
(fun fmt d -> fprintf fmt "%a" Dimension.pp_dimension d)) |
158 |
checks |
159 |
) nd.node_checks |
160 |
pp_node_eqs nd.node_eqs |
161 |
(*fprintf fmt "@ /* Scheduling: %a */ @ " (fprintf_list ~sep:", " pp_print_string) (Scheduling.schedule_node nd)*) |
162 |
|
163 |
let pp_imported_node fmt ind = |
164 |
fprintf fmt "@[<v>node %s (%a) returns (%a) %t@]" |
165 |
ind.nodei_id |
166 |
pp_node_args ind.nodei_inputs |
167 |
pp_node_args ind.nodei_outputs |
168 |
(fun fmt -> if ind.nodei_stateless then Format.fprintf fmt "stateless") |
169 |
|
170 |
let pp_imported_fun fmt ind = |
171 |
fprintf fmt "@[<v>function %s (%a) returns (%a)@]" |
172 |
ind.fun_id |
173 |
pp_node_args ind.fun_inputs |
174 |
pp_node_args ind.fun_outputs |
175 |
|
176 |
let pp_decl fmt decl = |
177 |
match decl.top_decl_desc with |
178 |
| Node nd -> fprintf fmt "%a@ " pp_node nd |
179 |
| ImportedNode ind -> |
180 |
fprintf fmt "imported %a;@ " pp_imported_node ind |
181 |
| ImportedFun ind -> |
182 |
fprintf fmt "%a;@ " pp_imported_fun ind |
183 |
| Consts clist -> ( |
184 |
fprintf fmt "const %a@ " |
185 |
(fprintf_list ~sep:"@ " (fun fmt cdecl -> |
186 |
fprintf fmt "%s = %a;" |
187 |
cdecl.const_id pp_const cdecl.const_value)) clist) |
188 |
| Include s -> fprintf fmt "include %s" s |
189 |
|
190 |
|
191 |
let pp_prog fmt prog = |
192 |
fprintf_list ~sep:"@ " pp_decl fmt prog |
193 |
|
194 |
let pp_short_decl fmt decl = |
195 |
match decl.top_decl_desc with |
196 |
| Node nd -> fprintf fmt "node %s@ " nd.node_id |
197 |
| ImportedNode ind -> fprintf fmt "imported node %s" ind.nodei_id |
198 |
| ImportedFun ind -> fprintf fmt "function %s" ind.fun_id |
199 |
| Consts clist -> ( |
200 |
fprintf fmt "const %a@ " |
201 |
(fprintf_list ~sep:"@ " (fun fmt cdecl -> |
202 |
pp_print_string fmt cdecl.const_id)) clist) |
203 |
| Include s -> fprintf fmt "include %s" s |
204 |
|
205 |
|
206 |
|
207 |
let pp_econst fmt c = |
208 |
match c with |
209 |
| EConst_int i -> pp_print_int fmt i |
210 |
| EConst_real r -> pp_print_string fmt r |
211 |
| EConst_float r -> pp_print_float fmt r |
212 |
| EConst_bool b -> pp_print_bool fmt b |
213 |
| EConst_string s -> pp_print_string fmt ("\"" ^ s ^ "\"") |
214 |
|
215 |
let rec pp_eexpr is_output fmt eexpr = |
216 |
let pp_eexpr = pp_eexpr is_output in |
217 |
match eexpr.eexpr_desc with |
218 |
| EExpr_const c -> pp_econst fmt c |
219 |
| EExpr_ident id -> |
220 |
if is_output id then pp_print_string fmt ("*" ^ id) else pp_print_string fmt id |
221 |
| EExpr_tuple el -> fprintf_list ~sep:"," pp_eexpr fmt el |
222 |
| EExpr_arrow (e1, e2) -> fprintf fmt "%a -> %a" pp_eexpr e1 pp_eexpr e2 |
223 |
| EExpr_fby (e1, e2) -> fprintf fmt "%a fby %a" pp_eexpr e1 pp_eexpr e2 |
224 |
| EExpr_concat (e1, e2) -> fprintf fmt "%a::%a" pp_eexpr e1 pp_eexpr e2 |
225 |
| EExpr_tail e -> fprintf fmt "tail %a" pp_eexpr e |
226 |
| EExpr_pre e -> fprintf fmt "pre %a" pp_eexpr e |
227 |
| EExpr_when (e, id) -> fprintf fmt "%a when %s" pp_eexpr e id |
228 |
| EExpr_merge (id, e1, e2) -> |
229 |
fprintf fmt "merge (%s, %a, %a)" id pp_eexpr e1 pp_eexpr e2 |
230 |
| EExpr_appl (id, e, r) -> pp_eapp is_output fmt id e r |
231 |
| EExpr_forall (vars, e) -> fprintf fmt "forall %a; %a" pp_node_args vars pp_eexpr e |
232 |
| EExpr_exists (vars, e) -> fprintf fmt "exists %a; %a" pp_node_args vars pp_eexpr e |
233 |
|
234 |
|
235 |
| EExpr_whennot _ |
236 |
| EExpr_uclock _ |
237 |
| EExpr_dclock _ |
238 |
| EExpr_phclock _ -> assert false |
239 |
and pp_eapp is_output fmt id e r = |
240 |
let pp_eexpr = pp_eexpr is_output in |
241 |
match r with |
242 |
| None -> |
243 |
(match id, e.eexpr_desc with |
244 |
| "+", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a + %a)" pp_eexpr e1 pp_eexpr e2 |
245 |
| "uminus", _ -> fprintf fmt "(- %a)" pp_eexpr e |
246 |
| "-", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a - %a)" pp_eexpr e1 pp_eexpr e2 |
247 |
| "*", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a * %a)" pp_eexpr e1 pp_eexpr e2 |
248 |
| "/", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a / %a)" pp_eexpr e1 pp_eexpr e2 |
249 |
| "mod", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a mod %a)" pp_eexpr e1 pp_eexpr e2 |
250 |
| "&&", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a && %a)" pp_eexpr e1 pp_eexpr e2 |
251 |
| "||", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a || %a)" pp_eexpr e1 pp_eexpr e2 |
252 |
| "xor", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a ^^ %a)" pp_eexpr e1 pp_eexpr e2 |
253 |
| "impl", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a ==> %a)" pp_eexpr e1 pp_eexpr e2 |
254 |
| "<", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a < %a)" pp_eexpr e1 pp_eexpr e2 |
255 |
| "<=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a <= %a)" pp_eexpr e1 pp_eexpr e2 |
256 |
| ">", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a > %a)" pp_eexpr e1 pp_eexpr e2 |
257 |
| ">=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a >= %a)" pp_eexpr e1 pp_eexpr e2 |
258 |
| "!=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a != %a)" pp_eexpr e1 pp_eexpr e2 |
259 |
| "=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a == %a)" pp_eexpr e1 pp_eexpr e2 |
260 |
| "not", _ -> fprintf fmt "(! %a)" pp_eexpr e |
261 |
| "ite", EExpr_tuple([e1;e2;e3]) -> fprintf fmt "(if %a then %a else %a)" pp_eexpr e1 pp_eexpr e2 pp_eexpr e3 |
262 |
| _ -> fprintf fmt "%s (%a)" id pp_eexpr e) |
263 |
| Some x -> fprintf fmt "%s (%a) every %s" id pp_eexpr e x |
264 |
|
265 |
|
266 |
let pp_ensures is_output fmt e = |
267 |
let pp_eexpr = pp_eexpr is_output in |
268 |
match e with |
269 |
| EnsuresExpr e -> fprintf fmt "ensures %a;@ " pp_eexpr e |
270 |
| SpecObserverNode (name, args) -> fprintf fmt "observer %s (%a);@ " name (fprintf_list ~sep:", " pp_eexpr) args |
271 |
|
272 |
let pp_acsl_spec outputs fmt spec = |
273 |
let is_output = fun oid -> List.exists (fun v -> v.var_id = oid) outputs in |
274 |
let pp_eexpr = pp_eexpr is_output in |
275 |
fprintf fmt "@[<v 2>/*@@ "; |
276 |
fprintf_list ~sep:"" (fun fmt r -> fprintf fmt "requires %a;@ " pp_eexpr r) fmt spec.requires; |
277 |
fprintf_list ~sep:"" (pp_ensures is_output) fmt spec.ensures; |
278 |
fprintf fmt "@ "; |
279 |
(* fprintf fmt "assigns *self%t%a;@ " *) |
280 |
(* (fun fmt -> if List.length outputs > 0 then fprintf fmt ", ") *) |
281 |
(* (fprintf_list ~sep:"," (fun fmt v -> fprintf fmt "*%s" v.var_id)) outputs; *) |
282 |
fprintf_list ~sep:"@ " (fun fmt (name, assumes, requires) -> |
283 |
fprintf fmt "behavior %s:@[@ %a@ %a@]" |
284 |
name |
285 |
(fprintf_list ~sep:"@ " (fun fmt r -> fprintf fmt "assumes %a;" pp_eexpr r)) assumes |
286 |
(fprintf_list ~sep:"@ " (pp_ensures is_output)) requires |
287 |
) fmt spec.behaviors; |
288 |
fprintf fmt "@]@ */@."; |
289 |
() |
290 |
(* Local Variables: *) |
291 |
(* compile-command:"make -C .." *) |
292 |
(* End: *) |