bsc-leon-vatthauer/slides/code-examples/reverse.agda

{-# OPTIONS --guardedness #-}
open import Codata.Musical.Notation
open import Data.Nat

module reverse where
  data Delay (A : Set) : Set where
    now : A → Delay A
    later : ∞ (Delay A) → Delay 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

  never : ∀ {A : Set} → Delay A
  never = later (♯ never)

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

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

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

  ones : Colist ℕ
  ones = 1 ∷ ♯ ones

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