module Generic.Family where

open import Generic.Core

record GenericFamily {ℓ} (U : AtomUniverse ℓ) : Type (ℓ-suc ℓ) where
  constructor genericFamily
  field
    typeCount       : ℕ
    Carrier         : Fin typeCount → Type ℓ
    desc            : Fin typeCount → TyDesc U typeCount
    typeNames       : Fin typeCount → String
    constructorNames : Fin typeCount → List String

    encodeAt : (i : Fin typeCount) → Carrier i → CodeIx U desc (desc i)
    decodeAt : (i : Fin typeCount) → CodeIx U desc (desc i) → Carrier i

    decode-encodeAt : (i : Fin typeCount) → (x : Carrier i) →
                      decodeAt i (encodeAt i x) ≡ x
    encode-decodeAt : (i : Fin typeCount) → (x : CodeIx U desc (desc i)) →
                      encodeAt i (decodeAt i x) ≡ x

  isoAt : (i : Fin typeCount) → Iso (Carrier i) (CodeIx U desc (desc i))
  isoAt i = iso (encodeAt i) (decodeAt i) (encode-decodeAt i) (decode-encodeAt i)

open GenericFamily public

genericAt : ∀ {ℓ} {U : AtomUniverse ℓ} →
            (family : GenericFamily U) →
            (i : Fin (GenericFamily.typeCount family)) →
            Generic U (GenericFamily.Carrier family i)
genericAt family i =
  generic
    (GenericFamily.typeCount family)
    (GenericFamily.desc family)
    (rootData i)
    (GenericFamily.typeNames family)
    (GenericFamily.constructorNames family)
    (λ x → rootDataIx (GenericFamily.encodeAt family i x))
    (λ { (rootDataIx x) → GenericFamily.decodeAt family i x })
    (GenericFamily.decode-encodeAt family i)
    (λ { (rootDataIx x) → cong rootDataIx (GenericFamily.encode-decodeAt family i x) })