Fixes #12682 (recursive notation printing bug with n-ary applications).

A special case for recursive n-ary applications was missing when the
head of the application was a reference.

5 files changed, 58 insertions, 14 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 95df626d4c..3667757a2f 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -858,10 +858,17 @@ let extern_possible_prim_token (custom,scopes) r =
       insert_entry_coercion coercion (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key)
 
 let filter_enough_applied nargs l =
+  (* This is to ensure that notations for coercions are used only when
+     the coercion is fully applied; not explicitly done yet, but we
+     could also expect that the notation is exactly talking about the
+     coercion *)
   match nargs with
   | None -> l
   | Some nargs ->
-  List.filter (fun (keyrule,pat,n as _rule) -> match n with Some n -> n > nargs | None -> false) l
+  List.filter (fun (keyrule,pat,n as _rule) ->
+      match n with
+      | AppBoundedNotation n -> n > nargs
+      | AppUnboundedNotation | NotAppNotation -> false) l
 
 (* Helper function for safe and optimal printing of primitive tokens  *)
 (* such as those for Int63                                            *)
@@ -1247,7 +1254,7 @@ and extern_notation (custom,scopes as allscopes) vars t rules =
             [], [] in
         (* Adjust to the number of arguments expected by the notation *)
         let (t,args,argsscopes,argsimpls) = match n with
-          | Some n when nallargs >= n ->
+          | AppBoundedNotation n when nallargs >= n ->
               let args1, args2 = List.chop n args in
               let args2scopes = try List.skipn n argsscopes with Failure _ -> [] in
               let args2impls =
@@ -1257,12 +1264,13 @@ and extern_notation (custom,scopes as allscopes) vars t rules =
                   []
                 else try List.skipn n argsimpls with Failure _ -> [] in
               DAst.make @@ GApp (f,args1), args2, args2scopes, args2impls
-          | None ->
+          | AppUnboundedNotation -> t, [], [], []
+          | NotAppNotation ->
             begin match DAst.get f with
             | GRef (ref,us) -> f, args, argsscopes, argsimpls
             | _ -> t, [], [], []
             end
-          | _ -> raise No_match in
+          | AppBoundedNotation _ -> raise No_match in
         (* Try matching ... *)
         let terms,termlists,binders,binderlists =
           match_notation_constr !print_universes t pat in
diff --git a/interp/notation.ml b/interp/notation.ml
index e282d62396..c4e9496b95 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -293,7 +293,12 @@ let key_compare k1 k2 = match k1, k2 with
 module KeyOrd = struct type t = key let compare = key_compare end
 module KeyMap = Map.Make(KeyOrd)
 
-type notation_rule = interp_rule * interpretation * int option
+type notation_applicative_status =
+  | AppBoundedNotation of int
+  | AppUnboundedNotation
+  | NotAppNotation
+
+type notation_rule = interp_rule * interpretation * notation_applicative_status
 
 let keymap_add key interp map =
   let old = try KeyMap.find key map with Not_found -> [] in
@@ -329,13 +334,14 @@ let cases_pattern_key c = match DAst.get c with
   | _ -> Oth
 
 let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *)
-  | NApp (NRef ref,args) -> RefKey(canonical_gr ref), Some (List.length args)
+  | NApp (NRef ref,args) -> RefKey(canonical_gr ref), AppBoundedNotation (List.length args)
   | NList (_,_,NApp (NRef ref,args),_,_)
   | NBinderList (_,_,NApp (NRef ref,args),_,_) ->
-      RefKey (canonical_gr ref), Some (List.length args)
-  | NRef ref -> RefKey(canonical_gr ref), None
-  | NApp (_,args) -> Oth, Some (List.length args)
-  | _ -> Oth, None
+      RefKey (canonical_gr ref), AppBoundedNotation (List.length args)
+  | NRef ref -> RefKey(canonical_gr ref), NotAppNotation
+  | NApp (_,args) -> Oth, AppBoundedNotation (List.length args)
+  | NList (_,_,NApp (NVar x,_),_,_) when x = Notation_ops.ldots_var -> Oth, AppUnboundedNotation
+  | _ -> Oth, NotAppNotation
 
 (** Dealing with precedences *)
 
diff --git a/interp/notation.mli b/interp/notation.mli
index c39bfa6e28..05ddd25a62 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -239,7 +239,12 @@ val declare_uninterpretation : interp_rule -> interpretation -> unit
 val interp_notation : ?loc:Loc.t -> notation -> subscopes ->
       interpretation * (notation_location * scope_name option)
 
-type notation_rule = interp_rule * interpretation * int option
+type notation_applicative_status =
+  | AppBoundedNotation of int
+  | AppUnboundedNotation
+  | NotAppNotation
+
+type notation_rule = interp_rule * interpretation * notation_applicative_status
 
 (** Return the possible notations for a given term *)
 val uninterp_notations : 'a glob_constr_g -> notation_rule list
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index 53ad8a9612..90a6a2ad96 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -80,6 +80,12 @@ NIL : list nat
      : Z * Z * (Z * Z) * (Z * Z) * (Z * bool * (Z * bool) * (Z * bool))
 fun f : Z -> Z -> Z -> Z => {|f; 0; 1; 2|} : Z
      : (Z -> Z -> Z -> Z) -> Z
+{|fun x : Z => x + x; 0|}
+     : Z
+{|op; 0; 1|}
+     : Z
+false = 0
+     : Prop
 Init.Nat.add
      : nat -> nat -> nat
 S
diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v
index 7d2f1e9ba8..d0b2f40f9c 100644
--- a/test-suite/output/Notations.v
+++ b/test-suite/output/Notations.v
@@ -216,13 +216,32 @@ Check [|0*(1,2,3);(4,5,6)*false|].
 
 (**********************************************************************)
 (* Test recursive notations involving applications                    *)
-(* Caveat: does not work for applied constant because constants are   *)
-(* classified as notations for the particular constant while this     *)
-(* generic application notation is classified as generic              *)
+
+Module Application.
 
 Notation "{| f ; x ; .. ; y |}" := ( .. (f x) .. y).
+
+(* Application to a variable *)
+
 Check fun f => {| f; 0; 1; 2 |} : Z.
 
+(* Application to a fun *)
+
+Check {| (fun x => x+x); 0 |}.
+
+(* Application to a reference *)
+
+Axiom op : Z -> Z -> Z.
+Check {| op; 0; 1 |}.
+
+(* Interaction with coercion *)
+
+Axiom c : Z -> bool.
+Coercion c : Z >-> bool.
+Check false = {| c; 0 |}.
+
+End Application.
+
 (**********************************************************************)
 (* Check printing of notations from other modules *)