module Uniform.IR where

open import Prelude.Basic

open import Prelude.Equality

open import Prelude.Fam
open import Prelude.Container


mutual
  data Uni (D : Set1) : Set1 where
    ι : Uni D
    σ : (G : Uni D)-> (Info G -> Set) -> Uni D
    δ : (G : Uni D)-> (Info G -> Set) -> Uni D

  Info : {D : Set1} -> Uni D -> Set1
  Info ι = Lift ⊤
  Info (σ G A) = Σ[ γ ∈ (Info G) ] (A γ)
  Info {D} (δ G A) = Σ[ γ ∈ (Info G) ] (A γ → D)   -- (Info G <| A) D

{- IR codes, uniform style. -}

UF : ∀ {a} → Set₁ -> Set a -> Set (a ⊔ lsuc lzero)
UF D E = (Uni D ◃ Info) E

UF-map : ∀ {a} → {I : Set₁}{O O' : Set a} -> (O -> O') -> UF I O -> UF I O'
UF-map g = ◃-map _ _ g -- UF-map g (c , α) = (c , g ∘ α)


{- Decoding of uniform IR codes -}

mutual

  ⟦_⟧Uni : {I : Set1}->(G : Uni I)-> Fam I -> Set
  ⟦ ι ⟧Uni Z = ⊤
  ⟦ σ G S ⟧Uni Z = Σ (⟦ G ⟧Uni Z) (S ∘ ⟦ G ⟧Info Z)
  ⟦ δ G S ⟧Uni Z = Σ[ x ∈ (⟦ G ⟧Uni Z)] (S (⟦ G ⟧Info Z x) -> ind Z)

  ⟦_⟧Info : {I : Set1}-> (c : Uni I)-> (Z : Fam I) -> ⟦ c ⟧Uni Z -> Info c
  ⟦ ι ⟧Info UT _ = lift tt
  ⟦ σ G S ⟧Info UT (x , a) = (⟦ G ⟧Info UT x , a)
  ⟦ δ G S ⟧Info UT (x , g) = (⟦ G ⟧Info UT x , fib UT ∘ g)

⟦_⟧ : {D E : Set1} -> UF D E -> Fam D -> Fam E
⟦ G , k ⟧ Z = Fam-map k (⟦ G ⟧Uni Z , ⟦ G ⟧Info Z)

⟦_⟧₀ : {D E : Set1}-> UF D E -> Fam D -> Set
⟦ c ⟧₀ Z = ind (⟦ c ⟧ Z)

⟦_⟧₁ : {D E : Set1}-> (γ : UF D E) -> (Z : Fam D) ->  ⟦ γ ⟧₀ Z -> E
⟦ c ⟧₁ Z = fib (⟦ c ⟧ Z)