sessions-2008.4.2: Session Types for Haskell Source code Contents Index

Control.Concurrent.Session.List

Description

Heterogeneous lists. This has been done many times, in many different ways. Explicit constructors are hidden deliberately.

Synopsis

data Nil data Cons class TyListLength list length | list -> length where tyListLength :: list -> length nil :: Nil cons :: TyList n => t -> n -> Cons t n modifyCons :: (TyList n1, TyList n2) => (t1 -> t2) -> (n1 -> n2) -> Cons t1 n1 -> Cons t2 n2 tyHead :: Cons t n -> t tyTail :: Cons t n -> n class TyList l class TyListIndex lst idx res | lst idx -> res where tyListIndex :: lst -> idx -> res tyListUpdate :: lst -> idx -> res -> lst class TyListUpdateVar lst1 idx val lst2 | lst1 idx val -> lst2 where tyListUpdateVar :: lst1 -> idx -> val -> lst2 class TyListTake cnt lst res | cnt lst -> res where tyListTake :: cnt -> lst -> res class TyListDrop cnt lst res | cnt lst -> res where tyListDrop :: cnt -> lst -> res class TyListAppend a b c | a b -> c where tyListAppend :: a -> b -> c class TyListReverse m n | m -> n, n -> m where tyListReverse :: m -> n class TyListElem lst val idx | lst val -> idx where tyListElem :: lst -> val -> idx class TyListMember lst val res | lst val -> res where isTyListMember :: val -> lst -> res class TyListConsSet e set set' | e set -> set' where tyListConsSet :: e -> set -> set' class TyListToSet lst set | lst -> set where tyListToSet :: lst -> set class TyListSortNums lstA lstB | lstA -> lstB where tyListSortNums :: lstA -> lstB class TyListMap a b | a -> b where tyListMap :: a -> b class TyListMapFunc x y | x -> y where tyListMapFunc :: x -> y

Documentation

data Nil Source

Instances Show Nil TyList Nil SListOfSessionTypes Nil SListOfJumps Nil TyListMap Nil Nil TyListSortNums Nil Nil TyListToSet Nil Nil MakeListOfJumps Nil Nil SNoJumpsBeyond Nil idx Dual Nil Nil FindNonEmptyIncoming mp Nil SetIncomingNotify mp Nil TyListMember Nil val False TyListReverse' Nil acc acc TyListDrop cnt Nil Nil TyListAppend Nil b b ProgramToMVarsOutgoing ref Nil Nil BuildPidTyMap' prog Nil acc acc Insert num val Nil (Cons ((,) num val) Nil) TyListLength Nil (D0 E) TyListTake (D0 E) Nil Nil TyListTake (D0 E) (Cons val nxt) Nil

data Cons Source

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', 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') (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', 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 (TyListMapFunc x x', TyListMap nxt nxt', TyList nxt, TyList nxt') => TyListMap (Cons x nxt) (Cons x' nxt') (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') (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)

class TyListLength list length | list -> length where Source

Find the length of a list. Methods tyListLength :: list -> length Source Instances TyListLength Nil (D0 E) TyListLength Nil (D0 E) (TyListLength n len, Succ len len') => TyListLength (Cons t n) len'

nil :: Nil Source

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

modifyCons :: (TyList n1, TyList n2) => (t1 -> t2) -> (n1 -> n2) -> Cons t1 n1 -> Cons t2 n2 Source

tyHead :: Cons t n -> t Source

tyTail :: Cons t n -> n Source

class TyList l Source

Instances TyList Nil TyList nxt => TyList (Cons val nxt)

class TyListIndex lst idx res | lst idx -> res where Source

Index or update a list. When updating, the type of the new value must be the same as the type of the old value. Methods tyListIndex :: lst -> idx -> res Source tyListUpdate :: lst -> idx -> res -> lst Source Instances (TyListIndex nxt idx' res, Pred idx idx', SmallerThanBool idx' len True, TyListLength nxt len) => TyListIndex (Cons val nxt) idx res TyListIndex (Cons res nxt) (D0 E) res TyListIndex (Cons res nxt) (D0 E) res

class TyListUpdateVar lst1 idx val lst2 | lst1 idx val -> lst2 where Source

Update a list but allow the type of the new value to be different from the type of the old value. Methods tyListUpdateVar :: lst1 -> idx -> val -> lst2 Source

class TyListTake cnt lst res | cnt lst -> res where Source

Take from the head of a list. Mirrors the Prelude function take. Methods tyListTake :: cnt -> lst -> res Source Instances TyListTake (D0 E) Nil Nil TyListTake (D0 E) Nil Nil TyListTake (D0 E) (Cons val nxt) Nil TyListTake (D0 E) (Cons val nxt) Nil 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 (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 (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 (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 (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 (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 (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 (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 (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') (TyListTake cnt' nxt nxt', Pred (D1 r) cnt') => TyListTake (D1 r) (Cons val nxt) (Cons val nxt')

class TyListDrop cnt lst res | cnt lst -> res where Source

Drop from the head of a list. Mirrors the Prelude function drop. Methods tyListDrop :: cnt -> lst -> res Source Instances TyListDrop cnt Nil Nil (TyListDrop cnt' nxt lst, Pred cnt cnt') => TyListDrop cnt (Cons val nxt) lst TyListDrop (D0 E) (Cons val nxt) (Cons val nxt) TyListDrop (D0 E) (Cons val nxt) (Cons val nxt)

class TyListAppend a b c | a b -> c where Source

Append two lists together. Mirrors the Prelude function '(++)'. Methods tyListAppend :: a -> b -> c Source Instances TyListAppend Nil b b TyListAppend nxt b nxt' => TyListAppend (Cons val nxt) b (Cons val nxt')

class TyListReverse m n | m -> n, n -> m where Source

Reverse a list. Methods tyListReverse :: m -> n Source

class TyListElem lst val idx | lst val -> idx where Source

Methods tyListElem :: lst -> val -> idx Source

class TyListMember lst val res | lst val -> res where Source

Methods isTyListMember :: val -> lst -> res Source Instances TyListMember Nil val False TyListMember Nil val False TyListMember nxt val res => TyListMember (Cons val' nxt) val res TyListMember (Cons val nxt) val True TyListMember (Cons val nxt) val True

class TyListConsSet e set set' | e set -> set' where Source

Methods tyListConsSet :: e -> set -> set' Source

class TyListToSet lst set | lst -> set where Source

Methods tyListToSet :: lst -> set Source Instances TyListToSet Nil Nil (TyListToSet nxt set, TyListConsSet v set set') => TyListToSet (Cons v nxt) set'

class TyListSortNums lstA lstB | lstA -> lstB where Source

Methods tyListSortNums :: lstA -> lstB Source Instances TyListSortNums Nil Nil (TyNum num, TyListSortNums nxt lst', Insert num val lst' lst'') => TyListSortNums (Cons ((,) num val) nxt) lst''

class TyListMap a b | a -> b where Source

Methods tyListMap :: a -> b Source Instances TyListMap Nil Nil (TyListMapFunc x x', TyListMap nxt nxt', TyList nxt, TyList nxt') => TyListMap (Cons x nxt) (Cons x' nxt')

class TyListMapFunc x y | x -> y where Source

Methods tyListMapFunc :: x -> y Source

Produced by Haddock version 2.3.0