/usr/share/agda-stdlib/Data/Stream.agda is in agda-stdlib 0.6-2.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 | ------------------------------------------------------------------------
-- The Agda standard library
--
-- Streams
------------------------------------------------------------------------
module Data.Stream where
open import Coinduction
open import Data.Colist using (Colist; []; _∷_)
open import Data.Vec using (Vec; []; _∷_)
open import Data.Nat using (ℕ; zero; suc)
open import Relation.Binary
------------------------------------------------------------------------
-- The type
infixr 5 _∷_
data Stream (A : Set) : Set where
_∷_ : (x : A) (xs : ∞ (Stream A)) → Stream A
{-# IMPORT Data.FFI #-}
{-# COMPILED_DATA Stream Data.FFI.AgdaStream Data.FFI.Cons #-}
------------------------------------------------------------------------
-- Some operations
head : ∀ {A} → Stream A → A
head (x ∷ xs) = x
tail : ∀ {A} → Stream A → Stream A
tail (x ∷ xs) = ♭ xs
map : ∀ {A B} → (A → B) → Stream A → Stream B
map f (x ∷ xs) = f x ∷ ♯ map f (♭ xs)
zipWith : ∀ {A B C} →
(A → B → C) → Stream A → Stream B → Stream C
zipWith _∙_ (x ∷ xs) (y ∷ ys) = (x ∙ y) ∷ ♯ zipWith _∙_ (♭ xs) (♭ ys)
take : ∀ {A} n → Stream A → Vec A n
take zero xs = []
take (suc n) (x ∷ xs) = x ∷ take n (♭ xs)
drop : ∀ {A} → ℕ → Stream A → Stream A
drop zero xs = xs
drop (suc n) (x ∷ xs) = drop n (♭ xs)
repeat : ∀ {A} → A → Stream A
repeat x = x ∷ ♯ repeat x
iterate : ∀ {A} → (A → A) → A → Stream A
iterate f x = x ∷ ♯ iterate f (f x)
-- Interleaves the two streams.
infixr 5 _⋎_
_⋎_ : ∀ {A} → Stream A → Stream A → Stream A
(x ∷ xs) ⋎ ys = x ∷ ♯ (ys ⋎ ♭ xs)
mutual
-- Takes every other element from the stream, starting with the
-- first one.
evens : ∀ {A} → Stream A → Stream A
evens (x ∷ xs) = x ∷ ♯ odds (♭ xs)
-- Takes every other element from the stream, starting with the
-- second one.
odds : ∀ {A} → Stream A → Stream A
odds (x ∷ xs) = evens (♭ xs)
toColist : ∀ {A} → Stream A → Colist A
toColist (x ∷ xs) = x ∷ ♯ toColist (♭ xs)
lookup : ∀ {A} → ℕ → Stream A → A
lookup zero (x ∷ xs) = x
lookup (suc n) (x ∷ xs) = lookup n (♭ xs)
infixr 5 _++_
_++_ : ∀ {A} → Colist A → Stream A → Stream A
[] ++ ys = ys
(x ∷ xs) ++ ys = x ∷ ♯ (♭ xs ++ ys)
------------------------------------------------------------------------
-- Equality and other relations
-- xs ≈ ys means that xs and ys are equal.
infix 4 _≈_
data _≈_ {A} : Stream A → Stream A → Set where
_∷_ : ∀ x {xs ys} (xs≈ : ∞ (♭ xs ≈ ♭ ys)) → x ∷ xs ≈ x ∷ ys
-- x ∈ xs means that x is a member of xs.
infix 4 _∈_
data _∈_ {A} : A → Stream A → Set where
here : ∀ {x xs} → x ∈ x ∷ xs
there : ∀ {x y xs} (x∈xs : x ∈ ♭ xs) → x ∈ y ∷ xs
-- xs ⊑ ys means that xs is a prefix of ys.
infix 4 _⊑_
data _⊑_ {A} : Colist A → Stream A → Set where
[] : ∀ {ys} → [] ⊑ ys
_∷_ : ∀ x {xs ys} (p : ∞ (♭ xs ⊑ ♭ ys)) → x ∷ xs ⊑ x ∷ ys
------------------------------------------------------------------------
-- Some proofs
setoid : Set → Setoid _ _
setoid A = record
{ Carrier = Stream A
; _≈_ = _≈_ {A}
; isEquivalence = record
{ refl = refl
; sym = sym
; trans = trans
}
}
where
refl : Reflexive _≈_
refl {x ∷ _} = x ∷ ♯ refl
sym : Symmetric _≈_
sym (x ∷ xs≈) = x ∷ ♯ sym (♭ xs≈)
trans : Transitive _≈_
trans (x ∷ xs≈) (.x ∷ ys≈) = x ∷ ♯ trans (♭ xs≈) (♭ ys≈)
map-cong : ∀ {A B} (f : A → B) {xs ys} →
xs ≈ ys → map f xs ≈ map f ys
map-cong f (x ∷ xs≈) = f x ∷ ♯ map-cong f (♭ xs≈)
zipWith-cong : ∀ {A B C} (_∙_ : A → B → C) {xs xs′ ys ys′} →
xs ≈ xs′ → ys ≈ ys′ →
zipWith _∙_ xs ys ≈ zipWith _∙_ xs′ ys′
zipWith-cong _∙_ (x ∷ xs≈) (y ∷ ys≈) =
(x ∙ y) ∷ ♯ zipWith-cong _∙_ (♭ xs≈) (♭ ys≈)
infixr 5 _⋎-cong_
_⋎-cong_ : ∀ {A} {xs xs′ ys ys′ : Stream A} →
xs ≈ xs′ → ys ≈ ys′ → xs ⋎ ys ≈ xs′ ⋎ ys′
(x ∷ xs≈) ⋎-cong ys≈ = x ∷ ♯ (ys≈ ⋎-cong ♭ xs≈)
|