63 open Hints_declaration
121 (** val typ_eq_dec : AST.typ -> AST.typ -> (__, __) Types.sum **)
122 let typ_eq_dec t1 t2 =
124 | AST.ASTint (x, x0) ->
126 | AST.ASTint (sz, sg) ->
132 AST.typ_eq (AST.ASTint (AST.I8, sg')) (AST.ASTint (AST.I8, sg))
134 AST.typ_eq (AST.ASTint (AST.I16, sg')) (AST.ASTint (AST.I8,
137 AST.typ_eq (AST.ASTint (AST.I32, sg')) (AST.ASTint (AST.I8,
142 AST.typ_eq (AST.ASTint (AST.I8, sg')) (AST.ASTint (AST.I16,
145 AST.typ_eq (AST.ASTint (AST.I16, sg')) (AST.ASTint (AST.I16,
148 AST.typ_eq (AST.ASTint (AST.I32, sg')) (AST.ASTint (AST.I16,
153 AST.typ_eq (AST.ASTint (AST.I8, sg')) (AST.ASTint (AST.I32,
156 AST.typ_eq (AST.ASTint (AST.I16, sg')) (AST.ASTint (AST.I32,
159 AST.typ_eq (AST.ASTint (AST.I32, sg')) (AST.ASTint (AST.I32,
161 | AST.ASTptr -> (fun sz sg -> Types.Inr __)) x x0
164 | AST.ASTint (sz, sg) -> Types.Inr __
165 | AST.ASTptr -> Types.Inl __)
167 (** val block_DeqSet : Deqsets.deqSet **)
169 Obj.magic Pointers.eq_block
171 (** val mem_assoc_env :
172 AST.ident -> (AST.ident, Csyntax.type0) Types.prod List.list -> Bool.bool **)
173 let rec mem_assoc_env i = function
174 | List.Nil -> Bool.False
175 | List.Cons (hd, tl) ->
176 let { Types.fst = id; Types.snd = ty } = hd in
177 (match Identifiers.identifier_eq PreIdentifiers.SymbolTag i id with
178 | Types.Inl _ -> Bool.True
179 | Types.Inr _ -> mem_assoc_env i tl)
181 type 'a lset = 'a List.list
183 (** val empty_lset : 'a1 List.list **)
187 (** val lset_union : 'a1 lset -> 'a1 lset -> 'a1 List.list **)
188 let lset_union l1 l2 =
191 (** val lset_remove : Deqsets.deqSet -> __ lset -> __ -> __ List.list **)
192 let lset_remove a l elt =
193 List.filter (fun x -> Bool.notb (Deqsets.eqb a x elt)) l
195 (** val lset_difference :
196 Deqsets.deqSet -> __ lset -> __ lset -> __ List.list **)
197 let lset_difference a l1 l2 =
198 List.filter (fun x -> Bool.notb (Listb.memb a x l2)) l1
200 (** val wF_rect : ('a1 -> __ -> ('a1 -> __ -> 'a2) -> 'a2) -> 'a1 -> 'a2 **)
201 let rec wF_rect f x =
202 f x __ (fun y _ -> wF_rect f y)
204 (** val one_bv : Nat.nat -> BitVector.bitVector **)
206 (Arithmetic.add_with_carries n (BitVector.zero n) (BitVector.zero n)
210 Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
212 let rec ith_carry n a b init =
214 | Nat.O -> (fun x x0 -> init)
217 let hd_a = Vector.head' x a' in
218 let hd_b = Vector.head' x b' in
219 let tl_a = Vector.tail x a' in
220 let tl_b = Vector.tail x b' in
221 Arithmetic.carry_of hd_a hd_b (ith_carry x tl_a tl_b init))) a b
224 Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
226 let ith_bit n a b init =
228 | Nat.O -> (fun x x0 -> init)
231 let hd_a = Vector.head' x a' in
232 let hd_b = Vector.head' x b' in
233 let tl_a = Vector.tail x a' in
234 let tl_b = Vector.tail x b' in
235 Bool.xorb (Bool.xorb hd_a hd_b) (ith_carry x tl_a tl_b init))) a b
237 (** val bitvector_fold :
238 Nat.nat -> BitVector.bitVector -> (Nat.nat -> BitVector.bitVector ->
239 Bool.bool) -> BitVector.bitVector **)
240 let rec bitvector_fold n v f =
242 | Vector.VEmpty -> Vector.VEmpty
243 | Vector.VCons (sz, elt, tl) ->
244 let bit = f n v in Vector.VCons (sz, bit, (bitvector_fold sz tl f))
246 (** val bitvector_fold2 :
247 Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> (Nat.nat ->
248 BitVector.bitVector -> BitVector.bitVector -> Bool.bool) ->
249 BitVector.bitVector **)
250 let rec bitvector_fold2 n v1 v2 f =
252 | Vector.VEmpty -> (fun x -> Vector.VEmpty)
253 | Vector.VCons (sz, elt, tl) ->
255 let bit = f n v1 v2 in
256 Vector.VCons (sz, bit, (bitvector_fold2 sz tl (Vector.tail sz v2') f))))
259 (** val addition_n_direct :
260 Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
261 BitVector.bitVector **)
262 let addition_n_direct n v1 v2 init =
263 bitvector_fold2 n v1 v2 (fun n0 v10 v20 -> ith_bit n0 v10 v20 init)
265 (** val increment_direct :
266 Nat.nat -> BitVector.bitVector -> BitVector.bitVector **)
267 let increment_direct n v =
268 addition_n_direct n v (one_bv n) Bool.False
270 (** val twocomp_neg_direct :
271 Nat.nat -> BitVector.bitVector -> BitVector.bitVector **)
272 let twocomp_neg_direct n v =
273 increment_direct n (BitVector.negation_bv n v)
275 (** val andb_fold : Nat.nat -> BitVector.bitVector -> Bool.bool **)
276 let rec andb_fold n = function
277 | Vector.VEmpty -> Bool.True
278 | Vector.VCons (sz, elt, tl) -> Bool.andb elt (andb_fold sz tl)