-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Session Types for Haskell
--   
--   Session Types for Haskell. Allows the specification of communication
--   protocols and then validation that an implementation does not violate
--   said protocol.
@package sessions
@version 2008.2.22

module Control.Concurrent.Session

-- | Use OfferImpls to construct the implementations of the branches of an
--   offer. Really, it's just a slightly fancy list.
data OfferImpls :: * -> * -> * -> * -> * -> * -> *
OfferImplsNil :: OfferImpls Nil prog progOut progIn finalState finalResult
(~||~) :: (ProgramToMVarsOutgoing prog' progIn, Dual prog prog', Elem progIn l (MVar (ProgramCell (Cell incoming))), Elem progOut l (MVar (ProgramCell (Cell outgoing))), StripLeadingZeros b''1 y'1, Reverse' b'1 E b''1, DecrementRightToLeft a'1 b'1, Reverse' len'1 E a'1, ListLength st1 len'1, Elem prog' l st1, SmallerThan l len1, SNoJumpsBeyond prog' len1, ListLength prog' len1, SListOfSessionTypes prog', StripLeadingZeros b'' y', Reverse' b' E b'', DecrementRightToLeft a' b', Reverse' len' E a', ListLength st len', Elem prog l st, SmallerThan l len, SNoJumpsBeyond prog len, ListLength prog len, SListOfSessionTypes prog, ProgramToMVarsOutgoing prog progOut) => SessionChain prog progOut progIn (outgoing, incoming) finalState finalResult -> OfferImpls jumps prog progOut progIn finalState finalResult -> OfferImpls (Cons (Cons (Jump l) Nil) jumps) prog progOut progIn finalState finalResult

-- | Perform a jump. Now you may think that you should indicate where you
--   want to jump to. But of coures, that's actually specified by the
--   session type so you don't have to specify it at all in the
--   implementation.
sjump :: (Dual prog prog', ProgramToMVarsOutgoing prog progOut, ProgramToMVarsOutgoing prog' progIn, SWellFormedConfig l (D0 E) prog, SWellFormedConfig l (D0 E) prog', Elem progOut l (MVar (ProgramCell (Cell outgoing))), Elem progIn l (MVar (ProgramCell (Cell incoming)))) => (SessionChain prog progOut progIn) (Cons (Jump l) Nil, Cons (Jump l) Nil) (outgoing, incoming) ()

-- | Offer a number of branches. This is basically an external choice - the
--   other party uses <a>sselect</a> to decide which branch to take. Use
--   OfferImpls in order to construct the list of implementations of
--   branches. Note that every implementation must result in the same final
--   state and emit the same value.
soffer :: (Dual prog prog', ProgramToMVarsOutgoing prog progOut, ProgramToMVarsOutgoing prog' progIn) => OfferImpls jumps prog progOut progIn finalState finalResult -> (SessionChain prog progOut progIn) (Cons (Choice jumps) Nil, Cons (Choice jumps) Nil) finalState finalResult

-- | Select which branch we're taking at a branch point. Use a type number
--   (<a>Control.Concurrent.Session.Number</a>) to indicate the branch to
--   take.
sselect :: (Dual prog prog', ProgramToMVarsOutgoing prog progOut, ProgramToMVarsOutgoing prog' progIn, ListLength jumps len, SmallerThan label len, TypeNumberToInt label, Elem jumps label (Cons (Jump jumpTarget) Nil), SWellFormedConfig jumpTarget (D0 E) prog, SWellFormedConfig jumpTarget (D0 E) prog', Elem progOut jumpTarget (MVar (ProgramCell (Cell outgoing))), Elem progIn jumpTarget (MVar (ProgramCell (Cell incoming)))) => label -> (SessionChain prog progOut progIn) (Cons (Choice jumps) Nil, Cons (Choice jumps) Nil) (outgoing, incoming) ()

-- | Send a value to the other party. Of course, the value must be of the
--   correct type indicated in the session type.
ssend :: (Dual prog prog', ProgramToMVarsOutgoing prog progOut, ProgramToMVarsOutgoing prog' progIn) => t -> (SessionChain prog progOut progIn) (Cons t nxt, incoming) (nxt, incoming) ()

-- | Recieve a value from the other party. This will block as necessary.
--   The type of the value received is specified by the session type. No
--   magic coercion needed.
srecv :: (Dual prog prog', ProgramToMVarsOutgoing prog progOut, ProgramToMVarsOutgoing prog' progIn) => (SessionChain prog progOut progIn) (outgoing, Cons t nxt) (outgoing, nxt) t

-- | Run! Provide a program and a start point within that program (which
--   also then means that all implementations must start with
--   <a>sjump</a>), the two implementations which must be duals of each
--   other, run them, have them communicate, wait until they both finish
--   and die and then return the results from both of them.
run :: (Dual prog prog', Dual prog' prog, ProgramToMVarsOutgoing prog progOut, ProgramToMVarsOutgoing prog' progIn, SWellFormedConfig init (D0 E) prog, SWellFormedConfig init (D0 E) prog', Elem progOut init (MVar (ProgramCell (Cell fromO))), Elem progIn init (MVar (ProgramCell (Cell fromI)))) => prog -> init -> SessionChain prog progOut progIn (fromO, fromI) (toO, toI) res -> SessionChain prog' progIn progOut (fromI, fromO) (toO', toI') res' -> IO (res, res')
data End
data Send :: * -> *
Send :: t -> Send t
SendInt :: Send Int
SendBool :: Send Bool
SendChar :: Send Char
SendStr :: Send String
SendDouble :: Send Double
data Recv :: * -> *
Recv :: t -> Recv t
RecvInt :: Recv Int
RecvBool :: Recv Bool
RecvChar :: Recv Char
RecvStr :: Recv String
RecvDouble :: Recv Double
data Jump l
data Select :: * -> *
data Offer :: * -> *
jump :: (TyNum n) => n -> Cons (Jump n) Nil
end :: Cons End Nil
select :: (SListOfJumps (Cons val nxt)) => (Cons val nxt) -> Cons (Select (Cons val nxt)) Nil
offer :: (SListOfJumps (Cons val nxt)) => (Cons val nxt) -> Cons (Offer (Cons val nxt)) Nil
class Dual a b | a -> b, b -> a
dual :: (Dual a b) => a -> b
(~>) :: (TyList nxt, SNonTerminal a, SValidSessionType nxt) => a -> nxt -> (Cons a nxt)
(~|~) :: (TyNum target, TyList nxt) => target -> nxt -> Cons (Cons (Jump target) Nil) nxt
class SWellFormedConfig idxA idxB ss
testWellformed :: (SWellFormedConfig idxA idxB ss) => ss -> idxA -> idxB -> Bool
data Cons :: * -> * -> *
cons :: (TyList n) => t -> n -> (Cons t n)
data Nil :: *
nil :: Nil
data E
E :: E
data D0 n
D0 :: n -> D0 n
data D1 n
D1 :: n -> D1 n
data D2 n
D2 :: n -> D2 n
data D3 n
D3 :: n -> D3 n
data D4 n
D4 :: n -> D4 n
data D5 n
D5 :: n -> D5 n
data D6 n
D6 :: n -> D6 n
data D7 n
D7 :: n -> D7 n
data D8 n
D8 :: n -> D8 n
data D9 n
D9 :: n -> D9 n
newtype SChain m x y a
SChain :: (x -> m (a, y)) -> SChain m x y a
runSChain :: SChain m x y a -> x -> m (a, y)

-- | An extension of the typical Monad such that you track additional
--   <tt>from</tt> and <tt>to</tt> parameters. Thus you can think of this
--   like <a>State</a> where the type of the <a>State</a> varies.
class SMonad m :: (* -> * -> * -> *)
(~>>) :: (SMonad m) => m x y a -> m y z b -> m x z b
(~>>=) :: (SMonad m) => m x y a -> (a -> m y z b) -> m x z b
sreturn :: (SMonad m) => a -> m x x a
newtype SStateT s m x y a
SStateT :: (s -> m x y (a, s)) -> SStateT s m x y a
runSStateT :: SStateT s m x y a -> s -> m x y (a, s)
class SMonadTrans t
slift :: (SMonadTrans t, SMonad m) => m x y a -> t m x y a
class (SMonad m) => SMonadIO m
sliftIO :: (SMonadIO m) => IO a -> m x x a
class (SMonad m) => SMonadState s m | m -> s
sget :: (SMonadState s m) => m x x s
sput :: (SMonadState s m) => s -> m x x ()