{-# options_haddock prune #-}
module Polysemy.Conc.Interpreter.Scoped where
import GHC.Err (errorWithoutStackTrace)
import Polysemy.Internal (Sem (Sem), hoistSem, liftSem, runSem)
import Polysemy.Internal.Sing (KnownList (singList))
import Polysemy.Internal.Tactics (liftT, runTactics)
import Polysemy.Internal.Union (
Union (Union),
Weaving (Weaving),
decomp,
extendMembershipLeft,
hoist,
injWeaving,
injectMembership,
)
import Polysemy.Membership (ElemOf)
import Polysemy.Resume (Stop, runStop, type (!!))
import Polysemy.Resume.Effect.Resumable (Resumable (Resumable))
import Polysemy.Conc.Effect.Scoped (Scoped (InScope, Run))
interpretWeaving ::
∀ e r .
(∀ x . Weaving e (Sem (e : r)) x -> Sem r x) ->
InterpreterFor e r
interpretWeaving :: forall (e :: Effect) (r :: [Effect]).
(forall x. Weaving e (Sem (e : r)) x -> Sem r x)
-> InterpreterFor e r
interpretWeaving forall x. Weaving e (Sem (e : r)) x -> Sem r x
h (Sem forall (m :: * -> *).
Monad m =>
(forall x. Union (e : r) (Sem (e : r)) x -> m x) -> m a
m) =
(forall (m :: * -> *).
Monad m =>
(forall x. Union r (Sem r) x -> m x) -> m a)
-> Sem r a
forall (r :: [Effect]) a.
(forall (m :: * -> *).
Monad m =>
(forall x. Union r (Sem r) x -> m x) -> m a)
-> Sem r a
Sem \ forall x. Union r (Sem r) x -> m x
k -> (forall x. Union (e : r) (Sem (e : r)) x -> m x) -> m a
forall (m :: * -> *).
Monad m =>
(forall x. Union (e : r) (Sem (e : r)) x -> m x) -> m a
m ((forall x. Union (e : r) (Sem (e : r)) x -> m x) -> m a)
-> (forall x. Union (e : r) (Sem (e : r)) x -> m x) -> m a
forall a b. (a -> b) -> a -> b
$ Union (e : r) (Sem (e : r)) x
-> Either (Union r (Sem (e : r)) x) (Weaving e (Sem (e : r)) x)
forall (e :: Effect) (r :: [Effect]) (m :: * -> *) a.
Union (e : r) m a -> Either (Union r m a) (Weaving e m a)
decomp (Union (e : r) (Sem (e : r)) x
-> Either (Union r (Sem (e : r)) x) (Weaving e (Sem (e : r)) x))
-> (Either (Union r (Sem (e : r)) x) (Weaving e (Sem (e : r)) x)
-> m x)
-> Union (e : r) (Sem (e : r)) x
-> m x
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> \case
Right Weaving e (Sem (e : r)) x
wav -> Sem r x
-> forall (m :: * -> *).
Monad m =>
(forall x. Union r (Sem r) x -> m x) -> m x
forall (r :: [Effect]) a.
Sem r a
-> forall (m :: * -> *).
Monad m =>
(forall x. Union r (Sem r) x -> m x) -> m a
runSem (Weaving e (Sem (e : r)) x -> Sem r x
forall x. Weaving e (Sem (e : r)) x -> Sem r x
h Weaving e (Sem (e : r)) x
wav) forall x. Union r (Sem r) x -> m x
k
Left Union r (Sem (e : r)) x
g -> Union r (Sem r) x -> m x
forall x. Union r (Sem r) x -> m x
k ((forall x. Sem (e : r) x -> Sem r x)
-> Union r (Sem (e : r)) x -> Union r (Sem r) x
forall (m :: * -> *) (n :: * -> *) (r :: [Effect]) a.
(forall x. m x -> n x) -> Union r m a -> Union r n a
hoist ((forall x. Weaving e (Sem (e : r)) x -> Sem r x)
-> forall x. Sem (e : r) x -> Sem r x
forall (e :: Effect) (r :: [Effect]).
(forall x. Weaving e (Sem (e : r)) x -> Sem r x)
-> InterpreterFor e r
interpretWeaving forall x. Weaving e (Sem (e : r)) x -> Sem r x
h) Union r (Sem (e : r)) x
g)
restack :: (∀ e . ElemOf e r -> ElemOf e r')
-> Sem r a
-> Sem r' a
restack :: forall (r :: [Effect]) (r' :: [Effect]) a.
(forall (e :: Effect). ElemOf e r -> ElemOf e r')
-> Sem r a -> Sem r' a
restack forall (e :: Effect). ElemOf e r -> ElemOf e r'
n =
(forall x. Union r (Sem r) x -> Union r' (Sem r') x)
-> Sem r a -> Sem r' a
forall (r :: [Effect]) (r' :: [Effect]) a.
(forall x. Union r (Sem r) x -> Union r' (Sem r') x)
-> Sem r a -> Sem r' a
hoistSem ((forall x. Union r (Sem r) x -> Union r' (Sem r') x)
-> Sem r a -> Sem r' a)
-> (forall x. Union r (Sem r) x -> Union r' (Sem r') x)
-> Sem r a
-> Sem r' a
forall a b. (a -> b) -> a -> b
$ \ (Union ElemOf e r
pr Weaving e (Sem r) x
wav) -> (forall x. Sem r x -> Sem r' x)
-> Union r' (Sem r) x -> Union r' (Sem r') x
forall (m :: * -> *) (n :: * -> *) (r :: [Effect]) a.
(forall x. m x -> n x) -> Union r m a -> Union r n a
hoist ((forall (e :: Effect). ElemOf e r -> ElemOf e r')
-> Sem r x -> Sem r' x
forall (r :: [Effect]) (r' :: [Effect]) a.
(forall (e :: Effect). ElemOf e r -> ElemOf e r')
-> Sem r a -> Sem r' a
restack forall (e :: Effect). ElemOf e r -> ElemOf e r'
n) (ElemOf e r' -> Weaving e (Sem r) x -> Union r' (Sem r) x
forall (e :: Effect) (r :: [Effect]) (mWoven :: * -> *) a.
ElemOf e r -> Weaving e mWoven a -> Union r mWoven a
Union (ElemOf e r -> ElemOf e r'
forall (e :: Effect). ElemOf e r -> ElemOf e r'
n ElemOf e r
pr) Weaving e (Sem r) x
wav)
{-# inline restack #-}
interpretScopedH ::
∀ resource param effect r .
(∀ x . param -> (resource -> Sem r x) -> Sem r x) ->
(∀ r0 x . resource -> effect (Sem r0) x -> Tactical effect (Sem r0) r x) ->
InterpreterFor (Scoped param effect) r
interpretScopedH :: forall resource param (effect :: Effect) (r :: [Effect]).
(forall x. param -> (resource -> Sem r x) -> Sem r x)
-> (forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Tactical effect (Sem r0) r x)
-> InterpreterFor (Scoped param effect) r
interpretScopedH forall x. param -> (resource -> Sem r x) -> Sem r x
withResource forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Tactical effect (Sem r0) r x
scopedHandler =
resource -> InterpreterFor (Scoped param effect) r
go ([Char] -> resource
forall a. [Char] -> a
errorWithoutStackTrace [Char]
"top level run")
where
go :: resource -> InterpreterFor (Scoped param effect) r
go :: resource -> InterpreterFor (Scoped param effect) r
go resource
resource =
(forall x.
Weaving (Scoped param effect) (Sem (Scoped param effect : r)) x
-> Sem r x)
-> InterpreterFor (Scoped param effect) r
forall (e :: Effect) (r :: [Effect]).
(forall x. Weaving e (Sem (e : r)) x -> Sem r x)
-> InterpreterFor e r
interpretWeaving \ (Weaving Scoped param effect (Sem rInitial) a
effect f ()
s forall x. f (Sem rInitial x) -> Sem (Scoped param effect : r) (f x)
wv f a -> x
ex forall x. f x -> Maybe x
ins) -> case Scoped param effect (Sem rInitial) a
effect of
Run effect (Sem rInitial) a
act ->
f a -> x
ex (f a -> x) -> Sem r (f a) -> Sem r x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f ()
-> (forall x. f (Sem rInitial x) -> Sem (effect : r) (f x))
-> (forall x. f x -> Maybe x)
-> (forall x. f (Sem rInitial x) -> Sem r (f x))
-> Sem (Tactics f (Sem rInitial) (effect : r) : r) (f a)
-> Sem r (f a)
forall (f :: * -> *) (m :: * -> *) (r2 :: [Effect]) (r :: [Effect])
a.
Functor f =>
f ()
-> (forall x. f (m x) -> Sem r2 (f x))
-> (forall x. f x -> Maybe x)
-> (forall x. f (m x) -> Sem r (f x))
-> Sem (Tactics f m r2 : r) a
-> Sem r a
runTactics f ()
s (Sem r (f x) -> Sem (effect : r) (f x)
forall (e :: Effect) (r :: [Effect]) a. Sem r a -> Sem (e : r) a
raise (Sem r (f x) -> Sem (effect : r) (f x))
-> (f (Sem rInitial x) -> Sem r (f x))
-> f (Sem rInitial x)
-> Sem (effect : r) (f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. resource -> InterpreterFor (Scoped param effect) r
go resource
resource (Sem (Scoped param effect : r) (f x) -> Sem r (f x))
-> (f (Sem rInitial x) -> Sem (Scoped param effect : r) (f x))
-> f (Sem rInitial x)
-> Sem r (f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Sem rInitial x) -> Sem (Scoped param effect : r) (f x)
forall x. f (Sem rInitial x) -> Sem (Scoped param effect : r) (f x)
wv) forall x. f x -> Maybe x
ins (resource -> InterpreterFor (Scoped param effect) r
go resource
resource (Sem (Scoped param effect : r) (f x) -> Sem r (f x))
-> (f (Sem rInitial x) -> Sem (Scoped param effect : r) (f x))
-> f (Sem rInitial x)
-> Sem r (f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Sem rInitial x) -> Sem (Scoped param effect : r) (f x)
forall x. f (Sem rInitial x) -> Sem (Scoped param effect : r) (f x)
wv)
(resource
-> effect (Sem rInitial) a -> Tactical effect (Sem rInitial) r a
forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Tactical effect (Sem r0) r x
scopedHandler resource
resource effect (Sem rInitial) a
act)
InScope param
param Sem rInitial a
main ->
param -> (resource -> Sem r x) -> Sem r x
forall x. param -> (resource -> Sem r x) -> Sem r x
withResource param
param \ resource
resource' -> f a -> x
ex (f a -> x) -> Sem r (f a) -> Sem r x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> resource -> InterpreterFor (Scoped param effect) r
go resource
resource' (f (Sem rInitial a) -> Sem (Scoped param effect : r) (f a)
forall x. f (Sem rInitial x) -> Sem (Scoped param effect : r) (f x)
wv (Sem rInitial a
main Sem rInitial a -> f () -> f (Sem rInitial a)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s))
{-# inline interpretScopedH #-}
interpretScopedH' ::
∀ resource param effect r .
(∀ e r0 x . param -> (resource -> Tactical e (Sem r0) r x) ->
Tactical e (Sem r0) r x) ->
(∀ r0 x .
resource -> effect (Sem r0) x ->
Tactical (Scoped param effect) (Sem r0) r x) ->
InterpreterFor (Scoped param effect) r
interpretScopedH' :: forall resource param (effect :: Effect) (r :: [Effect]).
(forall (e :: Effect) (r0 :: [Effect]) x.
param
-> (resource -> Tactical e (Sem r0) r x)
-> Tactical e (Sem r0) r x)
-> (forall (r0 :: [Effect]) x.
resource
-> effect (Sem r0) x
-> Tactical (Scoped param effect) (Sem r0) r x)
-> InterpreterFor (Scoped param effect) r
interpretScopedH' forall (e :: Effect) (r0 :: [Effect]) x.
param
-> (resource -> Tactical e (Sem r0) r x) -> Tactical e (Sem r0) r x
withResource forall (r0 :: [Effect]) x.
resource
-> effect (Sem r0) x -> Tactical (Scoped param effect) (Sem r0) r x
scopedHandler =
resource -> InterpreterFor (Scoped param effect) r
go ([Char] -> resource
forall a. [Char] -> a
errorWithoutStackTrace [Char]
"top level run")
where
go :: resource -> InterpreterFor (Scoped param effect) r
go :: resource -> InterpreterFor (Scoped param effect) r
go resource
resource =
(forall (rInitial :: [Effect]) x.
Scoped param effect (Sem rInitial) x
-> Tactical (Scoped param effect) (Sem rInitial) r x)
-> Sem (Scoped param effect : r) a -> Sem r a
forall (e :: Effect) (r :: [Effect]) a.
(forall (rInitial :: [Effect]) x.
e (Sem rInitial) x -> Tactical e (Sem rInitial) r x)
-> Sem (e : r) a -> Sem r a
interpretH \case
Run effect (Sem rInitial) x
act ->
resource
-> effect (Sem rInitial) x
-> Tactical (Scoped param effect) (Sem rInitial) r x
forall (r0 :: [Effect]) x.
resource
-> effect (Sem r0) x -> Tactical (Scoped param effect) (Sem r0) r x
scopedHandler resource
resource effect (Sem rInitial) x
act
InScope param
param Sem rInitial x
main ->
param
-> (resource -> Tactical (Scoped param effect) (Sem rInitial) r x)
-> Tactical (Scoped param effect) (Sem rInitial) r x
forall (e :: Effect) (r0 :: [Effect]) x.
param
-> (resource -> Tactical e (Sem r0) r x) -> Tactical e (Sem r0) r x
withResource param
param \ resource
resource' ->
Sem r (f x)
-> Sem (WithTactics (Scoped param effect) f (Sem rInitial) r) (f x)
forall (e :: Effect) (r :: [Effect]) a. Sem r a -> Sem (e : r) a
raise (Sem r (f x)
-> Sem
(WithTactics (Scoped param effect) f (Sem rInitial) r) (f x))
-> (Sem (Scoped param effect : r) (f x) -> Sem r (f x))
-> Sem (Scoped param effect : r) (f x)
-> Sem (WithTactics (Scoped param effect) f (Sem rInitial) r) (f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. resource -> InterpreterFor (Scoped param effect) r
go resource
resource' (Sem (Scoped param effect : r) (f x)
-> Sem
(WithTactics (Scoped param effect) f (Sem rInitial) r) (f x))
-> Sem
(WithTactics (Scoped param effect) f (Sem rInitial) r)
(Sem (Scoped param effect : r) (f x))
-> Sem (WithTactics (Scoped param effect) f (Sem rInitial) r) (f x)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Sem rInitial x
-> Sem
(WithTactics (Scoped param effect) f (Sem rInitial) r)
(Sem (Scoped param effect : r) (f x))
forall (m :: * -> *) a (e :: Effect) (f :: * -> *) (r :: [Effect]).
m a -> Sem (WithTactics e f m r) (Sem (e : r) (f a))
runT Sem rInitial x
main
{-# inline interpretScopedH' #-}
interpretScoped ::
∀ resource param effect r .
(∀ x . param -> (resource -> Sem r x) -> Sem r x) ->
(∀ m x . resource -> effect m x -> Sem r x) ->
InterpreterFor (Scoped param effect) r
interpretScoped :: forall resource param (effect :: Effect) (r :: [Effect]).
(forall x. param -> (resource -> Sem r x) -> Sem r x)
-> (forall (m :: * -> *) x. resource -> effect m x -> Sem r x)
-> InterpreterFor (Scoped param effect) r
interpretScoped forall x. param -> (resource -> Sem r x) -> Sem r x
withResource forall (m :: * -> *) x. resource -> effect m x -> Sem r x
scopedHandler =
(forall x. param -> (resource -> Sem r x) -> Sem r x)
-> (forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Tactical effect (Sem r0) r x)
-> InterpreterFor (Scoped param effect) r
forall resource param (effect :: Effect) (r :: [Effect]).
(forall x. param -> (resource -> Sem r x) -> Sem r x)
-> (forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Tactical effect (Sem r0) r x)
-> InterpreterFor (Scoped param effect) r
interpretScopedH forall x. param -> (resource -> Sem r x) -> Sem r x
withResource \ resource
r effect (Sem r0) x
e -> Sem r x -> Sem (WithTactics effect f (Sem r0) r) (f x)
forall (m :: * -> *) (f :: * -> *) (r :: [Effect]) (e :: Effect) a.
Functor f =>
Sem r a -> Sem (WithTactics e f m r) (f a)
liftT (resource -> effect (Sem r0) x -> Sem r x
forall (m :: * -> *) x. resource -> effect m x -> Sem r x
scopedHandler resource
r effect (Sem r0) x
e)
{-# inline interpretScoped #-}
interpretScopedAs ::
∀ resource param effect r .
(param -> Sem r resource) ->
(∀ m x . resource -> effect m x -> Sem r x) ->
InterpreterFor (Scoped param effect) r
interpretScopedAs :: forall resource param (effect :: Effect) (r :: [Effect]).
(param -> Sem r resource)
-> (forall (m :: * -> *) x. resource -> effect m x -> Sem r x)
-> InterpreterFor (Scoped param effect) r
interpretScopedAs param -> Sem r resource
resource =
(forall x. param -> (resource -> Sem r x) -> Sem r x)
-> (forall (m :: * -> *) x. resource -> effect m x -> Sem r x)
-> InterpreterFor (Scoped param effect) r
forall resource param (effect :: Effect) (r :: [Effect]).
(forall x. param -> (resource -> Sem r x) -> Sem r x)
-> (forall (m :: * -> *) x. resource -> effect m x -> Sem r x)
-> InterpreterFor (Scoped param effect) r
interpretScoped \ param
p resource -> Sem r x
use -> resource -> Sem r x
use (resource -> Sem r x) -> Sem r resource -> Sem r x
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< param -> Sem r resource
resource param
p
{-# inline interpretScopedAs #-}
interpretScopedWithH ::
∀ extra resource param effect 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 (Sem r0) r1 x) ->
InterpreterFor (Scoped param effect) r
interpretScopedWithH :: forall (extra :: [Effect]) resource param (effect :: Effect)
(r :: [Effect]) (r1 :: [Effect]).
(r1 ~ (extra ++ r), KnownList extra) =>
(forall x. param -> (resource -> Sem r1 x) -> Sem r x)
-> (forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Tactical effect (Sem r0) r1 x)
-> InterpreterFor (Scoped param effect) r
interpretScopedWithH forall x. param -> (resource -> Sem r1 x) -> Sem r x
withResource forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Tactical effect (Sem r0) r1 x
scopedHandler =
(forall x.
Weaving (Scoped param effect) (Sem (Scoped param effect : r)) x
-> Sem r x)
-> InterpreterFor (Scoped param effect) r
forall (e :: Effect) (r :: [Effect]).
(forall x. Weaving e (Sem (e : r)) x -> Sem r x)
-> InterpreterFor e r
interpretWeaving \case
Weaving (InScope param
param Sem rInitial a
main) f ()
s forall x. f (Sem rInitial x) -> Sem (Scoped param effect : r) (f x)
wv f a -> x
ex forall x. f x -> Maybe x
_ ->
f a -> x
ex (f a -> x) -> Sem r (f a) -> Sem r x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> param -> (resource -> Sem r1 (f a)) -> Sem r (f a)
forall x. param -> (resource -> Sem r1 x) -> Sem r x
withResource param
param \ resource
resource -> resource -> InterpreterFor (Scoped param effect) r1
inScope resource
resource (Sem (Scoped param effect : r1) (f a) -> Sem r1 (f a))
-> Sem (Scoped param effect : r1) (f a) -> Sem r1 (f a)
forall a b. (a -> b) -> a -> b
$
(forall (e :: Effect).
ElemOf e (Scoped param effect : r)
-> ElemOf e (Scoped param effect : r1))
-> Sem (Scoped param effect : r) (f a)
-> Sem (Scoped param effect : r1) (f a)
forall (r :: [Effect]) (r' :: [Effect]) a.
(forall (e :: Effect). ElemOf e r -> ElemOf e r')
-> Sem r a -> Sem r' a
restack
(SList '[Scoped param effect]
-> SList extra
-> ElemOf e (Append '[Scoped param effect] r)
-> ElemOf e (Append '[Scoped param effect] (extra ++ r))
forall {a} (right :: [a]) (e :: a) (left :: [a]) (mid :: [a]).
SList left
-> SList mid
-> ElemOf e (Append left right)
-> ElemOf e (Append left (Append mid right))
injectMembership
(forall (l :: [Effect]). KnownList l => SList l
forall {a} (l :: [a]). KnownList l => SList l
singList @'[Scoped param effect])
(forall (l :: [Effect]). KnownList l => SList l
forall {a} (l :: [a]). KnownList l => SList l
singList @extra)) (Sem (Scoped param effect : r) (f a)
-> Sem (Scoped param effect : r1) (f a))
-> Sem (Scoped param effect : r) (f a)
-> Sem (Scoped param effect : r1) (f a)
forall a b. (a -> b) -> a -> b
$ f (Sem rInitial a) -> Sem (Scoped param effect : r) (f a)
forall x. f (Sem rInitial x) -> Sem (Scoped param effect : r) (f x)
wv (Sem rInitial a
main Sem rInitial a -> f () -> f (Sem rInitial a)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s)
Weaving (Scoped param effect) (Sem (Scoped param effect : r)) x
_ ->
[Char] -> Sem r x
forall a. [Char] -> a
errorWithoutStackTrace [Char]
"top level Run"
where
inScope :: resource -> InterpreterFor (Scoped param effect) r1
inScope :: resource -> InterpreterFor (Scoped param effect) r1
inScope resource
resource =
(forall x.
Weaving (Scoped param effect) (Sem (Scoped param effect : r1)) x
-> Sem r1 x)
-> InterpreterFor (Scoped param effect) r1
forall (e :: Effect) (r :: [Effect]).
(forall x. Weaving e (Sem (e : r)) x -> Sem r x)
-> InterpreterFor e r
interpretWeaving \case
Weaving (InScope param
param Sem rInitial a
main) f ()
s forall x.
f (Sem rInitial x) -> Sem (Scoped param effect : r1) (f x)
wv f a -> x
ex forall x. f x -> Maybe x
_ ->
(forall (e :: Effect). ElemOf e r -> ElemOf e r1)
-> Sem r x -> Sem r1 x
forall (r :: [Effect]) (r' :: [Effect]) a.
(forall (e :: Effect). ElemOf e r -> ElemOf e r')
-> Sem r a -> Sem r' a
restack (SList extra -> ElemOf e r -> ElemOf e (extra ++ r)
forall {a} (l :: [a]) (r :: [a]) (e :: a).
SList l -> ElemOf e r -> ElemOf e (Append l r)
extendMembershipLeft (forall (l :: [Effect]). KnownList l => SList l
forall {a} (l :: [a]). KnownList l => SList l
singList @extra))
(f a -> x
ex (f a -> x) -> Sem r (f a) -> Sem r x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> param -> (resource -> Sem r1 (f a)) -> Sem r (f a)
forall x. param -> (resource -> Sem r1 x) -> Sem r x
withResource param
param \resource
resource' ->
resource -> InterpreterFor (Scoped param effect) r1
inScope resource
resource' (f (Sem rInitial a) -> Sem (Scoped param effect : r1) (f a)
forall x.
f (Sem rInitial x) -> Sem (Scoped param effect : r1) (f x)
wv (Sem rInitial a
main Sem rInitial a -> f () -> f (Sem rInitial a)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s)))
Weaving (Run effect (Sem rInitial) a
act) f ()
s forall x.
f (Sem rInitial x) -> Sem (Scoped param effect : r1) (f x)
wv f a -> x
ex forall x. f x -> Maybe x
ins ->
f a -> x
ex (f a -> x) -> Sem r1 (f a) -> Sem r1 x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f ()
-> (forall x. f (Sem rInitial x) -> Sem (effect : r1) (f x))
-> (forall x. f x -> Maybe x)
-> (forall x. f (Sem rInitial x) -> Sem r1 (f x))
-> Sem (Tactics f (Sem rInitial) (effect : r1) : r1) (f a)
-> Sem r1 (f a)
forall (f :: * -> *) (m :: * -> *) (r2 :: [Effect]) (r :: [Effect])
a.
Functor f =>
f ()
-> (forall x. f (m x) -> Sem r2 (f x))
-> (forall x. f x -> Maybe x)
-> (forall x. f (m x) -> Sem r (f x))
-> Sem (Tactics f m r2 : r) a
-> Sem r a
runTactics f ()
s (Sem r1 (f x) -> Sem (effect : r1) (f x)
forall (e :: Effect) (r :: [Effect]) a. Sem r a -> Sem (e : r) a
raise (Sem r1 (f x) -> Sem (effect : r1) (f x))
-> (f (Sem rInitial x) -> Sem r1 (f x))
-> f (Sem rInitial x)
-> Sem (effect : r1) (f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. resource -> InterpreterFor (Scoped param effect) r1
inScope resource
resource (Sem (Scoped param effect : r1) (f x) -> Sem r1 (f x))
-> (f (Sem rInitial x) -> Sem (Scoped param effect : r1) (f x))
-> f (Sem rInitial x)
-> Sem r1 (f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Sem rInitial x) -> Sem (Scoped param effect : r1) (f x)
forall x.
f (Sem rInitial x) -> Sem (Scoped param effect : r1) (f x)
wv) forall x. f x -> Maybe x
ins (resource -> InterpreterFor (Scoped param effect) r1
inScope resource
resource (Sem (Scoped param effect : r1) (f x) -> Sem r1 (f x))
-> (f (Sem rInitial x) -> Sem (Scoped param effect : r1) (f x))
-> f (Sem rInitial x)
-> Sem r1 (f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Sem rInitial x) -> Sem (Scoped param effect : r1) (f x)
forall x.
f (Sem rInitial x) -> Sem (Scoped param effect : r1) (f x)
wv)
(resource
-> effect (Sem rInitial) a -> Tactical effect (Sem rInitial) r1 a
forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Tactical effect (Sem r0) r1 x
scopedHandler resource
resource effect (Sem rInitial) a
act)
{-# inline interpretScopedWithH #-}
interpretScopedWith ::
∀ extra param resource effect r r1 .
r1 ~ (extra ++ r) =>
KnownList extra =>
(∀ x . param -> (resource -> Sem r1 x) -> Sem r x) ->
(∀ m x . resource -> effect m x -> Sem r1 x) ->
InterpreterFor (Scoped param effect) r
interpretScopedWith :: forall (extra :: [Effect]) param resource (effect :: Effect)
(r :: [Effect]) (r1 :: [Effect]).
(r1 ~ (extra ++ r), KnownList extra) =>
(forall x. param -> (resource -> Sem r1 x) -> Sem r x)
-> (forall (m :: * -> *) x. resource -> effect m x -> Sem r1 x)
-> InterpreterFor (Scoped param effect) r
interpretScopedWith forall x. param -> (resource -> Sem r1 x) -> Sem r x
withResource forall (m :: * -> *) x. resource -> effect m x -> Sem r1 x
scopedHandler =
forall (extra :: [Effect]) resource param (effect :: Effect)
(r :: [Effect]) (r1 :: [Effect]).
(r1 ~ (extra ++ r), KnownList extra) =>
(forall x. param -> (resource -> Sem r1 x) -> Sem r x)
-> (forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Tactical effect (Sem r0) r1 x)
-> InterpreterFor (Scoped param effect) r
interpretScopedWithH @extra forall x. param -> (resource -> Sem r1 x) -> Sem r x
withResource \ resource
r effect (Sem r0) x
e -> Sem r1 x -> Sem (WithTactics effect f (Sem r0) r1) (f x)
forall (m :: * -> *) (f :: * -> *) (r :: [Effect]) (e :: Effect) a.
Functor f =>
Sem r a -> Sem (WithTactics e f m r) (f a)
liftT (resource -> effect (Sem r0) x -> Sem r1 x
forall (m :: * -> *) x. resource -> effect m x -> Sem r1 x
scopedHandler resource
r effect (Sem r0) x
e)
{-# inline interpretScopedWith #-}
interpretScopedWith_ ::
∀ extra param effect r r1 .
r1 ~ (extra ++ r) =>
KnownList extra =>
(∀ x . param -> Sem r1 x -> Sem r x) ->
(∀ m x . effect m x -> Sem r1 x) ->
InterpreterFor (Scoped param effect) r
interpretScopedWith_ :: forall (extra :: [Effect]) param (effect :: Effect) (r :: [Effect])
(r1 :: [Effect]).
(r1 ~ (extra ++ r), KnownList extra) =>
(forall x. param -> Sem r1 x -> Sem r x)
-> (forall (m :: * -> *) x. effect m x -> Sem r1 x)
-> InterpreterFor (Scoped param effect) r
interpretScopedWith_ forall x. param -> Sem r1 x -> Sem r x
withResource forall (m :: * -> *) x. effect m x -> Sem r1 x
scopedHandler =
forall (extra :: [Effect]) resource param (effect :: Effect)
(r :: [Effect]) (r1 :: [Effect]).
(r1 ~ (extra ++ r), KnownList extra) =>
(forall x. param -> (resource -> Sem r1 x) -> Sem r x)
-> (forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Tactical effect (Sem r0) r1 x)
-> InterpreterFor (Scoped param effect) r
interpretScopedWithH @extra (\ param
p () -> Sem r1 x
f -> param -> Sem r1 x -> Sem r x
forall x. param -> Sem r1 x -> Sem r x
withResource param
p (() -> Sem r1 x
f ())) \ () effect (Sem r0) x
e -> Sem r1 x -> Sem (WithTactics effect f (Sem r0) r1) (f x)
forall (m :: * -> *) (f :: * -> *) (r :: [Effect]) (e :: Effect) a.
Functor f =>
Sem r a -> Sem (WithTactics e f m r) (f a)
liftT (effect (Sem r0) x -> Sem r1 x
forall (m :: * -> *) x. effect m x -> Sem r1 x
scopedHandler effect (Sem r0) x
e)
{-# inline interpretScopedWith_ #-}
runScoped ::
∀ resource param effect r .
(∀ x . param -> (resource -> Sem r x) -> Sem r x) ->
(resource -> InterpreterFor effect r) ->
InterpreterFor (Scoped param effect) r
runScoped :: forall resource param (effect :: Effect) (r :: [Effect]).
(forall x. param -> (resource -> Sem r x) -> Sem r x)
-> (resource -> InterpreterFor effect r)
-> InterpreterFor (Scoped param effect) r
runScoped forall x. param -> (resource -> Sem r x) -> Sem r x
withResource resource -> InterpreterFor effect r
scopedInterpreter =
resource -> InterpreterFor (Scoped param effect) r
go ([Char] -> resource
forall a. [Char] -> a
errorWithoutStackTrace [Char]
"top level run")
where
go :: resource -> InterpreterFor (Scoped param effect) r
go :: resource -> InterpreterFor (Scoped param effect) r
go resource
resource =
(forall x.
Weaving (Scoped param effect) (Sem (Scoped param effect : r)) x
-> Sem r x)
-> InterpreterFor (Scoped param effect) r
forall (e :: Effect) (r :: [Effect]).
(forall x. Weaving e (Sem (e : r)) x -> Sem r x)
-> InterpreterFor e r
interpretWeaving \ (Weaving Scoped param effect (Sem rInitial) a
effect f ()
s forall x. f (Sem rInitial x) -> Sem (Scoped param effect : r) (f x)
wv f a -> x
ex forall x. f x -> Maybe x
ins) -> case Scoped param effect (Sem rInitial) a
effect of
Run effect (Sem rInitial) a
act ->
resource -> InterpreterFor effect r
scopedInterpreter resource
resource
(Sem (effect : r) x -> Sem r x) -> Sem (effect : r) x -> Sem r x
forall a b. (a -> b) -> a -> b
$ Union (effect : r) (Sem (effect : r)) x -> Sem (effect : r) x
forall (r :: [Effect]) a. Union r (Sem r) a -> Sem r a
liftSem (Union (effect : r) (Sem (effect : r)) x -> Sem (effect : r) x)
-> Union (effect : r) (Sem (effect : r)) x -> Sem (effect : r) x
forall a b. (a -> b) -> a -> b
$ Weaving effect (Sem (effect : r)) x
-> Union (effect : r) (Sem (effect : r)) x
forall (e :: Effect) (r :: [Effect]) (m :: * -> *) a.
Member e r =>
Weaving e m a -> Union r m a
injWeaving (Weaving effect (Sem (effect : r)) x
-> Union (effect : r) (Sem (effect : r)) x)
-> Weaving effect (Sem (effect : r)) x
-> Union (effect : r) (Sem (effect : r)) x
forall a b. (a -> b) -> a -> b
$ effect (Sem rInitial) a
-> f ()
-> (forall x. f (Sem rInitial x) -> Sem (effect : r) (f x))
-> (f a -> x)
-> (forall x. f x -> Maybe x)
-> Weaving effect (Sem (effect : r)) x
forall (f :: * -> *) (e :: Effect) (rInitial :: [Effect]) a
resultType (mAfter :: * -> *).
Functor f =>
e (Sem rInitial) a
-> f ()
-> (forall x. f (Sem rInitial x) -> mAfter (f x))
-> (f a -> resultType)
-> (forall x. f x -> Maybe x)
-> Weaving e mAfter resultType
Weaving effect (Sem rInitial) a
act f ()
s (Sem r (f x) -> Sem (effect : r) (f x)
forall (e :: Effect) (r :: [Effect]) a. Sem r a -> Sem (e : r) a
raise (Sem r (f x) -> Sem (effect : r) (f x))
-> (f (Sem rInitial x) -> Sem r (f x))
-> f (Sem rInitial x)
-> Sem (effect : r) (f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. resource -> InterpreterFor (Scoped param effect) r
go resource
resource (Sem (Scoped param effect : r) (f x) -> Sem r (f x))
-> (f (Sem rInitial x) -> Sem (Scoped param effect : r) (f x))
-> f (Sem rInitial x)
-> Sem r (f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Sem rInitial x) -> Sem (Scoped param effect : r) (f x)
forall x. f (Sem rInitial x) -> Sem (Scoped param effect : r) (f x)
wv) f a -> x
ex forall x. f x -> Maybe x
ins
InScope param
param Sem rInitial a
main ->
param -> (resource -> Sem r x) -> Sem r x
forall x. param -> (resource -> Sem r x) -> Sem r x
withResource param
param \ resource
resource' -> f a -> x
ex (f a -> x) -> Sem r (f a) -> Sem r x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> resource -> InterpreterFor (Scoped param effect) r
go resource
resource' (f (Sem rInitial a) -> Sem (Scoped param effect : r) (f a)
forall x. f (Sem rInitial x) -> Sem (Scoped param effect : r) (f x)
wv (Sem rInitial a
main Sem rInitial a -> f () -> f (Sem rInitial a)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s))
{-# inline runScoped #-}
runScopedAs ::
∀ resource param effect r .
(param -> Sem r resource) ->
(resource -> InterpreterFor effect r) ->
InterpreterFor (Scoped param effect) r
runScopedAs :: forall resource param (effect :: Effect) (r :: [Effect]).
(param -> Sem r resource)
-> (resource -> InterpreterFor effect r)
-> InterpreterFor (Scoped param effect) r
runScopedAs param -> Sem r resource
resource = (forall x. param -> (resource -> Sem r x) -> Sem r x)
-> (resource -> InterpreterFor effect r)
-> InterpreterFor (Scoped param effect) r
forall resource param (effect :: Effect) (r :: [Effect]).
(forall x. param -> (resource -> Sem r x) -> Sem r x)
-> (resource -> InterpreterFor effect r)
-> InterpreterFor (Scoped param effect) r
runScoped \ param
p resource -> Sem r x
use -> resource -> Sem r x
use (resource -> Sem r x) -> Sem r resource -> Sem r x
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< param -> Sem r resource
resource param
p
{-# inline runScopedAs #-}
interpretScopedResumableH ::
∀ param resource effect err r .
(∀ x . param -> (resource -> Sem (Stop err : r) x) -> Sem (Stop err : r) x) ->
(∀ r0 x . resource -> effect (Sem r0) x -> Tactical effect (Sem r0) (Stop err : r) x) ->
InterpreterFor (Scoped param effect !! err) r
interpretScopedResumableH :: forall param resource (effect :: Effect) err (r :: [Effect]).
(forall x.
param
-> (resource -> Sem (Stop err : r) x) -> Sem (Stop err : r) x)
-> (forall (r0 :: [Effect]) x.
resource
-> effect (Sem r0) x -> Tactical effect (Sem r0) (Stop err : r) x)
-> InterpreterFor (Scoped param effect !! err) r
interpretScopedResumableH forall x.
param -> (resource -> Sem (Stop err : r) x) -> Sem (Stop err : r) x
withResource forall (r0 :: [Effect]) x.
resource
-> effect (Sem r0) x -> Tactical effect (Sem r0) (Stop err : r) x
scopedHandler =
resource -> InterpreterFor (Scoped param effect !! err) r
run ([Char] -> resource
forall a. [Char] -> a
errorWithoutStackTrace [Char]
"top level run")
where
run :: resource -> InterpreterFor (Scoped param effect !! err) r
run :: resource -> InterpreterFor (Scoped param effect !! err) r
run resource
resource =
(forall x.
Weaving
(Scoped param effect !! err)
(Sem ((Scoped param effect !! err) : r))
x
-> Sem r x)
-> InterpreterFor (Scoped param effect !! err) r
forall (e :: Effect) (r :: [Effect]).
(forall x. Weaving e (Sem (e : r)) x -> Sem r x)
-> InterpreterFor e r
interpretWeaving \ (Weaving (Resumable Weaving (Scoped param effect) (Sem r) a1
inner) f ()
s' forall x.
f (Sem rInitial x) -> Sem ((Scoped param effect !! err) : r) (f x)
dist' f a -> x
ex' forall x. f x -> Maybe x
ins') ->
case Weaving (Scoped param effect) (Sem r) a1
inner of
Weaving Scoped param effect (Sem rInitial) a
effect f ()
s forall x. f (Sem rInitial x) -> Sem r (f x)
dist f a -> a1
ex forall x. f x -> Maybe x
ins -> do
let
handleScoped :: Scoped param effect (Sem rInitial) a
-> Sem
(WithTactics effect (Compose f f) (Sem rInitial) (Stop err : r))
(Compose f f a)
handleScoped = \case
Run effect (Sem rInitial) a
act ->
resource
-> effect (Sem rInitial) a
-> Tactical effect (Sem rInitial) (Stop err : r) a
forall (r0 :: [Effect]) x.
resource
-> effect (Sem r0) x -> Tactical effect (Sem r0) (Stop err : r) x
scopedHandler resource
resource effect (Sem rInitial) a
act
InScope param
param Sem rInitial a
main ->
Sem (Stop err : r) (Compose f f a)
-> Sem
(WithTactics effect (Compose f f) (Sem rInitial) (Stop err : r))
(Compose f f a)
forall (e :: Effect) (r :: [Effect]) a. Sem r a -> Sem (e : r) a
raise (param
-> (resource -> Sem (Stop err : r) (Compose f f a))
-> Sem (Stop err : r) (Compose f f a)
forall x.
param -> (resource -> Sem (Stop err : r) x) -> Sem (Stop err : r) x
withResource param
param \ resource
resource' -> f (f a) -> Compose f f a
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (f (f a) -> Compose f f a)
-> Sem (Stop err : r) (f (f a))
-> Sem (Stop err : r) (Compose f f a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sem r (f (f a)) -> Sem (Stop err : r) (f (f a))
forall (e :: Effect) (r :: [Effect]) a. Sem r a -> Sem (e : r) a
raise (resource -> InterpreterFor (Scoped param effect !! err) r
run resource
resource' (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)
dist' (f (Sem rInitial a) -> Sem r (f a)
forall x. f (Sem rInitial x) -> Sem r (f x)
dist (Sem rInitial a
main Sem rInitial a -> f () -> f (Sem rInitial a)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s) Sem r (f a) -> f () -> f (Sem r (f a))
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s'))))
tac :: Sem (Stop err : r) (Compose f f a)
tac =
Compose f f ()
-> (forall x.
Compose f f (Sem rInitial x)
-> Sem (effect : Stop err : r) (Compose f f x))
-> (forall x. Compose f f x -> Maybe x)
-> (forall x.
Compose f f (Sem rInitial x) -> Sem (Stop err : r) (Compose f f x))
-> Sem
(WithTactics effect (Compose f f) (Sem rInitial) (Stop err : r))
(Compose f f a)
-> Sem (Stop err : r) (Compose f f a)
forall (f :: * -> *) (m :: * -> *) (r2 :: [Effect]) (r :: [Effect])
a.
Functor f =>
f ()
-> (forall x. f (m x) -> Sem r2 (f x))
-> (forall x. f x -> Maybe x)
-> (forall x. f (m x) -> Sem r (f x))
-> Sem (Tactics f m r2 : r) a
-> Sem r a
runTactics
(f (f ()) -> Compose f f ()
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (f ()
s f () -> f () -> f (f ())
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s'))
(Sem (Stop err : r) (Compose f f x)
-> Sem (effect : Stop err : r) (Compose f f x)
forall (e :: Effect) (r :: [Effect]) a. Sem r a -> Sem (e : r) a
raise (Sem (Stop err : r) (Compose f f x)
-> Sem (effect : Stop err : r) (Compose f f x))
-> (Compose f f (Sem rInitial x)
-> Sem (Stop err : r) (Compose f f x))
-> Compose f f (Sem rInitial x)
-> Sem (effect : Stop err : r) (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sem r (Compose f f x) -> Sem (Stop err : r) (Compose f f x)
forall (e :: Effect) (r :: [Effect]) a. Sem r a -> Sem (e : r) a
raise (Sem r (Compose f f x) -> Sem (Stop err : r) (Compose f f x))
-> (Compose f f (Sem rInitial x) -> Sem r (Compose f f x))
-> Compose f f (Sem rInitial x)
-> Sem (Stop err : r) (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. resource -> InterpreterFor (Scoped param effect !! err) r
run resource
resource (Sem ((Scoped param effect !! err) : r) (Compose f f x)
-> Sem r (Compose f f x))
-> (Compose f f (Sem rInitial x)
-> Sem ((Scoped param effect !! err) : r) (Compose f f x))
-> Compose f f (Sem rInitial x)
-> Sem r (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f (f x) -> Compose f f x)
-> Sem ((Scoped param effect !! err) : r) (f (f x))
-> Sem ((Scoped param effect !! err) : r) (Compose f f x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (f x) -> Compose f f x
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (Sem ((Scoped param effect !! err) : r) (f (f x))
-> Sem ((Scoped param effect !! err) : r) (Compose f f x))
-> (Compose f f (Sem rInitial x)
-> Sem ((Scoped param effect !! err) : r) (f (f x)))
-> Compose f f (Sem rInitial x)
-> Sem ((Scoped param effect !! err) : r) (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Sem rInitial (f x))
-> Sem ((Scoped param effect !! err) : r) (f (f x))
forall x.
f (Sem rInitial x) -> Sem ((Scoped param effect !! err) : r) (f x)
dist' (f (Sem rInitial (f x))
-> Sem ((Scoped param effect !! err) : r) (f (f x)))
-> (Compose f f (Sem rInitial x) -> f (Sem rInitial (f x)))
-> Compose f f (Sem rInitial x)
-> Sem ((Scoped param effect !! err) : r) (f (f x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f (Sem rInitial x) -> Sem r (f x))
-> f (f (Sem rInitial x)) -> f (Sem r (f x))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (Sem rInitial x) -> Sem r (f x)
forall x. f (Sem rInitial x) -> Sem r (f x)
dist (f (f (Sem rInitial x)) -> f (Sem r (f x)))
-> (Compose f f (Sem rInitial x) -> f (f (Sem rInitial x)))
-> Compose f f (Sem rInitial x)
-> f (Sem r (f x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose f f (Sem rInitial x) -> f (f (Sem rInitial x))
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose)
(f x -> Maybe x
forall x. f x -> Maybe x
ins (f x -> Maybe x)
-> (Compose f f x -> Maybe (f x)) -> Compose f f x -> Maybe x
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< f (f x) -> Maybe (f x)
forall x. f x -> Maybe x
ins' (f (f x) -> Maybe (f x))
-> (Compose f f x -> f (f x)) -> Compose f f x -> Maybe (f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose f f x -> f (f x)
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose)
(Sem r (Compose f f x) -> Sem (Stop err : r) (Compose f f x)
forall (e :: Effect) (r :: [Effect]) a. Sem r a -> Sem (e : r) a
raise (Sem r (Compose f f x) -> Sem (Stop err : r) (Compose f f x))
-> (Compose f f (Sem rInitial x) -> Sem r (Compose f f x))
-> Compose f f (Sem rInitial x)
-> Sem (Stop err : r) (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. resource -> InterpreterFor (Scoped param effect !! err) r
run resource
resource (Sem ((Scoped param effect !! err) : r) (Compose f f x)
-> Sem r (Compose f f x))
-> (Compose f f (Sem rInitial x)
-> Sem ((Scoped param effect !! err) : r) (Compose f f x))
-> Compose f f (Sem rInitial x)
-> Sem r (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f (f x) -> Compose f f x)
-> Sem ((Scoped param effect !! err) : r) (f (f x))
-> Sem ((Scoped param effect !! err) : r) (Compose f f x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (f x) -> Compose f f x
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (Sem ((Scoped param effect !! err) : r) (f (f x))
-> Sem ((Scoped param effect !! err) : r) (Compose f f x))
-> (Compose f f (Sem rInitial x)
-> Sem ((Scoped param effect !! err) : r) (f (f x)))
-> Compose f f (Sem rInitial x)
-> Sem ((Scoped param effect !! err) : r) (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Sem rInitial (f x))
-> Sem ((Scoped param effect !! err) : r) (f (f x))
forall x.
f (Sem rInitial x) -> Sem ((Scoped param effect !! err) : r) (f x)
dist' (f (Sem rInitial (f x))
-> Sem ((Scoped param effect !! err) : r) (f (f x)))
-> (Compose f f (Sem rInitial x) -> f (Sem rInitial (f x)))
-> Compose f f (Sem rInitial x)
-> Sem ((Scoped param effect !! err) : r) (f (f x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f (Sem rInitial x) -> Sem r (f x))
-> f (f (Sem rInitial x)) -> f (Sem r (f x))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (Sem rInitial x) -> Sem r (f x)
forall x. f (Sem rInitial x) -> Sem r (f x)
dist (f (f (Sem rInitial x)) -> f (Sem r (f x)))
-> (Compose f f (Sem rInitial x) -> f (f (Sem rInitial x)))
-> Compose f f (Sem rInitial x)
-> f (Sem r (f x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose f f (Sem rInitial x) -> f (f (Sem rInitial x))
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose)
(Scoped param effect (Sem rInitial) a
-> Sem
(WithTactics effect (Compose f f) (Sem rInitial) (Stop err : r))
(Compose f f a)
handleScoped Scoped param effect (Sem rInitial) a
effect)
exFinal :: Either err (Compose f f a) -> x
exFinal = f a -> x
ex' (f a -> x)
-> (Either err (Compose f f a) -> f a)
-> Either err (Compose f f a)
-> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
Right (Compose f (f a)
a) -> a1 -> Either err a1
forall a b. b -> Either a b
Right (a1 -> Either err a1) -> (f a -> a1) -> f a -> Either err a1
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> a1
ex (f a -> Either err a1) -> f (f a) -> f (Either err a1)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (f a)
a
Left err
err -> err -> Either err a1
forall a b. a -> Either a b
Left err
err Either err a1 -> f () -> f (Either err a1)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s'
Either err (Compose f f a) -> x
exFinal (Either err (Compose f f a) -> x)
-> Sem r (Either err (Compose f f a)) -> Sem r x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sem (Stop err : r) (Compose f f a)
-> Sem r (Either err (Compose f f a))
forall e (r :: [Effect]) a.
Sem (Stop e : r) a -> Sem r (Either e a)
runStop Sem (Stop err : r) (Compose f f a)
tac
interpretScopedResumable ::
∀ param resource effect err r .
(∀ x . param -> (resource -> Sem (Stop err : r) x) -> Sem (Stop err : r) x) ->
(∀ r0 x . resource -> effect (Sem r0) x -> Sem (Stop err : r) x) ->
InterpreterFor (Scoped param effect !! err) r
interpretScopedResumable :: forall param resource (effect :: Effect) err (r :: [Effect]).
(forall x.
param
-> (resource -> Sem (Stop err : r) x) -> Sem (Stop err : r) x)
-> (forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Sem (Stop err : r) x)
-> InterpreterFor (Scoped param effect !! err) r
interpretScopedResumable forall x.
param -> (resource -> Sem (Stop err : r) x) -> Sem (Stop err : r) x
withResource forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Sem (Stop err : r) x
scopedHandler =
(forall x.
param
-> (resource -> Sem (Stop err : r) x) -> Sem (Stop err : r) x)
-> (forall (r0 :: [Effect]) x.
resource
-> effect (Sem r0) x -> Tactical effect (Sem r0) (Stop err : r) x)
-> InterpreterFor (Scoped param effect !! err) r
forall param resource (effect :: Effect) err (r :: [Effect]).
(forall x.
param
-> (resource -> Sem (Stop err : r) x) -> Sem (Stop err : r) x)
-> (forall (r0 :: [Effect]) x.
resource
-> effect (Sem r0) x -> Tactical effect (Sem r0) (Stop err : r) x)
-> InterpreterFor (Scoped param effect !! err) r
interpretScopedResumableH forall x.
param -> (resource -> Sem (Stop err : r) x) -> Sem (Stop err : r) x
withResource \ resource
r effect (Sem r0) x
e -> Sem (Stop err : r) x
-> Sem (WithTactics effect f (Sem r0) (Stop err : r)) (f x)
forall (m :: * -> *) (f :: * -> *) (r :: [Effect]) (e :: Effect) a.
Functor f =>
Sem r a -> Sem (WithTactics e f m r) (f a)
liftT (resource -> effect (Sem r0) x -> Sem (Stop err : r) x
forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Sem (Stop err : r) x
scopedHandler resource
r effect (Sem r0) x
e)
interpretScopedResumable_ ::
∀ param resource effect err r .
(param -> Sem (Stop err : r) resource) ->
(∀ r0 x . resource -> effect (Sem r0) x -> Sem (Stop err : r) x) ->
InterpreterFor (Scoped param effect !! err) r
interpretScopedResumable_ :: forall param resource (effect :: Effect) err (r :: [Effect]).
(param -> Sem (Stop err : r) resource)
-> (forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Sem (Stop err : r) x)
-> InterpreterFor (Scoped param effect !! err) r
interpretScopedResumable_ param -> Sem (Stop err : r) resource
resource =
(forall x.
param
-> (resource -> Sem (Stop err : r) x) -> Sem (Stop err : r) x)
-> (forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Sem (Stop err : r) x)
-> InterpreterFor (Scoped param effect !! err) r
forall param resource (effect :: Effect) err (r :: [Effect]).
(forall x.
param
-> (resource -> Sem (Stop err : r) x) -> Sem (Stop err : r) x)
-> (forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Sem (Stop err : r) x)
-> InterpreterFor (Scoped param effect !! err) r
interpretScopedResumable \ param
p resource -> Sem (Stop err : r) x
use -> resource -> Sem (Stop err : r) x
use (resource -> Sem (Stop err : r) x)
-> Sem (Stop err : r) resource -> Sem (Stop err : r) x
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< param -> Sem (Stop err : r) resource
resource param
p
interpretScopedResumableWithH ::
∀ extra param resource effect err r r1 .
r1 ~ (extra ++ (Stop err : r)) =>
r1 ~ ((extra ++ '[Stop err]) ++ r) =>
KnownList extra =>
KnownList (extra ++ '[Stop err]) =>
(∀ x . param -> (resource -> Sem r1 x) -> Sem (Stop err : r) x) ->
(∀ r0 x . resource -> effect (Sem r0) x -> Tactical effect (Sem r0) r1 x) ->
InterpreterFor (Scoped param effect !! err) r
interpretScopedResumableWithH :: forall (extra :: [Effect]) param resource (effect :: Effect) err
(r :: [Effect]) (r1 :: [Effect]).
(r1 ~ (extra ++ (Stop err : r)),
r1 ~ ((extra ++ '[Stop err]) ++ r), KnownList extra,
KnownList (extra ++ '[Stop err])) =>
(forall x. param -> (resource -> Sem r1 x) -> Sem (Stop err : r) x)
-> (forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Tactical effect (Sem r0) r1 x)
-> InterpreterFor (Scoped param effect !! err) r
interpretScopedResumableWithH forall x. param -> (resource -> Sem r1 x) -> Sem (Stop err : r) x
withResource forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Tactical effect (Sem r0) r1 x
scopedHandler =
resource -> InterpreterFor (Scoped param effect !! err) r
run ([Char] -> resource
forall a. [Char] -> a
errorWithoutStackTrace [Char]
"top level run")
where
run :: resource -> InterpreterFor (Scoped param effect !! err) r
run :: resource -> InterpreterFor (Scoped param effect !! err) r
run resource
resource =
(forall x.
Weaving
(Scoped param effect !! err)
(Sem ((Scoped param effect !! err) : r))
x
-> Sem r x)
-> InterpreterFor (Scoped param effect !! err) r
forall (e :: Effect) (r :: [Effect]).
(forall x. Weaving e (Sem (e : r)) x -> Sem r x)
-> InterpreterFor e r
interpretWeaving \ (Weaving (Resumable Weaving (Scoped param effect) (Sem r) a1
inner) f ()
s' forall x.
f (Sem rInitial x) -> Sem ((Scoped param effect !! err) : r) (f x)
dist' f a -> x
ex' forall x. f x -> Maybe x
ins') ->
case Weaving (Scoped param effect) (Sem r) a1
inner of
Weaving Scoped param effect (Sem rInitial) a
effect f ()
s forall x. f (Sem rInitial x) -> Sem r (f x)
dist f a -> a1
ex forall x. f x -> Maybe x
ins -> do
let
handleScoped :: Scoped param effect (Sem rInitial) a
-> Sem
(Tactics (Compose f f) (Sem rInitial) (Any : Any : r)
: Stop err : r)
(Compose f f a)
handleScoped = \case
Run effect (Sem rInitial) a
_ ->
[Char]
-> Sem
(Tactics (Compose f f) (Sem rInitial) (Any : Any : r)
: Stop err : r)
(Compose f f a)
forall a. HasCallStack => [Char] -> a
error [Char]
"top level Run"
InScope param
param Sem rInitial a
main ->
Sem (Stop err : r) (Compose f f a)
-> Sem
(Tactics (Compose f f) (Sem rInitial) (Any : Any : r)
: Stop err : r)
(Compose f f a)
forall (e :: Effect) (r :: [Effect]) a. Sem r a -> Sem (e : r) a
raise (Sem (Stop err : r) (Compose f f a)
-> Sem
(Tactics (Compose f f) (Sem rInitial) (Any : Any : r)
: Stop err : r)
(Compose f f a))
-> Sem (Stop err : r) (Compose f f a)
-> Sem
(Tactics (Compose f f) (Sem rInitial) (Any : Any : r)
: Stop err : r)
(Compose f f a)
forall a b. (a -> b) -> a -> b
$ param
-> (resource -> Sem r1 (Compose f f a))
-> Sem (Stop err : r) (Compose f f a)
forall x. param -> (resource -> Sem r1 x) -> Sem (Stop err : r) x
withResource param
param \ resource
resource' ->
f (f a) -> Compose f f a
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (f (f a) -> Compose f f a)
-> Sem r1 (f (f a)) -> Sem r1 (Compose f f a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> resource -> InterpreterFor (Scoped param effect !! err) r1
inScope resource
resource' ((forall (e :: Effect).
ElemOf e ((Scoped param effect !! err) : r)
-> ElemOf e ((Scoped param effect !! err) : r1))
-> Sem ((Scoped param effect !! err) : r) (f (f a))
-> Sem ((Scoped param effect !! err) : r1) (f (f a))
forall (r :: [Effect]) (r' :: [Effect]) a.
(forall (e :: Effect). ElemOf e r -> ElemOf e r')
-> Sem r a -> Sem r' a
restack (SList '[Scoped param effect !! err]
-> SList (extra ++ '[Stop err])
-> ElemOf e (Append '[Scoped param effect !! err] r)
-> ElemOf
e
(Append
'[Scoped param effect !! err] ((extra ++ '[Stop err]) ++ r))
forall {a} (right :: [a]) (e :: a) (left :: [a]) (mid :: [a]).
SList left
-> SList mid
-> ElemOf e (Append left right)
-> ElemOf e (Append left (Append mid right))
injectMembership (forall (l :: [Effect]). KnownList l => SList l
forall {a} (l :: [a]). KnownList l => SList l
singList @'[Scoped param effect !! err]) (forall (l :: [Effect]). KnownList l => SList l
forall {a} (l :: [a]). KnownList l => SList l
singList @(extra ++ '[Stop err]))) (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)
dist' (f (Sem rInitial a) -> Sem r (f a)
forall x. f (Sem rInitial x) -> Sem r (f x)
dist (Sem rInitial a
main Sem rInitial a -> f () -> f (Sem rInitial a)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s) Sem r (f a) -> f () -> f (Sem r (f a))
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s')))
tac :: Sem (Stop err : r) (Compose f f a)
tac =
Compose f f ()
-> (forall x.
Compose f f (Sem rInitial x)
-> Sem (Any : Any : r) (Compose f f x))
-> (forall x. Compose f f x -> Maybe x)
-> (forall x.
Compose f f (Sem rInitial x) -> Sem (Stop err : r) (Compose f f x))
-> Sem
(Tactics (Compose f f) (Sem rInitial) (Any : Any : r)
: Stop err : r)
(Compose f f a)
-> Sem (Stop err : r) (Compose f f a)
forall (f :: * -> *) (m :: * -> *) (r2 :: [Effect]) (r :: [Effect])
a.
Functor f =>
f ()
-> (forall x. f (m x) -> Sem r2 (f x))
-> (forall x. f x -> Maybe x)
-> (forall x. f (m x) -> Sem r (f x))
-> Sem (Tactics f m r2 : r) a
-> Sem r a
runTactics
(f (f ()) -> Compose f f ()
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (f ()
s f () -> f () -> f (f ())
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s'))
(Sem (Any : r) (Compose f f x)
-> Sem (Any : Any : r) (Compose f f x)
forall (e :: Effect) (r :: [Effect]) a. Sem r a -> Sem (e : r) a
raise (Sem (Any : r) (Compose f f x)
-> Sem (Any : Any : r) (Compose f f x))
-> (Compose f f (Sem rInitial x) -> Sem (Any : r) (Compose f f x))
-> Compose f f (Sem rInitial x)
-> Sem (Any : Any : r) (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sem r (Compose f f x) -> Sem (Any : r) (Compose f f x)
forall (e :: Effect) (r :: [Effect]) a. Sem r a -> Sem (e : r) a
raise (Sem r (Compose f f x) -> Sem (Any : r) (Compose f f x))
-> (Compose f f (Sem rInitial x) -> Sem r (Compose f f x))
-> Compose f f (Sem rInitial x)
-> Sem (Any : r) (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. resource -> InterpreterFor (Scoped param effect !! err) r
run resource
resource (Sem ((Scoped param effect !! err) : r) (Compose f f x)
-> Sem r (Compose f f x))
-> (Compose f f (Sem rInitial x)
-> Sem ((Scoped param effect !! err) : r) (Compose f f x))
-> Compose f f (Sem rInitial x)
-> Sem r (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f (f x) -> Compose f f x)
-> Sem ((Scoped param effect !! err) : r) (f (f x))
-> Sem ((Scoped param effect !! err) : r) (Compose f f x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (f x) -> Compose f f x
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (Sem ((Scoped param effect !! err) : r) (f (f x))
-> Sem ((Scoped param effect !! err) : r) (Compose f f x))
-> (Compose f f (Sem rInitial x)
-> Sem ((Scoped param effect !! err) : r) (f (f x)))
-> Compose f f (Sem rInitial x)
-> Sem ((Scoped param effect !! err) : r) (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Sem rInitial (f x))
-> Sem ((Scoped param effect !! err) : r) (f (f x))
forall x.
f (Sem rInitial x) -> Sem ((Scoped param effect !! err) : r) (f x)
dist' (f (Sem rInitial (f x))
-> Sem ((Scoped param effect !! err) : r) (f (f x)))
-> (Compose f f (Sem rInitial x) -> f (Sem rInitial (f x)))
-> Compose f f (Sem rInitial x)
-> Sem ((Scoped param effect !! err) : r) (f (f x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f (Sem rInitial x) -> Sem r (f x))
-> f (f (Sem rInitial x)) -> f (Sem r (f x))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (Sem rInitial x) -> Sem r (f x)
forall x. f (Sem rInitial x) -> Sem r (f x)
dist (f (f (Sem rInitial x)) -> f (Sem r (f x)))
-> (Compose f f (Sem rInitial x) -> f (f (Sem rInitial x)))
-> Compose f f (Sem rInitial x)
-> f (Sem r (f x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose f f (Sem rInitial x) -> f (f (Sem rInitial x))
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose)
(f x -> Maybe x
forall x. f x -> Maybe x
ins (f x -> Maybe x)
-> (Compose f f x -> Maybe (f x)) -> Compose f f x -> Maybe x
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< f (f x) -> Maybe (f x)
forall x. f x -> Maybe x
ins' (f (f x) -> Maybe (f x))
-> (Compose f f x -> f (f x)) -> Compose f f x -> Maybe (f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose f f x -> f (f x)
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose)
(Sem r (Compose f f x) -> Sem (Stop err : r) (Compose f f x)
forall (e :: Effect) (r :: [Effect]) a. Sem r a -> Sem (e : r) a
raise (Sem r (Compose f f x) -> Sem (Stop err : r) (Compose f f x))
-> (Compose f f (Sem rInitial x) -> Sem r (Compose f f x))
-> Compose f f (Sem rInitial x)
-> Sem (Stop err : r) (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. resource -> InterpreterFor (Scoped param effect !! err) r
run resource
resource (Sem ((Scoped param effect !! err) : r) (Compose f f x)
-> Sem r (Compose f f x))
-> (Compose f f (Sem rInitial x)
-> Sem ((Scoped param effect !! err) : r) (Compose f f x))
-> Compose f f (Sem rInitial x)
-> Sem r (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f (f x) -> Compose f f x)
-> Sem ((Scoped param effect !! err) : r) (f (f x))
-> Sem ((Scoped param effect !! err) : r) (Compose f f x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (f x) -> Compose f f x
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (Sem ((Scoped param effect !! err) : r) (f (f x))
-> Sem ((Scoped param effect !! err) : r) (Compose f f x))
-> (Compose f f (Sem rInitial x)
-> Sem ((Scoped param effect !! err) : r) (f (f x)))
-> Compose f f (Sem rInitial x)
-> Sem ((Scoped param effect !! err) : r) (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Sem rInitial (f x))
-> Sem ((Scoped param effect !! err) : r) (f (f x))
forall x.
f (Sem rInitial x) -> Sem ((Scoped param effect !! err) : r) (f x)
dist' (f (Sem rInitial (f x))
-> Sem ((Scoped param effect !! err) : r) (f (f x)))
-> (Compose f f (Sem rInitial x) -> f (Sem rInitial (f x)))
-> Compose f f (Sem rInitial x)
-> Sem ((Scoped param effect !! err) : r) (f (f x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f (Sem rInitial x) -> Sem r (f x))
-> f (f (Sem rInitial x)) -> f (Sem r (f x))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (Sem rInitial x) -> Sem r (f x)
forall x. f (Sem rInitial x) -> Sem r (f x)
dist (f (f (Sem rInitial x)) -> f (Sem r (f x)))
-> (Compose f f (Sem rInitial x) -> f (f (Sem rInitial x)))
-> Compose f f (Sem rInitial x)
-> f (Sem r (f x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose f f (Sem rInitial x) -> f (f (Sem rInitial x))
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose)
(Scoped param effect (Sem rInitial) a
-> Sem
(Tactics (Compose f f) (Sem rInitial) (Any : Any : r)
: Stop err : r)
(Compose f f a)
handleScoped Scoped param effect (Sem rInitial) a
effect)
exFinal :: Either err (Compose f f a) -> x
exFinal = f a -> x
ex' (f a -> x)
-> (Either err (Compose f f a) -> f a)
-> Either err (Compose f f a)
-> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
Right (Compose f (f a)
a) -> a1 -> Either err a1
forall a b. b -> Either a b
Right (a1 -> Either err a1) -> (f a -> a1) -> f a -> Either err a1
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> a1
ex (f a -> Either err a1) -> f (f a) -> f (Either err a1)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (f a)
a
Left err
err -> err -> Either err a1
forall a b. a -> Either a b
Left err
err Either err a1 -> f () -> f (Either err a1)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s'
Either err (Compose f f a) -> x
exFinal (Either err (Compose f f a) -> x)
-> Sem r (Either err (Compose f f a)) -> Sem r x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sem (Stop err : r) (Compose f f a)
-> Sem r (Either err (Compose f f a))
forall e (r :: [Effect]) a.
Sem (Stop e : r) a -> Sem r (Either e a)
runStop Sem (Stop err : r) (Compose f f a)
tac
inScope :: resource -> InterpreterFor (Scoped param effect !! err) r1
inScope :: resource -> InterpreterFor (Scoped param effect !! err) r1
inScope resource
resource =
(forall x.
Weaving
(Scoped param effect !! err)
(Sem ((Scoped param effect !! err) : r1))
x
-> Sem r1 x)
-> InterpreterFor (Scoped param effect !! err) r1
forall (e :: Effect) (r :: [Effect]).
(forall x. Weaving e (Sem (e : r)) x -> Sem r x)
-> InterpreterFor e r
interpretWeaving \ (Weaving (Resumable Weaving (Scoped param effect) (Sem r) a1
inner) f ()
s' forall x.
f (Sem rInitial x) -> Sem ((Scoped param effect !! err) : r1) (f x)
dist' f a -> x
ex' forall x. f x -> Maybe x
ins') ->
case Weaving (Scoped param effect) (Sem r) a1
inner of
Weaving Scoped param effect (Sem rInitial) a
effect f ()
s forall x. f (Sem rInitial x) -> Sem r (f x)
dist f a -> a1
ex forall x. f x -> Maybe x
ins -> do
let
handleScoped :: Scoped param effect (Sem rInitial) a
-> Sem
(WithTactics effect (Compose f f) (Sem rInitial) r1)
(Compose f f a)
handleScoped = \case
Run effect (Sem rInitial) a
act ->
resource
-> effect (Sem rInitial) a -> Tactical effect (Sem rInitial) r1 a
forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Tactical effect (Sem r0) r1 x
scopedHandler resource
resource effect (Sem rInitial) a
act
InScope param
param Sem rInitial a
main ->
Sem r1 (Compose f f a)
-> Sem
(WithTactics effect (Compose f f) (Sem rInitial) r1)
(Compose f f a)
forall (e :: Effect) (r :: [Effect]) a. Sem r a -> Sem (e : r) a
raise (Sem r1 (Compose f f a)
-> Sem
(WithTactics effect (Compose f f) (Sem rInitial) r1)
(Compose f f a))
-> Sem r1 (Compose f f a)
-> Sem
(WithTactics effect (Compose f f) (Sem rInitial) r1)
(Compose f f a)
forall a b. (a -> b) -> a -> b
$ (forall (e :: Effect). ElemOf e (Stop err : r) -> ElemOf e r1)
-> Sem (Stop err : r) (Compose f f a) -> Sem r1 (Compose f f a)
forall (r :: [Effect]) (r' :: [Effect]) a.
(forall (e :: Effect). ElemOf e r -> ElemOf e r')
-> Sem r a -> Sem r' a
restack (SList extra
-> ElemOf e (Stop err : r) -> ElemOf e (extra ++ (Stop err : r))
forall {a} (l :: [a]) (r :: [a]) (e :: a).
SList l -> ElemOf e r -> ElemOf e (Append l r)
extendMembershipLeft (forall (l :: [Effect]). KnownList l => SList l
forall {a} (l :: [a]). KnownList l => SList l
singList @extra)) (Sem (Stop err : r) (Compose f f a) -> Sem r1 (Compose f f a))
-> Sem (Stop err : r) (Compose f f a) -> Sem r1 (Compose f f a)
forall a b. (a -> b) -> a -> b
$ param
-> (resource -> Sem r1 (Compose f f a))
-> Sem (Stop err : r) (Compose f f a)
forall x. param -> (resource -> Sem r1 x) -> Sem (Stop err : r) x
withResource param
param \ resource
resource' ->
f (f a) -> Compose f f a
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (f (f a) -> Compose f f a)
-> Sem r1 (f (f a)) -> Sem r1 (Compose f f a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> resource -> InterpreterFor (Scoped param effect !! err) r1
inScope resource
resource' (f (Sem rInitial (f a))
-> Sem ((Scoped param effect !! err) : r1) (f (f a))
forall x.
f (Sem rInitial x) -> Sem ((Scoped param effect !! err) : r1) (f x)
dist' (f (Sem rInitial a) -> Sem r (f a)
forall x. f (Sem rInitial x) -> Sem r (f x)
dist (Sem rInitial a
main Sem rInitial a -> f () -> f (Sem rInitial a)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s) Sem r (f a) -> f () -> f (Sem r (f a))
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s'))
tac :: Sem r1 (Compose f f a)
tac =
Compose f f ()
-> (forall x.
Compose f f (Sem rInitial x) -> Sem (effect : r1) (Compose f f x))
-> (forall x. Compose f f x -> Maybe x)
-> (forall x.
Compose f f (Sem rInitial x) -> Sem r1 (Compose f f x))
-> Sem
(WithTactics effect (Compose f f) (Sem rInitial) r1)
(Compose f f a)
-> Sem r1 (Compose f f a)
forall (f :: * -> *) (m :: * -> *) (r2 :: [Effect]) (r :: [Effect])
a.
Functor f =>
f ()
-> (forall x. f (m x) -> Sem r2 (f x))
-> (forall x. f x -> Maybe x)
-> (forall x. f (m x) -> Sem r (f x))
-> Sem (Tactics f m r2 : r) a
-> Sem r a
runTactics
(f (f ()) -> Compose f f ()
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (f ()
s f () -> f () -> f (f ())
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s'))
(Sem r1 (Compose f f x) -> Sem (effect : r1) (Compose f f x)
forall (e :: Effect) (r :: [Effect]) a. Sem r a -> Sem (e : r) a
raise (Sem r1 (Compose f f x) -> Sem (effect : r1) (Compose f f x))
-> (Compose f f (Sem rInitial x) -> Sem r1 (Compose f f x))
-> Compose f f (Sem rInitial x)
-> Sem (effect : r1) (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. resource -> InterpreterFor (Scoped param effect !! err) r1
inScope resource
resource (Sem ((Scoped param effect !! err) : r1) (Compose f f x)
-> Sem r1 (Compose f f x))
-> (Compose f f (Sem rInitial x)
-> Sem ((Scoped param effect !! err) : r1) (Compose f f x))
-> Compose f f (Sem rInitial x)
-> Sem r1 (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f (f x) -> Compose f f x)
-> Sem ((Scoped param effect !! err) : r1) (f (f x))
-> Sem ((Scoped param effect !! err) : r1) (Compose f f x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (f x) -> Compose f f x
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (Sem ((Scoped param effect !! err) : r1) (f (f x))
-> Sem ((Scoped param effect !! err) : r1) (Compose f f x))
-> (Compose f f (Sem rInitial x)
-> Sem ((Scoped param effect !! err) : r1) (f (f x)))
-> Compose f f (Sem rInitial x)
-> Sem ((Scoped param effect !! err) : r1) (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Sem rInitial (f x))
-> Sem ((Scoped param effect !! err) : r1) (f (f x))
forall x.
f (Sem rInitial x) -> Sem ((Scoped param effect !! err) : r1) (f x)
dist' (f (Sem rInitial (f x))
-> Sem ((Scoped param effect !! err) : r1) (f (f x)))
-> (Compose f f (Sem rInitial x) -> f (Sem rInitial (f x)))
-> Compose f f (Sem rInitial x)
-> Sem ((Scoped param effect !! err) : r1) (f (f x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f (Sem rInitial x) -> Sem r (f x))
-> f (f (Sem rInitial x)) -> f (Sem r (f x))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (Sem rInitial x) -> Sem r (f x)
forall x. f (Sem rInitial x) -> Sem r (f x)
dist (f (f (Sem rInitial x)) -> f (Sem r (f x)))
-> (Compose f f (Sem rInitial x) -> f (f (Sem rInitial x)))
-> Compose f f (Sem rInitial x)
-> f (Sem r (f x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose f f (Sem rInitial x) -> f (f (Sem rInitial x))
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose)
(f x -> Maybe x
forall x. f x -> Maybe x
ins (f x -> Maybe x)
-> (Compose f f x -> Maybe (f x)) -> Compose f f x -> Maybe x
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< f (f x) -> Maybe (f x)
forall x. f x -> Maybe x
ins' (f (f x) -> Maybe (f x))
-> (Compose f f x -> f (f x)) -> Compose f f x -> Maybe (f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose f f x -> f (f x)
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose)
(resource -> InterpreterFor (Scoped param effect !! err) r1
inScope resource
resource (Sem ((Scoped param effect !! err) : r1) (Compose f f x)
-> Sem r1 (Compose f f x))
-> (Compose f f (Sem rInitial x)
-> Sem ((Scoped param effect !! err) : r1) (Compose f f x))
-> Compose f f (Sem rInitial x)
-> Sem r1 (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f (f x) -> Compose f f x)
-> Sem ((Scoped param effect !! err) : r1) (f (f x))
-> Sem ((Scoped param effect !! err) : r1) (Compose f f x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (f x) -> Compose f f x
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (Sem ((Scoped param effect !! err) : r1) (f (f x))
-> Sem ((Scoped param effect !! err) : r1) (Compose f f x))
-> (Compose f f (Sem rInitial x)
-> Sem ((Scoped param effect !! err) : r1) (f (f x)))
-> Compose f f (Sem rInitial x)
-> Sem ((Scoped param effect !! err) : r1) (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Sem rInitial (f x))
-> Sem ((Scoped param effect !! err) : r1) (f (f x))
forall x.
f (Sem rInitial x) -> Sem ((Scoped param effect !! err) : r1) (f x)
dist' (f (Sem rInitial (f x))
-> Sem ((Scoped param effect !! err) : r1) (f (f x)))
-> (Compose f f (Sem rInitial x) -> f (Sem rInitial (f x)))
-> Compose f f (Sem rInitial x)
-> Sem ((Scoped param effect !! err) : r1) (f (f x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f (Sem rInitial x) -> Sem r (f x))
-> f (f (Sem rInitial x)) -> f (Sem r (f x))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (Sem rInitial x) -> Sem r (f x)
forall x. f (Sem rInitial x) -> Sem r (f x)
dist (f (f (Sem rInitial x)) -> f (Sem r (f x)))
-> (Compose f f (Sem rInitial x) -> f (f (Sem rInitial x)))
-> Compose f f (Sem rInitial x)
-> f (Sem r (f x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose f f (Sem rInitial x) -> f (f (Sem rInitial x))
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose)
(Scoped param effect (Sem rInitial) a
-> Sem
(WithTactics effect (Compose f f) (Sem rInitial) r1)
(Compose f f a)
handleScoped Scoped param effect (Sem rInitial) a
effect)
exFinal :: Either err (Compose f f a) -> x
exFinal = f a -> x
ex' (f a -> x)
-> (Either err (Compose f f a) -> f a)
-> Either err (Compose f f a)
-> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
Right (Compose f (f a)
a) -> a1 -> Either err a1
forall a b. b -> Either a b
Right (a1 -> Either err a1) -> (f a -> a1) -> f a -> Either err a1
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> a1
ex (f a -> Either err a1) -> f (f a) -> f (Either err a1)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (f a)
a
Left err
err -> err -> Either err a1
forall a b. a -> Either a b
Left err
err Either err a1 -> f () -> f (Either err a1)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s'
Either err (Compose f f a) -> x
exFinal (Either err (Compose f f a) -> x)
-> Sem r1 (Either err (Compose f f a)) -> Sem r1 x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sem (Stop err : r1) (Compose f f a)
-> Sem r1 (Either err (Compose f f a))
forall e (r :: [Effect]) a.
Sem (Stop e : r) a -> Sem r (Either e a)
runStop (Sem r1 (Compose f f a) -> Sem (Stop err : r1) (Compose f f a)
forall (e :: Effect) (r :: [Effect]) a. Sem r a -> Sem (e : r) a
raise Sem r1 (Compose f f a)
tac)
interpretScopedResumableWith ::
∀ extra param resource effect err r r1 .
r1 ~ (extra ++ (Stop err : r)) =>
r1 ~ ((extra ++ '[Stop err]) ++ r) =>
KnownList extra =>
KnownList (extra ++ '[Stop err]) =>
(∀ x . param -> (resource -> Sem r1 x) -> Sem (Stop err : r) x) ->
(∀ r0 x . resource -> effect (Sem r0) x -> Sem r1 x) ->
InterpreterFor (Scoped param effect !! err) r
interpretScopedResumableWith :: forall (extra :: [Effect]) param resource (effect :: Effect) err
(r :: [Effect]) (r1 :: [Effect]).
(r1 ~ (extra ++ (Stop err : r)),
r1 ~ ((extra ++ '[Stop err]) ++ r), KnownList extra,
KnownList (extra ++ '[Stop err])) =>
(forall x. param -> (resource -> Sem r1 x) -> Sem (Stop err : r) x)
-> (forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Sem r1 x)
-> InterpreterFor (Scoped param effect !! err) r
interpretScopedResumableWith forall x. param -> (resource -> Sem r1 x) -> Sem (Stop err : r) x
withResource forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Sem r1 x
scopedHandler =
forall (extra :: [Effect]) param resource (effect :: Effect) err
(r :: [Effect]) (r1 :: [Effect]).
(r1 ~ (extra ++ (Stop err : r)),
r1 ~ ((extra ++ '[Stop err]) ++ r), KnownList extra,
KnownList (extra ++ '[Stop err])) =>
(forall x. param -> (resource -> Sem r1 x) -> Sem (Stop err : r) x)
-> (forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Tactical effect (Sem r0) r1 x)
-> InterpreterFor (Scoped param effect !! err) r
interpretScopedResumableWithH @extra forall x. param -> (resource -> Sem r1 x) -> Sem (Stop err : r) x
withResource \ resource
r effect (Sem r0) x
e -> Sem r1 x -> Sem (WithTactics effect f (Sem r0) r1) (f x)
forall (m :: * -> *) (f :: * -> *) (r :: [Effect]) (e :: Effect) a.
Functor f =>
Sem r a -> Sem (WithTactics e f m r) (f a)
liftT (resource -> effect (Sem r0) x -> Sem r1 x
forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Sem r1 x
scopedHandler resource
r effect (Sem r0) x
e)
interpretScopedResumableWith_ ::
∀ extra param effect err r r1 .
r1 ~ (extra ++ (Stop err : r)) =>
r1 ~ ((extra ++ '[Stop err]) ++ r) =>
KnownList extra =>
KnownList (extra ++ '[Stop err]) =>
(∀ x . param -> Sem r1 x -> Sem (Stop err : r) x) ->
(∀ r0 x . effect (Sem r0) x -> Sem r1 x) ->
InterpreterFor (Scoped param effect !! err) r
interpretScopedResumableWith_ :: forall (extra :: [Effect]) param (effect :: Effect) err
(r :: [Effect]) (r1 :: [Effect]).
(r1 ~ (extra ++ (Stop err : r)),
r1 ~ ((extra ++ '[Stop err]) ++ r), KnownList extra,
KnownList (extra ++ '[Stop err])) =>
(forall x. param -> Sem r1 x -> Sem (Stop err : r) x)
-> (forall (r0 :: [Effect]) x. effect (Sem r0) x -> Sem r1 x)
-> InterpreterFor (Scoped param effect !! err) r
interpretScopedResumableWith_ forall x. param -> Sem r1 x -> Sem (Stop err : r) x
extra forall (r0 :: [Effect]) x. effect (Sem r0) x -> Sem r1 x
scopedHandler =
forall (extra :: [Effect]) param resource (effect :: Effect) err
(r :: [Effect]) (r1 :: [Effect]).
(r1 ~ (extra ++ (Stop err : r)),
r1 ~ ((extra ++ '[Stop err]) ++ r), KnownList extra,
KnownList (extra ++ '[Stop err])) =>
(forall x. param -> (resource -> Sem r1 x) -> Sem (Stop err : r) x)
-> (forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Sem r1 x)
-> InterpreterFor (Scoped param effect !! err) r
interpretScopedResumableWith @extra (\ param
p () -> Sem r1 x
f -> param -> Sem r1 x -> Sem (Stop err : r) x
forall x. param -> Sem r1 x -> Sem (Stop err : r) x
extra param
p (() -> Sem r1 x
f ())) ((effect (Sem r0) x -> Sem r1 x)
-> () -> effect (Sem r0) x -> Sem r1 x
forall a b. a -> b -> a
const effect (Sem r0) x -> Sem r1 x
forall (r0 :: [Effect]) x. effect (Sem r0) x -> Sem r1 x
scopedHandler)
interpretResumableScopedH ::
∀ param resource effect err r .
(∀ x . param -> (resource -> Sem r x) -> Sem r x) ->
(∀ r0 x . resource -> effect (Sem r0) x -> Tactical effect (Sem r0) (Stop err : r) x) ->
InterpreterFor (Scoped param (effect !! err)) r
interpretResumableScopedH :: forall param resource (effect :: Effect) err (r :: [Effect]).
(forall x. param -> (resource -> Sem r x) -> Sem r x)
-> (forall (r0 :: [Effect]) x.
resource
-> effect (Sem r0) x -> Tactical effect (Sem r0) (Stop err : r) x)
-> InterpreterFor (Scoped param (effect !! err)) r
interpretResumableScopedH forall x. param -> (resource -> Sem r x) -> Sem r x
withResource forall (r0 :: [Effect]) x.
resource
-> effect (Sem r0) x -> Tactical effect (Sem r0) (Stop err : r) x
scopedHandler =
resource -> InterpreterFor (Scoped param (effect !! err)) r
run ([Char] -> resource
forall a. [Char] -> a
errorWithoutStackTrace [Char]
"top level run")
where
run :: resource -> InterpreterFor (Scoped param (effect !! err)) r
run :: resource -> InterpreterFor (Scoped param (effect !! err)) r
run resource
resource =
(forall x.
Weaving
(Scoped param (effect !! err))
(Sem (Scoped param (effect !! err) : r))
x
-> Sem r x)
-> InterpreterFor (Scoped param (effect !! err)) r
forall (e :: Effect) (r :: [Effect]).
(forall x. Weaving e (Sem (e : r)) x -> Sem r x)
-> InterpreterFor e r
interpretWeaving \ (Weaving Scoped param (effect !! err) (Sem rInitial) a
inner f ()
s' forall x.
f (Sem rInitial x) -> Sem (Scoped param (effect !! err) : r) (f x)
dist' f a -> x
ex' forall x. f x -> Maybe x
ins') -> case Scoped param (effect !! err) (Sem rInitial) a
inner of
Run (Resumable (Weaving effect (Sem rInitial) a
effect f ()
s forall x. f (Sem rInitial x) -> Sem r (f x)
dist f a -> a1
ex forall x. f x -> Maybe x
ins)) ->
Either err (Compose f f a) -> x
exFinal (Either err (Compose f f a) -> x)
-> Sem r (Either err (Compose f f a)) -> Sem r x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sem (Stop err : r) (Compose f f a)
-> Sem r (Either err (Compose f f a))
forall e (r :: [Effect]) a.
Sem (Stop e : r) a -> Sem r (Either e a)
runStop (Sem
(Tactics (Compose f f) (Sem rInitial) (effect : Stop err : r)
: Stop err : r)
(Compose f f a)
-> Sem (Stop err : r) (Compose f f a)
tac (resource
-> effect (Sem rInitial) a
-> Tactical effect (Sem rInitial) (Stop err : r) a
forall (r0 :: [Effect]) x.
resource
-> effect (Sem r0) x -> Tactical effect (Sem r0) (Stop err : r) x
scopedHandler resource
resource effect (Sem rInitial) a
effect))
where
tac :: Sem
(Tactics (Compose f f) (Sem rInitial) (effect : Stop err : r)
: Stop err : r)
(Compose f f a)
-> Sem (Stop err : r) (Compose f f a)
tac =
Compose f f ()
-> (forall x.
Compose f f (Sem rInitial x)
-> Sem (effect : Stop err : r) (Compose f f x))
-> (forall x. Compose f f x -> Maybe x)
-> (forall x.
Compose f f (Sem rInitial x) -> Sem (Stop err : r) (Compose f f x))
-> Sem
(Tactics (Compose f f) (Sem rInitial) (effect : Stop err : r)
: Stop err : r)
(Compose f f a)
-> Sem (Stop err : r) (Compose f f a)
forall (f :: * -> *) (m :: * -> *) (r2 :: [Effect]) (r :: [Effect])
a.
Functor f =>
f ()
-> (forall x. f (m x) -> Sem r2 (f x))
-> (forall x. f x -> Maybe x)
-> (forall x. f (m x) -> Sem r (f x))
-> Sem (Tactics f m r2 : r) a
-> Sem r a
runTactics
(f (f ()) -> Compose f f ()
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (f ()
s f () -> f () -> f (f ())
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s'))
(Sem (Stop err : r) (Compose f f x)
-> Sem (effect : Stop err : r) (Compose f f x)
forall (e :: Effect) (r :: [Effect]) a. Sem r a -> Sem (e : r) a
raise (Sem (Stop err : r) (Compose f f x)
-> Sem (effect : Stop err : r) (Compose f f x))
-> (Compose f f (Sem rInitial x)
-> Sem (Stop err : r) (Compose f f x))
-> Compose f f (Sem rInitial x)
-> Sem (effect : Stop err : r) (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sem r (Compose f f x) -> Sem (Stop err : r) (Compose f f x)
forall (e :: Effect) (r :: [Effect]) a. Sem r a -> Sem (e : r) a
raise (Sem r (Compose f f x) -> Sem (Stop err : r) (Compose f f x))
-> (Compose f f (Sem rInitial x) -> Sem r (Compose f f x))
-> Compose f f (Sem rInitial x)
-> Sem (Stop err : r) (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. resource -> InterpreterFor (Scoped param (effect !! err)) r
run resource
resource (Sem (Scoped param (effect !! err) : r) (Compose f f x)
-> Sem r (Compose f f x))
-> (Compose f f (Sem rInitial x)
-> Sem (Scoped param (effect !! err) : r) (Compose f f x))
-> Compose f f (Sem rInitial x)
-> Sem r (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f (f x) -> Compose f f x)
-> Sem (Scoped param (effect !! err) : r) (f (f x))
-> Sem (Scoped param (effect !! err) : r) (Compose f f x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (f x) -> Compose f f x
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (Sem (Scoped param (effect !! err) : r) (f (f x))
-> Sem (Scoped param (effect !! err) : r) (Compose f f x))
-> (Compose f f (Sem rInitial x)
-> Sem (Scoped param (effect !! err) : r) (f (f x)))
-> Compose f f (Sem rInitial x)
-> Sem (Scoped param (effect !! err) : r) (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Sem rInitial (f x))
-> Sem (Scoped param (effect !! err) : r) (f (f x))
forall x.
f (Sem rInitial x) -> Sem (Scoped param (effect !! err) : r) (f x)
dist' (f (Sem rInitial (f x))
-> Sem (Scoped param (effect !! err) : r) (f (f x)))
-> (Compose f f (Sem rInitial x) -> f (Sem rInitial (f x)))
-> Compose f f (Sem rInitial x)
-> Sem (Scoped param (effect !! err) : r) (f (f x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f (Sem rInitial x) -> Sem r (f x))
-> f (f (Sem rInitial x)) -> f (Sem r (f x))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (Sem rInitial x) -> Sem r (f x)
forall x. f (Sem rInitial x) -> Sem r (f x)
dist (f (f (Sem rInitial x)) -> f (Sem r (f x)))
-> (Compose f f (Sem rInitial x) -> f (f (Sem rInitial x)))
-> Compose f f (Sem rInitial x)
-> f (Sem r (f x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose f f (Sem rInitial x) -> f (f (Sem rInitial x))
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose)
(f x -> Maybe x
forall x. f x -> Maybe x
ins (f x -> Maybe x)
-> (Compose f f x -> Maybe (f x)) -> Compose f f x -> Maybe x
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< f (f x) -> Maybe (f x)
forall x. f x -> Maybe x
ins' (f (f x) -> Maybe (f x))
-> (Compose f f x -> f (f x)) -> Compose f f x -> Maybe (f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose f f x -> f (f x)
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose)
(Sem r (Compose f f x) -> Sem (Stop err : r) (Compose f f x)
forall (e :: Effect) (r :: [Effect]) a. Sem r a -> Sem (e : r) a
raise (Sem r (Compose f f x) -> Sem (Stop err : r) (Compose f f x))
-> (Compose f f (Sem rInitial x) -> Sem r (Compose f f x))
-> Compose f f (Sem rInitial x)
-> Sem (Stop err : r) (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. resource -> InterpreterFor (Scoped param (effect !! err)) r
run resource
resource (Sem (Scoped param (effect !! err) : r) (Compose f f x)
-> Sem r (Compose f f x))
-> (Compose f f (Sem rInitial x)
-> Sem (Scoped param (effect !! err) : r) (Compose f f x))
-> Compose f f (Sem rInitial x)
-> Sem r (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f (f x) -> Compose f f x)
-> Sem (Scoped param (effect !! err) : r) (f (f x))
-> Sem (Scoped param (effect !! err) : r) (Compose f f x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (f x) -> Compose f f x
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (Sem (Scoped param (effect !! err) : r) (f (f x))
-> Sem (Scoped param (effect !! err) : r) (Compose f f x))
-> (Compose f f (Sem rInitial x)
-> Sem (Scoped param (effect !! err) : r) (f (f x)))
-> Compose f f (Sem rInitial x)
-> Sem (Scoped param (effect !! err) : r) (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Sem rInitial (f x))
-> Sem (Scoped param (effect !! err) : r) (f (f x))
forall x.
f (Sem rInitial x) -> Sem (Scoped param (effect !! err) : r) (f x)
dist' (f (Sem rInitial (f x))
-> Sem (Scoped param (effect !! err) : r) (f (f x)))
-> (Compose f f (Sem rInitial x) -> f (Sem rInitial (f x)))
-> Compose f f (Sem rInitial x)
-> Sem (Scoped param (effect !! err) : r) (f (f x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f (Sem rInitial x) -> Sem r (f x))
-> f (f (Sem rInitial x)) -> f (Sem r (f x))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (Sem rInitial x) -> Sem r (f x)
forall x. f (Sem rInitial x) -> Sem r (f x)
dist (f (f (Sem rInitial x)) -> f (Sem r (f x)))
-> (Compose f f (Sem rInitial x) -> f (f (Sem rInitial x)))
-> Compose f f (Sem rInitial x)
-> f (Sem r (f x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose f f (Sem rInitial x) -> f (f (Sem rInitial x))
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose)
exFinal :: Either err (Compose f f a) -> x
exFinal = f a -> x
ex' (f a -> x)
-> (Either err (Compose f f a) -> f a)
-> Either err (Compose f f a)
-> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
Right (Compose f (f a)
a) -> a1 -> Either err a1
forall a b. b -> Either a b
Right (a1 -> Either err a1) -> (f a -> a1) -> f a -> Either err a1
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> a1
ex (f a -> Either err a1) -> f (f a) -> f (Either err a1)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (f a)
a
Left err
err -> err -> Either err a1
forall a b. a -> Either a b
Left err
err Either err a1 -> f () -> f (Either err a1)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s'
InScope param
param Sem rInitial a
main ->
f a -> x
ex' (f a -> x) -> Sem r (f a) -> Sem r x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> param -> (resource -> Sem r (f a)) -> Sem r (f a)
forall x. param -> (resource -> Sem r x) -> Sem r x
withResource param
param \ resource
resource' -> resource -> InterpreterFor (Scoped param (effect !! err)) r
run resource
resource' (f (Sem rInitial a) -> Sem (Scoped param (effect !! err) : r) (f a)
forall x.
f (Sem rInitial x) -> Sem (Scoped param (effect !! err) : r) (f x)
dist' (Sem rInitial a
main Sem rInitial a -> f () -> f (Sem rInitial a)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s'))
interpretResumableScoped ::
∀ param resource effect err r .
(∀ x . param -> (resource -> Sem r x) -> Sem r x) ->
(∀ r0 x . resource -> effect (Sem r0) x -> Sem (Stop err : r) x) ->
InterpreterFor (Scoped param (effect !! err)) r
interpretResumableScoped :: forall param resource (effect :: Effect) err (r :: [Effect]).
(forall x. param -> (resource -> Sem r x) -> Sem r x)
-> (forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Sem (Stop err : r) x)
-> InterpreterFor (Scoped param (effect !! err)) r
interpretResumableScoped forall x. param -> (resource -> Sem r x) -> Sem r x
withResource forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Sem (Stop err : r) x
scopedHandler =
(forall x. param -> (resource -> Sem r x) -> Sem r x)
-> (forall (r0 :: [Effect]) x.
resource
-> effect (Sem r0) x -> Tactical effect (Sem r0) (Stop err : r) x)
-> InterpreterFor (Scoped param (effect !! err)) r
forall param resource (effect :: Effect) err (r :: [Effect]).
(forall x. param -> (resource -> Sem r x) -> Sem r x)
-> (forall (r0 :: [Effect]) x.
resource
-> effect (Sem r0) x -> Tactical effect (Sem r0) (Stop err : r) x)
-> InterpreterFor (Scoped param (effect !! err)) r
interpretResumableScopedH forall x. param -> (resource -> Sem r x) -> Sem r x
withResource \ resource
r effect (Sem r0) x
e -> Sem (Stop err : r) x
-> Sem (WithTactics effect f (Sem r0) (Stop err : r)) (f x)
forall (m :: * -> *) (f :: * -> *) (r :: [Effect]) (e :: Effect) a.
Functor f =>
Sem r a -> Sem (WithTactics e f m r) (f a)
liftT (resource -> effect (Sem r0) x -> Sem (Stop err : r) x
forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Sem (Stop err : r) x
scopedHandler resource
r effect (Sem r0) x
e)
interpretResumableScoped_ ::
∀ param resource effect err r .
(param -> Sem r resource) ->
(∀ r0 x . resource -> effect (Sem r0) x -> Sem (Stop err : r) x) ->
InterpreterFor (Scoped param (effect !! err)) r
interpretResumableScoped_ :: forall param resource (effect :: Effect) err (r :: [Effect]).
(param -> Sem r resource)
-> (forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Sem (Stop err : r) x)
-> InterpreterFor (Scoped param (effect !! err)) r
interpretResumableScoped_ param -> Sem r resource
resource =
(forall x. param -> (resource -> Sem r x) -> Sem r x)
-> (forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Sem (Stop err : r) x)
-> InterpreterFor (Scoped param (effect !! err)) r
forall param resource (effect :: Effect) err (r :: [Effect]).
(forall x. param -> (resource -> Sem r x) -> Sem r x)
-> (forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Sem (Stop err : r) x)
-> InterpreterFor (Scoped param (effect !! err)) r
interpretResumableScoped \ param
p resource -> Sem r x
use -> resource -> Sem r x
use (resource -> Sem r x) -> Sem r resource -> Sem r x
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< param -> Sem r resource
resource param
p
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 (Sem r0) (Stop err : r1) x) ->
InterpreterFor (Scoped param (effect !! err)) r
interpretResumableScopedWithH :: forall (extra :: [Effect]) param resource (effect :: Effect) err
(r :: [Effect]) (r1 :: [Effect]).
(r1 ~ (extra ++ r), KnownList extra) =>
(forall x. param -> (resource -> Sem r1 x) -> Sem r x)
-> (forall (r0 :: [Effect]) x.
resource
-> effect (Sem r0) x -> Tactical effect (Sem r0) (Stop err : r1) x)
-> InterpreterFor (Scoped param (effect !! err)) r
interpretResumableScopedWithH forall x. param -> (resource -> Sem r1 x) -> Sem r x
withResource forall (r0 :: [Effect]) x.
resource
-> effect (Sem r0) x -> Tactical effect (Sem r0) (Stop err : r1) x
scopedHandler =
(forall x.
Weaving
(Scoped param (effect !! err))
(Sem (Scoped param (effect !! err) : r))
x
-> Sem r x)
-> InterpreterFor (Scoped param (effect !! err)) r
forall (e :: Effect) (r :: [Effect]).
(forall x. Weaving e (Sem (e : r)) x -> Sem r x)
-> InterpreterFor e r
interpretWeaving \case
Weaving (InScope param
param Sem rInitial a
main) f ()
s forall x.
f (Sem rInitial x) -> Sem (Scoped param (effect !! err) : r) (f x)
dist f a -> x
ex forall x. f x -> Maybe x
_ ->
f a -> x
ex (f a -> x) -> Sem r (f a) -> Sem r x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> param -> (resource -> Sem r1 (f a)) -> Sem r (f a)
forall x. param -> (resource -> Sem r1 x) -> Sem r x
withResource param
param \ resource
resource' -> resource -> InterpreterFor (Scoped param (effect !! err)) r1
inScope resource
resource' ((forall (e :: Effect).
ElemOf e (Scoped param (effect !! err) : r)
-> ElemOf e (Scoped param (effect !! err) : r1))
-> Sem (Scoped param (effect !! err) : r) (f a)
-> Sem (Scoped param (effect !! err) : r1) (f a)
forall (r :: [Effect]) (r' :: [Effect]) a.
(forall (e :: Effect). ElemOf e r -> ElemOf e r')
-> Sem r a -> Sem r' a
restack (SList '[Scoped param (effect !! err)]
-> SList extra
-> ElemOf e (Append '[Scoped param (effect !! err)] r)
-> ElemOf e (Append '[Scoped param (effect !! err)] (extra ++ r))
forall {a} (right :: [a]) (e :: a) (left :: [a]) (mid :: [a]).
SList left
-> SList mid
-> ElemOf e (Append left right)
-> ElemOf e (Append left (Append mid right))
injectMembership (forall (l :: [Effect]). KnownList l => SList l
forall {a} (l :: [a]). KnownList l => SList l
singList @'[Scoped param (effect !! err)]) (forall (l :: [Effect]). KnownList l => SList l
forall {a} (l :: [a]). KnownList l => SList l
singList @extra)) (f (Sem rInitial a) -> Sem (Scoped param (effect !! err) : r) (f a)
forall x.
f (Sem rInitial x) -> Sem (Scoped param (effect !! err) : r) (f x)
dist (Sem rInitial a
main Sem rInitial a -> f () -> f (Sem rInitial a)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s)))
Weaving
(Scoped param (effect !! err))
(Sem (Scoped param (effect !! err) : r))
x
_ ->
[Char] -> Sem r x
forall a. [Char] -> a
errorWithoutStackTrace [Char]
"top level run"
where
inScope :: resource -> InterpreterFor (Scoped param (effect !! err)) r1
inScope :: resource -> InterpreterFor (Scoped param (effect !! err)) r1
inScope resource
resource =
(forall x.
Weaving
(Scoped param (effect !! err))
(Sem (Scoped param (effect !! err) : r1))
x
-> Sem r1 x)
-> InterpreterFor (Scoped param (effect !! err)) r1
forall (e :: Effect) (r :: [Effect]).
(forall x. Weaving e (Sem (e : r)) x -> Sem r x)
-> InterpreterFor e r
interpretWeaving \case
Weaving (Run (Resumable (Weaving effect (Sem rInitial) a
effect f ()
s forall x. f (Sem rInitial x) -> Sem r (f x)
dist f a -> a1
ex forall x. f x -> Maybe x
ins))) f ()
s' forall x.
f (Sem rInitial x) -> Sem (Scoped param (effect !! err) : r1) (f x)
dist' f a -> x
ex' forall x. f x -> Maybe x
ins' ->
Either err (Compose f f a) -> x
exFinal (Either err (Compose f f a) -> x)
-> Sem r1 (Either err (Compose f f a)) -> Sem r1 x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sem (Stop err : r1) (Compose f f a)
-> Sem r1 (Either err (Compose f f a))
forall e (r :: [Effect]) a.
Sem (Stop e : r) a -> Sem r (Either e a)
runStop (Sem
(Tactics (Compose f f) (Sem rInitial) (effect : Stop err : r1)
: Stop err : r1)
(Compose f f a)
-> Sem (Stop err : r1) (Compose f f a)
tac (resource
-> effect (Sem rInitial) a
-> Tactical effect (Sem rInitial) (Stop err : r1) a
forall (r0 :: [Effect]) x.
resource
-> effect (Sem r0) x -> Tactical effect (Sem r0) (Stop err : r1) x
scopedHandler resource
resource effect (Sem rInitial) a
effect))
where
tac :: Sem
(Tactics (Compose f f) (Sem rInitial) (effect : Stop err : r1)
: Stop err : r1)
(Compose f f a)
-> Sem (Stop err : r1) (Compose f f a)
tac =
Compose f f ()
-> (forall x.
Compose f f (Sem rInitial x)
-> Sem (effect : Stop err : r1) (Compose f f x))
-> (forall x. Compose f f x -> Maybe x)
-> (forall x.
Compose f f (Sem rInitial x)
-> Sem (Stop err : r1) (Compose f f x))
-> Sem
(Tactics (Compose f f) (Sem rInitial) (effect : Stop err : r1)
: Stop err : r1)
(Compose f f a)
-> Sem (Stop err : r1) (Compose f f a)
forall (f :: * -> *) (m :: * -> *) (r2 :: [Effect]) (r :: [Effect])
a.
Functor f =>
f ()
-> (forall x. f (m x) -> Sem r2 (f x))
-> (forall x. f x -> Maybe x)
-> (forall x. f (m x) -> Sem r (f x))
-> Sem (Tactics f m r2 : r) a
-> Sem r a
runTactics
(f (f ()) -> Compose f f ()
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (f ()
s f () -> f () -> f (f ())
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s'))
(Sem (Stop err : r1) (Compose f f x)
-> Sem (effect : Stop err : r1) (Compose f f x)
forall (e :: Effect) (r :: [Effect]) a. Sem r a -> Sem (e : r) a
raise (Sem (Stop err : r1) (Compose f f x)
-> Sem (effect : Stop err : r1) (Compose f f x))
-> (Compose f f (Sem rInitial x)
-> Sem (Stop err : r1) (Compose f f x))
-> Compose f f (Sem rInitial x)
-> Sem (effect : Stop err : r1) (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sem r1 (Compose f f x) -> Sem (Stop err : r1) (Compose f f x)
forall (e :: Effect) (r :: [Effect]) a. Sem r a -> Sem (e : r) a
raise (Sem r1 (Compose f f x) -> Sem (Stop err : r1) (Compose f f x))
-> (Compose f f (Sem rInitial x) -> Sem r1 (Compose f f x))
-> Compose f f (Sem rInitial x)
-> Sem (Stop err : r1) (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. resource -> InterpreterFor (Scoped param (effect !! err)) r1
inScope resource
resource (Sem (Scoped param (effect !! err) : r1) (Compose f f x)
-> Sem r1 (Compose f f x))
-> (Compose f f (Sem rInitial x)
-> Sem (Scoped param (effect !! err) : r1) (Compose f f x))
-> Compose f f (Sem rInitial x)
-> Sem r1 (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f (f x) -> Compose f f x)
-> Sem (Scoped param (effect !! err) : r1) (f (f x))
-> Sem (Scoped param (effect !! err) : r1) (Compose f f x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (f x) -> Compose f f x
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (Sem (Scoped param (effect !! err) : r1) (f (f x))
-> Sem (Scoped param (effect !! err) : r1) (Compose f f x))
-> (Compose f f (Sem rInitial x)
-> Sem (Scoped param (effect !! err) : r1) (f (f x)))
-> Compose f f (Sem rInitial x)
-> Sem (Scoped param (effect !! err) : r1) (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Sem rInitial (f x))
-> Sem (Scoped param (effect !! err) : r1) (f (f x))
forall x.
f (Sem rInitial x) -> Sem (Scoped param (effect !! err) : r1) (f x)
dist' (f (Sem rInitial (f x))
-> Sem (Scoped param (effect !! err) : r1) (f (f x)))
-> (Compose f f (Sem rInitial x) -> f (Sem rInitial (f x)))
-> Compose f f (Sem rInitial x)
-> Sem (Scoped param (effect !! err) : r1) (f (f x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f (Sem rInitial x) -> Sem r (f x))
-> f (f (Sem rInitial x)) -> f (Sem r (f x))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (Sem rInitial x) -> Sem r (f x)
forall x. f (Sem rInitial x) -> Sem r (f x)
dist (f (f (Sem rInitial x)) -> f (Sem r (f x)))
-> (Compose f f (Sem rInitial x) -> f (f (Sem rInitial x)))
-> Compose f f (Sem rInitial x)
-> f (Sem r (f x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose f f (Sem rInitial x) -> f (f (Sem rInitial x))
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose)
(f x -> Maybe x
forall x. f x -> Maybe x
ins (f x -> Maybe x)
-> (Compose f f x -> Maybe (f x)) -> Compose f f x -> Maybe x
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< f (f x) -> Maybe (f x)
forall x. f x -> Maybe x
ins' (f (f x) -> Maybe (f x))
-> (Compose f f x -> f (f x)) -> Compose f f x -> Maybe (f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose f f x -> f (f x)
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose)
(Sem r1 (Compose f f x) -> Sem (Stop err : r1) (Compose f f x)
forall (e :: Effect) (r :: [Effect]) a. Sem r a -> Sem (e : r) a
raise (Sem r1 (Compose f f x) -> Sem (Stop err : r1) (Compose f f x))
-> (Compose f f (Sem rInitial x) -> Sem r1 (Compose f f x))
-> Compose f f (Sem rInitial x)
-> Sem (Stop err : r1) (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. resource -> InterpreterFor (Scoped param (effect !! err)) r1
inScope resource
resource (Sem (Scoped param (effect !! err) : r1) (Compose f f x)
-> Sem r1 (Compose f f x))
-> (Compose f f (Sem rInitial x)
-> Sem (Scoped param (effect !! err) : r1) (Compose f f x))
-> Compose f f (Sem rInitial x)
-> Sem r1 (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f (f x) -> Compose f f x)
-> Sem (Scoped param (effect !! err) : r1) (f (f x))
-> Sem (Scoped param (effect !! err) : r1) (Compose f f x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (f x) -> Compose f f x
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (Sem (Scoped param (effect !! err) : r1) (f (f x))
-> Sem (Scoped param (effect !! err) : r1) (Compose f f x))
-> (Compose f f (Sem rInitial x)
-> Sem (Scoped param (effect !! err) : r1) (f (f x)))
-> Compose f f (Sem rInitial x)
-> Sem (Scoped param (effect !! err) : r1) (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Sem rInitial (f x))
-> Sem (Scoped param (effect !! err) : r1) (f (f x))
forall x.
f (Sem rInitial x) -> Sem (Scoped param (effect !! err) : r1) (f x)
dist' (f (Sem rInitial (f x))
-> Sem (Scoped param (effect !! err) : r1) (f (f x)))
-> (Compose f f (Sem rInitial x) -> f (Sem rInitial (f x)))
-> Compose f f (Sem rInitial x)
-> Sem (Scoped param (effect !! err) : r1) (f (f x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f (Sem rInitial x) -> Sem r (f x))
-> f (f (Sem rInitial x)) -> f (Sem r (f x))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (Sem rInitial x) -> Sem r (f x)
forall x. f (Sem rInitial x) -> Sem r (f x)
dist (f (f (Sem rInitial x)) -> f (Sem r (f x)))
-> (Compose f f (Sem rInitial x) -> f (f (Sem rInitial x)))
-> Compose f f (Sem rInitial x)
-> f (Sem r (f x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose f f (Sem rInitial x) -> f (f (Sem rInitial x))
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose)
exFinal :: Either err (Compose f f a) -> x
exFinal = f a -> x
ex' (f a -> x)
-> (Either err (Compose f f a) -> f a)
-> Either err (Compose f f a)
-> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
Right (Compose f (f a)
a) -> a1 -> Either err a1
forall a b. b -> Either a b
Right (a1 -> Either err a1) -> (f a -> a1) -> f a -> Either err a1
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> a1
ex (f a -> Either err a1) -> f (f a) -> f (Either err a1)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (f a)
a
Left err
err -> err -> Either err a1
forall a b. a -> Either a b
Left err
err Either err a1 -> f () -> f (Either err a1)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s'
Weaving (InScope param
param Sem rInitial a
main) f ()
s forall x.
f (Sem rInitial x) -> Sem (Scoped param (effect !! err) : r1) (f x)
wv f a -> x
ex forall x. f x -> Maybe x
_ ->
(forall (e :: Effect). ElemOf e r -> ElemOf e r1)
-> Sem r x -> Sem r1 x
forall (r :: [Effect]) (r' :: [Effect]) a.
(forall (e :: Effect). ElemOf e r -> ElemOf e r')
-> Sem r a -> Sem r' a
restack (SList extra -> ElemOf e r -> ElemOf e (extra ++ r)
forall {a} (l :: [a]) (r :: [a]) (e :: a).
SList l -> ElemOf e r -> ElemOf e (Append l r)
extendMembershipLeft (forall (l :: [Effect]). KnownList l => SList l
forall {a} (l :: [a]). KnownList l => SList l
singList @extra)) (f a -> x
ex (f a -> x) -> Sem r (f a) -> Sem r x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> param -> (resource -> Sem r1 (f a)) -> Sem r (f a)
forall x. param -> (resource -> Sem r1 x) -> Sem r x
withResource param
param \ resource
resource' -> resource -> InterpreterFor (Scoped param (effect !! err)) r1
inScope resource
resource' (f (Sem rInitial a) -> Sem (Scoped param (effect !! err) : r1) (f a)
forall x.
f (Sem rInitial x) -> Sem (Scoped param (effect !! err) : r1) (f x)
wv (Sem rInitial a
main Sem rInitial a -> f () -> f (Sem rInitial a)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s)))
interpretResumableScopedWith ::
∀ extra param resource effect err r r1 .
r1 ~ (extra ++ r) =>
KnownList extra =>
(∀ x . param -> (resource -> Sem r1 x) -> Sem r x) ->
(∀ r0 x . resource -> effect (Sem r0) x -> Sem (Stop err : r1) x) ->
InterpreterFor (Scoped param (effect !! err)) r
interpretResumableScopedWith :: forall (extra :: [Effect]) param resource (effect :: Effect) err
(r :: [Effect]) (r1 :: [Effect]).
(r1 ~ (extra ++ r), KnownList extra) =>
(forall x. param -> (resource -> Sem r1 x) -> Sem r x)
-> (forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Sem (Stop err : r1) x)
-> InterpreterFor (Scoped param (effect !! err)) r
interpretResumableScopedWith forall x. param -> (resource -> Sem r1 x) -> Sem r x
withResource forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Sem (Stop err : r1) x
scopedHandler =
forall (extra :: [Effect]) param resource (effect :: Effect) err
(r :: [Effect]) (r1 :: [Effect]).
(r1 ~ (extra ++ r), KnownList extra) =>
(forall x. param -> (resource -> Sem r1 x) -> Sem r x)
-> (forall (r0 :: [Effect]) x.
resource
-> effect (Sem r0) x -> Tactical effect (Sem r0) (Stop err : r1) x)
-> InterpreterFor (Scoped param (effect !! err)) r
interpretResumableScopedWithH @extra forall x. param -> (resource -> Sem r1 x) -> Sem r x
withResource \ resource
r effect (Sem r0) x
e -> Sem (Stop err : r1) x
-> Sem (WithTactics effect f (Sem r0) (Stop err : r1)) (f x)
forall (m :: * -> *) (f :: * -> *) (r :: [Effect]) (e :: Effect) a.
Functor f =>
Sem r a -> Sem (WithTactics e f m r) (f a)
liftT (resource -> effect (Sem r0) x -> Sem (Stop err : r1) x
forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Sem (Stop err : r1) x
scopedHandler resource
r effect (Sem r0) x
e)
interpretResumableScopedWith_ ::
∀ extra param effect err r r1 .
r1 ~ (extra ++ r) =>
KnownList extra =>
(∀ x . param -> Sem r1 x -> Sem r x) ->
(∀ r0 x . effect (Sem r0) x -> Sem (Stop err : r1) x) ->
InterpreterFor (Scoped param (effect !! err)) r
interpretResumableScopedWith_ :: forall (extra :: [Effect]) param (effect :: Effect) err
(r :: [Effect]) (r1 :: [Effect]).
(r1 ~ (extra ++ r), KnownList extra) =>
(forall x. param -> Sem r1 x -> Sem r x)
-> (forall (r0 :: [Effect]) x.
effect (Sem r0) x -> Sem (Stop err : r1) x)
-> InterpreterFor (Scoped param (effect !! err)) r
interpretResumableScopedWith_ forall x. param -> Sem r1 x -> Sem r x
extra forall (r0 :: [Effect]) x.
effect (Sem r0) x -> Sem (Stop err : r1) x
scopedHandler =
forall (extra :: [Effect]) param resource (effect :: Effect) err
(r :: [Effect]) (r1 :: [Effect]).
(r1 ~ (extra ++ r), KnownList extra) =>
(forall x. param -> (resource -> Sem r1 x) -> Sem r x)
-> (forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Sem (Stop err : r1) x)
-> InterpreterFor (Scoped param (effect !! err)) r
interpretResumableScopedWith @extra @param @() @effect @err @r @r1 (\ param
p () -> Sem r1 x
f -> param -> Sem r1 x -> Sem r x
forall x. param -> Sem r1 x -> Sem r x
extra param
p (() -> Sem r1 x
f ())) ((effect (Sem r0) x -> Sem (Stop err : r1) x)
-> () -> effect (Sem r0) x -> Sem (Stop err : r1) x
forall a b. a -> b -> a
const effect (Sem r0) x -> Sem (Stop err : r1) x
forall (r0 :: [Effect]) x.
effect (Sem r0) x -> Sem (Stop err : r1) x
scopedHandler)
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 (Sem r0) (Stop ei : r) x) ->
InterpreterFor (Scoped param (effect !! ei) !! eo) r
interpretScopedRH :: forall param resource (effect :: Effect) eo ei (r :: [Effect]).
(forall x.
param -> (resource -> Sem (Stop eo : r) x) -> Sem (Stop eo : r) x)
-> (forall (r0 :: [Effect]) x.
resource
-> effect (Sem r0) x -> Tactical effect (Sem r0) (Stop ei : r) x)
-> InterpreterFor (Scoped param (effect !! ei) !! eo) r
interpretScopedRH forall x.
param -> (resource -> Sem (Stop eo : r) x) -> Sem (Stop eo : r) x
withResource forall (r0 :: [Effect]) x.
resource
-> effect (Sem r0) x -> Tactical effect (Sem r0) (Stop ei : r) x
scopedHandler =
resource -> InterpreterFor (Scoped param (effect !! ei) !! eo) r
run ([Char] -> resource
forall a. [Char] -> a
errorWithoutStackTrace [Char]
"top level run")
where
run :: resource -> InterpreterFor (Scoped param (effect !! ei) !! eo) r
run :: resource -> InterpreterFor (Scoped param (effect !! ei) !! eo) r
run resource
resource =
(forall x.
Weaving
(Scoped param (effect !! ei) !! eo)
(Sem ((Scoped param (effect !! ei) !! eo) : r))
x
-> Sem r x)
-> InterpreterFor (Scoped param (effect !! ei) !! eo) r
forall (e :: Effect) (r :: [Effect]).
(forall x. Weaving e (Sem (e : r)) x -> Sem r x)
-> InterpreterFor e r
interpretWeaving \ (Weaving (Resumable (Weaving Scoped param (effect !! ei) (Sem rInitial) a
inner f ()
s' forall x. f (Sem rInitial x) -> Sem r (f x)
dist' 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) : r) (f x)
dist'' f a -> x
ex'' forall x. f x -> Maybe x
ins'') -> case Scoped param (effect !! ei) (Sem rInitial) a
inner of
Run (Resumable (Weaving effect (Sem rInitial) a
effect f ()
s forall x. f (Sem rInitial x) -> Sem r (f x)
dist f a -> a1
ex forall x. f x -> Maybe x
ins)) ->
Either ei (Compose f (Compose f f) a) -> x
exFinal (Either ei (Compose f (Compose f f) a) -> x)
-> Sem r (Either ei (Compose f (Compose f f) a)) -> Sem r x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall e (r :: [Effect]) a.
Sem (Stop e : r) a -> Sem r (Either e a)
runStop @ei (Sem
(Tactics
(Compose f (Compose f f)) (Sem rInitial) (effect : Stop ei : r)
: Stop ei : r)
(Compose f (Compose f f) a)
-> Sem (Stop ei : r) (Compose f (Compose f f) a)
tac (resource
-> effect (Sem rInitial) a
-> Tactical effect (Sem rInitial) (Stop ei : r) a
forall (r0 :: [Effect]) x.
resource
-> effect (Sem r0) x -> Tactical effect (Sem r0) (Stop ei : r) x
scopedHandler resource
resource effect (Sem rInitial) a
effect))
where
tac :: Sem
(Tactics
(Compose f (Compose f f)) (Sem rInitial) (effect : Stop ei : r)
: Stop ei : r)
(Compose f (Compose f f) a)
-> Sem (Stop ei : r) (Compose f (Compose f f) a)
tac =
Compose f (Compose f f) ()
-> (forall x.
Compose f (Compose f f) (Sem rInitial x)
-> Sem (effect : Stop ei : r) (Compose f (Compose f f) x))
-> (forall x. Compose f (Compose f f) x -> Maybe x)
-> (forall x.
Compose f (Compose f f) (Sem rInitial x)
-> Sem (Stop ei : r) (Compose f (Compose f f) x))
-> Sem
(Tactics
(Compose f (Compose f f)) (Sem rInitial) (effect : Stop ei : r)
: Stop ei : r)
(Compose f (Compose f f) a)
-> Sem (Stop ei : r) (Compose f (Compose f f) a)
forall (f :: * -> *) (m :: * -> *) (r2 :: [Effect]) (r :: [Effect])
a.
Functor f =>
f ()
-> (forall x. f (m x) -> Sem r2 (f x))
-> (forall x. f x -> Maybe x)
-> (forall x. f (m x) -> Sem r (f x))
-> Sem (Tactics f m r2 : r) a
-> Sem r a
runTactics
(f (Compose f f ()) -> Compose f (Compose f f) ()
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (f (f ()) -> Compose f f ()
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (f ()
s f () -> f () -> f (f ())
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s') Compose f f () -> f () -> f (Compose f f ())
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s''))
(Sem (Stop ei : r) (Compose f (Compose f f) x)
-> Sem (effect : Stop ei : r) (Compose f (Compose f f) x)
forall (e :: Effect) (r :: [Effect]) a. Sem r a -> Sem (e : r) a
raise (Sem (Stop ei : r) (Compose f (Compose f f) x)
-> Sem (effect : Stop ei : r) (Compose f (Compose f f) x))
-> (Compose f (Compose f f) (Sem rInitial x)
-> Sem (Stop ei : r) (Compose f (Compose f f) x))
-> Compose f (Compose f f) (Sem rInitial x)
-> Sem (effect : Stop ei : r) (Compose f (Compose f f) x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sem r (Compose f (Compose f f) x)
-> Sem (Stop ei : r) (Compose f (Compose f f) x)
forall (e :: Effect) (r :: [Effect]) a. Sem r a -> Sem (e : r) a
raise (Sem r (Compose f (Compose f f) x)
-> Sem (Stop ei : r) (Compose f (Compose f f) x))
-> (Compose f (Compose f f) (Sem rInitial x)
-> Sem r (Compose f (Compose f f) x))
-> Compose f (Compose f f) (Sem rInitial x)
-> Sem (Stop ei : r) (Compose f (Compose f f) x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. resource -> InterpreterFor (Scoped param (effect !! ei) !! eo) r
run resource
resource (Sem
((Scoped param (effect !! ei) !! eo) : r)
(Compose f (Compose f f) x)
-> Sem r (Compose f (Compose f f) x))
-> (Compose f (Compose f f) (Sem rInitial x)
-> Sem
((Scoped param (effect !! ei) !! eo) : r)
(Compose f (Compose f f) x))
-> Compose f (Compose f f) (Sem rInitial x)
-> Sem r (Compose f (Compose f f) x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f (Compose f f x) -> Compose f (Compose f f) x)
-> Sem
((Scoped param (effect !! ei) !! eo) : r) (f (Compose f f x))
-> Sem
((Scoped param (effect !! ei) !! eo) : r)
(Compose f (Compose f f) x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (Compose f f x) -> Compose f (Compose f f) x
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (Sem ((Scoped param (effect !! ei) !! eo) : r) (f (Compose f f x))
-> Sem
((Scoped param (effect !! ei) !! eo) : r)
(Compose f (Compose f f) x))
-> (Compose f (Compose f f) (Sem rInitial x)
-> Sem
((Scoped param (effect !! ei) !! eo) : r) (f (Compose f f x)))
-> Compose f (Compose f f) (Sem rInitial x)
-> Sem
((Scoped param (effect !! ei) !! eo) : r)
(Compose f (Compose f f) x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f (f (f x)) -> f (Compose f f x))
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (f (f (f x)))
-> Sem
((Scoped param (effect !! ei) !! eo) : r) (f (Compose f f x))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((f (f x) -> Compose f f x) -> f (f (f x)) -> f (Compose f f x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (f x) -> Compose f f x
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose) (Sem ((Scoped param (effect !! ei) !! eo) : r) (f (f (f x)))
-> Sem
((Scoped param (effect !! ei) !! eo) : r) (f (Compose f f x)))
-> (Compose f (Compose f f) (Sem rInitial x)
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (f (f (f x))))
-> Compose f (Compose f f) (Sem rInitial x)
-> Sem
((Scoped param (effect !! ei) !! eo) : r) (f (Compose f f x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Sem rInitial (f (f x)))
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (f (f (f x)))
forall x.
f (Sem rInitial x)
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (f x)
dist'' (f (Sem rInitial (f (f x)))
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (f (f (f x))))
-> (Compose f (Compose f f) (Sem rInitial x)
-> f (Sem rInitial (f (f x))))
-> Compose f (Compose f f) (Sem rInitial x)
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (f (f (f x)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f (Sem rInitial (f x)) -> Sem r (f (f x)))
-> f (f (Sem rInitial (f x))) -> f (Sem r (f (f x)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (Sem rInitial (f x)) -> Sem r (f (f x))
forall x. f (Sem rInitial x) -> Sem r (f x)
dist' (f (f (Sem rInitial (f x))) -> f (Sem r (f (f x))))
-> (Compose f (Compose f f) (Sem rInitial x)
-> f (f (Sem rInitial (f x))))
-> Compose f (Compose f f) (Sem rInitial x)
-> f (Sem r (f (f x)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Compose f f (Sem rInitial x) -> f (Sem r (f x)))
-> f (Compose f f (Sem rInitial x)) -> f (f (Sem r (f x)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((f (Sem rInitial x) -> Sem r (f x))
-> f (f (Sem rInitial x)) -> f (Sem r (f x))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (Sem rInitial x) -> Sem r (f x)
forall x. f (Sem rInitial x) -> Sem r (f x)
dist (f (f (Sem rInitial x)) -> f (Sem r (f x)))
-> (Compose f f (Sem rInitial x) -> f (f (Sem rInitial x)))
-> Compose f f (Sem rInitial x)
-> f (Sem r (f x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose f f (Sem rInitial x) -> f (f (Sem rInitial x))
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose) (f (Compose f f (Sem rInitial x)) -> f (f (Sem r (f x))))
-> (Compose f (Compose f f) (Sem rInitial x)
-> f (Compose f f (Sem rInitial x)))
-> Compose f (Compose f f) (Sem rInitial x)
-> f (f (Sem r (f x)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose f (Compose f f) (Sem rInitial x)
-> f (Compose f f (Sem rInitial x))
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose)
(f x -> Maybe x
forall x. f x -> Maybe x
ins (f x -> Maybe x)
-> (Compose f (Compose f f) x -> Maybe (f x))
-> Compose f (Compose f f) x
-> Maybe x
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< f (f x) -> Maybe (f x)
forall x. f x -> Maybe x
ins' (f (f x) -> Maybe (f x))
-> (Compose f f x -> f (f x)) -> Compose f f x -> Maybe (f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose f f x -> f (f x)
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose (Compose f f x -> Maybe (f x))
-> (Compose f (Compose f f) x -> Maybe (Compose f f x))
-> Compose f (Compose f f) x
-> Maybe (f x)
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< f (Compose f f x) -> Maybe (Compose f f x)
forall x. f x -> Maybe x
ins'' (f (Compose f f x) -> Maybe (Compose f f x))
-> (Compose f (Compose f f) x -> f (Compose f f x))
-> Compose f (Compose f f) x
-> Maybe (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose f (Compose f f) x -> f (Compose f f x)
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose)
(Sem r (Compose f (Compose f f) x)
-> Sem (Stop ei : r) (Compose f (Compose f f) x)
forall (e :: Effect) (r :: [Effect]) a. Sem r a -> Sem (e : r) a
raise (Sem r (Compose f (Compose f f) x)
-> Sem (Stop ei : r) (Compose f (Compose f f) x))
-> (Compose f (Compose f f) (Sem rInitial x)
-> Sem r (Compose f (Compose f f) x))
-> Compose f (Compose f f) (Sem rInitial x)
-> Sem (Stop ei : r) (Compose f (Compose f f) x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. resource -> InterpreterFor (Scoped param (effect !! ei) !! eo) r
run resource
resource (Sem
((Scoped param (effect !! ei) !! eo) : r)
(Compose f (Compose f f) x)
-> Sem r (Compose f (Compose f f) x))
-> (Compose f (Compose f f) (Sem rInitial x)
-> Sem
((Scoped param (effect !! ei) !! eo) : r)
(Compose f (Compose f f) x))
-> Compose f (Compose f f) (Sem rInitial x)
-> Sem r (Compose f (Compose f f) x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f (Compose f f x) -> Compose f (Compose f f) x)
-> Sem
((Scoped param (effect !! ei) !! eo) : r) (f (Compose f f x))
-> Sem
((Scoped param (effect !! ei) !! eo) : r)
(Compose f (Compose f f) x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (Compose f f x) -> Compose f (Compose f f) x
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (Sem ((Scoped param (effect !! ei) !! eo) : r) (f (Compose f f x))
-> Sem
((Scoped param (effect !! ei) !! eo) : r)
(Compose f (Compose f f) x))
-> (Compose f (Compose f f) (Sem rInitial x)
-> Sem
((Scoped param (effect !! ei) !! eo) : r) (f (Compose f f x)))
-> Compose f (Compose f f) (Sem rInitial x)
-> Sem
((Scoped param (effect !! ei) !! eo) : r)
(Compose f (Compose f f) x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f (f (f x)) -> f (Compose f f x))
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (f (f (f x)))
-> Sem
((Scoped param (effect !! ei) !! eo) : r) (f (Compose f f x))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((f (f x) -> Compose f f x) -> f (f (f x)) -> f (Compose f f x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (f x) -> Compose f f x
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose) (Sem ((Scoped param (effect !! ei) !! eo) : r) (f (f (f x)))
-> Sem
((Scoped param (effect !! ei) !! eo) : r) (f (Compose f f x)))
-> (Compose f (Compose f f) (Sem rInitial x)
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (f (f (f x))))
-> Compose f (Compose f f) (Sem rInitial x)
-> Sem
((Scoped param (effect !! ei) !! eo) : r) (f (Compose f f x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Sem rInitial (f (f x)))
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (f (f (f x)))
forall x.
f (Sem rInitial x)
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (f x)
dist'' (f (Sem rInitial (f (f x)))
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (f (f (f x))))
-> (Compose f (Compose f f) (Sem rInitial x)
-> f (Sem rInitial (f (f x))))
-> Compose f (Compose f f) (Sem rInitial x)
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (f (f (f x)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f (Sem rInitial (f x)) -> Sem r (f (f x)))
-> f (f (Sem rInitial (f x))) -> f (Sem r (f (f x)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (Sem rInitial (f x)) -> Sem r (f (f x))
forall x. f (Sem rInitial x) -> Sem r (f x)
dist' (f (f (Sem rInitial (f x))) -> f (Sem r (f (f x))))
-> (Compose f (Compose f f) (Sem rInitial x)
-> f (f (Sem rInitial (f x))))
-> Compose f (Compose f f) (Sem rInitial x)
-> f (Sem r (f (f x)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Compose f f (Sem rInitial x) -> f (Sem r (f x)))
-> f (Compose f f (Sem rInitial x)) -> f (f (Sem r (f x)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((f (Sem rInitial x) -> Sem r (f x))
-> f (f (Sem rInitial x)) -> f (Sem r (f x))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (Sem rInitial x) -> Sem r (f x)
forall x. f (Sem rInitial x) -> Sem r (f x)
dist (f (f (Sem rInitial x)) -> f (Sem r (f x)))
-> (Compose f f (Sem rInitial x) -> f (f (Sem rInitial x)))
-> Compose f f (Sem rInitial x)
-> f (Sem r (f x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose f f (Sem rInitial x) -> f (f (Sem rInitial x))
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose) (f (Compose f f (Sem rInitial x)) -> f (f (Sem r (f x))))
-> (Compose f (Compose f f) (Sem rInitial x)
-> f (Compose f f (Sem rInitial x)))
-> Compose f (Compose f f) (Sem rInitial x)
-> f (f (Sem r (f x)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose f (Compose f f) (Sem rInitial x)
-> f (Compose f f (Sem rInitial x))
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose)
exFinal :: Either ei (Compose f (Compose f f) a) -> x
exFinal = \case
Right (Compose f (Compose f f a)
fffa) ->
f a -> x
ex'' (f a -> x) -> f a -> x
forall a b. (a -> b) -> a -> b
$ f (Compose f f a)
fffa f (Compose f f a)
-> (Compose f f a -> Either eo a1) -> f (Either eo a1)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> a1 -> Either eo a1
forall a b. b -> Either a b
Right (a1 -> Either eo a1)
-> (Compose f f a -> a1) -> Compose f f a -> Either eo a1
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \ (Compose f (f a)
ffa) ->
f a -> a1
ex' (a1 -> Either ei a1
forall a b. b -> Either a b
Right (a1 -> Either ei a1) -> (f a -> a1) -> f a -> Either ei a1
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> a1
ex (f a -> Either ei a1) -> f (f a) -> f (Either ei a1)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (f a)
ffa)
Left ei
err ->
f a -> x
ex'' (a1 -> Either eo a1
forall a b. b -> Either a b
Right (f a -> a1
ex' (ei -> Either ei a1
forall a b. a -> Either a b
Left ei
err Either ei a1 -> f () -> f (Either ei a1)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s')) Either eo a1 -> f () -> f (Either eo a1)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s'')
InScope param
param Sem rInitial a
main -> do
let
inScope :: Sem
(Tactics (Compose f f) (Sem rInitial) (Any : Any : r)
: Stop eo : r)
(Compose f f a)
inScope =
Sem (Stop eo : r) (Compose f f a)
-> Sem
(Tactics (Compose f f) (Sem rInitial) (Any : Any : r)
: Stop eo : r)
(Compose f f a)
forall (e :: Effect) (r :: [Effect]) a. Sem r a -> Sem (e : r) a
raise (param
-> (resource -> Sem (Stop eo : r) (Compose f f a))
-> Sem (Stop eo : r) (Compose f f a)
forall x.
param -> (resource -> Sem (Stop eo : r) x) -> Sem (Stop eo : r) x
withResource param
param \ resource
resource' -> f (f a) -> Compose f f a
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (f (f a) -> Compose f f a)
-> Sem (Stop eo : r) (f (f a)) -> Sem (Stop eo : r) (Compose f f a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sem r (f (f a)) -> Sem (Stop eo : r) (f (f a))
forall (e :: Effect) (r :: [Effect]) a. Sem r a -> Sem (e : r) a
raise (resource -> InterpreterFor (Scoped param (effect !! ei) !! eo) r
run resource
resource' (f (Sem rInitial (f a))
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (f (f a))
forall x.
f (Sem rInitial x)
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (f x)
dist'' (f (Sem rInitial a) -> Sem r (f a)
forall x. f (Sem rInitial x) -> Sem r (f x)
dist' (Sem rInitial a
main Sem rInitial a -> f () -> f (Sem rInitial a)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s') Sem r (f a) -> f () -> f (Sem r (f a))
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s''))))
tac :: Sem (Stop eo : r) (Compose f f a)
tac =
Compose f f ()
-> (forall x.
Compose f f (Sem rInitial x)
-> Sem (Any : Any : r) (Compose f f x))
-> (forall x. Compose f f x -> Maybe x)
-> (forall x.
Compose f f (Sem rInitial x) -> Sem (Stop eo : r) (Compose f f x))
-> Sem
(Tactics (Compose f f) (Sem rInitial) (Any : Any : r)
: Stop eo : r)
(Compose f f a)
-> Sem (Stop eo : r) (Compose f f a)
forall (f :: * -> *) (m :: * -> *) (r2 :: [Effect]) (r :: [Effect])
a.
Functor f =>
f ()
-> (forall x. f (m x) -> Sem r2 (f x))
-> (forall x. f x -> Maybe x)
-> (forall x. f (m x) -> Sem r (f x))
-> Sem (Tactics f m r2 : r) a
-> Sem r a
runTactics
(f (f ()) -> Compose f f ()
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (f ()
s' f () -> f () -> f (f ())
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s''))
(Sem (Any : r) (Compose f f x)
-> Sem (Any : Any : r) (Compose f f x)
forall (e :: Effect) (r :: [Effect]) a. Sem r a -> Sem (e : r) a
raise (Sem (Any : r) (Compose f f x)
-> Sem (Any : Any : r) (Compose f f x))
-> (Compose f f (Sem rInitial x) -> Sem (Any : r) (Compose f f x))
-> Compose f f (Sem rInitial x)
-> Sem (Any : Any : r) (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sem r (Compose f f x) -> Sem (Any : r) (Compose f f x)
forall (e :: Effect) (r :: [Effect]) a. Sem r a -> Sem (e : r) a
raise (Sem r (Compose f f x) -> Sem (Any : r) (Compose f f x))
-> (Compose f f (Sem rInitial x) -> Sem r (Compose f f x))
-> Compose f f (Sem rInitial x)
-> Sem (Any : r) (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. resource -> InterpreterFor (Scoped param (effect !! ei) !! eo) r
run resource
resource (Sem ((Scoped param (effect !! ei) !! eo) : r) (Compose f f x)
-> Sem r (Compose f f x))
-> (Compose f f (Sem rInitial x)
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (Compose f f x))
-> Compose f f (Sem rInitial x)
-> Sem r (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f (f x) -> Compose f f x)
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (f (f x))
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (Compose f f x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (f x) -> Compose f f x
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (Sem ((Scoped param (effect !! ei) !! eo) : r) (f (f x))
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (Compose f f x))
-> (Compose f f (Sem rInitial x)
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (f (f x)))
-> Compose f f (Sem rInitial x)
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Sem rInitial (f x))
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (f (f x))
forall x.
f (Sem rInitial x)
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (f x)
dist'' (f (Sem rInitial (f x))
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (f (f x)))
-> (Compose f f (Sem rInitial x) -> f (Sem rInitial (f x)))
-> Compose f f (Sem rInitial x)
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (f (f x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f (Sem rInitial x) -> Sem r (f x))
-> f (f (Sem rInitial x)) -> f (Sem r (f x))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (Sem rInitial x) -> Sem r (f x)
forall x. f (Sem rInitial x) -> Sem r (f x)
dist' (f (f (Sem rInitial x)) -> f (Sem r (f x)))
-> (Compose f f (Sem rInitial x) -> f (f (Sem rInitial x)))
-> Compose f f (Sem rInitial x)
-> f (Sem r (f x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose f f (Sem rInitial x) -> f (f (Sem rInitial x))
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose)
(f x -> Maybe x
forall x. f x -> Maybe x
ins' (f x -> Maybe x)
-> (Compose f f x -> Maybe (f x)) -> Compose f f x -> Maybe x
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< f (f x) -> Maybe (f x)
forall x. f x -> Maybe x
ins'' (f (f x) -> Maybe (f x))
-> (Compose f f x -> f (f x)) -> Compose f f x -> Maybe (f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose f f x -> f (f x)
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose)
(Sem r (Compose f f x) -> Sem (Stop eo : r) (Compose f f x)
forall (e :: Effect) (r :: [Effect]) a. Sem r a -> Sem (e : r) a
raise (Sem r (Compose f f x) -> Sem (Stop eo : r) (Compose f f x))
-> (Compose f f (Sem rInitial x) -> Sem r (Compose f f x))
-> Compose f f (Sem rInitial x)
-> Sem (Stop eo : r) (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. resource -> InterpreterFor (Scoped param (effect !! ei) !! eo) r
run resource
resource (Sem ((Scoped param (effect !! ei) !! eo) : r) (Compose f f x)
-> Sem r (Compose f f x))
-> (Compose f f (Sem rInitial x)
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (Compose f f x))
-> Compose f f (Sem rInitial x)
-> Sem r (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f (f x) -> Compose f f x)
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (f (f x))
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (Compose f f x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (f x) -> Compose f f x
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (Sem ((Scoped param (effect !! ei) !! eo) : r) (f (f x))
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (Compose f f x))
-> (Compose f f (Sem rInitial x)
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (f (f x)))
-> Compose f f (Sem rInitial x)
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Sem rInitial (f x))
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (f (f x))
forall x.
f (Sem rInitial x)
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (f x)
dist'' (f (Sem rInitial (f x))
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (f (f x)))
-> (Compose f f (Sem rInitial x) -> f (Sem rInitial (f x)))
-> Compose f f (Sem rInitial x)
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (f (f x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f (Sem rInitial x) -> Sem r (f x))
-> f (f (Sem rInitial x)) -> f (Sem r (f x))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (Sem rInitial x) -> Sem r (f x)
forall x. f (Sem rInitial x) -> Sem r (f x)
dist' (f (f (Sem rInitial x)) -> f (Sem r (f x)))
-> (Compose f f (Sem rInitial x) -> f (f (Sem rInitial x)))
-> Compose f f (Sem rInitial x)
-> f (Sem r (f x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose f f (Sem rInitial x) -> f (f (Sem rInitial x))
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose)
Sem
(Tactics (Compose f f) (Sem rInitial) (Any : Any : r)
: Stop eo : r)
(Compose f f a)
inScope
exFinal :: Either eo (Compose f f a) -> x
exFinal = f a -> x
ex'' (f a -> x)
-> (Either eo (Compose f f a) -> f a)
-> Either eo (Compose f f a)
-> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
Right (Compose f (f a)
a) -> a1 -> Either eo a1
forall a b. b -> Either a b
Right (a1 -> Either eo a1) -> (f a -> a1) -> f a -> Either eo a1
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> a1
ex' (f a -> Either eo a1) -> f (f a) -> f (Either eo a1)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (f a)
a
Left eo
err -> eo -> Either eo a1
forall a b. a -> Either a b
Left eo
err Either eo a1 -> f () -> f (Either eo a1)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s''
Either eo (Compose f f a) -> x
exFinal (Either eo (Compose f f a) -> x)
-> Sem r (Either eo (Compose f f a)) -> Sem r x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sem (Stop eo : r) (Compose f f a)
-> Sem r (Either eo (Compose f f a))
forall e (r :: [Effect]) a.
Sem (Stop e : r) a -> Sem r (Either e a)
runStop Sem (Stop eo : r) (Compose f f a)
tac
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 : r) x) ->
InterpreterFor (Scoped param (effect !! ei) !! eo) r
interpretScopedR :: forall param resource (effect :: Effect) eo ei (r :: [Effect]).
(forall x.
param -> (resource -> Sem (Stop eo : r) x) -> Sem (Stop eo : r) x)
-> (forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Sem (Stop ei : r) x)
-> InterpreterFor (Scoped param (effect !! ei) !! eo) r
interpretScopedR forall x.
param -> (resource -> Sem (Stop eo : r) x) -> Sem (Stop eo : r) x
withResource forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Sem (Stop ei : r) x
scopedHandler =
(forall x.
param -> (resource -> Sem (Stop eo : r) x) -> Sem (Stop eo : r) x)
-> (forall (r0 :: [Effect]) x.
resource
-> effect (Sem r0) x -> Tactical effect (Sem r0) (Stop ei : r) x)
-> InterpreterFor (Scoped param (effect !! ei) !! eo) r
forall param resource (effect :: Effect) eo ei (r :: [Effect]).
(forall x.
param -> (resource -> Sem (Stop eo : r) x) -> Sem (Stop eo : r) x)
-> (forall (r0 :: [Effect]) x.
resource
-> effect (Sem r0) x -> Tactical effect (Sem r0) (Stop ei : r) x)
-> InterpreterFor (Scoped param (effect !! ei) !! eo) r
interpretScopedRH forall x.
param -> (resource -> Sem (Stop eo : r) x) -> Sem (Stop eo : r) x
withResource \ resource
r effect (Sem r0) x
e -> Sem (Stop ei : r) x
-> Sem (WithTactics effect f (Sem r0) (Stop ei : r)) (f x)
forall (m :: * -> *) (f :: * -> *) (r :: [Effect]) (e :: Effect) a.
Functor f =>
Sem r a -> Sem (WithTactics e f m r) (f a)
liftT (resource -> effect (Sem r0) x -> Sem (Stop ei : r) x
forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Sem (Stop ei : r) x
scopedHandler resource
r effect (Sem r0) x
e)
interpretScopedR_ ::
∀ param resource effect eo ei r .
(param -> Sem (Stop eo : r) resource) ->
(∀ r0 x . resource -> effect (Sem r0) x -> Sem (Stop ei : r) x) ->
InterpreterFor (Scoped param (effect !! ei) !! eo) r
interpretScopedR_ :: forall param resource (effect :: Effect) eo ei (r :: [Effect]).
(param -> Sem (Stop eo : r) resource)
-> (forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Sem (Stop ei : r) x)
-> InterpreterFor (Scoped param (effect !! ei) !! eo) r
interpretScopedR_ param -> Sem (Stop eo : r) resource
resource =
(forall x.
param -> (resource -> Sem (Stop eo : r) x) -> Sem (Stop eo : r) x)
-> (forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Sem (Stop ei : r) x)
-> InterpreterFor (Scoped param (effect !! ei) !! eo) r
forall param resource (effect :: Effect) eo ei (r :: [Effect]).
(forall x.
param -> (resource -> Sem (Stop eo : r) x) -> Sem (Stop eo : r) x)
-> (forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Sem (Stop ei : r) x)
-> InterpreterFor (Scoped param (effect !! ei) !! eo) r
interpretScopedR \ param
p resource -> Sem (Stop eo : r) x
use -> resource -> Sem (Stop eo : r) x
use (resource -> Sem (Stop eo : r) x)
-> Sem (Stop eo : r) resource -> Sem (Stop eo : r) x
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< param -> Sem (Stop eo : r) resource
resource param
p
interpretScopedRWithH ::
∀ extra param resource effect eo ei r r1 .
r1 ~ (extra ++ Stop eo : r) =>
r1 ~ ((extra ++ '[Stop eo]) ++ r) =>
KnownList extra =>
KnownList (extra ++ '[Stop eo]) =>
(∀ x . param -> (resource -> Sem r1 x) -> Sem (Stop eo : r) x) ->
(∀ r0 x . resource -> effect (Sem r0) x -> Tactical effect (Sem r0) (Stop ei : r1) x) ->
InterpreterFor (Scoped param (effect !! ei) !! eo) r
interpretScopedRWithH :: forall (extra :: [Effect]) param resource (effect :: Effect) eo ei
(r :: [Effect]) (r1 :: [Effect]).
(r1 ~ (extra ++ (Stop eo : r)), r1 ~ ((extra ++ '[Stop eo]) ++ r),
KnownList extra, KnownList (extra ++ '[Stop eo])) =>
(forall x. param -> (resource -> Sem r1 x) -> Sem (Stop eo : r) x)
-> (forall (r0 :: [Effect]) x.
resource
-> effect (Sem r0) x -> Tactical effect (Sem r0) (Stop ei : r1) x)
-> InterpreterFor (Scoped param (effect !! ei) !! eo) r
interpretScopedRWithH forall x. param -> (resource -> Sem r1 x) -> Sem (Stop eo : r) x
withResource forall (r0 :: [Effect]) x.
resource
-> effect (Sem r0) x -> Tactical effect (Sem r0) (Stop ei : r1) x
scopedHandler =
Sem ((Scoped param (effect !! ei) !! eo) : r) a -> Sem r a
InterpreterFor (Scoped param (effect !! ei) !! eo) r
run
where
run :: InterpreterFor (Scoped param (effect !! ei) !! eo) r
run :: InterpreterFor (Scoped param (effect !! ei) !! eo) r
run =
(forall x.
Weaving
(Scoped param (effect !! ei) !! eo)
(Sem ((Scoped param (effect !! ei) !! eo) : r))
x
-> Sem r x)
-> InterpreterFor (Scoped param (effect !! ei) !! eo) r
forall (e :: Effect) (r :: [Effect]).
(forall x. Weaving e (Sem (e : r)) x -> Sem r x)
-> InterpreterFor e r
interpretWeaving \ (Weaving (Resumable (Weaving Scoped param (effect !! ei) (Sem rInitial) a
inner f ()
s' forall x. f (Sem rInitial x) -> Sem r (f x)
dist' 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) : r) (f x)
dist'' f a -> x
ex'' forall x. f x -> Maybe x
ins'') -> case Scoped param (effect !! ei) (Sem rInitial) a
inner of
InScope param
param Sem rInitial a
main -> do
let
ma :: Sem
(Tactics (Compose f f) (Sem rInitial) (Any : Any : r)
: Stop eo : r)
(Compose f f a)
ma =
Sem (Stop eo : r) (Compose f f a)
-> Sem
(Tactics (Compose f f) (Sem rInitial) (Any : Any : r)
: Stop eo : r)
(Compose f f a)
forall (e :: Effect) (r :: [Effect]) a. Sem r a -> Sem (e : r) a
raise (Sem (Stop eo : r) (Compose f f a)
-> Sem
(Tactics (Compose f f) (Sem rInitial) (Any : Any : r)
: Stop eo : r)
(Compose f f a))
-> Sem (Stop eo : r) (Compose f f a)
-> Sem
(Tactics (Compose f f) (Sem rInitial) (Any : Any : r)
: Stop eo : r)
(Compose f f a)
forall a b. (a -> b) -> a -> b
$ param
-> (resource -> Sem r1 (Compose f f a))
-> Sem (Stop eo : r) (Compose f f a)
forall x. param -> (resource -> Sem r1 x) -> Sem (Stop eo : r) x
withResource param
param \ resource
resource ->
f (f a) -> Compose f f a
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (f (f a) -> Compose f f a)
-> Sem r1 (f (f a)) -> Sem r1 (Compose f f a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> resource -> InterpreterFor (Scoped param (effect !! ei) !! eo) r1
inScope resource
resource ((forall (e :: Effect).
ElemOf e ((Scoped param (effect !! ei) !! eo) : r)
-> ElemOf e ((Scoped param (effect !! ei) !! eo) : r1))
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (f (f a))
-> Sem ((Scoped param (effect !! ei) !! eo) : r1) (f (f a))
forall (r :: [Effect]) (r' :: [Effect]) a.
(forall (e :: Effect). ElemOf e r -> ElemOf e r')
-> Sem r a -> Sem r' a
restack (SList '[Scoped param (effect !! ei) !! eo]
-> SList (extra ++ '[Stop eo])
-> ElemOf e (Append '[Scoped param (effect !! ei) !! eo] r)
-> ElemOf
e
(Append
'[Scoped param (effect !! ei) !! eo] ((extra ++ '[Stop eo]) ++ r))
forall {a} (right :: [a]) (e :: a) (left :: [a]) (mid :: [a]).
SList left
-> SList mid
-> ElemOf e (Append left right)
-> ElemOf e (Append left (Append mid right))
injectMembership (forall (l :: [Effect]). KnownList l => SList l
forall {a} (l :: [a]). KnownList l => SList l
singList @'[Scoped param (effect !! ei) !! eo]) (forall (l :: [Effect]). KnownList l => SList l
forall {a} (l :: [a]). KnownList l => SList l
singList @(extra ++ '[Stop eo]))) (f (Sem rInitial (f a))
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (f (f a))
forall x.
f (Sem rInitial x)
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (f x)
dist'' (f (Sem rInitial a) -> Sem r (f a)
forall x. f (Sem rInitial x) -> Sem r (f x)
dist' (Sem rInitial a
main Sem rInitial a -> f () -> f (Sem rInitial a)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s') Sem r (f a) -> f () -> f (Sem r (f a))
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s'')))
tac :: Sem (Stop eo : r) (Compose f f a)
tac =
Compose f f ()
-> (forall x.
Compose f f (Sem rInitial x)
-> Sem (Any : Any : r) (Compose f f x))
-> (forall x. Compose f f x -> Maybe x)
-> (forall x.
Compose f f (Sem rInitial x) -> Sem (Stop eo : r) (Compose f f x))
-> Sem
(Tactics (Compose f f) (Sem rInitial) (Any : Any : r)
: Stop eo : r)
(Compose f f a)
-> Sem (Stop eo : r) (Compose f f a)
forall (f :: * -> *) (m :: * -> *) (r2 :: [Effect]) (r :: [Effect])
a.
Functor f =>
f ()
-> (forall x. f (m x) -> Sem r2 (f x))
-> (forall x. f x -> Maybe x)
-> (forall x. f (m x) -> Sem r (f x))
-> Sem (Tactics f m r2 : r) a
-> Sem r a
runTactics
(f (f ()) -> Compose f f ()
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (f ()
s' f () -> f () -> f (f ())
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s''))
(Sem (Any : r) (Compose f f x)
-> Sem (Any : Any : r) (Compose f f x)
forall (e :: Effect) (r :: [Effect]) a. Sem r a -> Sem (e : r) a
raise (Sem (Any : r) (Compose f f x)
-> Sem (Any : Any : r) (Compose f f x))
-> (Compose f f (Sem rInitial x) -> Sem (Any : r) (Compose f f x))
-> Compose f f (Sem rInitial x)
-> Sem (Any : Any : r) (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sem r (Compose f f x) -> Sem (Any : r) (Compose f f x)
forall (e :: Effect) (r :: [Effect]) a. Sem r a -> Sem (e : r) a
raise (Sem r (Compose f f x) -> Sem (Any : r) (Compose f f x))
-> (Compose f f (Sem rInitial x) -> Sem r (Compose f f x))
-> Compose f f (Sem rInitial x)
-> Sem (Any : r) (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sem ((Scoped param (effect !! ei) !! eo) : r) (Compose f f x)
-> Sem r (Compose f f x)
InterpreterFor (Scoped param (effect !! ei) !! eo) r
run (Sem ((Scoped param (effect !! ei) !! eo) : r) (Compose f f x)
-> Sem r (Compose f f x))
-> (Compose f f (Sem rInitial x)
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (Compose f f x))
-> Compose f f (Sem rInitial x)
-> Sem r (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f (f x) -> Compose f f x)
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (f (f x))
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (Compose f f x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (f x) -> Compose f f x
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (Sem ((Scoped param (effect !! ei) !! eo) : r) (f (f x))
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (Compose f f x))
-> (Compose f f (Sem rInitial x)
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (f (f x)))
-> Compose f f (Sem rInitial x)
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Sem rInitial (f x))
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (f (f x))
forall x.
f (Sem rInitial x)
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (f x)
dist'' (f (Sem rInitial (f x))
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (f (f x)))
-> (Compose f f (Sem rInitial x) -> f (Sem rInitial (f x)))
-> Compose f f (Sem rInitial x)
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (f (f x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f (Sem rInitial x) -> Sem r (f x))
-> f (f (Sem rInitial x)) -> f (Sem r (f x))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (Sem rInitial x) -> Sem r (f x)
forall x. f (Sem rInitial x) -> Sem r (f x)
dist' (f (f (Sem rInitial x)) -> f (Sem r (f x)))
-> (Compose f f (Sem rInitial x) -> f (f (Sem rInitial x)))
-> Compose f f (Sem rInitial x)
-> f (Sem r (f x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose f f (Sem rInitial x) -> f (f (Sem rInitial x))
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose)
(f x -> Maybe x
forall x. f x -> Maybe x
ins' (f x -> Maybe x)
-> (Compose f f x -> Maybe (f x)) -> Compose f f x -> Maybe x
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< f (f x) -> Maybe (f x)
forall x. f x -> Maybe x
ins'' (f (f x) -> Maybe (f x))
-> (Compose f f x -> f (f x)) -> Compose f f x -> Maybe (f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose f f x -> f (f x)
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose)
(Sem r (Compose f f x) -> Sem (Stop eo : r) (Compose f f x)
forall (e :: Effect) (r :: [Effect]) a. Sem r a -> Sem (e : r) a
raise (Sem r (Compose f f x) -> Sem (Stop eo : r) (Compose f f x))
-> (Compose f f (Sem rInitial x) -> Sem r (Compose f f x))
-> Compose f f (Sem rInitial x)
-> Sem (Stop eo : r) (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sem ((Scoped param (effect !! ei) !! eo) : r) (Compose f f x)
-> Sem r (Compose f f x)
InterpreterFor (Scoped param (effect !! ei) !! eo) r
run (Sem ((Scoped param (effect !! ei) !! eo) : r) (Compose f f x)
-> Sem r (Compose f f x))
-> (Compose f f (Sem rInitial x)
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (Compose f f x))
-> Compose f f (Sem rInitial x)
-> Sem r (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f (f x) -> Compose f f x)
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (f (f x))
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (Compose f f x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (f x) -> Compose f f x
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (Sem ((Scoped param (effect !! ei) !! eo) : r) (f (f x))
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (Compose f f x))
-> (Compose f f (Sem rInitial x)
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (f (f x)))
-> Compose f f (Sem rInitial x)
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Sem rInitial (f x))
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (f (f x))
forall x.
f (Sem rInitial x)
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (f x)
dist'' (f (Sem rInitial (f x))
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (f (f x)))
-> (Compose f f (Sem rInitial x) -> f (Sem rInitial (f x)))
-> Compose f f (Sem rInitial x)
-> Sem ((Scoped param (effect !! ei) !! eo) : r) (f (f x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f (Sem rInitial x) -> Sem r (f x))
-> f (f (Sem rInitial x)) -> f (Sem r (f x))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (Sem rInitial x) -> Sem r (f x)
forall x. f (Sem rInitial x) -> Sem r (f x)
dist' (f (f (Sem rInitial x)) -> f (Sem r (f x)))
-> (Compose f f (Sem rInitial x) -> f (f (Sem rInitial x)))
-> Compose f f (Sem rInitial x)
-> f (Sem r (f x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose f f (Sem rInitial x) -> f (f (Sem rInitial x))
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose)
Sem
(Tactics (Compose f f) (Sem rInitial) (Any : Any : r)
: Stop eo : r)
(Compose f f a)
ma
exFinal :: Either eo (Compose f f a) -> x
exFinal = f a -> x
ex'' (f a -> x)
-> (Either eo (Compose f f a) -> f a)
-> Either eo (Compose f f a)
-> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
Right (Compose f (f a)
a) -> a1 -> Either eo a1
forall a b. b -> Either a b
Right (a1 -> Either eo a1) -> (f a -> a1) -> f a -> Either eo a1
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> a1
ex' (f a -> Either eo a1) -> f (f a) -> f (Either eo a1)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (f a)
a
Left eo
err -> eo -> Either eo a1
forall a b. a -> Either a b
Left eo
err Either eo a1 -> f () -> f (Either eo a1)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s''
Either eo (Compose f f a) -> x
exFinal (Either eo (Compose f f a) -> x)
-> Sem r (Either eo (Compose f f a)) -> Sem r x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sem (Stop eo : r) (Compose f f a)
-> Sem r (Either eo (Compose f f a))
forall e (r :: [Effect]) a.
Sem (Stop e : r) a -> Sem r (Either e a)
runStop Sem (Stop eo : r) (Compose f f a)
tac
Scoped param (effect !! ei) (Sem rInitial) a
_ ->
[Char] -> Sem r x
forall a. HasCallStack => [Char] -> a
error [Char]
"top level Run"
inScope :: resource -> InterpreterFor (Scoped param (effect !! ei) !! eo) r1
inScope :: resource -> InterpreterFor (Scoped param (effect !! ei) !! eo) r1
inScope resource
resource =
(forall x.
Weaving
(Scoped param (effect !! ei) !! eo)
(Sem ((Scoped param (effect !! ei) !! eo) : r1))
x
-> Sem r1 x)
-> InterpreterFor (Scoped param (effect !! ei) !! eo) r1
forall (e :: Effect) (r :: [Effect]).
(forall x. Weaving e (Sem (e : r)) x -> Sem r x)
-> InterpreterFor e r
interpretWeaving \ (Weaving (Resumable (Weaving Scoped param (effect !! ei) (Sem rInitial) a
inner f ()
s' forall x. f (Sem rInitial x) -> Sem r (f x)
dist' 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) : r1) (f x)
dist'' f a -> x
ex'' forall x. f x -> Maybe x
ins'') -> case Scoped param (effect !! ei) (Sem rInitial) a
inner of
Run (Resumable (Weaving effect (Sem rInitial) a
effect f ()
s forall x. f (Sem rInitial x) -> Sem r (f x)
dist f a -> a1
ex forall x. f x -> Maybe x
ins)) ->
Either ei (Compose f (Compose f f) a) -> x
exFinal (Either ei (Compose f (Compose f f) a) -> x)
-> Sem r1 (Either ei (Compose f (Compose f f) a)) -> Sem r1 x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall e (r :: [Effect]) a.
Sem (Stop e : r) a -> Sem r (Either e a)
runStop @ei (Sem
(Tactics
(Compose f (Compose f f)) (Sem rInitial) (effect : Stop ei : r1)
: Stop ei : r1)
(Compose f (Compose f f) a)
-> Sem (Stop ei : r1) (Compose f (Compose f f) a)
tac (resource
-> effect (Sem rInitial) a
-> Tactical effect (Sem rInitial) (Stop ei : r1) a
forall (r0 :: [Effect]) x.
resource
-> effect (Sem r0) x -> Tactical effect (Sem r0) (Stop ei : r1) x
scopedHandler resource
resource effect (Sem rInitial) a
effect))
where
tac :: Sem
(Tactics
(Compose f (Compose f f)) (Sem rInitial) (effect : Stop ei : r1)
: Stop ei : r1)
(Compose f (Compose f f) a)
-> Sem (Stop ei : r1) (Compose f (Compose f f) a)
tac =
Compose f (Compose f f) ()
-> (forall x.
Compose f (Compose f f) (Sem rInitial x)
-> Sem (effect : Stop ei : r1) (Compose f (Compose f f) x))
-> (forall x. Compose f (Compose f f) x -> Maybe x)
-> (forall x.
Compose f (Compose f f) (Sem rInitial x)
-> Sem (Stop ei : r1) (Compose f (Compose f f) x))
-> Sem
(Tactics
(Compose f (Compose f f)) (Sem rInitial) (effect : Stop ei : r1)
: Stop ei : r1)
(Compose f (Compose f f) a)
-> Sem (Stop ei : r1) (Compose f (Compose f f) a)
forall (f :: * -> *) (m :: * -> *) (r2 :: [Effect]) (r :: [Effect])
a.
Functor f =>
f ()
-> (forall x. f (m x) -> Sem r2 (f x))
-> (forall x. f x -> Maybe x)
-> (forall x. f (m x) -> Sem r (f x))
-> Sem (Tactics f m r2 : r) a
-> Sem r a
runTactics
(f (Compose f f ()) -> Compose f (Compose f f) ()
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (f (f ()) -> Compose f f ()
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (f ()
s f () -> f () -> f (f ())
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s') Compose f f () -> f () -> f (Compose f f ())
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s''))
(Sem (Stop ei : r1) (Compose f (Compose f f) x)
-> Sem (effect : Stop ei : r1) (Compose f (Compose f f) x)
forall (e :: Effect) (r :: [Effect]) a. Sem r a -> Sem (e : r) a
raise (Sem (Stop ei : r1) (Compose f (Compose f f) x)
-> Sem (effect : Stop ei : r1) (Compose f (Compose f f) x))
-> (Compose f (Compose f f) (Sem rInitial x)
-> Sem (Stop ei : r1) (Compose f (Compose f f) x))
-> Compose f (Compose f f) (Sem rInitial x)
-> Sem (effect : Stop ei : r1) (Compose f (Compose f f) x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sem r1 (Compose f (Compose f f) x)
-> Sem (Stop ei : r1) (Compose f (Compose f f) x)
forall (e :: Effect) (r :: [Effect]) a. Sem r a -> Sem (e : r) a
raise (Sem r1 (Compose f (Compose f f) x)
-> Sem (Stop ei : r1) (Compose f (Compose f f) x))
-> (Compose f (Compose f f) (Sem rInitial x)
-> Sem r1 (Compose f (Compose f f) x))
-> Compose f (Compose f f) (Sem rInitial x)
-> Sem (Stop ei : r1) (Compose f (Compose f f) x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. resource -> InterpreterFor (Scoped param (effect !! ei) !! eo) r1
inScope resource
resource (Sem
((Scoped param (effect !! ei) !! eo) : r1)
(Compose f (Compose f f) x)
-> Sem r1 (Compose f (Compose f f) x))
-> (Compose f (Compose f f) (Sem rInitial x)
-> Sem
((Scoped param (effect !! ei) !! eo) : r1)
(Compose f (Compose f f) x))
-> Compose f (Compose f f) (Sem rInitial x)
-> Sem r1 (Compose f (Compose f f) x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f (Compose f f x) -> Compose f (Compose f f) x)
-> Sem
((Scoped param (effect !! ei) !! eo) : r1) (f (Compose f f x))
-> Sem
((Scoped param (effect !! ei) !! eo) : r1)
(Compose f (Compose f f) x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (Compose f f x) -> Compose f (Compose f f) x
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (Sem ((Scoped param (effect !! ei) !! eo) : r1) (f (Compose f f x))
-> Sem
((Scoped param (effect !! ei) !! eo) : r1)
(Compose f (Compose f f) x))
-> (Compose f (Compose f f) (Sem rInitial x)
-> Sem
((Scoped param (effect !! ei) !! eo) : r1) (f (Compose f f x)))
-> Compose f (Compose f f) (Sem rInitial x)
-> Sem
((Scoped param (effect !! ei) !! eo) : r1)
(Compose f (Compose f f) x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f (f (f x)) -> f (Compose f f x))
-> Sem ((Scoped param (effect !! ei) !! eo) : r1) (f (f (f x)))
-> Sem
((Scoped param (effect !! ei) !! eo) : r1) (f (Compose f f x))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((f (f x) -> Compose f f x) -> f (f (f x)) -> f (Compose f f x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (f x) -> Compose f f x
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose) (Sem ((Scoped param (effect !! ei) !! eo) : r1) (f (f (f x)))
-> Sem
((Scoped param (effect !! ei) !! eo) : r1) (f (Compose f f x)))
-> (Compose f (Compose f f) (Sem rInitial x)
-> Sem ((Scoped param (effect !! ei) !! eo) : r1) (f (f (f x))))
-> Compose f (Compose f f) (Sem rInitial x)
-> Sem
((Scoped param (effect !! ei) !! eo) : r1) (f (Compose f f x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Sem rInitial (f (f x)))
-> Sem ((Scoped param (effect !! ei) !! eo) : r1) (f (f (f x)))
forall x.
f (Sem rInitial x)
-> Sem ((Scoped param (effect !! ei) !! eo) : r1) (f x)
dist'' (f (Sem rInitial (f (f x)))
-> Sem ((Scoped param (effect !! ei) !! eo) : r1) (f (f (f x))))
-> (Compose f (Compose f f) (Sem rInitial x)
-> f (Sem rInitial (f (f x))))
-> Compose f (Compose f f) (Sem rInitial x)
-> Sem ((Scoped param (effect !! ei) !! eo) : r1) (f (f (f x)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f (Sem rInitial (f x)) -> Sem r (f (f x)))
-> f (f (Sem rInitial (f x))) -> f (Sem r (f (f x)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (Sem rInitial (f x)) -> Sem r (f (f x))
forall x. f (Sem rInitial x) -> Sem r (f x)
dist' (f (f (Sem rInitial (f x))) -> f (Sem r (f (f x))))
-> (Compose f (Compose f f) (Sem rInitial x)
-> f (f (Sem rInitial (f x))))
-> Compose f (Compose f f) (Sem rInitial x)
-> f (Sem r (f (f x)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Compose f f (Sem rInitial x) -> f (Sem r (f x)))
-> f (Compose f f (Sem rInitial x)) -> f (f (Sem r (f x)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((f (Sem rInitial x) -> Sem r (f x))
-> f (f (Sem rInitial x)) -> f (Sem r (f x))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (Sem rInitial x) -> Sem r (f x)
forall x. f (Sem rInitial x) -> Sem r (f x)
dist (f (f (Sem rInitial x)) -> f (Sem r (f x)))
-> (Compose f f (Sem rInitial x) -> f (f (Sem rInitial x)))
-> Compose f f (Sem rInitial x)
-> f (Sem r (f x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose f f (Sem rInitial x) -> f (f (Sem rInitial x))
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose) (f (Compose f f (Sem rInitial x)) -> f (f (Sem r (f x))))
-> (Compose f (Compose f f) (Sem rInitial x)
-> f (Compose f f (Sem rInitial x)))
-> Compose f (Compose f f) (Sem rInitial x)
-> f (f (Sem r (f x)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose f (Compose f f) (Sem rInitial x)
-> f (Compose f f (Sem rInitial x))
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose)
(f x -> Maybe x
forall x. f x -> Maybe x
ins (f x -> Maybe x)
-> (Compose f (Compose f f) x -> Maybe (f x))
-> Compose f (Compose f f) x
-> Maybe x
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< f (f x) -> Maybe (f x)
forall x. f x -> Maybe x
ins' (f (f x) -> Maybe (f x))
-> (Compose f f x -> f (f x)) -> Compose f f x -> Maybe (f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose f f x -> f (f x)
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose (Compose f f x -> Maybe (f x))
-> (Compose f (Compose f f) x -> Maybe (Compose f f x))
-> Compose f (Compose f f) x
-> Maybe (f x)
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< f (Compose f f x) -> Maybe (Compose f f x)
forall x. f x -> Maybe x
ins'' (f (Compose f f x) -> Maybe (Compose f f x))
-> (Compose f (Compose f f) x -> f (Compose f f x))
-> Compose f (Compose f f) x
-> Maybe (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose f (Compose f f) x -> f (Compose f f x)
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose)
(Sem r1 (Compose f (Compose f f) x)
-> Sem (Stop ei : r1) (Compose f (Compose f f) x)
forall (e :: Effect) (r :: [Effect]) a. Sem r a -> Sem (e : r) a
raise (Sem r1 (Compose f (Compose f f) x)
-> Sem (Stop ei : r1) (Compose f (Compose f f) x))
-> (Compose f (Compose f f) (Sem rInitial x)
-> Sem r1 (Compose f (Compose f f) x))
-> Compose f (Compose f f) (Sem rInitial x)
-> Sem (Stop ei : r1) (Compose f (Compose f f) x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. resource -> InterpreterFor (Scoped param (effect !! ei) !! eo) r1
inScope resource
resource (Sem
((Scoped param (effect !! ei) !! eo) : r1)
(Compose f (Compose f f) x)
-> Sem r1 (Compose f (Compose f f) x))
-> (Compose f (Compose f f) (Sem rInitial x)
-> Sem
((Scoped param (effect !! ei) !! eo) : r1)
(Compose f (Compose f f) x))
-> Compose f (Compose f f) (Sem rInitial x)
-> Sem r1 (Compose f (Compose f f) x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f (Compose f f x) -> Compose f (Compose f f) x)
-> Sem
((Scoped param (effect !! ei) !! eo) : r1) (f (Compose f f x))
-> Sem
((Scoped param (effect !! ei) !! eo) : r1)
(Compose f (Compose f f) x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (Compose f f x) -> Compose f (Compose f f) x
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (Sem ((Scoped param (effect !! ei) !! eo) : r1) (f (Compose f f x))
-> Sem
((Scoped param (effect !! ei) !! eo) : r1)
(Compose f (Compose f f) x))
-> (Compose f (Compose f f) (Sem rInitial x)
-> Sem
((Scoped param (effect !! ei) !! eo) : r1) (f (Compose f f x)))
-> Compose f (Compose f f) (Sem rInitial x)
-> Sem
((Scoped param (effect !! ei) !! eo) : r1)
(Compose f (Compose f f) x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f (f (f x)) -> f (Compose f f x))
-> Sem ((Scoped param (effect !! ei) !! eo) : r1) (f (f (f x)))
-> Sem
((Scoped param (effect !! ei) !! eo) : r1) (f (Compose f f x))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((f (f x) -> Compose f f x) -> f (f (f x)) -> f (Compose f f x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (f x) -> Compose f f x
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose) (Sem ((Scoped param (effect !! ei) !! eo) : r1) (f (f (f x)))
-> Sem
((Scoped param (effect !! ei) !! eo) : r1) (f (Compose f f x)))
-> (Compose f (Compose f f) (Sem rInitial x)
-> Sem ((Scoped param (effect !! ei) !! eo) : r1) (f (f (f x))))
-> Compose f (Compose f f) (Sem rInitial x)
-> Sem
((Scoped param (effect !! ei) !! eo) : r1) (f (Compose f f x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Sem rInitial (f (f x)))
-> Sem ((Scoped param (effect !! ei) !! eo) : r1) (f (f (f x)))
forall x.
f (Sem rInitial x)
-> Sem ((Scoped param (effect !! ei) !! eo) : r1) (f x)
dist'' (f (Sem rInitial (f (f x)))
-> Sem ((Scoped param (effect !! ei) !! eo) : r1) (f (f (f x))))
-> (Compose f (Compose f f) (Sem rInitial x)
-> f (Sem rInitial (f (f x))))
-> Compose f (Compose f f) (Sem rInitial x)
-> Sem ((Scoped param (effect !! ei) !! eo) : r1) (f (f (f x)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f (Sem rInitial (f x)) -> Sem r (f (f x)))
-> f (f (Sem rInitial (f x))) -> f (Sem r (f (f x)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (Sem rInitial (f x)) -> Sem r (f (f x))
forall x. f (Sem rInitial x) -> Sem r (f x)
dist' (f (f (Sem rInitial (f x))) -> f (Sem r (f (f x))))
-> (Compose f (Compose f f) (Sem rInitial x)
-> f (f (Sem rInitial (f x))))
-> Compose f (Compose f f) (Sem rInitial x)
-> f (Sem r (f (f x)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Compose f f (Sem rInitial x) -> f (Sem r (f x)))
-> f (Compose f f (Sem rInitial x)) -> f (f (Sem r (f x)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((f (Sem rInitial x) -> Sem r (f x))
-> f (f (Sem rInitial x)) -> f (Sem r (f x))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (Sem rInitial x) -> Sem r (f x)
forall x. f (Sem rInitial x) -> Sem r (f x)
dist (f (f (Sem rInitial x)) -> f (Sem r (f x)))
-> (Compose f f (Sem rInitial x) -> f (f (Sem rInitial x)))
-> Compose f f (Sem rInitial x)
-> f (Sem r (f x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose f f (Sem rInitial x) -> f (f (Sem rInitial x))
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose) (f (Compose f f (Sem rInitial x)) -> f (f (Sem r (f x))))
-> (Compose f (Compose f f) (Sem rInitial x)
-> f (Compose f f (Sem rInitial x)))
-> Compose f (Compose f f) (Sem rInitial x)
-> f (f (Sem r (f x)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose f (Compose f f) (Sem rInitial x)
-> f (Compose f f (Sem rInitial x))
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose)
exFinal :: Either ei (Compose f (Compose f f) a) -> x
exFinal = \case
Right (Compose f (Compose f f a)
fffa) ->
f a -> x
ex'' (f a -> x) -> f a -> x
forall a b. (a -> b) -> a -> b
$ f (Compose f f a)
fffa f (Compose f f a)
-> (Compose f f a -> Either eo a1) -> f (Either eo a1)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> a1 -> Either eo a1
forall a b. b -> Either a b
Right (a1 -> Either eo a1)
-> (Compose f f a -> a1) -> Compose f f a -> Either eo a1
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \ (Compose f (f a)
ffa) ->
f a -> a1
ex' (a1 -> Either ei a1
forall a b. b -> Either a b
Right (a1 -> Either ei a1) -> (f a -> a1) -> f a -> Either ei a1
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> a1
ex (f a -> Either ei a1) -> f (f a) -> f (Either ei a1)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (f a)
ffa)
Left ei
err ->
f a -> x
ex'' (a1 -> Either eo a1
forall a b. b -> Either a b
Right (f a -> a1
ex' (ei -> Either ei a1
forall a b. a -> Either a b
Left ei
err Either ei a1 -> f () -> f (Either ei a1)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s')) Either eo a1 -> f () -> f (Either eo a1)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s'')
InScope param
param Sem rInitial a
main -> do
let
ma :: Sem
(Tactics (Compose f f) (Sem rInitial) (Any : Any : r1)
: Stop eo : r1)
(Compose f f a)
ma =
Sem (Stop eo : r1) (Compose f f a)
-> Sem
(Tactics (Compose f f) (Sem rInitial) (Any : Any : r1)
: Stop eo : r1)
(Compose f f a)
forall (e :: Effect) (r :: [Effect]) a. Sem r a -> Sem (e : r) a
raise (Sem (Stop eo : r1) (Compose f f a)
-> Sem
(Tactics (Compose f f) (Sem rInitial) (Any : Any : r1)
: Stop eo : r1)
(Compose f f a))
-> Sem (Stop eo : r1) (Compose f f a)
-> Sem
(Tactics (Compose f f) (Sem rInitial) (Any : Any : r1)
: Stop eo : r1)
(Compose f f a)
forall a b. (a -> b) -> a -> b
$ (forall (e :: Effect).
ElemOf e (Stop eo : r) -> ElemOf e (Stop eo : r1))
-> Sem (Stop eo : r) (Compose f f a)
-> Sem (Stop eo : r1) (Compose f f a)
forall (r :: [Effect]) (r' :: [Effect]) a.
(forall (e :: Effect). ElemOf e r -> ElemOf e r')
-> Sem r a -> Sem r' a
restack (SList (Stop eo : extra)
-> ElemOf e (Stop eo : r)
-> ElemOf e (Append (Stop eo : extra) (Stop eo : r))
forall {a} (l :: [a]) (r :: [a]) (e :: a).
SList l -> ElemOf e r -> ElemOf e (Append l r)
extendMembershipLeft (forall (l :: [Effect]). KnownList l => SList l
forall {a} (l :: [a]). KnownList l => SList l
singList @(Stop eo : extra))) (Sem (Stop eo : r) (Compose f f a)
-> Sem (Stop eo : r1) (Compose f f a))
-> Sem (Stop eo : r) (Compose f f a)
-> Sem (Stop eo : r1) (Compose f f a)
forall a b. (a -> b) -> a -> b
$ param
-> (resource -> Sem r1 (Compose f f a))
-> Sem (Stop eo : r) (Compose f f a)
forall x. param -> (resource -> Sem r1 x) -> Sem (Stop eo : r) x
withResource param
param \ resource
resource' ->
f (f a) -> Compose f f a
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (f (f a) -> Compose f f a)
-> Sem r1 (f (f a)) -> Sem r1 (Compose f f a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> resource -> InterpreterFor (Scoped param (effect !! ei) !! eo) r1
inScope resource
resource' (f (Sem rInitial (f a))
-> Sem ((Scoped param (effect !! ei) !! eo) : r1) (f (f a))
forall x.
f (Sem rInitial x)
-> Sem ((Scoped param (effect !! ei) !! eo) : r1) (f x)
dist'' (f (Sem rInitial a) -> Sem r (f a)
forall x. f (Sem rInitial x) -> Sem r (f x)
dist' (Sem rInitial a
main Sem rInitial a -> f () -> f (Sem rInitial a)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s') Sem r (f a) -> f () -> f (Sem r (f a))
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s''))
tac :: Sem (Stop eo : r1) (Compose f f a)
tac =
Compose f f ()
-> (forall x.
Compose f f (Sem rInitial x)
-> Sem (Any : Any : r1) (Compose f f x))
-> (forall x. Compose f f x -> Maybe x)
-> (forall x.
Compose f f (Sem rInitial x) -> Sem (Stop eo : r1) (Compose f f x))
-> Sem
(Tactics (Compose f f) (Sem rInitial) (Any : Any : r1)
: Stop eo : r1)
(Compose f f a)
-> Sem (Stop eo : r1) (Compose f f a)
forall (f :: * -> *) (m :: * -> *) (r2 :: [Effect]) (r :: [Effect])
a.
Functor f =>
f ()
-> (forall x. f (m x) -> Sem r2 (f x))
-> (forall x. f x -> Maybe x)
-> (forall x. f (m x) -> Sem r (f x))
-> Sem (Tactics f m r2 : r) a
-> Sem r a
runTactics
(f (f ()) -> Compose f f ()
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (f ()
s' f () -> f () -> f (f ())
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s''))
(Sem (Any : r1) (Compose f f x)
-> Sem (Any : Any : r1) (Compose f f x)
forall (e :: Effect) (r :: [Effect]) a. Sem r a -> Sem (e : r) a
raise (Sem (Any : r1) (Compose f f x)
-> Sem (Any : Any : r1) (Compose f f x))
-> (Compose f f (Sem rInitial x) -> Sem (Any : r1) (Compose f f x))
-> Compose f f (Sem rInitial x)
-> Sem (Any : Any : r1) (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sem r1 (Compose f f x) -> Sem (Any : r1) (Compose f f x)
forall (e :: Effect) (r :: [Effect]) a. Sem r a -> Sem (e : r) a
raise (Sem r1 (Compose f f x) -> Sem (Any : r1) (Compose f f x))
-> (Compose f f (Sem rInitial x) -> Sem r1 (Compose f f x))
-> Compose f f (Sem rInitial x)
-> Sem (Any : r1) (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. resource -> InterpreterFor (Scoped param (effect !! ei) !! eo) r1
inScope resource
resource (Sem ((Scoped param (effect !! ei) !! eo) : r1) (Compose f f x)
-> Sem r1 (Compose f f x))
-> (Compose f f (Sem rInitial x)
-> Sem ((Scoped param (effect !! ei) !! eo) : r1) (Compose f f x))
-> Compose f f (Sem rInitial x)
-> Sem r1 (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f (f x) -> Compose f f x)
-> Sem ((Scoped param (effect !! ei) !! eo) : r1) (f (f x))
-> Sem ((Scoped param (effect !! ei) !! eo) : r1) (Compose f f x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (f x) -> Compose f f x
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (Sem ((Scoped param (effect !! ei) !! eo) : r1) (f (f x))
-> Sem ((Scoped param (effect !! ei) !! eo) : r1) (Compose f f x))
-> (Compose f f (Sem rInitial x)
-> Sem ((Scoped param (effect !! ei) !! eo) : r1) (f (f x)))
-> Compose f f (Sem rInitial x)
-> Sem ((Scoped param (effect !! ei) !! eo) : r1) (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Sem rInitial (f x))
-> Sem ((Scoped param (effect !! ei) !! eo) : r1) (f (f x))
forall x.
f (Sem rInitial x)
-> Sem ((Scoped param (effect !! ei) !! eo) : r1) (f x)
dist'' (f (Sem rInitial (f x))
-> Sem ((Scoped param (effect !! ei) !! eo) : r1) (f (f x)))
-> (Compose f f (Sem rInitial x) -> f (Sem rInitial (f x)))
-> Compose f f (Sem rInitial x)
-> Sem ((Scoped param (effect !! ei) !! eo) : r1) (f (f x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f (Sem rInitial x) -> Sem r (f x))
-> f (f (Sem rInitial x)) -> f (Sem r (f x))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (Sem rInitial x) -> Sem r (f x)
forall x. f (Sem rInitial x) -> Sem r (f x)
dist' (f (f (Sem rInitial x)) -> f (Sem r (f x)))
-> (Compose f f (Sem rInitial x) -> f (f (Sem rInitial x)))
-> Compose f f (Sem rInitial x)
-> f (Sem r (f x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose f f (Sem rInitial x) -> f (f (Sem rInitial x))
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose)
(f x -> Maybe x
forall x. f x -> Maybe x
ins' (f x -> Maybe x)
-> (Compose f f x -> Maybe (f x)) -> Compose f f x -> Maybe x
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< f (f x) -> Maybe (f x)
forall x. f x -> Maybe x
ins'' (f (f x) -> Maybe (f x))
-> (Compose f f x -> f (f x)) -> Compose f f x -> Maybe (f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose f f x -> f (f x)
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose)
(Sem r1 (Compose f f x) -> Sem (Stop eo : r1) (Compose f f x)
forall (e :: Effect) (r :: [Effect]) a. Sem r a -> Sem (e : r) a
raise (Sem r1 (Compose f f x) -> Sem (Stop eo : r1) (Compose f f x))
-> (Compose f f (Sem rInitial x) -> Sem r1 (Compose f f x))
-> Compose f f (Sem rInitial x)
-> Sem (Stop eo : r1) (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. resource -> InterpreterFor (Scoped param (effect !! ei) !! eo) r1
inScope resource
resource (Sem ((Scoped param (effect !! ei) !! eo) : r1) (Compose f f x)
-> Sem r1 (Compose f f x))
-> (Compose f f (Sem rInitial x)
-> Sem ((Scoped param (effect !! ei) !! eo) : r1) (Compose f f x))
-> Compose f f (Sem rInitial x)
-> Sem r1 (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f (f x) -> Compose f f x)
-> Sem ((Scoped param (effect !! ei) !! eo) : r1) (f (f x))
-> Sem ((Scoped param (effect !! ei) !! eo) : r1) (Compose f f x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (f x) -> Compose f f x
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (Sem ((Scoped param (effect !! ei) !! eo) : r1) (f (f x))
-> Sem ((Scoped param (effect !! ei) !! eo) : r1) (Compose f f x))
-> (Compose f f (Sem rInitial x)
-> Sem ((Scoped param (effect !! ei) !! eo) : r1) (f (f x)))
-> Compose f f (Sem rInitial x)
-> Sem ((Scoped param (effect !! ei) !! eo) : r1) (Compose f f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Sem rInitial (f x))
-> Sem ((Scoped param (effect !! ei) !! eo) : r1) (f (f x))
forall x.
f (Sem rInitial x)
-> Sem ((Scoped param (effect !! ei) !! eo) : r1) (f x)
dist'' (f (Sem rInitial (f x))
-> Sem ((Scoped param (effect !! ei) !! eo) : r1) (f (f x)))
-> (Compose f f (Sem rInitial x) -> f (Sem rInitial (f x)))
-> Compose f f (Sem rInitial x)
-> Sem ((Scoped param (effect !! ei) !! eo) : r1) (f (f x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f (Sem rInitial x) -> Sem r (f x))
-> f (f (Sem rInitial x)) -> f (Sem r (f x))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (Sem rInitial x) -> Sem r (f x)
forall x. f (Sem rInitial x) -> Sem r (f x)
dist' (f (f (Sem rInitial x)) -> f (Sem r (f x)))
-> (Compose f f (Sem rInitial x) -> f (f (Sem rInitial x)))
-> Compose f f (Sem rInitial x)
-> f (Sem r (f x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose f f (Sem rInitial x) -> f (f (Sem rInitial x))
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose)
Sem
(Tactics (Compose f f) (Sem rInitial) (Any : Any : r1)
: Stop eo : r1)
(Compose f f a)
ma
exFinal :: Either eo (Compose f f a) -> x
exFinal = f a -> x
ex'' (f a -> x)
-> (Either eo (Compose f f a) -> f a)
-> Either eo (Compose f f a)
-> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
Right (Compose f (f a)
a) -> a1 -> Either eo a1
forall a b. b -> Either a b
Right (a1 -> Either eo a1) -> (f a -> a1) -> f a -> Either eo a1
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> a1
ex' (f a -> Either eo a1) -> f (f a) -> f (Either eo a1)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (f a)
a
Left eo
err -> eo -> Either eo a1
forall a b. a -> Either a b
Left eo
err Either eo a1 -> f () -> f (Either eo a1)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
s''
Either eo (Compose f f a) -> x
exFinal (Either eo (Compose f f a) -> x)
-> Sem r1 (Either eo (Compose f f a)) -> Sem r1 x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sem (Stop eo : r1) (Compose f f a)
-> Sem r1 (Either eo (Compose f f a))
forall e (r :: [Effect]) a.
Sem (Stop e : r) a -> Sem r (Either e a)
runStop Sem (Stop eo : r1) (Compose f f a)
tac
interpretScopedRWith ::
∀ extra param resource effect eo ei r r1 .
r1 ~ (extra ++ Stop eo : r) =>
r1 ~ ((extra ++ '[Stop eo]) ++ r) =>
KnownList extra =>
KnownList (extra ++ '[Stop eo]) =>
(∀ x . param -> (resource -> Sem r1 x) -> Sem (Stop eo : r) x) ->
(∀ r0 x . resource -> effect (Sem r0) x -> Sem (Stop ei : r1) x) ->
InterpreterFor (Scoped param (effect !! ei) !! eo) r
interpretScopedRWith :: forall (extra :: [Effect]) param resource (effect :: Effect) eo ei
(r :: [Effect]) (r1 :: [Effect]).
(r1 ~ (extra ++ (Stop eo : r)), r1 ~ ((extra ++ '[Stop eo]) ++ r),
KnownList extra, KnownList (extra ++ '[Stop eo])) =>
(forall x. param -> (resource -> Sem r1 x) -> Sem (Stop eo : r) x)
-> (forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Sem (Stop ei : r1) x)
-> InterpreterFor (Scoped param (effect !! ei) !! eo) r
interpretScopedRWith forall x. param -> (resource -> Sem r1 x) -> Sem (Stop eo : r) x
withResource forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Sem (Stop ei : r1) x
scopedHandler =
forall (extra :: [Effect]) param resource (effect :: Effect) eo ei
(r :: [Effect]) (r1 :: [Effect]).
(r1 ~ (extra ++ (Stop eo : r)), r1 ~ ((extra ++ '[Stop eo]) ++ r),
KnownList extra, KnownList (extra ++ '[Stop eo])) =>
(forall x. param -> (resource -> Sem r1 x) -> Sem (Stop eo : r) x)
-> (forall (r0 :: [Effect]) x.
resource
-> effect (Sem r0) x -> Tactical effect (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 -> Sem (Stop ei : r1) x
-> Sem (WithTactics effect f (Sem r0) (Stop ei : r1)) (f x)
forall (m :: * -> *) (f :: * -> *) (r :: [Effect]) (e :: Effect) a.
Functor f =>
Sem r a -> Sem (WithTactics e f m r) (f a)
liftT (resource -> effect (Sem r0) x -> Sem (Stop ei : r1) x
forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Sem (Stop ei : r1) x
scopedHandler resource
r effect (Sem r0) x
e)
interpretScopedRWith_ ::
∀ extra param effect eo ei r r1 .
r1 ~ (extra ++ Stop eo : r) =>
r1 ~ ((extra ++ '[Stop eo]) ++ r) =>
KnownList extra =>
KnownList (extra ++ '[Stop eo]) =>
(∀ x . param -> Sem r1 x -> Sem (Stop eo : r) x) ->
(∀ r0 x . effect (Sem r0) x -> Sem (Stop ei : r1) x) ->
InterpreterFor (Scoped param (effect !! ei) !! eo) r
interpretScopedRWith_ :: forall (extra :: [Effect]) param (effect :: Effect) eo ei
(r :: [Effect]) (r1 :: [Effect]).
(r1 ~ (extra ++ (Stop eo : r)), r1 ~ ((extra ++ '[Stop eo]) ++ r),
KnownList extra, KnownList (extra ++ '[Stop eo])) =>
(forall x. param -> Sem r1 x -> Sem (Stop eo : r) x)
-> (forall (r0 :: [Effect]) x.
effect (Sem r0) x -> Sem (Stop ei : r1) x)
-> InterpreterFor (Scoped param (effect !! ei) !! eo) r
interpretScopedRWith_ forall x. param -> Sem r1 x -> Sem (Stop eo : r) x
extra forall (r0 :: [Effect]) x.
effect (Sem r0) x -> Sem (Stop ei : r1) x
scopedHandler =
forall (extra :: [Effect]) param resource (effect :: Effect) eo ei
(r :: [Effect]) (r1 :: [Effect]).
(r1 ~ (extra ++ (Stop eo : r)), r1 ~ ((extra ++ '[Stop eo]) ++ r),
KnownList extra, KnownList (extra ++ '[Stop eo])) =>
(forall x. param -> (resource -> Sem r1 x) -> Sem (Stop eo : r) x)
-> (forall (r0 :: [Effect]) x.
resource -> effect (Sem r0) x -> Sem (Stop ei : r1) x)
-> InterpreterFor (Scoped param (effect !! ei) !! eo) r
interpretScopedRWith @extra (\ param
p () -> Sem r1 x
f -> param -> Sem r1 x -> Sem (Stop eo : r) x
forall x. param -> Sem r1 x -> Sem (Stop eo : r) x
extra param
p (() -> Sem r1 x
f ())) ((effect (Sem r0) x -> Sem (Stop ei : r1) x)
-> () -> effect (Sem r0) x -> Sem (Stop ei : r1) x
forall a b. a -> b -> a
const effect (Sem r0) x -> Sem (Stop ei : r1) x
forall (r0 :: [Effect]) x.
effect (Sem r0) x -> Sem (Stop ei : r1) x
scopedHandler)