{-# OPTIONS --without-K --safe --sized-types #-}
module Codata.Delay where
open import Size
open import Codata.Thunk using (Thunk; force)
open import Codata.Conat using (Conat; zero; suc; Finite)
open import Data.Empty
open import Relation.Nullary
open import Data.Nat.Base
open import Data.Maybe.Base hiding (map ; fromMaybe ; zipWith ; alignWith ; zip ; align)
open import Data.Product as P hiding (map ; zip)
open import Data.Sum as S hiding (map)
open import Data.These as T using (These; this; that; these)
open import Function
data Delay {ℓ} (A : Set ℓ) (i : Size) : Set ℓ where
now : A → Delay A i
later : Thunk (Delay A) i → Delay A i
module _ {ℓ} {A : Set ℓ} where
length : ∀ {i} → Delay A i → Conat i
length (now _) = zero
length (later d) = suc λ where .force → length (d .force)
never : ∀ {i} → Delay A i
never = later λ where .force → never
fromMaybe : Maybe A → Delay A ∞
fromMaybe = maybe now never
runFor : ℕ → Delay A ∞ → Maybe A
runFor zero d = nothing
runFor (suc n) (now a) = just a
runFor (suc n) (later d) = runFor n (d .force)
module _ {ℓ ℓ′} {A : Set ℓ} {B : Set ℓ′} where
map : (A → B) → ∀ {i} → Delay A i → Delay B i
map f (now a) = now (f a)
map f (later d) = later λ where .force → map f (d .force)
bind : ∀ {i} → Delay A i → (A → Delay B i) → Delay B i
bind (now a) f = f a
bind (later d) f = later λ where .force → bind (d .force) f
unfold : (A → A ⊎ B) → A → ∀ {i} → Delay B i
unfold next seed with next seed
... | inj₁ seed′ = later λ where .force → unfold next seed′
... | inj₂ b = now b
module _ {a b c} {A : Set a} {B : Set b} {C : Set c} where
zipWith : (A → B → C) → ∀ {i} → Delay A i → Delay B i → Delay C i
zipWith f (now a) d = map (f a) d
zipWith f d (now b) = map (λ a → f a b) d
zipWith f (later a) (later b) = later λ where .force → zipWith f (a .force) (b .force)
alignWith : (These A B → C) → ∀ {i} → Delay A i → Delay B i → Delay C i
alignWith f (now a) (now b) = now (f (these a b))
alignWith f (now a) (later _) = now (f (this a))
alignWith f (later _) (now b) = now (f (that b))
alignWith f (later a) (later b) = later λ where
.force → alignWith f (a .force) (b .force)
module _ {a b} {A : Set a} {B : Set b} where
zip : ∀ {i} → Delay A i → Delay B i → Delay (A × B) i
zip = zipWith _,_
align : ∀ {i} → Delay A i → Delay B i → Delay (These A B) i
align = alignWith id
module _ {ℓ} {A : Set ℓ} where
infix 3 _⇓
data _⇓ : Delay A ∞ → Set ℓ where
now : ∀ a → now a ⇓
later : ∀ {d} → d .force ⇓ → later d ⇓
extract : ∀ {d} → d ⇓ → A
extract (now a) = a
extract (later d) = extract d
¬never⇓ : ¬ (never ⇓)
¬never⇓ (later p) = ¬never⇓ p
length-⇓ : ∀ {d} → d ⇓ → Finite (length d)
length-⇓ (now a) = zero
length-⇓ (later d⇓) = suc (length-⇓ d⇓)
module _ {ℓ ℓ′} {A : Set ℓ} {B : Set ℓ′} where
map-⇓ : ∀ (f : A → B) {d} → d ⇓ → map f d ⇓
map-⇓ f (now a) = now (f a)
map-⇓ f (later d) = later (map-⇓ f d)
bind-⇓ : ∀ {m} (m⇓ : m ⇓) {f : A → Delay B ∞} → f (extract m⇓) ⇓ → bind m f ⇓
bind-⇓ (now a) fa⇓ = fa⇓
bind-⇓ (later p) fa⇓ = later (bind-⇓ p fa⇓)