{-# options_haddock prune #-}

-- |Description: Scoped Interpreters, Internal
module Polysemy.Conc.Interpreter.Scoped where

import GHC.Err (errorWithoutStackTrace)
import Polysemy.Internal (Sem (Sem), hoistSem, liftSem, runSem)
import Polysemy.Internal.Sing (KnownList (singList))
import Polysemy.Internal.Tactics (liftT)
import Polysemy.Internal.Union (
  Union (Union),
  Weaving (Weaving),
  decomp,
  extendMembershipLeft,
  hoist,
  injWeaving,
  injectMembership,
  weave,
  )
import Polysemy.Membership (ElemOf)
import Polysemy.Resume (Stop, interpretResumableH, runStop, type (!!))
import Polysemy.Resume.Effect.Resumable (Resumable (Resumable))

import Polysemy.Conc.Effect.Scoped (Scoped (InScope, Run))

interpretWeaving ::
  ∀ e r .
  (∀ x . Weaving e (Sem (e : r)) x -> Sem r x) ->
  InterpreterFor e r
interpretWeaving :: forall (e :: Effect) (r :: [Effect]).
(forall x. Weaving e (Sem (e : r)) x -> Sem r x)
-> InterpreterFor e r
interpretWeaving forall x. Weaving e (Sem (e : r)) x -> Sem r x
h (Sem forall (m :: * -> *).
Monad m =>
(forall x. Union (e : r) (Sem (e : r)) x -> m x) -> m a
m) =
  (forall (m :: * -> *).
 Monad m =>
 (forall x. Union r (Sem r) x -> m x) -> m a)
-> Sem r a
forall (r :: [Effect]) a.
(forall (m :: * -> *).
 Monad m =>
 (forall x. Union r (Sem r) x -> m x) -> m a)
-> Sem r a
Sem \ forall x. Union r (Sem r) x -> m x
k -> (forall x. Union (e : r) (Sem (e : r)) x -> m x) -> m a
forall (m :: * -> *).
Monad m =>
(forall x. Union (e : r) (Sem (e : r)) x -> m x) -> m a
m ((forall x. Union (e : r) (Sem (e : r)) x -> m x) -> m a)
-> (forall x. Union (e : r) (Sem (e : r)) x -> m x) -> m a
forall a b. (a -> b) -> a -> b
$ Union (e : r) (Sem (e : r)) x
-> Either (Union r (Sem (e : r)) x) (Weaving e (Sem (e : r)) x)
forall (e :: Effect) (r :: [Effect]) (m :: * -> *) a.
Union (e : r) m a -> Either (Union r m a) (Weaving e m a)
decomp (Union (e : r) (Sem (e : r)) x
 -> Either (Union r (Sem (e : r)) x) (Weaving e (Sem (e : r)) x))
-> (Either (Union r (Sem (e : r)) x) (Weaving e (Sem (e : r)) x)
    -> m x)
-> Union (e : r) (Sem (e : r)) x
-> m x
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> \case
    Right Weaving e (Sem (e : r)) x
wav -> Sem r x
-> forall (m :: * -> *).
   Monad m =>
   (forall x. Union r (Sem r) x -> m x) -> m x
forall (r :: [Effect]) a.
Sem r a
-> forall (m :: * -> *).
   Monad m =>
   (forall x. Union r (Sem r) x -> m x) -> m a
runSem (Weaving e (Sem (e : r)) x -> Sem r x
forall x. Weaving e (Sem (e : r)) x -> Sem r x
h Weaving e (Sem (e : r)) x
wav) forall x. Union r (Sem r) x -> m x
k
    Left Union r (Sem (e : r)) x
g -> Union r (Sem r) x -> m x
forall x. Union r (Sem r) x -> m x
k ((forall x. Sem (e : r) x -> Sem r x)
-> Union r (Sem (e : r)) x -> Union r (Sem r) x
forall (m :: * -> *) (n :: * -> *) (r :: [Effect]) a.
(forall x. m x -> n x) -> Union r m a -> Union r n a
hoist ((forall x. Weaving e (Sem (e : r)) x -> Sem r x)
-> forall x. Sem (e : r) x -> Sem r x
forall (e :: Effect) (r :: [Effect]).
(forall x. Weaving e (Sem (e : r)) x -> Sem r x)
-> InterpreterFor e r
interpretWeaving forall x. Weaving e (Sem (e : r)) x -> Sem r x
h) Union r (Sem (e : r)) x
g)

restack :: (∀ e . ElemOf e r -> ElemOf e r')
        -> Sem r a
        -> Sem r' a
restack :: forall (r :: [Effect]) (r' :: [Effect]) a.
(forall (e :: Effect). ElemOf e r -> ElemOf e r')
-> Sem r a -> Sem r' a
restack forall (e :: Effect). ElemOf e r -> ElemOf e r'
n =
  (forall x. Union r (Sem r) x -> Union r' (Sem r') x)
-> Sem r a -> Sem r' a
forall (r :: [Effect]) (r' :: [Effect]) a.
(forall x. Union r (Sem r) x -> Union r' (Sem r') x)
-> Sem r a -> Sem r' a
hoistSem ((forall x. Union r (Sem r) x -> Union r' (Sem r') x)
 -> Sem r a -> Sem r' a)
-> (forall x. Union r (Sem r) x -> Union r' (Sem r') x)
-> Sem r a
-> Sem r' a
forall a b. (a -> b) -> a -> b
$ \ (Union ElemOf e r
pr Weaving e (Sem r) x
wav) -> (forall x. Sem r x -> Sem r' x)
-> Union r' (Sem r) x -> Union r' (Sem r') x
forall (m :: * -> *) (n :: * -> *) (r :: [Effect]) a.
(forall x. m x -> n x) -> Union r m a -> Union r n a
hoist ((forall (e :: Effect). ElemOf e r -> ElemOf e r')
-> Sem r x -> Sem r' x
forall (r :: [Effect]) (r' :: [Effect]) a.
(forall (e :: Effect). ElemOf e r -> ElemOf e r')
-> Sem r a -> Sem r' a
restack forall (e :: Effect). ElemOf e r -> ElemOf e r'
n) (ElemOf e r' -> Weaving e (Sem r) x -> Union r' (Sem r) x
forall (e :: Effect) (r :: [Effect]) (mWoven :: * -> *) a.
ElemOf e r -> Weaving e mWoven a -> Union r mWoven a
Union (ElemOf e r -> ElemOf e r'
forall (e :: Effect). ElemOf e r -> ElemOf e r'
n ElemOf e r
pr) Weaving e (Sem r) x
wav)
{-# inline restack #-}

exResumable ::
  Functor f =>
  f () ->
  (f (Either err a) -> x) ->
  (f' a' -> a) ->
  Sem r (Either err (f (f' a'))) ->
  Sem r x
exResumable :: forall {k} (f :: * -> *) err a x (f' :: k -> *) (a' :: k)
       (r :: [Effect]).
Functor f =>
f ()
-> (f (Either err a) -> x)
-> (f' a' -> a)
-> Sem r (Either err (f (f' a')))
-> Sem r x
exResumable f ()
s f (Either err a) -> x
ex f' a' -> a
ex' =
  (Either err (f (f' a')) -> x)
-> Sem r (Either err (f (f' a'))) -> Sem r x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Either err (f (f' a')) -> x)
 -> Sem r (Either err (f (f' a'))) -> Sem r x)
-> (Either err (f (f' a')) -> x)
-> Sem r (Either err (f (f' a')))
-> Sem r x
forall a b. (a -> b) -> a -> b
$ f (Either err a) -> x
ex (f (Either err a) -> x)
-> (Either err (f (f' a')) -> f (Either err a))
-> Either err (f (f' a'))
-> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
    Right f (f' a')
a -> a -> Either err a
forall a b. b -> Either a b
Right (a -> Either err a) -> (f' a' -> a) -> f' a' -> Either err a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f' a' -> a
ex' (f' a' -> Either err a) -> f (f' a') -> f (Either err a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (f' a')
a
    Left err
err -> err -> Either err a
forall a b. a -> Either a b
Left err
err Either err a -> f () -> f (Either err a)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s
{-# inline exResumable #-}

-- | Construct an interpreter for a higher-order effect wrapped in a 'Scoped',
-- given a resource allocation function and a parameterized handler for the
-- plain effect.
--
-- This combinator is analogous to 'interpretH' in that it allows the handler to
-- use the 'Tactical' environment and transforms the effect into other effects
-- on the stack.
interpretScopedH ::
  ∀ resource param effect r .
  -- | A callback function that allows the user to acquire a resource for each
  -- computation wrapped by 'Polysemy.Conc.scoped' using other effects, with an additional
  -- argument that contains the call site parameter passed to 'Polysemy.Conc.scoped'.
  (∀ x . param -> (resource -> Sem r x) -> Sem r x) ->
  -- | A handler like the one expected by 'interpretH' with an additional
  -- parameter that contains the @resource@ allocated by the first argument.
  (∀ r0 x . resource -> effect (Sem r0) x -> Tactical effect (Sem r0) r x) ->
  InterpreterFor (Scoped param effect) r
interpretScopedH :: forall resource param (effect :: Effect) (r :: [Effect]).
(forall x. param -> (resource -> Sem r x) -> Sem r x)
-> (forall (r0 :: [Effect]) x.
    resource -> effect (Sem r0) x -> Tactical effect (Sem r0) r x)
-> InterpreterFor (Scoped param effect) r
interpretScopedH forall x. param -> (resource -> Sem r x) -> Sem r x
withResource forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Tactical effect (Sem r0) r x
scopedHandler =
  (forall x.
 Weaving (Scoped param effect) (Sem (Scoped param effect : r)) x
 -> Sem r x)
-> Sem (Scoped param effect : r) a -> Sem r a
forall (e :: Effect) (r :: [Effect]).
(forall x. Weaving e (Sem (e : r)) x -> Sem r x)
-> InterpreterFor e r
interpretWeaving ((forall x.
  Weaving (Scoped param effect) (Sem (Scoped param effect : r)) x
  -> Sem r x)
 -> Sem (Scoped param effect : r) a -> Sem r a)
-> (forall x.
    Weaving (Scoped param effect) (Sem (Scoped param effect : r)) x
    -> Sem r x)
-> Sem (Scoped param effect : r) a
-> Sem r a
forall a b. (a -> b) -> a -> b
$ \(Weaving Scoped param effect (Sem rInitial) a
effect f ()
s forall x. f (Sem rInitial x) -> Sem (Scoped param effect : r) (f x)
wv f a -> x
ex forall x. f x -> Maybe x
_) -> case Scoped param effect (Sem rInitial) a
effect of
    Run effect (Sem rInitial) a
_ -> [Char] -> Sem r x
forall a. [Char] -> a
errorWithoutStackTrace [Char]
"top level run"
    InScope param
param Sem rInitial a
main -> param -> (resource -> Sem r x) -> Sem r x
forall x. param -> (resource -> Sem r x) -> Sem r x
withResource param
param \ resource
resource ->
          f a -> x
ex
      (f a -> x) -> Sem r (f a) -> Sem r x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (rInitial :: [Effect]) x.
 effect (Sem rInitial) x -> Tactical effect (Sem rInitial) r x)
-> Sem (effect : r) (f a) -> Sem r (f a)
forall (e :: Effect) (r :: [Effect]) a.
(forall (rInitial :: [Effect]) x.
 e (Sem rInitial) x -> Tactical e (Sem rInitial) r x)
-> Sem (e : r) a -> Sem r a
interpretH (resource
-> effect (Sem rInitial) x -> Tactical effect (Sem rInitial) r x
forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Tactical effect (Sem r0) r x
scopedHandler resource
resource) (Sem (Scoped param effect : effect : r) (f a)
-> Sem (effect : r) (f a)
InterpreterFor (Scoped param effect) (effect : r)
go (Sem (Scoped param effect : effect : r) (f a)
 -> Sem (effect : r) (f a))
-> Sem (Scoped param effect : effect : r) (f a)
-> Sem (effect : r) (f a)
forall a b. (a -> b) -> a -> b
$ Sem (Scoped param effect : r) (f a)
-> Sem (Scoped param effect : effect : r) (f a)
forall (e2 :: Effect) (e1 :: Effect) (r :: [Effect]) a.
Sem (e1 : r) a -> Sem (e1 : e2 : r) a
raiseUnder (Sem (Scoped param effect : r) (f a)
 -> Sem (Scoped param effect : effect : r) (f a))
-> Sem (Scoped param effect : r) (f a)
-> Sem (Scoped param effect : effect : r) (f a)
forall a b. (a -> b) -> a -> b
$ f (Sem rInitial a) -> Sem (Scoped param effect : r) (f a)
forall x. f (Sem rInitial x) -> Sem (Scoped param effect : r) (f x)
wv (Sem rInitial a
main Sem rInitial a -> f () -> f (Sem rInitial a)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s))
  where
    -- TODO investigate whether loopbreaker optimization is effective here
    go :: InterpreterFor (Scoped param effect) (effect : r)
    go :: InterpreterFor (Scoped param effect) (effect : r)
go =
      (forall x.
 Weaving
   (Scoped param effect) (Sem (Scoped param effect : effect : r)) x
 -> Sem (effect : r) x)
-> InterpreterFor (Scoped param effect) (effect : r)
forall (e :: Effect) (r :: [Effect]).
(forall x. Weaving e (Sem (e : r)) x -> Sem r x)
-> InterpreterFor e r
interpretWeaving \ (Weaving Scoped param effect (Sem rInitial) a
effect f ()
s forall x.
f (Sem rInitial x) -> Sem (Scoped param effect : effect : r) (f x)
wv f a -> x
ex forall x. f x -> Maybe x
ins) -> case Scoped param effect (Sem rInitial) a
effect of
        Run effect (Sem rInitial) a
act -> Union (effect : r) (Sem (effect : r)) x -> Sem (effect : r) x
forall (r :: [Effect]) a. Union r (Sem r) a -> Sem r a
liftSem (Union (effect : r) (Sem (effect : r)) x -> Sem (effect : r) x)
-> Union (effect : r) (Sem (effect : r)) x -> Sem (effect : r) x
forall a b. (a -> b) -> a -> b
$ Weaving effect (Sem (effect : r)) x
-> Union (effect : r) (Sem (effect : r)) x
forall (e :: Effect) (r :: [Effect]) (m :: * -> *) a.
Member e r =>
Weaving e m a -> Union r m a
injWeaving (Weaving effect (Sem (effect : r)) x
 -> Union (effect : r) (Sem (effect : r)) x)
-> Weaving effect (Sem (effect : r)) x
-> Union (effect : r) (Sem (effect : r)) x
forall a b. (a -> b) -> a -> b
$ effect (Sem rInitial) a
-> f ()
-> (forall x. f (Sem rInitial x) -> Sem (effect : r) (f x))
-> (f a -> x)
-> (forall x. f x -> Maybe x)
-> Weaving effect (Sem (effect : r)) x
forall (f :: * -> *) (e :: Effect) (rInitial :: [Effect]) 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 effect (Sem rInitial) a
act f ()
s (Sem (Scoped param effect : effect : r) (f x)
-> Sem (effect : r) (f x)
InterpreterFor (Scoped param effect) (effect : r)
go (Sem (Scoped param effect : effect : r) (f x)
 -> Sem (effect : r) (f x))
-> (f (Sem rInitial x)
    -> Sem (Scoped param effect : effect : r) (f x))
-> f (Sem rInitial x)
-> Sem (effect : r) (f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Sem rInitial x) -> Sem (Scoped param effect : effect : r) (f x)
forall x.
f (Sem rInitial x) -> Sem (Scoped param effect : effect : r) (f x)
wv) f a -> x
ex forall x. f x -> Maybe x
ins
        InScope param
param Sem rInitial a
main -> Sem r x -> Sem (effect : r) x
forall (e :: Effect) (r :: [Effect]) a. Sem r a -> Sem (e : r) a
raise (Sem r x -> Sem (effect : r) x) -> Sem r x -> Sem (effect : r) x
forall a b. (a -> b) -> a -> b
$ param -> (resource -> Sem r x) -> Sem r x
forall x. param -> (resource -> Sem r x) -> Sem r x
withResource param
param \ resource
resource ->
          f a -> x
ex (f a -> x) -> Sem r (f a) -> Sem r x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (rInitial :: [Effect]) x.
 effect (Sem rInitial) x -> Tactical effect (Sem rInitial) r x)
-> Sem (effect : r) (f a) -> Sem r (f a)
forall (e :: Effect) (r :: [Effect]) a.
(forall (rInitial :: [Effect]) x.
 e (Sem rInitial) x -> Tactical e (Sem rInitial) r x)
-> Sem (e : r) a -> Sem r a
interpretH (resource
-> effect (Sem rInitial) x -> Tactical effect (Sem rInitial) r x
forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Tactical effect (Sem r0) r x
scopedHandler resource
resource) (Sem (Scoped param effect : effect : r) (f a)
-> Sem (effect : r) (f a)
InterpreterFor (Scoped param effect) (effect : r)
go (Sem (Scoped param effect : effect : r) (f a)
 -> Sem (effect : r) (f a))
-> Sem (Scoped param effect : effect : r) (f a)
-> Sem (effect : r) (f a)
forall a b. (a -> b) -> a -> b
$ f (Sem rInitial a) -> Sem (Scoped param effect : effect : r) (f a)
forall x.
f (Sem rInitial x) -> Sem (Scoped param effect : effect : r) (f x)
wv (Sem rInitial a
main Sem rInitial a -> f () -> f (Sem rInitial a)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s))
{-# inline interpretScopedH #-}

-- | Variant of 'interpretScopedH' that allows the resource acquisition function
-- to use 'Tactical'.
interpretScopedH' ::
  ∀ resource param effect r .
  (∀ e r0 x . param -> (resource -> Tactical e (Sem r0) r x) ->
    Tactical e (Sem r0) r x) ->
  (∀ r0 x .
    resource -> effect (Sem r0) x ->
    Tactical (Scoped param effect) (Sem r0) r x) ->
  InterpreterFor (Scoped param effect) r
interpretScopedH' :: forall resource param (effect :: Effect) (r :: [Effect]).
(forall (e :: Effect) (r0 :: [Effect]) x.
 param
 -> (resource -> Tactical e (Sem r0) r x)
 -> Tactical e (Sem r0) r x)
-> (forall (r0 :: [Effect]) x.
    resource
    -> effect (Sem r0) x
    -> Tactical (Scoped param effect) (Sem r0) r x)
-> InterpreterFor (Scoped param effect) r
interpretScopedH' forall (e :: Effect) (r0 :: [Effect]) x.
param
-> (resource -> Tactical e (Sem r0) r x) -> Tactical e (Sem r0) r x
withResource forall (r0 :: [Effect]) x.
resource
-> effect (Sem r0) x -> Tactical (Scoped param effect) (Sem r0) r x
scopedHandler =
  resource -> InterpreterFor (Scoped param effect) r
go ([Char] -> resource
forall a. [Char] -> a
errorWithoutStackTrace [Char]
"top level run")
  where
    go :: resource -> InterpreterFor (Scoped param effect) r
    go :: resource -> InterpreterFor (Scoped param effect) r
go resource
resource =
      (forall (rInitial :: [Effect]) x.
 Scoped param effect (Sem rInitial) x
 -> Tactical (Scoped param effect) (Sem rInitial) r x)
-> Sem (Scoped param effect : r) a -> Sem r a
forall (e :: Effect) (r :: [Effect]) a.
(forall (rInitial :: [Effect]) x.
 e (Sem rInitial) x -> Tactical e (Sem rInitial) r x)
-> Sem (e : r) a -> Sem r a
interpretH \case
        Run effect (Sem rInitial) x
act ->
          resource
-> effect (Sem rInitial) x
-> Tactical (Scoped param effect) (Sem rInitial) r x
forall (r0 :: [Effect]) x.
resource
-> effect (Sem r0) x -> Tactical (Scoped param effect) (Sem r0) r x
scopedHandler resource
resource effect (Sem rInitial) x
act
        InScope param
param Sem rInitial x
main ->
          param
-> (resource -> Tactical (Scoped param effect) (Sem rInitial) r x)
-> Tactical (Scoped param effect) (Sem rInitial) r x
forall (e :: Effect) (r0 :: [Effect]) x.
param
-> (resource -> Tactical e (Sem r0) r x) -> Tactical e (Sem r0) r x
withResource param
param \ resource
resource' ->
            Sem r (f x)
-> Sem (WithTactics (Scoped param effect) f (Sem rInitial) r) (f x)
forall (e :: Effect) (r :: [Effect]) a. Sem r a -> Sem (e : r) a
raise (Sem r (f x)
 -> Sem
      (WithTactics (Scoped param effect) f (Sem rInitial) r) (f x))
-> (Sem (Scoped param effect : r) (f x) -> Sem r (f x))
-> Sem (Scoped param effect : r) (f x)
-> Sem (WithTactics (Scoped param effect) f (Sem rInitial) r) (f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. resource -> InterpreterFor (Scoped param effect) r
go resource
resource' (Sem (Scoped param effect : r) (f x)
 -> Sem
      (WithTactics (Scoped param effect) f (Sem rInitial) r) (f x))
-> Sem
     (WithTactics (Scoped param effect) f (Sem rInitial) r)
     (Sem (Scoped param effect : r) (f x))
-> Sem (WithTactics (Scoped param effect) f (Sem rInitial) r) (f x)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Sem rInitial x
-> Sem
     (WithTactics (Scoped param effect) f (Sem rInitial) r)
     (Sem (Scoped param effect : r) (f x))
forall (m :: * -> *) a (e :: Effect) (f :: * -> *) (r :: [Effect]).
m a -> Sem (WithTactics e f m r) (Sem (e : r) (f a))
runT Sem rInitial x
main
{-# inline interpretScopedH' #-}

-- | First-order variant of 'interpretScopedH'.
interpretScoped ::
  ∀ resource param effect r .
  (∀ x . param -> (resource -> Sem r x) -> Sem r x) ->
  (∀ m x . resource -> effect m x -> Sem r x) ->
  InterpreterFor (Scoped param effect) r
interpretScoped :: forall resource param (effect :: Effect) (r :: [Effect]).
(forall x. param -> (resource -> Sem r x) -> Sem r x)
-> (forall (m :: * -> *) x. resource -> effect m x -> Sem r x)
-> InterpreterFor (Scoped param effect) r
interpretScoped forall x. param -> (resource -> Sem r x) -> Sem r x
withResource forall (m :: * -> *) x. resource -> effect m x -> Sem r x
scopedHandler =
  (forall x. param -> (resource -> Sem r x) -> Sem r x)
-> (forall (r0 :: [Effect]) x.
    resource -> effect (Sem r0) x -> Tactical effect (Sem r0) r x)
-> InterpreterFor (Scoped param effect) r
forall resource param (effect :: Effect) (r :: [Effect]).
(forall x. param -> (resource -> Sem r x) -> Sem r x)
-> (forall (r0 :: [Effect]) x.
    resource -> effect (Sem r0) x -> Tactical effect (Sem r0) r x)
-> InterpreterFor (Scoped param effect) r
interpretScopedH forall x. param -> (resource -> Sem r x) -> Sem r x
withResource \ resource
r effect (Sem r0) x
e -> Sem r x -> Sem (WithTactics effect f (Sem r0) r) (f x)
forall (m :: * -> *) (f :: * -> *) (r :: [Effect]) (e :: Effect) a.
Functor f =>
Sem r a -> Sem (WithTactics e f m r) (f a)
liftT (resource -> effect (Sem r0) x -> Sem r x
forall (m :: * -> *) x. resource -> effect m x -> Sem r x
scopedHandler resource
r effect (Sem r0) x
e)
{-# inline interpretScoped #-}

-- | Variant of 'interpretScoped' in which the resource allocator is a plain
-- action.
interpretScopedAs ::
  ∀ resource param effect r .
  (param -> Sem r resource) ->
  (∀ m x . resource -> effect m x -> Sem r x) ->
  InterpreterFor (Scoped param effect) r
interpretScopedAs :: forall resource param (effect :: Effect) (r :: [Effect]).
(param -> Sem r resource)
-> (forall (m :: * -> *) x. resource -> effect m x -> Sem r x)
-> InterpreterFor (Scoped param effect) r
interpretScopedAs param -> Sem r resource
resource =
  (forall x. param -> (resource -> Sem r x) -> Sem r x)
-> (forall (m :: * -> *) x. resource -> effect m x -> Sem r x)
-> InterpreterFor (Scoped param effect) r
forall resource param (effect :: Effect) (r :: [Effect]).
(forall x. param -> (resource -> Sem r x) -> Sem r x)
-> (forall (m :: * -> *) x. resource -> effect m x -> Sem r x)
-> InterpreterFor (Scoped param effect) r
interpretScoped \ param
p resource -> Sem r x
use -> resource -> Sem r x
use (resource -> Sem r x) -> Sem r resource -> Sem r x
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< param -> Sem r resource
resource param
p
{-# inline interpretScopedAs #-}

-- | Higher-order interpreter for 'Scoped' that allows the handler to use
-- additional effects that are interpreted by the resource allocator.
--
-- /Note/: It is necessary to specify the list of local interpreters with a type
-- application; GHC won't be able to figure them out from the type of
-- @withResource@.
--
-- As an example for a higher order effect, consider a mutexed concurrent state
-- effect, where an effectful function may lock write access to the state while
-- making it still possible to read it:
--
-- > data MState s :: Effect where
-- >   MState :: (s -> m (s, a)) -> MState s m a
-- >   MRead :: MState s m s
-- >
-- > makeSem ''MState
--
-- We can now use an 'Polysemy.AtomicState.AtomicState' to store the current
-- value and lock write access with an @MVar@. Since the state callback is
-- effectful, we need a higher order interpreter:
--
-- > withResource ::
-- >   Member (Embed IO) r =>
-- >   s ->
-- >   (MVar () -> Sem (AtomicState s : r) a) ->
-- >   Sem r a
-- > withResource initial use = do
-- >   tv <- embed (newTVarIO initial)
-- >   lock <- embed (newMVar ())
-- >   runAtomicStateTVar tv $ use lock
-- >
-- > interpretMState ::
-- >   ∀ s r .
-- >   Members [Resource, Embed IO] r =>
-- >   InterpreterFor (Scoped s (MState s)) r
-- > interpretMState =
-- >   interpretScopedWithH @'[AtomicState s] withResource \ lock -> \case
-- >     MState f ->
-- >       bracket_ (embed (takeMVar lock)) (embed (tryPutMVar lock ())) do
-- >         s0 <- atomicGet
-- >         res <- runTSimple (f s0)
-- >         Inspector ins <- getInspectorT
-- >         for_ (ins res) \ (s, _) -> atomicPut s
-- >         pure (snd <$> res)
-- >     MRead ->
-- >       liftT atomicGet
interpretScopedWithH ::
  ∀ extra resource param effect r r1 .
  KnownList extra =>
  r1 ~ (extra ++ r) =>
  (∀ x . param -> (resource -> Sem r1 x) -> Sem r x) ->
  (∀ r0 x . resource -> effect (Sem r0) x -> Tactical effect (Sem r0) r1 x) ->
  InterpreterFor (Scoped param effect) r
interpretScopedWithH :: forall (extra :: [Effect]) resource param (effect :: Effect)
       (r :: [Effect]) (r1 :: [Effect]).
(KnownList extra, r1 ~ (extra ++ r)) =>
(forall x. param -> (resource -> Sem r1 x) -> Sem r x)
-> (forall (r0 :: [Effect]) x.
    resource -> effect (Sem r0) x -> Tactical effect (Sem r0) r1 x)
-> InterpreterFor (Scoped param effect) r
interpretScopedWithH forall x. param -> (resource -> Sem r1 x) -> Sem r x
withResource forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Tactical effect (Sem r0) r1 x
scopedHandler =
  (forall x.
 Weaving (Scoped param effect) (Sem (Scoped param effect : r)) x
 -> Sem r x)
-> InterpreterFor (Scoped param effect) r
forall (e :: Effect) (r :: [Effect]).
(forall x. Weaving e (Sem (e : r)) x -> Sem r x)
-> InterpreterFor e r
interpretWeaving \case
    Weaving (InScope param
param Sem rInitial a
main) f ()
s forall x. f (Sem rInitial x) -> Sem (Scoped param effect : r) (f x)
wv f a -> x
ex forall x. f x -> Maybe x
_ ->
      f a -> x
ex (f a -> x) -> Sem r (f a) -> Sem r x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> param -> (resource -> Sem r1 (f a)) -> Sem r (f a)
forall x. param -> (resource -> Sem r1 x) -> Sem r x
withResource param
param \ resource
resource ->
        (forall (rInitial :: [Effect]) x.
 effect (Sem rInitial) x -> Tactical effect (Sem rInitial) r1 x)
-> Sem (effect : r1) (f a) -> Sem r1 (f a)
forall (e :: Effect) (r :: [Effect]) a.
(forall (rInitial :: [Effect]) x.
 e (Sem rInitial) x -> Tactical e (Sem rInitial) r x)
-> Sem (e : r) a -> Sem r a
interpretH (resource
-> effect (Sem rInitial) x -> Tactical effect (Sem rInitial) r1 x
forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Tactical effect (Sem r0) r1 x
scopedHandler resource
resource) (Sem (effect : r1) (f a) -> Sem r1 (f a))
-> Sem (effect : r1) (f a) -> Sem r1 (f a)
forall a b. (a -> b) -> a -> b
$ Sem (Scoped param effect : effect : r1) (f a)
-> Sem (effect : r1) (f a)
InterpreterFor (Scoped param effect) (effect : r1)
inScope (Sem (Scoped param effect : effect : r1) (f a)
 -> Sem (effect : r1) (f a))
-> Sem (Scoped param effect : effect : r1) (f a)
-> Sem (effect : r1) (f a)
forall a b. (a -> b) -> a -> b
$
          (forall (e :: Effect).
 ElemOf e (Scoped param effect : r)
 -> ElemOf e (Scoped param effect : effect : r1))
-> Sem (Scoped param effect : r) (f a)
-> Sem (Scoped param effect : effect : r1) (f a)
forall (r :: [Effect]) (r' :: [Effect]) a.
(forall (e :: Effect). ElemOf e r -> ElemOf e r')
-> Sem r a -> Sem r' a
restack
            (SList '[Scoped param effect]
-> SList (effect : extra)
-> ElemOf e (Append '[Scoped param effect] r)
-> ElemOf
     e (Append '[Scoped param effect] (Append (effect : extra) r))
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
             (forall (l :: [Effect]). KnownList l => SList l
forall {a} (l :: [a]). KnownList l => SList l
singList @'[Scoped param effect])
             (forall (l :: [Effect]). KnownList l => SList l
forall {a} (l :: [a]). KnownList l => SList l
singList @(effect : extra))) (Sem (Scoped param effect : r) (f a)
 -> Sem (Scoped param effect : effect : r1) (f a))
-> Sem (Scoped param effect : r) (f a)
-> Sem (Scoped param effect : effect : r1) (f a)
forall a b. (a -> b) -> a -> b
$ f (Sem rInitial a) -> Sem (Scoped param effect : r) (f a)
forall x. f (Sem rInitial x) -> Sem (Scoped param effect : r) (f x)
wv (Sem rInitial a
main Sem rInitial a -> f () -> f (Sem rInitial a)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s)
    Weaving (Scoped param effect) (Sem (Scoped param effect : r)) x
_ ->
      [Char] -> Sem r x
forall a. [Char] -> a
errorWithoutStackTrace [Char]
"top level Run"
  where
    inScope :: InterpreterFor (Scoped param effect) (effect : r1)
    inScope :: InterpreterFor (Scoped param effect) (effect : r1)
inScope =
      (forall x.
 Weaving
   (Scoped param effect) (Sem (Scoped param effect : effect : r1)) x
 -> Sem (effect : r1) x)
-> InterpreterFor (Scoped param effect) (effect : r1)
forall (e :: Effect) (r :: [Effect]).
(forall x. Weaving e (Sem (e : r)) x -> Sem r x)
-> InterpreterFor e r
interpretWeaving \case
        Weaving (InScope param
param Sem rInitial a
main) f ()
s forall x.
f (Sem rInitial x) -> Sem (Scoped param effect : effect : r1) (f x)
wv f a -> x
ex forall x. f x -> Maybe x
_ ->
          (forall (e :: Effect). ElemOf e r -> ElemOf e (effect : r1))
-> Sem r x -> Sem (effect : r1) x
forall (r :: [Effect]) (r' :: [Effect]) a.
(forall (e :: Effect). ElemOf e r -> ElemOf e r')
-> Sem r a -> Sem r' a
restack
            (SList (effect : extra)
-> ElemOf e r -> ElemOf e (Append (effect : extra) r)
forall {a} (l :: [a]) (r :: [a]) (e :: a).
SList l -> ElemOf e r -> ElemOf e (Append l r)
extendMembershipLeft (forall (l :: [Effect]). KnownList l => SList l
forall {a} (l :: [a]). KnownList l => SList l
singList @(effect : extra)))
            (f a -> x
ex (f a -> x) -> Sem r (f a) -> Sem r x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> param -> (resource -> Sem r1 (f a)) -> Sem r (f a)
forall x. param -> (resource -> Sem r1 x) -> Sem r x
withResource param
param \resource
resource ->
                (forall (rInitial :: [Effect]) x.
 effect (Sem rInitial) x -> Tactical effect (Sem rInitial) r1 x)
-> Sem (effect : r1) (f a) -> Sem r1 (f a)
forall (e :: Effect) (r :: [Effect]) a.
(forall (rInitial :: [Effect]) x.
 e (Sem rInitial) x -> Tactical e (Sem rInitial) r x)
-> Sem (e : r) a -> Sem r a
interpretH (resource
-> effect (Sem rInitial) x -> Tactical effect (Sem rInitial) r1 x
forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Tactical effect (Sem r0) r1 x
scopedHandler resource
resource) (Sem (effect : r1) (f a) -> Sem r1 (f a))
-> Sem (effect : r1) (f a) -> Sem r1 (f a)
forall a b. (a -> b) -> a -> b
$ Sem (Scoped param effect : effect : r1) (f a)
-> Sem (effect : r1) (f a)
InterpreterFor (Scoped param effect) (effect : r1)
inScope (Sem (Scoped param effect : effect : r1) (f a)
 -> Sem (effect : r1) (f a))
-> Sem (Scoped param effect : effect : r1) (f a)
-> Sem (effect : r1) (f a)
forall a b. (a -> b) -> a -> b
$ f (Sem rInitial a) -> Sem (Scoped param effect : effect : r1) (f a)
forall x.
f (Sem rInitial x) -> Sem (Scoped param effect : effect : r1) (f x)
wv (Sem rInitial a
main Sem rInitial a -> f () -> f (Sem rInitial a)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s))
        Weaving (Run effect (Sem rInitial) a
act) f ()
s forall x.
f (Sem rInitial x) -> Sem (Scoped param effect : effect : r1) (f x)
wv f a -> x
ex forall x. f x -> Maybe x
ins ->
          Union (effect : r1) (Sem (effect : r1)) x -> Sem (effect : r1) x
forall (r :: [Effect]) a. Union r (Sem r) a -> Sem r a
liftSem (Union (effect : r1) (Sem (effect : r1)) x -> Sem (effect : r1) x)
-> Union (effect : r1) (Sem (effect : r1)) x -> Sem (effect : r1) x
forall a b. (a -> b) -> a -> b
$ Weaving effect (Sem (effect : r1)) x
-> Union (effect : r1) (Sem (effect : r1)) x
forall (e :: Effect) (r :: [Effect]) (m :: * -> *) a.
Member e r =>
Weaving e m a -> Union r m a
injWeaving (Weaving effect (Sem (effect : r1)) x
 -> Union (effect : r1) (Sem (effect : r1)) x)
-> Weaving effect (Sem (effect : r1)) x
-> Union (effect : r1) (Sem (effect : r1)) x
forall a b. (a -> b) -> a -> b
$ effect (Sem rInitial) a
-> f ()
-> (forall x. f (Sem rInitial x) -> Sem (effect : r1) (f x))
-> (f a -> x)
-> (forall x. f x -> Maybe x)
-> Weaving effect (Sem (effect : r1)) x
forall (f :: * -> *) (e :: Effect) (rInitial :: [Effect]) 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 effect (Sem rInitial) a
act f ()
s (Sem (Scoped param effect : effect : r1) (f x)
-> Sem (effect : r1) (f x)
InterpreterFor (Scoped param effect) (effect : r1)
inScope (Sem (Scoped param effect : effect : r1) (f x)
 -> Sem (effect : r1) (f x))
-> (f (Sem rInitial x)
    -> Sem (Scoped param effect : effect : r1) (f x))
-> f (Sem rInitial x)
-> Sem (effect : r1) (f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Sem rInitial x) -> Sem (Scoped param effect : effect : r1) (f x)
forall x.
f (Sem rInitial x) -> Sem (Scoped param effect : effect : r1) (f x)
wv) f a -> x
ex forall x. f x -> Maybe x
ins
{-# inline interpretScopedWithH #-}

-- | First-order variant of 'interpretScopedWithH'.
--
-- /Note/: It is necessary to specify the list of local interpreters with a type
-- application; GHC won't be able to figure them out from the type of
-- @withResource@:
--
-- > data SomeAction :: Effect where
-- >   SomeAction :: SomeAction m ()
-- >
-- > foo :: InterpreterFor (Scoped () SomeAction) r
-- > foo =
-- >   interpretScopedWith @[Reader Int, State Bool] localEffects \ () -> \case
-- >     SomeAction -> put . (> 0) =<< ask @Int
-- >   where
-- >     localEffects () use = evalState False (runReader 5 (use ()))
interpretScopedWith ::
  ∀ extra param resource effect r r1 .
  r1 ~ (extra ++ r) =>
  KnownList extra =>
  (∀ x . param -> (resource -> Sem r1 x) -> Sem r x) ->
  (∀ m x . resource -> effect m x -> Sem r1 x) ->
  InterpreterFor (Scoped param effect) r
interpretScopedWith :: forall (extra :: [Effect]) param resource (effect :: Effect)
       (r :: [Effect]) (r1 :: [Effect]).
(r1 ~ (extra ++ r), KnownList extra) =>
(forall x. param -> (resource -> Sem r1 x) -> Sem r x)
-> (forall (m :: * -> *) x. resource -> effect m x -> Sem r1 x)
-> InterpreterFor (Scoped param effect) r
interpretScopedWith forall x. param -> (resource -> Sem r1 x) -> Sem r x
withResource forall (m :: * -> *) x. resource -> effect m x -> Sem r1 x
scopedHandler =
  forall (extra :: [Effect]) resource param (effect :: Effect)
       (r :: [Effect]) (r1 :: [Effect]).
(KnownList extra, r1 ~ (extra ++ r)) =>
(forall x. param -> (resource -> Sem r1 x) -> Sem r x)
-> (forall (r0 :: [Effect]) x.
    resource -> effect (Sem r0) x -> Tactical effect (Sem r0) r1 x)
-> InterpreterFor (Scoped param effect) r
interpretScopedWithH @extra forall x. param -> (resource -> Sem r1 x) -> Sem r x
withResource \ resource
r effect (Sem r0) x
e -> Sem r1 x -> Sem (WithTactics effect f (Sem r0) r1) (f x)
forall (m :: * -> *) (f :: * -> *) (r :: [Effect]) (e :: Effect) a.
Functor f =>
Sem r a -> Sem (WithTactics e f m r) (f a)
liftT (resource -> effect (Sem r0) x -> Sem r1 x
forall (m :: * -> *) x. resource -> effect m x -> Sem r1 x
scopedHandler resource
r effect (Sem r0) x
e)
{-# inline interpretScopedWith #-}

-- | Variant of 'interpretScopedWith' in which no resource is used and the
-- resource allocator is a plain interpreter.
-- This is useful for scopes that only need local effects, but no resources in
-- the handler.
--
-- See the /Note/ on 'interpretScopedWithH'.
interpretScopedWith_ ::
  ∀ extra param effect r r1 .
  r1 ~ (extra ++ r) =>
  KnownList extra =>
  (∀ x . param -> Sem r1 x -> Sem r x) ->
  (∀ m x . effect m x -> Sem r1 x) ->
  InterpreterFor (Scoped param effect) r
interpretScopedWith_ :: forall (extra :: [Effect]) param (effect :: Effect) (r :: [Effect])
       (r1 :: [Effect]).
(r1 ~ (extra ++ r), KnownList extra) =>
(forall x. param -> Sem r1 x -> Sem r x)
-> (forall (m :: * -> *) x. effect m x -> Sem r1 x)
-> InterpreterFor (Scoped param effect) r
interpretScopedWith_ forall x. param -> Sem r1 x -> Sem r x
withResource forall (m :: * -> *) x. effect m x -> Sem r1 x
scopedHandler =
  forall (extra :: [Effect]) resource param (effect :: Effect)
       (r :: [Effect]) (r1 :: [Effect]).
(KnownList extra, r1 ~ (extra ++ r)) =>
(forall x. param -> (resource -> Sem r1 x) -> Sem r x)
-> (forall (r0 :: [Effect]) x.
    resource -> effect (Sem r0) x -> Tactical effect (Sem r0) r1 x)
-> InterpreterFor (Scoped param effect) r
interpretScopedWithH @extra (\ param
p () -> Sem r1 x
f -> param -> Sem r1 x -> Sem r x
forall x. param -> Sem r1 x -> Sem r x
withResource param
p (() -> Sem r1 x
f ())) \ () effect (Sem r0) x
e -> Sem r1 x -> Sem (WithTactics effect f (Sem r0) r1) (f x)
forall (m :: * -> *) (f :: * -> *) (r :: [Effect]) (e :: Effect) a.
Functor f =>
Sem r a -> Sem (WithTactics e f m r) (f a)
liftT (effect (Sem r0) x -> Sem r1 x
forall (m :: * -> *) x. effect m x -> Sem r1 x
scopedHandler effect (Sem r0) x
e)
{-# inline interpretScopedWith_ #-}

-- | Variant of 'interpretScoped' that uses another interpreter instead of a
-- handler.
--
-- This is mostly useful if you want to reuse an interpreter that you cannot
-- easily rewrite (like from another library). If you have full control over the
-- implementation, 'interpretScoped' should be preferred.
--
-- /Note/: In previous versions of Polysemy, the wrapped interpreter was
-- executed fully, including the initializing code surrounding its handler,
-- for each action in the program. However, new and continuing discoveries
-- regarding 'Scoped' has allowed the improvement of having the interpreter be
-- used only once per use of 'scoped', and have it cover the same scope of
-- actions that @withResource@ does.
--
-- This renders @withResource@ practically redundant; for the moment, the API
-- surrounding 'Scoped' remains the same, but work is in progress to revamp the
-- entire API of 'Scoped'.
runScoped ::
  ∀ resource param effect r .
  (∀ x . param -> (resource -> Sem r x) -> Sem r x) ->
  (resource -> InterpreterFor effect r) ->
  InterpreterFor (Scoped param effect) r
runScoped :: forall resource param (effect :: Effect) (r :: [Effect]).
(forall x. param -> (resource -> Sem r x) -> Sem r x)
-> (resource -> InterpreterFor effect r)
-> InterpreterFor (Scoped param effect) r
runScoped forall x. param -> (resource -> Sem r x) -> Sem r x
withResource resource -> InterpreterFor effect r
scopedInterpreter =
  (forall x.
 Weaving (Scoped param effect) (Sem (Scoped param effect : r)) x
 -> Sem r x)
-> InterpreterFor (Scoped param effect) r
forall (e :: Effect) (r :: [Effect]).
(forall x. Weaving e (Sem (e : r)) x -> Sem r x)
-> InterpreterFor e r
interpretWeaving \(Weaving Scoped param effect (Sem rInitial) a
effect f ()
s forall x. f (Sem rInitial x) -> Sem (Scoped param effect : r) (f x)
wv f a -> x
ex forall x. f x -> Maybe x
_) -> case Scoped param effect (Sem rInitial) a
effect of
    Run effect (Sem rInitial) a
_ -> [Char] -> Sem r x
forall a. [Char] -> a
errorWithoutStackTrace [Char]
"top level run"
    InScope param
param Sem rInitial a
main -> param -> (resource -> Sem r x) -> Sem r x
forall x. param -> (resource -> Sem r x) -> Sem r x
withResource param
param \ resource
resource ->
      f a -> x
ex (f a -> x) -> Sem r (f a) -> Sem r x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> resource -> InterpreterFor effect r
scopedInterpreter resource
resource (Sem (Scoped param effect : effect : r) (f a)
-> Sem (effect : r) (f a)
InterpreterFor (Scoped param effect) (effect : r)
go (Sem (Scoped param effect : r) (f a)
-> Sem (Scoped param effect : effect : r) (f a)
forall (e2 :: Effect) (e1 :: Effect) (r :: [Effect]) a.
Sem (e1 : r) a -> Sem (e1 : e2 : r) a
raiseUnder (Sem (Scoped param effect : r) (f a)
 -> Sem (Scoped param effect : effect : r) (f a))
-> Sem (Scoped param effect : r) (f a)
-> Sem (Scoped param effect : effect : r) (f a)
forall a b. (a -> b) -> a -> b
$ f (Sem rInitial a) -> Sem (Scoped param effect : r) (f a)
forall x. f (Sem rInitial x) -> Sem (Scoped param effect : r) (f x)
wv (Sem rInitial a
main Sem rInitial a -> f () -> f (Sem rInitial a)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s)))
  where
    go :: InterpreterFor (Scoped param effect) (effect : r)
    go :: InterpreterFor (Scoped param effect) (effect : r)
go =
      (forall x.
 Weaving
   (Scoped param effect) (Sem (Scoped param effect : effect : r)) x
 -> Sem (effect : r) x)
-> InterpreterFor (Scoped param effect) (effect : r)
forall (e :: Effect) (r :: [Effect]).
(forall x. Weaving e (Sem (e : r)) x -> Sem r x)
-> InterpreterFor e r
interpretWeaving \ (Weaving Scoped param effect (Sem rInitial) a
effect f ()
s forall x.
f (Sem rInitial x) -> Sem (Scoped param effect : effect : r) (f x)
wv f a -> x
ex forall x. f x -> Maybe x
ins) -> case Scoped param effect (Sem rInitial) a
effect of
        Run effect (Sem rInitial) a
act -> Union (effect : r) (Sem (effect : r)) x -> Sem (effect : r) x
forall (r :: [Effect]) a. Union r (Sem r) a -> Sem r a
liftSem (Union (effect : r) (Sem (effect : r)) x -> Sem (effect : r) x)
-> Union (effect : r) (Sem (effect : r)) x -> Sem (effect : r) x
forall a b. (a -> b) -> a -> b
$ Weaving effect (Sem (effect : r)) x
-> Union (effect : r) (Sem (effect : r)) x
forall (e :: Effect) (r :: [Effect]) (m :: * -> *) a.
Member e r =>
Weaving e m a -> Union r m a
injWeaving (Weaving effect (Sem (effect : r)) x
 -> Union (effect : r) (Sem (effect : r)) x)
-> Weaving effect (Sem (effect : r)) x
-> Union (effect : r) (Sem (effect : r)) x
forall a b. (a -> b) -> a -> b
$ effect (Sem rInitial) a
-> f ()
-> (forall x. f (Sem rInitial x) -> Sem (effect : r) (f x))
-> (f a -> x)
-> (forall x. f x -> Maybe x)
-> Weaving effect (Sem (effect : r)) x
forall (f :: * -> *) (e :: Effect) (rInitial :: [Effect]) 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 effect (Sem rInitial) a
act f ()
s (Sem (Scoped param effect : effect : r) (f x)
-> Sem (effect : r) (f x)
InterpreterFor (Scoped param effect) (effect : r)
go (Sem (Scoped param effect : effect : r) (f x)
 -> Sem (effect : r) (f x))
-> (f (Sem rInitial x)
    -> Sem (Scoped param effect : effect : r) (f x))
-> f (Sem rInitial x)
-> Sem (effect : r) (f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Sem rInitial x) -> Sem (Scoped param effect : effect : r) (f x)
forall x.
f (Sem rInitial x) -> Sem (Scoped param effect : effect : r) (f x)
wv) f a -> x
ex forall x. f x -> Maybe x
ins
        InScope param
param Sem rInitial a
main ->
          Sem r x -> Sem (effect : r) x
forall (e :: Effect) (r :: [Effect]) a. Sem r a -> Sem (e : r) a
raise (Sem r x -> Sem (effect : r) x) -> Sem r x -> Sem (effect : r) x
forall a b. (a -> b) -> a -> b
$ param -> (resource -> Sem r x) -> Sem r x
forall x. param -> (resource -> Sem r x) -> Sem r x
withResource param
param \ resource
resource ->
            f a -> x
ex (f a -> x) -> Sem r (f a) -> Sem r x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> resource -> InterpreterFor effect r
scopedInterpreter resource
resource (Sem (Scoped param effect : effect : r) (f a)
-> Sem (effect : r) (f a)
InterpreterFor (Scoped param effect) (effect : r)
go (f (Sem rInitial a) -> Sem (Scoped param effect : effect : r) (f a)
forall x.
f (Sem rInitial x) -> Sem (Scoped param effect : effect : r) (f x)
wv (Sem rInitial a
main Sem rInitial a -> f () -> f (Sem rInitial a)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s)))
{-# inline runScoped #-}

-- | Variant of 'runScoped' in which the resource allocator returns the resource
-- rather tnen calling a continuation.
runScopedAs ::
  ∀ resource param effect r .
  (param -> Sem r resource) ->
  (resource -> InterpreterFor effect r) ->
  InterpreterFor (Scoped param effect) r
runScopedAs :: forall resource param (effect :: Effect) (r :: [Effect]).
(param -> Sem r resource)
-> (resource -> InterpreterFor effect r)
-> InterpreterFor (Scoped param effect) r
runScopedAs param -> Sem r resource
resource = (forall x. param -> (resource -> Sem r x) -> Sem r x)
-> (resource -> InterpreterFor effect r)
-> InterpreterFor (Scoped param effect) r
forall resource param (effect :: Effect) (r :: [Effect]).
(forall x. param -> (resource -> Sem r x) -> Sem r x)
-> (resource -> InterpreterFor effect r)
-> InterpreterFor (Scoped param effect) r
runScoped \ param
p resource -> Sem r x
use -> resource -> Sem r x
use (resource -> Sem r x) -> Sem r resource -> Sem r x
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< param -> Sem r resource
resource param
p
{-# inline runScopedAs #-}

-- |Combined higher-order interpreter for 'Scoped' and 'Resumable'.
-- This allows 'Stop' to be sent from within the resource allocator so that the consumer receives it, terminating the
-- entire scope.
interpretScopedResumableH ::
  ∀ param resource effect err r .
  (∀ x . param -> (resource -> Sem (Stop err : r) x) -> Sem (Stop err : r) x) ->
  (∀ r0 x . resource -> effect (Sem r0) x -> Tactical effect (Sem r0) (Stop err : r) x) ->
  InterpreterFor (Scoped param effect !! err) r
interpretScopedResumableH :: forall param resource (effect :: Effect) err (r :: [Effect]).
(forall x.
 param
 -> (resource -> Sem (Stop err : r) x) -> Sem (Stop err : r) x)
-> (forall (r0 :: [Effect]) x.
    resource
    -> effect (Sem r0) x -> Tactical effect (Sem r0) (Stop err : r) x)
-> InterpreterFor (Scoped param effect !! err) r
interpretScopedResumableH forall x.
param -> (resource -> Sem (Stop err : r) x) -> Sem (Stop err : r) x
withResource forall (r0 :: [Effect]) x.
resource
-> effect (Sem r0) x -> Tactical effect (Sem r0) (Stop err : r) x
scopedHandler =
  (forall x.
 Weaving
   (Scoped param effect !! err)
   (Sem ((Scoped param effect !! err) : r))
   x
 -> Sem r x)
-> InterpreterFor (Scoped param effect !! err) r
forall (e :: Effect) (r :: [Effect]).
(forall x. Weaving e (Sem (e : r)) x -> Sem r x)
-> InterpreterFor e r
interpretWeaving \case
    Weaving (Resumable (Weaving (InScope param
param Sem rInitial a
main) f ()
s' forall x. f (Sem rInitial x) -> Sem r (f x)
wv' f a -> a1
ex' forall x. f x -> Maybe x
_)) f ()
s forall x.
f (Sem rInitial x) -> Sem ((Scoped param effect !! err) : r) (f x)
wv f a -> x
ex forall x. f x -> Maybe x
_ -> do
      f ()
-> (f (Either err a1) -> x)
-> (f a -> a1)
-> Sem r (Either err (f (f a)))
-> Sem r x
forall {k} (f :: * -> *) err a x (f' :: k -> *) (a' :: k)
       (r :: [Effect]).
Functor f =>
f ()
-> (f (Either err a) -> x)
-> (f' a' -> a)
-> Sem r (Either err (f (f' a')))
-> Sem r x
exResumable f ()
s f a -> x
f (Either err a1) -> x
ex f a -> a1
ex' (Sem r (Either err (f (f a))) -> Sem r x)
-> Sem r (Either err (f (f a))) -> Sem r x
forall a b. (a -> b) -> a -> b
$ Sem (Stop err : r) (f (f a)) -> Sem r (Either err (f (f a)))
forall e (r :: [Effect]) a.
Sem (Stop e : r) a -> Sem r (Either e a)
runStop (Sem (Stop err : r) (f (f a)) -> Sem r (Either err (f (f a))))
-> Sem (Stop err : r) (f (f a)) -> Sem r (Either err (f (f a)))
forall a b. (a -> b) -> a -> b
$ param
-> (resource -> Sem (Stop err : r) (f (f a)))
-> Sem (Stop err : r) (f (f a))
forall x.
param -> (resource -> Sem (Stop err : r) x) -> Sem (Stop err : r) x
withResource param
param \ resource
resource ->
        (forall (rInitial :: [Effect]) x.
 effect (Sem rInitial) x
 -> Tactical effect (Sem rInitial) (Stop err : r) x)
-> Sem (effect : Stop err : r) (f (f a))
-> Sem (Stop err : r) (f (f a))
forall (e :: Effect) (r :: [Effect]) a.
(forall (rInitial :: [Effect]) x.
 e (Sem rInitial) x -> Tactical e (Sem rInitial) r x)
-> Sem (e : r) a -> Sem r a
interpretH (resource
-> effect (Sem rInitial) x
-> Tactical effect (Sem rInitial) (Stop err : r) x
forall (r0 :: [Effect]) x.
resource
-> effect (Sem r0) x -> Tactical effect (Sem r0) (Stop err : r) x
scopedHandler resource
resource) (Sem (effect : r) (f (f a)) -> Sem (effect : Stop err : r) (f (f a))
forall (e2 :: Effect) (e1 :: Effect) (r :: [Effect]) a.
Sem (e1 : r) a -> Sem (e1 : e2 : r) a
raiseUnder (Sem ((Scoped param effect !! err) : effect : r) (f (f a))
-> Sem (effect : r) (f (f a))
InterpreterFor (Scoped param effect !! err) (effect : r)
go (Sem ((Scoped param effect !! err) : effect : r) (f (f a))
 -> Sem (effect : r) (f (f a)))
-> Sem ((Scoped param effect !! err) : effect : r) (f (f a))
-> Sem (effect : r) (f (f a))
forall a b. (a -> b) -> a -> b
$ Sem ((Scoped param effect !! err) : r) (f (f a))
-> Sem ((Scoped param effect !! err) : effect : r) (f (f a))
forall (e2 :: Effect) (e1 :: Effect) (r :: [Effect]) a.
Sem (e1 : r) a -> Sem (e1 : e2 : r) a
raiseUnder (Sem ((Scoped param effect !! err) : r) (f (f a))
 -> Sem ((Scoped param effect !! err) : effect : r) (f (f a)))
-> Sem ((Scoped param effect !! err) : r) (f (f a))
-> Sem ((Scoped param effect !! err) : effect : r) (f (f a))
forall a b. (a -> b) -> a -> b
$ f (Sem rInitial (f a))
-> Sem ((Scoped param effect !! err) : r) (f (f a))
forall x.
f (Sem rInitial x) -> Sem ((Scoped param effect !! err) : r) (f x)
wv ((f (Sem rInitial a) -> Sem r (f a)
forall x. f (Sem rInitial x) -> Sem r (f x)
wv' (Sem rInitial a
main Sem rInitial a -> f () -> f (Sem rInitial a)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s')) Sem r (f a) -> f () -> f (Sem r (f a))
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s)))
    Weaving
  (Scoped param effect !! err)
  (Sem ((Scoped param effect !! err) : r))
  x
_ ->
      [Char] -> Sem r x
forall a. [Char] -> a
errorWithoutStackTrace [Char]
"top level run"
  where
    go :: InterpreterFor (Scoped param effect !! err) (effect : r)
    go :: InterpreterFor (Scoped param effect !! err) (effect : r)
go =
      (forall x.
 Weaving
   (Scoped param effect !! err)
   (Sem ((Scoped param effect !! err) : effect : r))
   x
 -> Sem (effect : r) x)
-> InterpreterFor (Scoped param effect !! err) (effect : r)
forall (e :: Effect) (r :: [Effect]).
(forall x. Weaving e (Sem (e : r)) x -> Sem r x)
-> InterpreterFor e r
interpretWeaving \ (Weaving (Resumable (Weaving Scoped param effect (Sem rInitial) a
effect f ()
s' forall x. f (Sem rInitial x) -> Sem r (f x)
wv' f a -> a1
ex' forall x. f x -> Maybe x
ins')) f ()
s forall x.
f (Sem rInitial x)
-> Sem ((Scoped param effect !! err) : effect : r) (f x)
wv f a -> x
ex forall x. f x -> Maybe x
ins) -> case Scoped param effect (Sem rInitial) a
effect of
        Run effect (Sem rInitial) a
act ->
          f a -> x
ex (f a -> x) -> (f a1 -> f a) -> f a1 -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a1 -> Either err a1) -> f a1 -> f (Either err a1)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a1 -> Either err a1
forall a b. b -> Either a b
Right (f a1 -> x) -> Sem (effect : r) (f a1) -> Sem (effect : r) x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Union (effect : r) (Sem (effect : r)) (f a1)
-> Sem (effect : r) (f a1)
forall (r :: [Effect]) a. Union r (Sem r) a -> Sem r a
liftSem (f ()
-> (forall x. f (Sem rInitial x) -> Sem (effect : r) (f x))
-> (forall x. f x -> Maybe x)
-> Union (effect : r) (Sem rInitial) a1
-> Union (effect : r) (Sem (effect : r)) (f a1)
forall (s :: * -> *) (n :: * -> *) (m :: * -> *) (r :: [Effect]) a.
(Functor s, Functor n) =>
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 f ()
s (Sem ((Scoped param effect !! err) : effect : r) (f x)
-> Sem (effect : r) (f x)
InterpreterFor (Scoped param effect !! err) (effect : r)
go (Sem ((Scoped param effect !! err) : effect : r) (f x)
 -> Sem (effect : r) (f x))
-> (f (Sem rInitial x)
    -> Sem ((Scoped param effect !! err) : effect : r) (f x))
-> f (Sem rInitial x)
-> Sem (effect : r) (f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Sem rInitial x)
-> Sem ((Scoped param effect !! err) : effect : r) (f x)
forall x.
f (Sem rInitial x)
-> Sem ((Scoped param effect !! err) : effect : r) (f x)
wv) forall x. f x -> Maybe x
ins (Weaving effect (Sem rInitial) a1
-> Union (effect : r) (Sem rInitial) a1
forall (e :: Effect) (r :: [Effect]) (m :: * -> *) a.
Member e r =>
Weaving e m a -> Union r m a
injWeaving (effect (Sem rInitial) a
-> f ()
-> (forall x. f (Sem rInitial x) -> Sem rInitial (f x))
-> (f a -> a1)
-> (forall x. f x -> Maybe x)
-> Weaving effect (Sem rInitial) a1
forall (f :: * -> *) (e :: Effect) (rInitial :: [Effect]) 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 effect (Sem rInitial) a
act f ()
s' forall x. f (Sem rInitial x) -> Sem rInitial (f x)
forall x. f (Sem rInitial x) -> Sem r (f x)
wv' f a -> a1
ex' forall x. f x -> Maybe x
ins')))
        InScope param
param Sem rInitial a
main -> do
          f ()
-> (f (Either err a1) -> x)
-> (f a -> a1)
-> Sem (effect : r) (Either err (f (f a)))
-> Sem (effect : r) x
forall {k} (f :: * -> *) err a x (f' :: k -> *) (a' :: k)
       (r :: [Effect]).
Functor f =>
f ()
-> (f (Either err a) -> x)
-> (f' a' -> a)
-> Sem r (Either err (f (f' a')))
-> Sem r x
exResumable f ()
s f a -> x
f (Either err a1) -> x
ex f a -> a1
ex' (Sem (effect : r) (Either err (f (f a))) -> Sem (effect : r) x)
-> Sem (effect : r) (Either err (f (f a))) -> Sem (effect : r) x
forall a b. (a -> b) -> a -> b
$ Sem r (Either err (f (f a)))
-> Sem (effect : r) (Either err (f (f a)))
forall (e :: Effect) (r :: [Effect]) a. Sem r a -> Sem (e : r) a
raise (Sem r (Either err (f (f a)))
 -> Sem (effect : r) (Either err (f (f a))))
-> Sem r (Either err (f (f a)))
-> Sem (effect : r) (Either err (f (f a)))
forall a b. (a -> b) -> a -> b
$ Sem (Stop err : r) (f (f a)) -> Sem r (Either err (f (f a)))
forall e (r :: [Effect]) a.
Sem (Stop e : r) a -> Sem r (Either e a)
runStop (Sem (Stop err : r) (f (f a)) -> Sem r (Either err (f (f a))))
-> Sem (Stop err : r) (f (f a)) -> Sem r (Either err (f (f a)))
forall a b. (a -> b) -> a -> b
$ param
-> (resource -> Sem (Stop err : r) (f (f a)))
-> Sem (Stop err : r) (f (f a))
forall x.
param -> (resource -> Sem (Stop err : r) x) -> Sem (Stop err : r) x
withResource param
param \ resource
resource ->
            (forall (rInitial :: [Effect]) x.
 effect (Sem rInitial) x
 -> Tactical effect (Sem rInitial) (Stop err : r) x)
-> Sem (effect : Stop err : r) (f (f a))
-> Sem (Stop err : r) (f (f a))
forall (e :: Effect) (r :: [Effect]) a.
(forall (rInitial :: [Effect]) x.
 e (Sem rInitial) x -> Tactical e (Sem rInitial) r x)
-> Sem (e : r) a -> Sem r a
interpretH (resource
-> effect (Sem rInitial) x
-> Tactical effect (Sem rInitial) (Stop err : r) x
forall (r0 :: [Effect]) x.
resource
-> effect (Sem r0) x -> Tactical effect (Sem r0) (Stop err : r) x
scopedHandler resource
resource) (Sem (effect : r) (f (f a)) -> Sem (effect : Stop err : r) (f (f a))
forall (e2 :: Effect) (e1 :: Effect) (r :: [Effect]) a.
Sem (e1 : r) a -> Sem (e1 : e2 : r) a
raiseUnder (Sem ((Scoped param effect !! err) : effect : r) (f (f a))
-> Sem (effect : r) (f (f a))
InterpreterFor (Scoped param effect !! err) (effect : r)
go (Sem ((Scoped param effect !! err) : effect : r) (f (f a))
 -> Sem (effect : r) (f (f a)))
-> Sem ((Scoped param effect !! err) : effect : r) (f (f a))
-> Sem (effect : r) (f (f a))
forall a b. (a -> b) -> a -> b
$ f (Sem rInitial (f a))
-> Sem ((Scoped param effect !! err) : effect : r) (f (f a))
forall x.
f (Sem rInitial x)
-> Sem ((Scoped param effect !! err) : effect : r) (f x)
wv (f (Sem rInitial a) -> Sem r (f a)
forall x. f (Sem rInitial x) -> Sem r (f x)
wv' (Sem rInitial a
main Sem rInitial a -> f () -> f (Sem rInitial a)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s') Sem r (f a) -> f () -> f (Sem r (f a))
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s)))

-- |Combined interpreter for 'Scoped' and 'Resumable'.
-- This allows 'Stop' to be sent from within the resource allocator so that the consumer receives it, terminating the
-- entire scope.
interpretScopedResumable ::
  ∀ param resource effect err r .
  (∀ x . param -> (resource -> Sem (Stop err : r) x) -> Sem (Stop err : r) x) ->
  (∀ r0 x . resource -> effect (Sem r0) x -> Sem (Stop err : r) x) ->
  InterpreterFor (Scoped param effect !! err) r
interpretScopedResumable :: forall param resource (effect :: Effect) err (r :: [Effect]).
(forall x.
 param
 -> (resource -> Sem (Stop err : r) x) -> Sem (Stop err : r) x)
-> (forall (r0 :: [Effect]) x.
    resource -> effect (Sem r0) x -> Sem (Stop err : r) x)
-> InterpreterFor (Scoped param effect !! err) r
interpretScopedResumable forall x.
param -> (resource -> Sem (Stop err : r) x) -> Sem (Stop err : r) x
withResource forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Sem (Stop err : r) x
scopedHandler =
  (forall x.
 param
 -> (resource -> Sem (Stop err : r) x) -> Sem (Stop err : r) x)
-> (forall (r0 :: [Effect]) x.
    resource
    -> effect (Sem r0) x -> Tactical effect (Sem r0) (Stop err : r) x)
-> InterpreterFor (Scoped param effect !! err) r
forall param resource (effect :: Effect) err (r :: [Effect]).
(forall x.
 param
 -> (resource -> Sem (Stop err : r) x) -> Sem (Stop err : r) x)
-> (forall (r0 :: [Effect]) x.
    resource
    -> effect (Sem r0) x -> Tactical effect (Sem r0) (Stop err : r) x)
-> InterpreterFor (Scoped param effect !! err) r
interpretScopedResumableH forall x.
param -> (resource -> Sem (Stop err : r) x) -> Sem (Stop err : r) x
withResource \ resource
r effect (Sem r0) x
e -> Sem (Stop err : r) x
-> Sem (WithTactics effect f (Sem r0) (Stop err : r)) (f x)
forall (m :: * -> *) (f :: * -> *) (r :: [Effect]) (e :: Effect) a.
Functor f =>
Sem r a -> Sem (WithTactics e f m r) (f a)
liftT (resource -> effect (Sem r0) x -> Sem (Stop err : r) x
forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Sem (Stop err : r) x
scopedHandler resource
r effect (Sem r0) x
e)

-- |Combined interpreter for 'Scoped' and 'Resumable'.
-- This allows 'Stop' to be sent from within the resource allocator so that the consumer receives it, terminating the
-- entire scope.
-- In this variant, the resource allocator is a plain action.
interpretScopedResumable_ ::
  ∀ param resource effect err r .
  (param -> Sem (Stop err : r) resource) ->
  (∀ r0 x . resource -> effect (Sem r0) x -> Sem (Stop err : r) x) ->
  InterpreterFor (Scoped param effect !! err) r
interpretScopedResumable_ :: forall param resource (effect :: Effect) err (r :: [Effect]).
(param -> Sem (Stop err : r) resource)
-> (forall (r0 :: [Effect]) x.
    resource -> effect (Sem r0) x -> Sem (Stop err : r) x)
-> InterpreterFor (Scoped param effect !! err) r
interpretScopedResumable_ param -> Sem (Stop err : r) resource
resource =
  (forall x.
 param
 -> (resource -> Sem (Stop err : r) x) -> Sem (Stop err : r) x)
-> (forall (r0 :: [Effect]) x.
    resource -> effect (Sem r0) x -> Sem (Stop err : r) x)
-> InterpreterFor (Scoped param effect !! err) r
forall param resource (effect :: Effect) err (r :: [Effect]).
(forall x.
 param
 -> (resource -> Sem (Stop err : r) x) -> Sem (Stop err : r) x)
-> (forall (r0 :: [Effect]) x.
    resource -> effect (Sem r0) x -> Sem (Stop err : r) x)
-> InterpreterFor (Scoped param effect !! err) r
interpretScopedResumable \ param
p resource -> Sem (Stop err : r) x
use -> resource -> Sem (Stop err : r) x
use (resource -> Sem (Stop err : r) x)
-> Sem (Stop err : r) resource -> Sem (Stop err : r) x
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< param -> Sem (Stop err : r) resource
resource param
p

-- |Combined higher-order interpreter for 'Scoped' and 'Resumable' that allows the handler to use additional effects
-- that are interpreted by the resource allocator.
-- This allows 'Stop' to be sent from within the resource allocator so that the consumer receives it, terminating the
-- entire scope.
interpretScopedResumableWithH ::
  ∀ extra param resource effect err r r1 extraerr .
  extraerr ~ (extra ++ '[Stop err]) =>
  r1 ~ (extraerr ++ r) =>
  KnownList (extra ++ '[Stop err]) =>
  (∀ x . param -> (resource -> Sem r1 x) -> Sem (Stop err : r) x) ->
  (∀ r0 x . resource -> effect (Sem r0) x -> Tactical effect (Sem r0) r1 x) ->
  InterpreterFor (Scoped param effect !! err) r
interpretScopedResumableWithH :: forall (extra :: [Effect]) param resource (effect :: Effect) err
       (r :: [Effect]) (r1 :: [Effect]) (extraerr :: [Effect]).
(extraerr ~ (extra ++ '[Stop err]), r1 ~ (extraerr ++ r),
 KnownList (extra ++ '[Stop err])) =>
(forall x. param -> (resource -> Sem r1 x) -> Sem (Stop err : r) x)
-> (forall (r0 :: [Effect]) x.
    resource -> effect (Sem r0) x -> Tactical effect (Sem r0) r1 x)
-> InterpreterFor (Scoped param effect !! err) r
interpretScopedResumableWithH forall x. param -> (resource -> Sem r1 x) -> Sem (Stop err : r) x
withResource forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Tactical effect (Sem r0) r1 x
scopedHandler =
  (forall x.
 Weaving
   (Scoped param effect !! err)
   (Sem ((Scoped param effect !! err) : r))
   x
 -> Sem r x)
-> InterpreterFor (Scoped param effect !! err) r
forall (e :: Effect) (r :: [Effect]).
(forall x. Weaving e (Sem (e : r)) x -> Sem r x)
-> InterpreterFor e r
interpretWeaving \case
    Weaving (Resumable (Weaving (InScope param
param Sem rInitial a
main) f ()
s' forall x. f (Sem rInitial x) -> Sem r (f x)
wv' f a -> a1
ex' forall x. f x -> Maybe x
_)) f ()
s forall x.
f (Sem rInitial x) -> Sem ((Scoped param effect !! err) : r) (f x)
wv f a -> x
ex forall x. f x -> Maybe x
_ -> do
      f ()
-> (f (Either err a1) -> x)
-> (f a -> a1)
-> Sem r (Either err (f (f a)))
-> Sem r x
forall {k} (f :: * -> *) err a x (f' :: k -> *) (a' :: k)
       (r :: [Effect]).
Functor f =>
f ()
-> (f (Either err a) -> x)
-> (f' a' -> a)
-> Sem r (Either err (f (f' a')))
-> Sem r x
exResumable f ()
s f a -> x
f (Either err a1) -> x
ex f a -> a1
ex' (Sem r (Either err (f (f a))) -> Sem r x)
-> Sem r (Either err (f (f a))) -> Sem r x
forall a b. (a -> b) -> a -> b
$ Sem (Stop err : r) (f (f a)) -> Sem r (Either err (f (f a)))
forall e (r :: [Effect]) a.
Sem (Stop e : r) a -> Sem r (Either e a)
runStop (Sem (Stop err : r) (f (f a)) -> Sem r (Either err (f (f a))))
-> Sem (Stop err : r) (f (f a)) -> Sem r (Either err (f (f a)))
forall a b. (a -> b) -> a -> b
$ param
-> (resource -> Sem r1 (f (f a))) -> Sem (Stop err : r) (f (f a))
forall x. param -> (resource -> Sem r1 x) -> Sem (Stop err : r) x
withResource param
param \ resource
resource ->
        (forall (rInitial :: [Effect]) x.
 effect (Sem rInitial) x -> Tactical effect (Sem rInitial) r1 x)
-> Sem (effect : r1) (f (f a)) -> Sem r1 (f (f a))
forall (e :: Effect) (r :: [Effect]) a.
(forall (rInitial :: [Effect]) x.
 e (Sem rInitial) x -> Tactical e (Sem rInitial) r x)
-> Sem (e : r) a -> Sem r a
interpretH (resource
-> effect (Sem rInitial) x -> Tactical effect (Sem rInitial) r1 x
forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Tactical effect (Sem r0) r1 x
scopedHandler resource
resource) (Sem (effect : r1) (f (f a)) -> Sem r1 (f (f a)))
-> Sem (effect : r1) (f (f a)) -> Sem r1 (f (f a))
forall a b. (a -> b) -> a -> b
$ Sem ((Scoped param effect !! err) : effect : r1) (f (f a))
-> Sem (effect : r1) (f (f a))
InterpreterFor (Scoped param effect !! err) (effect : r1)
inScope (Sem ((Scoped param effect !! err) : effect : r1) (f (f a))
 -> Sem (effect : r1) (f (f a)))
-> Sem ((Scoped param effect !! err) : effect : r1) (f (f a))
-> Sem (effect : r1) (f (f a))
forall a b. (a -> b) -> a -> b
$
          (forall (e :: Effect).
 ElemOf e ((Scoped param effect !! err) : r)
 -> ElemOf e ((Scoped param effect !! err) : effect : r1))
-> Sem ((Scoped param effect !! err) : r) (f (f a))
-> Sem ((Scoped param effect !! err) : effect : r1) (f (f a))
forall (r :: [Effect]) (r' :: [Effect]) a.
(forall (e :: Effect). ElemOf e r -> ElemOf e r')
-> Sem r a -> Sem r' a
restack
            (SList '[Scoped param effect !! err]
-> SList (effect : extraerr)
-> ElemOf e (Append '[Scoped param effect !! err] r)
-> ElemOf
     e
     (Append
        '[Scoped param effect !! err] (Append (effect : extraerr) r))
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
             (forall (l :: [Effect]). KnownList l => SList l
forall {a} (l :: [a]). KnownList l => SList l
singList @'[Scoped param effect !! err])
             (forall (l :: [Effect]). KnownList l => SList l
forall {a} (l :: [a]). KnownList l => SList l
singList @(effect : extraerr))) (Sem ((Scoped param effect !! err) : r) (f (f a))
 -> Sem ((Scoped param effect !! err) : effect : r1) (f (f a)))
-> Sem ((Scoped param effect !! err) : r) (f (f a))
-> Sem ((Scoped param effect !! err) : effect : r1) (f (f a))
forall a b. (a -> b) -> a -> b
$ f (Sem rInitial (f a))
-> Sem ((Scoped param effect !! err) : r) (f (f a))
forall x.
f (Sem rInitial x) -> Sem ((Scoped param effect !! err) : r) (f x)
wv (f (Sem rInitial a) -> Sem r (f a)
forall x. f (Sem rInitial x) -> Sem r (f x)
wv' (Sem rInitial a
main Sem rInitial a -> f () -> f (Sem rInitial a)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s') Sem r (f a) -> f () -> f (Sem r (f a))
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s)
    Weaving
  (Scoped param effect !! err)
  (Sem ((Scoped param effect !! err) : r))
  x
_ ->
      [Char] -> Sem r x
forall a. [Char] -> a
errorWithoutStackTrace [Char]
"top level Run"
  where
    inScope :: InterpreterFor (Scoped param effect !! err) (effect : r1)
    inScope :: InterpreterFor (Scoped param effect !! err) (effect : r1)
inScope =
      (forall x.
 Weaving
   (Scoped param effect !! err)
   (Sem ((Scoped param effect !! err) : effect : r1))
   x
 -> Sem (effect : r1) x)
-> InterpreterFor (Scoped param effect !! err) (effect : r1)
forall (e :: Effect) (r :: [Effect]).
(forall x. Weaving e (Sem (e : r)) x -> Sem r x)
-> InterpreterFor e r
interpretWeaving \ (Weaving (Resumable (Weaving Scoped param effect (Sem rInitial) a
effect f ()
s' forall x. f (Sem rInitial x) -> Sem r (f x)
wv' f a -> a1
ex' forall x. f x -> Maybe x
ins')) f ()
s forall x.
f (Sem rInitial x)
-> Sem ((Scoped param effect !! err) : effect : r1) (f x)
wv f a -> x
ex forall x. f x -> Maybe x
ins) -> case Scoped param effect (Sem rInitial) a
effect of
        InScope param
param Sem rInitial a
main ->
          (forall (e :: Effect). ElemOf e r -> ElemOf e (effect : r1))
-> Sem r x -> Sem (effect : r1) x
forall (r :: [Effect]) (r' :: [Effect]) a.
(forall (e :: Effect). ElemOf e r -> ElemOf e r')
-> Sem r a -> Sem r' a
restack
            (SList (effect : extraerr)
-> ElemOf e r -> ElemOf e (Append (effect : extraerr) r)
forall {a} (l :: [a]) (r :: [a]) (e :: a).
SList l -> ElemOf e r -> ElemOf e (Append l r)
extendMembershipLeft (forall (l :: [Effect]). KnownList l => SList l
forall {a} (l :: [a]). KnownList l => SList l
singList @(effect : extraerr))) (Sem r x -> Sem (effect : r1) x) -> Sem r x -> Sem (effect : r1) x
forall a b. (a -> b) -> a -> b
$
            f ()
-> (f (Either err a1) -> x)
-> (f a -> a1)
-> Sem r (Either err (f (f a)))
-> Sem r x
forall {k} (f :: * -> *) err a x (f' :: k -> *) (a' :: k)
       (r :: [Effect]).
Functor f =>
f ()
-> (f (Either err a) -> x)
-> (f' a' -> a)
-> Sem r (Either err (f (f' a')))
-> Sem r x
exResumable f ()
s f a -> x
f (Either err a1) -> x
ex f a -> a1
ex' (Sem r (Either err (f (f a))) -> Sem r x)
-> Sem r (Either err (f (f a))) -> Sem r x
forall a b. (a -> b) -> a -> b
$ Sem (Stop err : r) (f (f a)) -> Sem r (Either err (f (f a)))
forall e (r :: [Effect]) a.
Sem (Stop e : r) a -> Sem r (Either e a)
runStop (Sem (Stop err : r) (f (f a)) -> Sem r (Either err (f (f a))))
-> Sem (Stop err : r) (f (f a)) -> Sem r (Either err (f (f a)))
forall a b. (a -> b) -> a -> b
$ param
-> (resource -> Sem r1 (f (f a))) -> Sem (Stop err : r) (f (f a))
forall x. param -> (resource -> Sem r1 x) -> Sem (Stop err : r) x
withResource param
param \ resource
resource ->
              (forall (rInitial :: [Effect]) x.
 effect (Sem rInitial) x -> Tactical effect (Sem rInitial) r1 x)
-> Sem (effect : r1) (f (f a)) -> Sem r1 (f (f a))
forall (e :: Effect) (r :: [Effect]) a.
(forall (rInitial :: [Effect]) x.
 e (Sem rInitial) x -> Tactical e (Sem rInitial) r x)
-> Sem (e : r) a -> Sem r a
interpretH (resource
-> effect (Sem rInitial) x -> Tactical effect (Sem rInitial) r1 x
forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Tactical effect (Sem r0) r1 x
scopedHandler resource
resource) (Sem ((Scoped param effect !! err) : effect : r1) (f (f a))
-> Sem (effect : r1) (f (f a))
InterpreterFor (Scoped param effect !! err) (effect : r1)
inScope (Sem ((Scoped param effect !! err) : effect : r1) (f (f a))
 -> Sem (effect : r1) (f (f a)))
-> Sem ((Scoped param effect !! err) : effect : r1) (f (f a))
-> Sem (effect : r1) (f (f a))
forall a b. (a -> b) -> a -> b
$ f (Sem rInitial (f a))
-> Sem ((Scoped param effect !! err) : effect : r1) (f (f a))
forall x.
f (Sem rInitial x)
-> Sem ((Scoped param effect !! err) : effect : r1) (f x)
wv (f (Sem rInitial a) -> Sem r (f a)
forall x. f (Sem rInitial x) -> Sem r (f x)
wv' (Sem rInitial a
main Sem rInitial a -> f () -> f (Sem rInitial a)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s') Sem r (f a) -> f () -> f (Sem r (f a))
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s))
        Run effect (Sem rInitial) a
act ->
          f a -> x
ex (f a -> x) -> (f a1 -> f a) -> f a1 -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a1 -> Either err a1) -> f a1 -> f (Either err a1)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a1 -> Either err a1
forall a b. b -> Either a b
Right (f a1 -> x) -> Sem (effect : r1) (f a1) -> Sem (effect : r1) x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Union (effect : r1) (Sem (effect : r1)) (f a1)
-> Sem (effect : r1) (f a1)
forall (r :: [Effect]) a. Union r (Sem r) a -> Sem r a
liftSem (f ()
-> (forall x. f (Sem rInitial x) -> Sem (effect : r1) (f x))
-> (forall x. f x -> Maybe x)
-> Union (effect : r1) (Sem rInitial) a1
-> Union (effect : r1) (Sem (effect : r1)) (f a1)
forall (s :: * -> *) (n :: * -> *) (m :: * -> *) (r :: [Effect]) a.
(Functor s, Functor n) =>
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 f ()
s (Sem ((Scoped param effect !! err) : effect : r1) (f x)
-> Sem (effect : r1) (f x)
InterpreterFor (Scoped param effect !! err) (effect : r1)
inScope (Sem ((Scoped param effect !! err) : effect : r1) (f x)
 -> Sem (effect : r1) (f x))
-> (f (Sem rInitial x)
    -> Sem ((Scoped param effect !! err) : effect : r1) (f x))
-> f (Sem rInitial x)
-> Sem (effect : r1) (f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Sem rInitial x)
-> Sem ((Scoped param effect !! err) : effect : r1) (f x)
forall x.
f (Sem rInitial x)
-> Sem ((Scoped param effect !! err) : effect : r1) (f x)
wv) forall x. f x -> Maybe x
ins (Weaving effect (Sem rInitial) a1
-> Union (effect : r1) (Sem rInitial) a1
forall (e :: Effect) (r :: [Effect]) (m :: * -> *) a.
Member e r =>
Weaving e m a -> Union r m a
injWeaving (effect (Sem rInitial) a
-> f ()
-> (forall x. f (Sem rInitial x) -> Sem rInitial (f x))
-> (f a -> a1)
-> (forall x. f x -> Maybe x)
-> Weaving effect (Sem rInitial) a1
forall (f :: * -> *) (e :: Effect) (rInitial :: [Effect]) 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 effect (Sem rInitial) a
act f ()
s' forall x. f (Sem rInitial x) -> Sem rInitial (f x)
forall x. f (Sem rInitial x) -> Sem r (f x)
wv' f a -> a1
ex' forall x. f x -> Maybe x
ins')))

-- |Combined interpreter for 'Scoped' and 'Resumable' that allows the handler to use additional effects that are
-- interpreted by the resource allocator.
-- This allows 'Stop' to be sent from within the resource allocator so that the consumer receives it, terminating the
-- entire scope.
interpretScopedResumableWith ::
  ∀ extra param resource effect err r r1 .
  r1 ~ ((extra ++ '[Stop err]) ++ r) =>
  KnownList (extra ++ '[Stop err]) =>
  (∀ x . param -> (resource -> Sem r1 x) -> Sem (Stop err : r) x) ->
  (∀ r0 x . resource -> effect (Sem r0) x -> Sem r1 x) ->
  InterpreterFor (Scoped param effect !! err) r
interpretScopedResumableWith :: forall (extra :: [Effect]) param resource (effect :: Effect) err
       (r :: [Effect]) (r1 :: [Effect]).
(r1 ~ ((extra ++ '[Stop err]) ++ r),
 KnownList (extra ++ '[Stop err])) =>
(forall x. param -> (resource -> Sem r1 x) -> Sem (Stop err : r) x)
-> (forall (r0 :: [Effect]) x.
    resource -> effect (Sem r0) x -> Sem r1 x)
-> InterpreterFor (Scoped param effect !! err) r
interpretScopedResumableWith forall x. param -> (resource -> Sem r1 x) -> Sem (Stop err : r) x
withResource forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Sem r1 x
scopedHandler =
  forall (extra :: [Effect]) param resource (effect :: Effect) err
       (r :: [Effect]) (r1 :: [Effect]) (extraerr :: [Effect]).
(extraerr ~ (extra ++ '[Stop err]), r1 ~ (extraerr ++ r),
 KnownList (extra ++ '[Stop err])) =>
(forall x. param -> (resource -> Sem r1 x) -> Sem (Stop err : r) x)
-> (forall (r0 :: [Effect]) x.
    resource -> effect (Sem r0) x -> Tactical effect (Sem r0) r1 x)
-> InterpreterFor (Scoped param effect !! err) r
interpretScopedResumableWithH @extra forall x. param -> (resource -> Sem r1 x) -> Sem (Stop err : r) x
withResource \ resource
r effect (Sem r0) x
e -> Sem r1 x -> Sem (WithTactics effect f (Sem r0) r1) (f x)
forall (m :: * -> *) (f :: * -> *) (r :: [Effect]) (e :: Effect) a.
Functor f =>
Sem r a -> Sem (WithTactics e f m r) (f a)
liftT (resource -> effect (Sem r0) x -> Sem r1 x
forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Sem r1 x
scopedHandler resource
r effect (Sem r0) x
e)

-- |Combined interpreter for 'Scoped' and 'Resumable' that allows the handler to use additional effects that are
-- interpreted by the resource allocator.
-- This allows 'Stop' to be sent from within the resource allocator so that the consumer receives it, terminating the
-- entire scope.
-- In this variant, no resource is used and the allocator is a plain interpreter.
interpretScopedResumableWith_ ::
  ∀ extra param effect err r r1 .
  r1 ~ ((extra ++ '[Stop err]) ++ r) =>
  KnownList (extra ++ '[Stop err]) =>
  (∀ x . param -> Sem r1 x -> Sem (Stop err : r) x) ->
  (∀ r0 x . effect (Sem r0) x -> Sem r1 x) ->
  InterpreterFor (Scoped param effect !! err) r
interpretScopedResumableWith_ :: forall (extra :: [Effect]) param (effect :: Effect) err
       (r :: [Effect]) (r1 :: [Effect]).
(r1 ~ ((extra ++ '[Stop err]) ++ r),
 KnownList (extra ++ '[Stop err])) =>
(forall x. param -> Sem r1 x -> Sem (Stop err : r) x)
-> (forall (r0 :: [Effect]) x. effect (Sem r0) x -> Sem r1 x)
-> InterpreterFor (Scoped param effect !! err) r
interpretScopedResumableWith_ forall x. param -> Sem r1 x -> Sem (Stop err : r) x
extra forall (r0 :: [Effect]) x. effect (Sem r0) x -> Sem r1 x
scopedHandler =
  forall (extra :: [Effect]) param resource (effect :: Effect) err
       (r :: [Effect]) (r1 :: [Effect]).
(r1 ~ ((extra ++ '[Stop err]) ++ r),
 KnownList (extra ++ '[Stop err])) =>
(forall x. param -> (resource -> Sem r1 x) -> Sem (Stop err : r) x)
-> (forall (r0 :: [Effect]) x.
    resource -> effect (Sem r0) x -> Sem r1 x)
-> InterpreterFor (Scoped param effect !! err) r
interpretScopedResumableWith @extra (\ param
p () -> Sem r1 x
f -> param -> Sem r1 x -> Sem (Stop err : r) x
forall x. param -> Sem r1 x -> Sem (Stop err : r) x
extra param
p (() -> Sem r1 x
f ())) ((effect (Sem r0) x -> Sem r1 x)
-> () -> effect (Sem r0) x -> Sem r1 x
forall a b. a -> b -> a
const effect (Sem r0) x -> Sem r1 x
forall (r0 :: [Effect]) x. effect (Sem r0) x -> Sem r1 x
scopedHandler)

-- |Combined higher-order interpreter for 'Resumable' and 'Scoped'.
-- In this variant, only the handler may send 'Stop', but this allows resumption to happen on each action inside of the
-- scope.
interpretResumableScopedH ::
  ∀ param resource effect err r .
  (∀ x . param -> (resource -> Sem r x) -> Sem r x) ->
  (∀ r0 x . resource -> effect (Sem r0) x -> Tactical (effect !! err) (Sem r0) (Stop err : r) x) ->
  InterpreterFor (Scoped param (effect !! err)) r
interpretResumableScopedH :: forall param resource (effect :: Effect) err (r :: [Effect]).
(forall x. param -> (resource -> Sem r x) -> Sem r x)
-> (forall (r0 :: [Effect]) x.
    resource
    -> effect (Sem r0) x
    -> Tactical (effect !! err) (Sem r0) (Stop err : r) x)
-> InterpreterFor (Scoped param (effect !! err)) r
interpretResumableScopedH forall x. param -> (resource -> Sem r x) -> Sem r x
withResource forall (r0 :: [Effect]) x.
resource
-> effect (Sem r0) x
-> Tactical (effect !! err) (Sem r0) (Stop err : r) x
scopedHandler =
  (forall x.
 Weaving
   (Scoped param (effect !! err))
   (Sem (Scoped param (effect !! err) : r))
   x
 -> Sem r x)
-> Sem (Scoped param (effect !! err) : r) a -> Sem r a
forall (e :: Effect) (r :: [Effect]).
(forall x. Weaving e (Sem (e : r)) x -> Sem r x)
-> InterpreterFor e r
interpretWeaving ((forall x.
  Weaving
    (Scoped param (effect !! err))
    (Sem (Scoped param (effect !! err) : r))
    x
  -> Sem r x)
 -> Sem (Scoped param (effect !! err) : r) a -> Sem r a)
-> (forall x.
    Weaving
      (Scoped param (effect !! err))
      (Sem (Scoped param (effect !! err) : r))
      x
    -> Sem r x)
-> Sem (Scoped param (effect !! err) : r) a
-> Sem r a
forall a b. (a -> b) -> a -> b
$ \(Weaving Scoped param (effect !! err) (Sem rInitial) a
effect f ()
s forall x.
f (Sem rInitial x) -> Sem (Scoped param (effect !! err) : r) (f x)
wv f a -> x
ex forall x. f x -> Maybe x
_) -> case Scoped param (effect !! err) (Sem rInitial) a
effect of
    Run (!!) effect err (Sem rInitial) a
_ -> [Char] -> Sem r x
forall a. [Char] -> a
errorWithoutStackTrace [Char]
"top level run"
    InScope param
param Sem rInitial a
main -> param -> (resource -> Sem r x) -> Sem r x
forall x. param -> (resource -> Sem r x) -> Sem r x
withResource param
param \ resource
resource ->
      f a -> x
ex (f a -> x) -> Sem r (f a) -> Sem r x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall x (r0 :: [Effect]).
 effect (Sem r0) x
 -> Tactical (effect !! err) (Sem r0) (Stop err : r) x)
-> InterpreterFor (effect !! err) r
forall err (eff :: Effect) (r :: [Effect]).
(forall x (r0 :: [Effect]).
 eff (Sem r0) x
 -> Tactical (Resumable err eff) (Sem r0) (Stop err : r) x)
-> InterpreterFor (Resumable err eff) r
interpretResumableH (resource
-> effect (Sem r0) x
-> Tactical (effect !! err) (Sem r0) (Stop err : r) x
forall (r0 :: [Effect]) x.
resource
-> effect (Sem r0) x
-> Tactical (effect !! err) (Sem r0) (Stop err : r) x
scopedHandler resource
resource) (Sem (Scoped param (effect !! err) : (effect !! err) : r) (f a)
-> Sem ((effect !! err) : r) (f a)
InterpreterFor (Scoped param (effect !! err)) ((effect !! err) : r)
inScope (Sem (Scoped param (effect !! err) : (effect !! err) : r) (f a)
 -> Sem ((effect !! err) : r) (f a))
-> Sem (Scoped param (effect !! err) : (effect !! err) : r) (f a)
-> Sem ((effect !! err) : r) (f a)
forall a b. (a -> b) -> a -> b
$ Sem (Scoped param (effect !! err) : r) (f a)
-> Sem (Scoped param (effect !! err) : (effect !! err) : r) (f a)
forall (e2 :: Effect) (e1 :: Effect) (r :: [Effect]) a.
Sem (e1 : r) a -> Sem (e1 : e2 : r) a
raiseUnder (Sem (Scoped param (effect !! err) : r) (f a)
 -> Sem (Scoped param (effect !! err) : (effect !! err) : r) (f a))
-> Sem (Scoped param (effect !! err) : r) (f a)
-> Sem (Scoped param (effect !! err) : (effect !! err) : r) (f a)
forall a b. (a -> b) -> a -> b
$ f (Sem rInitial a) -> Sem (Scoped param (effect !! err) : r) (f a)
forall x.
f (Sem rInitial x) -> Sem (Scoped param (effect !! err) : r) (f x)
wv (Sem rInitial a
main Sem rInitial a -> f () -> f (Sem rInitial a)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s))
  where
    inScope :: InterpreterFor (Scoped param (effect !! err)) (effect !! err : r)
    inScope :: InterpreterFor (Scoped param (effect !! err)) ((effect !! err) : r)
inScope =
      (forall x.
 Weaving
   (Scoped param (effect !! err))
   (Sem (Scoped param (effect !! err) : (effect !! err) : r))
   x
 -> Sem ((effect !! err) : r) x)
-> InterpreterFor
     (Scoped param (effect !! err)) ((effect !! err) : r)
forall (e :: Effect) (r :: [Effect]).
(forall x. Weaving e (Sem (e : r)) x -> Sem r x)
-> InterpreterFor e r
interpretWeaving \ (Weaving Scoped param (effect !! err) (Sem rInitial) a
effect f ()
s forall x.
f (Sem rInitial x)
-> Sem (Scoped param (effect !! err) : (effect !! err) : r) (f x)
wv f a -> x
ex forall x. f x -> Maybe x
ins) -> case Scoped param (effect !! err) (Sem rInitial) a
effect of
        Run (!!) effect err (Sem rInitial) a
act -> Union ((effect !! err) : r) (Sem ((effect !! err) : r)) x
-> Sem ((effect !! err) : r) x
forall (r :: [Effect]) a. Union r (Sem r) a -> Sem r a
liftSem (Union ((effect !! err) : r) (Sem ((effect !! err) : r)) x
 -> Sem ((effect !! err) : r) x)
-> Union ((effect !! err) : r) (Sem ((effect !! err) : r)) x
-> Sem ((effect !! err) : r) x
forall a b. (a -> b) -> a -> b
$ Weaving (effect !! err) (Sem ((effect !! err) : r)) x
-> Union ((effect !! err) : r) (Sem ((effect !! err) : r)) x
forall (e :: Effect) (r :: [Effect]) (m :: * -> *) a.
Member e r =>
Weaving e m a -> Union r m a
injWeaving (Weaving (effect !! err) (Sem ((effect !! err) : r)) x
 -> Union ((effect !! err) : r) (Sem ((effect !! err) : r)) x)
-> Weaving (effect !! err) (Sem ((effect !! err) : r)) x
-> Union ((effect !! err) : r) (Sem ((effect !! err) : r)) x
forall a b. (a -> b) -> a -> b
$ (!!) effect err (Sem rInitial) a
-> f ()
-> (forall x.
    f (Sem rInitial x) -> Sem ((effect !! err) : r) (f x))
-> (f a -> x)
-> (forall x. f x -> Maybe x)
-> Weaving (effect !! err) (Sem ((effect !! err) : r)) x
forall (f :: * -> *) (e :: Effect) (rInitial :: [Effect]) 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 (!!) effect err (Sem rInitial) a
act f ()
s (Sem (Scoped param (effect !! err) : (effect !! err) : r) (f x)
-> Sem ((effect !! err) : r) (f x)
InterpreterFor (Scoped param (effect !! err)) ((effect !! err) : r)
inScope (Sem (Scoped param (effect !! err) : (effect !! err) : r) (f x)
 -> Sem ((effect !! err) : r) (f x))
-> (f (Sem rInitial x)
    -> Sem (Scoped param (effect !! err) : (effect !! err) : r) (f x))
-> f (Sem rInitial x)
-> Sem ((effect !! err) : r) (f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Sem rInitial x)
-> Sem (Scoped param (effect !! err) : (effect !! err) : r) (f x)
forall x.
f (Sem rInitial x)
-> Sem (Scoped param (effect !! err) : (effect !! err) : r) (f x)
wv) f a -> x
ex forall x. f x -> Maybe x
ins
        InScope param
param Sem rInitial a
main -> Sem r x -> Sem ((effect !! err) : r) x
forall (e :: Effect) (r :: [Effect]) a. Sem r a -> Sem (e : r) a
raise (Sem r x -> Sem ((effect !! err) : r) x)
-> Sem r x -> Sem ((effect !! err) : r) x
forall a b. (a -> b) -> a -> b
$ param -> (resource -> Sem r x) -> Sem r x
forall x. param -> (resource -> Sem r x) -> Sem r x
withResource param
param \ resource
resource ->
          f a -> x
ex (f a -> x) -> Sem r (f a) -> Sem r x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall x (r0 :: [Effect]).
 effect (Sem r0) x
 -> Tactical (effect !! err) (Sem r0) (Stop err : r) x)
-> InterpreterFor (effect !! err) r
forall err (eff :: Effect) (r :: [Effect]).
(forall x (r0 :: [Effect]).
 eff (Sem r0) x
 -> Tactical (Resumable err eff) (Sem r0) (Stop err : r) x)
-> InterpreterFor (Resumable err eff) r
interpretResumableH (resource
-> effect (Sem r0) x
-> Tactical (effect !! err) (Sem r0) (Stop err : r) x
forall (r0 :: [Effect]) x.
resource
-> effect (Sem r0) x
-> Tactical (effect !! err) (Sem r0) (Stop err : r) x
scopedHandler resource
resource) (Sem (Scoped param (effect !! err) : (effect !! err) : r) (f a)
-> Sem ((effect !! err) : r) (f a)
InterpreterFor (Scoped param (effect !! err)) ((effect !! err) : r)
inScope (Sem (Scoped param (effect !! err) : (effect !! err) : r) (f a)
 -> Sem ((effect !! err) : r) (f a))
-> Sem (Scoped param (effect !! err) : (effect !! err) : r) (f a)
-> Sem ((effect !! err) : r) (f a)
forall a b. (a -> b) -> a -> b
$ f (Sem rInitial a)
-> Sem (Scoped param (effect !! err) : (effect !! err) : r) (f a)
forall x.
f (Sem rInitial x)
-> Sem (Scoped param (effect !! err) : (effect !! err) : r) (f x)
wv (Sem rInitial a
main Sem rInitial a -> f () -> f (Sem rInitial a)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s))

-- |Combined interpreter for 'Resumable' and 'Scoped'.
-- In this variant, only the handler may send 'Stop', but this allows resumption to happen on each action inside of the
-- scope.
interpretResumableScoped ::
  ∀ param resource effect err r .
  (∀ x . param -> (resource -> Sem r x) -> Sem r x) ->
  (∀ r0 x . resource -> effect (Sem r0) x -> Sem (Stop err : r) x) ->
  InterpreterFor (Scoped param (effect !! err)) r
interpretResumableScoped :: forall param resource (effect :: Effect) err (r :: [Effect]).
(forall x. param -> (resource -> Sem r x) -> Sem r x)
-> (forall (r0 :: [Effect]) x.
    resource -> effect (Sem r0) x -> Sem (Stop err : r) x)
-> InterpreterFor (Scoped param (effect !! err)) r
interpretResumableScoped forall x. param -> (resource -> Sem r x) -> Sem r x
withResource forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Sem (Stop err : r) x
scopedHandler =
  (forall x. param -> (resource -> Sem r x) -> Sem r x)
-> (forall (r0 :: [Effect]) x.
    resource
    -> effect (Sem r0) x
    -> Tactical (effect !! err) (Sem r0) (Stop err : r) x)
-> InterpreterFor (Scoped param (effect !! err)) r
forall param resource (effect :: Effect) err (r :: [Effect]).
(forall x. param -> (resource -> Sem r x) -> Sem r x)
-> (forall (r0 :: [Effect]) x.
    resource
    -> effect (Sem r0) x
    -> Tactical (effect !! err) (Sem r0) (Stop err : r) x)
-> InterpreterFor (Scoped param (effect !! err)) r
interpretResumableScopedH forall x. param -> (resource -> Sem r x) -> Sem r x
withResource \ resource
r effect (Sem r0) x
e -> Sem (Stop err : r) x
-> Sem
     (WithTactics (effect !! err) f (Sem r0) (Stop err : r)) (f x)
forall (m :: * -> *) (f :: * -> *) (r :: [Effect]) (e :: Effect) a.
Functor f =>
Sem r a -> Sem (WithTactics e f m r) (f a)
liftT (resource -> effect (Sem r0) x -> Sem (Stop err : r) x
forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Sem (Stop err : r) x
scopedHandler resource
r effect (Sem r0) x
e)

-- |Combined interpreter for 'Resumable' and 'Scoped'.
-- In this variant:
-- - Only the handler may send 'Stop', but this allows resumption to happen on each action inside of the scope.
-- - The resource allocator is a plain action.
interpretResumableScoped_ ::
  ∀ param resource effect err r .
  (param -> Sem r resource) ->
  (∀ r0 x . resource -> effect (Sem r0) x -> Sem (Stop err : r) x) ->
  InterpreterFor (Scoped param (effect !! err)) r
interpretResumableScoped_ :: forall param resource (effect :: Effect) err (r :: [Effect]).
(param -> Sem r resource)
-> (forall (r0 :: [Effect]) x.
    resource -> effect (Sem r0) x -> Sem (Stop err : r) x)
-> InterpreterFor (Scoped param (effect !! err)) r
interpretResumableScoped_ param -> Sem r resource
resource =
  (forall x. param -> (resource -> Sem r x) -> Sem r x)
-> (forall (r0 :: [Effect]) x.
    resource -> effect (Sem r0) x -> Sem (Stop err : r) x)
-> InterpreterFor (Scoped param (effect !! err)) r
forall param resource (effect :: Effect) err (r :: [Effect]).
(forall x. param -> (resource -> Sem r x) -> Sem r x)
-> (forall (r0 :: [Effect]) x.
    resource -> effect (Sem r0) x -> Sem (Stop err : r) x)
-> InterpreterFor (Scoped param (effect !! err)) r
interpretResumableScoped \ param
p resource -> Sem r x
use -> resource -> Sem r x
use (resource -> Sem r x) -> Sem r resource -> Sem r x
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< param -> Sem r resource
resource param
p

-- |Combined higher-order interpreter for 'Resumable' and 'Scoped' that allows the handler to use additional effects
-- that are interpreted by the resource allocator.
-- In this variant, only the handler may send 'Stop', but this allows resumption to happen on each action inside of the
-- scope.
interpretResumableScopedWithH ::
  ∀ extra param resource effect err r r1 .
  r1 ~ (extra ++ r) =>
  KnownList extra =>
  (∀ x . param -> (resource -> Sem r1 x) -> Sem r x) ->
  (∀ r0 x . resource -> effect (Sem r0) x -> Tactical (effect !! err) (Sem r0) (Stop err : r1) x) ->
  InterpreterFor (Scoped param (effect !! err)) r
interpretResumableScopedWithH :: forall (extra :: [Effect]) param resource (effect :: Effect) err
       (r :: [Effect]) (r1 :: [Effect]).
(r1 ~ (extra ++ r), KnownList extra) =>
(forall x. param -> (resource -> Sem r1 x) -> Sem r x)
-> (forall (r0 :: [Effect]) x.
    resource
    -> effect (Sem r0) x
    -> Tactical (effect !! err) (Sem r0) (Stop err : r1) x)
-> InterpreterFor (Scoped param (effect !! err)) r
interpretResumableScopedWithH forall x. param -> (resource -> Sem r1 x) -> Sem r x
withResource forall (r0 :: [Effect]) x.
resource
-> effect (Sem r0) x
-> Tactical (effect !! err) (Sem r0) (Stop err : r1) x
scopedHandler =
  (forall x.
 Weaving
   (Scoped param (effect !! err))
   (Sem (Scoped param (effect !! err) : r))
   x
 -> Sem r x)
-> InterpreterFor (Scoped param (effect !! err)) r
forall (e :: Effect) (r :: [Effect]).
(forall x. Weaving e (Sem (e : r)) x -> Sem r x)
-> InterpreterFor e r
interpretWeaving \case
    Weaving (InScope param
param Sem rInitial a
main) f ()
s forall x.
f (Sem rInitial x) -> Sem (Scoped param (effect !! err) : r) (f x)
wv f a -> x
ex forall x. f x -> Maybe x
_ ->
      f a -> x
ex (f a -> x) -> Sem r (f a) -> Sem r x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> param -> (resource -> Sem r1 (f a)) -> Sem r (f a)
forall x. param -> (resource -> Sem r1 x) -> Sem r x
withResource param
param \ resource
resource ->
        (forall x (r0 :: [Effect]).
 effect (Sem r0) x
 -> Tactical (effect !! err) (Sem r0) (Stop err : r1) x)
-> InterpreterFor (effect !! err) r1
forall err (eff :: Effect) (r :: [Effect]).
(forall x (r0 :: [Effect]).
 eff (Sem r0) x
 -> Tactical (Resumable err eff) (Sem r0) (Stop err : r) x)
-> InterpreterFor (Resumable err eff) r
interpretResumableH (resource
-> effect (Sem r0) x
-> Tactical (effect !! err) (Sem r0) (Stop err : r1) x
forall (r0 :: [Effect]) x.
resource
-> effect (Sem r0) x
-> Tactical (effect !! err) (Sem r0) (Stop err : r1) x
scopedHandler resource
resource) (Sem ((effect !! err) : r1) (f a) -> Sem r1 (f a))
-> Sem ((effect !! err) : r1) (f a) -> Sem r1 (f a)
forall a b. (a -> b) -> a -> b
$ Sem (Scoped param (effect !! err) : (effect !! err) : r1) (f a)
-> Sem ((effect !! err) : r1) (f a)
InterpreterFor
  (Scoped param (effect !! err)) ((effect !! err) : r1)
inScope (Sem (Scoped param (effect !! err) : (effect !! err) : r1) (f a)
 -> Sem ((effect !! err) : r1) (f a))
-> Sem (Scoped param (effect !! err) : (effect !! err) : r1) (f a)
-> Sem ((effect !! err) : r1) (f a)
forall a b. (a -> b) -> a -> b
$
          (forall (e :: Effect).
 ElemOf e (Scoped param (effect !! err) : r)
 -> ElemOf e (Scoped param (effect !! err) : (effect !! err) : r1))
-> Sem (Scoped param (effect !! err) : r) (f a)
-> Sem (Scoped param (effect !! err) : (effect !! err) : r1) (f a)
forall (r :: [Effect]) (r' :: [Effect]) a.
(forall (e :: Effect). ElemOf e r -> ElemOf e r')
-> Sem r a -> Sem r' a
restack
            (SList '[Scoped param (effect !! err)]
-> SList ((effect !! err) : extra)
-> ElemOf e (Append '[Scoped param (effect !! err)] r)
-> ElemOf
     e
     (Append
        '[Scoped param (effect !! err)]
        (Append ((effect !! err) : extra) r))
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
             (forall (l :: [Effect]). KnownList l => SList l
forall {a} (l :: [a]). KnownList l => SList l
singList @'[Scoped param (effect !! err)])
             (forall (l :: [Effect]). KnownList l => SList l
forall {a} (l :: [a]). KnownList l => SList l
singList @(effect !! err : extra))) (Sem (Scoped param (effect !! err) : r) (f a)
 -> Sem (Scoped param (effect !! err) : (effect !! err) : r1) (f a))
-> Sem (Scoped param (effect !! err) : r) (f a)
-> Sem (Scoped param (effect !! err) : (effect !! err) : r1) (f a)
forall a b. (a -> b) -> a -> b
$ f (Sem rInitial a) -> Sem (Scoped param (effect !! err) : r) (f a)
forall x.
f (Sem rInitial x) -> Sem (Scoped param (effect !! err) : r) (f x)
wv (Sem rInitial a
main Sem rInitial a -> f () -> f (Sem rInitial a)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s)
    Weaving
  (Scoped param (effect !! err))
  (Sem (Scoped param (effect !! err) : r))
  x
_ ->
      [Char] -> Sem r x
forall a. [Char] -> a
errorWithoutStackTrace [Char]
"top level Run"
  where
    inScope :: InterpreterFor (Scoped param (effect !! err)) (effect !! err : r1)
    inScope :: InterpreterFor
  (Scoped param (effect !! err)) ((effect !! err) : r1)
inScope =
      (forall x.
 Weaving
   (Scoped param (effect !! err))
   (Sem (Scoped param (effect !! err) : (effect !! err) : r1))
   x
 -> Sem ((effect !! err) : r1) x)
-> InterpreterFor
     (Scoped param (effect !! err)) ((effect !! err) : r1)
forall (e :: Effect) (r :: [Effect]).
(forall x. Weaving e (Sem (e : r)) x -> Sem r x)
-> InterpreterFor e r
interpretWeaving \case
        Weaving (InScope param
param Sem rInitial a
main) f ()
s forall x.
f (Sem rInitial x)
-> Sem (Scoped param (effect !! err) : (effect !! err) : r1) (f x)
wv f a -> x
ex forall x. f x -> Maybe x
_ ->
          (forall (e :: Effect).
 ElemOf e r -> ElemOf e ((effect !! err) : r1))
-> Sem r x -> Sem ((effect !! err) : r1) x
forall (r :: [Effect]) (r' :: [Effect]) a.
(forall (e :: Effect). ElemOf e r -> ElemOf e r')
-> Sem r a -> Sem r' a
restack
            (SList ((effect !! err) : extra)
-> ElemOf e r -> ElemOf e (Append ((effect !! err) : extra) r)
forall {a} (l :: [a]) (r :: [a]) (e :: a).
SList l -> ElemOf e r -> ElemOf e (Append l r)
extendMembershipLeft (forall (l :: [Effect]). KnownList l => SList l
forall {a} (l :: [a]). KnownList l => SList l
singList @(effect !! err : extra)))
            (f a -> x
ex (f a -> x) -> Sem r (f a) -> Sem r x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> param -> (resource -> Sem r1 (f a)) -> Sem r (f a)
forall x. param -> (resource -> Sem r1 x) -> Sem r x
withResource param
param \resource
resource ->
                (forall x (r0 :: [Effect]).
 effect (Sem r0) x
 -> Tactical (effect !! err) (Sem r0) (Stop err : r1) x)
-> InterpreterFor (effect !! err) r1
forall err (eff :: Effect) (r :: [Effect]).
(forall x (r0 :: [Effect]).
 eff (Sem r0) x
 -> Tactical (Resumable err eff) (Sem r0) (Stop err : r) x)
-> InterpreterFor (Resumable err eff) r
interpretResumableH (resource
-> effect (Sem r0) x
-> Tactical (effect !! err) (Sem r0) (Stop err : r1) x
forall (r0 :: [Effect]) x.
resource
-> effect (Sem r0) x
-> Tactical (effect !! err) (Sem r0) (Stop err : r1) x
scopedHandler resource
resource) (Sem ((effect !! err) : r1) (f a) -> Sem r1 (f a))
-> Sem ((effect !! err) : r1) (f a) -> Sem r1 (f a)
forall a b. (a -> b) -> a -> b
$ Sem (Scoped param (effect !! err) : (effect !! err) : r1) (f a)
-> Sem ((effect !! err) : r1) (f a)
InterpreterFor
  (Scoped param (effect !! err)) ((effect !! err) : r1)
inScope (Sem (Scoped param (effect !! err) : (effect !! err) : r1) (f a)
 -> Sem ((effect !! err) : r1) (f a))
-> Sem (Scoped param (effect !! err) : (effect !! err) : r1) (f a)
-> Sem ((effect !! err) : r1) (f a)
forall a b. (a -> b) -> a -> b
$ f (Sem rInitial a)
-> Sem (Scoped param (effect !! err) : (effect !! err) : r1) (f a)
forall x.
f (Sem rInitial x)
-> Sem (Scoped param (effect !! err) : (effect !! err) : r1) (f x)
wv (Sem rInitial a
main Sem rInitial a -> f () -> f (Sem rInitial a)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s))
        Weaving (Run (!!) effect err (Sem rInitial) a
act) f ()
s forall x.
f (Sem rInitial x)
-> Sem (Scoped param (effect !! err) : (effect !! err) : r1) (f x)
wv f a -> x
ex forall x. f x -> Maybe x
ins ->
          Union ((effect !! err) : r1) (Sem ((effect !! err) : r1)) x
-> Sem ((effect !! err) : r1) x
forall (r :: [Effect]) a. Union r (Sem r) a -> Sem r a
liftSem (Union ((effect !! err) : r1) (Sem ((effect !! err) : r1)) x
 -> Sem ((effect !! err) : r1) x)
-> Union ((effect !! err) : r1) (Sem ((effect !! err) : r1)) x
-> Sem ((effect !! err) : r1) x
forall a b. (a -> b) -> a -> b
$ Weaving (effect !! err) (Sem ((effect !! err) : r1)) x
-> Union ((effect !! err) : r1) (Sem ((effect !! err) : r1)) x
forall (e :: Effect) (r :: [Effect]) (m :: * -> *) a.
Member e r =>
Weaving e m a -> Union r m a
injWeaving (Weaving (effect !! err) (Sem ((effect !! err) : r1)) x
 -> Union ((effect !! err) : r1) (Sem ((effect !! err) : r1)) x)
-> Weaving (effect !! err) (Sem ((effect !! err) : r1)) x
-> Union ((effect !! err) : r1) (Sem ((effect !! err) : r1)) x
forall a b. (a -> b) -> a -> b
$ (!!) effect err (Sem rInitial) a
-> f ()
-> (forall x.
    f (Sem rInitial x) -> Sem ((effect !! err) : r1) (f x))
-> (f a -> x)
-> (forall x. f x -> Maybe x)
-> Weaving (effect !! err) (Sem ((effect !! err) : r1)) x
forall (f :: * -> *) (e :: Effect) (rInitial :: [Effect]) 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 (!!) effect err (Sem rInitial) a
act f ()
s (Sem (Scoped param (effect !! err) : (effect !! err) : r1) (f x)
-> Sem ((effect !! err) : r1) (f x)
InterpreterFor
  (Scoped param (effect !! err)) ((effect !! err) : r1)
inScope (Sem (Scoped param (effect !! err) : (effect !! err) : r1) (f x)
 -> Sem ((effect !! err) : r1) (f x))
-> (f (Sem rInitial x)
    -> Sem (Scoped param (effect !! err) : (effect !! err) : r1) (f x))
-> f (Sem rInitial x)
-> Sem ((effect !! err) : r1) (f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Sem rInitial x)
-> Sem (Scoped param (effect !! err) : (effect !! err) : r1) (f x)
forall x.
f (Sem rInitial x)
-> Sem (Scoped param (effect !! err) : (effect !! err) : r1) (f x)
wv) f a -> x
ex forall x. f x -> Maybe x
ins

-- |Combined interpreter for 'Resumable' and 'Scoped' that allows the handler to use additional effects that are
-- interpreted by the resource allocator.
-- In this variant, only the handler may send 'Stop', but this allows resumption to happen on each action inside of the
-- scope.
interpretResumableScopedWith ::
  ∀ extra param resource effect err r r1 .
  r1 ~ (extra ++ r) =>
  KnownList extra =>
  (∀ x . param -> (resource -> Sem r1 x) -> Sem r x) ->
  (∀ r0 x . resource -> effect (Sem r0) x -> Sem (Stop err : r1) x) ->
  InterpreterFor (Scoped param (effect !! err)) r
interpretResumableScopedWith :: forall (extra :: [Effect]) param resource (effect :: Effect) err
       (r :: [Effect]) (r1 :: [Effect]).
(r1 ~ (extra ++ r), KnownList extra) =>
(forall x. param -> (resource -> Sem r1 x) -> Sem r x)
-> (forall (r0 :: [Effect]) x.
    resource -> effect (Sem r0) x -> Sem (Stop err : r1) x)
-> InterpreterFor (Scoped param (effect !! err)) r
interpretResumableScopedWith forall x. param -> (resource -> Sem r1 x) -> Sem r x
withResource forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Sem (Stop err : r1) x
scopedHandler =
  forall (extra :: [Effect]) param resource (effect :: Effect) err
       (r :: [Effect]) (r1 :: [Effect]).
(r1 ~ (extra ++ r), KnownList extra) =>
(forall x. param -> (resource -> Sem r1 x) -> Sem r x)
-> (forall (r0 :: [Effect]) x.
    resource
    -> effect (Sem r0) x
    -> Tactical (effect !! err) (Sem r0) (Stop err : r1) x)
-> InterpreterFor (Scoped param (effect !! err)) r
interpretResumableScopedWithH @extra forall x. param -> (resource -> Sem r1 x) -> Sem r x
withResource \ resource
r effect (Sem r0) x
e -> Sem (Stop err : r1) x
-> Sem
     (WithTactics (effect !! err) f (Sem r0) (Stop err : r1)) (f x)
forall (m :: * -> *) (f :: * -> *) (r :: [Effect]) (e :: Effect) a.
Functor f =>
Sem r a -> Sem (WithTactics e f m r) (f a)
liftT (resource -> effect (Sem r0) x -> Sem (Stop err : r1) x
forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Sem (Stop err : r1) x
scopedHandler resource
r effect (Sem r0) x
e)

-- |Combined interpreter for 'Resumable' and 'Scoped' that allows the handler to use additional effects that are
-- interpreted by the resource allocator.
-- In this variant:
-- - Only the handler may send 'Stop', but this allows resumption to happen on each action inside of the scope.
-- - No resource is used and the allocator is a plain interpreter.
interpretResumableScopedWith_ ::
  ∀ extra param effect err r r1 .
  r1 ~ (extra ++ r) =>
  KnownList extra =>
  (∀ x . param -> Sem r1 x -> Sem r x) ->
  (∀ r0 x . effect (Sem r0) x -> Sem (Stop err : r1) x) ->
  InterpreterFor (Scoped param (effect !! err)) r
interpretResumableScopedWith_ :: forall (extra :: [Effect]) param (effect :: Effect) err
       (r :: [Effect]) (r1 :: [Effect]).
(r1 ~ (extra ++ r), KnownList extra) =>
(forall x. param -> Sem r1 x -> Sem r x)
-> (forall (r0 :: [Effect]) x.
    effect (Sem r0) x -> Sem (Stop err : r1) x)
-> InterpreterFor (Scoped param (effect !! err)) r
interpretResumableScopedWith_ forall x. param -> Sem r1 x -> Sem r x
extra forall (r0 :: [Effect]) x.
effect (Sem r0) x -> Sem (Stop err : r1) x
scopedHandler =
  forall (extra :: [Effect]) param resource (effect :: Effect) err
       (r :: [Effect]) (r1 :: [Effect]).
(r1 ~ (extra ++ r), KnownList extra) =>
(forall x. param -> (resource -> Sem r1 x) -> Sem r x)
-> (forall (r0 :: [Effect]) x.
    resource -> effect (Sem r0) x -> Sem (Stop err : r1) x)
-> InterpreterFor (Scoped param (effect !! err)) r
interpretResumableScopedWith @extra @param @() @effect @err @r @r1 (\ param
p () -> Sem r1 x
f -> param -> Sem r1 x -> Sem r x
forall x. param -> Sem r1 x -> Sem r x
extra param
p (() -> Sem r1 x
f ())) ((effect (Sem r0) x -> Sem (Stop err : r1) x)
-> () -> effect (Sem r0) x -> Sem (Stop err : r1) x
forall a b. a -> b -> a
const effect (Sem r0) x -> Sem (Stop err : r1) x
forall (r0 :: [Effect]) x.
effect (Sem r0) x -> Sem (Stop err : r1) x
scopedHandler)

-- |Combined higher-order interpreter for 'Resumable' and 'Scoped'.
-- In this variant, both the handler and the scope may send different errors via 'Stop', encoding the concept that the
-- resource allocation may fail to prevent the scope from being executed, and each individual scoped action may fail,
-- continuing the scope execution on resumption.
interpretScopedRH ::
  ∀ param resource effect eo ei r .
  (∀ x . param -> (resource -> Sem (Stop eo : r) x) -> Sem (Stop eo : r) x) ->
  (∀ r0 x . resource -> effect (Sem r0) x -> Tactical (effect !! ei) (Sem r0) (Stop ei : Stop eo : r) x) ->
  InterpreterFor (Scoped param (effect !! ei) !! eo) r
interpretScopedRH :: forall param resource (effect :: Effect) eo ei (r :: [Effect]).
(forall x.
 param -> (resource -> Sem (Stop eo : r) x) -> Sem (Stop eo : r) x)
-> (forall (r0 :: [Effect]) x.
    resource
    -> effect (Sem r0) x
    -> Tactical (effect !! ei) (Sem r0) (Stop ei : Stop eo : r) x)
-> InterpreterFor (Scoped param (effect !! ei) !! eo) r
interpretScopedRH forall x.
param -> (resource -> Sem (Stop eo : r) x) -> Sem (Stop eo : r) x
withResource forall (r0 :: [Effect]) x.
resource
-> effect (Sem r0) x
-> Tactical (effect !! ei) (Sem r0) (Stop ei : Stop eo : r) x
scopedHandler =
  (forall x.
 Weaving
   (Scoped param (effect !! ei) !! eo)
   (Sem ((Scoped param (effect !! ei) !! eo) : r))
   x
 -> Sem r x)
-> InterpreterFor (Scoped param (effect !! ei) !! eo) r
forall (e :: Effect) (r :: [Effect]).
(forall x. Weaving e (Sem (e : r)) x -> Sem r x)
-> InterpreterFor e r
interpretWeaving \case
    Weaving (Resumable (Weaving (InScope param
param Sem rInitial a
main) f ()
s' forall x. f (Sem rInitial x) -> Sem r (f x)
wv' f a -> a1
ex' forall x. f x -> Maybe x
_)) f ()
s forall x.
f (Sem rInitial x)
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (f x)
wv f a -> x
ex forall x. f x -> Maybe x
_ -> do
      f ()
-> (f (Either eo a1) -> x)
-> (f a -> a1)
-> Sem r (Either eo (f (f a)))
-> Sem r x
forall {k} (f :: * -> *) err a x (f' :: k -> *) (a' :: k)
       (r :: [Effect]).
Functor f =>
f ()
-> (f (Either err a) -> x)
-> (f' a' -> a)
-> Sem r (Either err (f (f' a')))
-> Sem r x
exResumable f ()
s f a -> x
f (Either eo a1) -> x
ex f a -> a1
ex' (Sem r (Either eo (f (f a))) -> Sem r x)
-> Sem r (Either eo (f (f a))) -> Sem r x
forall a b. (a -> b) -> a -> b
$ Sem (Stop eo : r) (f (f a)) -> Sem r (Either eo (f (f a)))
forall e (r :: [Effect]) a.
Sem (Stop e : r) a -> Sem r (Either e a)
runStop (Sem (Stop eo : r) (f (f a)) -> Sem r (Either eo (f (f a))))
-> Sem (Stop eo : r) (f (f a)) -> Sem r (Either eo (f (f a)))
forall a b. (a -> b) -> a -> b
$ param
-> (resource -> Sem (Stop eo : r) (f (f a)))
-> Sem (Stop eo : r) (f (f a))
forall x.
param -> (resource -> Sem (Stop eo : r) x) -> Sem (Stop eo : r) x
withResource param
param \ resource
resource ->
        (forall x (r0 :: [Effect]).
 effect (Sem r0) x
 -> Tactical (effect !! ei) (Sem r0) (Stop ei : Stop eo : r) x)
-> InterpreterFor (effect !! ei) (Stop eo : r)
forall err (eff :: Effect) (r :: [Effect]).
(forall x (r0 :: [Effect]).
 eff (Sem r0) x
 -> Tactical (Resumable err eff) (Sem r0) (Stop err : r) x)
-> InterpreterFor (Resumable err eff) r
interpretResumableH (resource
-> effect (Sem r0) x
-> Tactical (effect !! ei) (Sem r0) (Stop ei : Stop eo : r) x
forall (r0 :: [Effect]) x.
resource
-> effect (Sem r0) x
-> Tactical (effect !! ei) (Sem r0) (Stop ei : Stop eo : r) x
scopedHandler resource
resource) (Sem ((effect !! ei) : r) (f (f a))
-> Sem ((effect !! ei) : Stop eo : r) (f (f a))
forall (e2 :: Effect) (e1 :: Effect) (r :: [Effect]) a.
Sem (e1 : r) a -> Sem (e1 : e2 : r) a
raiseUnder (Sem
  ((Scoped param (effect !! ei) !! eo) : (effect !! ei) : r)
  (f (f a))
-> Sem ((effect !! ei) : r) (f (f a))
InterpreterFor
  (Scoped param (effect !! ei) !! eo) ((effect !! ei) : r)
inScope (Sem
   ((Scoped param (effect !! ei) !! eo) : (effect !! ei) : r)
   (f (f a))
 -> Sem ((effect !! ei) : r) (f (f a)))
-> Sem
     ((Scoped param (effect !! ei) !! eo) : (effect !! ei) : r)
     (f (f a))
-> Sem ((effect !! ei) : r) (f (f a))
forall a b. (a -> b) -> a -> b
$ Sem ((Scoped param (effect !! ei) !! eo) : r) (f (f a))
-> Sem
     ((Scoped param (effect !! ei) !! eo) : (effect !! ei) : r)
     (f (f a))
forall (e2 :: Effect) (e1 :: Effect) (r :: [Effect]) a.
Sem (e1 : r) a -> Sem (e1 : e2 : r) a
raiseUnder (Sem ((Scoped param (effect !! ei) !! eo) : r) (f (f a))
 -> Sem
      ((Scoped param (effect !! ei) !! eo) : (effect !! ei) : r)
      (f (f a)))
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (f (f a))
-> Sem
     ((Scoped param (effect !! ei) !! eo) : (effect !! ei) : r)
     (f (f a))
forall a b. (a -> b) -> a -> b
$ f (Sem rInitial (f a))
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (f (f a))
forall x.
f (Sem rInitial x)
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (f x)
wv (f (Sem rInitial a) -> Sem r (f a)
forall x. f (Sem rInitial x) -> Sem r (f x)
wv' (Sem rInitial a
main Sem rInitial a -> f () -> f (Sem rInitial a)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s') Sem r (f a) -> f () -> f (Sem r (f a))
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s)))
    Weaving
  (Scoped param (effect !! ei) !! eo)
  (Sem ((Scoped param (effect !! ei) !! eo) : r))
  x
_ ->
      [Char] -> Sem r x
forall a. [Char] -> a
errorWithoutStackTrace [Char]
"top level run"
  where
    inScope :: InterpreterFor (Scoped param (effect !! ei) !! eo) (effect !! ei : r)
    inScope :: InterpreterFor
  (Scoped param (effect !! ei) !! eo) ((effect !! ei) : r)
inScope =
      (forall x.
 Weaving
   (Scoped param (effect !! ei) !! eo)
   (Sem ((Scoped param (effect !! ei) !! eo) : (effect !! ei) : r))
   x
 -> Sem ((effect !! ei) : r) x)
-> InterpreterFor
     (Scoped param (effect !! ei) !! eo) ((effect !! ei) : r)
forall (e :: Effect) (r :: [Effect]).
(forall x. Weaving e (Sem (e : r)) x -> Sem r x)
-> InterpreterFor e r
interpretWeaving \ (Weaving (Resumable (Weaving Scoped param (effect !! ei) (Sem rInitial) a
effect f ()
s' forall x. f (Sem rInitial x) -> Sem r (f x)
wv' f a -> a1
ex' forall x. f x -> Maybe x
ins')) f ()
s forall x.
f (Sem rInitial x)
-> Sem
     ((Scoped param (effect !! ei) !! eo) : (effect !! ei) : r) (f x)
wv f a -> x
ex forall x. f x -> Maybe x
ins) -> case Scoped param (effect !! ei) (Sem rInitial) a
effect of
        Run (!!) effect ei (Sem rInitial) a
act ->
          f a -> x
ex (f a -> x) -> (f a1 -> f a) -> f a1 -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a1 -> Either eo a1) -> f a1 -> f (Either eo a1)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a1 -> Either eo a1
forall a b. b -> Either a b
Right (f a1 -> x)
-> Sem ((effect !! ei) : r) (f a1) -> Sem ((effect !! ei) : r) x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Union ((effect !! ei) : r) (Sem ((effect !! ei) : r)) (f a1)
-> Sem ((effect !! ei) : r) (f a1)
forall (r :: [Effect]) a. Union r (Sem r) a -> Sem r a
liftSem (f ()
-> (forall x. f (Sem rInitial x) -> Sem ((effect !! ei) : r) (f x))
-> (forall x. f x -> Maybe x)
-> Union ((effect !! ei) : r) (Sem rInitial) a1
-> Union ((effect !! ei) : r) (Sem ((effect !! ei) : r)) (f a1)
forall (s :: * -> *) (n :: * -> *) (m :: * -> *) (r :: [Effect]) a.
(Functor s, Functor n) =>
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 f ()
s (Sem
  ((Scoped param (effect !! ei) !! eo) : (effect !! ei) : r) (f x)
-> Sem ((effect !! ei) : r) (f x)
InterpreterFor
  (Scoped param (effect !! ei) !! eo) ((effect !! ei) : r)
inScope (Sem
   ((Scoped param (effect !! ei) !! eo) : (effect !! ei) : r) (f x)
 -> Sem ((effect !! ei) : r) (f x))
-> (f (Sem rInitial x)
    -> Sem
         ((Scoped param (effect !! ei) !! eo) : (effect !! ei) : r) (f x))
-> f (Sem rInitial x)
-> Sem ((effect !! ei) : r) (f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Sem rInitial x)
-> Sem
     ((Scoped param (effect !! ei) !! eo) : (effect !! ei) : r) (f x)
forall x.
f (Sem rInitial x)
-> Sem
     ((Scoped param (effect !! ei) !! eo) : (effect !! ei) : r) (f x)
wv) forall x. f x -> Maybe x
ins (Weaving (effect !! ei) (Sem rInitial) a1
-> Union ((effect !! ei) : r) (Sem rInitial) a1
forall (e :: Effect) (r :: [Effect]) (m :: * -> *) a.
Member e r =>
Weaving e m a -> Union r m a
injWeaving ((!!) effect ei (Sem rInitial) a
-> f ()
-> (forall x. f (Sem rInitial x) -> Sem rInitial (f x))
-> (f a -> a1)
-> (forall x. f x -> Maybe x)
-> Weaving (effect !! ei) (Sem rInitial) a1
forall (f :: * -> *) (e :: Effect) (rInitial :: [Effect]) 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 (!!) effect ei (Sem rInitial) a
act f ()
s' forall x. f (Sem rInitial x) -> Sem rInitial (f x)
forall x. f (Sem rInitial x) -> Sem r (f x)
wv' f a -> a1
ex' forall x. f x -> Maybe x
ins')))
        InScope param
param Sem rInitial a
main -> do
          f ()
-> (f (Either eo a1) -> x)
-> (f a -> a1)
-> Sem ((effect !! ei) : r) (Either eo (f (f a)))
-> Sem ((effect !! ei) : r) x
forall {k} (f :: * -> *) err a x (f' :: k -> *) (a' :: k)
       (r :: [Effect]).
Functor f =>
f ()
-> (f (Either err a) -> x)
-> (f' a' -> a)
-> Sem r (Either err (f (f' a')))
-> Sem r x
exResumable f ()
s f a -> x
f (Either eo a1) -> x
ex f a -> a1
ex' (Sem ((effect !! ei) : r) (Either eo (f (f a)))
 -> Sem ((effect !! ei) : r) x)
-> Sem ((effect !! ei) : r) (Either eo (f (f a)))
-> Sem ((effect !! ei) : r) x
forall a b. (a -> b) -> a -> b
$ Sem r (Either eo (f (f a)))
-> Sem ((effect !! ei) : r) (Either eo (f (f a)))
forall (e :: Effect) (r :: [Effect]) a. Sem r a -> Sem (e : r) a
raise (Sem r (Either eo (f (f a)))
 -> Sem ((effect !! ei) : r) (Either eo (f (f a))))
-> Sem r (Either eo (f (f a)))
-> Sem ((effect !! ei) : r) (Either eo (f (f a)))
forall a b. (a -> b) -> a -> b
$ Sem (Stop eo : r) (f (f a)) -> Sem r (Either eo (f (f a)))
forall e (r :: [Effect]) a.
Sem (Stop e : r) a -> Sem r (Either e a)
runStop (Sem (Stop eo : r) (f (f a)) -> Sem r (Either eo (f (f a))))
-> Sem (Stop eo : r) (f (f a)) -> Sem r (Either eo (f (f a)))
forall a b. (a -> b) -> a -> b
$ param
-> (resource -> Sem (Stop eo : r) (f (f a)))
-> Sem (Stop eo : r) (f (f a))
forall x.
param -> (resource -> Sem (Stop eo : r) x) -> Sem (Stop eo : r) x
withResource param
param \ resource
resource ->
            (forall x (r0 :: [Effect]).
 effect (Sem r0) x
 -> Tactical (effect !! ei) (Sem r0) (Stop ei : Stop eo : r) x)
-> InterpreterFor (effect !! ei) (Stop eo : r)
forall err (eff :: Effect) (r :: [Effect]).
(forall x (r0 :: [Effect]).
 eff (Sem r0) x
 -> Tactical (Resumable err eff) (Sem r0) (Stop err : r) x)
-> InterpreterFor (Resumable err eff) r
interpretResumableH (resource
-> effect (Sem r0) x
-> Tactical (effect !! ei) (Sem r0) (Stop ei : Stop eo : r) x
forall (r0 :: [Effect]) x.
resource
-> effect (Sem r0) x
-> Tactical (effect !! ei) (Sem r0) (Stop ei : Stop eo : r) x
scopedHandler resource
resource) (Sem ((effect !! ei) : r) (f (f a))
-> Sem ((effect !! ei) : Stop eo : r) (f (f a))
forall (e2 :: Effect) (e1 :: Effect) (r :: [Effect]) a.
Sem (e1 : r) a -> Sem (e1 : e2 : r) a
raiseUnder (Sem
  ((Scoped param (effect !! ei) !! eo) : (effect !! ei) : r)
  (f (f a))
-> Sem ((effect !! ei) : r) (f (f a))
InterpreterFor
  (Scoped param (effect !! ei) !! eo) ((effect !! ei) : r)
inScope (Sem
   ((Scoped param (effect !! ei) !! eo) : (effect !! ei) : r)
   (f (f a))
 -> Sem ((effect !! ei) : r) (f (f a)))
-> Sem
     ((Scoped param (effect !! ei) !! eo) : (effect !! ei) : r)
     (f (f a))
-> Sem ((effect !! ei) : r) (f (f a))
forall a b. (a -> b) -> a -> b
$ f (Sem rInitial (f a))
-> Sem
     ((Scoped param (effect !! ei) !! eo) : (effect !! ei) : r)
     (f (f a))
forall x.
f (Sem rInitial x)
-> Sem
     ((Scoped param (effect !! ei) !! eo) : (effect !! ei) : r) (f x)
wv (f (Sem rInitial a) -> Sem r (f a)
forall x. f (Sem rInitial x) -> Sem r (f x)
wv' (Sem rInitial a
main Sem rInitial a -> f () -> f (Sem rInitial a)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s') Sem r (f a) -> f () -> f (Sem r (f a))
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s)))

-- |Combined interpreter for 'Scoped' and 'Resumable'.
-- In this variant, both the handler and the scope may send different errors via 'Stop', encoding the concept that the
-- resource allocation may fail to prevent the scope from being executed, and each individual scoped action may fail,
-- continuing the scope execution on resumption.
interpretScopedR ::
  ∀ param resource effect eo ei r .
  (∀ x . param -> (resource -> Sem (Stop eo : r) x) -> Sem (Stop eo : r) x) ->
  (∀ r0 x . resource -> effect (Sem r0) x -> Sem (Stop ei : Stop eo : r) x) ->
  InterpreterFor (Scoped param (effect !! ei) !! eo) r
interpretScopedR :: forall param resource (effect :: Effect) eo ei (r :: [Effect]).
(forall x.
 param -> (resource -> Sem (Stop eo : r) x) -> Sem (Stop eo : r) x)
-> (forall (r0 :: [Effect]) x.
    resource -> effect (Sem r0) x -> Sem (Stop ei : Stop eo : r) x)
-> InterpreterFor (Scoped param (effect !! ei) !! eo) r
interpretScopedR forall x.
param -> (resource -> Sem (Stop eo : r) x) -> Sem (Stop eo : r) x
withResource forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Sem (Stop ei : Stop eo : r) x
scopedHandler =
  (forall x.
 param -> (resource -> Sem (Stop eo : r) x) -> Sem (Stop eo : r) x)
-> (forall (r0 :: [Effect]) x.
    resource
    -> effect (Sem r0) x
    -> Tactical (effect !! ei) (Sem r0) (Stop ei : Stop eo : r) x)
-> InterpreterFor (Scoped param (effect !! ei) !! eo) r
forall param resource (effect :: Effect) eo ei (r :: [Effect]).
(forall x.
 param -> (resource -> Sem (Stop eo : r) x) -> Sem (Stop eo : r) x)
-> (forall (r0 :: [Effect]) x.
    resource
    -> effect (Sem r0) x
    -> Tactical (effect !! ei) (Sem r0) (Stop ei : Stop eo : r) x)
-> InterpreterFor (Scoped param (effect !! ei) !! eo) r
interpretScopedRH forall x.
param -> (resource -> Sem (Stop eo : r) x) -> Sem (Stop eo : r) x
withResource \ resource
r effect (Sem r0) x
e -> Sem (Stop ei : Stop eo : r) x
-> Sem
     (WithTactics (effect !! ei) f (Sem r0) (Stop ei : Stop eo : r))
     (f x)
forall (m :: * -> *) (f :: * -> *) (r :: [Effect]) (e :: Effect) a.
Functor f =>
Sem r a -> Sem (WithTactics e f m r) (f a)
liftT (resource -> effect (Sem r0) x -> Sem (Stop ei : Stop eo : r) x
forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Sem (Stop ei : Stop eo : r) x
scopedHandler resource
r effect (Sem r0) x
e)

-- |Combined interpreter for 'Scoped' and 'Resumable'.
-- In this variant:
-- - Both the handler and the scope may send different errors via 'Stop', encoding the concept that the
--   resource allocation may fail to prevent the scope from being executed, and each individual scoped action may fail,
--   continuing the scope execution on resumption.
-- - The resource allocator is a plain action.
interpretScopedR_ ::
  ∀ param resource effect eo ei r .
  (param -> Sem (Stop eo : r) resource) ->
  (∀ r0 x . resource -> effect (Sem r0) x -> Sem (Stop ei : Stop eo : r) x) ->
  InterpreterFor (Scoped param (effect !! ei) !! eo) r
interpretScopedR_ :: forall param resource (effect :: Effect) eo ei (r :: [Effect]).
(param -> Sem (Stop eo : r) resource)
-> (forall (r0 :: [Effect]) x.
    resource -> effect (Sem r0) x -> Sem (Stop ei : Stop eo : r) x)
-> InterpreterFor (Scoped param (effect !! ei) !! eo) r
interpretScopedR_ param -> Sem (Stop eo : r) resource
resource =
  (forall x.
 param -> (resource -> Sem (Stop eo : r) x) -> Sem (Stop eo : r) x)
-> (forall (r0 :: [Effect]) x.
    resource -> effect (Sem r0) x -> Sem (Stop ei : Stop eo : r) x)
-> InterpreterFor (Scoped param (effect !! ei) !! eo) r
forall param resource (effect :: Effect) eo ei (r :: [Effect]).
(forall x.
 param -> (resource -> Sem (Stop eo : r) x) -> Sem (Stop eo : r) x)
-> (forall (r0 :: [Effect]) x.
    resource -> effect (Sem r0) x -> Sem (Stop ei : Stop eo : r) x)
-> InterpreterFor (Scoped param (effect !! ei) !! eo) r
interpretScopedR \ param
p resource -> Sem (Stop eo : r) x
use -> resource -> Sem (Stop eo : r) x
use (resource -> Sem (Stop eo : r) x)
-> Sem (Stop eo : r) resource -> Sem (Stop eo : r) x
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< param -> Sem (Stop eo : r) resource
resource param
p

-- |Combined higher-order interpreter for 'Scoped' and 'Resumable' that allows the handler to use additional effects
-- that are interpreted by the resource allocator.
-- In this variant, both the handler and the scope may send different errors via 'Stop', encoding the concept that the
-- resource allocation may fail to prevent the scope from being executed, and each individual scoped action may fail,
-- continuing the scope execution on resumption.
interpretScopedRWithH ::
  ∀ extra param resource effect eo ei r r1 extraerr .
  extraerr ~ (extra ++ '[Stop eo]) =>
  r1 ~ (extra ++ Stop eo : r) =>
  r1 ~ ((extra ++ '[Stop eo]) ++ r) =>
  KnownList (extra ++ '[Stop eo]) =>
  (∀ x . param -> (resource -> Sem (extra ++ Stop eo : r) x) -> Sem (Stop eo : r) x) ->
  (∀ r0 x . resource -> effect (Sem r0) x -> Tactical (effect !! ei) (Sem r0) (Stop ei : r1) x) ->
  InterpreterFor (Scoped param (effect !! ei) !! eo) r
interpretScopedRWithH :: forall (extra :: [Effect]) param resource (effect :: Effect) eo ei
       (r :: [Effect]) (r1 :: [Effect]) (extraerr :: [Effect]).
(extraerr ~ (extra ++ '[Stop eo]), r1 ~ (extra ++ (Stop eo : r)),
 r1 ~ ((extra ++ '[Stop eo]) ++ r),
 KnownList (extra ++ '[Stop eo])) =>
(forall x.
 param
 -> (resource -> Sem (extra ++ (Stop eo : r)) x)
 -> Sem (Stop eo : r) x)
-> (forall (r0 :: [Effect]) x.
    resource
    -> effect (Sem r0) x
    -> Tactical (effect !! ei) (Sem r0) (Stop ei : r1) x)
-> InterpreterFor (Scoped param (effect !! ei) !! eo) r
interpretScopedRWithH forall x.
param
-> (resource -> Sem (extra ++ (Stop eo : r)) x)
-> Sem (Stop eo : r) x
withResource forall (r0 :: [Effect]) x.
resource
-> effect (Sem r0) x
-> Tactical (effect !! ei) (Sem r0) (Stop ei : r1) x
scopedHandler =
  (forall x.
 Weaving
   (Scoped param (effect !! ei) !! eo)
   (Sem ((Scoped param (effect !! ei) !! eo) : r))
   x
 -> Sem r x)
-> InterpreterFor (Scoped param (effect !! ei) !! eo) r
forall (e :: Effect) (r :: [Effect]).
(forall x. Weaving e (Sem (e : r)) x -> Sem r x)
-> InterpreterFor e r
interpretWeaving \case
    Weaving (Resumable (Weaving (InScope param
param Sem rInitial a
main) f ()
s' forall x. f (Sem rInitial x) -> Sem r (f x)
wv' f a -> a1
ex' forall x. f x -> Maybe x
_)) f ()
s forall x.
f (Sem rInitial x)
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (f x)
wv f a -> x
ex forall x. f x -> Maybe x
_ -> do
      f ()
-> (f (Either eo a1) -> x)
-> (f a -> a1)
-> Sem r (Either eo (f (f a)))
-> Sem r x
forall {k} (f :: * -> *) err a x (f' :: k -> *) (a' :: k)
       (r :: [Effect]).
Functor f =>
f ()
-> (f (Either err a) -> x)
-> (f' a' -> a)
-> Sem r (Either err (f (f' a')))
-> Sem r x
exResumable f ()
s f a -> x
f (Either eo a1) -> x
ex f a -> a1
ex' (Sem r (Either eo (f (f a))) -> Sem r x)
-> Sem r (Either eo (f (f a))) -> Sem r x
forall a b. (a -> b) -> a -> b
$ Sem (Stop eo : r) (f (f a)) -> Sem r (Either eo (f (f a)))
forall e (r :: [Effect]) a.
Sem (Stop e : r) a -> Sem r (Either e a)
runStop (Sem (Stop eo : r) (f (f a)) -> Sem r (Either eo (f (f a))))
-> Sem (Stop eo : r) (f (f a)) -> Sem r (Either eo (f (f a)))
forall a b. (a -> b) -> a -> b
$ param
-> (resource -> Sem (extra ++ (Stop eo : r)) (f (f a)))
-> Sem (Stop eo : r) (f (f a))
forall x.
param
-> (resource -> Sem (extra ++ (Stop eo : r)) x)
-> Sem (Stop eo : r) x
withResource param
param \ resource
resource ->
        (forall x (r0 :: [Effect]).
 effect (Sem r0) x
 -> Tactical (effect !! ei) (Sem r0) (Stop ei : r1) x)
-> InterpreterFor (effect !! ei) r1
forall err (eff :: Effect) (r :: [Effect]).
(forall x (r0 :: [Effect]).
 eff (Sem r0) x
 -> Tactical (Resumable err eff) (Sem r0) (Stop err : r) x)
-> InterpreterFor (Resumable err eff) r
interpretResumableH (resource
-> effect (Sem r0) x
-> Tactical (effect !! ei) (Sem r0) (Stop ei : r1) x
forall (r0 :: [Effect]) x.
resource
-> effect (Sem r0) x
-> Tactical (effect !! ei) (Sem r0) (Stop ei : r1) x
scopedHandler resource
resource) (Sem ((effect !! ei) : r1) (f (f a)) -> Sem r1 (f (f a)))
-> Sem ((effect !! ei) : r1) (f (f a)) -> Sem r1 (f (f a))
forall a b. (a -> b) -> a -> b
$ Sem
  ((Scoped param (effect !! ei) !! eo) : (effect !! ei) : r1)
  (f (f a))
-> Sem ((effect !! ei) : r1) (f (f a))
InterpreterFor
  (Scoped param (effect !! ei) !! eo) ((effect !! ei) : r1)
inScope (Sem
   ((Scoped param (effect !! ei) !! eo) : (effect !! ei) : r1)
   (f (f a))
 -> Sem ((effect !! ei) : r1) (f (f a)))
-> Sem
     ((Scoped param (effect !! ei) !! eo) : (effect !! ei) : r1)
     (f (f a))
-> Sem ((effect !! ei) : r1) (f (f a))
forall a b. (a -> b) -> a -> b
$
          (forall (e :: Effect).
 ElemOf e ((Scoped param (effect !! ei) !! eo) : r)
 -> ElemOf
      e ((Scoped param (effect !! ei) !! eo) : (effect !! ei) : r1))
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (f (f a))
-> Sem
     ((Scoped param (effect !! ei) !! eo) : (effect !! ei) : r1)
     (f (f a))
forall (r :: [Effect]) (r' :: [Effect]) a.
(forall (e :: Effect). ElemOf e r -> ElemOf e r')
-> Sem r a -> Sem r' a
restack
            (SList '[Scoped param (effect !! ei) !! eo]
-> SList ((effect !! ei) : extraerr)
-> ElemOf e (Append '[Scoped param (effect !! ei) !! eo] r)
-> ElemOf
     e
     (Append
        '[Scoped param (effect !! ei) !! eo]
        (Append ((effect !! ei) : extraerr) r))
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
             (forall (l :: [Effect]). KnownList l => SList l
forall {a} (l :: [a]). KnownList l => SList l
singList @'[Scoped param (effect !! ei) !! eo])
             (forall (l :: [Effect]). KnownList l => SList l
forall {a} (l :: [a]). KnownList l => SList l
singList @(effect !! ei : extraerr))) (Sem ((Scoped param (effect !! ei) !! eo) : r) (f (f a))
 -> Sem
      ((Scoped param (effect !! ei) !! eo) : (effect !! ei) : r1)
      (f (f a)))
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (f (f a))
-> Sem
     ((Scoped param (effect !! ei) !! eo) : (effect !! ei) : r1)
     (f (f a))
forall a b. (a -> b) -> a -> b
$ f (Sem rInitial (f a))
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (f (f a))
forall x.
f (Sem rInitial x)
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (f x)
wv (f (Sem rInitial a) -> Sem r (f a)
forall x. f (Sem rInitial x) -> Sem r (f x)
wv' (Sem rInitial a
main Sem rInitial a -> f () -> f (Sem rInitial a)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s') Sem r (f a) -> f () -> f (Sem r (f a))
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s)
    Weaving
  (Scoped param (effect !! ei) !! eo)
  (Sem ((Scoped param (effect !! ei) !! eo) : r))
  x
_ ->
      [Char] -> Sem r x
forall a. [Char] -> a
errorWithoutStackTrace [Char]
"top level Run"
  where
    inScope :: InterpreterFor (Scoped param (effect !! ei) !! eo) (effect !! ei : r1)
    inScope :: InterpreterFor
  (Scoped param (effect !! ei) !! eo) ((effect !! ei) : r1)
inScope =
      (forall x.
 Weaving
   (Scoped param (effect !! ei) !! eo)
   (Sem ((Scoped param (effect !! ei) !! eo) : (effect !! ei) : r1))
   x
 -> Sem ((effect !! ei) : r1) x)
-> InterpreterFor
     (Scoped param (effect !! ei) !! eo) ((effect !! ei) : r1)
forall (e :: Effect) (r :: [Effect]).
(forall x. Weaving e (Sem (e : r)) x -> Sem r x)
-> InterpreterFor e r
interpretWeaving \ (Weaving (Resumable (Weaving Scoped param (effect !! ei) (Sem rInitial) a
effect f ()
s' forall x. f (Sem rInitial x) -> Sem r (f x)
wv' f a -> a1
ex' forall x. f x -> Maybe x
ins')) f ()
s forall x.
f (Sem rInitial x)
-> Sem
     ((Scoped param (effect !! ei) !! eo) : (effect !! ei) : r1) (f x)
wv f a -> x
ex forall x. f x -> Maybe x
ins) -> case Scoped param (effect !! ei) (Sem rInitial) a
effect of
        InScope param
param Sem rInitial a
main ->
          f ()
-> (f (Either eo a1) -> x)
-> (f a -> a1)
-> Sem ((effect !! ei) : r1) (Either eo (f (f a)))
-> Sem ((effect !! ei) : r1) x
forall {k} (f :: * -> *) err a x (f' :: k -> *) (a' :: k)
       (r :: [Effect]).
Functor f =>
f ()
-> (f (Either err a) -> x)
-> (f' a' -> a)
-> Sem r (Either err (f (f' a')))
-> Sem r x
exResumable f ()
s f a -> x
f (Either eo a1) -> x
ex f a -> a1
ex' (Sem ((effect !! ei) : r1) (Either eo (f (f a)))
 -> Sem ((effect !! ei) : r1) x)
-> Sem ((effect !! ei) : r1) (Either eo (f (f a)))
-> Sem ((effect !! ei) : r1) x
forall a b. (a -> b) -> a -> b
$
          (forall (e :: Effect).
 ElemOf e r -> ElemOf e ((effect !! ei) : r1))
-> Sem r (Either eo (f (f a)))
-> Sem ((effect !! ei) : r1) (Either eo (f (f a)))
forall (r :: [Effect]) (r' :: [Effect]) a.
(forall (e :: Effect). ElemOf e r -> ElemOf e r')
-> Sem r a -> Sem r' a
restack (SList ((effect !! ei) : extraerr)
-> ElemOf e r -> ElemOf e (Append ((effect !! ei) : extraerr) r)
forall {a} (l :: [a]) (r :: [a]) (e :: a).
SList l -> ElemOf e r -> ElemOf e (Append l r)
extendMembershipLeft (forall (l :: [Effect]). KnownList l => SList l
forall {a} (l :: [a]). KnownList l => SList l
singList @(effect !! ei : extraerr))) (Sem r (Either eo (f (f a)))
 -> Sem ((effect !! ei) : r1) (Either eo (f (f a))))
-> Sem r (Either eo (f (f a)))
-> Sem ((effect !! ei) : r1) (Either eo (f (f a)))
forall a b. (a -> b) -> a -> b
$
          Sem (Stop eo : r) (f (f a)) -> Sem r (Either eo (f (f a)))
forall e (r :: [Effect]) a.
Sem (Stop e : r) a -> Sem r (Either e a)
runStop (Sem (Stop eo : r) (f (f a)) -> Sem r (Either eo (f (f a))))
-> Sem (Stop eo : r) (f (f a)) -> Sem r (Either eo (f (f a)))
forall a b. (a -> b) -> a -> b
$
          param
-> (resource -> Sem (extra ++ (Stop eo : r)) (f (f a)))
-> Sem (Stop eo : r) (f (f a))
forall x.
param
-> (resource -> Sem (extra ++ (Stop eo : r)) x)
-> Sem (Stop eo : r) x
withResource param
param \ resource
resource ->
            (forall x (r0 :: [Effect]).
 effect (Sem r0) x
 -> Tactical (effect !! ei) (Sem r0) (Stop ei : r1) x)
-> InterpreterFor (effect !! ei) r1
forall err (eff :: Effect) (r :: [Effect]).
(forall x (r0 :: [Effect]).
 eff (Sem r0) x
 -> Tactical (Resumable err eff) (Sem r0) (Stop err : r) x)
-> InterpreterFor (Resumable err eff) r
interpretResumableH (resource
-> effect (Sem r0) x
-> Tactical (effect !! ei) (Sem r0) (Stop ei : r1) x
forall (r0 :: [Effect]) x.
resource
-> effect (Sem r0) x
-> Tactical (effect !! ei) (Sem r0) (Stop ei : r1) x
scopedHandler resource
resource) (Sem
  ((Scoped param (effect !! ei) !! eo) : (effect !! ei) : r1)
  (f (f a))
-> Sem ((effect !! ei) : r1) (f (f a))
InterpreterFor
  (Scoped param (effect !! ei) !! eo) ((effect !! ei) : r1)
inScope (Sem
   ((Scoped param (effect !! ei) !! eo) : (effect !! ei) : r1)
   (f (f a))
 -> Sem ((effect !! ei) : r1) (f (f a)))
-> Sem
     ((Scoped param (effect !! ei) !! eo) : (effect !! ei) : r1)
     (f (f a))
-> Sem ((effect !! ei) : r1) (f (f a))
forall a b. (a -> b) -> a -> b
$ f (Sem rInitial (f a))
-> Sem
     ((Scoped param (effect !! ei) !! eo) : (effect !! ei) : r1)
     (f (f a))
forall x.
f (Sem rInitial x)
-> Sem
     ((Scoped param (effect !! ei) !! eo) : (effect !! ei) : r1) (f x)
wv (f (Sem rInitial a) -> Sem r (f a)
forall x. f (Sem rInitial x) -> Sem r (f x)
wv' (Sem rInitial a
main Sem rInitial a -> f () -> f (Sem rInitial a)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s') Sem r (f a) -> f () -> f (Sem r (f a))
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s))
        Run (!!) effect ei (Sem rInitial) a
act ->
          f a -> x
ex (f a -> x) -> (f a1 -> f a) -> f a1 -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a1 -> Either eo a1) -> f a1 -> f (Either eo a1)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a1 -> Either eo a1
forall a b. b -> Either a b
Right (f a1 -> x)
-> Sem ((effect !! ei) : r1) (f a1) -> Sem ((effect !! ei) : r1) x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Union ((effect !! ei) : r1) (Sem ((effect !! ei) : r1)) (f a1)
-> Sem ((effect !! ei) : r1) (f a1)
forall (r :: [Effect]) a. Union r (Sem r) a -> Sem r a
liftSem (f ()
-> (forall x.
    f (Sem rInitial x) -> Sem ((effect !! ei) : r1) (f x))
-> (forall x. f x -> Maybe x)
-> Union ((effect !! ei) : r1) (Sem rInitial) a1
-> Union ((effect !! ei) : r1) (Sem ((effect !! ei) : r1)) (f a1)
forall (s :: * -> *) (n :: * -> *) (m :: * -> *) (r :: [Effect]) a.
(Functor s, Functor n) =>
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 f ()
s (Sem
  ((Scoped param (effect !! ei) !! eo) : (effect !! ei) : r1) (f x)
-> Sem ((effect !! ei) : r1) (f x)
InterpreterFor
  (Scoped param (effect !! ei) !! eo) ((effect !! ei) : r1)
inScope (Sem
   ((Scoped param (effect !! ei) !! eo) : (effect !! ei) : r1) (f x)
 -> Sem ((effect !! ei) : r1) (f x))
-> (f (Sem rInitial x)
    -> Sem
         ((Scoped param (effect !! ei) !! eo) : (effect !! ei) : r1) (f x))
-> f (Sem rInitial x)
-> Sem ((effect !! ei) : r1) (f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Sem rInitial x)
-> Sem
     ((Scoped param (effect !! ei) !! eo) : (effect !! ei) : r1) (f x)
forall x.
f (Sem rInitial x)
-> Sem
     ((Scoped param (effect !! ei) !! eo) : (effect !! ei) : r1) (f x)
wv) forall x. f x -> Maybe x
ins (Weaving (effect !! ei) (Sem rInitial) a1
-> Union ((effect !! ei) : r1) (Sem rInitial) a1
forall (e :: Effect) (r :: [Effect]) (m :: * -> *) a.
Member e r =>
Weaving e m a -> Union r m a
injWeaving ((!!) effect ei (Sem rInitial) a
-> f ()
-> (forall x. f (Sem rInitial x) -> Sem rInitial (f x))
-> (f a -> a1)
-> (forall x. f x -> Maybe x)
-> Weaving (effect !! ei) (Sem rInitial) a1
forall (f :: * -> *) (e :: Effect) (rInitial :: [Effect]) 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 (!!) effect ei (Sem rInitial) a
act f ()
s' forall x. f (Sem rInitial x) -> Sem rInitial (f x)
forall x. f (Sem rInitial x) -> Sem r (f x)
wv' f a -> a1
ex' forall x. f x -> Maybe x
ins')))

-- |Combined interpreter for 'Scoped' and 'Resumable' that allows the handler to use additional effects that are
-- interpreted by the resource allocator.
-- In this variant, both the handler and the scope may send different errors via 'Stop', encoding the concept that the
-- resource allocation may fail to prevent the scope from being executed, and each individual scoped action may fail,
-- continuing the scope execution on resumption.
interpretScopedRWith ::
  ∀ extra param resource effect eo ei r r1 .
  r1 ~ (extra ++ Stop eo : r) =>
  r1 ~ ((extra ++ '[Stop eo]) ++ r) =>
  KnownList (extra ++ '[Stop eo]) =>
  (∀ x . param -> (resource -> Sem r1 x) -> Sem (Stop eo : r) x) ->
  (∀ r0 x . resource -> effect (Sem r0) x -> Sem (Stop ei : r1) x) ->
  InterpreterFor (Scoped param (effect !! ei) !! eo) r
interpretScopedRWith :: forall (extra :: [Effect]) param resource (effect :: Effect) eo ei
       (r :: [Effect]) (r1 :: [Effect]).
(r1 ~ (extra ++ (Stop eo : r)), r1 ~ ((extra ++ '[Stop eo]) ++ r),
 KnownList (extra ++ '[Stop eo])) =>
(forall x. param -> (resource -> Sem r1 x) -> Sem (Stop eo : r) x)
-> (forall (r0 :: [Effect]) x.
    resource -> effect (Sem r0) x -> Sem (Stop ei : r1) x)
-> InterpreterFor (Scoped param (effect !! ei) !! eo) r
interpretScopedRWith forall x. param -> (resource -> Sem r1 x) -> Sem (Stop eo : r) x
withResource forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Sem (Stop ei : r1) x
scopedHandler =
  forall (extra :: [Effect]) param resource (effect :: Effect) eo ei
       (r :: [Effect]) (r1 :: [Effect]) (extraerr :: [Effect]).
(extraerr ~ (extra ++ '[Stop eo]), r1 ~ (extra ++ (Stop eo : r)),
 r1 ~ ((extra ++ '[Stop eo]) ++ r),
 KnownList (extra ++ '[Stop eo])) =>
(forall x.
 param
 -> (resource -> Sem (extra ++ (Stop eo : r)) x)
 -> Sem (Stop eo : r) x)
-> (forall (r0 :: [Effect]) x.
    resource
    -> effect (Sem r0) x
    -> Tactical (effect !! ei) (Sem r0) (Stop ei : r1) x)
-> InterpreterFor (Scoped param (effect !! ei) !! eo) r
interpretScopedRWithH @extra forall x. param -> (resource -> Sem r1 x) -> Sem (Stop eo : r) x
forall x.
param
-> (resource -> Sem (extra ++ (Stop eo : r)) x)
-> Sem (Stop eo : r) x
withResource \ resource
r effect (Sem r0) x
e -> Sem (Stop ei : r1) x
-> Sem (WithTactics (effect !! ei) f (Sem r0) (Stop ei : r1)) (f x)
forall (m :: * -> *) (f :: * -> *) (r :: [Effect]) (e :: Effect) a.
Functor f =>
Sem r a -> Sem (WithTactics e f m r) (f a)
liftT (resource -> effect (Sem r0) x -> Sem (Stop ei : r1) x
forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Sem (Stop ei : r1) x
scopedHandler resource
r effect (Sem r0) x
e)

-- |Combined interpreter for 'Scoped' and 'Resumable' that allows the handler to use additional effects that are
-- interpreted by the resource allocator.
-- - Both the handler and the scope may send different errors via 'Stop', encoding the concept that the
--   resource allocation may fail to prevent the scope from being executed, and each individual scoped action may fail,
--   continuing the scope execution on resumption.
-- - The resource allocator is a plain action.
interpretScopedRWith_ ::
  ∀ extra param effect eo ei r r1 .
  r1 ~ (extra ++ Stop eo : r) =>
  r1 ~ ((extra ++ '[Stop eo]) ++ r) =>
  KnownList (extra ++ '[Stop eo]) =>
  (∀ x . param -> Sem r1 x -> Sem (Stop eo : r) x) ->
  (∀ r0 x . effect (Sem r0) x -> Sem (Stop ei : r1) x) ->
  InterpreterFor (Scoped param (effect !! ei) !! eo) r
interpretScopedRWith_ :: forall (extra :: [Effect]) param (effect :: Effect) eo ei
       (r :: [Effect]) (r1 :: [Effect]).
(r1 ~ (extra ++ (Stop eo : r)), r1 ~ ((extra ++ '[Stop eo]) ++ r),
 KnownList (extra ++ '[Stop eo])) =>
(forall x. param -> Sem r1 x -> Sem (Stop eo : r) x)
-> (forall (r0 :: [Effect]) x.
    effect (Sem r0) x -> Sem (Stop ei : r1) x)
-> InterpreterFor (Scoped param (effect !! ei) !! eo) r
interpretScopedRWith_ forall x. param -> Sem r1 x -> Sem (Stop eo : r) x
extra forall (r0 :: [Effect]) x.
effect (Sem r0) x -> Sem (Stop ei : r1) x
scopedHandler =
  forall (extra :: [Effect]) param resource (effect :: Effect) eo ei
       (r :: [Effect]) (r1 :: [Effect]).
(r1 ~ (extra ++ (Stop eo : r)), r1 ~ ((extra ++ '[Stop eo]) ++ r),
 KnownList (extra ++ '[Stop eo])) =>
(forall x. param -> (resource -> Sem r1 x) -> Sem (Stop eo : r) x)
-> (forall (r0 :: [Effect]) x.
    resource -> effect (Sem r0) x -> Sem (Stop ei : r1) x)
-> InterpreterFor (Scoped param (effect !! ei) !! eo) r
interpretScopedRWith @extra (\ param
p () -> Sem r1 x
f -> param -> Sem r1 x -> Sem (Stop eo : r) x
forall x. param -> Sem r1 x -> Sem (Stop eo : r) x
extra param
p (() -> Sem r1 x
f ())) ((effect (Sem r0) x -> Sem (Stop ei : r1) x)
-> () -> effect (Sem r0) x -> Sem (Stop ei : r1) x
forall a b. a -> b -> a
const effect (Sem r0) x -> Sem (Stop ei : r1) x
forall (r0 :: [Effect]) x.
effect (Sem r0) x -> Sem (Stop ei : r1) x
scopedHandler)