module Control.Proxy.Core.Correct (
ProxyCorrect(..),
ProxyF(..),
runProxy,
runProxyK,
runPipe
) where
import Control.Applicative (Applicative(pure, (<*>)))
import Control.Monad.IO.Class (MonadIO(liftIO))
import Control.Monad.Trans.Class (MonadTrans(lift))
import Control.MFunctor (MFunctor(hoist))
import Control.Proxy.Class
import Control.Proxy.Synonym (C)
data ProxyCorrect a' a b' b m r =
Proxy { unProxy :: m (ProxyF a' a b' b r (ProxyCorrect a' a b' b m r)) }
data ProxyF a' a b' b r x
= Request a' (a -> x)
| Respond b (b' -> x)
| Pure r
instance (Monad m) => Functor (ProxyCorrect a' a b' b m) where
fmap f p0 = go p0 where
go p = Proxy (do
x <- unProxy p
return (case x of
Request a' fa -> Request a' (\a -> go (fa a ))
Respond b fb' -> Respond b (\b' -> go (fb' b'))
Pure r -> Pure (f r) ) )
instance (Monad m) => Applicative (ProxyCorrect a' a b' b m) where
pure r = Proxy (return (Pure r))
pf <*> px = go pf where
go p = Proxy (do
x <- unProxy p
case x of
Request a' fa -> return (Request a' (\a -> go (fa a )))
Respond b fb' -> return (Respond b (\b' -> go (fb' b')))
Pure f -> unProxy (fmap f px) )
instance (Monad m) => Monad (ProxyCorrect a' a b' b m) where
return = \r -> Proxy (return (Pure r))
p0 >>= f = go p0 where
go p = Proxy (do
x <- unProxy p
case x of
Request a' fa -> return (Request a' (\a -> go (fa a )))
Respond b fb' -> return (Respond b (\b' -> go (fb' b')))
Pure r -> unProxy (f r) )
instance MonadTrans (ProxyCorrect a' a b' b) where
lift = lift_P
instance (MonadIO m) => MonadIO (ProxyCorrect a' a b' b m) where
liftIO m = Proxy (liftIO (m >>= \r -> return (Pure r)))
instance MonadIOP ProxyCorrect where
liftIO_P = liftIO
instance Proxy ProxyCorrect where
fb'_0 >-> fc' = \c' -> fb'_0 >-| fc' c' where
fb' >-| p1 = Proxy (do
x <- unProxy p1
case x of
Request b' fb -> unProxy (fb' b' |-> fb)
Respond c fc' -> return (Respond c (\c' -> fb' >-| fc' c'))
Pure r -> return (Pure r) )
p2 |-> fb = Proxy (do
x <- unProxy p2
case x of
Request a' fa -> return (Request a' (\a -> fa a |-> fb))
Respond b fb' -> unProxy (fb' >-| fb b)
Pure r -> return (Pure r) )
fa_0 >~> fb_0 = \a -> fa_0 a |-> fb_0 where
fb' >-| p1 = Proxy (do
x <- unProxy p1
case x of
Request b' fb -> unProxy (fb' b' |-> fb)
Respond c fc' -> return (Respond c (\c' -> fb' >-| fc' c'))
Pure r -> return (Pure r) )
p2 |-> fb = Proxy (do
x <- unProxy p2
case x of
Request a' fa -> return (Request a' (\a -> fa a |-> fb))
Respond b fb' -> unProxy (fb' >-| fb b)
Pure r -> return (Pure r) )
request a' = Proxy (return (Request a' (\a -> Proxy (return (Pure a )))))
respond b = Proxy (return (Respond b (\b' -> Proxy (return (Pure b')))))
return_P = return
(?>=) = (>>=)
lift_P m = Proxy (m >>= \r -> return (Pure r))
hoist_P = hoist
instance Interact ProxyCorrect where
k2 \>\ k1 = \a' -> go (k1 a') where
go p = Proxy (do
x <- unProxy p
case x of
Request b' fb -> unProxy (k2 b' >>= \b -> go (fb b))
Respond x fx' -> return (Respond x (\x' -> go (fx' x')))
Pure a -> return (Pure a) )
k2 />/ k1 = \a' -> go (k2 a') where
go p = Proxy (do
x <- unProxy p
case x of
Request x' fx -> return (Request x' (\x -> go (fx x)))
Respond b fb' -> unProxy (k1 b >>= \b' -> go (fb' b'))
Pure a -> return (Pure a) )
instance MFunctor (ProxyCorrect a' a b' b) where
hoist nat p0 = go p0 where
go p = Proxy (nat (do
x <- unProxy p
return (case x of
Request a' fa -> Request a' (\a -> go (fa a ))
Respond b fb' -> Respond b (\b' -> go (fb' b'))
Pure r -> Pure r )))
runProxy :: (Monad m) => (() -> ProxyCorrect a' () () b m r) -> m r
runProxy k = go (k ()) where
go p = do
x <- unProxy p
case x of
Request _ fa -> go (fa ())
Respond _ fb' -> go (fb' ())
Pure r -> return r
runProxyK :: (Monad m) => (() -> ProxyCorrect a' () () b m r) -> (() -> m r)
runProxyK p = \() -> runProxy p
runPipe :: (Monad m) => ProxyCorrect a' () () b m r -> m r
runPipe p = runProxy (\_ -> p)