Revision ca7ff3f7
Added by Lélio Brun 7 months 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