Revision 58272238
Added by Teme Kahsai almost 10 years ago
src/basic_library.ml | ||
---|---|---|
23 | 23 |
type_static (mkdim_var ()) ty |
24 | 24 |
|
25 | 25 |
let type_env = |
26 |
List.fold_left
|
|
26 |
List.fold_left |
|
27 | 27 |
(fun env (op, op_type) -> TE.add_value env op op_type) |
28 | 28 |
TE.initial |
29 | 29 |
[ |
30 | 30 |
"true", (static_op type_bool); |
31 | 31 |
"false", (static_op type_bool); |
32 | 32 |
"+", (static_op type_bin_poly_op); |
33 |
"uminus", (static_op type_unary_poly_op);
|
|
34 |
"-", (static_op type_bin_poly_op);
|
|
33 |
"uminus", (static_op type_unary_poly_op); |
|
34 |
"-", (static_op type_bin_poly_op); |
|
35 | 35 |
"*", (static_op type_bin_poly_op); |
36 | 36 |
"/", (static_op type_bin_poly_op); |
37 | 37 |
"mod", (static_op type_bin_int_op); |
... | ... | |
48 | 48 |
"=", (static_op type_bin_comp_op); |
49 | 49 |
"not", (static_op type_unary_bool_op) |
50 | 50 |
] |
51 |
|
|
51 |
|
|
52 | 52 |
module CE = Env |
53 | 53 |
|
54 | 54 |
let clock_env = |
... | ... | |
56 | 56 |
let env' = |
57 | 57 |
List.fold_right (fun op env -> CE.add_value env op ck_nullary_univ) |
58 | 58 |
["true"; "false"] init_env in |
59 |
let env' =
|
|
59 |
let env' = |
|
60 | 60 |
List.fold_right (fun op env -> CE.add_value env op ck_unary_univ) |
61 | 61 |
["uminus"; "not"] env' in |
62 |
let env' =
|
|
62 |
let env' = |
|
63 | 63 |
List.fold_right (fun op env -> CE.add_value env op ck_bin_univ) |
64 | 64 |
["+"; "-"; "*"; "/"; "mod"; "&&"; "||"; "xor"; "equi"; "impl"; "<"; "<="; ">"; ">="; "!="; "="] env' in |
65 | 65 |
env' |
... | ... | |
74 | 74 |
let env' = |
75 | 75 |
List.fold_right (fun op env -> DE.add_value env op delay_unary_poly_op) |
76 | 76 |
["uminus"; "not"] env' in |
77 |
let env' =
|
|
77 |
let env' = |
|
78 | 78 |
List.fold_right (fun op env -> DE.add_value env op delay_binary_poly_op) |
79 | 79 |
["+"; "-"; "*"; "/"; "mod"; "&&"; "||"; "xor"; "equi"; "impl"; "<"; "<="; ">"; ">="; "!="; "="] env' in |
80 |
let env' =
|
|
80 |
let env' = |
|
81 | 81 |
List.fold_right (fun op env -> DE.add_value env op delay_ternary_poly_op) |
82 | 82 |
[] env' in |
83 | 83 |
env' |
... | ... | |
85 | 85 |
module VE = Env |
86 | 86 |
|
87 | 87 |
let eval_env = |
88 |
let defs = [
|
|
88 |
let defs = [ |
|
89 | 89 |
"uminus", (function [Dint a] -> Dint (-a) | _ -> assert false); |
90 | 90 |
"not", (function [Dbool b] -> Dbool (not b) | _ -> assert false); |
91 | 91 |
"+", (function [Dint a; Dint b] -> Dint (a+b) | _ -> assert false); |
... | ... | |
106 | 106 |
"=", (function [a; b] -> Dbool (a=b) | _ -> assert false); |
107 | 107 |
] |
108 | 108 |
in |
109 |
List.fold_left
|
|
109 |
List.fold_left |
|
110 | 110 |
(fun env (op, op_eval) -> VE.add_value env op op_eval) |
111 | 111 |
VE.initial |
112 | 112 |
defs |
... | ... | |
120 | 120 |
match i, vl with |
121 | 121 |
(* | "ite", [v1; v2; v3] -> Format.fprintf fmt "(%a?(%a):(%a))" pp_val v1 pp_val v2 pp_val v3 *) |
122 | 122 |
| "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v |
123 |
| "not", [v] -> Format.fprintf fmt "(!%a)" pp_val v
|
|
124 |
| "impl", [v1; v2] -> Format.fprintf fmt "(!%a || %a)" pp_val v1 pp_val v2
|
|
125 |
| "=", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2
|
|
123 |
| "not", [v] -> Format.fprintf fmt "(!%a)" pp_val v |
|
124 |
| "impl", [v1; v2] -> Format.fprintf fmt "(!%a || %a)" pp_val v1 pp_val v2 |
|
125 |
| "=", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2 |
|
126 | 126 |
| "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2 |
127 | 127 |
| "equi", [v1; v2] -> Format.fprintf fmt "(!%a == !%a)" pp_val v1 pp_val v2 |
128 | 128 |
| "xor", [v1; v2] -> Format.fprintf fmt "(!%a != !%a)" pp_val v1 pp_val v2 |
129 |
| _, [v1; v2] -> Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2
|
|
129 |
| _, [v1; v2] -> Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2 |
|
130 | 130 |
| _ -> failwith i |
131 | 131 |
|
132 | 132 |
let pp_java i pp_val fmt vl = |
133 | 133 |
match i, vl with |
134 | 134 |
(* | "ite", [v1; v2; v3] -> Format.fprintf fmt "(%a?(%a):(%a))" pp_val v1 pp_val v2 pp_val v3 *) |
135 | 135 |
| "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v |
136 |
| "not", [v] -> Format.fprintf fmt "(!%a)" pp_val v
|
|
137 |
| "impl", [v1; v2] -> Format.fprintf fmt "(!%a || %a)" pp_val v1 pp_val v2
|
|
138 |
| "=", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2
|
|
136 |
| "not", [v] -> Format.fprintf fmt "(!%a)" pp_val v |
|
137 |
| "impl", [v1; v2] -> Format.fprintf fmt "(!%a || %a)" pp_val v1 pp_val v2 |
|
138 |
| "=", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2 |
|
139 | 139 |
| "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2 |
140 | 140 |
| "equi", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2 |
141 | 141 |
| "xor", [v1; v2] -> Format.fprintf fmt "(%a != %a)" pp_val v1 pp_val v2 |
142 |
| _, [v1; v2] -> Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2
|
|
142 |
| _, [v1; v2] -> Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2 |
|
143 | 143 |
| _ -> assert false |
144 | 144 |
|
145 |
let pp_horn i pp_val fmt vl =
|
|
145 |
let pp_horn i pp_val fmt vl = |
|
146 | 146 |
match i, vl with |
147 |
| "ite", [v1; v2; v3] -> Format.fprintf fmt "(@[<hov 2>ite %a@ %a@ %a@])" pp_val v1 pp_val v2 pp_val v3 |
|
147 |
| "ite", [v1; v2; v3] -> Format.fprintf fmt "(@[<hov 2>ite %a@ %a@ %a@])" pp_val v1 pp_val v2 pp_val v3 |
|
148 |
|
|
148 | 149 |
| "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v |
149 |
| "not", [v] -> Format.fprintf fmt "(not %a)" pp_val v
|
|
150 |
| "=", [v1; v2] -> Format.fprintf fmt "(= %a %a)" pp_val v1 pp_val v2
|
|
151 |
| "&&", [v1; v2] -> Format.fprintf fmt "(and %a %a)" pp_val v1 pp_val v2
|
|
152 |
| "||", [v1; v2] -> Format.fprintf fmt "(or %a %a)" pp_val v1 pp_val v2
|
|
153 |
| "impl", [v1; v2] -> Format.fprintf fmt "(=> %a %a)" pp_val v1 pp_val v2
|
|
150 |
| "not", [v] -> Format.fprintf fmt "(not %a)" pp_val v |
|
151 |
| "=", [v1; v2] -> Format.fprintf fmt "(= %a %a)" pp_val v1 pp_val v2 |
|
152 |
| "&&", [v1; v2] -> Format.fprintf fmt "(and %a %a)" pp_val v1 pp_val v2 |
|
153 |
| "||", [v1; v2] -> Format.fprintf fmt "(or %a %a)" pp_val v1 pp_val v2 |
|
154 |
| "impl", [v1; v2] -> Format.fprintf fmt "(=> %a %a)" pp_val v1 pp_val v2 |
|
154 | 155 |
| "mod", [v1; v2] -> Format.fprintf fmt "(mod %a %a)" pp_val v1 pp_val v2 |
155 | 156 |
| "equi", [v1; v2] -> Format.fprintf fmt "(%a = %a)" pp_val v1 pp_val v2 |
156 | 157 |
| "xor", [v1; v2] -> Format.fprintf fmt "(%a xor %a)" pp_val v1 pp_val v2 |
157 |
| "!=", [v1; v2] -> Format.fprintf fmt "(not (= %a %a))" pp_val v1 pp_val v2 |
|
158 |
| _, [v1; v2] -> Format.fprintf fmt "(%s %a %a)" i pp_val v1 pp_val v2 |
|
158 |
| "!=", [v1; v2] -> Format.fprintf fmt "(not (= %a %a))" pp_val v1 pp_val v2 |
|
159 |
| "/", [v1; v2] -> Format.fprintf fmt "(div %a %a)" pp_val v1 pp_val v2 |
|
160 |
| _, [v1; v2] -> Format.fprintf fmt "(%s %a %a)" i pp_val v1 pp_val v2 |
|
159 | 161 |
| _ -> assert false |
160 |
(* | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2
|
|
161 |
|
|
162 |
(* | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2 |
|
163 |
|
|
162 | 164 |
*) |
163 | 165 |
|
164 | 166 |
(* Local Variables: *) |
Also available in: Unified diff
modifed / to div in horn backend