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)