\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
        head  : A
        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  _∈_
_∈_ : 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  _∈²_
_∈²_ : 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}