{-# 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
-- Copyright   :  (C) 2020 Csongor Kiss
-- License     :  BSD3
-- Maintainer  :  Csongor Kiss <kiss.csongor.kiss@gmail.com>
-- Stability   :  experimental
-- Portability :  non-portable
--
-- Structural subtype relationships between sum types.
--
-----------------------------------------------------------------------------

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 #-}

--------------------------------------------------------------------------------  

-- |As 'AsSubtype' but over generic representations as defined by
--  "GHC.Generics".
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 #-}