------------------------------------------------------------------------ -- The Agda standard library -- -- Streams ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --guardedness #-} module Codata.Musical.Stream where open import Level using (Level) open import Codata.Musical.Notation open import Codata.Musical.Colist using (Colist; []; _∷_) open import Data.Vec.Base using (Vec; []; _∷_) open import Data.Nat.Base using (ℕ; zero; suc) open import Relation.Binary open import Relation.Binary.PropositionalEquality as P using (_≡_) private variable a b c : Level A : Set a B : Set b C : Set c ------------------------------------------------------------------------ -- The type infixr 5 _∷_ data Stream (A : Set a) : Set a where _∷_ : (x : A) (xs : ∞ (Stream A)) → Stream A {-# FOREIGN GHC data AgdaStream a = Cons a (MAlonzo.RTE.Inf (AgdaStream a)) type AgdaStream' l a = AgdaStream a #-} {-# COMPILE GHC Stream = data AgdaStream' (Cons) #-} ------------------------------------------------------------------------ -- Some operations head : Stream A → A head (x ∷ xs) = x tail : Stream A → Stream A tail (x ∷ xs) = ♭ xs map : (A → B) → Stream A → Stream B map f (x ∷ xs) = f x ∷ ♯ map f (♭ xs) zipWith : (A → B → C) → Stream A → Stream B → Stream C zipWith _∙_ (x ∷ xs) (y ∷ ys) = (x ∙ y) ∷ ♯ zipWith _∙_ (♭ xs) (♭ ys) take : ∀ n → Stream A → Vec A n take zero xs = [] take (suc n) (x ∷ xs) = x ∷ take n (♭ xs) drop : ℕ → Stream A → Stream A drop zero xs = xs drop (suc n) (x ∷ xs) = drop n (♭ xs) repeat : A → Stream A repeat x = x ∷ ♯ repeat x iterate : (A → A) → A → Stream A iterate f x = x ∷ ♯ iterate f (f x) -- Interleaves the two streams. infixr 5 _⋎_ _⋎_ : 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 : Stream A → Stream A evens (x ∷ xs) = x ∷ ♯ odds (♭ xs) -- Takes every other element from the stream, starting with the -- second one. odds : Stream A → Stream A odds (x ∷ xs) = evens (♭ xs) toColist : Stream A → Colist A toColist (x ∷ xs) = x ∷ ♯ toColist (♭ xs) lookup : Stream A → ℕ → A lookup (x ∷ xs) zero = x lookup (x ∷ xs) (suc n) = lookup (♭ xs) n infixr 5 _++_ _++_ : ∀ {a} {A : Set 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 : Set a} : Stream A → Stream A → Set a where _∷_ : ∀ {x y xs ys} (x≡ : x ≡ y) (xs≈ : ∞ (♭ xs ≈ ♭ ys)) → x ∷ xs ≈ y ∷ ys -- x ∈ xs means that x is a member of xs. infix 4 _∈_ data _∈_ {A : Set a} : A → Stream A → Set a 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 : Set a} : Colist A → Stream A → Set a where [] : ∀ {ys} → [] ⊑ ys _∷_ : ∀ x {xs ys} (p : ∞ (♭ xs ⊑ ♭ ys)) → x ∷ xs ⊑ x ∷ ys ------------------------------------------------------------------------ -- Some proofs setoid : ∀ {a} → Set a → Setoid _ _ setoid A = record { Carrier = Stream A ; _≈_ = _≈_ {A = A} ; isEquivalence = record { refl = refl ; sym = sym ; trans = trans } } where refl : Reflexive _≈_ refl {_ ∷ _} = P.refl ∷ ♯ refl sym : Symmetric _≈_ sym (x≡ ∷ xs≈) = P.sym x≡ ∷ ♯ sym (♭ xs≈) trans : Transitive _≈_ trans (x≡ ∷ xs≈) (y≡ ∷ ys≈) = P.trans x≡ y≡ ∷ ♯ trans (♭ xs≈) (♭ ys≈) head-cong : {xs ys : Stream A} → xs ≈ ys → head xs ≡ head ys head-cong (x≡ ∷ _) = x≡ tail-cong : {xs ys : Stream A} → xs ≈ ys → tail xs ≈ tail ys tail-cong (_ ∷ xs≈) = ♭ xs≈ map-cong : ∀ (f : A → B) {xs ys} → xs ≈ ys → map f xs ≈ map f ys map-cong f (x≡ ∷ xs≈) = P.cong f x≡ ∷ ♯ map-cong f (♭ xs≈) zipWith-cong : ∀ (_∙_ : A → B → C) {xs xs′ ys ys′} → xs ≈ xs′ → ys ≈ ys′ → zipWith _∙_ xs ys ≈ zipWith _∙_ xs′ ys′ zipWith-cong _∙_ (x≡ ∷ xs≈) (y≡ ∷ ys≈) = P.cong₂ _∙_ x≡ y≡ ∷ ♯ zipWith-cong _∙_ (♭ xs≈) (♭ ys≈) infixr 5 _⋎-cong_ _⋎-cong_ : {xs xs′ ys ys′ : Stream A} → xs ≈ xs′ → ys ≈ ys′ → xs ⋎ ys ≈ xs′ ⋎ ys′ (x ∷ xs≈) ⋎-cong ys≈ = x ∷ ♯ (ys≈ ⋎-cong ♭ xs≈)