Control.Concurrent.Session.List

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

Documentation

data Nil where

Constructors

Nil :: Nil

Instances

Show Nil

TyList Nil

SListOfSessionTypes Nil

SListOfJumps Nil

SNoJumpsBeyond Nil idx

Dual Nil Nil

ProgramToMVarsOutgoing Nil Nil

ListLength Nil (D0 E)

STerminal a => SValidSessionType (Cons a Nil)

(SListOfJumps nxt, TyNum val) => SListOfJumps (Cons (Cons (Jump val) Nil) 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)

data Cons where

Constructors

Cons :: t -> n -> Cons t n

Instances

SListOfJumps (Cons val nxt) => STerminal (Offer (Cons val nxt))

SListOfJumps (Cons val nxt) => STerminal (Select (Cons val nxt))

(ListLength 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)

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

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

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

(Elem nxt idx' res, Pred idx idx', SmallerThan idx' len, ListLength nxt len) => Elem (Cons val nxt) idx res

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

OnlyOutgoing (Cons End Nil) (Cons End Nil)

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

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

class ListLength list length | list -> length where

Find the length of a list.

Methods

listLength :: list -> length

Instances

ListLength Nil (D0 E)

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

nil :: Nil

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

class TyList l

Instances

TyList Nil

TyList nxt => TyList (Cons val nxt)

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

Index or update a list

Methods

tyListElem :: lst -> idx -> res

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

Instances

(Elem nxt idx' res, Pred idx idx', SmallerThan idx' len, ListLength nxt len) => Elem (Cons val nxt) idx res

Elem (Cons res nxt) (D0 E) res