Merge PR #11120: Refactoring code for application printing + fixing #11091 (inconsistencies in parsing/printing notations to partial applications)

Ack-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: jfehrle

6 files changed, 217 insertions, 80 deletions

diff --git a/test-suite/bugs/bug_4690.v b/test-suite/bugs/bug_4690.v
new file mode 100644
index 0000000000..f50866a990
--- /dev/null
+++ b/test-suite/bugs/bug_4690.v
@@ -0,0 +1,3 @@
+(* Check that @f is not allowed in notation when f is a notation variable *)
+
+Fail Notation "# g" := (@g O) (at level 0).
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index b870fa6f6f..53ad8a9612 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -107,14 +107,15 @@ fun x : option Z => match x with
                     end
      : option Z -> Z
 fun x : option Z => match x with
-                    | SOME2 x0 => x0
-                    | NONE2 => 0
+                    | SOME3 _ x0 => x0
+                    | NONE3 _ => 0
                     end
      : option Z -> Z
-fun x : list ?T => match x with
-                   | NIL => NONE2
-                   | (_ :') t => SOME2 t
-                   end
+fun x : list ?T =>
+match x with
+| NIL => NONE3 (list ?T)
+| (_ :') t => SOME3 (list ?T) t
+end
      : list ?T -> option (list ?T)
 where
 ?T : [x : list ?T  x1 : list ?T  x0 := x1 : list ?T |- Type] (x, x1,
diff --git a/test-suite/output/Notations5.out b/test-suite/output/Notations5.out
index c5b4d6f291..f59306c454 100644
--- a/test-suite/output/Notations5.out
+++ b/test-suite/output/Notations5.out
@@ -78,11 +78,11 @@ f
        T a1 a2 -> forall (B : Type) (b : B), a1 = a2 /\ b = b
 f
      : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b
-p
+u ?A
      : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
 where
 ?A : [ |- Type]
-p
+u ?A
      : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
 where
 ?A : [ |- Type]
@@ -90,23 +90,23 @@ u
      : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
 u
      : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
-p 0 0
+u nat 0 0 ?B
      : forall b : ?B, 0 = 0 /\ b = b
 where
 ?B : [ |- Type]
-p 0 0
+u nat 0 0 bool
      : forall b : bool, 0 = 0 /\ b = b
-@p nat 0 0
+u nat 0 0
      : forall (B : Type) (b : B), 0 = 0 /\ b = b
-@p nat 0 0
+u nat 0 0
      : forall (B : Type) (b : B), 0 = 0 /\ b = b
 u
      : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
 where
 ?A : [ |- Type]
-u
+@u
      : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
-u
+@u
      : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
 u
      : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
@@ -138,7 +138,7 @@ v 0
      : forall b : ?B, 0 = 0 /\ b = b
 where
 ?B : [ |- Type]
-v 0 (B:=bool) true
+v 0 true
      : 0 = 0 /\ true = true
 v
      : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
@@ -158,7 +158,7 @@ v 0
      : forall b : ?B, 0 = 0 /\ b = b
 where
 ?B : [ |- Type]
-v 0 (B:=bool) true
+v 0 true
      : 0 = 0 /\ true = true
 v
      : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
@@ -188,15 +188,15 @@ where
      : forall b : ?B, 0 = 0 /\ b = b
 where
 ?B : [ |- Type]
-## 0 0 (B:=bool) true
+## 0 0 true
      : 0 = 0 /\ true = true
-## 0 0 (B:=bool) true
+## 0 0 true
      : 0 = 0 /\ true = true
 ## 0 0 (B:=bool)
      : forall b : bool, 0 = 0 /\ b = b
 ## 0 0 (B:=bool)
      : forall b : bool, 0 = 0 /\ b = b
-p
+## ?A
      : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
 where
 ?A : [ |- Type]
@@ -204,45 +204,109 @@ where
      : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
 ##
      : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
-p 0
+## nat 0
      : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
-p 0
+## nat 0
      : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
-@p nat 0 0
+## nat 0 0
      : forall (B : Type) (b : B), 0 = 0 /\ b = b
-p 0 0
+## nat 0 0 ?B
      : forall b : ?B, 0 = 0 /\ b = b
 where
 ?B : [ |- Type]
-p 0 0
+## nat 0 0 ?B
      : forall b : ?B, 0 = 0 /\ b = b
 where
 ?B : [ |- Type]
-p 0 0
+## nat 0 0 bool
      : forall b : bool, 0 = 0 /\ b = b
-p 0 0 true
+## nat 0 0 bool true
      : 0 = 0 /\ true = true
 ## 0
      : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
 ## 0
      : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
+## 0 0
+     : forall b : ?B, 0 = 0 /\ b = b
+where
+?B : [ |- Type]
 ## 0 0 (B:=bool)
      : forall b : bool, 0 = 0 /\ b = b
 ## 0 0 (B:=bool)
      : forall b : bool, 0 = 0 /\ b = b
-## 0 0 (B:=bool) true
+## 0 0 true
      : 0 = 0 /\ true = true
-## 0 0 (B:=bool) true
+## 0 0 true
      : 0 = 0 /\ true = true
 ## 0
      : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
 ## 0
      : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
+## 0 0
+     : forall b : ?B, 0 = 0 /\ b = b
+where
+?B : [ |- Type]
 ## 0 0 (B:=bool)
      : forall b : bool, 0 = 0 /\ b = b
 ## 0 0 (B:=bool)
      : forall b : bool, 0 = 0 /\ b = b
-## 0 0 (B:=bool) true
+## 0 0 true
      : 0 = 0 /\ true = true
-## 0 0 (B:=bool) true
+## 0 0 true
      : 0 = 0 /\ true = true
+# 0 0 bool 0%bool
+     : T
+fun a : T => match a with
+             | # 0 0 _ _ => 1
+             | _ => 2
+             end
+     : T -> nat
+#' 0 0 0%bool
+     : T
+fun a : T => match a with
+             | #' 0 0 _ => 1
+             | _ => 2
+             end
+     : T -> nat
+## 0 0 0%bool
+     : T
+fun a : T => match a with
+             | ## 0 0 _ => 1
+             | _ => 2
+             end
+     : T -> nat
+##' 0 0 0%bool
+     : T
+fun a : T => match a with
+             | ##' 0 0 _ => 1
+             | _ => 2
+             end
+     : T -> nat
+P 0 0 bool 0%bool
+     : T
+fun a : T => match a with
+             | P 0 0 _ _ => 1
+             | _ => 2
+             end
+     : T -> nat
+P' 0 0 0%bool
+     : T
+fun a : T => match a with
+             | P' 0 0 _ => 1
+             | _ => 2
+             end
+     : T -> nat
+Q 0 0 0%bool
+     : T
+fun a : T => match a with
+             | Q 0 0 _ => 1
+             | _ => 2
+             end
+     : T -> nat
+Q' 0 0 0%bool
+     : T
+fun a : T => match a with
+             | Q' 0 0 _ => 1
+             | _ => 2
+             end
+     : T -> nat
diff --git a/test-suite/output/Notations5.v b/test-suite/output/Notations5.v
index b3bea929ba..09d5e31c48 100644
--- a/test-suite/output/Notations5.v
+++ b/test-suite/output/Notations5.v
@@ -115,21 +115,21 @@ Module AppliedTermsPrinting.
   Notation u := @p.
 
   Check u _.
-  (* p *)
+  (* u ?A *)
   Check p.
-  (* p *)
+  (* u ?A *)
   Check @p.
   (* u *)
   Check u.
   (* u *)
   Check p 0 0.
-  (* p 0 0 *)
+  (* u nat 0 0 ?B *)
   Check u nat 0 0 bool.
-  (* p 0 0 -- WEAKNESS should ideally be (B:=bool) *)
+  (* u nat 0 0 bool *)
   Check u nat 0 0.
-  (* @p nat 0 0 *)
+  (* u nat 0 0 *)
   Check @p nat 0 0.
-  (* @p nat 0 0 *)
+  (* u nat 0 0 *)
 
   End AtAbbreviationForApplicationHead.
 
@@ -145,9 +145,9 @@ Module AppliedTermsPrinting.
   Check p.
   (* u *)
   Check @p.
-  (* u -- BUG *)
+  (* @u *)
   Check @u.
-  (* u -- BUG *)
+  (* @u *)
   Check u.
   (* u *)
   Check p 0 0.
@@ -181,7 +181,7 @@ Module AppliedTermsPrinting.
   Check v 0.
   (* v 0 *)
   Check v 0 true.
-  (* v 0 (B:=bool) true -- BUG *)
+  (* v 0 true *)
   Check @p nat 0.
   (* v *)
   Check @p nat 0 0.
@@ -209,7 +209,7 @@ Module AppliedTermsPrinting.
   Check v 0.
   (* v 0 *)
   Check v 0 true.
-  (* v 0 (B:=bool) true -- BUG *)
+  (* v 0 true *)
   Check @p nat 0.
   (* v *)
   Check @p nat 0 0.
@@ -243,9 +243,9 @@ Module AppliedTermsPrinting.
   Check ## 0 0.
   (* ## 0 0 *)
   Check p 0 0 true.
-  (* ## 0 0 (B:=bool) true -- BUG B should not be displayed *)
+  (* ## 0 0 true *)
   Check ## 0 0 true.
-  (* ## 0 0 (B:=bool) true -- BUG B should not be displayed *)
+  (* ## 0 0 true *)
   Check p 0 0 (B:=bool).
   (* ## 0 0 (B:=bool) *)
   Check ## 0 0 (B:=bool).
@@ -263,25 +263,25 @@ Module AppliedTermsPrinting.
   Notation "##" := @p (at level 0).
 
   Check p.
-  (* p *)
+  (* ## ?A *)
   Check @p.
   (* ## *)
   Check ##.
   (* ## *)
   Check p 0.
-  (* p 0 -- why not "## nat 0" *)
+  (* ## nat 0 *)
   Check ## nat 0.
-  (* p 0 *)
+  (* ## nat 0 *)
   Check ## nat 0 0.
-  (* @p nat 0 0 *)
+  (* ## nat 0 0 *)
   Check p 0 0.
-  (* p 0 0 *)
+  (* ## nat 0 0 ?B *)
   Check ## nat 0 0 _.
-  (* p 0 0 *)
+  (* ## nat 0 0 ?B *)
   Check ## nat 0 0 bool.
-  (* p 0 0 (B:=bool) *)
+  (* ## nat 0 0 bool *)
   Check ## nat 0 0 bool true.
-  (* p 0 0 true *)
+  (* ## nat 0 0 bool true *)
 
   End AtNotationForHeadApplication.
 
@@ -298,16 +298,16 @@ Module AppliedTermsPrinting.
   (* ## 0 *)
   Check ## 0.
   (* ## 0 *)
-  (* Check ## 0 0. *)
-  (* Anomaly *)
+  Check ## 0 0.
+  (* ## 0 0 *)
   Check p 0 0 (B:=bool).
   (* ## 0 0 (B:=bool) *)
-  Check ## 0 0 bool.
-  (* ## 0 0 (B:=bool) -- INCONSISTENT parsing/printing *)
+  Check ## 0 0 (B:=bool).
+  (* ## 0 0 (B:=bool) *)
   Check p 0 0 true.
-  (* ## 0 0 (B:=bool) true -- BUG B should not be displayed *)
-  Check ## 0 0 bool true.
-  (* ## 0 0 (B:=bool) true -- INCONSISTENT parsing/printing + BUG B should not be displayed *)
+  (* ## 0 0 true *)
+  Check ## 0 0 true.
+  (* ## 0 0 true *)
 
   End NotationForPartialApplication.
 
@@ -324,17 +324,75 @@ Module AppliedTermsPrinting.
   (* ## 0 *)
   Check ## 0.
   (* ## 0 *)
-  (* Check ## 0 0. *)
-  (* Anomaly *)
+  Check ## 0 0.
+  (* ## 0 0 *)
   Check p 0 0 (B:=bool).
   (* ## 0 0 (B:=bool) *)
-  Check ## 0 0 bool.
-  (* ## 0 0 (B:=bool) -- INCONSISTENT parsing/printing *)
+  Check ## 0 0 (B:=bool).
+  (* ## 0 0 (B:=bool) *)
   Check p 0 0 true.
-  (* ## 0 0 (B:=bool) true -- BUG B should not be displayed *)
-  Check ## 0 0 bool true.
-  (* ## 0 0 (B:=bool) true -- INCONSISTENCY parsing/printing + BUG B should not be displayed *)
+  (* ## 0 0 true *)
+  Check ## 0 0 true.
+  (* ## 0 0 true *)
 
   End AtNotationForPartialApplication.
 
 End AppliedTermsPrinting.
+
+Module AppliedPatternsPrinting.
+
+  (* Other tests testing inheritance of scope and implicit in
+     term and pattern for parsing and printing *)
+
+  Inductive T := p (a:nat) (b:bool) {B} (b:B) : T.
+  Notation "0" := true : bool_scope.
+
+  Module A.
+  Notation "#" := @p (at level 0).
+  Check # 0 0 _ true.
+  Check fun a => match a with # 0 0 _ _ => 1 | _ => 2 end. (* !! *)
+  End A.
+
+  Module B.
+  Notation "#'" := p (at level 0).
+  Check #' 0 0 true.
+  Check fun a => match a with #' 0 0 _ => 1 | _ => 2 end.
+  End B.
+
+  Module C.
+  Notation "## q" := (@p q) (at level 0, q at level 0).
+  Check ## 0 0 true.
+  Check fun a => match a with ## 0 0 _ => 1 | _ => 2 end.
+  End C.
+
+  Module D.
+  Notation "##' q" := (p q) (at level 0, q at level 0).
+  Check ##' 0 0 true.
+  Check fun a => match a with ##' 0 0 _ => 1 | _ => 2 end.
+  End D.
+
+  Module E.
+  Notation P := @ p.
+  Check P 0 0 _ true.
+  Check fun a => match a with P 0 0 _ _ => 1 | _ => 2 end.
+  End E.
+
+  Module F.
+  Notation P' := p.
+  Check P' 0 0 true.
+  Check fun a => match a with P' 0 0 _ => 1 | _ => 2 end.
+  End F.
+
+  Module G.
+  Notation Q q := (@p q).
+  Check Q 0 0 true.
+  Check fun a => match a with Q 0 0 _ => 1 | _ => 2 end.
+  End G.
+
+  Module H.
+  Notation Q' q := (p q).
+  Check Q' 0 0 true.
+  Check fun a => match a with Q' 0 0 _ => 1 | _ => 2 end.
+  End H.
+
+End AppliedPatternsPrinting.
diff --git a/test-suite/output/Record.v b/test-suite/output/Record.v
index d9a649fadc..71a8afa131 100644
--- a/test-suite/output/Record.v
+++ b/test-suite/output/Record.v
@@ -20,6 +20,8 @@ Check {| field := 5 |}.
 Check build_r 5.
 Check build_c 5.
 
+Set Printing Records.
+
 Record N := C { T : Type; _ : True }.
 Check fun x:N => let 'C _ p := x in p.
 Check fun x:N => let 'C T _ := x in T.
diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v
index b26e725d9b..f166a53256 100644
--- a/test-suite/success/Notations2.v
+++ b/test-suite/success/Notations2.v
@@ -7,21 +7,21 @@ The convention is:
 Constant foo with implicit arguments and scopes used in a term or a pattern:
 
        foo      do not deactivate further arguments and scopes
-       @foo     deactivates further arguments and scopes
-       (foo x)  deactivates further arguments and scopes
-       (@foo x) deactivates further arguments and scopes
+       @foo     deactivate further arguments and scopes
+       (foo x)  deactivate further arguments and scopes
+       (@foo x) deactivate further arguments and scopes
 
 Notations binding to foo:
 
 #   := foo      do not deactivate further arguments and scopes
-#   := @foo     deactivates further arguments and scopes
-# x := foo x    deactivates further arguments and scopes
-# x := @foo x   deactivates further arguments and scopes
+#   := @foo     deactivate further arguments and scopes
+# x := foo x    do not deactivate further arguments and scopes
+# x := @foo x   do not deactivate further arguments and scopes
 
 Abbreviations binding to foo:
 
 f   := foo      do not deactivate further arguments and scopes
-f   := @foo     deactivates further arguments and scopes
+f   := @foo     deactivate further arguments and scopes
 f x := foo x    do not deactivate further arguments and scopes
 f x := @foo x   do not deactivate further arguments and scopes
 *)
@@ -62,18 +62,18 @@ Check c4 _ 0%bool _ 0%bool 0%bool : prod' bool bool.
 Check fun A (x :prod' bool A) => match x with c4 _ 0%bool _ y 0%bool => 2 | _ => 1 end.
 Check fun A (x :prod' bool A) => match x with (@pair') _ 0%bool _ y 0%bool => 2 | _ => 1 end.
 
-(* 5. Notations stop further implicit arguments to be inserted and scopes to be used *)
+(* 5. Non-@id notations inherit implicit arguments to be inserted and scopes to be used *)
 Notation "# x" := (pair' x) (at level 0, x at level 1).
 Check pair' 0 0 0 : prod' bool bool.
-Check # 0 _ 0%bool 0%bool : prod' bool bool.
-Check fun A (x :prod' bool A) => match x with # 0 _ y 0%bool => 2 | _ => 1 end.
+Check # 0 0 0 : prod' bool bool.
+Check fun A (x :prod' bool A) => match x with # 0 y 0 => 2 | _ => 1 end.
 
-(* 6. Notations stop further implicit arguments to be inserted and scopes to be used *)
+(* 6. Non-@id notations inherit implicit arguments to be inserted and scopes to be used *)
 Notation "## x" := ((@pair') _ x) (at level 0, x at level 1).
 Check (@pair') _ 0%bool _ 0%bool 0%bool : prod' bool bool.
 Check ((@pair') _ 0%bool) _ 0%bool 0%bool : prod' bool bool.
-Check ## 0%bool _ 0%bool 0%bool : prod' bool bool.
-Check fun A (x :prod' bool A) => match x with ## 0%bool _ y 0%bool => 2 | _ => 1 end.
+Check ## 0%bool 0 0 : prod' bool bool.
+Check fun A (x :prod' bool A) => match x with ## 0%bool y 0 => 2 | _ => 1 end.
 
 (* 7. Notations stop further implicit arguments to be inserted and scopes to be used *)
 Notation "###" := (@pair') (at level 0).
@@ -86,10 +86,10 @@ Notation "####" := pair' (at level 0).
 Check #### 0 0 0 : prod' bool bool.
 Check fun A (x :prod' bool A) => match x with #### 0 y 0 => 2 | _ => 1 end.
 
-(* 9. Notations w/o @ but arguments do not preserve further implicit arguments and scopes *)
+(* 9. Non-@id notations inherit implicit arguments and scopes *)
 Notation "##### x" := (pair' x) (at level 0, x at level 1).
-Check ##### 0 _ 0%bool 0%bool : prod' bool bool.
-Check fun A (x :prod' bool A) => match x with ##### 0 _ y 0%bool => 2 | _ => 1 end.
+Check ##### 0 0 0 : prod' bool bool.
+Check fun A (x :prod' bool A) => match x with ##### 0 y 0 => 2 | _ => 1 end.
 
 (* 10. Check computation of binding variable through other notations *)
 (* it should be detected as binding variable and the scopes not being checked *)
@@ -185,3 +185,12 @@ Import A.
 Infix "+++" := Nat.add (at level 80).
 
 End M18.
+
+Module InheritanceArgumentScopes.
+
+Axiom p : forall (A:Type) (b:nat), A = A /\ b = b.
+Check fun A n => p (A * A) (n * n). (* safety check *)
+Notation q := @p.
+Check fun A n => q (A * A) (n * n). (* check that argument scopes are propagated *)
+
+End InheritanceArgumentScopes.