module Generic.Certified where

open import Generic.Core
open import Generic.Family

infixr  _∷ⁿ_

data ConstructorNamesFit {ℓ n} {U : AtomUniverse ℓ} :
                         List (ConDesc U n) → List String → Type₀ where
  []ⁿ   : ConstructorNamesFit [] []
  _∷ⁿ_ : ∀ {c cs name names} →
          ConstructorNamesFit cs names →
          ConstructorNamesFit (c ∷ cs) (name ∷ names)

constructorNameFromFit : ∀ {ℓ n} {U : AtomUniverse ℓ}
                         {cs : List (ConDesc U n)} {names : List String} →
                         ConstructorNamesFit cs names → ListIx cs → String
constructorNameFromFit (_∷ⁿ_ {name = name} fit) here = name
constructorNameFromFit (_∷ⁿ_ fit) (there i) = constructorNameFromFit fit i

record CertifiedGeneric {ℓ} (U : AtomUniverse ℓ) (A : Type ℓ) : Type (ℓ-suc ℓ) where
  constructor certifiedGeneric
  field
    base : Generic U A
    constructorNames-fit :
      (i : Fin (Generic.typeCount base)) →
      ConstructorNamesFit
        (constructorsOf (Generic.desc base i))
        (Generic.constructorNames base i)

  constructorName :
    (i : Fin (Generic.typeCount base)) →
    ListIx (constructorsOf (Generic.desc base i)) → String
  constructorName i = constructorNameFromFit (constructorNames-fit i)

open CertifiedGeneric public

forgetCertified : ∀ {ℓ} {U : AtomUniverse ℓ} {A : Type ℓ} →
                  CertifiedGeneric U A → Generic U A
forgetCertified = base

InferredCertifiedGeneric : ∀ {ℓ} → Type ℓ → Type (ℓ-suc ℓ)
InferredCertifiedGeneric {ℓ} A = Σ[ U ∈ AtomUniverse ℓ ] CertifiedGeneric U A

certifiedAtomicGeneric : ∀ {ℓ} (U : AtomUniverse ℓ) (a : AtomCode U) →
                         CertifiedGeneric U (Atom U a)
certifiedAtomicGeneric U a = certifiedGeneric (atomicGeneric U a) (λ ())

record CertifiedFamily {ℓ} (U : AtomUniverse ℓ) : Type (ℓ-suc ℓ) where
  constructor certifiedFamily
  field
    family : GenericFamily U
    constructorNames-fit :
      (i : Fin (GenericFamily.typeCount family)) →
      ConstructorNamesFit
        (constructorsOf (GenericFamily.desc family i))
        (GenericFamily.constructorNames family i)

open CertifiedFamily public

forgetCertifiedFamily : ∀ {ℓ} {U : AtomUniverse ℓ} →
                        CertifiedFamily U → GenericFamily U
forgetCertifiedFamily = family

certifiedAt : ∀ {ℓ} {U : AtomUniverse ℓ} →
              (certified : CertifiedFamily U) →
              (i : Fin (GenericFamily.typeCount (CertifiedFamily.family certified))) →
              CertifiedGeneric U
                (GenericFamily.Carrier (CertifiedFamily.family certified) i)
certifiedAt certified i =
  certifiedGeneric
    (genericAt (CertifiedFamily.family certified) i)
    (CertifiedFamily.constructorNames-fit certified)