Safe Haskell	Safe-Inferred
Language	Haskell2010

TypedSession.State.Type

Synopsis

type family XMsg eta
type family XLabel eta
type family XBranch eta
type family XBranchSt eta
type family XGoto eta
type family XTerminal eta
type ForallX (f :: Type -> Constraint) eta = (f (XMsg eta), f (XLabel eta), f (XBranch eta), f (XBranchSt eta), f (XGoto eta), f (XTerminal eta))
data BranchSt eta r bst = BranchSt (XBranchSt eta) bst [[String]] (Protocol eta r bst)
data MsgOrLabel eta r
- = Msg (XMsg eta) String [[String]] r r
- | Label (XLabel eta) Int
data Protocol eta r bst
- = (MsgOrLabel eta r) :> (Protocol eta r bst)
- | Branch (XBranch eta) r String [BranchSt eta r bst]
- | Goto (XGoto eta) Int
- | Terminal (XTerminal eta)
type XTraverse (m :: Type -> Type) eta gama r bst = ((XMsg eta, (String, [[String]], r, r, Protocol eta r bst)) -> m (XMsg gama), (XLabel eta, (Int, Protocol eta r bst)) -> m (XLabel gama), (XBranch eta, (r, String, [BranchSt eta r bst])) -> m (XBranch gama, m (Protocol gama r bst) -> m (Protocol gama r bst)), (XBranchSt eta, (bst, [[String]], Protocol eta r bst)) -> m (XBranchSt gama), (XGoto eta, Int) -> m (XGoto gama), XTerminal eta -> m (XTerminal gama))
xtraverse :: Monad m => XTraverse m eta gama r bst -> Protocol eta r bst -> m (Protocol gama r bst)
type XFold (m :: Type -> Type) eta r bst = ((XMsg eta, (String, [[String]], r, r, Protocol eta r bst)) -> m (), (XLabel eta, Int) -> m (), (XBranch eta, (r, String, [BranchSt eta r bst])) -> m (m () -> m ()), (XBranchSt eta, (bst, [[String]], Protocol eta r bst)) -> m (), (XGoto eta, Int) -> m (), XTerminal eta -> m ())
xfold :: Monad m => XFold m eta r bst -> Protocol eta r bst -> m ()
data ProtocolError r bst
- = DefLabelMultTimes Int
- | LabelUndefined Int
- | BranchFirstMsgMustHaveTheSameSender r String r
- | UndecideStateCanNotSendMsg String
- | UndecideStateCanNotStartBranch [BranchSt (GenConst r) r bst]
- | TerminalNeedAllRoleDecide String
- | BranchAtLeastOneBranch
- | AStateOnlyBeUsedForTheSamePair
- | MsgDoNotExistBeforeNextTerm String
internalError :: String
data Tracer r bst
- = TracerProtocolCreat (Protocol Creat r bst)
- | TracerProtocolIdx (Protocol Idx r bst)
- | TracerReRank (IntMap Int)
- | TracerProtocolAddNum (Protocol AddNums r bst)
- | TracerProtocolGenConst (Protocol (GenConst r) r bst)
- | TracerConstraints (Seq Constraint)
- | TracerSubMap SubMap
- | TracerProtocolGenConstN (Protocol (GenConst r) r bst)
- | TracerVerifyResult (IntMap (r, r))
- | TracerCollectBranchDynVal (Set Int)
- | TracerProtocolMsgT (Protocol (MsgT r bst) r bst)
- | TracerProtocolMsgT1 (Protocol (MsgT1 r bst) r bst)
- | TracerBranchResultTI [(r, String, T bst)] (Map String [(bst, [[String]], T bst)])
traceWrapper :: String -> String -> String
data Creat
data Idx
data AddNums
data GenConst r
data T bst
- = TNum Int
- | BstList Int bst
- | TAny Int
- | TEnd
data MsgT r bst
data MsgT1 r bst

Documentation

type family XMsg eta Source #

Instances

Instances details

type XMsg AddNums Source #
Instance details Defined in TypedSession.State.Type type XMsg AddNums = ([Int], [Int], Int)
type XMsg Creat Source #
Instance details Defined in TypedSession.State.Type type XMsg Creat = ()
type XMsg Idx Source #
Instance details Defined in TypedSession.State.Type type XMsg Idx = (Int, Int, Int)
type XMsg (GenConst r) Source #
Instance details Defined in TypedSession.State.Type type XMsg (GenConst r) = (([Int], [Int]), (r, r), Int)
type XMsg (MsgT r bst) Source #
Instance details Defined in TypedSession.State.Type type XMsg (MsgT r bst) = ([T bst], (r, r), Int)
type XMsg (MsgT1 r bst) Source #
Instance details Defined in TypedSession.State.Type type XMsg (MsgT1 r bst) = ((T bst, T bst, T bst), (r, r), Int)

type family XLabel eta Source #

Instances

Instances details

type XLabel AddNums Source #
Instance details Defined in TypedSession.State.Type type XLabel AddNums = [Int]
type XLabel Creat Source #
Instance details Defined in TypedSession.State.Type type XLabel Creat = ()
type XLabel Idx Source #
Instance details Defined in TypedSession.State.Type type XLabel Idx = Int
type XLabel (GenConst r) Source #
Instance details Defined in TypedSession.State.Type type XLabel (GenConst r) = ([Int], Int)
type XLabel (MsgT r bst) Source #
Instance details Defined in TypedSession.State.Type type XLabel (MsgT r bst) = ([T bst], Int)
type XLabel (MsgT1 r bst) Source #
Instance details Defined in TypedSession.State.Type type XLabel (MsgT1 r bst) = ([T bst], Int)

type family XBranch eta Source #

Instances

Instances details

type XBranch AddNums Source #
Instance details Defined in TypedSession.State.Type type XBranch AddNums = [Int]
type XBranch Creat Source #
Instance details Defined in TypedSession.State.Type type XBranch Creat = ()
type XBranch Idx Source #
Instance details Defined in TypedSession.State.Type type XBranch Idx = Int
type XBranch (GenConst r) Source #
Instance details Defined in TypedSession.State.Type type XBranch (GenConst r) = [Int]
type XBranch (MsgT r bst) Source #
Instance details Defined in TypedSession.State.Type type XBranch (MsgT r bst) = [T bst]
type XBranch (MsgT1 r bst) Source #
Instance details Defined in TypedSession.State.Type type XBranch (MsgT1 r bst) = [T bst]

type family XBranchSt eta Source #

Instances

Instances details

type XBranchSt AddNums Source #
Instance details Defined in TypedSession.State.Type type XBranchSt AddNums = ()
type XBranchSt Creat Source #
Instance details Defined in TypedSession.State.Type type XBranchSt Creat = ()
type XBranchSt Idx Source #
Instance details Defined in TypedSession.State.Type type XBranchSt Idx = ()
type XBranchSt (GenConst r) Source #
Instance details Defined in TypedSession.State.Type type XBranchSt (GenConst r) = ()
type XBranchSt (MsgT r bst) Source #
Instance details Defined in TypedSession.State.Type type XBranchSt (MsgT r bst) = ()
type XBranchSt (MsgT1 r bst) Source #
Instance details Defined in TypedSession.State.Type type XBranchSt (MsgT1 r bst) = ()

type family XGoto eta Source #

Instances

Instances details

type XGoto AddNums Source #
Instance details Defined in TypedSession.State.Type type XGoto AddNums = [Int]
type XGoto Creat Source #
Instance details Defined in TypedSession.State.Type type XGoto Creat = ()
type XGoto Idx Source #
Instance details Defined in TypedSession.State.Type type XGoto Idx = Int
type XGoto (GenConst r) Source #
Instance details Defined in TypedSession.State.Type type XGoto (GenConst r) = ([Int], Int)
type XGoto (MsgT r bst) Source #
Instance details Defined in TypedSession.State.Type type XGoto (MsgT r bst) = ([T bst], Int)
type XGoto (MsgT1 r bst) Source #
Instance details Defined in TypedSession.State.Type type XGoto (MsgT1 r bst) = ([T bst], Int)

type family XTerminal eta Source #

Instances

Instances details

type XTerminal AddNums Source #
Instance details Defined in TypedSession.State.Type type XTerminal AddNums = [Int]
type XTerminal Creat Source #
Instance details Defined in TypedSession.State.Type type XTerminal Creat = ()
type XTerminal Idx Source #
Instance details Defined in TypedSession.State.Type type XTerminal Idx = Int
type XTerminal (GenConst r) Source #
Instance details Defined in TypedSession.State.Type type XTerminal (GenConst r) = [Int]
type XTerminal (MsgT r bst) Source #
Instance details Defined in TypedSession.State.Type type XTerminal (MsgT r bst) = [T bst]
type XTerminal (MsgT1 r bst) Source #
Instance details Defined in TypedSession.State.Type type XTerminal (MsgT1 r bst) = [T bst]

type ForallX (f :: Type -> Constraint) eta = (f (XMsg eta), f (XLabel eta), f (XBranch eta), f (XBranchSt eta), f (XGoto eta), f (XTerminal eta)) Source #

ForallX

data BranchSt eta r bst Source #

BranchSt

Constructors

BranchSt (XBranchSt eta) bst [[String]] (Protocol eta r bst)

Instances

Instances details

Functor (BranchSt eta r) Source #
Instance details Defined in TypedSession.State.Type Methods fmap :: (a -> b) -> BranchSt eta r a -> BranchSt eta r b # (<$) :: a -> BranchSt eta r b -> BranchSt eta r a #
(Pretty (Protocol eta r bst), Show (XBranchSt eta), Show bst) => Show (BranchSt eta r bst) Source #
Instance details Defined in TypedSession.State.Type Methods showsPrec :: Int -> BranchSt eta r bst -> ShowS # show :: BranchSt eta r bst -> String # showList :: [BranchSt eta r bst] -> ShowS #
(Pretty (Protocol eta r bst), Show (XBranchSt eta), Show bst) => Pretty (BranchSt eta r bst) Source #
Instance details Defined in TypedSession.State.Type Methods pretty :: BranchSt eta r bst -> Doc ann # prettyList :: [BranchSt eta r bst] -> Doc ann #

data MsgOrLabel eta r Source #

MsgOrLabel

Constructors

Msg (XMsg eta) String [[String]] r r
Label (XLabel eta) Int

Instances

Instances details

Functor (MsgOrLabel eta) Source #
Instance details Defined in TypedSession.State.Type Methods fmap :: (a -> b) -> MsgOrLabel eta a -> MsgOrLabel eta b # (<$) :: a -> MsgOrLabel eta b -> MsgOrLabel eta a #
(Show (XMsg eta), Show (XLabel eta), Show r) => Show (MsgOrLabel eta r) Source #
Instance details Defined in TypedSession.State.Type Methods showsPrec :: Int -> MsgOrLabel eta r -> ShowS # show :: MsgOrLabel eta r -> String # showList :: [MsgOrLabel eta r] -> ShowS #
(Show (XMsg eta), Show (XLabel eta), Show r) => Pretty (MsgOrLabel eta r) Source #
Instance details Defined in TypedSession.State.Type Methods pretty :: MsgOrLabel eta r -> Doc ann # prettyList :: [MsgOrLabel eta r] -> Doc ann #

data Protocol eta r bst Source #

Protocol

Constructors

(MsgOrLabel eta r) :> (Protocol eta r bst) infixr 5
Branch (XBranch eta) r String [BranchSt eta r bst]
Goto (XGoto eta) Int
Terminal (XTerminal eta)

Instances

Instances details

Functor (Protocol eta r) Source #
Instance details Defined in TypedSession.State.Type Methods fmap :: (a -> b) -> Protocol eta r a -> Protocol eta r b # (<$) :: a -> Protocol eta r b -> Protocol eta r a #
(ForallX Show eta, Show r, Show bst) => Show (Protocol eta r bst) Source #
Instance details Defined in TypedSession.State.Type Methods showsPrec :: Int -> Protocol eta r bst -> ShowS # show :: Protocol eta r bst -> String # showList :: [Protocol eta r bst] -> ShowS #
(ForallX Show eta, Show r, Show bst) => Pretty (Protocol eta r bst) Source #
Instance details Defined in TypedSession.State.Type Methods pretty :: Protocol eta r bst -> Doc ann # prettyList :: [Protocol eta r bst] -> Doc ann #

type XTraverse (m :: Type -> Type) eta gama r bst = ((XMsg eta, (String, [[String]], r, r, Protocol eta r bst)) -> m (XMsg gama), (XLabel eta, (Int, Protocol eta r bst)) -> m (XLabel gama), (XBranch eta, (r, String, [BranchSt eta r bst])) -> m (XBranch gama, m (Protocol gama r bst) -> m (Protocol gama r bst)), (XBranchSt eta, (bst, [[String]], Protocol eta r bst)) -> m (XBranchSt gama), (XGoto eta, Int) -> m (XGoto gama), XTerminal eta -> m (XTerminal gama)) Source #

XTraverse

xtraverse :: Monad m => XTraverse m eta gama r bst -> Protocol eta r bst -> m (Protocol gama r bst) Source #

xtraverse

type XFold (m :: Type -> Type) eta r bst = ((XMsg eta, (String, [[String]], r, r, Protocol eta r bst)) -> m (), (XLabel eta, Int) -> m (), (XBranch eta, (r, String, [BranchSt eta r bst])) -> m (m () -> m ()), (XBranchSt eta, (bst, [[String]], Protocol eta r bst)) -> m (), (XGoto eta, Int) -> m (), XTerminal eta -> m ()) Source #

XFold

xfold :: Monad m => XFold m eta r bst -> Protocol eta r bst -> m () Source #

xfold

data ProtocolError r bst Source #

ProtocolError

Constructors

DefLabelMultTimes Int
LabelUndefined Int
BranchFirstMsgMustHaveTheSameSender r String r
UndecideStateCanNotSendMsg String
UndecideStateCanNotStartBranch [BranchSt (GenConst r) r bst]
TerminalNeedAllRoleDecide String
BranchAtLeastOneBranch
AStateOnlyBeUsedForTheSamePair
MsgDoNotExistBeforeNextTerm String

Instances

Instances details

(Show r, Show bst) => Show (ProtocolError r bst) Source #
Instance details Defined in TypedSession.State.Type Methods showsPrec :: Int -> ProtocolError r bst -> ShowS # show :: ProtocolError r bst -> String # showList :: [ProtocolError r bst] -> ShowS #

internalError :: String Source #

data Tracer r bst Source #

Constructors

TracerProtocolCreat (Protocol Creat r bst)
TracerProtocolIdx (Protocol Idx r bst)
TracerReRank (IntMap Int)
TracerProtocolAddNum (Protocol AddNums r bst)
TracerProtocolGenConst (Protocol (GenConst r) r bst)
TracerConstraints (Seq Constraint)
TracerSubMap SubMap
TracerProtocolGenConstN (Protocol (GenConst r) r bst)
TracerVerifyResult (IntMap (r, r))
TracerCollectBranchDynVal (Set Int)
TracerProtocolMsgT (Protocol (MsgT r bst) r bst)
TracerProtocolMsgT1 (Protocol (MsgT1 r bst) r bst)
TracerBranchResultTI [(r, String, T bst)] (Map String [(bst, [[String]], T bst)])

Instances

Instances details

(Show r, Show bst) => Show (Tracer r bst) Source #
Instance details Defined in TypedSession.State.Type Methods showsPrec :: Int -> Tracer r bst -> ShowS # show :: Tracer r bst -> String # showList :: [Tracer r bst] -> ShowS #

traceWrapper :: String -> String -> String Source #

data Creat Source #

Instances

Instances details

type XBranch Creat Source #
Instance details Defined in TypedSession.State.Type type XBranch Creat = ()
type XBranchSt Creat Source #
Instance details Defined in TypedSession.State.Type type XBranchSt Creat = ()
type XGoto Creat Source #
Instance details Defined in TypedSession.State.Type type XGoto Creat = ()
type XLabel Creat Source #
Instance details Defined in TypedSession.State.Type type XLabel Creat = ()
type XMsg Creat Source #
Instance details Defined in TypedSession.State.Type type XMsg Creat = ()
type XTerminal Creat Source #
Instance details Defined in TypedSession.State.Type type XTerminal Creat = ()

data Idx Source #

Instances

Instances details

type XBranch Idx Source #
Instance details Defined in TypedSession.State.Type type XBranch Idx = Int
type XBranchSt Idx Source #
Instance details Defined in TypedSession.State.Type type XBranchSt Idx = ()
type XGoto Idx Source #
Instance details Defined in TypedSession.State.Type type XGoto Idx = Int
type XLabel Idx Source #
Instance details Defined in TypedSession.State.Type type XLabel Idx = Int
type XMsg Idx Source #
Instance details Defined in TypedSession.State.Type type XMsg Idx = (Int, Int, Int)
type XTerminal Idx Source #
Instance details Defined in TypedSession.State.Type type XTerminal Idx = Int

data AddNums Source #

Instances

Instances details

type XBranch AddNums Source #
Instance details Defined in TypedSession.State.Type type XBranch AddNums = [Int]
type XBranchSt AddNums Source #
Instance details Defined in TypedSession.State.Type type XBranchSt AddNums = ()
type XGoto AddNums Source #
Instance details Defined in TypedSession.State.Type type XGoto AddNums = [Int]
type XLabel AddNums Source #
Instance details Defined in TypedSession.State.Type type XLabel AddNums = [Int]
type XMsg AddNums Source #
Instance details Defined in TypedSession.State.Type type XMsg AddNums = ([Int], [Int], Int)
type XTerminal AddNums Source #
Instance details Defined in TypedSession.State.Type type XTerminal AddNums = [Int]

data GenConst r Source #

Instances

Instances details

type XBranch (GenConst r) Source #
Instance details Defined in TypedSession.State.Type type XBranch (GenConst r) = [Int]
type XBranchSt (GenConst r) Source #
Instance details Defined in TypedSession.State.Type type XBranchSt (GenConst r) = ()
type XGoto (GenConst r) Source #
Instance details Defined in TypedSession.State.Type type XGoto (GenConst r) = ([Int], Int)
type XLabel (GenConst r) Source #
Instance details Defined in TypedSession.State.Type type XLabel (GenConst r) = ([Int], Int)
type XMsg (GenConst r) Source #
Instance details Defined in TypedSession.State.Type type XMsg (GenConst r) = (([Int], [Int]), (r, r), Int)
type XTerminal (GenConst r) Source #
Instance details Defined in TypedSession.State.Type type XTerminal (GenConst r) = [Int]

data T bst Source #

Constructors

TNum Int
BstList Int bst
TAny Int
TEnd

Instances

Instances details

Show bst => Show (T bst) Source #
Instance details Defined in TypedSession.State.Type Methods showsPrec :: Int -> T bst -> ShowS # show :: T bst -> String # showList :: [T bst] -> ShowS #

data MsgT r bst Source #

Instances

Instances details

type XBranch (MsgT r bst) Source #
Instance details Defined in TypedSession.State.Type type XBranch (MsgT r bst) = [T bst]
type XBranchSt (MsgT r bst) Source #
Instance details Defined in TypedSession.State.Type type XBranchSt (MsgT r bst) = ()
type XGoto (MsgT r bst) Source #
Instance details Defined in TypedSession.State.Type type XGoto (MsgT r bst) = ([T bst], Int)
type XLabel (MsgT r bst) Source #
Instance details Defined in TypedSession.State.Type type XLabel (MsgT r bst) = ([T bst], Int)
type XMsg (MsgT r bst) Source #
Instance details Defined in TypedSession.State.Type type XMsg (MsgT r bst) = ([T bst], (r, r), Int)
type XTerminal (MsgT r bst) Source #
Instance details Defined in TypedSession.State.Type type XTerminal (MsgT r bst) = [T bst]

data MsgT1 r bst Source #

Instances

Instances details

type XBranch (MsgT1 r bst) Source #
Instance details Defined in TypedSession.State.Type type XBranch (MsgT1 r bst) = [T bst]
type XBranchSt (MsgT1 r bst) Source #
Instance details Defined in TypedSession.State.Type type XBranchSt (MsgT1 r bst) = ()
type XGoto (MsgT1 r bst) Source #
Instance details Defined in TypedSession.State.Type type XGoto (MsgT1 r bst) = ([T bst], Int)
type XLabel (MsgT1 r bst) Source #
Instance details Defined in TypedSession.State.Type type XLabel (MsgT1 r bst) = ([T bst], Int)
type XMsg (MsgT1 r bst) Source #
Instance details Defined in TypedSession.State.Type type XMsg (MsgT1 r bst) = ((T bst, T bst, T bst), (r, r), Int)
type XTerminal (MsgT1 r bst) Source #
Instance details Defined in TypedSession.State.Type type XTerminal (MsgT1 r bst) = [T bst]