Revision ca7ff3f7
Added by Lélio Brun over 1 year ago
src/basic_library.ml | ||
---|---|---|
16 | 16 |
open Clock_predef |
17 | 17 |
open Delay_predef |
18 | 18 |
open Dimension |
19 |
|
|
20 | 19 |
module TE = Env |
21 | 20 |
|
22 |
let static_op ty = |
|
23 |
type_static (mkdim_var ()) ty |
|
21 |
let static_op ty = type_static (mkdim_var ()) ty |
|
24 | 22 |
|
25 | 23 |
let type_env = |
26 | 24 |
List.fold_left |
27 | 25 |
(fun env (op, op_type) -> TE.add_value env op op_type) |
28 | 26 |
TE.initial |
29 | 27 |
[ |
30 |
"true", (static_op type_bool);
|
|
31 |
"false", (static_op type_bool);
|
|
32 |
"+", (static_op type_bin_poly_op);
|
|
33 |
"uminus", (static_op type_unary_poly_op);
|
|
34 |
"-", (static_op type_bin_poly_op);
|
|
35 |
"*", (static_op type_bin_poly_op);
|
|
36 |
"/", (static_op type_bin_poly_op);
|
|
37 |
"mod", (static_op type_bin_int_op);
|
|
38 |
"&&", (static_op type_bin_bool_op);
|
|
39 |
"||", (static_op type_bin_bool_op);
|
|
40 |
"xor", (static_op type_bin_bool_op);
|
|
41 |
"equi", (static_op type_bin_bool_op);
|
|
42 |
"impl", (static_op type_bin_bool_op);
|
|
43 |
"<", (static_op type_bin_comp_op);
|
|
44 |
"<=", (static_op type_bin_comp_op);
|
|
45 |
">", (static_op type_bin_comp_op);
|
|
46 |
">=", (static_op type_bin_comp_op);
|
|
47 |
"!=", (static_op type_bin_comp_op);
|
|
48 |
"=", (static_op type_bin_comp_op);
|
|
49 |
"not", (static_op type_unary_bool_op)
|
|
50 |
] |
|
28 |
"true", static_op type_bool;
|
|
29 |
"false", static_op type_bool;
|
|
30 |
"+", static_op type_bin_poly_op;
|
|
31 |
"uminus", static_op type_unary_poly_op;
|
|
32 |
"-", static_op type_bin_poly_op;
|
|
33 |
"*", static_op type_bin_poly_op;
|
|
34 |
"/", static_op type_bin_poly_op;
|
|
35 |
"mod", static_op type_bin_int_op;
|
|
36 |
"&&", static_op type_bin_bool_op;
|
|
37 |
"||", static_op type_bin_bool_op;
|
|
38 |
"xor", static_op type_bin_bool_op;
|
|
39 |
"equi", static_op type_bin_bool_op;
|
|
40 |
"impl", static_op type_bin_bool_op;
|
|
41 |
"<", static_op type_bin_comp_op;
|
|
42 |
"<=", static_op type_bin_comp_op;
|
|
43 |
">", static_op type_bin_comp_op;
|
|
44 |
">=", static_op type_bin_comp_op;
|
|
45 |
"!=", static_op type_bin_comp_op;
|
|
46 |
"=", static_op type_bin_comp_op;
|
|
47 |
"not", static_op type_unary_bool_op;
|
|
48 |
]
|
|
51 | 49 |
|
52 | 50 |
module CE = Env |
53 | 51 |
|
54 | 52 |
let clock_env = |
55 | 53 |
let init_env = CE.initial in |
56 | 54 |
let env' = |
57 |
List.fold_right (fun op env -> CE.add_value env op ck_nullary_univ) |
|
58 |
["true"; "false"] init_env in |
|
55 |
List.fold_right |
|
56 |
(fun op env -> CE.add_value env op ck_nullary_univ) |
|
57 |
[ "true"; "false" ] init_env |
|
58 |
in |
|
59 | 59 |
let env' = |
60 |
List.fold_right (fun op env -> CE.add_value env op ck_unary_univ) |
|
61 |
["uminus"; "not"] env' in |
|
60 |
List.fold_right |
|
61 |
(fun op env -> CE.add_value env op ck_unary_univ) |
|
62 |
[ "uminus"; "not" ] env' |
|
63 |
in |
|
62 | 64 |
let env' = |
63 |
List.fold_right (fun op env -> CE.add_value env op ck_bin_univ) |
|
64 |
["+"; "-"; "*"; "/"; "mod"; "&&"; "||"; "xor"; "equi"; "impl"; "<"; "<="; ">"; ">="; "!="; "="] env' in |
|
65 |
List.fold_right |
|
66 |
(fun op env -> CE.add_value env op ck_bin_univ) |
|
67 |
[ |
|
68 |
"+"; |
|
69 |
"-"; |
|
70 |
"*"; |
|
71 |
"/"; |
|
72 |
"mod"; |
|
73 |
"&&"; |
|
74 |
"||"; |
|
75 |
"xor"; |
|
76 |
"equi"; |
|
77 |
"impl"; |
|
78 |
"<"; |
|
79 |
"<="; |
|
80 |
">"; |
|
81 |
">="; |
|
82 |
"!="; |
|
83 |
"="; |
|
84 |
] |
|
85 |
env' |
|
86 |
in |
|
65 | 87 |
env' |
66 | 88 |
|
67 | 89 |
module DE = Env |
... | ... | |
69 | 91 |
let delay_env = |
70 | 92 |
let init_env = DE.initial in |
71 | 93 |
let env' = |
72 |
List.fold_right (fun op env -> DE.add_value env op delay_nullary_poly_op) |
|
73 |
["true"; "false"] init_env in |
|
94 |
List.fold_right |
|
95 |
(fun op env -> DE.add_value env op delay_nullary_poly_op) |
|
96 |
[ "true"; "false" ] init_env |
|
97 |
in |
|
74 | 98 |
let env' = |
75 |
List.fold_right (fun op env -> DE.add_value env op delay_unary_poly_op) |
|
76 |
["uminus"; "not"] env' in |
|
99 |
List.fold_right |
|
100 |
(fun op env -> DE.add_value env op delay_unary_poly_op) |
|
101 |
[ "uminus"; "not" ] env' |
|
102 |
in |
|
77 | 103 |
let env' = |
78 |
List.fold_right (fun op env -> DE.add_value env op delay_binary_poly_op) |
|
79 |
["+"; "-"; "*"; "/"; "mod"; "&&"; "||"; "xor"; "equi"; "impl"; "<"; "<="; ">"; ">="; "!="; "="] env' in |
|
104 |
List.fold_right |
|
105 |
(fun op env -> DE.add_value env op delay_binary_poly_op) |
|
106 |
[ |
|
107 |
"+"; |
|
108 |
"-"; |
|
109 |
"*"; |
|
110 |
"/"; |
|
111 |
"mod"; |
|
112 |
"&&"; |
|
113 |
"||"; |
|
114 |
"xor"; |
|
115 |
"equi"; |
|
116 |
"impl"; |
|
117 |
"<"; |
|
118 |
"<="; |
|
119 |
">"; |
|
120 |
">="; |
|
121 |
"!="; |
|
122 |
"="; |
|
123 |
] |
|
124 |
env' |
|
125 |
in |
|
80 | 126 |
let env' = |
81 |
List.fold_right (fun op env -> DE.add_value env op delay_ternary_poly_op) |
|
82 |
[] env' in |
|
127 |
List.fold_right |
|
128 |
(fun op env -> DE.add_value env op delay_ternary_poly_op) |
|
129 |
[] env' |
|
130 |
in |
|
83 | 131 |
env' |
84 | 132 |
|
85 | 133 |
module VE = Env |
86 | 134 |
|
87 | 135 |
let eval_dim_env = |
88 |
let defs = [ |
|
89 |
"uminus", (function [Dint a] -> Dint (-a) | _ -> assert false); |
|
90 |
"not", (function [Dbool b] -> Dbool (not b) | _ -> assert false); |
|
91 |
"+", (function [Dint a; Dint b] -> Dint (a+b) | _ -> assert false); |
|
92 |
"-", (function [Dint a; Dint b] -> Dint (a-b) | _ -> assert false); |
|
93 |
"*", (function [Dint a; Dint b] -> Dint (a*b) | _ -> assert false); |
|
94 |
"/", (function [Dint a; Dint b] -> Dint (a/b) | _ -> assert false); |
|
95 |
"mod", (function [Dint a; Dint b] -> Dint (a mod b) | _ -> assert false); |
|
96 |
"&&", (function [Dbool a; Dbool b] -> Dbool (a&&b) | _ -> assert false); |
|
97 |
"||", (function [Dbool a; Dbool b] -> Dbool (a||b) | _ -> assert false); |
|
98 |
"xor", (function [Dbool a; Dbool b] -> Dbool (a<>b) | _ -> assert false); |
|
99 |
"equi", (function [Dbool a; Dbool b] -> Dbool (a=b) | _ -> assert false); |
|
100 |
"impl", (function [Dbool a; Dbool b] -> Dbool (a<=b)| _ -> assert false); |
|
101 |
"<", (function [Dint a; Dint b] -> Dbool (a<b) | _ -> assert false); |
|
102 |
">", (function [Dint a; Dint b] -> Dbool (a>b) | _ -> assert false); |
|
103 |
"<=", (function [Dint a; Dint b] -> Dbool (a<=b) | _ -> assert false); |
|
104 |
">=", (function [Dint a; Dint b] -> Dbool (a>=b) | _ -> assert false); |
|
105 |
"!=", (function [a; b] -> Dbool (a<>b) | _ -> assert false); |
|
106 |
"=", (function [a; b] -> Dbool (a=b) | _ -> assert false); |
|
107 |
] |
|
136 |
let defs = |
|
137 |
[ |
|
138 |
("uminus", function [ Dint a ] -> Dint (-a) | _ -> assert false); |
|
139 |
("not", function [ Dbool b ] -> Dbool (not b) | _ -> assert false); |
|
140 |
("+", function [ Dint a; Dint b ] -> Dint (a + b) | _ -> assert false); |
|
141 |
("-", function [ Dint a; Dint b ] -> Dint (a - b) | _ -> assert false); |
|
142 |
("*", function [ Dint a; Dint b ] -> Dint (a * b) | _ -> assert false); |
|
143 |
("/", function [ Dint a; Dint b ] -> Dint (a / b) | _ -> assert false); |
|
144 |
( "mod", |
|
145 |
function [ Dint a; Dint b ] -> Dint (a mod b) | _ -> assert false ); |
|
146 |
( "&&", |
|
147 |
function [ Dbool a; Dbool b ] -> Dbool (a && b) | _ -> assert false ); |
|
148 |
( "||", |
|
149 |
function [ Dbool a; Dbool b ] -> Dbool (a || b) | _ -> assert false ); |
|
150 |
( "xor", |
|
151 |
function [ Dbool a; Dbool b ] -> Dbool (a <> b) | _ -> assert false ); |
|
152 |
( "equi", |
|
153 |
function [ Dbool a; Dbool b ] -> Dbool (a = b) | _ -> assert false ); |
|
154 |
( "impl", |
|
155 |
function [ Dbool a; Dbool b ] -> Dbool (a <= b) | _ -> assert false ); |
|
156 |
("<", function [ Dint a; Dint b ] -> Dbool (a < b) | _ -> assert false); |
|
157 |
(">", function [ Dint a; Dint b ] -> Dbool (a > b) | _ -> assert false); |
|
158 |
("<=", function [ Dint a; Dint b ] -> Dbool (a <= b) | _ -> assert false); |
|
159 |
(">=", function [ Dint a; Dint b ] -> Dbool (a >= b) | _ -> assert false); |
|
160 |
("!=", function [ a; b ] -> Dbool (a <> b) | _ -> assert false); |
|
161 |
("=", function [ a; b ] -> Dbool (a = b) | _ -> assert false); |
|
162 |
] |
|
108 | 163 |
in |
109 | 164 |
List.fold_left |
110 | 165 |
(fun env (op, op_eval) -> VE.add_value env op op_eval) |
111 |
VE.initial |
|
112 |
defs |
|
166 |
VE.initial defs |
|
167 |
|
|
168 |
let arith_funs = [ "+"; "-"; "*"; "/"; "mod"; "uminus" ] |
|
113 | 169 |
|
114 |
let arith_funs = ["+";"-";"*";"/";"mod"; "uminus"] |
|
115 |
let bool_funs = ["&&";"||";"xor";"equi";"impl"; "not"] |
|
116 |
let rel_funs = ["<";">";"<=";">=";"!=";"="] |
|
170 |
let bool_funs = [ "&&"; "||"; "xor"; "equi"; "impl"; "not" ] |
|
171 |
|
|
172 |
let rel_funs = [ "<"; ">"; "<="; ">="; "!="; "=" ] |
|
173 |
|
|
174 |
let internal_funs = arith_funs @ bool_funs @ rel_funs |
|
117 | 175 |
|
118 |
let internal_funs = arith_funs@bool_funs@rel_funs |
|
119 |
|
|
120 | 176 |
let rec is_internal_fun x targs = |
121 |
(*Format.eprintf "is_internal_fun %s %a@." x Types.print_ty (List.hd targs);*) |
|
177 |
(*Format.eprintf "is_internal_fun %s %a@." x Types.print_ty (List.hd targs);*)
|
|
122 | 178 |
match targs with |
123 |
| [] -> assert false |
|
124 |
| t::_ when Types.is_real_type t -> List.mem x internal_funs && not !Options.mpfr |
|
125 |
| t::_ when Types.is_array_type t -> is_internal_fun x [Types.array_element_type t] |
|
126 |
| _ -> List.mem x internal_funs |
|
179 |
| [] -> |
|
180 |
assert false |
|
181 |
| t :: _ when Types.is_real_type t -> |
|
182 |
List.mem x internal_funs && not !Options.mpfr |
|
183 |
| t :: _ when Types.is_array_type t -> |
|
184 |
is_internal_fun x [ Types.array_element_type t ] |
|
185 |
| _ -> |
|
186 |
List.mem x internal_funs |
|
127 | 187 |
|
128 | 188 |
let is_expr_internal_fun expr = |
129 | 189 |
let open Lustre_types in |
130 | 190 |
match expr.expr_desc with |
131 |
| Expr_appl (f, e, _) -> is_internal_fun f (Types.type_list_of_type e.expr_type) |
|
132 |
| _ -> assert false |
|
191 |
| Expr_appl (f, e, _) -> |
|
192 |
is_internal_fun f (Types.type_list_of_type e.expr_type) |
|
193 |
| _ -> |
|
194 |
assert false |
|
133 | 195 |
|
134 | 196 |
let is_value_internal_fun v = |
135 | 197 |
let open Machine_code_types in |
136 | 198 |
match v.value_desc with |
137 |
| Fun (f, vl) -> is_internal_fun f (List.map (fun v -> v.value_type) vl) |
|
138 |
| _ -> assert false |
|
139 |
|
|
140 |
let is_numeric_operator x = |
|
141 |
List.mem x arith_funs |
|
199 |
| Fun (f, vl) -> |
|
200 |
is_internal_fun f (List.map (fun v -> v.value_type) vl) |
|
201 |
| _ -> |
|
202 |
assert false |
|
142 | 203 |
|
143 |
let is_homomorphic_fun x = |
|
144 |
List.mem x internal_funs |
|
204 |
let is_numeric_operator x = List.mem x arith_funs |
|
145 | 205 |
|
146 |
let is_stateless_fun x = |
|
147 |
List.mem x internal_funs |
|
206 |
let is_homomorphic_fun x = List.mem x internal_funs |
|
148 | 207 |
|
208 |
let is_stateless_fun x = List.mem x internal_funs |
|
149 | 209 |
|
150 | 210 |
(* let pp_java i pp_val fmt vl = *) |
151 | 211 |
(* match i, vl with *) |
152 |
(* (\* | "ite", [v1; v2; v3] -> Format.fprintf fmt "(%a?(%a):(%a))" pp_val v1 pp_val v2 pp_val v3 *\) *) |
|
212 |
(* (\* | "ite", [v1; v2; v3] -> Format.fprintf fmt "(%a?(%a):(%a))" pp_val v1 |
|
213 |
pp_val v2 pp_val v3 *\) *) |
|
153 | 214 |
(* | "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v *) |
154 | 215 |
(* | "not", [v] -> Format.fprintf fmt "(!%a)" pp_val v *) |
155 |
(* | "impl", [v1; v2] -> Format.fprintf fmt "(!%a || %a)" pp_val v1 pp_val v2 *) |
|
156 |
(* | "=", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2 *) |
|
157 |
(* | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2 *) |
|
158 |
(* | "equi", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2 *) |
|
159 |
(* | "xor", [v1; v2] -> Format.fprintf fmt "(%a != %a)" pp_val v1 pp_val v2 *) |
|
160 |
(* | _, [v1; v2] -> Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2 *) |
|
161 |
(* | _ -> (Format.eprintf "internal error: Basic_library.pp_java %s@." i; assert false) *) |
|
216 |
(* | "impl", [v1; v2] -> Format.fprintf fmt "(!%a || %a)" pp_val v1 pp_val v2 *) |
|
217 |
(* | "=", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2 *) |
|
218 |
(* | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2 *) |
|
219 |
(* | "equi", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2 *) |
|
220 |
(* | "xor", [v1; v2] -> Format.fprintf fmt "(%a != %a)" pp_val v1 pp_val v2 *) |
|
221 |
(* | _, [v1; v2] -> Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2 *) |
|
222 |
(* | _ -> (Format.eprintf "internal error: Basic_library.pp_java %s@." i; assert |
|
223 |
false) *) |
|
162 | 224 |
|
163 | 225 |
let partial_eval op e opt = |
164 | 226 |
let open Lustre_types in |
165 | 227 |
let is_zero e = |
166 | 228 |
match e.expr_desc with |
167 |
| Expr_const (Const_int 0) -> true |
|
168 |
| Expr_const (Const_real r) when Real.is_zero r -> true |
|
169 |
| _ -> false |
|
229 |
| Expr_const (Const_int 0) -> |
|
230 |
true |
|
231 |
| Expr_const (Const_real r) when Real.is_zero r -> |
|
232 |
true |
|
233 |
| _ -> |
|
234 |
false |
|
170 | 235 |
in |
171 | 236 |
let is_one e = |
172 | 237 |
match e.expr_desc with |
173 |
| Expr_const (Const_int 1) -> true |
|
174 |
| Expr_const (Const_real r) when Real.is_one r -> true |
|
175 |
| _ -> false |
|
238 |
| Expr_const (Const_int 1) -> |
|
239 |
true |
|
240 |
| Expr_const (Const_real r) when Real.is_one r -> |
|
241 |
true |
|
242 |
| _ -> |
|
243 |
false |
|
176 | 244 |
in |
177 | 245 |
let is_true, is_false = |
178 | 246 |
let is_tag t e = e.expr_desc = Expr_const (Const_tag t) in |
179 | 247 |
is_tag tag_true, is_tag tag_false |
180 | 248 |
in |
181 |
let int_arith_op, real_arith_op= |
|
182 |
let assoc op= |
|
249 |
let int_arith_op, real_arith_op =
|
|
250 |
let assoc op =
|
|
183 | 251 |
match op with |
184 |
| "+" -> (+), Real.add |
|
185 |
| "-" -> (-), Real.minus |
|
186 |
| "*" -> ( * ), Real.times |
|
187 |
| "/" -> (/), Real.div |
|
188 |
| "mod" -> (mod), (fun _ _ -> assert false) |
|
189 |
| _ -> assert false |
|
252 |
| "+" -> |
|
253 |
( + ), Real.add |
|
254 |
| "-" -> |
|
255 |
( - ), Real.minus |
|
256 |
| "*" -> |
|
257 |
( * ), Real.times |
|
258 |
| "/" -> |
|
259 |
( / ), Real.div |
|
260 |
| "mod" -> |
|
261 |
( mod ), fun _ _ -> assert false |
|
262 |
| _ -> |
|
263 |
assert false |
|
190 | 264 |
in |
191 |
(fun op -> fst(assoc op)), (fun op -> snd(assoc op))
|
|
265 |
(fun op -> fst (assoc op)), fun op -> snd (assoc op)
|
|
192 | 266 |
in |
193 | 267 |
let int_rel_op, real_rel_op = |
194 | 268 |
let assoc op = |
195 | 269 |
match op with |
196 |
| "<" -> (<), Real.lt |
|
197 |
|">" -> (>), Real.gt |
|
198 |
|"<="-> (<=), Real.le |
|
199 |
| ">=" -> (>=), Real.ge |
|
200 |
|"!=" -> (!=), Real.diseq |
|
201 |
|"=" -> (=), Real.eq |
|
202 |
| _ -> assert false |
|
270 |
| "<" -> |
|
271 |
( < ), Real.lt |
|
272 |
| ">" -> |
|
273 |
( > ), Real.gt |
|
274 |
| "<=" -> |
|
275 |
( <= ), Real.le |
|
276 |
| ">=" -> |
|
277 |
( >= ), Real.ge |
|
278 |
| "!=" -> |
|
279 |
( != ), Real.diseq |
|
280 |
| "=" -> |
|
281 |
( = ), Real.eq |
|
282 |
| _ -> |
|
283 |
assert false |
|
203 | 284 |
in |
204 |
(fun op -> fst(assoc op)), (fun op -> snd(assoc op))
|
|
285 |
(fun op -> fst (assoc op)), fun op -> snd (assoc op)
|
|
205 | 286 |
in |
206 |
let eval_bool_fun op e1 e2 = |
|
207 |
let s2b s = if s= tag_true then true else if s=tag_false then false else assert false in |
|
287 |
let eval_bool_fun op e1 e2 = |
|
288 |
let s2b s = |
|
289 |
if s = tag_true then true |
|
290 |
else if s = tag_false then false |
|
291 |
else assert false |
|
292 |
in |
|
208 | 293 |
let e1, e2 = s2b e1, s2b e2 in |
209 | 294 |
let r = |
210 | 295 |
match op with |
211 |
"&&" -> e1 && e2 |
|
212 |
| "||" -> e1 || e2 |
|
213 |
| "xor" -> (e1 && e2) || ((not e1) && (not e2)) |
|
214 |
| "impl" -> (not e1) || e2 |
|
215 |
| "equi" -> ((not e1) || e2) && ((not e2) || e1) |
|
216 |
| _ -> assert false |
|
296 |
| "&&" -> |
|
297 |
e1 && e2 |
|
298 |
| "||" -> |
|
299 |
e1 || e2 |
|
300 |
| "xor" -> |
|
301 |
(e1 && e2) || ((not e1) && not e2) |
|
302 |
| "impl" -> |
|
303 |
(not e1) || e2 |
|
304 |
| "equi" -> |
|
305 |
((not e1) || e2) && ((not e2) || e1) |
|
306 |
| _ -> |
|
307 |
assert false |
|
217 | 308 |
in |
218 | 309 |
if r then Const_tag tag_true else Const_tag tag_false |
219 |
in |
|
220 |
let is_const e = |
|
221 |
match e.expr_desc with Expr_const _ -> true | _ -> false |
|
222 | 310 |
in |
311 |
let is_const e = match e.expr_desc with Expr_const _ -> true | _ -> false in |
|
223 | 312 |
let deconst e = |
224 |
match e.expr_desc with |
|
225 |
| Expr_const c -> c |
|
226 |
| _ -> assert false |
|
313 |
match e.expr_desc with Expr_const c -> c | _ -> assert false |
|
227 | 314 |
in |
228 |
match op, (match e.expr_desc with Expr_tuple el -> el | _ -> [e]) with
|
|
229 |
| _, el when List.for_all is_const el -> (
|
|
230 |
let new_cst =
|
|
315 |
match op, match e.expr_desc with Expr_tuple el -> el | _ -> [ e ] with
|
|
316 |
| _, el when List.for_all is_const el -> |
|
317 |
let new_cst = |
|
231 | 318 |
match op, List.map deconst el with |
232 |
| ("+"|"-"|"*"|"/"|"mod"), [Const_int c1; Const_int c2] -> |
|
233 |
Const_int (int_arith_op op c1 c2) |
|
234 |
| ("+"|"-"|"*"|"/"), [Const_real c1; Const_real c2] -> |
|
235 |
Const_real (real_arith_op op c1 c2) |
|
236 |
| "uminus", [Const_int c] -> Const_int (-c) |
|
237 |
| "uminus", [Const_real c] -> Const_real (Real.uminus c) |
|
238 |
| rel_fun, [Const_int c1; Const_int c2] |
|
239 |
when List.mem rel_fun rel_funs -> |
|
240 |
if int_rel_op op c1 c2 then |
|
241 |
Const_tag tag_true |
|
242 |
else |
|
243 |
Const_tag tag_false |
|
244 |
| rel_fun, [Const_real c1; Const_real c2] |
|
245 |
when List.mem rel_fun rel_funs -> |
|
246 |
if real_rel_op op c1 c2 then |
|
247 |
Const_tag tag_true |
|
248 |
else |
|
249 |
Const_tag tag_false |
|
250 |
| "=", [Const_tag t1; Const_tag t2] |
|
251 |
-> |
|
252 |
if t1 = t2 then |
|
253 |
Const_tag tag_true |
|
254 |
else |
|
255 |
Const_tag tag_false |
|
256 |
| "!=", [Const_tag t1; Const_tag t2] |
|
257 |
-> |
|
258 |
if t1 = t2 then |
|
259 |
Const_tag tag_false |
|
260 |
else |
|
261 |
Const_tag tag_true |
|
262 |
| "not", [Const_tag c] -> Const_tag( if c = tag_true then tag_false else if c = tag_false then tag_true else assert false) |
|
263 |
| bool_fun, [Const_tag c1; Const_tag c2] |
|
264 |
when List.mem bool_fun bool_funs -> |
|
265 |
eval_bool_fun bool_fun c1 c2 |
|
266 |
| _ -> let loc= e.expr_loc in |
|
267 |
let err =Error.Unbound_symbol (op ^ (string_of_bool (List.mem op rel_funs)) ^ " in basic library") in |
|
268 |
raise (Error.Error (loc, err)) |
|
319 |
| ("+" | "-" | "*" | "/" | "mod"), [ Const_int c1; Const_int c2 ] -> |
|
320 |
Const_int (int_arith_op op c1 c2) |
|
321 |
| ("+" | "-" | "*" | "/"), [ Const_real c1; Const_real c2 ] -> |
|
322 |
Const_real (real_arith_op op c1 c2) |
|
323 |
| "uminus", [ Const_int c ] -> |
|
324 |
Const_int (-c) |
|
325 |
| "uminus", [ Const_real c ] -> |
|
326 |
Const_real (Real.uminus c) |
|
327 |
| rel_fun, [ Const_int c1; Const_int c2 ] when List.mem rel_fun rel_funs |
|
328 |
-> |
|
329 |
if int_rel_op op c1 c2 then Const_tag tag_true else Const_tag tag_false |
|
330 |
| rel_fun, [ Const_real c1; Const_real c2 ] when List.mem rel_fun rel_funs |
|
331 |
-> |
|
332 |
if real_rel_op op c1 c2 then Const_tag tag_true else Const_tag tag_false |
|
333 |
| "=", [ Const_tag t1; Const_tag t2 ] -> |
|
334 |
if t1 = t2 then Const_tag tag_true else Const_tag tag_false |
|
335 |
| "!=", [ Const_tag t1; Const_tag t2 ] -> |
|
336 |
if t1 = t2 then Const_tag tag_false else Const_tag tag_true |
|
337 |
| "not", [ Const_tag c ] -> |
|
338 |
Const_tag |
|
339 |
(if c = tag_true then tag_false |
|
340 |
else if c = tag_false then tag_true |
|
341 |
else assert false) |
|
342 |
| bool_fun, [ Const_tag c1; Const_tag c2 ] |
|
343 |
when List.mem bool_fun bool_funs -> |
|
344 |
eval_bool_fun bool_fun c1 c2 |
|
345 |
| _ -> |
|
346 |
let loc = e.expr_loc in |
|
347 |
let err = |
|
348 |
Error.Unbound_symbol |
|
349 |
(op ^ string_of_bool (List.mem op rel_funs) ^ " in basic library") |
|
350 |
in |
|
351 |
raise (Error.Error (loc, err)) |
|
269 | 352 |
in |
270 |
Expr_const new_cst
|
|
271 |
)
|
|
272 |
| op, el -> ( (* at least one of the arguments is non constant *)
|
|
353 |
Expr_const new_cst |
|
354 |
| op, el -> (
|
|
355 |
(* at least one of the arguments is non constant *)
|
|
273 | 356 |
match op, el with |
274 |
| "+", [e0; e] when is_zero e0 -> |
|
275 |
e.expr_desc |
|
276 |
| "+", [e; e0] when is_zero e0 -> |
|
277 |
e.expr_desc |
|
278 |
| "-", [e; e0] when is_zero e0 -> |
|
279 |
e.expr_desc |
|
280 |
| "-", [e0; e] when is_zero e0 -> |
|
281 |
Expr_appl("uminus", e, None) |
|
282 |
| ("*"|"/"), [e0; _] when is_zero e0 -> e0.expr_desc |
|
283 |
| "*", [_; e0] when is_zero e0 -> e0.expr_desc |
|
284 |
| "*", [e1; e] when is_one e1 -> e.expr_desc |
|
285 |
| "/", [e; e1] when is_one e1 -> e.expr_desc |
|
286 |
| "&&", [efalse; _] when is_false efalse -> |
|
287 |
Expr_const (Const_tag tag_false) |
|
288 |
| "&&", [_; efalse] when is_false efalse -> |
|
289 |
Expr_const (Const_tag tag_false) |
|
290 |
| "||", [etrue; _] when is_true etrue -> |
|
291 |
Expr_const (Const_tag tag_true) |
|
292 |
| "||", [_; etrue] when is_true etrue -> |
|
293 |
Expr_const (Const_tag tag_true) |
|
294 |
| "impl", [efalse; _] when is_false efalse -> |
|
295 |
Expr_const (Const_tag tag_true) |
|
357 |
| "+", [ e0; e ] when is_zero e0 -> |
|
358 |
e.expr_desc |
|
359 |
| "+", [ e; e0 ] when is_zero e0 -> |
|
360 |
e.expr_desc |
|
361 |
| "-", [ e; e0 ] when is_zero e0 -> |
|
362 |
e.expr_desc |
|
363 |
| "-", [ e0; e ] when is_zero e0 -> |
|
364 |
Expr_appl ("uminus", e, None) |
|
365 |
| ("*" | "/"), [ e0; _ ] when is_zero e0 -> |
|
366 |
e0.expr_desc |
|
367 |
| "*", [ _; e0 ] when is_zero e0 -> |
|
368 |
e0.expr_desc |
|
369 |
| "*", [ e1; e ] when is_one e1 -> |
|
370 |
e.expr_desc |
|
371 |
| "/", [ e; e1 ] when is_one e1 -> |
|
372 |
e.expr_desc |
|
373 |
| "&&", [ efalse; _ ] when is_false efalse -> |
|
374 |
Expr_const (Const_tag tag_false) |
|
375 |
| "&&", [ _; efalse ] when is_false efalse -> |
|
376 |
Expr_const (Const_tag tag_false) |
|
377 |
| "||", [ etrue; _ ] when is_true etrue -> |
|
378 |
Expr_const (Const_tag tag_true) |
|
379 |
| "||", [ _; etrue ] when is_true etrue -> |
|
380 |
Expr_const (Const_tag tag_true) |
|
381 |
| "impl", [ efalse; _ ] when is_false efalse -> |
|
382 |
Expr_const (Const_tag tag_true) |
|
296 | 383 |
| _ -> |
297 |
Expr_appl(op, e, opt) |
|
298 |
) |
|
299 |
(* Local Variables: *) |
|
300 |
(* compile-command:"make -C .." *) |
|
301 |
(* End: *) |
|
384 |
Expr_appl (op, e, opt)) |
|
302 | 385 |
|
386 |
(* Local Variables: *) |
|
387 |
(* compile-command:"make -C .." *) |
|
388 |
(* End: *) |
|
303 | 389 |
|
304 | 390 |
let _ = |
305 | 391 |
(* Loading environement *) |
Also available in: Unified diff
reformatting