{-# 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
( GAsSubtype (..)
) where
import Data.Generics.Product.Internal.HList
import Data.Generics.Sum.Internal.Typed
import Data.Kind
import GHC.Generics
import Data.Generics.Internal.Profunctor.Iso
import Data.Generics.Internal.Profunctor.Prism
import Data.Generics.Internal.Families.Has
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 (sub x) (sub x) -> p (sup x) (sup x)
_GSub f :: p (sub x) (sub x)
f = (sub x -> sup x)
-> (sup x -> Either (sup x) (sub x))
-> p (sub x) (sub x)
-> p (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 (sub x) (sub x)
f
{-# INLINE[0] _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 rep :: a x
rep) = a x -> sup x
forall (sub :: * -> *) (sup :: * -> *) x.
GSplash sub sup =>
sub x -> sup x
_GSplash a x
rep
_GSplash (R1 rep :: b x
rep) = b x -> sup x
forall (sub :: * -> *) (sup :: * -> *) x.
GSplash sub sup =>
sub x -> sup x
_GSplash b x
rep
{-# INLINE[0] _GSplash #-}
instance
( GIsList subf subf as as
, GAsType supf as
) => GSplash (C1 meta subf) supf where
_GSplash :: C1 meta subf x -> supf x
_GSplash p :: C1 meta subf x
p = (Tagged (C1 meta subf x) (C1 meta subf x)
-> Tagged (supf x) (supf x))
-> C1 meta subf x -> supf x
forall b t. (Tagged b b -> Tagged t t) -> b -> t
build (Tagged (HList as) (HList as) -> Tagged (supf x) (supf x)
forall (f :: * -> *) (as :: [*]) x.
GAsType f as =>
Prism (f x) (f x) (HList as) (HList as)
_GTyped (Tagged (HList as) (HList as) -> Tagged (supf x) (supf x))
-> (Tagged (C1 meta subf x) (C1 meta subf x)
-> Tagged (HList as) (HList as))
-> Tagged (C1 meta subf x) (C1 meta subf x)
-> Tagged (supf x) (supf x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Iso (C1 meta subf x) (C1 meta subf x) (HList as) (HList as)
-> Iso (HList as) (HList 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 (subf x) (subf x) -> p (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 (subf x) (subf x) -> p (C1 meta subf x) (C1 meta subf x))
-> (p (HList as) (HList as) -> p (subf x) (subf x))
-> p (HList as) (HList as)
-> p (C1 meta subf x) (C1 meta subf x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p (HList as) (HList as) -> p (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)) C1 meta subf x
p
{-# INLINE[0] _GSplash #-}
instance GSplash sub sup => GSplash (D1 c sub) sup where
_GSplash :: D1 c sub x -> sup x
_GSplash (M1 m :: sub x
m) = sub x -> sup x
forall (sub :: * -> *) (sup :: * -> *) x.
GSplash sub sup =>
sub x -> sup x
_GSplash sub x
m
{-# INLINE[0] _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 m :: 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 _ -> 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 r :: sub x
r -> sub x -> Either (C1 m sup x) (sub x)
forall a b. b -> Either a b
Right sub x
r
{-# INLINE[0] _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 x :: 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 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 r :: sub x
r -> sub x -> Either ((:+:) l r x) (sub x)
forall a b. b -> Either a b
Right sub x
r
_GDowncast (R1 x :: 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 _ -> (:+:) 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 r :: sub x
r -> sub x -> Either ((:+:) l r x) (sub x)
forall a b. b -> Either a b
Right sub x
r
{-# INLINE[0] _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 m :: 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 _ -> 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 r :: sub x
r -> sub x -> Either (D1 m sup x) (sub x)
forall a b. b -> Either a b
Right sub x
r
{-# INLINE[0] _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 :: sup x
sup = sup x -> Either (sup x) (sub x)
forall a b. a -> Either a b
Left sup x
sup
{-# INLINE[0] _GDowncastC #-}
instance
( GAsType sub subl
, GIsList sup sup subl subl
) => GDowncastC 'True sub sup where
_GDowncastC :: sup x -> Either (sup x) (sub x)
_GDowncastC sup :: sup x
sup = sub x -> Either (sup x) (sub x)
forall a b. b -> Either a b
Right ((Tagged (sup x) (sup x) -> Tagged (sub x) (sub x))
-> sup x -> sub x
forall b t. (Tagged b b -> Tagged t t) -> b -> t
build (Tagged (HList subl) (HList subl) -> Tagged (sub x) (sub x)
forall (f :: * -> *) (as :: [*]) x.
GAsType f as =>
Prism (f x) (f x) (HList as) (HList as)
_GTyped (Tagged (HList subl) (HList subl) -> Tagged (sub x) (sub x))
-> (Tagged (sup x) (sup x) -> Tagged (HList subl) (HList subl))
-> Tagged (sup x) (sup x)
-> Tagged (sub x) (sub x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Iso (sup x) (sup x) (HList subl) (HList subl)
-> Iso (HList subl) (HList subl) (sup x) (sup x)
forall s t a b. Iso s t a b -> Iso b a t s
fromIso forall (f :: * -> *) (g :: * -> *) (as :: [*]) (bs :: [*]) x.
GIsList f g as bs =>
Iso (f x) (g x) (HList as) (HList bs)
Iso (sup x) (sup x) (HList subl) (HList subl)
glist) sup x
sup)
{-# INLINE[0] _GDowncastC #-}