11 open Hints_declaration
53 (** val z_of_unsigned_bitvector : Nat.nat -> BitVector.bitVector -> Z.z **)
54 let rec z_of_unsigned_bitvector n = function
55 | Vector.VEmpty -> Z.OZ
56 | Vector.VCons (n', h, t) ->
60 (Vector.fold_left n' (fun acc b ->
62 | Bool.True -> Positive.P1 acc
63 | Bool.False -> Positive.P0 acc) Positive.One t)
64 | Bool.False -> z_of_unsigned_bitvector n' t)
66 (** val z_of_signed_bitvector : Nat.nat -> BitVector.bitVector -> Z.z **)
67 let z_of_signed_bitvector n = function
68 | Vector.VEmpty -> Z.OZ
69 | Vector.VCons (n', h, t) ->
73 (Z.zsucc (z_of_unsigned_bitvector n' (BitVector.negation_bv n' t)))
74 | Bool.False -> z_of_unsigned_bitvector n' t)
76 (** val bits_of_pos : Positive.pos -> Bool.bool List.list **)
77 let rec bits_of_pos = function
78 | Positive.One -> List.Cons (Bool.True, List.Nil)
79 | Positive.P1 p' -> List.Cons (Bool.True, (bits_of_pos p'))
80 | Positive.P0 p' -> List.Cons (Bool.False, (bits_of_pos p'))
82 (** val zeroext_reversed :
83 Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector **)
84 let rec zeroext_reversed n m bv =
86 | Nat.O -> Vector.VEmpty
89 | Vector.VEmpty -> BitVector.zero (Nat.S m')
90 | Vector.VCons (n', h, t) ->
91 Vector.VCons (m', h, (zeroext_reversed n' m' t)))
93 (** val bitvector_of_Z : Nat.nat -> Z.z -> BitVector.bitVector **)
94 let rec bitvector_of_Z n = function
95 | Z.OZ -> BitVector.zero n
97 let bits = bits_of_pos p in
99 (zeroext_reversed (List.length bits) n (Vector.vector_of_list bits))
102 | Positive.One -> BitVector.maximum n
104 let bits = bits_of_pos (Positive.pred p) in
107 (zeroext_reversed (List.length bits) n (Vector.vector_of_list bits))
109 BitVector.negation_bv n pz
111 let bits = bits_of_pos (Positive.pred p) in
114 (zeroext_reversed (List.length bits) n (Vector.vector_of_list bits))
116 BitVector.negation_bv n pz)
118 (** val pos_length : Positive.pos -> Nat.nat **)
119 let rec pos_length = function
120 | Positive.One -> Nat.O
121 | Positive.P1 q -> Nat.S (pos_length q)
122 | Positive.P0 q -> Nat.S (pos_length q)