Control.Concurrent.Session.List

Description

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

Synopsis

data Nil

data Cons

class TyListLength list length | list -> length where

tyListLength :: list -> length

nil :: Nil

cons :: TyList n => t -> n -> (Cons t n)

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

tyHead :: (Cons t n) -> t

tyTail :: TyList n => (Cons t n) -> n

class TyList l

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

tyListIndex :: lst -> idx -> res

tyListUpdate :: lst -> idx -> res -> lst

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

tyListUpdateVar :: lst1 -> idx -> val -> lst2

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

tyListTake :: cnt -> lst -> res

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

tyListDrop :: cnt -> lst -> res

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

tyListAppend :: a -> b -> c

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

tyListReverse :: m -> n

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

tyListElem :: Monad m => lst -> val -> m idx

Documentation

data Nil

Instances

Show Nil

TyList Nil

SListOfSessionTypes Nil

SListOfJumps Nil

Dual Nil Nil

SNoJumpsBeyond Nil idx

ProgramToMVarsOutgoing Nil Nil

TyListAppend Nil b b

TyListDrop cnt Nil Nil

TyListReverse' Nil acc acc

TyListElem' Nil acc val idx

TyListLength Nil (D0 E)

TyListTake (D0 E) Nil Nil

TyListTake (D0 E) (Cons val nxt) Nil

data Cons

Instances

(TyListDrop cnt' nxt lst, Pred cnt cnt') => TyListDrop cnt (Cons val nxt) lst

TyListTake (D0 E) (Cons val nxt) Nil

TyListDrop (D0 E) (Cons val nxt) (Cons val nxt)

(TyListTake cnt' nxt nxt', Pred (D1 r) cnt') => TyListTake (D1 r) (Cons val nxt) (Cons val nxt')

(TyListTake cnt' nxt nxt', Pred (D2 r) cnt') => TyListTake (D2 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 (D4 r) cnt') => TyListTake (D4 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 (D6 r) cnt') => TyListTake (D6 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 (D8 r) cnt') => TyListTake (D8 r) (Cons val nxt) (Cons val nxt')

(TyListTake cnt' nxt nxt', Pred (D9 r) cnt') => TyListTake (D9 r) (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 val, SListOfSessionTypes nxt) => SListOfSessionTypes (Cons val nxt)

(SValidSessionType nxt, SNonTerminal val) => SValidSessionType (Cons val nxt)

STerminal a => SValidSessionType (Cons a Nil)

(SListOfJumps nxt, TyNum val) => SListOfJumps (Cons (Cons (Jump val) Nil) nxt)

(TyListLength n len, Succ len len') => TyListLength (Cons t n) len'

(SNoJumpsBeyond val idx, SNoJumpsBeyond nxt idx) => SNoJumpsBeyond (Cons val nxt) idx

(OnlyOutgoing nxt nxt', TyList nxt, TyList nxt') => OnlyOutgoing (Cons (Recv t) nxt) nxt'

(TyListIndex nxt idx' res, Pred idx idx', SmallerThan idx' len, TyListLength nxt len) => TyListIndex (Cons val nxt) idx res

(TyListReverse' nxt (Cons v acc) n, TyList acc) => TyListReverse' (Cons v nxt) acc n

(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

(TyList nxt, TyList nxt', Dual val val', Dual nxt nxt') => Dual (Cons val nxt) (Cons val' nxt')

(OnlyOutgoing nxt nxt', TyList nxt, TyList nxt') => OnlyOutgoing (Cons (Send t) nxt) (Cons t nxt')

OnlyOutgoing (Cons (Offer jl) Nil) (Cons (Choice jl) Nil)

OnlyOutgoing (Cons (Select jl) Nil) (Cons (Choice jl) Nil)

OnlyOutgoing (Cons (Jump l) Nil) (Cons (Jump l) Nil)

OnlyOutgoing (Cons End Nil) (Cons End Nil)

(ProgramToMVarsOutgoing nxt nxt', OnlyOutgoing val val', TyList nxt, TyList nxt') => ProgramToMVarsOutgoing (Cons val nxt) (Cons (MVar (ProgramCell (Cell val'))) nxt')

class TyListLength list length | list -> length where

Find the length of a list.

Methods

tyListLength :: list -> length

Instances

TyListLength Nil (D0 E)

(TyListLength n len, Succ len len') => TyListLength (Cons t n) len'

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 :: TyList n => (Cons t n) -> n

class TyList l

Instances

TyList Nil

TyList nxt => TyList (Cons val nxt)

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

Index or update a list. When updating, the type of the new value must be the same as the type of the old value.

Methods

tyListIndex :: lst -> idx -> res

tyListUpdate :: lst -> idx -> res -> lst

Instances

(TyListIndex nxt idx' res, Pred idx idx', SmallerThan idx' len, TyListLength nxt len) => TyListIndex (Cons val nxt) idx res

TyListIndex (Cons res nxt) (D0 E) res

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

Update a list but allow the type of the new value to be different from the type of the old value.

Methods

tyListUpdateVar :: lst1 -> idx -> val -> lst2

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

Take from the head of a list. Mirrors the Prelude function take.

Methods

tyListTake :: cnt -> lst -> res

Instances

TyListTake (D0 E) Nil Nil

TyListTake (D0 E) (Cons val nxt) Nil

(TyListTake cnt' nxt nxt', Pred (D1 r) cnt') => TyListTake (D1 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 (D3 r) cnt') => TyListTake (D3 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 (D5 r) cnt') => TyListTake (D5 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 (D7 r) cnt') => TyListTake (D7 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 (D9 r) cnt') => TyListTake (D9 r) (Cons val nxt) (Cons val nxt')

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

Drop from the head of a list. Mirrors the Prelude function drop.

Methods

tyListDrop :: cnt -> lst -> res

Instances

TyListDrop cnt Nil Nil

(TyListDrop cnt' nxt lst, Pred cnt cnt') => TyListDrop cnt (Cons val nxt) lst

TyListDrop (D0 E) (Cons val nxt) (Cons val nxt)

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

Append two lists together. Mirrors the Prelude function '(++)'.

Methods

tyListAppend :: a -> b -> c

Instances

TyListAppend Nil b b

TyListAppend nxt b nxt' => TyListAppend (Cons val nxt) b (Cons val nxt')

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

Reverse a list.

Methods

tyListReverse :: m -> n

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

Methods

tyListElem :: Monad m => lst -> val -> m idx

Produced by Haddock version 2.1.0