{-# 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 (Scoped (InScope, Run))
import Polysemy.Internal.Sing (KnownList (singList))
import Polysemy.Internal.Tactics (liftT)
import Polysemy.Internal.Union (Weaving (Weaving), extendMembershipLeft, injWeaving, injectMembership, weave)

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 #-}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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