module Hix.Class.SOP where

import Generics.SOP (I (I), NP (Nil, (:*)), NS (S, Z), SOP (SOP))
import Generics.SOP.GGP (GCode, GDatatypeInfoOf, GFrom, gfrom)
import Generics.SOP.Type.Metadata (ConstructorInfo (Record), DatatypeInfo (..), FieldInfo (FieldInfo))

data FieldK =
  FieldK {
    FieldK -> Symbol
name :: Symbol,
    FieldK -> *
tpe :: Type
  }

type Field :: FieldK -> Type
data Field k where
  Field :: a -> Field ('FieldK name a)

type ProdFields :: [FieldInfo] -> [Type] -> [FieldK] -> Constraint
class ProdFields info as fields | info as -> fields where
  prodFields :: NP I as -> NP Field fields

instance ProdFields '[] '[] '[] where
  prodFields :: NP I '[] -> NP Field '[]
prodFields NP I '[]
Nil = NP Field '[]
forall {k} (a :: k -> *). NP a '[]
Nil

instance (
    ProdFields info as fields
  ) => ProdFields ('FieldInfo name : info) (a : as) ('FieldK name a : fields) where
    prodFields :: NP I (a : as) -> NP Field ('FieldK name a : fields)
prodFields (I x
a :* NP I xs
fields) = a -> Field ('FieldK name a)
forall a (name :: Symbol). a -> Field ('FieldK name a)
Field a
x
a Field ('FieldK name a)
-> NP Field fields -> NP Field ('FieldK name a : fields)
forall {k} (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* forall (info :: [FieldInfo]) (as :: [*]) (fields :: [FieldK]).
ProdFields info as fields =>
NP I as -> NP Field fields
prodFields @info NP I xs
fields

type SumFields :: [ConstructorInfo] -> [[Type]] -> [[FieldK]] -> Constraint
class SumFields cons ass fields | cons ass -> fields where
  sumFields :: NS (NP I) ass -> NS (NP Field) fields

instance SumFields '[] '[] '[] where
  sumFields :: NS (NP I) '[] -> NS (NP Field) '[]
sumFields = NS (NP I) '[] -> NS (NP Field) '[]
\case

instance (
    ProdFields info as conFields,
    SumFields cons ass fields
  ) => SumFields ('Record con info : cons) (as : ass) (conFields : fields) where
    sumFields :: NS (NP I) (as : ass) -> NS (NP Field) (conFields : fields)
sumFields = \case
      Z NP I x
con -> NP Field conFields -> NS (NP Field) (conFields : fields)
forall {k} (a :: k -> *) (x :: k) (xs :: [k]). a x -> NS a (x : xs)
Z (forall (info :: [FieldInfo]) (as :: [*]) (fields :: [FieldK]).
ProdFields info as fields =>
NP I as -> NP Field fields
prodFields @info NP I x
con)
      S NS (NP I) xs
cons -> NS (NP Field) fields -> NS (NP Field) (conFields : fields)
forall {k} (a :: k -> *) (xs :: [k]) (x :: k).
NS a xs -> NS a (x : xs)
S (forall (cons :: [ConstructorInfo]) (ass :: [[*]])
       (fields :: [[FieldK]]).
SumFields cons ass fields =>
NS (NP I) ass -> NS (NP Field) fields
sumFields @cons NS (NP I) xs
cons)

class ToFields a fields | a -> fields where
  toFields :: a -> SOP Field fields

instance (
    Generic a,
    GFrom a,
    'ADT mod name cons sni ~ GDatatypeInfoOf a,
    ass ~ GCode a,
    SumFields cons ass fields
  ) => ToFields a fields where
    toFields :: a -> SOP Field fields
toFields (a -> SOP I (GCode a)
forall a. (GFrom a, Generic a) => a -> SOP I (GCode a)
gfrom -> SOP NS (NP I) (GCode a)
fields) = NS (NP Field) fields -> SOP Field fields
forall k (f :: k -> *) (xss :: [[k]]). NS (NP f) xss -> SOP f xss
SOP (forall (cons :: [ConstructorInfo]) (ass :: [[*]])
       (fields :: [[FieldK]]).
SumFields cons ass fields =>
NS (NP I) ass -> NS (NP Field) fields
sumFields @cons NS (NP I) ass
NS (NP I) (GCode a)
fields)