module FullSession.SMonad where
import FullSession.Base
import FullSession.Types
import FullSession.Ended
newtype Session t ss tt a = Session { session :: ss -> IO (tt,a) }
(>>>=) :: Session t ss tt a -> (a -> Session t tt uu b) -> Session t ss uu b
(Session m) >>>= f = Session (\ss -> m ss >>= \(tt,x) -> session (f x) tt)
(>>>) :: Session t ss tt a -> Session t tt uu b -> Session t ss uu b
(Session m) >>> (Session n) = Session (\ss -> m ss >>= \(tt,_) -> n tt)
ireturn :: a -> Session t ss ss a
ireturn a = Session (\ss -> return (ss, a))
runS :: Ended n ss => forall a n. (forall t. Session t Nil ss a) -> IO a
runS s = case s of Session m -> m Nil >>= \(_,a) -> return a
typecheck1
:: (Length ss l) =>
(Channel t l -> Session t (ss:>s) ss' a)
-> Session t (ss:>s) ss' a
typecheck1 = error "ERROR - for type checking purpose only!"
typecheck2
:: (Length ss l) =>
(Channel t (S l) -> Channel t l -> Session t (ss:>s1:>s2) ss' a)
-> Session t (ss:>s1:>s2) ss' a
typecheck2 = error "ERROR - for type checking purpose only!"
inspect1 :: Length tt l => (Channel t l -> Session t ss ss () -> Session t (tt:>t1) tt' a) -> (ss, Session t (tt:>t1) tt' a)
inspect1 = undefined