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 |
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 |
TyListAppend nxt b nxt' => TyListAppend (Cons val nxt) b (Cons val nxt') |
TyListIndex (Cons res nxt) (D0 E) res |
(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') |
(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) |
(BuildInvertedSessionsSet nxt set, TyList set) => BuildInvertedSessionsSet (Cons ((,) init True) nxt) (Cons init set) |