module Polynomial.Container.Equivalence where

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

open import Polynomial.IR
import Polynomial.Container.IR as Cont

-- maps back and forth on codes

-- The codes are the same, except the Container version has bundled up
-- idPN and con into a container

mutual
  IRContToPoly : {D : Set1} -> Cont.IRCont D -> Poly D
  IRContToPoly (Cont.eta (S , P))
     = sigma (con S) (λ {(lift s) → pi (P s) (λ _ → idPN) })
  IRContToPoly (Cont.sigma R f)
     = sigma (IRContToPoly R) (λ x → IRContToPoly (f (InfoToIRPos R x)))
  IRContToPoly (Cont.π A f) = pi A (λ x → IRContToPoly (f x))

  InfoToIRPos : ∀ {D} -> (x : Cont.IRCont D) ->
                Info (IRContToPoly x) -> Cont.IRPos x
  InfoToIRPos (Cont.eta (S , P)) (lift s , f) = s , f
  InfoToIRPos (Cont.sigma R f) (x , y)
     = InfoToIRPos R x , InfoToIRPos (f (InfoToIRPos R x)) y
  InfoToIRPos (Cont.π A f) g = λ a → InfoToIRPos (f a) (g a)

ConttoPoly : {D E : Set1} -> Cont.IR D E -> IR D E
ConttoPoly (c , α) = IRContToPoly c , α ∘ (InfoToIRPos c)

mutual

  PolyToIRCont : {D : Set1} -> Poly D -> Cont.IRCont D
  PolyToIRCont idPN = Cont.eta (⊤ , (λ _ → ⊤))
  PolyToIRCont (con A) = Cont.con A
  PolyToIRCont (sigma R f)
    = Cont.sigma (PolyToIRCont R) (λ x → PolyToIRCont (f (IRPosToInfo R x)))
  PolyToIRCont (pi A f) = Cont.π A (λ a → PolyToIRCont (f a))

  IRPosToInfo : ∀ {D} -> (x : Poly D) ->
                Cont.IRPos (PolyToIRCont x) -> Info x
  IRPosToInfo idPN (_ , d) = d tt
  IRPosToInfo (con A) (a , _) = lift a
  IRPosToInfo (sigma S T) (x , y)
    = (IRPosToInfo S x) , (IRPosToInfo (T (IRPosToInfo S x)) y)
  IRPosToInfo (pi A T) f = λ a → IRPosToInfo (T a) (f a)


PolytoCont : {D E : Set1} -> IR D E -> Cont.IR D E
PolytoCont (F , α) = PolyToIRCont F , α ∘ IRPosToInfo F