|
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 | | | | (~||~) :: 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 prog prog' nxt nxt' incoming. t -> SessionChain prog prog' (Cons (Send t) nxt, Cons t nxt', incoming) (nxt, nxt', incoming) () | | srecv :: forall t prog prog' nxt nxt' outgoing. SessionChain prog prog' (Cons (Recv 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 | | | | | | 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 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 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 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.SMonad | | emptyMap :: TyMap Nil Nil | | data Pid | | data InterleavedChain internalPid from to res | | class CreateSession invert init prog prog' fromO fromI progOut progIn 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 | | | | | (~|||~) :: MapLookup (TyMap keyToIdx idxToValue) ch (SessionState progS progS' (Cons (Recv 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 |
|
|
Documentation |
|
|
Constructors | | 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 | 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, 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' fromO fromI progOut progIn 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 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 |
|
|
|
|
Constructors | | 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, 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' fromO fromI progOut progIn 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 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 |
|
|
|
|
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 finalResult | Source |
|
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.
|
|
|
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.
|
|
|
Send a value to the other party. Of course, the value must be of
the correct type indicated in the session type.
|
|
|
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.
|
|
|
Instances | |
|
|
|
Constructors | | 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 (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 (SessionState prog prog' ((,,) current outgoing incoming))) | (Dual prog prog', BuildInvertedSessionsSet idxs invertedSessions, BuildPidTyMap prog' idxs (TyMap sessionsToIdx idxsToPairStructs)) => ExpandPid prog (SendPid True idxs) (Send (Pid prog' prog invertedSessions sessionsToIdx idxsToPairStructs)) | (Dual prog prog', BuildInvertedSessionsSet idxs invertedSessions, BuildPidTyMap prog idxs (TyMap sessionsToIdx idxsToPairStructs)) => ExpandPid prog (SendPid False idxs) (Send (Pid prog prog' invertedSessions sessionsToIdx idxsToPairStructs)) | SNonTerminal (Send t) | SNoJumpsBeyond (Send t) idx | Dual (Recv t) (Send t) | Dual (Send t) (Recv t) |
|
|
|
|
Constructors | | 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 (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 (SessionState prog prog' ((,,) current outgoing incoming))) | (Dual prog prog', BuildInvertedSessionsSet idxs invertedSessions, BuildPidTyMap prog' idxs (TyMap sessionsToIdx idxsToPairStructs)) => ExpandPid prog (RecvPid True idxs) (Recv (Pid prog' prog invertedSessions sessionsToIdx idxsToPairStructs)) | (Dual prog prog', BuildInvertedSessionsSet idxs invertedSessions, BuildPidTyMap prog idxs (TyMap sessionsToIdx idxsToPairStructs)) => ExpandPid prog (RecvPid False idxs) (Recv (Pid prog prog' invertedSessions sessionsToIdx idxsToPairStructs)) | SNonTerminal (Recv t) | SNoJumpsBeyond (Recv t) idx | Dual (Recv t) (Send t) | Dual (Send t) (Recv t) |
|
|
|
|
|
|
|
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 | Source |
|
|
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 | Source |
|
|
|
Instances | |
|
|
|
Instances | |
|
|
|
Instances | |
|
|
|
|
|
|
|
|
|
|
|
|
(~|~) :: (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 | Source |
|
|
class SWellFormedConfig idxA idxB ss | Source |
|
|
|
|
|
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.
| Instances | |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Constructors | | Instances | |
|
|
|
Instances | TyList lstA => Insert' True num val lstA (Cons ((,) num val) lstA) | 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 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) |
|
|
|
|
|
|
Instances | |
|
|
|
|
|
Constructors | | Instances | |
|
|
|
Constructors | | Instances | |
|
|
|
Constructors | | Instances | |
|
|
|
Constructors | | Instances | |
|
|
|
Constructors | | Instances | |
|
|
|
Constructors | | Instances | |
|
|
|
Constructors | | Instances | |
|
|
|
Constructors | | Instances | |
|
|
|
Constructors | | Instances | |
|
|
|
Constructors | | Instances | |
|
|
|
Constructors | | Instances | |
|
|
module Control.Concurrent.Session.SMonad |
|
|
|
|
A process ID. This is a tiny bit like ThreadId but rather heavily annotated.
| Instances | 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 |
|
Instances | |
|
|
class CreateSession invert init prog prog' fromO fromI progOut progIn sessionsToIdxMe sessionsToIdxThem idxsToPairStructsMe idxsToPairStructsThem keyToIdxMe idxToValueMe keyToIdxMe' idxToValueMe' idxOfThem invertedSessionsMe invertedSessionsThem where | Source |
|
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') idxOfThem | Source |
|
| | 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' fromO fromI progOut progIn 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' fromO fromI progOut progIn 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 |
|
|
|
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 | | | Instances | PidEq (Pid progA progA' invertedSessionsA sessionsToIdxA idxsToPairStructsA) (Pid progB progB' invertedSessionsB sessionsToIdxB idxsToPairStructsB) |
|
|
|
|
Constructors | MultiReceiveNil :: MultiReceive Nil prog prog' invertedSessions sessionsToIdx idxsToPairStructs keyToIdx idxToValue keyToIdx' idxToValue' res | |
|
|
|
(~|||~) :: MapLookup (TyMap keyToIdx idxToValue) ch (SessionState progS progS' (Cons (Recv 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 | Source |
|
|
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 | Source |
|
|
module Control.Concurrent.Session.Interleaving |
|
Produced by Haddock version 2.4.2 |