{-# LANGUAGE AllowAmbiguousTypes     #-}
{-# LANGUAGE CPP                     #-}
{-# LANGUAGE ConstraintKinds         #-}
{-# LANGUAGE EmptyCase               #-}
{-# LANGUAGE FlexibleInstances       #-}
{-# LANGUAGE FunctionalDependencies  #-}
{-# LANGUAGE InstanceSigs            #-}
{-# LANGUAGE MultiParamTypeClasses   #-}
{-# LANGUAGE PatternSynonyms         #-}
{-# LANGUAGE RoleAnnotations         #-}
{-# LANGUAGE StrictData              #-}
{-# LANGUAGE TypeFamilies            #-}
{-# LANGUAGE UndecidableInstances    #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# LANGUAGE ViewPatterns            #-}

{-# OPTIONS_HADDOCK not-home #-}

module Polysemy.Internal.Union
  ( Union (..)
  , Weaving (..)
  , Member
  , weave
  , hoist
  -- * Building Unions
  , inj
  , injUsing
  , injWeaving
  , weaken
  -- * Using Unions
  , decomp
  , prj
  , prjUsing
  , extract
  , absurdU
  , decompCoerce
  -- * Witnesses
  , ElemOf (Here, There)
  , membership
  , sameMember
  -- * Checking membership
  , KnownRow
  , tryMembership
  , extendMembershipLeft
  , extendMembershipRight
  , injectMembership
  , weakenList
  , weakenMid) where

import Control.Monad
import Data.Functor.Compose
import Data.Functor.Identity
import Data.Kind
import Data.Typeable
import Polysemy.Internal.Kind
import {-# SOURCE #-} Polysemy.Internal
import Polysemy.Internal.Sing (SList (SEnd, SCons))
import Unsafe.Coerce (unsafeCoerce)


------------------------------------------------------------------------------
-- | An extensible, type-safe union. The @r@ type parameter is a type-level
-- list of effects, any one of which may be held within the 'Union'.
data Union (r :: EffectRow) (mWoven :: Type -> Type) a where
  Union
      :: -- A proof that the effect is actually in @r@.
         ElemOf e r
         -- The effect to wrap. The functions 'prj' and 'decomp' can help
         -- retrieve this value later.
      -> Weaving e m a
      -> Union r m a

instance Functor (Union r mWoven) where
  fmap :: (a -> b) -> Union r mWoven a -> Union r mWoven b
fmap a -> b
f (Union ElemOf e r
w Weaving e mWoven a
t) = ElemOf e r -> Weaving e mWoven b -> Union r mWoven b
forall (e :: (* -> *) -> * -> *) (r :: EffectRow) (m :: * -> *) a.
ElemOf e r -> Weaving e m a -> Union r m a
Union ElemOf e r
w (Weaving e mWoven b -> Union r mWoven b)
-> Weaving e mWoven b -> Union r mWoven b
forall a b. (a -> b) -> a -> b
$ a -> b
f (a -> b) -> Weaving e mWoven a -> Weaving e mWoven b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Weaving e mWoven a
t
  {-# INLINE fmap #-}


data Weaving e mAfter resultType where
  Weaving
    :: forall f e rInitial a resultType mAfter. (Functor f)
    => {
      ()
weaveEffect :: e (Sem rInitial) a
      -- ^ The original effect GADT originally lifted via
      -- 'Polysemy.Internal.send'.
      -- ^ @rInitial@ is the effect row that was in scope when this 'Weaving'
      -- was originally created.
      , ()
weaveState :: f ()
      -- ^ A piece of state that other effects' interpreters have already
      -- woven through this 'Weaving'. @f@ is a 'Functor', so you can always
      -- 'fmap' into this thing.
      , ()
weaveDistrib :: forall x. f (Sem rInitial x) -> mAfter (f x)
      -- ^ Distribute @f@ by transforming @Sem rInitial@ into @mAfter@. This is
      -- usually of the form @f ('Polysemy.Sem' (Some ': Effects ': r) x) ->
      --   Sem r (f x)@
      , ()
weaveResult :: f a -> resultType
      -- ^ Even though @f a@ is the moral resulting type of 'Weaving', we
      -- can't expose that fact; such a thing would prevent 'Polysemy.Sem'
      -- from being a 'Monad'.
      , ()
weaveInspect :: forall x. f x -> Maybe x
      -- ^ A function for attempting to see inside an @f@. This is no
      -- guarantees that such a thing will succeed (for example,
      -- 'Polysemy.Error.Error' might have 'Polysemy.Error.throw'n.)
      } -> Weaving e mAfter resultType

instance Functor (Weaving e m) where
  fmap :: (a -> b) -> Weaving e m a -> Weaving e m b
fmap a -> b
f (Weaving e (Sem rInitial) a
e f ()
s forall x. f (Sem rInitial x) -> m (f x)
d f a -> a
f' forall x. f x -> Maybe x
v) = e (Sem rInitial) a
-> f ()
-> (forall x. f (Sem rInitial x) -> m (f x))
-> (f a -> b)
-> (forall x. f x -> Maybe x)
-> Weaving e m b
forall (f :: * -> *) (e :: (* -> *) -> * -> *)
       (rInitial :: EffectRow) a resultType (mAfter :: * -> *).
Functor f =>
e (Sem rInitial) a
-> f ()
-> (forall x. f (Sem rInitial x) -> mAfter (f x))
-> (f a -> resultType)
-> (forall x. f x -> Maybe x)
-> Weaving e mAfter resultType
Weaving e (Sem rInitial) a
e f ()
s forall x. f (Sem rInitial x) -> m (f x)
d (a -> b
f (a -> b) -> (f a -> a) -> f a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> a
f') forall x. f x -> Maybe x
v
  {-# INLINE fmap #-}



weave
    :: (Functor s, Functor n)
    => s ()
    -> (∀ x. s (m x) -> n (s x))
    -> (∀ x. s x -> Maybe x)
    -> Union r m a
    -> Union r n (s a)
weave :: s ()
-> (forall x. s (m x) -> n (s x))
-> (forall x. s x -> Maybe x)
-> Union r m a
-> Union r n (s a)
weave s ()
s' forall x. s (m x) -> n (s x)
d forall x. s x -> Maybe x
v' (Union ElemOf e r
w (Weaving e (Sem rInitial) a
e f ()
s forall x. f (Sem rInitial x) -> m (f x)
nt f a -> a
f forall x. f x -> Maybe x
v)) =
  ElemOf e r -> Weaving e n (s a) -> Union r n (s a)
forall (e :: (* -> *) -> * -> *) (r :: EffectRow) (m :: * -> *) a.
ElemOf e r -> Weaving e m a -> Union r m a
Union ElemOf e r
w (Weaving e n (s a) -> Union r n (s a))
-> Weaving e n (s a) -> Union r n (s a)
forall a b. (a -> b) -> a -> b
$ e (Sem rInitial) a
-> Compose s f ()
-> (forall x. Compose s f (Sem rInitial x) -> n (Compose s f x))
-> (Compose s f a -> s a)
-> (forall x. Compose s f x -> Maybe x)
-> Weaving e n (s a)
forall (f :: * -> *) (e :: (* -> *) -> * -> *)
       (rInitial :: EffectRow) a resultType (mAfter :: * -> *).
Functor f =>
e (Sem rInitial) a
-> f ()
-> (forall x. f (Sem rInitial x) -> mAfter (f x))
-> (f a -> resultType)
-> (forall x. f x -> Maybe x)
-> Weaving e mAfter resultType
Weaving
              e (Sem rInitial) a
e (s (f ()) -> Compose s f ()
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (s (f ()) -> Compose s f ()) -> s (f ()) -> Compose s f ()
forall a b. (a -> b) -> a -> b
$ f ()
s f () -> s () -> s (f ())
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ s ()
s')
              ((s (f x) -> Compose s f x) -> n (s (f x)) -> n (Compose s f x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap s (f x) -> Compose s f x
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (n (s (f x)) -> n (Compose s f x))
-> (Compose s f (Sem rInitial x) -> n (s (f x)))
-> Compose s f (Sem rInitial x)
-> n (Compose s f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. s (m (f x)) -> n (s (f x))
forall x. s (m x) -> n (s x)
d (s (m (f x)) -> n (s (f x)))
-> (Compose s f (Sem rInitial x) -> s (m (f x)))
-> Compose s f (Sem rInitial x)
-> n (s (f x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f (Sem rInitial x) -> m (f x))
-> s (f (Sem rInitial x)) -> s (m (f x))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (Sem rInitial x) -> m (f x)
forall x. f (Sem rInitial x) -> m (f x)
nt (s (f (Sem rInitial x)) -> s (m (f x)))
-> (Compose s f (Sem rInitial x) -> s (f (Sem rInitial x)))
-> Compose s f (Sem rInitial x)
-> s (m (f x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose s f (Sem rInitial x) -> s (f (Sem rInitial x))
forall k1 (f :: k1 -> *) k2 (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose)
              ((f a -> a) -> s (f a) -> s a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f a -> a
f (s (f a) -> s a)
-> (Compose s f a -> s (f a)) -> Compose s f a -> s a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose s f a -> s (f a)
forall k1 (f :: k1 -> *) k2 (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose)
              (f x -> Maybe x
forall x. f x -> Maybe x
v (f x -> Maybe x)
-> (Compose s f x -> Maybe (f x)) -> Compose s f x -> Maybe x
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< s (f x) -> Maybe (f x)
forall x. s x -> Maybe x
v' (s (f x) -> Maybe (f x))
-> (Compose s f x -> s (f x)) -> Compose s f x -> Maybe (f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose s f x -> s (f x)
forall k1 (f :: k1 -> *) k2 (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose)
{-# INLINE weave #-}


hoist
    :: (∀ x. m x -> n x)
    -> Union r m a
    -> Union r n a
hoist :: (forall x. m x -> n x) -> Union r m a -> Union r n a
hoist forall x. m x -> n x
f' (Union ElemOf e r
w (Weaving e (Sem rInitial) a
e f ()
s forall x. f (Sem rInitial x) -> m (f x)
nt f a -> a
f forall x. f x -> Maybe x
v)) =
  ElemOf e r -> Weaving e n a -> Union r n a
forall (e :: (* -> *) -> * -> *) (r :: EffectRow) (m :: * -> *) a.
ElemOf e r -> Weaving e m a -> Union r m a
Union ElemOf e r
w (Weaving e n a -> Union r n a) -> Weaving e n a -> Union r n a
forall a b. (a -> b) -> a -> b
$ e (Sem rInitial) a
-> f ()
-> (forall x. f (Sem rInitial x) -> n (f x))
-> (f a -> a)
-> (forall x. f x -> Maybe x)
-> Weaving e n a
forall (f :: * -> *) (e :: (* -> *) -> * -> *)
       (rInitial :: EffectRow) a resultType (mAfter :: * -> *).
Functor f =>
e (Sem rInitial) a
-> f ()
-> (forall x. f (Sem rInitial x) -> mAfter (f x))
-> (f a -> resultType)
-> (forall x. f x -> Maybe x)
-> Weaving e mAfter resultType
Weaving e (Sem rInitial) a
e f ()
s (m (f x) -> n (f x)
forall x. m x -> n x
f' (m (f x) -> n (f x))
-> (f (Sem rInitial x) -> m (f x)) -> f (Sem rInitial x) -> n (f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Sem rInitial x) -> m (f x)
forall x. f (Sem rInitial x) -> m (f x)
nt) f a -> a
f forall x. f x -> Maybe x
v
{-# INLINE hoist #-}

------------------------------------------------------------------------------
-- | A proof that @e@ is an element of @r@.
--
-- Due to technical reasons, @'ElemOf' e r@ is not powerful enough to
-- prove @'Member' e r@; however, it can still be used send actions of @e@
-- into @r@ by using 'Polysemy.Internal.subsumeUsing'.
--
-- @since 1.3.0.0
type role ElemOf nominal nominal
newtype ElemOf (e :: k) (r :: [k]) = UnsafeMkElemOf Int

data MatchHere e r where
  MHYes :: MatchHere e (e ': r)
  MHNo  :: MatchHere e r

data MatchThere e r where
  MTYes :: ElemOf e r -> MatchThere e (e' ': r)
  MTNo  :: MatchThere e r

matchHere :: forall e r. ElemOf e r -> MatchHere e r
matchHere :: ElemOf e r -> MatchHere e r
matchHere (UnsafeMkElemOf Int
0) = MatchHere Any (Any : Any) -> MatchHere e r
forall a b. a -> b
unsafeCoerce (MatchHere Any (Any : Any) -> MatchHere e r)
-> MatchHere Any (Any : Any) -> MatchHere e r
forall a b. (a -> b) -> a -> b
$ MatchHere Any (Any : Any)
forall a (e :: a) (r :: [a]). MatchHere e (e : r)
MHYes
matchHere ElemOf e r
_ = MatchHere e r
forall a (e :: a) (r :: [a]). MatchHere e r
MHNo

matchThere :: forall e r. ElemOf e r -> MatchThere e r
matchThere :: ElemOf e r -> MatchThere e r
matchThere (UnsafeMkElemOf Int
0) = MatchThere e r
forall a (e :: a) (r :: [a]). MatchThere e r
MTNo
matchThere (UnsafeMkElemOf Int
e) = MatchThere Any (Any : Any) -> MatchThere e r
forall a b. a -> b
unsafeCoerce (MatchThere Any (Any : Any) -> MatchThere e r)
-> MatchThere Any (Any : Any) -> MatchThere e r
forall a b. (a -> b) -> a -> b
$ ElemOf Any Any -> MatchThere Any (Any : Any)
forall a (e :: a) (r :: [a]) (e' :: a).
ElemOf e r -> MatchThere e (e' : r)
MTYes (ElemOf Any Any -> MatchThere Any (Any : Any))
-> ElemOf Any Any -> MatchThere Any (Any : Any)
forall a b. (a -> b) -> a -> b
$ Int -> ElemOf Any Any
forall k (e :: k) (r :: [k]). Int -> ElemOf e r
UnsafeMkElemOf (Int -> ElemOf Any Any) -> Int -> ElemOf Any Any
forall a b. (a -> b) -> a -> b
$ Int
e Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1

pattern Here :: () => (r ~ (e ': r')) => ElemOf e r
pattern $bHere :: ElemOf e r
$mHere :: forall r k (r :: [k]) (e :: k).
ElemOf e r
-> (forall (r' :: [k]). (r ~ (e : r')) => r) -> (Void# -> r) -> r
Here <- (matchHere -> MHYes)
  where
    Here = Int -> ElemOf e r
forall k (e :: k) (r :: [k]). Int -> ElemOf e r
UnsafeMkElemOf Int
0

pattern There :: () => (r' ~ (e' ': r)) => ElemOf e r -> ElemOf e r'
pattern $bThere :: ElemOf e r -> ElemOf e r'
$mThere :: forall r k (r' :: [k]) (e :: k).
ElemOf e r'
-> (forall (e' :: k) (r :: [k]).
    (r' ~ (e' : r)) =>
    ElemOf e r -> r)
-> (Void# -> r)
-> r
There e <- (matchThere -> MTYes e)
  where
    There (UnsafeMkElemOf Int
e) = Int -> ElemOf e r'
forall k (e :: k) (r :: [k]). Int -> ElemOf e r
UnsafeMkElemOf (Int -> ElemOf e r') -> Int -> ElemOf e r'
forall a b. (a -> b) -> a -> b
$ Int
e Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1

{-# COMPLETE Here, There #-}

------------------------------------------------------------------------------
-- | Checks if two membership proofs are equal. If they are, then that means
-- that the effects for which membership is proven must also be equal.
sameMember :: forall e e' r
            . ElemOf e r
           -> ElemOf e' r
           -> Maybe (e :~: e')
sameMember :: ElemOf e r -> ElemOf e' r -> Maybe (e :~: e')
sameMember ElemOf e r
Here       ElemOf e' r
Here =
  (e :~: e) -> Maybe (e :~: e)
forall a. a -> Maybe a
Just e :~: e
forall k (a :: k). a :~: a
Refl
sameMember (There ElemOf e r
pr) (There ElemOf e' r
pr') =
  ElemOf e r -> ElemOf e' r -> Maybe (e :~: e')
forall k (e :: k) (e' :: k) (r :: [k]).
ElemOf e r -> ElemOf e' r -> Maybe (e :~: e')
sameMember @e @e' ElemOf e r
pr ElemOf e' r
ElemOf e' r
pr'
sameMember (There ElemOf e r
_)  ElemOf e' r
_ =
  Maybe (e :~: e')
forall a. Maybe a
Nothing
sameMember ElemOf e r
_          ElemOf e' r
_ =
  Maybe (e :~: e')
forall a. Maybe a
Nothing


class Member (t :: Effect) (r :: EffectRow) where
  membership' :: ElemOf t r

instance {-# OVERLAPPING #-} Member t (t ': z) where
  membership' :: ElemOf t (t : z)
membership' = ElemOf t (t : z)
forall k (r :: [k]) (e :: k) (r' :: [k]).
(r ~ (e : r')) =>
ElemOf e r
Here
  {-# INLINE membership' #-}

instance Member t z => Member t (_1 ': z) where
  membership' :: ElemOf t (_1 : z)
membership' = ElemOf t z -> ElemOf t (_1 : z)
forall k (r' :: [k]) (e :: k) (e' :: k) (r :: [k]).
(r' ~ (e' : r)) =>
ElemOf e r -> ElemOf e r'
There (ElemOf t z -> ElemOf t (_1 : z))
-> ElemOf t z -> ElemOf t (_1 : z)
forall a b. (a -> b) -> a -> b
$ Member t z => ElemOf t z
forall (t :: (* -> *) -> * -> *) (r :: EffectRow).
Member t r =>
ElemOf t r
membership' @t @z
  {-# INLINE membership' #-}

------------------------------------------------------------------------------
-- | A class for effect rows whose elements are inspectable.
--
-- This constraint is eventually satisfied as @r@ is instantied to a
-- monomorphic list.
-- (E.g when @r@ becomes something like
-- @'['Polysemy.State.State' Int, 'Polysemy.Output.Output' String, 'Polysemy.Embed' IO]@)
class KnownRow r where
  tryMembership' :: forall e. Typeable e => Maybe (ElemOf e r)

instance KnownRow '[] where
  tryMembership' :: Maybe (ElemOf e '[])
tryMembership' = Maybe (ElemOf e '[])
forall a. Maybe a
Nothing
  {-# INLINE tryMembership' #-}

instance (Typeable e, KnownRow r) => KnownRow (e ': r) where
  tryMembership' :: forall e'. Typeable e' => Maybe (ElemOf e' (e ': r))
  tryMembership' :: Maybe (ElemOf e' (e : r))
tryMembership' = case (Typeable e, Typeable e') => Maybe (e :~: e')
forall k (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @e @e' of
    Just e :~: e'
Refl -> ElemOf e' (e : r) -> Maybe (ElemOf e' (e : r))
forall a. a -> Maybe a
Just ElemOf e' (e : r)
forall k (r :: [k]) (e :: k) (r' :: [k]).
(r ~ (e : r')) =>
ElemOf e r
Here
    Maybe (e :~: e')
_         -> ElemOf e' r -> ElemOf e' (e : r)
forall k (r' :: [k]) (e :: k) (e' :: k) (r :: [k]).
(r' ~ (e' : r)) =>
ElemOf e r -> ElemOf e r'
There (ElemOf e' r -> ElemOf e' (e : r))
-> Maybe (ElemOf e' r) -> Maybe (ElemOf e' (e : r))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Typeable e' => Maybe (ElemOf e' r)
forall k (r :: [k]) (e :: k).
(KnownRow r, Typeable e) =>
Maybe (ElemOf e r)
tryMembership' @r @e'
  {-# INLINE tryMembership' #-}

------------------------------------------------------------------------------
-- | Given @'Member' e r@, extract a proof that @e@ is an element of @r@.
membership :: Member e r => ElemOf e r
membership :: ElemOf e r
membership = ElemOf e r
forall (t :: (* -> *) -> * -> *) (r :: EffectRow).
Member t r =>
ElemOf t r
membership'
{-# INLINE membership #-}

------------------------------------------------------------------------------
-- | Extracts a proof that @e@ is an element of @r@ if that
-- is indeed the case; otherwise returns @Nothing@.
tryMembership :: forall e r. (Typeable e, KnownRow r) => Maybe (ElemOf e r)
tryMembership :: Maybe (ElemOf e r)
tryMembership = Typeable e => Maybe (ElemOf e r)
forall k (r :: [k]) (e :: k).
(KnownRow r, Typeable e) =>
Maybe (ElemOf e r)
tryMembership' @r @e
{-# INLINE tryMembership #-}


------------------------------------------------------------------------------
-- | Extends a proof that @e@ is an element of @r@ to a proof that @e@ is an
-- element of the concatenation of the lists @l@ and @r@.
-- @l@ must be specified as a singleton list proof.
extendMembershipLeft :: forall l r e. SList l -> ElemOf e r -> ElemOf e (Append l r)
extendMembershipLeft :: SList l -> ElemOf e r -> ElemOf e (Append l r)
extendMembershipLeft SList l
SEnd ElemOf e r
pr = ElemOf e r
ElemOf e (Append l r)
pr
extendMembershipLeft (SCons SList xs
l) ElemOf e r
pr = ElemOf e (Append xs r) -> ElemOf e (x : Append xs r)
forall k (r' :: [k]) (e :: k) (e' :: k) (r :: [k]).
(r' ~ (e' : r)) =>
ElemOf e r -> ElemOf e r'
There (SList xs -> ElemOf e r -> ElemOf e (Append xs r)
forall a (l :: [a]) (r :: [a]) (e :: a).
SList l -> ElemOf e r -> ElemOf e (Append l r)
extendMembershipLeft SList xs
l ElemOf e r
pr)
{-# INLINE extendMembershipLeft #-}


------------------------------------------------------------------------------
-- | Extends a proof that @e@ is an element of @l@ to a proof that @e@ is an
-- element of the concatenation of the lists @l@ and @r@.
extendMembershipRight :: forall l r e. ElemOf e l -> ElemOf e (Append l r)
extendMembershipRight :: ElemOf e l -> ElemOf e (Append l r)
extendMembershipRight ElemOf e l
Here = ElemOf e (Append l r)
forall k (r :: [k]) (e :: k) (r' :: [k]).
(r ~ (e : r')) =>
ElemOf e r
Here
extendMembershipRight (There ElemOf e r
e) = ElemOf e (Append r r) -> ElemOf e (e' : Append r r)
forall k (r' :: [k]) (e :: k) (e' :: k) (r :: [k]).
(r' ~ (e' : r)) =>
ElemOf e r -> ElemOf e r'
There (ElemOf e r -> ElemOf e (Append r r)
forall a (l :: [a]) (r :: [a]) (e :: a).
ElemOf e l -> ElemOf e (Append l r)
extendMembershipRight @_ @r ElemOf e r
e)
{-# INLINE extendMembershipRight #-}


------------------------------------------------------------------------------
-- | Extends a proof that @e@ is an element of @left <> right@ to a proof that
-- @e@ is an element of @left <> mid <> right@.
-- Both @left@ and @right@ must be specified as singleton list proofs.
injectMembership :: forall right e left mid
                  . SList left
                 -> SList mid
                 -> ElemOf e (Append left right)
                 -> ElemOf e (Append left (Append mid right))
injectMembership :: SList left
-> SList mid
-> ElemOf e (Append left right)
-> ElemOf e (Append left (Append mid right))
injectMembership SList left
SEnd SList mid
sm ElemOf e (Append left right)
pr = SList mid -> ElemOf e right -> ElemOf e (Append mid right)
forall a (l :: [a]) (r :: [a]) (e :: a).
SList l -> ElemOf e r -> ElemOf e (Append l r)
extendMembershipLeft SList mid
sm ElemOf e right
ElemOf e (Append left right)
pr
injectMembership (SCons SList xs
_) SList mid
_ ElemOf e (Append left right)
Here = ElemOf e (Append left (Append mid right))
forall k (r :: [k]) (e :: k) (r' :: [k]).
(r ~ (e : r')) =>
ElemOf e r
Here
injectMembership (SCons SList xs
sl) SList mid
sm (There pr) = ElemOf e (Append xs (Append mid right))
-> ElemOf e (x : Append xs (Append mid right))
forall k (r' :: [k]) (e :: k) (e' :: k) (r :: [k]).
(r' ~ (e' : r)) =>
ElemOf e r -> ElemOf e r'
There (SList xs
-> SList mid
-> ElemOf e (Append xs right)
-> ElemOf e (Append xs (Append mid right))
forall a (right :: [a]) (e :: a) (left :: [a]) (mid :: [a]).
SList left
-> SList mid
-> ElemOf e (Append left right)
-> ElemOf e (Append left (Append mid right))
injectMembership @right SList xs
sl SList mid
sm ElemOf e r
ElemOf e (Append xs right)
pr)
{-# INLINE injectMembership #-}


------------------------------------------------------------------------------
-- | Decompose a 'Union'. Either this union contains an effect @e@---the head
-- of the @r@ list---or it doesn't.
decomp :: Union (e ': r) m a -> Either (Union r m a) (Weaving e m a)
decomp :: Union (e : r) m a -> Either (Union r m a) (Weaving e m a)
decomp (Union ElemOf e (e : r)
p Weaving e m a
a) =
  case ElemOf e (e : r)
p of
    ElemOf e (e : r)
Here  -> Weaving e m a -> Either (Union r m a) (Weaving e m a)
forall a b. b -> Either a b
Right Weaving e m a
a
    There ElemOf e r
pr -> Union r m a -> Either (Union r m a) (Weaving e m a)
forall a b. a -> Either a b
Left (Union r m a -> Either (Union r m a) (Weaving e m a))
-> Union r m a -> Either (Union r m a) (Weaving e m a)
forall a b. (a -> b) -> a -> b
$ ElemOf e r -> Weaving e m a -> Union r m a
forall (e :: (* -> *) -> * -> *) (r :: EffectRow) (m :: * -> *) a.
ElemOf e r -> Weaving e m a -> Union r m a
Union ElemOf e r
pr Weaving e m a
a
{-# INLINE decomp #-}

------------------------------------------------------------------------------
-- | Retrieve the last effect in a 'Union'.
extract :: Union '[e] m a -> Weaving e m a
extract :: Union '[e] m a -> Weaving e m a
extract (Union ElemOf e '[e]
Here Weaving e m a
a)   = Weaving e m a
Weaving e m a
a
extract (Union (There ElemOf e r
_) Weaving e m a
_) = [Char] -> Weaving e m a
forall a. HasCallStack => [Char] -> a
error [Char]
"Unsafe use of UnsafeMkElemOf"
{-# INLINE extract #-}


------------------------------------------------------------------------------
-- | An empty union contains nothing, so this function is uncallable.
absurdU :: Union '[] m a -> b
absurdU :: Union '[] m a -> b
absurdU (Union ElemOf e '[]
_ Weaving e m a
_) = [Char] -> b
forall a. HasCallStack => [Char] -> a
error [Char]
"Unsafe use of UnsafeMkElemOf"


------------------------------------------------------------------------------
-- | Weaken a 'Union' so it is capable of storing a new sort of effect at the
-- head.
weaken :: forall e r m a. Union r m a -> Union (e ': r) m a
weaken :: Union r m a -> Union (e : r) m a
weaken (Union ElemOf e r
pr Weaving e m a
a) = ElemOf e (e : r) -> Weaving e m a -> Union (e : r) m a
forall (e :: (* -> *) -> * -> *) (r :: EffectRow) (m :: * -> *) a.
ElemOf e r -> Weaving e m a -> Union r m a
Union (ElemOf e r -> ElemOf e (e : r)
forall k (r' :: [k]) (e :: k) (e' :: k) (r :: [k]).
(r' ~ (e' : r)) =>
ElemOf e r -> ElemOf e r'
There ElemOf e r
pr) Weaving e m a
a
{-# INLINE weaken #-}


------------------------------------------------------------------------------
-- | Weaken a 'Union' so it is capable of storing a number of new effects at
-- the head, specified as a singleton list proof.
weakenList :: SList l -> Union r m a -> Union (Append l r) m a
weakenList :: SList l -> Union r m a -> Union (Append l r) m a
weakenList SList l
sl (Union ElemOf e r
pr Weaving e m a
e) = ElemOf e (Append l r) -> Weaving e m a -> Union (Append l r) m a
forall (e :: (* -> *) -> * -> *) (r :: EffectRow) (m :: * -> *) a.
ElemOf e r -> Weaving e m a -> Union r m a
Union (SList l -> ElemOf e r -> ElemOf e (Append l r)
forall a (l :: [a]) (r :: [a]) (e :: a).
SList l -> ElemOf e r -> ElemOf e (Append l r)
extendMembershipLeft SList l
sl ElemOf e r
pr) Weaving e m a
e
{-# INLINE weakenList #-}


------------------------------------------------------------------------------
-- | Weaken a 'Union' so it is capable of storing a number of new effects
-- somewhere within the previous effect list.
-- Both the prefix and the new effects are specified as singleton list proofs.
weakenMid :: forall right m a left mid
           . SList left -> SList mid
          -> Union (Append left right) m a
          -> Union (Append left (Append mid right)) m a
weakenMid :: SList left
-> SList mid
-> Union (Append left right) m a
-> Union (Append left (Append mid right)) m a
weakenMid SList left
sl SList mid
sm (Union ElemOf e (Append left right)
pr Weaving e m a
e) = ElemOf e (Append left (Append mid right))
-> Weaving e m a -> Union (Append left (Append mid right)) m a
forall (e :: (* -> *) -> * -> *) (r :: EffectRow) (m :: * -> *) a.
ElemOf e r -> Weaving e m a -> Union r m a
Union (SList left
-> SList mid
-> ElemOf e (Append left right)
-> ElemOf e (Append left (Append mid right))
forall a (right :: [a]) (e :: a) (left :: [a]) (mid :: [a]).
SList left
-> SList mid
-> ElemOf e (Append left right)
-> ElemOf e (Append left (Append mid right))
injectMembership @right SList left
sl SList mid
sm ElemOf e (Append left right)
pr) Weaving e m a
e
{-# INLINE weakenMid #-}


------------------------------------------------------------------------------
-- | Lift an effect @e@ into a 'Union' capable of holding it.
inj :: forall e r rInitial a. (Member e r) => e (Sem rInitial) a -> Union r (Sem rInitial) a
inj :: e (Sem rInitial) a -> Union r (Sem rInitial) a
inj e (Sem rInitial) a
e = Weaving e (Sem rInitial) a -> Union r (Sem rInitial) a
forall (e :: (* -> *) -> * -> *) (r :: EffectRow) (m :: * -> *) a.
Member e r =>
Weaving e m a -> Union r m a
injWeaving (Weaving e (Sem rInitial) a -> Union r (Sem rInitial) a)
-> Weaving e (Sem rInitial) a -> Union r (Sem rInitial) a
forall a b. (a -> b) -> a -> b
$ e (Sem rInitial) a
-> Identity ()
-> (forall x.
    Identity (Sem rInitial x) -> Sem rInitial (Identity x))
-> (Identity a -> a)
-> (forall x. Identity x -> Maybe x)
-> Weaving e (Sem rInitial) a
forall (f :: * -> *) (e :: (* -> *) -> * -> *)
       (rInitial :: EffectRow) a resultType (mAfter :: * -> *).
Functor f =>
e (Sem rInitial) a
-> f ()
-> (forall x. f (Sem rInitial x) -> mAfter (f x))
-> (f a -> resultType)
-> (forall x. f x -> Maybe x)
-> Weaving e mAfter resultType
Weaving
  e (Sem rInitial) a
e
  (() -> Identity ()
forall a. a -> Identity a
Identity ())
  ((x -> Identity x) -> Sem rInitial x -> Sem rInitial (Identity x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap x -> Identity x
forall a. a -> Identity a
Identity (Sem rInitial x -> Sem rInitial (Identity x))
-> (Identity (Sem rInitial x) -> Sem rInitial x)
-> Identity (Sem rInitial x)
-> Sem rInitial (Identity x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Identity (Sem rInitial x) -> Sem rInitial x
forall a. Identity a -> a
runIdentity)
  Identity a -> a
forall a. Identity a -> a
runIdentity
  (x -> Maybe x
forall a. a -> Maybe a
Just (x -> Maybe x) -> (Identity x -> x) -> Identity x -> Maybe x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Identity x -> x
forall a. Identity a -> a
runIdentity)
{-# INLINE inj #-}


------------------------------------------------------------------------------
-- | Lift an effect @e@ into a 'Union' capable of holding it,
-- given an explicit proof that the effect exists in @r@
injUsing :: forall e r rInitial a.
  ElemOf e r -> e (Sem rInitial) a -> Union r (Sem rInitial) a
injUsing :: ElemOf e r -> e (Sem rInitial) a -> Union r (Sem rInitial) a
injUsing ElemOf e r
pr e (Sem rInitial) a
e = ElemOf e r
-> Weaving e (Sem rInitial) a -> Union r (Sem rInitial) a
forall (e :: (* -> *) -> * -> *) (r :: EffectRow) (m :: * -> *) a.
ElemOf e r -> Weaving e m a -> Union r m a
Union ElemOf e r
pr (Weaving e (Sem rInitial) a -> Union r (Sem rInitial) a)
-> Weaving e (Sem rInitial) a -> Union r (Sem rInitial) a
forall a b. (a -> b) -> a -> b
$ e (Sem rInitial) a
-> Identity ()
-> (forall x.
    Identity (Sem rInitial x) -> Sem rInitial (Identity x))
-> (Identity a -> a)
-> (forall x. Identity x -> Maybe x)
-> Weaving e (Sem rInitial) a
forall (f :: * -> *) (e :: (* -> *) -> * -> *)
       (rInitial :: EffectRow) a resultType (mAfter :: * -> *).
Functor f =>
e (Sem rInitial) a
-> f ()
-> (forall x. f (Sem rInitial x) -> mAfter (f x))
-> (f a -> resultType)
-> (forall x. f x -> Maybe x)
-> Weaving e mAfter resultType
Weaving
  e (Sem rInitial) a
e
  (() -> Identity ()
forall a. a -> Identity a
Identity ())
  ((x -> Identity x) -> Sem rInitial x -> Sem rInitial (Identity x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap x -> Identity x
forall a. a -> Identity a
Identity (Sem rInitial x -> Sem rInitial (Identity x))
-> (Identity (Sem rInitial x) -> Sem rInitial x)
-> Identity (Sem rInitial x)
-> Sem rInitial (Identity x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Identity (Sem rInitial x) -> Sem rInitial x
forall a. Identity a -> a
runIdentity)
  Identity a -> a
forall a. Identity a -> a
runIdentity
  (x -> Maybe x
forall a. a -> Maybe a
Just (x -> Maybe x) -> (Identity x -> x) -> Identity x -> Maybe x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Identity x -> x
forall a. Identity a -> a
runIdentity)
{-# INLINE injUsing #-}

------------------------------------------------------------------------------
-- | Lift a @'Weaving' e@ into a 'Union' capable of holding it.
injWeaving :: forall e r m a. Member e r => Weaving e m a -> Union r m a
injWeaving :: Weaving e m a -> Union r m a
injWeaving = ElemOf e r -> Weaving e m a -> Union r m a
forall (e :: (* -> *) -> * -> *) (r :: EffectRow) (m :: * -> *) a.
ElemOf e r -> Weaving e m a -> Union r m a
Union ElemOf e r
forall (t :: (* -> *) -> * -> *) (r :: EffectRow).
Member t r =>
ElemOf t r
membership
{-# INLINE injWeaving #-}

------------------------------------------------------------------------------
-- | Attempt to take an @e@ effect out of a 'Union'.
prj :: forall e r m a
     . ( Member e r
       )
    => Union r m a
    -> Maybe (Weaving e m a)
prj :: Union r m a -> Maybe (Weaving e m a)
prj = ElemOf e r -> Union r m a -> Maybe (Weaving e m a)
forall (e :: (* -> *) -> * -> *) (r :: EffectRow) (m :: * -> *) a.
ElemOf e r -> Union r m a -> Maybe (Weaving e m a)
prjUsing ElemOf e r
forall (t :: (* -> *) -> * -> *) (r :: EffectRow).
Member t r =>
ElemOf t r
membership
{-# INLINE prj #-}

------------------------------------------------------------------------------
-- | Attempt to take an @e@ effect out of a 'Union', given an explicit
-- proof that the effect exists in @r@.
prjUsing
  :: forall e r m a
   . ElemOf e r
  -> Union r m a
  -> Maybe (Weaving e m a)
prjUsing :: ElemOf e r -> Union r m a -> Maybe (Weaving e m a)
prjUsing ElemOf e r
pr (Union ElemOf e r
sn Weaving e m a
a) = (\e :~: e
Refl -> Weaving e m a
Weaving e m a
a) ((e :~: e) -> Weaving e m a)
-> Maybe (e :~: e) -> Maybe (Weaving e m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ElemOf e r -> ElemOf e r -> Maybe (e :~: e)
forall k (e :: k) (e' :: k) (r :: [k]).
ElemOf e r -> ElemOf e' r -> Maybe (e :~: e')
sameMember ElemOf e r
pr ElemOf e r
sn
{-# INLINE prjUsing #-}

------------------------------------------------------------------------------
-- | Like 'decomp', but allows for a more efficient
-- 'Polysemy.Interpretation.reinterpret' function.
decompCoerce
    :: Union (e ': r) m a
    -> Either (Union (f ': r) m a) (Weaving e m a)
decompCoerce :: Union (e : r) m a -> Either (Union (f : r) m a) (Weaving e m a)
decompCoerce (Union ElemOf e (e : r)
p Weaving e m a
a) =
  case ElemOf e (e : r)
p of
    ElemOf e (e : r)
Here  -> Weaving e m a -> Either (Union (f : r) m a) (Weaving e m a)
forall a b. b -> Either a b
Right Weaving e m a
a
    There ElemOf e r
pr -> Union (f : r) m a -> Either (Union (f : r) m a) (Weaving e m a)
forall a b. a -> Either a b
Left (ElemOf e (f : r) -> Weaving e m a -> Union (f : r) m a
forall (e :: (* -> *) -> * -> *) (r :: EffectRow) (m :: * -> *) a.
ElemOf e r -> Weaving e m a -> Union r m a
Union (ElemOf e r -> ElemOf e (f : r)
forall k (r' :: [k]) (e :: k) (e' :: k) (r :: [k]).
(r' ~ (e' : r)) =>
ElemOf e r -> ElemOf e r'
There ElemOf e r
pr) Weaving e m a
a)
{-# INLINE decompCoerce #-}