Library Coq.Numbers.Cyclic.Int63.Sint63
Require Import ZArith.
Import Znumtheory.
Require Export Uint63.
Require Int63.
Require Import Lia.
Declare Scope sint63_scope.
Definition printer (
x :
int_wrapper) :
pos_neg_int63 :=
if (
int_wrap x <? 4611686018427387904)%
uint63 then
Pos (
int_wrap x)
else
Neg (
(int_wrap x) lxor max_int + 1)%
uint63.
Definition parser (
x :
pos_neg_int63) :
option int :=
match x with
|
Pos p =>
if (
p <? 4611686018427387904)%
uint63 then Some p else None
|
Neg n =>
if (
n <=? 4611686018427387904)%
uint63
then Some (
(n - 1
) lxor max_int)%
uint63 else None
end.
Module Import Sint63NotationsInternalA.
Delimit Scope sint63_scope with sint63.
Bind Scope sint63_scope with int.
End Sint63NotationsInternalA.
Module Import Sint63NotationsInternalB.
Infix "<<" :=
Int63.lsl (
at level 30,
no associativity) :
sint63_scope.
Infix ">>" :=
asr (
at level 30,
no associativity) :
sint63_scope.
Infix "land" :=
Int63.land (
at level 40,
left associativity) :
sint63_scope.
Infix "lor" :=
Int63.lor (
at level 40,
left associativity) :
sint63_scope.
Infix "lxor" :=
Int63.lxor (
at level 40,
left associativity) :
sint63_scope.
Infix "+" :=
Int63.add :
sint63_scope.
Infix "-" :=
Int63.sub :
sint63_scope.
Infix "*" :=
Int63.mul :
sint63_scope.
Infix "/" :=
divs :
sint63_scope.
Infix "mod" :=
mods (
at level 40,
no associativity) :
sint63_scope.
Infix "=?" :=
Int63.eqb (
at level 70,
no associativity) :
sint63_scope.
Infix "<?" :=
ltsb (
at level 70,
no associativity) :
sint63_scope.
Infix "<=?" :=
lesb (
at level 70,
no associativity) :
sint63_scope.
Infix "≤?" :=
lesb (
at level 70,
no associativity) :
sint63_scope.
Notation "- x" := (
opp x) :
sint63_scope.
Notation "n ?= m" := (
compares n m)
(
at level 70,
no associativity) :
sint63_scope.
End Sint63NotationsInternalB.
Definition min_int :=
Eval vm_compute in (
lsl 1 62).
Definition max_int :=
Eval vm_compute in (
min_int - 1)%
sint63.
Translation to and from Z
Centered modulo
Specification of operations that differ on signed and unsigned ints
Specification of operations that coincide on signed and unsigned ints
Behaviour when there is no under or overflow
Relationship with of_Z
Comparison
Absolute value
ASR
Lemma asr_0 (
i :
int) : (0
>> i)%
sint63 = 0%
sint63.
Lemma asr_0_r (
i :
int) : (
i >> 0)%
sint63 = i.
Lemma asr_neg_r (
i n :
int) :
to_Z n < 0
-> (
i >> n)%
sint63 = 0%
sint63.
Lemma asr_1 (
n :
int) : (1
>> n)%
sint63 = (
n =? 0)%
sint63.
Notation asr :=
asr (
only parsing).
Notation div :=
divs (
only parsing).
Notation rem :=
mods (
only parsing).
Notation ltb :=
ltsb (
only parsing).
Notation leb :=
lesb (
only parsing).
Notation compare :=
compares (
only parsing).
Module Export Sint63Notations.
Export Sint63NotationsInternalA.
Export Sint63NotationsInternalB.
End Sint63Notations.