← Back to branch summary

~ubuntu-branches/ubuntu/precise/agda-stdlib/precise

« back to all changes in this revision

Viewing changes to src/Data/Stream.agda

  • Committer: Bazaar Package Importer
  • Author(s): Iain Lane
  • Date: 2011-02-25 22:28:40 UTC
  • mfrom: (1.1.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20110225222840-jt16gl302kca7h0g
Tags: 0.5-1~ubuntu1
https://launchpad.net/bugs/725364
http://bugs.debian.org/573807
http://bugs.debian.org/598708

* Upload to Ubuntu from Debian's VCS due to delays in unstable caused by
  the GHC 7 transition (LP: #725364)
* [ba20206] Make package architecture independent (Closes: #573807, #598708,
  #599958)
* [0fb0600] Standards-Version → 3.9.1, no changes required
* [d3f13b8] Update required Agda version to 2.2.8
* [cc1f5c8] Imported Upstream version 0.4
* [2c82171] Add watch file
* [9251e0b] Imported Upstream version 0.5
* [0518fa6] No longer need procps | hurd BD as we no longer have the ticker
* [daf2445] Don't use upstream's make install — handled ourselves by
  dh_install
* [1b86533] Update watchfile to point at new location
* [637f47d] Remove debian/gbp.conf as we are no longer building for exp
* [cc88671] Require Agda 2.2.10
* [e99dab5] Set maximum stack size to 1G to prevent overflows in the build
* [251cd1d] Run the test suite manually
* [a7db697] Set the variable in the emacs loading script properly

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Data/Stream.agda
21
21
------------------------------------------------------------------------
22
22
-- Some operations
23
23
 
24
 
head : forall {A} -> Stream A -> A
 
24
head : forall {A} → Stream A → A
25
25
head (x ∷ xs) = x
26
26
 
27
 
tail : forall {A} -> Stream A -> Stream A
 
27
tail : forall {A} → Stream A → Stream A
28
28
tail (x ∷ xs) = ♭ xs
29
29
 
30
30
map : ∀ {A B} → (A → B) → Stream A → Stream B
31
31
map f (x ∷ xs) = f x ∷ ♯ map f (♭ xs)
32
32
 
33
 
zipWith : forall {A B C} ->
34
 
          (A -> B -> C) -> Stream A -> Stream B -> Stream C
 
33
zipWith : forall {A B C} →
 
34
          (A → B → C) → Stream A → Stream B → Stream C
35
35
zipWith _∙_ (x ∷ xs) (y ∷ ys) = (x ∙ y) ∷ ♯ zipWith _∙_ (♭ xs) (♭ ys)
36
36
 
37
37
take : ∀ {A} (n : ℕ) → Stream A → Vec A n
38
38
take zero    xs       = []
39
39
take (suc n) (x ∷ xs) = x ∷ take n (♭ xs)
40
40
 
41
 
drop : ∀ {A} -> ℕ -> Stream A -> Stream A
 
41
drop : ∀ {A} → ℕ → Stream A → Stream A
42
42
drop zero    xs       = xs
43
43
drop (suc n) (x ∷ xs) = drop n (♭ xs)
44
44
 
45
 
repeat : forall {A} -> A -> Stream A
 
45
repeat : forall {A} → A → Stream A
46
46
repeat x = x ∷ ♯ repeat x
47
47
 
48
48
iterate : ∀ {A} → (A → A) → A → Stream A
55
55
_⋎_ : ∀ {A} → Stream A → Stream A → Stream A
56
56
(x ∷ xs) ⋎ ys = x ∷ ♯ (ys ⋎ ♭ xs)
57
57
 
 
58
mutual
 
59
 
 
60
  -- Takes every other element from the stream, starting with the
 
61
  -- first one.
 
62
 
 
63
  evens : {A : Set} → Stream A → Stream A
 
64
  evens (x ∷ xs) = x ∷ ♯ odds (♭ xs)
 
65
 
 
66
  -- Takes every other element from the stream, starting with the
 
67
  -- second one.
 
68
 
 
69
  odds : {A : Set} → Stream A → Stream A
 
70
  odds (x ∷ xs) = evens (♭ xs)
 
71
 
58
72
toColist : ∀ {A} → Stream A → Colist A
59
73
toColist (x ∷ xs) = x ∷ ♯ toColist (♭ xs)
60
74
 
120
134
map-cong : ∀ {A B} (f : A → B) {xs ys : Stream A} →
121
135
           xs ≈ ys → map f xs ≈ map f ys
122
136
map-cong f (x ∷ xs≈) = f x ∷ ♯ map-cong f (♭ xs≈)
 
137
 
 
138
zipWith-cong : ∀ {A B C} (_∙_ : A → B → C) {xs xs′ ys ys′} →
 
139
               xs ≈ xs′ → ys ≈ ys′ →
 
140
               zipWith _∙_ xs ys ≈ zipWith _∙_ xs′ ys′
 
141
zipWith-cong _∙_ (x ∷ xs≈) (y ∷ ys≈) =
 
142
  (x ∙ y) ∷ ♯ zipWith-cong _∙_ (♭ xs≈) (♭ ys≈)
 
143
 
 
144
infixr 5 _⋎-cong_
 
145
 
 
146
_⋎-cong_ : ∀ {A} {xs xs′ ys ys′ : Stream A} →
 
147
           xs ≈ xs′ → ys ≈ ys′ → xs ⋎ ys ≈ xs′ ⋎ ys′
 
148
(x ∷ xs≈) ⋎-cong ys≈ = x ∷ ♯ (ys≈ ⋎-cong ♭ xs≈)