From 2d44c8246eccba7c1c452cbfbc6751cd222d0a6a Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Sat, 12 Sep 2020 09:10:26 +0200
Subject: Renaming Numeral.v into Number.v

---
 theories/Init/Nat.v     | 20 +++++++--------
 theories/Init/Number.v  | 33 ++++++++++++++++++++++++
 theories/Init/Numeral.v | 67 ++++++++++++++++++++++++++++++++-----------------
 theories/Init/Prelude.v |  9 ++++---
 4 files changed, 92 insertions(+), 37 deletions(-)
 create mode 100644 theories/Init/Number.v

(limited to 'theories/Init')

diff --git a/theories/Init/Nat.v b/theories/Init/Nat.v
index 7c8cf0b536..bc48311151 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.UIntDec d => of_uint d
+  | Number.UIntHex 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.UIntDec (to_uint n).
 
-Definition to_num_hex_uint n := Numeral.UIntHex (to_hex_uint n).
+Definition to_num_hex_uint n := Number.UIntHex (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.IntDec d => of_int d
+  | Number.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).
+Definition to_num_int n := Number.IntDec (to_int n).
 
 (** ** Euclidean division *)
 
diff --git a/theories/Init/Number.v b/theories/Init/Number.v
new file mode 100644
index 0000000000..228f84b179
--- /dev/null
+++ b/theories/Init/Number.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 number := Dec (d:Decimal.decimal) | Hex (h:Hexadecimal.hexadecimal).
+
+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..c87f17ee5a 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.UintDec instead.")]
+Notation UIntDec := UIntDec (only parsing).
+#[deprecated(since="8.13",note="Use Number.UintHex instead.")]
+Notation UIntHex := UIntHex (only parsing).
+
+#[deprecated(since="8.13",note="Use Number.int instead.")]
+Notation int := int (only parsing).
+#[deprecated(since="8.13",note="Use Number.IntDec instead.")]
+Notation IntDec := IntDec (only parsing).
+#[deprecated(since="8.13",note="Use Number.IntHex instead.")]
+Notation IntHex := IntHex (only parsing).
+
+#[deprecated(since="8.13",note="Use Number.numeral instead.")]
+Notation numeral := number (only parsing).
+#[deprecated(since="8.13",note="Use Number.Dec instead.")]
+Notation Dec := Dec (only parsing).
+#[deprecated(since="8.13",note="Use Number.Hex instead.")]
+Notation Hex := Hex (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..141864d257 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.
@@ -35,17 +36,17 @@ 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 *)
-- 
cgit v1.2.3


From 11a8997dd8fa83537607272692a3baf10dab342a Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Thu, 3 Sep 2020 13:12:00 +0200
Subject: [numeral notation] Adding the via ... using ... option

This enables numeral notations for non inductive types by
pre/postprocessing them to a given proxy inductive type.
For instance, this should enable the use of numeral notations for R.
---
 theories/Init/Prelude.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'theories/Init')

diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v
index 141864d257..0239778bac 100644
--- a/theories/Init/Prelude.v
+++ b/theories/Init/Prelude.v
@@ -50,8 +50,8 @@ 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.
-- 
cgit v1.2.3


From ec24b26be7795af27256d39431e1c4e3d42fe3b7 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Thu, 3 Sep 2020 13:16:00 +0200
Subject: [numeral notation] Q

Previously rationals were all parsed as a pair numerator, denominator.
This means 1.02 and 102e-2 were both parsed as 102 # 100 and could not
be tell apart when printing. So the printer had to choose between two
representations : without exponent or without decimal dot. The choice
was made heuristically toward a most compact representation.

Now, decimal dot is still parsed as a power of ten denominator but
exponents are parsed as a product or division by Z.pow_pos. For
instance, 1.02 is parsed as 102 # 100 whereas 102e-2 is parsed as
(102 # 1) / (Z.pow_pos 10 2 # 1).

1.02 and 102e-2 remain equal (proved by reflexivity) but 1.02e1
= (102 # 100) * (10 # 1) = 1020 # 100 and 10.2 = 102 # 10 no longer are.

A nice side effect is that exponents can no longer blow up during
parsing. Previously 1e1_000_000 literally produced a numerator with a
million digits, now it just yields (1 # 1) * (Z.pow_pos 10 1_000_000 # 1).
---
 theories/Init/Decimal.v     |  6 ++++++
 theories/Init/Hexadecimal.v | 38 ++++++++++++++++++++++++++++++++++++++
 2 files changed, 44 insertions(+)

(limited to 'theories/Init')

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 *)
-- 
cgit v1.2.3


From 3b766fd8859b692e3e93cf83bf87d393e32c572e Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Thu, 3 Sep 2020 13:26:00 +0200
Subject: Merge numeral and string notation plugins

---
 theories/Init/Byte.v    | 2 +-
 theories/Init/Prelude.v | 2 --
 2 files changed, 1 insertion(+), 3 deletions(-)

(limited to 'theories/Init')

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/Prelude.v b/theories/Init/Prelude.v
index 0239778bac..9f8a054b5c 100644
--- a/theories/Init/Prelude.v
+++ b/theories/Init/Prelude.v
@@ -30,8 +30,6 @@ 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.
-- 
cgit v1.2.3


From 36ac26532028bfc6f84e4dfc849b51f42a3d8286 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Wed, 28 Oct 2020 10:32:58 +0100
Subject: Rename Dec and HexDec to Decimal and Hexadecimal

As noted by Hugo Herbelin, Dec is rather used for "decidable".
---
 theories/Init/Nat.v     | 14 +++++++-------
 theories/Init/Number.v  | 22 +++++++++++++++++-----
 theories/Init/Numeral.v | 24 ++++++++++++------------
 3 files changed, 36 insertions(+), 24 deletions(-)

(limited to 'theories/Init')

diff --git a/theories/Init/Nat.v b/theories/Init/Nat.v
index bc48311151..9a3a3ec99b 100644
--- a/theories/Init/Nat.v
+++ b/theories/Init/Nat.v
@@ -214,8 +214,8 @@ Definition of_hex_uint (d:Hexadecimal.uint) := of_hex_uint_acc d O.
 
 Definition of_num_uint (d:Number.uint) :=
   match d with
-  | Number.UIntDec d => of_uint d
-  | Number.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 := Number.UIntDec (to_uint n).
+Definition to_num_uint n := Number.UIntDecimal (to_uint n).
 
-Definition to_num_hex_uint n := Number.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
@@ -254,15 +254,15 @@ Definition of_hex_int (d:Hexadecimal.int) : option nat :=
 
 Definition of_num_int (d:Number.int) : option nat :=
   match d with
-  | Number.IntDec d => of_int d
-  | Number.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 := Number.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
index 228f84b179..eb9cc856ac 100644
--- a/theories/Init/Number.v
+++ b/theories/Init/Number.v
@@ -12,11 +12,23 @@
 
 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 number := Dec (d:Decimal.decimal) | Hex (h:Hexadecimal.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.
diff --git a/theories/Init/Numeral.v b/theories/Init/Numeral.v
index c87f17ee5a..50fa312e7e 100644
--- a/theories/Init/Numeral.v
+++ b/theories/Init/Numeral.v
@@ -14,24 +14,24 @@ 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.UintDec instead.")]
-Notation UIntDec := UIntDec (only parsing).
-#[deprecated(since="8.13",note="Use Number.UintHex instead.")]
-Notation UIntHex := UIntHex (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.IntDec instead.")]
-Notation IntDec := IntDec (only parsing).
-#[deprecated(since="8.13",note="Use Number.IntHex instead.")]
-Notation IntHex := IntHex (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.Dec instead.")]
-Notation Dec := Dec (only parsing).
-#[deprecated(since="8.13",note="Use Number.Hex instead.")]
-Notation Hex := Hex (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).
-- 
cgit v1.2.3