{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
module Generic.Data.Function.Traverse.Constructor where
import GHC.Generics
import GHC.TypeNats ( Natural, KnownNat, type (+) )
import Generic.Data.Function.Util.Generic ( datatypeName', conName', selName'' )
import Generic.Data.Function.Util.TypeNats ( natVal'' )
import Control.Applicative qualified as Applicative
import Control.Applicative ( Alternative(empty) )
import Data.Kind ( type Type, type Constraint )
import Generic.Data.Wrappers ( NoRec0, type ENoRec0, EmptyRec0 )
import GHC.TypeLits ( TypeError )
class GenericTraverse tag where
type GenericTraverseF tag :: Type -> Type
type GenericTraverseC tag a :: Constraint
genericTraverseAction
:: GenericTraverseC tag a
=> String
-> String
-> Maybe String
-> Natural
-> GenericTraverseF tag a
instance GenericTraverse (NoRec0 (f :: Type -> Type)) where
type GenericTraverseF (NoRec0 f) = f
type GenericTraverseC (NoRec0 _) _ = TypeError ENoRec0
genericTraverseAction :: forall a.
GenericTraverseC (NoRec0 f) a =>
String
-> String
-> Maybe String
-> Natural
-> GenericTraverseF (NoRec0 f) a
genericTraverseAction = String -> String -> Maybe String -> Natural -> f a
String
-> String
-> Maybe String
-> Natural
-> GenericTraverseF (NoRec0 f) a
forall a. HasCallStack => a
undefined
instance GenericTraverse (EmptyRec0 (f :: Type -> Type)) where
type GenericTraverseF (EmptyRec0 f) = f
type GenericTraverseC (EmptyRec0 f) _ = Alternative f
genericTraverseAction :: forall a.
GenericTraverseC (EmptyRec0 f) a =>
String
-> String
-> Maybe String
-> Natural
-> GenericTraverseF (EmptyRec0 f) a
genericTraverseAction String
_ String
_ Maybe String
_ Natural
_ = f a
GenericTraverseF (EmptyRec0 f) a
forall a. f a
forall (f :: Type -> Type) a. Alternative f => f a
empty
class GTraverseC cd cc (si :: Natural) tag gf where
gTraverseC :: GenericTraverseF tag (gf p)
instance
( Applicative (GenericTraverseF tag)
, GTraverseC cd cc si tag l
, GTraverseC cd cc (si + ProdArity r) tag r
) => GTraverseC cd cc si tag (l :*: r) where
gTraverseC :: forall p. GenericTraverseF tag ((:*:) l r p)
gTraverseC = (l p -> r p -> (:*:) l r p)
-> GenericTraverseF tag (l p)
-> GenericTraverseF tag (r p)
-> GenericTraverseF tag ((:*:) l r p)
forall a b c.
(a -> b -> c)
-> GenericTraverseF tag a
-> GenericTraverseF tag b
-> GenericTraverseF tag c
forall (f :: Type -> Type) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
Applicative.liftA2 l p -> r p -> (:*:) l r p
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
(:*:)
(forall (cd :: k) (cc :: k) (si :: Natural) (tag :: k)
(gf :: Type -> Type) p.
GTraverseC cd cc si tag gf =>
GenericTraverseF tag (gf p)
forall {k} {k} {k} {k} (cd :: k) (cc :: k) (si :: Natural)
(tag :: k) (gf :: k -> Type) (p :: k).
GTraverseC cd cc si tag gf =>
GenericTraverseF tag (gf p)
gTraverseC @cd @cc @si @tag)
(forall (cd :: k) (cc :: k) (si :: Natural) (tag :: k)
(gf :: Type -> Type) p.
GTraverseC cd cc si tag gf =>
GenericTraverseF tag (gf p)
forall {k} {k} {k} {k} (cd :: k) (cc :: k) (si :: Natural)
(tag :: k) (gf :: k -> Type) (p :: k).
GTraverseC cd cc si tag gf =>
GenericTraverseF tag (gf p)
gTraverseC @cd @cc @(si + ProdArity r) @tag)
instance
( GenericTraverse tag, GenericTraverseC tag a
, Functor (GenericTraverseF tag)
, KnownNat si, Selector cs, Constructor cc, Datatype cd
) => GTraverseC cd cc si tag (S1 cs (Rec0 a)) where
gTraverseC :: forall (p :: k). GenericTraverseF tag (S1 cs (Rec0 a) p)
gTraverseC = (K1 R a p -> M1 S cs (Rec0 a) p
forall k i (c :: Meta) (f :: k -> Type) (p :: k). f p -> M1 i c f p
M1 (K1 R a p -> M1 S cs (Rec0 a) p)
-> (a -> K1 R a p) -> a -> M1 S cs (Rec0 a) p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> K1 R a p
forall k i c (p :: k). c -> K1 i c p
K1) (a -> M1 S cs (Rec0 a) p)
-> GenericTraverseF tag a
-> GenericTraverseF tag (M1 S cs (Rec0 a) p)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (tag :: k) a.
(GenericTraverse tag, GenericTraverseC tag a) =>
String
-> String -> Maybe String -> Natural -> GenericTraverseF tag a
forall {k} (tag :: k) a.
(GenericTraverse tag, GenericTraverseC tag a) =>
String
-> String -> Maybe String -> Natural -> GenericTraverseF tag a
genericTraverseAction @tag String
cd String
cc Maybe String
cs Natural
si
where
cs :: Maybe String
cs = forall {k} (s :: k). Selector s => Maybe String
forall (s :: Meta). Selector s => Maybe String
selName'' @cs
cd :: String
cd = forall (d :: k). Datatype d => String
forall {k} (d :: k). Datatype d => String
datatypeName' @cd
cc :: String
cc = forall (c :: k). Constructor c => String
forall {k} (c :: k). Constructor c => String
conName' @cc
si :: Natural
si = forall (n :: Natural). KnownNat n => Natural
natVal'' @si
instance Applicative (GenericTraverseF tag) => GTraverseC cd cc 0 tag U1 where
gTraverseC :: forall (p :: k). GenericTraverseF tag (U1 p)
gTraverseC = U1 p -> GenericTraverseF tag (U1 p)
forall a. a -> GenericTraverseF tag a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure U1 p
forall k (p :: k). U1 p
U1
type family ProdArity (f :: Type -> Type) :: Natural where
ProdArity (S1 c f) = 1
ProdArity (l :*: r) = ProdArity l + ProdArity r