module Generic.Macro.Family where

open import Generic.Core
open import Generic.Macro
open import Generic.Family
open import Generic.Certified

import Agda.Builtin.Reflection as R
open import Agda.Builtin.Bool using (Bool; true; false)

-- Recursive-family derivation for the safe part of the library.
--
-- `Generic.Macro` handles a single non-recursive type by constructing a
-- `Generic` record whose proofs are all `refl`. This module handles finite
-- families of datatypes. The macro first turns each constructor field into
-- either an atom field or a recursive reference to another type in the same
-- finite family, then declares mutually recursive helper functions for
-- encode/decode and for the two roundtrip proofs.

data MaybeNat : Type₀ where
  noNat   : MaybeNat
  justNat : ℕ → MaybeNat

data MaybeName : Type₀ where
  noName   : MaybeName
  justName : R.Name → MaybeName

data FamilyField : Type₀ where
  atomField : R.Term → FamilyField
  recField  : ℕ → R.Term → FamilyField

familyFieldType : FamilyField → R.Term
familyFieldType (atomField t) = t
familyFieldType (recField _ t) = t

record FamilyCtor : Type₀ where
  constructor familyCtor
  field
    familyCtorName   : R.Name
    familyCtorFields : List FamilyField

open FamilyCtor

record FamilyType : Type₀ where
  constructor familyType
  field
    familyTypeName  : R.Name
    familyTypeIndex : ℕ
    familyCtors     : List FamilyCtor

open FamilyType

termName : R.Term → MaybeName
termName (R.def f []) = justName f
termName (R.con f []) = justName f
termName _ = noName

findNameIndexFrom : ℕ → List R.Name → R.Name → MaybeNat
findNameIndexFrom i [] name = noNat
findNameIndexFrom i (x ∷ xs) name with R.primQNameEquality x name
... | true = justNat i
... | false = findNameIndexFrom (suc i) xs name

findFamilyIndex : List R.Name → R.Term → MaybeNat
findFamilyIndex family t with termName t
... | noName = noNat
... | justName name = findNameIndexFrom zero family name

familyFieldInfo : List R.Name → R.Term → R.TC FamilyField
familyFieldInfo family fieldTy =
  R.reduce fieldTy >>= λ reduced →
  choose (findFamilyIndex family reduced)
  where
  choose : MaybeNat → R.TC FamilyField
  choose noNat = R.returnTC (atomField fieldTy)
  choose (justNat i) = R.returnTC (recField i fieldTy)

collectFamilyFields : ℕ → List R.Name → R.Name → R.Name → List FamilyField → R.Term → R.TC FamilyCtor
collectFamilyFields zero family ty c fields _ =
  R.typeError
    ( R.strErr "deriveGenericFamilyIn: out of fuel while reading constructor type: "
    ∷ R.nameErr c ∷ [] )
collectFamilyFields (suc fuel) family ty c fields
  (R.pi (R.arg (R.arg-info R.visible _) fieldTy) (R.abs _ body)) =
  familyFieldInfo family fieldTy >>= λ f →
  collectFamilyFields fuel family ty c (fields ++ [ f ]) body
collectFamilyFields (suc fuel) family ty c fields (R.pi _ _) =
  R.typeError
    ( R.strErr "deriveGenericFamilyIn: hidden or instance constructor fields are not supported: "
    ∷ R.nameErr c ∷ [] )
collectFamilyFields (suc fuel) family ty c fields result with termName result
... | justName resultName with R.primQNameEquality ty resultName
...   | true = R.returnTC (familyCtor c fields)
...   | false =
  R.typeError
    ( R.strErr "deriveGenericFamilyIn: constructor result is not the datatype itself: "
    ∷ R.nameErr c ∷ [] )
collectFamilyFields (suc fuel) family ty c fields result | noName =
  R.typeError
    ( R.strErr "deriveGenericFamilyIn: constructor result is not the datatype itself: "
    ∷ R.nameErr c ∷ [] )

familyConstructorInfo : List R.Name → R.Name → R.Name → R.TC FamilyCtor
familyConstructorInfo family ty c =
  R.getType c >>= λ cTy →
  R.reduce cTy >>= λ reducedCTy →
  collectFamilyFields macroFuel family ty c [] reducedCTy

familyConstructorInfos : List R.Name → R.Name → List R.Name → R.TC (List FamilyCtor)
familyConstructorInfos family ty [] = R.returnTC []
familyConstructorInfos family ty (c ∷ cs) =
  familyConstructorInfo family ty c >>= λ i →
  familyConstructorInfos family ty cs >>= λ is →
  R.returnTC (i ∷ is)

familyTypeInfo : List R.Name → ℕ → R.Name → R.TC FamilyType
familyTypeInfo family i ty =
  ensureNonIndexedType ty >>
  R.getDefinition ty >>= λ
    { (R.data-type zero cs) →
        familyConstructorInfos family ty cs >>= λ infos →
        R.returnTC (familyType ty i infos)
    ; (R.data-type (suc _) _) →
        R.typeError (R.strErr "deriveGenericFamilyIn: parameterized datatypes are not supported" ∷ R.nameErr ty ∷ [])
    ; _ →
        R.typeError (R.strErr "deriveGenericFamilyIn: expected a datatype" ∷ R.nameErr ty ∷ [])
    }

familyTypeInfosFrom : List R.Name → ℕ → List R.Name → R.TC (List FamilyType)
familyTypeInfosFrom family i [] = R.returnTC []
familyTypeInfosFrom family i (ty ∷ tys) =
  familyTypeInfo family i ty >>= λ info →
  familyTypeInfosFrom family (suc i) tys >>= λ infos →
  R.returnTC (info ∷ infos)

familyTypeInfos : List R.Name → R.TC (List FamilyType)
familyTypeInfos family = familyTypeInfosFrom family zero family

-- A `FamilyType` is still only a compact analysis result. The next block turns
-- it into actual reflected terms for `TyDesc`, type names, constructor names,
-- and clauses indexed by `Fin typeCount`.
familyFieldDescTerm : FamilyField → R.Term
familyFieldDescTerm (atomField _) =
  R.con (quote fieldAtom) (varg R.unknown ∷ [])
familyFieldDescTerm (recField i _) =
  R.con (quote fieldRec) (varg (finTerm i) ∷ [])

familyFieldDescTerms : List FamilyField → List R.Term
familyFieldDescTerms [] = []
familyFieldDescTerms (f ∷ fs) = familyFieldDescTerm f ∷ familyFieldDescTerms fs

familyConDescTerm : FamilyCtor → R.Term
familyConDescTerm c =
  R.con (quote con) (varg (termList (familyFieldDescTerms (familyCtorFields c))) ∷ [])

familyConDescTerms : List FamilyCtor → List R.Term
familyConDescTerms [] = []
familyConDescTerms (c ∷ cs) = familyConDescTerm c ∷ familyConDescTerms cs

familyDescClause : FamilyType → R.Clause
familyDescClause info =
  R.clause []
    (varg (finPattern (familyTypeIndex info)) ∷ [])
    (R.con (quote dataD) (varg (termList (familyConDescTerms (familyCtors info))) ∷ []))

familyDescClauses : List FamilyType → List R.Clause
familyDescClauses [] = []
familyDescClauses (i ∷ is) = familyDescClause i ∷ familyDescClauses is

familyConstructorNameTerms : List FamilyCtor → List R.Term
familyConstructorNameTerms [] = []
familyConstructorNameTerms (c ∷ cs) =
  R.lit (R.string (R.primShowQName (familyCtorName c))) ∷ familyConstructorNameTerms cs

familyConstructorNamesClause : FamilyType → R.Clause
familyConstructorNamesClause info =
  R.clause []
    (varg (finPattern (familyTypeIndex info)) ∷ [])
    (termList (familyConstructorNameTerms (familyCtors info)))

familyConstructorNamesClauses : List FamilyType → List R.Clause
familyConstructorNamesClauses [] = []
familyConstructorNamesClauses (i ∷ is) =
  familyConstructorNamesClause i ∷ familyConstructorNamesClauses is

familyTypeNameClause : FamilyType → R.Clause
familyTypeNameClause info =
  R.clause []
    (varg (finPattern (familyTypeIndex info)) ∷ [])
    (R.lit (R.string (R.primShowQName (familyTypeName info))))

familyTypeNameClauses : List FamilyType → List R.Clause
familyTypeNameClauses [] = []
familyTypeNameClauses (i ∷ is) = familyTypeNameClause i ∷ familyTypeNameClauses is

familyCarrierClause : FamilyType → R.Clause
familyCarrierClause info =
  R.clause []
    (varg (finPattern (familyTypeIndex info)) ∷ [])
    (R.def (familyTypeName info) [])

familyCarrierClauses : List FamilyType → List R.Clause
familyCarrierClauses [] = []
familyCarrierClauses (i ∷ is) = familyCarrierClause i ∷ familyCarrierClauses is

familyConstructorNamesFitTerm : List FamilyCtor → R.Term
familyConstructorNamesFitTerm [] = R.con (quote []ⁿ) []
familyConstructorNamesFitTerm (_ ∷ cs) =
  R.con (quote _∷ⁿ_) (varg (familyConstructorNamesFitTerm cs) ∷ [])

familyConstructorNamesFitClause : FamilyType → R.Clause
familyConstructorNamesFitClause info =
  R.clause []
    (varg (finPattern (familyTypeIndex info)) ∷ [])
    (familyConstructorNamesFitTerm (familyCtors info))

familyConstructorNamesFitClauses : List FamilyType → List R.Clause
familyConstructorNamesFitClauses [] = []
familyConstructorNamesFitClauses (i ∷ is) =
  familyConstructorNamesFitClause i ∷ familyConstructorNamesFitClauses is

familyFieldTypes : List FamilyField → List R.Term
familyFieldTypes [] = []
familyFieldTypes (f ∷ fs) = familyFieldType f ∷ familyFieldTypes fs

familyTeleFromFields : List FamilyField → R.Telescope
familyTeleFromFields [] = []
familyTeleFromFields (f ∷ fs) =
  ("x" , varg (familyFieldType f)) ∷ familyTeleFromFields fs

lookupName : List R.Name → ℕ → R.Name
lookupName (x ∷ xs) zero = x
lookupName (x ∷ xs) (suc i) = lookupName xs i
lookupName [] _ = quote refl

nameIn : R.Name → List R.Name → Bool
nameIn name [] = false
nameIn name (x ∷ xs) with R.primQNameEquality name x
... | true = true
... | false = nameIn name xs

enqueueFresh : List R.Name → List R.Name → R.Name → List R.Name
enqueueFresh visited queue name with nameIn name visited
... | true = queue
... | false with nameIn name queue
...   | true = queue
...   | false = queue ++ [ name ]

-- Encoding recursive fields calls the generated encoder for the referenced
-- family member and then wraps the result in `recIx`. Atomic fields are passed
-- through as `atomIx`. Decoding performs the inverse operation by calling the
-- corresponding generated decoder for recursive fields.
familyArgsCodeTerm : List R.Name → ℕ → List FamilyField → R.Term
familyArgsCodeTerm encs n [] = unitArgsTerm
familyArgsCodeTerm encs n (atomField _ ∷ fs) =
  R.con (quote _∷ⁱ_)
    ( varg (R.con (quote atomIx) (varg (R.var n []) ∷ []))
    ∷ varg (familyArgsCodeTerm encs (suc n) fs) ∷ [] )
familyArgsCodeTerm encs n (recField i _ ∷ fs) =
  R.con (quote _∷ⁱ_)
    ( varg (R.con (quote recIx)
      (varg (R.def (lookupName encs i) (varg (R.var n []) ∷ [])) ∷ []))
    ∷ varg (familyArgsCodeTerm encs (suc n) fs) ∷ [] )

familyArgsCodePattern : ℕ → List FamilyField → R.Pattern
familyArgsCodePattern n [] = unitArgsPattern
familyArgsCodePattern n (atomField _ ∷ fs) =
  R.con (quote _∷ⁱ_)
    ( varg (R.con (quote atomIx) (varg (R.var n) ∷ []))
    ∷ varg (familyArgsCodePattern (suc n) fs) ∷ [] )
familyArgsCodePattern n (recField _ _ ∷ fs) =
  R.con (quote _∷ⁱ_)
    ( varg (R.con (quote recIx) (varg (R.var n) ∷ []))
    ∷ varg (familyArgsCodePattern (suc n) fs) ∷ [] )

familyDecodeArgs : List R.Name → ℕ → List FamilyField → List (R.Arg R.Term)
familyDecodeArgs decs n [] = []
familyDecodeArgs decs n (atomField _ ∷ fs) =
  varg (R.var n []) ∷ familyDecodeArgs decs (suc n) fs
familyDecodeArgs decs n (recField i _ ∷ fs) =
  varg (R.def (lookupName decs i) (varg (R.var n []) ∷ []))
  ∷ familyDecodeArgs decs (suc n) fs

familyEncodeClause : List R.Name → ℕ → FamilyCtor → R.Clause
familyEncodeClause encs n c =
  R.clause
    (familyTeleFromFields (familyCtorFields c))
    (varg (R.con (familyCtorName c) (varPatternArgs zero (familyFieldTypes (familyCtorFields c)))) ∷ [])
    (R.con (quote nodeIx)
      (varg (listIxTerm n) ∷ varg (familyArgsCodeTerm encs zero (familyCtorFields c)) ∷ []))

familyEncodeClauses : List R.Name → ℕ → List FamilyCtor → List R.Clause
familyEncodeClauses encs n [] = []
familyEncodeClauses encs n (c ∷ cs) =
  familyEncodeClause encs n c ∷ familyEncodeClauses encs (suc n) cs

familyDecodeClause : List R.Name → ℕ → FamilyCtor → R.Clause
familyDecodeClause decs n c =
  R.clause
    (familyTeleFromFields (familyCtorFields c))
    (varg (R.con (quote nodeIx)
      (varg (listIxPattern n) ∷ varg (familyArgsCodePattern zero (familyCtorFields c)) ∷ []))
    ∷ [])
    (R.con (familyCtorName c) (familyDecodeArgs decs zero (familyCtorFields c)))

familyDecodeClauses : List R.Name → ℕ → List FamilyCtor → List R.Clause
familyDecodeClauses decs n [] = []
familyDecodeClauses decs n (c ∷ cs) =
  familyDecodeClause decs n c ∷ familyDecodeClauses decs (suc n) cs

-- The non-trivial part of the safe recursive macro is proof generation.
-- Instead of composing one `cong` per recursive field, we generate a Cubical
-- path lambda. At interval variable `i`, every recursive argument is replaced
-- by its recursive roundtrip proof applied to `i`; atom arguments stay fixed.
-- This works uniformly for zero, one, or many recursive fields in one
-- constructor.
decodeEncodeFieldAt : List R.Name → ℕ → FamilyField → R.Arg R.Term
decodeEncodeFieldAt des n (atomField _) = varg (R.var (suc n) [])
decodeEncodeFieldAt des n (recField i _) =
  varg (R.def (lookupName des i)
    (varg (R.var (suc n) []) ∷ varg (R.var zero []) ∷ []))

decodeEncodeFieldsAt : List R.Name → ℕ → List FamilyField → List (R.Arg R.Term)
decodeEncodeFieldsAt des n [] = []
decodeEncodeFieldsAt des n (f ∷ fs) =
  decodeEncodeFieldAt des n f ∷ decodeEncodeFieldsAt des (suc n) fs

decodeEncodeProofClause : List R.Name → FamilyCtor → R.Clause
decodeEncodeProofClause des c =
  R.clause
    (familyTeleFromFields (familyCtorFields c))
    (varg (R.con (familyCtorName c) (varPatternArgs zero (familyFieldTypes (familyCtorFields c)))) ∷ [])
    (R.lam R.visible
      (R.abs "i"
        (R.con (familyCtorName c)
          (decodeEncodeFieldsAt des zero (familyCtorFields c)))))

decodeEncodeProofClauses : List R.Name → List FamilyCtor → List R.Clause
decodeEncodeProofClauses des [] = []
decodeEncodeProofClauses des (c ∷ cs) =
  decodeEncodeProofClause des c ∷ decodeEncodeProofClauses des cs

encodeDecodeFieldAt : List R.Name → ℕ → FamilyField → R.Arg R.Term
encodeDecodeFieldAt eds n (atomField _) =
  varg (R.con (quote atomIx) (varg (R.var (suc n) []) ∷ []))
encodeDecodeFieldAt eds n (recField i _) =
  varg (R.con (quote recIx)
    (varg (R.def (lookupName eds i)
      (varg (R.var (suc n) []) ∷ varg (R.var zero []) ∷ []))
    ∷ []))

encodeDecodeFieldsAt : List R.Name → ℕ → List FamilyField → R.Term
encodeDecodeFieldsAt eds n [] = unitArgsTerm
encodeDecodeFieldsAt eds n (f ∷ fs) =
  R.con (quote _∷ⁱ_)
    (encodeDecodeFieldAt eds n f ∷ varg (encodeDecodeFieldsAt eds (suc n) fs) ∷ [])

encodeDecodeProofClause : List R.Name → ℕ → FamilyCtor → R.Clause
encodeDecodeProofClause eds conIx c =
  R.clause
    (familyTeleFromFields (familyCtorFields c))
    (varg (R.con (quote nodeIx)
      (varg (listIxPattern conIx) ∷ varg (familyArgsCodePattern zero (familyCtorFields c)) ∷ []))
    ∷ [])
    (R.lam R.visible
      (R.abs "i"
        (R.con (quote nodeIx)
          (varg (listIxTerm conIx)
          ∷ varg (encodeDecodeFieldsAt eds zero (familyCtorFields c)) ∷ []))))

encodeDecodeProofClauses : List R.Name → ℕ → List FamilyCtor → List R.Clause
encodeDecodeProofClauses eds n [] = []
encodeDecodeProofClauses eds n (c ∷ cs) =
  encodeDecodeProofClause eds n c ∷ encodeDecodeProofClauses eds (suc n) cs

finType : ℕ → R.Term
finType n = R.def (quote Fin) (varg (R.lit (R.nat n)) ∷ [])

tyDescTypeWith : R.Term → ℕ → R.Term
tyDescTypeWith atoms n = R.def (quote TyDesc) (varg atoms ∷ varg (R.lit (R.nat n)) ∷ [])

descTypeWith : R.Term → ℕ → R.Term
descTypeWith atoms n = R.pi (varg (finType n)) (R.abs "_" (tyDescTypeWith atoms n))

descAt : R.Name → ℕ → R.Term
descAt descName i = R.def descName (varg (finTerm i) ∷ [])

codeTypeWith : R.Term → R.Name → ℕ → R.Term
codeTypeWith atoms descName i =
  R.def (quote CodeIx)
    (varg atoms ∷ varg (R.def descName []) ∷ varg (descAt descName i) ∷ [])

arrowTerm : R.Term → R.Term → R.Term
arrowTerm a b = R.pi (varg a) (R.abs "_" b)

eqTypeTerm : R.Term → R.Term → R.Term
eqTypeTerm lhs rhs = R.def (quote _≡_) (varg lhs ∷ varg rhs ∷ [])

decodeEncodeProofType : R.Name → R.Name → FamilyType → R.Term
decodeEncodeProofType enc dec info =
  R.pi (varg (R.def (familyTypeName info) []))
    (R.abs "x"
      (eqTypeTerm
        (R.def dec (varg (R.def enc (varg (R.var zero []) ∷ [])) ∷ []))
        (R.var zero [])))

encodeDecodeProofType : R.Term → R.Name → R.Name → R.Name → FamilyType → R.Term
encodeDecodeProofType atoms descName enc dec info =
  R.pi (varg (codeTypeWith atoms descName (familyTypeIndex info)))
    (R.abs "x"
      (eqTypeTerm
        (R.def enc (varg (R.def dec (varg (R.var zero []) ∷ [])) ∷ []))
        (R.var zero [])))

-- All helper functions are declared before any one of them is defined. This is
-- the reflection-level analogue of a mutual block and is what lets, for
-- example, the encoder for type 0 call the encoder for type 1 and vice versa.
declareFamilyHelpers :
  R.Term → R.Name → List FamilyType → List R.Name → List R.Name → List R.Name → List R.Name → R.TC Unit
declareFamilyHelpers atoms descName [] [] [] [] [] = R.returnTC tt
declareFamilyHelpers atoms descName (info ∷ infos)
  (enc ∷ encs) (dec ∷ decs) (de ∷ des) (ed ∷ eds) =
  R.declareDef (varg enc)
    (arrowTerm (R.def (familyTypeName info) []) (codeTypeWith atoms descName (familyTypeIndex info))) >>
  R.declareDef (varg dec)
    (arrowTerm (codeTypeWith atoms descName (familyTypeIndex info)) (R.def (familyTypeName info) [])) >>
  R.declareDef (varg de) (decodeEncodeProofType enc dec info) >>
  R.declareDef (varg ed) (encodeDecodeProofType atoms descName enc dec info) >>
  declareFamilyHelpers atoms descName infos encs decs des eds
declareFamilyHelpers _ _ _ _ _ _ _ =
  R.typeError (R.strErr "deriveGenericFamilyIn: internal arity mismatch while declaring helpers" ∷ [])

defineFamilyHelpersFrom :
  List R.Name → List R.Name → List R.Name → List R.Name →
  List FamilyType → List R.Name → List R.Name → List R.Name → List R.Name → R.TC Unit
defineFamilyHelpersFrom allEncs allDecs allDEs allEDs [] [] [] [] [] = R.returnTC tt
defineFamilyHelpersFrom allEncs allDecs allDEs allEDs (info ∷ infos)
  (enc ∷ encs) (dec ∷ decs) (de ∷ des) (ed ∷ eds) =
  R.defineFun enc (familyEncodeClauses allEncs zero (familyCtors info)) >>
  R.defineFun dec (familyDecodeClauses allDecs zero (familyCtors info)) >>
  R.defineFun de (decodeEncodeProofClauses allDEs (familyCtors info)) >>
  R.defineFun ed (encodeDecodeProofClauses allEDs zero (familyCtors info)) >>
  defineFamilyHelpersFrom allEncs allDecs allDEs allEDs infos encs decs des eds
defineFamilyHelpersFrom _ _ _ _ _ _ _ _ _ =
  R.typeError (R.strErr "deriveGenericFamilyIn: internal arity mismatch while defining helpers" ∷ [])

defineFamilyHelpers :
  List FamilyType → List R.Name → List R.Name → List R.Name → List R.Name → R.TC Unit
defineFamilyHelpers infos encs decs des eds =
  defineFamilyHelpersFrom encs decs des eds infos encs decs des eds

freshNames : String → ℕ → R.TC (List R.Name)
freshNames prefix zero = R.returnTC []
freshNames prefix (suc n) =
  R.freshName prefix >>= λ x →
  freshNames prefix n >>= λ xs →
  R.returnTC (x ∷ xs)

lookupFamilyName : List R.Name → ℕ → R.Name
lookupFamilyName = lookupName

rootEncodeTermWith : R.Name → R.Term
rootEncodeTermWith enc =
  R.pat-lam
    (R.clause (("x" , varg R.unknown) ∷ [])
      (varg (R.var zero) ∷ [])
      (R.con (quote rootDataIx) (varg (R.def enc (varg (R.var zero []) ∷ [])) ∷ []))
    ∷ []) []

rootDecodeTermWith : R.Name → R.Term
rootDecodeTermWith dec =
  R.pat-lam
    (R.clause (("x" , varg R.unknown) ∷ [])
      (varg (R.con (quote rootDataIx) (varg (R.var zero) ∷ [])) ∷ [])
      (R.def dec (varg (R.var zero []) ∷ []))
    ∷ []) []

rootEncodeDecodeTermWith : R.Name → R.Term
rootEncodeDecodeTermWith ed =
  R.pat-lam
    (R.clause (("x" , varg R.unknown) ∷ [])
      (varg (R.con (quote rootDataIx) (varg (R.var zero) ∷ [])) ∷ [])
      (R.lam R.visible
        (R.abs "i"
          (R.con (quote rootDataIx)
            (varg (R.def ed (varg (R.var (suc zero) []) ∷ varg (R.var zero []) ∷ [])) ∷ []))))
    ∷ []) []

familyHelperClause : FamilyType → R.Name → R.Clause
familyHelperClause info helper =
  R.clause (("x" , varg R.unknown) ∷ [])
    ( varg (finPattern (familyTypeIndex info))
    ∷ varg (R.var zero)
    ∷ [] )
    (R.def helper (varg (R.var zero []) ∷ []))

familyHelperClauses : List FamilyType → List R.Name → List R.Clause
familyHelperClauses [] [] = []
familyHelperClauses (info ∷ infos) (helper ∷ helpers) =
  familyHelperClause info helper ∷ familyHelperClauses infos helpers
familyHelperClauses _ _ = []

familyHelperTerm : List FamilyType → List R.Name → R.Term
familyHelperTerm infos helpers =
  R.pat-lam (familyHelperClauses infos helpers) []

genericFamilyBundleTerm :
  ℕ → R.Name → List FamilyType →
  List R.Name → List R.Name → List R.Name → List R.Name → R.Term
genericFamilyBundleTerm count descName infos encs decs des eds =
  R.con (quote genericFamily)
    ( varg (R.lit (R.nat count))
    ∷ varg (R.pat-lam (familyCarrierClauses infos) [])
    ∷ varg (R.def descName [])
    ∷ varg (R.pat-lam (familyTypeNameClauses infos) [])
    ∷ varg (R.pat-lam (familyConstructorNamesClauses infos) [])
    ∷ varg (familyHelperTerm infos encs)
    ∷ varg (familyHelperTerm infos decs)
    ∷ varg (familyHelperTerm infos des)
    ∷ varg (familyHelperTerm infos eds)
    ∷ [] )

certifiedFamilyBundleTerm :
  ℕ → R.Name → List FamilyType →
  List R.Name → List R.Name → List R.Name → List R.Name → R.Term
certifiedFamilyBundleTerm count descName infos encs decs des eds =
  R.con (quote certifiedFamily)
    ( varg (genericFamilyBundleTerm count descName infos encs decs des eds)
    ∷ varg (R.pat-lam (familyConstructorNamesFitClauses infos) [])
    ∷ [] )

genericFamilyTerm :
  R.Term → ℕ → ℕ → R.Name → List FamilyType →
  List R.Name → List R.Name → List R.Name → List R.Name → R.Term
genericFamilyTerm atoms count rootIx descName infos encs decs des eds =
  R.con (quote generic)
    ( varg (R.lit (R.nat count))
    ∷ varg (R.def descName [])
    ∷ varg (R.con (quote rootData) (varg (finTerm rootIx) ∷ []))
    ∷ varg (R.pat-lam (familyTypeNameClauses infos) [])
    ∷ varg (R.pat-lam (familyConstructorNamesClauses infos) [])
    ∷ varg (rootEncodeTermWith (lookupFamilyName encs rootIx))
    ∷ varg (rootDecodeTermWith (lookupFamilyName decs rootIx))
    ∷ varg (R.def (lookupFamilyName des rootIx) [])
    ∷ varg (rootEncodeDecodeTermWith (lookupFamilyName eds rootIx))
    ∷ [] )

finishFamily :
  R.Term → List R.Name → R.Name → R.Term → R.Name → List FamilyType →
  List R.Name → List R.Name → List R.Name → List R.Name → MaybeNat → R.TC Unit
finishFamily atoms family root hole descName infos encs decs des eds noNat =
  R.typeError (R.strErr "deriveGenericFamilyIn: root type is not in family: " ∷ R.nameErr root ∷ [])
finishFamily atoms family root hole descName infos encs decs des eds (justNat rootIx) =
  R.noConstraints (R.unify hole (genericFamilyTerm atoms (length family) rootIx descName infos encs decs des eds))

buildGenericFamilyInTC :
  R.Term → List R.Name →
  (R.Name → List FamilyType →
   List R.Name → List R.Name → List R.Name → List R.Name → R.TC Unit) →
  R.TC Unit
buildGenericFamilyInTC atoms family finish =
  familyTypeInfos family >>= λ infos →
  R.freshName "generic-family-desc" >>= λ descName →
  freshNames "encode-helper" (length family) >>= λ encs →
  freshNames "decode-helper" (length family) >>= λ decs →
  freshNames "decode-encode-helper" (length family) >>= λ des →
  freshNames "encode-decode-helper" (length family) >>= λ eds →
  let count = length family in
  R.declareDef (varg descName) (descTypeWith atoms count) >>
  R.defineFun descName (familyDescClauses infos) >>
  declareFamilyHelpers atoms descName infos encs decs des eds >>
  defineFamilyHelpers infos encs decs des eds >>
  finish descName infos encs decs des eds

deriveGenericFamilyInTC : R.Term → List R.Name → R.Name → R.Term → R.TC Unit
deriveGenericFamilyInTC atoms family root hole =
  buildGenericFamilyInTC atoms family λ descName infos encs decs des eds →
  finishFamily atoms family root hole descName infos encs decs des eds
    (findFamilyIndex family (R.def root []))

deriveGenericFamilyBundleInTC : R.Term → List R.Name → R.Term → R.TC Unit
deriveGenericFamilyBundleInTC atoms family hole =
  buildGenericFamilyInTC atoms family λ descName infos encs decs des eds →
  R.noConstraints
    (R.unify hole
      (genericFamilyBundleTerm
        (length family) descName infos encs decs des eds))

deriveCertifiedGenericFamilyBundleInTC : R.Term → List R.Name → R.Term → R.TC Unit
deriveCertifiedGenericFamilyBundleInTC atoms family hole =
  buildGenericFamilyInTC atoms family λ descName infos encs decs des eds →
  R.noConstraints
    (R.unify hole
      (certifiedFamilyBundleTerm
        (length family) descName infos encs decs des eds))

finishCertifiedFamilyRoot :
  List R.Name → R.Name → R.Term → R.Name → List FamilyType →
  List R.Name → List R.Name → List R.Name → List R.Name → MaybeNat → R.TC Unit
finishCertifiedFamilyRoot family root hole descName infos encs decs des eds noNat =
  R.typeError (R.strErr "deriveCertifiedGenericFamilyIn: root type is not in family: " ∷ R.nameErr root ∷ [])
finishCertifiedFamilyRoot family root hole descName infos encs decs des eds (justNat rootIx) =
  R.noConstraints
    (R.unify hole
      (R.def (quote certifiedAt)
        ( varg
            (certifiedFamilyBundleTerm
              (length family) descName infos encs decs des eds)
        ∷ varg (finTerm rootIx)
        ∷ [] )))

deriveCertifiedGenericFamilyInTC :
  R.Term → List R.Name → R.Name → R.Term → R.TC Unit
deriveCertifiedGenericFamilyInTC atoms family root hole =
  buildGenericFamilyInTC atoms family λ descName infos encs decs des eds →
  finishCertifiedFamilyRoot family root hole descName infos encs decs des eds
    (findFamilyIndex family (R.def root []))

-- Reachable-family discovery needs to decide whether a field should remain
-- atomic or become another described datatype. The rule is atom-first: we ask
-- Agda whether `λ x → atomIx x` can be checked at a type whose codomain is
-- `FieldCodeIx atoms _ (fieldAtom _)`. Unknown atom codes are solved only
-- inside `runSpeculative`, so failed or successful probes do not leak metas
-- into the real macro invocation.
atomEncoderTerm : R.Term
atomEncoderTerm =
  R.lam R.visible
    (R.abs "x"
      (R.con (quote atomIx) (varg (R.var zero []) ∷ [])))

atomFieldCodeType : R.Term → R.Term
atomFieldCodeType atoms =
  R.def (quote FieldCodeIx)
    (varg atoms
    ∷ varg R.unknown
    ∷ varg (R.con (quote fieldAtom) (varg R.unknown ∷ []))
    ∷ [])

atomEncoderType : R.Term → R.Term → R.Term
atomEncoderType atoms fieldTy =
  arrowTerm fieldTy (atomFieldCodeType atoms)

canUseAtom : R.Term → R.Term → R.TC Bool
canUseAtom atoms fieldTy =
  R.runSpeculative
    (R.catchTC
      (R.noConstraints (R.checkType atomEncoderTerm (atomEncoderType atoms fieldTy)) >>
       R.returnTC (true , false))
      (R.returnTC (false , false)))

discoverField : R.Term → List R.Name → List R.Name → R.Name → R.Term → R.TC (List R.Name)
discoverField atoms visited queue c fieldTy =
  canUseAtom atoms fieldTy >>= λ
    { true → R.returnTC queue
    ; false →
        R.reduce fieldTy >>= λ reduced →
        discoverReduced reduced
    }
  where
  discoverReduced : R.Term → R.TC (List R.Name)
  discoverReduced reduced with termName reduced
  ... | noName =
    R.typeError
      ( R.strErr "deriveGenericReachableIn: field is neither an atom nor a named datatype: "
      ∷ R.nameErr c ∷ [] )
  ... | justName name =
    R.getDefinition name >>= λ
      { (R.data-type zero _) →
          R.returnTC (enqueueFresh visited queue name)
      ; (R.data-type (suc _) _) →
          R.typeError
            ( R.strErr "deriveGenericReachableIn: field expands to a parameterized datatype: "
            ∷ R.nameErr name ∷ [] )
      ; _ →
          R.typeError
            ( R.strErr "deriveGenericReachableIn: field is neither an atom nor a supported datatype: "
            ∷ R.nameErr name ∷ [] )
      }

-- Reachability is a local worklist algorithm, not persistent global macro
-- state. `visited` preserves the final family order, and `queue` contains
-- datatypes discovered from fields but not yet inspected. The same fuel value
-- bounds both constructor-telescope traversal and the breadth of discovery.
discoverConstructorFields :
  ℕ → R.Term → List R.Name → List R.Name → R.Name → R.Name → R.Term → R.TC (List R.Name)
discoverConstructorFields zero atoms visited queue ty c _ =
  R.typeError
    ( R.strErr "deriveGenericReachableIn: out of fuel while reading constructor type: "
    ∷ R.nameErr c ∷ [] )
discoverConstructorFields (suc fuel) atoms visited queue ty c
  (R.pi (R.arg (R.arg-info R.visible _) fieldTy) (R.abs _ body)) =
  discoverField atoms visited queue c fieldTy >>= λ queue' →
  discoverConstructorFields fuel atoms visited queue' ty c body
discoverConstructorFields (suc fuel) atoms visited queue ty c (R.pi _ _) =
  R.typeError
    ( R.strErr "deriveGenericReachableIn: hidden or instance constructor fields are not supported: "
    ∷ R.nameErr c ∷ [] )
discoverConstructorFields (suc fuel) atoms visited queue ty c result with termName result
... | justName resultName with R.primQNameEquality ty resultName
...   | true = R.returnTC queue
...   | false =
  R.typeError
    ( R.strErr "deriveGenericReachableIn: constructor result is not the datatype itself: "
    ∷ R.nameErr c ∷ [] )
discoverConstructorFields (suc fuel) atoms visited queue ty c result | noName =
  R.typeError
    ( R.strErr "deriveGenericReachableIn: constructor result is not the datatype itself: "
    ∷ R.nameErr c ∷ [] )

discoverConstructor : R.Term → List R.Name → List R.Name → R.Name → R.Name → R.TC (List R.Name)
discoverConstructor atoms visited queue ty c =
  R.getType c >>= λ cTy →
  R.reduce cTy >>= λ reducedCTy →
  discoverConstructorFields macroFuel atoms visited queue ty c reducedCTy

discoverConstructors :
  R.Term → List R.Name → List R.Name → R.Name → List R.Name → R.TC (List R.Name)
discoverConstructors atoms visited queue ty [] = R.returnTC queue
discoverConstructors atoms visited queue ty (c ∷ cs) =
  discoverConstructor atoms visited queue ty c >>= λ queue' →
  discoverConstructors atoms visited queue' ty cs

discoverReachable : ℕ → R.Term → List R.Name → List R.Name → R.TC (List R.Name)
discoverReachable zero atoms visited queue =
  R.typeError (R.strErr "deriveGenericReachableIn: out of fuel while discovering reachable datatypes" ∷ [])
discoverReachable (suc fuel) atoms visited [] = R.returnTC visited
discoverReachable (suc fuel) atoms visited (ty ∷ queue) with nameIn ty visited
... | true = discoverReachable fuel atoms visited queue
... | false =
  ensureNonIndexedType ty >>
  R.getDefinition ty >>= λ
    { (R.data-type zero cs) →
        let visited' = visited ++ [ ty ] in
        discoverConstructors atoms visited' queue ty cs >>= λ queue' →
        discoverReachable fuel atoms visited' queue'
    ; (R.data-type (suc _) _) →
        R.typeError (R.strErr "deriveGenericReachableIn: parameterized datatypes are not supported" ∷ R.nameErr ty ∷ [])
    ; _ →
        R.typeError (R.strErr "deriveGenericReachableIn: expected a datatype" ∷ R.nameErr ty ∷ [])
    }

deriveGenericReachableInTC : R.Term → R.Name → R.Term → R.TC Unit
deriveGenericReachableInTC atoms root hole =
  discoverReachable macroFuel atoms [] (root ∷ []) >>= λ family →
  deriveGenericFamilyInTC atoms family root hole

deriveGenericReachableFamilyInTC : R.Term → R.Name → R.Term → R.TC Unit
deriveGenericReachableFamilyInTC atoms root hole =
  discoverReachable macroFuel atoms [] (root ∷ []) >>= λ family →
  deriveGenericFamilyBundleInTC atoms family hole

deriveCertifiedGenericReachableInTC : R.Term → R.Name → R.Term → R.TC Unit
deriveCertifiedGenericReachableInTC atoms root hole =
  discoverReachable macroFuel atoms [] (root ∷ []) >>= λ family →
  deriveCertifiedGenericFamilyInTC atoms family root hole

deriveCertifiedGenericReachableFamilyInTC : R.Term → R.Name → R.Term → R.TC Unit
deriveCertifiedGenericReachableFamilyInTC atoms root hole =
  discoverReachable macroFuel atoms [] (root ∷ []) >>= λ family →
  deriveCertifiedGenericFamilyBundleInTC atoms family hole

-- Explicit-family macros are useful when the user wants full control over
-- which datatypes are recursive. `deriveGenericReachableIn` is the ergonomic
-- variant that discovers the family using the atom-first policy above.
macro
  deriveGenericFamilyIn1 : R.Term → R.Name → R.Term → R.TC Unit
  deriveGenericFamilyIn1 atoms ty hole =
    deriveGenericFamilyInTC atoms (ty ∷ []) ty hole

  deriveGenericFamilyIn2 : R.Term → R.Name → R.Name → R.Name → R.Term → R.TC Unit
  deriveGenericFamilyIn2 atoms a b root hole =
    deriveGenericFamilyInTC atoms (a ∷ b ∷ []) root hole

  deriveGenericFamilyIn3 : R.Term → R.Name → R.Name → R.Name → R.Name → R.Term → R.TC Unit
  deriveGenericFamilyIn3 atoms a b c root hole =
    deriveGenericFamilyInTC atoms (a ∷ b ∷ c ∷ []) root hole

  deriveGenericFamilyIn4 : R.Term → R.Name → R.Name → R.Name → R.Name → R.Name → R.Term → R.TC Unit
  deriveGenericFamilyIn4 atoms a b c d root hole =
    deriveGenericFamilyInTC atoms (a ∷ b ∷ c ∷ d ∷ []) root hole

  deriveGenericReachableIn : R.Term → R.Name → R.Term → R.TC Unit
  deriveGenericReachableIn = deriveGenericReachableInTC

  deriveGenericFamilyBundleIn1 : R.Term → R.Name → R.Term → R.TC Unit
  deriveGenericFamilyBundleIn1 atoms a hole =
    deriveGenericFamilyBundleInTC atoms (a ∷ []) hole

  deriveGenericFamilyBundleIn2 : R.Term → R.Name → R.Name → R.Term → R.TC Unit
  deriveGenericFamilyBundleIn2 atoms a b hole =
    deriveGenericFamilyBundleInTC atoms (a ∷ b ∷ []) hole

  deriveGenericFamilyBundleIn3 : R.Term → R.Name → R.Name → R.Name → R.Term → R.TC Unit
  deriveGenericFamilyBundleIn3 atoms a b c hole =
    deriveGenericFamilyBundleInTC atoms (a ∷ b ∷ c ∷ []) hole

  deriveGenericFamilyBundleIn4 : R.Term → R.Name → R.Name → R.Name → R.Name → R.Term → R.TC Unit
  deriveGenericFamilyBundleIn4 atoms a b c d hole =
    deriveGenericFamilyBundleInTC atoms (a ∷ b ∷ c ∷ d ∷ []) hole

  deriveCertifiedGenericFamilyIn1 : R.Term → R.Name → R.Term → R.TC Unit
  deriveCertifiedGenericFamilyIn1 atoms a hole =
    deriveCertifiedGenericFamilyInTC atoms (a ∷ []) a hole

  deriveCertifiedGenericFamilyIn2 : R.Term → R.Name → R.Name → R.Name → R.Term → R.TC Unit
  deriveCertifiedGenericFamilyIn2 atoms a b root hole =
    deriveCertifiedGenericFamilyInTC atoms (a ∷ b ∷ []) root hole

  deriveCertifiedGenericFamilyIn3 : R.Term → R.Name → R.Name → R.Name → R.Name → R.Term → R.TC Unit
  deriveCertifiedGenericFamilyIn3 atoms a b c root hole =
    deriveCertifiedGenericFamilyInTC atoms (a ∷ b ∷ c ∷ []) root hole

  deriveCertifiedGenericFamilyIn4 : R.Term → R.Name → R.Name → R.Name → R.Name → R.Name → R.Term → R.TC Unit
  deriveCertifiedGenericFamilyIn4 atoms a b c d root hole =
    deriveCertifiedGenericFamilyInTC atoms (a ∷ b ∷ c ∷ d ∷ []) root hole

  deriveCertifiedGenericFamilyBundleIn1 : R.Term → R.Name → R.Term → R.TC Unit
  deriveCertifiedGenericFamilyBundleIn1 atoms a hole =
    deriveCertifiedGenericFamilyBundleInTC atoms (a ∷ []) hole

  deriveCertifiedGenericFamilyBundleIn2 : R.Term → R.Name → R.Name → R.Term → R.TC Unit
  deriveCertifiedGenericFamilyBundleIn2 atoms a b hole =
    deriveCertifiedGenericFamilyBundleInTC atoms (a ∷ b ∷ []) hole

  deriveCertifiedGenericFamilyBundleIn3 : R.Term → R.Name → R.Name → R.Name → R.Term → R.TC Unit
  deriveCertifiedGenericFamilyBundleIn3 atoms a b c hole =
    deriveCertifiedGenericFamilyBundleInTC atoms (a ∷ b ∷ c ∷ []) hole

  deriveCertifiedGenericFamilyBundleIn4 : R.Term → R.Name → R.Name → R.Name → R.Name → R.Term → R.TC Unit
  deriveCertifiedGenericFamilyBundleIn4 atoms a b c d hole =
    deriveCertifiedGenericFamilyBundleInTC atoms (a ∷ b ∷ c ∷ d ∷ []) hole

  deriveGenericReachableFamilyIn : R.Term → R.Name → R.Term → R.TC Unit
  deriveGenericReachableFamilyIn = deriveGenericReachableFamilyInTC

  deriveCertifiedGenericReachableIn : R.Term → R.Name → R.Term → R.TC Unit
  deriveCertifiedGenericReachableIn = deriveCertifiedGenericReachableInTC

  deriveCertifiedGenericReachableFamilyIn : R.Term → R.Name → R.Term → R.TC Unit
  deriveCertifiedGenericReachableFamilyIn = deriveCertifiedGenericReachableFamilyInTC