From 6bd55e5c17463d3868becba4064dba46c95c4028 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Fri, 28 Mar 2008 20:22:43 +0000
Subject: - Second pass on implementation of let pattern. Parse "let ' par [as
 x]?   [in I] := t [return pred] in b", just as SSReflect does with let:.  
 Change implementation: no longer a separate AST node, just add a case_style  
 annotation on Cases to indicate it (if ML was dependently typed we   could
 ensure that LetPatternStyle Cases have only one term to be   matched and one
 branch, alas...). This factors out most code and we lose   no functionality
 (win ! win !). Add LetPat.v test suite.

- Slight improvement of inference of return clauses for dependent
  pattern matching. If matching a variable of non-dependent type
  under a tycon that mentions it while giving no return clause, the
  dependency will be automatically infered. Examples at the end of
  DepPat. Should get rid of most explicit returns under tycons.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10727 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/success/LetPat.v | 55 +++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 55 insertions(+)
 create mode 100644 test-suite/success/LetPat.v

(limited to 'test-suite')

diff --git a/test-suite/success/LetPat.v b/test-suite/success/LetPat.v
new file mode 100644
index 0000000000..72c7cc1553
--- /dev/null
+++ b/test-suite/success/LetPat.v
@@ -0,0 +1,55 @@
+(* Simple let-patterns *)
+Variable A B : Type.
+
+Definition l1 (t : A * B * B) : A := let '(x, y, z) := t in x.
+Print l1.
+Definition l2 (t : (A * B) * B) : A := let '((x, y), z) := t in x.
+Definition l3 (t : A * (B * B)) : A := let '(x, (y, z)) := t in x.
+Print l3.
+
+Record someT (A : Type) := mkT { a : nat; b: A }.
+
+Definition l4 A (t : someT A) : nat := let 'mkT x y := t in x.
+Print l4.
+Print sigT.
+
+Definition l5 A (B : A -> Type) (t : sigT B) : B (projT1 t) := 
+  let 'existT x y := t return B (projT1 t) in y.
+
+Definition l6 A (B : A -> Type) (t : sigT B) : B (projT1 t) := 
+  let 'existT x y as t' := t return B (projT1 t') in y.
+
+Definition l7 A (B : A -> Type) (t : sigT B) : B (projT1 t) := 
+  let 'existT x y as t' in sigT _ := t return B (projT1 t') in y.
+
+Definition l8 A (B : A -> Type) (t : sigT B) : B (projT1 t) := 
+  match t with
+    existT x y => y
+  end.
+
+(** An example from algebra, using let' and inference of return clauses
+   to deconstruct contexts. *)
+
+Record a_category (A : Type) (hom : A -> A -> Type) := {  }.
+
+Definition category := { A : Type & { hom : A -> A -> Type & a_category A hom } }.
+
+Record a_functor (A : Type) (hom : A -> A -> Type) (C : a_category A hom) := {  }.
+
+Notation " x :& y " := (@existT _ _ x y) (right associativity, at level 55) : core_scope.
+
+Definition functor (c d : category) :=
+  let ' A :& homA :& CA := c in
+  let ' B :& homB :& CB := d in
+    A -> B.
+
+Definition identity_functor (c : category) : functor c c :=
+  let 'A :& homA :& CA := c in
+    fun x => x.
+
+Definition functor_composition (a b c : category) : functor a b -> functor b c -> functor a c := 
+  let ' (A :& homA :& CA) := a in
+  let ' (B :& homB :& CB) := b in
+  let ' (C :& homB :& CB) := c in
+    fun f g => 
+      fun x : A => g (f x).
-- 
cgit v1.2.3