← Back to branch summary

~ubuntu-branches/ubuntu/wily/agda/wily-proposed

« back to all changes in this revision

Viewing changes to test/succeed/RecordPatternMatching.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 06:38:12 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805063812-io8e77niomivhd49
Tags: 2.4.0.2-1
* [6e140ac] Imported Upstream version 2.4.0.2
* [2049fc8] Update Build-Depends to match control
* [93dc4d4] Install the new primitives
* [e48f40f] Fix typo dev→doc

Show diffs side-by-side

added added

removed removed

Lines of Context:
test/succeed/RecordPatternMatching.agda
1
 
module RecordPatternMatching where
2
 
 
3
 
 
4
 
record Σ (A : Set) (B : A → Set) : Set where
5
 
  constructor _,_
6
 
  field
7
 
    proj₁ : A
8
 
    proj₂ : B proj₁
9
 
 
10
 
open Σ
11
 
 
12
 
_×_ : Set → Set → Set
13
 
A × B = Σ A λ _ → B
14
 
 
15
 
 
16
 
curry : ∀ {A : Set} {B : A → Set} {C : Σ A B → Set} →
17
 
        ((p : Σ A B) → C p) →
18
 
        ((x : A) → (y : B x) → C (x , y))
19
 
curry f x y = f (x , y)
20
 
 
21
 
uncurry : ∀ {A : Set} {B : A → Set} {C : Σ A B → Set} →
22
 
          ((x : A) → (y : B x) → C (x , y)) →
23
 
          ((p : Σ A B) → C p)
24
 
uncurry f (x , y) = f x y
25
 
 
26
 
 
27
 
data _≡_ {A : Set} (x : A) : A → Set where
28
 
  refl : x ≡ x
29
 
 
30
 
curry∘uncurry : ∀ {A : Set} {B : A → Set} {C : Σ A B → Set} →
31
 
                (f : (x : A) → (y : B x) → C (x , y)) →
32
 
                (x : A) → (y : B x) →
33
 
                curry {C = C} (uncurry f) x y ≡ f x y
34
 
curry∘uncurry f x y = refl
35
 
 
36
 
uncurry∘curry : ∀ {A : Set} {B : A → Set} {C : Σ A B → Set} →
37
 
                (f : (p : Σ A B) → C p) →
38
 
                (p : Σ A B) →
39
 
                uncurry {C = C} (curry f) p ≡ f p
40
 
uncurry∘curry f p = refl
41
 
 
42
 
 
43
 
to : {A B C : Set} → A × (B × C) → (A × B) × C
44
 
to (x , (y , z)) = ((x , y) , z)
45
 
 
46
 
from : {A B C : Set} → (A × B) × C → A × (B × C)
47
 
from ((x , y) , z) = (x , (y , z))
48
 
 
49
 
from∘to : {A B C : Set} (p : A × (B × C)) → from (to p) ≡ p
50
 
from∘to p = refl
51
 
 
52
 
data Bool : Set where
53
 
  true false : Bool
54
 
 
55
 
data ⊥ : Set where
56
 
 
57
 
F : Bool → Set
58
 
F true  = Bool
59
 
F false = ⊥
60
 
 
61
 
foo : Σ Bool F → Bool
62
 
foo (true  , b)  = b
63
 
foo (false , ())
64
 
 
65
 
bar : ∀ p → F (foo p) → F (foo p)
66
 
bar (true  , true)  = λ b → b
67
 
bar (true  , false) = λ ()
68
 
bar (false , ())
69
 
 
70
 
baz : (Σ Bool λ _ → Σ Bool λ _ → Bool) → Bool
71
 
baz (true  , (b , c)) = b
72
 
baz (false , (b , c)) = c
73
 
 
74
 
lemma : ∀ p → baz (false , p) ≡ proj₂ p
75
 
lemma p = refl
76
 
 
77
 
data ℕ : Set where
78
 
  zero : ℕ
79
 
  suc  : ℕ → ℕ
80
 
 
81
 
add : ℕ × ℕ → ℕ
82
 
add (zero  , n) = n
83
 
add (suc m , n) = suc (add (m , n))
84
 
 
85
 
 
86
 
data Unit : Set where
87
 
  unit : Unit
88
 
 
89
 
B : Set
90
 
B = Σ Unit λ _ → Unit
91
 
 
92
 
C : B → Set₁
93
 
C (_ , _) = Set
94
 
 
95
 
 
96
 
data P : ⊥ → ⊥ → Set where
97
 
  p : (x y : ⊥) → P x y
98
 
 
99
 
Bar : (x : ⊥) → P x x → P x x → Set₁
100
 
Bar .x _ (p x .x) = Set
101
 
 
102
 
 
103
 
G : (Σ ⊥ λ x → Σ ⊥ λ y → x ≡ y) → Set₁
104
 
G (x , (.x , refl)) = Set
105
 
 
106
 
 
107
 
Foo : (p₁ p₂ : B) → proj₁ p₁ ≡ proj₁ p₂ → Unit
108
 
Foo (x , y) (.x , y′) refl = unit
109
 
 
110
 
Foo-eval : (p : B) → Foo p p refl ≡ unit
111
 
Foo-eval _ = refl
112
 
 
113
 
 
114
 
D : (p₁ p₂ : B) → proj₁ p₁ ≡ proj₁ p₂ → Set₁
115
 
D (x , y) (.x , unit) refl = Set