Merge branch 'funpattern-tests' into trunk.

Was PR#225: Patterns-in-binder syntax tests.

3 files changed, 152 insertions, 0 deletions

diff --git a/test-suite/output/PatternsInBinders.out b/test-suite/output/PatternsInBinders.out
new file mode 100644
index 000000000..6a28475d7
--- /dev/null
+++ b/test-suite/output/PatternsInBinders.out
@@ -0,0 +1,31 @@
+swap = fun '(x, y) => (y, x)
+     : A * B -> B * A
+fun '(x, y) => (y, x)
+     : A * B -> B * A
+forall '(x, y), swap (x, y) = (y, x)
+     : Prop
+proj_informative = fun 'exist _ x _ => x : A
+     : {x : A | P x} -> A
+foo = fun 'Bar n b tt p => if b then n + p else n - p
+     : Foo -> nat
+baz = 
+fun 'Bar n1 _ tt p1 => fun 'Bar _ _ tt _ => n1 + p1
+     : Foo -> Foo -> nat
+λ '(x, y), (y, x)
+     : A * B → B * A
+∀ '(x, y), swap (x, y) = (y, x)
+     : Prop
+swap = 
+fun (A B : Type) (pat : A * B) => let '(x, y) := pat in (y, x)
+     : forall A B : Type, A * B -> B * A
+
+Arguments A, B are implicit and maximally inserted
+Argument scopes are [type_scope type_scope _]
+forall (A B : Type) (pat : A * B), let '(x, y) := pat in swap (x, y) = (y, x)
+     : Prop
+exists pat : A * A, let '(x, y) := pat in swap (x, y) = (y, x)
+     : Prop
+both_z = 
+fun pat : nat * nat =>
+let '(n, p) as pat0 := pat return (F pat0) in (Z n, Z p) : F (n, p)
+     : forall pat : nat * nat, F pat
diff --git a/test-suite/output/PatternsInBinders.v b/test-suite/output/PatternsInBinders.v
new file mode 100644
index 000000000..8911909ab
--- /dev/null
+++ b/test-suite/output/PatternsInBinders.v
@@ -0,0 +1,54 @@
+(** The purpose of this file is to test printing of the destructive
+    patterns used in binders ([fun] and [forall]). *)
+
+Parameters (A B : Type) (P:A->Prop).
+
+Definition swap '((x,y) : A*B) := (y,x).
+Print swap.
+
+Check fun '((x,y) : A*B) => (y,x).
+
+Check forall '(x,y), swap (x,y) = (y,x).
+
+Definition proj_informative '(exist _ x _ : { x:A | P x }) : A := x.
+Print proj_informative.
+
+Inductive Foo := Bar : nat -> bool -> unit -> nat -> Foo.
+Definition foo '(Bar n b tt p) :=
+  if b then n+p else n-p.
+Print foo.
+
+Definition baz '(Bar n1 b1 tt p1) '(Bar n2 b2 tt p2) := n1+p1.
+Print baz.
+
+(** Some test involving unicode noations. *)
+Module WithUnicode.
+
+  Require Import Coq.Unicode.Utf8.
+
+  Check λ '((x,y) : A*B),  (y,x).
+  Check ∀ '(x,y), swap (x,y) = (y,x).
+
+End WithUnicode.
+
+
+(** * Suboptimal printing *)
+
+(** These tests show examples which expose the [let] introduced by
+    the pattern notation in binders. *)
+
+Module Suboptimal.
+
+Definition swap {A B} '((x,y) : A*B) := (y,x).
+Print swap.
+
+Check forall (A B:Type) '((x,y) : A*B), swap (x,y) = (y,x).
+
+Check exists '((x,y):A*A), swap (x,y) = (y,x).
+
+Inductive Fin (n:nat) := Z : Fin n.
+Definition F '(n,p) : Type := (Fin n * Fin p)%type.
+Definition both_z '(n,p) : F (n,p) := (Z _,Z _).
+Print both_z.
+
+End Suboptimal.
diff --git a/test-suite/success/PatternsInBinders.v b/test-suite/success/PatternsInBinders.v
new file mode 100644
index 000000000..777107915
--- /dev/null
+++ b/test-suite/success/PatternsInBinders.v
@@ -0,0 +1,67 @@
+(** The purpose of this file is to test functional properties of the
+    destructive patterns used in binders ([fun] and [forall]). *)
+
+
+Definition swap {A B} '((x,y) : A*B) := (y,x).
+
+(** Tests the use of patterns in [fun] and [Definition] *)
+Section TestFun.
+
+  Variables A B : Type.
+
+  Goal forall (x:A) (y:B), swap (x,y) = (y,x).
+  Proof. reflexivity. Qed.
+
+  Goal forall u:A*B, swap (swap u) = u.
+  Proof. destruct u. reflexivity. Qed.
+
+  Goal @swap A B = fun '(x,y) => (y,x).
+  Proof. reflexivity. Qed.
+
+End TestFun.
+
+
+(** Tests the use of patterns in [forall] *)
+Section TestForall.
+
+  Variables A B : Type.
+
+  Goal forall '((x,y) : A*B), swap (x,y) = (y,x).
+  Proof. intros [x y]. reflexivity. Qed.
+
+  Goal forall x0:A, exists '((x,y) : A*A), swap (x,y) = (x,y).
+  Proof.
+    intros x0.
+    exists (x0,x0).
+    reflexivity.
+  Qed.
+
+End TestForall.
+
+
+
+(** Tests the use of patterns in dependent definitions. *)
+
+Section TestDependent.
+
+  Inductive Fin (n:nat) := Z : Fin n.
+
+  Definition F '(n,p) : Type := (Fin n * Fin p)%type.
+
+  Definition both_z '(n,p) : F (n,p) := (Z _,Z _).
+
+End TestDependent.
+
+
+(** Tests with a few other types just to make sure parsing is
+    robust. *)
+Section TestExtra.
+
+  Definition proj_informative {A P} '(exist _ x _ : { x:A | P x }) : A := x.
+
+  Inductive Foo := Bar : nat -> bool -> unit -> nat -> Foo.
+
+  Definition foo '(Bar n b tt p) :=
+    if b then n+p else n-p.
+
+End TestExtra.