← Back to branch summary

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

« back to all changes in this revision

Viewing changes to test/succeed/InductiveAndCoinductiveConstructors.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/InductiveAndCoinductiveConstructors.agda
1
 
 
2
 
module InductiveAndCoinductiveConstructors where
3
 
 
4
 
open import Common.Coinduction
5
 
 
6
 
record ⊤ : Set where
7
 
 
8
 
data _×_ (A : Set) (B : Set) : Set where
9
 
  _,_ : (x : A) (y : B) → A × B
10
 
 
11
 
data Stream (A : Set) : Set where
12
 
  _≺_ : (x : A) (xs : ∞ (Stream A)) → Stream A
13
 
 
14
 
data U : Set where
15
 
  stream : (a : U) → U
16
 
  _⊗_    : (a b : U) → U
17
 
  unit   : U
18
 
 
19
 
El : U → Set
20
 
El (stream a) = Stream (El a)
21
 
El (a ⊗ b)    = El a × El b
22
 
El unit       = ⊤
23
 
 
24
 
mutual
25
 
 
26
 
  data WHNF : U → Set where
27
 
    _≺_  : ∀ {a} → El a → Prog (stream a) → WHNF (stream a)
28
 
    _,_  : ∀ {a b} → WHNF a → WHNF b → WHNF (a ⊗ b)
29
 
 
30
 
  data Prog : U → Set where
31
 
    ↓_  : ∀ {a} → ∞ (WHNF a) → Prog a
32
 
    fst : ∀ {a b} → Prog (a ⊗ b) → Prog a
33
 
    snd : ∀ {a b} → Prog (a ⊗ b) → Prog b
34
 
    lab : Prog (stream unit) → Prog (stream (stream unit)) →
35
 
          Prog (stream unit ⊗ stream (stream unit))
36
 
 
37
 
whnf : ∀ {a} → Prog a → WHNF a
38
 
whnf (↓ w) = ♭ w
39
 
whnf (fst p) with whnf p
40
 
... | (x , y) = x
41
 
whnf (snd p) with whnf p
42
 
... | (x , y) = y
43
 
whnf (lab xs lss) with whnf xs | whnf lss
44
 
... | _ ≺ xs′ | (x ≺ ls) ≺ lss′ =
45
 
  ((_ ≺ fst (lab xs′ lss′)) , (♭ ls ≺ snd (lab xs′ lss′)))
46
 
 
47
 
⟦_⟧ : Prog (stream unit) → Stream ⊤
48
 
⟦ p ⟧ with whnf p
49
 
... | x ≺ xs = x ≺ ♯ ⟦ xs ⟧
50
 
 
51
 
data _≈_ : Stream ⊤ → Stream ⊤ → Set where
52
 
  cons : ∀ {xs xs′} → ∞ ((♭ xs) ≈ (♭ xs′)) → (_ ≺ xs) ≈ (_ ≺ xs′)
53
 
 
54
 
lemma : ∀ xs lss → ⟦ fst (lab xs lss) ⟧ ≈ ⟦ xs ⟧
55
 
lemma xs lss with whnf xs | whnf lss
56
 
... | _ ≺ xs′ | (x ≺ ls) ≺ lss′ = cons (♯ lemma xs′ lss′)
57
 
 
58
 
{- Andreas, 2012-09-07 WAS:
59
 
label : Prog (stream unit) → Stream ⊤ →
60
 
        Prog (stream unit ⊗ stream (stream unit))
61
 
label xs ls = lab xs (↓ (♯ (ls ≺ snd (label xs ls))))
62
 
 
63
 
shape-preserved : ∀ xs ls → ⟦ fst (label xs ls) ⟧ ≈ ⟦ xs ⟧
64
 
shape-preserved xs ls = lemma xs _
65
 
-}
66
 
 
67
 
mutual
68
 
  label : Prog (stream unit) → Stream ⊤ →
69
 
          Prog (stream unit ⊗ stream (stream unit))
70
 
  label xs ls = lab xs (lss xs ls)
71
 
 
72
 
  lss   : Prog (stream unit) → Stream ⊤ → _
73
 
  lss   xs ls = (↓ (♯ (ls ≺ snd (label xs ls))))
74
 
 
75
 
shape-preserved : ∀ xs ls → ⟦ fst (label xs ls) ⟧ ≈ ⟦ xs ⟧
76
 
shape-preserved xs ls = lemma xs (lss xs ls)