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

Source

Instances

Show Nil

TyList Nil

SListOfSessionTypes Nil

SListOfJumps Nil

SNoJumpsBeyond Nil idx

Dual Nil Nil

ProgramToMVarsOutgoing Nil Nil

TyListReverse' Nil acc acc

TyListDrop cnt Nil Nil

TyListAppend Nil b b

TyListElem' Nil acc val idx

TyListLength Nil (D0 E)

TyListTake (D0 E) Nil Nil

TyListTake (D0 E) (Cons val nxt) Nil

data Cons

Source

Instances

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

TyListTake (D0 E) (Cons val nxt) Nil

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

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

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

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

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

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

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

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

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

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

(TyListLength n l, Succ l l', Show n, Show t) => Show (Cons t n)

TyList nxt => TyList (Cons val nxt)

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

STerminal a => SValidSessionType (Cons a Nil)

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

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

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

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

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

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

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

(Succ acc acc', TyListElem' nxt acc' val idx) => TyListElem' (Cons val' nxt) acc val idx

TyListElem' (Cons val nxt) idx val idx

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

TyListIndex (Cons res nxt) (D0 E) res

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 nxt nxt', TyList nxt, TyList nxt') => OnlyOutgoing (Cons (Send t) nxt) (Cons t nxt')

OnlyOutgoing (Cons End Nil) (Cons End Nil)

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

(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

Source

Find the length of a list.

Methods

tyListLength :: list -> length

Source

Instances

TyListLength Nil (D0 E)

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

nil :: Nil

Source

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

Source

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

Source

tyHead :: Cons t n -> t

Source

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

Source

class TyList l

Source

Instances

TyList Nil

TyList nxt => TyList (Cons val nxt)

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

Source

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

Methods

tyListIndex :: lst -> idx -> res

Source

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

Source

Instances

(TyListIndex nxt idx' res, Pred idx idx', 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

Source

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

Methods

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

Source

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

Source

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

Methods

tyListTake :: cnt -> lst -> res

Source

Instances

TyListTake (D0 E) Nil Nil

TyListTake (D0 E) (Cons val nxt) Nil

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

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

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

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

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

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

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

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

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

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

Source

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

Methods

tyListDrop :: cnt -> lst -> res

Source

Instances

TyListDrop cnt Nil Nil

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

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

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

Source

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

Methods

tyListAppend :: a -> b -> c

Source

Instances

TyListAppend Nil b b

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

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

Source

Reverse a list.

Methods

tyListReverse :: m -> n

Source

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

Source

Methods

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

Source

Produced by Haddock version 2.3.0