{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE UnboxedTuples       #-}
{-# OPTIONS_HADDOCK not-home #-}
-- | This module contains functions for interpreting effects. Most of the times you won't need to import this directly;
-- the module "Cleff" reexports most of the functionalities.
--
-- __This is an /internal/ module and its API may change even between minor versions.__ Therefore you should be
-- extra careful if you're to depend on this module.
module Cleff.Internal.Interpret where

import           Cleff.Internal.Effect
import           Cleff.Internal.Monad
import           Data.Mem              (MemPtr)
import qualified Data.Mem              as Mem
import           Data.Rec              (pattern (:++:))
import qualified Data.Rec              as Env
import           Unsafe.Coerce         (unsafeCoerce)

-- * Trivial handling

-- | Lift a computation into a bigger effect stack with one more effect. For a more general version see 'raiseN'.
raise :: ∀ e es. Eff es ~> Eff (e ': es)
raise :: Eff es a -> Eff (e : es) a
raise = forall (es :: [(Type -> Type) -> Type -> Type]).
KnownList '[e] =>
Eff es ~> Eff ('[e] ++ es)
forall (es' :: [(Type -> Type) -> Type -> Type])
       (es :: [(Type -> Type) -> Type -> Type]).
KnownList es' =>
Eff es ~> Eff (es' ++ es)
raiseN @'[e]

-- | Lift a computation into a bigger effect stack with arbitrarily more effects. This function requires
-- @TypeApplications@.
raiseN :: ∀ es' es. KnownList es' => Eff es ~> Eff (es' ++ es)
raiseN :: Eff es ~> Eff (es' ++ es)
raiseN Eff es a
m = (Env (es' ++ es) -> IO a) -> Eff (es' ++ es) a
forall (es :: [(Type -> Type) -> Type -> Type]) a.
(Env es -> IO a) -> Eff es a
Eff (Eff es a -> Env es -> IO a
forall (es :: [(Type -> Type) -> Type -> Type]) a.
Eff es a -> Env es -> IO a
unEff Eff es a
m (Env es -> IO a)
-> (Env (es' ++ es) -> Env es) -> Env (es' ++ es) -> IO a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Rec (MemPtr InternalHandler) (es' ++ es)
 -> Rec (MemPtr InternalHandler) es)
-> Env (es' ++ es) -> Env es
forall k (es' :: [k]) (es :: [k]) (f :: k -> Type).
(Rec (MemPtr f) es -> Rec (MemPtr f) es') -> Mem f es -> Mem f es'
Mem.adjust (forall (es' :: [(Type -> Type) -> Type -> Type])
       (f :: ((Type -> Type) -> Type -> Type) -> Type).
KnownList es' =>
Rec f (es' ++ es') -> Rec f es'
forall k (es :: [k]) (es' :: [k]) (f :: k -> Type).
KnownList es =>
Rec f (es ++ es') -> Rec f es'
Env.drop @es'))

-- | Lift a computation with a fixed, known effect stack into some superset of the stack.
inject :: ∀ es' es. Subset es' es => Eff es' ~> Eff es
inject :: Eff es' ~> Eff es
inject Eff es' a
m = (Env es -> IO a) -> Eff es a
forall (es :: [(Type -> Type) -> Type -> Type]) a.
(Env es -> IO a) -> Eff es a
Eff (Eff es' a -> Env es' -> IO a
forall (es :: [(Type -> Type) -> Type -> Type]) a.
Eff es a -> Env es -> IO a
unEff Eff es' a
m (Env es' -> IO a) -> (Env es -> Env es') -> Env es -> IO a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Rec (MemPtr InternalHandler) es
 -> Rec (MemPtr InternalHandler) es')
-> Env es -> Env es'
forall k (es' :: [k]) (es :: [k]) (f :: k -> Type).
(Rec (MemPtr f) es -> Rec (MemPtr f) es') -> Mem f es -> Mem f es'
Mem.adjust (forall (es' :: [(Type -> Type) -> Type -> Type])
       (f :: ((Type -> Type) -> Type -> Type) -> Type).
Subset es' es' =>
Rec f es' -> Rec f es'
forall k (es :: [k]) (es' :: [k]) (f :: k -> Type).
Subset es es' =>
Rec f es' -> Rec f es
Env.pick @es'))

-- | Eliminate a duplicate effect from the top of the effect stack. For a more general version see 'subsumeN'.
subsume :: ∀ e es. e :> es => Eff (e ': es) ~> Eff es
subsume :: Eff (e : es) ~> Eff es
subsume = forall (es :: [(Type -> Type) -> Type -> Type]).
Subset '[e] es =>
Eff ('[e] ++ es) ~> Eff es
forall (es' :: [(Type -> Type) -> Type -> Type])
       (es :: [(Type -> Type) -> Type -> Type]).
Subset es' es =>
Eff (es' ++ es) ~> Eff es
subsumeN @'[e]

-- | Eliminate several duplicate effects from the top of the effect stack. This function requires @TypeApplications@.
subsumeN :: ∀ es' es. Subset es' es => Eff (es' ++ es) ~> Eff es
subsumeN :: Eff (es' ++ es) ~> Eff es
subsumeN Eff (es' ++ es) a
m = (Env es -> IO a) -> Eff es a
forall (es :: [(Type -> Type) -> Type -> Type]) a.
(Env es -> IO a) -> Eff es a
Eff (Eff (es' ++ es) a -> Env (es' ++ es) -> IO a
forall (es :: [(Type -> Type) -> Type -> Type]) a.
Eff es a -> Env es -> IO a
unEff Eff (es' ++ es) a
m (Env (es' ++ es) -> IO a)
-> (Env es -> Env (es' ++ es)) -> Env es -> IO a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Rec (MemPtr InternalHandler) es
 -> Rec (MemPtr InternalHandler) (es' ++ es))
-> Env es -> Env (es' ++ es)
forall k (es' :: [k]) (es :: [k]) (f :: k -> Type).
(Rec (MemPtr f) es -> Rec (MemPtr f) es') -> Mem f es -> Mem f es'
Mem.adjust (\Rec (MemPtr InternalHandler) es
re -> Rec (MemPtr InternalHandler) es -> Rec (MemPtr InternalHandler) es'
forall k (es :: [k]) (es' :: [k]) (f :: k -> Type).
Subset es es' =>
Rec f es' -> Rec f es
Env.pick @es' Rec (MemPtr InternalHandler) es
re Rec (MemPtr InternalHandler) es'
-> Rec (MemPtr InternalHandler) es
-> Rec (MemPtr InternalHandler) (es' ++ es)
forall a (es :: [a]) (es' :: [a]) (f :: a -> Type).
KnownList es =>
Rec f es -> Rec f es' -> Rec f (es ++ es')
:++: Rec (MemPtr InternalHandler) es
re))

-- * Handler types

-- | The send-site environment.
data SendSite e esSend = SendSite
  {-# UNPACK #-} !(MemPtr InternalHandler e) -- ^ The pointer to the effect handler of the effect being handled.
  {-# UNPACK #-} !(Env esSend) -- ^ The send-site 'Env'.

-- | The typeclass that indicates a handler scope, handling effect @e@ sent from the effect stack @esSend@ in the
-- effect stack @es@.
--
-- You should not define instances for this typeclass whatsoever.
class Handling e es esSend | e -> es esSend, es -> e esSend, esSend -> e es where
  -- | Obtain the send-site environment.
  sendSite :: SendSite e esSend
  sendSite = [Char] -> SendSite e esSend
forall a. HasCallStack => [Char] -> a
error
    [Char]
"Cleff.Internal.Interpret.sendSite: Attempting to access the send site without a reflected value. This is perhaps \
    \because you are trying to define an instance for the 'Handling' typeclass, which you should not be doing \
    \whatsoever. If that or other shenanigans seem unlikely, please report this as a bug."

-- | Get the pointer to the current effect handler itself.
hdlPtr :: Handling e es esSend => MemPtr InternalHandler e
hdlPtr :: MemPtr InternalHandler e
hdlPtr = let SendSite MemPtr InternalHandler e
ptr Env esSend
_ = SendSite e esSend
forall k (e :: (Type -> Type) -> Type -> Type) (es :: k)
       (esSend :: [(Type -> Type) -> Type -> Type]).
Handling e es esSend =>
SendSite e esSend
sendSite in MemPtr InternalHandler e
ptr
{-# INLINE hdlPtr #-}

-- | Get the send-site 'Env'.
sendEnv :: Handling e es esSend => Env esSend
sendEnv :: Env esSend
sendEnv = let SendSite MemPtr InternalHandler e
_ Env esSend
env = SendSite e esSend
forall k (e :: (Type -> Type) -> Type -> Type) (es :: k)
       (esSend :: [(Type -> Type) -> Type -> Type]).
Handling e es esSend =>
SendSite e esSend
sendSite in Env esSend
env
{-# INLINE sendEnv #-}

-- | Newtype wrapper for instantiating the 'Handling' typeclass locally, a la the reflection trick. We do not use
-- the @reflection@ library directly so as not to expose this piece of implementation detail to the user.
newtype InstHandling e es esSend a = InstHandling (Handling e es esSend => a)

-- | Instantiate an 'Handling' typeclass, i.e. pass an implicit send-site environment in. This function shouldn't
-- be directly used anyhow.
instHandling :: ∀ e es esSend a. (Handling e es esSend => a) -> SendSite e esSend -> a
instHandling :: (Handling e es esSend => a) -> SendSite e esSend -> a
instHandling Handling e es esSend => a
x = InstHandling e es esSend a -> SendSite e esSend -> a
forall a b. a -> b
unsafeCoerce ((Handling e es esSend => a) -> InstHandling e es esSend a
forall k (e :: (Type -> Type) -> Type -> Type) (es :: k)
       (esSend :: [(Type -> Type) -> Type -> Type]) a.
(Handling e es esSend => a) -> InstHandling e es esSend a
InstHandling Handling e es esSend => a
x :: InstHandling e es esSend a)
{-# INLINE instHandling #-}

-- | The type of an /effect handler/, which is a function that transforms an effect @e@ from an arbitrary effect stack
-- into computations in the effect stack @es@.
type Handler e es = ∀ esSend. Handling e es esSend => e (Eff esSend) ~> Eff es

-- | The type of a simple transformation function from effect @e@ to @e'@.
type Translator e e' = ∀ esSend. e (Eff esSend) ~> e' (Eff esSend)

-- * Interpreting effects

-- | Transform a 'Handler' into an 'InternalHandler' given a pointer that is going to point to the 'InternalHandler'
-- and the current 'Env'.
mkInternalHandler :: MemPtr InternalHandler e -> Env es -> Handler e es -> InternalHandler e
mkInternalHandler :: MemPtr InternalHandler e
-> Env es -> Handler e es -> InternalHandler e
mkInternalHandler MemPtr InternalHandler e
ptr Env es
es Handler e es
handle = (forall (es :: [(Type -> Type) -> Type -> Type]).
 e (Eff es) ~> Eff es)
-> InternalHandler e
forall (e :: (Type -> Type) -> Type -> Type).
(forall (es :: [(Type -> Type) -> Type -> Type]).
 e (Eff es) ~> Eff es)
-> InternalHandler e
InternalHandler \e (Eff es) a
eff -> (Env es -> IO a) -> Eff es a
forall (es :: [(Type -> Type) -> Type -> Type]) a.
(Env es -> IO a) -> Eff es a
Eff \Env es
esSend ->
  Eff es a -> Env es -> IO a
forall (es :: [(Type -> Type) -> Type -> Type]) a.
Eff es a -> Env es -> IO a
unEff ((Handling e es es => e (Eff es) a -> Eff es a)
-> SendSite e es -> e (Eff es) a -> Eff es a
forall k (e :: (Type -> Type) -> Type -> Type) (es :: k)
       (esSend :: [(Type -> Type) -> Type -> Type]) a.
(Handling e es esSend => a) -> SendSite e esSend -> a
instHandling Handling e es es => e (Eff es) a -> Eff es a
Handler e es
handle (MemPtr InternalHandler e -> Env es -> SendSite e es
forall (e :: (Type -> Type) -> Type -> Type)
       (esSend :: [(Type -> Type) -> Type -> Type]).
MemPtr InternalHandler e -> Env esSend -> SendSite e esSend
SendSite MemPtr InternalHandler e
ptr Env es
esSend) e (Eff es) a
eff) (Env es -> Env es -> Env es
forall k (es :: [k]) (es' :: [k]) (f :: k -> Type).
Mem f es' -> Mem f es -> Mem f es
Mem.update Env es
esSend Env es
es)

-- | Interpret an effect @e@ in terms of effects in the effect stack @es@ with an effect handler.
interpret :: ∀ e es. Handler e es -> Eff (e ': es) ~> Eff es
interpret :: Handler e es -> Eff (e : es) ~> Eff es
interpret = forall (es' :: [(Type -> Type) -> Type -> Type])
       (e :: (Type -> Type) -> Type -> Type)
       (es :: [(Type -> Type) -> Type -> Type]).
KnownList es' =>
Handler e (es' ++ es) -> Eff (e : es) ~> Eff (es' ++ es)
forall (e :: (Type -> Type) -> Type -> Type)
       (es :: [(Type -> Type) -> Type -> Type]).
KnownList '[] =>
Handler e ('[] ++ es) -> Eff (e : es) ~> Eff ('[] ++ es)
reinterpretN @'[]

-- | Like 'interpret', but adds a new effect @e'@ that can be used in the handler.
reinterpret :: ∀ e' e es. Handler e (e' ': es) -> Eff (e ': es) ~> Eff (e' ': es)
reinterpret :: Handler e (e' : es) -> Eff (e : es) ~> Eff (e' : es)
reinterpret = forall (es' :: [(Type -> Type) -> Type -> Type])
       (e :: (Type -> Type) -> Type -> Type)
       (es :: [(Type -> Type) -> Type -> Type]).
KnownList es' =>
Handler e (es' ++ es) -> Eff (e : es) ~> Eff (es' ++ es)
forall (e :: (Type -> Type) -> Type -> Type)
       (es :: [(Type -> Type) -> Type -> Type]).
KnownList '[e'] =>
Handler e ('[e'] ++ es) -> Eff (e : es) ~> Eff ('[e'] ++ es)
reinterpretN @'[e']

-- | Like 'reinterpret', but adds two new effects.
reinterpret2 :: ∀ e' e'' e es. Handler e (e' ': e'' ': es) -> Eff (e ': es) ~> Eff (e' ': e'' ': es)
reinterpret2 :: Handler e (e' : e'' : es) -> Eff (e : es) ~> Eff (e' : e'' : es)
reinterpret2 = forall (es' :: [(Type -> Type) -> Type -> Type])
       (e :: (Type -> Type) -> Type -> Type)
       (es :: [(Type -> Type) -> Type -> Type]).
KnownList es' =>
Handler e (es' ++ es) -> Eff (e : es) ~> Eff (es' ++ es)
forall (e :: (Type -> Type) -> Type -> Type)
       (es :: [(Type -> Type) -> Type -> Type]).
KnownList '[e', e''] =>
Handler e ('[e', e''] ++ es)
-> Eff (e : es) ~> Eff ('[e', e''] ++ es)
reinterpretN @'[e', e'']

-- | Like 'reinterpret', but adds three new effects.
reinterpret3 :: ∀ e' e'' e''' e es. Handler e (e' ': e'' ': e''' ': es) -> Eff (e ': es) ~> Eff (e' ': e'' ': e''' ': es)
reinterpret3 :: Handler e (e' : e'' : e''' : es)
-> Eff (e : es) ~> Eff (e' : e'' : e''' : es)
reinterpret3 = forall (es' :: [(Type -> Type) -> Type -> Type])
       (e :: (Type -> Type) -> Type -> Type)
       (es :: [(Type -> Type) -> Type -> Type]).
KnownList es' =>
Handler e (es' ++ es) -> Eff (e : es) ~> Eff (es' ++ es)
forall (e :: (Type -> Type) -> Type -> Type)
       (es :: [(Type -> Type) -> Type -> Type]).
KnownList '[e', e'', e'''] =>
Handler e ('[e', e'', e'''] ++ es)
-> Eff (e : es) ~> Eff ('[e', e'', e'''] ++ es)
reinterpretN @'[e', e'', e''']

-- | Like 'reinterpret', but adds arbitrarily many new effects. This function requires @TypeApplications@.
reinterpretN :: ∀ es' e es. KnownList es' => Handler e (es' ++ es) -> Eff (e ': es) ~> Eff (es' ++ es)
reinterpretN :: Handler e (es' ++ es) -> Eff (e : es) ~> Eff (es' ++ es)
reinterpretN Handler e (es' ++ es)
handle Eff (e : es) a
m = (Env (es' ++ es) -> IO a) -> Eff (es' ++ es) a
forall (es :: [(Type -> Type) -> Type -> Type]) a.
(Env es -> IO a) -> Eff es a
Eff \Env (es' ++ es)
es ->
  let (# MemPtr InternalHandler e
ptr, Env (es' ++ es)
es' #) = Env (es' ++ es) -> (# MemPtr InternalHandler e, Env (es' ++ es) #)
forall k (e :: k) (es :: [k]) (f :: k -> Type).
Mem f es -> (# MemPtr f e, Mem f es #)
Mem.alloca Env (es' ++ es)
es
  in Eff (e : es) a -> Env (e : es) -> IO a
forall (es :: [(Type -> Type) -> Type -> Type]) a.
Eff es a -> Env es -> IO a
unEff Eff (e : es) a
m (Env (e : es) -> IO a) -> Env (e : es) -> IO a
forall a b. (a -> b) -> a -> b
$ MemPtr InternalHandler e
-> InternalHandler e -> Mem InternalHandler es -> Env (e : es)
forall a (e :: a) (es :: [a]) (f :: a -> Type).
MemPtr f e -> f e -> Mem f es -> Mem f (e : es)
Mem.append MemPtr InternalHandler e
ptr (MemPtr InternalHandler e
-> Env (es' ++ es) -> Handler e (es' ++ es) -> InternalHandler e
forall (e :: (Type -> Type) -> Type -> Type)
       (es :: [(Type -> Type) -> Type -> Type]).
MemPtr InternalHandler e
-> Env es -> Handler e es -> InternalHandler e
mkInternalHandler MemPtr InternalHandler e
ptr Env (es' ++ es)
es' Handler e (es' ++ es)
handle) (Mem InternalHandler es -> Env (e : es))
-> Mem InternalHandler es -> Env (e : es)
forall a b. (a -> b) -> a -> b
$ (Rec (MemPtr InternalHandler) (es' ++ es)
 -> Rec (MemPtr InternalHandler) es)
-> Env (es' ++ es) -> Mem InternalHandler es
forall k (es' :: [k]) (es :: [k]) (f :: k -> Type).
(Rec (MemPtr f) es -> Rec (MemPtr f) es') -> Mem f es -> Mem f es'
Mem.adjust (forall (es' :: [(Type -> Type) -> Type -> Type])
       (f :: ((Type -> Type) -> Type -> Type) -> Type).
KnownList es' =>
Rec f (es' ++ es') -> Rec f es'
forall k (es :: [k]) (es' :: [k]) (f :: k -> Type).
KnownList es =>
Rec f (es ++ es') -> Rec f es'
Env.drop @es') Env (es' ++ es)
es'

-- | Respond to an effect while being able to leave it unhandled (i.e. you can resend the effects in the handler).
interpose :: ∀ e es. e :> es => Handler e es -> Eff es ~> Eff es
interpose :: Handler e es -> Eff es ~> Eff es
interpose = forall (es' :: [(Type -> Type) -> Type -> Type])
       (e :: (Type -> Type) -> Type -> Type)
       (es :: [(Type -> Type) -> Type -> Type]).
(KnownList es', e :> es) =>
Handler e (es' ++ es) -> Eff es ~> Eff (es' ++ es)
forall (e :: (Type -> Type) -> Type -> Type)
       (es :: [(Type -> Type) -> Type -> Type]).
(KnownList '[], e :> es) =>
Handler e ('[] ++ es) -> Eff es ~> Eff ('[] ++ es)
imposeN @'[]

-- | Like 'interpose', but allows to introduce one new effect to use in the handler.
impose :: ∀ e' e es. e :> es => Handler e (e' ': es) -> Eff es ~> Eff (e' ': es)
impose :: Handler e (e' : es) -> Eff es ~> Eff (e' : es)
impose = forall (es' :: [(Type -> Type) -> Type -> Type])
       (e :: (Type -> Type) -> Type -> Type)
       (es :: [(Type -> Type) -> Type -> Type]).
(KnownList es', e :> es) =>
Handler e (es' ++ es) -> Eff es ~> Eff (es' ++ es)
forall (e :: (Type -> Type) -> Type -> Type)
       (es :: [(Type -> Type) -> Type -> Type]).
(KnownList '[e'], e :> es) =>
Handler e ('[e'] ++ es) -> Eff es ~> Eff ('[e'] ++ es)
imposeN @'[e']

-- | Like 'impose', but allows introducing arbitrarily many effects. This requires @TypeApplications@.
imposeN :: ∀ es' e es. (KnownList es', e :> es) => Handler e (es' ++ es) -> Eff es ~> Eff (es' ++ es)
imposeN :: Handler e (es' ++ es) -> Eff es ~> Eff (es' ++ es)
imposeN Handler e (es' ++ es)
handle Eff es a
m = (Env (es' ++ es) -> IO a) -> Eff (es' ++ es) a
forall (es :: [(Type -> Type) -> Type -> Type]) a.
(Env es -> IO a) -> Eff es a
Eff \Env (es' ++ es)
es ->
  let (# MemPtr InternalHandler e
ptr, Env (es' ++ es)
es' #) = Env (es' ++ es) -> (# MemPtr InternalHandler e, Env (es' ++ es) #)
forall k (e :: k) (es :: [k]) (f :: k -> Type).
Mem f es -> (# MemPtr f e, Mem f es #)
Mem.alloca Env (es' ++ es)
es
  in Eff es a -> Env es -> IO a
forall (es :: [(Type -> Type) -> Type -> Type]) a.
Eff es a -> Env es -> IO a
unEff Eff es a
m (Env es -> IO a) -> Env es -> IO a
forall a b. (a -> b) -> a -> b
$ MemPtr InternalHandler e -> InternalHandler e -> Env es -> Env es
forall k (e :: k) (es :: [k]) (f :: k -> Type).
Elem e es =>
MemPtr f e -> f e -> Mem f es -> Mem f es
Mem.replace MemPtr InternalHandler e
ptr (MemPtr InternalHandler e
-> Env (es' ++ es) -> Handler e (es' ++ es) -> InternalHandler e
forall (e :: (Type -> Type) -> Type -> Type)
       (es :: [(Type -> Type) -> Type -> Type]).
MemPtr InternalHandler e
-> Env es -> Handler e es -> InternalHandler e
mkInternalHandler MemPtr InternalHandler e
ptr Env (es' ++ es)
es' Handler e (es' ++ es)
handle) (Env es -> Env es) -> Env es -> Env es
forall a b. (a -> b) -> a -> b
$ (Rec (MemPtr InternalHandler) (es' ++ es)
 -> Rec (MemPtr InternalHandler) es)
-> Env (es' ++ es) -> Env es
forall k (es' :: [k]) (es :: [k]) (f :: k -> Type).
(Rec (MemPtr f) es -> Rec (MemPtr f) es') -> Mem f es -> Mem f es'
Mem.adjust (forall (es' :: [(Type -> Type) -> Type -> Type])
       (f :: ((Type -> Type) -> Type -> Type) -> Type).
KnownList es' =>
Rec f (es' ++ es') -> Rec f es'
forall k (es :: [k]) (es' :: [k]) (f :: k -> Type).
KnownList es =>
Rec f (es ++ es') -> Rec f es'
Env.drop @es') Env (es' ++ es)
es'

-- * Translating effects

-- | Interpret an effect in terms of another effect in the stack via a simple 'Translator'.
transform :: ∀ e' e es. e' :> es => Translator e e' -> Eff (e ': es) ~> Eff es
transform :: Translator e e' -> Eff (e : es) ~> Eff es
transform = forall (es' :: [(Type -> Type) -> Type -> Type])
       (e' :: (Type -> Type) -> Type -> Type)
       (e :: (Type -> Type) -> Type -> Type)
       (es :: [(Type -> Type) -> Type -> Type]).
(KnownList es', e' :> (es' ++ es)) =>
Translator e e' -> Eff (e : es) ~> Eff (es' ++ es)
forall (e' :: (Type -> Type) -> Type -> Type)
       (e :: (Type -> Type) -> Type -> Type)
       (es :: [(Type -> Type) -> Type -> Type]).
(KnownList '[], e' :> ('[] ++ es)) =>
Translator e e' -> Eff (e : es) ~> Eff ('[] ++ es)
translateN @'[]

-- | Like 'transform', but instead of using an effect in stack, add a new one to the top of it.
translate :: ∀ e' e es. Translator e e' -> Eff (e ': es) ~> Eff (e' ': es)
translate :: Translator e e' -> Eff (e : es) ~> Eff (e' : es)
translate = forall (es' :: [(Type -> Type) -> Type -> Type])
       (e' :: (Type -> Type) -> Type -> Type)
       (e :: (Type -> Type) -> Type -> Type)
       (es :: [(Type -> Type) -> Type -> Type]).
(KnownList es', e' :> (es' ++ es)) =>
Translator e e' -> Eff (e : es) ~> Eff (es' ++ es)
forall (e' :: (Type -> Type) -> Type -> Type)
       (e :: (Type -> Type) -> Type -> Type)
       (es :: [(Type -> Type) -> Type -> Type]).
(KnownList '[e'], e' :> ('[e'] ++ es)) =>
Translator e e' -> Eff (e : es) ~> Eff ('[e'] ++ es)
translateN @'[e']

-- | Common implementation of 'transform' and 'translate'. It is overly general on its own so it is not exported in
-- "Cleff".
translateN :: ∀ es' e' e es. (KnownList es', e' :> es' ++ es) => Translator e e' -> Eff (e ': es) ~> Eff (es' ++ es)
translateN :: Translator e e' -> Eff (e : es) ~> Eff (es' ++ es)
translateN Translator e e'
trans Eff (e : es) a
m = (Env (es' ++ es) -> IO a) -> Eff (es' ++ es) a
forall (es :: [(Type -> Type) -> Type -> Type]) a.
(Env es -> IO a) -> Eff es a
Eff \Env (es' ++ es)
es ->
  let (# MemPtr InternalHandler e
ptr, Env (es' ++ es)
es' #) = Env (es' ++ es) -> (# MemPtr InternalHandler e, Env (es' ++ es) #)
forall k (e :: k) (es :: [k]) (f :: k -> Type).
Mem f es -> (# MemPtr f e, Mem f es #)
Mem.alloca Env (es' ++ es)
es
  in let handler :: InternalHandler e
handler = (forall (es :: [(Type -> Type) -> Type -> Type]).
 e (Eff es) ~> Eff es)
-> InternalHandler e
forall (e :: (Type -> Type) -> Type -> Type).
(forall (es :: [(Type -> Type) -> Type -> Type]).
 e (Eff es) ~> Eff es)
-> InternalHandler e
InternalHandler (InternalHandler e'
-> forall (es :: [(Type -> Type) -> Type -> Type]) a.
   e' (Eff es) a -> Eff es a
forall (e :: (Type -> Type) -> Type -> Type).
InternalHandler e
-> forall (es :: [(Type -> Type) -> Type -> Type]).
   e (Eff es) ~> Eff es
runHandler (Env (es' ++ es) -> InternalHandler e'
forall k (e :: k) (es :: [k]) (f :: k -> Type).
Elem e es =>
Mem f es -> f e
Mem.read Env (es' ++ es)
es') (e' (Eff es) a -> Eff es a)
-> (e (Eff es) a -> e' (Eff es) a) -> e (Eff es) a -> Eff es a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e (Eff es) a -> e' (Eff es) a
Translator e e'
trans)
  in Eff (e : es) a -> Env (e : es) -> IO a
forall (es :: [(Type -> Type) -> Type -> Type]) a.
Eff es a -> Env es -> IO a
unEff Eff (e : es) a
m (Env (e : es) -> IO a) -> Env (e : es) -> IO a
forall a b. (a -> b) -> a -> b
$ MemPtr InternalHandler e
-> InternalHandler e -> Mem InternalHandler es -> Env (e : es)
forall a (e :: a) (es :: [a]) (f :: a -> Type).
MemPtr f e -> f e -> Mem f es -> Mem f (e : es)
Mem.append MemPtr InternalHandler e
ptr InternalHandler e
handler (Mem InternalHandler es -> Env (e : es))
-> Mem InternalHandler es -> Env (e : es)
forall a b. (a -> b) -> a -> b
$ (Rec (MemPtr InternalHandler) (es' ++ es)
 -> Rec (MemPtr InternalHandler) es)
-> Env (es' ++ es) -> Mem InternalHandler es
forall k (es' :: [k]) (es :: [k]) (f :: k -> Type).
(Rec (MemPtr f) es -> Rec (MemPtr f) es') -> Mem f es -> Mem f es'
Mem.adjust (forall (es' :: [(Type -> Type) -> Type -> Type])
       (f :: ((Type -> Type) -> Type -> Type) -> Type).
KnownList es' =>
Rec f (es' ++ es') -> Rec f es'
forall k (es :: [k]) (es' :: [k]) (f :: k -> Type).
KnownList es =>
Rec f (es ++ es') -> Rec f es'
Env.drop @es') Env (es' ++ es)
es'

-- * Combinators for interpreting higher effects

-- | Run a computation in the current effect stack. This is useful for interpreting higher-order effects, like a
-- bracketing effect:
--
-- @
-- data Resource m a where
--   Bracket :: m a -> (a -> m ()) -> (a -> m b) -> Resource m b
-- @
--
-- @
-- Bracket alloc dealloc use ->
--   'UnliftIO.bracket'
--     ('toEff' alloc)
--     ('toEff' . dealloc)
--     ('toEff' . use)
-- @
toEff :: Handling e es esSend => Eff esSend ~> Eff es
toEff :: Eff esSend ~> Eff es
toEff Eff esSend a
m = (Env es -> IO a) -> Eff es a
forall (es :: [(Type -> Type) -> Type -> Type]) a.
(Env es -> IO a) -> Eff es a
Eff \Env es
es -> Eff esSend a -> Env esSend -> IO a
forall (es :: [(Type -> Type) -> Type -> Type]) a.
Eff es a -> Env es -> IO a
unEff Eff esSend a
m (Env es -> Env esSend -> Env esSend
forall k (es :: [k]) (es' :: [k]) (f :: k -> Type).
Mem f es' -> Mem f es -> Mem f es
Mem.update Env es
es Env esSend
forall k (e :: (Type -> Type) -> Type -> Type) (es :: k)
       (esSend :: [(Type -> Type) -> Type -> Type]).
Handling e es esSend =>
Env esSend
sendEnv)

-- | Run a computation in the current effect stack, but handles the current effect inside the computation differently
-- by providing a new 'Handler'. This is useful for interpreting effects with local contexts, like 'Cleff.Reader.Local':
--
-- @
-- runReader :: r -> 'Eff' ('Cleff.Reader.Reader' r ': es) '~>' 'Eff' es
-- runReader x = 'interpret' (handle x)
--   where
--     handle :: r -> 'Handler' ('Reader' r) es
--     handle r = \\case
--       'Cleff.Reader.Ask'       -> 'pure' r
--       'Cleff.Reader.Local' f m -> 'toEffWith' (handle $ f r) m
-- @
toEffWith :: Handling e es esSend => Handler e es -> Eff esSend ~> Eff es
toEffWith :: Handler e es -> Eff esSend ~> Eff es
toEffWith Handler e es
handle Eff esSend a
m = (Env es -> IO a) -> Eff es a
forall (es :: [(Type -> Type) -> Type -> Type]) a.
(Env es -> IO a) -> Eff es a
Eff \Env es
es -> Eff esSend a -> Env esSend -> IO a
forall (es :: [(Type -> Type) -> Type -> Type]) a.
Eff es a -> Env es -> IO a
unEff Eff esSend a
m (Env esSend -> IO a) -> Env esSend -> IO a
forall a b. (a -> b) -> a -> b
$
  MemPtr InternalHandler e
-> InternalHandler e -> Env esSend -> Env esSend
forall k (e :: k) (es :: [k]) (f :: k -> Type).
MemPtr f e -> f e -> Mem f es -> Mem f es
Mem.write MemPtr InternalHandler e
forall k (e :: (Type -> Type) -> Type -> Type) (es :: k)
       (esSend :: [(Type -> Type) -> Type -> Type]).
Handling e es esSend =>
MemPtr InternalHandler e
hdlPtr (MemPtr InternalHandler e
-> Env es -> Handler e es -> InternalHandler e
forall (e :: (Type -> Type) -> Type -> Type)
       (es :: [(Type -> Type) -> Type -> Type]).
MemPtr InternalHandler e
-> Env es -> Handler e es -> InternalHandler e
mkInternalHandler MemPtr InternalHandler e
forall k (e :: (Type -> Type) -> Type -> Type) (es :: k)
       (esSend :: [(Type -> Type) -> Type -> Type]).
Handling e es esSend =>
MemPtr InternalHandler e
hdlPtr Env es
es Handler e es
handle) (Env esSend -> Env esSend) -> Env esSend -> Env esSend
forall a b. (a -> b) -> a -> b
$ Env es -> Env esSend -> Env esSend
forall k (es :: [k]) (es' :: [k]) (f :: k -> Type).
Mem f es' -> Mem f es -> Mem f es
Mem.update Env es
es Env esSend
forall k (e :: (Type -> Type) -> Type -> Type) (es :: k)
       (esSend :: [(Type -> Type) -> Type -> Type]).
Handling e es esSend =>
Env esSend
sendEnv

-- | Temporarily gain the ability to lift some @'Eff' es@ actions into @'Eff' esSend@. This is useful for dealing with
-- effect operations with the monad type in the negative position, which means it's unlikely that you need to use this
-- function in implementing your effects.
withFromEff :: Handling e es esSend => ((Eff es ~> Eff esSend) -> Eff esSend a) -> Eff es a
withFromEff :: ((Eff es ~> Eff esSend) -> Eff esSend a) -> Eff es a
withFromEff (Eff es ~> Eff esSend) -> Eff esSend a
f = (Env es -> IO a) -> Eff es a
forall (es :: [(Type -> Type) -> Type -> Type]) a.
(Env es -> IO a) -> Eff es a
Eff \Env es
es -> Eff esSend a -> Env esSend -> IO a
forall (es :: [(Type -> Type) -> Type -> Type]) a.
Eff es a -> Env es -> IO a
unEff ((Eff es ~> Eff esSend) -> Eff esSend a
f \Eff es a
m -> (Env esSend -> IO a) -> Eff esSend a
forall (es :: [(Type -> Type) -> Type -> Type]) a.
(Env es -> IO a) -> Eff es a
Eff \Env esSend
esSend -> Eff es a -> Env es -> IO a
forall (es :: [(Type -> Type) -> Type -> Type]) a.
Eff es a -> Env es -> IO a
unEff Eff es a
m (Env esSend -> Env es -> Env es
forall k (es :: [k]) (es' :: [k]) (f :: k -> Type).
Mem f es' -> Mem f es -> Mem f es
Mem.update Env esSend
esSend Env es
es)) (Env es -> Env esSend -> Env esSend
forall k (es :: [k]) (es' :: [k]) (f :: k -> Type).
Mem f es' -> Mem f es -> Mem f es
Mem.update Env es
es Env esSend
forall k (e :: (Type -> Type) -> Type -> Type) (es :: k)
       (esSend :: [(Type -> Type) -> Type -> Type]).
Handling e es esSend =>
Env esSend
sendEnv)