1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
let pos_of_z z =
let open Z.Compare in
assert (Z.one <= z);
let rec pos_of_z z =
if z <= Z.one then BinNums.Coq_xH
else
let p = pos_of_z (Z.shift_right z 1) in
if (Z.erem z (Z.of_int 2)) = Z.one
then BinNums.Coq_xI p
else BinNums.Coq_xO p
in pos_of_z z
let rec z_of_pos pos =
let open Z in
match pos with
| BinNums.Coq_xH -> Z.one
| BinNums.Coq_xO p -> Z.shift_left (z_of_pos p) 1
| BinNums.Coq_xI p -> Z.shift_left (z_of_pos p) 1 + Z.one
let cz_of_z z =
let open Z.Compare in
if z = Z.zero then BinNums.Z0
else if z < Z.zero then BinNums.Zneg (pos_of_z (Z.abs z))
else BinNums.Zpos (pos_of_z z)
let z_of_cz z =
match z with
| BinNums.Zneg p -> Z.neg (z_of_pos p)
| BinNums.Z0 -> Z.zero
| BinNums.Zpos p -> z_of_pos p
let cz_of_int i = cz_of_z (Z.of_int i)
let int_of_cz z = Z.to_int (z_of_cz z)