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

{-# OPTIONS_HADDOCK not-home #-}

module Polysemy.Internal.Union
  ( Union (..)
  , Weaving (..)
  , Member
  , MemberWithError
  , weave
  , hoist
  -- * Building Unions
  , inj
  , injUsing
  , injWeaving
  , weaken
  -- * Using Unions
  , decomp
  , prj
  , prjUsing
  , extract
  , absurdU
  , decompCoerce
  -- * Witnesses
  , ElemOf (..)
  , 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))

#ifndef NO_ERROR_MESSAGES
import Polysemy.Internal.CustomErrors
#endif


------------------------------------------------------------------------------
-- | 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 the effect @e@ is available somewhere inside of the effect
-- stack @r@.
type Member e r = MemberNoError e r

------------------------------------------------------------------------------
-- | Like 'Member', but will produce an error message if the types are
-- ambiguous. This is the constraint used for actions generated by
-- 'Polysemy.makeSem'.
--
-- /Be careful with this./ Due to quirks of 'GHC.TypeLits.TypeError',
-- the custom error messages emitted by this can potentially override other,
-- more helpful error messages.
-- See the discussion in
-- <https://github.com/polysemy-research/polysemy/issues/227 Issue #227>.
--
-- @since 1.2.3.0
type MemberWithError e r =
  ( MemberNoError e r
#ifndef NO_ERROR_MESSAGES
    -- NOTE: The plugin explicitly pattern matches on
    -- `WhenStuck (LocateEffect _ r) _`, so if you change this, make sure to change
    -- the corresponding implementation in
    -- Polysemy.Plugin.Fundep.solveBogusError
  , WhenStuck (LocateEffect e r) (AmbiguousSend e r)
#endif
  )

type MemberNoError e r =
  ( Find e r
#ifndef NO_ERROR_MESSAGES
  , LocateEffect e r ~ '()
#endif
  )

------------------------------------------------------------------------------
-- | 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
data ElemOf e r where
  -- | @e@ is located at the head of the list.
  Here  :: ElemOf e (e ': r)
  -- | @e@ is located somewhere in the tail of the list.
  There :: ElemOf e r -> ElemOf e (e' ': r)

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


------------------------------------------------------------------------------
-- | Used to detect ambiguous uses of effects. If @r@ isn't concrete,
-- and we haven't been given @'LocateEffect' e r ~ '()@ from a
-- @'Member' e r@ constraint, then @'LocateEffect' e r@ will get stuck.
type family LocateEffect (t :: k) (ts :: [k]) :: () where
#ifndef NO_ERROR_MESSAGES
  LocateEffect t '[] = UnhandledEffect t
#endif
  LocateEffect t (t ': ts) = '()
  LocateEffect t (u ': ts) = LocateEffect t ts

class Find (t :: k) (r :: [k]) where
  membership' :: ElemOf t r

instance {-# OVERLAPPING #-} Find t (t ': z) where
  membership' :: ElemOf t (t : z)
membership' = ElemOf t (t : z)
forall a (t :: a) (z :: [a]). ElemOf t (t : z)
Here
  {-# INLINE membership' #-}

instance Find t z => Find t (_1 ': z) where
  membership' :: ElemOf t (_1 : z)
membership' = ElemOf t z -> ElemOf t (_1 : z)
forall a (e :: a) (r :: [a]) (e' :: a).
ElemOf e r -> ElemOf e (e' : r)
There (ElemOf t z -> ElemOf t (_1 : z))
-> ElemOf t z -> ElemOf t (_1 : z)
forall a b. (a -> b) -> a -> b
$ Find t z => ElemOf t z
forall k (t :: k) (r :: [k]). Find 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 a (t :: a) (z :: [a]). ElemOf t (t : z)
Here
    Maybe (e :~: e')
_         -> ElemOf e' r -> ElemOf e' (e : r)
forall a (e :: a) (r :: [a]) (e' :: a).
ElemOf e r -> ElemOf e (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 a (r :: [a]) (e :: a).
(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 k (t :: k) (r :: [k]). Find 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 a (r :: [a]) (e :: a).
(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 a (e :: a) (r :: [a]) (e' :: a).
ElemOf e r -> ElemOf e (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 a (t :: a) (z :: [a]). ElemOf t (t : z)
Here
extendMembershipRight (There ElemOf e r
e) = ElemOf e (Append r r) -> ElemOf e (e' : Append r r)
forall a (e :: a) (r :: [a]) (e' :: a).
ElemOf e r -> ElemOf e (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 a (t :: a) (z :: [a]). ElemOf t (t : z)
Here
injectMembership (SCons SList xs
sl) SList mid
sm (There ElemOf e r
pr) = ElemOf e (Append xs (Append mid right))
-> ElemOf e (x : Append xs (Append mid right))
forall a (e :: a) (r :: [a]) (e' :: a).
ElemOf e r -> ElemOf e (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
#if __GLASGOW_HASKELL__ < 808
extract (Union (There g) _) = case g of {}
#endif
{-# INLINE extract #-}


------------------------------------------------------------------------------
-- | An empty union contains nothing, so this function is uncallable.
absurdU :: Union '[] m a -> b
#if __GLASGOW_HASKELL__ < 808
absurdU (Union pr _) = case pr of {}
#else
absurdU :: Union '[] m a -> b
absurdU = \case {}
#endif


------------------------------------------------------------------------------
-- | 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 a (e :: a) (r :: [a]) (e' :: a).
ElemOf e r -> ElemOf e (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 a (e :: a) (r :: [a]). Member e r => ElemOf e 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 a (e :: a) (r :: [a]). Member e r => ElemOf e 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 a (e :: a) (r :: [a]) (e' :: a).
ElemOf e r -> ElemOf e (e' : r)
There ElemOf e r
pr) Weaving e m a
a)
{-# INLINE decompCoerce #-}