[numeral notation] Handle implicit arguments

3 files changed, 75 insertions, 2 deletions

diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index f07eb02946..4c6d300b13 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -1562,7 +1562,7 @@ Number notations
       number_modifier ::= warning after @bignat
       | abstract after @bignat
       | @number_via
-      number_via ::= via @qualid mapping [ {+, @qualid => @qualid } ]
+      number_via ::= via @qualid mapping [ {+, {| @qualid => @qualid | [ @qualid ] => @qualid } } ]
 
    This command allows the user to customize the way number literals
    are parsed and printed.
@@ -1619,6 +1619,26 @@ Number notations
          :n:`@qualid__type` is then replaced by :n:`@qualid__ind` in the
          above parser and printer types.
 
+         When :n:`@qualid__constant` is surrounded by square brackets,
+         all the implicit arguments of :n:`@qualid__constant` (whether maximally inserted or not) are ignored
+         when translating to :n:`@qualid__constructor` (i.e., before
+         applying :n:`@qualid__print`) and replaced with implicit
+         argument holes :g:`_` when translating from
+         :n:`@qualid__constructor` to :n:`@qualid__constant` (after
+         :n:`@qualid__parse`). See below for an :ref:`example <example-number-notation-implicit-args>`.
+
+         .. note::
+            The implicit status of the arguments is considered
+            only at notation declaration time, any further
+            modification of this status has no impact
+            on the previously declared notations.
+
+         .. note::
+            In case of multiple implicit options (for instance
+            :g:`Arguments eq_refl {A}%type_scope {x}, [_] _`), an
+            argument is considered implicit when it is implicit in any of the
+            options.
+
          .. 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>`.
@@ -1775,6 +1795,58 @@ Number notations
          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.
+
 .. _string-notations:
 
 String notations
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 17fc220f6c..3a0c3a8bc7 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -2557,6 +2557,7 @@ deprecated_number_modifier: [
 
 number_mapping: [
 | reference "=>" reference
+| "[" reference "]" "=>" reference
 ]
 
 number_via: [
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 3d1041e592..13d8979208 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -1282,7 +1282,7 @@ number_modifier: [
 ]
 
 number_via: [
-| "via" qualid "mapping" "[" LIST1 ( qualid "=>" qualid ) SEP "," "]"
+| "via" qualid "mapping" "[" LIST1 [ qualid "=>" qualid | "[" qualid "]" "=>" qualid ] SEP "," "]"
 ]
 
 hints_path: [