Revision 36454535
Added by Pierre-Loïc Garoche over 10 years ago
src/printers.ml | ||
---|---|---|
40 | 40 |
|
41 | 41 |
let pp_eq_lhs = fprintf_list ~sep:", " pp_print_string |
42 | 42 |
|
43 |
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 |
|
44 |
|
|
45 |
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 |
|
46 |
|
|
47 |
let pp_node_args = fprintf_list ~sep:"; " pp_node_var |
|
48 |
|
|
49 |
let pp_quantifiers fmt (q, vars) = |
|
50 |
match q with |
|
51 |
| Forall -> fprintf fmt "forall %a" (fprintf_list ~sep:"; " pp_var) vars |
|
52 |
| Exists -> fprintf fmt "exists %a" (fprintf_list ~sep:"; " pp_var) vars |
|
53 |
|
|
54 |
(* |
|
55 |
let pp_econst fmt c = |
|
56 |
match c with |
|
57 |
| EConst_int i -> pp_print_int fmt i |
|
58 |
| EConst_real r -> pp_print_string fmt r |
|
59 |
| EConst_float r -> pp_print_float fmt r |
|
60 |
| EConst_tag t -> pp_print_string fmt t |
|
61 |
| EConst_string s -> pp_print_string fmt ("\"" ^ s ^ "\"") |
|
62 |
|
|
63 |
|
|
64 |
let rec pp_eexpr fmt eexpr = |
|
65 |
match eexpr.eexpr_desc with |
|
66 |
| EExpr_const c -> pp_econst fmt c |
|
67 |
| EExpr_ident id -> pp_print_string fmt id |
|
68 |
| EExpr_tuple el -> fprintf_list ~sep:"," pp_eexpr fmt el |
|
69 |
| EExpr_arrow (e1, e2) -> fprintf fmt "%a -> %a" pp_eexpr e1 pp_eexpr e2 |
|
70 |
| EExpr_fby (e1, e2) -> fprintf fmt "%a fby %a" pp_eexpr e1 pp_eexpr e2 |
|
71 |
(* | EExpr_concat (e1, e2) -> fprintf fmt "%a::%a" pp_eexpr e1 pp_eexpr e2 *) |
|
72 |
(* | EExpr_tail e -> fprintf fmt "tail %a" pp_eexpr e *) |
|
73 |
| EExpr_pre e -> fprintf fmt "pre %a" pp_eexpr e |
|
74 |
| EExpr_when (e, id) -> fprintf fmt "%a when %s" pp_eexpr e id |
|
75 |
| EExpr_merge (id, e1, e2) -> |
|
76 |
fprintf fmt "merge (%s, %a, %a)" id pp_eexpr e1 pp_eexpr e2 |
|
77 |
| EExpr_appl (id, e, r) -> pp_eapp fmt id e r |
|
78 |
| EExpr_forall (vars, e) -> fprintf fmt "forall %a; %a" pp_node_args vars pp_eexpr e |
|
79 |
| EExpr_exists (vars, e) -> fprintf fmt "exists %a; %a" pp_node_args vars pp_eexpr e |
|
80 |
|
|
81 |
|
|
82 |
(* | EExpr_whennot _ *) |
|
83 |
(* | EExpr_uclock _ *) |
|
84 |
(* | EExpr_dclock _ *) |
|
85 |
(* | EExpr_phclock _ -> assert false *) |
|
86 |
and pp_eapp fmt id e r = |
|
87 |
match r with |
|
88 |
| None -> |
|
89 |
(match id, e.eexpr_desc with |
|
90 |
| "+", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a + %a)" pp_eexpr e1 pp_eexpr e2 |
|
91 |
| "uminus", _ -> fprintf fmt "(- %a)" pp_eexpr e |
|
92 |
| "-", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a - %a)" pp_eexpr e1 pp_eexpr e2 |
|
93 |
| "*", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a * %a)" pp_eexpr e1 pp_eexpr e2 |
|
94 |
| "/", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a / %a)" pp_eexpr e1 pp_eexpr e2 |
|
95 |
| "mod", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a mod %a)" pp_eexpr e1 pp_eexpr e2 |
|
96 |
| "&&", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a && %a)" pp_eexpr e1 pp_eexpr e2 |
|
97 |
| "||", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a || %a)" pp_eexpr e1 pp_eexpr e2 |
|
98 |
| "xor", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a ^^ %a)" pp_eexpr e1 pp_eexpr e2 |
|
99 |
| "impl", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a ==> %a)" pp_eexpr e1 pp_eexpr e2 |
|
100 |
| "<", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a < %a)" pp_eexpr e1 pp_eexpr e2 |
|
101 |
| "<=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a <= %a)" pp_eexpr e1 pp_eexpr e2 |
|
102 |
| ">", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a > %a)" pp_eexpr e1 pp_eexpr e2 |
|
103 |
| ">=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a >= %a)" pp_eexpr e1 pp_eexpr e2 |
|
104 |
| "!=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a != %a)" pp_eexpr e1 pp_eexpr e2 |
|
105 |
| "=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a == %a)" pp_eexpr e1 pp_eexpr e2 |
|
106 |
| "not", _ -> fprintf fmt "(! %a)" pp_eexpr e |
|
107 |
| "ite", EExpr_tuple([e1;e2;e3]) -> fprintf fmt "(if %a then %a else %a)" pp_eexpr e1 pp_eexpr e2 pp_eexpr e3 |
|
108 |
| _ -> fprintf fmt "%s (%a)" id pp_eexpr e) |
|
109 |
| Some x -> fprintf fmt "%s (%a) every %s" id pp_eexpr e x |
|
110 |
*) |
|
111 |
|
|
112 |
|
|
43 | 113 |
let rec pp_struct_const_field fmt (label, c) = |
44 | 114 |
fprintf fmt "%a = %a;" pp_print_string label pp_const c |
45 | 115 |
and pp_const fmt c = |
... | ... | |
52 | 122 |
| Const_struct fl -> Format.fprintf fmt "{%a }" (Utils.fprintf_list ~sep:" " pp_struct_const_field) fl |
53 | 123 |
| Const_string s -> pp_print_string fmt ("\"" ^ s ^ "\"") |
54 | 124 |
|
55 |
and 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 |
|
56 |
|
|
57 |
and 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 |
|
58 | 125 |
|
59 |
and pp_expr fmt expr = |
|
60 |
match expr.expr_desc with |
|
126 |
let rec pp_expr fmt expr = |
|
127 |
(match expr.expr_annot with |
|
128 |
| None -> fprintf fmt "%t" |
|
129 |
| Some ann -> fprintf fmt "(%a %t)" pp_expr_annot ann) |
|
130 |
(fun fmt -> |
|
131 |
match expr.expr_desc with |
|
61 | 132 |
| Expr_const c -> pp_const fmt c |
62 | 133 |
| Expr_ident id -> Format.fprintf fmt "%s" id |
63 | 134 |
| Expr_array a -> fprintf fmt "[%a]" pp_tuple a |
... | ... | |
72 | 143 |
| Expr_merge (id, hl) -> |
73 | 144 |
fprintf fmt "merge %s %a" id pp_handlers hl |
74 | 145 |
| Expr_appl (id, e, r) -> pp_app fmt id e r |
75 |
|
|
146 |
) |
|
76 | 147 |
and pp_tuple fmt el = |
77 | 148 |
fprintf_list ~sep:"," pp_expr fmt el |
78 | 149 |
|
... | ... | |
107 | 178 |
| _ -> fprintf fmt "%s (%a)" id pp_expr e |
108 | 179 |
) |
109 | 180 |
| Some (x, l) -> fprintf fmt "%s (%a) every %s(%s)" id pp_expr e l x |
181 |
|
|
182 |
|
|
183 |
|
|
184 |
and pp_eexpr fmt e = |
|
185 |
fprintf fmt "%a%t %a" |
|
186 |
(Utils.fprintf_list ~sep:"; " pp_quantifiers) e.eexpr_quantifiers |
|
187 |
(fun fmt -> match e.eexpr_quantifiers with [] -> () | _ -> fprintf fmt ";") |
|
188 |
pp_expr e.eexpr_qfexpr |
|
189 |
|
|
190 |
|
|
191 |
and pp_expr_annot fmt expr_ann = |
|
192 |
let pp_annot fmt (kwds, ee) = |
|
193 |
Format.fprintf fmt "(*! %t: %a *)" |
|
194 |
(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) |
|
195 |
pp_eexpr ee |
|
196 |
in |
|
197 |
fprintf_list ~sep:"@ " pp_annot fmt expr_ann.annots |
|
198 |
|
|
110 | 199 |
|
111 | 200 |
let pp_node_eq fmt eq = |
112 | 201 |
fprintf fmt "%a = %a;" |
... | ... | |
115 | 204 |
|
116 | 205 |
let pp_node_eqs = fprintf_list ~sep:"@ " pp_node_eq |
117 | 206 |
|
118 |
let pp_node_args = fprintf_list ~sep:"; " pp_node_var |
|
119 | 207 |
|
120 | 208 |
let pp_var_type_dec fmt ty = |
121 | 209 |
let rec pp_var_struct_type_field fmt (label, tdesc) = |
... | ... | |
146 | 234 |
(* ) *) |
147 | 235 |
|
148 | 236 |
|
149 |
|
|
150 |
let pp_quantifiers fmt (q, vars) = |
|
151 |
match q with |
|
152 |
| Forall -> fprintf fmt "forall %a" (fprintf_list ~sep:"; " pp_var) vars |
|
153 |
| Exists -> fprintf fmt "exists %a" (fprintf_list ~sep:"; " pp_var) vars |
|
154 |
|
|
155 |
let pp_eexpr fmt e = |
|
156 |
fprintf fmt "%a%t %a" |
|
157 |
(Utils.fprintf_list ~sep:"; " pp_quantifiers) e.eexpr_quantifiers |
|
158 |
(fun fmt -> match e.eexpr_quantifiers with [] -> () | _ -> fprintf fmt ";") |
|
159 |
pp_expr e.eexpr_qfexpr |
|
160 |
|
|
161 | 237 |
let pp_spec fmt spec = |
162 | 238 |
fprintf fmt "@[<hov 2>(*@@ "; |
163 | 239 |
fprintf_list ~sep:"@;@@ " (fun fmt r -> fprintf fmt "requires %a;" pp_eexpr r) fmt spec.requires; |
... | ... | |
171 | 247 |
fprintf fmt "@]*)"; |
172 | 248 |
() |
173 | 249 |
|
250 |
|
|
251 |
let pp_asserts fmt asserts = |
|
252 |
match asserts with |
|
253 |
| _::_ -> ( |
|
254 |
fprintf fmt "(* Asserts definitions *)@ "; |
|
255 |
fprintf_list ~sep:"@ " (fun fmt assert_ -> |
|
256 |
let expr = assert_.assert_expr in |
|
257 |
fprintf fmt "assert %a;" pp_expr expr |
|
258 |
) fmt asserts |
|
259 |
) |
|
260 |
| _ -> () |
|
261 |
|
|
174 | 262 |
let pp_node fmt nd = |
175 |
fprintf fmt "@[<v 0>%a%t%s %s (%a) returns (%a)@.%a%alet@.@[<h 2> @ @[<v>%a@]@ @]@.tel@]@." |
|
263 |
fprintf fmt "@[<v 0>%a%t%s %s (%a) returns (%a)@.%a%alet@.@[<h 2> @ @[<v>%a@ %a@ %a@]@ @]@.tel@]@."
|
|
176 | 264 |
(fun fmt s -> match s with Some s -> pp_spec fmt s | _ -> ()) nd.node_spec |
177 | 265 |
(fun fmt -> match nd.node_spec with None -> () | Some _ -> Format.fprintf fmt "@.") |
178 | 266 |
(if nd.node_dec_stateless then "function" else "node") |
... | ... | |
193 | 281 |
(fun fmt d -> fprintf fmt "%a" Dimension.pp_dimension d)) |
194 | 282 |
checks |
195 | 283 |
) nd.node_checks |
284 |
(fprintf_list ~sep:"@ " pp_expr_annot) nd.node_annot |
|
196 | 285 |
pp_node_eqs nd.node_eqs |
286 |
pp_asserts nd.node_asserts |
|
197 | 287 |
(*fprintf fmt "@ /* Scheduling: %a */ @ " (fprintf_list ~sep:", " pp_print_string) (Scheduling.schedule_node nd)*) |
198 | 288 |
|
199 | 289 |
let pp_imported_node fmt ind = |
Also available in: Unified diff
Merged horn_traces branch