Chapter6.EnumU

module Chapter6.EnumU where

open import Level 
  renaming ( zero to zeroL 
           ; suc to sucL )

open import Data.Unit
open import Data.Nat
open import Data.Fin hiding (lift)
open import Data.Product
open import Data.String

open import Chapter4.Desc
open import Chapter4.Desc.Fixpoint

UId = String

EnumUD : ∀{ℓ} → Desc ℓ
EnumUD = `Σ (Lift (Fin 2)) λ { (lift zero) → `1 
                      ; (lift (suc zero)) → `Σ (Lift UId) λ _ → `var `× `1 
                      ; (lift (suc (suc ()))) }

EnumU : ∀{ℓ} → Set ℓ
EnumU {ℓ} = μ (EnumUD {ℓ})

nilE : ∀{ℓ} → EnumU {ℓ}
nilE = ⟨ lift zero , lift tt ⟩

consE : ∀{ℓ} → UId → EnumU {ℓ} → EnumU {ℓ}
consE t e = ⟨ lift (suc zero) , lift t , e , lift tt ⟩

data EnumT {ℓ : Level} : EnumU {ℓ} → Set ℓ where
  ze : ∀{t e} → EnumT (consE t e)
  su : ∀{t e} → EnumT e → EnumT (consE t e)