Merge PR #12218: Numeral notations for non inductive types

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

7 files changed, 151 insertions, 42 deletions

diff --git a/theories/Init/Byte.v b/theories/Init/Byte.v
index 7449b52d76..e03820ef22 100644
--- a/theories/Init/Byte.v
+++ b/theories/Init/Byte.v
@@ -16,7 +16,7 @@ Require Import Coq.Init.Logic.
 Require Import Coq.Init.Specif.
 Require Coq.Init.Nat.
 
-Declare ML Module "string_notation_plugin".
+Declare ML Module "number_string_notation_plugin".
 
 (** We define an inductive for use with the [String Notation] command
     which contains all ascii characters.  We use 256 constructors for
diff --git a/theories/Init/Decimal.v b/theories/Init/Decimal.v
index 025264ab01..bb12f9ca3e 100644
--- a/theories/Init/Decimal.v
+++ b/theories/Init/Decimal.v
@@ -118,6 +118,12 @@ Definition opp (d:int) :=
   | Neg d => Pos d
   end.
 
+Definition abs (d:int) : uint :=
+  match d with
+  | Pos d => d
+  | Neg d => d
+  end.
+
 (** For conversions with binary numbers, it is easier to operate
     on little-endian numbers. *)
 
diff --git a/theories/Init/Hexadecimal.v b/theories/Init/Hexadecimal.v
index 36f5e5ad1f..7467aa1262 100644
--- a/theories/Init/Hexadecimal.v
+++ b/theories/Init/Hexadecimal.v
@@ -125,6 +125,12 @@ Definition opp (d:int) :=
   | Neg d => Pos d
   end.
 
+Definition abs (d:int) : uint :=
+  match d with
+  | Pos d => d
+  | Neg d => d
+  end.
+
 (** For conversions with binary numbers, it is easier to operate
     on little-endian numbers. *)
 
@@ -173,6 +179,38 @@ Definition nztail_int d :=
   | Neg d => let (r, n) := nztail d in pair (Neg r) n
   end.
 
+(** [del_head n d] removes [n] digits at beginning of [d]
+    or returns [zero] if [d] has less than [n] digits. *)
+
+Fixpoint del_head n d :=
+  match n with
+  | O => d
+  | S n =>
+    match d with
+    | Nil => zero
+    | 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 =>
+      del_head n d
+    end
+  end.
+
+Definition del_head_int n d :=
+  match d with
+  | Pos d => del_head n d
+  | Neg d => del_head n d
+  end.
+
+(** [del_tail n d] removes [n] digits at end of [d]
+    or returns [zero] if [d] has less than [n] digits. *)
+
+Definition del_tail n d := rev (del_head n (rev d)).
+
+Definition del_tail_int n d :=
+  match d with
+  | Pos d => Pos (del_tail n d)
+  | Neg d => Neg (del_tail n d)
+  end.
+
 Module Little.
 
 (** Successor of little-endian numbers *)
diff --git a/theories/Init/Nat.v b/theories/Init/Nat.v
index 7c8cf0b536..9a3a3ec99b 100644
--- a/theories/Init/Nat.v
+++ b/theories/Init/Nat.v
@@ -9,7 +9,7 @@
 (************************************************************************)
 
 Require Import Notations Logic Datatypes.
-Require Decimal Hexadecimal Numeral.
+Require Decimal Hexadecimal Number.
 Local Open Scope nat_scope.
 
 (**********************************************************************)
@@ -212,10 +212,10 @@ Fixpoint of_hex_uint_acc (d:Hexadecimal.uint)(acc:nat) :=
 
 Definition of_hex_uint (d:Hexadecimal.uint) := of_hex_uint_acc d O.
 
-Definition of_num_uint (d:Numeral.uint) :=
+Definition of_num_uint (d:Number.uint) :=
   match d with
-  | Numeral.UIntDec d => of_uint d
-  | Numeral.UIntHex d => of_hex_uint d
+  | Number.UIntDecimal d => of_uint d
+  | Number.UIntHexadecimal d => of_hex_uint d
   end.
 
 Fixpoint to_little_uint n acc :=
@@ -236,9 +236,9 @@ Fixpoint to_little_hex_uint n acc :=
 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_uint n := Number.UIntDecimal (to_uint n).
 
-Definition to_num_hex_uint n := Numeral.UIntHex (to_hex_uint n).
+Definition to_num_hex_uint n := Number.UIntHexadecimal (to_hex_uint n).
 
 Definition of_int (d:Decimal.int) : option nat :=
   match Decimal.norm d with
@@ -252,17 +252,17 @@ Definition of_hex_int (d:Hexadecimal.int) : option nat :=
     | _ => None
   end.
 
-Definition of_num_int (d:Numeral.int) : option nat :=
+Definition of_num_int (d:Number.int) : option nat :=
   match d with
-  | Numeral.IntDec d => of_int d
-  | Numeral.IntHex d => of_hex_int d
+  | Number.IntDecimal d => of_int d
+  | Number.IntHexadecimal 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).
+Definition to_num_int n := Number.IntDecimal (to_int n).
 
 (** ** Euclidean division *)
 
diff --git a/theories/Init/Number.v b/theories/Init/Number.v
new file mode 100644
index 0000000000..eb9cc856ac
--- /dev/null
+++ b/theories/Init/Number.v
@@ -0,0 +1,45 @@
+(************************************************************************)
+(*         *   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 := UIntDecimal (u:Decimal.uint) | UIntHexadecimal (u:Hexadecimal.uint).
+#[deprecated(since="8.13",note="Use UintDecimal instead.")]
+Notation UIntDec := UIntDecimal (only parsing).
+#[deprecated(since="8.13",note="Use UintHexadecimal instead.")]
+Notation UIntHex := UIntHexadecimal (only parsing).
+
+Variant int := IntDecimal (i:Decimal.int) | IntHexadecimal (i:Hexadecimal.int).
+#[deprecated(since="8.13",note="Use IntDecimal instead.")]
+Notation IntDec := IntDecimal (only parsing).
+#[deprecated(since="8.13",note="Use IntHexadecimal instead.")]
+Notation IntHex := IntHexadecimal (only parsing).
+
+Variant number := Decimal (d:Decimal.decimal) | Hexadecimal (h:Hexadecimal.hexadecimal).
+#[deprecated(since="8.13",note="Use Decimal instead.")]
+Notation Dec := Decimal (only parsing).
+#[deprecated(since="8.13",note="Use Hexadecimal instead.")]
+Notation Hex := Hexadecimal (only parsing).
+
+Scheme Equality for uint.
+Scheme Equality for int.
+Scheme Equality for number.
+
+Register uint as num.num_uint.type.
+Register int as num.num_int.type.
+Register number as num.number.type.
+
+(** Pseudo-conversion functions used when declaring
+    Number Notations on [uint] and [int]. *)
+
+Definition uint_of_uint (i:uint) := i.
+Definition int_of_int (i:int) := i.
diff --git a/theories/Init/Numeral.v b/theories/Init/Numeral.v
index 179547d0b3..50fa312e7e 100644
--- a/theories/Init/Numeral.v
+++ b/theories/Init/Numeral.v
@@ -8,26 +8,47 @@
 (*         *     (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
-    Number Notations on [uint] and [int]. *)
-
-Definition uint_of_uint (i:uint) := i.
-Definition int_of_int (i:int) := i.
+(** * Deprecated: use Number.v instead *)
+
+Require Import Decimal Hexadecimal Number.
+
+#[deprecated(since="8.13",note="Use Number.uint instead.")]
+Notation uint := uint (only parsing).
+#[deprecated(since="8.13",note="Use Number.UintDecimal instead.")]
+Notation UIntDec := UIntDecimal (only parsing).
+#[deprecated(since="8.13",note="Use Number.UintHexadecimal instead.")]
+Notation UIntHex := UIntHexadecimal (only parsing).
+
+#[deprecated(since="8.13",note="Use Number.int instead.")]
+Notation int := int (only parsing).
+#[deprecated(since="8.13",note="Use Number.IntDecimal instead.")]
+Notation IntDec := IntDecimal (only parsing).
+#[deprecated(since="8.13",note="Use Number.IntHexadecimal instead.")]
+Notation IntHex := IntHexadecimal (only parsing).
+
+#[deprecated(since="8.13",note="Use Number.numeral instead.")]
+Notation numeral := number (only parsing).
+#[deprecated(since="8.13",note="Use Number.Decimal instead.")]
+Notation Dec := Decimal (only parsing).
+#[deprecated(since="8.13",note="Use Number.Hexadecimal instead.")]
+Notation Hex := Hexadecimal (only parsing).
+
+#[deprecated(since="8.13",note="Use Number.uint_beq instead.")]
+Notation uint_beq := uint_beq (only parsing).
+#[deprecated(since="8.13",note="Use Number.uint_eq_dec instead.")]
+Notation uint_eq_dec := uint_eq_dec (only parsing).
+#[deprecated(since="8.13",note="Use Number.int_beq instead.")]
+Notation int_beq := int_beq (only parsing).
+#[deprecated(since="8.13",note="Use Number.int_eq_dec instead.")]
+Notation int_eq_dec := int_eq_dec (only parsing).
+#[deprecated(since="8.13",note="Use Number.numeral_beq instead.")]
+Notation numeral_beq := number_beq (only parsing).
+#[deprecated(since="8.13",note="Use Number.numeral_eq_dec instead.")]
+Notation numeral_eq_dec := number_eq_dec (only parsing).
+
+Register number as num.numeral.type.
+
+#[deprecated(since="8.13",note="Use Number.uint_of_uint instead.")]
+Notation uint_of_uint := uint_of_uint (only parsing).
+#[deprecated(since="8.13",note="Use Number.int_of_int instead.")]
+Notation int_of_int := int_of_int (only parsing).
diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v
index 0fe3d5491e..9f8a054b5c 100644
--- a/theories/Init/Prelude.v
+++ b/theories/Init/Prelude.v
@@ -17,6 +17,7 @@ Require Coq.Init.Byte.
 Require Coq.Init.Decimal.
 Require Coq.Init.Hexadecimal.
 Require Coq.Init.Numeral.
+Require Coq.Init.Number.
 Require Coq.Init.Nat.
 Require Export Peano.
 Require Export Coq.Init.Wf.
@@ -29,28 +30,26 @@ Require Export Coq.Init.Tauto.
 *)
 Declare ML Module "cc_plugin".
 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.
-Number Notation Numeral.uint Numeral.uint_of_uint Numeral.uint_of_uint
+Number Notation Number.uint Number.uint_of_uint Number.uint_of_uint
   : hex_uint_scope.
-Number Notation Numeral.int Numeral.int_of_int Numeral.int_of_int
+Number Notation Number.int Number.int_of_int Number.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.
-Number Notation Numeral.uint Numeral.uint_of_uint Numeral.uint_of_uint
+Number Notation Number.uint Number.uint_of_uint Number.uint_of_uint
   : dec_uint_scope.
-Number Notation Numeral.int Numeral.int_of_int Numeral.int_of_int
+Number Notation Number.int Number.int_of_int Number.int_of_int
   : dec_int_scope.
 
 (* Parsing / printing of [nat] numbers *)
-Number Notation nat Nat.of_num_uint Nat.to_num_hex_uint : hex_nat_scope (abstract after 5001).
-Number Notation nat Nat.of_num_uint Nat.to_num_uint : nat_scope (abstract after 5001).
+Number Notation nat Nat.of_num_uint Nat.to_num_hex_uint (abstract after 5001) : hex_nat_scope.
+Number Notation nat Nat.of_num_uint Nat.to_num_uint (abstract after 5001) : nat_scope.
 
 (* Printing/Parsing of bytes *)
 Export Byte.ByteSyntaxNotations.