← Back to branch summary

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

« back to all changes in this revision

Viewing changes to test/succeed/CoPatStream.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/CoPatStream.agda
1
 
{-# OPTIONS --copatterns #-}
2
 
module CoPatStream where
3
 
 
4
 
open import Common.Equality
5
 
 
6
 
record Stream (A : Set) : Set where
7
 
  coinductive
8
 
  field
9
 
    head : A
10
 
    tail : Stream A
11
 
module S = Stream
12
 
 
13
 
record _≈_ {A : Set}(s t : Stream A) : Set where
14
 
  coinductive
15
 
  field
16
 
    head : S.head s ≡ S.head t
17
 
    tail : S.tail s ≈ S.tail t
18
 
module B = _≈_
19
 
 
20
 
repeat : {A : Set}(a : A) → Stream A
21
 
S.head (repeat a) = a
22
 
S.tail (repeat a) = repeat a
23
 
 
24
 
module CoPat where
25
 
 
26
 
  map : {A B : Set} → (A → B) → Stream A → Stream B
27
 
  S.head (map f s) = f (S.head s)
28
 
  S.tail (map f s) = map f (S.tail s)
29
 
 
30
 
  map_id : {A : Set}(s : Stream A) → map (λ x → x) s ≈ s
31
 
  B.head (map_id s) = refl
32
 
  B.tail (map_id s) = map_id (S.tail s)
33
 
 
34
 
module HandTranslated where
35
 
 
36
 
  {-# NO_TERMINATION_CHECK #-}
37
 
  map : {A B : Set} → (A → B) → Stream A → Stream B
38
 
  map f s = record
39
 
    { head = f (S.head s)
40
 
    ; tail = map f (S.tail s)
41
 
    }
42
 
 
43
 
  {- loops
44
 
  {-# NO_TERMINATION_CHECK #-}
45
 
  map_id : {A : Set}(s : Stream A) → map (λ x → x) s ≈ s
46
 
  map_id s = record
47
 
    { head = refl
48
 
    ; tail = map_id (S.tail s)
49
 
    }
50
 
  -}
51
 
 
52
 
module DeepCoPat where
53
 
 
54
 
  repeat₂ : {A : Set}(a₁ a₂ : A) → Stream A
55
 
  (       (S.head (repeat₂ a₁ a₂))) = a₁
56
 
  (S.head (S.tail (repeat₂ a₁ a₂))) = a₂
57
 
  (S.tail (S.tail (repeat₂ a₁ a₂))) = repeat₂ a₁ a₂
58
 
 
59
 
  repeat≈repeat₂ : {A : Set}(a : A) → repeat a ≈ repeat₂ a a
60
 
  (       (B.head (repeat≈repeat₂ a))) = refl
61
 
  (B.head (B.tail (repeat≈repeat₂ a))) = refl
62
 
  (B.tail (B.tail (repeat≈repeat₂ a))) = repeat≈repeat₂ a
63
 
 
64
 
module ProjectionRHS where
65
 
 
66
 
  -- THIS SHOULD NOT TERMINATION CHECK WITH CURRENT TRANSLATION SEMANTICS
67
 
  {-# NO_TERMINATION_CHECK #-}
68
 
  repeat′ : {A : Set}(a : A) → Stream A
69
 
  (       (S.head (repeat′ a))) = a
70
 
  (S.head (S.tail (repeat′ a))) = a
71
 
  (S.tail (S.tail (repeat′ a))) = S.tail (repeat′ a)
72
 
 
73
 
{- LOOPS
74
 
  repeat≈repeat′ : {A : Set}(a : A) → repeat a ≈ repeat′ a
75
 
  (       (B.head (repeat≈repeat′ a))) = refl
76
 
  (B.head (B.tail (repeat≈repeat′ a))) = refl
77
 
  (B.tail (B.tail (repeat≈repeat′ a))) = repeat≈repeat′ a
78
 
-}