Adopting the same rules for interpreting @, abbreviations and

notations in patterns than in terms, wrt implicit arguments and
scopes.

See file Notations2.v for the conventions in use in terms.

Somehow this could be put in 8.5 since it puts in agreement the
interpretation of abbreviations and notations in "symmetric patterns"
to what is done in terms (even though the interpretation rules for
terms are a bit ad hoc).

There is one exception: in terms, "(foo args) args'" deactivates the
implicit arguments and scopes in args'. This is a bit complicated to
implement in patterns so the syntax is not supported (and anyway, this
convention is a bit questionable).

1 files changed, 56 insertions, 54 deletions

diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v
index ac41819f5..9505a56e3 100644
--- a/test-suite/success/Notations2.v
+++ b/test-suite/success/Notations2.v
@@ -1,40 +1,33 @@
 (* This file is giving some examples about how implicit arguments and
-   scopes are (inconsistently) treated when using abbreviations or
-   notations, in terms or patterns, or when using @ and parentheses in
-   terms and patterns *)
-
-(* One compromise would be that:
-   - Neither abbreviations nor notations break implicit arguments and
-     scopes unless the head constant is with @ and surrounded with parentheses.
-     + This would change 3. terms and patterns to behave like 4. terms,
-       with former behavior possible by using instead (@pair' _ x%nat)
-       or (pair' x%nat).
-     + This would change 4. patterns to behave like 4. terms, introducing the
-       possibibility to have the deactivation in patterns, as it is in terms,
-       by using (@pair').
-     + This would change 5. terms to behave like 5. patterns, introducing the
-       possibibility to have the activation behavior in terms, as it with
-       abbreviations, using either (@(pair') _ x%nat) or (pair' _ x).
-     + This would change 6. patterns to behave like 6. terms, introducing the
-       possibibility to have the deactivation behavior in patterns, as it with
-       abbreviations in terms, using either (@(pair') _ x%nat) or (pair' _ x).
-   - "(foo args)" directly in terms would still deactivation implicit
-     arguments and scopes for further arguments, as of today.
-   - "(@foo args)" directly in terms would deactivate implicit arguments and scopes
-     in args as of today, but not for further arguments, on the contrary of today
-   - "((@foo) args)" directly in terms would deactivate implicit
-     arguments and scopes in args and for further arguments, as it is today
-
-   Then, in both terms and patterns:
-   - "(@foo args)" in an abbreviation or notation would behave the same as
-     "(@foo args)" when expanded, i.e. with deactivation of implicit arguments
-     and scopes only for args, but not for further arguments.
-   - "((@foo) args)" in an abbreviation or notation would behave the same as
-     "((@foo) args)" when expanded, i.e. with deactivation of implicit arguments and scopes.
-   - "(foo args)" in an abbreviation or notation would behave the same as
-     "foo args" when expanded, i.e. with no change on implicit arguments and scopes.
+   scopes are treated when using abbreviations or notations, in terms
+   or patterns, or when using @ and parentheses in terms and patterns.
+
+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
+
+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
+
+Abbreviations binding to foo:
+
+f   := foo      do not deactivate further arguments and scopes
+f   := @foo     deactivates 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
 *)
 
+(* One checks that abbreviations and notations in patterns now behave like in terms *)
+
 Inductive prod' A : Type -> Type :=
 | pair' (a:A) B (b:B) (c:bool) : prod' A B.
 Arguments pair' [A] a%bool_scope [B] b%bool_scope c%bool_scope.
@@ -46,14 +39,13 @@ Check pair' 0 0 0 : prod' bool bool.
 Check (pair' 0) _ 0%bool 0%bool : prod' bool bool. (* parentheses are blocking implicit and scopes *)
 Check c1 0 0 0 : prod' bool bool.
 Check fun x : prod' bool bool => match x with c1 0 y 0 => 2 | _ => 1 end.
-Check fun x : prod' bool bool => match x with (pair' 0) y 0 => 2 | _ => 1 end. (* Inconsistent with terms *)
 
 (* 2. Abbreviations do not stop implicit arguments to be inserted and scopes to be used *)
 Notation c2 x := (@pair' _ x).
 Check (@pair' _ 0) _ 0%bool 0%bool : prod' bool bool. (* parentheses are blocking implicit and scopes *)
 Check c2 0 0 0 : prod' bool bool.
 Check fun A (x : prod' bool A) => match x with c2 0 y 0 => 2 | _ => 1 end.
-Check fun A (x : prod' bool A) => match x with (@pair' _ 0) y 0 => 2 | _ => 1 end. (* Inconsistent with terms *)
+Check fun A (x : prod' bool A) => match x with (@pair' _ 0) _ y 0%bool => 2 | _ => 1 end.
 
 (* 3. Abbreviations do not stop implicit arguments to be inserted and scopes to be used *)
 Notation c3 x := ((@pair') _ x).
@@ -61,30 +53,40 @@ Check (@pair') _ 0%bool _ 0%bool 0%bool : prod' bool bool. (* @ is blocking impl
 Check ((@pair') _ 0%bool) _ 0%bool 0%bool : prod' bool bool. (* parentheses and @ are blocking implicit and scopes *)
 Check c3 0 0 0 : prod' nat bool. (* First scope is blocked but not the last two scopes *)
 Check fun A (x :prod' nat A) => match x with c3 0 y 0 => 2 | _ => 1 end.
-(* Check fun A (x :prod' nat A) => match x with ((@pair') _ 0) y 0 => 2 | _ => 1 end.*)
 
 (* 4. Abbreviations do not stop implicit arguments to be inserted and scopes to be used *)
-(* unless an atomic @ is given, in terms but not in patterns *)
+(* unless an atomic @ is given *)
 Notation c4 := (@pair').
 Check (@pair') _ 0%bool _ 0%bool 0%bool : prod' bool bool.
-Check c4 _ 0 _ 0 0%bool : prod' nat nat. (* all 0 are in nat_scope: would there be incompatibilities to change that? *)
-Check fun A (x :prod' bool A) => match x with c4 _ 0 _ y 0 => 2 | _ => 1 end. (* Inconsistent with terms: both 0 are in bool_scope *)
-Check fun A (x :prod' nat A) => match x with (@pair') _ 0 y 0 => 2 | _ => 1 end. (* Inconsistent with terms: the implicit arguments and scopes are not deactivated *)
+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 *)
-(* in terms but not in patterns *)
-Notation "% x" := (pair' x) (at level 0, x at level 0).
+Notation "# x" := (pair' x) (at level 0, x at level 1).
 Check pair' 0 0 0 : prod' bool bool.
-Check % 0 _ 0 0%bool : prod' bool nat. (* last two 0 are in nat_scope *)
-Check fun A (x :prod' bool A) => match x with % 0 y 0 => 2 | _ => 1 end. (* Inconsistent with terms: both 0 are in bool_scope *)
-Check fun A (x :prod' bool A) => match x with pair' 0 y 0 => 2 | _ => 1 end.
+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.
 
 (* 6. Notations stop further implicit arguments to be inserted and scopes to be used *)
-(* in terms but not in patterns *)
-Notation "% x" := ((@pair') _ x%nat) (at level 0, x at level 0).
-Check (@pair') _ 0 _ 0%bool 0%bool : prod' nat bool.
-Check ((@pair') _ 0) _ 0%bool 0%bool : prod' nat bool.
-Check % 0 _ 0 0%bool : prod' nat nat. (* last two 0 are in nat_scope *)
-Check fun A (x :prod' nat A) => match x with % 0 y 0 => 2 | _ => 1 end. (* Inconsistent with terms: last 0 is in bool_scope, and implicit is not given *)
-Check fun A (x :prod' bool A) => match x with (@pair') 0 y 0 => 2 | _ => 1 end. (* inconsistent with terms: the implicit arguments and scopes are not deactivated *)
-Check fun A (x :prod' nat A) => match x with ((@pair') _) 0 y 0 => 2 | _ => 1 end.
+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.
+
+(* 7. Notations stop further implicit arguments to be inserted and scopes to be used *)
+Notation "###" := (@pair') (at level 0).
+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.
+
+(* 8. Notations w/o @ preserves implicit arguments and scopes *)
+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 *)
+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.