Library Coq.Numbers.Cyclic.Int31.Int31
31-bit integers
This file contains basic definitions of a 31-bit integer
arithmetic. In fact it is more general than that. The only reason
for this use of 31 is the underlying mecanism for hardware-efficient
computations by A. Spiwack. Apart from this, a switch to, say,
63-bit integers is now just a matter of replacing every occurences
of 31 by 63. This is actually made possible by the use of
dependently-typed n-ary constructions for the inductive type
int31, its constructor
I31 and any pattern matching on it.
If you modify this file, please preserve this genericity.
Definition size := 31%
nat.
Digits
The type of 31-bit integers
The type
int31 has a unique constructor
I31 that expects
31 arguments of type
digits.
Constants
Zero is
I31 D0 ... D0
One is I31 D0 ... D0 D1
The biggest integer is I31 D1 ... D1, corresponding to (2^size)-1
Two is I31 D0 ... D0 D1 D0
Bits manipulation
sneakr b x shifts
x to the right by one bit.
Rightmost digit is lost while leftmost digit becomes
b.
Pseudo-code is
match x with (I31 d0 ... dN) => I31 b d0 ... d(N-1) end
sneakl b x shifts x to the left by one bit.
Leftmost digit is lost while rightmost digit becomes b.
Pseudo-code is
match x with (I31 d0 ... dN) => I31 d1 ... dN b end
shiftl, shiftr, twice and twice_plus_one are direct
consequences of sneakl and sneakr.
firstl x returns the leftmost digit of number x.
Pseudo-code is match x with (I31 d0 ... dN) => d0 end
firstr x returns the rightmost digit of number x.
Pseudo-code is match x with (I31 d0 ... dN) => dN end
iszero x is true iff x = I31 D0 ... D0. Pseudo-code is
match x with (I31 D0 ... D0) => true | _ => false end
base is 2^31, obtained via iterations of Z.double.
It can also be seen as the smallest b > 0 s.t. phi_inv b = 0
(see below)
Conversions
From int31 to Z, we simply iterates
Z.double or
Z.succ_double.
From positive to int31. An abstract definition could be :
phi_inv (2n) = 2*(phi_inv n) /\
phi_inv 2n+1 = 2*(phi_inv n) + 1
The negative part : 2-complement
A simple incrementation function
We can now define the conversion from Z to int31.
phi_inv2 is similar to phi_inv but returns a double word
zn2z int31
phi2 is similar to phi but takes a double word (two args)
Addition
Addition modulo
2^31
Addition with carry (the result is thus exact)
Addition plus one with carry (the result is thus exact)
Substraction
Subtraction modulo
2^31
Subtraction with carry (thus exact)
subtraction minus one with carry (thus exact)
Opposite
Definition opp31 x :=
On - x.
Notation "- x" := (
opp31 x) :
int31_scope.
Multiplication
multiplication modulo
2^31
multiplication with double word result (thus exact)
Division
Division of a double size word modulo
2^31
Division modulo 2^31
Computing the i-th iterate of a function:
iter_int31 i A f = f^i
Combining the (31-p) low bits of i above the p high bits of j:
addmuldiv31 p i j = i*2^p+j/2^(31-p) (modulo 2^31)
Square root functions using newton iteration
we use a very naive upper-bound on the iteration
2^31 instead of the usual 31.
Definition sqrt31_step (
rec:
int31 ->
int31 ->
int31) (
i j:
int31) :=
Eval lazy delta [
Twon]
in
let (
quo,
_) :=
i/j in
match quo ?= j with
Lt =>
rec i (
fst (
(j + quo)/Twon))
|
_ =>
j
end.
Fixpoint iter31_sqrt (
n:
nat) (
rec:
int31 ->
int31 ->
int31)
(
i j:
int31) {
struct n} :
int31 :=
sqrt31_step
(
match n with
O =>
rec
|
S n => (
iter31_sqrt n (
iter31_sqrt n rec))
end)
i j.
Definition sqrt31 i :=
Eval lazy delta [
On In Twon]
in
match compare31 In i with
Gt =>
On
|
Eq =>
In
|
Lt =>
iter31_sqrt 31 (
fun i j =>
j)
i (
fst (
i/Twon))
end.
Definition v30 :=
Eval compute in (
addmuldiv31 (
phi_inv (
Z.of_nat size - 1))
In On).
Definition sqrt312_step (
rec:
int31 ->
int31 ->
int31 ->
int31)
(
ih il j:
int31) :=
Eval lazy delta [
Twon v30]
in
match ih ?= j with Eq =>
j |
Gt =>
j |
_ =>
let (
quo,
_) :=
div3121 ih il j in
match quo ?= j with
Lt =>
let m :=
match j +c quo with
C0 m1 =>
fst (
m1/Twon)
|
C1 m1 =>
fst (
m1/Twon)
+ v30
end in rec ih il m
|
_ =>
j
end end.
Fixpoint iter312_sqrt (
n:
nat)
(
rec:
int31 ->
int31 ->
int31 ->
int31)
(
ih il j:
int31) {
struct n} :
int31 :=
sqrt312_step
(
match n with
O =>
rec
|
S n => (
iter312_sqrt n (
iter312_sqrt n rec))
end)
ih il j.
Definition sqrt312 ih il :=
Eval lazy delta [
On In]
in
let s :=
iter312_sqrt 31 (
fun ih il j =>
j)
ih il Tn in
match s *c s with
W0 =>
(On, C0 On)
|
WW ih1 il1 =>
match il -c il1 with
C0 il2 =>
match ih ?= ih1 with
Gt =>
(s, C1 il2)
|
_ =>
(s, C0 il2)
end
|
C1 il2 =>
match (ih - In) ?= ih1 with
Gt =>
(s, C1 il2)
|
_ =>
(s, C0 il2)
end
end
end.
Fixpoint p2i n p : (
N*int31)%
type :=
match n with
|
O =>
(Npos p, On)
|
S n =>
match p with
|
xO p =>
let (
r,
i) :=
p2i n p in (r, Twon*i)
|
xI p =>
let (
r,
i) :=
p2i n p in (r, Twon*i+In)
|
xH =>
(N0, In)
end
end.
Definition positive_to_int31 (
p:
positive) :=
p2i size p.
Constant 31 converted into type int31.
It is used as default answer for numbers of zeros
in head0 and tail0