{-# options_haddock prune #-}

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

import Polysemy.Internal (Sem (Sem, runSem), liftSem)
import Polysemy.Internal.Index (InsertAtIndex)
import Polysemy.Internal.Tactics (liftT, runTactics)
import Polysemy.Internal.Union (Weaving (Weaving), decomp, hoist, injWeaving)
import Polysemy.Resume (Stop, runStop, type (!!))
import Polysemy.Resume.Data.Resumable (Resumable (Resumable))

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

interpretH' ::
  ∀ e r .
  (∀ x . Weaving e (Sem (e : r)) x -> Sem r x) ->
  InterpreterFor e r
interpretH' :: forall (e :: Effect) (r :: [Effect]).
(forall x. Weaving e (Sem (e : r)) x -> Sem r x)
-> InterpreterFor e r
interpretH' 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 (Union r (Sem r) x -> m x) -> Union r (Sem r) x -> m x
forall a b. (a -> b) -> a -> b
$ (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
interpretH' forall x. Weaving e (Sem (e : r)) x -> Sem r x
h) Union r (Sem (e : r)) x
g


-- |Interpreter for 'Scoped', taking a @resource@ allocation function and a parameterized interpreter for the plain
-- @effect@.
--
-- @withResource@ is a callback function, allowing the user to acquire the resource for each program from other effects.
--
-- @scopedInterpreter@ is a regular interpreter that is called with the @resource@ argument produced by @scope@.
-- /Note/: This function will be called for each action in the program, so if the interpreter allocates any resources,
-- they will be scoped to a single action. Move them to @withResource@ instead.
runScoped ::
  ∀ resource effect r .
  (∀ x . (resource -> Sem r x) -> Sem r x) ->
  (resource -> InterpreterFor effect r) ->
  InterpreterFor (Scoped resource effect) r
runScoped :: forall resource (effect :: Effect) (r :: [Effect]).
(forall x. (resource -> Sem r x) -> Sem r x)
-> (resource -> InterpreterFor effect r)
-> InterpreterFor (Scoped resource effect) r
runScoped forall x. (resource -> Sem r x) -> Sem r x
withResource resource -> InterpreterFor effect r
scopedInterpreter =
  Sem (Scoped resource effect : r) a -> Sem r a
InterpreterFor (Scoped resource effect) r
run
  where
    run :: InterpreterFor (Scoped resource effect) r
    run :: InterpreterFor (Scoped resource effect) r
run =
      (forall x.
 Weaving
   (Scoped resource effect) (Sem (Scoped resource effect : r)) x
 -> Sem r x)
-> InterpreterFor (Scoped resource effect) r
forall (e :: Effect) (r :: [Effect]).
(forall x. Weaving e (Sem (e : r)) x -> Sem r x)
-> InterpreterFor e r
interpretH' \ (Weaving Scoped resource effect (Sem rInitial) a
effect f ()
s forall x.
f (Sem rInitial x) -> Sem (Scoped resource effect : r) (f x)
wv f a -> x
ex forall x. f x -> Maybe x
ins) -> case Scoped resource effect (Sem rInitial) a
effect of
        Run resource
resource effect (Sem rInitial) a
act ->
          resource -> InterpreterFor effect r
scopedInterpreter resource
resource (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 r (f x) -> Sem (effect : r) (f x)
forall (e :: Effect) (r :: [Effect]) a. Sem r a -> Sem (e : r) a
raise (Sem r (f x) -> Sem (effect : r) (f x))
-> (f (Sem rInitial x) -> Sem r (f x))
-> f (Sem rInitial x)
-> Sem (effect : r) (f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sem (Scoped resource effect : r) (f x) -> Sem r (f x)
InterpreterFor (Scoped resource effect) r
run (Sem (Scoped resource effect : r) (f x) -> Sem r (f x))
-> (f (Sem rInitial x) -> Sem (Scoped resource effect : r) (f x))
-> f (Sem rInitial x)
-> Sem r (f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Sem rInitial x) -> Sem (Scoped resource effect : r) (f x)
forall x.
f (Sem rInitial x) -> Sem (Scoped resource effect : r) (f x)
wv) f a -> x
ex forall x. f x -> Maybe x
ins)
        InScope resource -> Sem rInitial a
main ->
          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 -> Sem r (f a)) -> Sem r (f a)
forall x. (resource -> Sem r x) -> Sem r x
withResource \ resource
resource -> Sem (Scoped resource effect : r) (f a) -> Sem r (f a)
InterpreterFor (Scoped resource effect) r
run (f (Sem rInitial a) -> Sem (Scoped resource effect : r) (f a)
forall x.
f (Sem rInitial x) -> Sem (Scoped resource effect : r) (f x)
wv (resource -> Sem rInitial a
main resource
resource Sem rInitial a -> f () -> f (Sem rInitial a)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s))

-- |Variant of 'runScoped' in which the resource allocator is a plain action.
runScopedAs ::
  ∀ resource effect r .
  Sem r resource ->
  (resource -> InterpreterFor effect r) ->
  InterpreterFor (Scoped resource effect) r
runScopedAs :: forall resource (effect :: Effect) (r :: [Effect]).
Sem r resource
-> (resource -> InterpreterFor effect r)
-> InterpreterFor (Scoped resource effect) r
runScopedAs Sem r resource
resource =
  (forall x. (resource -> Sem r x) -> Sem r x)
-> (resource -> InterpreterFor effect r)
-> InterpreterFor (Scoped resource effect) r
forall resource (effect :: Effect) (r :: [Effect]).
(forall x. (resource -> Sem r x) -> Sem r x)
-> (resource -> InterpreterFor effect r)
-> InterpreterFor (Scoped resource effect) r
runScoped \ resource -> Sem r x
f -> resource -> Sem r x
f (resource -> Sem r x) -> Sem r resource -> Sem r x
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Sem r resource
resource

-- |Variant of 'runScoped' that takes a higher-order handler instead of an interpreter.
interpretScopedH ::
  ∀ resource effect r .
  (∀ x . (resource -> Sem r x) -> Sem r x) ->
  (∀ r0 x . resource -> effect (Sem r0) x -> Tactical effect (Sem r0) r x) ->
  InterpreterFor (Scoped resource effect) r
interpretScopedH :: forall resource (effect :: Effect) (r :: [Effect]).
(forall x. (resource -> Sem r x) -> Sem r x)
-> (forall (r0 :: [Effect]) x.
    resource -> effect (Sem r0) x -> Tactical effect (Sem r0) r x)
-> InterpreterFor (Scoped resource effect) r
interpretScopedH forall x. (resource -> Sem r x) -> Sem r x
withResource forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Tactical effect (Sem r0) r x
scopedHandler =
  Sem (Scoped resource effect : r) a -> Sem r a
InterpreterFor (Scoped resource effect) r
run
  where
    run :: InterpreterFor (Scoped resource effect) r
    run :: InterpreterFor (Scoped resource effect) r
run =
      (forall x.
 Weaving
   (Scoped resource effect) (Sem (Scoped resource effect : r)) x
 -> Sem r x)
-> InterpreterFor (Scoped resource effect) r
forall (e :: Effect) (r :: [Effect]).
(forall x. Weaving e (Sem (e : r)) x -> Sem r x)
-> InterpreterFor e r
interpretH' \ (Weaving Scoped resource effect (Sem rInitial) a
effect f ()
s forall x.
f (Sem rInitial x) -> Sem (Scoped resource effect : r) (f x)
wv f a -> x
ex forall x. f x -> Maybe x
ins) -> case Scoped resource effect (Sem rInitial) a
effect of
        Run resource
resource effect (Sem rInitial) a
act ->
          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
<$> f ()
-> (forall x. f (Sem rInitial x) -> Sem (effect : r) (f x))
-> (forall x. f x -> Maybe x)
-> (forall x. f (Sem rInitial x) -> Sem r (f x))
-> Sem (Tactics f (Sem rInitial) (effect : r) : r) (f a)
-> Sem r (f a)
forall (f :: * -> *) (m :: * -> *) (r2 :: [Effect]) (r :: [Effect])
       a.
Functor f =>
f ()
-> (forall x. f (m x) -> Sem r2 (f x))
-> (forall x. f x -> Maybe x)
-> (forall x. f (m x) -> Sem r (f x))
-> Sem (Tactics f m r2 : r) a
-> Sem r a
runTactics f ()
s (Sem r (f x) -> Sem (effect : r) (f x)
forall (e :: Effect) (r :: [Effect]) a. Sem r a -> Sem (e : r) a
raise (Sem r (f x) -> Sem (effect : r) (f x))
-> (f (Sem rInitial x) -> Sem r (f x))
-> f (Sem rInitial x)
-> Sem (effect : r) (f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sem (Scoped resource effect : r) (f x) -> Sem r (f x)
InterpreterFor (Scoped resource effect) r
run (Sem (Scoped resource effect : r) (f x) -> Sem r (f x))
-> (f (Sem rInitial x) -> Sem (Scoped resource effect : r) (f x))
-> f (Sem rInitial x)
-> Sem r (f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Sem rInitial x) -> Sem (Scoped resource effect : r) (f x)
forall x.
f (Sem rInitial x) -> Sem (Scoped resource effect : r) (f x)
wv) forall x. f x -> Maybe x
ins (Sem (Scoped resource effect : r) (f x) -> Sem r (f x)
InterpreterFor (Scoped resource effect) r
run (Sem (Scoped resource effect : r) (f x) -> Sem r (f x))
-> (f (Sem rInitial x) -> Sem (Scoped resource effect : r) (f x))
-> f (Sem rInitial x)
-> Sem r (f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Sem rInitial x) -> Sem (Scoped resource effect : r) (f x)
forall x.
f (Sem rInitial x) -> Sem (Scoped resource effect : r) (f x)
wv) (resource
-> effect (Sem rInitial) a -> Tactical effect (Sem rInitial) r a
forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Tactical effect (Sem r0) r x
scopedHandler resource
resource effect (Sem rInitial) a
act)
        InScope resource -> Sem rInitial a
main ->
          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 -> Sem r (f a)) -> Sem r (f a)
forall x. (resource -> Sem r x) -> Sem r x
withResource \ resource
resource -> Sem (Scoped resource effect : r) (f a) -> Sem r (f a)
InterpreterFor (Scoped resource effect) r
run (f (Sem rInitial a) -> Sem (Scoped resource effect : r) (f a)
forall x.
f (Sem rInitial x) -> Sem (Scoped resource effect : r) (f x)
wv (resource -> Sem rInitial a
main resource
resource Sem rInitial a -> f () -> f (Sem rInitial a)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s))

-- |Variant of 'runScoped' that takes a handler instead of an interpreter.
interpretScoped ::
  ∀ resource effect r .
  (∀ x . (resource -> Sem r x) -> Sem r x) ->
  (∀ r0 x . resource -> effect (Sem r0) x -> Sem r x) ->
  InterpreterFor (Scoped resource effect) r
interpretScoped :: forall resource (effect :: Effect) (r :: [Effect]).
(forall x. (resource -> Sem r x) -> Sem r x)
-> (forall (r0 :: [Effect]) x.
    resource -> effect (Sem r0) x -> Sem r x)
-> InterpreterFor (Scoped resource effect) r
interpretScoped forall x. (resource -> Sem r x) -> Sem r x
withResource forall (r0 :: [Effect]) x. resource -> effect (Sem r0) x -> Sem r x
scopedHandler =
  (forall x. (resource -> Sem r x) -> Sem r x)
-> (forall (r0 :: [Effect]) x.
    resource -> effect (Sem r0) x -> Tactical effect (Sem r0) r x)
-> InterpreterFor (Scoped resource effect) r
forall resource (effect :: Effect) (r :: [Effect]).
(forall x. (resource -> Sem r x) -> Sem r x)
-> (forall (r0 :: [Effect]) x.
    resource -> effect (Sem r0) x -> Tactical effect (Sem r0) r x)
-> InterpreterFor (Scoped resource effect) r
interpretScopedH forall x. (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 (r0 :: [Effect]) x. resource -> effect (Sem r0) x -> Sem r x
scopedHandler resource
r effect (Sem r0) x
e)

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

-- |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.
interpretScopedResumableH ::
  ∀ resource effect err r .
  (∀ x . (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 resource effect !! err) r
interpretScopedResumableH :: forall resource (effect :: Effect) err (r :: [Effect]).
(forall x.
 (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 resource effect !! err) r
interpretScopedResumableH forall x.
(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 =
  Sem ((Scoped resource effect !! err) : r) a -> Sem r a
InterpreterFor (Scoped resource effect !! err) r
run
  where
    run :: InterpreterFor (Scoped resource effect !! err) r
    run :: InterpreterFor (Scoped resource effect !! err) r
run =
      (forall x.
 Weaving
   (Scoped resource effect !! err)
   (Sem ((Scoped resource effect !! err) : r))
   x
 -> Sem r x)
-> InterpreterFor (Scoped resource effect !! err) r
forall (e :: Effect) (r :: [Effect]).
(forall x. Weaving e (Sem (e : r)) x -> Sem r x)
-> InterpreterFor e r
interpretH' \ (Weaving (Resumable Weaving (Scoped resource effect) (Sem r) a1
inner) f ()
s' forall x.
f (Sem rInitial x)
-> Sem ((Scoped resource effect !! err) : r) (f x)
dist' f a -> x
ex' forall x. f x -> Maybe x
ins') ->
        case Weaving (Scoped resource effect) (Sem r) a1
inner of
          Weaving Scoped resource effect (Sem rInitial) a
effect f ()
s forall x. f (Sem rInitial x) -> Sem r (f x)
dist f a -> a1
ex forall x. f x -> Maybe x
ins -> do
            let
              handleScoped :: Scoped resource effect (Sem rInitial) a
-> Sem
     (WithTactics effect (Compose f f) (Sem rInitial) (Stop err : r))
     (Compose f f a)
handleScoped = \case
                Run resource
resource effect (Sem rInitial) a
act ->
                  resource
-> effect (Sem rInitial) a
-> Tactical effect (Sem rInitial) (Stop err : r) a
forall (r0 :: [Effect]) x.
resource
-> effect (Sem r0) x -> Tactical effect (Sem r0) (Stop err : r) x
scopedHandler resource
resource effect (Sem rInitial) a
act
                InScope resource -> Sem rInitial a
main ->
                  Sem (Stop err : r) (Compose f f a)
-> Sem
     (WithTactics effect (Compose f f) (Sem rInitial) (Stop err : r))
     (Compose f f a)
forall (e :: Effect) (r :: [Effect]) a. Sem r a -> Sem (e : r) a
raise ((resource -> Sem (Stop err : r) (Compose f f a))
-> Sem (Stop err : r) (Compose f f a)
forall x.
(resource -> Sem (Stop err : r) x) -> Sem (Stop err : r) x
withResource \ resource
resource -> f (f a) -> Compose f f a
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (f (f a) -> Compose f f a)
-> Sem (Stop err : r) (f (f a))
-> Sem (Stop err : r) (Compose f f a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sem r (f (f a)) -> Sem (Stop err : r) (f (f a))
forall (e :: Effect) (r :: [Effect]) a. Sem r a -> Sem (e : r) a
raise (Sem ((Scoped resource effect !! err) : r) (f (f a))
-> Sem r (f (f a))
InterpreterFor (Scoped resource effect !! err) r
run (f (Sem rInitial (f a))
-> Sem ((Scoped resource effect !! err) : r) (f (f a))
forall x.
f (Sem rInitial x)
-> Sem ((Scoped resource effect !! err) : r) (f x)
dist' (f (Sem rInitial a) -> Sem r (f a)
forall x. f (Sem rInitial x) -> Sem r (f x)
dist (resource -> Sem rInitial a
main resource
resource 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'))))
              tac :: Sem (Stop err : r) (Compose f f a)
tac =
                Compose f f ()
-> (forall x.
    Compose f f (Sem rInitial x)
    -> Sem (effect : Stop err : r) (Compose f f x))
-> (forall x. Compose f f x -> Maybe x)
-> (forall x.
    Compose f f (Sem rInitial x) -> Sem (Stop err : r) (Compose f f x))
-> Sem
     (WithTactics effect (Compose f f) (Sem rInitial) (Stop err : r))
     (Compose f f a)
-> Sem (Stop err : r) (Compose f f a)
forall (f :: * -> *) (m :: * -> *) (r2 :: [Effect]) (r :: [Effect])
       a.
Functor f =>
f ()
-> (forall x. f (m x) -> Sem r2 (f x))
-> (forall x. f x -> Maybe x)
-> (forall x. f (m x) -> Sem r (f x))
-> Sem (Tactics f m r2 : r) a
-> Sem r a
runTactics
                (f (f ()) -> Compose f f ()
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (f ()
s f () -> f () -> f (f ())
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s'))
                (Sem (Stop err : r) (Compose f f x)
-> Sem (effect : Stop err : r) (Compose f f x)
forall (e :: Effect) (r :: [Effect]) a. Sem r a -> Sem (e : r) a
raise (Sem (Stop err : r) (Compose f f x)
 -> Sem (effect : Stop err : r) (Compose f f x))
-> (Compose f f (Sem rInitial x)
    -> Sem (Stop err : r) (Compose f f x))
-> Compose f f (Sem rInitial x)
-> Sem (effect : Stop err : r) (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sem r (Compose f f x) -> Sem (Stop err : r) (Compose f f x)
forall (e :: Effect) (r :: [Effect]) a. Sem r a -> Sem (e : r) a
raise (Sem r (Compose f f x) -> Sem (Stop err : r) (Compose f f x))
-> (Compose f f (Sem rInitial x) -> Sem r (Compose f f x))
-> Compose f f (Sem rInitial x)
-> Sem (Stop err : r) (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sem ((Scoped resource effect !! err) : r) (Compose f f x)
-> Sem r (Compose f f x)
InterpreterFor (Scoped resource effect !! err) r
run (Sem ((Scoped resource effect !! err) : r) (Compose f f x)
 -> Sem r (Compose f f x))
-> (Compose f f (Sem rInitial x)
    -> Sem ((Scoped resource effect !! err) : r) (Compose f f x))
-> Compose f f (Sem rInitial x)
-> Sem r (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f (f x) -> Compose f f x)
-> Sem ((Scoped resource effect !! err) : r) (f (f x))
-> Sem ((Scoped resource effect !! err) : r) (Compose f f x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (f x) -> Compose f f x
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (Sem ((Scoped resource effect !! err) : r) (f (f x))
 -> Sem ((Scoped resource effect !! err) : r) (Compose f f x))
-> (Compose f f (Sem rInitial x)
    -> Sem ((Scoped resource effect !! err) : r) (f (f x)))
-> Compose f f (Sem rInitial x)
-> Sem ((Scoped resource effect !! err) : r) (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Sem rInitial (f x))
-> Sem ((Scoped resource effect !! err) : r) (f (f x))
forall x.
f (Sem rInitial x)
-> Sem ((Scoped resource effect !! err) : r) (f x)
dist' (f (Sem rInitial (f x))
 -> Sem ((Scoped resource effect !! err) : r) (f (f x)))
-> (Compose f f (Sem rInitial x) -> f (Sem rInitial (f x)))
-> Compose f f (Sem rInitial x)
-> Sem ((Scoped resource effect !! err) : r) (f (f x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f (Sem rInitial x) -> Sem r (f x))
-> f (f (Sem rInitial x)) -> f (Sem r (f x))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (Sem rInitial x) -> Sem r (f x)
forall x. f (Sem rInitial x) -> Sem r (f x)
dist (f (f (Sem rInitial x)) -> f (Sem r (f x)))
-> (Compose f f (Sem rInitial x) -> f (f (Sem rInitial x)))
-> Compose f f (Sem rInitial x)
-> f (Sem r (f x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose f f (Sem rInitial x) -> f (f (Sem rInitial x))
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose)
                (f x -> Maybe x
forall x. f x -> Maybe x
ins (f x -> Maybe x)
-> (Compose f f x -> Maybe (f x)) -> Compose f f x -> Maybe x
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< f (f x) -> Maybe (f x)
forall x. f x -> Maybe x
ins' (f (f x) -> Maybe (f x))
-> (Compose f f x -> f (f x)) -> Compose f f x -> Maybe (f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose f f x -> f (f x)
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose)
                (Sem r (Compose f f x) -> Sem (Stop err : r) (Compose f f x)
forall (e :: Effect) (r :: [Effect]) a. Sem r a -> Sem (e : r) a
raise (Sem r (Compose f f x) -> Sem (Stop err : r) (Compose f f x))
-> (Compose f f (Sem rInitial x) -> Sem r (Compose f f x))
-> Compose f f (Sem rInitial x)
-> Sem (Stop err : r) (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sem ((Scoped resource effect !! err) : r) (Compose f f x)
-> Sem r (Compose f f x)
InterpreterFor (Scoped resource effect !! err) r
run (Sem ((Scoped resource effect !! err) : r) (Compose f f x)
 -> Sem r (Compose f f x))
-> (Compose f f (Sem rInitial x)
    -> Sem ((Scoped resource effect !! err) : r) (Compose f f x))
-> Compose f f (Sem rInitial x)
-> Sem r (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f (f x) -> Compose f f x)
-> Sem ((Scoped resource effect !! err) : r) (f (f x))
-> Sem ((Scoped resource effect !! err) : r) (Compose f f x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (f x) -> Compose f f x
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (Sem ((Scoped resource effect !! err) : r) (f (f x))
 -> Sem ((Scoped resource effect !! err) : r) (Compose f f x))
-> (Compose f f (Sem rInitial x)
    -> Sem ((Scoped resource effect !! err) : r) (f (f x)))
-> Compose f f (Sem rInitial x)
-> Sem ((Scoped resource effect !! err) : r) (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Sem rInitial (f x))
-> Sem ((Scoped resource effect !! err) : r) (f (f x))
forall x.
f (Sem rInitial x)
-> Sem ((Scoped resource effect !! err) : r) (f x)
dist' (f (Sem rInitial (f x))
 -> Sem ((Scoped resource effect !! err) : r) (f (f x)))
-> (Compose f f (Sem rInitial x) -> f (Sem rInitial (f x)))
-> Compose f f (Sem rInitial x)
-> Sem ((Scoped resource effect !! err) : r) (f (f x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f (Sem rInitial x) -> Sem r (f x))
-> f (f (Sem rInitial x)) -> f (Sem r (f x))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (Sem rInitial x) -> Sem r (f x)
forall x. f (Sem rInitial x) -> Sem r (f x)
dist (f (f (Sem rInitial x)) -> f (Sem r (f x)))
-> (Compose f f (Sem rInitial x) -> f (f (Sem rInitial x)))
-> Compose f f (Sem rInitial x)
-> f (Sem r (f x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose f f (Sem rInitial x) -> f (f (Sem rInitial x))
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose)
                (Scoped resource effect (Sem rInitial) a
-> Sem
     (WithTactics effect (Compose f f) (Sem rInitial) (Stop err : r))
     (Compose f f a)
handleScoped Scoped resource effect (Sem rInitial) a
effect)
              exFinal :: Either err (Compose f f a) -> x
exFinal = f a -> x
ex' (f a -> x)
-> (Either err (Compose f f a) -> f a)
-> Either err (Compose f f a)
-> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
                Right (Compose f (f a)
a) -> a1 -> Either err a1
forall a b. b -> Either a b
Right (a1 -> Either err a1) -> (f a -> a1) -> f a -> Either err a1
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> a1
ex (f a -> Either err a1) -> f (f a) -> f (Either err a1)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (f a)
a
                Left err
err -> err -> Either err a1
forall a b. a -> Either a b
Left err
err Either err a1 -> f () -> f (Either err a1)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s'
            Either err (Compose f f a) -> x
exFinal (Either err (Compose f f a) -> x)
-> Sem r (Either err (Compose f f a)) -> Sem r x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sem (Stop err : r) (Compose f f a)
-> Sem r (Either err (Compose f f a))
forall e (r :: [Effect]) a.
Sem (Stop e : r) a -> Sem r (Either e a)
runStop Sem (Stop err : r) (Compose f f a)
tac

-- |Combined interpreter for 'Scoped' and 'Resumable'.
-- This allows 'Stop' to be sent from within the resource allocator so that the consumer receives it.
interpretScopedResumable ::
  ∀ resource effect err r .
  (∀ x . (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 resource effect !! err) r
interpretScopedResumable :: forall resource (effect :: Effect) err (r :: [Effect]).
(forall x.
 (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 resource effect !! err) r
interpretScopedResumable forall x.
(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.
 (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 resource effect !! err) r
forall resource (effect :: Effect) err (r :: [Effect]).
(forall x.
 (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 resource effect !! err) r
interpretScopedResumableH forall x.
(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)

interpretScopedWithH ::
  ∀ extra resource effect r r1 .
  r1 ~ (extra ++ r) =>
  InsertAtIndex 1 '[Scoped resource effect] r1 r (Scoped resource effect : r1) extra =>
  (∀ x . (resource -> Sem r1 x) -> Sem r x) ->
  (∀ m x . resource -> effect m x -> Tactical effect m r1 x) ->
  InterpreterFor (Scoped resource effect) r
interpretScopedWithH :: forall (extra :: [Effect]) resource (effect :: Effect)
       (r :: [Effect]) (r1 :: [Effect]).
(r1 ~ (extra ++ r),
 InsertAtIndex
   1
   '[Scoped resource effect]
   r1
   r
   (Scoped resource effect : r1)
   extra) =>
(forall x. (resource -> Sem r1 x) -> Sem r x)
-> (forall (m :: * -> *) x.
    resource -> effect m x -> Tactical effect m r1 x)
-> InterpreterFor (Scoped resource effect) r
interpretScopedWithH forall x. (resource -> Sem r1 x) -> Sem r x
withResource forall (m :: * -> *) x.
resource -> effect m x -> Tactical effect m r1 x
scopedHandler =
  (forall x.
 Weaving
   (Scoped resource effect) (Sem (Scoped resource effect : r)) x
 -> Sem r x)
-> InterpreterFor (Scoped resource effect) r
forall (e :: Effect) (r :: [Effect]).
(forall x. Weaving e (Sem (e : r)) x -> Sem r x)
-> InterpreterFor e r
interpretH' \case
    Weaving (InScope resource -> Sem rInitial a
main) f ()
s forall x.
f (Sem rInitial x) -> Sem (Scoped resource 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
<$> (resource -> Sem r1 (f a)) -> Sem r (f a)
forall x. (resource -> Sem r1 x) -> Sem r x
withResource \ resource
resource -> Sem (Scoped resource effect : r1) (f a) -> Sem r1 (f a)
InterpreterFor (Scoped resource effect) r1
inScope (forall (index :: Nat) (inserted :: [Effect]) (head :: [Effect])
       (oldTail :: [Effect]) (tail :: [Effect]) (old :: [Effect])
       (full :: [Effect]) a.
(ListOfLength index head, WhenStuck index InsertAtUnprovidedIndex,
 old ~ Append head oldTail, tail ~ Append inserted oldTail,
 full ~ Append head tail,
 InsertAtIndex index head tail oldTail full inserted) =>
Sem old a -> Sem full a
insertAt @1 @extra (f (Sem rInitial a) -> Sem (Scoped resource effect : r) (f a)
forall x.
f (Sem rInitial x) -> Sem (Scoped resource effect : r) (f x)
wv (resource -> Sem rInitial a
main resource
resource Sem rInitial a -> f () -> f (Sem rInitial a)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s)))
    Weaving
  (Scoped resource effect) (Sem (Scoped resource effect : r)) x
_ ->
      [Char] -> Sem r x
forall a. HasCallStack => [Char] -> a
error [Char]
"top level Run"
  where
    inScope :: InterpreterFor (Scoped resource effect) r1
    inScope :: InterpreterFor (Scoped resource effect) r1
inScope =
      (forall x.
 Weaving
   (Scoped resource effect) (Sem (Scoped resource effect : r1)) x
 -> Sem r1 x)
-> InterpreterFor (Scoped resource effect) r1
forall (e :: Effect) (r :: [Effect]).
(forall x. Weaving e (Sem (e : r)) x -> Sem r x)
-> InterpreterFor e r
interpretH' \case
        Weaving (Run resource
resource effect (Sem rInitial) a
act) f ()
s forall x.
f (Sem rInitial x) -> Sem (Scoped resource effect : r1) (f x)
wv f a -> x
ex forall x. f x -> Maybe x
ins ->
          f a -> x
ex (f a -> x) -> Sem r1 (f a) -> Sem r1 x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f ()
-> (forall x. f (Sem rInitial x) -> Sem (effect : r1) (f x))
-> (forall x. f x -> Maybe x)
-> (forall x. f (Sem rInitial x) -> Sem r1 (f x))
-> Sem (Tactics f (Sem rInitial) (effect : r1) : r1) (f a)
-> Sem r1 (f a)
forall (f :: * -> *) (m :: * -> *) (r2 :: [Effect]) (r :: [Effect])
       a.
Functor f =>
f ()
-> (forall x. f (m x) -> Sem r2 (f x))
-> (forall x. f x -> Maybe x)
-> (forall x. f (m x) -> Sem r (f x))
-> Sem (Tactics f m r2 : r) a
-> Sem r a
runTactics f ()
s (Sem r1 (f x) -> Sem (effect : r1) (f x)
forall (e :: Effect) (r :: [Effect]) a. Sem r a -> Sem (e : r) a
raise (Sem r1 (f x) -> Sem (effect : r1) (f x))
-> (f (Sem rInitial x) -> Sem r1 (f x))
-> f (Sem rInitial x)
-> Sem (effect : r1) (f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sem (Scoped resource effect : r1) (f x) -> Sem r1 (f x)
InterpreterFor (Scoped resource effect) r1
inScope (Sem (Scoped resource effect : r1) (f x) -> Sem r1 (f x))
-> (f (Sem rInitial x) -> Sem (Scoped resource effect : r1) (f x))
-> f (Sem rInitial x)
-> Sem r1 (f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Sem rInitial x) -> Sem (Scoped resource effect : r1) (f x)
forall x.
f (Sem rInitial x) -> Sem (Scoped resource effect : r1) (f x)
wv) forall x. f x -> Maybe x
ins (Sem (Scoped resource effect : r1) (f x) -> Sem r1 (f x)
InterpreterFor (Scoped resource effect) r1
inScope (Sem (Scoped resource effect : r1) (f x) -> Sem r1 (f x))
-> (f (Sem rInitial x) -> Sem (Scoped resource effect : r1) (f x))
-> f (Sem rInitial x)
-> Sem r1 (f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Sem rInitial x) -> Sem (Scoped resource effect : r1) (f x)
forall x.
f (Sem rInitial x) -> Sem (Scoped resource effect : r1) (f x)
wv) (resource
-> effect (Sem rInitial) a -> Tactical effect (Sem rInitial) r1 a
forall (m :: * -> *) x.
resource -> effect m x -> Tactical effect m r1 x
scopedHandler resource
resource effect (Sem rInitial) a
act)
        Weaving
  (Scoped resource effect) (Sem (Scoped resource effect : r1)) x
_ ->
          [Char] -> Sem r1 x
forall a. HasCallStack => [Char] -> a
error [Char]
"nested InScope"

interpretScopedWith ::
  ∀ extra resource effect r r1 .
  r1 ~ (extra ++ r) =>
  InsertAtIndex 1 '[Scoped resource effect] r1 r (Scoped resource effect : r1) extra =>
  (∀ x . (resource -> Sem r1 x) -> Sem r x) ->
  (∀ m x . resource -> effect m x -> Sem r1 x) ->
  InterpreterFor (Scoped resource effect) r
interpretScopedWith :: forall (extra :: [Effect]) resource (effect :: Effect)
       (r :: [Effect]) (r1 :: [Effect]).
(r1 ~ (extra ++ r),
 InsertAtIndex
   1
   '[Scoped resource effect]
   r1
   r
   (Scoped resource effect : r1)
   extra) =>
(forall x. (resource -> Sem r1 x) -> Sem r x)
-> (forall (m :: * -> *) x. resource -> effect m x -> Sem r1 x)
-> InterpreterFor (Scoped resource effect) r
interpretScopedWith forall x. (resource -> Sem r1 x) -> Sem r x
withResource forall (m :: * -> *) x. resource -> effect m x -> Sem r1 x
scopedHandler =
  forall (extra :: [Effect]) resource (effect :: Effect)
       (r :: [Effect]) (r1 :: [Effect]).
(r1 ~ (extra ++ r),
 InsertAtIndex
   1
   '[Scoped resource effect]
   r1
   r
   (Scoped resource effect : r1)
   extra) =>
(forall x. (resource -> Sem r1 x) -> Sem r x)
-> (forall (m :: * -> *) x.
    resource -> effect m x -> Tactical effect m r1 x)
-> InterpreterFor (Scoped resource effect) r
interpretScopedWithH @extra forall x. (resource -> Sem r1 x) -> Sem r x
withResource \ resource
r effect m x
e -> Sem r1 x -> Sem (WithTactics effect f m 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 m x -> Sem r1 x
forall (m :: * -> *) x. resource -> effect m x -> Sem r1 x
scopedHandler resource
r effect m x
e)

interpretScopedWith_ ::
  ∀ extra effect r r1 .
  r1 ~ (extra ++ r) =>
  InsertAtIndex 1 '[Scoped () effect] r1 r (Scoped () effect : r1) extra =>
  (∀ x . Sem r1 x -> Sem r x) ->
  (∀ m x . effect m x -> Sem r1 x) ->
  InterpreterFor (Scoped () effect) r
interpretScopedWith_ :: forall (extra :: [Effect]) (effect :: Effect) (r :: [Effect])
       (r1 :: [Effect]).
(r1 ~ (extra ++ r),
 InsertAtIndex
   1 '[Scoped () effect] r1 r (Scoped () effect : r1) extra) =>
(forall x. Sem r1 x -> Sem r x)
-> (forall (m :: * -> *) x. effect m x -> Sem r1 x)
-> InterpreterFor (Scoped () effect) r
interpretScopedWith_ forall x. Sem r1 x -> Sem r x
withResource forall (m :: * -> *) x. effect m x -> Sem r1 x
scopedHandler =
  forall (extra :: [Effect]) resource (effect :: Effect)
       (r :: [Effect]) (r1 :: [Effect]).
(r1 ~ (extra ++ r),
 InsertAtIndex
   1
   '[Scoped resource effect]
   r1
   r
   (Scoped resource effect : r1)
   extra) =>
(forall x. (resource -> Sem r1 x) -> Sem r x)
-> (forall (m :: * -> *) x.
    resource -> effect m x -> Tactical effect m r1 x)
-> InterpreterFor (Scoped resource effect) r
interpretScopedWithH @extra (\ () -> Sem r1 x
f -> Sem r1 x -> Sem r x
forall x. Sem r1 x -> Sem r x
withResource (() -> Sem r1 x
f ())) \ () effect m x
e -> Sem r1 x -> Sem (WithTactics effect f m 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 m x -> Sem r1 x
forall (m :: * -> *) x. effect m x -> Sem r1 x
scopedHandler effect m x
e)

interpretScopedResumableWithH ::
  ∀ extra resource effect err r r1 .
  r1 ~ ((extra ++ '[Stop err]) ++ r) =>
  InsertAtIndex 1 '[Scoped resource effect !! err] r1 r (Scoped resource effect !! err : r1) (extra ++ '[Stop err]) =>
  (∀ x . (resource -> Sem r1 x) -> Sem (Stop err : r) x) ->
  (∀ r0 x . resource -> effect (Sem r0) x -> Tactical effect (Sem r0) r1 x) ->
  InterpreterFor (Scoped resource effect !! err) r
interpretScopedResumableWithH :: forall (extra :: [Effect]) resource (effect :: Effect) err
       (r :: [Effect]) (r1 :: [Effect]).
(r1 ~ ((extra ++ '[Stop err]) ++ r),
 InsertAtIndex
   1
   '[Scoped resource effect !! err]
   r1
   r
   ((Scoped resource effect !! err) : r1)
   (extra ++ '[Stop err])) =>
(forall x. (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 resource effect !! err) r
interpretScopedResumableWithH forall x. (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 =
  Sem ((Scoped resource effect !! err) : r) a -> Sem r a
InterpreterFor (Scoped resource effect !! err) r
run
  where
    run :: InterpreterFor (Scoped resource effect !! err) r
    run :: InterpreterFor (Scoped resource effect !! err) r
run =
      (forall x.
 Weaving
   (Scoped resource effect !! err)
   (Sem ((Scoped resource effect !! err) : r))
   x
 -> Sem r x)
-> InterpreterFor (Scoped resource effect !! err) r
forall (e :: Effect) (r :: [Effect]).
(forall x. Weaving e (Sem (e : r)) x -> Sem r x)
-> InterpreterFor e r
interpretH' \ (Weaving (Resumable Weaving (Scoped resource effect) (Sem r) a1
inner) f ()
s' forall x.
f (Sem rInitial x)
-> Sem ((Scoped resource effect !! err) : r) (f x)
dist' f a -> x
ex' forall x. f x -> Maybe x
ins') ->
        case Weaving (Scoped resource effect) (Sem r) a1
inner of
          Weaving Scoped resource effect (Sem rInitial) a
effect f ()
s forall x. f (Sem rInitial x) -> Sem r (f x)
dist f a -> a1
ex forall x. f x -> Maybe x
ins -> do
            let
              handleScoped :: Scoped resource effect (Sem rInitial) a
-> Sem
     (Tactics (Compose f f) (Sem rInitial) (Any : Any : r)
        : Stop err : r)
     (Compose f f a)
handleScoped = \case
                Run resource
_ effect (Sem rInitial) a
_ ->
                  [Char]
-> Sem
     (Tactics (Compose f f) (Sem rInitial) (Any : Any : r)
        : Stop err : r)
     (Compose f f a)
forall a. HasCallStack => [Char] -> a
error [Char]
"top level Run"
                InScope resource -> Sem rInitial a
main ->
                  Sem (Stop err : r) (Compose f f a)
-> Sem
     (Tactics (Compose f f) (Sem rInitial) (Any : Any : r)
        : Stop err : r)
     (Compose f f a)
forall (e :: Effect) (r :: [Effect]) a. Sem r a -> Sem (e : r) a
raise ((resource -> Sem r1 (Compose f f a))
-> Sem (Stop err : r) (Compose f f a)
forall x. (resource -> Sem r1 x) -> Sem (Stop err : r) x
withResource \ resource
resource -> f (f a) -> Compose f f a
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (f (f a) -> Compose f f a)
-> Sem r1 (f (f a)) -> Sem r1 (Compose f f a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sem ((Scoped resource effect !! err) : r1) (f (f a))
-> Sem r1 (f (f a))
InterpreterFor (Scoped resource effect !! err) r1
inScope (forall (index :: Nat) (inserted :: [Effect]) (head :: [Effect])
       (oldTail :: [Effect]) (tail :: [Effect]) (old :: [Effect])
       (full :: [Effect]) a.
(ListOfLength index head, WhenStuck index InsertAtUnprovidedIndex,
 old ~ Append head oldTail, tail ~ Append inserted oldTail,
 full ~ Append head tail,
 InsertAtIndex index head tail oldTail full inserted) =>
Sem old a -> Sem full a
insertAt @1 @(extra ++ '[Stop err]) (f (Sem rInitial (f a))
-> Sem ((Scoped resource effect !! err) : r) (f (f a))
forall x.
f (Sem rInitial x)
-> Sem ((Scoped resource effect !! err) : r) (f x)
dist' (f (Sem rInitial a) -> Sem r (f a)
forall x. f (Sem rInitial x) -> Sem r (f x)
dist (resource -> Sem rInitial a
main resource
resource 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'))))
              tac :: Sem (Stop err : r) (Compose f f a)
tac =
                Compose f f ()
-> (forall x.
    Compose f f (Sem rInitial x)
    -> Sem (Any : Any : r) (Compose f f x))
-> (forall x. Compose f f x -> Maybe x)
-> (forall x.
    Compose f f (Sem rInitial x) -> Sem (Stop err : r) (Compose f f x))
-> Sem
     (Tactics (Compose f f) (Sem rInitial) (Any : Any : r)
        : Stop err : r)
     (Compose f f a)
-> Sem (Stop err : r) (Compose f f a)
forall (f :: * -> *) (m :: * -> *) (r2 :: [Effect]) (r :: [Effect])
       a.
Functor f =>
f ()
-> (forall x. f (m x) -> Sem r2 (f x))
-> (forall x. f x -> Maybe x)
-> (forall x. f (m x) -> Sem r (f x))
-> Sem (Tactics f m r2 : r) a
-> Sem r a
runTactics
                (f (f ()) -> Compose f f ()
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (f ()
s f () -> f () -> f (f ())
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s'))
                (Sem (Any : r) (Compose f f x)
-> Sem (Any : Any : r) (Compose f f x)
forall (e :: Effect) (r :: [Effect]) a. Sem r a -> Sem (e : r) a
raise (Sem (Any : r) (Compose f f x)
 -> Sem (Any : Any : r) (Compose f f x))
-> (Compose f f (Sem rInitial x) -> Sem (Any : r) (Compose f f x))
-> Compose f f (Sem rInitial x)
-> Sem (Any : Any : r) (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sem r (Compose f f x) -> Sem (Any : r) (Compose f f x)
forall (e :: Effect) (r :: [Effect]) a. Sem r a -> Sem (e : r) a
raise (Sem r (Compose f f x) -> Sem (Any : r) (Compose f f x))
-> (Compose f f (Sem rInitial x) -> Sem r (Compose f f x))
-> Compose f f (Sem rInitial x)
-> Sem (Any : r) (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sem ((Scoped resource effect !! err) : r) (Compose f f x)
-> Sem r (Compose f f x)
InterpreterFor (Scoped resource effect !! err) r
run (Sem ((Scoped resource effect !! err) : r) (Compose f f x)
 -> Sem r (Compose f f x))
-> (Compose f f (Sem rInitial x)
    -> Sem ((Scoped resource effect !! err) : r) (Compose f f x))
-> Compose f f (Sem rInitial x)
-> Sem r (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f (f x) -> Compose f f x)
-> Sem ((Scoped resource effect !! err) : r) (f (f x))
-> Sem ((Scoped resource effect !! err) : r) (Compose f f x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (f x) -> Compose f f x
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (Sem ((Scoped resource effect !! err) : r) (f (f x))
 -> Sem ((Scoped resource effect !! err) : r) (Compose f f x))
-> (Compose f f (Sem rInitial x)
    -> Sem ((Scoped resource effect !! err) : r) (f (f x)))
-> Compose f f (Sem rInitial x)
-> Sem ((Scoped resource effect !! err) : r) (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Sem rInitial (f x))
-> Sem ((Scoped resource effect !! err) : r) (f (f x))
forall x.
f (Sem rInitial x)
-> Sem ((Scoped resource effect !! err) : r) (f x)
dist' (f (Sem rInitial (f x))
 -> Sem ((Scoped resource effect !! err) : r) (f (f x)))
-> (Compose f f (Sem rInitial x) -> f (Sem rInitial (f x)))
-> Compose f f (Sem rInitial x)
-> Sem ((Scoped resource effect !! err) : r) (f (f x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f (Sem rInitial x) -> Sem r (f x))
-> f (f (Sem rInitial x)) -> f (Sem r (f x))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (Sem rInitial x) -> Sem r (f x)
forall x. f (Sem rInitial x) -> Sem r (f x)
dist (f (f (Sem rInitial x)) -> f (Sem r (f x)))
-> (Compose f f (Sem rInitial x) -> f (f (Sem rInitial x)))
-> Compose f f (Sem rInitial x)
-> f (Sem r (f x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose f f (Sem rInitial x) -> f (f (Sem rInitial x))
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose)
                (f x -> Maybe x
forall x. f x -> Maybe x
ins (f x -> Maybe x)
-> (Compose f f x -> Maybe (f x)) -> Compose f f x -> Maybe x
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< f (f x) -> Maybe (f x)
forall x. f x -> Maybe x
ins' (f (f x) -> Maybe (f x))
-> (Compose f f x -> f (f x)) -> Compose f f x -> Maybe (f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose f f x -> f (f x)
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose)
                (Sem r (Compose f f x) -> Sem (Stop err : r) (Compose f f x)
forall (e :: Effect) (r :: [Effect]) a. Sem r a -> Sem (e : r) a
raise (Sem r (Compose f f x) -> Sem (Stop err : r) (Compose f f x))
-> (Compose f f (Sem rInitial x) -> Sem r (Compose f f x))
-> Compose f f (Sem rInitial x)
-> Sem (Stop err : r) (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sem ((Scoped resource effect !! err) : r) (Compose f f x)
-> Sem r (Compose f f x)
InterpreterFor (Scoped resource effect !! err) r
run (Sem ((Scoped resource effect !! err) : r) (Compose f f x)
 -> Sem r (Compose f f x))
-> (Compose f f (Sem rInitial x)
    -> Sem ((Scoped resource effect !! err) : r) (Compose f f x))
-> Compose f f (Sem rInitial x)
-> Sem r (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f (f x) -> Compose f f x)
-> Sem ((Scoped resource effect !! err) : r) (f (f x))
-> Sem ((Scoped resource effect !! err) : r) (Compose f f x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (f x) -> Compose f f x
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (Sem ((Scoped resource effect !! err) : r) (f (f x))
 -> Sem ((Scoped resource effect !! err) : r) (Compose f f x))
-> (Compose f f (Sem rInitial x)
    -> Sem ((Scoped resource effect !! err) : r) (f (f x)))
-> Compose f f (Sem rInitial x)
-> Sem ((Scoped resource effect !! err) : r) (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Sem rInitial (f x))
-> Sem ((Scoped resource effect !! err) : r) (f (f x))
forall x.
f (Sem rInitial x)
-> Sem ((Scoped resource effect !! err) : r) (f x)
dist' (f (Sem rInitial (f x))
 -> Sem ((Scoped resource effect !! err) : r) (f (f x)))
-> (Compose f f (Sem rInitial x) -> f (Sem rInitial (f x)))
-> Compose f f (Sem rInitial x)
-> Sem ((Scoped resource effect !! err) : r) (f (f x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f (Sem rInitial x) -> Sem r (f x))
-> f (f (Sem rInitial x)) -> f (Sem r (f x))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (Sem rInitial x) -> Sem r (f x)
forall x. f (Sem rInitial x) -> Sem r (f x)
dist (f (f (Sem rInitial x)) -> f (Sem r (f x)))
-> (Compose f f (Sem rInitial x) -> f (f (Sem rInitial x)))
-> Compose f f (Sem rInitial x)
-> f (Sem r (f x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose f f (Sem rInitial x) -> f (f (Sem rInitial x))
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose)
                (Scoped resource effect (Sem rInitial) a
-> Sem
     (Tactics (Compose f f) (Sem rInitial) (Any : Any : r)
        : Stop err : r)
     (Compose f f a)
handleScoped Scoped resource effect (Sem rInitial) a
effect)
              exFinal :: Either err (Compose f f a) -> x
exFinal = f a -> x
ex' (f a -> x)
-> (Either err (Compose f f a) -> f a)
-> Either err (Compose f f a)
-> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
                Right (Compose f (f a)
a) -> a1 -> Either err a1
forall a b. b -> Either a b
Right (a1 -> Either err a1) -> (f a -> a1) -> f a -> Either err a1
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> a1
ex (f a -> Either err a1) -> f (f a) -> f (Either err a1)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (f a)
a
                Left err
err -> err -> Either err a1
forall a b. a -> Either a b
Left err
err Either err a1 -> f () -> f (Either err a1)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s'
            Either err (Compose f f a) -> x
exFinal (Either err (Compose f f a) -> x)
-> Sem r (Either err (Compose f f a)) -> Sem r x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sem (Stop err : r) (Compose f f a)
-> Sem r (Either err (Compose f f a))
forall e (r :: [Effect]) a.
Sem (Stop e : r) a -> Sem r (Either e a)
runStop Sem (Stop err : r) (Compose f f a)
tac
    inScope :: InterpreterFor (Scoped resource effect !! err) r1
    inScope :: InterpreterFor (Scoped resource effect !! err) r1
inScope =
      (forall x.
 Weaving
   (Scoped resource effect !! err)
   (Sem ((Scoped resource effect !! err) : r1))
   x
 -> Sem r1 x)
-> InterpreterFor (Scoped resource effect !! err) r1
forall (e :: Effect) (r :: [Effect]).
(forall x. Weaving e (Sem (e : r)) x -> Sem r x)
-> InterpreterFor e r
interpretH' \ (Weaving (Resumable Weaving (Scoped resource effect) (Sem r) a1
inner) f ()
s' forall x.
f (Sem rInitial x)
-> Sem ((Scoped resource effect !! err) : r1) (f x)
dist' f a -> x
ex' forall x. f x -> Maybe x
ins') ->
        case Weaving (Scoped resource effect) (Sem r) a1
inner of
          Weaving Scoped resource effect (Sem rInitial) a
effect f ()
s forall x. f (Sem rInitial x) -> Sem r (f x)
dist f a -> a1
ex forall x. f x -> Maybe x
ins -> do
            let
              handleScoped :: Scoped resource effect (Sem rInitial) a
-> Sem
     (WithTactics effect (Compose f f) (Sem rInitial) r1)
     (Compose f f a)
handleScoped = \case
                Run resource
resource effect (Sem rInitial) a
act ->
                  resource
-> effect (Sem rInitial) a -> Tactical effect (Sem rInitial) r1 a
forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Tactical effect (Sem r0) r1 x
scopedHandler resource
resource effect (Sem rInitial) a
act
                InScope resource -> Sem rInitial a
_ ->
                  [Char]
-> Sem
     (WithTactics effect (Compose f f) (Sem rInitial) r1)
     (Compose f f a)
forall a. HasCallStack => [Char] -> a
error [Char]
"nested InScope"
              tac :: Sem r1 (Compose f f a)
tac =
                Compose f f ()
-> (forall x.
    Compose f f (Sem rInitial x) -> Sem (effect : r1) (Compose f f x))
-> (forall x. Compose f f x -> Maybe x)
-> (forall x.
    Compose f f (Sem rInitial x) -> Sem r1 (Compose f f x))
-> Sem
     (WithTactics effect (Compose f f) (Sem rInitial) r1)
     (Compose f f a)
-> Sem r1 (Compose f f a)
forall (f :: * -> *) (m :: * -> *) (r2 :: [Effect]) (r :: [Effect])
       a.
Functor f =>
f ()
-> (forall x. f (m x) -> Sem r2 (f x))
-> (forall x. f x -> Maybe x)
-> (forall x. f (m x) -> Sem r (f x))
-> Sem (Tactics f m r2 : r) a
-> Sem r a
runTactics
                (f (f ()) -> Compose f f ()
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (f ()
s f () -> f () -> f (f ())
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s'))
                (Sem r1 (Compose f f x) -> Sem (effect : r1) (Compose f f x)
forall (e :: Effect) (r :: [Effect]) a. Sem r a -> Sem (e : r) a
raise (Sem r1 (Compose f f x) -> Sem (effect : r1) (Compose f f x))
-> (Compose f f (Sem rInitial x) -> Sem r1 (Compose f f x))
-> Compose f f (Sem rInitial x)
-> Sem (effect : r1) (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sem ((Scoped resource effect !! err) : r1) (Compose f f x)
-> Sem r1 (Compose f f x)
InterpreterFor (Scoped resource effect !! err) r1
inScope (Sem ((Scoped resource effect !! err) : r1) (Compose f f x)
 -> Sem r1 (Compose f f x))
-> (Compose f f (Sem rInitial x)
    -> Sem ((Scoped resource effect !! err) : r1) (Compose f f x))
-> Compose f f (Sem rInitial x)
-> Sem r1 (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f (f x) -> Compose f f x)
-> Sem ((Scoped resource effect !! err) : r1) (f (f x))
-> Sem ((Scoped resource effect !! err) : r1) (Compose f f x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (f x) -> Compose f f x
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (Sem ((Scoped resource effect !! err) : r1) (f (f x))
 -> Sem ((Scoped resource effect !! err) : r1) (Compose f f x))
-> (Compose f f (Sem rInitial x)
    -> Sem ((Scoped resource effect !! err) : r1) (f (f x)))
-> Compose f f (Sem rInitial x)
-> Sem ((Scoped resource effect !! err) : r1) (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Sem rInitial (f x))
-> Sem ((Scoped resource effect !! err) : r1) (f (f x))
forall x.
f (Sem rInitial x)
-> Sem ((Scoped resource effect !! err) : r1) (f x)
dist' (f (Sem rInitial (f x))
 -> Sem ((Scoped resource effect !! err) : r1) (f (f x)))
-> (Compose f f (Sem rInitial x) -> f (Sem rInitial (f x)))
-> Compose f f (Sem rInitial x)
-> Sem ((Scoped resource effect !! err) : r1) (f (f x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f (Sem rInitial x) -> Sem r (f x))
-> f (f (Sem rInitial x)) -> f (Sem r (f x))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (Sem rInitial x) -> Sem r (f x)
forall x. f (Sem rInitial x) -> Sem r (f x)
dist (f (f (Sem rInitial x)) -> f (Sem r (f x)))
-> (Compose f f (Sem rInitial x) -> f (f (Sem rInitial x)))
-> Compose f f (Sem rInitial x)
-> f (Sem r (f x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose f f (Sem rInitial x) -> f (f (Sem rInitial x))
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose)
                (f x -> Maybe x
forall x. f x -> Maybe x
ins (f x -> Maybe x)
-> (Compose f f x -> Maybe (f x)) -> Compose f f x -> Maybe x
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< f (f x) -> Maybe (f x)
forall x. f x -> Maybe x
ins' (f (f x) -> Maybe (f x))
-> (Compose f f x -> f (f x)) -> Compose f f x -> Maybe (f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose f f x -> f (f x)
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose)
                (Sem ((Scoped resource effect !! err) : r1) (Compose f f x)
-> Sem r1 (Compose f f x)
InterpreterFor (Scoped resource effect !! err) r1
inScope (Sem ((Scoped resource effect !! err) : r1) (Compose f f x)
 -> Sem r1 (Compose f f x))
-> (Compose f f (Sem rInitial x)
    -> Sem ((Scoped resource effect !! err) : r1) (Compose f f x))
-> Compose f f (Sem rInitial x)
-> Sem r1 (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f (f x) -> Compose f f x)
-> Sem ((Scoped resource effect !! err) : r1) (f (f x))
-> Sem ((Scoped resource effect !! err) : r1) (Compose f f x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (f x) -> Compose f f x
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (Sem ((Scoped resource effect !! err) : r1) (f (f x))
 -> Sem ((Scoped resource effect !! err) : r1) (Compose f f x))
-> (Compose f f (Sem rInitial x)
    -> Sem ((Scoped resource effect !! err) : r1) (f (f x)))
-> Compose f f (Sem rInitial x)
-> Sem ((Scoped resource effect !! err) : r1) (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Sem rInitial (f x))
-> Sem ((Scoped resource effect !! err) : r1) (f (f x))
forall x.
f (Sem rInitial x)
-> Sem ((Scoped resource effect !! err) : r1) (f x)
dist' (f (Sem rInitial (f x))
 -> Sem ((Scoped resource effect !! err) : r1) (f (f x)))
-> (Compose f f (Sem rInitial x) -> f (Sem rInitial (f x)))
-> Compose f f (Sem rInitial x)
-> Sem ((Scoped resource effect !! err) : r1) (f (f x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f (Sem rInitial x) -> Sem r (f x))
-> f (f (Sem rInitial x)) -> f (Sem r (f x))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (Sem rInitial x) -> Sem r (f x)
forall x. f (Sem rInitial x) -> Sem r (f x)
dist (f (f (Sem rInitial x)) -> f (Sem r (f x)))
-> (Compose f f (Sem rInitial x) -> f (f (Sem rInitial x)))
-> Compose f f (Sem rInitial x)
-> f (Sem r (f x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose f f (Sem rInitial x) -> f (f (Sem rInitial x))
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose)
                (Scoped resource effect (Sem rInitial) a
-> Sem
     (WithTactics effect (Compose f f) (Sem rInitial) r1)
     (Compose f f a)
handleScoped Scoped resource effect (Sem rInitial) a
effect)
              exFinal :: Either err (Compose f f a) -> x
exFinal = f a -> x
ex' (f a -> x)
-> (Either err (Compose f f a) -> f a)
-> Either err (Compose f f a)
-> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
                Right (Compose f (f a)
a) -> a1 -> Either err a1
forall a b. b -> Either a b
Right (a1 -> Either err a1) -> (f a -> a1) -> f a -> Either err a1
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> a1
ex (f a -> Either err a1) -> f (f a) -> f (Either err a1)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (f a)
a
                Left err
err -> err -> Either err a1
forall a b. a -> Either a b
Left err
err Either err a1 -> f () -> f (Either err a1)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s'
            Either err (Compose f f a) -> x
exFinal (Either err (Compose f f a) -> x)
-> Sem r1 (Either err (Compose f f a)) -> Sem r1 x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sem (Stop err : r1) (Compose f f a)
-> Sem r1 (Either err (Compose f f a))
forall e (r :: [Effect]) a.
Sem (Stop e : r) a -> Sem r (Either e a)
runStop (Sem r1 (Compose f f a) -> Sem (Stop err : r1) (Compose f f a)
forall (e :: Effect) (r :: [Effect]) a. Sem r a -> Sem (e : r) a
raise Sem r1 (Compose f f a)
tac)

interpretScopedResumableWith ::
  ∀ extra resource effect err r r1 .
  r1 ~ ((extra ++ '[Stop err]) ++ r) =>
  InsertAtIndex 1 '[Scoped resource effect !! err] r1 r (Scoped resource effect !! err : r1) (extra ++ '[Stop err]) =>
  (∀ x . (resource -> Sem r1 x) -> Sem (Stop err : r) x) ->
  (∀ r0 x . resource -> effect (Sem r0) x -> Sem r1 x) ->
  InterpreterFor (Scoped resource effect !! err) r
interpretScopedResumableWith :: forall (extra :: [Effect]) resource (effect :: Effect) err
       (r :: [Effect]) (r1 :: [Effect]).
(r1 ~ ((extra ++ '[Stop err]) ++ r),
 InsertAtIndex
   1
   '[Scoped resource effect !! err]
   r1
   r
   ((Scoped resource effect !! err) : r1)
   (extra ++ '[Stop err])) =>
(forall x. (resource -> Sem r1 x) -> Sem (Stop err : r) x)
-> (forall (r0 :: [Effect]) x.
    resource -> effect (Sem r0) x -> Sem r1 x)
-> InterpreterFor (Scoped resource effect !! err) r
interpretScopedResumableWith forall x. (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]) resource (effect :: Effect) err
       (r :: [Effect]) (r1 :: [Effect]).
(r1 ~ ((extra ++ '[Stop err]) ++ r),
 InsertAtIndex
   1
   '[Scoped resource effect !! err]
   r1
   r
   ((Scoped resource effect !! err) : r1)
   (extra ++ '[Stop err])) =>
(forall x. (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 resource effect !! err) r
interpretScopedResumableWithH @extra forall x. (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)

interpretScopedResumableWith_ ::
  ∀ extra effect err r r1 .
  r1 ~ ((extra ++ '[Stop err]) ++ r) =>
  InsertAtIndex 1 '[Scoped () effect !! err] r1 r (Scoped () effect !! err : r1) (extra ++ '[Stop err]) =>
  (∀ x . Sem r1 x -> Sem (Stop err : r) x) ->
  (∀ r0 x . effect (Sem r0) x -> Sem r1 x) ->
  InterpreterFor (Scoped () effect !! err) r
interpretScopedResumableWith_ :: forall (extra :: [Effect]) (effect :: Effect) err (r :: [Effect])
       (r1 :: [Effect]).
(r1 ~ ((extra ++ '[Stop err]) ++ r),
 InsertAtIndex
   1
   '[Scoped () effect !! err]
   r1
   r
   ((Scoped () effect !! err) : r1)
   (extra ++ '[Stop err])) =>
(forall x. Sem r1 x -> Sem (Stop err : r) x)
-> (forall (r0 :: [Effect]) x. effect (Sem r0) x -> Sem r1 x)
-> InterpreterFor (Scoped () effect !! err) r
interpretScopedResumableWith_ forall x. Sem r1 x -> Sem (Stop err : r) x
withResource forall (r0 :: [Effect]) x. effect (Sem r0) x -> Sem r1 x
scopedHandler =
  forall (extra :: [Effect]) resource (effect :: Effect) err
       (r :: [Effect]) (r1 :: [Effect]).
(r1 ~ ((extra ++ '[Stop err]) ++ r),
 InsertAtIndex
   1
   '[Scoped resource effect !! err]
   r1
   r
   ((Scoped resource effect !! err) : r1)
   (extra ++ '[Stop err])) =>
(forall x. (resource -> Sem r1 x) -> Sem (Stop err : r) x)
-> (forall (r0 :: [Effect]) x.
    resource -> effect (Sem r0) x -> Sem r1 x)
-> InterpreterFor (Scoped resource effect !! err) r
interpretScopedResumableWith @extra (\ () -> Sem r1 x
f -> Sem r1 x -> Sem (Stop err : r) x
forall x. Sem r1 x -> Sem (Stop err : r) x
withResource (() -> 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)