source: extracted/bitVectorZ.ml @ 2649

Last change on this file since 2649 was 2649, checked in by sacerdot, 7 years ago

...

File size: 2.6 KB
Line 
1open Preamble
2
3open Types
4
5open Bool
6
7open Relations
8
9open Nat
10
11open Hints_declaration
12
13open Core_notation
14
15open Pts
16
17open Logic
18
19open Positive
20
21open Z
22
23open Extranat
24
25open Vector
26
27open Div_and_mod
28
29open Jmeq
30
31open Russell
32
33open List
34
35open Util
36
37open FoldStuff
38
39open BitVector
40
41open Arithmetic
42
43open Division
44
45(** val z_of_unsigned_bitvector : Nat.nat -> BitVector.bitVector -> Z.z **)
46let rec z_of_unsigned_bitvector n = function
47| Vector.VEmpty -> Z.OZ
48| Vector.VCons (n', h, t) ->
49  (match h with
50   | Bool.True ->
51     Z.Pos
52       (Vector.fold_left n' (fun acc b ->
53         match b with
54         | Bool.True -> Positive.P1 acc
55         | Bool.False -> Positive.P0 acc) Positive.One t)
56   | Bool.False -> z_of_unsigned_bitvector n' t)
57
58(** val z_of_signed_bitvector : Nat.nat -> BitVector.bitVector -> Z.z **)
59let z_of_signed_bitvector n = function
60| Vector.VEmpty -> Z.OZ
61| Vector.VCons (n', h, t) ->
62  (match h with
63   | Bool.True ->
64     Z.zopp
65       (Z.zsucc (z_of_unsigned_bitvector n' (BitVector.negation_bv n' t)))
66   | Bool.False -> z_of_unsigned_bitvector n' t)
67
68(** val bits_of_pos : Positive.pos -> Bool.bool List.list **)
69let rec bits_of_pos = function
70| Positive.One -> List.Cons (Bool.True, List.Nil)
71| Positive.P1 p' -> List.Cons (Bool.True, (bits_of_pos p'))
72| Positive.P0 p' -> List.Cons (Bool.False, (bits_of_pos p'))
73
74(** val zeroext_reversed :
75    Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector **)
76let rec zeroext_reversed n m bv =
77  match m with
78  | Nat.O -> Vector.VEmpty
79  | Nat.S m' ->
80    (match bv with
81     | Vector.VEmpty -> BitVector.zero (Nat.S m')
82     | Vector.VCons (n', h, t) ->
83       Vector.VCons (m', h, (zeroext_reversed n' m' t)))
84
85(** val bitvector_of_Z : Nat.nat -> Z.z -> BitVector.bitVector **)
86let rec bitvector_of_Z n = function
87| Z.OZ -> BitVector.zero n
88| Z.Pos p ->
89  let bits = bits_of_pos p in
90  Vector.reverse0 n
91    (zeroext_reversed (List.length bits) n (Vector.vector_of_list bits))
92| Z.Neg p ->
93  (match p with
94   | Positive.One -> BitVector.maximum n
95   | Positive.P1 x ->
96     let bits = bits_of_pos (Positive.pred0 p) in
97     let pz =
98       Vector.reverse0 n
99         (zeroext_reversed (List.length bits) n (Vector.vector_of_list bits))
100     in
101     BitVector.negation_bv n pz
102   | Positive.P0 x ->
103     let bits = bits_of_pos (Positive.pred0 p) in
104     let pz =
105       Vector.reverse0 n
106         (zeroext_reversed (List.length bits) n (Vector.vector_of_list bits))
107     in
108     BitVector.negation_bv n pz)
109
110(** val pos_length : Positive.pos -> Nat.nat **)
111let rec pos_length = function
112| Positive.One -> Nat.O
113| Positive.P1 q -> Nat.S (pos_length q)
114| Positive.P0 q -> Nat.S (pos_length q)
115
Note: See TracBrowser for help on using the repository browser.