-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Session Types for Haskell
--   
--   Session Types for Haskell. Allows the specification of communication
--   protocols and then validation that an implementation does not violate
--   said protocol. Ignore the build failure for hackage - it's just
--   haddock being rubbish.
@package sessions
@version 2008.5.12

module Control.Concurrent.Session.Base.Bool
type :$ a :: (* -> *) b = a b
type :. a :: (* -> *) b :: (* -> *) c = a (b c)
data True
TT :: True
data False
FF :: False
class And x y z | x y -> z
tyAnd :: (And x y z) => x -> y -> z
class Or x y z | x y -> z
tyOr :: (Or x y z) => x -> y -> z
class If c x y z | c x y -> z
tyIf :: (If c x y z) => c -> x -> y -> z
class Not x y | x -> y where { type family NotT x; }
tyNot :: (Not x y) => x -> y
instance Show False
instance Show True
instance Not False True
instance Not True False
instance If False x y y
instance If True x y x
instance Or False False False
instance Or False True True
instance Or True y True
instance And False y False
instance And True False False
instance And True True True


-- | Type level Integers. These are all base 10.
module Control.Concurrent.Session.Base.Number
data E
E :: E
data D0 n
D0 :: n -> D0 n
data D1 n
D1 :: n -> D1 n
data D2 n
D2 :: n -> D2 n
data D3 n
D3 :: n -> D3 n
data D4 n
D4 :: n -> D4 n
data D5 n
D5 :: n -> D5 n
data D6 n
D6 :: n -> D6 n
data D7 n
D7 :: n -> D7 n
data D8 n
D8 :: n -> D8 n
data D9 n
D9 :: n -> D9 n
class Succ x y | x -> y
tySucc :: (Succ x y) => x -> y
class Pred x y | x -> y
tyPred :: (Pred x y) => x -> y
class Add m n s | m n -> s
tyAdd :: (Add m n s) => m -> n -> s
class SmallerThan x y
class SmallerThanBool x y res | x y -> res
isSmallerThan :: (SmallerThanBool x y res) => x -> y -> res
class TyNum n

-- | Convert a type-level number to an Int. Of course, we can only go this
--   way...
class TypeNumberToInt ty
tyNumToInt :: (TypeNumberToInt ty) => ty -> Int
instance [overlap ok] (Show n) => Show (D9 n)
instance [overlap ok] (Show n) => Show (D8 n)
instance [overlap ok] (Show n) => Show (D7 n)
instance [overlap ok] (Show n) => Show (D6 n)
instance [overlap ok] (Show n) => Show (D5 n)
instance [overlap ok] (Show n) => Show (D4 n)
instance [overlap ok] (Show n) => Show (D3 n)
instance [overlap ok] (Show n) => Show (D2 n)
instance [overlap ok] (Show n) => Show (D1 n)
instance [overlap ok] (Show n) => Show (D0 n)
instance [overlap ok] Show E
instance [overlap ok] (Pred a b, TypeNumberToInt b) => TypeNumberToInt a
instance [overlap ok] TypeNumberToInt (D0 E)
instance [overlap ok] (TyNum n) => TyNum (D9 n)
instance [overlap ok] (TyNum n) => TyNum (D8 n)
instance [overlap ok] (TyNum n) => TyNum (D7 n)
instance [overlap ok] (TyNum n) => TyNum (D6 n)
instance [overlap ok] (TyNum n) => TyNum (D5 n)
instance [overlap ok] (TyNum n) => TyNum (D4 n)
instance [overlap ok] (TyNum n) => TyNum (D3 n)
instance [overlap ok] (TyNum n) => TyNum (D2 n)
instance [overlap ok] (TyNum n) => TyNum (D1 n)
instance [overlap ok] (TyNum n) => TyNum (D0 n)
instance [overlap ok] TyNum (D9 E)
instance [overlap ok] TyNum (D8 E)
instance [overlap ok] TyNum (D7 E)
instance [overlap ok] TyNum (D6 E)
instance [overlap ok] TyNum (D5 E)
instance [overlap ok] TyNum (D4 E)
instance [overlap ok] TyNum (D3 E)
instance [overlap ok] TyNum (D2 E)
instance [overlap ok] TyNum (D1 E)
instance [overlap ok] TyNum (D0 E)
instance [overlap ok] (Pred (D9 a) x') => Pred' (D9 a) x' True
instance [overlap ok] (Pred (D8 a) x') => Pred' (D8 a) x' True
instance [overlap ok] (Pred (D7 a) x') => Pred' (D7 a) x' True
instance [overlap ok] (Pred (D6 a) x') => Pred' (D6 a) x' True
instance [overlap ok] (Pred (D5 a) x') => Pred' (D5 a) x' True
instance [overlap ok] (Pred (D4 a) x') => Pred' (D4 a) x' True
instance [overlap ok] (Pred (D3 a) x') => Pred' (D3 a) x' True
instance [overlap ok] (Pred (D2 a) x') => Pred' (D2 a) x' True
instance [overlap ok] (Pred (D1 a) x') => Pred' (D1 a) x' True
instance [overlap ok] Pred' (D0 E) y False
instance [overlap ok] SmallerThanBool' x y False False False
instance [overlap ok] SmallerThanBool' x y True False False
instance [overlap ok] SmallerThanBool' x y False True True
instance [overlap ok] (SmallerThanBool x y res) => SmallerThanBool' x y True True res
instance [overlap ok] (Pred' x x' resX, Pred' y y' resY, SmallerThanBool' x' y' resX resY res) => SmallerThanBool x y res
instance [overlap ok] (Pred x x', Pred y y', SmallerThan x' y') => SmallerThan x y
instance [overlap ok] (Pred y y') => SmallerThan (D0 E) y
instance [overlap ok] (Add m' n' s, Pred m m', Pred n n', Succ s s', Succ s' s'') => Add m n s''
instance [overlap ok] (Pred n n') => Add (D0 E) n n
instance [overlap ok] (Pred m m') => Add m (D0 E) m
instance [overlap ok] Add (D0 E) (D0 E) (D0 E)
instance [overlap ok] (Reverse a a', DecrementRightToLeft a' b', Reverse b' b'', StripLeadingZeros b'' b) => Pred a b
instance [overlap ok] (StripLeadingZeros a b) => StripLeadingZeros (D0 a) b
instance [overlap ok] StripLeadingZeros (D9 a) (D9 a)
instance [overlap ok] StripLeadingZeros (D8 a) (D8 a)
instance [overlap ok] StripLeadingZeros (D7 a) (D7 a)
instance [overlap ok] StripLeadingZeros (D6 a) (D6 a)
instance [overlap ok] StripLeadingZeros (D5 a) (D5 a)
instance [overlap ok] StripLeadingZeros (D4 a) (D4 a)
instance [overlap ok] StripLeadingZeros (D3 a) (D3 a)
instance [overlap ok] StripLeadingZeros (D2 a) (D2 a)
instance [overlap ok] StripLeadingZeros (D1 a) (D1 a)
instance [overlap ok] StripLeadingZeros (D0 E) (D0 E)
instance [overlap ok] (DecrementRightToLeft a b) => DecrementRightToLeft (D0 a) (D9 b)
instance [overlap ok] DecrementRightToLeft (D1 a) (D0 a)
instance [overlap ok] DecrementRightToLeft (D2 a) (D1 a)
instance [overlap ok] DecrementRightToLeft (D3 a) (D2 a)
instance [overlap ok] DecrementRightToLeft (D4 a) (D3 a)
instance [overlap ok] DecrementRightToLeft (D5 a) (D4 a)
instance [overlap ok] DecrementRightToLeft (D6 a) (D5 a)
instance [overlap ok] DecrementRightToLeft (D7 a) (D6 a)
instance [overlap ok] DecrementRightToLeft (D8 a) (D7 a)
instance [overlap ok] DecrementRightToLeft (D9 a) (D8 a)
instance [overlap ok] (Reverse a a', IncrementRightToLeft a' b', Reverse b' b) => Succ a b
instance [overlap ok] (IncrementRightToLeft a b) => IncrementRightToLeft (D9 a) (D0 b)
instance [overlap ok] IncrementRightToLeft (D8 a) (D9 a)
instance [overlap ok] IncrementRightToLeft (D7 a) (D8 a)
instance [overlap ok] IncrementRightToLeft (D6 a) (D7 a)
instance [overlap ok] IncrementRightToLeft (D5 a) (D6 a)
instance [overlap ok] IncrementRightToLeft (D4 a) (D5 a)
instance [overlap ok] IncrementRightToLeft (D3 a) (D4 a)
instance [overlap ok] IncrementRightToLeft (D2 a) (D3 a)
instance [overlap ok] IncrementRightToLeft (D1 a) (D2 a)
instance [overlap ok] IncrementRightToLeft (D0 a) (D1 a)
instance [overlap ok] IncrementRightToLeft E (D1 E)
instance [overlap ok] (Reverse' n (D9 a) r) => Reverse' (D9 n) a r
instance [overlap ok] (Reverse' n (D8 a) r) => Reverse' (D8 n) a r
instance [overlap ok] (Reverse' n (D7 a) r) => Reverse' (D7 n) a r
instance [overlap ok] (Reverse' n (D6 a) r) => Reverse' (D6 n) a r
instance [overlap ok] (Reverse' n (D5 a) r) => Reverse' (D5 n) a r
instance [overlap ok] (Reverse' n (D4 a) r) => Reverse' (D4 n) a r
instance [overlap ok] (Reverse' n (D3 a) r) => Reverse' (D3 n) a r
instance [overlap ok] (Reverse' n (D2 a) r) => Reverse' (D2 n) a r
instance [overlap ok] (Reverse' n (D1 a) r) => Reverse' (D1 n) a r
instance [overlap ok] (Reverse' n (D0 a) r) => Reverse' (D0 n) a r
instance [overlap ok] Reverse' E a a
instance [overlap ok] (Reverse' x E y) => Reverse x y


-- | Heterogeneous lists. This has been done many times, in many different
--   ways. Explicit constructors are hidden deliberately.
module Control.Concurrent.Session.Base.List
data Nil :: *
data Cons :: * -> * -> *

-- | Find the length of a list.
class TyListLength list length | list -> length
tyListLength :: (TyListLength list length) => 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

-- | Index or update a list. When updating, the type of the new value must
--   be the same as the type of the old value.
class TyListIndex lst idx res | lst idx -> res
tyListIndex :: (TyListIndex lst idx res) => lst -> idx -> res
tyListUpdate :: (TyListIndex lst idx res) => lst -> idx -> res -> lst

-- | Update a list but allow the type of the new value to be different from
--   the type of the old value.
class TyListUpdateVar lst1 idx val lst2 | lst1 idx val -> lst2
tyListUpdateVar :: (TyListUpdateVar lst1 idx val lst2) => lst1 -> idx -> val -> lst2

-- | Take from the head of a list. Mirrors the <a>Prelude</a> function
--   <a>take</a>.
class TyListTake cnt lst res | cnt lst -> res
tyListTake :: (TyListTake cnt lst res) => cnt -> lst -> res

-- | Drop from the head of a list. Mirrors the <a>Prelude</a> function
--   <a>drop</a>.
class TyListDrop cnt lst res | cnt lst -> res
tyListDrop :: (TyListDrop cnt lst res) => cnt -> lst -> res

-- | Append two lists together. Mirrors the <a>Prelude</a> function '(++)'.
class TyListAppend a b c | a b -> c
tyListAppend :: (TyListAppend a b c) => a -> b -> c

-- | Reverse a list.
class TyListReverse m n | m -> n, n -> m
tyListReverse :: (TyListReverse m n) => m -> n
class TyListElem lst val idx | lst val -> idx
tyListElem :: (TyListElem lst val idx) => lst -> val -> idx
class TyListMember lst val res | lst val -> res
isTyListMember :: (TyListMember lst val res) => val -> lst -> res
class TyListConsSet e set set' | e set -> set'
tyListConsSet :: (TyListConsSet e set set') => e -> set -> set'
class TyListToSet lst set | lst -> set
tyListToSet :: (TyListToSet lst set) => lst -> set
class TyListSortNums lstA lstB | lstA -> lstB
tyListSortNums :: (TyListSortNums lstA lstB) => lstA -> lstB
class TyListDelete lst idx lst' | lst idx -> lst'
tyListDelete :: (TyListDelete lst idx lst') => idx -> lst -> lst'
class TySubList smaller bigger result | smaller bigger -> result
isTySubList :: (TySubList smaller bigger result) => smaller -> bigger -> result
instance [overlap ok] (TyListMember b a resMember, TySubList as b resSubList, And resMember resSubList res) => TySubList (Cons a as) b res
instance [overlap ok] TySubList Nil b True
instance [overlap ok] (Insert num val nxt lstB, TyList lstB) => Insert' False num val (Cons (num', val') nxt) (Cons (num', val') lstB)
instance [overlap ok] (TyList lstA) => Insert' True num val lstA (Cons (num, val) lstA)
instance [overlap ok] (SmallerThanBool num num' isSmaller, Insert' isSmaller num val (Cons (num', val') nxt) lstB) => Insert num val (Cons (num', val') nxt) lstB
instance [overlap ok] Insert num val Nil (Cons (num, val) Nil)
instance [overlap ok] (TyNum num, TyListSortNums nxt lst', Insert num val lst' lst'') => TyListSortNums (Cons (num, val) nxt) lst''
instance [overlap ok] TyListSortNums Nil Nil
instance [overlap ok] (TyListToSet nxt set, TyListConsSet v set set') => TyListToSet (Cons v nxt) set'
instance [overlap ok] TyListToSet Nil Nil
instance [overlap ok] TyListConsSet' True e set set
instance [overlap ok] (TyList set) => TyListConsSet' False e set (Cons e set)
instance [overlap ok] (TyListMember set e res, TyListConsSet' res e set set') => TyListConsSet e set set'
instance [overlap ok] (TyListMember nxt val res) => TyListMember (Cons val' nxt) val res
instance [overlap ok] TyListMember (Cons val nxt) val True
instance [overlap ok] TyListMember Nil val False
instance [overlap ok] (TyListTake idx lst prefix, Succ idx idxS, TyListDrop idxS lst suffix, TyListAppend prefix suffix lst') => TyListDelete lst idx lst'
instance [overlap ok] (TyListReverse' nxt (Cons v acc) n, TyList acc) => TyListReverse' (Cons v nxt) acc n
instance [overlap ok] TyListReverse' Nil acc acc
instance [overlap ok] (TyListReverse' m Nil n) => TyListReverse m n
instance [overlap ok] (Succ acc acc', TyListElem' nxt acc' val idx) => TyListElem' (Cons val' nxt) acc val idx
instance [overlap ok] TyListElem' (Cons val nxt) idx val idx
instance [overlap ok] (TyListElem' lst (D0 E) val idx) => TyListElem lst val idx
instance [overlap ok] (TyListTake cnt' nxt nxt', Pred (D9 r) cnt') => TyListTake (D9 r) (Cons val nxt) (Cons val nxt')
instance [overlap ok] (TyListTake cnt' nxt nxt', Pred (D8 r) cnt') => TyListTake (D8 r) (Cons val nxt) (Cons val nxt')
instance [overlap ok] (TyListTake cnt' nxt nxt', Pred (D7 r) cnt') => TyListTake (D7 r) (Cons val nxt) (Cons val nxt')
instance [overlap ok] (TyListTake cnt' nxt nxt', Pred (D6 r) cnt') => TyListTake (D6 r) (Cons val nxt) (Cons val nxt')
instance [overlap ok] (TyListTake cnt' nxt nxt', Pred (D5 r) cnt') => TyListTake (D5 r) (Cons val nxt) (Cons val nxt')
instance [overlap ok] (TyListTake cnt' nxt nxt', Pred (D4 r) cnt') => TyListTake (D4 r) (Cons val nxt) (Cons val nxt')
instance [overlap ok] (TyListTake cnt' nxt nxt', Pred (D3 r) cnt') => TyListTake (D3 r) (Cons val nxt) (Cons val nxt')
instance [overlap ok] (TyListTake cnt' nxt nxt', Pred (D2 r) cnt') => TyListTake (D2 r) (Cons val nxt) (Cons val nxt')
instance [overlap ok] (TyListTake cnt' nxt nxt', Pred (D1 r) cnt') => TyListTake (D1 r) (Cons val nxt) (Cons val nxt')
instance [overlap ok] TyListTake (D0 E) (Cons val nxt) Nil
instance [overlap ok] TyListTake (D0 E) Nil Nil
instance [overlap ok] (TyListDrop cnt' nxt lst, Pred cnt cnt') => TyListDrop cnt (Cons val nxt) lst
instance [overlap ok] TyListDrop cnt Nil Nil
instance [overlap ok] TyListDrop (D0 E) (Cons val nxt) (Cons val nxt)
instance [overlap ok] (TyListAppend nxt b nxt') => TyListAppend (Cons val nxt) b (Cons val nxt')
instance [overlap ok] TyListAppend Nil b b
instance [overlap ok] (TyListTake idx lst1 prefix, TyListDrop idxP lst1 suffix, Succ idx idxP, TyListAppend prefix (Cons val suffix) lst2) => TyListUpdateVar lst1 idx val lst2
instance [overlap ok] (TyListIndex nxt idx' res, Pred idx idx', SmallerThanBool idx' len True, TyListLength nxt len) => TyListIndex (Cons val nxt) idx res
instance [overlap ok] TyListIndex (Cons res nxt) (D0 E) res
instance [overlap ok] (TyList nxt) => TyList (Cons val nxt)
instance [overlap ok] TyList Nil
instance [overlap ok] (TyListLength n l, Succ l l', Show n, Show t) => Show (Cons t n)
instance [overlap ok] Show Nil
instance [overlap ok] (TyListLength n len, Succ len len') => TyListLength (Cons t n) len'
instance [overlap ok] TyListLength Nil (D0 E)


-- | Heterogeneous maps at the type level. Obviously equality is done on
--   types and not values. Duplicate keys are not permitted, as you'd
--   expect.
module Control.Concurrent.Session.Base.Map
data TyMap keyToIdx idxToValue
TM :: keyToIdx -> idxToValue -> TyMap keyToIdx idxToValue
emptyMap :: TyMap Nil Nil

-- | Insert into a map. Remember, the values are irrelevant, it's only the
--   types that matter. Inserting a key that already exists is not
--   permitted.
class MapInsert m1 key val m2 | m1 key val -> m2
mapInsert :: (MapInsert m1 key val m2) => key -> val -> m1 -> m2

-- | lookup in a map. Will call fail in Monad if it's not there.
class MapLookup mp key val | mp key -> val
mapLookup :: (MapLookup mp key val) => mp -> key -> val

-- | Update a map. The key must already be in the map. The value is the
--   type of the value, if you see what I mean and so obviously, updating
--   the map means changing the type of the value.
class MapUpdate mp key val' mp' | mp key val' -> mp'
mapUpdate :: (MapUpdate mp key val' mp') => mp -> key -> val' -> mp'

-- | Find the size of a map.
class MapSize mp size | mp -> size
mapSize :: (MapSize mp size) => mp -> size
tyMapKeys :: TyMap keyToIdx idxToValue -> keyToIdx
class MapDelete mp key mp' | mp key -> mp'
mapDelete :: (MapDelete mp key mp') => mp -> key -> mp'
instance (Show keyToIdx, Show idxToValue) => Show (TyMap keyToIdx idxToValue)
instance (TyListElem keyToIdx key idx, TyListTake idx keyToIdx keyToIdxPrefix, TyListTake idx idxToValue idxToValuePrefix, TyListDrop idxP keyToIdx keyToIdxSuffix, TyListDrop idxP idxToValue idxToValueSuffix, Succ idx idxP, Pred idxP idx, TyListAppend keyToIdxPrefix keyToIdxSuffix keyToIdx', TyListAppend idxToValuePrefix idxToValueSuffix idxToValue') => MapDelete (TyMap keyToIdx idxToValue) key (TyMap keyToIdx' idxToValue')
instance (TyListLength keyToIdx len) => MapSize (TyMap keyToIdx idxToValue) len
instance (TyListUpdateVar idxToValue idx val' idxToValue', TyListElem keyToIdx key idx, MapLookup (TyMap keyToIdx idxToValue') key val') => MapUpdate (TyMap keyToIdx idxToValue) key val' (TyMap keyToIdx idxToValue')
instance (TyListElem keyToIdx key idx, TyListIndex idxToValue idx val) => MapLookup (TyMap keyToIdx idxToValue) key val
instance (TyListLength keyToIdx newIdx, TyListReverse keyToIdx keyToIdxRev, TyListReverse (Cons key keyToIdxRev) keyToIdx', TyListUpdateVar idxToValue newIdx value idxToValue', TyList keyToIdxRev, MapDelete (TyMap keyToIdx' idxToValue') key (TyMap keyToIdx idxToValue)) => MapInsert' False (TyMap keyToIdx idxToValue) key value (TyMap keyToIdx' idxToValue')
instance (TyListMember keyToIdx key res, MapInsert' res (TyMap keyToIdx idxToValue) key val (TyMap keyToIdx' idxToValue'), MapDelete (TyMap keyToIdx' idxToValue') key (TyMap keyToIdx idxToValue)) => MapInsert (TyMap keyToIdx idxToValue) key val (TyMap keyToIdx' idxToValue')


-- | Super magic Monads.
module Control.Concurrent.Session.Base.SMonad
newtype SChain m x y a
SChain :: (x -> m (a, y)) -> SChain m x y a
runSChain :: SChain m x y a -> x -> m (a, y)

-- | An extension of the typical Monad such that you track additional
--   <tt>from</tt> and <tt>to</tt> parameters. Thus you can think of this
--   like <a>State</a> where the type of the <a>State</a> varies.
class SMonad m :: (* -> * -> * -> *)
(~>>) :: (SMonad m) => m x y a -> m y z b -> m x z b
(~>>=) :: (SMonad m) => m x y a -> (a -> m y z b) -> m x z b
sreturn :: (SMonad m) => a -> m x x a
newtype SStateT s m x y a
SStateT :: (s -> m x y (a, s)) -> SStateT s m x y a
runSStateT :: SStateT s m x y a -> s -> m x y (a, s)
class SMonadTrans t
slift :: (SMonadTrans t, SMonad m) => m x y a -> t m x y a
class (SMonad m) => SMonadIO m
sliftIO :: (SMonadIO m) => IO a -> m x x a
class (SMonad m) => SMonadState s m | m -> s
sget :: (SMonadState s m) => m x x s
sput :: (SMonadState s m) => s -> m x x ()
ssequence_ :: (SMonad m) => [m x x a] -> m x x ()
ssequence :: (SMonad m) => [m x x a] -> m x x [a]
sjoin :: (SMonad m) => m x y (m y z b) -> m x z b
smapM :: (SMonad m) => (a -> m x x b) -> [a] -> m x x [b]
smapM_ :: (SMonad m) => (a -> m x x b) -> [a] -> m x x ()
instance (SMonad m) => SMonadState s (SStateT s m)
instance (MonadIO m) => SMonadIO (SChain m)
instance SMonadTrans (SStateT s)
instance (SMonad m) => SMonad (SStateT s m)
instance (Monad m) => Monad (SChain m x x)
instance (Monad m) => SMonad (SChain m)


-- | 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 <a>Control.Concurrent.Session.Tests</a> for examples
module Control.Concurrent.Session.SessionType
data End
End :: End
end :: Cons End Nil
sendPid :: (TyListSortNums lst lst') => lst -> SendPid False lst'
recvPid :: (TyListSortNums lst lst') => lst -> RecvPid False lst'
data SendPid inverted lst
SendPid :: inverted -> lst -> SendPid inverted lst
data RecvPid inverted lst
RecvPid :: inverted -> lst -> RecvPid inverted lst
sendSession :: idx -> SendSession False idx
recvSession :: idx -> RecvSession False idx
data SendSession inverted idx
SendSession :: inverted -> idx -> SendSession inverted idx
data RecvSession inverted idx
RecvSession :: inverted -> idx -> RecvSession inverted idx
data Send t
Send :: t -> Send t
data Recv t
Recv :: t -> Recv t
data Jump l
Jump :: l -> Jump l
jump :: (TyNum n) => n -> Cons (Jump n) Nil
data Select :: * -> *
Select :: lstOfLabels -> Select lstOfLabels
select :: (SListOfJumps (Cons val nxt)) => (Cons val nxt) -> Cons (Select (Cons val nxt)) Nil
data Offer :: * -> *
Offer :: lstOfLabels -> Offer lstOfLabels
offer :: (SListOfJumps (Cons val nxt)) => (Cons val nxt) -> Cons (Offer (Cons val nxt)) Nil
class Dual a b | a -> b, b -> a where { type family DualT a; }
dual :: (Dual a b) => a -> b
class SListOfJumps lst
class SListOfSessionTypes lstOfLists
class SNonTerminal a
class STerminal a
class SValidSessionType lst
(~>) :: (TyList nxt, SNonTerminal a, SValidSessionType nxt) => a -> nxt -> (Cons a nxt)
(~|~) :: (TyNum target, TyList nxt) => target -> nxt -> Cons (Cons (Jump target) Nil) nxt
class SNoJumpsBeyond s idx
class MakeListOfJumps x y | x -> y
makeListOfJumps :: (MakeListOfJumps x y) => x -> y
class SWellFormedConfig idxA idxB ss
testWellformed :: (SWellFormedConfig idxA idxB ss) => ss -> idxA -> idxB -> Bool
data Choice :: * -> *
Choice :: lstOfLabels -> Choice lstOfLabels
class Expand prog frag expanded | prog frag -> expanded where { type family ExpandT prog frag; }
instance [overlap ok] (Show l) => Show (Jump l)
instance [overlap ok] (Show inverted, Show idx) => Show (RecvSession inverted idx)
instance [overlap ok] (Show inverted, Show idx) => Show (SendSession inverted idx)
instance [overlap ok] (Show inverted, Show lst) => Show (RecvPid inverted lst)
instance [overlap ok] (Show inverted, Show lst) => Show (SendPid inverted lst)
instance [overlap ok] Show End
instance [overlap ok] Expand prog (Cons End Nil) (Cons End Nil)
instance [overlap ok] Expand prog (Cons (Jump l) Nil) (Cons (Jump l) Nil)
instance [overlap ok] Expand prog (Cons (Offer loj) Nil) (Cons (Offer loj) Nil)
instance [overlap ok] Expand prog (Cons (Select loj) Nil) (Cons (Select loj) Nil)
instance [overlap ok] (Expand prog nxt nxt') => Expand prog (Cons (Recv t) nxt) (Cons (Recv t) nxt')
instance [overlap ok] (Expand prog nxt nxt') => Expand prog (Cons (Send t) nxt) (Cons (Send t) nxt')
instance [overlap ok] (SListOfSessionTypes ss, TyListLength ss len, SNoJumpsBeyond ss len, SmallerThanBool idxA len True, TyListIndex ss idxA st, TyListLength st len', SmallerThanBool idxB len' True) => SWellFormedConfig idxA idxB ss
instance [overlap ok] (TyNum num, MakeListOfJumps nxt nxt', TyList nxt, TyList nxt') => MakeListOfJumps (Cons (num, invert) nxt) (Cons (Cons (Jump num) Nil) nxt')
instance [overlap ok] MakeListOfJumps Nil Nil
instance [overlap ok] (SNoJumpsBeyond val idx, SNoJumpsBeyond nxt idx) => SNoJumpsBeyond (Cons val nxt) idx
instance [overlap ok] SNoJumpsBeyond Nil idx
instance [overlap ok] (SNoJumpsBeyond l idx) => SNoJumpsBeyond (RecvSession inverted l) idx
instance [overlap ok] (SNoJumpsBeyond l idx) => SNoJumpsBeyond (SendSession inverted l) idx
instance [overlap ok] (MakeListOfJumps lol lol', SNoJumpsBeyond lol' idx) => SNoJumpsBeyond (RecvPid inverted lol) idx
instance [overlap ok] (MakeListOfJumps lol lol', SNoJumpsBeyond lol' idx) => SNoJumpsBeyond (SendPid inverted lol) idx
instance [overlap ok] (SNoJumpsBeyond lol idx) => SNoJumpsBeyond (Offer lol) idx
instance [overlap ok] (SNoJumpsBeyond lol idx) => SNoJumpsBeyond (Select lol) idx
instance [overlap ok] SNoJumpsBeyond (Recv t) idx
instance [overlap ok] SNoJumpsBeyond (Send t) idx
instance [overlap ok] (SmallerThanBool l idx True) => SNoJumpsBeyond (Jump l) idx
instance [overlap ok] SNoJumpsBeyond End idx
instance [overlap ok] (SValidSessionType nxt, SNonTerminal val) => SValidSessionType (Cons val nxt)
instance [overlap ok] (STerminal a) => SValidSessionType (Cons a Nil)
instance [overlap ok] (SListOfJumps (Cons val nxt)) => STerminal (Offer (Cons val nxt))
instance [overlap ok] (SListOfJumps (Cons val nxt)) => STerminal (Select (Cons val nxt))
instance [overlap ok] (TyNum l) => STerminal (Jump l)
instance [overlap ok] STerminal End
instance [overlap ok] (SValidSessionType idx) => SNonTerminal (RecvSession inverted idx)
instance [overlap ok] (SValidSessionType idx) => SNonTerminal (SendSession inverted idx)
instance [overlap ok] SNonTerminal (RecvPid inverted t)
instance [overlap ok] SNonTerminal (SendPid inverted t)
instance [overlap ok] SNonTerminal (Recv t)
instance [overlap ok] SNonTerminal (Send t)
instance [overlap ok] (SValidSessionType val, SListOfSessionTypes nxt) => SListOfSessionTypes (Cons val nxt)
instance [overlap ok] SListOfSessionTypes Nil
instance [overlap ok] (SListOfJumps nxt, TyNum val) => SListOfJumps (Cons (Cons (Jump val) Nil) nxt)
instance [overlap ok] SListOfJumps Nil
instance [overlap ok] (TyList nxt, TyList nxt', Dual val val', Dual nxt nxt') => Dual (Cons val nxt) (Cons val' nxt')
instance [overlap ok] Dual Nil Nil
instance [overlap ok] (Not inverted inverted') => Dual (RecvSession inverted idx) (SendSession inverted' idx)
instance [overlap ok] (Not inverted inverted') => Dual (SendSession inverted idx) (RecvSession inverted' idx)
instance [overlap ok] Dual (Offer lst) (Select lst)
instance [overlap ok] Dual (Select lst) (Offer lst)
instance [overlap ok] (Not inverted inverted') => Dual (RecvPid inverted lst) (SendPid inverted' lst)
instance [overlap ok] (Not inverted inverted') => Dual (SendPid inverted lst) (RecvPid inverted' lst)
instance [overlap ok] Dual (Recv t) (Send t)
instance [overlap ok] Dual (Send t) (Recv t)
instance [overlap ok] Dual (Jump l) (Jump l)
instance [overlap ok] Dual End End

module Control.Concurrent.Session.Types
data Cell :: * -> *
Cell :: val -> MVar (Cell nxt) -> Cell (Cons val nxt)
SelectCell :: Int -> Cell (Cons (Choice jumps) Nil)
data ProgramCell :: * -> *
ProgramCell :: MVar a -> MVar (ProgramCell a) -> ProgramCell a
class ProgramToMVarsOutgoing progRef prog mvars | progRef prog -> mvars where { type family ProgramToMVarsOutgoingT progRef prog; }
programToMVarsOutgoing :: (ProgramToMVarsOutgoing progRef prog mvars) => progRef -> prog -> IO mvars
data SessionState :: * -> * -> * -> *
SessionState :: progOut -> progIn -> current -> MVar (Maybe (Chan ())) -> (MVar (Cell currentOutgoing)) -> MVar (Maybe (Chan ())) -> (MVar (Cell currentIncoming)) -> SessionState prog prog' (current, currentOutgoing, currentIncoming)

-- | The representation of a computation that performs work using session
--   types. Again, really quite similar to a more-parameterized State
--   monad.
newtype SessionChain prog prog' from to res
SessionChain :: ((SessionState prog prog' from) -> IO (res, SessionState prog prog' to)) -> SessionChain prog prog' from to res
runSessionChain :: SessionChain prog prog' from to res -> (SessionState prog prog' from) -> IO (res, SessionState prog prog' to)
type RawPid = [Int]

-- | A process ID. This is a tiny bit like ThreadId but rather heavily
--   annotated.
data Pid :: * -> * -> * -> * -> * -> *
Pid :: RawPid -> TyMap sessionsToIdx idxsToPairStructs -> Pid prog prog' invertedSessions sessionsToIdx idxsToPairStructs
data InternalPid :: * -> * -> * -> * -> * -> *
IPid :: Pid prog prog' invertedSessions sessionsToIdx idxsToPairStructs -> [RawPid] -> InternalPid prog prog' invertedSessions sessionsToIdx idxsToPairStructs
pidToRawPid :: Pid prog prog' invertedSessions sessionsToIdx idxsToPairStructs -> RawPid
iPidToPid :: InternalPid prog prog' invertedSessions sessionsToIdx idxsToPairStructs -> Pid prog prog' invertedSessions sessionsToIdx idxsToPairStructs

-- | Provides a way to compare two Pids. Of course, if the Pids have
--   different type params, then they are definitely different, but it's
--   still convenient to be able to do something like (==) on them.
class PidEq a b
(=~=) :: (PidEq a b) => a -> b -> Bool
newtype InterleavedChain internalPid from to res
InterleavedChain :: (internalPid -> from -> IO (res, to, internalPid)) -> InterleavedChain internalPid from to res
runInterleavedChain :: InterleavedChain internalPid from to res -> internalPid -> from -> IO (res, to, internalPid)
data SpecialSession
data SpecialPid
data SpecialNormal
data PairStruct :: * -> * -> * -> * -> *
PS :: RawPid -> (SessionState prog prog' (Cons (Jump init) Nil, Cons (Jump init) Nil, Cons (Jump init) Nil) -> IO ()) -> PairStruct init prog prog' (Cons (Jump init) Nil, Cons (Jump init) Nil, Cons (Jump init) Nil)
instance Ord (PairStruct init prog prog' start)
instance Eq (PairStruct init prog prog' start)
instance SMonadIO (InterleavedChain internalPid)
instance SMonad (InterleavedChain internalPid)
instance PidEq (Pid progA progA' invertedSessionsA sessionsToIdxA idxsToPairStructsA) (Pid progB progB' invertedSessionsB sessionsToIdxB idxsToPairStructsB)
instance Ord (InternalPid prog prog' invertedSessions sessionsToIdx idxsToPairStructs)
instance Eq (InternalPid prog prog' invertedSessions sessionsToIdx idxsToPairStructs)
instance Ord (Pid prog prog' invertedSessions sessionsToIdx idxsToPairStructs)
instance Eq (Pid prog prog' invertedSessions sessionsToIdx idxsToPairStructs)
instance Show (Pid prog prog' invertedSessions sessionsToIdx idxsToPairStructs)
instance SMonadIO (SessionChain prog prog')
instance SMonad (SessionChain prog prog')
instance (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')
instance ProgramToMVarsOutgoing ref Nil Nil

module Control.Concurrent.Session.SessionTypeMonad
data TypeState :: * -> * -> * -> * -> *
TypeState :: nxtLabel -> declareable -> useable -> st -> TypeState nxtLabel declareable useable st
newtype SessionType f t r
SessionType :: (f -> (r, t)) -> SessionType f t r
buildSessionType :: SessionType f t r -> f -> (r, t)
newLabel :: (Succ nxtLabel nxtLabel', TyListConsSet nxtLabel declareable declareable', TyListConsSet nxtLabel useable useable') => SessionType (TypeState nxtLabel declareable useable st) (TypeState nxtLabel' declareable' useable' st) nxtLabel
declareLabel :: (TyListMember declareable label True, TyListElem declareable label idx, TyListDelete declareable idx declareable', TyList st) => label -> (SessionType (TypeState nxtLabel declareable' useable (Cons (label, Nil) st)) (TypeState nxtLabel' declareable'' useable' st') a) -> SessionType (TypeState nxtLabel declareable useable st) (TypeState nxtLabel' declareable'' useable' st') a
(.=) :: (TyListMember declareable label True, TyListElem declareable label idx, TyListDelete declareable idx declareable', TyList st) => label -> (SessionType (TypeState nxtLabel declareable' useable (Cons (label, Nil) st)) (TypeState nxtLabel' declareable'' useable' st') a) -> SessionType (TypeState nxtLabel declareable useable st) (TypeState nxtLabel' declareable'' useable' st') a
send :: (TyList f, TyList fs) => t -> SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs)) (TypeState nxtLabel declareable useable (Cons (label, Cons (Send (SpecialNormal, t)) f) fs)) ()
recv :: (TyList f, TyList fs) => t -> SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs)) (TypeState nxtLabel declareable useable (Cons (label, Cons (Recv (SpecialNormal, t)) f) fs)) ()
sendPid :: (TyList f, TyList fs, TyListSortNums lst lst') => lst -> SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs)) (TypeState nxtLabel declareable useable (Cons (label, Cons (SendPid False lst') f) fs)) ()
recvPid :: (TyList f, TyList fs, TyListSortNums lst lst') => lst -> SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs)) (TypeState nxtLabel declareable useable (Cons (label, Cons (RecvPid False lst') f) fs)) ()
sendSession :: (TyList f, TyList fs, TyList fs', TyListReverse frag fragRev, TyListTake (D1 E) fragRev (Cons (label, fragHead) Nil), TyListDrop (D1 E) fragRev fragTailRev, TyListReverse fragTailRev fragTail, TyListAppend fragTail fs fs') => SessionType (TypeState nxtLabel declareable useable (Cons (label, Nil) Nil)) (TypeState nxtLabel' declareable' useable' frag) res -> SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs)) (TypeState nxtLabel' declareable' useable' (Cons (label, Cons (SendSession False fragHead) f) fs')) res
recvSession :: (TyList f, TyList fs, TyList fs', TyListReverse frag fragRev, TyListTake (D1 E) fragRev (Cons (label, fragHead) Nil), TyListDrop (D1 E) fragRev fragTailRev, TyListReverse fragTailRev fragTail, TyListAppend fragTail fs fs') => SessionType (TypeState nxtLabel declareable useable (Cons (label, Nil) Nil)) (TypeState nxtLabel' declareable' useable' frag) res -> SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs)) (TypeState nxtLabel' declareable' useable' (Cons (label, Cons (RecvSession False fragHead) f) fs')) res
end :: (TyListReverse (Cons End f) f', TyList f, TyList fs) => SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs)) (TypeState nxtLabel declareable useable (Cons (label, f') fs)) ()
jump :: (TyListReverse (Cons (Jump jt) f) f', TyList f, TyList fs, TyListMember useable jt True) => jt -> SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs)) (TypeState nxtLabel declareable useable (Cons (label, f') fs)) ()
data BranchesList :: * -> * -> * -> * -> * -> *
BLNil :: BranchesList Nil Nil z z z
BLCons :: (SessionType (TypeState nxtLabel declareable useable st) (TypeState nxtLabel' declareable' useable' st') (resLst -> Cons res resLst, labs -> Cons (Cons (Jump nxtLabel) Nil) labs)) -> (BranchesList resLst labs (TypeState nxtLabel' declareable' useable' st') to finalTo) -> BranchesList (Cons res resLst) (Cons (Cons (Jump nxtLabel) Nil) labs) (TypeState nxtLabel declareable useable st) (TypeState nxtLabel' declareable' useable' st', to) finalTo
(~|~) :: (Succ label nxtLabel, TyListConsSet label declareable declareable', TyListElem declareable' label idx, TyListDelete declareable' idx declareable'', TyListConsSet label useable useable', TyList st, TyListMember declareable' label True, TyList labs, TyList resLst) => (SessionType (TypeState nxtLabel declareable'' useable' (Cons (label, Nil) st)) (TypeState nxtLabel' declareable''' useable'' st') res) -> (BranchesList resLst labs (TypeState nxtLabel' declareable''' useable'' st') to finalTo) -> (BranchesList (Cons res resLst) (Cons (Cons (Jump label) Nil) labs) (TypeState label declareable useable st) (TypeState nxtLabel' declareable''' useable'' st', to) finalTo)
class BuildBranches bl st
buildBranches :: (BuildBranches bl st) => bl -> st
select :: (TyListReverse (Cons (Select listOfJumps) f) f', TyList f, TyList fs, BuildBranches (BranchesList listOfRes listOfJumps (TypeState nxtLabel declareable useable (Cons (label, f') fs)) to finalTo) (SessionType (TypeState nxtLabel declareable useable (Cons (label, f') fs)) finalTo (listOfRes, listOfJumps))) => (BranchesList listOfRes listOfJumps (TypeState nxtLabel declareable useable (Cons (label, f') fs)) to finalTo) -> (SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs)) finalTo listOfRes)
offer :: (TyListReverse (Cons (Offer listOfJumps) f) f', TyList f, TyList fs, BuildBranches (BranchesList listOfRes listOfJumps (TypeState nxtLabel declareable useable (Cons (label, f') fs)) to finalTo) (SessionType (TypeState nxtLabel declareable useable (Cons (label, f') fs)) finalTo (listOfRes, listOfJumps))) => (BranchesList listOfRes listOfJumps (TypeState nxtLabel declareable useable (Cons (label, f') fs)) to finalTo) -> (SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs)) finalTo listOfRes)
currentLabel :: SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs)) (TypeState nxtLabel declareable useable (Cons (label, f) fs)) label
makeSessionType :: (TyListSortNums st st', TyListSnd st' st'') => SessionType (TypeState (D0 E) Nil Nil Nil) (TypeState nxtLabel Nil useable st) res -> (st'', res)
class TyListSnd lstA lstB | lstA -> lstB
tyListSnd :: (TyListSnd lstA lstB) => lstA -> lstB
dual :: True
notDual :: False
instance (TyListSnd nxt nxt', TyList nxt, TyList nxt') => TyListSnd (Cons (a, b) nxt) (Cons b nxt')
instance TyListSnd Nil Nil
instance (BuildBranches (BranchesList resLst labs (TypeState nxtLabel' declareable' useable' st') to finalTo) (SessionType (TypeState nxtLabel' declareable' useable' st') finalTo (resLst, labs))) => BuildBranches (BranchesList (Cons res resLst) (Cons (Cons (Jump nxtLabel) Nil) labs) (TypeState nxtLabel declareable useable st) (TypeState nxtLabel' declareable' useable' st', to) finalTo) (SessionType (TypeState nxtLabel declareable useable st) finalTo (Cons res resLst, Cons (Cons (Jump nxtLabel) Nil) labs))
instance BuildBranches (BranchesList Nil Nil (TypeState nxtLabel declareLabel useable st) (TypeState nxtLabel declareLabel useable st) (TypeState nxtLabel declareLabel useable st)) (SessionType (TypeState nxtLabel declareLabel useable st) (TypeState nxtLabel declareLabel useable st) (Nil, Nil))
instance SMonad SessionType


-- | Having actually described a session type, you'll now want to implement
--   it! Use the methods of <a>SMonad</a> to chain functions together.
module Control.Concurrent.Session.Runtime

-- | Use OfferImpls to construct the implementations of the branches of an
--   offer. Really, it's just a slightly fancy list.
data OfferImpls :: * -> * -> * -> * -> * -> *
OfferImplsNil :: OfferImpls Nil prog prog' finalState finalResult

-- | Use to construct OfferImpls. This function automatically adds the
--   necessary <a>sjump</a> to the start of each branch implementation.
(~||~) :: ((ProgramToMVarsOutgoingT prog prog) ~ progOut, (ProgramToMVarsOutgoingT prog' prog') ~ progIn, ProgramToMVarsOutgoing prog prog progOut, ProgramToMVarsOutgoing prog' prog' progIn, SWellFormedConfig l (D0 E) prog, SWellFormedConfig l (D0 E) prog', TyListIndex progOut l (MVar (ProgramCell (Cell outgoing))), TyListIndex progIn l (MVar (ProgramCell (Cell incoming))), TyListIndex prog l currentUX, Expand prog currentUX current) => (SessionChain prog prog' (current, outgoing, incoming) finalState finalResult) -> (OfferImpls jumps prog prog' finalState finalResult) -> (OfferImpls (Cons (Cons (Jump l) Nil) jumps) prog prog' finalState finalResult)

-- | Perform a jump. Now you may think that you should indicate where you
--   want to jump to. But of course, that's actually specified by the
--   session type so you don't have to specify it at all in the
--   implementation.
sjump :: ((ProgramToMVarsOutgoingT prog prog) ~ progOut, (ProgramToMVarsOutgoingT prog' prog') ~ progIn, SWellFormedConfig l (D0 E) prog, SWellFormedConfig l (D0 E) prog', TyListIndex progOut l (MVar (ProgramCell (Cell outgoing))), TyListIndex progIn l (MVar (ProgramCell (Cell incoming))), TyListIndex prog l currentUX, Expand prog currentUX current) => (SessionChain prog prog') (Cons (Jump l) Nil, Cons (Jump l) Nil, Cons (Jump l) Nil) (current, outgoing, incoming) ()

-- | Send a value to the other party. Of course, the value must be of the
--   correct type indicated in the session type.
ssend :: (CompatibleTypes sp t' t) => t' -> SessionChain prog prog' (Cons (Send (sp, t)) nxtCur, Cons t nxtOut, incoming) (nxtCur, nxtOut, incoming) ()
class CompatibleTypes special a b | special a -> b, special b -> a
convert :: (CompatibleTypes special a b) => special -> a -> b

-- | Recieve a value from the other party. This will block as necessary.
--   The type of the value received is specified by the session type. No
--   magic coercion needed.
srecv :: (SessionChain prog prog') (Cons (Recv (sp, t)) nxt, outgoing, Cons t nxt') (nxt, outgoing, nxt') t

-- | Offer a number of branches. This is basically an external choice - the
--   other party uses <a>sselect</a> to decide which branch to take. Use
--   OfferImpls in order to construct the list of implementations of
--   branches. Note that every implementation must result in the same final
--   state and emit the same value.
soffer :: OfferImpls jumps prog prog' (current, outgoing, incoming) finalResult -> (SessionChain prog prog') (Cons (Offer jumps) Nil, Cons (Choice jumps) Nil, Cons (Choice jumps) Nil) (current, outgoing, incoming) finalResult

-- | Select which branch we're taking at a branch point. Use a type number
--   (<a>Control.Concurrent.Session.Number</a>) to indicate the branch to
--   take.
sselect :: ((ProgramToMVarsOutgoingT prog prog) ~ progOut, (ProgramToMVarsOutgoingT prog' prog') ~ progIn, TyListLength jumps len, SmallerThanBool label len True, TypeNumberToInt label, TyListIndex jumps label (Cons (Jump jumpTarget) Nil), SWellFormedConfig jumpTarget (D0 E) prog, SWellFormedConfig jumpTarget (D0 E) prog', TyListIndex progOut jumpTarget (MVar (ProgramCell (Cell outgoing))), TyListIndex progIn jumpTarget (MVar (ProgramCell (Cell incoming))), TyListIndex prog jumpTarget currentUX, Expand prog currentUX current) => label -> (SessionChain prog prog') (Cons (Select jumps) Nil, Cons (Choice jumps) Nil, Cons (Choice jumps) Nil) (current, outgoing, incoming) ()

-- | Run! Provide a program and a start point within that program (which is
--   automatically <a>sjump</a>ed to), the two implementations which must
--   be duals of each other, run them, have them communicate, wait until
--   they both finish and die and then return the results from both of
--   them.
run :: (ProgramToMVarsOutgoing prog prog progOut, ProgramToMVarsOutgoing prog' prog' progIn, (ProgramToMVarsOutgoingT prog prog) ~ progOut, (ProgramToMVarsOutgoingT prog' prog') ~ progIn, SWellFormedConfig init (D0 E) prog, SWellFormedConfig init (D0 E) prog', TyListIndex progOut init (MVar (ProgramCell (Cell fromO))), TyListIndex progIn init (MVar (ProgramCell (Cell fromI))), (DualT prog) ~ prog', Dual prog prog', TyListIndex prog init currentUX, Expand prog currentUX current, TyListIndex prog' init currentUX', Expand prog' currentUX' current') => prog -> init -> SessionChain prog prog' (current, fromO, fromI) (toCur, toO, toI) res -> SessionChain prog' prog (current', fromI, fromO) (toCur', toI, toO) res' -> IO (res, res')
carefullySwapToNextCell :: MVar (ProgramCell a) -> IO (ProgramCell a)
instance CompatibleTypes SpecialSession t t
instance CompatibleTypes SpecialNormal t t
instance (ReducePairStructs (TyMap origKeys origVals) (TyMap keys vals') (TyMap accKeys' accVals') result, MapInsert (TyMap accKeys accVals) key val (TyMap accKeys' accVals'), MapLookup (TyMap origKeys origVals) key val, MapLookup (TyMap (Cons key keys) vals) key val, MapDelete (TyMap (Cons key keys) vals) key (TyMap keys vals'), TyListElem origKeys key idx, TyListIndex origKeys idx key) => ReducePairStructs (TyMap origKeys origVals) (TyMap (Cons key keys) vals) (TyMap accKeys accVals) result
instance ReducePairStructs orig (TyMap Nil Nil) acc acc
instance (TySubList invertedSessionsB invertedSessionsA True, TySubList sessionsToIdxB sessionsToIdxA True, ReducePairStructs (TyMap sessionsToIdxA idxsToPairStructsA) (TyMap sessionsToIdxB idxsToPairStructsB) (TyMap Nil Nil) (TyMap sessionsToIdxB idxsToPairStructsB)) => CompatibleTypes SpecialPid (Pid prog prog' invertedSessionsA sessionsToIdxA idxsToPairStructsA) (Pid prog prog' invertedSessionsB sessionsToIdxB idxsToPairStructsB)
instance (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)))
instance (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)))
instance (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)))
instance (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)))
instance (Expand prog nxt nxt', ExpandSession prog (RecvSession invert frag) expandedRecvSession) => Expand prog (Cons (RecvSession invert frag) nxt) (Cons expandedRecvSession nxt')
instance (Expand prog nxt nxt', ExpandSession prog (SendSession invert frag) expandedSendSession) => Expand prog (Cons (SendSession invert frag) nxt) (Cons expandedSendSession nxt')
instance WalkOfferImpls prog prog' finalState finalResult


-- | Defines what a <a>Pid</a> is and provides functionality to create new
--   sessions <i> channels to a given pid. Obviously this is </i>safe/ in
--   some way - in particular, a Pid carries about with it the set of
--   Session Types it is willing to use. This means that you can't try to
--   start any old Session Type with any given Pid. However, it doesn't
--   mean that given an acceptable Session Type, the other thread will ever
--   actually get around to agreeing to create the new session / channel
--   with you.
module Control.Concurrent.Session.Pid
makePid :: InternalPid prog prog' invertedSessionsO sessionsToIdxO idxsToPairStructsO -> invertedSessionsN -> TyMap sessionsToIdxN idxsToPairStructsN -> (InternalPid prog prog' invertedSessionsO sessionsToIdxO idxsToPairStructsO, InternalPid prog prog' invertedSessionsN sessionsToIdxN idxsToPairStructsN)
rootPid :: (Dual prog prog', (DualT prog) ~ prog') => TyMap sessionsToIdx idxsToPairStructs -> invertedSessions -> prog -> InternalPid prog prog' invertedSessions sessionsToIdx idxsToPairStructs
iPidToPid :: InternalPid prog prog' invertedSessions sessionsToIdx idxsToPairStructs -> Pid prog prog' invertedSessions sessionsToIdx idxsToPairStructs
myPid :: InterleavedChain (InternalPid prog prog' invertedSessions sessionsToIdx idxsToPairStructs) from from (Pid prog prog' invertedSessions sessionsToIdx idxsToPairStructs)
class BuildPidTyMap prog stlst tymap | prog stlst -> tymap where { type family BuildPidTyMapT prog stlst; }
buildPidTyMap :: (BuildPidTyMap prog stlst tymap) => prog -> stlst -> IO tymap
class BuildInvertedSessionsSet stlist set | stlist -> set where { type family BuildInvertedSessionsSetT stlist; }
buildInvertedSessionsSet :: (BuildInvertedSessionsSet stlist set) => stlist -> set

-- | Provides the ability to make a new session / channel with the given
--   Pid. Supply the index to the Session Type, whether or not you're
--   locally inverting (dualing) the Session Type, and the Pid, and so long
--   as the Pid supports the dual of your local Session Type, this will
--   block until the Pid gets around to servicing you. Thus this is a
--   synchronous operation and both Pids must know of each other to create
--   a new session / channel between them.
class CreateSession invert init prog prog' sessionsToIdxMe sessionsToIdxThem idxsToPairStructsMe idxsToPairStructsThem keyToIdxMe idxToValueMe keyToIdxMe' idxToValueMe' idxOfThem invertedSessionsMe invertedSessionsThem
createSession :: (CreateSession invert init prog prog' sessionsToIdxMe sessionsToIdxThem idxsToPairStructsMe idxsToPairStructsThem keyToIdxMe idxToValueMe keyToIdxMe' idxToValueMe' idxOfThem invertedSessionsMe invertedSessionsThem) => init -> invert -> Pid prog prog' invertedSessionsThem sessionsToIdxThem idxsToPairStructsThem -> InterleavedChain (InternalPid prog prog' invertedSessionsMe sessionsToIdxMe idxsToPairStructsMe) (TyMap keyToIdxMe idxToValueMe) (TyMap keyToIdxMe' idxToValueMe') idxOfThem

-- | Provides a way to compare two Pids. Of course, if the Pids have
--   different type params, then they are definitely different, but it's
--   still convenient to be able to do something like (==) on them.
class PidEq a b
(=~=) :: (PidEq a b) => a -> b -> Bool
data MultiReceive :: * -> * -> * -> * -> * -> * -> * -> * -> * -> * -> * -> *
MultiReceiveNil :: MultiReceive Nil prog prog' invertedSessions sessionsToIdx idxsToPairStructs keyToIdx idxToValue keyToIdx' idxToValue' res
(~|||~) :: (MapLookup (TyMap keyToIdx idxToValue) ch (SessionState progS progS' (Cons (Recv (sp, t)) nxt, fromO, Cons t nxt'))) => (ch, InterleavedChain (InternalPid prog prog' invertedSessions sessionsToIdx idxsToPairStructs) (TyMap keyToIdx idxToValue) (TyMap keyToIdx' idxToValue') res) -> MultiReceive chs prog prog' invertedSessions sessionsToIdx idxsToPairStructs keyToIdx idxToValue keyToIdx' idxToValue' res -> MultiReceive (Cons ch chs) prog prog' invertedSessions sessionsToIdx idxsToPairStructs keyToIdx idxToValue keyToIdx' idxToValue' res
multiReceive :: (TyListLength chs len, SmallerThanBool (D0 E) len True, SetIncomingNotify (TyMap keyToIdx idxToValue) chs, FindNonEmptyIncoming (TyMap keyToIdx idxToValue) chs, TypeNumberToInt len) => (MultiReceive chs prog prog' invertedSessions sessionsToIdx idxsToPairStructs keyToIdx idxToValue keyToIdx' idxToValue' res) -> InterleavedChain (InternalPid prog prog' invertedSessions sessionsToIdx idxsToPairStructs) (TyMap keyToIdx idxToValue) (TyMap keyToIdx' idxToValue') res
instance (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)
instance FindNonEmptyIncoming mp Nil
instance WalkMultiReceives chs prog prog' invertedSessions sessionsToIdx idxsToPairStructs keyToIdx idxToValue keyToIdx' idxToValue' res
instance (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)
instance SetIncomingNotify mp Nil
instance (ProgramToMVarsOutgoingT prog prog ~ progOut, ProgramToMVarsOutgoingT prog' prog' ~ progIn, ProgramToMVarsOutgoing prog prog progOut, ProgramToMVarsOutgoing prog' prog' progIn, SWellFormedConfig init (D0 E) prog, SWellFormedConfig init (D0 E) prog', TyListIndex progOut init (MVar (ProgramCell (Cell fromO))), TyListIndex progIn init (MVar (ProgramCell (Cell fromI))), TyListIndex prog init currentUX, Expand prog currentUX current, TyListIndex prog' init currentUX', Expand prog' currentUX' current', MapLookup (TyMap sessionsToIdxThem idxsToPairStructsThem) init (MVar (Map (RawPid, RawPid) (MVar (PairStruct init prog prog' (Cons (Jump init) Nil, Cons (Jump init) Nil, Cons (Jump init) Nil))))), TyListMember invertedSessionsMe init True, MapSize (TyMap keyToIdxMe idxToValueMe) idxOfThem, MapInsert (TyMap keyToIdxMe idxToValueMe) idxOfThem (SessionState prog' prog (current', fromI, fromO)) (TyMap keyToIdxMe' idxToValueMe')) => CreateSession True init prog prog' sessionsToIdxMe sessionsToIdxThem idxsToPairStructsMe idxsToPairStructsThem keyToIdxMe idxToValueMe keyToIdxMe' idxToValueMe' idxOfThem invertedSessionsMe invertedSessionsThem
instance (ProgramToMVarsOutgoingT prog prog ~ progOut, ProgramToMVarsOutgoingT prog' prog' ~ progIn, SWellFormedConfig init (D0 E) prog, SWellFormedConfig init (D0 E) prog', TyListIndex progOut init (MVar (ProgramCell (Cell fromO))), TyListIndex progIn init (MVar (ProgramCell (Cell fromI))), TyListIndex prog init current', Expand prog current' current, MapLookup (TyMap sessionsToIdxMe idxsToPairStructsMe) init (MVar (Map (RawPid, RawPid) (MVar (PairStruct init prog prog' (Cons (Jump init) Nil, Cons (Jump init) Nil, Cons (Jump init) Nil))))), TyListMember invertedSessionsThem init True, MapSize (TyMap keyToIdxMe idxToValueMe) idxOfThem, MapInsert (TyMap keyToIdxMe idxToValueMe) idxOfThem (SessionState prog prog' (current, fromO, fromI)) (TyMap keyToIdxMe' idxToValueMe')) => CreateSession False init prog prog' sessionsToIdxMe sessionsToIdxThem idxsToPairStructsMe idxsToPairStructsThem keyToIdxMe idxToValueMe keyToIdxMe' idxToValueMe' idxOfThem invertedSessionsMe invertedSessionsThem
instance (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))
instance (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))
instance (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))
instance (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))
instance (Expand prog nxt nxt', ExpandPid prog (RecvPid invert idxs) expandedRecvPid) => Expand prog (Cons (RecvPid invert idxs) nxt) (Cons expandedRecvPid nxt')
instance (Expand prog nxt nxt', ExpandPid prog (SendPid invert idxs) expandedSendPid) => Expand prog (Cons (SendPid invert idxs) nxt) (Cons expandedSendPid nxt')
instance (BuildInvertedSessionsSet nxt set, TyList set) => BuildInvertedSessionsSet (Cons (init, True) nxt) (Cons init set)
instance (BuildInvertedSessionsSet nxt set) => BuildInvertedSessionsSet (Cons (init, False) nxt) set
instance BuildInvertedSessionsSet Nil Nil
instance (BuildPidTyMap' prog nxt (TyMap keyToIdx idxToValue) (TyMap keyToIdx' idxToValue'), TyList nxt) => BuildPidTyMap' prog (Cons (init, True) nxt) (TyMap keyToIdx idxToValue) (TyMap keyToIdx' idxToValue')
instance (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'')
instance BuildPidTyMap' prog Nil acc acc
instance (BuildPidTyMap' prog stlst (TyMap Nil Nil) tymap) => BuildPidTyMap prog stlst tymap


-- | A single thread should be able to have multiple concurrent
--   conversations with other threads. So this module places
--   <a>InterleavedChain</a> as an instance of <a>SMonad</a>, and equipts
--   it with the capability to manage and modify a mapping of channels to
--   other threads. Note there is some danger in here. Deadlocks can start
--   to appear if you're silly or deliberately mean. However, this is
--   starting to get towards the Actor / Erlang model of message passing.
module Control.Concurrent.Session.Interleaving

-- | Perform the given actions on the given channel. Note that the value
--   emitted by the actions will be passed out.
withChannel :: (MapLookup (TyMap keyToIdx idxToValue) idx (SessionState prog prog' (current, fromO, fromI)), MapUpdate (TyMap keyToIdx idxToValue) idx (SessionState prog prog' (current', toO, toI)) (TyMap keyToIdx idxToValue'), MapDelete (TyMap keyToIdx idxToValue) idx (TyMap keyToIdx'' idxToValue''), MapDelete (TyMap keyToIdx idxToValue') idx (TyMap keyToIdx'' idxToValue'')) => idx -> SessionChain prog prog' (current, fromO, fromI) (current', toO, toI) res -> InterleavedChain (InternalPid pidProg pidProg' invertedSessions sessionsToIdx idxsToPairStructs) (TyMap keyToIdx idxToValue) (TyMap keyToIdx idxToValue') res

-- | Think of this as <i>spawn</i> or <i>fork</i> - it creates a child
--   thread which must be prepared to communicate with you. You get a
--   channel set up to the child which is emitted by this function. The
--   child is first told about the channel back to you and your Pid. The
--   child can go off and do what ever it wants, including creating
--   additional channels. The child starts off knowing with only one open
--   channel which is to the parent.
class Fork invert init sessionsList prog prog' sessionsToIdxThem idxsToPairStructsThem sessionsToIdxMe idxsToPairStructsMe fromO fromI progOut progIn keyToIdxMe idxToValueMe keyToIdxMe' idxToValueMe' keyToIdxChild' idxToValueChild' keyToIdxChild'' idxToValueChild'' idxOfChild current current' currentUX currentUX' invertedSessionsMe invertedSessionsThem
fork :: (Fork invert init sessionsList prog prog' sessionsToIdxThem idxsToPairStructsThem sessionsToIdxMe idxsToPairStructsMe fromO fromI progOut progIn keyToIdxMe idxToValueMe keyToIdxMe' idxToValueMe' keyToIdxChild' idxToValueChild' keyToIdxChild'' idxToValueChild'' idxOfChild current current' currentUX currentUX' invertedSessionsMe invertedSessionsThem) => init -> invert -> sessionsList -> ((D0 E) -> Pid prog prog' invertedSessionsMe sessionsToIdxMe idxsToPairStructsMe -> InterleavedChain (InternalPid prog prog' invertedSessionsThem sessionsToIdxThem idxsToPairStructsThem) (TyMap keyToIdxChild' idxToValueChild') (TyMap keyToIdxChild'' idxToValueChild'') ()) -> InterleavedChain (InternalPid prog prog' invertedSessionsMe sessionsToIdxMe idxsToPairStructsMe) (TyMap keyToIdxMe idxToValueMe) (TyMap keyToIdxMe' idxToValueMe') (idxOfChild, Pid prog prog' invertedSessionsThem sessionsToIdxThem idxsToPairStructsThem)

-- | Run the root. Use this to start up a family from a single root.
runInterleaved :: (BuildPidTyMap prog sessionsListSorted (TyMap sessionsToIdx idxsToPairStructs), TyListSortNums sessionsList sessionsListSortedRev, TyListReverse sessionsListSortedRev sessionsListSorted, BuildInvertedSessionsSet sessionsListSorted invertedSessions, Dual prog prog', (DualT prog) ~ prog') => sessionsList -> prog -> InterleavedChain (InternalPid prog prog' invertedSessions sessionsToIdx idxsToPairStructs) (TyMap Nil Nil) (TyMap keyToIdx idxToValue) res -> IO res

-- | Convenience combination of <a>withChannel</a> and <a>sjump</a>
sjumpCh :: ((ProgramToMVarsOutgoingT prog prog) ~ progOut, (ProgramToMVarsOutgoingT prog' prog') ~ progIn, SWellFormedConfig l (D0 E) prog, SWellFormedConfig l (D0 E) prog', TyListIndex progOut l (MVar (ProgramCell (Cell outgoing))), TyListIndex progIn l (MVar (ProgramCell (Cell incoming))), TyListIndex prog l current', Expand prog current' current, MapLookup (TyMap keyToIdx idxToValue) idx (SessionState prog prog' (Cons (Jump l) Nil, Cons (Jump l) Nil, Cons (Jump l) Nil)), MapUpdate (TyMap keyToIdx idxToValue) idx (SessionState prog prog' (current, outgoing, incoming)) (TyMap keyToIdx idxToValue'), MapDelete (TyMap keyToIdx idxToValue) idx (TyMap keyToIdx'' idxToValue''), MapDelete (TyMap keyToIdx idxToValue') idx (TyMap keyToIdx'' idxToValue'')) => idx -> InterleavedChain (InternalPid pidProg pidProg' invertedSessions sessionsToIdx idxsToPairStructs) (TyMap keyToIdx idxToValue) (TyMap keyToIdx idxToValue') ()

-- | Convenience combination of <a>withChannel</a> and <a>ssend</a>
ssendCh :: (MapLookup (TyMap keyToIdx idxToValue) idx (SessionState prog prog' (Cons (Send (sp, t)) nxt, Cons t nxt', incoming)), MapUpdate (TyMap keyToIdx idxToValue) idx (SessionState prog prog' (nxt, nxt', incoming)) (TyMap keyToIdx idxToValue'), MapDelete (TyMap keyToIdx idxToValue) idx (TyMap keyToIdx'' idxToValue''), MapDelete (TyMap keyToIdx idxToValue') idx (TyMap keyToIdx'' idxToValue''), CompatibleTypes sp t' t) => idx -> t' -> InterleavedChain (InternalPid pidProg pidProg' invertedSessions sessionsToIdx idxsToPairStructs) (TyMap keyToIdx idxToValue) (TyMap keyToIdx idxToValue') ()

-- | Convenience combination of <a>withChannel</a> and <a>srecv</a>
srecvCh :: (MapLookup (TyMap keyToIdx idxToValue) idx (SessionState prog prog' (Cons (Recv (sp, t)) nxt, outgoing, Cons t nxt')), MapUpdate (TyMap keyToIdx idxToValue) idx (SessionState prog prog' (nxt, outgoing, nxt')) (TyMap keyToIdx idxToValue'), MapDelete (TyMap keyToIdx idxToValue) idx (TyMap keyToIdx'' idxToValue''), MapDelete (TyMap keyToIdx idxToValue') idx (TyMap keyToIdx'' idxToValue'')) => idx -> InterleavedChain (InternalPid pidProg pidProg' invertedSessions sessionsToIdx idxsToPairStructs) (TyMap keyToIdx idxToValue) (TyMap keyToIdx idxToValue') t

-- | Convenience combination of <a>withChannel</a> and <a>soffer</a>
sofferCh :: (MapLookup (TyMap keyToIdx idxToValue) idx (SessionState prog prog' (Cons (Offer jumps) Nil, Cons (Choice jumps) Nil, Cons (Choice jumps) Nil)), MapUpdate (TyMap keyToIdx idxToValue) idx (SessionState prog prog' (current, outgoing, incoming)) (TyMap keyToIdx idxToValue'), MapDelete (TyMap keyToIdx idxToValue) idx (TyMap keyToIdx'' idxToValue''), MapDelete (TyMap keyToIdx idxToValue') idx (TyMap keyToIdx'' idxToValue'')) => idx -> OfferImpls jumps prog prog' (current, outgoing, incoming) finalResult -> InterleavedChain (InternalPid pidProg pidProg' sessionsToIdx invertedSessions idxsToPairStructs) (TyMap keyToIdx idxToValue) (TyMap keyToIdx idxToValue') finalResult

-- | Convenience combination of <a>withChannel</a> and <a>sselectCh</a>
sselectCh :: ((ProgramToMVarsOutgoingT prog prog) ~ progOut, (ProgramToMVarsOutgoingT prog' prog') ~ progIn, MapLookup (TyMap keyToIdx idxToValue) idx (SessionState prog prog' (Cons (Select jumps) Nil, Cons (Choice jumps) Nil, Cons (Choice jumps) Nil)), MapUpdate (TyMap keyToIdx idxToValue) idx (SessionState prog prog' (current, outgoing, incoming)) (TyMap keyToIdx idxToValue'), TyListLength jumps len, SmallerThanBool label len True, TypeNumberToInt label, TyListIndex jumps label (Cons (Jump jumpTarget) Nil), SWellFormedConfig jumpTarget (D0 E) prog, SWellFormedConfig jumpTarget (D0 E) prog', TyListIndex progOut jumpTarget (MVar (ProgramCell (Cell outgoing))), TyListIndex progIn jumpTarget (MVar (ProgramCell (Cell incoming))), TyListIndex prog jumpTarget currentUX, Expand prog currentUX current, MapDelete (TyMap keyToIdx idxToValue) idx (TyMap keyToIdx'' idxToValue''), MapDelete (TyMap keyToIdx idxToValue') idx (TyMap keyToIdx'' idxToValue'')) => idx -> label -> InterleavedChain (InternalPid pidProg pidProg' invertedSessions sessionsToIdx idxsToPairStructs) (TyMap keyToIdx idxToValue) (TyMap keyToIdx idxToValue') ()
scloseCh :: (MapDelete (TyMap keyToIdx idxToValue) ch (TyMap keyToIdx' idxToValue'), MapLookup (TyMap keyToIdx idxToValue) ch (SessionState prog prog' (Cons End Nil, outgoing, incoming))) => ch -> InterleavedChain (InternalPid pidProg pidProg' invertedSessions sessionsToIdx idxsToPairStructs) (TyMap keyToIdx idxToValue) (TyMap keyToIdx' idxToValue') ()
sendChannel :: (MapLookup (TyMap keyToIdx idxToValue) chToSend (SessionState prog prog' (current, outgoing, incoming)), MapLookup (TyMap keyToIdx idxToValue) chOnWhichToSend (SessionState prog'' prog''' (Cons (Send (SpecialSession, SessionState prog prog' (current, outgoing, incoming))) nxt, Cons (SessionState prog prog' (current, outgoing, incoming)) nxt', incoming')), MapUpdate (TyMap keyToIdx idxToValue) chOnWhichToSend (SessionState prog'' prog''' (nxt, nxt', incoming')) (TyMap keyToIdx idxToValue'), MapDelete (TyMap keyToIdx idxToValue') chToSend (TyMap keyToIdx' idxToValue'')) => chToSend -> chOnWhichToSend -> InterleavedChain (InternalPid pidProg pidProg' invertedSessions sessionsToIdx idxsToPairStructs) (TyMap keyToIdx idxToValue) (TyMap keyToIdx' idxToValue'') ()
recvChannel :: (MapLookup (TyMap keyToIdx idxToValue) idx (SessionState prog prog' (Cons (Recv (SpecialSession, SessionState prog'' prog''' (current', outgoing', incoming'))) nxt, outgoing, Cons (SessionState prog'' prog''' (current', outgoing', incoming')) nxt')), MapUpdate (TyMap keyToIdx idxToValue) idx (SessionState prog prog' (nxt, outgoing, nxt')) (TyMap keyToIdx idxToValue'), MapSize (TyMap keyToIdx idxToValue') idx', MapInsert (TyMap keyToIdx idxToValue') idx' (SessionState prog'' prog''' (current', outgoing', incoming')) (TyMap keyToIdx' idxToValue'')) => idx -> InterleavedChain (InternalPid pidProg pidProg' invertedSessions sessionsToIdx idxsToPairStructs) (TyMap keyToIdx idxToValue) (TyMap keyToIdx' idxToValue'') idx'
instance (ProgramToMVarsOutgoingT prog prog ~ progOut, ProgramToMVarsOutgoingT prog' prog' ~ progIn, ProgramToMVarsOutgoing prog prog progOut, ProgramToMVarsOutgoing prog' prog' progIn, SWellFormedConfig init (D0 E) prog, SWellFormedConfig init (D0 E) prog', TyListIndex progOut init (MVar (ProgramCell (Cell fromO))), TyListIndex progIn init (MVar (ProgramCell (Cell fromI))), TyListIndex prog init currentUX, TyListIndex prog' init currentUX', Expand prog currentUX current, Expand prog' currentUX' current', BuildPidTyMap prog sessionsListSorted (TyMap sessionsToIdxThem idxsToPairStructsThem), BuildInvertedSessionsSet sessionsListSorted invertedSessionsThem, TyListSortNums sessionsList sessionsListSortedRev, TyListReverse sessionsListSortedRev sessionsListSorted, MapSize (TyMap keyToIdxMe idxToValueMe) idxOfChild, MapInsert (TyMap keyToIdxMe idxToValueMe) idxOfChild (SessionState prog' prog (current', fromI, fromO)) (TyMap keyToIdxMe' idxToValueMe'), MapInsert (TyMap Nil Nil) (D0 E) (SessionState prog prog' (current, fromO, fromI)) (TyMap keyToIdxChild' idxToValueChild')) => Fork True init sessionsList prog prog' sessionsToIdxThem idxsToPairStructsThem sessionsToIdxMe idxsToPairStructsMe fromO fromI progOut progIn keyToIdxMe idxToValueMe keyToIdxMe' idxToValueMe' keyToIdxChild' idxToValueChild' keyToIdxChild'' idxToValueChild'' idxOfChild current current' currentUX currentUX' invertedSessionsMe invertedSessionsThem
instance (ProgramToMVarsOutgoingT prog prog ~ progOut, ProgramToMVarsOutgoingT prog' prog' ~ progIn, ProgramToMVarsOutgoing prog prog progOut, ProgramToMVarsOutgoing prog' prog' progIn, SWellFormedConfig init (D0 E) prog, SWellFormedConfig init (D0 E) prog', TyListIndex progOut init (MVar (ProgramCell (Cell fromO))), TyListIndex progIn init (MVar (ProgramCell (Cell fromI))), TyListIndex prog init currentUX, TyListIndex prog' init currentUX', Expand prog currentUX current, Expand prog' currentUX' current', BuildPidTyMap prog sessionsListSorted (TyMap sessionsToIdxThem idxsToPairStructsThem), BuildInvertedSessionsSet sessionsListSorted invertedSessionsThem, TyListSortNums sessionsList sessionsListSortedRev, TyListReverse sessionsListSortedRev sessionsListSorted, MapSize (TyMap keyToIdxMe idxToValueMe) idxOfChild, MapInsert (TyMap keyToIdxMe idxToValueMe) idxOfChild (SessionState prog prog' (current, fromO, fromI)) (TyMap keyToIdxMe' idxToValueMe'), MapInsert (TyMap Nil Nil) (D0 E) (SessionState prog' prog (current', fromI, fromO)) (TyMap keyToIdxChild' idxToValueChild')) => Fork False init sessionsList prog prog' sessionsToIdxThem idxsToPairStructsThem sessionsToIdxMe idxsToPairStructsMe fromO fromI progOut progIn keyToIdxMe idxToValueMe keyToIdxMe' idxToValueMe' keyToIdxChild' idxToValueChild' keyToIdxChild'' idxToValueChild'' idxOfChild current current' currentUX currentUX' invertedSessionsMe invertedSessionsThem

module Control.Concurrent.Session.Network.Socket
runOverNetwork :: (ProgramToMVarsOutgoing prog prog progOut, ProgramToMVarsOutgoing prog' prog' progIn, (ProgramToMVarsOutgoingT prog prog) ~ progOut, (ProgramToMVarsOutgoingT prog' prog') ~ progIn, SWellFormedConfig init (D0 E) prog, SWellFormedConfig init (D0 E) prog', TyListIndex progOut init (MVar (ProgramCell (Cell fromO))), TyListIndex progIn init (MVar (ProgramCell (Cell fromI))), (DualT prog) ~ prog', Dual prog prog', TyListIndex prog init currentUX, Expand prog currentUX current, TyListIndex prog' init currentUX', Expand prog' currentUX' current', BuildNetworkRunner prog' prog (toCur', toI, toO) () prog' (D0 E), NetworkRuntime prog' prog (current', fromI, fromO) (toCur', toI, toO) ()) => prog -> init -> SessionChain prog prog' (current, fromO, fromI) (toCur, toO, toI) res' -> Maybe HostName -> PortID -> IO res'
class CreateSessionOverNetwork invert init prog prog' invertedSessionsMe sessionsToIdxMe idxsToPairStructsMe keyToIdxMe idxToValueMe keyToIdxMe' idxToValueMe' idxOfThem
createSessionOverNetwork :: (CreateSessionOverNetwork invert init prog prog' invertedSessionsMe sessionsToIdxMe idxsToPairStructsMe keyToIdxMe idxToValueMe keyToIdxMe' idxToValueMe' idxOfThem) => init -> invert -> Handle -> InterleavedChain (InternalPid prog prog' invertedSessionsMe sessionsToIdxMe idxsToPairStructsMe) (TyMap keyToIdxMe idxToValueMe) (TyMap keyToIdxMe' idxToValueMe') idxOfThem
instance (ProgramToMVarsOutgoingT prog prog ~ progOut, ProgramToMVarsOutgoingT prog' prog' ~ progIn, DualT prog ~ prog', ProgramToMVarsOutgoing prog prog progOut, ProgramToMVarsOutgoing prog' prog' progIn, SWellFormedConfig init (D0 E) prog, SWellFormedConfig init (D0 E) prog', TyListIndex progOut init (MVar (ProgramCell (Cell fromO))), TyListIndex progIn init (MVar (ProgramCell (Cell fromI))), TyListIndex prog init currentUX, Expand prog currentUX current, Dual prog prog', TyListIndex prog' init currentUX', Expand prog' currentUX' current', MapSize (TyMap keyToIdxMe idxToValueMe) idxOfThem, MapInsert (TyMap keyToIdxMe idxToValueMe) idxOfThem (SessionState prog' prog (current', fromI, fromO)) (TyMap keyToIdxMe' idxToValueMe'), BuildNetworkRunner prog prog' (toCur, toO, toI) () prog init, NetworkRuntime prog prog' (current, fromO, fromI) (toCur, toO, toI) (), TyListMember invertedSessionsMe init True) => CreateSessionOverNetwork True init prog prog' invertedSessionsMe sessionsToIdxMe idxsToPairStructsMe keyToIdxMe idxToValueMe keyToIdxMe' idxToValueMe' idxOfThem
instance (ProgramToMVarsOutgoingT prog prog ~ progOut, ProgramToMVarsOutgoingT prog' prog' ~ progIn, DualT prog ~ prog', ProgramToMVarsOutgoing prog prog progOut, ProgramToMVarsOutgoing prog' prog' progIn, SWellFormedConfig init (D0 E) prog, SWellFormedConfig init (D0 E) prog', TyListIndex progOut init (MVar (ProgramCell (Cell fromO))), TyListIndex progIn init (MVar (ProgramCell (Cell fromI))), TyListIndex prog init currentUX, Expand prog currentUX current, Dual prog prog', TyListIndex prog' init currentUX', Expand prog' currentUX' current', MapSize (TyMap keyToIdxMe idxToValueMe) idxOfThem, MapInsert (TyMap keyToIdxMe idxToValueMe) idxOfThem (SessionState prog prog' (current, fromO, fromI)) (TyMap keyToIdxMe' idxToValueMe'), BuildNetworkRunner prog' prog (toCur, toI, toO) () prog' init, NetworkRuntime prog' prog (current', fromI, fromO) (toCur, toI, toO) (), MapLookup (TyMap sessionsToIdxMe idxsToPairStructsMe) init (MVar (Map (RawPid, RawPid) (MVar (PairStruct init prog prog' (Cons (Jump init) Nil, Cons (Jump init) Nil, Cons (Jump init) Nil)))))) => CreateSessionOverNetwork False init prog prog' invertedSessionsMe sessionsToIdxMe idxsToPairStructsMe keyToIdxMe idxToValueMe keyToIdxMe' idxToValueMe' idxOfThem
instance (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]
instance JumpsToList prog prog' to result Nil [a]
instance (JumpsToList prog prog' to result jumps [SessionChain prog prog' (Cons (Select jumps) Nil, Cons (Choice jumps) Nil, Cons (Choice jumps) Nil) to result]) => NetworkRuntime prog prog' (Cons (Select jumps) Nil, Cons (Choice jumps) Nil, Cons (Choice jumps) Nil) to result
instance (JumpsToList prog prog' to result jumps [SessionChain prog prog' (Cons (Offer jumps) Nil, Cons (Choice jumps) Nil, Cons (Choice jumps) Nil) to result]) => NetworkRuntime prog prog' (Cons (Offer jumps) Nil, Cons (Choice jumps) Nil, Cons (Choice jumps) Nil) to result
instance (TypeNumberToInt l) => NetworkRuntime prog prog' (Cons (Jump l) Nil, Cons (Jump l) Nil, Cons (Jump l) Nil) to result
instance NetworkRuntime prog prog' (Cons End Nil, Cons End Nil, Cons End Nil) (current, outgoing, incoming) ()
instance (NetworkRuntime prog prog' (nxtC, outgoing, nxtI) (nxtC', outgoing', nxtI') result, Binary t) => NetworkRuntime prog prog' (Cons (Recv (sp, t)) nxtC, outgoing, Cons t nxtI) (nxtC', outgoing', nxtI') result
instance (NetworkRuntime prog prog' (nxtC, nxtO, incoming) (nxtC', nxtO', incoming') result, Binary t', CompatibleTypes sp t' t) => NetworkRuntime prog prog' (Cons (Send (sp, t)) nxtC, Cons t nxtO, incoming) (nxtC', nxtO', incoming') result
instance (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
instance BuildNetworkRunner prog prog' to result Nil idx


-- | This is just a convenience module that reexports everything you're
--   expected to need.
module Control.Concurrent.Session
data True
TT :: True
data False
FF :: False

-- | Use OfferImpls to construct the implementations of the branches of an
--   offer. Really, it's just a slightly fancy list.
data OfferImpls :: * -> * -> * -> * -> * -> *
OfferImplsNil :: OfferImpls Nil prog prog' finalState finalResult

-- | Use to construct OfferImpls. This function automatically adds the
--   necessary <a>sjump</a> to the start of each branch implementation.
(~||~) :: ((ProgramToMVarsOutgoingT prog prog) ~ progOut, (ProgramToMVarsOutgoingT prog' prog') ~ progIn, ProgramToMVarsOutgoing prog prog progOut, ProgramToMVarsOutgoing prog' prog' progIn, SWellFormedConfig l (D0 E) prog, SWellFormedConfig l (D0 E) prog', TyListIndex progOut l (MVar (ProgramCell (Cell outgoing))), TyListIndex progIn l (MVar (ProgramCell (Cell incoming))), TyListIndex prog l currentUX, Expand prog currentUX current) => (SessionChain prog prog' (current, outgoing, incoming) finalState finalResult) -> (OfferImpls jumps prog prog' finalState finalResult) -> (OfferImpls (Cons (Cons (Jump l) Nil) jumps) prog prog' finalState finalResult)

-- | Perform a jump. Now you may think that you should indicate where you
--   want to jump to. But of course, that's actually specified by the
--   session type so you don't have to specify it at all in the
--   implementation.
sjump :: ((ProgramToMVarsOutgoingT prog prog) ~ progOut, (ProgramToMVarsOutgoingT prog' prog') ~ progIn, SWellFormedConfig l (D0 E) prog, SWellFormedConfig l (D0 E) prog', TyListIndex progOut l (MVar (ProgramCell (Cell outgoing))), TyListIndex progIn l (MVar (ProgramCell (Cell incoming))), TyListIndex prog l currentUX, Expand prog currentUX current) => (SessionChain prog prog') (Cons (Jump l) Nil, Cons (Jump l) Nil, Cons (Jump l) Nil) (current, outgoing, incoming) ()

-- | Offer a number of branches. This is basically an external choice - the
--   other party uses <a>sselect</a> to decide which branch to take. Use
--   OfferImpls in order to construct the list of implementations of
--   branches. Note that every implementation must result in the same final
--   state and emit the same value.
soffer :: OfferImpls jumps prog prog' (current, outgoing, incoming) finalResult -> (SessionChain prog prog') (Cons (Offer jumps) Nil, Cons (Choice jumps) Nil, Cons (Choice jumps) Nil) (current, outgoing, incoming) finalResult

-- | Select which branch we're taking at a branch point. Use a type number
--   (<a>Control.Concurrent.Session.Number</a>) to indicate the branch to
--   take.
sselect :: ((ProgramToMVarsOutgoingT prog prog) ~ progOut, (ProgramToMVarsOutgoingT prog' prog') ~ progIn, TyListLength jumps len, SmallerThanBool label len True, TypeNumberToInt label, TyListIndex jumps label (Cons (Jump jumpTarget) Nil), SWellFormedConfig jumpTarget (D0 E) prog, SWellFormedConfig jumpTarget (D0 E) prog', TyListIndex progOut jumpTarget (MVar (ProgramCell (Cell outgoing))), TyListIndex progIn jumpTarget (MVar (ProgramCell (Cell incoming))), TyListIndex prog jumpTarget currentUX, Expand prog currentUX current) => label -> (SessionChain prog prog') (Cons (Select jumps) Nil, Cons (Choice jumps) Nil, Cons (Choice jumps) Nil) (current, outgoing, incoming) ()

-- | Send a value to the other party. Of course, the value must be of the
--   correct type indicated in the session type.
ssend :: (CompatibleTypes sp t' t) => t' -> SessionChain prog prog' (Cons (Send (sp, t)) nxtCur, Cons t nxtOut, incoming) (nxtCur, nxtOut, incoming) ()

-- | Recieve a value from the other party. This will block as necessary.
--   The type of the value received is specified by the session type. No
--   magic coercion needed.
srecv :: (SessionChain prog prog') (Cons (Recv (sp, t)) nxt, outgoing, Cons t nxt') (nxt, outgoing, nxt') t

-- | Run! Provide a program and a start point within that program (which is
--   automatically <a>sjump</a>ed to), the two implementations which must
--   be duals of each other, run them, have them communicate, wait until
--   they both finish and die and then return the results from both of
--   them.
run :: (ProgramToMVarsOutgoing prog prog progOut, ProgramToMVarsOutgoing prog' prog' progIn, (ProgramToMVarsOutgoingT prog prog) ~ progOut, (ProgramToMVarsOutgoingT prog' prog') ~ progIn, SWellFormedConfig init (D0 E) prog, SWellFormedConfig init (D0 E) prog', TyListIndex progOut init (MVar (ProgramCell (Cell fromO))), TyListIndex progIn init (MVar (ProgramCell (Cell fromI))), (DualT prog) ~ prog', Dual prog prog', TyListIndex prog init currentUX, Expand prog currentUX current, TyListIndex prog' init currentUX', Expand prog' currentUX' current') => prog -> init -> SessionChain prog prog' (current, fromO, fromI) (toCur, toO, toI) res -> SessionChain prog' prog (current', fromI, fromO) (toCur', toI, toO) res' -> IO (res, res')
data End
data Send t
Send :: t -> Send t
data Recv t
Recv :: t -> Recv t
sendPid :: (TyList f, TyList fs, TyListSortNums lst lst') => lst -> SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs)) (TypeState nxtLabel declareable useable (Cons (label, Cons (SendPid False lst') f) fs)) ()
recvPid :: (TyList f, TyList fs, TyListSortNums lst lst') => lst -> SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs)) (TypeState nxtLabel declareable useable (Cons (label, Cons (RecvPid False lst') f) fs)) ()
sendSession :: (TyList f, TyList fs, TyList fs', TyListReverse frag fragRev, TyListTake (D1 E) fragRev (Cons (label, fragHead) Nil), TyListDrop (D1 E) fragRev fragTailRev, TyListReverse fragTailRev fragTail, TyListAppend fragTail fs fs') => SessionType (TypeState nxtLabel declareable useable (Cons (label, Nil) Nil)) (TypeState nxtLabel' declareable' useable' frag) res -> SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs)) (TypeState nxtLabel' declareable' useable' (Cons (label, Cons (SendSession False fragHead) f) fs')) res
recvSession :: (TyList f, TyList fs, TyList fs', TyListReverse frag fragRev, TyListTake (D1 E) fragRev (Cons (label, fragHead) Nil), TyListDrop (D1 E) fragRev fragTailRev, TyListReverse fragTailRev fragTail, TyListAppend fragTail fs fs') => SessionType (TypeState nxtLabel declareable useable (Cons (label, Nil) Nil)) (TypeState nxtLabel' declareable' useable' frag) res -> SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs)) (TypeState nxtLabel' declareable' useable' (Cons (label, Cons (RecvSession False fragHead) f) fs')) res
data Jump l
data Select :: * -> *
data Offer :: * -> *
jump :: (TyListReverse (Cons (Jump jt) f) f', TyList f, TyList fs, TyListMember useable jt True) => jt -> SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs)) (TypeState nxtLabel declareable useable (Cons (label, f') fs)) ()
end :: (TyListReverse (Cons End f) f', TyList f, TyList fs) => SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs)) (TypeState nxtLabel declareable useable (Cons (label, f') fs)) ()
select :: (TyListReverse (Cons (Select listOfJumps) f) f', TyList f, TyList fs, BuildBranches (BranchesList listOfRes listOfJumps (TypeState nxtLabel declareable useable (Cons (label, f') fs)) to finalTo) (SessionType (TypeState nxtLabel declareable useable (Cons (label, f') fs)) finalTo (listOfRes, listOfJumps))) => (BranchesList listOfRes listOfJumps (TypeState nxtLabel declareable useable (Cons (label, f') fs)) to finalTo) -> (SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs)) finalTo listOfRes)
offer :: (TyListReverse (Cons (Offer listOfJumps) f) f', TyList f, TyList fs, BuildBranches (BranchesList listOfRes listOfJumps (TypeState nxtLabel declareable useable (Cons (label, f') fs)) to finalTo) (SessionType (TypeState nxtLabel declareable useable (Cons (label, f') fs)) finalTo (listOfRes, listOfJumps))) => (BranchesList listOfRes listOfJumps (TypeState nxtLabel declareable useable (Cons (label, f') fs)) to finalTo) -> (SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs)) finalTo listOfRes)
(~>) :: (TyList nxt, SNonTerminal a, SValidSessionType nxt) => a -> nxt -> (Cons a nxt)
(~|~) :: (Succ label nxtLabel, TyListConsSet label declareable declareable', TyListElem declareable' label idx, TyListDelete declareable' idx declareable'', TyListConsSet label useable useable', TyList st, TyListMember declareable' label True, TyList labs, TyList resLst) => (SessionType (TypeState nxtLabel declareable'' useable' (Cons (label, Nil) st)) (TypeState nxtLabel' declareable''' useable'' st') res) -> (BranchesList resLst labs (TypeState nxtLabel' declareable''' useable'' st') to finalTo) -> (BranchesList (Cons res resLst) (Cons (Cons (Jump label) Nil) labs) (TypeState label declareable useable st) (TypeState nxtLabel' declareable''' useable'' st', to) finalTo)
class SWellFormedConfig idxA idxB ss
testWellformed :: (SWellFormedConfig idxA idxB ss) => ss -> idxA -> idxB -> Bool

-- | The representation of a computation that performs work using session
--   types. Again, really quite similar to a more-parameterized State
--   monad.
data SessionChain prog prog' from to res
(.=) :: (TyListMember declareable label True, TyListElem declareable label idx, TyListDelete declareable idx declareable', TyList st) => label -> (SessionType (TypeState nxtLabel declareable' useable (Cons (label, Nil) st)) (TypeState nxtLabel' declareable'' useable' st') a) -> SessionType (TypeState nxtLabel declareable useable st) (TypeState nxtLabel' declareable'' useable' st') a
dual :: True
notDual :: False
newLabel :: (Succ nxtLabel nxtLabel', TyListConsSet nxtLabel declareable declareable', TyListConsSet nxtLabel useable useable') => SessionType (TypeState nxtLabel declareable useable st) (TypeState nxtLabel' declareable' useable' st) nxtLabel
send :: (TyList f, TyList fs) => t -> SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs)) (TypeState nxtLabel declareable useable (Cons (label, Cons (Send (SpecialNormal, t)) f) fs)) ()
recv :: (TyList f, TyList fs) => t -> SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs)) (TypeState nxtLabel declareable useable (Cons (label, Cons (Recv (SpecialNormal, t)) f) fs)) ()
makeSessionType :: (TyListSortNums st st', TyListSnd st' st'') => SessionType (TypeState (D0 E) Nil Nil Nil) (TypeState nxtLabel Nil useable st) res -> (st'', res)
currentLabel :: SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs)) (TypeState nxtLabel declareable useable (Cons (label, f) fs)) label
data BranchesList :: * -> * -> * -> * -> * -> *
BLNil :: BranchesList Nil Nil z z z
data Cons :: * -> * -> *
cons :: (TyList n) => t -> n -> (Cons t n)
data Nil :: *
nil :: Nil
data E
E :: E
data D0 n
D0 :: n -> D0 n
data D1 n
D1 :: n -> D1 n
data D2 n
D2 :: n -> D2 n
data D3 n
D3 :: n -> D3 n
data D4 n
D4 :: n -> D4 n
data D5 n
D5 :: n -> D5 n
data D6 n
D6 :: n -> D6 n
data D7 n
D7 :: n -> D7 n
data D8 n
D8 :: n -> D8 n
data D9 n
D9 :: n -> D9 n
emptyMap :: TyMap Nil Nil

-- | A process ID. This is a tiny bit like ThreadId but rather heavily
--   annotated.
data Pid :: * -> * -> * -> * -> * -> *
data InterleavedChain internalPid from to res

-- | Provides the ability to make a new session / channel with the given
--   Pid. Supply the index to the Session Type, whether or not you're
--   locally inverting (dualing) the Session Type, and the Pid, and so long
--   as the Pid supports the dual of your local Session Type, this will
--   block until the Pid gets around to servicing you. Thus this is a
--   synchronous operation and both Pids must know of each other to create
--   a new session / channel between them.
class CreateSession invert init prog prog' sessionsToIdxMe sessionsToIdxThem idxsToPairStructsMe idxsToPairStructsThem keyToIdxMe idxToValueMe keyToIdxMe' idxToValueMe' idxOfThem invertedSessionsMe invertedSessionsThem
createSession :: (CreateSession invert init prog prog' sessionsToIdxMe sessionsToIdxThem idxsToPairStructsMe idxsToPairStructsThem keyToIdxMe idxToValueMe keyToIdxMe' idxToValueMe' idxOfThem invertedSessionsMe invertedSessionsThem) => init -> invert -> Pid prog prog' invertedSessionsThem sessionsToIdxThem idxsToPairStructsThem -> InterleavedChain (InternalPid prog prog' invertedSessionsMe sessionsToIdxMe idxsToPairStructsMe) (TyMap keyToIdxMe idxToValueMe) (TyMap keyToIdxMe' idxToValueMe') idxOfThem
myPid :: InterleavedChain (InternalPid prog prog' invertedSessions sessionsToIdx idxsToPairStructs) from from (Pid prog prog' invertedSessions sessionsToIdx idxsToPairStructs)

-- | Provides a way to compare two Pids. Of course, if the Pids have
--   different type params, then they are definitely different, but it's
--   still convenient to be able to do something like (==) on them.
class PidEq a b
(=~=) :: (PidEq a b) => a -> b -> Bool
data MultiReceive :: * -> * -> * -> * -> * -> * -> * -> * -> * -> * -> * -> *
MultiReceiveNil :: MultiReceive Nil prog prog' invertedSessions sessionsToIdx idxsToPairStructs keyToIdx idxToValue keyToIdx' idxToValue' res
(~|||~) :: (MapLookup (TyMap keyToIdx idxToValue) ch (SessionState progS progS' (Cons (Recv (sp, t)) nxt, fromO, Cons t nxt'))) => (ch, InterleavedChain (InternalPid prog prog' invertedSessions sessionsToIdx idxsToPairStructs) (TyMap keyToIdx idxToValue) (TyMap keyToIdx' idxToValue') res) -> MultiReceive chs prog prog' invertedSessions sessionsToIdx idxsToPairStructs keyToIdx idxToValue keyToIdx' idxToValue' res -> MultiReceive (Cons ch chs) prog prog' invertedSessions sessionsToIdx idxsToPairStructs keyToIdx idxToValue keyToIdx' idxToValue' res
multiReceive :: (TyListLength chs len, SmallerThanBool (D0 E) len True, SetIncomingNotify (TyMap keyToIdx idxToValue) chs, FindNonEmptyIncoming (TyMap keyToIdx idxToValue) chs, TypeNumberToInt len) => (MultiReceive chs prog prog' invertedSessions sessionsToIdx idxsToPairStructs keyToIdx idxToValue keyToIdx' idxToValue' res) -> InterleavedChain (InternalPid prog prog' invertedSessions sessionsToIdx idxsToPairStructs) (TyMap keyToIdx idxToValue) (TyMap keyToIdx' idxToValue') res