{-# OPTIONS --safe --with-K #-}

module Generics.SimpleContainer where

open import Prelude
open import Prelude.Sum as Sum
open import Generics.Telescope
open import Generics.Description

private variable
  cb  : ConB
  cbs : ConBs

SCᵇ : ConB  Set
SCᵇ = All Sum.[ const Bool , const  ]

scConB : Level  (cb : ConB)  SCᵇ cb  ConB
scConB  []            _           = []
scConB  (inl ℓ'  cb) (false  s) = inl ℓ'  scConB  cb s
scConB  (inl ℓ'  cb) (true   s) = inl ℓ'  inl   scConB  cb s
scConB  (inr rb  cb) (_      s) = inr rb  scConB  cb s

hasEl? : Level  (cb : ConB)  SCᵇ cb  Level
hasEl?  []           _           = lzero
hasEl?  (inl _  cb) (false  s) = hasEl?  cb s
hasEl?  (inl _  cb) (true   s) =   hasEl?  cb s
hasEl?  (inr _  cb) (_      s) = hasEl?  cb s

hasEl?-bound : ( : Level) (cb : ConB) (sb : SCᵇ cb) {ℓ' : Level}
                ℓ'  hasEl?  cb sb  ℓ'
hasEl?-bound  []           []           ℓ⊑ℓ' = refl
hasEl?-bound  (inl _  cb) (false  sb) ℓ⊑ℓ' = hasEl?-bound  cb sb ℓ⊑ℓ'
hasEl?-bound  (inl _  cb) (true   sb) ℓ⊑ℓ' = trans (cong ( ⊔_)
                                               (hasEl?-bound  cb sb ℓ⊑ℓ')) ℓ⊑ℓ'
hasEl?-bound  (inr _  cb) (_      sb) ℓ⊑ℓ' = hasEl?-bound  cb sb ℓ⊑ℓ'

hasEl?-dist-⊔ : ( ℓ' : Level) (cb : ConB) (sb : SCᵇ cb)
               hasEl? (  ℓ') cb sb  hasEl?  cb sb  hasEl? ℓ' cb sb
hasEl?-dist-⊔  ℓ' []           []           = refl
hasEl?-dist-⊔  ℓ' (inl _  cb) (false  sb) = hasEl?-dist-⊔  ℓ' cb sb
hasEl?-dist-⊔  ℓ' (inl _  cb) (true   sb) = cong (  ℓ' ⊔_) (hasEl?-dist-⊔  ℓ' cb sb)
hasEl?-dist-⊔  ℓ' (inr _  cb) (_      sb) = hasEl?-dist-⊔  ℓ' cb sb

SCᶜ : {I : Set ℓⁱ} (D : ConD I cb)  SCᵇ cb  Set   Setω
SCᶜ (ι i  ) _           X = Liftω 
SCᶜ (σ A D) (false  s) X = (a : A)  SCᶜ (D a) s X
SCᶜ (σ A D) (true   s) X = Σωω[ _  (_ ,ℓ A) ≡ω ((_ ,ℓ X) ⦂ω Σℓ[  ] Set ) ]
                           ((a : A)  SCᶜ (D a) s X)
SCᶜ (ρ D E) (_      s) X = SCᶜ E s X

SCᶜˢ : {I : Set ℓⁱ}  ConDs I cbs  All SCᵇ cbs  Set ℓᵉ  Setω
SCᶜˢ []            ss  E = Liftω 
SCᶜˢ (D  Ds) (s  ss) E = Σωω[ _  SCᶜ D s E ] SCᶜˢ Ds ss E

record SC (D : PDataD) : Setω where
  field
    {elevel} : Level
    El  :  PDataD.Param D ⟧ᵗ  Set elevel
    pos : All SCᵇ (PDataD.struct D)
    coe : (ps :  PDataD.Param D ⟧ᵗ)  SCᶜˢ (PDataD.applyP D ps) pos (El ps)

SCᵈ : DataD  Setω
SCᵈ D =  {ℓs}  SC (DataD.applyL D ℓs)