Control.Concurrent.Session.SessionType

Description

This module is concerned with allowing you to describe a session type. A session type is treated as a table or 2D array, where each row represents a particular session type function which can refer, by index, to the other rows.

Basically, what you have here is the ability to describe a program at the type level.

Just look at Control.Concurrent.Session.Tests for examples

Documentation

data End

Source

Constructors

End

Instances

Show End

STerminal End

SNoJumpsBeyond End idx

Dual End End

end :: Cons End Nil

Source

sendPid :: TyListSortNums lst lst' => lst -> SendPid False lst'

Source

recvPid :: TyListSortNums lst lst' => lst -> RecvPid False lst'

Source

data SendPid inverted lst

Source

Constructors

SendPid inverted lst

Instances

(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)))

(Show inverted, Show lst) => Show (SendPid inverted lst)

SNonTerminal (SendPid inverted t)

(MakeListOfJumps lol lol', SNoJumpsBeyond lol' idx) => SNoJumpsBeyond (SendPid inverted lol) idx

Not inverted inverted' => Dual (RecvPid inverted lst) (SendPid inverted' lst)

Not inverted inverted' => Dual (SendPid inverted lst) (RecvPid inverted' lst)

data RecvPid inverted lst

Source

Constructors

RecvPid inverted lst

Instances

(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)))

(Show inverted, Show lst) => Show (RecvPid inverted lst)

SNonTerminal (RecvPid inverted t)

(MakeListOfJumps lol lol', SNoJumpsBeyond lol' idx) => SNoJumpsBeyond (RecvPid inverted lol) idx

Not inverted inverted' => Dual (RecvPid inverted lst) (SendPid inverted' lst)

Not inverted inverted' => Dual (SendPid inverted lst) (RecvPid inverted' lst)

sendSession :: idx -> SendSession False idx

Source

recvSession :: idx -> RecvSession False idx

Source

data SendSession inverted idx

Source

Constructors

SendSession inverted idx

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))))

(Show inverted, Show idx) => Show (SendSession inverted idx)

SValidSessionType idx => SNonTerminal (SendSession inverted idx)

SNoJumpsBeyond l idx => SNoJumpsBeyond (SendSession inverted l) idx

Not inverted inverted' => Dual (RecvSession inverted idx) (SendSession inverted' idx)

Not inverted inverted' => Dual (SendSession inverted idx) (RecvSession inverted' idx)

data RecvSession inverted idx

Source

Constructors

RecvSession inverted idx

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))))

(Show inverted, Show idx) => Show (RecvSession inverted idx)

SValidSessionType idx => SNonTerminal (RecvSession inverted idx)

SNoJumpsBeyond l idx => SNoJumpsBeyond (RecvSession inverted l) idx

Not inverted inverted' => Dual (RecvSession inverted idx) (SendSession inverted' idx)

Not inverted inverted' => Dual (SendSession inverted idx) (RecvSession inverted' idx)

data Send t

Source

Constructors

Send t

Instances

SNonTerminal (Send t)

SNoJumpsBeyond (Send t) idx

Dual (Recv t) (Send t)

Dual (Send t) (Recv t)

NextSend (Cons (Send ((,) sp t)) nxt) (Send ((,) sp t)) nxt

data Recv t

Source

Constructors

Recv t

Instances

SNonTerminal (Recv t)

SNoJumpsBeyond (Recv t) idx

RecvOrOffer (Recv ((,) sp t)) t cur' inc'

Dual (Recv t) (Send t)

Dual (Send t) (Recv t)

data Jump l

Source

Constructors

Jump l

Instances

Show l => Show (Jump l)

TyNum l => STerminal (Jump l)

SmallerThanBool l idx True => SNoJumpsBeyond (Jump l) idx

Dual (Jump l) (Jump l)

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

Source

data Select where

Source

Constructors

Select :: lstOfLabels -> Select lstOfLabels

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)

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

Source

data Offer where

Source

Constructors

Offer :: lstOfLabels -> Offer lstOfLabels

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)

RecvOrOffer (Offer lst) (Choice lst) Nil Nil

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

Source

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

Source

Associated Types

type DualT a

Source

Methods

dual :: a -> b

Source

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)

(TyList nxt, TyList nxt', Dual val val', Dual nxt nxt') => Dual (Cons val nxt) (Cons val' nxt')

Not inverted inverted' => Dual (RecvSession inverted idx) (SendSession inverted' idx)

Not inverted inverted' => Dual (SendSession inverted idx) (RecvSession inverted' idx)

Not inverted inverted' => Dual (RecvPid inverted lst) (SendPid inverted' lst)

Not inverted inverted' => Dual (SendPid inverted lst) (RecvPid inverted' lst)

class SListOfJumps lst

Source

Instances

SListOfJumps Nil

(SListOfJumps nxt, TyNum val) => SListOfJumps (Cons (Cons (Jump val) Nil) nxt)

class SListOfSessionTypes lstOfLists

Source

Instances

SListOfSessionTypes Nil

(SValidSessionType val, SListOfSessionTypes nxt) => SListOfSessionTypes (Cons val nxt)

class SNonTerminal a

Source

Instances

SNonTerminal (Recv t)

SNonTerminal (Send t)

SValidSessionType idx => SNonTerminal (RecvSession inverted idx)

SValidSessionType idx => SNonTerminal (SendSession inverted idx)

SNonTerminal (RecvPid inverted t)

SNonTerminal (SendPid inverted t)

class STerminal a

Source

Instances

STerminal End

SListOfJumps (Cons val nxt) => STerminal (Offer (Cons val nxt))

SListOfJumps (Cons val nxt) => STerminal (Select (Cons val nxt))

TyNum l => STerminal (Jump l)

class SValidSessionType lst

Source

Instances

(SValidSessionType nxt, SNonTerminal val) => SValidSessionType (Cons val nxt)

STerminal a => SValidSessionType (Cons a Nil)

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

Source

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

Source

class SNoJumpsBeyond s idx

Source

Instances

SNoJumpsBeyond Nil idx

SNoJumpsBeyond End idx

SNoJumpsBeyond lol idx => SNoJumpsBeyond (Offer lol) idx

SNoJumpsBeyond lol idx => SNoJumpsBeyond (Select lol) idx

SmallerThanBool l idx True => SNoJumpsBeyond (Jump l) idx

SNoJumpsBeyond (Recv t) idx

SNoJumpsBeyond (Send t) idx

(SNoJumpsBeyond val idx, SNoJumpsBeyond nxt idx) => SNoJumpsBeyond (Cons val nxt) idx

SNoJumpsBeyond l idx => SNoJumpsBeyond (RecvSession inverted l) idx

SNoJumpsBeyond l idx => SNoJumpsBeyond (SendSession inverted l) idx

(MakeListOfJumps lol lol', SNoJumpsBeyond lol' idx) => SNoJumpsBeyond (RecvPid inverted lol) idx

(MakeListOfJumps lol lol', SNoJumpsBeyond lol' idx) => SNoJumpsBeyond (SendPid inverted lol) idx

class MakeListOfJumps x y | x -> y where

Source

Methods

makeListOfJumps :: x -> y

Source

Instances

MakeListOfJumps Nil Nil

(TyNum num, MakeListOfJumps nxt nxt', TyList nxt, TyList nxt') => MakeListOfJumps (Cons ((,) num invert) nxt) (Cons (Cons (Jump num) Nil) nxt')

class SWellFormedConfig idxA idxB ss

Source

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

Source

data Choice where

Source

Constructors

Choice :: lstOfLabels -> Choice lstOfLabels

Instances

RecvOrOffer (Offer lst) (Choice lst) Nil Nil

type family Outgoing frag

Source

class Expand prog frag expanded | prog frag -> expanded

Source

Associated Types

type ExpandT prog frag

Source

Methods

Instances

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')

Produced by Haddock version 2.4.2