sessions-2008.5.12: Session Types for HaskellSource codeContentsIndex
Control.Concurrent.Session
Description
This is just a convenience module that reexports everything you're expected to need.
Synopsis
data True = TT
data False = FF
data OfferImpls where
OfferImplsNil :: OfferImpls Nil prog prog' finalState finalResult
(~||~) :: forall prog prog' progOut progIn outgoing incoming finalState finalResult jumps l current currentUX. (ProgramToMVarsOutgoingT prog prog ~ progOut, ProgramToMVarsOutgoingT prog' prog' ~ progIn, ProgramToMVarsOutgoing prog prog progOut, ProgramToMVarsOutgoing prog' prog' progIn, SWellFormedConfig l (D0 E) prog, SWellFormedConfig l (D0 E) prog', TyListIndex progOut l (MVar (ProgramCell (Cell outgoing))), TyListIndex progIn l (MVar (ProgramCell (Cell incoming))), TyListIndex prog l currentUX, Expand prog currentUX current) => SessionChain prog prog' (current, outgoing, incoming) finalState finalResult -> OfferImpls jumps prog prog' finalState finalResult -> OfferImpls (Cons (Cons (Jump l) Nil) jumps) prog prog' finalState finalResult
sjump :: forall l prog prog' progOut progIn outgoing incoming current currentUX. (ProgramToMVarsOutgoingT prog prog ~ progOut, ProgramToMVarsOutgoingT prog' prog' ~ progIn, SWellFormedConfig l (D0 E) prog, SWellFormedConfig l (D0 E) prog', TyListIndex progOut l (MVar (ProgramCell (Cell outgoing))), TyListIndex progIn l (MVar (ProgramCell (Cell incoming))), TyListIndex prog l currentUX, Expand prog currentUX current) => SessionChain prog prog' (Cons (Jump l) Nil, Cons (Jump l) Nil, Cons (Jump l) Nil) (current, outgoing, incoming) ()
soffer :: forall current outgoing incoming finalResult prog prog' jumps. OfferImpls jumps prog prog' (current, outgoing, incoming) finalResult -> SessionChain prog prog' (Cons (Offer jumps) Nil, Cons (Choice jumps) Nil, Cons (Choice jumps) Nil) (current, outgoing, incoming) finalResult
sselect :: forall prog prog' progOut progIn label jumps outgoing incoming current currentUX len jumpTarget. (ProgramToMVarsOutgoingT prog prog ~ progOut, ProgramToMVarsOutgoingT prog' prog' ~ progIn, TyListLength jumps len, SmallerThanBool label len True, TypeNumberToInt label, TyListIndex jumps label (Cons (Jump jumpTarget) Nil), SWellFormedConfig jumpTarget (D0 E) prog, SWellFormedConfig jumpTarget (D0 E) prog', TyListIndex progOut jumpTarget (MVar (ProgramCell (Cell outgoing))), TyListIndex progIn jumpTarget (MVar (ProgramCell (Cell incoming))), TyListIndex prog jumpTarget currentUX, Expand prog currentUX current) => label -> SessionChain prog prog' (Cons (Select jumps) Nil, Cons (Choice jumps) Nil, Cons (Choice jumps) Nil) (current, outgoing, incoming) ()
ssend :: forall t t' sp prog prog' nxtCur nxtOut incoming. CompatibleTypes sp t' t => t' -> SessionChain prog prog' (Cons (Send (sp, t)) nxtCur, Cons t nxtOut, incoming) (nxtCur, nxtOut, incoming) ()
srecv :: forall sp t prog prog' nxt nxt' outgoing. SessionChain prog prog' (Cons (Recv (sp, t)) nxt, outgoing, Cons t nxt') (nxt, outgoing, nxt') t
run :: forall prog prog' progOut progIn init fromO fromI toO toI res res' currentUX currentUX' current current' toCur toCur'. (ProgramToMVarsOutgoing prog prog progOut, ProgramToMVarsOutgoing prog' prog' progIn, ProgramToMVarsOutgoingT prog prog ~ progOut, ProgramToMVarsOutgoingT prog' prog' ~ progIn, SWellFormedConfig init (D0 E) prog, SWellFormedConfig init (D0 E) prog', TyListIndex progOut init (MVar (ProgramCell (Cell fromO))), TyListIndex progIn init (MVar (ProgramCell (Cell fromI))), DualT prog ~ prog', Dual prog prog', TyListIndex prog init currentUX, Expand prog currentUX current, TyListIndex prog' init currentUX', Expand prog' currentUX' current') => prog -> init -> SessionChain prog prog' (current, fromO, fromI) (toCur, toO, toI) res -> SessionChain prog' prog (current', fromI, fromO) (toCur', toI, toO) res' -> IO (res, res')
data End
data Send t = Send t
data Recv t = Recv t
sendPid :: (TyList f, TyList fs, TyListSortNums lst lst') => lst -> SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs)) (TypeState nxtLabel declareable useable (Cons (label, Cons (SendPid False lst') f) fs)) ()
recvPid :: (TyList f, TyList fs, TyListSortNums lst lst') => lst -> SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs)) (TypeState nxtLabel declareable useable (Cons (label, Cons (RecvPid False lst') f) fs)) ()
sendSession :: (TyList f, TyList fs, TyList fs', TyListReverse frag fragRev, TyListTake (D1 E) fragRev (Cons (label, fragHead) Nil), TyListDrop (D1 E) fragRev fragTailRev, TyListReverse fragTailRev fragTail, TyListAppend fragTail fs fs') => SessionType (TypeState nxtLabel declareable useable (Cons (label, Nil) Nil)) (TypeState nxtLabel' declareable' useable' frag) res -> SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs)) (TypeState nxtLabel' declareable' useable' (Cons (label, Cons (SendSession False fragHead) f) fs')) res
recvSession :: (TyList f, TyList fs, TyList fs', TyListReverse frag fragRev, TyListTake (D1 E) fragRev (Cons (label, fragHead) Nil), TyListDrop (D1 E) fragRev fragTailRev, TyListReverse fragTailRev fragTail, TyListAppend fragTail fs fs') => SessionType (TypeState nxtLabel declareable useable (Cons (label, Nil) Nil)) (TypeState nxtLabel' declareable' useable' frag) res -> SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs)) (TypeState nxtLabel' declareable' useable' (Cons (label, Cons (RecvSession False fragHead) f) fs')) res
data Jump l
data Select
data Offer
jump :: (TyListReverse (Cons (Jump jt) f) f', TyList f, TyList fs, TyListMember useable jt True) => jt -> SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs)) (TypeState nxtLabel declareable useable (Cons (label, f') fs)) ()
end :: (TyListReverse (Cons End f) f', TyList f, TyList fs) => SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs)) (TypeState nxtLabel declareable useable (Cons (label, f') fs)) ()
select :: forall f f' fs listOfRes listOfJumps label nxtLabel declareable useable to finalTo. (TyListReverse (Cons (Select listOfJumps) f) f', TyList f, TyList fs, BuildBranches (BranchesList listOfRes listOfJumps (TypeState nxtLabel declareable useable (Cons (label, f') fs)) to finalTo) (SessionType (TypeState nxtLabel declareable useable (Cons (label, f') fs)) finalTo (listOfRes, listOfJumps))) => BranchesList listOfRes listOfJumps (TypeState nxtLabel declareable useable (Cons (label, f') fs)) to finalTo -> SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs)) finalTo listOfRes
offer :: forall f f' fs listOfRes listOfJumps label nxtLabel declareable useable to finalTo. (TyListReverse (Cons (Offer listOfJumps) f) f', TyList f, TyList fs, BuildBranches (BranchesList listOfRes listOfJumps (TypeState nxtLabel declareable useable (Cons (label, f') fs)) to finalTo) (SessionType (TypeState nxtLabel declareable useable (Cons (label, f') fs)) finalTo (listOfRes, listOfJumps))) => BranchesList listOfRes listOfJumps (TypeState nxtLabel declareable useable (Cons (label, f') fs)) to finalTo -> SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs)) finalTo listOfRes
(~>) :: (TyList nxt, SNonTerminal a, SValidSessionType nxt) => a -> nxt -> Cons a nxt
(~|~) :: (Succ label nxtLabel, TyListConsSet label declareable declareable', TyListElem declareable' label idx, TyListDelete declareable' idx declareable'', TyListConsSet label useable useable', TyList st, TyListMember declareable' label True, TyList labs, TyList resLst) => SessionType (TypeState nxtLabel declareable'' useable' (Cons (label, Nil) st)) (TypeState nxtLabel' declareable''' useable'' st') res -> BranchesList resLst labs (TypeState nxtLabel' declareable''' useable'' st') to finalTo -> BranchesList (Cons res resLst) (Cons (Cons (Jump label) Nil) labs) (TypeState label declareable useable st) (TypeState nxtLabel' declareable''' useable'' st', to) finalTo
class SWellFormedConfig idxA idxB ss
testWellformed :: SWellFormedConfig idxA idxB ss => ss -> idxA -> idxB -> Bool
data SessionChain prog prog' from to res
(.=) :: (TyListMember declareable label True, TyListElem declareable label idx, TyListDelete declareable idx declareable', TyList st) => label -> SessionType (TypeState nxtLabel declareable' useable (Cons (label, Nil) st)) (TypeState nxtLabel' declareable'' useable' st') a -> SessionType (TypeState nxtLabel declareable useable st) (TypeState nxtLabel' declareable'' useable' st') a
dual :: True
notDual :: False
newLabel :: (Succ nxtLabel nxtLabel', TyListConsSet nxtLabel declareable declareable', TyListConsSet nxtLabel useable useable') => SessionType (TypeState nxtLabel declareable useable st) (TypeState nxtLabel' declareable' useable' st) nxtLabel
send :: (TyList f, TyList fs) => t -> SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs)) (TypeState nxtLabel declareable useable (Cons (label, Cons (Send (SpecialNormal, t)) f) fs)) ()
recv :: (TyList f, TyList fs) => t -> SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs)) (TypeState nxtLabel declareable useable (Cons (label, Cons (Recv (SpecialNormal, t)) f) fs)) ()
makeSessionType :: (TyListSortNums st st', TyListSnd st' st'') => SessionType (TypeState (D0 E) Nil Nil Nil) (TypeState nxtLabel Nil useable st) res -> (st'', res)
currentLabel :: SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs)) (TypeState nxtLabel declareable useable (Cons (label, f) fs)) label
data BranchesList where
BLNil :: BranchesList Nil Nil z z z
data Cons
cons :: TyList n => t -> n -> Cons t n
data Nil
nil :: Nil
data E = E
data D0 n = D0 n
data D1 n = D1 n
data D2 n = D2 n
data D3 n = D3 n
data D4 n = D4 n
data D5 n = D5 n
data D6 n = D6 n
data D7 n = D7 n
data D8 n = D8 n
data D9 n = D9 n
module Control.Concurrent.Session.Base.SMonad
emptyMap :: TyMap Nil Nil
data Pid
data InterleavedChain internalPid from to res
class CreateSession invert init prog prog' sessionsToIdxMe sessionsToIdxThem idxsToPairStructsMe idxsToPairStructsThem keyToIdxMe idxToValueMe keyToIdxMe' idxToValueMe' idxOfThem invertedSessionsMe invertedSessionsThem where
createSession :: init -> invert -> Pid prog prog' invertedSessionsThem sessionsToIdxThem idxsToPairStructsThem -> InterleavedChain (InternalPid prog prog' invertedSessionsMe sessionsToIdxMe idxsToPairStructsMe) (TyMap keyToIdxMe idxToValueMe) (TyMap keyToIdxMe' idxToValueMe') idxOfThem
myPid :: InterleavedChain (InternalPid prog prog' invertedSessions sessionsToIdx idxsToPairStructs) from from (Pid prog prog' invertedSessions sessionsToIdx idxsToPairStructs)
class PidEq a b where
(=~=) :: a -> b -> Bool
data MultiReceive where
MultiReceiveNil :: MultiReceive Nil prog prog' invertedSessions sessionsToIdx idxsToPairStructs keyToIdx idxToValue keyToIdx' idxToValue' res
(~|||~) :: MapLookup (TyMap keyToIdx idxToValue) ch (SessionState progS progS' (Cons (Recv (sp, t)) nxt, fromO, Cons t nxt')) => (ch, InterleavedChain (InternalPid prog prog' invertedSessions sessionsToIdx idxsToPairStructs) (TyMap keyToIdx idxToValue) (TyMap keyToIdx' idxToValue') res) -> MultiReceive chs prog prog' invertedSessions sessionsToIdx idxsToPairStructs keyToIdx idxToValue keyToIdx' idxToValue' res -> MultiReceive (Cons ch chs) prog prog' invertedSessions sessionsToIdx idxsToPairStructs keyToIdx idxToValue keyToIdx' idxToValue' res
multiReceive :: forall chs len keyToIdx idxToValue prog prog' invertedSessions sessionsToIdx idxsToPairStructs keyToIdx' idxToValue' res. (TyListLength chs len, SmallerThanBool (D0 E) len True, SetIncomingNotify (TyMap keyToIdx idxToValue) chs, FindNonEmptyIncoming (TyMap keyToIdx idxToValue) chs, TypeNumberToInt len) => MultiReceive chs prog prog' invertedSessions sessionsToIdx idxsToPairStructs keyToIdx idxToValue keyToIdx' idxToValue' res -> InterleavedChain (InternalPid prog prog' invertedSessions sessionsToIdx idxsToPairStructs) (TyMap keyToIdx idxToValue) (TyMap keyToIdx' idxToValue') res
module Control.Concurrent.Session.Interleaving
module Control.Concurrent.Session.Network.Socket
Documentation
data True Source
Constructors
TT
show/hide Instances
Show True
Not False True
Not True False
Or False True True
Or True y True
And True False False
And True True True
TySubList Nil b True
If True x y x
TyListConsSet' True e set set
SmallerThanBool' x y True False False
SmallerThanBool' x y False True True
SmallerThanBool x y res => SmallerThanBool' x y True True res
(ProgramToMVarsOutgoingT prog prog ~ progOut, ProgramToMVarsOutgoingT prog' prog' ~ progIn, DualT prog ~ prog', ProgramToMVarsOutgoing prog prog progOut, ProgramToMVarsOutgoing prog' prog' progIn, SWellFormedConfig init (D0 E) prog, SWellFormedConfig init (D0 E) prog', TyListIndex progOut init (MVar (ProgramCell (Cell fromO))), TyListIndex progIn init (MVar (ProgramCell (Cell fromI))), TyListIndex prog init currentUX, Expand prog currentUX current, Dual prog prog', TyListIndex prog' init currentUX', Expand prog' currentUX' current', MapSize (TyMap keyToIdxMe idxToValueMe) idxOfThem, MapInsert (TyMap keyToIdxMe idxToValueMe) idxOfThem (SessionState prog' prog ((,,) current' fromI fromO)) (TyMap keyToIdxMe' idxToValueMe'), BuildNetworkRunner prog prog' ((,,) toCur toO toI) () prog init, NetworkRuntime prog prog' ((,,) current fromO fromI) ((,,) toCur toO toI) (), TyListMember invertedSessionsMe init True) => CreateSessionOverNetwork True init prog prog' invertedSessionsMe sessionsToIdxMe idxsToPairStructsMe keyToIdxMe idxToValueMe keyToIdxMe' idxToValueMe' idxOfThem
(ProgramToMVarsOutgoingT prog prog ~ progOut, ProgramToMVarsOutgoingT prog' prog' ~ progIn, ProgramToMVarsOutgoing prog prog progOut, ProgramToMVarsOutgoing prog' prog' progIn, SWellFormedConfig init (D0 E) prog, SWellFormedConfig init (D0 E) prog', TyListIndex progOut init (MVar (ProgramCell (Cell fromO))), TyListIndex progIn init (MVar (ProgramCell (Cell fromI))), TyListIndex prog init currentUX, Expand prog currentUX current, TyListIndex prog' init currentUX', Expand prog' currentUX' current', MapLookup (TyMap sessionsToIdxThem idxsToPairStructsThem) init (MVar (Map ((,) RawPid RawPid) (MVar (PairStruct init prog prog' ((,,) (Cons (Jump init) Nil) (Cons (Jump init) Nil) (Cons (Jump init) Nil)))))), TyListMember invertedSessionsMe init True, MapSize (TyMap keyToIdxMe idxToValueMe) idxOfThem, MapInsert (TyMap keyToIdxMe idxToValueMe) idxOfThem (SessionState prog' prog ((,,) current' fromI fromO)) (TyMap keyToIdxMe' idxToValueMe')) => CreateSession True init prog prog' sessionsToIdxMe sessionsToIdxThem idxsToPairStructsMe idxsToPairStructsThem keyToIdxMe idxToValueMe keyToIdxMe' idxToValueMe' idxOfThem invertedSessionsMe invertedSessionsThem
(ProgramToMVarsOutgoingT prog prog ~ progOut, ProgramToMVarsOutgoingT prog' prog' ~ progIn, ProgramToMVarsOutgoing prog prog progOut, ProgramToMVarsOutgoing prog' prog' progIn, SWellFormedConfig init (D0 E) prog, SWellFormedConfig init (D0 E) prog', TyListIndex progOut init (MVar (ProgramCell (Cell fromO))), TyListIndex progIn init (MVar (ProgramCell (Cell fromI))), TyListIndex prog init currentUX, TyListIndex prog' init currentUX', Expand prog currentUX current, Expand prog' currentUX' current', BuildPidTyMap prog sessionsListSorted (TyMap sessionsToIdxThem idxsToPairStructsThem), BuildInvertedSessionsSet sessionsListSorted invertedSessionsThem, TyListSortNums sessionsList sessionsListSortedRev, TyListReverse sessionsListSortedRev sessionsListSorted, MapSize (TyMap keyToIdxMe idxToValueMe) idxOfChild, MapInsert (TyMap keyToIdxMe idxToValueMe) idxOfChild (SessionState prog' prog ((,,) current' fromI fromO)) (TyMap keyToIdxMe' idxToValueMe'), MapInsert (TyMap Nil Nil) (D0 E) (SessionState prog prog' ((,,) current fromO fromI)) (TyMap keyToIdxChild' idxToValueChild')) => Fork True init sessionsList prog prog' sessionsToIdxThem idxsToPairStructsThem sessionsToIdxMe idxsToPairStructsMe fromO fromI progOut progIn keyToIdxMe idxToValueMe keyToIdxMe' idxToValueMe' keyToIdxChild' idxToValueChild' keyToIdxChild'' idxToValueChild'' idxOfChild current current' currentUX currentUX' invertedSessionsMe invertedSessionsThem
TyList lstA => Insert' True num val lstA (Cons ((,) num val) lstA)
Pred (D9 a) x' => Pred' (D9 a) x' True
Pred (D8 a) x' => Pred' (D8 a) x' True
Pred (D7 a) x' => Pred' (D7 a) x' True
Pred (D6 a) x' => Pred' (D6 a) x' True
Pred (D5 a) x' => Pred' (D5 a) x' True
Pred (D4 a) x' => Pred' (D4 a) x' True
Pred (D3 a) x' => Pred' (D3 a) x' True
Pred (D2 a) x' => Pred' (D2 a) x' True
Pred (D1 a) x' => Pred' (D1 a) x' True
TyListMember (Cons val nxt) val True
data False Source
Constructors
FF
show/hide Instances
Show False
Not False True
Not True False
Or False False False
Or False True True
And False y False
And True False False
TyListMember Nil val False
If False x y y
SmallerThanBool' x y False False False
SmallerThanBool' x y True False False
SmallerThanBool' x y False True True
(ProgramToMVarsOutgoingT prog prog ~ progOut, ProgramToMVarsOutgoingT prog' prog' ~ progIn, DualT prog ~ prog', ProgramToMVarsOutgoing prog prog progOut, ProgramToMVarsOutgoing prog' prog' progIn, SWellFormedConfig init (D0 E) prog, SWellFormedConfig init (D0 E) prog', TyListIndex progOut init (MVar (ProgramCell (Cell fromO))), TyListIndex progIn init (MVar (ProgramCell (Cell fromI))), TyListIndex prog init currentUX, Expand prog currentUX current, Dual prog prog', TyListIndex prog' init currentUX', Expand prog' currentUX' current', MapSize (TyMap keyToIdxMe idxToValueMe) idxOfThem, MapInsert (TyMap keyToIdxMe idxToValueMe) idxOfThem (SessionState prog prog' ((,,) current fromO fromI)) (TyMap keyToIdxMe' idxToValueMe'), BuildNetworkRunner prog' prog ((,,) toCur toI toO) () prog' init, NetworkRuntime prog' prog ((,,) current' fromI fromO) ((,,) toCur toI toO) (), MapLookup (TyMap sessionsToIdxMe idxsToPairStructsMe) init (MVar (Map ((,) RawPid RawPid) (MVar (PairStruct init prog prog' ((,,) (Cons (Jump init) Nil) (Cons (Jump init) Nil) (Cons (Jump init) Nil))))))) => CreateSessionOverNetwork False init prog prog' invertedSessionsMe sessionsToIdxMe idxsToPairStructsMe keyToIdxMe idxToValueMe keyToIdxMe' idxToValueMe' idxOfThem
(ProgramToMVarsOutgoingT prog prog ~ progOut, ProgramToMVarsOutgoingT prog' prog' ~ progIn, SWellFormedConfig init (D0 E) prog, SWellFormedConfig init (D0 E) prog', TyListIndex progOut init (MVar (ProgramCell (Cell fromO))), TyListIndex progIn init (MVar (ProgramCell (Cell fromI))), TyListIndex prog init current', Expand prog current' current, MapLookup (TyMap sessionsToIdxMe idxsToPairStructsMe) init (MVar (Map ((,) RawPid RawPid) (MVar (PairStruct init prog prog' ((,,) (Cons (Jump init) Nil) (Cons (Jump init) Nil) (Cons (Jump init) Nil)))))), TyListMember invertedSessionsThem init True, MapSize (TyMap keyToIdxMe idxToValueMe) idxOfThem, MapInsert (TyMap keyToIdxMe idxToValueMe) idxOfThem (SessionState prog prog' ((,,) current fromO fromI)) (TyMap keyToIdxMe' idxToValueMe')) => CreateSession False init prog prog' sessionsToIdxMe sessionsToIdxThem idxsToPairStructsMe idxsToPairStructsThem keyToIdxMe idxToValueMe keyToIdxMe' idxToValueMe' idxOfThem invertedSessionsMe invertedSessionsThem
(ProgramToMVarsOutgoingT prog prog ~ progOut, ProgramToMVarsOutgoingT prog' prog' ~ progIn, ProgramToMVarsOutgoing prog prog progOut, ProgramToMVarsOutgoing prog' prog' progIn, SWellFormedConfig init (D0 E) prog, SWellFormedConfig init (D0 E) prog', TyListIndex progOut init (MVar (ProgramCell (Cell fromO))), TyListIndex progIn init (MVar (ProgramCell (Cell fromI))), TyListIndex prog init currentUX, TyListIndex prog' init currentUX', Expand prog currentUX current, Expand prog' currentUX' current', BuildPidTyMap prog sessionsListSorted (TyMap sessionsToIdxThem idxsToPairStructsThem), BuildInvertedSessionsSet sessionsListSorted invertedSessionsThem, TyListSortNums sessionsList sessionsListSortedRev, TyListReverse sessionsListSortedRev sessionsListSorted, MapSize (TyMap keyToIdxMe idxToValueMe) idxOfChild, MapInsert (TyMap keyToIdxMe idxToValueMe) idxOfChild (SessionState prog prog' ((,,) current fromO fromI)) (TyMap keyToIdxMe' idxToValueMe'), MapInsert (TyMap Nil Nil) (D0 E) (SessionState prog' prog ((,,) current' fromI fromO)) (TyMap keyToIdxChild' idxToValueChild')) => Fork False init sessionsList prog prog' sessionsToIdxThem idxsToPairStructsThem sessionsToIdxMe idxsToPairStructsMe fromO fromI progOut progIn keyToIdxMe idxToValueMe keyToIdxMe' idxToValueMe' keyToIdxChild' idxToValueChild' keyToIdxChild'' idxToValueChild'' idxOfChild current current' currentUX currentUX' invertedSessionsMe invertedSessionsThem
TyList set => TyListConsSet' False e set (Cons e set)
(Insert num val nxt lstB, TyList lstB) => Insert' False num val (Cons ((,) num' val') nxt) (Cons ((,) num' val') lstB)
(TyListLength keyToIdx newIdx, TyListReverse keyToIdx keyToIdxRev, TyListReverse (Cons key keyToIdxRev) keyToIdx', TyListUpdateVar idxToValue newIdx value idxToValue', TyList keyToIdxRev, MapDelete (TyMap keyToIdx' idxToValue') key (TyMap keyToIdx idxToValue)) => MapInsert' False (TyMap keyToIdx idxToValue) key value (TyMap keyToIdx' idxToValue')
Pred' (D0 E) y False
data OfferImpls whereSource
Use OfferImpls to construct the implementations of the branches of an offer. Really, it's just a slightly fancy list.
Constructors
OfferImplsNil :: OfferImpls Nil prog prog' finalState finalResult
(~||~) :: forall prog prog' progOut progIn outgoing incoming finalState finalResult jumps l current currentUX. (ProgramToMVarsOutgoingT prog prog ~ progOut, ProgramToMVarsOutgoingT prog' prog' ~ progIn, ProgramToMVarsOutgoing prog prog progOut, ProgramToMVarsOutgoing prog' prog' progIn, SWellFormedConfig l (D0 E) prog, SWellFormedConfig l (D0 E) prog', TyListIndex progOut l (MVar (ProgramCell (Cell outgoing))), TyListIndex progIn l (MVar (ProgramCell (Cell incoming))), TyListIndex prog l currentUX, Expand prog currentUX current) => SessionChain prog prog' (current, outgoing, incoming) finalState finalResult -> OfferImpls jumps prog prog' finalState finalResult -> OfferImpls (Cons (Cons (Jump l) Nil) jumps) prog prog' finalState finalResultSource
Use to construct OfferImpls. This function automatically adds the necessary sjump to the start of each branch implementation.
sjump :: forall l prog prog' progOut progIn outgoing incoming current currentUX. (ProgramToMVarsOutgoingT prog prog ~ progOut, ProgramToMVarsOutgoingT prog' prog' ~ progIn, SWellFormedConfig l (D0 E) prog, SWellFormedConfig l (D0 E) prog', TyListIndex progOut l (MVar (ProgramCell (Cell outgoing))), TyListIndex progIn l (MVar (ProgramCell (Cell incoming))), TyListIndex prog l currentUX, Expand prog currentUX current) => SessionChain prog prog' (Cons (Jump l) Nil, Cons (Jump l) Nil, Cons (Jump l) Nil) (current, outgoing, incoming) ()Source
Perform a jump. Now you may think that you should indicate where you want to jump to. But of course, that's actually specified by the session type so you don't have to specify it at all in the implementation.
soffer :: forall current outgoing incoming finalResult prog prog' jumps. OfferImpls jumps prog prog' (current, outgoing, incoming) finalResult -> SessionChain prog prog' (Cons (Offer jumps) Nil, Cons (Choice jumps) Nil, Cons (Choice jumps) Nil) (current, outgoing, incoming) finalResultSource
Offer a number of branches. This is basically an external choice - the other party uses sselect 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.
sselect :: forall prog prog' progOut progIn label jumps outgoing incoming current currentUX len jumpTarget. (ProgramToMVarsOutgoingT prog prog ~ progOut, ProgramToMVarsOutgoingT prog' prog' ~ progIn, TyListLength jumps len, SmallerThanBool label len True, TypeNumberToInt label, TyListIndex jumps label (Cons (Jump jumpTarget) Nil), SWellFormedConfig jumpTarget (D0 E) prog, SWellFormedConfig jumpTarget (D0 E) prog', TyListIndex progOut jumpTarget (MVar (ProgramCell (Cell outgoing))), TyListIndex progIn jumpTarget (MVar (ProgramCell (Cell incoming))), TyListIndex prog jumpTarget currentUX, Expand prog currentUX current) => label -> SessionChain prog prog' (Cons (Select jumps) Nil, Cons (Choice jumps) Nil, Cons (Choice jumps) Nil) (current, outgoing, incoming) ()Source
Select which branch we're taking at a branch point. Use a type number (Control.Concurrent.Session.Number) to indicate the branch to take.
ssend :: forall t t' sp prog prog' nxtCur nxtOut incoming. CompatibleTypes sp t' t => t' -> SessionChain prog prog' (Cons (Send (sp, t)) nxtCur, Cons t nxtOut, incoming) (nxtCur, nxtOut, incoming) ()Source
Send a value to the other party. Of course, the value must be of the correct type indicated in the session type.
srecv :: forall sp t prog prog' nxt nxt' outgoing. SessionChain prog prog' (Cons (Recv (sp, t)) nxt, outgoing, Cons t nxt') (nxt, outgoing, nxt') tSource
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.
run :: forall prog prog' progOut progIn init fromO fromI toO toI res res' currentUX currentUX' current current' toCur toCur'. (ProgramToMVarsOutgoing prog prog progOut, ProgramToMVarsOutgoing prog' prog' progIn, ProgramToMVarsOutgoingT prog prog ~ progOut, ProgramToMVarsOutgoingT prog' prog' ~ progIn, SWellFormedConfig init (D0 E) prog, SWellFormedConfig init (D0 E) prog', TyListIndex progOut init (MVar (ProgramCell (Cell fromO))), TyListIndex progIn init (MVar (ProgramCell (Cell fromI))), DualT prog ~ prog', Dual prog prog', TyListIndex prog init currentUX, Expand prog currentUX current, TyListIndex prog' init currentUX', Expand prog' currentUX' current') => prog -> init -> SessionChain prog prog' (current, fromO, fromI) (toCur, toO, toI) res -> SessionChain prog' prog (current', fromI, fromO) (toCur', toI, toO) res' -> IO (res, res')Source
Run! Provide a program and a start point within that program (which is automatically sjumped to), 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.
data End Source
show/hide Instances
data Send t Source
Constructors
Send t
show/hide Instances
(Outgoing current ~ outgoing, Outgoing current' ~ incoming, Dual prog prog', Expand prog' frag current, Dual frag frag', Expand prog' frag' current') => ExpandSession prog (SendSession True frag) (Send ((,) SpecialSession (SessionState prog' prog ((,,) current outgoing incoming))))
(Outgoing current ~ outgoing, Outgoing current' ~ incoming, Dual prog prog', Expand prog frag current, Dual frag frag', Expand prog frag' current') => ExpandSession prog (SendSession False frag) (Send ((,) SpecialSession (SessionState prog prog' ((,,) current outgoing incoming))))
(Dual prog prog', BuildInvertedSessionsSet idxs invertedSessions, BuildPidTyMap prog' idxs (TyMap sessionsToIdx idxsToPairStructs)) => ExpandPid prog (SendPid True idxs) (Send ((,) SpecialPid (Pid prog' prog invertedSessions sessionsToIdx idxsToPairStructs)))
(Dual prog prog', BuildInvertedSessionsSet idxs invertedSessions, BuildPidTyMap prog idxs (TyMap sessionsToIdx idxsToPairStructs)) => ExpandPid prog (SendPid False idxs) (Send ((,) SpecialPid (Pid prog prog' invertedSessions sessionsToIdx idxsToPairStructs)))
SNonTerminal (Send t)
SNoJumpsBeyond (Send t) idx
Dual (Recv t) (Send t)
Dual (Send t) (Recv t)
data Recv t Source
Constructors
Recv t
show/hide Instances
(Outgoing current ~ outgoing, Outgoing current' ~ incoming, Dual prog prog', Expand prog' frag current, Dual frag frag', Expand prog' frag' current') => ExpandSession prog (RecvSession True frag) (Recv ((,) SpecialSession (SessionState prog' prog ((,,) current outgoing incoming))))
(Outgoing current ~ outgoing, Outgoing current' ~ incoming, Dual prog prog', Expand prog frag current, Dual frag frag', Expand prog frag' current') => ExpandSession prog (RecvSession False frag) (Recv ((,) SpecialSession (SessionState prog prog' ((,,) current outgoing incoming))))
(Dual prog prog', BuildInvertedSessionsSet idxs invertedSessions, BuildPidTyMap prog' idxs (TyMap sessionsToIdx idxsToPairStructs)) => ExpandPid prog (RecvPid True idxs) (Recv ((,) SpecialPid (Pid prog' prog invertedSessions sessionsToIdx idxsToPairStructs)))
(Dual prog prog', BuildInvertedSessionsSet idxs invertedSessions, BuildPidTyMap prog idxs (TyMap sessionsToIdx idxsToPairStructs)) => ExpandPid prog (RecvPid False idxs) (Recv ((,) SpecialPid (Pid prog prog' invertedSessions sessionsToIdx idxsToPairStructs)))
SNonTerminal (Recv t)
SNoJumpsBeyond (Recv t) idx
Dual (Recv t) (Send t)
Dual (Send t) (Recv t)
sendPid :: (TyList f, TyList fs, TyListSortNums lst lst') => lst -> SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs)) (TypeState nxtLabel declareable useable (Cons (label, Cons (SendPid False lst') f) fs)) ()Source
recvPid :: (TyList f, TyList fs, TyListSortNums lst lst') => lst -> SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs)) (TypeState nxtLabel declareable useable (Cons (label, Cons (RecvPid False lst') f) fs)) ()Source
sendSession :: (TyList f, TyList fs, TyList fs', TyListReverse frag fragRev, TyListTake (D1 E) fragRev (Cons (label, fragHead) Nil), TyListDrop (D1 E) fragRev fragTailRev, TyListReverse fragTailRev fragTail, TyListAppend fragTail fs fs') => SessionType (TypeState nxtLabel declareable useable (Cons (label, Nil) Nil)) (TypeState nxtLabel' declareable' useable' frag) res -> SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs)) (TypeState nxtLabel' declareable' useable' (Cons (label, Cons (SendSession False fragHead) f) fs')) resSource
recvSession :: (TyList f, TyList fs, TyList fs', TyListReverse frag fragRev, TyListTake (D1 E) fragRev (Cons (label, fragHead) Nil), TyListDrop (D1 E) fragRev fragTailRev, TyListReverse fragTailRev fragTail, TyListAppend fragTail fs fs') => SessionType (TypeState nxtLabel declareable useable (Cons (label, Nil) Nil)) (TypeState nxtLabel' declareable' useable' frag) res -> SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs)) (TypeState nxtLabel' declareable' useable' (Cons (label, Cons (RecvSession False fragHead) f) fs')) resSource
data Jump l Source
show/hide Instances
data Select Source
show/hide Instances
SListOfJumps (Cons val nxt) => STerminal (Select (Cons val nxt))
SNoJumpsBeyond lol idx => SNoJumpsBeyond (Select lol) idx
Dual (Offer lst) (Select lst)
Dual (Select lst) (Offer lst)
data Offer Source
show/hide Instances
SListOfJumps (Cons val nxt) => STerminal (Offer (Cons val nxt))
SNoJumpsBeyond lol idx => SNoJumpsBeyond (Offer lol) idx
Dual (Offer lst) (Select lst)
Dual (Select lst) (Offer lst)
jump :: (TyListReverse (Cons (Jump jt) f) f', TyList f, TyList fs, TyListMember useable jt True) => jt -> SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs)) (TypeState nxtLabel declareable useable (Cons (label, f') fs)) ()Source
end :: (TyListReverse (Cons End f) f', TyList f, TyList fs) => SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs)) (TypeState nxtLabel declareable useable (Cons (label, f') fs)) ()Source
select :: forall f f' fs listOfRes listOfJumps label nxtLabel declareable useable to finalTo. (TyListReverse (Cons (Select listOfJumps) f) f', TyList f, TyList fs, BuildBranches (BranchesList listOfRes listOfJumps (TypeState nxtLabel declareable useable (Cons (label, f') fs)) to finalTo) (SessionType (TypeState nxtLabel declareable useable (Cons (label, f') fs)) finalTo (listOfRes, listOfJumps))) => BranchesList listOfRes listOfJumps (TypeState nxtLabel declareable useable (Cons (label, f') fs)) to finalTo -> SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs)) finalTo listOfResSource
offer :: forall f f' fs listOfRes listOfJumps label nxtLabel declareable useable to finalTo. (TyListReverse (Cons (Offer listOfJumps) f) f', TyList f, TyList fs, BuildBranches (BranchesList listOfRes listOfJumps (TypeState nxtLabel declareable useable (Cons (label, f') fs)) to finalTo) (SessionType (TypeState nxtLabel declareable useable (Cons (label, f') fs)) finalTo (listOfRes, listOfJumps))) => BranchesList listOfRes listOfJumps (TypeState nxtLabel declareable useable (Cons (label, f') fs)) to finalTo -> SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs)) finalTo listOfResSource
(~>) :: (TyList nxt, SNonTerminal a, SValidSessionType nxt) => a -> nxt -> Cons a nxtSource
(~|~) :: (Succ label nxtLabel, TyListConsSet label declareable declareable', TyListElem declareable' label idx, TyListDelete declareable' idx declareable'', TyListConsSet label useable useable', TyList st, TyListMember declareable' label True, TyList labs, TyList resLst) => SessionType (TypeState nxtLabel declareable'' useable' (Cons (label, Nil) st)) (TypeState nxtLabel' declareable''' useable'' st') res -> BranchesList resLst labs (TypeState nxtLabel' declareable''' useable'' st') to finalTo -> BranchesList (Cons res resLst) (Cons (Cons (Jump label) Nil) labs) (TypeState label declareable useable st) (TypeState nxtLabel' declareable''' useable'' st', to) finalToSource
class SWellFormedConfig idxA idxB ss Source
testWellformed :: SWellFormedConfig idxA idxB ss => ss -> idxA -> idxB -> BoolSource
data SessionChain prog prog' from to res Source
The representation of a computation that performs work using session types. Again, really quite similar to a more-parameterized State monad.
show/hide Instances
SMonadIO (SessionChain prog prog')
SMonad (SessionChain prog prog')
(.=) :: (TyListMember declareable label True, TyListElem declareable label idx, TyListDelete declareable idx declareable', TyList st) => label -> SessionType (TypeState nxtLabel declareable' useable (Cons (label, Nil) st)) (TypeState nxtLabel' declareable'' useable' st') a -> SessionType (TypeState nxtLabel declareable useable st) (TypeState nxtLabel' declareable'' useable' st') aSource
dual :: TrueSource
notDual :: FalseSource
newLabel :: (Succ nxtLabel nxtLabel', TyListConsSet nxtLabel declareable declareable', TyListConsSet nxtLabel useable useable') => SessionType (TypeState nxtLabel declareable useable st) (TypeState nxtLabel' declareable' useable' st) nxtLabelSource
send :: (TyList f, TyList fs) => t -> SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs)) (TypeState nxtLabel declareable useable (Cons (label, Cons (Send (SpecialNormal, t)) f) fs)) ()Source
recv :: (TyList f, TyList fs) => t -> SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs)) (TypeState nxtLabel declareable useable (Cons (label, Cons (Recv (SpecialNormal, t)) f) fs)) ()Source
makeSessionType :: (TyListSortNums st st', TyListSnd st' st'') => SessionType (TypeState (D0 E) Nil Nil Nil) (TypeState nxtLabel Nil useable st) res -> (st'', res)Source
currentLabel :: SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs)) (TypeState nxtLabel declareable useable (Cons (label, f) fs)) labelSource
data BranchesList whereSource
Constructors
BLNil :: BranchesList Nil Nil z z z
show/hide Instances
BuildBranches (BranchesList resLst labs (TypeState nxtLabel' declareable' useable' st') to finalTo) (SessionType (TypeState nxtLabel' declareable' useable' st') finalTo ((,) resLst labs)) => BuildBranches (BranchesList (Cons res resLst) (Cons (Cons (Jump nxtLabel) Nil) labs) (TypeState nxtLabel declareable useable st) ((,) (TypeState nxtLabel' declareable' useable' st') to) finalTo) (SessionType (TypeState nxtLabel declareable useable st) finalTo ((,) (Cons res resLst) (Cons (Cons (Jump nxtLabel) Nil) labs)))
BuildBranches (BranchesList Nil Nil (TypeState nxtLabel declareLabel useable st) (TypeState nxtLabel declareLabel useable st) (TypeState nxtLabel declareLabel useable st)) (SessionType (TypeState nxtLabel declareLabel useable st) (TypeState nxtLabel declareLabel useable st) ((,) Nil Nil))
data Cons Source
show/hide Instances
TyList lstA => Insert' True num val lstA (Cons ((,) num val) lstA)
(ProgramToMVarsOutgoingT prog prog ~ progOut, ProgramToMVarsOutgoingT prog' prog' ~ progIn, Succ idx idxSucc, BuildNetworkRunner prog prog' to result progList idxSucc, TyListIndex progOut idx (MVar (ProgramCell (Cell outgoing))), TyListIndex progIn idx (MVar (ProgramCell (Cell incoming))), TyListIndex prog idx currentUX, Expand prog currentUX current, NetworkRuntime prog prog' ((,,) current outgoing incoming) to result) => BuildNetworkRunner prog prog' to result (Cons frag progList) idx
(JumpsToList prog prog' to result jumps' ([] (SessionChain prog prog' from to result)), NetworkRuntime prog prog' ((,,) (Cons (Jump t) Nil) (Cons (Jump t) Nil) (Cons (Jump t) Nil)) to result, TypeNumberToInt t) => JumpsToList prog prog' to result (Cons (Cons (Jump t) Nil) jumps') ([] (SessionChain prog prog' from to result))
Insert num val Nil (Cons ((,) num val) Nil)
TyList set => TyListConsSet' False e set (Cons e set)
(Insert num val nxt lstB, TyList lstB) => Insert' False num val (Cons ((,) num' val') nxt) (Cons ((,) num' val') lstB)
(SmallerThanBool num num' isSmaller, Insert' isSmaller num val (Cons ((,) num' val') nxt) lstB) => Insert num val (Cons ((,) num' val') nxt) lstB
(TyListDrop cnt' nxt lst, Pred cnt cnt') => TyListDrop cnt (Cons val nxt) lst
Expand prog (Cons End Nil) (Cons End Nil)
Expand prog (Cons (Jump l) Nil) (Cons (Jump l) Nil)
Expand prog (Cons (Offer loj) Nil) (Cons (Offer loj) Nil)
Expand prog (Cons (Select loj) Nil) (Cons (Select loj) Nil)
Expand prog nxt nxt' => Expand prog (Cons (Recv t) nxt) (Cons (Recv t) nxt')
Expand prog nxt nxt' => Expand prog (Cons (Send t) nxt) (Cons (Send t) nxt')
(Expand prog nxt nxt', ExpandSession prog (RecvSession invert frag) expandedRecvSession) => Expand prog (Cons (RecvSession invert frag) nxt) (Cons expandedRecvSession nxt')
(Expand prog nxt nxt', ExpandSession prog (SendSession invert frag) expandedSendSession) => Expand prog (Cons (SendSession invert frag) nxt) (Cons expandedSendSession nxt')
(Expand prog nxt nxt', ExpandPid prog (RecvPid invert idxs) expandedRecvPid) => Expand prog (Cons (RecvPid invert idxs) nxt) (Cons expandedRecvPid nxt')
(Expand prog nxt nxt', ExpandPid prog (SendPid invert idxs) expandedSendPid) => Expand prog (Cons (SendPid invert idxs) nxt) (Cons expandedSendPid nxt')
(Outgoing val'' ~ val', ProgramToMVarsOutgoing ref nxt nxt', TyList nxt, TyList nxt', Expand ref val val'') => ProgramToMVarsOutgoing ref (Cons val nxt) (Cons (MVar (ProgramCell (Cell val'))) nxt')
(BuildPidTyMap' prog nxt (TyMap keyToIdx idxToValue) (TyMap keyToIdx' idxToValue'), TyList nxt) => BuildPidTyMap' prog (Cons ((,) init True) nxt) (TyMap keyToIdx idxToValue) (TyMap keyToIdx' idxToValue')
(BuildPidTyMap' prog nxt (TyMap keyToIdx idxToValue) (TyMap keyToIdx' idxToValue'), MapInsert (TyMap keyToIdx' idxToValue') init (MVar (Map ((,) RawPid RawPid) (MVar (PairStruct init prog prog' ((,,) (Cons (Jump init) Nil) (Cons (Jump init) Nil) (Cons (Jump init) Nil)))))) (TyMap keyToIdx'' idxToValue''), TyList nxt) => BuildPidTyMap' prog (Cons ((,) init False) nxt) (TyMap keyToIdx idxToValue) (TyMap keyToIdx'' idxToValue'')
TyListTake (D0 E) (Cons val nxt) Nil
(TyListTake cnt' nxt nxt', Pred (D9 r) cnt') => TyListTake (D9 r) (Cons val nxt) (Cons val nxt')
(TyListTake cnt' nxt nxt', Pred (D8 r) cnt') => TyListTake (D8 r) (Cons val nxt) (Cons val nxt')
(TyListTake cnt' nxt nxt', Pred (D7 r) cnt') => TyListTake (D7 r) (Cons val nxt) (Cons val nxt')
(TyListTake cnt' nxt nxt', Pred (D6 r) cnt') => TyListTake (D6 r) (Cons val nxt) (Cons val nxt')
(TyListTake cnt' nxt nxt', Pred (D5 r) cnt') => TyListTake (D5 r) (Cons val nxt) (Cons val nxt')
(TyListTake cnt' nxt nxt', Pred (D4 r) cnt') => TyListTake (D4 r) (Cons val nxt) (Cons val nxt')
(TyListTake cnt' nxt nxt', Pred (D3 r) cnt') => TyListTake (D3 r) (Cons val nxt) (Cons val nxt')
(TyListTake cnt' nxt nxt', Pred (D2 r) cnt') => TyListTake (D2 r) (Cons val nxt) (Cons val nxt')
(TyListTake cnt' nxt nxt', Pred (D1 r) cnt') => TyListTake (D1 r) (Cons val nxt) (Cons val nxt')
TyListDrop (D0 E) (Cons val nxt) (Cons val nxt)
(TyListLength n l, Succ l l', Show n, Show t) => Show (Cons t n)
TyList nxt => TyList (Cons val nxt)
(SValidSessionType nxt, SNonTerminal val) => SValidSessionType (Cons val nxt)
STerminal a => SValidSessionType (Cons a Nil)
(SValidSessionType val, SListOfSessionTypes nxt) => SListOfSessionTypes (Cons val nxt)
(SListOfJumps nxt, TyNum val) => SListOfJumps (Cons (Cons (Jump val) Nil) nxt)
(TyNum num, TyListSortNums nxt lst', Insert num val lst' lst'') => TyListSortNums (Cons ((,) num val) nxt) lst''
(TyListToSet nxt set, TyListConsSet v set set') => TyListToSet (Cons v nxt) set'
(TyListLength n len, Succ len len') => TyListLength (Cons t n) len'
(SNoJumpsBeyond val idx, SNoJumpsBeyond nxt idx) => SNoJumpsBeyond (Cons val nxt) idx
BuildInvertedSessionsSet nxt set => BuildInvertedSessionsSet (Cons ((,) init False) nxt) set
(TyListMember b a resMember, TySubList as b resSubList, And resMember resSubList res) => TySubList (Cons a as) b res
TyListMember nxt val res => TyListMember (Cons val' nxt) val res
TyListMember (Cons val nxt) val True
(TyListReverse' nxt (Cons v acc) n, TyList acc) => TyListReverse' (Cons v nxt) acc n
(TyListIndex nxt idx' res, Pred idx idx', SmallerThanBool idx' len True, TyListLength nxt len) => TyListIndex (Cons val nxt) idx res
(Succ acc acc', TyListElem' nxt acc' val idx) => TyListElem' (Cons val' nxt) acc val idx
TyListElem' (Cons val nxt) idx val idx
TyListAppend nxt b nxt' => TyListAppend (Cons val nxt) b (Cons val nxt')
TyListIndex (Cons res nxt) (D0 E) res
(TyNum num, MakeListOfJumps nxt nxt', TyList nxt, TyList nxt') => MakeListOfJumps (Cons ((,) num invert) nxt) (Cons (Cons (Jump num) Nil) nxt')
(TyList nxt, TyList nxt', Dual val val', Dual nxt nxt') => Dual (Cons val nxt) (Cons val' nxt')
(TyListSnd nxt nxt', TyList nxt, TyList nxt') => TyListSnd (Cons ((,) a b) nxt) (Cons b nxt')
(FindNonEmptyIncoming (TyMap keyToIdx idxToValue) nxt, MapLookup (TyMap keyToIdx idxToValue) idx (SessionState prog prog' ((,,) current fromO fromI)), TypeNumberToInt idx) => FindNonEmptyIncoming (TyMap keyToIdx idxToValue) (Cons idx nxt)
(MapLookup (TyMap keyToIdx idxToValue) idx (SessionState prog prog' ((,,) current fromO fromI)), SetIncomingNotify (TyMap keyToIdx idxToValue) nxt, TypeNumberToInt idx) => SetIncomingNotify (TyMap keyToIdx idxToValue) (Cons idx nxt)
(BuildInvertedSessionsSet nxt set, TyList set) => BuildInvertedSessionsSet (Cons ((,) init True) nxt) (Cons init set)
cons :: TyList n => t -> n -> Cons t nSource
data Nil Source
show/hide Instances
Show Nil
TyList Nil
SListOfSessionTypes Nil
SListOfJumps Nil
TyListSortNums Nil Nil
TyListToSet Nil Nil
MakeListOfJumps Nil Nil
SNoJumpsBeyond Nil idx
Dual Nil Nil
TyListSnd Nil Nil
FindNonEmptyIncoming mp Nil
SetIncomingNotify mp Nil
BuildInvertedSessionsSet Nil Nil
TySubList Nil b True
TyListMember Nil val False
TyListReverse' Nil acc acc
TyListDrop cnt Nil Nil
TyListAppend Nil b b
ProgramToMVarsOutgoing ref Nil Nil
BuildPidTyMap' prog Nil acc acc
BuildNetworkRunner prog prog' to result Nil idx
JumpsToList prog prog' to result Nil ([] a)
Insert num val Nil (Cons ((,) num val) Nil)
TyListLength Nil (D0 E)
TyListTake (D0 E) Nil Nil
TyListTake (D0 E) (Cons val nxt) Nil
nil :: NilSource
data E Source
Constructors
E
show/hide Instances
Show E
Reverse' E a a
IncrementRightToLeft E (D1 E)
data D0 n Source
Constructors
D0 n
show/hide Instances
TyListLength Nil (D0 E)
Pred m m' => Add m (D0 E) m
Show n => Show (D0 n)
TypeNumberToInt (D0 E)
TyNum n => TyNum (D0 n)
TyNum (D0 E)
Pred y y' => SmallerThan (D0 E) y
StripLeadingZeros a b => StripLeadingZeros (D0 a) b
Pred' (D0 E) y False
Pred n n' => Add (D0 E) n n
Reverse' n (D0 a) r => Reverse' (D0 n) a r
TyListTake (D0 E) Nil Nil
StripLeadingZeros (D0 E) (D0 E)
DecrementRightToLeft (D1 a) (D0 a)
DecrementRightToLeft a b => DecrementRightToLeft (D0 a) (D9 b)
IncrementRightToLeft a b => IncrementRightToLeft (D9 a) (D0 b)
IncrementRightToLeft (D0 a) (D1 a)
Add (D0 E) (D0 E) (D0 E)
TyListTake (D0 E) (Cons val nxt) Nil
TyListDrop (D0 E) (Cons val nxt) (Cons val nxt)
TyListIndex (Cons res nxt) (D0 E) res
data D1 n Source
Constructors
D1 n
show/hide Instances
IncrementRightToLeft E (D1 E)
Show n => Show (D1 n)
TyNum n => TyNum (D1 n)
TyNum (D1 E)
Pred (D1 a) x' => Pred' (D1 a) x' True
Reverse' n (D1 a) r => Reverse' (D1 n) a r
StripLeadingZeros (D1 a) (D1 a)
DecrementRightToLeft (D2 a) (D1 a)
DecrementRightToLeft (D1 a) (D0 a)
IncrementRightToLeft (D1 a) (D2 a)
IncrementRightToLeft (D0 a) (D1 a)
(TyListTake cnt' nxt nxt', Pred (D1 r) cnt') => TyListTake (D1 r) (Cons val nxt) (Cons val nxt')
data D2 n Source
Constructors
D2 n
show/hide Instances
Show n => Show (D2 n)
TyNum n => TyNum (D2 n)
TyNum (D2 E)
Pred (D2 a) x' => Pred' (D2 a) x' True
Reverse' n (D2 a) r => Reverse' (D2 n) a r
StripLeadingZeros (D2 a) (D2 a)
DecrementRightToLeft (D3 a) (D2 a)
DecrementRightToLeft (D2 a) (D1 a)
IncrementRightToLeft (D2 a) (D3 a)
IncrementRightToLeft (D1 a) (D2 a)
(TyListTake cnt' nxt nxt', Pred (D2 r) cnt') => TyListTake (D2 r) (Cons val nxt) (Cons val nxt')
data D3 n Source
Constructors
D3 n
show/hide Instances
Show n => Show (D3 n)
TyNum n => TyNum (D3 n)
TyNum (D3 E)
Pred (D3 a) x' => Pred' (D3 a) x' True
Reverse' n (D3 a) r => Reverse' (D3 n) a r
StripLeadingZeros (D3 a) (D3 a)
DecrementRightToLeft (D4 a) (D3 a)
DecrementRightToLeft (D3 a) (D2 a)
IncrementRightToLeft (D3 a) (D4 a)
IncrementRightToLeft (D2 a) (D3 a)
(TyListTake cnt' nxt nxt', Pred (D3 r) cnt') => TyListTake (D3 r) (Cons val nxt) (Cons val nxt')
data D4 n Source
Constructors
D4 n
show/hide Instances
Show n => Show (D4 n)
TyNum n => TyNum (D4 n)
TyNum (D4 E)
Pred (D4 a) x' => Pred' (D4 a) x' True
Reverse' n (D4 a) r => Reverse' (D4 n) a r
StripLeadingZeros (D4 a) (D4 a)
DecrementRightToLeft (D5 a) (D4 a)
DecrementRightToLeft (D4 a) (D3 a)
IncrementRightToLeft (D4 a) (D5 a)
IncrementRightToLeft (D3 a) (D4 a)
(TyListTake cnt' nxt nxt', Pred (D4 r) cnt') => TyListTake (D4 r) (Cons val nxt) (Cons val nxt')
data D5 n Source
Constructors
D5 n
show/hide Instances
Show n => Show (D5 n)
TyNum n => TyNum (D5 n)
TyNum (D5 E)
Pred (D5 a) x' => Pred' (D5 a) x' True
Reverse' n (D5 a) r => Reverse' (D5 n) a r
StripLeadingZeros (D5 a) (D5 a)
DecrementRightToLeft (D6 a) (D5 a)
DecrementRightToLeft (D5 a) (D4 a)
IncrementRightToLeft (D5 a) (D6 a)
IncrementRightToLeft (D4 a) (D5 a)
(TyListTake cnt' nxt nxt', Pred (D5 r) cnt') => TyListTake (D5 r) (Cons val nxt) (Cons val nxt')
data D6 n Source
Constructors
D6 n
show/hide Instances
Show n => Show (D6 n)
TyNum n => TyNum (D6 n)
TyNum (D6 E)
Pred (D6 a) x' => Pred' (D6 a) x' True
Reverse' n (D6 a) r => Reverse' (D6 n) a r
StripLeadingZeros (D6 a) (D6 a)
DecrementRightToLeft (D7 a) (D6 a)
DecrementRightToLeft (D6 a) (D5 a)
IncrementRightToLeft (D6 a) (D7 a)
IncrementRightToLeft (D5 a) (D6 a)
(TyListTake cnt' nxt nxt', Pred (D6 r) cnt') => TyListTake (D6 r) (Cons val nxt) (Cons val nxt')
data D7 n Source
Constructors
D7 n
show/hide Instances
Show n => Show (D7 n)
TyNum n => TyNum (D7 n)
TyNum (D7 E)
Pred (D7 a) x' => Pred' (D7 a) x' True
Reverse' n (D7 a) r => Reverse' (D7 n) a r
StripLeadingZeros (D7 a) (D7 a)
DecrementRightToLeft (D8 a) (D7 a)
DecrementRightToLeft (D7 a) (D6 a)
IncrementRightToLeft (D7 a) (D8 a)
IncrementRightToLeft (D6 a) (D7 a)
(TyListTake cnt' nxt nxt', Pred (D7 r) cnt') => TyListTake (D7 r) (Cons val nxt) (Cons val nxt')
data D8 n Source
Constructors
D8 n
show/hide Instances
Show n => Show (D8 n)
TyNum n => TyNum (D8 n)
TyNum (D8 E)
Pred (D8 a) x' => Pred' (D8 a) x' True
Reverse' n (D8 a) r => Reverse' (D8 n) a r
StripLeadingZeros (D8 a) (D8 a)
DecrementRightToLeft (D9 a) (D8 a)
DecrementRightToLeft (D8 a) (D7 a)
IncrementRightToLeft (D8 a) (D9 a)
IncrementRightToLeft (D7 a) (D8 a)
(TyListTake cnt' nxt nxt', Pred (D8 r) cnt') => TyListTake (D8 r) (Cons val nxt) (Cons val nxt')
data D9 n Source
Constructors
D9 n
show/hide Instances
Show n => Show (D9 n)
TyNum n => TyNum (D9 n)
TyNum (D9 E)
Pred (D9 a) x' => Pred' (D9 a) x' True
Reverse' n (D9 a) r => Reverse' (D9 n) a r
StripLeadingZeros (D9 a) (D9 a)
DecrementRightToLeft (D9 a) (D8 a)
DecrementRightToLeft a b => DecrementRightToLeft (D0 a) (D9 b)
IncrementRightToLeft a b => IncrementRightToLeft (D9 a) (D0 b)
IncrementRightToLeft (D8 a) (D9 a)
(TyListTake cnt' nxt nxt', Pred (D9 r) cnt') => TyListTake (D9 r) (Cons val nxt) (Cons val nxt')
module Control.Concurrent.Session.Base.SMonad
emptyMap :: TyMap Nil NilSource
data Pid Source
A process ID. This is a tiny bit like ThreadId but rather heavily annotated.
show/hide Instances
(TySubList invertedSessionsB invertedSessionsA True, TySubList sessionsToIdxB sessionsToIdxA True, ReducePairStructs (TyMap sessionsToIdxA idxsToPairStructsA) (TyMap sessionsToIdxB idxsToPairStructsB) (TyMap Nil Nil) (TyMap sessionsToIdxB idxsToPairStructsB)) => CompatibleTypes SpecialPid (Pid prog prog' invertedSessionsA sessionsToIdxA idxsToPairStructsA) (Pid prog prog' invertedSessionsB sessionsToIdxB idxsToPairStructsB)
Eq (Pid prog prog' invertedSessions sessionsToIdx idxsToPairStructs)
Ord (Pid prog prog' invertedSessions sessionsToIdx idxsToPairStructs)
Show (Pid prog prog' invertedSessions sessionsToIdx idxsToPairStructs)
PidEq (Pid progA progA' invertedSessionsA sessionsToIdxA idxsToPairStructsA) (Pid progB progB' invertedSessionsB sessionsToIdxB idxsToPairStructsB)
data InterleavedChain internalPid from to res Source
show/hide Instances
class CreateSession invert init prog prog' sessionsToIdxMe sessionsToIdxThem idxsToPairStructsMe idxsToPairStructsThem keyToIdxMe idxToValueMe keyToIdxMe' idxToValueMe' idxOfThem invertedSessionsMe invertedSessionsThem whereSource
Provides the ability to make a new session / channel with the given Pid. Supply the index to the Session Type, whether or not you're locally inverting (dualing) the Session Type, and the Pid, and so long as the Pid supports the dual of your local Session Type, this will block until the Pid gets around to servicing you. Thus this is a synchronous operation and both Pids must know of each other to create a new session / channel between them.
Methods
createSession :: init -> invert -> Pid prog prog' invertedSessionsThem sessionsToIdxThem idxsToPairStructsThem -> InterleavedChain (InternalPid prog prog' invertedSessionsMe sessionsToIdxMe idxsToPairStructsMe) (TyMap keyToIdxMe idxToValueMe) (TyMap keyToIdxMe' idxToValueMe') idxOfThemSource
show/hide Instances
(ProgramToMVarsOutgoingT prog prog ~ progOut, ProgramToMVarsOutgoingT prog' prog' ~ progIn, SWellFormedConfig init (D0 E) prog, SWellFormedConfig init (D0 E) prog', TyListIndex progOut init (MVar (ProgramCell (Cell fromO))), TyListIndex progIn init (MVar (ProgramCell (Cell fromI))), TyListIndex prog init current', Expand prog current' current, MapLookup (TyMap sessionsToIdxMe idxsToPairStructsMe) init (MVar (Map ((,) RawPid RawPid) (MVar (PairStruct init prog prog' ((,,) (Cons (Jump init) Nil) (Cons (Jump init) Nil) (Cons (Jump init) Nil)))))), TyListMember invertedSessionsThem init True, MapSize (TyMap keyToIdxMe idxToValueMe) idxOfThem, MapInsert (TyMap keyToIdxMe idxToValueMe) idxOfThem (SessionState prog prog' ((,,) current fromO fromI)) (TyMap keyToIdxMe' idxToValueMe')) => CreateSession False init prog prog' sessionsToIdxMe sessionsToIdxThem idxsToPairStructsMe idxsToPairStructsThem keyToIdxMe idxToValueMe keyToIdxMe' idxToValueMe' idxOfThem invertedSessionsMe invertedSessionsThem
(ProgramToMVarsOutgoingT prog prog ~ progOut, ProgramToMVarsOutgoingT prog' prog' ~ progIn, ProgramToMVarsOutgoing prog prog progOut, ProgramToMVarsOutgoing prog' prog' progIn, SWellFormedConfig init (D0 E) prog, SWellFormedConfig init (D0 E) prog', TyListIndex progOut init (MVar (ProgramCell (Cell fromO))), TyListIndex progIn init (MVar (ProgramCell (Cell fromI))), TyListIndex prog init currentUX, Expand prog currentUX current, TyListIndex prog' init currentUX', Expand prog' currentUX' current', MapLookup (TyMap sessionsToIdxThem idxsToPairStructsThem) init (MVar (Map ((,) RawPid RawPid) (MVar (PairStruct init prog prog' ((,,) (Cons (Jump init) Nil) (Cons (Jump init) Nil) (Cons (Jump init) Nil)))))), TyListMember invertedSessionsMe init True, MapSize (TyMap keyToIdxMe idxToValueMe) idxOfThem, MapInsert (TyMap keyToIdxMe idxToValueMe) idxOfThem (SessionState prog' prog ((,,) current' fromI fromO)) (TyMap keyToIdxMe' idxToValueMe')) => CreateSession True init prog prog' sessionsToIdxMe sessionsToIdxThem idxsToPairStructsMe idxsToPairStructsThem keyToIdxMe idxToValueMe keyToIdxMe' idxToValueMe' idxOfThem invertedSessionsMe invertedSessionsThem
myPid :: InterleavedChain (InternalPid prog prog' invertedSessions sessionsToIdx idxsToPairStructs) from from (Pid prog prog' invertedSessions sessionsToIdx idxsToPairStructs)Source
class PidEq a b whereSource
Provides a way to compare two Pids. Of course, if the Pids have different type params, then they are definitely different, but it's still convenient to be able to do something like (==) on them.
Methods
(=~=) :: a -> b -> BoolSource
show/hide Instances
PidEq (Pid progA progA' invertedSessionsA sessionsToIdxA idxsToPairStructsA) (Pid progB progB' invertedSessionsB sessionsToIdxB idxsToPairStructsB)
data MultiReceive whereSource
Constructors
MultiReceiveNil :: MultiReceive Nil prog prog' invertedSessions sessionsToIdx idxsToPairStructs keyToIdx idxToValue keyToIdx' idxToValue' res
(~|||~) :: MapLookup (TyMap keyToIdx idxToValue) ch (SessionState progS progS' (Cons (Recv (sp, t)) nxt, fromO, Cons t nxt')) => (ch, InterleavedChain (InternalPid prog prog' invertedSessions sessionsToIdx idxsToPairStructs) (TyMap keyToIdx idxToValue) (TyMap keyToIdx' idxToValue') res) -> MultiReceive chs prog prog' invertedSessions sessionsToIdx idxsToPairStructs keyToIdx idxToValue keyToIdx' idxToValue' res -> MultiReceive (Cons ch chs) prog prog' invertedSessions sessionsToIdx idxsToPairStructs keyToIdx idxToValue keyToIdx' idxToValue' resSource
multiReceive :: forall chs len keyToIdx idxToValue prog prog' invertedSessions sessionsToIdx idxsToPairStructs keyToIdx' idxToValue' res. (TyListLength chs len, SmallerThanBool (D0 E) len True, SetIncomingNotify (TyMap keyToIdx idxToValue) chs, FindNonEmptyIncoming (TyMap keyToIdx idxToValue) chs, TypeNumberToInt len) => MultiReceive chs prog prog' invertedSessions sessionsToIdx idxsToPairStructs keyToIdx idxToValue keyToIdx' idxToValue' res -> InterleavedChain (InternalPid prog prog' invertedSessions sessionsToIdx idxsToPairStructs) (TyMap keyToIdx idxToValue) (TyMap keyToIdx' idxToValue') resSource
module Control.Concurrent.Session.Interleaving
module Control.Concurrent.Session.Network.Socket
Produced by Haddock version 2.4.2