mirror of
https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git
synced 2024-05-31 07:28:34 +02:00
36 lines
No EOL
1.1 KiB
Agda
36 lines
No EOL
1.1 KiB
Agda
{-# 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 |