From 53720903b96f9616f8bd53318575e8bcc13c6fce Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Sat, 4 Apr 2020 22:36:02 +0200
Subject: Decimal: specify numeral notation for Q
---
doc/stdlib/index-list.html.template | 1 +
1 file changed, 1 insertion(+)
(limited to 'doc')
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 4a62888552..340e855a05 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -235,6 +235,7 @@ through the Require Import command.
theories/Numbers/DecimalPos.v
theories/Numbers/DecimalN.v
theories/Numbers/DecimalZ.v
+ theories/Numbers/DecimalQ.v
theories/Numbers/DecimalString.v
--
cgit v1.2.3
From 0ee6e30022e5b5b244f5d9cd16acb6017817a6c0 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Sat, 28 Mar 2020 14:25:27 +0100
Subject: [doc] Add hexadecimal numerals
---
doc/changelog/03-notations/11948-hexadecimal.rst | 12 ++++++++
doc/sphinx/language/core/basic.rst | 19 +++++++++---
doc/sphinx/user-extensions/syntax-extensions.rst | 39 ++++++++++++++----------
doc/stdlib/index-list.html.template | 2 ++
4 files changed, 51 insertions(+), 21 deletions(-)
create mode 100644 doc/changelog/03-notations/11948-hexadecimal.rst
(limited to 'doc')
diff --git a/doc/changelog/03-notations/11948-hexadecimal.rst b/doc/changelog/03-notations/11948-hexadecimal.rst
new file mode 100644
index 0000000000..e4b76d238c
--- /dev/null
+++ b/doc/changelog/03-notations/11948-hexadecimal.rst
@@ -0,0 +1,12 @@
+- **Added:**
+ Numeral notations now parse hexadecimal constants such as ``0x2a``
+ or ``0xb.2ap-2``. Parsers added for :g:`nat`, :g:`positive`, :g:`Z`,
+ :g:`N`, :g:`Q`, :g:`R`, primitive integers and primitive floats
+ (`#11948 `_,
+ by Pierre Roux).
+- **Deprecated:**
+ Numeral Notation on ``Decimal.uint``, ``Decimal.int`` and
+ ``Decimal.decimal`` are replaced respectively by numeral notations
+ on ``Numeral.uint``, ``Numeral.int`` and ``Numeral.numeral``
+ (`#11948 `_,
+ by Pierre Roux).
diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst
index 9473cc5a15..50e68276d2 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 d72409e0d9..4d722b6615 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -1406,26 +1406,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
@@ -1449,7 +1455,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
@@ -1479,12 +1485,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.
@@ -1500,7 +1507,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
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 340e855a05..8db6b63273 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -21,6 +21,8 @@ through the Require Import command.
theories/Init/Byte.v
theories/Init/Nat.v
theories/Init/Decimal.v
+ theories/Init/Hexadecimal.v
+ theories/Init/Numeral.v
theories/Init/Peano.v
theories/Init/Specif.v
theories/Init/Tactics.v
--
cgit v1.2.3
From da4a78d9fe25b000005a968d17c2e17bb42b71f4 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Thu, 2 Apr 2020 15:42:32 +0200
Subject: Hexadecimal: proofs that conversions from/to nat,N,Z and Q are
bijections
---
doc/stdlib/index-list.html.template | 6 ++++++
1 file changed, 6 insertions(+)
(limited to 'doc')
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 8db6b63273..7896b59a8b 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -239,6 +239,12 @@ through the Require Import command.
theories/Numbers/DecimalZ.v
theories/Numbers/DecimalQ.v
theories/Numbers/DecimalString.v
+ theories/Numbers/HexadecimalFacts.v
+ theories/Numbers/HexadecimalNat.v
+ theories/Numbers/HexadecimalPos.v
+ theories/Numbers/HexadecimalN.v
+ theories/Numbers/HexadecimalZ.v
+ theories/Numbers/HexadecimalQ.v
NatInt:
--
cgit v1.2.3
From 2d6c26cfab4055ff2b25a311544bdf59363686a7 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Thu, 2 Apr 2020 15:42:59 +0200
Subject: Hexadecimal: conversion to/from Coq strings
---
doc/stdlib/index-list.html.template | 1 +
1 file changed, 1 insertion(+)
(limited to 'doc')
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 7896b59a8b..426f67eb53 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -245,6 +245,7 @@ through the Require Import command.
theories/Numbers/HexadecimalN.v
theories/Numbers/HexadecimalZ.v
theories/Numbers/HexadecimalQ.v
+ theories/Numbers/HexadecimalString.v
NatInt:
--
cgit v1.2.3