module ColistQuestion where

open import Codata.Musical.Notation
open import Data.Maybe
open import Data.Sum

case_of_ : ∀ {a b} {A : Set a} {B : Set b} → A → (A → B) → B
case x of f = f x

--
-- Streams with coinductive records
--

record Stream (A : Set) : Set where
  coinductive
  field hd : A
        tl : Stream A
open Stream public

iterate : ∀ {a} → (a → a) → a → Stream a
hd (iterate f a) = a
tl (iterate f a) = iterate f (f a)

--
-- Colist using musical notation
--

data Colist (A : Set) : Set where
  []  : Colist A
  _∷_ : A → (∞ (Colist A)) → Colist A  

iterate1 : ∀ {a} → (a → Maybe a) → a → Colist a
iterate1 f a = a ∷ ♯ (case f a of
                       λ { (just a₁) → (iterate1 f a₁)
                         ; nothing   → []
                         })

data T (e : Set) (a : Set) : Set where
   V    : a → T e a
   _<<_ : e → ∞ (T e a) → T e a

iterT : ∀ {e a} → (e → e) → e → T e a
iterT f e = e << ♯ (iterT f (f e))

iterT1 : ∀ {e a} → (e → (e ⊎ a)) → e → T e a
iterT1 f e = e << ♯ (case f e of
                      λ { (inj₁ e₁) → iterT1 f e₁
                        ; (inj₂ a)  → V a
                        })