module Generic.Core where

open import Generic.Base public

infixr  _∷ⁱ_

record AtomUniverse (ℓ : Level) : Type (ℓ-suc ℓ) where
  constructor atomUniverse
  field
    AtomCode : Type₀
    Atom     : AtomCode → Type ℓ

open AtomUniverse public

data FieldDesc {ℓ} (U : AtomUniverse ℓ) (n : ℕ) : Type₀ where
  fieldRec  : Fin n → FieldDesc U n
  fieldAtom : AtomCode U → FieldDesc U n

data ConDesc {ℓ} (U : AtomUniverse ℓ) (n : ℕ) : Type₀ where
  con : List (FieldDesc U n) → ConDesc U n

data TyDesc {ℓ} (U : AtomUniverse ℓ) (n : ℕ) : Type₀ where
  dataD : List (ConDesc U n) → TyDesc U n

constructorsOf : ∀ {ℓ n} {U : AtomUniverse ℓ} → TyDesc U n → List (ConDesc U n)
constructorsOf (dataD cs) = cs

data RootDesc {ℓ} (U : AtomUniverse ℓ) (n : ℕ) : Type₀ where
  rootData : Fin n → RootDesc U n
  rootAtom : AtomCode U → RootDesc U n

pattern μ i = fieldRec i
pattern α a = fieldAtom a

pattern κ₀ = con []
pattern κ₁ a = con (a ∷ [])
pattern κ₂ a b = con (a ∷ b ∷ [])
pattern κ₃ a b c = con (a ∷ b ∷ c ∷ [])
pattern κ₄ a b c d = con (a ∷ b ∷ c ∷ d ∷ [])
pattern κ₅ a b c d e = con (a ∷ b ∷ c ∷ d ∷ e ∷ [])

data ListIx {ℓ} {A : Type ℓ} : List A → Type ℓ where
  here  : ∀ {x xs} → ListIx (x ∷ xs)
  there : ∀ {x xs} → ListIx xs → ListIx (x ∷ xs)

lookup : ∀ {ℓ} {A : Type ℓ} {xs : List A} → ListIx xs → A
lookup (here {x = x}) = x
lookup (there i) = lookup i

pattern ι₀ = here
pattern ι₁ = there ι₀
pattern ι₂ = there ι₁
pattern ι₃ = there ι₂
pattern ι₄ = there ι₃
pattern ι₅ = there ι₄
pattern ι₆ = there ι₅
pattern ι₇ = there ι₆
pattern ι₈ = there ι₇
pattern ι₉ = there ι₈

mutual
  data CodeIx {ℓ n} (U : AtomUniverse ℓ) (D : Fin n → TyDesc U n) : TyDesc U n → Type ℓ where
    nodeIx : ∀ {cs} (c : ListIx cs) → ArgsCodeIx U D (lookup c) → CodeIx U D (dataD cs)

  data FieldCodeIx {ℓ n} (U : AtomUniverse ℓ) (D : Fin n → TyDesc U n) : FieldDesc U n → Type ℓ where
    recIx  : ∀ {i} → CodeIx U D (D i) → FieldCodeIx U D (fieldRec i)
    atomIx : ∀ {a} → Atom U a → FieldCodeIx U D (fieldAtom a)

  data ArgsCodeIx {ℓ n} (U : AtomUniverse ℓ) (D : Fin n → TyDesc U n) : ConDesc U n → Type ℓ where
    []ⁱ  : ArgsCodeIx U D (con [])
    _∷ⁱ_ : ∀ {f fs} → FieldCodeIx U D f → ArgsCodeIx U D (con fs) → ArgsCodeIx U D (con (f ∷ fs))

data RootCodeIx {ℓ n} (U : AtomUniverse ℓ) (D : Fin n → TyDesc U n) : RootDesc U n → Type ℓ where
  rootDataIx : ∀ {i} → CodeIx U D (D i) → RootCodeIx U D (rootData i)
  rootAtomIx : ∀ {a} → Atom U a → RootCodeIx U D (rootAtom a)

pattern ν₀ c = nodeIx c []ⁱ
pattern ν₁ c a = nodeIx c (a ∷ⁱ []ⁱ)
pattern ν₂ c a b = nodeIx c (a ∷ⁱ b ∷ⁱ []ⁱ)
pattern ν₃ c a b d = nodeIx c (a ∷ⁱ b ∷ⁱ d ∷ⁱ []ⁱ)
pattern ν₄ c a b d e = nodeIx c (a ∷ⁱ b ∷ⁱ d ∷ⁱ e ∷ⁱ []ⁱ)
pattern ν₅ c a b d e f = nodeIx c (a ∷ⁱ b ∷ⁱ d ∷ⁱ e ∷ⁱ f ∷ⁱ []ⁱ)

record Generic {ℓ} (U : AtomUniverse ℓ) (A : Type ℓ) : Type (ℓ-suc ℓ) where
  constructor generic
  field
    typeCount : ℕ
    desc      : Fin typeCount → TyDesc U typeCount
    root      : RootDesc U typeCount
    typeNames : Fin typeCount → String
    constructorNames : Fin typeCount → List String

    encode : A → RootCodeIx U desc root
    decode : RootCodeIx U desc root → A

    decode-encode : (x : A) → decode (encode x) ≡ x
    encode-decode : (x : RootCodeIx U desc root) → encode (decode x) ≡ x

  asIso : Iso A (RootCodeIx U desc root)
  asIso = iso encode decode encode-decode decode-encode

  encode-injective : ∀ {x y} → encode x ≡ encode y → x ≡ y
  encode-injective {x} {y} p =
    sym (decode-encode x) ∙ cong decode p ∙ decode-encode y

  decode-injective : ∀ {x y} → decode x ≡ decode y → x ≡ y
  decode-injective {x} {y} p =
    sym (encode-decode x) ∙ cong encode p ∙ encode-decode y

  encode-preimage : (x : RootCodeIx U desc root) → Σ[ y ∈ A ] encode y ≡ x
  encode-preimage x = decode x , encode-decode x

  decode-preimage : (x : A) → Σ[ y ∈ RootCodeIx U desc root ] decode y ≡ x
  decode-preimage x = encode x , decode-encode x

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

singletonAtomUniverse : ∀ {ℓ} → Type ℓ → AtomUniverse ℓ
singletonAtomUniverse A = atomUniverse Unit (λ _ → A)

data BuiltinAtomCode : Type₀ where
  natAtom stringAtom boolAtom unitAtom : BuiltinAtomCode

BuiltinAtom : BuiltinAtomCode → Type₀
BuiltinAtom natAtom = ℕ
BuiltinAtom stringAtom = String
BuiltinAtom boolAtom = Bool
BuiltinAtom unitAtom = Unit

BuiltinAtoms : AtomUniverse ℓ-zero
BuiltinAtoms = atomUniverse BuiltinAtomCode BuiltinAtom

atomicGeneric : ∀ {ℓ} (U : AtomUniverse ℓ) (a : AtomCode U) → Generic U (Atom U a)
atomicGeneric U a =
  generic
    zero
    (λ ())
    (rootAtom a)
    (λ ())
    (λ ())
    (λ x → rootAtomIx x)
    (λ { (rootAtomIx x) → x })
    (λ _ → refl)
    (λ { (rootAtomIx _) → refl })

inferAtomicGeneric : ∀ {ℓ} {A : Type ℓ} → InferredGeneric A
inferAtomicGeneric {A = A} = singletonAtomUniverse A , atomicGeneric (singletonAtomUniverse A) tt

withAtomUniverse : ∀ {ℓ} (U : AtomUniverse ℓ) {A : Type ℓ} → Generic U A → Generic U A
withAtomUniverse U g = g