|
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, ExpandPids 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, 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, ExpandPids 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, ProgramToMVarsOutgoing prog prog progOut, ProgramToMVarsOutgoing prog' prog' progIn, TyListLength jumps len, SmallerThan label len, 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, ExpandPids 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, ExpandPids prog currentUX current, TyListIndex prog' init currentUX', ExpandPids 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 :: (TyListSortNums lst lst', TyListReverse lst' lst'') => lst -> SendPid False lst'' | | recvPid :: (TyListSortNums lst lst', TyListReverse lst' lst'') => lst -> RecvPid False lst'' | | data Jump l | | data Select | | data Offer | | jump :: TyNum n => n -> Cons (Jump n) Nil | | end :: Cons End Nil | | select :: SListOfJumps (Cons val nxt) => Cons val nxt -> Cons (Select (Cons val nxt)) Nil | | offer :: SListOfJumps (Cons val nxt) => Cons val nxt -> Cons (Offer (Cons val nxt)) Nil | | class Dual a b | a -> b, b -> a where | | | (~>) :: (TyList nxt, SNonTerminal a, SValidSessionType nxt) => a -> nxt -> Cons a nxt | | (~|~) :: (TyNum target, TyList nxt) => target -> nxt -> Cons (Cons (Jump target) Nil) nxt | | class SWellFormedConfig idxA idxB ss | | testWellformed :: SWellFormedConfig idxA idxB ss => ss -> idxA -> idxB -> Bool | | data SessionChain prog prog' from to res | | 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 | | newtype InterleavedChain internalPid from to res = InterleavedChain {} | | class BuildPidTyMap prog stlst tymap | prog stlst -> tymap where | | | class CreateSession invert init prog prog' fromO fromI progOut progIn sessionsToIdxMe sessionsToIdxThem idxsToPairStructsMe idxsToPairStructsThem keyToIdxMe idxToValueMe keyToIdxMe' idxToValueMe' idxOfThem where | | | myPid :: InterleavedChain (InternalPid prog sessionsToIdx idxsToPairStructs) from from (Pid prog sessionsToIdx idxsToPairStructs) | | class PidEq a b where | | | 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, ExpandPids prog currentUX current, TyListIndex prog' init currentUX', ExpandPids 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)))))), MapSize (TyMap keyToIdxMe idxToValueMe) idxOfThem, MapInsert (TyMap keyToIdxMe idxToValueMe) idxOfThem (SessionState prog' prog ((,,) current' fromI fromO)) (TyMap keyToIdxMe' idxToValueMe'), Dual prog prog') => CreateSession True init prog prog' fromO fromI progOut progIn sessionsToIdxMe sessionsToIdxThem idxsToPairStructsMe idxsToPairStructsThem 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, TyListIndex prog' init currentUX', ExpandPids prog currentUX current, ExpandPids prog' currentUX' current', BuildPidTyMap prog sessionsListSorted (TyMap sessionsToIdxThem idxsToPairStructsThem), 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'), Dual prog prog') => 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' | TyList lstA => Insert' True num val lstA (Cons ((,) num val) lstA) | (TyListUpdateVar idxToValue idx value idxToValue', TyListElem keyToIdx key idx) => MapInsert' True (TyMap keyToIdx idxToValue) key value (TyMap keyToIdx idxToValue') | 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, 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 current', ExpandPids 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)))))), 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 | (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', ExpandPids prog currentUX current, ExpandPids prog' currentUX' current', BuildPidTyMap prog sessionsListSorted (TyMap sessionsToIdxThem idxsToPairStructsThem), 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'), Dual prog prog') => 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' | 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) => 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, ExpandPids 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, 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, ExpandPids 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, ProgramToMVarsOutgoing prog prog progOut, ProgramToMVarsOutgoing prog' prog' progIn, TyListLength jumps len, SmallerThan label len, 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, ExpandPids 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 prog prog' nxt nxt' incoming. t -> SessionChain prog prog' (Cons (Send t) nxt, Cons t nxt', incoming) (nxt, nxt', incoming) () | Source |
|
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, ExpandPids prog currentUX current, TyListIndex prog' init currentUX', ExpandPids 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 | |
|
|
|
Constructors | | Instances | |
|
|
|
|
|
|
|
Instances | |
|
|
|
Instances | |
|
|
|
Instances | |
|
|
|
|
|
|
|
|
|
|
class Dual a b | a -> b, b -> a where | Source |
|
| Associated Types | | | Methods | | | Instances | |
|
|
|
|
|
|
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 | |
|
|
|
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 | ExpandPids p (Cons (Select loj) Nil) (Cons (Select loj) Nil) | ExpandPids p (Cons (Offer loj) Nil) (Cons (Offer loj) Nil) | ExpandPids p (Cons (Jump l) Nil) (Cons (Jump l) Nil) | (ExpandPids p nxt nxt', TyList nxt, TyList nxt') => ExpandPids p (Cons (Send t) nxt) (Cons (Send t) nxt') | (ExpandPids p nxt nxt', TyList nxt, TyList nxt') => ExpandPids p (Cons (Recv t) nxt) (Cons (Recv t) nxt') | ExpandPids p (Cons End Nil) (Cons End Nil) | (ExpandPids prog nxt nxt', TyList nxt, TyList nxt', BuildPidTyMap progO t (TyMap sessionsToIdx idxsToPairStructs), If invert prog' prog progO, Dual prog prog') => ExpandPids prog (Cons (SendPid invert t) nxt) (Cons (Send (Pid progO sessionsToIdx idxsToPairStructs)) nxt') | (ExpandPids prog nxt nxt', TyList nxt, TyList nxt', BuildPidTyMap progO t (TyMap sessionsToIdx idxsToPairStructs), If invert prog' prog progO, Dual prog prog') => ExpandPids prog (Cons (RecvPid invert t) nxt) (Cons (Recv (Pid progO sessionsToIdx idxsToPairStructs)) nxt') | (ProgramToMVarsOutgoing ref nxt nxt', TyList nxt, TyList nxt') => 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 | 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', SmallerThan idx' len, 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') |
|
|
|
|
|
|
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 sessionsToIdx idxsToPairStructs) | Ord (Pid prog sessionsToIdx idxsToPairStructs) | Show (Pid prog sessionsToIdx idxsToPairStructs) | PidEq (Pid progA sessionsToIdxA idxsToPairStructsA) (Pid progB sessionsToIdxB idxsToPairStructsB) |
|
|
|
newtype InterleavedChain internalPid from to res | Source |
|
Constructors | InterleavedChain | | runInterleavedChain :: internalPid -> from -> IO (res, to, internalPid) | |
|
| Instances | |
|
|
class BuildPidTyMap prog stlst tymap | prog stlst -> tymap where | Source |
|
| Associated Types | type BuildPidTyMapT prog stlst | Source |
|
| | Methods | buildPidTyMap :: prog -> stlst -> IO tymap | Source |
|
|
|
|
class CreateSession invert init prog prog' fromO fromI progOut progIn sessionsToIdxMe sessionsToIdxThem idxsToPairStructsMe idxsToPairStructsThem keyToIdxMe idxToValueMe keyToIdxMe' idxToValueMe' idxOfThem 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 sessionsToIdxThem idxsToPairStructsThem -> InterleavedChain (InternalPid prog sessionsToIdxMe idxsToPairStructsMe) (TyMap keyToIdxMe idxToValueMe) (TyMap keyToIdxMe' idxToValueMe') idxOfThem | Source |
|
| | Instances | (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 current', ExpandPids 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)))))), 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 | (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, ExpandPids prog currentUX current, TyListIndex prog' init currentUX', ExpandPids 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)))))), MapSize (TyMap keyToIdxMe idxToValueMe) idxOfThem, MapInsert (TyMap keyToIdxMe idxToValueMe) idxOfThem (SessionState prog' prog ((,,) current' fromI fromO)) (TyMap keyToIdxMe' idxToValueMe'), Dual prog prog') => CreateSession True init prog prog' fromO fromI progOut progIn sessionsToIdxMe sessionsToIdxThem idxsToPairStructsMe idxsToPairStructsThem keyToIdxMe idxToValueMe keyToIdxMe' idxToValueMe' idxOfThem |
|
|
|
|
|
|
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 sessionsToIdxA idxsToPairStructsA) (Pid progB sessionsToIdxB idxsToPairStructsB) |
|
|
|
module Control.Concurrent.Session.Interleaving |
|
Produced by Haddock version 2.3.0 |