{-# 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.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' =
  (Either err (f (f' a')) -> x)
-> Sem r (Either err (f (f' a'))) -> Sem r x
forall a b. (a -> b) -> Sem r a -> Sem r b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Either err (f (f' a')) -> x)
 -> Sem r (Either err (f (f' a'))) -> Sem r x)
-> (Either err (f (f' a')) -> x)
-> Sem r (Either err (f (f' a')))
-> Sem r x
forall a b. (a -> b) -> a -> b
$ f (Either err a) -> x
ex (f (Either err a) -> x)
-> (Either err (f (f' a')) -> f (Either err a))
-> Either err (f (f' a'))
-> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
    Right f (f' a')
a -> a -> Either err a
forall a b. b -> Either a b
Right (a -> Either err a) -> (f' a' -> a) -> f' a' -> Either err a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f' a' -> a
ex' (f' a' -> Either err a) -> f (f' a') -> f (Either err a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (f' a')
a
    Left err
err -> err -> Either err a
forall a b. a -> Either a b
Left err
err Either err a -> f () -> f (Either err a)
forall a b. a -> f b -> f a
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 x.
 Weaving
   (Scoped param effect !! err)
   (Sem ((Scoped param effect !! err) : r))
   x
 -> Sem r x)
-> InterpreterFor (Scoped param effect !! err) r
forall (e :: Effect) (r :: 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
_ -> [Char] -> Sem r x
forall a. [Char] -> a
errorWithoutStackTrace ([Char] -> Sem r x) -> [Char] -> Sem r x
forall a b. (a -> b) -> a -> b
$ [Char]
"top level run with depth " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Word -> [Char]
forall b a. (Show a, IsString b) => a -> b
show Word
w
    InScope param
param Word -> Sem rInitial a
main ->
      f (Sem rInitial (f a))
-> Sem ((Scoped param effect !! err) : r) (f (f a))
forall x.
f (Sem rInitial x) -> Sem ((Scoped param effect !! err) : r) (f x)
wv (f (Sem rInitial a) -> Sem r (f a)
forall x. f (Sem rInitial x) -> Sem r (f x)
wv' (Word -> Sem rInitial a
main Word
0 Sem rInitial a -> f () -> f (Sem rInitial a)
forall a b. a -> f b -> f a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s') Sem rInitial (f a) -> f () -> f (Sem rInitial (f a))
forall a b. a -> f b -> f a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s)
        Sem ((Scoped param effect !! err) : r) (f (f a))
-> (Sem ((Scoped param effect !! err) : r) (f (f a))
    -> Sem
         ((Scoped param effect !! err)
            : effect : Opaque (OuterRun effect) : r)
         (f (f a)))
-> Sem
     ((Scoped param effect !! err)
        : effect : Opaque (OuterRun effect) : r)
     (f (f a))
forall a b. a -> (a -> b) -> b
& Sem ((Scoped param effect !! err) : r) (f (f a))
-> Sem
     ((Scoped param effect !! err)
        : effect : Opaque (OuterRun effect) : r)
     (f (f a))
forall (e2 :: Effect) (e3 :: Effect) (e1 :: Effect)
       (r :: EffectRow) a.
Sem (e1 : r) a -> Sem (e1 : e2 : e3 : r) a
raiseUnder2
        Sem
  ((Scoped param effect !! err)
     : effect : Opaque (OuterRun effect) : r)
  (f (f a))
-> (Sem
      ((Scoped param effect !! err)
         : effect : Opaque (OuterRun effect) : r)
      (f (f a))
    -> Sem (effect : Opaque (OuterRun effect) : r) (f (f a)))
-> Sem (effect : Opaque (OuterRun effect) : r) (f (f a))
forall a b. a -> (a -> b) -> b
& Word
-> InterpreterFor
     (Scoped param effect !! err)
     (effect : Opaque (OuterRun effect) : r)
go Word
0
        Sem (effect : Opaque (OuterRun effect) : r) (f (f a))
-> (Sem (effect : Opaque (OuterRun effect) : r) (f (f a))
    -> Sem
         (effect : Stop err : Opaque (OuterRun effect) : r) (f (f a)))
-> Sem (effect : Stop err : Opaque (OuterRun effect) : r) (f (f a))
forall a b. a -> (a -> b) -> b
& Sem (effect : Opaque (OuterRun effect) : r) (f (f a))
-> Sem (effect : Stop err : Opaque (OuterRun effect) : r) (f (f a))
forall (e2 :: Effect) (e1 :: Effect) (r :: EffectRow) a.
Sem (e1 : r) a -> Sem (e1 : e2 : r) a
raiseUnder
        Sem (effect : Stop err : Opaque (OuterRun effect) : r) (f (f a))
-> (Sem
      (effect : Stop err : Opaque (OuterRun effect) : r) (f (f a))
    -> Sem (Stop err : Opaque (OuterRun effect) : r) (f (f a)))
-> Sem (Stop err : Opaque (OuterRun effect) : r) (f (f a))
forall a b. a -> (a -> b) -> b
& param
-> InterpreterFor effect (Stop err : Opaque (OuterRun effect) : r)
forall (q :: Effect).
param -> InterpreterFor effect (Stop err : Opaque q : r)
h param
param
        Sem (Stop err : Opaque (OuterRun effect) : r) (f (f a))
-> (Sem (Stop err : Opaque (OuterRun effect) : r) (f (f a))
    -> Sem (Opaque (OuterRun effect) : r) (Either err (f (f a))))
-> Sem (Opaque (OuterRun effect) : r) (Either err (f (f a)))
forall a b. a -> (a -> b) -> b
& Sem (Stop err : Opaque (OuterRun effect) : r) (f (f a))
-> Sem (Opaque (OuterRun effect) : r) (Either err (f (f a)))
forall err (r :: EffectRow) a.
Sem (Stop err : r) a -> Sem r (Either err a)
runStop
        Sem (Opaque (OuterRun effect) : r) (Either err (f (f a)))
-> (Sem (Opaque (OuterRun effect) : r) (Either err (f (f a)))
    -> Sem r (Either err (f (f a))))
-> Sem r (Either err (f (f a)))
forall a b. a -> (a -> b) -> b
& (forall (rInitial :: EffectRow) x.
 Opaque (OuterRun effect) (Sem rInitial) x
 -> Tactical (Opaque (OuterRun effect)) (Sem rInitial) r x)
-> Sem (Opaque (OuterRun effect) : r) (Either err (f (f a)))
-> Sem r (Either err (f (f a)))
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
_)) ->
            [Char]
-> Sem
     (WithTactics (Opaque (OuterRun effect)) f (Sem rInitial) r) (f x)
forall a. [Char] -> a
errorWithoutStackTrace ([Char]
 -> Sem
      (WithTactics (Opaque (OuterRun effect)) f (Sem rInitial) r) (f x))
-> [Char]
-> Sem
     (WithTactics (Opaque (OuterRun effect)) f (Sem rInitial) r) (f x)
forall a b. (a -> b) -> a -> b
$ [Char]
"unhandled OuterRun with depth " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Word -> [Char]
forall b a. (Show a, IsString b) => a -> b
show Word
w)
        Sem r (Either err (f (f a)))
-> (Sem r (Either err (f (f a))) -> Sem r x) -> Sem r x
forall a b. a -> (a -> b) -> b
& f ()
-> (f (Either err a1) -> x)
-> (f a -> a1)
-> Sem r (Either err (f (f a)))
-> Sem r x
forall {k} (f :: * -> *) err a x (f' :: k -> *) (a' :: k)
       (r :: 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
f (Either err a1) -> 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 x.
 Weaving
   (Opaque (OuterRun effect))
   (Sem
      (Opaque (OuterRun effect) : effect : Opaque (OuterRun effect) : r))
   x
 -> Sem (effect : Opaque (OuterRun effect) : r) x)
-> InterpreterFor
     (Opaque (OuterRun effect)) (effect : Opaque (OuterRun effect) : r)
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 Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== Word
depth then
          Union
  (effect : Opaque (OuterRun effect) : r)
  (Sem (effect : Opaque (OuterRun effect) : r))
  x
-> Sem (effect : Opaque (OuterRun effect) : r) x
forall (r :: EffectRow) a. Union r (Sem r) a -> Sem r a
liftSem (Union
   (effect : Opaque (OuterRun effect) : r)
   (Sem (effect : Opaque (OuterRun effect) : r))
   x
 -> Sem (effect : Opaque (OuterRun effect) : r) x)
-> Union
     (effect : Opaque (OuterRun effect) : r)
     (Sem (effect : Opaque (OuterRun effect) : r))
     x
-> Sem (effect : Opaque (OuterRun effect) : r) x
forall a b. (a -> b) -> a -> b
$ Weaving effect (Sem (effect : Opaque (OuterRun effect) : r)) x
-> Union
     (effect : Opaque (OuterRun effect) : r)
     (Sem (effect : Opaque (OuterRun effect) : r))
     x
forall (e :: Effect) (r :: EffectRow) (m :: * -> *) a.
Member e r =>
Weaving e m a -> Union r m a
injWeaving (Weaving effect (Sem (effect : Opaque (OuterRun effect) : r)) x
 -> Union
      (effect : Opaque (OuterRun effect) : r)
      (Sem (effect : Opaque (OuterRun effect) : r))
      x)
-> Weaving effect (Sem (effect : Opaque (OuterRun effect) : r)) x
-> Union
     (effect : Opaque (OuterRun effect) : r)
     (Sem (effect : Opaque (OuterRun effect) : r))
     x
forall a b. (a -> b) -> a -> b
$ effect (Sem rInitial) a
-> f ()
-> (forall x.
    f (Sem rInitial x)
    -> Sem (effect : Opaque (OuterRun effect) : r) (f x))
-> (f a -> x)
-> (forall x. f x -> Maybe x)
-> Weaving effect (Sem (effect : Opaque (OuterRun effect) : r)) x
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 (Sem
   (Opaque (OuterRun effect) : effect : Opaque (OuterRun effect) : r)
   (f x)
 -> Sem (effect : Opaque (OuterRun effect) : r) (f x))
-> (f (Sem rInitial x)
    -> Sem
         (Opaque (OuterRun effect) : effect : Opaque (OuterRun effect) : r)
         (f x))
-> f (Sem rInitial x)
-> Sem (effect : Opaque (OuterRun effect) : r) (f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Sem rInitial x)
-> Sem
     (Opaque (OuterRun effect) : effect : Opaque (OuterRun effect) : r)
     (f x)
forall x.
f (Sem rInitial x)
-> Sem
     (Opaque (OuterRun effect) : effect : Opaque (OuterRun effect) : r)
     (f x)
wv) f a -> x
ex f x -> Maybe x
forall x. f x -> Maybe x
ins
        else
          Union
  (effect : Opaque (OuterRun effect) : r)
  (Sem (effect : Opaque (OuterRun effect) : r))
  x
-> Sem (effect : Opaque (OuterRun effect) : r) x
forall (r :: EffectRow) a. Union r (Sem r) a -> Sem r a
liftSem (Union
   (effect : Opaque (OuterRun effect) : r)
   (Sem (effect : Opaque (OuterRun effect) : r))
   x
 -> Sem (effect : Opaque (OuterRun effect) : r) x)
-> Union
     (effect : Opaque (OuterRun effect) : r)
     (Sem (effect : Opaque (OuterRun effect) : r))
     x
-> Sem (effect : Opaque (OuterRun effect) : r) x
forall a b. (a -> b) -> a -> b
$ Weaving
  (Opaque (OuterRun effect))
  (Sem (effect : Opaque (OuterRun effect) : r))
  x
-> Union
     (effect : Opaque (OuterRun effect) : r)
     (Sem (effect : Opaque (OuterRun effect) : r))
     x
forall (e :: Effect) (r :: EffectRow) (m :: * -> *) a.
Member e r =>
Weaving e m a -> Union r m a
injWeaving (Weaving
   (Opaque (OuterRun effect))
   (Sem (effect : Opaque (OuterRun effect) : r))
   x
 -> Union
      (effect : Opaque (OuterRun effect) : r)
      (Sem (effect : Opaque (OuterRun effect) : r))
      x)
-> Weaving
     (Opaque (OuterRun effect))
     (Sem (effect : Opaque (OuterRun effect) : r))
     x
-> Union
     (effect : Opaque (OuterRun effect) : r)
     (Sem (effect : Opaque (OuterRun effect) : r))
     x
forall a b. (a -> b) -> a -> b
$ Opaque (OuterRun effect) (Sem rInitial) a
-> f ()
-> (forall x.
    f (Sem rInitial x)
    -> Sem (effect : Opaque (OuterRun effect) : r) (f x))
-> (f a -> x)
-> (forall x. f x -> Maybe x)
-> Weaving
     (Opaque (OuterRun effect))
     (Sem (effect : Opaque (OuterRun effect) : r))
     x
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 (Sem
   (Opaque (OuterRun effect) : effect : Opaque (OuterRun effect) : r)
   (f x)
 -> Sem (effect : Opaque (OuterRun effect) : r) (f x))
-> (f (Sem rInitial x)
    -> Sem
         (Opaque (OuterRun effect) : effect : Opaque (OuterRun effect) : r)
         (f x))
-> f (Sem rInitial x)
-> Sem (effect : Opaque (OuterRun effect) : r) (f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Sem rInitial x)
-> Sem
     (Opaque (OuterRun effect) : effect : Opaque (OuterRun effect) : r)
     (f x)
forall x.
f (Sem rInitial x)
-> Sem
     (Opaque (OuterRun effect) : effect : Opaque (OuterRun effect) : r)
     (f x)
wv) f a -> x
ex f x -> Maybe x
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 x.
 Weaving
   (Scoped param effect !! err)
   (Sem
      ((Scoped param effect !! err)
         : effect : Opaque (OuterRun effect) : r))
   x
 -> Sem (effect : Opaque (OuterRun effect) : r) x)
-> InterpreterFor
     (Scoped param effect !! err)
     (effect : Opaque (OuterRun effect) : r)
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 Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== Word
depth ->
            f a -> x
ex (f a -> x) -> (f a1 -> f a) -> f a1 -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a1 -> a) -> f a1 -> f a
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a1 -> a
a1 -> Either err a1
forall a b. b -> Either a b
Right (f a1 -> x)
-> Sem (effect : Opaque (OuterRun effect) : r) (f a1)
-> Sem (effect : Opaque (OuterRun effect) : r) x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Union
  (effect : Opaque (OuterRun effect) : r)
  (Sem (effect : Opaque (OuterRun effect) : r))
  (f a1)
-> Sem (effect : Opaque (OuterRun effect) : r) (f a1)
forall (r :: EffectRow) a. Union r (Sem r) a -> Sem r a
liftSem (f ()
-> (forall x.
    f (Sem rInitial x)
    -> Sem (effect : Opaque (OuterRun effect) : r) (f x))
-> (forall x. f x -> Maybe x)
-> Union (effect : Opaque (OuterRun effect) : r) (Sem rInitial) a1
-> Union
     (effect : Opaque (OuterRun effect) : r)
     (Sem (effect : Opaque (OuterRun effect) : r))
     (f a1)
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 (Sem
   ((Scoped param effect !! err)
      : effect : Opaque (OuterRun effect) : r)
   (f x)
 -> Sem (effect : Opaque (OuterRun effect) : r) (f x))
-> (f (Sem rInitial x)
    -> Sem
         ((Scoped param effect !! err)
            : effect : Opaque (OuterRun effect) : r)
         (f x))
-> f (Sem rInitial x)
-> Sem (effect : Opaque (OuterRun effect) : r) (f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Sem rInitial x)
-> Sem
     ((Scoped param effect !! err)
        : effect : Opaque (OuterRun effect) : r)
     (f x)
forall x.
f (Sem rInitial x)
-> Sem
     ((Scoped param effect !! err)
        : effect : Opaque (OuterRun effect) : r)
     (f x)
wv) f x -> Maybe x
forall x. f x -> Maybe x
ins (Weaving effect (Sem rInitial) a1
-> Union (effect : Opaque (OuterRun effect) : r) (Sem rInitial) a1
forall (e :: Effect) (r :: EffectRow) (m :: * -> *) a.
Member e r =>
Weaving e m a -> Union r m a
injWeaving (effect (Sem rInitial) a
-> f ()
-> (forall x. f (Sem rInitial x) -> Sem rInitial (f x))
-> (f a -> a1)
-> (forall x. f x -> Maybe x)
-> Weaving effect (Sem rInitial) a1
forall (f :: * -> *) (e :: Effect) (rInitial :: 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' f (Sem rInitial x) -> Sem rInitial (f x)
f (Sem rInitial x) -> Sem r (f x)
forall x. f (Sem rInitial x) -> Sem rInitial (f x)
forall x. f (Sem rInitial x) -> Sem r (f x)
wv' f a -> a1
ex' f x -> Maybe x
forall x. f x -> Maybe x
ins')))
          | Bool
otherwise ->
            f a -> x
ex (f a -> x) -> (f a1 -> f a) -> f a1 -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a1 -> a) -> f a1 -> f a
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a1 -> a
a1 -> Either err a1
forall a b. b -> Either a b
Right (f a1 -> x)
-> Sem (effect : Opaque (OuterRun effect) : r) (f a1)
-> Sem (effect : Opaque (OuterRun effect) : r) x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Union
  (effect : Opaque (OuterRun effect) : r)
  (Sem (effect : Opaque (OuterRun effect) : r))
  (f a1)
-> Sem (effect : Opaque (OuterRun effect) : r) (f a1)
forall (r :: EffectRow) a. Union r (Sem r) a -> Sem r a
liftSem (f ()
-> (forall x.
    f (Sem rInitial x)
    -> Sem (effect : Opaque (OuterRun effect) : r) (f x))
-> (forall x. f x -> Maybe x)
-> Union (effect : Opaque (OuterRun effect) : r) (Sem rInitial) a1
-> Union
     (effect : Opaque (OuterRun effect) : r)
     (Sem (effect : Opaque (OuterRun effect) : r))
     (f a1)
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 (Sem
   ((Scoped param effect !! err)
      : effect : Opaque (OuterRun effect) : r)
   (f x)
 -> Sem (effect : Opaque (OuterRun effect) : r) (f x))
-> (f (Sem rInitial x)
    -> Sem
         ((Scoped param effect !! err)
            : effect : Opaque (OuterRun effect) : r)
         (f x))
-> f (Sem rInitial x)
-> Sem (effect : Opaque (OuterRun effect) : r) (f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Sem rInitial x)
-> Sem
     ((Scoped param effect !! err)
        : effect : Opaque (OuterRun effect) : r)
     (f x)
forall x.
f (Sem rInitial x)
-> Sem
     ((Scoped param effect !! err)
        : effect : Opaque (OuterRun effect) : r)
     (f x)
wv) f x -> Maybe x
forall x. f x -> Maybe x
ins (Weaving (Opaque (OuterRun effect)) (Sem rInitial) a1
-> Union (effect : Opaque (OuterRun effect) : r) (Sem rInitial) a1
forall (e :: Effect) (r :: EffectRow) (m :: * -> *) a.
Member e r =>
Weaving e m a -> Union r m a
injWeaving (Opaque (OuterRun effect) (Sem rInitial) a
-> f ()
-> (forall x. f (Sem rInitial x) -> Sem rInitial (f x))
-> (f a -> a1)
-> (forall x. f x -> Maybe x)
-> Weaving (Opaque (OuterRun effect)) (Sem rInitial) a1
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 (OuterRun effect (Sem rInitial) a
-> Opaque (OuterRun effect) (Sem rInitial) a
forall (e :: Effect) (m :: * -> *) a. e m a -> Opaque e m a
Opaque (Word -> effect (Sem rInitial) a -> OuterRun effect (Sem rInitial) a
forall (effect :: Effect) (a :: * -> *) b.
Word -> effect a b -> OuterRun effect a b
OuterRun Word
w effect (Sem rInitial) a
act)) f ()
s' f (Sem rInitial x) -> Sem rInitial (f x)
f (Sem rInitial x) -> Sem r (f x)
forall x. f (Sem rInitial x) -> Sem rInitial (f x)
forall x. f (Sem rInitial x) -> Sem r (f x)
wv' f a -> a1
ex' f x -> Maybe x
forall x. f x -> Maybe x
ins')))
        InScope param
param Word -> Sem rInitial a
main -> do
          let !depth' :: Word
depth' = Word
depth Word -> Word -> Word
forall a. Num a => a -> a -> a
+ Word
1
          f (Sem rInitial (f a))
-> Sem
     ((Scoped param effect !! err)
        : effect : Opaque (OuterRun effect) : r)
     (f (f a))
forall x.
f (Sem rInitial x)
-> Sem
     ((Scoped param effect !! err)
        : effect : Opaque (OuterRun effect) : r)
     (f x)
wv (f (Sem rInitial a) -> Sem r (f a)
forall x. f (Sem rInitial x) -> Sem r (f x)
wv' (Word -> Sem rInitial a
main Word
depth' Sem rInitial a -> f () -> f (Sem rInitial a)
forall a b. a -> f b -> f a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s') Sem rInitial (f a) -> f () -> f (Sem rInitial (f a))
forall a b. a -> f b -> f a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s)
            Sem
  ((Scoped param effect !! err)
     : effect : Opaque (OuterRun effect) : r)
  (f (f a))
-> (Sem
      ((Scoped param effect !! err)
         : effect : Opaque (OuterRun effect) : r)
      (f (f a))
    -> Sem (effect : Opaque (OuterRun effect) : r) (f (f a)))
-> Sem (effect : Opaque (OuterRun effect) : r) (f (f a))
forall a b. a -> (a -> b) -> b
& Word
-> InterpreterFor
     (Scoped param effect !! err)
     (effect : Opaque (OuterRun effect) : r)
go Word
depth'
            Sem (effect : Opaque (OuterRun effect) : r) (f (f a))
-> (Sem (effect : Opaque (OuterRun effect) : r) (f (f a))
    -> Sem
         (effect : Stop err : Opaque (OuterRun effect) : r) (f (f a)))
-> Sem (effect : Stop err : Opaque (OuterRun effect) : r) (f (f a))
forall a b. a -> (a -> b) -> b
& Sem (effect : Opaque (OuterRun effect) : r) (f (f a))
-> Sem (effect : Stop err : Opaque (OuterRun effect) : r) (f (f a))
forall (e2 :: Effect) (e1 :: Effect) (r :: EffectRow) a.
Sem (e1 : r) a -> Sem (e1 : e2 : r) a
raiseUnder
            Sem (effect : Stop err : Opaque (OuterRun effect) : r) (f (f a))
-> (Sem
      (effect : Stop err : Opaque (OuterRun effect) : r) (f (f a))
    -> Sem (Stop err : Opaque (OuterRun effect) : r) (f (f a)))
-> Sem (Stop err : Opaque (OuterRun effect) : r) (f (f a))
forall a b. a -> (a -> b) -> b
& param
-> InterpreterFor effect (Stop err : Opaque (OuterRun effect) : r)
forall (q :: Effect).
param -> InterpreterFor effect (Stop err : Opaque q : r)
h param
param
            Sem (Stop err : Opaque (OuterRun effect) : r) (f (f a))
-> (Sem (Stop err : Opaque (OuterRun effect) : r) (f (f a))
    -> Sem (Opaque (OuterRun effect) : r) (Either err (f (f a))))
-> Sem (Opaque (OuterRun effect) : r) (Either err (f (f a)))
forall a b. a -> (a -> b) -> b
& Sem (Stop err : Opaque (OuterRun effect) : r) (f (f a))
-> Sem (Opaque (OuterRun effect) : r) (Either err (f (f a)))
forall err (r :: EffectRow) a.
Sem (Stop err : r) a -> Sem r (Either err a)
runStop
            Sem (Opaque (OuterRun effect) : r) (Either err (f (f a)))
-> (Sem (Opaque (OuterRun effect) : r) (Either err (f (f a)))
    -> Sem
         (Opaque (OuterRun effect) : effect : Opaque (OuterRun effect) : r)
         (Either err (f (f a))))
-> Sem
     (Opaque (OuterRun effect) : effect : Opaque (OuterRun effect) : r)
     (Either err (f (f a)))
forall a b. a -> (a -> b) -> b
& Sem (Opaque (OuterRun effect) : r) (Either err (f (f a)))
-> Sem
     (Opaque (OuterRun effect) : effect : Opaque (OuterRun effect) : r)
     (Either err (f (f a)))
forall (e2 :: Effect) (e3 :: Effect) (e1 :: Effect)
       (r :: EffectRow) a.
Sem (e1 : r) a -> Sem (e1 : e2 : e3 : r) a
raiseUnder2
            Sem
  (Opaque (OuterRun effect) : effect : Opaque (OuterRun effect) : r)
  (Either err (f (f a)))
-> (Sem
      (Opaque (OuterRun effect) : effect : Opaque (OuterRun effect) : r)
      (Either err (f (f a)))
    -> Sem
         (effect : Opaque (OuterRun effect) : r) (Either err (f (f a))))
-> Sem
     (effect : Opaque (OuterRun effect) : r) (Either err (f (f a)))
forall a b. a -> (a -> b) -> b
& Word
-> InterpreterFor
     (Opaque (OuterRun effect)) (effect : Opaque (OuterRun effect) : r)
go' Word
depth
            Sem (effect : Opaque (OuterRun effect) : r) (Either err (f (f a)))
-> (Sem
      (effect : Opaque (OuterRun effect) : r) (Either err (f (f a)))
    -> Sem (effect : Opaque (OuterRun effect) : r) x)
-> Sem (effect : Opaque (OuterRun effect) : r) x
forall a b. a -> (a -> b) -> b
& f ()
-> (f (Either err a1) -> x)
-> (f a -> a1)
-> Sem
     (effect : Opaque (OuterRun effect) : r) (Either err (f (f a)))
-> Sem (effect : Opaque (OuterRun effect) : r) x
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
f (Either err a1) -> 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 (q :: Effect).
 param -> InterpreterFor effect (Stop err : Opaque q : r))
-> InterpreterFor (Scoped param effect !! err) r
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 ->
    param
-> (resource -> Sem (Stop err : Opaque q : r) a)
-> Sem (Stop err : Opaque q : r) a
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 (rInitial :: EffectRow) x.
 effect (Sem rInitial) x
 -> Tactical effect (Sem rInitial) (Stop err : Opaque q : r) x)
-> Sem (effect : Stop err : Opaque q : r) a
-> Sem (Stop err : Opaque q : r) a
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 (resource
-> effect (Sem rInitial) x
-> Tactical effect (Sem rInitial) (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
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 (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
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 param
-> (resource -> Sem (Stop err : Opaque q : r) x)
-> Sem (Stop err : Opaque q : r) x
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 -> Sem (Stop err : Opaque q : r) x
-> Sem
     (WithTactics effect f (Sem r0) (Stop err : Opaque q : r)) (f x)
forall (m :: * -> *) (f :: * -> *) (r :: EffectRow) (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 : Opaque q : r) x
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 (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)
-> forall {a}.
   Sem (Resumable err (Scoped param effect) : r) a -> Sem r a
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 (resource -> Sem (Stop err : Opaque q : r) x)
-> Sem (Stop err : Opaque q : r) resource
-> Sem (Stop err : Opaque q : r) x
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< param -> Sem (Stop err : Opaque q : r) resource
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 (q :: Effect).
 param -> InterpreterFor effect (Stop err : Opaque q : r))
-> InterpreterFor (Scoped param effect !! err) r
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) ->
    param
-> (resource -> Sem (extra ++ (Stop err : Opaque q : r)) a)
-> Sem (Stop err : Opaque q : r) a
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 (rInitial :: EffectRow) x.
 effect (Sem rInitial) x
 -> Tactical
      effect (Sem rInitial) (extra ++ (Stop err : Opaque q : r)) x)
-> Sem (effect : (extra ++ (Stop err : Opaque q : r))) a
-> Sem (extra ++ (Stop err : Opaque q : r)) a
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) (Sem (effect : (extra ++ (Stop err : Opaque q : r))) a
 -> Sem (extra ++ (Stop err : Opaque q : r)) a)
-> Sem (effect : (extra ++ (Stop err : Opaque q : r))) a
-> Sem (extra ++ (Stop err : Opaque q : r)) a
forall a b. (a -> b) -> a -> b
$
      (forall (e :: Effect).
 ElemOf e (effect : Stop err : Opaque q : r)
 -> ElemOf e (effect : (extra ++ (Stop err : Opaque q : r))))
-> Sem (effect : Stop err : Opaque q : r) a
-> Sem (effect : (extra ++ (Stop err : Opaque q : r))) a
forall (r :: EffectRow) (r' :: EffectRow) a.
(forall (e :: Effect). ElemOf e r -> ElemOf e r')
-> Sem r a -> Sem r' a
restack (SList '[effect]
-> SList extra
-> ElemOf e (Append '[effect] (Stop err : Opaque q : r))
-> ElemOf e (Append '[effect] (extra ++ (Stop err : Opaque q : r)))
forall {a} (right :: [a]) (e :: a) (left :: [a]) (mid :: [a]).
SList left
-> SList mid
-> ElemOf e (Append left right)
-> ElemOf e (Append left (Append mid right))
injectMembership (forall (l :: EffectRow). KnownList l => SList l
forall {k} (l :: [k]). KnownList l => SList l
singList @'[effect]) (forall (l :: EffectRow). KnownList l => SList l
forall {k} (l :: [k]). KnownList l => SList l
singList @extra)) (Sem (effect : Stop err : Opaque q : r) a
 -> Sem (effect : (extra ++ (Stop err : Opaque q : r))) a)
-> Sem (effect : Stop err : Opaque q : r) a
-> Sem (effect : (extra ++ (Stop err : Opaque q : r))) a
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 (q :: Effect).
 param -> InterpreterFor effect (Stop err : Opaque q : r))
-> InterpreterFor (Scoped param effect !! err) r
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) ->
    param
-> (resource -> Sem (extra ++ (Stop err : Opaque q : r)) a)
-> Sem (Stop err : Opaque q : r) a
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
      Sem (effect : Stop err : Opaque q : r) a
-> (Sem (effect : Stop err : Opaque q : r) a
    -> Sem (effect : (extra ++ (Stop err : Opaque q : r))) a)
-> Sem (effect : (extra ++ (Stop err : Opaque q : r))) a
forall a b. a -> (a -> b) -> b
& (forall (e :: Effect).
 ElemOf e (effect : Stop err : Opaque q : r)
 -> ElemOf e (effect : (extra ++ (Stop err : Opaque q : r))))
-> Sem (effect : Stop err : Opaque q : r) a
-> Sem (effect : (extra ++ (Stop err : Opaque q : r))) a
forall (r :: EffectRow) (r' :: EffectRow) a.
(forall (e :: Effect). ElemOf e r -> ElemOf e r')
-> Sem r a -> Sem r' a
restack (SList '[effect]
-> SList extra
-> ElemOf e (Append '[effect] (Stop err : Opaque q : r))
-> ElemOf e (Append '[effect] (extra ++ (Stop err : Opaque q : r)))
forall {a} (right :: [a]) (e :: a) (left :: [a]) (mid :: [a]).
SList left
-> SList mid
-> ElemOf e (Append left right)
-> ElemOf e (Append left (Append mid right))
injectMembership (forall (l :: EffectRow). KnownList l => SList l
forall {k} (l :: [k]). KnownList l => SList l
singList @'[effect]) (forall (l :: EffectRow). KnownList l => SList l
forall {k} (l :: [k]). KnownList l => SList l
singList @extra))
      Sem (effect : (extra ++ (Stop err : Opaque q : r))) a
-> (Sem (effect : (extra ++ (Stop err : Opaque q : r))) a
    -> Sem (extra ++ (Stop err : Opaque q : r)) a)
-> Sem (extra ++ (Stop err : Opaque q : r)) a
forall a b. a -> (a -> b) -> b
& (forall (rInitial :: EffectRow) x.
 effect (Sem rInitial) x
 -> Tactical
      effect (Sem rInitial) (extra ++ (Stop err : Opaque q : r)) x)
-> Sem (effect : (extra ++ (Stop err : Opaque q : r))) a
-> Sem (extra ++ (Stop err : Opaque q : r)) a
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 -> Sem (extra ++ (Stop err : Opaque q : r)) x
-> Sem
     (WithTactics
        effect f (Sem rInitial) (extra ++ (Stop err : Opaque q : r)))
     (f x)
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 (q :: Effect).
 param -> InterpreterFor effect (Stop err : Opaque q : r))
-> InterpreterFor (Scoped param effect !! err) r
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 (Sem (extra ++ (Stop err : Opaque q : r)) a
 -> Sem (Stop err : Opaque q : r) a)
-> Sem (extra ++ (Stop err : Opaque q : r)) a
-> Sem (Stop err : Opaque q : r) a
forall a b. (a -> b) -> a -> b
$
      Sem (effect : Stop err : Opaque q : r) a
sem
      Sem (effect : Stop err : Opaque q : r) a
-> (Sem (effect : Stop err : Opaque q : r) a
    -> Sem (effect : (extra ++ (Stop err : Opaque q : r))) a)
-> Sem (effect : (extra ++ (Stop err : Opaque q : r))) a
forall a b. a -> (a -> b) -> b
& (forall (e :: Effect).
 ElemOf e (effect : Stop err : Opaque q : r)
 -> ElemOf e (effect : (extra ++ (Stop err : Opaque q : r))))
-> Sem (effect : Stop err : Opaque q : r) a
-> Sem (effect : (extra ++ (Stop err : Opaque q : r))) a
forall (r :: EffectRow) (r' :: EffectRow) a.
(forall (e :: Effect). ElemOf e r -> ElemOf e r')
-> Sem r a -> Sem r' a
restack (SList '[effect]
-> SList extra
-> ElemOf e (Append '[effect] (Stop err : Opaque q : r))
-> ElemOf e (Append '[effect] (extra ++ (Stop err : Opaque q : r)))
forall {a} (right :: [a]) (e :: a) (left :: [a]) (mid :: [a]).
SList left
-> SList mid
-> ElemOf e (Append left right)
-> ElemOf e (Append left (Append mid right))
injectMembership (forall (l :: EffectRow). KnownList l => SList l
forall {k} (l :: [k]). KnownList l => SList l
singList @'[effect]) (forall (l :: EffectRow). KnownList l => SList l
forall {k} (l :: [k]). KnownList l => SList l
singList @extra))
      Sem (effect : (extra ++ (Stop err : Opaque q : r))) a
-> (Sem (effect : (extra ++ (Stop err : Opaque q : r))) a
    -> Sem (extra ++ (Stop err : Opaque q : r)) a)
-> Sem (extra ++ (Stop err : Opaque q : r)) a
forall a b. a -> (a -> b) -> b
& (forall (rInitial :: EffectRow) x.
 effect (Sem rInitial) x
 -> Tactical
      effect (Sem rInitial) (extra ++ (Stop err : Opaque q : r)) x)
-> Sem (effect : (extra ++ (Stop err : Opaque q : r))) a
-> Sem (extra ++ (Stop err : Opaque q : r)) a
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 -> Sem (extra ++ (Stop err : Opaque q : r)) x
-> Sem
     (WithTactics
        effect f (Sem rInitial) (extra ++ (Stop err : Opaque q : r)))
     (f x)
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 (q :: Effect).
 param -> InterpreterFor (effect !! err) (Opaque q : r))
-> InterpreterFor (Scoped param (effect !! err)) r
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 ->
    param -> (resource -> Sem (Opaque q : r) a) -> Sem (Opaque q : r) a
forall (q :: Effect) x.
param -> (resource -> Sem (Opaque q : r) x) -> Sem (Opaque q : r) x
withResource param
param \ resource
r ->
      (forall x (r0 :: EffectRow).
 effect (Sem r0) x
 -> Tactical (effect !! err) (Sem r0) (Stop err : Opaque q : r) x)
-> forall {a}.
   Sem ((effect !! err) : Opaque q : r) a -> Sem (Opaque q : r) a
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 (resource
-> effect (Sem r0) x
-> Tactical (effect !! err) (Sem r0) (Stop err : 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
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 (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
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 param -> (resource -> Sem (Opaque q : r) x) -> Sem (Opaque q : r) x
forall (q :: Effect) x.
param -> (resource -> Sem (Opaque q : r) x) -> Sem (Opaque q : r) x
withResource \ resource
r effect (Sem r0) x
e -> Sem (Stop err : Opaque q : r) x
-> Sem
     (WithTactics (effect !! err) f (Sem r0) (Stop err : Opaque q : r))
     (f x)
forall (m :: * -> *) (f :: * -> *) (r :: EffectRow) (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 : Opaque q : r) x
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 (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)
-> forall {a}.
   Sem (Scoped param (Resumable err effect) : r) a -> Sem r a
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 (resource -> Sem (Opaque q : r) x)
-> Sem (Opaque q : r) resource -> Sem (Opaque q : r) x
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Sem r resource -> Sem (Opaque q : r) resource
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 (q :: Effect).
 param -> InterpreterFor (effect !! err) (Opaque q : r))
-> InterpreterFor (Scoped param (effect !! err)) r
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) ->
    param
-> (resource -> Sem (extra ++ (Opaque q : r)) a)
-> Sem (Opaque q : r) a
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
        Sem ((effect !! err) : Opaque q : r) a
-> (Sem ((effect !! err) : Opaque q : r) a
    -> Sem ((effect !! err) : (extra ++ (Opaque q : r))) a)
-> Sem ((effect !! err) : (extra ++ (Opaque q : r))) a
forall a b. a -> (a -> b) -> b
& (forall (e :: Effect).
 ElemOf e ((effect !! err) : Opaque q : r)
 -> ElemOf e ((effect !! err) : (extra ++ (Opaque q : r))))
-> Sem ((effect !! err) : Opaque q : r) a
-> Sem ((effect !! err) : (extra ++ (Opaque q : r))) a
forall (r :: EffectRow) (r' :: EffectRow) a.
(forall (e :: Effect). ElemOf e r -> ElemOf e r')
-> Sem r a -> Sem r' a
restack (SList '[effect !! err]
-> SList extra
-> ElemOf e (Append '[effect !! err] (Opaque q : r))
-> ElemOf e (Append '[effect !! err] (extra ++ (Opaque q : r)))
forall {a} (right :: [a]) (e :: a) (left :: [a]) (mid :: [a]).
SList left
-> SList mid
-> ElemOf e (Append left right)
-> ElemOf e (Append left (Append mid right))
injectMembership (forall (l :: EffectRow). KnownList l => SList l
forall {k} (l :: [k]). KnownList l => SList l
singList @'[effect !! err]) (forall (l :: EffectRow). KnownList l => SList l
forall {k} (l :: [k]). KnownList l => SList l
singList @extra))
        Sem ((effect !! err) : (extra ++ (Opaque q : r))) a
-> (Sem ((effect !! err) : (extra ++ (Opaque q : r))) a
    -> Sem (extra ++ (Opaque q : r)) a)
-> Sem (extra ++ (Opaque q : r)) a
forall a b. a -> (a -> b) -> b
& (forall x (r0 :: EffectRow).
 effect (Sem r0) x
 -> Tactical
      (effect !! err) (Sem r0) (Stop err : (extra ++ (Opaque q : r))) x)
-> InterpreterFor (effect !! err) (extra ++ (Opaque q : 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 : (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 (q :: Effect).
 param -> InterpreterFor (effect !! err) (Opaque q : r))
-> InterpreterFor (Scoped param (effect !! err)) r
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) ->
    param
-> (resource -> Sem (extra ++ (Opaque q : r)) a)
-> Sem (Opaque q : r) a
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
        Sem ((effect !! err) : Opaque q : r) a
-> (Sem ((effect !! err) : Opaque q : r) a
    -> Sem ((effect !! err) : (extra ++ (Opaque q : r))) a)
-> Sem ((effect !! err) : (extra ++ (Opaque q : r))) a
forall a b. a -> (a -> b) -> b
& (forall (e :: Effect).
 ElemOf e ((effect !! err) : Opaque q : r)
 -> ElemOf e ((effect !! err) : (extra ++ (Opaque q : r))))
-> Sem ((effect !! err) : Opaque q : r) a
-> Sem ((effect !! err) : (extra ++ (Opaque q : r))) a
forall (r :: EffectRow) (r' :: EffectRow) a.
(forall (e :: Effect). ElemOf e r -> ElemOf e r')
-> Sem r a -> Sem r' a
restack (SList '[effect !! err]
-> SList extra
-> ElemOf e (Append '[effect !! err] (Opaque q : r))
-> ElemOf e (Append '[effect !! err] (extra ++ (Opaque q : r)))
forall {a} (right :: [a]) (e :: a) (left :: [a]) (mid :: [a]).
SList left
-> SList mid
-> ElemOf e (Append left right)
-> ElemOf e (Append left (Append mid right))
injectMembership (forall (l :: EffectRow). KnownList l => SList l
forall {k} (l :: [k]). KnownList l => SList l
singList @'[effect !! err]) (forall (l :: EffectRow). KnownList l => SList l
forall {k} (l :: [k]). KnownList l => SList l
singList @extra))
        Sem ((effect !! err) : (extra ++ (Opaque q : r))) a
-> (Sem ((effect !! err) : (extra ++ (Opaque q : r))) a
    -> Sem (extra ++ (Opaque q : r)) a)
-> Sem (extra ++ (Opaque q : r)) a
forall a b. a -> (a -> b) -> b
& (forall x (r0 :: EffectRow).
 effect (Sem r0) x
 -> Tactical
      (effect !! err) (Sem r0) (Stop err : (extra ++ (Opaque q : r))) x)
-> InterpreterFor (effect !! err) (extra ++ (Opaque q : 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 \ effect (Sem r0) x
e ->
          Sem (Stop err : (extra ++ (Opaque q : r))) x
-> Sem
     (WithTactics
        (effect !! err) f (Sem r0) (Stop err : (extra ++ (Opaque q : r))))
     (f x)
forall (m :: * -> *) (f :: * -> *) (r :: EffectRow) (e :: Effect)
       a.
Functor f =>
Sem r a -> Sem (WithTactics e f m r) (f a)
liftT (Sem (Stop err : (extra ++ (Opaque q : r))) x
 -> Sem
      (WithTactics
         (effect !! err) f (Sem r0) (Stop err : (extra ++ (Opaque q : r))))
      (f x))
-> Sem (Stop err : (extra ++ (Opaque q : r))) x
-> Sem
     (WithTactics
        (effect !! err) f (Sem r0) (Stop err : (extra ++ (Opaque q : r))))
     (f x)
forall a b. (a -> b) -> a -> b
$
          (forall (e :: Effect).
 ElemOf e (Stop err : (extra ++ r))
 -> ElemOf e (Stop err : (extra ++ (Opaque q : r))))
-> Sem (Stop err : (extra ++ r)) x
-> Sem (Stop err : (extra ++ (Opaque q : r))) x
forall (r :: EffectRow) (r' :: EffectRow) a.
(forall (e :: Effect). ElemOf e r -> ElemOf e r')
-> Sem r a -> Sem r' a
restack (forall (right :: EffectRow) (e :: Effect) (left :: EffectRow)
       (mid :: EffectRow).
SList left
-> SList mid
-> ElemOf e (Append left right)
-> ElemOf e (Append left (Append mid right))
forall {a} (right :: [a]) (e :: a) (left :: [a]) (mid :: [a]).
SList left
-> SList mid
-> ElemOf e (Append left right)
-> ElemOf e (Append left (Append mid right))
injectMembership @r (forall (l :: EffectRow). KnownList l => SList l
forall {k} (l :: [k]). KnownList l => SList l
singList @(Stop err : extra)) (forall (l :: EffectRow). KnownList l => SList l
forall {k} (l :: [k]). KnownList l => SList l
singList @'[Opaque q])) (resource -> effect (Sem r0) x -> Sem (Stop err : (extra ++ r)) x
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 -> param -> Sem (extra ++ (Opaque q : r)) x -> Sem (Opaque q : r) x
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 ())) ((effect (Sem r0) x -> Sem (Stop err : (extra ++ r)) x)
-> () -> effect (Sem r0) x -> Sem (Stop err : (extra ++ r)) x
forall a b. a -> b -> a
const effect (Sem r0) x -> Sem (Stop err : (extra ++ r)) x
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 (q :: Effect).
 param -> InterpreterFor (effect !! ei) (Stop eo : Opaque q : r))
-> InterpreterFor (Scoped param (effect !! ei) !! eo) r
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 ->
    param
-> (resource -> Sem (Stop eo : Opaque q : r) a)
-> Sem (Stop eo : Opaque q : r) a
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 x (r0 :: EffectRow).
 effect (Sem r0) x
 -> Tactical
      (effect !! ei) (Sem r0) (Stop ei : Stop eo : Opaque q : r) x)
-> forall {a}.
   Sem ((effect !! ei) : Stop eo : Opaque q : r) a
   -> Sem (Stop eo : Opaque q : r) a
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 (resource
-> effect (Sem r0) x
-> Tactical
     (effect !! ei) (Sem r0) (Stop ei : 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
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 (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
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 param
-> (resource -> Sem (Stop eo : Opaque q : r) x)
-> Sem (Stop eo : Opaque q : r) x
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 -> Sem (Stop ei : Stop eo : Opaque q : r) x
-> Sem
     (WithTactics
        (effect !! ei) f (Sem r0) (Stop ei : Stop eo : Opaque q : r))
     (f x)
forall (m :: * -> *) (f :: * -> *) (r :: EffectRow) (e :: Effect)
       a.
Functor f =>
Sem r a -> Sem (WithTactics e f m r) (f a)
liftT (resource
-> effect (Sem r0) x -> Sem (Stop ei : Stop eo : Opaque q : r) x
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 (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)
-> forall {a}.
   Sem (Resumable eo (Scoped param (Resumable ei effect)) : r) a
   -> Sem r a
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 (resource -> Sem (Stop eo : Opaque q : r) x)
-> Sem (Stop eo : Opaque q : r) resource
-> Sem (Stop eo : Opaque q : r) x
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Sem (Stop eo : r) resource -> Sem (Stop eo : Opaque q : r) resource
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 (q :: Effect).
 param -> InterpreterFor (effect !! ei) (Stop eo : Opaque q : r))
-> InterpreterFor (Scoped param (effect !! ei) !! eo) r
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) ->
    param
-> (resource -> Sem (extra ++ (Stop eo : Opaque q : r)) a)
-> Sem (Stop eo : Opaque q : r) a
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
        Sem ((effect !! ei) : Stop eo : Opaque q : r) a
-> (Sem ((effect !! ei) : Stop eo : Opaque q : r) a
    -> Sem ((effect !! ei) : (extra ++ (Stop eo : Opaque q : r))) a)
-> Sem ((effect !! ei) : (extra ++ (Stop eo : Opaque q : r))) a
forall a b. a -> (a -> b) -> b
& (forall (e :: Effect).
 ElemOf e ((effect !! ei) : Stop eo : Opaque q : r)
 -> ElemOf e ((effect !! ei) : (extra ++ (Stop eo : Opaque q : r))))
-> Sem ((effect !! ei) : Stop eo : Opaque q : r) a
-> Sem ((effect !! ei) : (extra ++ (Stop eo : Opaque q : r))) a
forall (r :: EffectRow) (r' :: EffectRow) a.
(forall (e :: Effect). ElemOf e r -> ElemOf e r')
-> Sem r a -> Sem r' a
restack (SList '[effect !! ei]
-> SList extra
-> ElemOf e (Append '[effect !! ei] (Stop eo : Opaque q : r))
-> ElemOf
     e (Append '[effect !! ei] (extra ++ (Stop eo : Opaque q : r)))
forall {a} (right :: [a]) (e :: a) (left :: [a]) (mid :: [a]).
SList left
-> SList mid
-> ElemOf e (Append left right)
-> ElemOf e (Append left (Append mid right))
injectMembership (forall (l :: EffectRow). KnownList l => SList l
forall {k} (l :: [k]). KnownList l => SList l
singList @'[effect !! ei]) (forall (l :: EffectRow). KnownList l => SList l
forall {k} (l :: [k]). KnownList l => SList l
singList @extra))
        Sem ((effect !! ei) : (extra ++ (Stop eo : Opaque q : r))) a
-> (Sem ((effect !! ei) : (extra ++ (Stop eo : Opaque q : r))) a
    -> Sem (extra ++ (Stop eo : Opaque q : r)) a)
-> Sem (extra ++ (Stop eo : Opaque q : r)) a
forall a b. a -> (a -> b) -> b
& (forall x (r0 :: EffectRow).
 effect (Sem r0) x
 -> Tactical
      (effect !! ei)
      (Sem r0)
      (Stop ei : (extra ++ (Stop eo : Opaque q : r)))
      x)
-> InterpreterFor
     (effect !! ei) (extra ++ (Stop eo : Opaque q : 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 : (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 (q :: Effect).
 param -> InterpreterFor (effect !! ei) (Stop eo : Opaque q : r))
-> InterpreterFor (Scoped param (effect !! ei) !! eo) r
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) ->
    param
-> (resource -> Sem (extra ++ (Stop eo : Opaque q : r)) a)
-> Sem (Stop eo : Opaque q : r) a
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
      Sem ((effect !! ei) : Stop eo : Opaque q : r) a
-> (Sem ((effect !! ei) : Stop eo : Opaque q : r) a
    -> Sem ((effect !! ei) : (extra ++ (Stop eo : Opaque q : r))) a)
-> Sem ((effect !! ei) : (extra ++ (Stop eo : Opaque q : r))) a
forall a b. a -> (a -> b) -> b
& (forall (e :: Effect).
 ElemOf e ((effect !! ei) : Stop eo : Opaque q : r)
 -> ElemOf e ((effect !! ei) : (extra ++ (Stop eo : Opaque q : r))))
-> Sem ((effect !! ei) : Stop eo : Opaque q : r) a
-> Sem ((effect !! ei) : (extra ++ (Stop eo : Opaque q : r))) a
forall (r :: EffectRow) (r' :: EffectRow) a.
(forall (e :: Effect). ElemOf e r -> ElemOf e r')
-> Sem r a -> Sem r' a
restack (SList '[effect !! ei]
-> SList extra
-> ElemOf e (Append '[effect !! ei] (Stop eo : Opaque q : r))
-> ElemOf
     e (Append '[effect !! ei] (extra ++ (Stop eo : Opaque q : r)))
forall {a} (right :: [a]) (e :: a) (left :: [a]) (mid :: [a]).
SList left
-> SList mid
-> ElemOf e (Append left right)
-> ElemOf e (Append left (Append mid right))
injectMembership (forall (l :: EffectRow). KnownList l => SList l
forall {k} (l :: [k]). KnownList l => SList l
singList @'[effect !! ei]) (forall (l :: EffectRow). KnownList l => SList l
forall {k} (l :: [k]). KnownList l => SList l
singList @extra))
      Sem ((effect !! ei) : (extra ++ (Stop eo : Opaque q : r))) a
-> (Sem ((effect !! ei) : (extra ++ (Stop eo : Opaque q : r))) a
    -> Sem (extra ++ (Stop eo : Opaque q : r)) a)
-> Sem (extra ++ (Stop eo : Opaque q : r)) a
forall a b. a -> (a -> b) -> b
& (forall x (r0 :: EffectRow).
 effect (Sem r0) x
 -> Tactical
      (effect !! ei)
      (Sem r0)
      (Stop ei : (extra ++ (Stop eo : Opaque q : r)))
      x)
-> InterpreterFor
     (effect !! ei) (extra ++ (Stop eo : Opaque q : 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 \ effect (Sem r0) x
e ->
        Sem (Stop ei : (extra ++ (Stop eo : Opaque q : r))) x
-> Sem
     (WithTactics
        (effect !! ei)
        f
        (Sem r0)
        (Stop ei : (extra ++ (Stop eo : Opaque q : r))))
     (f x)
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 (q :: Effect).
 param -> InterpreterFor (effect !! ei) (Stop eo : Opaque q : r))
-> InterpreterFor (Scoped param (effect !! ei) !! eo) r
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) ->
    param
-> Sem (extra ++ (Stop eo : Opaque q : r)) a
-> Sem (Stop eo : Opaque q : r) a
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
        Sem ((effect !! ei) : Stop eo : Opaque q : r) a
-> (Sem ((effect !! ei) : Stop eo : Opaque q : r) a
    -> Sem ((effect !! ei) : (extra ++ (Stop eo : Opaque q : r))) a)
-> Sem ((effect !! ei) : (extra ++ (Stop eo : Opaque q : r))) a
forall a b. a -> (a -> b) -> b
& (forall (e :: Effect).
 ElemOf e ((effect !! ei) : Stop eo : Opaque q : r)
 -> ElemOf e ((effect !! ei) : (extra ++ (Stop eo : Opaque q : r))))
-> Sem ((effect !! ei) : Stop eo : Opaque q : r) a
-> Sem ((effect !! ei) : (extra ++ (Stop eo : Opaque q : r))) a
forall (r :: EffectRow) (r' :: EffectRow) a.
(forall (e :: Effect). ElemOf e r -> ElemOf e r')
-> Sem r a -> Sem r' a
restack (SList '[effect !! ei]
-> SList extra
-> ElemOf e (Append '[effect !! ei] (Stop eo : Opaque q : r))
-> ElemOf
     e (Append '[effect !! ei] (extra ++ (Stop eo : Opaque q : r)))
forall {a} (right :: [a]) (e :: a) (left :: [a]) (mid :: [a]).
SList left
-> SList mid
-> ElemOf e (Append left right)
-> ElemOf e (Append left (Append mid right))
injectMembership (forall (l :: EffectRow). KnownList l => SList l
forall {k} (l :: [k]). KnownList l => SList l
singList @'[effect !! ei]) (forall (l :: EffectRow). KnownList l => SList l
forall {k} (l :: [k]). KnownList l => SList l
singList @extra))
        Sem ((effect !! ei) : (extra ++ (Stop eo : Opaque q : r))) a
-> (Sem ((effect !! ei) : (extra ++ (Stop eo : Opaque q : r))) a
    -> Sem (extra ++ (Stop eo : Opaque q : r)) a)
-> Sem (extra ++ (Stop eo : Opaque q : r)) a
forall a b. a -> (a -> b) -> b
& (forall x (r0 :: EffectRow).
 effect (Sem r0) x
 -> Tactical
      (effect !! ei)
      (Sem r0)
      (Stop ei : (extra ++ (Stop eo : Opaque q : r)))
      x)
-> InterpreterFor
     (effect !! ei) (extra ++ (Stop eo : Opaque q : 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 \ effect (Sem r0) x
e ->
          Sem (Stop ei : (extra ++ (Stop eo : Opaque q : r))) x
-> Sem
     (WithTactics
        (effect !! ei)
        f
        (Sem r0)
        (Stop ei : (extra ++ (Stop eo : Opaque q : r))))
     (f x)
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)