diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/Notations2.v | 110 |
1 files changed, 56 insertions, 54 deletions
diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v index ac41819f56..9505a56e3f 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. |