{-# LANGUAGE EmptyCase, PolyKinds, UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}
module Generics.SOP.GGP
( GCode
, GFrom
, GTo
, GDatatypeInfo
, GDatatypeInfoOf
, gfrom
, gto
, gdatatypeInfo
) where
import Data.Proxy (Proxy (..))
import Data.Kind (Type)
import GHC.Generics as GHC
import Generics.SOP.NP as SOP
import Generics.SOP.NS as SOP
import Generics.SOP.BasicFunctors as SOP
import qualified Generics.SOP.Type.Metadata as SOP.T
import Generics.SOP.Metadata as SOP
type family ToSingleCode (a :: Type -> Type) :: Type
type instance ToSingleCode (K1 _i a) = a
type family ToProductCode (a :: Type -> Type) (xs :: [Type]) :: [Type]
type instance ToProductCode (a :*: b) xs = ToProductCode a (ToProductCode b xs)
type instance ToProductCode U1 xs = xs
type instance ToProductCode (M1 S _c a) xs = ToSingleCode a ': xs
type family ToSumCode (a :: Type -> Type) (xs :: [[Type]]) :: [[Type]]
type instance ToSumCode (a :+: b) xs = ToSumCode a (ToSumCode b xs)
type instance ToSumCode V1 xs = xs
type instance ToSumCode (M1 D _c a) xs = ToSumCode a xs
type instance ToSumCode (M1 C _c a) xs = ToProductCode a '[] ': xs
data InfoProxy (c :: Meta) (f :: Type -> Type) (x :: Type) = InfoProxy
type family ToInfo (a :: Type -> Type) :: SOP.T.DatatypeInfo
type instance ToInfo (M1 D (MetaData n m p False) a) =
SOP.T.ADT m n (ToSumInfo a '[]) (ToStrictnessInfoss a '[])
type instance ToInfo (M1 D (MetaData n m p True) a) =
SOP.T.Newtype m n (ToSingleConstructorInfo a)
type family ToStrictnessInfoss (a :: Type -> Type) (xss :: [[SOP.T.StrictnessInfo]]) :: [[SOP.T.StrictnessInfo]]
type instance ToStrictnessInfoss (a :+: b) xss = ToStrictnessInfoss a (ToStrictnessInfoss b xss)
type instance ToStrictnessInfoss V1 xss = xss
type instance ToStrictnessInfoss (M1 C _ a) xss = ToStrictnessInfos a '[] ': xss
type family ToStrictnessInfos (a :: Type -> Type) (xs :: [SOP.T.StrictnessInfo]) :: [SOP.T.StrictnessInfo]
type instance ToStrictnessInfos (a :*: b) xs = ToStrictnessInfos a (ToStrictnessInfos b xs)
type instance ToStrictnessInfos U1 xs = xs
type instance ToStrictnessInfos (M1 S s a) xs = ToStrictnessInfo s ': xs
type family ToStrictnessInfo (s :: Meta) :: SOP.T.StrictnessInfo
type instance ToStrictnessInfo (MetaSel _ su ss ds) = 'SOP.T.StrictnessInfo su ss ds
type family ToSumInfo (a :: Type -> Type) (xs :: [SOP.T.ConstructorInfo]) :: [SOP.T.ConstructorInfo]
type instance ToSumInfo (a :+: b) xs = ToSumInfo a (ToSumInfo b xs)
type instance ToSumInfo V1 xs = xs
type instance ToSumInfo (M1 C c a) xs = ToSingleConstructorInfo (M1 C c a) ': xs
type family ToSingleConstructorInfo (a :: Type -> Type) :: SOP.T.ConstructorInfo
type instance ToSingleConstructorInfo (M1 C (MetaCons n PrefixI False) a) =
SOP.T.Constructor n
type instance ToSingleConstructorInfo (M1 C (MetaCons n (InfixI assoc fix) False) a) =
SOP.T.Infix n assoc fix
type instance ToSingleConstructorInfo (M1 C (MetaCons n f True) a) =
SOP.T.Record n (ToProductInfo a '[])
type family ToProductInfo (a :: Type -> Type) (xs :: [SOP.T.FieldInfo]) :: [SOP.T.FieldInfo]
type instance ToProductInfo (a :*: b) xs = ToProductInfo a (ToProductInfo b xs)
type instance ToProductInfo U1 xs = xs
type instance ToProductInfo (M1 S c a) xs = ToSingleInfo (M1 S c a) ': xs
type family ToSingleInfo (a :: Type -> Type) :: SOP.T.FieldInfo
type instance ToSingleInfo (M1 S (MetaSel (Just n) _su _ss _ds) a) = 'SOP.T.FieldInfo n
class GFieldInfos (a :: Type -> Type) where
gFieldInfos :: proxy a -> NP FieldInfo xs -> NP FieldInfo (ToProductCode a xs)
instance (GFieldInfos a, GFieldInfos b) => GFieldInfos (a :*: b) where
gFieldInfos :: forall (proxy :: (* -> *) -> *) (xs :: [*]).
proxy (a :*: b)
-> NP FieldInfo xs -> NP FieldInfo (ToProductCode (a :*: b) xs)
gFieldInfos proxy (a :*: b)
_ NP FieldInfo xs
xs = Proxy a
-> NP FieldInfo (ToProductCode b xs)
-> NP FieldInfo (ToProductCode a (ToProductCode b xs))
forall (a :: * -> *) (proxy :: (* -> *) -> *) (xs :: [*]).
GFieldInfos a =>
proxy a -> NP FieldInfo xs -> NP FieldInfo (ToProductCode a xs)
forall (proxy :: (* -> *) -> *) (xs :: [*]).
proxy a -> NP FieldInfo xs -> NP FieldInfo (ToProductCode a xs)
gFieldInfos (Proxy a
forall {k} (t :: k). Proxy t
Proxy :: Proxy a) (Proxy b -> NP FieldInfo xs -> NP FieldInfo (ToProductCode b xs)
forall (a :: * -> *) (proxy :: (* -> *) -> *) (xs :: [*]).
GFieldInfos a =>
proxy a -> NP FieldInfo xs -> NP FieldInfo (ToProductCode a xs)
forall (proxy :: (* -> *) -> *) (xs :: [*]).
proxy b -> NP FieldInfo xs -> NP FieldInfo (ToProductCode b xs)
gFieldInfos (Proxy b
forall {k} (t :: k). Proxy t
Proxy :: Proxy b) NP FieldInfo xs
xs)
instance GFieldInfos U1 where
gFieldInfos :: forall (proxy :: (* -> *) -> *) (xs :: [*]).
proxy U1 -> NP FieldInfo xs -> NP FieldInfo (ToProductCode U1 xs)
gFieldInfos proxy U1
_ NP FieldInfo xs
xs = NP FieldInfo xs
NP FieldInfo (ToProductCode U1 xs)
xs
instance (Selector c) => GFieldInfos (M1 S c a) where
gFieldInfos :: forall (proxy :: (* -> *) -> *) (xs :: [*]).
proxy (M1 S c a)
-> NP FieldInfo xs -> NP FieldInfo (ToProductCode (M1 S c a) xs)
gFieldInfos proxy (M1 S c a)
_ NP FieldInfo xs
xs = FieldName -> FieldInfo (ToSingleCode a)
forall a. FieldName -> FieldInfo a
FieldInfo (InfoProxy c a Any -> FieldName
forall {k} (s :: k) k1 (t :: k -> (k1 -> *) -> k1 -> *)
(f :: k1 -> *) (a :: k1).
Selector s =>
t s f a -> FieldName
forall k1 (t :: Meta -> (k1 -> *) -> k1 -> *) (f :: k1 -> *)
(a :: k1).
t c f a -> FieldName
selName InfoProxy c a Any
forall x. InfoProxy c a x
p) FieldInfo (ToSingleCode a)
-> NP FieldInfo xs -> NP FieldInfo (ToSingleCode a : xs)
forall {k} (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* NP FieldInfo xs
xs
where
p :: InfoProxy c a x
p :: forall x. InfoProxy c a x
p = InfoProxy c a x
forall (c :: Meta) (f :: * -> *) x. InfoProxy c f x
InfoProxy
class GSingleFrom (a :: Type -> Type) where
gSingleFrom :: a x -> ToSingleCode a
instance GSingleFrom (K1 i a) where
gSingleFrom :: forall x. K1 i a x -> ToSingleCode (K1 i a)
gSingleFrom (K1 a
a) = a
ToSingleCode (K1 i a)
a
class GProductFrom (a :: Type -> Type) where
gProductFrom :: a x -> NP I xs -> NP I (ToProductCode a xs)
instance (GProductFrom a, GProductFrom b) => GProductFrom (a :*: b) where
gProductFrom :: forall x (xs :: [*]).
(:*:) a b x -> NP I xs -> NP I (ToProductCode (a :*: b) xs)
gProductFrom (a x
a :*: b x
b) NP I xs
xs = a x
-> NP I (ToProductCode b xs)
-> NP I (ToProductCode a (ToProductCode b xs))
forall x (xs :: [*]). a x -> NP I xs -> NP I (ToProductCode a xs)
forall (a :: * -> *) x (xs :: [*]).
GProductFrom a =>
a x -> NP I xs -> NP I (ToProductCode a xs)
gProductFrom a x
a (b x -> NP I xs -> NP I (ToProductCode b xs)
forall x (xs :: [*]). b x -> NP I xs -> NP I (ToProductCode b xs)
forall (a :: * -> *) x (xs :: [*]).
GProductFrom a =>
a x -> NP I xs -> NP I (ToProductCode a xs)
gProductFrom b x
b NP I xs
xs)
instance GProductFrom U1 where
gProductFrom :: forall x (xs :: [*]). U1 x -> NP I xs -> NP I (ToProductCode U1 xs)
gProductFrom U1 x
U1 NP I xs
xs = NP I xs
NP I (ToProductCode U1 xs)
xs
instance GSingleFrom a => GProductFrom (M1 S c a) where
gProductFrom :: forall x (xs :: [*]).
M1 S c a x -> NP I xs -> NP I (ToProductCode (M1 S c a) xs)
gProductFrom (M1 a x
a) NP I xs
xs = ToSingleCode a -> I (ToSingleCode a)
forall a. a -> I a
I (a x -> ToSingleCode a
forall x. a x -> ToSingleCode a
forall (a :: * -> *) x. GSingleFrom a => a x -> ToSingleCode a
gSingleFrom a x
a) I (ToSingleCode a) -> NP I xs -> NP I (ToSingleCode a : xs)
forall {k} (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* NP I xs
xs
class GSingleTo (a :: Type -> Type) where
gSingleTo :: ToSingleCode a -> a x
instance GSingleTo (K1 i a) where
gSingleTo :: forall x. ToSingleCode (K1 i a) -> K1 i a x
gSingleTo ToSingleCode (K1 i a)
a = a -> K1 i a x
forall k i c (p :: k). c -> K1 i c p
K1 a
ToSingleCode (K1 i a)
a
class GProductTo (a :: Type -> Type) where
gProductTo :: NP I (ToProductCode a xs) -> (a x -> NP I xs -> r) -> r
instance (GProductTo a, GProductTo b) => GProductTo (a :*: b) where
gProductTo :: forall (xs :: [*]) x r.
NP I (ToProductCode (a :*: b) xs)
-> ((:*:) a b x -> NP I xs -> r) -> r
gProductTo NP I (ToProductCode (a :*: b) xs)
xs (:*:) a b x -> NP I xs -> r
k = NP I (ToProductCode a (ToProductCode b xs))
-> (a x -> NP I (ToProductCode b xs) -> r) -> r
forall (xs :: [*]) x r.
NP I (ToProductCode a xs) -> (a x -> NP I xs -> r) -> r
forall (a :: * -> *) (xs :: [*]) x r.
GProductTo a =>
NP I (ToProductCode a xs) -> (a x -> NP I xs -> r) -> r
gProductTo NP I (ToProductCode a (ToProductCode b xs))
NP I (ToProductCode (a :*: b) xs)
xs (\ a x
a NP I (ToProductCode b xs)
ys -> NP I (ToProductCode b xs) -> (b x -> NP I xs -> r) -> r
forall (xs :: [*]) x r.
NP I (ToProductCode b xs) -> (b x -> NP I xs -> r) -> r
forall (a :: * -> *) (xs :: [*]) x r.
GProductTo a =>
NP I (ToProductCode a xs) -> (a x -> NP I xs -> r) -> r
gProductTo NP I (ToProductCode b xs)
ys (\ b x
b NP I xs
zs -> (:*:) a b x -> NP I xs -> r
k (a x
a a x -> b x -> (:*:) a b x
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: b x
b) NP I xs
zs))
instance GSingleTo a => GProductTo (M1 S c a) where
gProductTo :: forall (xs :: [*]) x r.
NP I (ToProductCode (M1 S c a) xs)
-> (M1 S c a x -> NP I xs -> r) -> r
gProductTo (SOP.I x
a :* NP I xs
xs) M1 S c a x -> NP I xs -> r
k = M1 S c a x -> NP I xs -> r
k (a x -> M1 S c a x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (ToSingleCode a -> a x
forall x. ToSingleCode a -> a x
forall (a :: * -> *) x. GSingleTo a => ToSingleCode a -> a x
gSingleTo x
ToSingleCode a
a)) NP I xs
NP I xs
xs
instance GProductTo U1 where
gProductTo :: forall (xs :: [*]) x r.
NP I (ToProductCode U1 xs) -> (U1 x -> NP I xs -> r) -> r
gProductTo NP I (ToProductCode U1 xs)
xs U1 x -> NP I xs -> r
k = U1 x -> NP I xs -> r
k U1 x
forall k (p :: k). U1 p
U1 NP I xs
NP I (ToProductCode U1 xs)
xs
class GSumFrom (a :: Type -> Type) where
gSumFrom :: a x -> proxy xss -> SOP I (ToSumCode a xss)
gSumSkip :: proxy a -> SOP I xss -> SOP I (ToSumCode a xss)
instance GSumFrom V1 where
gSumFrom :: forall x (proxy :: [[*]] -> *) (xss :: [[*]]).
V1 x -> proxy xss -> SOP I (ToSumCode V1 xss)
gSumFrom V1 x
x = case V1 x
x of {}
gSumSkip :: forall (proxy :: (* -> *) -> *) (xss :: [[*]]).
proxy V1 -> SOP I xss -> SOP I (ToSumCode V1 xss)
gSumSkip proxy V1
_ SOP I xss
xss = SOP I xss
SOP I (ToSumCode V1 xss)
xss
instance (GSumFrom a, GSumFrom b) => GSumFrom (a :+: b) where
gSumFrom :: forall x (proxy :: [[*]] -> *) (xss :: [[*]]).
(:+:) a b x -> proxy xss -> SOP I (ToSumCode (a :+: b) xss)
gSumFrom (L1 a x
a) proxy xss
xss = a x
-> Proxy (ToSumCode b xss) -> SOP I (ToSumCode a (ToSumCode b xss))
forall x (proxy :: [[*]] -> *) (xss :: [[*]]).
a x -> proxy xss -> SOP I (ToSumCode a xss)
forall (a :: * -> *) x (proxy :: [[*]] -> *) (xss :: [[*]]).
GSumFrom a =>
a x -> proxy xss -> SOP I (ToSumCode a xss)
gSumFrom a x
a (proxy xss -> Proxy (ToSumCode b xss)
forall (proxy :: [[*]] -> *) (xss :: [[*]]).
proxy xss -> Proxy (ToSumCode b xss)
toSumCodeProxy proxy xss
xss) where
toSumCodeProxy :: proxy xss -> Proxy (ToSumCode b xss)
toSumCodeProxy :: forall (proxy :: [[*]] -> *) (xss :: [[*]]).
proxy xss -> Proxy (ToSumCode b xss)
toSumCodeProxy proxy xss
_ = Proxy (ToSumCode b xss)
forall {k} (t :: k). Proxy t
Proxy
gSumFrom (R1 b x
b) proxy xss
xss = Proxy a
-> SOP I (ToSumCode b xss) -> SOP I (ToSumCode a (ToSumCode b xss))
forall (a :: * -> *) (proxy :: (* -> *) -> *) (xss :: [[*]]).
GSumFrom a =>
proxy a -> SOP I xss -> SOP I (ToSumCode a xss)
forall (proxy :: (* -> *) -> *) (xss :: [[*]]).
proxy a -> SOP I xss -> SOP I (ToSumCode a xss)
gSumSkip (Proxy a
forall {k} (t :: k). Proxy t
Proxy :: Proxy a) (b x -> proxy xss -> SOP I (ToSumCode b xss)
forall x (proxy :: [[*]] -> *) (xss :: [[*]]).
b x -> proxy xss -> SOP I (ToSumCode b xss)
forall (a :: * -> *) x (proxy :: [[*]] -> *) (xss :: [[*]]).
GSumFrom a =>
a x -> proxy xss -> SOP I (ToSumCode a xss)
gSumFrom b x
b proxy xss
xss)
gSumSkip :: forall (proxy :: (* -> *) -> *) (xss :: [[*]]).
proxy (a :+: b) -> SOP I xss -> SOP I (ToSumCode (a :+: b) xss)
gSumSkip proxy (a :+: b)
_ SOP I xss
xss = Proxy a
-> SOP I (ToSumCode b xss) -> SOP I (ToSumCode a (ToSumCode b xss))
forall (a :: * -> *) (proxy :: (* -> *) -> *) (xss :: [[*]]).
GSumFrom a =>
proxy a -> SOP I xss -> SOP I (ToSumCode a xss)
forall (proxy :: (* -> *) -> *) (xss :: [[*]]).
proxy a -> SOP I xss -> SOP I (ToSumCode a xss)
gSumSkip (Proxy a
forall {k} (t :: k). Proxy t
Proxy :: Proxy a) (Proxy b -> SOP I xss -> SOP I (ToSumCode b xss)
forall (a :: * -> *) (proxy :: (* -> *) -> *) (xss :: [[*]]).
GSumFrom a =>
proxy a -> SOP I xss -> SOP I (ToSumCode a xss)
forall (proxy :: (* -> *) -> *) (xss :: [[*]]).
proxy b -> SOP I xss -> SOP I (ToSumCode b xss)
gSumSkip (Proxy b
forall {k} (t :: k). Proxy t
Proxy :: Proxy b) SOP I xss
xss)
instance (GSumFrom a) => GSumFrom (M1 D c a) where
gSumFrom :: forall x (proxy :: [[*]] -> *) (xss :: [[*]]).
M1 D c a x -> proxy xss -> SOP I (ToSumCode (M1 D c a) xss)
gSumFrom (M1 a x
a) proxy xss
xss = a x -> proxy xss -> SOP I (ToSumCode a xss)
forall x (proxy :: [[*]] -> *) (xss :: [[*]]).
a x -> proxy xss -> SOP I (ToSumCode a xss)
forall (a :: * -> *) x (proxy :: [[*]] -> *) (xss :: [[*]]).
GSumFrom a =>
a x -> proxy xss -> SOP I (ToSumCode a xss)
gSumFrom a x
a proxy xss
xss
gSumSkip :: forall (proxy :: (* -> *) -> *) (xss :: [[*]]).
proxy (M1 D c a) -> SOP I xss -> SOP I (ToSumCode (M1 D c a) xss)
gSumSkip proxy (M1 D c a)
_ SOP I xss
xss = Proxy a -> SOP I xss -> SOP I (ToSumCode a xss)
forall (a :: * -> *) (proxy :: (* -> *) -> *) (xss :: [[*]]).
GSumFrom a =>
proxy a -> SOP I xss -> SOP I (ToSumCode a xss)
forall (proxy :: (* -> *) -> *) (xss :: [[*]]).
proxy a -> SOP I xss -> SOP I (ToSumCode a xss)
gSumSkip (Proxy a
forall {k} (t :: k). Proxy t
Proxy :: Proxy a) SOP I xss
xss
instance (GProductFrom a) => GSumFrom (M1 C c a) where
gSumFrom :: forall x (proxy :: [[*]] -> *) (xss :: [[*]]).
M1 C c a x -> proxy xss -> SOP I (ToSumCode (M1 C c a) xss)
gSumFrom (M1 a x
a) proxy xss
_ = NS (NP I) (ToProductCode a '[] : xss)
-> SOP I (ToProductCode a '[] : xss)
forall k (f :: k -> *) (xss :: [[k]]). NS (NP f) xss -> SOP f xss
SOP (NP I (ToProductCode a '[]) -> NS (NP I) (ToProductCode a '[] : xss)
forall {k} (a :: k -> *) (x :: k) (xs :: [k]). a x -> NS a (x : xs)
Z (a x -> NP I '[] -> NP I (ToProductCode a '[])
forall x (xs :: [*]). a x -> NP I xs -> NP I (ToProductCode a xs)
forall (a :: * -> *) x (xs :: [*]).
GProductFrom a =>
a x -> NP I xs -> NP I (ToProductCode a xs)
gProductFrom a x
a NP I '[]
forall {k} (a :: k -> *). NP a '[]
Nil))
gSumSkip :: forall (proxy :: (* -> *) -> *) (xss :: [[*]]).
proxy (M1 C c a) -> SOP I xss -> SOP I (ToSumCode (M1 C c a) xss)
gSumSkip proxy (M1 C c a)
_ (SOP NS (NP I) xss
xss) = NS (NP I) (ToProductCode a '[] : xss)
-> SOP I (ToProductCode a '[] : xss)
forall k (f :: k -> *) (xss :: [[k]]). NS (NP f) xss -> SOP f xss
SOP (NS (NP I) xss -> NS (NP I) (ToProductCode a '[] : xss)
forall {k} (a :: k -> *) (xs :: [k]) (x :: k).
NS a xs -> NS a (x : xs)
S NS (NP I) xss
xss)
class GSumTo (a :: Type -> Type) where
gSumTo :: SOP I (ToSumCode a xss) -> (a x -> r) -> (SOP I xss -> r) -> r
instance GSumTo V1 where
gSumTo :: forall (xss :: [[*]]) x r.
SOP I (ToSumCode V1 xss) -> (V1 x -> r) -> (SOP I xss -> r) -> r
gSumTo SOP I (ToSumCode V1 xss)
x V1 x -> r
_ SOP I xss -> r
k = SOP I xss -> r
k SOP I xss
SOP I (ToSumCode V1 xss)
x
instance (GSumTo a, GSumTo b) => GSumTo (a :+: b) where
gSumTo :: forall (xss :: [[*]]) x r.
SOP I (ToSumCode (a :+: b) xss)
-> ((:+:) a b x -> r) -> (SOP I xss -> r) -> r
gSumTo SOP I (ToSumCode (a :+: b) xss)
xss (:+:) a b x -> r
s SOP I xss -> r
k = SOP I (ToSumCode a (ToSumCode b xss))
-> (a x -> r) -> (SOP I (ToSumCode b xss) -> r) -> r
forall (xss :: [[*]]) x r.
SOP I (ToSumCode a xss) -> (a x -> r) -> (SOP I xss -> r) -> r
forall (a :: * -> *) (xss :: [[*]]) x r.
GSumTo a =>
SOP I (ToSumCode a xss) -> (a x -> r) -> (SOP I xss -> r) -> r
gSumTo SOP I (ToSumCode a (ToSumCode b xss))
SOP I (ToSumCode (a :+: b) xss)
xss ((:+:) a b x -> r
s ((:+:) a b x -> r) -> (a x -> (:+:) a b x) -> a x -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a x -> (:+:) a b x
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1) (\ SOP I (ToSumCode b xss)
r -> SOP I (ToSumCode b xss) -> (b x -> r) -> (SOP I xss -> r) -> r
forall (xss :: [[*]]) x r.
SOP I (ToSumCode b xss) -> (b x -> r) -> (SOP I xss -> r) -> r
forall (a :: * -> *) (xss :: [[*]]) x r.
GSumTo a =>
SOP I (ToSumCode a xss) -> (a x -> r) -> (SOP I xss -> r) -> r
gSumTo SOP I (ToSumCode b xss)
r ((:+:) a b x -> r
s ((:+:) a b x -> r) -> (b x -> (:+:) a b x) -> b x -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b x -> (:+:) a b x
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1) SOP I xss -> r
k)
instance (GProductTo a) => GSumTo (M1 C c a) where
gSumTo :: forall (xss :: [[*]]) x r.
SOP I (ToSumCode (M1 C c a) xss)
-> (M1 C c a x -> r) -> (SOP I xss -> r) -> r
gSumTo (SOP (Z NP I x
xs)) M1 C c a x -> r
s SOP I xss -> r
_ = M1 C c a x -> r
s (a x -> M1 C c a x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (NP I (ToProductCode a '[]) -> (a x -> NP I '[] -> a x) -> a x
forall (xs :: [*]) x r.
NP I (ToProductCode a xs) -> (a x -> NP I xs -> r) -> r
forall (a :: * -> *) (xs :: [*]) x r.
GProductTo a =>
NP I (ToProductCode a xs) -> (a x -> NP I xs -> r) -> r
gProductTo NP I x
NP I (ToProductCode a '[])
xs ((\ a x
x NP I '[]
Nil -> a x
x) :: a x -> NP I '[] -> a x)))
gSumTo (SOP (S NS (NP I) xs
xs)) M1 C c a x -> r
_ SOP I xss -> r
k = SOP I xss -> r
k (NS (NP I) xss -> SOP I xss
forall k (f :: k -> *) (xss :: [[k]]). NS (NP f) xss -> SOP f xss
SOP NS (NP I) xss
NS (NP I) xs
xs)
instance (GSumTo a) => GSumTo (M1 D c a) where
gSumTo :: forall (xss :: [[*]]) x r.
SOP I (ToSumCode (M1 D c a) xss)
-> (M1 D c a x -> r) -> (SOP I xss -> r) -> r
gSumTo SOP I (ToSumCode (M1 D c a) xss)
xss M1 D c a x -> r
s SOP I xss -> r
k = SOP I (ToSumCode a xss) -> (a x -> r) -> (SOP I xss -> r) -> r
forall (xss :: [[*]]) x r.
SOP I (ToSumCode a xss) -> (a x -> r) -> (SOP I xss -> r) -> r
forall (a :: * -> *) (xss :: [[*]]) x r.
GSumTo a =>
SOP I (ToSumCode a xss) -> (a x -> r) -> (SOP I xss -> r) -> r
gSumTo SOP I (ToSumCode a xss)
SOP I (ToSumCode (M1 D c a) xss)
xss (M1 D c a x -> r
s (M1 D c a x -> r) -> (a x -> M1 D c a x) -> a x -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a x -> M1 D c a x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1) SOP I xss -> r
k
type GCode (a :: Type) = ToSumCode (GHC.Rep a) '[]
type GFrom a = GSumFrom (GHC.Rep a)
type GTo a = GSumTo (GHC.Rep a)
type GDatatypeInfo a = SOP.T.DemoteDatatypeInfo (GDatatypeInfoOf a) (GCode a)
type GDatatypeInfoOf (a :: Type) = ToInfo (GHC.Rep a)
gfrom :: (GFrom a, GHC.Generic a) => a -> SOP I (GCode a)
gfrom :: forall a. (GFrom a, Generic a) => a -> SOP I (GCode a)
gfrom a
x = Rep a Any -> Proxy '[] -> SOP I (ToSumCode (Rep a) '[])
forall x (proxy :: [[*]] -> *) (xss :: [[*]]).
Rep a x -> proxy xss -> SOP I (ToSumCode (Rep a) xss)
forall (a :: * -> *) x (proxy :: [[*]] -> *) (xss :: [[*]]).
GSumFrom a =>
a x -> proxy xss -> SOP I (ToSumCode a xss)
gSumFrom (a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
GHC.from a
x) (Proxy '[]
forall {k}. Proxy '[]
forall {k} (t :: k). Proxy t
Proxy :: Proxy '[])
gto :: forall a. (GTo a, GHC.Generic a) => SOP I (GCode a) -> a
gto :: forall a. (GTo a, Generic a) => SOP I (GCode a) -> a
gto SOP I (GCode a)
x = Rep a Any -> a
forall a x. Generic a => Rep a x -> a
forall x. Rep a x -> a
GHC.to (SOP I (GCode a)
-> (Rep a Any -> Rep a Any)
-> (SOP I '[] -> Rep a Any)
-> Rep a Any
forall (xss :: [[*]]) x r.
SOP I (ToSumCode (Rep a) xss)
-> (Rep a x -> r) -> (SOP I xss -> r) -> r
forall (a :: * -> *) (xss :: [[*]]) x r.
GSumTo a =>
SOP I (ToSumCode a xss) -> (a x -> r) -> (SOP I xss -> r) -> r
gSumTo SOP I (GCode a)
x Rep a Any -> Rep a Any
forall a. a -> a
id ((\SOP I '[]
y -> case SOP I '[]
y of {}) :: SOP I '[] -> (GHC.Rep a) x))
gdatatypeInfo :: forall proxy a. (GDatatypeInfo a) => proxy a -> DatatypeInfo (GCode a)
gdatatypeInfo :: forall (proxy :: * -> *) a.
GDatatypeInfo a =>
proxy a -> DatatypeInfo (GCode a)
gdatatypeInfo proxy a
_ = Proxy (ToInfo (Rep a)) -> DatatypeInfo (ToSumCode (Rep a) '[])
forall (x :: DatatypeInfo) (xss :: [[*]])
(proxy :: DatatypeInfo -> *).
DemoteDatatypeInfo x xss =>
proxy x -> DatatypeInfo xss
forall (proxy :: DatatypeInfo -> *).
proxy (ToInfo (Rep a)) -> DatatypeInfo (ToSumCode (Rep a) '[])
SOP.T.demoteDatatypeInfo (Proxy (ToInfo (Rep a))
forall {k} (t :: k). Proxy t
Proxy :: Proxy (GDatatypeInfoOf a))