Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Notations2.v Sprache: Coq

Original von: Coq^©

(* This file is giving some examples about how implicit arguments and
   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.
Notation "0" := true : bool_scope.

(* 1. Abbreviations do not stop implicit arguments to be inserted and scopes to be used *)
Notation c1 x := (pair' x).
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.

(* 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%bool => 2 | _ => 1 end.

(* 3. Abbreviations do not stop implicit arguments to be inserted and scopes to be used *)
Notation c3 x := ((@pair') _ x).
Check (@pair') _ 0%bool _ 0%bool 0%bool : prod' bool bool. (* @ is blocking implicit and scopes *)
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.

(* 4. Abbreviations do not stop implicit arguments to be inserted and scopes to be used *)
(* unless an atomic @ is given *)
Notation c4 := (@pair').
Check (@pair') _ 0%bool _ 0%bool 0%bool : prod' bool bool.
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 *)
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.

(* 6. Notations stop further 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.

(* 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.

(* 10. Check computation of binding variable through other notations *)
(* it should be detected as binding variable and the scopes not being checked *)
Notation "'FUNNAT' i => t" := (fun i : nat => i = t) (at level 200).
Notation "'Funnat' i => t" := (FUNNAT i => t + i%nat) (at level 200).

(* 11. Notations with needed factorization of a recursive pattern *)
(* See https://github.com/coq/coq/issues/6078#issuecomment-342287412 *)
Module M11.
Notation "[:: x1 ; .. ; xn & s ]" := (cons x1 .. (cons xn s) ..).
Notation "[:: x1 ; .. ; xn ]" := (cons x1 .. (cons xn nil) ..).
Check [:: 1 ; 2 ; 3 ].
Check [:: 1 ; 2 ; 3 & nil ]. (* was failing *)
End M11.

(* 12. Preventively check that a variable which does not occur can be instantiated *)
(* by any term. In particular, it should not be restricted to a binder *)
Module M12.
Notation "N ++ x" := (S x) (only parsing).
Check 2 ++ 0.
End M12.

(* 13. Check that internal data about associativity are not used in comparing levels *)
Module M13.
Notation "x ;; z" := (x + z)
  (at level 100, z at level 200, only parsing, right associativity).
Notation "x ;; z" := (x * z)
  (at level 100, z at level 200, only parsing) : foo_scope.
End M13.

(* 14. Check that a notation with a "ident" binder does not include a pattern *)
Module M14.
Notation "'myexists' x , p" := (ex (fun x => p))
  (at level 200, x ident, p at level 200, right associativity) : type_scope.
Check myexists I, I = 0. (* Should not be seen as a constructor *)
End M14.

(* 15. Testing different ways to give the same levels without failing *)

Module M15.
  Local Notation "###### x" := (S x) (right associativity, at level 79, x at next level).
  Fail Local Notation "###### x" := (S x) (right associativity, at level 79).
  Local Notation "###### x" := (S x) (at level 79).
End M15.

(* 16. Some test about custom entries *)
Module M16.
  (* Test locality *)
  Local Declare Custom Entry foo.
  Fail Notation "#" := 0 (in custom foo). (* Should be local *)
  Local Notation "#" := 0 (in custom foo).

  (* Test import *)
  Module A.
  Declare Custom Entry foo2.
  End A.
  Fail Notation "##" := 0 (in custom foo2).
  Import A.
  Local Notation "##" := 0 (in custom foo2).

  (* Test Print Grammar *)
  Print Custom Grammar foo.
  Print Custom Grammar foo2.
End M16.

(* Example showing the need for strong evaluation of
   cases_pattern_of_glob_constr (this used to raise Not_found at some
   time) *)

Module M17.

Notation "# x ## t & u" := ((fun x => (x,t)),(fun x => (x,u))) (at level 0, x pattern).
Check fun y : nat => # (x,z) ## y & y.

End M17.

¤ Dauer der Verarbeitung: 0.18 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.