[numeral notation] Handle implicit arguments

6 files changed, 118 insertions, 24 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: [
diff --git a/plugins/syntax/g_numeral.mlg b/plugins/syntax/g_numeral.mlg
index e60ae45b01..a3cc786a4a 100644
--- a/plugins/syntax/g_numeral.mlg
+++ b/plugins/syntax/g_numeral.mlg
@@ -31,8 +31,13 @@ let warn_deprecated_numeral_notation =
     (fun () ->
       strbrk "Numeral Notation is deprecated, please use Number Notation instead.")
 
-let pr_number_mapping (n, n') =
-  Libnames.pr_qualid n ++ spc () ++ str "=>" ++ spc () ++ Libnames.pr_qualid n'
+let pr_number_mapping (b, n, n') =
+  if b then
+    str "[" ++ Libnames.pr_qualid n ++ str "]" ++ spc () ++ str "=>" ++ spc ()
+    ++ Libnames.pr_qualid n'
+  else
+    Libnames.pr_qualid n ++ spc () ++ str "=>" ++ spc ()
+    ++ Libnames.pr_qualid n'
 
 let pr_number_via (n, l) =
   str "via " ++ Libnames.pr_qualid n ++ str " mapping ["
@@ -56,7 +61,8 @@ END
 
 VERNAC ARGUMENT EXTEND number_mapping
   PRINTED BY { pr_number_mapping }
-| [ reference(n) "=>" reference(n') ] -> { n, n' }
+| [ reference(n) "=>" reference(n') ] -> { false, n, n' }
+| [ "[" reference(n) "]" "=>" reference(n') ] -> { true, n, n' }
 END
 
 VERNAC ARGUMENT EXTEND number_via
diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml
index 316ca456a4..1efe6b77d1 100644
--- a/plugins/syntax/numeral.ml
+++ b/plugins/syntax/numeral.ml
@@ -21,7 +21,7 @@ module CMap = CMap.Make (Constr)
 
 (** * Number notation *)
 
-type number_string_via = qualid * (qualid * qualid) list
+type number_string_via = qualid * (bool * qualid * qualid) list
 type number_option =
   | After of numnot_option
   | Via of number_string_via
@@ -231,9 +231,10 @@ let elaborate_to_post env sigma ty_name ty_ind l =
      For each constant [cnst] and inductive constructor [indc] in [l], retrieve:
      * its location: [lcnst] and [lindc]
      * its GlobRef: [cnst] and [indc]
-     * its type: [tcnst] and [tindc] (decomposed in product by [get_type] above) *)
+     * its type: [tcnst] and [tindc] (decomposed in product by [get_type] above)
+     * [impls] are the implicit arguments of [cnst] *)
   let l =
-    let read (cnst, indc) =
+    let read (consider_implicits, cnst, indc) =
       let lcnst, lindc = cnst.CAst.loc, indc.CAst.loc in
       let cnst, ccnst = locate_global_constructor_inductive_or_constant cnst in
       let indc, cindc =
@@ -247,13 +248,16 @@ let elaborate_to_post env sigma ty_name ty_ind l =
         let lc, tc = get_type env sigma c in
         List.map (fun (n, c) -> n, rm_params c) lc, rm_params tc in
       let tcnst, tindc = get_type_wo_params ccnst, get_type_wo_params cindc in
-      lcnst, cnst, tcnst, lindc, indc, tindc in
+      let impls =
+        if not consider_implicits then [] else
+          Impargs.(select_stronger_impargs (implicits_of_global cnst)) in
+      lcnst, cnst, tcnst, lindc, indc, tindc, impls in
     List.map read l in
-  let eq_indc indc (_, _, _, _, indc', _) = GlobRef.equal indc indc' in
+  let eq_indc indc (_, _, _, _, indc', _, _) = GlobRef.equal indc indc' in
   (* Collect all inductive types involved.
      That is [ty_ind] and all final codomains of [tindc] above. *)
   let inds =
-    List.fold_left (fun s (_, _, _, _, _, tindc) -> CSet.add (snd tindc) s)
+    List.fold_left (fun s (_, _, _, _, _, tindc, _) -> CSet.add (snd tindc) s)
       (CSet.singleton ty_ind) l in
   (* And for each inductive, retrieve its constructors. *)
   let constructors =
@@ -264,7 +268,7 @@ let elaborate_to_post env sigma ty_name ty_ind l =
   (* Error if one [constructor] in some inductive in [inds]
      doesn't appear exactly once in [l] *)
   let _ = (* check_for duplicate constructor and error *)
-    List.fold_left (fun already_seen (_, cnst, _, loc, indc, _) ->
+    List.fold_left (fun already_seen (_, cnst, _, loc, indc, _, _) ->
         try
           let cnst' = List.assoc_f GlobRef.equal indc already_seen in
           remapping_error ?loc indc cnst' cnst
@@ -289,16 +293,23 @@ let elaborate_to_post env sigma ty_name ty_ind l =
              warn_via_remapping ?loc (env, sigma, ckey, old_cval, cval);
            m in
       List.fold_left
-        (fun (ind2ty, ty2ind) (lcnst, _, (_, tcnst), lindc, _, (_, tindc)) ->
+        (fun (ind2ty, ty2ind) (lcnst, _, (_, tcnst), lindc, _, (_, tindc), _) ->
           add lcnst tindc tcnst ind2ty, add lindc tcnst tindc ty2ind)
         CMap.(singleton ty_ind ty_name, singleton ty_name ty_ind) l in
     (* check that type of constants and constructors mapped in [l]
        match modulo [ind2ty] *)
+    let rm_impls impls (l, t) =
+      let rec aux impls l = match impls, l with
+        | Some _ :: impls, _ :: b -> aux impls b
+        | None :: impls, (n, a) :: b -> (n, a) :: aux impls b
+        | _ -> l in
+      aux impls l, t in
     let replace m (l, t) =
       let apply_m c = try CMap.find c m with Not_found -> c in
       List.fold_right (fun (na, a) b -> Constr.mkProd (na, (apply_m a), b))
         l (apply_m t) in
-    List.iter (fun (_, cnst, tcnst, loc, indc, tindc) ->
+    List.iter (fun (_, cnst, tcnst, loc, indc, tindc, impls) ->
+        let tcnst = rm_impls impls tcnst in
         let tcnst' = replace CMap.empty tcnst in
         if not (Constr.equal tcnst' (replace ind2ty tindc)) then
           let actual = replace CMap.empty tindc in
@@ -313,17 +324,21 @@ let elaborate_to_post env sigma ty_name ty_ind l =
       (CMap.singleton ty_ind 0, Int.Map.singleton 0 ty_ind, 1) in
   (* Finally elaborate [to_post] *)
   let to_post =
-    let rec map_prod = function
-      | [] -> []
-      | (_, a) :: b ->
-         let t = match CMap.find_opt a ind2num with
-           | Some i -> ToPostAs i
-           | None -> ToPostCopy in
-         t :: map_prod b in
+    let rec map_prod impls tindc = match impls with
+      | Some _ :: impls -> ToPostHole :: map_prod impls tindc
+      | _ ->
+         match tindc with
+         | [] -> []
+         | (_, a) :: b ->
+            let t = match CMap.find_opt a ind2num with
+              | Some i -> ToPostAs i
+              | None -> ToPostCopy in
+            let impls = match impls with [] -> [] | _ :: t -> t in
+            t :: map_prod impls b in
     Array.init nb_ind (fun i ->
         List.map (fun indc ->
-            let _, cnst, _, _, _, tindc = List.find (eq_indc indc) l in
-            indc, cnst, map_prod (fst tindc))
+            let _, cnst, _, _, _, tindc, impls = List.find (eq_indc indc) l in
+            indc, cnst, map_prod impls (fst tindc))
           (CMap.find (Int.Map.find i num2ind) constructors)) in
   (* and use constants mapped to constructors of [ty_ind] as triggers. *)
   let pt_refs = List.map (fun (_, cnst, _) -> cnst) (to_post.(0)) in
diff --git a/plugins/syntax/numeral.mli b/plugins/syntax/numeral.mli
index 1f6896d549..5a13d1068b 100644
--- a/plugins/syntax/numeral.mli
+++ b/plugins/syntax/numeral.mli
@@ -14,7 +14,7 @@ open Notation
 
 (** * Number notation *)
 
-type number_string_via = qualid * (qualid * qualid) list
+type number_string_via = qualid * (bool * qualid * qualid) list
 type number_option =
   | After of numnot_option
   | Via of number_string_via