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