{-# LANGUAGE GADTs #-}
{-# LANGUAGE Rank2Types #-}
module Data.Machine.Pipe where
import Control.Monad
import Data.Void
import Data.Machine.Plan
import Data.Machine.Type
infixl 8 >~>
infixl 7 >+>
infixl 7 >>~
infixr 6 +>>
data Exchange a' a b' b c where
Request :: a' -> Exchange a' a b' b a
Respond :: b -> Exchange a' a b' b b'
type Proxy a' a b' b m c = MachineT m (Exchange a' a b' b) c
type Effect m r = Proxy Void () () Void m r
type Client a' a m r = Proxy a' a () Void m r
type Server b' b m r = Proxy Void () b' b m r
type Effect' m r = forall x' x y' y . Proxy x' x y' y m r
type Server' b' b m r = forall x' x . Proxy x' x b' b m r
type Client' a' a m r = forall y' y . Proxy a' a y' y m r
request :: a' -> PlanT (Exchange a' a y' y) o m a
request :: a' -> PlanT (Exchange a' a y' y) o m a
request a'
a = Exchange a' a y' y a -> Plan (Exchange a' a y' y) o a
forall (k :: * -> *) i o. k i -> Plan k o i
awaits (a' -> Exchange a' a y' y a
forall a' a b' b. a' -> Exchange a' a b' b a
Request a'
a)
respond :: a -> PlanT (Exchange x' x a' a) o m a'
respond :: a -> PlanT (Exchange x' x a' a) o m a'
respond a
a = Exchange x' x a' a a' -> Plan (Exchange x' x a' a) o a'
forall (k :: * -> *) i o. k i -> Plan k o i
awaits (a -> Exchange x' x a' a a'
forall b a' a b'. b -> Exchange a' a b' b b'
Respond a
a)
push :: Monad m => a -> Proxy a' a a' a m r
push :: a -> Proxy a' a a' a m r
push = PlanT (Exchange a' a a' a) r m Any -> Proxy a' a a' a m r
forall (m :: * -> *) (k :: * -> *) o a.
Monad m =>
PlanT k o m a -> MachineT m k o
construct (PlanT (Exchange a' a a' a) r m Any -> Proxy a' a a' a m r)
-> (a -> PlanT (Exchange a' a a' a) r m Any)
-> a
-> Proxy a' a a' a m r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> PlanT (Exchange a' a a' a) r m Any
forall x x' o (m :: * -> *) c.
x -> PlanT (Exchange x' x x' x) o m c
go
where
go :: x -> PlanT (Exchange x' x x' x) o m c
go = x -> PlanT (Exchange x' x x' x) o m x'
forall a x' x a' o (m :: * -> *).
a -> PlanT (Exchange x' x a' a) o m a'
respond (x -> PlanT (Exchange x' x x' x) o m x')
-> (x' -> PlanT (Exchange x' x x' x) o m c)
-> x
-> PlanT (Exchange x' x x' x) o m c
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> x' -> PlanT (Exchange x' x x' x) o m x
forall a' a y' y o (m :: * -> *).
a' -> PlanT (Exchange a' a y' y) o m a
request (x' -> PlanT (Exchange x' x x' x) o m x)
-> (x -> PlanT (Exchange x' x x' x) o m c)
-> x'
-> PlanT (Exchange x' x x' x) o m c
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> x -> PlanT (Exchange x' x x' x) o m c
go
(>~>) :: Monad m
=> (_a -> Proxy a' a b' b m r)
-> (b -> Proxy b' b c' c m r)
-> _a -> Proxy a' a c' c m r
(_a -> Proxy a' a b' b m r
fa >~> :: (_a -> Proxy a' a b' b m r)
-> (b -> Proxy b' b c' c m r) -> _a -> Proxy a' a c' c m r
>~> b -> Proxy b' b c' c m r
fb) _a
a = _a -> Proxy a' a b' b m r
fa _a
a Proxy a' a b' b m r
-> (b -> Proxy b' b c' c m r) -> Proxy a' a c' c m r
forall (m :: * -> *) a' a b' b r c' c.
Monad m =>
Proxy a' a b' b m r
-> (b -> Proxy b' b c' c m r) -> Proxy a' a c' c m r
>>~ b -> Proxy b' b c' c m r
fb
(>>~) :: Monad m
=> Proxy a' a b' b m r
-> (b -> Proxy b' b c' c m r)
-> Proxy a' a c' c m r
Proxy a' a b' b m r
pm >>~ :: Proxy a' a b' b m r
-> (b -> Proxy b' b c' c m r) -> Proxy a' a c' c m r
>>~ b -> Proxy b' b c' c m r
fb = m (Step (Exchange a' a c' c) r (Proxy a' a c' c m r))
-> Proxy a' a c' c m r
forall (m :: * -> *) (k :: * -> *) o.
m (Step k o (MachineT m k o)) -> MachineT m k o
MachineT (m (Step (Exchange a' a c' c) r (Proxy a' a c' c m r))
-> Proxy a' a c' c m r)
-> m (Step (Exchange a' a c' c) r (Proxy a' a c' c m r))
-> Proxy a' a c' c m r
forall a b. (a -> b) -> a -> b
$ Proxy a' a b' b m r
-> m (Step (Exchange a' a b' b) r (Proxy a' a b' b m r))
forall (m :: * -> *) (k :: * -> *) o.
MachineT m k o -> m (Step k o (MachineT m k o))
runMachineT Proxy a' a b' b m r
pm m (Step (Exchange a' a b' b) r (Proxy a' a b' b m r))
-> (Step (Exchange a' a b' b) r (Proxy a' a b' b m r)
-> m (Step (Exchange a' a c' c) r (Proxy a' a c' c m r)))
-> m (Step (Exchange a' a c' c) r (Proxy a' a c' c m r))
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Step (Exchange a' a b' b) r (Proxy a' a b' b m r)
p ->
case Step (Exchange a' a b' b) r (Proxy a' a b' b m r)
p of
Step (Exchange a' a b' b) r (Proxy a' a b' b m r)
Stop -> Step (Exchange a' a c' c) r (Proxy a' a c' c m r)
-> m (Step (Exchange a' a c' c) r (Proxy a' a c' c m r))
forall (m :: * -> *) a. Monad m => a -> m a
return Step (Exchange a' a c' c) r (Proxy a' a c' c m r)
forall (k :: * -> *) o r. Step k o r
Stop
Yield r
r Proxy a' a b' b m r
n -> Step (Exchange a' a c' c) r (Proxy a' a c' c m r)
-> m (Step (Exchange a' a c' c) r (Proxy a' a c' c m r))
forall (m :: * -> *) a. Monad m => a -> m a
return (Step (Exchange a' a c' c) r (Proxy a' a c' c m r)
-> m (Step (Exchange a' a c' c) r (Proxy a' a c' c m r)))
-> Step (Exchange a' a c' c) r (Proxy a' a c' c m r)
-> m (Step (Exchange a' a c' c) r (Proxy a' a c' c m r))
forall a b. (a -> b) -> a -> b
$ r
-> Proxy a' a c' c m r
-> Step (Exchange a' a c' c) r (Proxy a' a c' c m r)
forall (k :: * -> *) o r. o -> r -> Step k o r
Yield r
r (Proxy a' a b' b m r
n Proxy a' a b' b m r
-> (b -> Proxy b' b c' c m r) -> Proxy a' a c' c m r
forall (m :: * -> *) a' a b' b r c' c.
Monad m =>
Proxy a' a b' b m r
-> (b -> Proxy b' b c' c m r) -> Proxy a' a c' c m r
>>~ b -> Proxy b' b c' c m r
fb)
Await t -> Proxy a' a b' b m r
k (Request a'
a') Proxy a' a b' b m r
ff -> Step (Exchange a' t c' c) r (Proxy a' a c' c m r)
-> m (Step (Exchange a' t c' c) r (Proxy a' a c' c m r))
forall (m :: * -> *) a. Monad m => a -> m a
return (Step (Exchange a' t c' c) r (Proxy a' a c' c m r)
-> m (Step (Exchange a' t c' c) r (Proxy a' a c' c m r)))
-> Step (Exchange a' t c' c) r (Proxy a' a c' c m r)
-> m (Step (Exchange a' t c' c) r (Proxy a' a c' c m r))
forall a b. (a -> b) -> a -> b
$ (t -> Proxy a' a c' c m r)
-> Exchange a' t c' c t
-> Proxy a' a c' c m r
-> Step (Exchange a' t c' c) r (Proxy a' a c' c m r)
forall (k :: * -> *) o r t. (t -> r) -> k t -> r -> Step k o r
Await (\t
a -> t -> Proxy a' a b' b m r
k t
a Proxy a' a b' b m r
-> (b -> Proxy b' b c' c m r) -> Proxy a' a c' c m r
forall (m :: * -> *) a' a b' b r c' c.
Monad m =>
Proxy a' a b' b m r
-> (b -> Proxy b' b c' c m r) -> Proxy a' a c' c m r
>>~ b -> Proxy b' b c' c m r
fb) (a' -> Exchange a' t c' c t
forall a' a b' b. a' -> Exchange a' a b' b a
Request a'
a') (Proxy a' a b' b m r
ff Proxy a' a b' b m r
-> (b -> Proxy b' b c' c m r) -> Proxy a' a c' c m r
forall (m :: * -> *) a' a b' b r c' c.
Monad m =>
Proxy a' a b' b m r
-> (b -> Proxy b' b c' c m r) -> Proxy a' a c' c m r
>>~ b -> Proxy b' b c' c m r
fb)
Await t -> Proxy a' a b' b m r
k (Respond b
b) Proxy a' a b' b m r
_ -> Proxy a' a c' c m r
-> m (Step (Exchange a' a c' c) r (Proxy a' a c' c m r))
forall (m :: * -> *) (k :: * -> *) o.
MachineT m k o -> m (Step k o (MachineT m k o))
runMachineT (b' -> Proxy a' a b' b m r
t -> Proxy a' a b' b m r
k (b' -> Proxy a' a b' b m r)
-> Proxy b' b c' c m r -> Proxy a' a c' c m r
forall (m :: * -> *) b' a' a b r c' c.
Monad m =>
(b' -> Proxy a' a b' b m r)
-> Proxy b' b c' c m r -> Proxy a' a c' c m r
+>> b -> Proxy b' b c' c m r
fb b
b)
pull :: Monad m => a' -> Proxy a' a a' a m r
pull :: a' -> Proxy a' a a' a m r
pull = PlanT (Exchange a' a a' a) r m Any -> Proxy a' a a' a m r
forall (m :: * -> *) (k :: * -> *) o a.
Monad m =>
PlanT k o m a -> MachineT m k o
construct (PlanT (Exchange a' a a' a) r m Any -> Proxy a' a a' a m r)
-> (a' -> PlanT (Exchange a' a a' a) r m Any)
-> a'
-> Proxy a' a a' a m r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a' -> PlanT (Exchange a' a a' a) r m Any
forall y' y o (m :: * -> *) c.
y' -> PlanT (Exchange y' y y' y) o m c
go
where
go :: y' -> PlanT (Exchange y' y y' y) o m c
go = y' -> PlanT (Exchange y' y y' y) o m y
forall a' a y' y o (m :: * -> *).
a' -> PlanT (Exchange a' a y' y) o m a
request (y' -> PlanT (Exchange y' y y' y) o m y)
-> (y -> PlanT (Exchange y' y y' y) o m c)
-> y'
-> PlanT (Exchange y' y y' y) o m c
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> y -> PlanT (Exchange y' y y' y) o m y'
forall a x' x a' o (m :: * -> *).
a -> PlanT (Exchange x' x a' a) o m a'
respond (y -> PlanT (Exchange y' y y' y) o m y')
-> (y' -> PlanT (Exchange y' y y' y) o m c)
-> y
-> PlanT (Exchange y' y y' y) o m c
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> y' -> PlanT (Exchange y' y y' y) o m c
go
(>+>) :: Monad m
=> (b' -> Proxy a' a b' b m r)
-> (_c' -> Proxy b' b c' c m r)
-> _c' -> Proxy a' a c' c m r
(b' -> Proxy a' a b' b m r
fb' >+> :: (b' -> Proxy a' a b' b m r)
-> (_c' -> Proxy b' b c' c m r) -> _c' -> Proxy a' a c' c m r
>+> _c' -> Proxy b' b c' c m r
fc') _c'
c' = b' -> Proxy a' a b' b m r
fb' (b' -> Proxy a' a b' b m r)
-> Proxy b' b c' c m r -> Proxy a' a c' c m r
forall (m :: * -> *) b' a' a b r c' c.
Monad m =>
(b' -> Proxy a' a b' b m r)
-> Proxy b' b c' c m r -> Proxy a' a c' c m r
+>> _c' -> Proxy b' b c' c m r
fc' _c'
c'
(+>>) :: Monad m
=> (b' -> Proxy a' a b' b m r)
-> Proxy b' b c' c m r
-> Proxy a' a c' c m r
b' -> Proxy a' a b' b m r
fb' +>> :: (b' -> Proxy a' a b' b m r)
-> Proxy b' b c' c m r -> Proxy a' a c' c m r
+>> Proxy b' b c' c m r
pm = m (Step (Exchange a' a c' c) r (Proxy a' a c' c m r))
-> Proxy a' a c' c m r
forall (m :: * -> *) (k :: * -> *) o.
m (Step k o (MachineT m k o)) -> MachineT m k o
MachineT (m (Step (Exchange a' a c' c) r (Proxy a' a c' c m r))
-> Proxy a' a c' c m r)
-> m (Step (Exchange a' a c' c) r (Proxy a' a c' c m r))
-> Proxy a' a c' c m r
forall a b. (a -> b) -> a -> b
$ Proxy b' b c' c m r
-> m (Step (Exchange b' b c' c) r (Proxy b' b c' c m r))
forall (m :: * -> *) (k :: * -> *) o.
MachineT m k o -> m (Step k o (MachineT m k o))
runMachineT Proxy b' b c' c m r
pm m (Step (Exchange b' b c' c) r (Proxy b' b c' c m r))
-> (Step (Exchange b' b c' c) r (Proxy b' b c' c m r)
-> m (Step (Exchange a' a c' c) r (Proxy a' a c' c m r)))
-> m (Step (Exchange a' a c' c) r (Proxy a' a c' c m r))
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Step (Exchange b' b c' c) r (Proxy b' b c' c m r)
p ->
case Step (Exchange b' b c' c) r (Proxy b' b c' c m r)
p of
Step (Exchange b' b c' c) r (Proxy b' b c' c m r)
Stop -> Step (Exchange a' a c' c) r (Proxy a' a c' c m r)
-> m (Step (Exchange a' a c' c) r (Proxy a' a c' c m r))
forall (m :: * -> *) a. Monad m => a -> m a
return Step (Exchange a' a c' c) r (Proxy a' a c' c m r)
forall (k :: * -> *) o r. Step k o r
Stop
Yield r
r Proxy b' b c' c m r
n -> Step (Exchange a' a c' c) r (Proxy a' a c' c m r)
-> m (Step (Exchange a' a c' c) r (Proxy a' a c' c m r))
forall (m :: * -> *) a. Monad m => a -> m a
return (Step (Exchange a' a c' c) r (Proxy a' a c' c m r)
-> m (Step (Exchange a' a c' c) r (Proxy a' a c' c m r)))
-> Step (Exchange a' a c' c) r (Proxy a' a c' c m r)
-> m (Step (Exchange a' a c' c) r (Proxy a' a c' c m r))
forall a b. (a -> b) -> a -> b
$ r
-> Proxy a' a c' c m r
-> Step (Exchange a' a c' c) r (Proxy a' a c' c m r)
forall (k :: * -> *) o r. o -> r -> Step k o r
Yield r
r (b' -> Proxy a' a b' b m r
fb' (b' -> Proxy a' a b' b m r)
-> Proxy b' b c' c m r -> Proxy a' a c' c m r
forall (m :: * -> *) b' a' a b r c' c.
Monad m =>
(b' -> Proxy a' a b' b m r)
-> Proxy b' b c' c m r -> Proxy a' a c' c m r
+>> Proxy b' b c' c m r
n)
Await t -> Proxy b' b c' c m r
k (Request b'
b') Proxy b' b c' c m r
_ -> Proxy a' a c' c m r
-> m (Step (Exchange a' a c' c) r (Proxy a' a c' c m r))
forall (m :: * -> *) (k :: * -> *) o.
MachineT m k o -> m (Step k o (MachineT m k o))
runMachineT (b' -> Proxy a' a b' b m r
fb' b'
b' Proxy a' a b' b m r
-> (b -> Proxy b' b c' c m r) -> Proxy a' a c' c m r
forall (m :: * -> *) a' a b' b r c' c.
Monad m =>
Proxy a' a b' b m r
-> (b -> Proxy b' b c' c m r) -> Proxy a' a c' c m r
>>~ b -> Proxy b' b c' c m r
t -> Proxy b' b c' c m r
k)
Await t -> Proxy b' b c' c m r
k (Respond c
c) Proxy b' b c' c m r
ff -> Step (Exchange a' a t c) r (Proxy a' a c' c m r)
-> m (Step (Exchange a' a t c) r (Proxy a' a c' c m r))
forall (m :: * -> *) a. Monad m => a -> m a
return (Step (Exchange a' a t c) r (Proxy a' a c' c m r)
-> m (Step (Exchange a' a t c) r (Proxy a' a c' c m r)))
-> Step (Exchange a' a t c) r (Proxy a' a c' c m r)
-> m (Step (Exchange a' a t c) r (Proxy a' a c' c m r))
forall a b. (a -> b) -> a -> b
$ (t -> Proxy a' a c' c m r)
-> Exchange a' a t c t
-> Proxy a' a c' c m r
-> Step (Exchange a' a t c) r (Proxy a' a c' c m r)
forall (k :: * -> *) o r t. (t -> r) -> k t -> r -> Step k o r
Await (\t
c' -> b' -> Proxy a' a b' b m r
fb' (b' -> Proxy a' a b' b m r)
-> Proxy b' b c' c m r -> Proxy a' a c' c m r
forall (m :: * -> *) b' a' a b r c' c.
Monad m =>
(b' -> Proxy a' a b' b m r)
-> Proxy b' b c' c m r -> Proxy a' a c' c m r
+>> t -> Proxy b' b c' c m r
k t
c') (c -> Exchange a' a t c t
forall b a' a b'. b -> Exchange a' a b' b b'
Respond c
c) (b' -> Proxy a' a b' b m r
fb' (b' -> Proxy a' a b' b m r)
-> Proxy b' b c' c m r -> Proxy a' a c' c m r
forall (m :: * -> *) b' a' a b r c' c.
Monad m =>
(b' -> Proxy a' a b' b m r)
-> Proxy b' b c' c m r -> Proxy a' a c' c m r
+>> Proxy b' b c' c m r
ff)
absurdExchange :: Exchange Void a b Void t -> c
absurdExchange :: Exchange Void a b Void t -> c
absurdExchange (Request Void
z) = Void -> c
forall a. Void -> a
absurd Void
z
absurdExchange (Respond Void
z) = Void -> c
forall a. Void -> a
absurd Void
z
runEffect :: Monad m => Effect m o -> m [o]
runEffect :: Effect m o -> m [o]
runEffect (MachineT m (Step (Exchange Void () () Void) o (Effect m o))
m) = m (Step (Exchange Void () () Void) o (Effect m o))
m m (Step (Exchange Void () () Void) o (Effect m o))
-> (Step (Exchange Void () () Void) o (Effect m o) -> m [o])
-> m [o]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Step (Exchange Void () () Void) o (Effect m o)
v ->
case Step (Exchange Void () () Void) o (Effect m o)
v of
Step (Exchange Void () () Void) o (Effect m o)
Stop -> [o] -> m [o]
forall (m :: * -> *) a. Monad m => a -> m a
return []
Yield o
o Effect m o
n -> ([o] -> [o]) -> m [o] -> m [o]
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (o
oo -> [o] -> [o]
forall a. a -> [a] -> [a]
:) (Effect m o -> m [o]
forall (m :: * -> *) o. Monad m => Effect m o -> m [o]
runEffect Effect m o
n)
Await t -> Effect m o
_ Exchange Void () () Void t
y Effect m o
_ -> Exchange Void () () Void t -> m [o]
forall a b t c. Exchange Void a b Void t -> c
absurdExchange Exchange Void () () Void t
y
runEffect_ :: Monad m => Effect m o -> m ()
runEffect_ :: Effect m o -> m ()
runEffect_ (MachineT m (Step (Exchange Void () () Void) o (Effect m o))
m) = m (Step (Exchange Void () () Void) o (Effect m o))
m m (Step (Exchange Void () () Void) o (Effect m o))
-> (Step (Exchange Void () () Void) o (Effect m o) -> m ()) -> m ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Step (Exchange Void () () Void) o (Effect m o)
v ->
case Step (Exchange Void () () Void) o (Effect m o)
v of
Step (Exchange Void () () Void) o (Effect m o)
Stop -> () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Yield o
_ Effect m o
n -> Effect m o -> m ()
forall (m :: * -> *) o. Monad m => Effect m o -> m ()
runEffect_ Effect m o
n
Await t -> Effect m o
_ Exchange Void () () Void t
y Effect m o
_ -> Exchange Void () () Void t -> m ()
forall a b t c. Exchange Void a b Void t -> c
absurdExchange Exchange Void () () Void t
y