From e30e864d61431a0145853fcf90b5f16b781f4a46 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Wed, 7 Nov 2018 21:19:05 -0500
Subject: Add `String Notation` vernacular like `Numeral Notation`
Users can now register string notations for custom inductives.
Much of the code and documentation was copied from numeral notations.
I chose to use a 256-constructor inductive for primitive string syntax
because (a) it is easy to convert between character codes and
constructors, and (b) it is more efficient than the existing `ascii`
type.
Some choices about proofs of the new `byte` type were made based on
efficiency. For example, https://github.com/coq/coq/issues/8517 means
that we cannot simply use `Scheme Equality` for this type, and I have
taken some care to ensure that the proofs of decidable equality and
conversion are fast. (Unfortunately, the `Init/Byte.v` file is the
slowest one in the prelude (it takes a couple of seconds to build), and
I'm not sure where the slowness is.)
In String.v, some uses of `0` as a `nat` were replaced by `O`, because
the file initially refused to check interactively otherwise (it
complained that `0` could not be interpreted in `string_scope` before
loading `Coq.Strings.String`).
There is unfortunately a decent amount of code duplication between
numeral notations and string notations.
I have not put too much thought into chosing names; most names have been
chosen to be similar to numeral notations, though I chose the name
`byte` from
https://github.com/coq/coq/issues/8483#issuecomment-421671785.
Unfortunately, this feature does not support declaring string syntax for
`list ascii`, unless that type is wrapped in a record or other inductive
type. This is not a fundamental limitation; it should be relatively
easy for someone who knows the API of the reduction machinery in Coq to
extend both this and numeral notations to support any type whose hnf
starts with an inductive type. (The reason for needing an inductive
type to bottom out at is that this is how the plugin determines what
constructors are the entry points for printing the given notation.
However, see also https://github.com/coq/coq/issues/8964 for
complications that are more likely to arise if inductive type families
are supported.)
N.B. I generated the long lists of constructors for the `byte` type with
short python scripts.
Closes #8853
---
doc/sphinx/user-extensions/syntax-extensions.rst | 98 ++++++++++++++++++++++++
doc/stdlib/index-list.html.template | 2 +
2 files changed, 100 insertions(+)
(limited to 'doc')
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 65df89da6c..55508f04f2 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -1522,6 +1522,104 @@ Numeral notations
As noted above, the :n:`(abstract after @num)` directive has no
effect when :n:`@ident__2` lands in an :g:`option` type.
+String notations
+-----------------
+
+.. cmd:: String Notation @ident__1 @ident__2 @ident__3 : @scope.
+ :name: String Notation
+
+ This command allows the user to customize the way strings are parsed
+ and printed.
+
+ The token :n:`@ident__1` should be the name of an inductive type,
+ while :n:`@ident__2` and :n:`@ident__3` should be the names of the
+ parsing and printing functions, respectively. The parsing function
+ :n:`@ident__2` should have one of the following types:
+
+ * :n:`Byte.byte -> @ident__1`
+ * :n:`Byte.byte -> option @ident__1`
+ * :n:`list Byte.byte -> @ident__1`
+ * :n:`list Byte.byte -> option @ident__1`
+
+ And the printing function :n:`@ident__3` should have one of the
+ following types:
+
+ * :n:`@ident__1 -> Byte.byte`
+ * :n:`@ident__1 -> option Byte.byte`
+ * :n:`@ident__1 -> list Byte.byte`
+ * :n:`@ident__1 -> option (list Byte.byte)`
+
+ When parsing, the application of the parsing function
+ :n:`@ident__2` to the string will be fully reduced, and universes
+ of the resulting term will be refreshed.
+
+ .. exn:: Cannot interpret this string as a value of type @type
+
+ The string notation registered for :token:`type` does not support
+ the given string. This error is given when the interpretation
+ function returns :g:`None`.
+
+ .. exn:: @ident should go from Byte.byte or (list Byte.byte) to @type or (option @type).
+
+ The parsing function given to the :cmd:`String Notation`
+ vernacular is not of the right type.
+
+ .. exn:: @ident should go from @type to Byte.byte or (option Byte.byte) or (list Byte.byte) or (option (list Byte.byte)).
+
+ The printing function given to the :cmd:`String Notation`
+ vernacular is not of the right type.
+
+ .. exn:: @type is not an inductive type.
+
+ String notations can only be declared for inductive types with no
+ arguments.
+
+ .. exn:: Unexpected term @term while parsing a string notation.
+
+ Parsing functions must always return ground terms, made up of
+ applications of constructors and inductive types. Parsing
+ functions may not return terms containing axioms, bare
+ (co)fixpoints, lambdas, etc.
+
+ .. exn:: Unexpected non-option term @term while parsing a string notation.
+
+ Parsing functions expected to return an :g:`option` must always
+ return a concrete :g:`Some` or :g:`None` when applied to a
+ concrete string expressed as a decimal. They may not return
+ opaque constants.
+
+ .. exn:: Cannot interpret in @scope because @ident could not be found in the current environment.
+
+ The inductive type used to register the string notation is no
+ longer available in the environment. Most likely, this is because
+ the string notation was declared inside a functor for an
+ inductive type inside the functor. This use case is not currently
+ supported.
+
+ Alternatively, you might be trying to use a primitive token
+ notation from a plugin which forgot to specify which module you
+ must :g:`Require` for access to that notation.
+
+ .. exn:: Syntax error: [prim:reference] expected after 'Notation' (in [vernac:command]).
+
+ The type passed to :cmd:`String Notation` must be a single
+ identifier.
+
+ .. exn:: Syntax error: [prim:reference] expected after [prim:reference] (in [vernac:command]).
+
+ Both functions passed to :cmd:`String Notation` must be single
+ identifiers.
+
+ .. exn:: The reference @ident was not found in the current environment.
+
+ Identifiers passed to :cmd:`String Notation` must exist in the
+ global environment.
+
+ .. exn:: @ident is bound to a notation that does not denote a reference.
+
+ Identifiers passed to :cmd:`String Notation` must be global
+ references, or notations which denote to single identifiers.
+
.. _TacticNotation:
Tactic Notations
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 4fc9bf9e19..51f94d7e5a 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -17,6 +17,7 @@ through the Require Import command.
theories/Init/Datatypes.v
theories/Init/Logic.v
theories/Init/Logic_Type.v
+ theories/Init/Byte.v
theories/Init/Nat.v
theories/Init/Decimal.v
theories/Init/Peano.v
@@ -497,6 +498,7 @@ through the Require Import command.
Implementation of string as list of ascii characters
+ theories/Strings/Byte.v
theories/Strings/Ascii.v
theories/Strings/String.v
theories/Strings/BinaryString.v
--
cgit v1.2.3
From 5537151575195addd3e1e0003025384a85d957f7 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Wed, 28 Nov 2018 15:02:56 -0500
Subject: Fix string notation doc
As per https://github.com/coq/coq/pull/8965/files#r237225852
---
doc/sphinx/user-extensions/syntax-extensions.rst | 126 +++++++++++------------
1 file changed, 63 insertions(+), 63 deletions(-)
(limited to 'doc')
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 55508f04f2..c0e57aab53 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -1528,97 +1528,97 @@ String notations
.. cmd:: String Notation @ident__1 @ident__2 @ident__3 : @scope.
:name: String Notation
- This command allows the user to customize the way strings are parsed
- and printed.
+ This command allows the user to customize the way strings are parsed
+ and printed.
- The token :n:`@ident__1` should be the name of an inductive type,
- while :n:`@ident__2` and :n:`@ident__3` should be the names of the
- parsing and printing functions, respectively. The parsing function
- :n:`@ident__2` should have one of the following types:
+ The token :n:`@ident__1` should be the name of an inductive type,
+ while :n:`@ident__2` and :n:`@ident__3` should be the names of the
+ parsing and printing functions, respectively. The parsing function
+ :n:`@ident__2` should have one of the following types:
- * :n:`Byte.byte -> @ident__1`
- * :n:`Byte.byte -> option @ident__1`
- * :n:`list Byte.byte -> @ident__1`
- * :n:`list Byte.byte -> option @ident__1`
+ * :n:`Byte.byte -> @ident__1`
+ * :n:`Byte.byte -> option @ident__1`
+ * :n:`list Byte.byte -> @ident__1`
+ * :n:`list Byte.byte -> option @ident__1`
- And the printing function :n:`@ident__3` should have one of the
- following types:
+ And the printing function :n:`@ident__3` should have one of the
+ following types:
- * :n:`@ident__1 -> Byte.byte`
- * :n:`@ident__1 -> option Byte.byte`
- * :n:`@ident__1 -> list Byte.byte`
- * :n:`@ident__1 -> option (list Byte.byte)`
+ * :n:`@ident__1 -> Byte.byte`
+ * :n:`@ident__1 -> option Byte.byte`
+ * :n:`@ident__1 -> list Byte.byte`
+ * :n:`@ident__1 -> option (list Byte.byte)`
- When parsing, the application of the parsing function
- :n:`@ident__2` to the string will be fully reduced, and universes
- of the resulting term will be refreshed.
+ When parsing, the application of the parsing function
+ :n:`@ident__2` to the string will be fully reduced, and universes
+ of the resulting term will be refreshed.
- .. exn:: Cannot interpret this string as a value of type @type
+ .. exn:: Cannot interpret this string as a value of type @type
- The string notation registered for :token:`type` does not support
- the given string. This error is given when the interpretation
- function returns :g:`None`.
+ The string notation registered for :token:`type` does not support
+ the given string. This error is given when the interpretation
+ function returns :g:`None`.
- .. exn:: @ident should go from Byte.byte or (list Byte.byte) to @type or (option @type).
+ .. exn:: @ident should go from Byte.byte or (list Byte.byte) to @type or (option @type).
- The parsing function given to the :cmd:`String Notation`
- vernacular is not of the right type.
+ The parsing function given to the :cmd:`String Notation`
+ vernacular is not of the right type.
- .. exn:: @ident should go from @type to Byte.byte or (option Byte.byte) or (list Byte.byte) or (option (list Byte.byte)).
+ .. exn:: @ident should go from @type to Byte.byte or (option Byte.byte) or (list Byte.byte) or (option (list Byte.byte)).
- The printing function given to the :cmd:`String Notation`
- vernacular is not of the right type.
+ The printing function given to the :cmd:`String Notation`
+ vernacular is not of the right type.
- .. exn:: @type is not an inductive type.
+ .. exn:: @type is not an inductive type.
- String notations can only be declared for inductive types with no
- arguments.
+ String notations can only be declared for inductive types with no
+ arguments.
- .. exn:: Unexpected term @term while parsing a string notation.
+ .. exn:: Unexpected term @term while parsing a string notation.
- Parsing functions must always return ground terms, made up of
- applications of constructors and inductive types. Parsing
- functions may not return terms containing axioms, bare
- (co)fixpoints, lambdas, etc.
+ Parsing functions must always return ground terms, made up of
+ applications of constructors and inductive types. Parsing
+ functions may not return terms containing axioms, bare
+ (co)fixpoints, lambdas, etc.
- .. exn:: Unexpected non-option term @term while parsing a string notation.
+ .. exn:: Unexpected non-option term @term while parsing a string notation.
- Parsing functions expected to return an :g:`option` must always
- return a concrete :g:`Some` or :g:`None` when applied to a
- concrete string expressed as a decimal. They may not return
- opaque constants.
+ Parsing functions expected to return an :g:`option` must always
+ return a concrete :g:`Some` or :g:`None` when applied to a
+ concrete string expressed as a decimal. They may not return
+ opaque constants.
- .. exn:: Cannot interpret in @scope because @ident could not be found in the current environment.
+ .. exn:: Cannot interpret in @scope because @ident could not be found in the current environment.
- The inductive type used to register the string notation is no
- longer available in the environment. Most likely, this is because
- the string notation was declared inside a functor for an
- inductive type inside the functor. This use case is not currently
- supported.
+ The inductive type used to register the string notation is no
+ longer available in the environment. Most likely, this is because
+ the string notation was declared inside a functor for an
+ inductive type inside the functor. This use case is not currently
+ supported.
- Alternatively, you might be trying to use a primitive token
- notation from a plugin which forgot to specify which module you
- must :g:`Require` for access to that notation.
+ Alternatively, you might be trying to use a primitive token
+ notation from a plugin which forgot to specify which module you
+ must :g:`Require` for access to that notation.
- .. exn:: Syntax error: [prim:reference] expected after 'Notation' (in [vernac:command]).
+ .. exn:: Syntax error: [prim:reference] expected after 'Notation' (in [vernac:command]).
- The type passed to :cmd:`String Notation` must be a single
- identifier.
+ The type passed to :cmd:`String Notation` must be a single
+ identifier.
- .. exn:: Syntax error: [prim:reference] expected after [prim:reference] (in [vernac:command]).
+ .. exn:: Syntax error: [prim:reference] expected after [prim:reference] (in [vernac:command]).
- Both functions passed to :cmd:`String Notation` must be single
- identifiers.
+ Both functions passed to :cmd:`String Notation` must be single
+ identifiers.
- .. exn:: The reference @ident was not found in the current environment.
+ .. exn:: The reference @ident was not found in the current environment.
- Identifiers passed to :cmd:`String Notation` must exist in the
- global environment.
+ Identifiers passed to :cmd:`String Notation` must exist in the
+ global environment.
- .. exn:: @ident is bound to a notation that does not denote a reference.
+ .. exn:: @ident is bound to a notation that does not denote a reference.
- Identifiers passed to :cmd:`String Notation` must be global
- references, or notations which denote to single identifiers.
+ Identifiers passed to :cmd:`String Notation` must be global
+ references, or notations which denote to single identifiers.
.. _TacticNotation:
--
cgit v1.2.3