Revision 53206908 src/basic_library.ml
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 
113  113  
114 
let internal_funs = ["+";"";"*";"/";"mod";"&&";"";"xor";"equi";"impl";"<";">";"<=";">=";"!=";"=";"uminus";"not"] 

114 
let bool_ops = ["&&";"";"xor";"equi";"impl";"not"] 

115 
let rel_ops = ["<";">";"<=";">=";"!=";"="] 

116 
let num_ops = ["+";"";"*";"/";"mod";"uminus"] 

117  
118 
let internal_funs = bool_ops@rel_ops@num_ops 

119  
120 
let rec is_internal_fun x targs = 

121 
(*Format.eprintf "is_internal_fun %s %a@." x Types.print_ty (List.hd targs);*) 

122 
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 

127  
128 
let is_expr_internal_fun expr = 

129 
match expr.expr_desc with 

130 
 Expr_appl (f, e, _) > is_internal_fun f (Types.type_list_of_type e.expr_type) 

131 
 _ > assert false 

115  132  
116 
let is_internal_fun x = 

133 
let is_value_internal_fun v = 

134 
match v.value_desc with 

135 
 Fun (f, vl) > is_internal_fun f (List.map (fun v > v.value_type) vl) 

136 
 _ > assert false 

137  
138 
let is_numeric_operator x = 

139 
List.mem x num_ops 

140  
141 
let is_homomorphic_fun x = 

142 
List.mem x internal_funs 

143  
144 
let is_stateless_fun x = 

117  145 
List.mem x internal_funs 
118  146  
119  147 
let pp_c i pp_val fmt vl = 
...  ...  
133  161 
match i, vl with 
134  162 
(*  "ite", [v1; v2; v3] > Format.fprintf fmt "(%a?(%a):(%a))" pp_val v1 pp_val v2 pp_val v3 *) 
135  163 
 "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 

164 
 "not", [v] > Format.fprintf fmt "(!%a)" pp_val v


165 
 "impl", [v1; v2] > Format.fprintf fmt "(!%a  %a)" pp_val v1 pp_val v2


166 
 "=", [v1; v2] > Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2


139  167 
 "mod", [v1; v2] > Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2 
140  168 
 "equi", [v1; v2] > Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2 
141  169 
 "xor", [v1; v2] > Format.fprintf fmt "(%a != %a)" pp_val v1 pp_val v2 
142  170 
 _, [v1; v2] > Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2 
143  171 
 _ > (Format.eprintf "internal error: Basic_library.pp_java %s@." i; assert false) 
144  172  
145 
let pp_horn i pp_val fmt vl = 

173 
let pp_horn i pp_val fmt vl =


146  174 
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 

148  
175 
 "ite", [v1; v2; v3] > Format.fprintf fmt "(@[<hov 2>ite %a@ %a@ %a@])" pp_val v1 pp_val v2 pp_val v3 

149  176 
 "uminus", [v] > Format.fprintf fmt "( %a)" pp_val v 
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 

177 
 "not", [v] > Format.fprintf fmt "(not %a)" pp_val v


178 
 "=", [v1; v2] > Format.fprintf fmt "(= %a %a)" pp_val v1 pp_val v2


179 
 "&&", [v1; v2] > Format.fprintf fmt "(and %a %a)" pp_val v1 pp_val v2


180 
 "", [v1; v2] > Format.fprintf fmt "(or %a %a)" pp_val v1 pp_val v2


181 
 "impl", [v1; v2] > Format.fprintf fmt "(=> %a %a)" pp_val v1 pp_val v2


155  182 
 "mod", [v1; v2] > Format.fprintf fmt "(mod %a %a)" pp_val v1 pp_val v2 
156  183 
 "equi", [v1; v2] > Format.fprintf fmt "(%a = %a)" pp_val v1 pp_val v2 
157  184 
 "xor", [v1; v2] > Format.fprintf fmt "(%a xor %a)" pp_val v1 pp_val v2 
Also available in: Unified diff