{-# OPTIONS --guardedness #-}
open import Codata.Musical.Colist hiding (_++_)
open import Codata.Musical.Colist.Bisimilarity
open import Codata.Musical.Notation
open import Data.Nat
open import Data.Nat.Show renaming (show to showℕ)
open import Function.Base
open import Relation.Binary.PropositionalEquality
open import Data.String using (String; _++_)

module reverse where
  data Delay (A : Set) : Set where
    now : A → Delay A
    later : ∞ (Delay A) → Delay A

  reverse : ∀ {A : Set} → Colist A → Delay (Colist A)
  reverse {A} = reverseAcc []
    where
      reverseAcc : Colist A → Colist A → Delay (Colist A)
      reverseAcc [] a = now a
      reverseAcc (x ∷ xs) a = later (♯ reverseAcc (♭ xs) (x ∷ (♯ a)))

  run_for_steps : ∀ {A : Set} → Delay A → ℕ → Delay A
  run now   x for n     steps = now x
  run later x for zero  steps = later x
  run later x for suc n steps = run ♭ x for n steps


  fin-colist : Colist ℕ
  fin-colist = 1 ∷ ♯ (2 ∷ ♯ (3 ∷ ♯ []))

  inf-colist : Colist ℕ
  inf-colist = 1 ∷ ♯ inf-colist

  -- run reverse fin-colist for 5 steps
  -- run reverse inf-colist for 1000 steps