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

-- Slight variation of Polynomial.IR where idPN and con are replaced by a
-- container

module Polynomial.Container.IR where

mutual
   data IRCont (D : Set₁) : Set₁ where
        eta : Cont -> IRCont D
        sigma  : (R : IRCont D) ->  (IRPos R -> IRCont D) -> IRCont D
        π   : (A : Set) → (A → IRCont D) → IRCont D

   IRPos : {D : Set₁} -> IRCont D -> Set₁
   IRPos {D} (eta (S , P))  = (S ◃ P) D
   IRPos     (sigma R f) = Σ (IRPos R) (λ x → IRPos (f x))
   IRPos     (π A f) = ∏ A (λ x → IRPos (f x))

IR : ∀ {a} → Set₁ -> Set a -> Set (a ⊔ lsuc (lzero))
IR D E = (IRCont D ◃ IRPos) E

IR-map : ∀ {b c} → {C : Set₁}{D : Set b}{E : Set c} ->
      (D -> E) -> IR C D  -> IR C E
IR-map {C = C} f P = ◃-map (IRCont C) IRPos f P


con : {D : Set₁} → Set → IRCont D
con A = eta (A , λ a → ⊥)

ηIR : ∀ {a} → {D : Set₁} → {E : Set a} -> E -> IR D E
ηIR e = (con ⊤ , const e)

μIR : ∀ {a} → {D : Set₁} -> {E : Set a} → IR D (IR D E) → IR D E
μIR {a} {D} {E} (R , f) = (Q , α)
                          where Q : IRCont D
                                Q = sigma R (proj₁ ∘ f)
                                α : IRPos Q → E
                                α (x , q) = proj₂ (f x) q

_IRbind_ : ∀ {b c} → {I : Set₁}{X : Set b}{Y : Set c} ->
           IR I X → (X →  IR I Y) -> IR I Y
P IRbind f = μIR (IR-map f P)

_IRDbind_ : ∀ {a b} → {I : Set₁} -> {D : Set a} → {E : D -> Set b} ->
            IR I D -> ((d : D) -> IR I (E d)) -> IR I (Σ D E)
P IRDbind f = P IRbind (λ x → IR-map (λ p → (x , p)) (f x))


πIR : {D : Set1} -> (S : Set){E : S -> Set₁} ->
      (∏ S (IR D ∘ E)) -> IR D (∏ S E)
πIR S f = (π S (proj₁ ∘ f) , \ g s -> proj₂ (f s) (g s))

-- The decoding
mutual
  ix : {D : Set₁} -> (X : IRCont D) -> Fam D -> Set
  ix (eta (S , P)) (U , T) = (S ◃ P) U
  ix (sigma R f) P = Σ[ x ∈ ix R P ] (ix (f (dx R P x)) P)
  ix (π A f) P = (a : A) -> ix (f a) P

  dx : {D : Set₁} -> (X : IRCont D) -> (P : Fam D) -> ix X P -> IRPos X
  dx (eta (S , P)) (U , T) = ◃-map S P T
  dx (sigma R f) P (x , p) = dx R P x , dx (f (dx R P x)) P p
  dx (π A f) P g = λ a → dx (f a) P (g a)


⟦_⟧ : {D E : Set₁} -> IR D E -> Fam D -> Fam E
⟦ X , f ⟧ P = Fam-map f (ix X P , dx X P)