|
(**********************************************************************)
(* Check precedence, spacing, etc. in printing with curly brackets *)
Check {x|x=0}+{True/\False}+{forall x, x=0}.
(**********************************************************************)
(* Check printing of notations with several instances of a recursive pattern *)
(* Was wrong but I could not trigger a problem due to the collision between *)
(* different instances of ".." *)
Notation "[< x , y , .. , z >]" := (pair (.. (pair x y) ..) z,pair y ( .. (pair z x) ..)).
Check [<0,2>].
Check ((0,2),(2,0)).
Check ((0,2),(2,2)).
Unset Printing Notations.
Check [<0,2>].
Set Printing Notations.
Notation "<< x , y , .. , z >>" := ((.. (x,y) .., z),(z, .. (y,x) ..)).
Check <<0,2,4>>.
Check (((0,2),4),(4,(2,0))).
Check (((0,2),4),(2,(2,0))).
Check (((0,2),4),(0,(2,4))).
Unset Printing Notations.
Check <<0,2,4>>.
Set Printing Notations.
(**********************************************************************)
(* Check notations with recursive notations both in binders and terms *)
Notation "'ETA' x .. y , f" :=
(fun x => .. (fun y => (.. (f x) ..) y ) ..)
(at level 200, x binder, y binder).
Check ETA (x:nat) (y:nat), Nat.add.
Check ETA (x y:nat), Nat.add.
Check ETA x y, Nat.add.
Unset Printing Notations.
Check ETA (x:nat) (y:nat), Nat.add.
Set Printing Notations.
Check ETA x y, le_S.
Notation "'CURRY' x .. y , f" := (fun x => .. (fun y => f (x, .. (y,tt) ..)) ..)
(at level 200, x binder, y binder).
Check fun f => CURRY (x:nat) (y:bool), f.
Notation "'CURRYINV' x .. y , f" := (fun x => .. (fun y => f (y, .. (x,tt) ..)) ..)
(at level 200, x binder, y binder).
Check fun f => CURRYINV (x:nat) (y:bool), f.
Notation "'CURRYLEFT' x .. y , f" := (fun x => .. (fun y => f (.. (tt,x) .., y)) ..)
(at level 200, x binder, y binder).
Check fun f => CURRYLEFT (x:nat) (y:bool), f.
Notation "'CURRYINVLEFT' x .. y , f" := (fun x => .. (fun y => f (.. (tt,y) .., x)) ..)
(at level 200, x binder, y binder).
Check fun f => CURRYINVLEFT (x:nat) (y:bool), f.
(**********************************************************************)
(* Notations with variables bound both as a term and as a binder *)
(* This is #4592 *)
Notation "{# x | P }" := (ex2 (fun y => x = y) (fun x => P)).
Check forall n:nat, {# n | 1 > n}.
Parameter foo : forall {T}(x : T)(P : T -> Prop), Prop.
Notation "{| x | P |}" := (foo x (fun x => P)).
Check forall x:nat, {| x | x > 0 |}.
Check ex2 (fun x => x=1) (fun x0 => x0=2).
(* Other tests about alpha-conversions: the following notation
contains all three kinds of bindings:
- x is bound in the lhs as a term and a binder: its name is forced
by its position as a term; it can bind variables in P
- y is bound in the lhs as a binder only: its name is given by its
name as a binder in the term to display; it can bind variables in P
- z is a binder local to the rhs; it cannot bind a variable in P
*)
Parameter foo2 : forall {T}(x : T)(P : T -> T -> T -> Prop), Prop.
Notation "{| x , y | P |}_2" := (foo2 x (fun x y z => P z y x)).
(* Not printable: z (resp c, n) occurs in P *)
Check fun n => foo2 n (fun x y z => (fun _ _ _ => x+y+z=0) z y x).
Check fun n => foo2 n (fun a b c => (fun _ _ _ => a+b+c=0) c b a).
Check fun n => foo2 n (fun n y z => (fun _ _ _ => n+y+z=0) z y n).
Check fun n => foo2 n (fun x n z => (fun _ _ _ => x+n+z=0) z n x).
Check fun n => foo2 n (fun x y n => (fun _ _ _ => x+y+n=0) n y x).
(* Printable *)
Check fun n => foo2 n (fun x y z => (fun _ _ _ => x+y=0) z y x).
Check fun n => foo2 n (fun n y z => (fun _ _ _ => n+y=0) z y n).
Check fun n => foo2 n (fun x n z => (fun _ _ _ => x+n=0) z n x).
(* Not printable: renaming x into n would bind the 2nd occurrence of n *)
Check fun n => foo2 n (fun x y z => (fun _ _ _ => x+y+n=0) z y x).
Check fun n => foo2 n (fun x y z => (fun _ _ _ => x+y+n=0) z y x).
(* Other tests *)
Parameter foo3 : forall {T}(x : T)(P : T -> T -> T -> Prop), Prop.
Notation "{| x , P |}_3" := (foo3 x (fun x x x => P x)).
(* Printable *)
Check fun n : nat => foo3 n (fun x y z => (fun _ => 0=0) z).
Check fun n => foo3 n (fun x y z => (fun _ => z=0) z).
(* Not printable: renaming z in n would hide the renaming of x into n *)
Check fun n => foo3 n (fun x y z => (fun _ => x=0) z).
(* Other tests *)
Parameter foo4 : forall {T}(x : T)(P : T -> T -> T -> Prop), Prop.
Notation "{| x , P |}_4" := (foo4 x (fun x _ z => P z)).
(* Printable *)
Check fun n : nat => foo4 n (fun x y z => (fun _ => 0=0) z).
Check fun n => foo4 n (fun x y z => (fun _ => x=0) z).
(* Not printable: y, z not allowed to occur in P *)
Check fun n => foo4 n (fun x y z => (fun _ => z=0) z).
Check fun n => foo4 n (fun x y z => (fun _ => y=0) z).
(**********************************************************************)
(* Test printing of #4932 *)
Inductive ftele : Type :=
| fb {T:Type} : T -> ftele
| fr {T} : (T -> ftele) -> ftele.
Fixpoint args ftele : Type :=
match ftele with
| fb _ => unit
| fr f => sigT (fun t => args (f t))
end.
Definition fpack := sigT args.
Definition pack fp fa : fpack := existT _ fp fa.
Notation "'tele' x .. z := b" :=
(fun x => .. (fun z =>
pack (fr (fun x => .. ( fr (fun z => fb b) ) .. ) )
(existT _ x .. (existT _ z tt) .. )
) ..)
(at level 85, x binder, z binder).
Check tele (t:Type) '((y,z):nat*nat) (x:t) := tt.
(* Checking that "fun" in a notation does not mixed up with the
detection of a recursive binder *)
Notation "[ x ;; .. ;; y ]" := ((x,((fun u => S u), .. (y,(fun u => S u,fun v:nat => v)) ..))).
Check [ fun x => x+0 ;; fun x => x+1 ;; fun x => x+2 ].
(* Cyprien's part of bug #4765 *)
Section Bug4765.
Notation foo5 x T y := (fun x : T => y).
Check foo5 x nat x.
End Bug4765.
(**********************************************************************)
(* Test printing of #5526 *)
Notation "x === x" := (eq_refl x) (only printing, at level 10).
Check (fun x => eq_refl x).
(* Test recursive notations with the recursive pattern repeated on the right *)
Notation "{{ x , .. , y , z }}" := (pair x .. (pair y z) ..).
Check {{0,1}}.
Check {{0,1,2}}.
Check {{0,1,2,3}}.
(* Test printing of #5608 *)
Reserved Notation "'letpair' x [1] = { A } ; 'return' ( b0 , b1 , .. , b2 )"
(at level 200, format "'letpair' x [1] = { A } ; '//' 'return' ( b0 , b1 , .. , b2 )").
Notation "'letpair' x [1] = { a } ; 'return' ( b0 , b1 , .. , b2 )" :=
(let x:=a in ( .. (b0,b1) .., b2)).
Check letpair x [1] = {0}; return (1,2,3,4).
(* Test spacing in #5569 *)
Notation "{ { xL | xR // xcut } }" := (xL+xR+xcut)
(at level 0, xR at level 39, format "{ { xL | xR // xcut } }").
Check 1+1+1.
(* Test presence of notation variables in the recursive parts (introduced in dfdaf4de) *)
Notation "!!! x .. y , b" := ((fun x => b), .. ((fun y => b), True) ..) (at level 200, x binder).
Check !!! (x y:nat), True.
(* Allow level for leftmost nonterminal when printing-only, BZ#5739 *)
Notation "* x" := (id x) (only printing, at level 15, format "* x").
Notation "x . y" := (x + y) (only printing, at level 20, x at level 14, left associativity, format "x . y").
Check (((id 1) + 2) + 3).
Check (id (1 + 2)).
(* Test contraction of "forall x, let 'pat := x in ..." into "forall 'pat, ..." *)
(* for isolated "forall" (was not working already in 8.6) *)
Notation "! x .. y , A" := (id (forall x, .. (id (forall y, A)) .. )) (at level 200, x binder).
Check ! '(x,y), x+y=0.
(* Check that the terminator of a recursive pattern is interpreted in
the correct environment of bindings *)
Notation "'exists_mixed' x .. y , P" := (ex (fun x => forall z:nat, .. (ex (fun y => forall z:nat, z=0 /\ P)) ..)) (at level 200, x binder).
Check exists_mixed x y '(u,t), x+y=0/\u+t=0.
Check exists_mixed x y '(z,t), x+y=0/\z+t=0.
(* Check that intermediary let-in are inserted in between instances of
the repeated pattern *)
Notation "'exists_true' x .. y , P" := (exists x, True /\ .. (exists y, True /\ P) ..) (at level 200, x binder).
Check exists_true '(x,y) (u:=0) '(z,t), x+y=0/\z+t=0.
(* Check that generalized binders are correctly interpreted *)
Module G.
Generalizable Variables A R.
Class Reflexive {A:Type} (R : A->A->Prop) := reflexivity : forall x : A, R x x.
Check exists_true `{Reflexive A R}, forall x, R x x.
Check exists_true x `{Reflexive A R} y, x+y=0 -> forall z, R z z.
End G.
(* Allows recursive patterns for binders to be associative on the left *)
Notation "!! x .. y # A #" := (.. (A,(forall x, True)) ..,(forall y, True)) (at level 200, x binder).
Check !! a b : nat # True #.
(* Examples where the recursive pattern refer several times to the recursive variable *)
Notation "{{D x , .. , y }}" := ((x,x), .. ((y,y),(0,0)) ..).
Check {{D 1, 2 }}.
Notation "! x .. y # A #" :=
((forall x, x=x), .. ((forall y, y=y), A) ..)
(at level 200, x binder).
Check ! a b : nat # True #.
Notation "!!!! x .. y # A #" :=
(((forall x, x=x),(forall x, x=0)), .. (((forall y, y=y),(forall y, y=0)), A) ..)
(at level 200, x binder).
Check !!!! a b : nat # True #.
Notation "@@ x .. y # A # B #" :=
((forall x, .. (forall y, A) ..), (forall x, .. (forall y, B) ..))
(at level 200, x binder).
Check @@ a b : nat # a=b # b=a #.
Notation "'exists_non_null' x .. y , P" :=
(ex (fun x => x <> 0 /\ .. (ex (fun y => y <> 0 /\ P)) ..))
(at level 200, x binder).
Check exists_non_null x y z t , x=y/\z=t.
Notation "'forall_non_null' x .. y , P" :=
(forall x, x <> 0 -> .. (forall y, y <> 0 -> P) ..)
(at level 200, x binder).
Check forall_non_null x y z t , x=y/\z=t.
(* Examples where the recursive pattern is in reverse order *)
Notation "{{RL c , .. , d }}" := (pair d .. (pair c 0) ..).
Check {{RL 1 , 2}}.
Notation "{{RR c , .. , d }}" := (pair .. (pair 0 d) .. c).
Check {{RR 1 , 2}}.
Set Printing All.
Check {{RL 1 , 2}}.
Check {{RR 1 , 2}}.
Unset Printing All.
Notation "{{RLRR c , .. , d }}" := (pair d .. (pair c 0) .., pair .. (pair 0 d) .. c, pair c .. (pair d 0) .., pair .. (pair 0 c) .. d).
Check {{RLRR 1 , 2}}.
Unset Printing Notations.
Check {{RLRR 1 , 2}}.
Set Printing Notations.
(* Check insensitivity of "match" clauses to order *)
Module IfPat.
Notation "'if' t 'is' n .+ 1 'then' p 'else' q" :=
(match t with S n => p | 0 => q end)
(at level 200).
Check fun x => if x is n.+1 then n else 1.
End IfPat.
(* Examples with binding patterns *)
Check {'(x,y)|x+y=0}.
Module D.
Notation "'exists2'' x , p & q" := (ex2 (fun x => p) (fun x => q))
(at level 200, x pattern, p at level 200, right associativity,
format "'[' 'exists2'' '/ ' x , '/ ' '[' p & '/' q ']' ']'")
: type_scope.
Check exists2' (x,y), x=0 & y=0.
End D.
(* Ensuring for reparsability that printer of notations does not use a
pattern where only an ident could be reparsed *)
Module E.
Inductive myex2 {A:Type} (P Q:A -> Prop) : Prop :=
myex_intro2 : forall x:A, P x -> Q x -> myex2 P Q.
Notation "'myexists2' x : A , p & q" := (myex2 (A:=A) (fun x => p) (fun x => q))
(at level 200, x ident, A at level 200, p at level 200, right associativity,
format "'[' 'myexists2' '/ ' x : A , '/ ' '[' p & '/' q ']' ']'")
: type_scope.
Check myex2 (fun x => let '(y,z) := x in y>z) (fun x => let '(y,z) := x in z>y).
End E.
(* A canonical example of a notation with a non-recursive binder *)
Parameter myex : forall {A}, (A -> Prop) -> Prop.
Notation "'myexists' x , p" := (myex (fun x => p))
(at level 200, x pattern, p at level 200, right associativity).
(* A canonical example of a notation with recursive binders *)
Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..)
(at level 200, x binder, y binder, right associativity) : type_scope.
(* Check that printing 'pat uses an "as" when the variable bound to
the pattern is dependent. We check it for the three kinds of
notations involving bindings of patterns *)
Check fun '((x,y) as z) => x+y=0/\z=z. (* Primitive fun/forall *)
Check myexists ((x,y) as z), x+y=0/\z=z. (* Isolated binding pattern *)
Check exists '((x,y) as z), x+y=0/\z=z. (* Applicative recursive binder *)
Check ∀ '((x,y) as z), x+y=0/\z=z. (* Other example of recursive binder, now treated as the exists case *)
(* Check parsability and printability of irrefutable disjunctive patterns *)
Check fun '(((x,y),true)|((x,y),false)) => x+y.
Check myexists (((x,y),true)|((x,y),false)), x>y.
Check exists '(((x,y),true)|((x,y),false)), x>y.
Check ∀ '(((x,y),true)|((x,y),false)), x>y.
(* Check Georges' printability of a "if is then else" notation *)
Module IfPat2.
Notation "'if' c 'is' p 'then' u 'else' v" :=
(match c with p => u | _ => v end)
(at level 200, p pattern at level 100).
Check fun p => if p is S n then n else 0.
Check fun p => if p is Lt then 1 else 0.
End IfPat2.
(* Check that mixed binders and terms defaults to ident and not pattern *)
Module F.
(* First without an indirection *)
Notation "[ n | t ]" := (n, (fun n : nat => t)).
Check fun S : nat => [ S | S+S ].
Check fun N : nat => (N, (fun n => n+0)). (* another test in passing *)
(* Then with an indirection *)
Notation "[[ n | p | t ]]" := (n, (fun p : nat => t)).
Notation "[[ n | t ]]" := [[ n | n | t ]].
Check fun S : nat => [[ S | S+S ]].
End F.
(* Check parsability/printability of {x|P} and variants *)
Check {I:nat|I=I}.
Check {'I:True|I=I}.
Check {'(x,y)|x+y=0}.
(* Check exists2 with a pattern *)
Check ex2 (fun x => let '(y,z) := x in y>z) (fun x => let '(y,z) := x in z>y).
Module Issue7110.
Open Scope list_scope.
Notation "[ :: x1 , x2 , .. , xn & s ]" := (x1 :: x2 :: .. (xn :: s) ..)
(at level 0).
Definition foo (l : list nat) :=
match l with
| a :: (b :: l) as l1 => l1
| _ => l
end.
Print foo.
End Issue7110.
Module LocateNotations.
Locate "exists".
Locate "( _ , _ , .. , _ )".
End LocateNotations.
Module Issue7731.
Axiom (P : nat -> Prop).
Parameter (X : nat).
Notation "## @ E ^^^" := (P E) (at level 20, E at level 1, format "'[ ' ## '/' @ E '/' ^^^ ']'").
Notation "%" := X.
Set Printing Width 7.
Goal ## @ % ^^^.
Show.
Abort.
End Issue7731.
Module Issue8126.
Definition myfoo (x : nat) (y : nat) (z : unit) := y.
Notation myfoo0 := (@myfoo 0).
Notation myfoo01 := (@myfoo0 1).
Check myfoo 0 1 tt. (* was printing [myfoo0 1 HI], but should print [myfoo01 HI] *)
Check myfoo0 1 tt. (* was printing [myfoo0 1 HI], but should print [myfoo01 HI] *)
Check myfoo01 tt. (* was printing [myfoo0 1 HI], but should print [myfoo01 HI] *)
End Issue8126.
¤ Dauer der Verarbeitung: 0.21 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
