Merge PR #11948: Hexadecimal numerals

Reviewed-by: JasonGross
Ack-by: Zimmi48
Ack-by: herbelin

6 files changed, 363 insertions, 7 deletions

diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index b094f81dc6..cba90043d5 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -159,6 +159,9 @@ Inductive nat : Set :=
   | O : nat
   | S : nat -> nat.
 
+Declare Scope hex_nat_scope.
+Delimit Scope hex_nat_scope with xnat.
+
 Declare Scope nat_scope.
 Delimit Scope nat_scope with nat.
 Bind Scope nat_scope with nat.
diff --git a/theories/Init/Decimal.v b/theories/Init/Decimal.v
index 2a84456500..5eae5567d7 100644
--- a/theories/Init/Decimal.v
+++ b/theories/Init/Decimal.v
@@ -16,7 +16,7 @@
     We represent numbers in base 10 as lists of decimal digits,
     in big-endian order (most significant digit comes first). *)
 
-Require Import Datatypes.
+Require Import Datatypes Specif.
 
 (** Unsigned integers are just lists of digits.
     For instance, ten is (D1 (D0 Nil)) *)
@@ -53,6 +53,10 @@ Variant decimal :=
  | Decimal (i:int) (f:uint)
  | DecimalExp (i:int) (f:uint) (e:int).
 
+Scheme Equality for uint.
+Scheme Equality for int.
+Scheme Equality for decimal.
+
 Declare Scope dec_uint_scope.
 Delimit Scope dec_uint_scope with uint.
 Bind Scope dec_uint_scope with uint.
@@ -172,8 +176,8 @@ Fixpoint del_head n d :=
 
 Definition del_head_int n d :=
   match d with
-  | Pos d => Pos (del_head n d)
-  | Neg d => Neg (del_head n d)
+  | Pos d => del_head n d
+  | Neg d => del_head n d
   end.
 
 (** [del_tail n d] removes [n] digits at end of [d]
diff --git a/theories/Init/Hexadecimal.v b/theories/Init/Hexadecimal.v
new file mode 100644
index 0000000000..a4ddad2875
--- /dev/null
+++ b/theories/Init/Hexadecimal.v
@@ -0,0 +1,245 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(** * 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 [Numeral Notation] command.
+    We represent numbers in base 16 as lists of hexadecimal digits,
+    in big-endian order (most significant digit comes first). *)
+
+Require Import Datatypes Specif Decimal.
+
+(** Unsigned integers are just lists of digits.
+    For instance, sixteen is (D1 (D0 Nil)) *)
+
+Inductive uint :=
+ | Nil
+ | D0 (_:uint)
+ | D1 (_:uint)
+ | D2 (_:uint)
+ | D3 (_:uint)
+ | D4 (_:uint)
+ | D5 (_:uint)
+ | D6 (_:uint)
+ | D7 (_:uint)
+ | D8 (_:uint)
+ | D9 (_:uint)
+ | Da (_:uint)
+ | Db (_:uint)
+ | Dc (_:uint)
+ | Dd (_:uint)
+ | De (_:uint)
+ | Df (_:uint).
+
+(** [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]. *)
+
+Notation zero := (D0 Nil).
+
+(** For signed integers, we use two constructors [Pos] and [Neg]. *)
+
+Variant int := Pos (d:uint) | Neg (d:uint).
+
+(** 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 *)
+
+Fixpoint nzhead d :=
+  match d with
+  | D0 d => nzhead d
+  | _ => d
+  end.
+
+(** [unorm] : normalization of unsigned integers *)
+
+Definition unorm d :=
+  match nzhead d with
+  | Nil => zero
+  | d => d
+  end.
+
+(** [norm] : normalization of signed integers *)
+
+Definition norm d :=
+  match d with
+  | Pos d => Pos (unorm d)
+  | Neg d =>
+    match nzhead d with
+    | Nil => Pos zero
+    | d => Neg d
+    end
+  end.
+
+(** A few easy operations. For more advanced computations, use the conversions
+    with other Coq numeral datatypes (e.g. Z) and the operations on them. *)
+
+Definition opp (d:int) :=
+  match d with
+  | Pos d => Neg d
+  | Neg d => Pos d
+  end.
+
+(** For conversions with binary numbers, it is easier to operate
+    on little-endian numbers. *)
+
+Fixpoint revapp (d d' : uint) :=
+  match d with
+  | Nil => d'
+  | D0 d => revapp d (D0 d')
+  | D1 d => revapp d (D1 d')
+  | D2 d => revapp d (D2 d')
+  | D3 d => revapp d (D3 d')
+  | D4 d => revapp d (D4 d')
+  | D5 d => revapp d (D5 d')
+  | D6 d => revapp d (D6 d')
+  | D7 d => revapp d (D7 d')
+  | D8 d => revapp d (D8 d')
+  | D9 d => revapp d (D9 d')
+  | Da d => revapp d (Da d')
+  | Db d => revapp d (Db d')
+  | Dc d => revapp d (Dc d')
+  | Dd d => revapp d (Dd d')
+  | De d => revapp d (De d')
+  | Df d => revapp d (Df d')
+  end.
+
+Definition rev d := revapp d Nil.
+
+Definition app d d' := revapp (rev d) d'.
+
+Definition app_int d1 d2 :=
+  match d1 with Pos d1 => Pos (app d1 d2) | Neg d1 => Neg (app d1 d2) end.
+
+(** [nztail] removes all trailing zero digits and return both the
+    result and the number of removed digits. *)
+
+Definition nztail d :=
+  let fix aux d_rev :=
+    match d_rev with
+    | D0 d_rev => let (r, n) := aux d_rev in pair r (S n)
+    | _ => pair d_rev O
+    end in
+  let (r, n) := aux (rev d) in pair (rev r) n.
+
+Definition nztail_int d :=
+  match d with
+  | Pos d => let (r, n) := nztail d in pair (Pos r) n
+  | Neg d => let (r, n) := nztail d in pair (Neg r) n
+  end.
+
+Module Little.
+
+(** Successor of little-endian numbers *)
+
+Fixpoint succ d :=
+  match d with
+  | Nil => D1 Nil
+  | D0 d => D1 d
+  | D1 d => D2 d
+  | D2 d => D3 d
+  | D3 d => D4 d
+  | D4 d => D5 d
+  | D5 d => D6 d
+  | D6 d => D7 d
+  | D7 d => D8 d
+  | D8 d => D9 d
+  | D9 d => Da d
+  | Da d => Db d
+  | Db d => Dc d
+  | Dc d => Dd d
+  | Dd d => De d
+  | De d => Df d
+  | Df d => D0 (succ d)
+  end.
+
+(** Doubling little-endian numbers *)
+
+Fixpoint double d :=
+  match d with
+  | Nil => Nil
+  | D0 d => D0 (double d)
+  | D1 d => D2 (double d)
+  | D2 d => D4 (double d)
+  | D3 d => D6 (double d)
+  | D4 d => D8 (double d)
+  | D5 d => Da (double d)
+  | D6 d => Dc (double d)
+  | D7 d => De (double d)
+  | D8 d => D0 (succ_double d)
+  | D9 d => D2 (succ_double d)
+  | Da d => D4 (succ_double d)
+  | Db d => D6 (succ_double d)
+  | Dc d => D8 (succ_double d)
+  | Dd d => Da (succ_double d)
+  | De d => Dc (succ_double d)
+  | Df d => De (succ_double d)
+  end
+
+with succ_double d :=
+  match d with
+  | Nil => D1 Nil
+  | D0 d => D1 (double d)
+  | D1 d => D3 (double d)
+  | D2 d => D5 (double d)
+  | D3 d => D7 (double d)
+  | D4 d => D9 (double d)
+  | D5 d => Db (double d)
+  | D6 d => Dd (double d)
+  | D7 d => Df (double d)
+  | D8 d => D1 (succ_double d)
+  | D9 d => D3 (succ_double d)
+  | Da d => D5 (succ_double d)
+  | Db d => D7 (succ_double d)
+  | Dc d => D9 (succ_double d)
+  | Dd d => Db (succ_double d)
+  | De d => Dd (succ_double d)
+  | Df d => Df (succ_double d)
+  end.
+
+End Little.
diff --git a/theories/Init/Nat.v b/theories/Init/Nat.v
index bfd41c5017..7c8cf0b536 100644
--- a/theories/Init/Nat.v
+++ b/theories/Init/Nat.v
@@ -9,7 +9,7 @@
 (************************************************************************)
 
 Require Import Notations Logic Datatypes.
-Require Decimal.
+Require Decimal Hexadecimal Numeral.
 Local Open Scope nat_scope.
 
 (**********************************************************************)
@@ -187,6 +187,37 @@ Fixpoint of_uint_acc (d:Decimal.uint)(acc:nat) :=
 
 Definition of_uint (d:Decimal.uint) := of_uint_acc d O.
 
+Local Notation sixteen := (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))).
+
+Fixpoint of_hex_uint_acc (d:Hexadecimal.uint)(acc:nat) :=
+  match d with
+  | Hexadecimal.Nil => acc
+  | Hexadecimal.D0 d => of_hex_uint_acc d (tail_mul sixteen acc)
+  | Hexadecimal.D1 d => of_hex_uint_acc d (S (tail_mul sixteen acc))
+  | Hexadecimal.D2 d => of_hex_uint_acc d (S (S (tail_mul sixteen acc)))
+  | Hexadecimal.D3 d => of_hex_uint_acc d (S (S (S (tail_mul sixteen acc))))
+  | Hexadecimal.D4 d => of_hex_uint_acc d (S (S (S (S (tail_mul sixteen acc)))))
+  | Hexadecimal.D5 d => of_hex_uint_acc d (S (S (S (S (S (tail_mul sixteen acc))))))
+  | Hexadecimal.D6 d => of_hex_uint_acc d (S (S (S (S (S (S (tail_mul sixteen acc)))))))
+  | Hexadecimal.D7 d => of_hex_uint_acc d (S (S (S (S (S (S (S (tail_mul sixteen acc))))))))
+  | Hexadecimal.D8 d => of_hex_uint_acc d (S (S (S (S (S (S (S (S (tail_mul sixteen acc)))))))))
+  | Hexadecimal.D9 d => of_hex_uint_acc d (S (S (S (S (S (S (S (S (S (tail_mul sixteen acc))))))))))
+  | Hexadecimal.Da d => of_hex_uint_acc d (S (S (S (S (S (S (S (S (S (S (tail_mul sixteen acc)))))))))))
+  | Hexadecimal.Db d => of_hex_uint_acc d (S (S (S (S (S (S (S (S (S (S (S (tail_mul sixteen acc))))))))))))
+  | Hexadecimal.Dc d => of_hex_uint_acc d (S (S (S (S (S (S (S (S (S (S (S (S (tail_mul sixteen acc)))))))))))))
+  | Hexadecimal.Dd d => of_hex_uint_acc d (S (S (S (S (S (S (S (S (S (S (S (S (S (tail_mul sixteen acc))))))))))))))
+  | Hexadecimal.De d => of_hex_uint_acc d (S (S (S (S (S (S (S (S (S (S (S (S (S (S (tail_mul sixteen acc)))))))))))))))
+  | Hexadecimal.Df d => of_hex_uint_acc d (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (tail_mul sixteen acc))))))))))))))))
+  end.
+
+Definition of_hex_uint (d:Hexadecimal.uint) := of_hex_uint_acc d O.
+
+Definition of_num_uint (d:Numeral.uint) :=
+  match d with
+  | Numeral.UIntDec d => of_uint d
+  | Numeral.UIntHex d => of_hex_uint d
+  end.
+
 Fixpoint to_little_uint n acc :=
   match n with
   | O => acc
@@ -196,14 +227,43 @@ Fixpoint to_little_uint n acc :=
 Definition to_uint n :=
   Decimal.rev (to_little_uint n Decimal.zero).
 
+Fixpoint to_little_hex_uint n acc :=
+  match n with
+  | O => acc
+  | S n => to_little_hex_uint n (Hexadecimal.Little.succ acc)
+  end.
+
+Definition to_hex_uint n :=
+  Hexadecimal.rev (to_little_hex_uint n Hexadecimal.zero).
+
+Definition to_num_uint n := Numeral.UIntDec (to_uint n).
+
+Definition to_num_hex_uint n := Numeral.UIntHex (to_hex_uint n).
+
 Definition of_int (d:Decimal.int) : option nat :=
   match Decimal.norm d with
     | Decimal.Pos u => Some (of_uint u)
     | _ => None
   end.
 
+Definition of_hex_int (d:Hexadecimal.int) : option nat :=
+  match Hexadecimal.norm d with
+    | Hexadecimal.Pos u => Some (of_hex_uint u)
+    | _ => None
+  end.
+
+Definition of_num_int (d:Numeral.int) : option nat :=
+  match d with
+  | Numeral.IntDec d => of_int d
+  | Numeral.IntHex d => of_hex_int d
+  end.
+
 Definition to_int n := Decimal.Pos (to_uint n).
 
+Definition to_hex_int n := Hexadecimal.Pos (to_hex_uint n).
+
+Definition to_num_int n := Numeral.IntDec (to_int n).
+
 (** ** Euclidean division *)
 
 (** This division is linear and tail-recursive.
diff --git a/theories/Init/Numeral.v b/theories/Init/Numeral.v
new file mode 100644
index 0000000000..8a0531e004
--- /dev/null
+++ b/theories/Init/Numeral.v
@@ -0,0 +1,33 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(** * Decimal or Hexadecimal numbers *)
+
+Require Import Decimal Hexadecimal.
+
+Variant uint := UIntDec (u:Decimal.uint) | UIntHex (u:Hexadecimal.uint).
+
+Variant int := IntDec (i:Decimal.int) | IntHex (i:Hexadecimal.int).
+
+Variant numeral := Dec (d:Decimal.decimal) | Hex (h:Hexadecimal.hexadecimal).
+
+Scheme Equality for uint.
+Scheme Equality for int.
+Scheme Equality for numeral.
+
+Register uint as num.num_uint.type.
+Register int as num.num_int.type.
+Register numeral as num.numeral.type.
+
+(** Pseudo-conversion functions used when declaring
+    Numeral Notations on [uint] and [int]. *)
+
+Definition uint_of_uint (i:uint) := i.
+Definition int_of_int (i:int) := i.
diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v
index 6a81517d7e..8f862e8cec 100644
--- a/theories/Init/Prelude.v
+++ b/theories/Init/Prelude.v
@@ -15,6 +15,8 @@ Require Export Datatypes.
 Require Export Specif.
 Require Coq.Init.Byte.
 Require Coq.Init.Decimal.
+Require Coq.Init.Hexadecimal.
+Require Coq.Init.Numeral.
 Require Coq.Init.Nat.
 Require Export Peano.
 Require Export Coq.Init.Wf.
@@ -30,16 +32,25 @@ Declare ML Module "ground_plugin".
 Declare ML Module "numeral_notation_plugin".
 Declare ML Module "string_notation_plugin".
 
+(* Parsing / printing of hexadecimal numbers *)
+Arguments Nat.of_hex_uint d%hex_uint_scope.
+Arguments Nat.of_hex_int d%hex_int_scope.
+Numeral Notation Numeral.uint Numeral.uint_of_uint Numeral.uint_of_uint
+  : hex_uint_scope.
+Numeral Notation Numeral.int Numeral.int_of_int Numeral.int_of_int
+  : hex_int_scope.
+
 (* Parsing / printing of decimal numbers *)
 Arguments Nat.of_uint d%dec_uint_scope.
 Arguments Nat.of_int d%dec_int_scope.
-Numeral Notation Decimal.uint Decimal.uint_of_uint Decimal.uint_of_uint
+Numeral Notation Numeral.uint Numeral.uint_of_uint Numeral.uint_of_uint
   : dec_uint_scope.
-Numeral Notation Decimal.int Decimal.int_of_int Decimal.int_of_int
+Numeral Notation Numeral.int Numeral.int_of_int Numeral.int_of_int
   : dec_int_scope.
 
 (* Parsing / printing of [nat] numbers *)
-Numeral Notation nat Nat.of_uint Nat.to_uint : nat_scope (abstract after 5001).
+Numeral Notation nat Nat.of_num_uint Nat.to_num_hex_uint : hex_nat_scope (abstract after 5001).
+Numeral Notation nat Nat.of_num_uint Nat.to_num_uint : nat_scope (abstract after 5001).
 
 (* Printing/Parsing of bytes *)
 Export Byte.ByteSyntaxNotations.