{-# LANGUAGE MonoLocalBinds #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.Generics.Sum.Internal.Subtype
( Context
, derived
) where
import Data.Generics.Product.Internal.HList
import Data.Generics.Sum.Internal.Typed (GAsType (..))
import Data.Kind
import GHC.Generics
import Data.Generics.Internal.Profunctor.Iso
import Data.Generics.Internal.Profunctor.Prism
import Data.Generics.Internal.Families.Has
type Context sub sup
= ( Generic sub
, Generic sup
, GAsSubtype (Rep sub) (Rep sup)
)
derived :: Context sub sup => Prism' sup sub
derived :: Prism' sup sub
derived = p i (Rep sup Any) (Rep sup Any) -> p i sup sup
forall a b x. (Generic a, Generic b) => Iso a b (Rep a x) (Rep b x)
repIso (p i (Rep sup Any) (Rep sup Any) -> p i sup sup)
-> (p i sub sub -> p i (Rep sup Any) (Rep sup Any))
-> p i sub sub
-> p i sup sup
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p i (Rep sub Any) (Rep sub Any) -> p i (Rep sup Any) (Rep sup Any)
forall (subf :: * -> *) (supf :: * -> *) x.
GAsSubtype subf supf =>
Prism' (supf x) (subf x)
_GSub (p i (Rep sub Any) (Rep sub Any)
-> p i (Rep sup Any) (Rep sup Any))
-> (p i sub sub -> p i (Rep sub Any) (Rep sub Any))
-> p i sub sub
-> p i (Rep sup Any) (Rep sup Any)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Iso sub sub (Rep sub Any) (Rep sub Any)
-> Iso (Rep sub Any) (Rep sub Any) sub sub
forall s t a b. Iso s t a b -> Iso b a t s
fromIso forall a b x. (Generic a, Generic b) => Iso a b (Rep a x) (Rep b x)
Iso sub sub (Rep sub Any) (Rep sub Any)
repIso
{-# INLINE derived #-}
class GAsSubtype (subf :: Type -> Type) (supf :: Type -> Type) where
_GSub :: Prism' (supf x) (subf x)
instance
( GSplash sub sup
, GDowncast sub sup
) => GAsSubtype sub sup where
_GSub :: p i (sub x) (sub x) -> p i (sup x) (sup x)
_GSub p i (sub x) (sub x)
f = (sub x -> sup x)
-> (sup x -> Either (sup x) (sub x))
-> p i (sub x) (sub x)
-> p i (sup x) (sup x)
forall b t s a. (b -> t) -> (s -> Either t a) -> Prism s t a b
prism sub x -> sup x
forall (sub :: * -> *) (sup :: * -> *) x.
GSplash sub sup =>
sub x -> sup x
_GSplash sup x -> Either (sup x) (sub x)
forall k (sub :: k -> *) (sup :: k -> *) (x :: k).
GDowncast sub sup =>
sup x -> Either (sup x) (sub x)
_GDowncast p i (sub x) (sub x)
f
{-# INLINE _GSub #-}
class GSplash (sub :: Type -> Type) (sup :: Type -> Type) where
_GSplash :: sub x -> sup x
instance (GSplash a sup, GSplash b sup) => GSplash (a :+: b) sup where
_GSplash :: (:+:) a b x -> sup x
_GSplash (L1 a x
rep) = a x -> sup x
forall (sub :: * -> *) (sup :: * -> *) x.
GSplash sub sup =>
sub x -> sup x
_GSplash a x
rep
_GSplash (R1 b x
rep) = b x -> sup x
forall (sub :: * -> *) (sup :: * -> *) x.
GSplash sub sup =>
sub x -> sup x
_GSplash b x
rep
{-# INLINE _GSplash #-}
instance
( GIsList subf subf as as
, ListTuple as' as' as as
, GAsType supf as'
) => GSplash (C1 meta subf) supf where
_GSplash :: C1 meta subf x -> supf x
_GSplash C1 meta subf x
p = (Tagged Any (C1 meta subf x) (C1 meta subf x)
-> Tagged Any (supf x) (supf x))
-> C1 meta subf x -> supf x
forall i b t. (Tagged i b b -> Tagged i t t) -> b -> t
build (Tagged Any as' as' -> Tagged Any (supf x) (supf x)
forall (f :: * -> *) as x. GAsType f as => Prism (f x) (f x) as as
_GTyped (Tagged Any as' as' -> Tagged Any (supf x) (supf x))
-> (Tagged Any (C1 meta subf x) (C1 meta subf x)
-> Tagged Any as' as')
-> Tagged Any (C1 meta subf x) (C1 meta subf x)
-> Tagged Any (supf x) (supf x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Iso (C1 meta subf x) (C1 meta subf x) as' as'
-> Iso as' as' (C1 meta subf x) (C1 meta subf x)
forall s t a b. Iso s t a b -> Iso b a t s
fromIso (p i (subf x) (subf x) -> p i (C1 meta subf x) (C1 meta subf x)
forall i (c :: Meta) (f :: * -> *) p (g :: * -> *).
Iso (M1 i c f p) (M1 i c g p) (f p) (g p)
mIso (p i (subf x) (subf x) -> p i (C1 meta subf x) (C1 meta subf x))
-> (p i as' as' -> p i (subf x) (subf x))
-> p i as' as'
-> p i (C1 meta subf x) (C1 meta subf x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p i (HList as) (HList as) -> p i (subf x) (subf x)
forall (f :: * -> *) (g :: * -> *) (as :: [*]) (bs :: [*]) x.
GIsList f g as bs =>
Iso (f x) (g x) (HList as) (HList bs)
glist (p i (HList as) (HList as) -> p i (subf x) (subf x))
-> (p i as' as' -> p i (HList as) (HList as))
-> p i as' as'
-> p i (subf x) (subf x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p i as' as' -> p i (HList as) (HList as)
forall tuple tuple' (as :: [*]) (bs :: [*]).
ListTuple tuple tuple' as bs =>
Iso (HList as) (HList bs) tuple tuple'
tupled)) C1 meta subf x
p
{-# INLINE _GSplash #-}
instance GSplash sub sup => GSplash (D1 c sub) sup where
_GSplash :: D1 c sub x -> sup x
_GSplash (M1 sub x
m) = sub x -> sup x
forall (sub :: * -> *) (sup :: * -> *) x.
GSplash sub sup =>
sub x -> sup x
_GSplash sub x
m
{-# INLINE _GSplash #-}
class GDowncast sub sup where
_GDowncast :: sup x -> Either (sup x) (sub x)
instance
( GIsList sup sup as as
, GDowncastC (HasPartialTypeP as sub) sub sup
) => GDowncast sub (C1 m sup) where
_GDowncast :: C1 m sup x -> Either (C1 m sup x) (sub x)
_GDowncast (M1 sup x
m) = case sup x -> Either (sup x) (sub x)
forall k (contains :: Bool) (sub :: k -> *) (sup :: k -> *)
(x :: k).
GDowncastC contains sub sup =>
sup x -> Either (sup x) (sub x)
_GDowncastC @(HasPartialTypeP as sub) sup x
m of
Left sup x
_ -> C1 m sup x -> Either (C1 m sup x) (sub x)
forall a b. a -> Either a b
Left (sup x -> C1 m sup x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 sup x
m)
Right sub x
r -> sub x -> Either (C1 m sup x) (sub x)
forall a b. b -> Either a b
Right sub x
r
{-# INLINE _GDowncast #-}
instance (GDowncast sub l, GDowncast sub r) => GDowncast sub (l :+: r) where
_GDowncast :: (:+:) l r x -> Either ((:+:) l r x) (sub x)
_GDowncast (L1 l x
x) = case l x -> Either (l x) (sub x)
forall k (sub :: k -> *) (sup :: k -> *) (x :: k).
GDowncast sub sup =>
sup x -> Either (sup x) (sub x)
_GDowncast l x
x of
Left l x
_ -> (:+:) l r x -> Either ((:+:) l r x) (sub x)
forall a b. a -> Either a b
Left (l x -> (:+:) l r x
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 l x
x)
Right sub x
r -> sub x -> Either ((:+:) l r x) (sub x)
forall a b. b -> Either a b
Right sub x
r
_GDowncast (R1 r x
x) = case r x -> Either (r x) (sub x)
forall k (sub :: k -> *) (sup :: k -> *) (x :: k).
GDowncast sub sup =>
sup x -> Either (sup x) (sub x)
_GDowncast r x
x of
Left r x
_ -> (:+:) l r x -> Either ((:+:) l r x) (sub x)
forall a b. a -> Either a b
Left (r x -> (:+:) l r x
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 r x
x)
Right sub x
r -> sub x -> Either ((:+:) l r x) (sub x)
forall a b. b -> Either a b
Right sub x
r
{-# INLINE _GDowncast #-}
instance GDowncast sub sup => GDowncast sub (D1 m sup) where
_GDowncast :: D1 m sup x -> Either (D1 m sup x) (sub x)
_GDowncast (M1 sup x
m) = case sup x -> Either (sup x) (sub x)
forall k (sub :: k -> *) (sup :: k -> *) (x :: k).
GDowncast sub sup =>
sup x -> Either (sup x) (sub x)
_GDowncast sup x
m of
Left sup x
_ -> D1 m sup x -> Either (D1 m sup x) (sub x)
forall a b. a -> Either a b
Left (sup x -> D1 m sup x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 sup x
m)
Right sub x
r -> sub x -> Either (D1 m sup x) (sub x)
forall a b. b -> Either a b
Right sub x
r
{-# INLINE _GDowncast #-}
class GDowncastC (contains :: Bool) sub sup where
_GDowncastC :: sup x -> Either (sup x) (sub x)
instance GDowncastC 'False sub sup where
_GDowncastC :: sup x -> Either (sup x) (sub x)
_GDowncastC sup x
sup = sup x -> Either (sup x) (sub x)
forall a b. a -> Either a b
Left sup x
sup
{-# INLINE _GDowncastC #-}
instance
( GAsType sub subl'
, GIsList sup sup subl subl
, ListTuple subl' subl' subl subl
) => GDowncastC 'True sub sup where
_GDowncastC :: sup x -> Either (sup x) (sub x)
_GDowncastC sup x
sup = sub x -> Either (sup x) (sub x)
forall a b. b -> Either a b
Right ((Tagged Any (sup x) (sup x) -> Tagged Any (sub x) (sub x))
-> sup x -> sub x
forall i b t. (Tagged i b b -> Tagged i t t) -> b -> t
build (Tagged Any subl' subl' -> Tagged Any (sub x) (sub x)
forall (f :: * -> *) as x. GAsType f as => Prism (f x) (f x) as as
_GTyped (Tagged Any subl' subl' -> Tagged Any (sub x) (sub x))
-> (Tagged Any (sup x) (sup x) -> Tagged Any subl' subl')
-> Tagged Any (sup x) (sup x)
-> Tagged Any (sub x) (sub x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Iso (sup x) (sup x) subl' subl' -> Iso subl' subl' (sup x) (sup x)
forall s t a b. Iso s t a b -> Iso b a t s
fromIso (p i (HList subl) (HList subl) -> p i (sup x) (sup x)
forall (f :: * -> *) (g :: * -> *) (as :: [*]) (bs :: [*]) x.
GIsList f g as bs =>
Iso (f x) (g x) (HList as) (HList bs)
glist (p i (HList subl) (HList subl) -> p i (sup x) (sup x))
-> (p i subl' subl' -> p i (HList subl) (HList subl))
-> p i subl' subl'
-> p i (sup x) (sup x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p i subl' subl' -> p i (HList subl) (HList subl)
forall tuple tuple' (as :: [*]) (bs :: [*]).
ListTuple tuple tuple' as bs =>
Iso (HList as) (HList bs) tuple tuple'
tupled)) sup x
sup)
{-# INLINE _GDowncastC #-}