module DS.IR where

open import Prelude.Basic
open import Prelude.Equality
open import Prelude.Fam


{- Dybjer-Setzer codes -}
data DS (D : Set1) (E : Set1) : Set1 where
   ι : E →  DS D E
   σ : (A : Set) → (A → DS D E) → DS D E
   δ : (A : Set) → ((A → D) → DS D E) → DS D E

⟦_⟧₀ : {D E : Set1} -> DS D E -> Fam D -> Set
⟦ ι e ⟧₀ X = ⊤
⟦ σ A f ⟧₀ X = Σ[ a ∈ A ] ⟦ f a ⟧₀ X
⟦ δ A F ⟧₀ (U , T) = Σ[ g ∈ (A -> U) ] ⟦ F (T ∘ g) ⟧₀ (U , T)

⟦_⟧₁ : {D E : Set1} -> (c : DS D E) -> (F : Fam D) -> ⟦ c ⟧₀ F -> E
⟦ ι e ⟧₁ X _ = e
⟦ σ A f ⟧₁ X (a , x) = ⟦ f a ⟧₁ X x
⟦ δ A F ⟧₁ (U , T) (g , x) = ⟦ F (T ∘ g) ⟧₁ (U , T) x

⟦_⟧ : {D E : Set1} -> DS D E -> Fam D -> Fam E
⟦ c ⟧ X = ⟦ c ⟧₀ X , ⟦ c ⟧₁ X

-- DS D is functorial
DS-map : {D E E' : Set₁} -> (E -> E') -> DS D E  -> DS D E'
DS-map h (ι e) = ι (h e)
DS-map h (σ A f) = σ A (λ a → DS-map h (f a))
DS-map h (δ A F) = δ A (λ g → DS-map h (F g))

-- and monadic

ηDS : {I O : Set₁} → O → DS I O
ηDS o = ι o

μDS : {I O : Set₁} → DS I (DS I O) → DS I O
μDS (ι o) = o
μDS (σ A f) = σ A λ a → μDS (f a)
μDS (δ A F) = δ A λ h → μDS (F h)

-- and thus has a bind operation

_DS->>=_ : {D E E' : Set₁} → DS D E → (E → DS D E') → DS D E'
c DS->>= h = μDS (DS-map h c)