\begin{code}
{-# OPTIONS --cubical --safe #-}

module Codata.Stream where

open import Prelude
open import Data.List using (List; _∷_; [])
open import Data.List.Kleene
import Data.List.Kleene.Membership as Kleene
open import Data.Fin

private
module AsCodata where
\end{code}
%<*codata-stream>
\begin{code}
record Stream {a} (A : Type a) : Type a where
coinductive
field
tail  : Stream A
\end{code}
%</codata-stream>
\begin{code}

Stream : Type a → Type a
\end{code}
%<*stream-def>
\begin{code}
Stream A = ℕ → A
\end{code}
%</stream-def>
\begin{code}

infixr 5 _∈_
_∈_ : A → Stream A → Type _
x ∈ xs = fiber xs x

toList : ℕ → Stream A → List A
toList zero xs = []
toList (suc n) xs = xs zero ∷ toList n (xs ∘ suc)

mutual
concat⋆ : A ⋆ → Stream (A ⁺) → Stream A
concat⋆ []    xs = concat⁺ (xs zero) (xs ∘ suc)
concat⋆ (∹ x) xs = concat⁺ x xs

concat⁺ : A ⁺ → Stream (A ⁺) → Stream A
concat⁺ x xs zero    = x .head
concat⁺ x xs (suc n) = concat⋆ (x .tail) xs n

concat : Stream (A ⁺) → Stream A
concat xs = concat⁺ (xs zero) (xs ∘ suc)

infixr 5 _∈²_
_∈²_ : A → Stream (A ⁺) → Type _
x ∈² xs = ∃[ n ] x Kleene.∈⁺ xs n

mutual
◇++⋆ : ∀ (x : A) y ys → x Kleene.∈⋆ y → x ∈ concat⋆ y ys
◇++⋆ x (∹ y) ys x∈y = ◇++⁺ x y ys x∈y

◇++⁺ : ∀ (x : A) y ys → x Kleene.∈⁺ y → x ∈ concat⁺ y ys
◇++⁺ x y ys (f0 , x∈y) = zero , x∈y
◇++⁺ x y ys (fs n , x∈y) = let m , p = ◇++⋆ x (y .tail) ys (n , x∈y) in suc m , p

mutual
++◇⋆ : ∀ (x : A) y ys → x ∈ concat ys → x ∈ concat⋆ y ys
++◇⋆ x [] ys x∈ys = x∈ys
++◇⋆ x (∹ y) ys x∈ys = ++◇⁺ x y ys x∈ys

++◇⁺ : ∀ (x : A) y ys → x ∈ concat ys → x ∈ concat⁺ y ys
++◇⁺ x y ys x∈ys = let n , p = ++◇⋆ x (y .tail) ys x∈ys in suc n , p

concat-∈ : ∀ (x : A) xs → x ∈² xs → x ∈ concat xs
concat-∈ x xs (zero  , x∈xs) = ◇++⁺ x (xs zero) (xs ∘ suc) x∈xs
concat-∈ x xs (suc n , x∈xs) = ++◇⁺ x (xs zero) (xs ∘ suc) (concat-∈ x (xs ∘ suc) (n , x∈xs))
\end{code}