Library Coq.Init.Hexadecimal
Hexadecimal numbers
These numbers coded in base 16 will be used for parsing and printing
other Coq numeral datatypes in an human-readable way.
See the
Number Notation command.
We represent numbers in base 16 as lists of hexadecimal digits,
in big-endian order (most significant digit comes first).
Unsigned integers are just lists of digits.
For instance, sixteen is (D1 (D0 Nil))
Nil is the number terminator. Taken alone, it behaves as zero,
but rather use D0 Nil instead, since this form will be denoted
as 0, while Nil will be printed as Nil.
For signed integers, we use two constructors Pos and Neg.
For decimal numbers, we use two constructors Hexadecimal and
HexadecimalExp, depending on whether or not they are given with an
exponent (e.g., 0x1.a2p+01). i is the integral part while f is
the fractional part (beware that leading zeroes do matter).
Variant hexadecimal :=
|
Hexadecimal (
i:
int) (
f:
uint)
|
HexadecimalExp (
i:
int) (
f:
uint) (
e:
Decimal.int).
Scheme Equality for uint.
Scheme Equality for int.
Scheme Equality for hexadecimal.
Declare Scope hex_uint_scope.
Delimit Scope hex_uint_scope with huint.
Bind Scope hex_uint_scope with uint.
Declare Scope hex_int_scope.
Delimit Scope hex_int_scope with hint.
Bind Scope hex_int_scope with int.
Register uint as num.hexadecimal_uint.type.
Register int as num.hexadecimal_int.type.
Register hexadecimal as num.hexadecimal.type.
Fixpoint nb_digits d :=
match d with
|
Nil =>
O
|
D0 d |
D1 d |
D2 d |
D3 d |
D4 d |
D5 d |
D6 d |
D7 d |
D8 d |
D9 d
|
Da d |
Db d |
Dc d |
Dd d |
De d |
Df d =>
S (
nb_digits d)
end.
This representation favors simplicity over canonicity.
For normalizing numbers, we need to remove head zero digits,
and choose our canonical representation of 0 (here
D0 Nil
for unsigned numbers and
Pos (D0 Nil) for signed numbers).
nzhead removes all head zero digits
unorm : normalization of unsigned integers
norm : normalization of signed integers
A few easy operations. For more advanced computations, use the conversions
with other Coq numeral datatypes (e.g. Z) and the operations on them.
For conversions with binary numbers, it is easier to operate
on little-endian numbers.
nztail removes all trailing zero digits and return both the
result and the number of removed digits.
del_head n d removes n digits at beginning of d
or returns zero if d has less than n digits.
del_tail n d removes n digits at end of d
or returns zero if d has less than n digits.
Successor of little-endian numbers
Doubling little-endian numbers