{-# options_haddock prune #-}

-- |Description: Interpreters for 'Scoped' in combination with 'Resumable'
--
-- @since 0.6.0.0
module Polysemy.Resume.Interpreter.Scoped where

import GHC.Err (errorWithoutStackTrace)
import Polysemy.Internal (liftSem, restack)
import Polysemy.Internal.Combinators (interpretWeaving)
import Polysemy.Internal.Scoped (OuterRun (OuterRun), Scoped (InScope, Run))
import Polysemy.Internal.Sing (KnownList (singList))
import Polysemy.Internal.Tactics (liftT)
import Polysemy.Internal.Union (Weaving (Weaving), injWeaving, injectMembership, weave)
import Polysemy.Opaque (Opaque (Opaque))
import Polysemy.Scoped (runScopedNew)

import Polysemy.Resume.Effect.Resumable (Resumable (Resumable), type (!!))
import Polysemy.Resume.Effect.Stop (Stop)
import Polysemy.Resume.Interpreter.Resumable (interpretResumableH)
import Polysemy.Resume.Interpreter.Stop (runStop)

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 :: EffectRow).
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' =
  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a -> b) -> a -> b
$ f (Either err a) -> x
ex forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
    Right f (f' a')
a -> forall a b. b -> Either a b
Right forall b c a. (b -> c) -> (a -> b) -> a -> c
. f' a' -> a
ex' forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (f' a')
a
    Left err
err -> forall a b. a -> Either a b
Left err
err forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s
{-# inline exResumable #-}

runScopedResumable ::
  ∀ param effect err r .
  (∀ q. param -> InterpreterFor effect (Stop err : Opaque q : r)) ->
  InterpreterFor (Scoped param effect !! err) r
runScopedResumable :: forall param (effect :: Effect) err (r :: EffectRow).
(forall (q :: Effect).
 param -> InterpreterFor effect (Stop err : Opaque q : r))
-> InterpreterFor (Scoped param effect !! err) r
runScopedResumable forall (q :: Effect).
param -> InterpreterFor effect (Stop err : Opaque q : r)
h =
  forall (e :: Effect) (r :: EffectRow).
(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
_)) 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 (Sem rInitial) a
effect of
    Run Word
w effect (Sem rInitial) a
_ -> forall a. [Char] -> a
errorWithoutStackTrace forall a b. (a -> b) -> a -> b
$ [Char]
"top level run with depth " forall a. [a] -> [a] -> [a]
++ forall b a. (Show a, IsString b) => a -> b
show Word
w
    InScope param
param Word -> Sem rInitial a
main ->
      forall x.
f (Sem rInitial x) -> Sem ((Scoped param effect !! err) : r) (f x)
wv (forall x. f (Sem rInitial x) -> Sem r (f x)
wv' (Word -> Sem rInitial a
main Word
0 forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s') forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s)
        forall a b. a -> (a -> b) -> b
& forall (e2 :: Effect) (e3 :: Effect) (e1 :: Effect)
       (r :: EffectRow) a.
Sem (e1 : r) a -> Sem (e1 : e2 : e3 : r) a
raiseUnder2
        forall a b. a -> (a -> b) -> b
& Word
-> InterpreterFor
     (Scoped param effect !! err)
     (effect : Opaque (OuterRun effect) : r)
go Word
0
        forall a b. a -> (a -> b) -> b
& forall (e2 :: Effect) (e1 :: Effect) (r :: EffectRow) a.
Sem (e1 : r) a -> Sem (e1 : e2 : r) a
raiseUnder
        forall a b. a -> (a -> b) -> b
& forall (q :: Effect).
param -> InterpreterFor effect (Stop err : Opaque q : r)
h param
param
        forall a b. a -> (a -> b) -> b
& forall err (r :: EffectRow) a.
Sem (Stop err : r) a -> Sem r (Either err a)
runStop
        forall a b. a -> (a -> b) -> b
& forall (e :: Effect) (r :: EffectRow) a.
(forall (rInitial :: EffectRow) x.
 e (Sem rInitial) x -> Tactical e (Sem rInitial) r x)
-> Sem (e : r) a -> Sem r a
interpretH (\(Opaque (OuterRun Word
w effect (Sem rInitial) x
_)) ->
            forall a. [Char] -> a
errorWithoutStackTrace forall a b. (a -> b) -> a -> b
$ [Char]
"unhandled OuterRun with depth " forall a. [a] -> [a] -> [a]
++ forall b a. (Show a, IsString b) => a -> b
show Word
w)
        forall a b. a -> (a -> b) -> b
& forall {k} (f :: * -> *) err a x (f' :: k -> *) (a' :: k)
       (r :: EffectRow).
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
ex f a -> a1
ex'
  where
    go' ::
      Word ->
      InterpreterFor (Opaque (OuterRun effect)) (effect : Opaque (OuterRun effect) : r)
    go' :: Word
-> InterpreterFor
     (Opaque (OuterRun effect)) (effect : Opaque (OuterRun effect) : r)
go' Word
depth =
      forall (e :: Effect) (r :: EffectRow).
(forall x. Weaving e (Sem (e : r)) x -> Sem r x)
-> InterpreterFor e r
interpretWeaving \ (Weaving sr :: Opaque (OuterRun effect) (Sem rInitial) a
sr@(Opaque (OuterRun Word
w effect (Sem rInitial) a
act)) f ()
s forall x.
f (Sem rInitial x)
-> Sem
     (Opaque (OuterRun effect) : effect : Opaque (OuterRun effect) : r)
     (f x)
wv f a -> x
ex forall x. f x -> Maybe x
ins) ->
        if Word
w forall a. Eq a => a -> a -> Bool
== Word
depth then
          forall (r :: EffectRow) a. Union r (Sem r) a -> Sem r a
liftSem forall a b. (a -> b) -> a -> b
$ forall (e :: Effect) (r :: EffectRow) (m :: * -> *) a.
Member e r =>
Weaving e m a -> Union r m a
injWeaving forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) (e :: Effect) (rInitial :: EffectRow) a
       resultType (mAfter :: * -> *).
Functor f =>
e (Sem rInitial) a
-> f ()
-> (forall x. f (Sem rInitial x) -> mAfter (f x))
-> (f a -> resultType)
-> (forall x. f x -> Maybe x)
-> Weaving e mAfter resultType
Weaving effect (Sem rInitial) a
act f ()
s (Word
-> InterpreterFor
     (Opaque (OuterRun effect)) (effect : Opaque (OuterRun effect) : r)
go' Word
depth forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall x.
f (Sem rInitial x)
-> Sem
     (Opaque (OuterRun effect) : effect : Opaque (OuterRun effect) : r)
     (f x)
wv) f a -> x
ex forall x. f x -> Maybe x
ins
        else
          forall (r :: EffectRow) a. Union r (Sem r) a -> Sem r a
liftSem forall a b. (a -> b) -> a -> b
$ forall (e :: Effect) (r :: EffectRow) (m :: * -> *) a.
Member e r =>
Weaving e m a -> Union r m a
injWeaving forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) (e :: Effect) (rInitial :: EffectRow) a
       resultType (mAfter :: * -> *).
Functor f =>
e (Sem rInitial) a
-> f ()
-> (forall x. f (Sem rInitial x) -> mAfter (f x))
-> (f a -> resultType)
-> (forall x. f x -> Maybe x)
-> Weaving e mAfter resultType
Weaving Opaque (OuterRun effect) (Sem rInitial) a
sr f ()
s (Word
-> InterpreterFor
     (Opaque (OuterRun effect)) (effect : Opaque (OuterRun effect) : r)
go' Word
depth forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall x.
f (Sem rInitial x)
-> Sem
     (Opaque (OuterRun effect) : effect : Opaque (OuterRun effect) : r)
     (f x)
wv) f a -> x
ex forall x. f x -> Maybe x
ins
    go ::
      Word ->
      InterpreterFor (Scoped param effect !! err) (effect : Opaque (OuterRun effect) : r)
    go :: Word
-> InterpreterFor
     (Scoped param effect !! err)
     (effect : Opaque (OuterRun effect) : r)
go Word
depth =
      forall (e :: Effect) (r :: EffectRow).
(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 : Opaque (OuterRun 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 Word
w effect (Sem rInitial) a
act
          | Word
w forall a. Eq a => a -> a -> Bool
== Word
depth ->
            f a -> x
ex forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. b -> Either a b
Right forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (r :: EffectRow) a. Union r (Sem r) a -> Sem r a
liftSem (forall (s :: * -> *) (n :: * -> *) (m :: * -> *) (r :: EffectRow)
       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 (Word
-> InterpreterFor
     (Scoped param effect !! err)
     (effect : Opaque (OuterRun effect) : r)
go Word
depth forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall x.
f (Sem rInitial x)
-> Sem
     ((Scoped param effect !! err)
        : effect : Opaque (OuterRun effect) : r)
     (f x)
wv) forall x. f x -> Maybe x
ins (forall (e :: Effect) (r :: EffectRow) (m :: * -> *) a.
Member e r =>
Weaving e m a -> Union r m a
injWeaving (forall (f :: * -> *) (e :: Effect) (rInitial :: EffectRow) a
       resultType (mAfter :: * -> *).
Functor f =>
e (Sem rInitial) a
-> f ()
-> (forall x. f (Sem rInitial x) -> mAfter (f x))
-> (f a -> resultType)
-> (forall x. f x -> Maybe x)
-> Weaving e mAfter resultType
Weaving effect (Sem rInitial) a
act f ()
s' forall x. f (Sem rInitial x) -> Sem r (f x)
wv' f a -> a1
ex' forall x. f x -> Maybe x
ins')))
          | Bool
otherwise ->
            f a -> x
ex forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. b -> Either a b
Right forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (r :: EffectRow) a. Union r (Sem r) a -> Sem r a
liftSem (forall (s :: * -> *) (n :: * -> *) (m :: * -> *) (r :: EffectRow)
       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 (Word
-> InterpreterFor
     (Scoped param effect !! err)
     (effect : Opaque (OuterRun effect) : r)
go Word
depth forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall x.
f (Sem rInitial x)
-> Sem
     ((Scoped param effect !! err)
        : effect : Opaque (OuterRun effect) : r)
     (f x)
wv) forall x. f x -> Maybe x
ins (forall (e :: Effect) (r :: EffectRow) (m :: * -> *) a.
Member e r =>
Weaving e m a -> Union r m a
injWeaving (forall (f :: * -> *) (e :: Effect) (rInitial :: EffectRow) a
       resultType (mAfter :: * -> *).
Functor f =>
e (Sem rInitial) a
-> f ()
-> (forall x. f (Sem rInitial x) -> mAfter (f x))
-> (f a -> resultType)
-> (forall x. f x -> Maybe x)
-> Weaving e mAfter resultType
Weaving (forall (e :: Effect) (m :: * -> *) a. e m a -> Opaque e m a
Opaque (forall (effect :: Effect) (a :: * -> *) b.
Word -> effect a b -> OuterRun effect a b
OuterRun Word
w effect (Sem rInitial) a
act)) f ()
s' 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 Word -> Sem rInitial a
main -> do
          let !depth' :: Word
depth' = Word
depth forall a. Num a => a -> a -> a
+ Word
1
          forall x.
f (Sem rInitial x)
-> Sem
     ((Scoped param effect !! err)
        : effect : Opaque (OuterRun effect) : r)
     (f x)
wv (forall x. f (Sem rInitial x) -> Sem r (f x)
wv' (Word -> Sem rInitial a
main Word
depth' forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s') forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s)
            forall a b. a -> (a -> b) -> b
& Word
-> InterpreterFor
     (Scoped param effect !! err)
     (effect : Opaque (OuterRun effect) : r)
go Word
depth'
            forall a b. a -> (a -> b) -> b
& forall (e2 :: Effect) (e1 :: Effect) (r :: EffectRow) a.
Sem (e1 : r) a -> Sem (e1 : e2 : r) a
raiseUnder
            forall a b. a -> (a -> b) -> b
& forall (q :: Effect).
param -> InterpreterFor effect (Stop err : Opaque q : r)
h param
param
            forall a b. a -> (a -> b) -> b
& forall err (r :: EffectRow) a.
Sem (Stop err : r) a -> Sem r (Either err a)
runStop
            forall a b. a -> (a -> b) -> b
& forall (e2 :: Effect) (e3 :: Effect) (e1 :: Effect)
       (r :: EffectRow) a.
Sem (e1 : r) a -> Sem (e1 : e2 : e3 : r) a
raiseUnder2
            forall a b. a -> (a -> b) -> b
& Word
-> InterpreterFor
     (Opaque (OuterRun effect)) (effect : Opaque (OuterRun effect) : r)
go' Word
depth
            forall a b. a -> (a -> b) -> b
& forall {k} (f :: * -> *) err a x (f' :: k -> *) (a' :: k)
       (r :: EffectRow).
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
ex f a -> a1
ex'
{-# inline runScopedResumable #-}

-- |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 .
  (∀ q x . param -> (resource -> Sem (Stop err : Opaque q : r) x) -> Sem (Stop err : Opaque q : r) x) ->
  (∀ q r0 x . resource -> effect (Sem r0) x -> Tactical effect (Sem r0) (Stop err : Opaque q : r) x) ->
  InterpreterFor (Scoped param effect !! err) r
interpretScopedResumableH :: forall param resource (effect :: Effect) err (r :: EffectRow).
(forall (q :: Effect) x.
 param
 -> (resource -> Sem (Stop err : Opaque q : r) x)
 -> Sem (Stop err : Opaque q : r) x)
-> (forall (q :: Effect) (r0 :: EffectRow) x.
    resource
    -> effect (Sem r0) x
    -> Tactical effect (Sem r0) (Stop err : Opaque q : r) x)
-> InterpreterFor (Scoped param effect !! err) r
interpretScopedResumableH forall (q :: Effect) x.
param
-> (resource -> Sem (Stop err : Opaque q : r) x)
-> Sem (Stop err : Opaque q : r) x
withResource forall (q :: Effect) (r0 :: EffectRow) x.
resource
-> effect (Sem r0) x
-> Tactical effect (Sem r0) (Stop err : Opaque q : r) x
scopedHandler =
  forall param (effect :: Effect) err (r :: EffectRow).
(forall (q :: Effect).
 param -> InterpreterFor effect (Stop err : Opaque q : r))
-> InterpreterFor (Scoped param effect !! err) r
runScopedResumable \ param
param Sem (effect : Stop err : Opaque q : r) a
sem ->
    forall (q :: Effect) x.
param
-> (resource -> Sem (Stop err : Opaque q : r) x)
-> Sem (Stop err : Opaque q : r) x
withResource param
param \ resource
r -> forall (e :: Effect) (r :: EffectRow) a.
(forall (rInitial :: EffectRow) x.
 e (Sem rInitial) x -> Tactical e (Sem rInitial) r x)
-> Sem (e : r) a -> Sem r a
interpretH (forall (q :: Effect) (r0 :: EffectRow) x.
resource
-> effect (Sem r0) x
-> Tactical effect (Sem r0) (Stop err : Opaque q : r) x
scopedHandler resource
r) Sem (effect : Stop err : Opaque q : r) a
sem

-- |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 .
  (∀ q x . param -> (resource -> Sem (Stop err : Opaque q : r) x) -> Sem (Stop err : Opaque q : r) x) ->
  (∀ q r0 x . resource -> effect (Sem r0) x -> Sem (Stop err : Opaque q : r) x) ->
  InterpreterFor (Scoped param effect !! err) r
interpretScopedResumable :: forall param resource (effect :: Effect) err (r :: EffectRow).
(forall (q :: Effect) x.
 param
 -> (resource -> Sem (Stop err : Opaque q : r) x)
 -> Sem (Stop err : Opaque q : r) x)
-> (forall (q :: Effect) (r0 :: EffectRow) x.
    resource -> effect (Sem r0) x -> Sem (Stop err : Opaque q : r) x)
-> InterpreterFor (Scoped param effect !! err) r
interpretScopedResumable forall (q :: Effect) x.
param
-> (resource -> Sem (Stop err : Opaque q : r) x)
-> Sem (Stop err : Opaque q : r) x
withResource forall (q :: Effect) (r0 :: EffectRow) x.
resource -> effect (Sem r0) x -> Sem (Stop err : Opaque q : r) x
scopedHandler =
  forall param resource (effect :: Effect) err (r :: EffectRow).
(forall (q :: Effect) x.
 param
 -> (resource -> Sem (Stop err : Opaque q : r) x)
 -> Sem (Stop err : Opaque q : r) x)
-> (forall (q :: Effect) (r0 :: EffectRow) x.
    resource
    -> effect (Sem r0) x
    -> Tactical effect (Sem r0) (Stop err : Opaque q : r) x)
-> InterpreterFor (Scoped param effect !! err) r
interpretScopedResumableH forall (q :: Effect) x.
param
-> (resource -> Sem (Stop err : Opaque q : r) x)
-> Sem (Stop err : Opaque q : r) x
withResource \ resource
r effect (Sem r0) x
e -> forall (m :: * -> *) (f :: * -> *) (r :: EffectRow) (e :: Effect)
       a.
Functor f =>
Sem r a -> Sem (WithTactics e f m r) (f a)
liftT (forall (q :: Effect) (r0 :: EffectRow) x.
resource -> effect (Sem r0) x -> Sem (Stop err : Opaque q : 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 .
  (∀ q . param -> Sem (Stop err : Opaque q : r) resource) ->
  (∀ q r0 x . resource -> effect (Sem r0) x -> Sem (Stop err : Opaque q : r) x) ->
  InterpreterFor (Scoped param effect !! err) r
interpretScopedResumable_ :: forall param resource (effect :: Effect) err (r :: EffectRow).
(forall (q :: Effect).
 param -> Sem (Stop err : Opaque q : r) resource)
-> (forall (q :: Effect) (r0 :: EffectRow) x.
    resource -> effect (Sem r0) x -> Sem (Stop err : Opaque q : r) x)
-> InterpreterFor (Scoped param effect !! err) r
interpretScopedResumable_ forall (q :: Effect).
param -> Sem (Stop err : Opaque q : r) resource
resource =
  forall param resource (effect :: Effect) err (r :: EffectRow).
(forall (q :: Effect) x.
 param
 -> (resource -> Sem (Stop err : Opaque q : r) x)
 -> Sem (Stop err : Opaque q : r) x)
-> (forall (q :: Effect) (r0 :: EffectRow) x.
    resource -> effect (Sem r0) x -> Sem (Stop err : Opaque q : r) x)
-> InterpreterFor (Scoped param effect !! err) r
interpretScopedResumable \ param
p resource -> Sem (Stop err : Opaque q : r) x
use -> resource -> Sem (Stop err : Opaque q : r) x
use forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (q :: Effect).
param -> Sem (Stop err : Opaque q : 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 .
  KnownList extra =>
  (∀ q x . param -> (resource -> Sem (extra ++ Stop err : Opaque q : r) x) -> Sem (Stop err : Opaque q : r) x) ->
  (∀ q r0 x . resource -> effect (Sem r0) x -> Tactical effect (Sem r0) (extra ++ [Stop err, Opaque q] ++ r) x) ->
  InterpreterFor (Scoped param effect !! err) r
interpretScopedResumableWithH :: forall (extra :: EffectRow) param resource (effect :: Effect) err
       (r :: EffectRow).
KnownList extra =>
(forall (q :: Effect) x.
 param
 -> (resource -> Sem (extra ++ (Stop err : Opaque q : r)) x)
 -> Sem (Stop err : Opaque q : r) x)
-> (forall (q :: Effect) (r0 :: EffectRow) x.
    resource
    -> effect (Sem r0) x
    -> Tactical
         effect (Sem r0) (extra ++ ('[Stop err, Opaque q] ++ r)) x)
-> InterpreterFor (Scoped param effect !! err) r
interpretScopedResumableWithH forall (q :: Effect) x.
param
-> (resource -> Sem (extra ++ (Stop err : Opaque q : r)) x)
-> Sem (Stop err : Opaque q : r) x
withResource forall (q :: Effect) (r0 :: EffectRow) x.
resource
-> effect (Sem r0) x
-> Tactical
     effect (Sem r0) (extra ++ ('[Stop err, Opaque q] ++ r)) x
scopedHandler =
  forall param (effect :: Effect) err (r :: EffectRow).
(forall (q :: Effect).
 param -> InterpreterFor effect (Stop err : Opaque q : r))
-> InterpreterFor (Scoped param effect !! err) r
runScopedResumable \ param
param (Sem (effect : Stop err : Opaque q : r) a
sem :: Sem (effect : Stop err : Opaque q : r) x) ->
    forall (q :: Effect) x.
param
-> (resource -> Sem (extra ++ (Stop err : Opaque q : r)) x)
-> Sem (Stop err : Opaque q : r) x
withResource param
param \ resource
resource ->
      forall (e :: Effect) (r :: EffectRow) a.
(forall (rInitial :: EffectRow) x.
 e (Sem rInitial) x -> Tactical e (Sem rInitial) r x)
-> Sem (e : r) a -> Sem r a
interpretH (forall (q :: Effect) (r0 :: EffectRow) x.
resource
-> effect (Sem r0) x
-> Tactical
     effect (Sem r0) (extra ++ ('[Stop err, Opaque q] ++ r)) x
scopedHandler @q resource
resource) forall a b. (a -> b) -> a -> b
$
      forall (r :: EffectRow) (r' :: EffectRow) a.
(forall (e :: Effect). ElemOf e r -> ElemOf e r')
-> Sem r a -> Sem r' a
restack (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 {k} (l :: [k]). KnownList l => SList l
singList @'[effect]) (forall {k} (l :: [k]). KnownList l => SList l
singList @extra)) forall a b. (a -> b) -> a -> b
$
      Sem (effect : Stop err : Opaque q : r) a
sem

-- |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 .
  KnownList extra =>
  (∀ q x . param -> (resource -> Sem (extra ++ Stop err : Opaque q : r) x) -> Sem (Stop err : Opaque q : r) x) ->
  (∀ q r0 x . resource -> effect (Sem r0) x -> Sem (extra ++ Stop err : Opaque q : r) x) ->
  InterpreterFor (Scoped param effect !! err) r
interpretScopedResumableWith :: forall (extra :: EffectRow) param resource (effect :: Effect) err
       (r :: EffectRow).
KnownList extra =>
(forall (q :: Effect) x.
 param
 -> (resource -> Sem (extra ++ (Stop err : Opaque q : r)) x)
 -> Sem (Stop err : Opaque q : r) x)
-> (forall (q :: Effect) (r0 :: EffectRow) x.
    resource
    -> effect (Sem r0) x -> Sem (extra ++ (Stop err : Opaque q : r)) x)
-> InterpreterFor (Scoped param effect !! err) r
interpretScopedResumableWith forall (q :: Effect) x.
param
-> (resource -> Sem (extra ++ (Stop err : Opaque q : r)) x)
-> Sem (Stop err : Opaque q : r) x
withResource forall (q :: Effect) (r0 :: EffectRow) x.
resource
-> effect (Sem r0) x -> Sem (extra ++ (Stop err : Opaque q : r)) x
scopedHandler =
  forall param (effect :: Effect) err (r :: EffectRow).
(forall (q :: Effect).
 param -> InterpreterFor effect (Stop err : Opaque q : r))
-> InterpreterFor (Scoped param effect !! err) r
runScopedResumable \ param
param (Sem (effect : Stop err : Opaque q : r) a
sem :: Sem (effect : Stop err : Opaque q : r) x) ->
    forall (q :: Effect) x.
param
-> (resource -> Sem (extra ++ (Stop err : Opaque q : r)) x)
-> Sem (Stop err : Opaque q : r) x
withResource param
param \ resource
resource ->
      Sem (effect : Stop err : Opaque q : r) a
sem
      forall a b. a -> (a -> b) -> b
& forall (r :: EffectRow) (r' :: EffectRow) a.
(forall (e :: Effect). ElemOf e r -> ElemOf e r')
-> Sem r a -> Sem r' a
restack (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 {k} (l :: [k]). KnownList l => SList l
singList @'[effect]) (forall {k} (l :: [k]). KnownList l => SList l
singList @extra))
      forall a b. a -> (a -> b) -> b
& forall (e :: Effect) (r :: EffectRow) a.
(forall (rInitial :: EffectRow) x.
 e (Sem rInitial) x -> Tactical e (Sem rInitial) r x)
-> Sem (e : r) a -> Sem r a
interpretH \ effect (Sem rInitial) x
e -> forall (m :: * -> *) (f :: * -> *) (r :: EffectRow) (e :: Effect)
       a.
Functor f =>
Sem r a -> Sem (WithTactics e f m r) (f a)
liftT (forall (q :: Effect) (r0 :: EffectRow) x.
resource
-> effect (Sem r0) x -> Sem (extra ++ (Stop err : Opaque q : r)) x
scopedHandler @q resource
resource effect (Sem rInitial) 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 .
  KnownList extra =>
  (∀ q x . param -> Sem (extra ++ Stop err : Opaque q : r) x -> Sem (Stop err : Opaque q : r) x) ->
  (∀ q r0 x . effect (Sem r0) x -> Sem (extra ++ Stop err : Opaque q : r) x) ->
  InterpreterFor (Scoped param effect !! err) r
interpretScopedResumableWith_ :: forall (extra :: EffectRow) param (effect :: Effect) err
       (r :: EffectRow).
KnownList extra =>
(forall (q :: Effect) x.
 param
 -> Sem (extra ++ (Stop err : Opaque q : r)) x
 -> Sem (Stop err : Opaque q : r) x)
-> (forall (q :: Effect) (r0 :: EffectRow) x.
    effect (Sem r0) x -> Sem (extra ++ (Stop err : Opaque q : r)) x)
-> InterpreterFor (Scoped param effect !! err) r
interpretScopedResumableWith_ forall (q :: Effect) x.
param
-> Sem (extra ++ (Stop err : Opaque q : r)) x
-> Sem (Stop err : Opaque q : r) x
extra forall (q :: Effect) (r0 :: EffectRow) x.
effect (Sem r0) x -> Sem (extra ++ (Stop err : Opaque q : r)) x
scopedHandler =
  forall param (effect :: Effect) err (r :: EffectRow).
(forall (q :: Effect).
 param -> InterpreterFor effect (Stop err : Opaque q : r))
-> InterpreterFor (Scoped param effect !! err) r
runScopedResumable \ param
param (Sem (effect : Stop err : Opaque q : r) a
sem :: Sem (effect : Stop err : Opaque q : r) x) ->
    forall (q :: Effect) x.
param
-> Sem (extra ++ (Stop err : Opaque q : r)) x
-> Sem (Stop err : Opaque q : r) x
extra @q param
param forall a b. (a -> b) -> a -> b
$
      Sem (effect : Stop err : Opaque q : r) a
sem
      forall a b. a -> (a -> b) -> b
& forall (r :: EffectRow) (r' :: EffectRow) a.
(forall (e :: Effect). ElemOf e r -> ElemOf e r')
-> Sem r a -> Sem r' a
restack (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 {k} (l :: [k]). KnownList l => SList l
singList @'[effect]) (forall {k} (l :: [k]). KnownList l => SList l
singList @extra))
      forall a b. a -> (a -> b) -> b
& forall (e :: Effect) (r :: EffectRow) a.
(forall (rInitial :: EffectRow) x.
 e (Sem rInitial) x -> Tactical e (Sem rInitial) r x)
-> Sem (e : r) a -> Sem r a
interpretH \ effect (Sem rInitial) x
e -> forall (m :: * -> *) (f :: * -> *) (r :: EffectRow) (e :: Effect)
       a.
Functor f =>
Sem r a -> Sem (WithTactics e f m r) (f a)
liftT (forall (q :: Effect) (r0 :: EffectRow) x.
effect (Sem r0) x -> Sem (extra ++ (Stop err : Opaque q : r)) x
scopedHandler @q effect (Sem rInitial) x
e)

-- |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 .
  (∀ q x . param -> (resource -> Sem (Opaque q : r) x) -> Sem (Opaque q : r) x) ->
  (∀ q r0 x . resource -> effect (Sem r0) x -> Tactical (effect !! err) (Sem r0) (Stop err : Opaque q : r) x) ->
  InterpreterFor (Scoped param (effect !! err)) r
interpretResumableScopedH :: forall param resource (effect :: Effect) err (r :: EffectRow).
(forall (q :: Effect) x.
 param
 -> (resource -> Sem (Opaque q : r) x) -> Sem (Opaque q : r) x)
-> (forall (q :: Effect) (r0 :: EffectRow) x.
    resource
    -> effect (Sem r0) x
    -> Tactical (effect !! err) (Sem r0) (Stop err : Opaque q : r) x)
-> InterpreterFor (Scoped param (effect !! err)) r
interpretResumableScopedH forall (q :: Effect) x.
param -> (resource -> Sem (Opaque q : r) x) -> Sem (Opaque q : r) x
withResource forall (q :: Effect) (r0 :: EffectRow) x.
resource
-> effect (Sem r0) x
-> Tactical (effect !! err) (Sem r0) (Stop err : Opaque q : r) x
scopedHandler =
  forall param (effect :: Effect) (r :: EffectRow).
(forall (q :: Effect).
 param -> InterpreterFor effect (Opaque q : r))
-> InterpreterFor (Scoped param effect) r
runScopedNew \ param
param Sem ((effect !! err) : Opaque q : r) a
sem ->
    forall (q :: Effect) x.
param -> (resource -> Sem (Opaque q : r) x) -> Sem (Opaque q : r) x
withResource param
param \ resource
r ->
      forall err (eff :: Effect) (r :: EffectRow).
(forall x (r0 :: EffectRow).
 eff (Sem r0) x
 -> Tactical (Resumable err eff) (Sem r0) (Stop err : r) x)
-> InterpreterFor (Resumable err eff) r
interpretResumableH (forall (q :: Effect) (r0 :: EffectRow) x.
resource
-> effect (Sem r0) x
-> Tactical (effect !! err) (Sem r0) (Stop err : Opaque q : r) x
scopedHandler resource
r) Sem ((effect !! err) : Opaque q : r) a
sem

-- |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 .
  (∀ q x . param -> (resource -> Sem (Opaque q : r) x) -> Sem (Opaque q : r) x) ->
  (∀ q r0 x . resource -> effect (Sem r0) x -> Sem (Stop err : Opaque q : r) x) ->
  InterpreterFor (Scoped param (effect !! err)) r
interpretResumableScoped :: forall param resource (effect :: Effect) err (r :: EffectRow).
(forall (q :: Effect) x.
 param
 -> (resource -> Sem (Opaque q : r) x) -> Sem (Opaque q : r) x)
-> (forall (q :: Effect) (r0 :: EffectRow) x.
    resource -> effect (Sem r0) x -> Sem (Stop err : Opaque q : r) x)
-> InterpreterFor (Scoped param (effect !! err)) r
interpretResumableScoped forall (q :: Effect) x.
param -> (resource -> Sem (Opaque q : r) x) -> Sem (Opaque q : r) x
withResource forall (q :: Effect) (r0 :: EffectRow) x.
resource -> effect (Sem r0) x -> Sem (Stop err : Opaque q : r) x
scopedHandler =
  forall param resource (effect :: Effect) err (r :: EffectRow).
(forall (q :: Effect) x.
 param
 -> (resource -> Sem (Opaque q : r) x) -> Sem (Opaque q : r) x)
-> (forall (q :: Effect) (r0 :: EffectRow) x.
    resource
    -> effect (Sem r0) x
    -> Tactical (effect !! err) (Sem r0) (Stop err : Opaque q : r) x)
-> InterpreterFor (Scoped param (effect !! err)) r
interpretResumableScopedH forall (q :: Effect) x.
param -> (resource -> Sem (Opaque q : r) x) -> Sem (Opaque q : r) x
withResource \ resource
r effect (Sem r0) x
e -> forall (m :: * -> *) (f :: * -> *) (r :: EffectRow) (e :: Effect)
       a.
Functor f =>
Sem r a -> Sem (WithTactics e f m r) (f a)
liftT (forall (q :: Effect) (r0 :: EffectRow) x.
resource -> effect (Sem r0) x -> Sem (Stop err : Opaque q : 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) ->
  (∀ q r0 x . resource -> effect (Sem r0) x -> Sem (Stop err : Opaque q : r) x) ->
  InterpreterFor (Scoped param (effect !! err)) r
interpretResumableScoped_ :: forall param resource (effect :: Effect) err (r :: EffectRow).
(param -> Sem r resource)
-> (forall (q :: Effect) (r0 :: EffectRow) x.
    resource -> effect (Sem r0) x -> Sem (Stop err : Opaque q : r) x)
-> InterpreterFor (Scoped param (effect !! err)) r
interpretResumableScoped_ param -> Sem r resource
resource =
  forall param resource (effect :: Effect) err (r :: EffectRow).
(forall (q :: Effect) x.
 param
 -> (resource -> Sem (Opaque q : r) x) -> Sem (Opaque q : r) x)
-> (forall (q :: Effect) (r0 :: EffectRow) x.
    resource -> effect (Sem r0) x -> Sem (Stop err : Opaque q : r) x)
-> InterpreterFor (Scoped param (effect !! err)) r
interpretResumableScoped \ param
p resource -> Sem (Opaque q : r) x
use -> resource -> Sem (Opaque q : r) x
use forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (e :: Effect) (r :: EffectRow) a. Sem r a -> Sem (e : r) a
raise (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 .
  KnownList extra =>
  (∀ q x . param -> (resource -> Sem (extra ++ Opaque q : r) x) -> Sem (Opaque q : r) x) ->
  (∀ q r0 x . resource -> effect (Sem r0) x -> Tactical (effect !! err) (Sem r0) (Stop err : (extra ++ Opaque q : r)) x) ->
  InterpreterFor (Scoped param (effect !! err)) r
interpretResumableScopedWithH :: forall (extra :: EffectRow) param resource (effect :: Effect) err
       (r :: EffectRow).
KnownList extra =>
(forall (q :: Effect) x.
 param
 -> (resource -> Sem (extra ++ (Opaque q : r)) x)
 -> Sem (Opaque q : r) x)
-> (forall (q :: Effect) (r0 :: EffectRow) x.
    resource
    -> effect (Sem r0) x
    -> Tactical
         (effect !! err) (Sem r0) (Stop err : (extra ++ (Opaque q : r))) x)
-> InterpreterFor (Scoped param (effect !! err)) r
interpretResumableScopedWithH forall (q :: Effect) x.
param
-> (resource -> Sem (extra ++ (Opaque q : r)) x)
-> Sem (Opaque q : r) x
withResource forall (q :: Effect) (r0 :: EffectRow) x.
resource
-> effect (Sem r0) x
-> Tactical
     (effect !! err) (Sem r0) (Stop err : (extra ++ (Opaque q : r))) x
scopedHandler =
  forall param (effect :: Effect) (r :: EffectRow).
(forall (q :: Effect).
 param -> InterpreterFor effect (Opaque q : r))
-> InterpreterFor (Scoped param effect) r
runScopedNew \ param
param (Sem ((effect !! err) : Opaque q : r) a
sem :: Sem (effect !! err : Opaque q : r) x) ->
    forall (q :: Effect) x.
param
-> (resource -> Sem (extra ++ (Opaque q : r)) x)
-> Sem (Opaque q : r) x
withResource param
param \ resource
resource ->
      Sem ((effect !! err) : Opaque q : r) a
sem
        forall a b. a -> (a -> b) -> b
& forall (r :: EffectRow) (r' :: EffectRow) a.
(forall (e :: Effect). ElemOf e r -> ElemOf e r')
-> Sem r a -> Sem r' a
restack (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 {k} (l :: [k]). KnownList l => SList l
singList @'[effect !! err]) (forall {k} (l :: [k]). KnownList l => SList l
singList @extra))
        forall a b. a -> (a -> b) -> b
& forall err (eff :: Effect) (r :: EffectRow).
(forall x (r0 :: EffectRow).
 eff (Sem r0) x
 -> Tactical (Resumable err eff) (Sem r0) (Stop err : r) x)
-> InterpreterFor (Resumable err eff) r
interpretResumableH (forall (q :: Effect) (r0 :: EffectRow) x.
resource
-> effect (Sem r0) x
-> Tactical
     (effect !! err) (Sem r0) (Stop err : (extra ++ (Opaque q : r))) x
scopedHandler @q resource
resource)

-- |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 .
  KnownList extra =>
  (∀ q x . param -> (resource -> Sem (extra ++ Opaque q : r) x) -> Sem (Opaque q : r) x) ->
  (∀ r0 x . resource -> effect (Sem r0) x -> Sem (Stop err : (extra ++ r)) x) ->
  InterpreterFor (Scoped param (effect !! err)) r
interpretResumableScopedWith :: forall (extra :: EffectRow) param resource (effect :: Effect) err
       (r :: EffectRow).
KnownList extra =>
(forall (q :: Effect) x.
 param
 -> (resource -> Sem (extra ++ (Opaque q : r)) x)
 -> Sem (Opaque q : r) x)
-> (forall (r0 :: EffectRow) x.
    resource -> effect (Sem r0) x -> Sem (Stop err : (extra ++ r)) x)
-> InterpreterFor (Scoped param (effect !! err)) r
interpretResumableScopedWith forall (q :: Effect) x.
param
-> (resource -> Sem (extra ++ (Opaque q : r)) x)
-> Sem (Opaque q : r) x
withResource forall (r0 :: EffectRow) x.
resource -> effect (Sem r0) x -> Sem (Stop err : (extra ++ r)) x
scopedHandler =
  forall param (effect :: Effect) (r :: EffectRow).
(forall (q :: Effect).
 param -> InterpreterFor effect (Opaque q : r))
-> InterpreterFor (Scoped param effect) r
runScopedNew \ param
param (Sem ((effect !! err) : Opaque q : r) a
sem :: Sem (effect !! err : Opaque q : r) x) ->
    forall (q :: Effect) x.
param
-> (resource -> Sem (extra ++ (Opaque q : r)) x)
-> Sem (Opaque q : r) x
withResource param
param \resource
resource ->
      Sem ((effect !! err) : Opaque q : r) a
sem
        forall a b. a -> (a -> b) -> b
& forall (r :: EffectRow) (r' :: EffectRow) a.
(forall (e :: Effect). ElemOf e r -> ElemOf e r')
-> Sem r a -> Sem r' a
restack (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 {k} (l :: [k]). KnownList l => SList l
singList @'[effect !! err]) (forall {k} (l :: [k]). KnownList l => SList l
singList @extra))
        forall a b. a -> (a -> b) -> b
& forall err (eff :: Effect) (r :: EffectRow).
(forall x (r0 :: EffectRow).
 eff (Sem r0) x
 -> Tactical (Resumable err eff) (Sem r0) (Stop err : r) x)
-> InterpreterFor (Resumable err eff) r
interpretResumableH \ effect (Sem r0) x
e ->
          forall (m :: * -> *) (f :: * -> *) (r :: EffectRow) (e :: Effect)
       a.
Functor f =>
Sem r a -> Sem (WithTactics e f m r) (f a)
liftT forall a b. (a -> b) -> a -> b
$
          forall (r :: EffectRow) (r' :: EffectRow) a.
(forall (e :: Effect). ElemOf e r -> ElemOf e r')
-> Sem r a -> Sem r' a
restack (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 @r (forall {k} (l :: [k]). KnownList l => SList l
singList @(Stop err : extra)) (forall {k} (l :: [k]). KnownList l => SList l
singList @'[Opaque q])) (forall (r0 :: EffectRow) x.
resource -> effect (Sem r0) x -> Sem (Stop err : (extra ++ r)) x
scopedHandler resource
resource 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 .
  KnownList extra =>
  (∀ q x . param -> Sem (extra ++ Opaque q : r) x -> Sem (Opaque q : r) x) ->
  (∀ r0 x . effect (Sem r0) x -> Sem (Stop err : (extra ++ r)) x) ->
  InterpreterFor (Scoped param (effect !! err)) r
interpretResumableScopedWith_ :: forall (extra :: EffectRow) param (effect :: Effect) err
       (r :: EffectRow).
KnownList extra =>
(forall (q :: Effect) x.
 param -> Sem (extra ++ (Opaque q : r)) x -> Sem (Opaque q : r) x)
-> (forall (r0 :: EffectRow) x.
    effect (Sem r0) x -> Sem (Stop err : (extra ++ r)) x)
-> InterpreterFor (Scoped param (effect !! err)) r
interpretResumableScopedWith_ forall (q :: Effect) x.
param -> Sem (extra ++ (Opaque q : r)) x -> Sem (Opaque q : r) x
extra forall (r0 :: EffectRow) x.
effect (Sem r0) x -> Sem (Stop err : (extra ++ r)) x
scopedHandler =
  forall (extra :: EffectRow) param resource (effect :: Effect) err
       (r :: EffectRow).
KnownList extra =>
(forall (q :: Effect) x.
 param
 -> (resource -> Sem (extra ++ (Opaque q : r)) x)
 -> Sem (Opaque q : r) x)
-> (forall (r0 :: EffectRow) x.
    resource -> effect (Sem r0) x -> Sem (Stop err : (extra ++ r)) x)
-> InterpreterFor (Scoped param (effect !! err)) r
interpretResumableScopedWith @extra @param @() @effect @err @r (\ param
p () -> Sem (extra ++ (Opaque q : r)) x
f -> forall (q :: Effect) x.
param -> Sem (extra ++ (Opaque q : r)) x -> Sem (Opaque q : r) x
extra param
p (() -> Sem (extra ++ (Opaque q : r)) x
f ())) (forall a b. a -> b -> a
const forall (r0 :: EffectRow) x.
effect (Sem r0) x -> Sem (Stop err : (extra ++ r)) 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 .
  (∀ q x . param -> (resource -> Sem (Stop eo : Opaque q : r) x) -> Sem (Stop eo : Opaque q : r) x) ->
  (∀ q r0 x . resource -> effect (Sem r0) x -> Tactical (effect !! ei) (Sem r0) (Stop ei : Stop eo : Opaque q : r) x) ->
  InterpreterFor (Scoped param (effect !! ei) !! eo) r
interpretScopedRH :: forall param resource (effect :: Effect) eo ei (r :: EffectRow).
(forall (q :: Effect) x.
 param
 -> (resource -> Sem (Stop eo : Opaque q : r) x)
 -> Sem (Stop eo : Opaque q : r) x)
-> (forall (q :: Effect) (r0 :: EffectRow) x.
    resource
    -> effect (Sem r0) x
    -> Tactical
         (effect !! ei) (Sem r0) (Stop ei : Stop eo : Opaque q : r) x)
-> InterpreterFor (Scoped param (effect !! ei) !! eo) r
interpretScopedRH forall (q :: Effect) x.
param
-> (resource -> Sem (Stop eo : Opaque q : r) x)
-> Sem (Stop eo : Opaque q : r) x
withResource forall (q :: Effect) (r0 :: EffectRow) x.
resource
-> effect (Sem r0) x
-> Tactical
     (effect !! ei) (Sem r0) (Stop ei : Stop eo : Opaque q : r) x
scopedHandler =
  forall param (effect :: Effect) err (r :: EffectRow).
(forall (q :: Effect).
 param -> InterpreterFor effect (Stop err : Opaque q : r))
-> InterpreterFor (Scoped param effect !! err) r
runScopedResumable \ param
param Sem ((effect !! ei) : Stop eo : Opaque q : r) a
sem ->
    forall (q :: Effect) x.
param
-> (resource -> Sem (Stop eo : Opaque q : r) x)
-> Sem (Stop eo : Opaque q : r) x
withResource param
param \ resource
r ->
      forall err (eff :: Effect) (r :: EffectRow).
(forall x (r0 :: EffectRow).
 eff (Sem r0) x
 -> Tactical (Resumable err eff) (Sem r0) (Stop err : r) x)
-> InterpreterFor (Resumable err eff) r
interpretResumableH (forall (q :: Effect) (r0 :: EffectRow) x.
resource
-> effect (Sem r0) x
-> Tactical
     (effect !! ei) (Sem r0) (Stop ei : Stop eo : Opaque q : r) x
scopedHandler resource
r) Sem ((effect !! ei) : Stop eo : Opaque q : r) a
sem

-- |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 .
  (∀ q x . param -> (resource -> Sem (Stop eo : Opaque q : r) x) -> Sem (Stop eo : Opaque q : r) x) ->
  (∀ q r0 x . resource -> effect (Sem r0) x -> Sem (Stop ei : Stop eo : Opaque q : r) x) ->
  InterpreterFor (Scoped param (effect !! ei) !! eo) r
interpretScopedR :: forall param resource (effect :: Effect) eo ei (r :: EffectRow).
(forall (q :: Effect) x.
 param
 -> (resource -> Sem (Stop eo : Opaque q : r) x)
 -> Sem (Stop eo : Opaque q : r) x)
-> (forall (q :: Effect) (r0 :: EffectRow) x.
    resource
    -> effect (Sem r0) x -> Sem (Stop ei : Stop eo : Opaque q : r) x)
-> InterpreterFor (Scoped param (effect !! ei) !! eo) r
interpretScopedR forall (q :: Effect) x.
param
-> (resource -> Sem (Stop eo : Opaque q : r) x)
-> Sem (Stop eo : Opaque q : r) x
withResource forall (q :: Effect) (r0 :: EffectRow) x.
resource
-> effect (Sem r0) x -> Sem (Stop ei : Stop eo : Opaque q : r) x
scopedHandler =
  forall param resource (effect :: Effect) eo ei (r :: EffectRow).
(forall (q :: Effect) x.
 param
 -> (resource -> Sem (Stop eo : Opaque q : r) x)
 -> Sem (Stop eo : Opaque q : r) x)
-> (forall (q :: Effect) (r0 :: EffectRow) x.
    resource
    -> effect (Sem r0) x
    -> Tactical
         (effect !! ei) (Sem r0) (Stop ei : Stop eo : Opaque q : r) x)
-> InterpreterFor (Scoped param (effect !! ei) !! eo) r
interpretScopedRH forall (q :: Effect) x.
param
-> (resource -> Sem (Stop eo : Opaque q : r) x)
-> Sem (Stop eo : Opaque q : r) x
withResource \ resource
r effect (Sem r0) x
e -> forall (m :: * -> *) (f :: * -> *) (r :: EffectRow) (e :: Effect)
       a.
Functor f =>
Sem r a -> Sem (WithTactics e f m r) (f a)
liftT (forall (q :: Effect) (r0 :: EffectRow) x.
resource
-> effect (Sem r0) x -> Sem (Stop ei : Stop eo : Opaque q : 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) ->
  (∀ q r0 x . resource -> effect (Sem r0) x -> Sem (Stop ei : Stop eo : Opaque q : r) x) ->
  InterpreterFor (Scoped param (effect !! ei) !! eo) r
interpretScopedR_ :: forall param resource (effect :: Effect) eo ei (r :: EffectRow).
(param -> Sem (Stop eo : r) resource)
-> (forall (q :: Effect) (r0 :: EffectRow) x.
    resource
    -> effect (Sem r0) x -> Sem (Stop ei : Stop eo : Opaque q : r) x)
-> InterpreterFor (Scoped param (effect !! ei) !! eo) r
interpretScopedR_ param -> Sem (Stop eo : r) resource
resource =
  forall param resource (effect :: Effect) eo ei (r :: EffectRow).
(forall (q :: Effect) x.
 param
 -> (resource -> Sem (Stop eo : Opaque q : r) x)
 -> Sem (Stop eo : Opaque q : r) x)
-> (forall (q :: Effect) (r0 :: EffectRow) x.
    resource
    -> effect (Sem r0) x -> Sem (Stop ei : Stop eo : Opaque q : r) x)
-> InterpreterFor (Scoped param (effect !! ei) !! eo) r
interpretScopedR \ param
p resource -> Sem (Stop eo : Opaque q : r) x
use -> resource -> Sem (Stop eo : Opaque q : r) x
use forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (e2 :: Effect) (e1 :: Effect) (r :: EffectRow) a.
Sem (e1 : r) a -> Sem (e1 : e2 : r) a
raiseUnder (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 .
  KnownList extra =>
  (∀ q x . param -> (resource -> Sem (extra ++ Stop eo : Opaque q : r) x) -> Sem (Stop eo : Opaque q : r) x) ->
  (∀ q r0 x . resource -> effect (Sem r0) x -> Tactical (effect !! ei) (Sem r0) (Stop ei : (extra ++ Stop eo : Opaque q : r)) x) ->
  InterpreterFor (Scoped param (effect !! ei) !! eo) r
interpretScopedRWithH :: forall (extra :: EffectRow) param resource (effect :: Effect) eo ei
       (r :: EffectRow).
KnownList extra =>
(forall (q :: Effect) x.
 param
 -> (resource -> Sem (extra ++ (Stop eo : Opaque q : r)) x)
 -> Sem (Stop eo : Opaque q : r) x)
-> (forall (q :: Effect) (r0 :: EffectRow) x.
    resource
    -> effect (Sem r0) x
    -> Tactical
         (effect !! ei)
         (Sem r0)
         (Stop ei : (extra ++ (Stop eo : Opaque q : r)))
         x)
-> InterpreterFor (Scoped param (effect !! ei) !! eo) r
interpretScopedRWithH forall (q :: Effect) x.
param
-> (resource -> Sem (extra ++ (Stop eo : Opaque q : r)) x)
-> Sem (Stop eo : Opaque q : r) x
withResource forall (q :: Effect) (r0 :: EffectRow) x.
resource
-> effect (Sem r0) x
-> Tactical
     (effect !! ei)
     (Sem r0)
     (Stop ei : (extra ++ (Stop eo : Opaque q : r)))
     x
scopedHandler =
  forall param (effect :: Effect) err (r :: EffectRow).
(forall (q :: Effect).
 param -> InterpreterFor effect (Stop err : Opaque q : r))
-> InterpreterFor (Scoped param effect !! err) r
runScopedResumable \ param
param (Sem ((effect !! ei) : Stop eo : Opaque q : r) a
sem :: Sem (effect !! ei : Stop eo : Opaque q : r) x) ->
    forall (q :: Effect) x.
param
-> (resource -> Sem (extra ++ (Stop eo : Opaque q : r)) x)
-> Sem (Stop eo : Opaque q : r) x
withResource param
param \ resource
resource ->
      Sem ((effect !! ei) : Stop eo : Opaque q : r) a
sem
        forall a b. a -> (a -> b) -> b
& forall (r :: EffectRow) (r' :: EffectRow) a.
(forall (e :: Effect). ElemOf e r -> ElemOf e r')
-> Sem r a -> Sem r' a
restack (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 {k} (l :: [k]). KnownList l => SList l
singList @'[effect !! ei]) (forall {k} (l :: [k]). KnownList l => SList l
singList @extra))
        forall a b. a -> (a -> b) -> b
& forall err (eff :: Effect) (r :: EffectRow).
(forall x (r0 :: EffectRow).
 eff (Sem r0) x
 -> Tactical (Resumable err eff) (Sem r0) (Stop err : r) x)
-> InterpreterFor (Resumable err eff) r
interpretResumableH (forall (q :: Effect) (r0 :: EffectRow) x.
resource
-> effect (Sem r0) x
-> Tactical
     (effect !! ei)
     (Sem r0)
     (Stop ei : (extra ++ (Stop eo : Opaque q : r)))
     x
scopedHandler @q resource
resource)

-- |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 .
  KnownList extra =>
  (∀ q x . param -> (resource -> Sem (extra ++ Stop eo : Opaque q : r) x) -> Sem (Stop eo : Opaque q : r) x) ->
  (∀ q r0 x . resource -> effect (Sem r0) x -> Sem (Stop ei : (extra ++ Stop eo : Opaque q : r)) x) ->
  InterpreterFor (Scoped param (effect !! ei) !! eo) r
interpretScopedRWith :: forall (extra :: EffectRow) param resource (effect :: Effect) eo ei
       (r :: EffectRow).
KnownList extra =>
(forall (q :: Effect) x.
 param
 -> (resource -> Sem (extra ++ (Stop eo : Opaque q : r)) x)
 -> Sem (Stop eo : Opaque q : r) x)
-> (forall (q :: Effect) (r0 :: EffectRow) x.
    resource
    -> effect (Sem r0) x
    -> Sem (Stop ei : (extra ++ (Stop eo : Opaque q : r))) x)
-> InterpreterFor (Scoped param (effect !! ei) !! eo) r
interpretScopedRWith forall (q :: Effect) x.
param
-> (resource -> Sem (extra ++ (Stop eo : Opaque q : r)) x)
-> Sem (Stop eo : Opaque q : r) x
withResource forall (q :: Effect) (r0 :: EffectRow) x.
resource
-> effect (Sem r0) x
-> Sem (Stop ei : (extra ++ (Stop eo : Opaque q : r))) x
scopedHandler =
  forall param (effect :: Effect) err (r :: EffectRow).
(forall (q :: Effect).
 param -> InterpreterFor effect (Stop err : Opaque q : r))
-> InterpreterFor (Scoped param effect !! err) r
runScopedResumable \ param
param (Sem ((effect !! ei) : Stop eo : Opaque q : r) a
sem :: Sem (effect !! ei : Stop eo : Opaque q : r) x) ->
    forall (q :: Effect) x.
param
-> (resource -> Sem (extra ++ (Stop eo : Opaque q : r)) x)
-> Sem (Stop eo : Opaque q : r) x
withResource param
param \ resource
resource ->
      Sem ((effect !! ei) : Stop eo : Opaque q : r) a
sem
      forall a b. a -> (a -> b) -> b
& forall (r :: EffectRow) (r' :: EffectRow) a.
(forall (e :: Effect). ElemOf e r -> ElemOf e r')
-> Sem r a -> Sem r' a
restack (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 {k} (l :: [k]). KnownList l => SList l
singList @'[effect !! ei]) (forall {k} (l :: [k]). KnownList l => SList l
singList @extra))
      forall a b. a -> (a -> b) -> b
& forall err (eff :: Effect) (r :: EffectRow).
(forall x (r0 :: EffectRow).
 eff (Sem r0) x
 -> Tactical (Resumable err eff) (Sem r0) (Stop err : r) x)
-> InterpreterFor (Resumable err eff) r
interpretResumableH \ effect (Sem r0) x
e ->
        forall (m :: * -> *) (f :: * -> *) (r :: EffectRow) (e :: Effect)
       a.
Functor f =>
Sem r a -> Sem (WithTactics e f m r) (f a)
liftT (forall (q :: Effect) (r0 :: EffectRow) x.
resource
-> effect (Sem r0) x
-> Sem (Stop ei : (extra ++ (Stop eo : Opaque q : r))) x
scopedHandler @q resource
resource 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 .
  KnownList extra =>
  (∀ q x . param -> Sem (extra ++ Stop eo : Opaque q : r) x -> Sem (Stop eo : Opaque q : r) x) ->
  (∀ q r0 x . effect (Sem r0) x -> Sem (Stop ei : (extra ++ Stop eo : Opaque q : r)) x) ->
  InterpreterFor (Scoped param (effect !! ei) !! eo) r
interpretScopedRWith_ :: forall (extra :: EffectRow) param (effect :: Effect) eo ei
       (r :: EffectRow).
KnownList extra =>
(forall (q :: Effect) x.
 param
 -> Sem (extra ++ (Stop eo : Opaque q : r)) x
 -> Sem (Stop eo : Opaque q : r) x)
-> (forall (q :: Effect) (r0 :: EffectRow) x.
    effect (Sem r0) x
    -> Sem (Stop ei : (extra ++ (Stop eo : Opaque q : r))) x)
-> InterpreterFor (Scoped param (effect !! ei) !! eo) r
interpretScopedRWith_ forall (q :: Effect) x.
param
-> Sem (extra ++ (Stop eo : Opaque q : r)) x
-> Sem (Stop eo : Opaque q : r) x
extra forall (q :: Effect) (r0 :: EffectRow) x.
effect (Sem r0) x
-> Sem (Stop ei : (extra ++ (Stop eo : Opaque q : r))) x
scopedHandler =
  forall param (effect :: Effect) err (r :: EffectRow).
(forall (q :: Effect).
 param -> InterpreterFor effect (Stop err : Opaque q : r))
-> InterpreterFor (Scoped param effect !! err) r
runScopedResumable \ param
param (Sem ((effect !! ei) : Stop eo : Opaque q : r) a
sem :: Sem (effect !! ei : Stop eo : Opaque q : r) x) ->
    forall (q :: Effect) x.
param
-> Sem (extra ++ (Stop eo : Opaque q : r)) x
-> Sem (Stop eo : Opaque q : r) x
extra param
param do
      Sem ((effect !! ei) : Stop eo : Opaque q : r) a
sem
        forall a b. a -> (a -> b) -> b
& forall (r :: EffectRow) (r' :: EffectRow) a.
(forall (e :: Effect). ElemOf e r -> ElemOf e r')
-> Sem r a -> Sem r' a
restack (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 {k} (l :: [k]). KnownList l => SList l
singList @'[effect !! ei]) (forall {k} (l :: [k]). KnownList l => SList l
singList @extra))
        forall a b. a -> (a -> b) -> b
& forall err (eff :: Effect) (r :: EffectRow).
(forall x (r0 :: EffectRow).
 eff (Sem r0) x
 -> Tactical (Resumable err eff) (Sem r0) (Stop err : r) x)
-> InterpreterFor (Resumable err eff) r
interpretResumableH \ effect (Sem r0) x
e ->
          forall (m :: * -> *) (f :: * -> *) (r :: EffectRow) (e :: Effect)
       a.
Functor f =>
Sem r a -> Sem (WithTactics e f m r) (f a)
liftT (forall (q :: Effect) (r0 :: EffectRow) x.
effect (Sem r0) x
-> Sem (Stop ei : (extra ++ (Stop eo : Opaque q : r))) x
scopedHandler @q effect (Sem r0) x
e)