{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
module Data.Extensible.Effect (
Instruction(..)
, Eff
, liftEff
, liftsEff
, hoistEff
, castEff
, Interpreter(..)
, handleEff
, peelEff
, Rebinder
, rebindEff0
, peelEff0
, rebindEff1
, peelEff1
, rebindEff2
, leaveEff
, retractEff
, Action(..)
, Function
, runAction
, (@!?)
, peelAction
, peelAction0
, ReaderEff
, askEff
, asksEff
, localEff
, runReaderEff
, State
, getEff
, getsEff
, putEff
, modifyEff
, stateEff
, runStateEff
, execStateEff
, evalStateEff
, WriterEff
, writerEff
, tellEff
, listenEff
, passEff
, runWriterEff
, execWriterEff
, MaybeEff
, nothingEff
, runMaybeEff
, EitherEff
, throwEff
, catchEff
, runEitherEff
, mapLeftEff
, Identity
, tickEff
, runIterEff
, ContT
, contEff
, runContEff
, callCCEff
) where
import Control.Applicative
import Data.Bifunctor (first)
import Control.Monad.Skeleton
import Control.Monad.Trans.State.Strict
import Control.Monad.Trans.Cont (ContT(..))
import Data.Extensible.Field
import Data.Extensible.Inclusion
import Data.Extensible.Internal.Rig
import Data.Extensible.Product
import Data.Extensible.Class
import Data.Kind (Type)
import Data.Functor.Identity
import Data.Type.Equality
import Type.Membership
data Instruction (xs :: [Assoc k (Type -> Type)]) a where
Instruction :: !(Membership xs kv) -> TargetOf kv a -> Instruction xs a
type Eff xs = Skeleton (Instruction xs)
liftEff :: forall s t xs a. Lookup xs s t => Proxy s -> t a -> Eff xs a
liftEff :: Proxy s -> t a -> Eff xs a
liftEff Proxy s
p t a
x = Proxy s -> t a -> (a -> a) -> Eff xs a
forall k (s :: k) (t :: * -> *) (xs :: [Assoc k (* -> *)]) a r.
Lookup xs s t =>
Proxy s -> t a -> (a -> r) -> Eff xs r
liftsEff Proxy s
p t a
x a -> a
forall a. a -> a
id
{-# INLINE liftEff #-}
liftsEff :: forall s t xs a r. Lookup xs s t
=> Proxy s -> t a -> (a -> r) -> Eff xs r
liftsEff :: Proxy s -> t a -> (a -> r) -> Eff xs r
liftsEff Proxy s
_ t a
x a -> r
k = MonadView (Instruction xs) (Skeleton (Instruction xs)) r
-> Eff xs r
forall (t :: * -> *) a. MonadView t (Skeleton t) a -> Skeleton t a
boned
(MonadView (Instruction xs) (Skeleton (Instruction xs)) r
-> Eff xs r)
-> MonadView (Instruction xs) (Skeleton (Instruction xs)) r
-> Eff xs r
forall a b. (a -> b) -> a -> b
$ Membership xs (s ':> t) -> TargetOf (s ':> t) a -> Instruction xs a
forall k (xs :: [Assoc k (* -> *)]) (kv :: Assoc k (* -> *)) a.
Membership xs kv -> TargetOf kv a -> Instruction xs a
Instruction (Membership xs (s ':> t)
forall k k1 (xs :: [Assoc k k1]) (k2 :: k) (v :: k1).
Lookup xs k2 v =>
Membership xs (k2 ':> v)
association :: Membership xs (s ':> t)) t a
TargetOf (s ':> t) a
x Instruction xs a
-> (a -> Eff xs r)
-> MonadView (Instruction xs) (Skeleton (Instruction xs)) r
forall (t :: * -> *) a (m :: * -> *) x.
t a -> (a -> m x) -> MonadView t m x
:>>= r -> Eff xs r
forall (m :: * -> *) a. Monad m => a -> m a
return (r -> Eff xs r) -> (a -> r) -> a -> Eff xs r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> r
k
{-# INLINE liftsEff #-}
hoistEff :: forall s t xs a. Lookup xs s t => Proxy s -> (forall x. t x -> t x) -> Eff xs a -> Eff xs a
hoistEff :: Proxy s -> (forall x. t x -> t x) -> Eff xs a -> Eff xs a
hoistEff Proxy s
_ forall x. t x -> t x
f = (forall x. Instruction xs x -> Instruction xs x)
-> Eff xs a -> Eff xs a
forall (s :: * -> *) (t :: * -> *) a.
(forall x. s x -> t x) -> Skeleton s a -> Skeleton t a
hoistSkeleton ((forall x. Instruction xs x -> Instruction xs x)
-> Eff xs a -> Eff xs a)
-> (forall x. Instruction xs x -> Instruction xs x)
-> Eff xs a
-> Eff xs a
forall a b. (a -> b) -> a -> b
$ \(Instruction i t) -> case Membership xs (s ':> t)
-> Membership xs kv -> Either Ordering ((s ':> t) :~: kv)
forall k (xs :: [k]) (x :: k) (y :: k).
Membership xs x -> Membership xs y -> Either Ordering (x :~: y)
compareMembership (Membership xs (s ':> t)
forall k k1 (xs :: [Assoc k k1]) (k2 :: k) (v :: k1).
Lookup xs k2 v =>
Membership xs (k2 ':> v)
association :: Membership xs (s ':> t)) Membership xs kv
i of
Right (s ':> t) :~: kv
Refl -> Membership xs kv -> TargetOf kv x -> Instruction xs x
forall k (xs :: [Assoc k (* -> *)]) (kv :: Assoc k (* -> *)) a.
Membership xs kv -> TargetOf kv a -> Instruction xs a
Instruction Membership xs kv
i (t x -> t x
forall x. t x -> t x
f t x
TargetOf kv x
t)
Either Ordering ((s ':> t) :~: kv)
_ -> Membership xs kv -> TargetOf kv x -> Instruction xs x
forall k (xs :: [Assoc k (* -> *)]) (kv :: Assoc k (* -> *)) a.
Membership xs kv -> TargetOf kv a -> Instruction xs a
Instruction Membership xs kv
i TargetOf kv x
t
{-# INLINABLE hoistEff #-}
castEff :: IncludeAssoc ys xs => Eff xs a -> Eff ys a
castEff :: Eff xs a -> Eff ys a
castEff = (forall x. Instruction xs x -> Instruction ys x)
-> Eff xs a -> Eff ys a
forall (s :: * -> *) (t :: * -> *) a.
(forall x. s x -> t x) -> Skeleton s a -> Skeleton t a
hoistSkeleton
((forall x. Instruction xs x -> Instruction ys x)
-> Eff xs a -> Eff ys a)
-> (forall x. Instruction xs x -> Instruction ys x)
-> Eff xs a
-> Eff ys a
forall a b. (a -> b) -> a -> b
$ \(Instruction i t) -> Membership ys kv -> TargetOf kv x -> Instruction ys x
forall k (xs :: [Assoc k (* -> *)]) (kv :: Assoc k (* -> *)) a.
Membership xs kv -> TargetOf kv a -> Instruction xs a
Instruction (Membership xs kv -> (xs :& Membership ys) -> Membership ys kv
forall k (xs :: [k]) (x :: k) (h :: k -> *).
Membership xs x -> (xs :& h) -> h x
hlookup Membership xs kv
i xs :& Membership ys
forall k v (xs :: [Assoc k v]) (ys :: [Assoc k v]).
IncludeAssoc ys xs =>
xs :& Membership ys
inclusionAssoc) TargetOf kv x
t
peelEff :: forall k t xs a r
. Rebinder xs r
-> (a -> r)
-> (forall x. t x -> (x -> r) -> r)
-> Eff (k >: t ': xs) a -> r
peelEff :: Rebinder xs r
-> (a -> r)
-> (forall x. t x -> (x -> r) -> r)
-> Eff ((k >: t) : xs) a
-> r
peelEff Rebinder xs r
pass a -> r
ret forall x. t x -> (x -> r) -> r
wrap = Eff ((k >: t) : xs) a -> r
go where
go :: Eff ((k >: t) : xs) a -> r
go Eff ((k >: t) : xs) a
m = case Eff ((k >: t) : xs) a
-> MonadView
(Instruction ((k >: t) : xs))
(Skeleton (Instruction ((k >: t) : xs)))
a
forall (t :: * -> *) a. Skeleton t a -> MonadView t (Skeleton t) a
debone Eff ((k >: t) : xs) a
m of
Return a
a -> a -> r
ret a
a
Instruction i t :>>= a -> Eff ((k >: t) : xs) a
k -> Membership ((k >: t) : xs) kv
-> ((kv :~: (k >: t)) -> r) -> (Membership xs kv -> r) -> r
forall k (y :: k) (xs :: [k]) (x :: k) r.
Membership (y : xs) x
-> ((x :~: y) -> r) -> (Membership xs x -> r) -> r
testMembership Membership ((k >: t) : xs) kv
i
(\kv :~: (k >: t)
Refl -> t a -> (a -> r) -> r
forall x. t x -> (x -> r) -> r
wrap t a
TargetOf kv a
t (Eff ((k >: t) : xs) a -> r
go (Eff ((k >: t) : xs) a -> r)
-> (a -> Eff ((k >: t) : xs) a) -> a -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Eff ((k >: t) : xs) a
k))
(\Membership xs kv
j -> Instruction xs a -> (a -> r) -> r
Rebinder xs r
pass (Membership xs kv -> TargetOf kv a -> Instruction xs a
forall k (xs :: [Assoc k (* -> *)]) (kv :: Assoc k (* -> *)) a.
Membership xs kv -> TargetOf kv a -> Instruction xs a
Instruction Membership xs kv
j TargetOf kv a
t) (Eff ((k >: t) : xs) a -> r
go (Eff ((k >: t) : xs) a -> r)
-> (a -> Eff ((k >: t) : xs) a) -> a -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Eff ((k >: t) : xs) a
k))
{-# INLINE peelEff #-}
peelEff0 :: forall k t xs a r. (a -> Eff xs r)
-> (forall x. t x -> (x -> Eff xs r) -> Eff xs r)
-> Eff (k >: t ': xs) a -> Eff xs r
peelEff0 :: (a -> Eff xs r)
-> (forall x. t x -> (x -> Eff xs r) -> Eff xs r)
-> Eff ((k >: t) : xs) a
-> Eff xs r
peelEff0 = Rebinder xs (Eff xs r)
-> (a -> Eff xs r)
-> (forall x. t x -> (x -> Eff xs r) -> Eff xs r)
-> Eff ((k >: t) : xs) a
-> Eff xs r
forall k (k :: k) (t :: * -> *) (xs :: [Assoc k (* -> *)]) a r.
Rebinder xs r
-> (a -> r)
-> (forall x. t x -> (x -> r) -> r)
-> Eff ((k >: t) : xs) a
-> r
peelEff Rebinder xs (Eff xs r)
forall k (xs :: [Assoc k (* -> *)]) r. Rebinder xs (Eff xs r)
rebindEff0
{-# INLINE peelEff0 #-}
peelEff1 :: forall k t xs a b r. (a -> b -> Eff xs r)
-> (forall x. t x -> (x -> b -> Eff xs r) -> b -> Eff xs r)
-> Eff (k >: t ': xs) a -> b -> Eff xs r
peelEff1 :: (a -> b -> Eff xs r)
-> (forall x. t x -> (x -> b -> Eff xs r) -> b -> Eff xs r)
-> Eff ((k >: t) : xs) a
-> b
-> Eff xs r
peelEff1 = Rebinder xs (b -> Eff xs r)
-> (a -> b -> Eff xs r)
-> (forall x. t x -> (x -> b -> Eff xs r) -> b -> Eff xs r)
-> Eff ((k >: t) : xs) a
-> b
-> Eff xs r
forall k (k :: k) (t :: * -> *) (xs :: [Assoc k (* -> *)]) a r.
Rebinder xs r
-> (a -> r)
-> (forall x. t x -> (x -> r) -> r)
-> Eff ((k >: t) : xs) a
-> r
peelEff Rebinder xs (b -> Eff xs r)
forall k (xs :: [Assoc k (* -> *)]) a r.
Rebinder xs (a -> Eff xs r)
rebindEff1
{-# INLINE peelEff1 #-}
type Rebinder xs r = forall x. Instruction xs x -> (x -> r) -> r
rebindEff0 :: Rebinder xs (Eff xs r)
rebindEff0 :: Instruction xs x -> (x -> Eff xs r) -> Eff xs r
rebindEff0 Instruction xs x
i x -> Eff xs r
k = MonadView (Instruction xs) (Skeleton (Instruction xs)) r
-> Eff xs r
forall (t :: * -> *) a. MonadView t (Skeleton t) a -> Skeleton t a
boned (MonadView (Instruction xs) (Skeleton (Instruction xs)) r
-> Eff xs r)
-> MonadView (Instruction xs) (Skeleton (Instruction xs)) r
-> Eff xs r
forall a b. (a -> b) -> a -> b
$ Instruction xs x
i Instruction xs x
-> (x -> Eff xs r)
-> MonadView (Instruction xs) (Skeleton (Instruction xs)) r
forall (t :: * -> *) a (m :: * -> *) x.
t a -> (a -> m x) -> MonadView t m x
:>>= x -> Eff xs r
k
rebindEff1 :: Rebinder xs (a -> Eff xs r)
rebindEff1 :: Instruction xs x -> (x -> a -> Eff xs r) -> a -> Eff xs r
rebindEff1 Instruction xs x
i x -> a -> Eff xs r
k a
a = MonadView (Instruction xs) (Skeleton (Instruction xs)) r
-> Eff xs r
forall (t :: * -> *) a. MonadView t (Skeleton t) a -> Skeleton t a
boned (MonadView (Instruction xs) (Skeleton (Instruction xs)) r
-> Eff xs r)
-> MonadView (Instruction xs) (Skeleton (Instruction xs)) r
-> Eff xs r
forall a b. (a -> b) -> a -> b
$ Instruction xs x
i Instruction xs x
-> (x -> Eff xs r)
-> MonadView (Instruction xs) (Skeleton (Instruction xs)) r
forall (t :: * -> *) a (m :: * -> *) x.
t a -> (a -> m x) -> MonadView t m x
:>>= (x -> a -> Eff xs r) -> a -> x -> Eff xs r
forall a b c. (a -> b -> c) -> b -> a -> c
flip x -> a -> Eff xs r
k a
a
rebindEff2 :: Rebinder xs (a -> b -> Eff xs r)
rebindEff2 :: Instruction xs x -> (x -> a -> b -> Eff xs r) -> a -> b -> Eff xs r
rebindEff2 Instruction xs x
i x -> a -> b -> Eff xs r
k a
a b
b = MonadView (Instruction xs) (Skeleton (Instruction xs)) r
-> Eff xs r
forall (t :: * -> *) a. MonadView t (Skeleton t) a -> Skeleton t a
boned (MonadView (Instruction xs) (Skeleton (Instruction xs)) r
-> Eff xs r)
-> MonadView (Instruction xs) (Skeleton (Instruction xs)) r
-> Eff xs r
forall a b. (a -> b) -> a -> b
$ Instruction xs x
i Instruction xs x
-> (x -> Eff xs r)
-> MonadView (Instruction xs) (Skeleton (Instruction xs)) r
forall (t :: * -> *) a (m :: * -> *) x.
t a -> (a -> m x) -> MonadView t m x
:>>= \x
x -> x -> a -> b -> Eff xs r
k x
x a
a b
b
leaveEff :: Eff '[] a -> a
leaveEff :: Eff '[] a -> a
leaveEff Eff '[] a
m = case Eff '[] a
-> MonadView (Instruction '[]) (Skeleton (Instruction '[])) a
forall (t :: * -> *) a. Skeleton t a -> MonadView t (Skeleton t) a
debone Eff '[] a
m of
Return a
a -> a
a
MonadView (Instruction '[]) (Skeleton (Instruction '[])) a
_ -> [Char] -> a
forall a. HasCallStack => [Char] -> a
error [Char]
"Impossible"
retractEff :: forall k m a. Monad m => Eff '[k >: m] a -> m a
retractEff :: Eff '[k >: m] a -> m a
retractEff Eff '[k >: m] a
m = case Eff '[k >: m] a
-> MonadView
(Instruction '[k >: m]) (Skeleton (Instruction '[k >: m])) a
forall (t :: * -> *) a. Skeleton t a -> MonadView t (Skeleton t) a
debone Eff '[k >: m] a
m of
Return a
a -> a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a
Instruction Membership '[k >: m] kv
i TargetOf kv a
t :>>= a -> Eff '[k >: m] a
k -> Membership '[k >: m] kv
-> ((kv :~: (k >: m)) -> m a) -> (Membership '[] kv -> m a) -> m a
forall k (y :: k) (xs :: [k]) (x :: k) r.
Membership (y : xs) x
-> ((x :~: y) -> r) -> (Membership xs x -> r) -> r
testMembership Membership '[k >: m] kv
i
(\kv :~: (k >: m)
Refl -> m a
TargetOf kv a
t m a -> (a -> m a) -> m a
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Eff '[k >: m] a -> m a
forall k (k :: k) (m :: * -> *) a.
Monad m =>
Eff '[k >: m] a -> m a
retractEff (Eff '[k >: m] a -> m a) -> (a -> Eff '[k >: m] a) -> a -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Eff '[k >: m] a
k)
((Membership '[] kv -> m a) -> m a)
-> (Membership '[] kv -> m a) -> m a
forall a b. (a -> b) -> a -> b
$ [Char] -> Membership '[] kv -> m a
forall a. HasCallStack => [Char] -> a
error [Char]
"Impossible"
newtype Interpreter f g = Interpreter { Interpreter f g -> forall (a :: k). g a -> f a
runInterpreter :: forall a. g a -> f a }
handleEff :: RecordOf (Interpreter m) xs -> Eff xs a -> MonadView m (Eff xs) a
handleEff :: RecordOf (Interpreter m) xs -> Eff xs a -> MonadView m (Eff xs) a
handleEff RecordOf (Interpreter m) xs
hs Eff xs a
m = case Eff xs a -> MonadView (Instruction xs) (Eff xs) a
forall (t :: * -> *) a. Skeleton t a -> MonadView t (Skeleton t) a
debone Eff xs a
m of
Instruction Membership xs kv
i TargetOf kv a
t :>>= a -> Eff xs a
k -> Optic'
(->)
(Const (TargetOf kv a -> m a))
(RecordOf (Interpreter m) xs)
(Field (Interpreter m) kv)
-> (Field (Interpreter m) kv -> TargetOf kv a -> m a)
-> RecordOf (Interpreter m) xs
-> TargetOf kv a
-> m a
forall r s a. Optic' (->) (Const r) s a -> (a -> r) -> s -> r
views (Membership xs kv
-> Optic'
(->)
(Const (TargetOf kv a -> m a))
(RecordOf (Interpreter m) xs)
(Field (Interpreter m) kv)
forall k (f :: * -> *) (p :: * -> * -> *)
(t :: [k] -> (k -> *) -> *) (xs :: [k]) (h :: k -> *) (x :: k).
(Extensible f p t, ExtensibleConstr t xs h x) =>
Membership xs x -> Optic' p f (t xs h) (h x)
pieceAt Membership xs kv
i) (\(Field (Interpreter x)) -> TargetOf kv a -> m a
forall a. TargetOf kv a -> m a
x) RecordOf (Interpreter m) xs
hs TargetOf kv a
t m a -> (a -> Eff xs a) -> MonadView m (Eff xs) a
forall (t :: * -> *) a (m :: * -> *) x.
t a -> (a -> m x) -> MonadView t m x
:>>= a -> Eff xs a
k
Return a
a -> a -> MonadView m (Eff xs) a
forall x (t :: * -> *) (m :: * -> *). x -> MonadView t m x
Return a
a
data Action (args :: [Type]) a r where
AResult :: Action '[] a a
AArgument :: x -> Action xs a r -> Action (x ': xs) a r
type family Function args r :: Type where
Function '[] r = r
Function (x ': xs) r = x -> Function xs r
runAction :: Function xs (f a) -> Action xs a r -> f r
runAction :: Function xs (f a) -> Action xs a r -> f r
runAction Function xs (f a)
r Action xs a r
AResult = f r
Function xs (f a)
r
runAction Function xs (f a)
f (AArgument x
x Action xs a r
a) = Function xs (f a) -> Action xs a r -> f r
forall k (xs :: [*]) (f :: k -> *) (a :: k) (r :: k).
Function xs (f a) -> Action xs a r -> f r
runAction (Function xs (f a)
x -> Function xs (f a)
f x
x) Action xs a r
a
(@!?) :: FieldName k -> Function xs (f a) -> Field (Interpreter f) (k ':> Action xs a)
FieldName k
_ @!? :: FieldName k
-> Function xs (f a) -> Field (Interpreter f) (k ':> Action xs a)
@!? Function xs (f a)
f = Interpreter f (TargetOf (k ':> Action xs a))
-> Field (Interpreter f) (k ':> Action xs a)
forall v k (h :: v -> *) (kv :: Assoc k v).
h (TargetOf kv) -> Field h kv
Field (Interpreter f (TargetOf (k ':> Action xs a))
-> Field (Interpreter f) (k ':> Action xs a))
-> Interpreter f (TargetOf (k ':> Action xs a))
-> Field (Interpreter f) (k ':> Action xs a)
forall a b. (a -> b) -> a -> b
$ (forall (a :: k). Action xs a a -> f a)
-> Interpreter f (Action xs a)
forall k (f :: k -> *) (g :: k -> *).
(forall (a :: k). g a -> f a) -> Interpreter f g
Interpreter ((forall (a :: k). Action xs a a -> f a)
-> Interpreter f (Action xs a))
-> (forall (a :: k). Action xs a a -> f a)
-> Interpreter f (Action xs a)
forall a b. (a -> b) -> a -> b
$ Function xs (f a) -> Action xs a a -> f a
forall k (xs :: [*]) (f :: k -> *) (a :: k) (r :: k).
Function xs (f a) -> Action xs a r -> f r
runAction Function xs (f a)
f
infix 1 @!?
peelAction :: forall k ps q xs a r
. (forall x. Instruction xs x -> (x -> r) -> r)
-> (a -> r)
-> Function ps ((q -> r) -> r)
-> Eff (k >: Action ps q ': xs) a -> r
peelAction :: (forall x. Instruction xs x -> (x -> r) -> r)
-> (a -> r)
-> Function ps ((q -> r) -> r)
-> Eff ((k >: Action ps q) : xs) a
-> r
peelAction forall x. Instruction xs x -> (x -> r) -> r
pass a -> r
ret Function ps ((q -> r) -> r)
wrap = Eff ((k >: Action ps q) : xs) a -> r
go where
go :: Eff ((k >: Action ps q) : xs) a -> r
go Eff ((k >: Action ps q) : xs) a
m = case Eff ((k >: Action ps q) : xs) a
-> MonadView
(Instruction ((k >: Action ps q) : xs))
(Skeleton (Instruction ((k >: Action ps q) : xs)))
a
forall (t :: * -> *) a. Skeleton t a -> MonadView t (Skeleton t) a
debone Eff ((k >: Action ps q) : xs) a
m of
Return a
a -> a -> r
ret a
a
Instruction i t :>>= a -> Eff ((k >: Action ps q) : xs) a
k -> Membership ((k >: Action ps q) : xs) kv
-> ((kv :~: (k >: Action ps q)) -> r)
-> (Membership xs kv -> r)
-> r
forall k (y :: k) (xs :: [k]) (x :: k) r.
Membership (y : xs) x
-> ((x :~: y) -> r) -> (Membership xs x -> r) -> r
testMembership Membership ((k >: Action ps q) : xs) kv
i
(\kv :~: (k >: Action ps q)
Refl -> case TargetOf kv a
t of
(_ :: Action ps q x) ->
let run :: forall t. Function t ((q -> r) -> r) -> Action t q x -> r
run :: Function t ((q -> r) -> r) -> Action t q a -> r
run Function t ((q -> r) -> r)
f Action t q a
AResult = Function t ((q -> r) -> r)
(a -> r) -> r
f (Eff ((k >: Action ps q) : xs) a -> r
go (Eff ((k >: Action ps q) : xs) a -> r)
-> (a -> Eff ((k >: Action ps q) : xs) a) -> a -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Eff ((k >: Action ps q) : xs) a
k)
run Function t ((q -> r) -> r)
f (AArgument x
x Action xs q a
a) = Function xs ((q -> r) -> r) -> Action xs q a -> r
forall (t :: [*]). Function t ((q -> r) -> r) -> Action t q a -> r
run (Function t ((q -> r) -> r)
x -> Function xs ((q -> r) -> r)
f x
x) Action xs q a
a
in Function ps ((q -> r) -> r) -> Action ps q a -> r
forall (t :: [*]). Function t ((q -> r) -> r) -> Action t q a -> r
run Function ps ((q -> r) -> r)
wrap TargetOf kv a
Action ps q a
t)
((Membership xs kv -> r) -> r) -> (Membership xs kv -> r) -> r
forall a b. (a -> b) -> a -> b
$ \Membership xs kv
j -> Instruction xs a -> (a -> r) -> r
forall x. Instruction xs x -> (x -> r) -> r
pass (Membership xs kv -> TargetOf kv a -> Instruction xs a
forall k (xs :: [Assoc k (* -> *)]) (kv :: Assoc k (* -> *)) a.
Membership xs kv -> TargetOf kv a -> Instruction xs a
Instruction Membership xs kv
j TargetOf kv a
t) (Eff ((k >: Action ps q) : xs) a -> r
go (Eff ((k >: Action ps q) : xs) a -> r)
-> (a -> Eff ((k >: Action ps q) : xs) a) -> a -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Eff ((k >: Action ps q) : xs) a
k)
{-# INLINE peelAction #-}
peelAction0 :: forall k ps q xs a. Function ps (Eff xs q)
-> Eff (k >: Action ps q ': xs) a -> Eff xs a
peelAction0 :: Function ps (Eff xs q)
-> Eff ((k >: Action ps q) : xs) a -> Eff xs a
peelAction0 Function ps (Eff xs q)
wrap = Eff ((k >: Action ps q) : xs) a -> Eff xs a
go where
go :: Eff ((k >: Action ps q) : xs) a -> Eff xs a
go Eff ((k >: Action ps q) : xs) a
m = case Eff ((k >: Action ps q) : xs) a
-> MonadView
(Instruction ((k >: Action ps q) : xs))
(Skeleton (Instruction ((k >: Action ps q) : xs)))
a
forall (t :: * -> *) a. Skeleton t a -> MonadView t (Skeleton t) a
debone Eff ((k >: Action ps q) : xs) a
m of
Return a
a -> a -> Eff xs a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a
Instruction i t :>>= a -> Eff ((k >: Action ps q) : xs) a
k -> Membership ((k >: Action ps q) : xs) kv
-> ((kv :~: (k >: Action ps q)) -> Eff xs a)
-> (Membership xs kv -> Eff xs a)
-> Eff xs a
forall k (y :: k) (xs :: [k]) (x :: k) r.
Membership (y : xs) x
-> ((x :~: y) -> r) -> (Membership xs x -> r) -> r
testMembership Membership ((k >: Action ps q) : xs) kv
i
(\kv :~: (k >: Action ps q)
Refl -> case TargetOf kv a
t of
(_ :: Action ps q x) ->
let run :: forall t. Function t (Eff xs q) -> Action t q x -> Eff xs a
run :: Function t (Eff xs q) -> Action t q a -> Eff xs a
run Function t (Eff xs q)
f Action t q a
AResult = Skeleton (Instruction xs) a
Function t (Eff xs q)
f Skeleton (Instruction xs) a -> (a -> Eff xs a) -> Eff xs a
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Eff ((k >: Action ps q) : xs) a -> Eff xs a
go (Eff ((k >: Action ps q) : xs) a -> Eff xs a)
-> (a -> Eff ((k >: Action ps q) : xs) a) -> a -> Eff xs a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Eff ((k >: Action ps q) : xs) a
k
run Function t (Eff xs q)
f (AArgument x
x Action xs q a
a) = Function xs (Eff xs q) -> Action xs q a -> Eff xs a
forall (t :: [*]).
Function t (Eff xs q) -> Action t q a -> Eff xs a
run (Function t (Eff xs q)
x -> Function xs (Eff xs q)
f x
x) Action xs q a
a
in Function ps (Eff xs q) -> Action ps q a -> Eff xs a
forall (t :: [*]).
Function t (Eff xs q) -> Action t q a -> Eff xs a
run Function ps (Eff xs q)
wrap TargetOf kv a
Action ps q a
t)
((Membership xs kv -> Eff xs a) -> Eff xs a)
-> (Membership xs kv -> Eff xs a) -> Eff xs a
forall a b. (a -> b) -> a -> b
$ \Membership xs kv
j -> Instruction xs a -> (a -> Eff xs a) -> Eff xs a
forall k (xs :: [Assoc k (* -> *)]) r. Rebinder xs (Eff xs r)
rebindEff0 (Membership xs kv -> TargetOf kv a -> Instruction xs a
forall k (xs :: [Assoc k (* -> *)]) (kv :: Assoc k (* -> *)) a.
Membership xs kv -> TargetOf kv a -> Instruction xs a
Instruction Membership xs kv
j TargetOf kv a
t) (Eff ((k >: Action ps q) : xs) a -> Eff xs a
go (Eff ((k >: Action ps q) : xs) a -> Eff xs a)
-> (a -> Eff ((k >: Action ps q) : xs) a) -> a -> Eff xs a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Eff ((k >: Action ps q) : xs) a
k)
{-# INLINE peelAction0 #-}
type ReaderEff = (:~:)
askEff :: forall k r xs. Lookup xs k (ReaderEff r)
=> Proxy k -> Eff xs r
askEff :: Proxy k -> Eff xs r
askEff Proxy k
p = Proxy k -> (r :~: r) -> Eff xs r
forall k (s :: k) (t :: * -> *) (xs :: [Assoc k (* -> *)]) a.
Lookup xs s t =>
Proxy s -> t a -> Eff xs a
liftEff Proxy k
p r :~: r
forall k (a :: k). a :~: a
Refl
{-# INLINE askEff #-}
asksEff :: forall k r xs a. Lookup xs k (ReaderEff r)
=> Proxy k -> (r -> a) -> Eff xs a
asksEff :: Proxy k -> (r -> a) -> Eff xs a
asksEff Proxy k
p = Proxy k -> (r :~: r) -> (r -> a) -> Eff xs a
forall k (s :: k) (t :: * -> *) (xs :: [Assoc k (* -> *)]) a r.
Lookup xs s t =>
Proxy s -> t a -> (a -> r) -> Eff xs r
liftsEff Proxy k
p r :~: r
forall k (a :: k). a :~: a
Refl
{-# INLINE asksEff #-}
localEff :: forall k r xs a. Lookup xs k (ReaderEff r)
=> Proxy k -> (r -> r) -> Eff xs a -> Eff xs a
localEff :: Proxy k -> (r -> r) -> Eff xs a -> Eff xs a
localEff Proxy k
_ r -> r
f = Eff xs a -> Eff xs a
go where
go :: Eff xs a -> Eff xs a
go Eff xs a
m = case Eff xs a
-> MonadView (Instruction xs) (Skeleton (Instruction xs)) a
forall (t :: * -> *) a. Skeleton t a -> MonadView t (Skeleton t) a
debone Eff xs a
m of
Return a
a -> a -> Eff xs a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a
Instruction i t :>>= a -> Eff xs a
k -> case Membership xs (k >: ReaderEff r)
-> Membership xs kv -> Either Ordering ((k >: ReaderEff r) :~: kv)
forall k (xs :: [k]) (x :: k) (y :: k).
Membership xs x -> Membership xs y -> Either Ordering (x :~: y)
compareMembership
(Membership xs (k >: ReaderEff r)
forall k k1 (xs :: [Assoc k k1]) (k2 :: k) (v :: k1).
Lookup xs k2 v =>
Membership xs (k2 ':> v)
association :: Membership xs (k >: ReaderEff r)) Membership xs kv
i of
Left Ordering
_ -> MonadView (Instruction xs) (Skeleton (Instruction xs)) a
-> Eff xs a
forall (t :: * -> *) a. MonadView t (Skeleton t) a -> Skeleton t a
boned (MonadView (Instruction xs) (Skeleton (Instruction xs)) a
-> Eff xs a)
-> MonadView (Instruction xs) (Skeleton (Instruction xs)) a
-> Eff xs a
forall a b. (a -> b) -> a -> b
$ Membership xs kv -> TargetOf kv a -> Instruction xs a
forall k (xs :: [Assoc k (* -> *)]) (kv :: Assoc k (* -> *)) a.
Membership xs kv -> TargetOf kv a -> Instruction xs a
Instruction Membership xs kv
i TargetOf kv a
t Instruction xs a
-> (a -> Eff xs a)
-> MonadView (Instruction xs) (Skeleton (Instruction xs)) a
forall (t :: * -> *) a (m :: * -> *) x.
t a -> (a -> m x) -> MonadView t m x
:>>= Eff xs a -> Eff xs a
go (Eff xs a -> Eff xs a) -> (a -> Eff xs a) -> a -> Eff xs a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Eff xs a
k
Right (k >: ReaderEff r) :~: kv
Refl -> case TargetOf kv a
t of
TargetOf kv a
Refl -> MonadView (Instruction xs) (Skeleton (Instruction xs)) a
-> Eff xs a
forall (t :: * -> *) a. MonadView t (Skeleton t) a -> Skeleton t a
boned (MonadView (Instruction xs) (Skeleton (Instruction xs)) a
-> Eff xs a)
-> MonadView (Instruction xs) (Skeleton (Instruction xs)) a
-> Eff xs a
forall a b. (a -> b) -> a -> b
$ Membership xs kv -> TargetOf kv r -> Instruction xs r
forall k (xs :: [Assoc k (* -> *)]) (kv :: Assoc k (* -> *)) a.
Membership xs kv -> TargetOf kv a -> Instruction xs a
Instruction Membership xs kv
i TargetOf kv r
TargetOf kv a
t Instruction xs r
-> (r -> Eff xs a)
-> MonadView (Instruction xs) (Skeleton (Instruction xs)) a
forall (t :: * -> *) a (m :: * -> *) x.
t a -> (a -> m x) -> MonadView t m x
:>>= Eff xs a -> Eff xs a
go (Eff xs a -> Eff xs a) -> (r -> Eff xs a) -> r -> Eff xs a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Eff xs a
k (a -> Eff xs a) -> (r -> a) -> r -> Eff xs a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. r -> r
r -> a
f
{-# INLINE localEff #-}
runReaderEff :: forall k r xs a. Eff (k >: ReaderEff r ': xs) a -> r -> Eff xs a
runReaderEff :: Eff ((k >: ReaderEff r) : xs) a -> r -> Eff xs a
runReaderEff Eff ((k >: ReaderEff r) : xs) a
m r
r = (a -> Eff xs a)
-> (forall x. ReaderEff r x -> (x -> Eff xs a) -> Eff xs a)
-> Eff ((k >: ReaderEff r) : xs) a
-> Eff xs a
forall k (k :: k) (t :: * -> *) (xs :: [Assoc k (* -> *)]) a r.
(a -> Eff xs r)
-> (forall x. t x -> (x -> Eff xs r) -> Eff xs r)
-> Eff ((k >: t) : xs) a
-> Eff xs r
peelEff0 a -> Eff xs a
forall (m :: * -> *) a. Monad m => a -> m a
return (\ReaderEff r x
Refl x -> Eff xs a
k -> x -> Eff xs a
k r
x
r) Eff ((k >: ReaderEff r) : xs) a
m
{-# INLINE runReaderEff #-}
getEff :: forall k s xs. Lookup xs k (State s)
=> Proxy k -> Eff xs s
getEff :: Proxy k -> Eff xs s
getEff Proxy k
k = Proxy k -> StateT s Identity s -> Eff xs s
forall k (s :: k) (t :: * -> *) (xs :: [Assoc k (* -> *)]) a.
Lookup xs s t =>
Proxy s -> t a -> Eff xs a
liftEff Proxy k
k StateT s Identity s
forall (m :: * -> *) s. Monad m => StateT s m s
get
{-# INLINE getEff #-}
getsEff :: forall k s a xs. Lookup xs k (State s)
=> Proxy k -> (s -> a) -> Eff xs a
getsEff :: Proxy k -> (s -> a) -> Eff xs a
getsEff Proxy k
k = Proxy k -> StateT s Identity s -> (s -> a) -> Eff xs a
forall k (s :: k) (t :: * -> *) (xs :: [Assoc k (* -> *)]) a r.
Lookup xs s t =>
Proxy s -> t a -> (a -> r) -> Eff xs r
liftsEff Proxy k
k StateT s Identity s
forall (m :: * -> *) s. Monad m => StateT s m s
get
{-# INLINE getsEff #-}
putEff :: forall k s xs. Lookup xs k (State s)
=> Proxy k -> s -> Eff xs ()
putEff :: Proxy k -> s -> Eff xs ()
putEff Proxy k
k = Proxy k -> StateT s Identity () -> Eff xs ()
forall k (s :: k) (t :: * -> *) (xs :: [Assoc k (* -> *)]) a.
Lookup xs s t =>
Proxy s -> t a -> Eff xs a
liftEff Proxy k
k (StateT s Identity () -> Eff xs ())
-> (s -> StateT s Identity ()) -> s -> Eff xs ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. s -> StateT s Identity ()
forall (m :: * -> *) s. Monad m => s -> StateT s m ()
put
{-# INLINE putEff #-}
modifyEff :: forall k s xs. Lookup xs k (State s)
=> Proxy k -> (s -> s) -> Eff xs ()
modifyEff :: Proxy k -> (s -> s) -> Eff xs ()
modifyEff Proxy k
k s -> s
f = Proxy k -> StateT s Identity () -> Eff xs ()
forall k (s :: k) (t :: * -> *) (xs :: [Assoc k (* -> *)]) a.
Lookup xs s t =>
Proxy s -> t a -> Eff xs a
liftEff Proxy k
k (StateT s Identity () -> Eff xs ())
-> StateT s Identity () -> Eff xs ()
forall a b. (a -> b) -> a -> b
$ (s -> ((), s)) -> StateT s Identity ()
forall (m :: * -> *) s a. Monad m => (s -> (a, s)) -> StateT s m a
state ((s -> ((), s)) -> StateT s Identity ())
-> (s -> ((), s)) -> StateT s Identity ()
forall a b. (a -> b) -> a -> b
$ \s
s -> ((), s -> s
f s
s)
{-# INLINE modifyEff #-}
stateEff :: forall k s xs a. Lookup xs k (State s)
=> Proxy k -> (s -> (a, s)) -> Eff xs a
stateEff :: Proxy k -> (s -> (a, s)) -> Eff xs a
stateEff Proxy k
k = Proxy k -> StateT s Identity a -> Eff xs a
forall k (s :: k) (t :: * -> *) (xs :: [Assoc k (* -> *)]) a.
Lookup xs s t =>
Proxy s -> t a -> Eff xs a
liftEff Proxy k
k (StateT s Identity a -> Eff xs a)
-> ((s -> (a, s)) -> StateT s Identity a)
-> (s -> (a, s))
-> Eff xs a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (s -> (a, s)) -> StateT s Identity a
forall (m :: * -> *) s a. Monad m => (s -> (a, s)) -> StateT s m a
state
{-# INLINE stateEff #-}
contState :: State s a -> (a -> s -> r) -> s -> r
contState :: State s a -> (a -> s -> r) -> s -> r
contState State s a
m a -> s -> r
k s
s = let (a
a, s
s') = State s a -> s -> (a, s)
forall s a. State s a -> s -> (a, s)
runState State s a
m s
s in a -> s -> r
k a
a (s -> r) -> s -> r
forall a b. (a -> b) -> a -> b
$! s
s'
runStateEff :: forall k s xs a. Eff (k >: State s ': xs) a -> s -> Eff xs (a, s)
runStateEff :: Eff ((k >: State s) : xs) a -> s -> Eff xs (a, s)
runStateEff = (a -> s -> Eff xs (a, s))
-> (forall x.
State s x -> (x -> s -> Eff xs (a, s)) -> s -> Eff xs (a, s))
-> Eff ((k >: State s) : xs) a
-> s
-> Eff xs (a, s)
forall k (k :: k) (t :: * -> *) (xs :: [Assoc k (* -> *)]) a b r.
(a -> b -> Eff xs r)
-> (forall x. t x -> (x -> b -> Eff xs r) -> b -> Eff xs r)
-> Eff ((k >: t) : xs) a
-> b
-> Eff xs r
peelEff1 (\a
a s
s -> (a, s) -> Eff xs (a, s)
forall (m :: * -> *) a. Monad m => a -> m a
return (a
a, s
s)) forall x.
State s x -> (x -> s -> Eff xs (a, s)) -> s -> Eff xs (a, s)
forall s a r. State s a -> (a -> s -> r) -> s -> r
contState
{-# INLINE runStateEff #-}
execStateEff :: forall k s xs a. Eff (k >: State s ': xs) a -> s -> Eff xs s
execStateEff :: Eff ((k >: State s) : xs) a -> s -> Eff xs s
execStateEff = (a -> s -> Eff xs s)
-> (forall x. State s x -> (x -> s -> Eff xs s) -> s -> Eff xs s)
-> Eff ((k >: State s) : xs) a
-> s
-> Eff xs s
forall k (k :: k) (t :: * -> *) (xs :: [Assoc k (* -> *)]) a b r.
(a -> b -> Eff xs r)
-> (forall x. t x -> (x -> b -> Eff xs r) -> b -> Eff xs r)
-> Eff ((k >: t) : xs) a
-> b
-> Eff xs r
peelEff1 ((s -> Eff xs s) -> a -> s -> Eff xs s
forall a b. a -> b -> a
const s -> Eff xs s
forall (m :: * -> *) a. Monad m => a -> m a
return) forall x. State s x -> (x -> s -> Eff xs s) -> s -> Eff xs s
forall s a r. State s a -> (a -> s -> r) -> s -> r
contState
{-# INLINE execStateEff #-}
evalStateEff :: forall k s xs a. Eff (k >: State s ': xs) a -> s -> Eff xs a
evalStateEff :: Eff ((k >: State s) : xs) a -> s -> Eff xs a
evalStateEff = (a -> s -> Eff xs a)
-> (forall x. State s x -> (x -> s -> Eff xs a) -> s -> Eff xs a)
-> Eff ((k >: State s) : xs) a
-> s
-> Eff xs a
forall k (k :: k) (t :: * -> *) (xs :: [Assoc k (* -> *)]) a b r.
(a -> b -> Eff xs r)
-> (forall x. t x -> (x -> b -> Eff xs r) -> b -> Eff xs r)
-> Eff ((k >: t) : xs) a
-> b
-> Eff xs r
peelEff1 (Eff xs a -> s -> Eff xs a
forall a b. a -> b -> a
const (Eff xs a -> s -> Eff xs a)
-> (a -> Eff xs a) -> a -> s -> Eff xs a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Eff xs a
forall (m :: * -> *) a. Monad m => a -> m a
return) forall x. State s x -> (x -> s -> Eff xs a) -> s -> Eff xs a
forall s a r. State s a -> (a -> s -> r) -> s -> r
contState
{-# INLINE evalStateEff #-}
type WriterEff w = (,) w
writerEff :: forall k w xs a. (Lookup xs k (WriterEff w))
=> Proxy k -> (a, w) -> Eff xs a
writerEff :: Proxy k -> (a, w) -> Eff xs a
writerEff Proxy k
k (a
a, w
w) = Proxy k -> (w, a) -> Eff xs a
forall k (s :: k) (t :: * -> *) (xs :: [Assoc k (* -> *)]) a.
Lookup xs s t =>
Proxy s -> t a -> Eff xs a
liftEff Proxy k
k (w
w, a
a)
{-# INLINE writerEff #-}
tellEff :: forall k w xs. (Lookup xs k (WriterEff w))
=> Proxy k -> w -> Eff xs ()
tellEff :: Proxy k -> w -> Eff xs ()
tellEff Proxy k
k w
w = Proxy k -> (w, ()) -> Eff xs ()
forall k (s :: k) (t :: * -> *) (xs :: [Assoc k (* -> *)]) a.
Lookup xs s t =>
Proxy s -> t a -> Eff xs a
liftEff Proxy k
k (w
w, ())
{-# INLINE tellEff #-}
listenEff :: forall k w xs a. (Lookup xs k (WriterEff w), Monoid w)
=> Proxy k -> Eff xs a -> Eff xs (a, w)
listenEff :: Proxy k -> Eff xs a -> Eff xs (a, w)
listenEff Proxy k
p = w -> Eff xs a -> Eff xs (a, w)
go w
forall a. Monoid a => a
mempty where
go :: w -> Eff xs a -> Eff xs (a, w)
go w
w Eff xs a
m = case Eff xs a
-> MonadView (Instruction xs) (Skeleton (Instruction xs)) a
forall (t :: * -> *) a. Skeleton t a -> MonadView t (Skeleton t) a
debone Eff xs a
m of
Return a
a -> Proxy k -> ((a, w), w) -> Eff xs (a, w)
forall k (k :: k) w (xs :: [Assoc k (* -> *)]) a.
Lookup xs k (WriterEff w) =>
Proxy k -> (a, w) -> Eff xs a
writerEff Proxy k
p ((a
a, w
w), w
w)
Instruction i t :>>= a -> Eff xs a
k -> case Membership xs (k ':> (,) w)
-> Membership xs kv -> Either Ordering ((k ':> (,) w) :~: kv)
forall k (xs :: [k]) (x :: k) (y :: k).
Membership xs x -> Membership xs y -> Either Ordering (x :~: y)
compareMembership (Membership xs (k ':> (,) w)
forall k k1 (xs :: [Assoc k k1]) (k2 :: k) (v :: k1).
Lookup xs k2 v =>
Membership xs (k2 ':> v)
association :: Membership xs (k ':> (,) w)) Membership xs kv
i of
Left Ordering
_ -> MonadView (Instruction xs) (Skeleton (Instruction xs)) (a, w)
-> Eff xs (a, w)
forall (t :: * -> *) a. MonadView t (Skeleton t) a -> Skeleton t a
boned (MonadView (Instruction xs) (Skeleton (Instruction xs)) (a, w)
-> Eff xs (a, w))
-> MonadView (Instruction xs) (Skeleton (Instruction xs)) (a, w)
-> Eff xs (a, w)
forall a b. (a -> b) -> a -> b
$ Membership xs kv -> TargetOf kv a -> Instruction xs a
forall k (xs :: [Assoc k (* -> *)]) (kv :: Assoc k (* -> *)) a.
Membership xs kv -> TargetOf kv a -> Instruction xs a
Instruction Membership xs kv
i TargetOf kv a
t Instruction xs a
-> (a -> Eff xs (a, w))
-> MonadView (Instruction xs) (Skeleton (Instruction xs)) (a, w)
forall (t :: * -> *) a (m :: * -> *) x.
t a -> (a -> m x) -> MonadView t m x
:>>= w -> Eff xs a -> Eff xs (a, w)
go w
w (Eff xs a -> Eff xs (a, w))
-> (a -> Eff xs a) -> a -> Eff xs (a, w)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Eff xs a
k
Right (k ':> (,) w) :~: kv
Refl -> let (w
w', a
a) = (w, a)
TargetOf kv a
t
!w'' :: w
w'' = w -> w -> w
forall a. Monoid a => a -> a -> a
mappend w
w w
w' in w -> Eff xs a -> Eff xs (a, w)
go w
w'' (a -> Eff xs a
k a
a)
{-# INLINE listenEff #-}
passEff :: forall k w xs a. (Lookup xs k (WriterEff w), Monoid w)
=> Proxy k -> Eff xs (a, w -> w) -> Eff xs a
passEff :: Proxy k -> Eff xs (a, w -> w) -> Eff xs a
passEff Proxy k
p = w -> Eff xs (a, w -> w) -> Eff xs a
go w
forall a. Monoid a => a
mempty where
go :: w -> Eff xs (a, w -> w) -> Eff xs a
go w
w Eff xs (a, w -> w)
m = case Eff xs (a, w -> w)
-> MonadView
(Instruction xs) (Skeleton (Instruction xs)) (a, w -> w)
forall (t :: * -> *) a. Skeleton t a -> MonadView t (Skeleton t) a
debone Eff xs (a, w -> w)
m of
Return (a
a, w -> w
f) -> Proxy k -> (a, w) -> Eff xs a
forall k (k :: k) w (xs :: [Assoc k (* -> *)]) a.
Lookup xs k (WriterEff w) =>
Proxy k -> (a, w) -> Eff xs a
writerEff Proxy k
p (a
a, w -> w
f w
w)
Instruction i t :>>= a -> Eff xs (a, w -> w)
k -> case Membership xs (k ':> (,) w)
-> Membership xs kv -> Either Ordering ((k ':> (,) w) :~: kv)
forall k (xs :: [k]) (x :: k) (y :: k).
Membership xs x -> Membership xs y -> Either Ordering (x :~: y)
compareMembership (Membership xs (k ':> (,) w)
forall k k1 (xs :: [Assoc k k1]) (k2 :: k) (v :: k1).
Lookup xs k2 v =>
Membership xs (k2 ':> v)
association :: Membership xs (k ':> (,) w)) Membership xs kv
i of
Left Ordering
_ -> MonadView (Instruction xs) (Skeleton (Instruction xs)) a
-> Eff xs a
forall (t :: * -> *) a. MonadView t (Skeleton t) a -> Skeleton t a
boned (MonadView (Instruction xs) (Skeleton (Instruction xs)) a
-> Eff xs a)
-> MonadView (Instruction xs) (Skeleton (Instruction xs)) a
-> Eff xs a
forall a b. (a -> b) -> a -> b
$ Membership xs kv -> TargetOf kv a -> Instruction xs a
forall k (xs :: [Assoc k (* -> *)]) (kv :: Assoc k (* -> *)) a.
Membership xs kv -> TargetOf kv a -> Instruction xs a
Instruction Membership xs kv
i TargetOf kv a
t Instruction xs a
-> (a -> Eff xs a)
-> MonadView (Instruction xs) (Skeleton (Instruction xs)) a
forall (t :: * -> *) a (m :: * -> *) x.
t a -> (a -> m x) -> MonadView t m x
:>>= w -> Eff xs (a, w -> w) -> Eff xs a
go w
w (Eff xs (a, w -> w) -> Eff xs a)
-> (a -> Eff xs (a, w -> w)) -> a -> Eff xs a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Eff xs (a, w -> w)
k
Right (k ':> (,) w) :~: kv
Refl -> let (w
w', a
a) = (w, a)
TargetOf kv a
t
!w'' :: w
w'' = w -> w -> w
forall a. Monoid a => a -> a -> a
mappend w
w w
w' in w -> Eff xs (a, w -> w) -> Eff xs a
go w
w'' (a -> Eff xs (a, w -> w)
k a
a)
{-# INLINE passEff #-}
contWriter :: Monoid w => (w, a) -> (a -> w -> r) -> w -> r
contWriter :: (w, a) -> (a -> w -> r) -> w -> r
contWriter (w
w', a
a) a -> w -> r
k w
w = a -> w -> r
k a
a (w -> r) -> w -> r
forall a b. (a -> b) -> a -> b
$! w -> w -> w
forall a. Monoid a => a -> a -> a
mappend w
w w
w'
runWriterEff :: forall k w xs a. Monoid w => Eff (k >: WriterEff w ': xs) a -> Eff xs (a, w)
runWriterEff :: Eff ((k >: WriterEff w) : xs) a -> Eff xs (a, w)
runWriterEff = (a -> w -> Eff xs (a, w))
-> (forall x.
WriterEff w x -> (x -> w -> Eff xs (a, w)) -> w -> Eff xs (a, w))
-> Eff ((k >: WriterEff w) : xs) a
-> w
-> Eff xs (a, w)
forall k (k :: k) (t :: * -> *) (xs :: [Assoc k (* -> *)]) a b r.
(a -> b -> Eff xs r)
-> (forall x. t x -> (x -> b -> Eff xs r) -> b -> Eff xs r)
-> Eff ((k >: t) : xs) a
-> b
-> Eff xs r
peelEff1 (\a
a w
w -> (a, w) -> Eff xs (a, w)
forall (m :: * -> *) a. Monad m => a -> m a
return (a
a, w
w)) forall x.
WriterEff w x -> (x -> w -> Eff xs (a, w)) -> w -> Eff xs (a, w)
forall w a r. Monoid w => (w, a) -> (a -> w -> r) -> w -> r
contWriter (Eff ((k >: WriterEff w) : xs) a -> w -> Eff xs (a, w))
-> w -> Eff ((k >: WriterEff w) : xs) a -> Eff xs (a, w)
forall a b c. (a -> b -> c) -> b -> a -> c
`flip` w
forall a. Monoid a => a
mempty
{-# INLINE runWriterEff #-}
execWriterEff :: forall k w xs a. Monoid w => Eff (k >: WriterEff w ': xs) a -> Eff xs w
execWriterEff :: Eff ((k >: WriterEff w) : xs) a -> Eff xs w
execWriterEff = (a -> w -> Eff xs w)
-> (forall x.
WriterEff w x -> (x -> w -> Eff xs w) -> w -> Eff xs w)
-> Eff ((k >: WriterEff w) : xs) a
-> w
-> Eff xs w
forall k (k :: k) (t :: * -> *) (xs :: [Assoc k (* -> *)]) a b r.
(a -> b -> Eff xs r)
-> (forall x. t x -> (x -> b -> Eff xs r) -> b -> Eff xs r)
-> Eff ((k >: t) : xs) a
-> b
-> Eff xs r
peelEff1 ((w -> Eff xs w) -> a -> w -> Eff xs w
forall a b. a -> b -> a
const w -> Eff xs w
forall (m :: * -> *) a. Monad m => a -> m a
return) forall x. WriterEff w x -> (x -> w -> Eff xs w) -> w -> Eff xs w
forall w a r. Monoid w => (w, a) -> (a -> w -> r) -> w -> r
contWriter (Eff ((k >: WriterEff w) : xs) a -> w -> Eff xs w)
-> w -> Eff ((k >: WriterEff w) : xs) a -> Eff xs w
forall a b c. (a -> b -> c) -> b -> a -> c
`flip` w
forall a. Monoid a => a
mempty
{-# INLINE execWriterEff #-}
type MaybeEff = Const ()
nothingEff :: Lookup xs k MaybeEff => Proxy k -> Eff xs a
nothingEff :: Proxy k -> Eff xs a
nothingEff = (Proxy k -> () -> Eff xs a) -> () -> Proxy k -> Eff xs a
forall a b c. (a -> b -> c) -> b -> a -> c
flip Proxy k -> () -> Eff xs a
forall k (xs :: [Assoc k (* -> *)]) (k :: k) e a.
Lookup xs k (EitherEff e) =>
Proxy k -> e -> Eff xs a
throwEff ()
runMaybeEff :: forall k xs a. Eff (k >: MaybeEff ': xs) a -> Eff xs (Maybe a)
runMaybeEff :: Eff ((k >: MaybeEff) : xs) a -> Eff xs (Maybe a)
runMaybeEff = (a -> Eff xs (Maybe a))
-> (forall x.
MaybeEff x -> (x -> Eff xs (Maybe a)) -> Eff xs (Maybe a))
-> Eff ((k >: MaybeEff) : xs) a
-> Eff xs (Maybe a)
forall k (k :: k) (t :: * -> *) (xs :: [Assoc k (* -> *)]) a r.
(a -> Eff xs r)
-> (forall x. t x -> (x -> Eff xs r) -> Eff xs r)
-> Eff ((k >: t) : xs) a
-> Eff xs r
peelEff0 (Maybe a -> Eff xs (Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe a -> Eff xs (Maybe a))
-> (a -> Maybe a) -> a -> Eff xs (Maybe a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Maybe a
forall a. a -> Maybe a
Just) ((forall x.
MaybeEff x -> (x -> Eff xs (Maybe a)) -> Eff xs (Maybe a))
-> Eff ((k >: MaybeEff) : xs) a -> Eff xs (Maybe a))
-> (forall x.
MaybeEff x -> (x -> Eff xs (Maybe a)) -> Eff xs (Maybe a))
-> Eff ((k >: MaybeEff) : xs) a
-> Eff xs (Maybe a)
forall a b. (a -> b) -> a -> b
$ \MaybeEff x
_ x -> Eff xs (Maybe a)
_ -> Maybe a -> Eff xs (Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe a
forall a. Maybe a
Nothing
{-# INLINE runMaybeEff #-}
type EitherEff = Const
throwEff :: Lookup xs k (EitherEff e) => Proxy k -> e -> Eff xs a
throwEff :: Proxy k -> e -> Eff xs a
throwEff Proxy k
k = Proxy k -> Const e a -> Eff xs a
forall k (s :: k) (t :: * -> *) (xs :: [Assoc k (* -> *)]) a.
Lookup xs s t =>
Proxy s -> t a -> Eff xs a
liftEff Proxy k
k (Const e a -> Eff xs a) -> (e -> Const e a) -> e -> Eff xs a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e -> Const e a
forall k a (b :: k). a -> Const a b
Const
{-# INLINE throwEff #-}
catchEff :: forall k e xs a. (Lookup xs k (EitherEff e))
=> Proxy k -> Eff xs a -> (e -> Eff xs a) -> Eff xs a
catchEff :: Proxy k -> Eff xs a -> (e -> Eff xs a) -> Eff xs a
catchEff Proxy k
_ Eff xs a
m0 e -> Eff xs a
handler = Eff xs a -> Eff xs a
go Eff xs a
m0 where
go :: Eff xs a -> Eff xs a
go Eff xs a
m = case Eff xs a
-> MonadView (Instruction xs) (Skeleton (Instruction xs)) a
forall (t :: * -> *) a. Skeleton t a -> MonadView t (Skeleton t) a
debone Eff xs a
m of
Return a
a -> a -> Eff xs a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a
Instruction i t :>>= a -> Eff xs a
k -> case Membership xs (k ':> Const e)
-> Membership xs kv -> Either Ordering ((k ':> Const e) :~: kv)
forall k (xs :: [k]) (x :: k) (y :: k).
Membership xs x -> Membership xs y -> Either Ordering (x :~: y)
compareMembership (Membership xs (k ':> Const e)
forall k k1 (xs :: [Assoc k k1]) (k2 :: k) (v :: k1).
Lookup xs k2 v =>
Membership xs (k2 ':> v)
association :: Membership xs (k ':> Const e)) Membership xs kv
i of
Left Ordering
_ -> MonadView (Instruction xs) (Skeleton (Instruction xs)) a
-> Eff xs a
forall (t :: * -> *) a. MonadView t (Skeleton t) a -> Skeleton t a
boned (MonadView (Instruction xs) (Skeleton (Instruction xs)) a
-> Eff xs a)
-> MonadView (Instruction xs) (Skeleton (Instruction xs)) a
-> Eff xs a
forall a b. (a -> b) -> a -> b
$ Membership xs kv -> TargetOf kv a -> Instruction xs a
forall k (xs :: [Assoc k (* -> *)]) (kv :: Assoc k (* -> *)) a.
Membership xs kv -> TargetOf kv a -> Instruction xs a
Instruction Membership xs kv
i TargetOf kv a
t Instruction xs a
-> (a -> Eff xs a)
-> MonadView (Instruction xs) (Skeleton (Instruction xs)) a
forall (t :: * -> *) a (m :: * -> *) x.
t a -> (a -> m x) -> MonadView t m x
:>>= Eff xs a -> Eff xs a
go (Eff xs a -> Eff xs a) -> (a -> Eff xs a) -> a -> Eff xs a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Eff xs a
k
Right (k ':> Const e) :~: kv
Refl -> e -> Eff xs a
handler (Const e a -> e
forall a k (b :: k). Const a b -> a
getConst Const e a
TargetOf kv a
t)
{-# INLINE catchEff #-}
runEitherEff :: forall k e xs a. Eff (k >: EitherEff e ': xs) a -> Eff xs (Either e a)
runEitherEff :: Eff ((k >: EitherEff e) : xs) a -> Eff xs (Either e a)
runEitherEff = (a -> Eff xs (Either e a))
-> (forall x.
EitherEff e x -> (x -> Eff xs (Either e a)) -> Eff xs (Either e a))
-> Eff ((k >: EitherEff e) : xs) a
-> Eff xs (Either e a)
forall k (k :: k) (t :: * -> *) (xs :: [Assoc k (* -> *)]) a r.
(a -> Eff xs r)
-> (forall x. t x -> (x -> Eff xs r) -> Eff xs r)
-> Eff ((k >: t) : xs) a
-> Eff xs r
peelEff0 (Either e a -> Eff xs (Either e a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either e a -> Eff xs (Either e a))
-> (a -> Either e a) -> a -> Eff xs (Either e a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Either e a
forall a b. b -> Either a b
Right) ((forall x.
EitherEff e x -> (x -> Eff xs (Either e a)) -> Eff xs (Either e a))
-> Eff ((k >: EitherEff e) : xs) a -> Eff xs (Either e a))
-> (forall x.
EitherEff e x -> (x -> Eff xs (Either e a)) -> Eff xs (Either e a))
-> Eff ((k >: EitherEff e) : xs) a
-> Eff xs (Either e a)
forall a b. (a -> b) -> a -> b
$ \(Const e) x -> Eff xs (Either e a)
_ -> Either e a -> Eff xs (Either e a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either e a -> Eff xs (Either e a))
-> Either e a -> Eff xs (Either e a)
forall a b. (a -> b) -> a -> b
$ e -> Either e a
forall a b. a -> Either a b
Left e
e
{-# INLINE runEitherEff #-}
tickEff :: Lookup xs k Identity => Proxy k -> Eff xs ()
tickEff :: Proxy k -> Eff xs ()
tickEff Proxy k
k = Proxy k -> Identity () -> Eff xs ()
forall k (s :: k) (t :: * -> *) (xs :: [Assoc k (* -> *)]) a.
Lookup xs s t =>
Proxy s -> t a -> Eff xs a
liftEff Proxy k
k (Identity () -> Eff xs ()) -> Identity () -> Eff xs ()
forall a b. (a -> b) -> a -> b
$ () -> Identity ()
forall a. a -> Identity a
Identity ()
{-# INLINE tickEff #-}
mapHeadEff :: (forall x. s x -> t x) -> Eff ((k >: s) ': xs) a -> Eff ((k' >: t) ': xs) a
mapHeadEff :: (forall x. s x -> t x)
-> Eff ((k >: s) : xs) a -> Eff ((k' >: t) : xs) a
mapHeadEff forall x. s x -> t x
f = (forall x.
Instruction ((k >: s) : xs) x -> Instruction ((k' >: t) : xs) x)
-> Eff ((k >: s) : xs) a -> Eff ((k' >: t) : xs) a
forall (s :: * -> *) (t :: * -> *) a.
(forall x. s x -> t x) -> Skeleton s a -> Skeleton t a
hoistSkeleton ((forall x.
Instruction ((k >: s) : xs) x -> Instruction ((k' >: t) : xs) x)
-> Eff ((k >: s) : xs) a -> Eff ((k' >: t) : xs) a)
-> (forall x.
Instruction ((k >: s) : xs) x -> Instruction ((k' >: t) : xs) x)
-> Eff ((k >: s) : xs) a
-> Eff ((k' >: t) : xs) a
forall a b. (a -> b) -> a -> b
$ \(Instruction i t) -> Membership ((k >: s) : xs) kv
-> ((kv :~: (k >: s)) -> Instruction ((k' >: t) : xs) x)
-> (Membership xs kv -> Instruction ((k' >: t) : xs) x)
-> Instruction ((k' >: t) : xs) x
forall k (y :: k) (xs :: [k]) (x :: k) r.
Membership (y : xs) x
-> ((x :~: y) -> r) -> (Membership xs x -> r) -> r
testMembership Membership ((k >: s) : xs) kv
i
(\kv :~: (k >: s)
Refl -> Membership ((k' >: t) : xs) (k' >: t)
-> TargetOf (k' >: t) x -> Instruction ((k' >: t) : xs) x
forall k (xs :: [Assoc k (* -> *)]) (kv :: Assoc k (* -> *)) a.
Membership xs kv -> TargetOf kv a -> Instruction xs a
Instruction Membership ((k' >: t) : xs) (k' >: t)
forall k (x :: k) (xs :: [k]). Membership (x : xs) x
leadership (TargetOf (k' >: t) x -> Instruction ((k' >: t) : xs) x)
-> TargetOf (k' >: t) x -> Instruction ((k' >: t) : xs) x
forall a b. (a -> b) -> a -> b
$ s x -> t x
forall x. s x -> t x
f s x
TargetOf kv x
t)
(\Membership xs kv
j -> Membership ((k' >: t) : xs) kv
-> TargetOf kv x -> Instruction ((k' >: t) : xs) x
forall k (xs :: [Assoc k (* -> *)]) (kv :: Assoc k (* -> *)) a.
Membership xs kv -> TargetOf kv a -> Instruction xs a
Instruction (Membership xs kv -> Membership ((k' >: t) : xs) kv
forall k (xs :: [k]) (y :: k) (x :: k).
Membership xs y -> Membership (x : xs) y
nextMembership Membership xs kv
j) TargetOf kv x
t)
mapLeftEff :: (e -> e') -> Eff ((k >: EitherEff e) ': xs) a -> Eff ((k >: EitherEff e') ': xs) a
mapLeftEff :: (e -> e')
-> Eff ((k >: EitherEff e) : xs) a
-> Eff ((k >: EitherEff e') : xs) a
mapLeftEff e -> e'
f = (forall x. EitherEff e x -> EitherEff e' x)
-> Eff ((k >: EitherEff e) : xs) a
-> Eff ((k >: EitherEff e') : xs) a
forall k (s :: * -> *) (t :: * -> *) (k :: k)
(xs :: [Assoc k (* -> *)]) a (k' :: k).
(forall x. s x -> t x)
-> Eff ((k >: s) : xs) a -> Eff ((k' >: t) : xs) a
mapHeadEff ((e -> e') -> Const e x -> Const e' x
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first e -> e'
f)
runIterEff :: Eff (k >: Identity ': xs) a
-> Eff xs (Either a (Eff (k >: Identity ': xs) a))
runIterEff :: Eff ((k >: Identity) : xs) a
-> Eff xs (Either a (Eff ((k >: Identity) : xs) a))
runIterEff Eff ((k >: Identity) : xs) a
m = case Eff ((k >: Identity) : xs) a
-> MonadView
(Instruction ((k >: Identity) : xs))
(Skeleton (Instruction ((k >: Identity) : xs)))
a
forall (t :: * -> *) a. Skeleton t a -> MonadView t (Skeleton t) a
debone Eff ((k >: Identity) : xs) a
m of
Return a
a -> Either a (Eff ((k >: Identity) : xs) a)
-> Eff xs (Either a (Eff ((k >: Identity) : xs) a))
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> Either a (Eff ((k >: Identity) : xs) a)
forall a b. a -> Either a b
Left a
a)
Instruction Membership ((k >: Identity) : xs) kv
i TargetOf kv a
t :>>= a -> Eff ((k >: Identity) : xs) a
k -> Membership ((k >: Identity) : xs) kv
-> ((kv :~: (k >: Identity))
-> Eff xs (Either a (Eff ((k >: Identity) : xs) a)))
-> (Membership xs kv
-> Eff xs (Either a (Eff ((k >: Identity) : xs) a)))
-> Eff xs (Either a (Eff ((k >: Identity) : xs) a))
forall k (y :: k) (xs :: [k]) (x :: k) r.
Membership (y : xs) x
-> ((x :~: y) -> r) -> (Membership xs x -> r) -> r
testMembership Membership ((k >: Identity) : xs) kv
i
(\kv :~: (k >: Identity)
Refl -> Either a (Eff ((k >: Identity) : xs) a)
-> Eff xs (Either a (Eff ((k >: Identity) : xs) a))
forall (m :: * -> *) a. Monad m => a -> m a
return (Either a (Eff ((k >: Identity) : xs) a)
-> Eff xs (Either a (Eff ((k >: Identity) : xs) a)))
-> Either a (Eff ((k >: Identity) : xs) a)
-> Eff xs (Either a (Eff ((k >: Identity) : xs) a))
forall a b. (a -> b) -> a -> b
$ Eff ((k >: Identity) : xs) a
-> Either a (Eff ((k >: Identity) : xs) a)
forall a b. b -> Either a b
Right (Eff ((k >: Identity) : xs) a
-> Either a (Eff ((k >: Identity) : xs) a))
-> Eff ((k >: Identity) : xs) a
-> Either a (Eff ((k >: Identity) : xs) a)
forall a b. (a -> b) -> a -> b
$ a -> Eff ((k >: Identity) : xs) a
k (a -> Eff ((k >: Identity) : xs) a)
-> a -> Eff ((k >: Identity) : xs) a
forall a b. (a -> b) -> a -> b
$ Identity a -> a
forall a. Identity a -> a
runIdentity Identity a
TargetOf kv a
t)
((Membership xs kv
-> Eff xs (Either a (Eff ((k >: Identity) : xs) a)))
-> Eff xs (Either a (Eff ((k >: Identity) : xs) a)))
-> (Membership xs kv
-> Eff xs (Either a (Eff ((k >: Identity) : xs) a)))
-> Eff xs (Either a (Eff ((k >: Identity) : xs) a))
forall a b. (a -> b) -> a -> b
$ \Membership xs kv
j -> MonadView
(Instruction xs)
(Skeleton (Instruction xs))
(Either a (Eff ((k >: Identity) : xs) a))
-> Eff xs (Either a (Eff ((k >: Identity) : xs) a))
forall (t :: * -> *) a. MonadView t (Skeleton t) a -> Skeleton t a
boned (MonadView
(Instruction xs)
(Skeleton (Instruction xs))
(Either a (Eff ((k >: Identity) : xs) a))
-> Eff xs (Either a (Eff ((k >: Identity) : xs) a)))
-> MonadView
(Instruction xs)
(Skeleton (Instruction xs))
(Either a (Eff ((k >: Identity) : xs) a))
-> Eff xs (Either a (Eff ((k >: Identity) : xs) a))
forall a b. (a -> b) -> a -> b
$ Membership xs kv -> TargetOf kv a -> Instruction xs a
forall k (xs :: [Assoc k (* -> *)]) (kv :: Assoc k (* -> *)) a.
Membership xs kv -> TargetOf kv a -> Instruction xs a
Instruction Membership xs kv
j TargetOf kv a
t Instruction xs a
-> (a -> Eff xs (Either a (Eff ((k >: Identity) : xs) a)))
-> MonadView
(Instruction xs)
(Skeleton (Instruction xs))
(Either a (Eff ((k >: Identity) : xs) a))
forall (t :: * -> *) a (m :: * -> *) x.
t a -> (a -> m x) -> MonadView t m x
:>>= Eff ((k >: Identity) : xs) a
-> Eff xs (Either a (Eff ((k >: Identity) : xs) a))
forall k (k :: k) (xs :: [Assoc k (* -> *)]) a.
Eff ((k >: Identity) : xs) a
-> Eff xs (Either a (Eff ((k >: Identity) : xs) a))
runIterEff (Eff ((k >: Identity) : xs) a
-> Eff xs (Either a (Eff ((k >: Identity) : xs) a)))
-> (a -> Eff ((k >: Identity) : xs) a)
-> a
-> Eff xs (Either a (Eff ((k >: Identity) : xs) a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Eff ((k >: Identity) : xs) a
k
contEff :: Lookup xs k (ContT r m) => Proxy k
-> ((a -> m r) -> m r) -> Eff xs a
contEff :: Proxy k -> ((a -> m r) -> m r) -> Eff xs a
contEff Proxy k
k = Proxy k -> ContT r m a -> Eff xs a
forall k (s :: k) (t :: * -> *) (xs :: [Assoc k (* -> *)]) a.
Lookup xs s t =>
Proxy s -> t a -> Eff xs a
liftEff Proxy k
k (ContT r m a -> Eff xs a)
-> (((a -> m r) -> m r) -> ContT r m a)
-> ((a -> m r) -> m r)
-> Eff xs a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((a -> m r) -> m r) -> ContT r m a
forall k (r :: k) (m :: k -> *) a.
((a -> m r) -> m r) -> ContT r m a
ContT
runContEff :: forall k r xs a. Eff (k >: ContT r (Eff xs) ': xs) a
-> (a -> Eff xs r)
-> Eff xs r
runContEff :: Eff ((k >: ContT r (Eff xs)) : xs) a -> (a -> Eff xs r) -> Eff xs r
runContEff Eff ((k >: ContT r (Eff xs)) : xs) a
m a -> Eff xs r
cont = case Eff ((k >: ContT r (Eff xs)) : xs) a
-> MonadView
(Instruction ((k >: ContT r (Eff xs)) : xs))
(Skeleton (Instruction ((k >: ContT r (Eff xs)) : xs)))
a
forall (t :: * -> *) a. Skeleton t a -> MonadView t (Skeleton t) a
debone Eff ((k >: ContT r (Eff xs)) : xs) a
m of
Return a
a -> a -> Eff xs r
cont a
a
Instruction Membership ((k >: ContT r (Eff xs)) : xs) kv
i TargetOf kv a
t :>>= a -> Eff ((k >: ContT r (Eff xs)) : xs) a
k -> Membership ((k >: ContT r (Eff xs)) : xs) kv
-> ((kv :~: (k >: ContT r (Eff xs))) -> Eff xs r)
-> (Membership xs kv -> Eff xs r)
-> Eff xs r
forall k (y :: k) (xs :: [k]) (x :: k) r.
Membership (y : xs) x
-> ((x :~: y) -> r) -> (Membership xs x -> r) -> r
testMembership Membership ((k >: ContT r (Eff xs)) : xs) kv
i
(\kv :~: (k >: ContT r (Eff xs))
Refl -> ContT r (Eff xs) a -> (a -> Eff xs r) -> Eff xs r
forall k (r :: k) (m :: k -> *) a. ContT r m a -> (a -> m r) -> m r
runContT TargetOf kv a
ContT r (Eff xs) a
t ((Eff ((k >: ContT r (Eff xs)) : xs) a
-> (a -> Eff xs r) -> Eff xs r)
-> (a -> Eff xs r)
-> Eff ((k >: ContT r (Eff xs)) : xs) a
-> Eff xs r
forall a b c. (a -> b -> c) -> b -> a -> c
flip Eff ((k >: ContT r (Eff xs)) : xs) a -> (a -> Eff xs r) -> Eff xs r
forall k (k :: k) r (xs :: [Assoc k (* -> *)]) a.
Eff ((k >: ContT r (Eff xs)) : xs) a -> (a -> Eff xs r) -> Eff xs r
runContEff a -> Eff xs r
cont (Eff ((k >: ContT r (Eff xs)) : xs) a -> Eff xs r)
-> (a -> Eff ((k >: ContT r (Eff xs)) : xs) a) -> a -> Eff xs r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Eff ((k >: ContT r (Eff xs)) : xs) a
k))
((Membership xs kv -> Eff xs r) -> Eff xs r)
-> (Membership xs kv -> Eff xs r) -> Eff xs r
forall a b. (a -> b) -> a -> b
$ \Membership xs kv
j -> MonadView (Instruction xs) (Eff xs) r -> Eff xs r
forall (t :: * -> *) a. MonadView t (Skeleton t) a -> Skeleton t a
boned (MonadView (Instruction xs) (Eff xs) r -> Eff xs r)
-> MonadView (Instruction xs) (Eff xs) r -> Eff xs r
forall a b. (a -> b) -> a -> b
$ Membership xs kv -> TargetOf kv a -> Instruction xs a
forall k (xs :: [Assoc k (* -> *)]) (kv :: Assoc k (* -> *)) a.
Membership xs kv -> TargetOf kv a -> Instruction xs a
Instruction Membership xs kv
j TargetOf kv a
t Instruction xs a
-> (a -> Eff xs r) -> MonadView (Instruction xs) (Eff xs) r
forall (t :: * -> *) a (m :: * -> *) x.
t a -> (a -> m x) -> MonadView t m x
:>>= (Eff ((k >: ContT r (Eff xs)) : xs) a
-> (a -> Eff xs r) -> Eff xs r)
-> (a -> Eff xs r)
-> Eff ((k >: ContT r (Eff xs)) : xs) a
-> Eff xs r
forall a b c. (a -> b -> c) -> b -> a -> c
flip Eff ((k >: ContT r (Eff xs)) : xs) a -> (a -> Eff xs r) -> Eff xs r
forall k (k :: k) r (xs :: [Assoc k (* -> *)]) a.
Eff ((k >: ContT r (Eff xs)) : xs) a -> (a -> Eff xs r) -> Eff xs r
runContEff a -> Eff xs r
cont (Eff ((k >: ContT r (Eff xs)) : xs) a -> Eff xs r)
-> (a -> Eff ((k >: ContT r (Eff xs)) : xs) a) -> a -> Eff xs r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Eff ((k >: ContT r (Eff xs)) : xs) a
k
callCCEff :: Proxy k -> ((a -> Eff ((k >: ContT r (Eff xs)) : xs) b) -> Eff ((k >: ContT r (Eff xs)) : xs) a) -> Eff ((k >: ContT r (Eff xs)) : xs) a
callCCEff :: Proxy k
-> ((a -> Eff ((k >: ContT r (Eff xs)) : xs) b)
-> Eff ((k >: ContT r (Eff xs)) : xs) a)
-> Eff ((k >: ContT r (Eff xs)) : xs) a
callCCEff Proxy k
k (a -> Eff ((k >: ContT r (Eff xs)) : xs) b)
-> Eff ((k >: ContT r (Eff xs)) : xs) a
f = Proxy k
-> ContT r (Eff xs) a -> Eff ((k >: ContT r (Eff xs)) : xs) a
forall k (k :: k) r (xs :: [Assoc k (* -> *)]) a.
Proxy k
-> ContT r (Eff xs) a -> Eff ((k >: ContT r (Eff xs)) : xs) a
contHead Proxy k
k (ContT r (Eff xs) a -> Eff ((k >: ContT r (Eff xs)) : xs) a)
-> (((a -> Eff xs r) -> Eff xs r) -> ContT r (Eff xs) a)
-> ((a -> Eff xs r) -> Eff xs r)
-> Eff ((k >: ContT r (Eff xs)) : xs) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((a -> Eff xs r) -> Eff xs r) -> ContT r (Eff xs) a
forall k (r :: k) (m :: k -> *) a.
((a -> m r) -> m r) -> ContT r m a
ContT (((a -> Eff xs r) -> Eff xs r)
-> Eff ((k >: ContT r (Eff xs)) : xs) a)
-> ((a -> Eff xs r) -> Eff xs r)
-> Eff ((k >: ContT r (Eff xs)) : xs) a
forall a b. (a -> b) -> a -> b
$ \a -> Eff xs r
c -> Eff ((k >: ContT r (Eff xs)) : xs) a -> (a -> Eff xs r) -> Eff xs r
forall k (k :: k) r (xs :: [Assoc k (* -> *)]) a.
Eff ((k >: ContT r (Eff xs)) : xs) a -> (a -> Eff xs r) -> Eff xs r
runContEff ((a -> Eff ((k >: ContT r (Eff xs)) : xs) b)
-> Eff ((k >: ContT r (Eff xs)) : xs) a
f (\a
x -> Proxy k
-> ContT r (Eff xs) b -> Eff ((k >: ContT r (Eff xs)) : xs) b
forall k (k :: k) r (xs :: [Assoc k (* -> *)]) a.
Proxy k
-> ContT r (Eff xs) a -> Eff ((k >: ContT r (Eff xs)) : xs) a
contHead Proxy k
k (ContT r (Eff xs) b -> Eff ((k >: ContT r (Eff xs)) : xs) b)
-> (((b -> Eff xs r) -> Eff xs r) -> ContT r (Eff xs) b)
-> ((b -> Eff xs r) -> Eff xs r)
-> Eff ((k >: ContT r (Eff xs)) : xs) b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((b -> Eff xs r) -> Eff xs r) -> ContT r (Eff xs) b
forall k (r :: k) (m :: k -> *) a.
((a -> m r) -> m r) -> ContT r m a
ContT (((b -> Eff xs r) -> Eff xs r)
-> Eff ((k >: ContT r (Eff xs)) : xs) b)
-> ((b -> Eff xs r) -> Eff xs r)
-> Eff ((k >: ContT r (Eff xs)) : xs) b
forall a b. (a -> b) -> a -> b
$ \b -> Eff xs r
_ -> a -> Eff xs r
c a
x)) a -> Eff xs r
c
where
contHead :: Proxy k -> ContT r (Eff xs) a -> Eff ((k >: ContT r (Eff xs)) ': xs) a
contHead :: Proxy k
-> ContT r (Eff xs) a -> Eff ((k >: ContT r (Eff xs)) : xs) a
contHead Proxy k
_ ContT r (Eff xs) a
c = MonadView
(Instruction ((k >: ContT r (Eff xs)) : xs))
(Skeleton (Instruction ((k >: ContT r (Eff xs)) : xs)))
a
-> Eff ((k >: ContT r (Eff xs)) : xs) a
forall (t :: * -> *) a. MonadView t (Skeleton t) a -> Skeleton t a
boned (MonadView
(Instruction ((k >: ContT r (Eff xs)) : xs))
(Skeleton (Instruction ((k >: ContT r (Eff xs)) : xs)))
a
-> Eff ((k >: ContT r (Eff xs)) : xs) a)
-> MonadView
(Instruction ((k >: ContT r (Eff xs)) : xs))
(Skeleton (Instruction ((k >: ContT r (Eff xs)) : xs)))
a
-> Eff ((k >: ContT r (Eff xs)) : xs) a
forall a b. (a -> b) -> a -> b
$ Membership ((k >: ContT r (Eff xs)) : xs) (k >: ContT r (Eff xs))
-> TargetOf (k >: ContT r (Eff xs)) a
-> Instruction ((k >: ContT r (Eff xs)) : xs) a
forall k (xs :: [Assoc k (* -> *)]) (kv :: Assoc k (* -> *)) a.
Membership xs kv -> TargetOf kv a -> Instruction xs a
Instruction Membership ((k >: ContT r (Eff xs)) : xs) (k >: ContT r (Eff xs))
forall k (x :: k) (xs :: [k]). Membership (x : xs) x
leadership TargetOf (k >: ContT r (Eff xs)) a
ContT r (Eff xs) a
c Instruction ((k >: ContT r (Eff xs)) : xs) a
-> (a -> Eff ((k >: ContT r (Eff xs)) : xs) a)
-> MonadView
(Instruction ((k >: ContT r (Eff xs)) : xs))
(Skeleton (Instruction ((k >: ContT r (Eff xs)) : xs)))
a
forall (t :: * -> *) a (m :: * -> *) x.
t a -> (a -> m x) -> MonadView t m x
:>>= a -> Eff ((k >: ContT r (Eff xs)) : xs) a
forall (m :: * -> *) a. Monad m => a -> m a
return