------------------------------------------------------------------------
-- The Agda standard library
--
-- Infinite streams defined as coinductive records
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe --guardedness #-}
module Codata.Guarded.Stream where
open import Level hiding (suc)
open import Data.Nat.Base using (ℕ; zero; suc)
open import Function.Base using (_∘′_; const; id; _∘₂_)
open import Data.List.Base as List using (List; []; _∷_)
open import Data.Product.Base hiding (map)
open import Data.Vec.Base using (Vec; []; _∷_)
open import Data.List.NonEmpty.Base as List⁺ using (List⁺; _∷_)
open import Algebra.Core using (Op₂)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
private
variable
a b c : Level
A : Set a
B : Set b
C : Set c
------------------------------------------------------------------------
-- Type
infixr 5 _∷_
record Stream (A : Set a) : Set a where
coinductive
constructor _∷_
field
head : A
tail : Stream A
open Stream public
------------------------------------------------------------------------
-- Creating streams
tabulate : (ℕ → A) → Stream A
tabulate f .head = f 0
tabulate f .tail = tabulate (f ∘′ suc)
repeat : A → Stream A
repeat = tabulate ∘′ const
infixr 5 _++_
_++_ : List A → Stream A → Stream A
[] ++ s = s
(x ∷ xs) ++ s = x ∷ xs ++ s
unfold : (A → A × B) → A → Stream B
unfold next seed .head = next seed .proj₂
unfold next seed .tail = unfold next (next seed .proj₁)
iterate : (A → A) → A → Stream A
iterate f = unfold < f , id >
nats : Stream ℕ
nats = tabulate id
------------------------------------------------------------------------
-- Lookup
lookup : Stream A → ℕ → A
lookup xs zero = head xs
lookup xs (suc n) = lookup (tail xs) n
infix 4 _[_]
_[_] : Stream A → ℕ → A
_[_] = lookup
------------------------------------------------------------------------
-- Transforming streams
map : (A → B) → Stream A → Stream B
map f s .head = f (s .head)
map f s .tail = map f (s .tail)
ap : Stream (A → B) → Stream A → Stream B
ap fs xs .head = fs .head (xs .head)
ap fs xs .tail = ap (fs .tail) (xs .tail)
scanl : (B → A → B) → B → Stream A → Stream B
scanl c n s .head = n
scanl c n s .tail = scanl c (c n (s .head)) (s .tail)
zipWith : (A → B → C) → Stream A → Stream B → Stream C
zipWith f s t .head = f (s .head) (t .head)
zipWith f s t .tail = zipWith f (s .tail) (t .tail)
transpose : List (Stream A) → Stream (List A)
transpose [] = repeat []
transpose (s ∷ ss) = zipWith _∷_ s (transpose ss)
tails : Stream A → Stream (Stream A)
tails s .head = s
tails s .tail = tails (s .tail)
evens : Stream A → Stream A
evens s .head = s .head
evens s .tail = evens (s .tail .tail)
odds : Stream A → Stream A
odds s = evens (s .tail)
------------------------------------------------------------------------
-- List⁺-related functions
infixr 5 _⁺++_
_⁺++_ : List⁺ A → Stream A → Stream A
(x ∷ xs) ⁺++ ys = x ∷ xs ++ ys
concat : Stream (List⁺ A) → Stream A
concat {A = A} = ++-concat []
module Concat where
++-concat : List A → Stream (List⁺ A) → Stream A
++-concat [] s .head = s .head .List⁺.head
++-concat [] s .tail = ++-concat (s .head .List⁺.tail) (s .tail)
++-concat (x ∷ xs) s .head = x
++-concat (x ∷ xs) s .tail = ++-concat xs s
cycle : List⁺ A → Stream A
cycle = concat ∘′ repeat
transpose⁺ : List⁺ (Stream A) → Stream (List⁺ A)
transpose⁺ (s ∷ ss) = zipWith _∷_ s (transpose ss)
------------------------------------------------------------------------
-- Chunking
splitAt : ∀ n → Stream A → Vec A n × Stream A
splitAt zero s = [] ,′ s
splitAt (suc n) s = map₁ (s .head ∷_) (splitAt n (s .tail))
take : ∀ n → Stream A → Vec A n
take = proj₁ ∘₂ splitAt
drop : ℕ → Stream A → Stream A
drop = proj₂ ∘₂ splitAt
chunksOf : ∀ n → Stream A → Stream (Vec A n)
chunksOf n s .head = take n s
chunksOf n s .tail = chunksOf n (drop n s)
------------------------------------------------------------------------
-- Interleaving streams
-- Interleaving two streams
interleave : Op₂ (Stream A)
interleave xs ys .head = xs .head
interleave xs ys .tail = interleave ys (xs .tail)
-- Interleaving multiple streams
interleave⁺ : List⁺ (Stream A) → Stream A
interleave⁺ = concat ∘′ transpose⁺
-- Interleaving a stream of streams using Cantor's zig zag function
-- (inverse of Cantor's pairing function)
cantor : Stream (Stream A) → Stream A
cantor s .head = s .head .head
cantor s .tail = cantor (zipWith _∷_ (s .head .tail) (s .tail))
-- A version of `bind` using the zig zag function that reaches any
-- point of the plane in a finite amout of time
plane : {B : A → Set b} → Stream A → (∀ a → Stream (B a)) → Stream (Σ A B)
plane xs fs = cantor (map (λ x → map (x ,_) (fs x)) xs)
-- Here is the beginning of the path we are following:
_ : take 21 (plane nats (const nats))
≡ (0 , 0)
∷ (0 , 1) ∷ (1 , 0)
∷ (0 , 2) ∷ (1 , 1) ∷ (2 , 0)
∷ (0 , 3) ∷ (1 , 2) ∷ (2 , 1) ∷ (3 , 0)
∷ (0 , 4) ∷ (1 , 3) ∷ (2 , 2) ∷ (3 , 1) ∷ (4 , 0)
∷ (0 , 5) ∷ (1 , 4) ∷ (2 , 3) ∷ (3 , 2) ∷ (4 , 1) ∷ (5 , 0)
∷ []
_ = refl
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