module stdlib-bounded-stream where

open import Level hiding (suc)
open import Data.List hiding (take ; zipWith)
open import Data.Nat hiding (_⊔_)

----------------------------------------------------------------------
-- datatypes
----------------------------------------------------------------------

data 𝕊-observer{ℓ ℓ'} (A : Set ℓ)(R : Set ℓ') : ℕ → Set (ℓ ⊔ ℓ') where
  ohead : {n : ℕ} → (A → R) → 𝕊-observer A R n
  otail : {n : ℕ} → 𝕊-observer A R n → 𝕊-observer A R (suc n)

-- streams map stream observers to results
𝕊 : ∀{ℓ}→ Set ℓ → ℕ → Set (Level.suc ℓ)
𝕊{ℓ} A n = ∀ {R : Set ℓ} → 𝕊-observer A R n → R

----------------------------------------------------------------------
-- operations
----------------------------------------------------------------------

head : ∀{ℓ}{A : Set ℓ}{n : ℕ} → 𝕊 A n → A
head s = s (ohead (λ x → x))

tail : ∀{ℓ}{A : Set ℓ}{n : ℕ} → 𝕊 A (suc n) → 𝕊 A n
tail s o = s (otail o)

_::𝕊_ : ∀{ℓ}{A : Set ℓ}{n : ℕ} → A → 𝕊 A n → 𝕊 A (suc n)
(x ::𝕊 xs) (ohead f) = f x
(x ::𝕊 xs) (otail o) = xs o

repeat : ∀{ℓ}{A : Set ℓ} → (a : A) → {n : ℕ} → 𝕊 A n
repeat a (ohead f) = f a
repeat a (otail o) = repeat a o

nats-from : ℕ → {n : ℕ} → 𝕊 ℕ n
nats-from x (ohead f) = f x
nats-from x (otail o) = nats-from (x + 1) o

nats : {n : ℕ} → 𝕊 ℕ n
nats = nats-from 0

take : ∀{ℓ}{A : Set ℓ} → (n : ℕ) → 𝕊 A n → List A
take 0 xs = []
take (suc n) xs = (head xs) ∷ (take n (tail xs))

zipWith : ∀ {ℓ} {A B C : Set ℓ} → (A → B → C) → {n : ℕ} → 𝕊 A n → 𝕊 B n → 𝕊 C n
zipWith _f_ xs ys (ohead g) = g ((head xs) f (head ys))
zipWith _f_ xs ys (otail o) = zipWith _f_ (tail xs) (tail ys) o

fib : {n : ℕ} → 𝕊 ℕ n
fib (ohead f) = f 0
fib (otail (ohead f)) = f 1
fib (otail (otail o)) = zipWith _+_ fib (tail fib) o

test-fib = take 10 fib