------------------------------------------------------------------------
-- 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.Definitions
using (Reflexive; Symmetric; Transitive)
open import Relation.Binary.Bundles using (Setoid)
open import Relation.Binary.PropositionalEquality.Core as ≡ 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 {_ ∷ _} = ≡.refl ∷ ♯ refl
sym : Symmetric _≈_
sym (x≡ ∷ xs≈) = ≡.sym x≡ ∷ ♯ sym (♭ xs≈)
trans : Transitive _≈_
trans (x≡ ∷ xs≈) (y≡ ∷ ys≈) = ≡.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≈) = ≡.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≈) =
≡.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≈)
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4