Merge PR #11948: Hexadecimal numerals

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

2 files changed, 37 insertions, 21 deletions

diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst
index aa93b4d21f..250a0f0326 100644
--- a/doc/sphinx/language/core/basic.rst
+++ b/doc/sphinx/language/core/basic.rst
@@ -111,18 +111,27 @@ Identifiers
 
 Numerals
   Numerals are sequences of digits with an optional fractional part
-  and exponent, optionally preceded by a minus sign. :n:`@int` is an integer;
-  a numeral without fractional or exponent parts. :n:`@num` is a non-negative
+  and exponent, optionally preceded by a minus sign. Hexadecimal numerals
+  start with ``0x`` or ``0X``. :n:`@int` is an integer;
+  a numeral without fractional nor exponent parts. :n:`@num` is a non-negative
   integer.  Underscores embedded in the digits are ignored, for example
   ``1_000_000`` is the same as ``1000000``.
 
   .. insertprodn numeral digit
 
   .. prodn::
-     numeral ::= {+ @digit } {? . {+ @digit } } {? {| e | E } {? {| + | - } } {+ @digit } }
-     int ::= {? - } {+ @digit }
-     num ::= {+ @digit }
      digit ::= 0 .. 9
+     digitu ::= {| @digit | _ }
+     hexdigit ::= {| 0 .. 9 | a..f | A..F }
+     hexdigitu ::= {| @hexdigit | _ }
+     decnum ::= @digit {* @digitu }
+     hexnum ::= {| 0x | 0X } @hexdigit {* @hexdigitu }
+     num ::= {| @decnum | @hexnum }
+     sign ::= {| + | - }
+     int ::= {? - } @num
+     decimal ::= @decnum {? . {+ @digitu } } {? {| e | E } {? @sign } @decnum }
+     hexadecimal ::= @hexnum {? . {+ @hexdigitu } } {? {| p | P } {? @sign } @decnum }
+     numeral ::= {? - } {| @decimal | @hexadecimal }
 
 Strings
   Strings begin and end with ``"`` (double quote).  Use ``""`` to represent
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index c5ec636d5f..60cd4c4ad8 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -1452,26 +1452,32 @@ Numeral notations
          parsing and printing functions, respectively.  The parsing function
          :n:`@qualid__parse` should have one of the following types:
 
-            * :n:`Decimal.int -> @qualid`
-            * :n:`Decimal.int -> option @qualid`
-            * :n:`Decimal.uint -> @qualid`
-            * :n:`Decimal.uint -> option @qualid`
+            * :n:`Numeral.int -> @qualid`
+            * :n:`Numeral.int -> option @qualid`
+            * :n:`Numeral.uint -> @qualid`
+            * :n:`Numeral.uint -> option @qualid`
             * :n:`Z -> @qualid`
             * :n:`Z -> option @qualid`
-            * :n:`Decimal.decimal -> @qualid`
-            * :n:`Decimal.decimal -> option @qualid`
+            * :n:`Numeral.numeral -> @qualid`
+            * :n:`Numeral.numeral -> option @qualid`
 
          And the printing function :n:`@qualid__print` should have one of the
          following types:
 
-            * :n:`@qualid -> Decimal.int`
-            * :n:`@qualid -> option Decimal.int`
-            * :n:`@qualid -> Decimal.uint`
-            * :n:`@qualid -> option Decimal.uint`
+            * :n:`@qualid -> Numeral.int`
+            * :n:`@qualid -> option Numeral.int`
+            * :n:`@qualid -> Numeral.uint`
+            * :n:`@qualid -> option Numeral.uint`
             * :n:`@qualid -> Z`
             * :n:`@qualid -> option Z`
-            * :n:`@qualid -> Decimal.decimal`
-            * :n:`@qualid -> option Decimal.decimal`
+            * :n:`@qualid -> Numeral.numeral`
+            * :n:`@qualid -> option Numeral.numeral`
+
+         .. deprecated:: 8.12
+            Numeral notations on :g:`Decimal.uint`, :g:`Decimal.int` and
+            :g:`Decimal.decimal` are replaced respectively by numeral
+            notations on :g:`Numeral.uint`, :g:`Numeral.int` and
+            :g:`Numeral.numeral`.
 
          When parsing, the application of the parsing function
          :n:`@qualid__parse` to the number will be fully reduced, and universes
@@ -1495,7 +1501,7 @@ Numeral notations
          returns :n:`(@qualid__parse m)` when parsing a literal
          :n:`m` that's greater than :n:`@numeral` rather than reducing it to a normal form.
          Here :g:`m` will be a
-         :g:`Decimal.int` or :g:`Decimal.uint` or :g:`Z`, depending on the
+         :g:`Numeral.int` or :g:`Numeral.uint` or :g:`Z`, depending on the
          type of the parsing function :n:`@qualid__parse`. This allows for a
          more compact representation of literals in types such as :g:`nat`,
          and limits parse failures due to stack overflow.  Note that a
@@ -1525,12 +1531,13 @@ Numeral notations
      only for integers or non-negative integers, and the given numeral
      has a fractional or exponent part or is negative.
 
-   .. exn:: @qualid__parse should go from Decimal.int to @type or (option @type). Instead of Decimal.int, the types Decimal.uint or Z or Int63.int or Decimal.decimal could be used (you may need to require BinNums or Decimal or Int63 first).
+
+   .. exn:: @qualid__parse should go from Numeral.int to @type or (option @type). Instead of Numeral.int, the types Numeral.uint or Z or Int63.int or Numeral.numeral could be used (you may need to require BinNums or Numeral or Int63 first).
 
      The parsing function given to the :cmd:`Numeral Notation`
      vernacular is not of the right type.
 
-   .. exn:: @qualid__print should go from @type to Decimal.int or (option Decimal.int).  Instead of Decimal.int, the types Decimal.uint or Z or Int63.int or Decimal.decimal could be used (you may need to require BinNums or Decimal or Int63 first).
+   .. exn:: @qualid__print should go from @type to Numeral.int or (option Numeral.int).  Instead of Numeral.int, the types Numeral.uint or Z or Int63.int or Numeral.numeral could be used (you may need to require BinNums or Numeral or Int63 first).
 
      The printing function given to the :cmd:`Numeral Notation`
      vernacular is not of the right type.
@@ -1546,7 +1553,7 @@ Numeral notations
 
      Parsing functions expected to return an :g:`option` must always
      return a concrete :g:`Some` or :g:`None` when applied to a
-     concrete numeral expressed as a decimal.  They may not return
+     concrete numeral expressed as a (hexa)decimal.  They may not return
      opaque constants.
 
 String notations