Revision ca7ff3f7
Added by Lélio Brun over 1 year ago
src/backends/Horn/horn_backend_printers.ml | ||
---|---|---|
12 | 12 |
(* The compilation presented here was first defined in Garoche, Gurfinkel, |
13 | 13 |
Kahsai, HCSV'14. |
14 | 14 |
|
15 |
This is a modified version that handle reset |
|
16 |
*) |
|
15 |
This is a modified version that handle reset *) |
|
17 | 16 |
|
18 | 17 |
open Format |
19 | 18 |
open Lustre_types |
20 | 19 |
open Machine_code_types |
21 | 20 |
open Corelang |
22 | 21 |
open Machine_code_common |
23 |
|
|
24 | 22 |
open Horn_backend_common |
25 |
|
|
23 |
|
|
26 | 24 |
(********************************************************************************************) |
27 |
(* Instruction Printing functions *)
|
|
25 |
(* Instruction Printing functions *)
|
|
28 | 26 |
(********************************************************************************************) |
29 | 27 |
|
30 | 28 |
let pp_horn_var _ fmt id = |
31 |
(*if Types.is_array_type id.var_type |
|
32 |
then |
|
33 |
assert false (* no arrays in Horn output *) |
|
34 |
else*) |
|
35 |
fprintf fmt "%s" id.var_id |
|
29 |
(*if Types.is_array_type id.var_type then assert false (* no arrays in Horn |
|
30 |
output *) else*) |
|
31 |
fprintf fmt "%s" id.var_id |
|
36 | 32 |
|
37 | 33 |
(* Used to print boolean constants *) |
38 | 34 |
let pp_horn_tag fmt t = |
39 |
pp_print_string fmt (if t = tag_true then "true" else if t = tag_false then "false" else t) |
|
40 |
|
|
35 |
pp_print_string fmt |
|
36 |
(if t = tag_true then "true" else if t = tag_false then "false" else t) |
|
37 |
|
|
41 | 38 |
(* Prints a constant value *) |
42 | 39 |
let pp_horn_const fmt c = |
43 | 40 |
match c with |
44 |
| Const_int i -> pp_print_int fmt i |
|
45 |
| Const_real r -> Real.pp fmt r |
|
46 |
| Const_tag t -> pp_horn_tag fmt t |
|
47 |
| _ -> assert false |
|
41 |
| Const_int i -> |
|
42 |
pp_print_int fmt i |
|
43 |
| Const_real r -> |
|
44 |
Real.pp fmt r |
|
45 |
| Const_tag t -> |
|
46 |
pp_horn_tag fmt t |
|
47 |
| _ -> |
|
48 |
assert false |
|
48 | 49 |
|
49 | 50 |
(* Default value for each type, used when building arrays. Eg integer array |
50 | 51 |
[2;7] is defined as (store (store (0) 1 7) 0 2) where 0 is this default value |
51 |
for the type integer (arrays). |
|
52 |
*) |
|
52 |
for the type integer (arrays). *) |
|
53 | 53 |
let rec pp_default_val fmt t = |
54 | 54 |
let t = Types.dynamic_type t in |
55 |
if Types.is_bool_type t then fprintf fmt "true" else |
|
56 |
if Types.is_int_type t then fprintf fmt "0" else |
|
57 |
if Types.is_real_type t then fprintf fmt "0" else |
|
58 |
match (Types.dynamic_type t).Types.tdesc with |
|
59 |
| Types.Tarray _ -> (* TODO PL: this strange code has to be (heavily) checked *) |
|
60 |
let valt = Types.array_element_type t in |
|
61 |
fprintf fmt "((as const (Array Int %a)) %a)" |
|
62 |
pp_type valt |
|
63 |
pp_default_val valt |
|
64 |
| Types.Tstruct _ -> assert false |
|
65 |
| Types.Ttuple _ -> assert false |
|
66 |
|_ -> assert false |
|
55 |
if Types.is_bool_type t then fprintf fmt "true" |
|
56 |
else if Types.is_int_type t then fprintf fmt "0" |
|
57 |
else if Types.is_real_type t then fprintf fmt "0" |
|
58 |
else |
|
59 |
match (Types.dynamic_type t).Types.tdesc with |
|
60 |
| Types.Tarray _ -> |
|
61 |
(* TODO PL: this strange code has to be (heavily) checked *) |
|
62 |
let valt = Types.array_element_type t in |
|
63 |
fprintf fmt "((as const (Array Int %a)) %a)" pp_type valt pp_default_val |
|
64 |
valt |
|
65 |
| Types.Tstruct _ -> |
|
66 |
assert false |
|
67 |
| Types.Ttuple _ -> |
|
68 |
assert false |
|
69 |
| _ -> |
|
70 |
assert false |
|
67 | 71 |
|
68 | 72 |
let pp_mod pp_val v1 v2 fmt = |
69 |
if Types.is_int_type v1.value_type && not !Options.integer_div_euclidean then |
|
70 |
(* C semantics: converting it from Euclidean operators |
|
71 |
(a mod_M b) - ((a mod_M b > 0 && a < 0) ? abs(b) : 0) |
|
72 |
*) |
|
73 |
Format.fprintf fmt "(- (mod %a %a) (ite (and (> (mod %a %a) 0) (< %a 0)) (abs %a) 0))" |
|
74 |
pp_val v1 pp_val v2 |
|
75 |
pp_val v1 pp_val v2 |
|
76 |
pp_val v1 |
|
77 |
pp_val v2 |
|
78 |
else |
|
79 |
Format.fprintf fmt "(mod %a %a)" pp_val v1 pp_val v2 |
|
73 |
if Types.is_int_type v1.value_type && not !Options.integer_div_euclidean then |
|
74 |
(* C semantics: converting it from Euclidean operators (a mod_M b) - ((a |
|
75 |
mod_M b > 0 && a < 0) ? abs(b) : 0) *) |
|
76 |
Format.fprintf fmt |
|
77 |
"(- (mod %a %a) (ite (and (> (mod %a %a) 0) (< %a 0)) (abs %a) 0))" pp_val |
|
78 |
v1 pp_val v2 pp_val v1 pp_val v2 pp_val v1 pp_val v2 |
|
79 |
else Format.fprintf fmt "(mod %a %a)" pp_val v1 pp_val v2 |
|
80 | 80 |
|
81 | 81 |
let pp_div pp_val v1 v2 fmt = |
82 |
if Types.is_int_type v1.value_type && not !Options.integer_div_euclidean then |
|
83 |
(* C semantics: converting it from Euclidean operators |
|
84 |
(a - (a mod_C b)) div_M b |
|
85 |
*) |
|
86 |
Format.fprintf fmt "(div (- %a %t) %a)" |
|
87 |
pp_val v1 |
|
88 |
(pp_mod pp_val v1 v2) |
|
82 |
if Types.is_int_type v1.value_type && not !Options.integer_div_euclidean then |
|
83 |
(* C semantics: converting it from Euclidean operators (a - (a mod_C b)) |
|
84 |
div_M b *) |
|
85 |
Format.fprintf fmt "(div (- %a %t) %a)" pp_val v1 (pp_mod pp_val v1 v2) |
|
89 | 86 |
pp_val v2 |
90 |
else |
|
91 |
Format.fprintf fmt "(div %a %a)" pp_val v1 pp_val v2 |
|
92 |
|
|
87 |
else Format.fprintf fmt "(div %a %a)" pp_val v1 pp_val v2 |
|
93 | 88 |
|
94 | 89 |
let pp_basic_lib_fun i pp_val fmt vl = |
95 | 90 |
match i, vl with |
96 |
| "ite", [v1; v2; v3] -> Format.fprintf fmt "(@[<hov 2>ite %a@ %a@ %a@])" pp_val v1 pp_val v2 pp_val v3 |
|
97 |
| "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v |
|
98 |
| "not", [v] -> Format.fprintf fmt "(not %a)" pp_val v |
|
99 |
| "=", [v1; v2] -> Format.fprintf fmt "(= %a %a)" pp_val v1 pp_val v2 |
|
100 |
| "&&", [v1; v2] -> Format.fprintf fmt "(and %a %a)" pp_val v1 pp_val v2 |
|
101 |
| "||", [v1; v2] -> Format.fprintf fmt "(or %a %a)" pp_val v1 pp_val v2 |
|
102 |
| "impl", [v1; v2] -> Format.fprintf fmt "(=> %a %a)" pp_val v1 pp_val v2 |
|
103 |
| "equi", [v1; v2] -> Format.fprintf fmt "(%a = %a)" pp_val v1 pp_val v2 |
|
104 |
| "xor", [v1; v2] -> Format.fprintf fmt "(%a xor %a)" pp_val v1 pp_val v2 |
|
105 |
| "!=", [v1; v2] -> Format.fprintf fmt "(not (= %a %a))" pp_val v1 pp_val v2 |
|
106 |
| "mod", [v1; v2] -> pp_mod pp_val v1 v2 fmt |
|
107 |
| "/", [v1; v2] -> pp_div pp_val v1 v2 fmt |
|
108 |
| _, [v1; v2] -> Format.fprintf fmt "(%s %a %a)" i pp_val v1 pp_val v2 |
|
109 |
| _ -> (Format.eprintf "internal error: Basic_library.pp_horn %s@." i; assert false) |
|
110 |
(* | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2 |
|
111 |
|
|
112 |
*) |
|
113 |
|
|
114 |
|
|
115 |
(* Prints a value expression [v], with internal function calls only. |
|
116 |
[pp_var] is a printer for variables (typically [pp_c_var_read]), |
|
117 |
but an offset suffix may be added for array variables |
|
118 |
*) |
|
119 |
let rec pp_horn_val ?(is_lhs=false) m self pp_var fmt v = |
|
120 |
match v.value_desc with |
|
121 |
| Cst c -> pp_horn_const fmt c |
|
91 |
| "ite", [ v1; v2; v3 ] -> |
|
92 |
Format.fprintf fmt "(@[<hov 2>ite %a@ %a@ %a@])" pp_val v1 pp_val v2 pp_val |
|
93 |
v3 |
|
94 |
| "uminus", [ v ] -> |
|
95 |
Format.fprintf fmt "(- %a)" pp_val v |
|
96 |
| "not", [ v ] -> |
|
97 |
Format.fprintf fmt "(not %a)" pp_val v |
|
98 |
| "=", [ v1; v2 ] -> |
|
99 |
Format.fprintf fmt "(= %a %a)" pp_val v1 pp_val v2 |
|
100 |
| "&&", [ v1; v2 ] -> |
|
101 |
Format.fprintf fmt "(and %a %a)" pp_val v1 pp_val v2 |
|
102 |
| "||", [ v1; v2 ] -> |
|
103 |
Format.fprintf fmt "(or %a %a)" pp_val v1 pp_val v2 |
|
104 |
| "impl", [ v1; v2 ] -> |
|
105 |
Format.fprintf fmt "(=> %a %a)" pp_val v1 pp_val v2 |
|
106 |
| "equi", [ v1; v2 ] -> |
|
107 |
Format.fprintf fmt "(%a = %a)" pp_val v1 pp_val v2 |
|
108 |
| "xor", [ v1; v2 ] -> |
|
109 |
Format.fprintf fmt "(%a xor %a)" pp_val v1 pp_val v2 |
|
110 |
| "!=", [ v1; v2 ] -> |
|
111 |
Format.fprintf fmt "(not (= %a %a))" pp_val v1 pp_val v2 |
|
112 |
| "mod", [ v1; v2 ] -> |
|
113 |
pp_mod pp_val v1 v2 fmt |
|
114 |
| "/", [ v1; v2 ] -> |
|
115 |
pp_div pp_val v1 v2 fmt |
|
116 |
| _, [ v1; v2 ] -> |
|
117 |
Format.fprintf fmt "(%s %a %a)" i pp_val v1 pp_val v2 |
|
118 |
| _ -> |
|
119 |
Format.eprintf "internal error: Basic_library.pp_horn %s@." i; |
|
120 |
assert false |
|
121 |
(* | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2 *) |
|
122 | 122 |
|
123 |
(* Prints a value expression [v], with internal function calls only. [pp_var] is |
|
124 |
a printer for variables (typically [pp_c_var_read]), but an offset suffix may |
|
125 |
be added for array variables *) |
|
126 |
let rec pp_horn_val ?(is_lhs = false) m self pp_var fmt v = |
|
127 |
match v.value_desc with |
|
128 |
| Cst c -> |
|
129 |
pp_horn_const fmt c |
|
123 | 130 |
(* Code specific for arrays *) |
124 |
| Array il -> |
|
125 |
(* An array definition: |
|
126 |
(store ( |
|
127 |
... |
|
128 |
(store ( |
|
129 |
store ( |
|
130 |
default_val |
|
131 |
) |
|
132 |
idx_n val_n |
|
133 |
) |
|
134 |
idx_n-1 val_n-1) |
|
135 |
... |
|
136 |
idx_1 val_1 |
|
137 |
) *) |
|
138 |
let rec print fmt (tab, x) = |
|
139 |
match tab with |
|
140 |
| [] -> pp_default_val fmt v.value_type(* (get_type v) *) |
|
141 |
| h::t -> |
|
142 |
fprintf fmt "(store %a %i %a)" |
|
143 |
print (t, (x+1)) |
|
144 |
x |
|
145 |
(pp_horn_val ~is_lhs:is_lhs m self pp_var) h |
|
146 |
in |
|
147 |
print fmt (il, 0) |
|
148 |
|
|
149 |
| Access(tab,index) -> |
|
150 |
fprintf fmt "(select %a %a)" |
|
151 |
(pp_horn_val ~is_lhs:is_lhs m self pp_var) tab |
|
152 |
(pp_horn_val ~is_lhs:is_lhs m self pp_var) index |
|
153 |
|
|
131 |
| Array il -> |
|
132 |
(* An array definition: (store ( ... (store ( store ( default_val ) idx_n |
|
133 |
val_n ) idx_n-1 val_n-1) ... idx_1 val_1 ) *) |
|
134 |
let rec print fmt (tab, x) = |
|
135 |
match tab with |
|
136 |
| [] -> |
|
137 |
pp_default_val fmt v.value_type (* (get_type v) *) |
|
138 |
| h :: t -> |
|
139 |
fprintf fmt "(store %a %i %a)" print |
|
140 |
(t, x + 1) |
|
141 |
x |
|
142 |
(pp_horn_val ~is_lhs m self pp_var) |
|
143 |
h |
|
144 |
in |
|
145 |
print fmt (il, 0) |
|
146 |
| Access (tab, index) -> |
|
147 |
fprintf fmt "(select %a %a)" |
|
148 |
(pp_horn_val ~is_lhs m self pp_var) |
|
149 |
tab |
|
150 |
(pp_horn_val ~is_lhs m self pp_var) |
|
151 |
index |
|
154 | 152 |
(* Code specific for arrays *) |
155 |
|
|
156 |
| Power _ -> assert false |
|
157 |
| Var v -> |
|
158 |
if is_memory m v then |
|
159 |
if Types.is_array_type v.var_type |
|
160 |
then assert false |
|
161 |
else pp_var fmt (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v)) |
|
162 |
else |
|
163 |
pp_var fmt (rename_machine self v) |
|
164 |
|
|
165 |
| Fun (n, vl) -> fprintf fmt "%a" (pp_basic_lib_fun n (pp_horn_val m self pp_var)) vl |
|
153 |
| Power _ -> |
|
154 |
assert false |
|
155 |
| Var v -> |
|
156 |
if is_memory m v then |
|
157 |
if Types.is_array_type v.var_type then assert false |
|
158 |
else |
|
159 |
pp_var fmt |
|
160 |
(rename_machine self |
|
161 |
((if is_lhs then rename_next else rename_current (* self *)) v)) |
|
162 |
else pp_var fmt (rename_machine self v) |
|
163 |
| Fun (n, vl) -> |
|
164 |
fprintf fmt "%a" (pp_basic_lib_fun n (pp_horn_val m self pp_var)) vl |
|
166 | 165 |
| ResetFlag -> |
167 | 166 |
(* TODO: handle reset flag *) |
168 | 167 |
assert false |
169 | 168 |
|
170 | 169 |
(* Prints a [value] indexed by the suffix list [loop_vars] *) |
171 | 170 |
let rec pp_value_suffix m self pp_value fmt value = |
172 |
match value.value_desc with |
|
173 |
| Fun (n, vl) ->
|
|
171 |
match value.value_desc with
|
|
172 |
| Fun (n, vl) ->
|
|
174 | 173 |
pp_basic_lib_fun n (pp_value_suffix m self pp_value) fmt vl |
175 |
| _ -> |
|
176 |
pp_horn_val m self pp_value fmt value |
|
177 |
|
|
178 |
(* type_directed assignment: array vs. statically sized type |
|
179 |
- [var_type]: type of variable to be assigned |
|
180 |
- [var_name]: name of variable to be assigned |
|
181 |
- [value]: assigned value |
|
182 |
- [pp_var]: printer for variables |
|
183 |
*) |
|
174 |
| _ -> |
|
175 |
pp_horn_val m self pp_value fmt value |
|
176 |
|
|
177 |
(* type_directed assignment: array vs. statically sized type - [var_type]: type |
|
178 |
of variable to be assigned - [var_name]: name of variable to be assigned - |
|
179 |
[value]: assigned value - [pp_var]: printer for variables *) |
|
184 | 180 |
let pp_assign m pp_var fmt var_name value = |
185 | 181 |
let self = m.mname.node_id in |
186 |
fprintf fmt "(= %a %a)" |
|
187 |
(pp_horn_val ~is_lhs:true m self pp_var) var_name |
|
188 |
(pp_value_suffix m self pp_var) value |
|
189 |
|
|
182 |
fprintf fmt "(= %a %a)" |
|
183 |
(pp_horn_val ~is_lhs:true m self pp_var) |
|
184 |
var_name |
|
185 |
(pp_value_suffix m self pp_var) |
|
186 |
value |
|
190 | 187 |
|
191 | 188 |
(* In case of no reset call, we define mid_mem = current_mem *) |
192 | 189 |
let pp_no_reset machines m fmt i = |
193 |
let (n,_) = List.assoc i m.minstances in |
|
194 |
let target_machine = List.find (fun m -> m.mname.node_id = (node_name n)) machines in |
|
190 |
let n, _ = List.assoc i m.minstances in |
|
191 |
let target_machine = |
|
192 |
List.find (fun m -> m.mname.node_id = node_name n) machines |
|
193 |
in |
|
195 | 194 |
|
196 |
let m_list = |
|
197 |
rename_machine_list |
|
198 |
(concat m.mname.node_id i) |
|
195 |
let m_list = |
|
196 |
rename_machine_list (concat m.mname.node_id i) |
|
199 | 197 |
(rename_mid_list (full_memory_vars machines target_machine)) |
200 | 198 |
in |
201 | 199 |
let c_list = |
202 |
rename_machine_list |
|
203 |
(concat m.mname.node_id i) |
|
200 |
rename_machine_list (concat m.mname.node_id i) |
|
204 | 201 |
(rename_current_list (full_memory_vars machines target_machine)) |
205 | 202 |
in |
206 | 203 |
match c_list, m_list with |
207 |
| [chd], [mhd] -> |
|
208 |
fprintf fmt "(= %a %a)" |
|
209 |
(pp_horn_var m) mhd |
|
210 |
(pp_horn_var m) chd |
|
211 |
|
|
212 |
| _ -> ( |
|
204 |
| [ chd ], [ mhd ] -> |
|
205 |
fprintf fmt "(= %a %a)" (pp_horn_var m) mhd (pp_horn_var m) chd |
|
206 |
| _ -> |
|
213 | 207 |
fprintf fmt "@[<v 0>(and @[<v 0>"; |
214 |
List.iter2 (fun mhd chd -> |
|
215 |
fprintf fmt "(= %a %a)@ " |
|
216 |
(pp_horn_var m) mhd |
|
217 |
(pp_horn_var m) chd |
|
218 |
) |
|
219 |
m_list |
|
220 |
c_list ; |
|
208 |
List.iter2 |
|
209 |
(fun mhd chd -> |
|
210 |
fprintf fmt "(= %a %a)@ " (pp_horn_var m) mhd (pp_horn_var m) chd) |
|
211 |
m_list c_list; |
|
221 | 212 |
fprintf fmt ")@]@ @]" |
222 |
) |
|
223 | 213 |
|
224 | 214 |
let pp_instance_reset machines m fmt i = |
225 |
let (n,_) = List.assoc i m.minstances in |
|
226 |
let target_machine = List.find (fun m -> m.mname.node_id = (node_name n)) machines in |
|
227 |
|
|
228 |
fprintf fmt "(%a @[<v 0>%a)@]" |
|
229 |
pp_machine_reset_name (node_name n) |
|
230 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) |
|
231 |
( |
|
232 |
(rename_machine_list |
|
233 |
(concat m.mname.node_id i) |
|
234 |
(rename_current_list (full_memory_vars machines target_machine)) |
|
235 |
) |
|
236 |
@ |
|
237 |
(rename_machine_list |
|
238 |
(concat m.mname.node_id i) |
|
239 |
(rename_mid_list (full_memory_vars machines target_machine)) |
|
240 |
) |
|
241 |
) |
|
215 |
let n, _ = List.assoc i m.minstances in |
|
216 |
let target_machine = |
|
217 |
List.find (fun m -> m.mname.node_id = node_name n) machines |
|
218 |
in |
|
219 |
|
|
220 |
fprintf fmt "(%a @[<v 0>%a)@]" pp_machine_reset_name (node_name n) |
|
221 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) |
|
222 |
(rename_machine_list (concat m.mname.node_id i) |
|
223 |
(rename_current_list (full_memory_vars machines target_machine)) |
|
224 |
@ rename_machine_list (concat m.mname.node_id i) |
|
225 |
(rename_mid_list (full_memory_vars machines target_machine))) |
|
242 | 226 |
|
243 | 227 |
let pp_instance_call machines reset_instances m fmt i inputs outputs = |
244 | 228 |
let self = m.mname.node_id in |
245 |
try (* stateful node instance *) |
|
246 |
begin |
|
247 |
let (n,_) = List.assoc i m.minstances in |
|
248 |
let target_machine = List.find (fun m -> m.mname.node_id = node_name n) machines in |
|
249 |
(* Checking whether this specific instances has been reset yet *) |
|
250 |
if not (List.mem i reset_instances) then |
|
251 |
(* If not, declare mem_m = mem_c *) |
|
252 |
pp_no_reset machines m fmt i; |
|
253 |
|
|
254 |
let mems = full_memory_vars machines target_machine in |
|
255 |
let rename_mems f = rename_machine_list (concat m.mname.node_id i) (f mems) in |
|
256 |
let mid_mems = rename_mems rename_mid_list in |
|
257 |
let next_mems = rename_mems rename_next_list in |
|
258 |
|
|
259 |
match node_name n, inputs, outputs, mid_mems, next_mems with |
|
260 |
| "_arrow", [i1; i2], [o], [mem_m], [mem_x] -> begin |
|
261 |
fprintf fmt "@[<v 5>(and "; |
|
262 |
fprintf fmt "(= %a (ite %a %a %a))" |
|
263 |
(pp_horn_val ~is_lhs:true m self (pp_horn_var m)) (mk_val (Var o) o.var_type) (* output var *) |
|
264 |
(pp_horn_var m) mem_m |
|
265 |
(pp_horn_val m self (pp_horn_var m)) i1 |
|
266 |
(pp_horn_val m self (pp_horn_var m)) i2 |
|
267 |
; |
|
268 |
fprintf fmt "@ "; |
|
269 |
fprintf fmt "(= %a false)" (pp_horn_var m) mem_x; |
|
270 |
fprintf fmt ")@]" |
|
271 |
end |
|
272 |
|
|
273 |
| _ -> begin |
|
274 |
fprintf fmt "(%a @[<v 0>%a%t%a%t%a)@]" |
|
275 |
pp_machine_step_name (node_name n) |
|
276 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_val m self (pp_horn_var m))) inputs |
|
277 |
(Utils.pp_final_char_if_non_empty "@ " inputs) |
|
278 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_val m self (pp_horn_var m))) |
|
279 |
(List.map (fun v -> mk_val (Var v) v.var_type) outputs) |
|
280 |
(Utils.pp_final_char_if_non_empty "@ " outputs) |
|
281 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (mid_mems@next_mems) |
|
282 |
|
|
283 |
end |
|
284 |
end |
|
285 |
with Not_found -> ( (* stateless node instance *) |
|
286 |
let (n,_) = List.assoc i m.mcalls in |
|
287 |
fprintf fmt "(%a @[<v 0>%a%t%a)@]" |
|
288 |
pp_machine_stateless_name (node_name n) |
|
229 |
try |
|
230 |
(* stateful node instance *) |
|
231 |
let n, _ = List.assoc i m.minstances in |
|
232 |
let target_machine = |
|
233 |
List.find (fun m -> m.mname.node_id = node_name n) machines |
|
234 |
in |
|
235 |
(* Checking whether this specific instances has been reset yet *) |
|
236 |
if not (List.mem i reset_instances) then |
|
237 |
(* If not, declare mem_m = mem_c *) |
|
238 |
pp_no_reset machines m fmt i; |
|
239 |
|
|
240 |
let mems = full_memory_vars machines target_machine in |
|
241 |
let rename_mems f = |
|
242 |
rename_machine_list (concat m.mname.node_id i) (f mems) |
|
243 |
in |
|
244 |
let mid_mems = rename_mems rename_mid_list in |
|
245 |
let next_mems = rename_mems rename_next_list in |
|
246 |
|
|
247 |
match node_name n, inputs, outputs, mid_mems, next_mems with |
|
248 |
| "_arrow", [ i1; i2 ], [ o ], [ mem_m ], [ mem_x ] -> |
|
249 |
fprintf fmt "@[<v 5>(and "; |
|
250 |
fprintf fmt "(= %a (ite %a %a %a))" |
|
251 |
(pp_horn_val ~is_lhs:true m self (pp_horn_var m)) |
|
252 |
(mk_val (Var o) o.var_type) |
|
253 |
(* output var *) |
|
254 |
(pp_horn_var m) |
|
255 |
mem_m |
|
256 |
(pp_horn_val m self (pp_horn_var m)) |
|
257 |
i1 |
|
258 |
(pp_horn_val m self (pp_horn_var m)) |
|
259 |
i2; |
|
260 |
fprintf fmt "@ "; |
|
261 |
fprintf fmt "(= %a false)" (pp_horn_var m) mem_x; |
|
262 |
fprintf fmt ")@]" |
|
263 |
| _ -> |
|
264 |
fprintf fmt "(%a @[<v 0>%a%t%a%t%a)@]" pp_machine_step_name (node_name n) |
|
265 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_val m self (pp_horn_var m))) |
|
266 |
inputs |
|
267 |
(Utils.pp_final_char_if_non_empty "@ " inputs) |
|
268 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_val m self (pp_horn_var m))) |
|
269 |
(List.map (fun v -> mk_val (Var v) v.var_type) outputs) |
|
270 |
(Utils.pp_final_char_if_non_empty "@ " outputs) |
|
271 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) |
|
272 |
(mid_mems @ next_mems) |
|
273 |
with Not_found -> |
|
274 |
(* stateless node instance *) |
|
275 |
let n, _ = List.assoc i m.mcalls in |
|
276 |
fprintf fmt "(%a @[<v 0>%a%t%a)@]" pp_machine_stateless_name (node_name n) |
|
289 | 277 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_val m self (pp_horn_var m))) |
290 | 278 |
inputs |
291 | 279 |
(Utils.pp_final_char_if_non_empty "@ " inputs) |
292 | 280 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_val m self (pp_horn_var m))) |
293 | 281 |
(List.map (fun v -> mk_val (Var v) v.var_type) outputs) |
294 |
) |
|
295 |
|
|
296 |
|
|
282 |
|
|
297 | 283 |
(* Print the instruction and update the set of reset instances *) |
298 |
let rec pp_machine_instr machines reset_instances (m: machine_t) fmt instr : ident list = |
|
284 |
let rec pp_machine_instr machines reset_instances (m : machine_t) fmt instr : |
|
285 |
ident list = |
|
299 | 286 |
match get_instr_desc instr with |
300 |
| MSpec _ | MComment _ -> reset_instances |
|
287 |
| MSpec _ | MComment _ -> |
|
288 |
reset_instances |
|
301 | 289 |
(* TODO: handle reset flag *) |
302 |
| MResetAssign _ -> reset_instances |
|
290 |
| MResetAssign _ -> |
|
291 |
reset_instances |
|
303 | 292 |
(* TODO: handle clear_reset *) |
304 |
| MClearReset -> reset_instances |
|
305 |
| MNoReset i -> (* we assign middle_mem with mem_m. And declare i as reset *) |
|
293 |
| MClearReset -> |
|
294 |
reset_instances |
|
295 |
| MNoReset i -> |
|
296 |
(* we assign middle_mem with mem_m. And declare i as reset *) |
|
306 | 297 |
pp_no_reset machines m fmt i; |
307 |
i::reset_instances |
|
308 |
| MSetReset i -> (* we assign middle_mem with reset: reset(mem_m) *) |
|
298 |
i :: reset_instances |
|
299 |
| MSetReset i -> |
|
300 |
(* we assign middle_mem with reset: reset(mem_m) *) |
|
309 | 301 |
pp_instance_reset machines m fmt i; |
310 |
i::reset_instances |
|
311 |
| MLocalAssign (i,v) -> |
|
312 |
pp_assign |
|
313 |
m (pp_horn_var m) fmt |
|
314 |
(mk_val (Var i) i.var_type) v; |
|
302 |
i :: reset_instances |
|
303 |
| MLocalAssign (i, v) -> |
|
304 |
pp_assign m (pp_horn_var m) fmt (mk_val (Var i) i.var_type) v; |
|
315 | 305 |
reset_instances |
316 |
| MStateAssign (i,v) -> |
|
317 |
pp_assign |
|
318 |
m (pp_horn_var m) fmt |
|
319 |
(mk_val (Var i) i.var_type) v; |
|
306 |
| MStateAssign (i, v) -> |
|
307 |
pp_assign m (pp_horn_var m) fmt (mk_val (Var i) i.var_type) v; |
|
320 | 308 |
reset_instances |
321 |
| MStep ([_], i, vl) when Basic_library.is_internal_fun i (List.map (fun v -> v.value_type) vl) -> |
|
309 |
| MStep ([ _ ], i, vl) |
|
310 |
when Basic_library.is_internal_fun i (List.map (fun v -> v.value_type) vl) |
|
311 |
-> |
|
322 | 312 |
assert false (* This should not happen anymore *) |
323 | 313 |
| MStep (il, i, vl) -> |
324 |
(* if reset instance, just print the call over mem_m , otherwise declare mem_m =
|
|
325 |
mem_c and print the call to mem_m *) |
|
314 |
(* if reset instance, just print the call over mem_m , otherwise declare |
|
315 |
mem_m = mem_c and print the call to mem_m *)
|
|
326 | 316 |
pp_instance_call machines reset_instances m fmt i vl il; |
327 |
reset_instances (* Since this instance call will only happen once, we
|
|
328 |
don't have to update reset_instances *)
|
|
329 |
|
|
330 |
| MBranch (g,hl) -> (* (g = tag1 => expr1) and (g = tag2 => expr2) ...
|
|
331 |
should not be produced yet. Later, we will have to
|
|
332 |
compare the reset_instances of each branch and
|
|
333 |
introduced the mem_m = mem_c for branches to do not
|
|
334 |
address it while other did. Am I clear ? *)
|
|
317 |
reset_instances |
|
318 |
(* Since this instance call will only happen once, we don't have to update
|
|
319 |
reset_instances *) |
|
320 |
| MBranch (g, hl) ->
|
|
321 |
(* (g = tag1 => expr1) and (g = tag2 => expr2) ... should not be produced
|
|
322 |
yet. Later, we will have to compare the reset_instances of each branch
|
|
323 |
and introduced the mem_m = mem_c for branches to do not address it while
|
|
324 |
other did. Am I clear ? *)
|
|
335 | 325 |
(* For each branch we obtain the logical encoding, and the information |
336 | 326 |
whether a sub node has been reset or not. If a node has been reset in one |
337 |
of the branch, then all others have to have the mem_m = mem_c |
|
338 |
statement. *) |
|
327 |
of the branch, then all others have to have the mem_m = mem_c statement. *) |
|
339 | 328 |
let self = m.mname.node_id in |
340 | 329 |
let pp_branch fmt (tag, instrs) = |
341 |
fprintf fmt |
|
342 |
"@[<v 3>(or (not (= %a %a))@ "
|
|
343 |
(*"@[<v 3>(=> (= %a %s)@ "*) (* Issues with some versions of Z3. It
|
|
344 |
seems that => within Horn predicate
|
|
345 |
may cause trouble. I have hard time
|
|
346 |
producing a MWE, so I'll just keep the
|
|
347 |
fix here as (not a) or b *)
|
|
348 |
(pp_horn_val m self (pp_horn_var m)) g
|
|
349 |
pp_horn_tag tag;
|
|
350 |
let _ (* rs *) = pp_machine_instrs machines reset_instances m fmt instrs in
|
|
330 |
fprintf fmt "@[<v 3>(or (not (= %a %a))@ "
|
|
331 |
(*"@[<v 3>(=> (= %a %s)@ "*)
|
|
332 |
(* Issues with some versions of Z3. It seems that => within Horn
|
|
333 |
predicate may cause trouble. I have hard time producing a MWE, so
|
|
334 |
I'll just keep the fix here as (not a) or b *)
|
|
335 |
(pp_horn_val m self (pp_horn_var m))
|
|
336 |
g pp_horn_tag tag;
|
|
337 |
let _ (* rs *) =
|
|
338 |
pp_machine_instrs machines reset_instances m fmt instrs
|
|
339 |
in
|
|
351 | 340 |
fprintf fmt "@])"; |
352 |
() (* rs *) |
|
341 |
() |
|
342 |
(* rs *) |
|
353 | 343 |
in |
354 | 344 |
pp_conj pp_branch fmt hl; |
355 |
reset_instances
|
|
345 |
reset_instances |
|
356 | 346 |
|
357 |
and pp_machine_instrs machines reset_instances m fmt instrs =
|
|
347 |
and pp_machine_instrs machines reset_instances m fmt instrs = |
|
358 | 348 |
let ppi rs fmt i = pp_machine_instr machines rs m fmt i in |
359 | 349 |
match instrs with |
360 |
| [x] -> ppi reset_instances fmt x |
|
361 |
| _::_ -> |
|
350 |
| [ x ] -> |
|
351 |
ppi reset_instances fmt x |
|
352 |
| _ :: _ -> |
|
362 | 353 |
fprintf fmt "(and @[<v 0>"; |
363 |
let rs = List.fold_left (fun rs i -> |
|
364 |
let rs = ppi rs fmt i in |
|
365 |
fprintf fmt "@ "; |
|
366 |
rs |
|
367 |
) |
|
368 |
reset_instances instrs |
|
354 |
let rs = |
|
355 |
List.fold_left |
|
356 |
(fun rs i -> |
|
357 |
let rs = ppi rs fmt i in |
|
358 |
fprintf fmt "@ "; |
|
359 |
rs) |
|
360 |
reset_instances instrs |
|
369 | 361 |
in |
370 | 362 |
fprintf fmt "@])"; |
371 | 363 |
rs |
372 |
|
|
373 |
| [] -> fprintf fmt "true"; reset_instances |
|
364 |
| [] -> |
|
365 |
fprintf fmt "true"; |
|
366 |
reset_instances |
|
374 | 367 |
|
375 | 368 |
let pp_machine_reset machines fmt m = |
376 | 369 |
let locals = local_memory_vars m in |
377 | 370 |
fprintf fmt "@[<v 5>(and @ "; |
378 | 371 |
|
379 | 372 |
(* print "x_m = x_c" for each local memory *) |
380 |
(Utils.fprintf_list ~sep:"@ " (fun fmt v -> |
|
381 |
fprintf fmt "(= %a %a)" |
|
382 |
(pp_horn_var m) (rename_mid v) |
|
383 |
(pp_horn_var m) (rename_current v) |
|
384 |
)) fmt locals; |
|
373 |
(Utils.fprintf_list ~sep:"@ " (fun fmt v -> |
|
374 |
fprintf fmt "(= %a %a)" (pp_horn_var m) (rename_mid v) (pp_horn_var m) |
|
375 |
(rename_current v))) |
|
376 |
fmt locals; |
|
385 | 377 |
fprintf fmt "@ "; |
386 | 378 |
|
387 |
(* print "child_reset ( associated vars _ {c,m} )" for each subnode. |
|
388 |
Special treatment for _arrow: _first = true |
|
389 |
*) |
|
379 |
(* print "child_reset ( associated vars _ {c,m} )" for each subnode. Special |
|
380 |
treatment for _arrow: _first = true *) |
|
390 | 381 |
(Utils.fprintf_list ~sep:"@ " (fun fmt (id, (n, _)) -> |
391 |
let name = node_name n in |
|
392 |
if name = "_arrow" then ( |
|
393 |
fprintf fmt "(= %s._arrow._first_m true)" |
|
394 |
(concat m.mname.node_id id) |
|
395 |
) else ( |
|
396 |
let machine_n = get_machine machines name in |
|
397 |
fprintf fmt "(%s_reset @[<hov 0>%a@])" |
|
398 |
name |
|
399 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) |
|
400 |
(rename_machine_list (concat m.mname.node_id id) (reset_vars machines machine_n)) |
|
401 |
) |
|
402 |
)) fmt m.minstances; |
|
382 |
let name = node_name n in |
|
383 |
if name = "_arrow" then |
|
384 |
fprintf fmt "(= %s._arrow._first_m true)" (concat m.mname.node_id id) |
|
385 |
else |
|
386 |
let machine_n = get_machine machines name in |
|
387 |
fprintf fmt "(%s_reset @[<hov 0>%a@])" name |
|
388 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) |
|
389 |
(rename_machine_list |
|
390 |
(concat m.mname.node_id id) |
|
391 |
(reset_vars machines machine_n)))) |
|
392 |
fmt m.minstances; |
|
403 | 393 |
|
404 | 394 |
fprintf fmt "@]@ )" |
405 | 395 |
|
406 |
|
|
407 |
|
|
408 | 396 |
(**************************************************************) |
409 | 397 |
|
410 |
|
|
411 |
(* Print the machine m: |
|
412 |
two functions: m_init and m_step |
|
413 |
- m_init is a predicate over m memories |
|
414 |
- m_step is a predicate over old_memories, inputs, new_memories, outputs |
|
415 |
We first declare all variables then the two /rules/. |
|
416 |
*) |
|
398 |
(* Print the machine m: two functions: m_init and m_step - m_init is a predicate |
|
399 |
over m memories - m_step is a predicate over old_memories, inputs, |
|
400 |
new_memories, outputs We first declare all variables then the two /rules/. *) |
|
417 | 401 |
let print_machine machines fmt m = |
418 |
if m.mname.node_id = Arrow.arrow_id then |
|
419 |
(* We don't print arrow function *) |
|
402 |
if m.mname.node_id = Arrow.arrow_id then (* We don't print arrow function *) |
|
420 | 403 |
() |
421 |
else |
|
422 |
begin |
|
423 |
fprintf fmt "; %s@." m.mname.node_id; |
|
424 |
|
|
425 |
(* Printing variables *) |
|
426 |
Utils.fprintf_list ~sep:"@." pp_decl_var fmt |
|
427 |
( |
|
428 |
(inout_vars m)@ |
|
429 |
(rename_current_list (full_memory_vars machines m)) @ |
|
430 |
(rename_mid_list (full_memory_vars machines m)) @ |
|
431 |
(rename_next_list (full_memory_vars machines m)) @ |
|
432 |
(rename_machine_list m.mname.node_id m.mstep.step_locals) |
|
433 |
); |
|
434 |
pp_print_newline fmt (); |
|
404 |
else ( |
|
405 |
fprintf fmt "; %s@." m.mname.node_id; |
|
406 |
|
|
407 |
(* Printing variables *) |
|
408 |
Utils.fprintf_list ~sep:"@." pp_decl_var fmt |
|
409 |
(inout_vars m |
|
410 |
@ rename_current_list (full_memory_vars machines m) |
|
411 |
@ rename_mid_list (full_memory_vars machines m) |
|
412 |
@ rename_next_list (full_memory_vars machines m) |
|
413 |
@ rename_machine_list m.mname.node_id m.mstep.step_locals); |
|
414 |
pp_print_newline fmt (); |
|
415 |
|
|
416 |
if is_stateless m then ( |
|
417 |
(* Declaring single predicate *) |
|
418 |
fprintf fmt "(declare-rel %a (%a))@." pp_machine_stateless_name |
|
419 |
m.mname.node_id |
|
420 |
(Utils.fprintf_list ~sep:" " pp_type) |
|
421 |
(List.map (fun v -> v.var_type) (inout_vars m)); |
|
422 |
|
|
423 |
match m.mstep.step_asserts with |
|
424 |
| [] -> |
|
425 |
(* Rule for single predicate *) |
|
426 |
fprintf fmt "; Stateless step rule @."; |
|
427 |
fprintf fmt "@[<v 2>(rule (=> @ "; |
|
428 |
ignore |
|
429 |
(pp_machine_instrs machines [] |
|
430 |
(* No reset info for stateless nodes *) m fmt m.mstep.step_instrs); |
|
431 |
fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@." pp_machine_stateless_name |
|
432 |
m.mname.node_id |
|
433 |
(Utils.fprintf_list ~sep:" " (pp_horn_var m)) |
|
434 |
(inout_vars m) |
|
435 |
| assertsl -> |
|
436 |
let pp_val = |
|
437 |
pp_horn_val ~is_lhs:true m m.mname.node_id (pp_horn_var m) |
|
438 |
in |
|
439 |
|
|
440 |
fprintf fmt "; Stateless step rule with Assertions @."; |
|
441 |
(*Rule for step*) |
|
442 |
fprintf fmt "@[<v 2>(rule (=> @ (and @ "; |
|
443 |
ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs); |
|
444 |
fprintf fmt "@. %a)@ (%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) |
|
445 |
assertsl pp_machine_stateless_name m.mname.node_id |
|
446 |
(Utils.fprintf_list ~sep:" " (pp_horn_var m)) |
|
447 |
(step_vars machines m)) |
|
448 |
else ( |
|
449 |
(* Declaring predicate *) |
|
450 |
fprintf fmt "(declare-rel %a (%a))@." pp_machine_reset_name |
|
451 |
m.mname.node_id |
|
452 |
(Utils.fprintf_list ~sep:" " pp_type) |
|
453 |
(List.map (fun v -> v.var_type) (reset_vars machines m)); |
|
454 |
|
|
455 |
fprintf fmt "(declare-rel %a (%a))@." pp_machine_step_name m.mname.node_id |
|
456 |
(Utils.fprintf_list ~sep:" " pp_type) |
|
457 |
(List.map (fun v -> v.var_type) (step_vars machines m)); |
|
435 | 458 |
|
436 |
if is_stateless m then |
|
437 |
begin |
|
438 |
(* Declaring single predicate *) |
|
439 |
fprintf fmt "(declare-rel %a (%a))@." |
|
440 |
pp_machine_stateless_name m.mname.node_id |
|
441 |
(Utils.fprintf_list ~sep:" " pp_type) |
|
442 |
(List.map (fun v -> v.var_type) (inout_vars m)); |
|
443 |
|
|
444 |
match m.mstep.step_asserts with |
|
445 |
| [] -> |
|
446 |
begin |
|
447 |
|
|
448 |
(* Rule for single predicate *) |
|
449 |
fprintf fmt "; Stateless step rule @."; |
|
450 |
fprintf fmt "@[<v 2>(rule (=> @ "; |
|
451 |
ignore (pp_machine_instrs machines ([] (* No reset info for stateless nodes *) ) m fmt m.mstep.step_instrs); |
|
452 |
fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@." |
|
453 |
pp_machine_stateless_name m.mname.node_id |
|
454 |
(Utils.fprintf_list ~sep:" " (pp_horn_var m)) (inout_vars m); |
|
455 |
end |
|
456 |
| assertsl -> |
|
457 |
begin |
|
458 |
let pp_val = pp_horn_val ~is_lhs:true m m.mname.node_id (pp_horn_var m) in |
|
459 |
|
|
460 |
fprintf fmt "; Stateless step rule with Assertions @."; |
|
461 |
(*Rule for step*) |
|
462 |
fprintf fmt "@[<v 2>(rule (=> @ (and @ "; |
|
463 |
ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs); |
|
464 |
fprintf fmt "@. %a)@ (%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl |
|
465 |
pp_machine_stateless_name m.mname.node_id |
|
466 |
(Utils.fprintf_list ~sep:" " (pp_horn_var m)) (step_vars machines m); |
|
467 |
|
|
468 |
end |
|
469 |
|
|
470 |
end |
|
471 |
else |
|
472 |
begin |
|
473 |
(* Declaring predicate *) |
|
474 |
fprintf fmt "(declare-rel %a (%a))@." |
|
475 |
pp_machine_reset_name m.mname.node_id |
|
476 |
(Utils.fprintf_list ~sep:" " pp_type) |
|
477 |
(List.map (fun v -> v.var_type) (reset_vars machines m)); |
|
478 |
|
|
479 |
fprintf fmt "(declare-rel %a (%a))@." |
|
480 |
pp_machine_step_name m.mname.node_id |
|
481 |
(Utils.fprintf_list ~sep:" " pp_type) |
|
482 |
(List.map (fun v -> v.var_type) (step_vars machines m)); |
|
483 |
|
|
484 |
pp_print_newline fmt (); |
|
485 |
|
|
486 |
(* Rule for reset *) |
|
487 |
fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a @[<v 0>%a)@]@]@.))@.@." |
|
488 |
(pp_machine_reset machines) m |
|
489 |
pp_machine_reset_name m.mname.node_id |
|
490 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (reset_vars machines m); |
|
491 |
|
|
492 |
match m.mstep.step_asserts with |
|
493 |
| [] -> |
|
494 |
begin |
|
495 |
fprintf fmt "; Step rule @."; |
|
496 |
(* Rule for step*) |
|
497 |
fprintf fmt "@[<v 2>(rule (=> @ "; |
|
498 |
ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs); |
|
499 |
fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@." |
|
500 |
pp_machine_step_name m.mname.node_id |
|
501 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (step_vars machines m); |
|
502 |
end |
|
503 |
| assertsl -> |
|
504 |
begin |
|
505 |
let pp_val = pp_horn_val ~is_lhs:true m m.mname.node_id (pp_horn_var m) in |
|
506 |
(* print_string pp_val; *) |
|
507 |
fprintf fmt "; Step rule with Assertions @."; |
|
508 |
|
|
509 |
(*Rule for step*) |
|
510 |
fprintf fmt "@[<v 2>(rule (=> @ (and @ "; |
|
511 |
ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs); |
|
512 |
fprintf fmt "@. %a)@ (%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl |
|
513 |
pp_machine_step_name m.mname.node_id |
|
514 |
(Utils.fprintf_list ~sep:" " (pp_horn_var m)) (step_vars machines m); |
|
515 |
end |
|
516 |
|
|
517 |
|
|
518 |
end |
|
519 |
end |
|
459 |
pp_print_newline fmt (); |
|
520 | 460 |
|
461 |
(* Rule for reset *) |
|
462 |
fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a @[<v 0>%a)@]@]@.))@.@." |
|
463 |
(pp_machine_reset machines) |
|
464 |
m pp_machine_reset_name m.mname.node_id |
|
465 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) |
|
466 |
(reset_vars machines m); |
|
467 |
|
|
468 |
match m.mstep.step_asserts with |
|
469 |
| [] -> |
|
470 |
fprintf fmt "; Step rule @."; |
|
471 |
(* Rule for step*) |
|
472 |
fprintf fmt "@[<v 2>(rule (=> @ "; |
|
473 |
ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs); |
|
474 |
fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@." pp_machine_step_name |
|
475 |
m.mname.node_id |
|
476 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) |
|
477 |
(step_vars machines m) |
|
478 |
| assertsl -> |
|
479 |
let pp_val = |
|
480 |
pp_horn_val ~is_lhs:true m m.mname.node_id (pp_horn_var m) |
|
481 |
in |
|
482 |
(* print_string pp_val; *) |
|
483 |
fprintf fmt "; Step rule with Assertions @."; |
|
484 |
|
|
485 |
(*Rule for step*) |
|
486 |
fprintf fmt "@[<v 2>(rule (=> @ (and @ "; |
|
487 |
ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs); |
|
488 |
fprintf fmt "@. %a)@ (%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) |
|
489 |
assertsl pp_machine_step_name m.mname.node_id |
|
490 |
(Utils.fprintf_list ~sep:" " (pp_horn_var m)) |
|
491 |
(step_vars machines m))) |
|
521 | 492 |
|
522 | 493 |
let mk_flags arity = |
523 | 494 |
let b_range = |
524 |
let rec range i j = |
|
525 |
if i > arity then [] else i :: (range (i+1) j) in |
|
526 |
range 2 arity; |
|
527 |
in |
|
528 |
List.fold_left (fun acc _ -> acc ^ " false") "true" b_range |
|
529 |
|
|
495 |
let rec range i j = if i > arity then [] else i :: range (i + 1) j in |
|
496 |
range 2 arity |
|
497 |
in |
|
498 |
List.fold_left (fun acc _ -> acc ^ " false") "true" b_range |
|
530 | 499 |
|
531 |
(*Get sfunction infos from command line*)
|
|
532 |
let get_sf_info() = |
|
500 |
(*Get sfunction infos from command line*) |
|
501 |
let get_sf_info () =
|
|
533 | 502 |
let splitted = Str.split (Str.regexp "@") !Options.sfunction in |
534 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. sfunction name: %s@," !Options.sfunction); |
|
535 |
let sf_name, flags, arity = match splitted with |
|
536 |
[h;flg;par] -> h, flg, par |
|
537 |
| _ -> failwith "Wrong Sfunction info" |
|
538 |
|
|
503 |
Log.report ~level:1 (fun fmt -> |
|
504 |
fprintf fmt ".. sfunction name: %s@," !Options.sfunction); |
|
505 |
let sf_name, flags, arity = |
|
506 |
match splitted with |
|
507 |
| [ h; flg; par ] -> |
|
508 |
h, flg, par |
|
509 |
| _ -> |
|
510 |
failwith "Wrong Sfunction info" |
|
539 | 511 |
in |
540 |
Log.report ~level:1 (fun fmt -> fprintf fmt "... sf_name: %s@, .. flags: %s@ .. arity: %s@," sf_name flags arity); |
|
541 |
sf_name, flags, arity |
|
542 |
|
|
543 | 512 |
|
544 |
(*a function to print the rules in case we have an s-function*) |
|
545 |
let print_sfunction machines fmt m = |
|
546 |
if m.mname.node_id = Arrow.arrow_id then |
|
547 |
(* We don't print arrow function *) |
|
548 |
() |
|
549 |
else |
|
550 |
begin |
|
551 |
Format.fprintf fmt "; SFUNCTION@."; |
|
552 |
Format.fprintf fmt "; %s@." m.mname.node_id; |
|
553 |
Format.fprintf fmt "; EndPoint Predicate %s." !Options.sfunction; |
|
554 |
|
|
555 |
(* Check if there is annotation for s-function *) |
|
556 |
if m.mannot != [] then( |
|
557 |
Format.fprintf fmt "; @[%a@]@]@\n" (Utils.fprintf_list ~sep:"@ " Printers.pp_s_function) m.mannot; |
|
558 |
); |
|
559 |
|
|
560 |
(* Printing variables *) |
|
561 |
Utils.fprintf_list ~sep:"@." pp_decl_var fmt |
|
562 |
((step_vars machines m)@ |
|
563 |
(rename_machine_list m.mname.node_id m.mstep.step_locals)); |
|
564 |
Format.pp_print_newline fmt (); |
|
565 |
let sf_name, flags, _ = get_sf_info() in |
|
566 |
|
|
567 |
if is_stateless m then |
|
568 |
begin |
|
569 |
(* Declaring single predicate *) |
|
570 |
Format.fprintf fmt "(declare-rel %a (%a))@." |
|
571 |
pp_machine_stateless_name m.mname.node_id |
|
572 |
(Utils.fprintf_list ~sep:" " pp_type) |
|
573 |
(List.map (fun v -> v.var_type) (reset_vars machines m)); |
|
574 |
Format.pp_print_newline fmt (); |
|
575 |
(* Rule for single predicate *) |
|
576 |
let str_flags = sf_name ^ " " ^ mk_flags (int_of_string flags) in |
|
577 |
Format.fprintf fmt "@[<v 2>(rule (=> @ (%s %a) (%a %a)@]@.))@.@." |
|
578 |
str_flags |
|
579 |
(Utils.fprintf_list ~sep:" " (pp_horn_var m)) (reset_vars machines m) |
|
580 |
pp_machine_stateless_name m.mname.node_id |
|
581 |
(Utils.fprintf_list ~sep:" " (pp_horn_var m)) (reset_vars machines m); |
|
582 |
end |
|
583 |
else |
|
584 |
begin |
|
585 |
(* Declaring predicate *) |
|
586 |
Format.fprintf fmt "(declare-rel %a (%a))@." |
|
587 |
pp_machine_reset_name m.mname.node_id |
|
588 |
(Utils.fprintf_list ~sep:" " pp_type) |
|
589 |
(List.map (fun v -> v.var_type) (inout_vars m)); |
|
590 |
|
|
591 |
Format.fprintf fmt "(declare-rel %a (%a))@." |
|
592 |
pp_machine_step_name m.mname.node_id |
|
593 |
(Utils.fprintf_list ~sep:" " pp_type) |
|
594 |
(List.map (fun v -> v.var_type) (step_vars machines m)); |
|
595 |
|
|
596 |
Format.pp_print_newline fmt (); |
|
597 |
(* Adding assertions *) |
|
598 |
match m.mstep.step_asserts with |
|
599 |
| [] -> |
|
600 |
begin |
|
601 |
|
|
602 |
(* Rule for step*) |
|
603 |
fprintf fmt "@[<v 2>(rule (=> @ "; |
|
604 |
ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs); |
|
605 |
fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@." |
|
606 |
pp_machine_step_name m.mname.node_id |
|
607 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (step_vars machines m); |
|
608 |
end |
|
609 |
| assertsl -> |
|
610 |
begin |
|
611 |
let pp_val = pp_horn_val ~is_lhs:true m m.mname.node_id (pp_horn_var m) in |
|
612 |
(* print_string pp_val; *) |
|
613 |
fprintf fmt "; with Assertions @."; |
|
614 |
|
|
615 |
(*Rule for step*) |
|
616 |
fprintf fmt "@[<v 2>(rule (=> @ (and @ "; |
|
617 |
ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs); |
|
618 |
fprintf fmt "@. %a)(%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl |
|
619 |
pp_machine_step_name m.mname.node_id |
|
620 |
(Utils.fprintf_list ~sep:" " (pp_horn_var m)) (step_vars machines m); |
|
621 |
end |
|
622 |
|
|
623 |
end |
|
624 |
|
|
625 |
end |
|
513 |
Log.report ~level:1 (fun fmt -> |
|
514 |
fprintf fmt "... sf_name: %s@, .. flags: %s@ .. arity: %s@," sf_name flags |
|
515 |
arity); |
|
516 |
sf_name, flags, arity |
|
626 | 517 |
|
518 |
(*a function to print the rules in case we have an s-function*) |
|
519 |
let print_sfunction machines fmt m = |
|
520 |
if m.mname.node_id = Arrow.arrow_id then (* We don't print arrow function *) |
|
521 |
() |
|
522 |
else ( |
|
523 |
Format.fprintf fmt "; SFUNCTION@."; |
|
524 |
Format.fprintf fmt "; %s@." m.mname.node_id; |
|
525 |
Format.fprintf fmt "; EndPoint Predicate %s." !Options.sfunction; |
|
526 |
|
|
527 |
(* Check if there is annotation for s-function *) |
|
528 |
if m.mannot != [] then |
|
529 |
Format.fprintf fmt "; @[%a@]@]@\n" |
|
530 |
(Utils.fprintf_list ~sep:"@ " Printers.pp_s_function) |
|
531 |
m.mannot; |
|
532 |
|
|
533 |
(* Printing variables *) |
|
534 |
Utils.fprintf_list ~sep:"@." pp_decl_var fmt |
|
535 |
(step_vars machines m |
|
536 |
@ rename_machine_list m.mname.node_id m.mstep.step_locals); |
|
537 |
Format.pp_print_newline fmt (); |
|
538 |
let sf_name, flags, _ = get_sf_info () in |
|
539 |
|
|
540 |
if is_stateless m then ( |
|
541 |
(* Declaring single predicate *) |
|
542 |
Format.fprintf fmt "(declare-rel %a (%a))@." pp_machine_stateless_name |
|
543 |
m.mname.node_id |
|
544 |
(Utils.fprintf_list ~sep:" " pp_type) |
|
545 |
(List.map (fun v -> v.var_type) (reset_vars machines m)); |
|
546 |
Format.pp_print_newline fmt (); |
|
547 |
(* Rule for single predicate *) |
|
548 |
let str_flags = sf_name ^ " " ^ mk_flags (int_of_string flags) in |
|
549 |
Format.fprintf fmt "@[<v 2>(rule (=> @ (%s %a) (%a %a)@]@.))@.@." |
|
550 |
str_flags |
|
551 |
(Utils.fprintf_list ~sep:" " (pp_horn_var m)) |
|
552 |
(reset_vars machines m) pp_machine_stateless_name m.mname.node_id |
|
553 |
(Utils.fprintf_list ~sep:" " (pp_horn_var m)) |
|
554 |
(reset_vars machines m)) |
|
555 |
else ( |
|
556 |
(* Declaring predicate *) |
|
557 |
Format.fprintf fmt "(declare-rel %a (%a))@." pp_machine_reset_name |
|
558 |
m.mname.node_id |
|
559 |
(Utils.fprintf_list ~sep:" " pp_type) |
|
560 |
(List.map (fun v -> v.var_type) (inout_vars m)); |
|
561 |
|
|
562 |
Format.fprintf fmt "(declare-rel %a (%a))@." pp_machine_step_name |
|
563 |
m.mname.node_id |
|
564 |
(Utils.fprintf_list ~sep:" " pp_type) |
|
565 |
(List.map (fun v -> v.var_type) (step_vars machines m)); |
|
566 |
|
|
567 |
Format.pp_print_newline fmt (); |
|
568 |
(* Adding assertions *) |
|
569 |
match m.mstep.step_asserts with |
|
570 |
| [] -> |
|
571 |
(* Rule for step*) |
|
572 |
fprintf fmt "@[<v 2>(rule (=> @ "; |
|
573 |
ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs); |
|
574 |
fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@." pp_machine_step_name |
|
575 |
m.mname.node_id |
|
576 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) |
|
577 |
(step_vars machines m) |
|
578 |
| assertsl -> |
|
579 |
let pp_val = |
|
580 |
pp_horn_val ~is_lhs:true m m.mname.node_id (pp_horn_var m) |
|
581 |
in |
|
582 |
(* print_string pp_val; *) |
|
583 |
fprintf fmt "; with Assertions @."; |
|
584 |
|
|
585 |
(*Rule for step*) |
|
586 |
fprintf fmt "@[<v 2>(rule (=> @ (and @ "; |
|
587 |
ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs); |
|
588 |
fprintf fmt "@. %a)(%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl |
|
589 |
pp_machine_step_name m.mname.node_id |
|
590 |
(Utils.fprintf_list ~sep:" " (pp_horn_var m)) |
|
591 |
(step_vars machines m))) |
|
627 | 592 |
|
628 | 593 |
(**************** XML printing functions *************) |
629 | 594 |
|
630 |
let rec pp_xml_expr fmt expr = |
|
631 |
(match expr.expr_annot with |
|
632 |
| None -> fprintf fmt "%t" |
|
633 |
| Some ann -> fprintf fmt "@[(%a %t)@]" pp_xml_expr_annot ann) |
|
634 |
(fun fmt -> |
|
595 |
let rec pp_xml_expr fmt expr = |
|
596 |
(match expr.expr_annot with |
|
597 |
| None -> |
|
598 |
fprintf fmt "%t" |
|
599 |
| Some ann -> |
|
600 |
fprintf fmt "@[(%a %t)@]" pp_xml_expr_annot ann) (fun fmt -> |
|
635 | 601 |
match expr.expr_desc with |
636 |
| Expr_const c -> Printers.pp_const fmt c |
|
637 |
| Expr_ident id -> fprintf fmt "%s" id |
|
638 |
| Expr_array a -> fprintf fmt "[%a]" pp_xml_tuple a |
|
639 |
| Expr_access (a, d) -> fprintf fmt "%a[%a]" pp_xml_expr a Dimension.pp_dimension d |
|
640 |
| Expr_power (a, d) -> fprintf fmt "(%a^%a)" pp_xml_expr a Dimension.pp_dimension d |
|
641 |
| Expr_tuple el -> fprintf fmt "(%a)" pp_xml_tuple el |
|
642 |
| Expr_ite (c, t, e) -> fprintf fmt "@[<hov 1>(if %a then@ @[<hov 2>%a@]@ else@ @[<hov 2>%a@]@])" pp_xml_expr c pp_xml_expr t pp_xml_expr e |
|
643 |
| Expr_arrow (e1, e2) -> fprintf fmt "(%a -> %a)" pp_xml_expr e1 pp_xml_expr e2 |
|
644 |
| Expr_fby (e1, e2) -> fprintf fmt "%a fby %a" pp_xml_expr e1 pp_xml_expr e2 |
|
645 |
| Expr_pre e -> fprintf fmt "pre %a" pp_xml_expr e |
|
646 |
| Expr_when (e, id, l) -> fprintf fmt "%a when %s(%s)" pp_xml_expr e l id |
|
647 |
| Expr_merge (id, hl) -> |
|
648 |
fprintf fmt "merge %s %a" id pp_xml_handlers hl |
|
649 |
| Expr_appl (id, e, r) -> pp_xml_app fmt id e r |
|
650 |
) |
|
651 |
and pp_xml_tuple fmt el = |
|
652 |
Utils.fprintf_list ~sep:"," pp_xml_expr fmt el |
|
653 |
|
|
654 |
and pp_xml_handler fmt (t, h) = |
|
655 |
fprintf fmt "(%s -> %a)" t pp_xml_expr h |
|
656 |
|
|
657 |
and pp_xml_handlers fmt hl = |
|
658 |
Utils.fprintf_list ~sep:" " pp_xml_handler fmt hl |
|
602 |
| Expr_const c -> |
|
603 |
Printers.pp_const fmt c |
|
604 |
| Expr_ident id -> |
|
605 |
fprintf fmt "%s" id |
|
606 |
| Expr_array a -> |
|
607 |
fprintf fmt "[%a]" pp_xml_tuple a |
|
608 |
| Expr_access (a, d) -> |
|
609 |
fprintf fmt "%a[%a]" pp_xml_expr a Dimension.pp_dimension d |
|
610 |
| Expr_power (a, d) -> |
|
611 |
fprintf fmt "(%a^%a)" pp_xml_expr a Dimension.pp_dimension d |
|
612 |
| Expr_tuple el -> |
|
613 |
fprintf fmt "(%a)" pp_xml_tuple el |
|
614 |
| Expr_ite (c, t, e) -> |
|
615 |
fprintf fmt |
|
616 |
"@[<hov 1>(if %a then@ @[<hov 2>%a@]@ else@ @[<hov 2>%a@]@])" |
|
617 |
pp_xml_expr c pp_xml_expr t pp_xml_expr e |
|
618 |
| Expr_arrow (e1, e2) -> |
|
619 |
fprintf fmt "(%a -> %a)" pp_xml_expr e1 pp_xml_expr e2 |
|
620 |
| Expr_fby (e1, e2) -> |
|
621 |
fprintf fmt "%a fby %a" pp_xml_expr e1 pp_xml_expr e2 |
|
622 |
| Expr_pre e -> |
|
623 |
fprintf fmt "pre %a" pp_xml_expr e |
|
624 |
| Expr_when (e, id, l) -> |
|
625 |
fprintf fmt "%a when %s(%s)" pp_xml_expr e l id |
|
626 |
| Expr_merge (id, hl) -> |
|
627 |
fprintf fmt "merge %s %a" id pp_xml_handlers hl |
|
628 |
| Expr_appl (id, e, r) -> |
|
629 |
pp_xml_app fmt id e r) |
|
630 |
|
|
631 |
and pp_xml_tuple fmt el = Utils.fprintf_list ~sep:"," pp_xml_expr fmt el |
|
632 |
|
|
633 |
and pp_xml_handler fmt (t, h) = fprintf fmt "(%s -> %a)" t pp_xml_expr h |
|
634 |
|
|
635 |
and pp_xml_handlers fmt hl = Utils.fprintf_list ~sep:" " pp_xml_handler fmt hl |
|
659 | 636 |
|
660 | 637 |
and pp_xml_app fmt id e r = |
661 | 638 |
match r with |
662 |
| None -> pp_xml_call fmt id e |
|
663 |
| Some c -> fprintf fmt "%t every (%a)" (fun fmt -> pp_xml_call fmt id e) pp_xml_expr c |
|
639 |
| None -> |
|
640 |
pp_xml_call fmt id e |
|
641 |
| Some c -> |
|
642 |
fprintf fmt "%t every (%a)" (fun fmt -> pp_xml_call fmt id e) pp_xml_expr c |
|
664 | 643 |
|
665 | 644 |
and pp_xml_call fmt id e = |
666 | 645 |
match id, e.expr_desc with |
667 |
| "+", Expr_tuple([e1;e2]) -> fprintf fmt "(%a + %a)" pp_xml_expr e1 pp_xml_expr e2 |
|
668 |
| "uminus", _ -> fprintf fmt "(- %a)" pp_xml_expr e |
|
669 |
| "-", Expr_tuple([e1;e2]) -> fprintf fmt "(%a - %a)" pp_xml_expr e1 pp_xml_expr e2 |
|
670 |
| "*", Expr_tuple([e1;e2]) -> fprintf fmt "(%a * %a)" pp_xml_expr e1 pp_xml_expr e2 |
|
671 |
| "/", Expr_tuple([e1;e2]) -> fprintf fmt "(%a / %a)" pp_xml_expr e1 pp_xml_expr e2 |
|
672 |
| "mod", Expr_tuple([e1;e2]) -> fprintf fmt "(%a mod %a)" pp_xml_expr e1 pp_xml_expr e2 |
|
673 |
| "&&", Expr_tuple([e1;e2]) -> fprintf fmt "(%a and %a)" pp_xml_expr e1 pp_xml_expr e2 |
|
674 |
| "||", Expr_tuple([e1;e2]) -> fprintf fmt "(%a or %a)" pp_xml_expr e1 pp_xml_expr e2 |
|
675 |
| "xor", Expr_tuple([e1;e2]) -> fprintf fmt "(%a xor %a)" pp_xml_expr e1 pp_xml_expr e2 |
|
676 |
| "impl", Expr_tuple([e1;e2]) -> fprintf fmt "(%a => %a)" pp_xml_expr e1 pp_xml_expr e2 |
|
677 |
| "<", Expr_tuple([e1;e2]) -> fprintf fmt "(%a < %a)" pp_xml_expr e1 pp_xml_expr e2 |
|
678 |
| "<=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a <= %a)" pp_xml_expr e1 pp_xml_expr e2 |
|
679 |
| ">", Expr_tuple([e1;e2]) -> fprintf fmt "(%a > %a)" pp_xml_expr e1 pp_xml_expr e2 |
|
680 |
| ">=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a >= %a)" pp_xml_expr e1 pp_xml_expr e2 |
|
681 |
| "!=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a != %a)" pp_xml_expr e1 pp_xml_expr e2 |
|
682 |
| "=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a = %a)" pp_xml_expr e1 pp_xml_expr e2 |
|
683 |
| "not", _ -> fprintf fmt "(not %a)" pp_xml_expr e |
|
684 |
| _, Expr_tuple _ -> fprintf fmt "%s %a" id pp_xml_expr e |
|
685 |
| _ -> fprintf fmt "%s (%a)" id pp_xml_expr e |
|
646 |
| "+", Expr_tuple [ e1; e2 ] -> |
|
647 |
fprintf fmt "(%a + %a)" pp_xml_expr e1 pp_xml_expr e2 |
|
648 |
| "uminus", _ -> |
|
649 |
fprintf fmt "(- %a)" pp_xml_expr e |
|
650 |
| "-", Expr_tuple [ e1; e2 ] -> |
|
651 |
fprintf fmt "(%a - %a)" pp_xml_expr e1 pp_xml_expr e2 |
|
652 |
| "*", Expr_tuple [ e1; e2 ] -> |
|
653 |
fprintf fmt "(%a * %a)" pp_xml_expr e1 pp_xml_expr e2 |
|
654 |
| "/", Expr_tuple [ e1; e2 ] -> |
|
655 |
fprintf fmt "(%a / %a)" pp_xml_expr e1 pp_xml_expr e2 |
|
656 |
| "mod", Expr_tuple [ e1; e2 ] -> |
|
657 |
fprintf fmt "(%a mod %a)" pp_xml_expr e1 pp_xml_expr e2 |
|
658 |
| "&&", Expr_tuple [ e1; e2 ] -> |
|
659 |
fprintf fmt "(%a and %a)" pp_xml_expr e1 pp_xml_expr e2 |
|
660 |
| "||", Expr_tuple [ e1; e2 ] -> |
|
661 |
fprintf fmt "(%a or %a)" pp_xml_expr e1 pp_xml_expr e2 |
|
662 |
| "xor", Expr_tuple [ e1; e2 ] -> |
|
663 |
fprintf fmt "(%a xor %a)" pp_xml_expr e1 pp_xml_expr e2 |
|
664 |
| "impl", Expr_tuple [ e1; e2 ] -> |
|
665 |
fprintf fmt "(%a => %a)" pp_xml_expr e1 pp_xml_expr e2 |
|
666 |
| "<", Expr_tuple [ e1; e2 ] -> |
|
667 |
fprintf fmt "(%a < %a)" pp_xml_expr e1 pp_xml_expr e2 |
|
668 |
| "<=", Expr_tuple [ e1; e2 ] -> |
|
669 |
fprintf fmt "(%a <= %a)" pp_xml_expr e1 pp_xml_expr e2 |
|
670 |
| ">", Expr_tuple [ e1; e2 ] -> |
|
671 |
fprintf fmt "(%a > %a)" pp_xml_expr e1 pp_xml_expr e2 |
|
672 |
| ">=", Expr_tuple [ e1; e2 ] -> |
|
673 |
fprintf fmt "(%a >= %a)" pp_xml_expr e1 pp_xml_expr e2 |
|
674 |
| "!=", Expr_tuple [ e1; e2 ] -> |
|
675 |
fprintf fmt "(%a != %a)" pp_xml_expr e1 pp_xml_expr e2 |
|
676 |
| "=", Expr_tuple [ e1; e2 ] -> |
|
677 |
fprintf fmt "(%a = %a)" pp_xml_expr e1 pp_xml_expr e2 |
|
678 |
| "not", _ -> |
|
679 |
fprintf fmt "(not %a)" pp_xml_expr e |
|
680 |
| _, Expr_tuple _ -> |
|
681 |
fprintf fmt "%s %a" id pp_xml_expr e |
|
682 |
| _ -> |
|
683 |
fprintf fmt "%s (%a)" id pp_xml_expr e |
|
686 | 684 |
|
687 | 685 |
and pp_xml_eexpr fmt e = |
688 | 686 |
fprintf fmt "%a%t %a" |
689 |
(Utils.fprintf_list ~sep:"; " Printers.pp_quantifiers) e.eexpr_quantifiers |
|
690 |
(fun fmt -> match e.eexpr_quantifiers with [] -> () | _ -> fprintf fmt ";") |
|
687 |
(Utils.fprintf_list ~sep:"; " Printers.pp_quantifiers) |
|
688 |
e.eexpr_quantifiers |
|
689 |
(fun fmt -> |
|
690 |
match e.eexpr_quantifiers with [] -> () | _ -> fprintf fmt ";") |
|
691 | 691 |
pp_xml_expr e.eexpr_qfexpr |
692 | 692 |
|
693 |
and pp_xml_sf_value fmt e =
|
|
694 |
fprintf fmt "%a"
|
|
695 |
(* (Utils.fprintf_list ~sep:"; " pp_xml_quantifiers) e.eexpr_quantifiers *)
|
|
696 |
(* (fun fmt -> match e.eexpr_quantifiers *)
|
|
697 |
(* with [] -> () *)
|
|
698 |
(* | _ -> fprintf fmt ";") *)
|
|
699 |
pp_xml_expr e.eexpr_qfexpr
|
|
693 |
and pp_xml_sf_value fmt e = |
|
694 |
fprintf fmt "%a" |
|
695 |
(* (Utils.fprintf_list ~sep:"; " pp_xml_quantifiers) e.eexpr_quantifiers *) |
|
696 |
(* (fun fmt -> match e.eexpr_quantifiers *) |
|
697 |
(* with [] -> () *) |
|
698 |
(* | _ -> fprintf fmt ";") *) |
|
699 |
pp_xml_expr e.eexpr_qfexpr |
|
700 | 700 |
|
701 | 701 |
and pp_xml_s_function fmt expr_ann = |
702 | 702 |
let pp_xml_annot fmt (kwds, ee) = |
703 | 703 |
Format.fprintf fmt " %t : %a" |
704 |
(fun fmt -> match kwds with |
|
705 |
| [] -> assert false |
|
706 |
| [x] -> Format.pp_print_string fmt x |
|
707 |
| _ -> Format.fprintf fmt "%a" (Utils.fprintf_list ~sep:"/" Format.pp_print_string) kwds) |
|
708 |
pp_xml_sf_value ee |
|
704 |
(fun fmt -> |
|
705 |
match kwds with |
|
706 |
| [] -> |
|
707 |
assert false |
|
708 |
| [ x ] -> |
|
709 |
Format.pp_print_string fmt x |
|
710 |
| _ -> |
|
711 |
Format.fprintf fmt "%a" |
|
712 |
(Utils.fprintf_list ~sep:"/" Format.pp_print_string) |
|
713 |
kwds) |
|
714 |
pp_xml_sf_value ee |
|
709 | 715 |
in |
710 | 716 |
Utils.fprintf_list ~sep:"@ " pp_xml_annot fmt expr_ann.annots |
711 | 717 |
|
712 | 718 |
and pp_xml_expr_annot fmt expr_ann = |
713 | 719 |
let pp_xml_annot fmt (kwds, ee) = |
714 | 720 |
Format.fprintf fmt "(*! %t: %a; *)" |
715 |
(fun fmt -> match kwds with | [] -> assert false | [x] -> Format.pp_print_string fmt x | _ -> Format.fprintf fmt "/%a/" (Utils.fprintf_list ~sep:"/" Format.pp_print_string) kwds) |
|
721 |
(fun fmt -> |
|
722 |
match kwds with |
|
723 |
| [] -> |
|
724 |
assert false |
|
725 |
| [ x ] -> |
|
726 |
Format.pp_print_string fmt x |
|
727 |
| _ -> |
|
728 |
Format.fprintf fmt "/%a/" |
|
729 |
(Utils.fprintf_list ~sep:"/" Format.pp_print_string) |
|
730 |
kwds) |
|
716 | 731 |
pp_xml_eexpr ee |
717 | 732 |
in |
718 | 733 |
Utils.fprintf_list ~sep:"@ " pp_xml_annot fmt expr_ann.annots |
719 | 734 |
|
720 |
|
|
721 | 735 |
(* Local Variables: *) |
722 | 736 |
(* compile-command:"make -C ../../.." *) |
723 | 737 |
(* End: *) |
Also available in: Unified diff
reformatting