[numeral notation] Document the via ... using ... option

4 files changed, 139 insertions, 29 deletions

diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index a36772b2d7..f07eb02946 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -1553,14 +1553,16 @@ numbers (see :ref:`datatypes`).
 Number notations
 ~~~~~~~~~~~~~~~~
 
-.. cmd:: Number Notation @qualid__type @qualid__parse @qualid__print : @scope_name {? @number_modifier }
+.. cmd:: Number Notation @qualid__type @qualid__parse @qualid__print {? ( {+, @number_modifier } ) } : @scope_name
    :name: Number Notation
 
-   .. insertprodn number_modifier number_modifier
+   .. insertprodn number_modifier number_via
 
    .. prodn::
-      number_modifier ::= ( warning after @bignat )
-      | ( abstract after @bignat )
+      number_modifier ::= warning after @bignat
+      | abstract after @bignat
+      | @number_via
+      number_via ::= via @qualid mapping [ {+, @qualid => @qualid } ]
 
    This command allows the user to customize the way number literals
    are parsed and printed.
@@ -1606,7 +1608,38 @@ Number notations
          function application, constructors, inductive type families,
          sorts, and primitive integers) will be considered for printing.
 
-      :n:`( warning after @bignat )`
+      :n:`via @qualid__ind mapping [ {+, @qualid__constant => @qualid__constructor } ]`
+         When using this option, :n:`@qualid__type` no
+         longer needs to be an inductive type and is instead mapped to the
+         inductive type :n:`@qualid__ind` according to the provided
+         list of pairs, whose first component :n:`@qualid__constant` is a
+         constant of type :n:`@qualid__type`
+         (or a function of type :n:`{* _ -> } @qualid__type`) and the second a
+         constructor of type :n:`@qualid__ind`. The type
+         :n:`@qualid__type` is then replaced by :n:`@qualid__ind` in the
+         above parser and printer types.
+
+         .. note::
+            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`.
 
@@ -1616,7 +1649,7 @@ Number notations
             with :n:`(warning after @bignat)`, this warning is emitted when
             parsing a number greater than or equal to :token:`bignat`.
 
-      :n:`( abstract after @bignat )`
+      :n:`abstract after @bignat`
          returns :n:`(@qualid__parse m)` when parsing a literal
          :n:`m` that's greater than :n:`@bignat` rather than reducing it to a normal form.
          Here :g:`m` will be a
@@ -1642,6 +1675,12 @@ Number notations
             As noted above, the :n:`(abstract after @natural)` directive has no
             effect when :n:`@qualid__parse` lands in an :g:`option` type.
 
+         .. exn:: 'via' and 'abstract' cannot be used together.
+
+            With the :n:`abstract after` option, the parser function
+            :n:`@qualid__parse` does not reduce large numbers to a normal form,
+            which prevents doing the translation given in the :n:`mapping` list.
+
    .. exn:: Cannot interpret this number as a value of type @type
 
      The number notation registered for :token:`type` does not support
@@ -1664,7 +1703,7 @@ Number notations
    .. exn:: Unexpected term @term while parsing a number 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.
 
@@ -1675,6 +1714,67 @@ Number notations
      concrete number expressed as a (hexa)decimal.  They may not return
      opaque constants.
 
+   .. exn:: Multiple 'via' options.
+
+     At most one :g:`via` option can be given.
+
+   .. exn:: Multiple 'warning after' or 'abstract after' options.
+
+     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.
+
 .. _string-notations:
 
 String notations
@@ -1746,7 +1846,7 @@ 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 with no
-     arguments.
+     arguments. Declare numeral notations for non-inductive types using :n:`@number_via`.
 
    .. exn:: Cannot interpret in @scope_name because @qualid could not be found in the current environment.
 
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 4d615a130a..e43583de09 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -1285,10 +1285,10 @@ command: [
 | WITH "Declare" "Scope" scope_name
 
 (* odd that these are in command while other notation-related ones are in syntax *)
-| REPLACE "Number" "Notation" reference OPT number_via reference reference ":" ident number_modifier
-| WITH "Number" "Notation" reference OPT number_via reference reference ":" scope_name number_modifier
-| REPLACE "Numeral" "Notation" reference OPT number_via reference reference ":" ident number_modifier
-| WITH "Numeral" "Notation" reference OPT number_via reference reference ":" scope_name number_modifier
+| REPLACE "Number" "Notation" reference reference reference OPT number_options ":" ident
+| 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
 
@@ -1358,10 +1358,6 @@ explicit_subentry: [
 | DELETE "constr"    (* covered by another prod *)
 ]
 
-number_modifier: [
-| OPTINREF
-]
-
 binder_tactic: [
 | REPLACE "let" [ "rec" | ] LIST1 let_clause SEP "with" "in" ltac_expr5
 | WITH "let" OPT "rec" let_clause LIST0 ( "with" let_clause ) "in" ltac_expr5
@@ -2464,6 +2460,8 @@ SPLICE: [
 | constr_with_bindings
 | simple_binding
 | ssexpr35 (* strange in mlg, ssexpr50 is after this *)
+| number_mapping
+| number_options
 ] (* end SPLICE *)
 
 RENAME: [
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 8a0feb0e2f..17fc220f6c 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -686,8 +686,8 @@ command: [
 | "Print" "Rings"      (* ring plugin *)
 | "Add" "Field" ident ":" constr OPT field_mods      (* ring plugin *)
 | "Print" "Fields"      (* ring plugin *)
-| "Number" "Notation" reference OPT number_via reference reference ":" ident number_modifier
-| "Numeral" "Notation" reference OPT number_via reference reference ":" ident number_modifier
+| "Number" "Notation" reference reference reference OPT number_options ":" ident
+| "Numeral" "Notation" reference reference reference ":" ident deprecated_number_modifier
 | "String" "Notation" reference reference reference ":" ident
 | "Ltac2" ltac2_entry      (* Ltac2 plugin *)
 | "Ltac2" "Eval" ltac2_expr6      (* Ltac2 plugin *)
@@ -2549,18 +2549,28 @@ field_mods: [
 | "(" LIST1 field_mod SEP "," ")"      (* ring plugin *)
 ]
 
-number_modifier: [
+deprecated_number_modifier: [
 |
 | "(" "warning" "after" bignat ")"
 | "(" "abstract" "after" bignat ")"
 ]
 
-number_using: [
-| reference reference
+number_mapping: [
+| reference "=>" reference
 ]
 
 number_via: [
-| "via" reference "using" "(" LIST1 number_using SEP "," ")"
+| "via" reference "mapping" "[" LIST1 number_mapping SEP "," "]"
+]
+
+number_modifier: [
+| "warning" "after" bignat
+| "abstract" "after" bignat
+| number_via
+]
+
+number_options: [
+| "(" LIST1 number_modifier SEP "," ")"
 ]
 
 tac2pat1: [
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index d12b3bf6cd..3d1041e592 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -884,8 +884,6 @@ command: [
 | "Print" "Rings"      (* ring plugin *)
 | "Add" "Field" ident ":" one_term OPT ( "(" LIST1 field_mod SEP "," ")" )      (* ring plugin *)
 | "Print" "Fields"      (* ring plugin *)
-| "Number" "Notation" qualid OPT number_via qualid qualid ":" scope_name OPT number_modifier
-| "Numeral" "Notation" qualid OPT number_via qualid qualid ":" scope_name OPT number_modifier
 | "Hint" "Cut" "[" hints_path "]" OPT ( ":" LIST1 ident )
 | "Typeclasses" "Transparent" LIST1 qualid
 | "Typeclasses" "Opaque" LIST1 qualid
@@ -910,7 +908,8 @@ command: [
 | "Derive" "Dependent" "Inversion_clear" ident "with" one_term "Sort" sort_family
 | "Declare" "Left" "Step" one_term
 | "Declare" "Right" "Step" one_term
-| "Numeral" "Notation" qualid OPT number_via qualid qualid ":" scope_name OPT number_modifier
+| "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
 | "SubClass" ident_decl def_body
 | thm_token ident_decl LIST0 binder ":" type LIST0 [ "with" ident_decl LIST0 binder ":" type ]
@@ -1270,17 +1269,20 @@ field_mod: [
 | "completeness" one_term      (* ring plugin *)
 ]
 
-number_modifier: [
+deprecated_number_modifier: [
+|
 | "(" "warning" "after" bignat ")"
 | "(" "abstract" "after" bignat ")"
 ]
 
-number_using: [
-| qualid qualid
+number_modifier: [
+| "warning" "after" bignat
+| "abstract" "after" bignat
+| number_via
 ]
 
 number_via: [
-| "via" qualid "using" "(" LIST1 number_using SEP "," ")"
+| "via" qualid "mapping" "[" LIST1 ( qualid "=>" qualid ) SEP "," "]"
 ]
 
 hints_path: [