Control.Concurrent.Session

Description

This is just a convenience module that reexports everything you're expected to need.

Synopsis

Documentation

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 progOut progIn finalState finalResult

(~||~) :: forall prog prog' progOut progIn outgoing incoming finalState finalResult jumps l. (Dual prog prog', ProgramToMVarsOutgoing prog progOut, ProgramToMVarsOutgoing prog' progIn, SWellFormedConfig l (D0 E) prog, SWellFormedConfig l (D0 E) prog', Elem progOut l (MVar (ProgramCell (Cell outgoing))), Elem progIn l (MVar (ProgramCell (Cell incoming)))) => SessionChain prog progOut progIn (outgoing, incoming) finalState finalResult -> OfferImpls jumps prog progOut progIn finalState finalResult -> OfferImpls (Cons (Cons (Jump l) Nil) jumps) prog progOut progIn 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. (Dual prog prog', ProgramToMVarsOutgoing prog progOut, ProgramToMVarsOutgoing prog' progIn, SWellFormedConfig l (D0 E) prog, SWellFormedConfig l (D0 E) prog', Elem progOut l (MVar (ProgramCell (Cell outgoing))), Elem progIn l (MVar (ProgramCell (Cell incoming)))) => SessionChain prog progOut progIn (Cons (Jump l) Nil, Cons (Jump l) Nil) (outgoing, incoming) ()Source

Perform a jump. Now you may think that you should indicate where you want to jump to. But of coures, that's actually specified by the session type so you don't have to specify it at all in the implementation.

soffer :: forall finalState finalResult prog prog' progOut progIn jumps. (Dual prog prog', ProgramToMVarsOutgoing prog progOut, ProgramToMVarsOutgoing prog' progIn) => OfferImpls jumps prog progOut progIn finalState finalResult -> SessionChain prog progOut progIn (Cons (Choice jumps) Nil, Cons (Choice jumps) Nil) finalState 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 len jumpTarget. (Dual prog prog', ProgramToMVarsOutgoing prog progOut, ProgramToMVarsOutgoing prog' progIn, ListLength jumps len, SmallerThan label len, TypeNumberToInt label, Elem jumps label (Cons (Jump jumpTarget) Nil), SWellFormedConfig jumpTarget (D0 E) prog, SWellFormedConfig jumpTarget (D0 E) prog', Elem progOut jumpTarget (MVar (ProgramCell (Cell outgoing))), Elem progIn jumpTarget (MVar (ProgramCell (Cell incoming)))) => label -> SessionChain prog progOut progIn (Cons (Choice jumps) Nil, Cons (Choice jumps) Nil) (outgoing, incoming) ()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' progOut progIn nxt incoming. (Dual prog prog', ProgramToMVarsOutgoing prog progOut, ProgramToMVarsOutgoing prog' progIn) => t -> SessionChain prog progOut progIn (Cons t nxt, incoming) (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.

srecv :: forall t prog prog' progOut progIn nxt outgoing. (Dual prog prog', ProgramToMVarsOutgoing prog progOut, ProgramToMVarsOutgoing prog' progIn) => SessionChain prog progOut progIn (outgoing, Cons t 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 toO' toI' res res'. (Dual prog prog', Dual prog' prog, ProgramToMVarsOutgoing prog progOut, ProgramToMVarsOutgoing prog' progIn, SWellFormedConfig init (D0 E) prog, SWellFormedConfig init (D0 E) prog', Elem progOut init (MVar (ProgramCell (Cell fromO))), Elem progIn init (MVar (ProgramCell (Cell fromI)))) => prog -> init -> SessionChain prog progOut progIn (fromO, fromI) (toO, toI) res -> SessionChain prog' progIn progOut (fromI, fromO) (toO', toI') res' -> IO (res, res')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

Instances

Show End
STerminal End
SNoJumpsBeyond End idx
Dual End End
OnlyOutgoing (Cons End Nil) (Cons End Nil)

data Send whereSource

Constructors

Send :: t -> Send t
SendInt :: Send Int
SendBool :: Send Bool
SendChar :: Send Char
SendStr :: Send String
SendDouble :: Send Double

Instances

SNonTerminal (Send t)
SNoJumpsBeyond (Send t) idx
Dual (Recv t) (Send t)
Dual (Send t) (Recv t)
OnlyOutgoing nxt nxt' => OnlyOutgoing (Cons (Send t) nxt) (Cons t nxt')

data Recv whereSource

Constructors

Recv :: t -> Recv t
RecvInt :: Recv Int
RecvBool :: Recv Bool
RecvChar :: Recv Char
RecvStr :: Recv String
RecvDouble :: Recv Double

Instances

SNonTerminal (Recv t)
SNoJumpsBeyond (Recv t) idx
Dual (Recv t) (Send t)
Dual (Send t) (Recv t)
OnlyOutgoing nxt nxt' => OnlyOutgoing (Cons (Recv t) nxt) nxt'

data Jump l Source

Instances

Show l => Show (Jump l)
TyNum l => STerminal (Jump l)
SmallerThan l idx => SNoJumpsBeyond (Jump l) idx
Dual (Jump l) (Jump l)
(SListOfJumps nxt, TyNum val) => SListOfJumps (Cons (Cons (Jump val) Nil) nxt)
OnlyOutgoing (Cons (Jump l) Nil) (Cons (Jump l) Nil)

data Select Source

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)
OnlyOutgoing (Cons (Select jl) Nil) (Cons (Choice jl) Nil)

data Offer Source

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)
OnlyOutgoing (Cons (Offer jl) Nil) (Cons (Choice jl) Nil)

jump :: TyNum n => n -> Cons (Jump n) Nil Source

end :: Cons End Nil Source

select :: SListOfJumps (Cons val nxt) => Cons val nxt -> Cons (Select (Cons val nxt)) Nil Source

offer :: SListOfJumps (Cons val nxt) => Cons val nxt -> Cons (Offer (Cons val nxt)) Nil Source

class Dual a b | a -> b, b -> a whereSource

Methods

dual :: a -> bSource

Instances

Dual Nil Nil
Dual End End
Dual (Offer lst) (Select lst)
Dual (Select lst) (Offer lst)
Dual (Jump l) (Jump l)
Dual (Recv t) (Send t)
Dual (Send t) (Recv t)
(Dual val val', Dual nxt nxt') => Dual (Cons val nxt) (Cons val' nxt')

(~>) :: (TyList nxt, SNonTerminal a, SValidSessionType nxt) => a -> nxt -> Cons a nxtSource

(~|~) :: (TyNum target, TyList nxt) => target -> nxt -> Cons (Cons (Jump target) Nil) nxtSource

class SWellFormedConfig idxA idxB ss Source

Instances

(SListOfSessionTypes ss, ListLength ss len, SNoJumpsBeyond ss len, SmallerThan idxA len, Elem ss idxA st, ListLength st len', SmallerThan idxB len') => SWellFormedConfig idxA idxB ss

testWellformed :: SWellFormedConfig idxA idxB ss => ss -> idxA -> idxB -> Bool Source

data Cons Source

Instances

SListOfJumps (Cons val nxt) => STerminal (Offer (Cons val nxt))
SListOfJumps (Cons val nxt) => STerminal (Select (Cons val nxt))
(ListLength 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)
(ListLength n len, Succ len len') => ListLength (Cons t n) len'
OnlyOutgoing nxt nxt' => OnlyOutgoing (Cons (Recv t) nxt) nxt'
(SNoJumpsBeyond val idx, SNoJumpsBeyond nxt idx) => SNoJumpsBeyond (Cons val nxt) idx
(Elem nxt idx' res, Pred idx idx', SmallerThan idx' len, ListLength nxt len) => Elem (Cons val nxt) idx res
Elem (Cons res nxt) (D0 E) res
OnlyOutgoing (Cons (Offer jl) Nil) (Cons (Choice jl) Nil)
OnlyOutgoing (Cons (Select jl) Nil) (Cons (Choice jl) Nil)
OnlyOutgoing (Cons (Jump l) Nil) (Cons (Jump l) Nil)
OnlyOutgoing nxt nxt' => OnlyOutgoing (Cons (Send t) nxt) (Cons t nxt')
OnlyOutgoing (Cons End Nil) (Cons End Nil)
(Dual val val', Dual nxt nxt') => Dual (Cons val nxt) (Cons val' nxt')
(ProgramToMVarsOutgoing nxt nxt', OnlyOutgoing val val') => ProgramToMVarsOutgoing (Cons val nxt) (Cons (MVar (ProgramCell (Cell val'))) nxt')

cons :: TyList n => t -> n -> Cons t nSource

data Nil Source

Instances

Show Nil
TyList Nil
SListOfSessionTypes Nil
SListOfJumps Nil
SNoJumpsBeyond Nil idx
Dual Nil Nil
ProgramToMVarsOutgoing Nil Nil
ListLength Nil (D0 E)
STerminal a => SValidSessionType (Cons a Nil)
(SListOfJumps nxt, TyNum val) => SListOfJumps (Cons (Cons (Jump val) Nil) nxt)
OnlyOutgoing (Cons (Offer jl) Nil) (Cons (Choice jl) Nil)
OnlyOutgoing (Cons (Select jl) Nil) (Cons (Choice jl) Nil)
OnlyOutgoing (Cons (Jump l) Nil) (Cons (Jump l) Nil)
OnlyOutgoing (Cons End Nil) (Cons End Nil)

nil :: Nil Source

data E Source

Constructors

E

Instances

Show E
Reverse' E a a
IncrementRightToLeft E (D1 E)
ListLength Nil (D0 E)
Pred m m' => Add m (D0 E) m
TypeNumberToInt (D0 E)
TyNum (D9 E)
TyNum (D8 E)
TyNum (D7 E)
TyNum (D6 E)
TyNum (D5 E)
TyNum (D4 E)
TyNum (D3 E)
TyNum (D2 E)
TyNum (D1 E)
TyNum (D0 E)
Pred y y' => SmallerThan (D0 E) y
Pred n n' => Add (D0 E) n n
StripLeadingZeros (D0 E) (D0 E)
Add (D0 E) (D0 E) (D0 E)
Elem (Cons res nxt) (D0 E) res

data D0 n Source

Constructors

D0 n

Instances

ListLength 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 n n' => Add (D0 E) n n
Reverse' n (D0 a) r => Reverse' (D0 n) a r
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)
Elem (Cons res nxt) (D0 E) res

data D1 n Source

Constructors

D1 n

Instances

IncrementRightToLeft E (D1 E)
Show n => Show (D1 n)
TyNum n => TyNum (D1 n)
TyNum (D1 E)
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)

data D2 n Source

Constructors

D2 n

Instances

Show n => Show (D2 n)
TyNum n => TyNum (D2 n)
TyNum (D2 E)
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)

data D3 n Source

Constructors

D3 n

Instances

Show n => Show (D3 n)
TyNum n => TyNum (D3 n)
TyNum (D3 E)
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)

data D4 n Source

Constructors

D4 n

Instances

Show n => Show (D4 n)
TyNum n => TyNum (D4 n)
TyNum (D4 E)
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)

data D5 n Source

Constructors

D5 n

Instances

Show n => Show (D5 n)
TyNum n => TyNum (D5 n)
TyNum (D5 E)
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)

data D6 n Source

Constructors

D6 n

Instances

Show n => Show (D6 n)
TyNum n => TyNum (D6 n)
TyNum (D6 E)
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)

data D7 n Source

Constructors

D7 n

Instances

Show n => Show (D7 n)
TyNum n => TyNum (D7 n)
TyNum (D7 E)
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)

data D8 n Source

Constructors

D8 n

Instances

Show n => Show (D8 n)
TyNum n => TyNum (D8 n)
TyNum (D8 E)
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)

data D9 n Source

Constructors

D9 n

Instances

Show n => Show (D9 n)
TyNum n => TyNum (D9 n)
TyNum (D9 E)
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)

module Control.Concurrent.Session.SMonad