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

Control.Concurrent.Session.Base.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 TyListDelete lst idx lst' | lst idx -> lst' where tyListDelete :: idx -> lst -> lst' class TySubList smaller bigger result | smaller bigger -> result where isTySubList :: smaller -> bigger -> result class TyListToList lst res | lst -> res where tyListToList :: lst -> res class TyListZip a b c | a b -> c where tyListZip :: a -> b -> c

Documentation

data Nil Source

Instances Show Nil TyList Nil SListOfSessionTypes Nil SListOfJumps Nil TyListSortNums Nil Nil TyListToSet Nil Nil MakeListOfJumps Nil Nil SNoJumpsBeyond Nil idx Dual Nil Nil TyListSnd Nil Nil SetIncomingNotify mp Nil BuildInvertedSessionsSet Nil Nil TyListZip Nil Nil Nil TySubList Nil b True TyListMember Nil val False TyListReverse' Nil acc acc TyListDrop cnt Nil Nil TyListAppend Nil b b MapSelectToList mp Nil Nil ProgramToMVarsOutgoing ref Nil Nil BuildPidTyMap' prog Nil acc acc BuildNetworkRunner prog prog' to result Nil idx MapChannelsRec Nil prog prog' current from to res keyToIdx idxToValue pid JumpsToList prog prog' to result Nil ([] a) Insert num val Nil (Cons ((,) num val) Nil) TyListToList Nil ([] res) TyListLength Nil (D0 E) TyListTake (D0 E) Nil Nil RecvOrOffer (Offer lst) (Choice lst) Nil Nil TyListTake (D0 E) (Cons val nxt) Nil

data Cons Source

Instances TyList lstA => Insert' True num val lstA (Cons ((,) num val) lstA) (ProgramToMVarsOutgoingT prog prog ~ progOut, ProgramToMVarsOutgoingT prog' prog' ~ progIn, Succ idx idxSucc, BuildNetworkRunner prog prog' to result progList idxSucc, TyListIndex progOut idx (MVar (ProgramCell (Cell outgoing))), TyListIndex progIn idx (MVar (ProgramCell (Cell incoming))), TyListIndex prog idx currentUX, Expand prog currentUX current, NetworkRuntime prog prog' ((,,) current outgoing incoming) to result) => BuildNetworkRunner prog prog' to result (Cons frag progList) idx (JumpsToList prog prog' to result jumps' ([] (SessionChain prog prog' from to result)), NetworkRuntime prog prog' ((,,) (Cons (Jump t) Nil) (Cons (Jump t) Nil) (Cons (Jump t) Nil)) to result, TypeNumberToInt t) => JumpsToList prog prog' to result (Cons (Cons (Jump t) Nil) jumps') ([] (SessionChain prog prog' from to result)) 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 (MapSelectToList mp keys vals, MapLookup mp key val, TyList vals) => MapSelectToList mp (Cons key keys) (Cons val vals) 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') (Outgoing val'' ~ val', ProgramToMVarsOutgoing ref nxt nxt', TyList nxt, TyList nxt', Expand ref val val'') => 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 BuildInvertedSessionsSet nxt set => BuildInvertedSessionsSet (Cons ((,) init False) nxt) set (TyListMember b a resMember, TySubList as b resSubList, And resMember resSubList res) => TySubList (Cons a as) b res 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 (MapChannelsRec idxs prog prog' current from to res keyToIdx idxToValue pid, MapLookup (TyMap keyToIdx idxToValue) idx (SessionState prog prog' ((,,) current from to))) => MapChannelsRec (Cons idx idxs) prog prog' current from to res keyToIdx idxToValue pid TyListAppend nxt b nxt' => TyListAppend (Cons val nxt) b (Cons val nxt') (NextSend nxt send edited, TyList edited) => NextSend (Cons (Recv ((,) sp t)) nxt) send (Cons (Recv ((,) sp t)) edited) TyListToList nxt ([] res) => TyListToList (Cons res nxt) ([] res) TyListIndex (Cons res nxt) (D0 E) res NextSend (Cons (Send ((,) sp t)) nxt) (Send ((,) sp t)) 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') (TyListSnd nxt nxt', TyList nxt, TyList nxt') => TyListSnd (Cons ((,) a b) nxt) (Cons b 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) (BuildInvertedSessionsSet nxt set, TyList set) => BuildInvertedSessionsSet (Cons ((,) init True) nxt) (Cons init set) (TyListZip as bs cs, TyList cs) => TyListZip (Cons a as) (Cons b bs) (Cons ((,) a b) cs)

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 TyListDelete lst idx lst' | lst idx -> lst' where Source

Methods tyListDelete :: idx -> lst -> lst' Source

class TySubList smaller bigger result | smaller bigger -> result where Source

Methods isTySubList :: smaller -> bigger -> result Source Instances TySubList Nil b True TySubList Nil b True (TyListMember b a resMember, TySubList as b resSubList, And resMember resSubList res) => TySubList (Cons a as) b res

class TyListToList lst res | lst -> res where Source

Methods tyListToList :: lst -> res Source Instances TyListToList Nil ([] res) TyListToList Nil ([] res) TyListToList nxt ([] res) => TyListToList (Cons res nxt) ([] res) TyListToList nxt ([] res) => TyListToList (Cons res nxt) ([] res)

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

Methods tyListZip :: a -> b -> c Source Instances TyListZip Nil Nil Nil (TyListZip as bs cs, TyList cs) => TyListZip (Cons a as) (Cons b bs) (Cons ((,) a b) cs)

Produced by Haddock version 2.4.2