[string notation] Handle parameterized inductives and non inductives

4 files changed, 193 insertions, 183 deletions

diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 60fbd68687..a52d7f08f0 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -1386,7 +1386,7 @@ Scopes` or :cmd:`Print Scope`.
 ``char_scope``
   This scope includes interpretation for all strings of the form ``"c"``
   where :g:`c` is an ASCII character, or of the form ``"nnn"`` where nnn is
-  a three-digits number (possibly with leading 0's), or of the form
+  a three-digit number (possibly with leading 0s), or of the form
   ``""""``. Their respective denotations are the ASCII code of :g:`c`, the
   decimal ASCII code ``nnn``, or the ascii code of the character ``"`` (i.e.
   the ASCII code 34), all of them being represented in the type :g:`ascii`.
@@ -1556,13 +1556,13 @@ Number notations
 .. cmd:: Number Notation @qualid__type @qualid__parse @qualid__print {? ( {+, @number_modifier } ) } : @scope_name
    :name: Number Notation
 
-   .. insertprodn number_modifier number_via
+   .. insertprodn number_modifier number_string_via
 
    .. prodn::
       number_modifier ::= warning after @bignat
       | abstract after @bignat
-      | @number_via
-      number_via ::= via @qualid mapping [ {+, {| @qualid => @qualid | [ @qualid ] => @qualid } } ]
+      | @number_string_via
+      number_string_via ::= via @qualid mapping [ {+, {| @qualid => @qualid | [ @qualid ] => @qualid } } ]
 
    This command allows the user to customize the way number literals
    are parsed and printed.
@@ -1608,11 +1608,7 @@ Number notations
          function application, constructors, inductive type families,
          sorts, and primitive integers) will be considered for printing.
 
-         .. note::
-            Number notations for parameterized inductive types can be
-            added by declaring an :ref:`abbreviation <Abbreviations>`
-            for the inductive which instantiates all parameters. See
-            example below.
+      .. _number-string-via:
 
       :n:`via @qualid__ind mapping [ {+, @qualid__constant => @qualid__constructor } ]`
          When using this option, :n:`@qualid__type` no
@@ -1649,22 +1645,6 @@ Number notations
             To use a :token:`sort` as the target type :n:`@qualid__type`, use an :ref:`abbreviation <Abbreviations>`
             as in the :ref:`example below <example-number-notation-non-inductive>`.
 
-         .. exn:: @qualid was already mapped to @qualid and cannot be remapped to @qualid
-
-            Duplicates are not allowed in the :n:`mapping` list.
-
-         .. exn:: Missing mapping for constructor @qualid
-
-            A mapping should be provided for :n:`@qualid` in the :n:`mapping` list.
-
-         .. warn:: @type was already mapped to @type, mapping it also to @type might yield ill typed terms when using the notation.
-
-            Two pairs in the :n:`mapping` list associate types that might be incompatible.
-
-         .. warn:: Type of @qualid seems incompatible with the type of @qualid. Expected type is: @type instead of @type. This might yield ill typed terms when using the notation.
-
-            A mapping given in the :n:`mapping` list associates a constant with a seemingly incompatible constructor.
-
       :n:`warning after @bignat`
          displays a warning message about a possible stack
          overflow when calling :n:`@qualid__parse` to parse a literal larger than :n:`@bignat`.
@@ -1748,166 +1728,47 @@ Number notations
 
      At most one :g:`warning after` or :g:`abstract after` option can be given.
 
-   .. _example-number-notation-non-inductive:
-
-   .. example:: Number Notation for a non inductive type
-
-      The following example encodes the terms in the form :g:`sum unit ( ... (sum unit unit) ... )`
-      as the number of units in the term. For instance :g:`sum unit (sum unit unit)`
-      is encoded as :g:`3` while :g:`unit` is :g:`1` and :g:`0` stands for :g:`Empty_set`.
-      The inductive :g:`I` will be used as :n:`@qualid__ind`.
-
-      .. coqtop:: in
-
-         Inductive I := Iempty : I | Iunit : I | Isum : I -> I -> I.
-
-      We then define :n:`@qualid__parse` and :n:`@qualid__print`
-
-      .. coqtop:: in
-
-         Definition of_uint (x : Number.uint) : I :=
-           let fix f n := match n with
-             | O => Iempty | S O => Iunit
-             | S n => Isum Iunit (f n) end in
-           f (Nat.of_num_uint x).
-
-         Definition to_uint (x : I) : Number.uint :=
-           let fix f i := match i with
-             | Iempty => O | Iunit => 1
-             | Isum i1 i2 => f i1 + f i2 end in
-           Nat.to_num_uint (f x).
-
-         Inductive sum (A : Set) (B : Set) : Set := pair : A -> B -> sum A B.
-
-      the number notation itself
-
-      .. coqtop:: in
-
-         Notation nSet := Set (only parsing).
-         Number Notation nSet of_uint to_uint (via I
-           mapping [Empty_set => Iempty, unit => Iunit, sum => Isum]) : type_scope.
-
-      and check the printer
-
-      .. coqtop:: all
-
-         Local Open Scope type_scope.
-         Check sum unit (sum unit unit).
-
-      and the parser
-
-      .. coqtop:: all
-
-         Set Printing All.
-         Check 3.
-
-   .. _example-number-notation-implicit-args:
-
-   .. example:: Number Notation with implicit arguments
-
-      The following example parses and prints natural numbers between
-      :g:`0` and :g:`n-1` as terms of type :g:`Fin.t n`.
-
-      .. coqtop:: all reset
-
-         Require Import Vector.
-         Print Fin.t.
-
-      Note the implicit arguments of :g:`Fin.F1` and :g:`Fin.FS`,
-      which won't appear in the corresponding inductive type.
-
-      .. coqtop:: in
-
-         Inductive I := I1 : I | IS : I -> I.
-
-         Definition of_uint (x : Number.uint) : I :=
-           let fix f n := match n with O => I1 | S n => IS (f n) end in
-           f (Nat.of_num_uint x).
-
-         Definition to_uint (x : I) : Number.uint :=
-           let fix f i := match i with I1 => O | IS n => S (f n) end in
-           Nat.to_num_uint (f x).
-
-         Declare Scope fin_scope.
-         Delimit Scope fin_scope with fin.
-         Local Open Scope fin_scope.
-         Number Notation Fin.t of_uint to_uint (via I
-           mapping [[Fin.F1] => I1, [Fin.FS] => IS]) : fin_scope.
-
-      Now :g:`2` is parsed as :g:`Fin.FS (Fin.FS Fin.F1)`, that is
-      :g:`@Fin.FS _ (@Fin.FS _ (@Fin.F1 _))`.
-
-      .. coqtop:: all
-
-         Check 2.
-
-      which can be of type :g:`Fin.t 3` (numbers :g:`0`, :g:`1` and :g:`2`)
-
-      .. coqtop:: all
-
-         Check 2 : Fin.t 3.
-
-      but cannot be of type :g:`Fin.t 2` (only :g:`0` and :g:`1`)
-
-      .. coqtop:: all fail
-
-         Check 2 : Fin.t 2.
-
-   .. example:: Number Notation with a parameterized inductive type
-
-      .. coqtop:: in reset
-
-         Definition of_uint u : list unit :=
-           let fix f n := match n with O => nil | S n => cons tt (f n) end in
-           f (Nat.of_num_uint u).
-         Definition to_uint (l : list unit) := Nat.to_num_uint (length l).
-
-      The parameter :g:`unit` for the parameterized inductive type
-      :g:`list` is given through an :ref:`abbreviation
-      <Abbreviations>`.
-
-      .. coqtop:: in
-
-         Notation list_unit := (list unit) (only parsing).
-         Number Notation list_unit of_uint to_uint : nat_scope.
-
 .. _string-notations:
 
 String notations
 ~~~~~~~~~~~~~~~~
 
-.. cmd:: String Notation @qualid @qualid__parse @qualid__print : @scope_name
+.. cmd:: String Notation @qualid__type @qualid__parse @qualid__print {? ( @number_string_via ) } : @scope_name
    :name: String Notation
 
    Allows the user to customize how strings are parsed and printed.
 
-   The token :n:`@qualid` should be the name of an inductive type,
-   while :n:`@qualid__parse` and :n:`@qualid__print` should be the names of the
-   parsing and printing functions, respectively.  The parsing function
-   :n:`@qualid__parse` should have one of the following types:
+      :n:`@qualid__type`
+         the name of an inductive type,
+         while :n:`@qualid__parse` and :n:`@qualid__print` should be the names of the
+         parsing and printing functions, respectively.  The parsing function
+         :n:`@qualid__parse` should have one of the following types:
 
-      * :n:`Byte.byte -> @qualid`
-      * :n:`Byte.byte -> option @qualid`
-      * :n:`list Byte.byte -> @qualid`
-      * :n:`list Byte.byte -> option @qualid`
+            * :n:`Byte.byte -> @qualid__type`
+            * :n:`Byte.byte -> option @qualid__type`
+            * :n:`list Byte.byte -> @qualid__type`
+            * :n:`list Byte.byte -> option @qualid__type`
 
-   The printing function :n:`@qualid__print` should have one of the
-   following types:
+         The printing function :n:`@qualid__print` should have one of the
+         following types:
 
-      * :n:`@qualid -> Byte.byte`
-      * :n:`@qualid -> option Byte.byte`
-      * :n:`@qualid -> list Byte.byte`
-      * :n:`@qualid -> option (list Byte.byte)`
+            * :n:`@qualid__type -> Byte.byte`
+            * :n:`@qualid__type -> option Byte.byte`
+            * :n:`@qualid__type -> list Byte.byte`
+            * :n:`@qualid__type -> option (list Byte.byte)`
 
-   When parsing, the application of the parsing function
-   :n:`@qualid__parse` 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:`@qualid__parse` to the string will be fully reduced, and universes
+         of the resulting term will be refreshed.
+
+         Note that only fully-reduced ground terms (terms containing only
+         function application, constructors, inductive type families,
+         sorts, and primitive integers) will be considered for printing.
 
-   Note that only fully-reduced ground terms (terms containing only
-   function application, constructors, inductive type families,
-   sorts, and primitive integers) will be considered for printing.
+      :n:`via @qualid__ind mapping [ {+, @qualid__constant => @qualid__constructor } ]`
+         works as for :ref:`number notations above <number-string-via>`.
 
-   .. 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
@@ -1926,7 +1787,7 @@ String notations
    .. exn:: Unexpected term @term while parsing a string notation.
 
      Parsing functions must always return ground terms, made up of
-     applications of constructors, inductive types, and primitive
+     function application, constructors, inductive type families, sorts and primitive
      integers.  Parsing functions may not return terms containing
      axioms, bare (co)fixpoints, lambdas, etc.
 
@@ -1937,12 +1798,33 @@ String notations
      concrete string expressed as a decimal.  They may not return
      opaque constants.
 
+.. note::
+   Number or string notations for parameterized inductive types can be
+   added by declaring an :ref:`abbreviation <Abbreviations>` for the
+   inductive which instantiates all parameters. See :ref:`example below <example-string-notation-parameterized-inductive>`.
+
 The following errors apply to both string and number notations:
 
    .. exn:: @type is not an inductive type.
 
      String and number notations can only be declared for inductive types.
-     Declare number notations for non-inductive types using :n:`@number_via`.
+     Declare string or numeral notations for non-inductive types using :n:`@number_string_via`.
+
+   .. exn:: @qualid was already mapped to @qualid and cannot be remapped to @qualid
+
+      Duplicates are not allowed in the :n:`mapping` list.
+
+   .. exn:: Missing mapping for constructor @qualid
+
+      A mapping should be provided for :n:`@qualid` in the :n:`mapping` list.
+
+   .. warn:: @type was already mapped to @type, mapping it also to @type might yield ill typed terms when using the notation.
+
+      Two pairs in the :n:`mapping` list associate types that might be incompatible.
+
+   .. warn:: Type of @qualid seems incompatible with the type of @qualid. Expected type is: @type instead of @type. This might yield ill typed terms when using the notation.
+
+      A mapping given in the :n:`mapping` list associates a constant with a seemingly incompatible constructor.
 
    .. exn:: Cannot interpret in @scope_name because @qualid could not be found in the current environment.
 
@@ -1975,6 +1857,129 @@ The following errors apply to both string and number notations:
 
      .. todo note on "single qualified identifiers" https://github.com/coq/coq/pull/11718#discussion_r415076703
 
+.. _example-number-notation-non-inductive:
+
+.. example:: Number Notation for a non inductive type
+
+   The following example encodes the terms in the form :g:`sum unit ( ... (sum unit unit) ... )`
+   as the number of units in the term. For instance :g:`sum unit (sum unit unit)`
+   is encoded as :g:`3` while :g:`unit` is :g:`1` and :g:`0` stands for :g:`Empty_set`.
+   The inductive :g:`I` will be used as :n:`@qualid__ind`.
+
+   .. coqtop:: in
+
+      Inductive I := Iempty : I | Iunit : I | Isum : I -> I -> I.
+
+   We then define :n:`@qualid__parse` and :n:`@qualid__print`
+
+   .. coqtop:: in
+
+      Definition of_uint (x : Number.uint) : I :=
+        let fix f n := match n with
+          | O => Iempty | S O => Iunit
+          | S n => Isum Iunit (f n) end in
+        f (Nat.of_num_uint x).
+
+      Definition to_uint (x : I) : Number.uint :=
+        let fix f i := match i with
+          | Iempty => O | Iunit => 1
+          | Isum i1 i2 => f i1 + f i2 end in
+        Nat.to_num_uint (f x).
+
+      Inductive sum (A : Set) (B : Set) : Set := pair : A -> B -> sum A B.
+
+   the number notation itself
+
+   .. coqtop:: in
+
+      Notation nSet := Set (only parsing).
+      Number Notation nSet of_uint to_uint (via I
+        mapping [Empty_set => Iempty, unit => Iunit, sum => Isum]) : type_scope.
+
+   and check the printer
+
+   .. coqtop:: all
+
+      Local Open Scope type_scope.
+      Check sum unit (sum unit unit).
+
+   and the parser
+
+   .. coqtop:: all
+
+      Set Printing All.
+      Check 3.
+
+.. _example-number-notation-implicit-args:
+
+.. example:: Number Notation with implicit arguments
+
+   The following example parses and prints natural numbers between
+   :g:`0` and :g:`n-1` as terms of type :g:`Fin.t n`.
+
+   .. coqtop:: all reset
+
+      Require Import Vector.
+      Print Fin.t.
+
+   Note the implicit arguments of :g:`Fin.F1` and :g:`Fin.FS`,
+   which won't appear in the corresponding inductive type.
+
+   .. coqtop:: in
+
+      Inductive I := I1 : I | IS : I -> I.
+
+      Definition of_uint (x : Number.uint) : I :=
+        let fix f n := match n with O => I1 | S n => IS (f n) end in
+        f (Nat.of_num_uint x).
+
+      Definition to_uint (x : I) : Number.uint :=
+        let fix f i := match i with I1 => O | IS n => S (f n) end in
+        Nat.to_num_uint (f x).
+
+      Declare Scope fin_scope.
+      Delimit Scope fin_scope with fin.
+      Local Open Scope fin_scope.
+      Number Notation Fin.t of_uint to_uint (via I
+        mapping [[Fin.F1] => I1, [Fin.FS] => IS]) : fin_scope.
+
+   Now :g:`2` is parsed as :g:`Fin.FS (Fin.FS Fin.F1)`, that is
+   :g:`@Fin.FS _ (@Fin.FS _ (@Fin.F1 _))`.
+
+   .. coqtop:: all
+
+      Check 2.
+
+   which can be of type :g:`Fin.t 3` (numbers :g:`0`, :g:`1` and :g:`2`)
+
+   .. coqtop:: all
+
+      Check 2 : Fin.t 3.
+
+   but cannot be of type :g:`Fin.t 2` (only :g:`0` and :g:`1`)
+
+   .. coqtop:: all fail
+
+      Check 2 : Fin.t 2.
+
+.. _example-string-notation-parameterized-inductive:
+
+.. example:: String Notation with a parameterized inductive type
+
+   The parameter :g:`Byte.byte` for the parameterized inductive type
+   :g:`list` is given through an :ref:`abbreviation <Abbreviations>`.
+
+   .. coqtop:: in reset
+
+      Notation string := (list Byte.byte) (only parsing).
+      Definition id_string := @id string.
+
+      String Notation string id_string id_string : list_scope.
+
+   .. coqtop:: all
+
+      Check "abc"%list.
+
 .. _TacticNotation:
 
 Tactic Notations
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index e43583de09..5de1f09c53 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -1289,8 +1289,8 @@ command: [
 | WITH "Number" "Notation" reference reference reference OPT number_options ":" scope_name
 | REPLACE "Numeral" "Notation" reference reference reference ":" ident deprecated_number_modifier
 | WITH "Numeral" "Notation" reference reference reference ":" scope_name deprecated_number_modifier
-| REPLACE "String" "Notation" reference reference reference ":" ident
-| WITH "String" "Notation" reference reference reference ":" scope_name
+| REPLACE "String" "Notation" reference reference reference OPT string_option ":" ident
+| WITH "String" "Notation" reference reference reference OPT string_option ":" scope_name
 
 | DELETE "Ltac2" ltac2_entry      (* was split up *)
 | DELETE "Add" "Zify" "InjTyp" constr      (* micromega plugin *)
@@ -2460,8 +2460,9 @@ SPLICE: [
 | constr_with_bindings
 | simple_binding
 | ssexpr35 (* strange in mlg, ssexpr50 is after this *)
-| number_mapping
+| number_string_mapping
 | number_options
+| string_option
 ] (* end SPLICE *)
 
 RENAME: [
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 3a0c3a8bc7..826a0b6f36 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -688,7 +688,7 @@ command: [
 | "Print" "Fields"      (* ring plugin *)
 | "Number" "Notation" reference reference reference OPT number_options ":" ident
 | "Numeral" "Notation" reference reference reference ":" ident deprecated_number_modifier
-| "String" "Notation" reference reference reference ":" ident
+| "String" "Notation" reference reference reference OPT string_option ":" ident
 | "Ltac2" ltac2_entry      (* Ltac2 plugin *)
 | "Ltac2" "Eval" ltac2_expr6      (* Ltac2 plugin *)
 | "Print" "Ltac2" reference      (* Ltac2 plugin *)
@@ -2555,25 +2555,29 @@ deprecated_number_modifier: [
 | "(" "abstract" "after" bignat ")"
 ]
 
-number_mapping: [
+number_string_mapping: [
 | reference "=>" reference
 | "[" reference "]" "=>" reference
 ]
 
-number_via: [
-| "via" reference "mapping" "[" LIST1 number_mapping SEP "," "]"
+number_string_via: [
+| "via" reference "mapping" "[" LIST1 number_string_mapping SEP "," "]"
 ]
 
 number_modifier: [
 | "warning" "after" bignat
 | "abstract" "after" bignat
-| number_via
+| number_string_via
 ]
 
 number_options: [
 | "(" LIST1 number_modifier SEP "," ")"
 ]
 
+string_option: [
+| "(" number_string_via ")"
+]
+
 tac2pat1: [
 | Prim.qualid LIST1 tac2pat0      (* Ltac2 plugin *)
 | Prim.qualid      (* Ltac2 plugin *)
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 13d8979208..151438bbbd 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -910,7 +910,7 @@ command: [
 | "Declare" "Right" "Step" one_term
 | "Number" "Notation" qualid qualid qualid OPT ( "(" LIST1 number_modifier SEP "," ")" ) ":" scope_name
 | "Numeral" "Notation" qualid qualid qualid ":" scope_name deprecated_number_modifier
-| "String" "Notation" qualid qualid qualid ":" scope_name
+| "String" "Notation" qualid qualid qualid OPT ( "(" number_string_via ")" ) ":" scope_name
 | "SubClass" ident_decl def_body
 | thm_token ident_decl LIST0 binder ":" type LIST0 [ "with" ident_decl LIST0 binder ":" type ]
 | assumption_token OPT ( "Inline" OPT ( "(" natural ")" ) ) [ LIST1 ( "(" assumpt ")" ) | assumpt ]
@@ -1278,10 +1278,10 @@ deprecated_number_modifier: [
 number_modifier: [
 | "warning" "after" bignat
 | "abstract" "after" bignat
-| number_via
+| number_string_via
 ]
 
-number_via: [
+number_string_via: [
 | "via" qualid "mapping" "[" LIST1 [ qualid "=>" qualid | "[" qualid "]" "=>" qualid ] SEP "," "]"
 ]