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', TyListReverse lst' lst'') => lst -> SendPid False lst''

Source

recvPid :: (TyListSortNums lst lst', TyListReverse lst' lst'') => lst -> RecvPid False lst''

Source

data SendPid inverted lst

Source

Constructors

SendPid inverted lst

Instances

(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

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

data Send where

Source

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)

data Recv where

Source

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)

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)

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

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

(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

type family Outgoing prog frag

Source

class ExpandPids p a b | p a -> b where

Source

Methods

expandPids :: p -> a -> b

Source

Instances

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', Dual progO progO') => ExpandPids prog (Cons (SendPid invert t) nxt) (Cons (Send (Pid progO 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', Dual progO progO') => ExpandPids prog (Cons (RecvPid invert t) nxt) (Cons (Recv (Pid progO progO' sessionsToIdx idxsToPairStructs)) nxt')

Produced by Haddock version 2.3.0