Copyright	(c) Evgeny Poberezkin
License	BSD3
Maintainer	evgeny@poberezkin.com
Stability	experimental
Portability	non-portable
Safe Haskell	Safe
Language	Haskell2010

Control.Protocol.Internal

Description

This module provides type families to combine/extract the individual states of parties as defined by command constructors intofrom the combined systemprotocol state defined as type-level list.

Synopsis

type family P (partyCmd :: (party, s, s)) where ...
type family Prj (parties :: [pk]) (state :: [k]) (party :: pk) :: k where ...
type family Inj (parties :: [pk]) (state :: [k]) (p :: pk) (s' :: k) :: [k] where ...
type NoParty p = (Text "Party " :<>: ShowType p) :<>: Text " is not found."
type StateError = Text "Specified fewer protocol states than parties."

Documentation

type family P (partyCmd :: (party, s, s)) where ... Source #

Extracts party from command type parameter.

Equations

P '(p, _, _) = p

type family Prj (parties :: [pk]) (state :: [k]) (party :: pk) :: k where ... Source #

Projects the state of one party from the list of states.

Equations

Prj (p ': _) (s ': _) p = s
Prj (_ ': ps) (_ ': ss) p = Prj ps ss p
Prj '[] _ p = TypeError (NoParty p)
Prj _ '[] p = TypeError (NoParty p :$$: StateError)

type family Inj (parties :: [pk]) (state :: [k]) (p :: pk) (s' :: k) :: [k] where ... Source #

Injects the state of some party into the party's position in the list of states.

Equations

Inj (p ': _) (_ ': ss) p s' = s' ': ss
Inj (_ ': ps) (s ': ss) p s' = s ': Inj ps ss p s'
Inj '[] _ p _ = TypeError (NoParty p)
Inj _ '[] p _ = TypeError (NoParty p :$$: StateError)

type NoParty p = (Text "Party " :<>: ShowType p) :<>: Text " is not found." Source #

type StateError = Text "Specified fewer protocol states than parties." Source #