{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeAbstractions #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module TypedSession.State.Type where

import Control.Monad
import Data.IntMap (IntMap)
import Data.Kind (Constraint, Type)
import qualified Data.List as L
import Data.Map (Map)
import Data.Sequence (Seq)
import Data.Set (Set)
import Prettyprinter
import Prettyprinter.Render.String (renderString)
import qualified TypedSession.State.Constraint as C

type family XMsg eta
type family XLabel eta
type family XBranch eta
type family XBranchSt eta
type family XGoto eta
type family XTerminal eta

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

-- | BranchSt
data BranchSt eta r bst = BranchSt (XBranchSt eta) bst [[String]] (Protocol eta r bst)
  deriving ((forall a b. (a -> b) -> BranchSt eta r a -> BranchSt eta r b)
-> (forall a b. a -> BranchSt eta r b -> BranchSt eta r a)
-> Functor (BranchSt eta r)
forall a b. a -> BranchSt eta r b -> BranchSt eta r a
forall a b. (a -> b) -> BranchSt eta r a -> BranchSt eta r b
forall eta r a b. a -> BranchSt eta r b -> BranchSt eta r a
forall eta r a b. (a -> b) -> BranchSt eta r a -> BranchSt eta r b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall eta r a b. (a -> b) -> BranchSt eta r a -> BranchSt eta r b
fmap :: forall a b. (a -> b) -> BranchSt eta r a -> BranchSt eta r b
$c<$ :: forall eta r a b. a -> BranchSt eta r b -> BranchSt eta r a
<$ :: forall a b. a -> BranchSt eta r b -> BranchSt eta r a
Functor)

-- | MsgOrLabel
data MsgOrLabel eta r
  = Msg (XMsg eta) String [[String]] r r
  | Label (XLabel eta) Int
  deriving ((forall a b. (a -> b) -> MsgOrLabel eta a -> MsgOrLabel eta b)
-> (forall a b. a -> MsgOrLabel eta b -> MsgOrLabel eta a)
-> Functor (MsgOrLabel eta)
forall a b. a -> MsgOrLabel eta b -> MsgOrLabel eta a
forall a b. (a -> b) -> MsgOrLabel eta a -> MsgOrLabel eta b
forall eta a b. a -> MsgOrLabel eta b -> MsgOrLabel eta a
forall eta a b. (a -> b) -> MsgOrLabel eta a -> MsgOrLabel eta b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall eta a b. (a -> b) -> MsgOrLabel eta a -> MsgOrLabel eta b
fmap :: forall a b. (a -> b) -> MsgOrLabel eta a -> MsgOrLabel eta b
$c<$ :: forall eta a b. a -> MsgOrLabel eta b -> MsgOrLabel eta a
<$ :: forall a b. a -> MsgOrLabel eta b -> MsgOrLabel eta a
Functor)

infixr 5 :>

-- | Protocol
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)
  deriving ((forall a b. (a -> b) -> Protocol eta r a -> Protocol eta r b)
-> (forall a b. a -> Protocol eta r b -> Protocol eta r a)
-> Functor (Protocol eta r)
forall a b. a -> Protocol eta r b -> Protocol eta r a
forall a b. (a -> b) -> Protocol eta r a -> Protocol eta r b
forall eta r a b. a -> Protocol eta r b -> Protocol eta r a
forall eta r a b. (a -> b) -> Protocol eta r a -> Protocol eta r b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall eta r a b. (a -> b) -> Protocol eta r a -> Protocol eta r b
fmap :: forall a b. (a -> b) -> Protocol eta r a -> Protocol eta r b
$c<$ :: forall eta r a b. a -> Protocol eta r b -> Protocol eta r a
<$ :: forall a b. a -> Protocol eta r b -> Protocol eta r a
Functor)

-- | XTraverse
type XTraverse m 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
xtraverse
  :: (Monad m)
  => XTraverse m eta gama r bst
  -> Protocol eta r bst
  -> m (Protocol gama r bst)
xtraverse :: forall (m :: * -> *) eta gama r bst.
Monad m =>
XTraverse m eta gama r bst
-> Protocol eta r bst -> m (Protocol gama r bst)
xtraverse xt :: XTraverse m eta gama r bst
xt@((XMsg eta, ([Char], [[[Char]]], r, r, Protocol eta r bst))
-> m (XMsg gama)
xmsg, (XLabel eta, (Int, Protocol eta r bst)) -> m (XLabel gama)
xlabel, (XBranch eta, (r, [Char], [BranchSt eta r bst]))
-> m (XBranch gama,
      m (Protocol gama r bst) -> m (Protocol gama r bst))
xbranch, (XBranchSt eta, (bst, [[[Char]]], Protocol eta r bst))
-> m (XBranchSt gama)
xbranchSt, (XGoto eta, Int) -> m (XGoto gama)
xgoto, XTerminal eta -> m (XTerminal gama)
xterminal) Protocol eta r bst
prot = case Protocol eta r bst
prot of
  MsgOrLabel eta r
msgOrLabel :> Protocol eta r bst
prots -> do
    res <- case MsgOrLabel eta r
msgOrLabel of
      Msg XMsg eta
xv [Char]
a [[[Char]]]
b r
c r
d -> do
        xv' <- (XMsg eta, ([Char], [[[Char]]], r, r, Protocol eta r bst))
-> m (XMsg gama)
xmsg (XMsg eta
xv, ([Char]
a, [[[Char]]]
b, r
c, r
d, Protocol eta r bst
prots))
        pure (Msg xv' a b c d)
      Label XLabel eta
xv Int
i -> do
        xv' <- (XLabel eta, (Int, Protocol eta r bst)) -> m (XLabel gama)
xlabel (XLabel eta
xv, (Int
i, Protocol eta r bst
prots))
        pure (Label xv' i)
    prots' <- xtraverse xt prots
    pure (res :> prots')
  Branch XBranch eta
xv r
r [Char]
st [BranchSt eta r bst]
ls -> do
    (xv', wrapper) <- (XBranch eta, (r, [Char], [BranchSt eta r bst]))
-> m (XBranch gama,
      m (Protocol gama r bst) -> m (Protocol gama r bst))
xbranch (XBranch eta
xv, (r
r, [Char]
st, [BranchSt eta r bst]
ls))
    ls' <- forM ls $ \(BranchSt XBranchSt eta
xbst bst
bst [[[Char]]]
args Protocol eta r bst
prot1) -> do
      xbst' <- (XBranchSt eta, (bst, [[[Char]]], Protocol eta r bst))
-> m (XBranchSt gama)
xbranchSt (XBranchSt eta
xbst, (bst
bst, [[[Char]]]
args, Protocol eta r bst
prot1))
      prot' <- wrapper $ xtraverse xt prot1
      pure (BranchSt xbst' bst args prot')
    pure (Branch xv' r st ls')
  Goto XGoto eta
xv Int
i -> do
    xv' <- (XGoto eta, Int) -> m (XGoto gama)
xgoto (XGoto eta
xv, Int
i)
    pure (Goto xv' i)
  Terminal XTerminal eta
xv -> do
    xv' <- XTerminal eta -> m (XTerminal gama)
xterminal XTerminal eta
xv
    pure (Terminal xv')

-- | XFold
type XFold m 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
xfold :: (Monad m) => XFold m eta r bst -> Protocol eta r bst -> m ()
xfold :: forall (m :: * -> *) eta r bst.
Monad m =>
XFold m eta r bst -> Protocol eta r bst -> m ()
xfold xt :: XFold m eta r bst
xt@((XMsg eta, ([Char], [[[Char]]], r, r, Protocol eta r bst)) -> m ()
xmsg, (XLabel eta, Int) -> m ()
xlabel, (XBranch eta, (r, [Char], [BranchSt eta r bst]))
-> m (m () -> m ())
xbranch, (XBranchSt eta, (bst, [[[Char]]], Protocol eta r bst)) -> m ()
xbranchst, (XGoto eta, Int) -> m ()
xgoto, XTerminal eta -> m ()
xterminal) Protocol eta r bst
prot = case Protocol eta r bst
prot of
  MsgOrLabel eta r
msgOrLabel :> Protocol eta r bst
prots -> do
    case MsgOrLabel eta r
msgOrLabel of
      Msg XMsg eta
xv [Char]
a [[[Char]]]
b r
c r
d -> (XMsg eta, ([Char], [[[Char]]], r, r, Protocol eta r bst)) -> m ()
xmsg (XMsg eta
xv, ([Char]
a, [[[Char]]]
b, r
c, r
d, Protocol eta r bst
prots))
      Label XLabel eta
xv Int
i -> (XLabel eta, Int) -> m ()
xlabel (XLabel eta
xv, Int
i)
    XFold m eta r bst -> Protocol eta r bst -> m ()
forall (m :: * -> *) eta r bst.
Monad m =>
XFold m eta r bst -> Protocol eta r bst -> m ()
xfold XFold m eta r bst
xt Protocol eta r bst
prots
  Branch XBranch eta
xv r
r [Char]
st [BranchSt eta r bst]
ls -> do
    wrapper <- (XBranch eta, (r, [Char], [BranchSt eta r bst]))
-> m (m () -> m ())
xbranch (XBranch eta
xv, (r
r, [Char]
st, [BranchSt eta r bst]
ls))
    forM_ ls $ \(BranchSt XBranchSt eta
xbst bst
bst [[[Char]]]
args Protocol eta r bst
prot1) -> do
      (XBranchSt eta, (bst, [[[Char]]], Protocol eta r bst)) -> m ()
xbranchst (XBranchSt eta
xbst, (bst
bst, [[[Char]]]
args, Protocol eta r bst
prot1))
      m () -> m ()
wrapper (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ XFold m eta r bst -> Protocol eta r bst -> m ()
forall (m :: * -> *) eta r bst.
Monad m =>
XFold m eta r bst -> Protocol eta r bst -> m ()
xfold XFold m eta r bst
xt Protocol eta r bst
prot1
  Goto XGoto eta
xv Int
i -> (XGoto eta, Int) -> m ()
xgoto (XGoto eta
xv, Int
i)
  Terminal XTerminal eta
xv -> XTerminal eta -> m ()
xterminal XTerminal eta
xv

-- | ProtocolError
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

instance (Show r, Show bst) => Show (ProtocolError r bst) where
  show :: ProtocolError r bst -> [Char]
show = \case
    DefLabelMultTimes Int
msgOrLabel -> [Char]
"Defining Label multiple times: " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> [Char]
forall a. Show a => a -> [Char]
show Int
msgOrLabel
    LabelUndefined Int
prot -> [Char]
"Label Undefined: " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> [Char]
forall a. Show a => a -> [Char]
show Int
prot
    BranchFirstMsgMustHaveTheSameSender r
psender [Char]
msgName r
from ->
      [Char]
"The first message of each branch must have the same sender. Sender: "
        [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> r -> [Char]
forall a. Show a => a -> [Char]
show r
psender
        [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
" But Msg: "
        [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
msgName
        [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
"'s sender is "
        [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> r -> [Char]
forall a. Show a => a -> [Char]
show r
from
    UndecideStateCanNotSendMsg [Char]
msgName -> [Char]
"Msg " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
msgName [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
" error, Undecide State can't send msg!"
    UndecideStateCanNotStartBranch [BranchSt (GenConst r) r bst]
brs -> [Char]
"Undecide State can't start branch! " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [BranchSt (GenConst r) r bst] -> [Char]
forall a. Show a => a -> [Char]
show [BranchSt (GenConst r) r bst]
brs
    TerminalNeedAllRoleDecide [Char]
msgName -> [Char]
"Msg " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
msgName [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
", Terminal need all role decide!"
    ProtocolError r bst
BranchAtLeastOneBranch -> [Char]
"Branch at least one branch!"
    ProtocolError r bst
AStateOnlyBeUsedForTheSamePair -> [Char]
"A state can only be used for the same pair of communicators." [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
internalError
    MsgDoNotExistBeforeNextTerm [Char]
st -> [Char]
"BranchSt " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
st [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
" do not exist any Msg before next term!"

internalError :: String
internalError :: [Char]
internalError = [Char]
"Internal error, please report: https://github.com/sdzx-1/typed-session/issues"

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 C.Constraint)
  | TracerSubMap C.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
traceWrapper :: [Char] -> ShowS
traceWrapper [Char]
desc [Char]
st =
  [Char]
"--------------------" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
desc [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"-----------------\n" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
st [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"\n"

instance (Show r, Show bst) => Show (Tracer r bst) where
  show :: Tracer r bst -> [Char]
show = \case
    TracerProtocolCreat Protocol Creat r bst
p -> [Char] -> ShowS
traceWrapper [Char]
"Creat" ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Protocol Creat r bst -> [Char]
forall a. Show a => a -> [Char]
show Protocol Creat r bst
p
    TracerProtocolIdx Protocol Idx r bst
p -> [Char] -> ShowS
traceWrapper [Char]
"Idx" ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Protocol Idx r bst -> [Char]
forall a. Show a => a -> [Char]
show Protocol Idx r bst
p
    TracerReRank IntMap Int
p -> [Char] -> ShowS
traceWrapper [Char]
"ReRank" ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ IntMap Int -> [Char]
forall a. Show a => a -> [Char]
show IntMap Int
p
    TracerProtocolAddNum Protocol AddNums r bst
p -> [Char] -> ShowS
traceWrapper [Char]
"AddNum" ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Protocol AddNums r bst -> [Char]
forall a. Show a => a -> [Char]
show Protocol AddNums r bst
p
    TracerProtocolGenConst Protocol (GenConst r) r bst
p -> [Char] -> ShowS
traceWrapper [Char]
"GenConst" ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Protocol (GenConst r) r bst -> [Char]
forall a. Show a => a -> [Char]
show Protocol (GenConst r) r bst
p
    TracerConstraints Seq Constraint
p -> [Char] -> ShowS
traceWrapper [Char]
"Constrains" ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Seq Constraint -> [Char]
forall a. Show a => a -> [Char]
show Seq Constraint
p
    TracerSubMap IntMap Int
p -> [Char] -> ShowS
traceWrapper [Char]
"SubMap" ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ IntMap Int -> [Char]
forall a. Show a => a -> [Char]
show IntMap Int
p
    TracerProtocolGenConstN Protocol (GenConst r) r bst
p -> [Char] -> ShowS
traceWrapper [Char]
"GenConstN" ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Protocol (GenConst r) r bst -> [Char]
forall a. Show a => a -> [Char]
show Protocol (GenConst r) r bst
p
    TracerVerifyResult IntMap (r, r)
m -> [Char] -> ShowS
traceWrapper [Char]
"VerifyResult Map" ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ IntMap (r, r) -> [Char]
forall a. Show a => a -> [Char]
show IntMap (r, r)
m
    TracerCollectBranchDynVal Set Int
dvs -> [Char] -> ShowS
traceWrapper [Char]
"CollectBranchDynVal" ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Set Int -> [Char]
forall a. Show a => a -> [Char]
show Set Int
dvs
    TracerProtocolMsgT Protocol (MsgT r bst) r bst
p -> [Char] -> ShowS
traceWrapper [Char]
"MsgT" ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Protocol (MsgT r bst) r bst -> [Char]
forall a. Show a => a -> [Char]
show Protocol (MsgT r bst) r bst
p
    TracerProtocolMsgT1 Protocol (MsgT1 r bst) r bst
p -> [Char] -> ShowS
traceWrapper [Char]
"MsgT1" ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Protocol (MsgT1 r bst) r bst -> [Char]
forall a. Show a => a -> [Char]
show Protocol (MsgT1 r bst) r bst
p
    TracerBranchResultTI [(r, [Char], T bst)]
v1 Map [Char] [(bst, [[[Char]]], T bst)]
st -> [Char] -> ShowS
traceWrapper [Char]
"BranchResultTI" ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ [(r, [Char], T bst)] -> [Char]
forall a. Show a => a -> [Char]
show [(r, [Char], T bst)]
v1 [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
"\n" [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> Map [Char] [(bst, [[[Char]]], T bst)] -> [Char]
forall a. Show a => a -> [Char]
show Map [Char] [(bst, [[[Char]]], T bst)]
st

------------------------

data Creat

type instance XMsg Creat = ()
type instance XLabel Creat = ()
type instance XBranch Creat = ()
type instance XBranchSt Creat = ()
type instance XGoto Creat = ()
type instance XTerminal Creat = ()

data Idx

type instance XMsg Idx = (Int, Int, Int)
type instance XLabel Idx = Int
type instance XBranch Idx = Int
type instance XBranchSt Idx = ()
type instance XGoto Idx = Int
type instance XTerminal Idx = Int

data AddNums

type instance XMsg AddNums = ([Int], [Int], Int)
type instance XLabel AddNums = [Int]
type instance XBranch AddNums = [Int]
type instance XBranchSt AddNums = ()
type instance XGoto AddNums = [Int]
type instance XTerminal AddNums = [Int]

data GenConst r

type instance XMsg (GenConst r) = (([Int], [Int]), (r, r), Int)
type instance XLabel (GenConst r) = ([Int], Int)
type instance XBranch (GenConst r) = [Int]
type instance XBranchSt (GenConst r) = ()
type instance XGoto (GenConst r) = ([Int], Int)
type instance XTerminal (GenConst r) = [Int]

data T bst
  = TNum Int
  | BstList Int bst
  | TAny Int
  | TEnd
instance (Show bst) => Show (T bst) where
  show :: T bst -> [Char]
show = \case
    TNum Int
i -> [Char]
"S" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
i
    BstList Int
i bst
bst -> [Char]
"S" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
i [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ bst -> [Char]
forall a. Show a => a -> [Char]
show bst
bst
    TAny Int
i -> [Char]
"S" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
i [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
" s"
    T bst
TEnd -> [Char]
"End"

data MsgT r bst

type instance XMsg (MsgT r bst) = ([T bst], (r, r), Int)
type instance XLabel (MsgT r bst) = ([T bst], Int)
type instance XBranch (MsgT r bst) = [T bst]
type instance XBranchSt (MsgT r bst) = ()
type instance XGoto (MsgT r bst) = ([T bst], Int)
type instance XTerminal (MsgT r bst) = [T bst]

data MsgT1 r bst

type instance XMsg (MsgT1 r bst) = ((T bst, T bst, T bst), (r, r), Int)
type instance XLabel (MsgT1 r bst) = ([T bst], Int)
type instance XBranch (MsgT1 r bst) = [T bst]
type instance XBranchSt (MsgT1 r bst) = ()
type instance XGoto (MsgT1 r bst) = ([T bst], Int)
type instance XTerminal (MsgT1 r bst) = [T bst]

------------------------

instance (Pretty (Protocol eta r bst), Show (XBranchSt eta), Show bst) => Pretty (BranchSt eta r bst) where
  pretty :: forall ann. BranchSt eta r bst -> Doc ann
pretty (BranchSt XBranchSt eta
xbst bst
bst [[[Char]]]
args Protocol eta r bst
prot) =
    Doc ann
"* BranchSt" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [Char] -> Doc ann
forall ann. [Char] -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (XBranchSt eta -> [Char]
forall a. Show a => a -> [Char]
show XBranchSt eta
xbst) Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [Char] -> Doc ann
forall ann. [Char] -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (bst -> [Char]
forall a. Show a => a -> [Char]
show bst
bst) Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [[Char]] -> Doc ann
forall ann. [[Char]] -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty ((([[Char]] -> [Char]) -> [[[Char]]] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
L.intercalate [Char]
" ") [[[Char]]]
args)) Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
forall ann. Doc ann
line Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> (Protocol eta r bst -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Protocol eta r bst -> Doc ann
pretty Protocol eta r bst
prot)

instance (Show (XMsg eta), Show (XLabel eta), Show r) => Pretty (MsgOrLabel eta r) where
  pretty :: forall ann. MsgOrLabel eta r -> Doc ann
pretty = \case
    Msg XMsg eta
xv [Char]
cst [[[Char]]]
args r
from r
to ->
      [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
hsep [Doc ann
"Msg", Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
angles ([Char] -> Doc ann
forall ann. [Char] -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty ([Char] -> Doc ann) -> [Char] -> Doc ann
forall a b. (a -> b) -> a -> b
$ XMsg eta -> [Char]
forall a. Show a => a -> [Char]
show XMsg eta
xv), [Char] -> Doc ann
forall ann. [Char] -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty [Char]
cst, [[Char]] -> Doc ann
forall ann. [[Char]] -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty ((([[Char]] -> [Char]) -> [[[Char]]] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
L.intercalate [Char]
" ") [[[Char]]]
args)), [Char] -> Doc ann
forall ann. [Char] -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (r -> [Char]
forall a. Show a => a -> [Char]
show r
from), [Char] -> Doc ann
forall ann. [Char] -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (r -> [Char]
forall a. Show a => a -> [Char]
show r
to)]
    Label XLabel eta
xv Int
i -> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
hsep [Doc ann
"Label", [Char] -> Doc ann
forall ann. [Char] -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty ([Char] -> Doc ann) -> [Char] -> Doc ann
forall a b. (a -> b) -> a -> b
$ XLabel eta -> [Char]
forall a. Show a => a -> [Char]
show XLabel eta
xv, Int -> Doc ann
forall ann. Int -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Int
i]

instance (ForallX Show eta, Show r, Show bst) => Pretty (Protocol eta r bst) where
  pretty :: forall ann. Protocol eta r bst -> Doc ann
pretty = \case
    MsgOrLabel eta r
msgOrLabel :> Protocol eta r bst
prots -> MsgOrLabel eta r -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. MsgOrLabel eta r -> Doc ann
pretty MsgOrLabel eta r
msgOrLabel Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
forall ann. Doc ann
line Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Protocol eta r bst -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Protocol eta r bst -> Doc ann
pretty Protocol eta r bst
prots
    Branch XBranch eta
is r
r [Char]
st [BranchSt eta r bst]
ls -> Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
nest Int
2 (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ Doc ann
"[Branch]" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [Char] -> Doc ann
forall ann. [Char] -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (XBranch eta -> [Char]
forall a. Show a => a -> [Char]
show XBranch eta
is) Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [Char] -> Doc ann
forall ann. [Char] -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (r -> [Char]
forall a. Show a => a -> [Char]
show r
r) Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [Char] -> Doc ann
forall ann. [Char] -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (ShowS
forall a. Show a => a -> [Char]
show [Char]
st) Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
forall ann. Doc ann
line Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vsep ((BranchSt eta r bst -> Doc ann)
-> [BranchSt eta r bst] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap BranchSt eta r bst -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. BranchSt eta r bst -> Doc ann
pretty [BranchSt eta r bst]
ls)
    Goto XGoto eta
xv Int
i -> Doc ann
"Goto" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [Char] -> Doc ann
forall ann. [Char] -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (XGoto eta -> [Char]
forall a. Show a => a -> [Char]
show XGoto eta
xv) Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Int -> Doc ann
forall ann. Int -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Int
i
    Terminal XTerminal eta
xv -> Doc ann
"Terminal" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [Char] -> Doc ann
forall ann. [Char] -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (XTerminal eta -> [Char]
forall a. Show a => a -> [Char]
show XTerminal eta
xv)

-----------------------------
instance (Pretty (Protocol eta r bst), Show (XBranchSt eta), Show bst) => Show (BranchSt eta r bst) where
  show :: BranchSt eta r bst -> [Char]
show = SimpleDocStream Any -> [Char]
forall ann. SimpleDocStream ann -> [Char]
renderString (SimpleDocStream Any -> [Char])
-> (BranchSt eta r bst -> SimpleDocStream Any)
-> BranchSt eta r bst
-> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LayoutOptions -> Doc Any -> SimpleDocStream Any
forall ann. LayoutOptions -> Doc ann -> SimpleDocStream ann
layoutPretty LayoutOptions
defaultLayoutOptions (Doc Any -> SimpleDocStream Any)
-> (BranchSt eta r bst -> Doc Any)
-> BranchSt eta r bst
-> SimpleDocStream Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BranchSt eta r bst -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. BranchSt eta r bst -> Doc ann
pretty

instance (Show (XMsg eta), Show (XLabel eta), Show r) => Show (MsgOrLabel eta r) where
  show :: MsgOrLabel eta r -> [Char]
show = SimpleDocStream Any -> [Char]
forall ann. SimpleDocStream ann -> [Char]
renderString (SimpleDocStream Any -> [Char])
-> (MsgOrLabel eta r -> SimpleDocStream Any)
-> MsgOrLabel eta r
-> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LayoutOptions -> Doc Any -> SimpleDocStream Any
forall ann. LayoutOptions -> Doc ann -> SimpleDocStream ann
layoutPretty LayoutOptions
defaultLayoutOptions (Doc Any -> SimpleDocStream Any)
-> (MsgOrLabel eta r -> Doc Any)
-> MsgOrLabel eta r
-> SimpleDocStream Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MsgOrLabel eta r -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. MsgOrLabel eta r -> Doc ann
pretty

instance (ForallX Show eta, Show r, Show bst) => Show (Protocol eta r bst) where
  show :: Protocol eta r bst -> [Char]
show = SimpleDocStream Any -> [Char]
forall ann. SimpleDocStream ann -> [Char]
renderString (SimpleDocStream Any -> [Char])
-> (Protocol eta r bst -> SimpleDocStream Any)
-> Protocol eta r bst
-> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LayoutOptions -> Doc Any -> SimpleDocStream Any
forall ann. LayoutOptions -> Doc ann -> SimpleDocStream ann
layoutPretty LayoutOptions
defaultLayoutOptions (Doc Any -> SimpleDocStream Any)
-> (Protocol eta r bst -> Doc Any)
-> Protocol eta r bst
-> SimpleDocStream Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Protocol eta r bst -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Protocol eta r bst -> Doc ann
pretty