typed-session-state-algorithm 0.1.0.2 → 0.2.0.0

raw patch · 11 files changed

+479/−670 lines, 11 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• CHANGELOG.md +4/−0
• src/TypedSession/State/GenDoc.hs +0/−199
• src/TypedSession/State/Parser.hs +7/−8
• src/TypedSession/State/Pattern.hs +0/−29
• src/TypedSession/State/Pipeline.hs +436/−0
• src/TypedSession/State/Piple.hs +0/−411
• src/TypedSession/State/Render.hs +1/−16
• src/TypedSession/State/Type.hs +23/−0
• src/TypedSession/State/Utils.hs +1/−1
• test/Main.hs +5/−2
• typed-session-state-algorithm.cabal +2/−4

@@ -1,5 +1,9 @@ # Revision history for typed-session-state-algorithm +## 0.2.0.0++* Fix Pipeline, add check and verify.+ ## 0.1.0.2  *New protocol check function.

@@ -1,199 +0,0 @@-{-# LANGUAGE AllowAmbiguousTypes #-}-{-# LANGUAGE ConstraintKinds #-}-{-# LANGUAGE DeriveFunctor #-}-{-# LANGUAGE EmptyCase #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE LambdaCase #-}-{-# LANGUAGE MultiWayIf #-}-{-# LANGUAGE NamedFieldPuns #-}-{-# LANGUAGE OverloadedStrings #-}-{-# LANGUAGE PatternSynonyms #-}-{-# LANGUAGE RankNTypes #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeAbstractions #-}-{-# LANGUAGE TypeApplications #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE UndecidableInstances #-}--module TypedSession.State.GenDoc where--import qualified Data.List as L-import qualified Data.Set as Set-import Prettyprinter-import Prettyprinter.Render.String (renderString)-import TypedSession.State.Piple-import TypedSession.State.Render-import TypedSession.State.Type (Creat, Protocol, ProtocolError)--genRole :: forall r ann. (Enum r, Bounded r, Show r) => String -> Doc ann-genRole rname =-  let rg = rRange @r-      sRole = pretty ("S" <> rname)-      header = "data" <+> sRole <+> "::" <+> pretty rname <+> "-> Type where"-   in vsep-        [ nest 2 $ vsep $ header : [(pretty ("S" <> show r) <+> "::" <+> sRole <+> pretty (show r)) | r <- rg]-        , "type" <+> "instance" <+> "Sing" <+> "=" <+> sRole-        ]-        <> line-        <> vsep-          [ nest-              2-              ( vsep-                  [ "instance" <+> "SingI" <+> pretty (show r) <+> " where"-                  , "sing" <+> "=" <+> pretty ("S" <> show r)-                  ]-              )-          | r <- rg-          ]-        <> line-        <> ( nest 2 $-              vsep-                [ "instance SingToInt" <+> pretty rname <+> "where"-                , "singToInt x = I# (dataToTag# x)"-                ]-           )--genSt :: forall r bst ann. String -> String -> PipleResult r bst -> Doc ann-genSt protName bstName (PipleResult{dnySet, stBound = (start, end)}) =-  let-    protNameSt = protName <> "St"-    sProtNameSt = "S" <> protName <> "St"-    protSt =-      nest 2 $-        vsep $-          ["data" <+> pretty protNameSt]-            ++ [ if-                  | i == -1 -> "= End"-                  | i `Set.member` dnySet -> pretty ("| S" ++ show i) <+> pretty bstName-                  | otherwise -> pretty ("| S" ++ show i)-               | i <- [start .. end]-               ]-    protSSt =-      nest 2 $-        vsep $-          ["data" <+> pretty sProtNameSt <+> "::" <+> pretty protNameSt <+> "-> Type where"]-            ++ [ if-                  | i == -1 -> "SEnd ::" <+> pretty sProtNameSt <+> "End"-                  | i `Set.member` dnySet -> pretty ("SS" ++ show i ++ " ::") <+> pretty sProtNameSt <+> pretty ("(S" <> show i <> " s)")-                  | otherwise -> pretty ("SS" ++ show i ++ " ::") <+> pretty sProtNameSt <+> pretty ("S" <> show i)-               | i <- [start .. end]-               ]-    instVal i =-      nest 2 $-        vsep $-          [ "instance SingI"-              <+> ( if i == -1-                      then "End"-                      else-                        if i-                          `Set.member` dnySet-                          then parens (pretty ("S" <> show i) <> " s")-                          else pretty ("S" <> show i)-                  )-              <+> "where"-          , "sing =" <+> if i == -1 then "SEnd" else pretty ("SS" <> show i)-          ]-    instVals = vsep [instVal i | i <- [start .. end]]-    stoInt =-      ( nest 2 $-          vsep-            [ "instance SingToInt" <+> pretty protNameSt <+> "where"-            , "singToInt x = I# (dataToTag# x)"-            ]-      )-   in-    vsep-      [ protSt-      , protSSt-      , "type instance Sing =" <+> pretty sProtNameSt-      , instVals-      , stoInt-      ]--genProtIns :: forall r bst ann. (Enum r, Bounded r, Show bst, Show r) => String -> String -> PipleResult r bst -> Doc ann-genProtIns roleName protName PipleResult{msgT1} =-  let-    protNameSt = protName <> "St"-    typeDone = ["type Done" <+> pretty (show r) <+> "= End" | r <- rRange @r]-   in-    nest 2 $-      vsep-        [ "instance Protocol" <+> pretty roleName <+> pretty protNameSt <+> "where"-        , vsep typeDone-        , nest 2 $-            vsep-              [ "data Msg" <+> pretty roleName <+> pretty protNameSt <+> "from send recv where"-              , vsep (genDoc roleName protName msgT1)-              ]-        ]--genGraph :: (Enum r, Bounded r, Show bst, Ord r, Show r) => StrFillEnv -> PipleResult r bst -> String-genGraph sfe PipleResult{msgT} = runRender sfe (stMsgT sfe) msgT--genAllDoc'-  :: forall r bst ann-   . (Enum r, Bounded r, Ord r, Show r, Show bst)-  => StrFillEnv-  -> Protocol Creat r bst-  -> String -- role name-  -> String -- protocol name-  -> String -- bst name-  -> [String] -- module Name-  -> Either (ProtocolError r bst) (Doc ann)-genAllDoc' sfe prot rName pName bstName moduleNames = case piple prot of-  Left e -> Left e-  Right pipResult1 ->-    Right $-      vsep-        [ "{-# LANGUAGE DataKinds #-}"-        , "{-# LANGUAGE FlexibleInstances #-}"-        , "{-# LANGUAGE GADTs #-}"-        , "{-# LANGUAGE MagicHash #-}"-        , "{-# LANGUAGE MultiParamTypeClasses #-}"-        , "{-# LANGUAGE TypeFamilies #-}"-        , "module" <+> pretty (L.intercalate "." moduleNames) <+> "where"-        , "import Data.IFunctor (Sing, SingI (sing))"-        , "import Data.Kind"-        , "import GHC.Exts (dataToTag#)"-        , "import GHC.Int (Int (I#))"-        , "import TypedProtocol.Core"-        , "{-"-        , pretty $ genGraph sfe pipResult1-        , "-}"-        , genRole @r rName-        , genSt pName bstName pipResult1-        , genProtIns rName pName pipResult1-        ]--genAllDoc-  :: forall r bst-   . (Enum r, Bounded r, Ord r, Show r, Show bst)-  => StrFillEnv-  -> Protocol Creat r bst-  -> String -- role name-  -> String -- protocol name-  -> String -- bst name-  -> [String] -- module names-  -> Either (ProtocolError r bst) String-genAllDoc sfe a b c d e =-  renderString . layoutPretty defaultLayoutOptions-    <$> genAllDoc' sfe a b c d e--genAllFile-  :: forall r bst-   . (Enum r, Bounded r, Ord r, Show r, Show bst)-  => StrFillEnv-  -> Protocol Creat r bst-  -> String -- role name-  -> String -- protocol name-  -> String -- bst name-  -> [String] -- module names-  -> IO ()-genAllFile sfe a b c d e = case genAllDoc sfe a b c d e of-  Left er -> print er-  Right st -> do-    let name = case e of-          [] -> "Type"-          xs -> last xs-    writeFile name st

@@ -12,8 +12,7 @@ import Text.Megaparsec hiding (Label, label) import Text.Megaparsec.Char (char, space1, string) import qualified Text.Megaparsec.Char.Lexer as L-import TypedSession.State.Pattern-import TypedSession.State.Type (BranchSt, Creat, MsgOrLabel, Protocol)+import TypedSession.State.Type  {- @@ -105,24 +104,24 @@   args <- brackets (constrOrType `sepBy` comma)   from <- mkParserA @r   to <- mkParserA @r-  pure $ Msg constr args from to+  pure $ Msg () constr args from to  parseLabel :: (Show r) => Parser (MsgOrLabel Creat r) parseLabel = dbg "Label" $ do   label   i <- fromIntegral <$> integer-  pure $ Label i+  pure $ Label () i  parseGoto :: (Show bst, Show r) => Parser (Protocol Creat r bst) parseGoto = dbg "Goto" $ do   goto   i <- fromIntegral <$> integer-  pure $ Goto i+  pure $ Goto () i  parseTerminal :: (Show bst, Show r) => Parser (Protocol Creat r bst) parseTerminal = dbg "Terminal" $ do   terminal-  pure $ Terminal+  pure $ Terminal ()  parseBranchSt   :: forall bst r@@ -132,7 +131,7 @@   branchSt   bst <- mkParserA @bst   prot <- parseProtocol @r @bst-  pure (BranchSt bst prot)+  pure (BranchSt () bst prot)  parseBranch   :: forall r bst@@ -142,7 +141,7 @@   r1 <- mkParserA @r   braces $ do     branchSts <- some (parseBranchSt @bst @r)-    pure (Branch r1 branchSts)+    pure (Branch () r1 branchSts)  parseMsgOrLabel   :: forall r bst

@@ -1,29 +0,0 @@-{-# LANGUAGE PatternSynonyms #-}--module TypedSession.State.Pattern where--import TypedSession.State.Type (Creat, Protocol)-import qualified TypedSession.State.Type as N--pattern Msg :: String -> [String] -> r -> r -> N.MsgOrLabel Creat r-pattern Msg a b c d = N.Msg () a b c d--pattern Label :: Int -> N.MsgOrLabel Creat r-pattern Label i = N.Label () i--pattern BranchSt :: bst -> Protocol Creat r bst -> N.BranchSt Creat r bst-pattern BranchSt a b = N.BranchSt () a b--infixr 5 :>--pattern (:>) :: N.MsgOrLabel Creat r -> Protocol Creat r bst -> Protocol Creat r bst-pattern (:>) a b = a N.:> b--pattern Branch :: r -> [N.BranchSt Creat r bst] -> Protocol Creat r bst-pattern Branch a b = N.Branch () a b--pattern Goto :: Int -> Protocol Creat r bst-pattern Goto i = N.Goto () i--pattern Terminal :: Protocol Creat r bst-pattern Terminal = N.Terminal ()

@@ -0,0 +1,436 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE EmptyCase #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MultiWayIf #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeAbstractions #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE NoFieldSelectors #-}+{-# OPTIONS_GHC -Wno-unused-do-bind #-}++module TypedSession.State.Pipeline where++import Control.Algebra ((:+:))+import Control.Carrier.Error.Either (runError)+import Control.Carrier.Fresh.Strict+import Control.Carrier.Reader (runReader)+import Control.Carrier.State.Strict+import Control.Carrier.Writer.Strict (runWriter)+import Control.Effect.Error+import Control.Effect.Reader+import Control.Effect.Writer+import Control.Monad+import Data.Foldable (Foldable (toList), for_)+import Data.IntMap (IntMap)+import qualified Data.IntMap as IntMap+import qualified Data.List as L+import Data.Map (Map)+import qualified Data.Map as Map+import Data.Sequence (Seq)+import qualified Data.Sequence as Seq+import Data.Set (Set)+import qualified Data.Set as Set+import Prettyprinter+import qualified TypedSession.State.Constraint as C+import TypedSession.State.Render+import TypedSession.State.Type+import TypedSession.State.Utils++------------------------++newtype Index = Index Int deriving (Show, Eq, Ord, Num)++addIdxXTraverse+  :: forall r bst sig m+   . ( Has (State Int :+: State Index :+: State (Set Int) :+: Error (ProtocolError r bst)) sig m+     , Enum r+     , Bounded r+     , Ord r+     )+  => XTraverse m Creat Idx r bst+addIdxXTraverse =+  ( \_ -> do+      inputIdx <- get @Int+      modify @Int (+ 1)+      Index idx <- get @Index+      modify @Index (+ 1)+      outputInx <- get @Int+      pure (inputIdx, outputInx, idx)+  , const get+  , \(_, _) -> do+      inputIdx <- get @Int+      modify (Set.insert inputIdx)+      pure (inputIdx, id)+  , \_ -> do+      put (Index 0)+      modify @Int (+ 1)+  , const get+  , const get+  )++reRankXTraverse :: (Monad m) => IntMap Int -> XTraverse m Idx Idx r bst+reRankXTraverse sbm =+  ( \((a, b, idx), _) -> pure (replaceVal sbm a, replaceVal sbm b, idx)+  , \(xs, _) -> pure (replaceVal sbm xs)+  , \(a, _) -> pure (replaceVal sbm a, id)+  , \_ -> pure ()+  , \(xs, _) -> pure (replaceVal sbm xs)+  , \xs -> pure (replaceVal sbm xs)+  )++addNumsXTraverse+  :: forall r bst sig m+   . ( Has (Error (ProtocolError r bst)) sig m+     , Enum r+     , Bounded r+     , Ord r+     )+  => XTraverse m Idx AddNums r bst+addNumsXTraverse =+  let mkNums i =+        let sized = fromEnum (maxBound @r) + 1+         in fmap (\x -> i * sized + fromEnum x) (rRange @r)+   in ( \((va, vb, idx), _) -> pure (mkNums va, mkNums vb, idx)+      , \(va, _) -> pure $ mkNums va+      , \(va, _) -> pure (mkNums va, id)+      , \_ -> pure ()+      , \(va, _) -> pure $ mkNums va+      , \va -> pure $ mkNums va+      )++toGenConstrXTraverse :: (Monad m) => XTraverse m AddNums (GenConst r) r bst+toGenConstrXTraverse =+  ( \((a, b, i), (_, _, from, to, _)) -> pure ((a, b), (from, to), i)+  , \(is, (i, _)) -> pure (is, i)+  , \(xv, _) -> pure (xv, id)+  , \_ -> pure ()+  , \(xs, i) -> pure (xs, i)+  , \xv -> pure xv+  )++data CurrSt = Decide | Undecide deriving (Show, Eq, Ord)++getRCurrSt :: forall r sig m. (Has (State (Map r CurrSt)) sig m, Ord r) => r -> m CurrSt+getRCurrSt r =+  gets @(Map r CurrSt) (Map.lookup r) >>= \case+    Nothing -> error internalError+    Just v -> pure v++restoreWrapper1 :: forall r sig m a. (Has (State (Map r CurrSt) :+: State r) sig m) => m a -> m a+restoreWrapper1 m = do+  s1 <- get @(Map r CurrSt)+  s2 <- get @r+  a <- m+  put s1+  put s2+  pure a++checkProtXFold+  :: forall r bst sig m+   . (Has (State (Map r CurrSt) :+: State r :+: Error (ProtocolError r bst)) sig m, Eq r, Ord r, Enum r, Bounded r)+  => XFold m (GenConst r) r bst+checkProtXFold =+  ( \((_, (from, to), idx), (msgName, _, _, _, prot)) -> do+      when (idx == 0) $ do+        r1 <- get @r+        if from == r1+          then pure ()+          else throwError @(ProtocolError r bst) (BranchFirstMsgMustHaveTheSameSender r1 msgName from)+      fromCurrSt <- getRCurrSt from+      when (fromCurrSt == Undecide) (throwError @(ProtocolError r bst) (UndecideStateCanNotSendMsg msgName))+      modify (Map.insert to Decide)+      case prot of+        Terminal _ -> do+          vals <- gets @(Map r CurrSt) Map.elems+          when (any (/= Decide) vals) (throwError @(ProtocolError r bst) (TerminalNeedAllRoleDecide msgName))+        _ -> pure ()+  , \_ -> pure ()+  , \(_, (r1, ls)) -> do+      r1CurrSt <- getRCurrSt r1+      when (r1CurrSt == Undecide) (throwError @(ProtocolError r bst) (UndecideStateCanNotStartBranch ls))+      for_ [r | r <- rRange, r /= r1] $ \r -> modify (Map.insert r Undecide)+      when (length ls < 1) (throwError @(ProtocolError r bst) BranchAtLeastOneBranch)+      put r1+      pure (restoreWrapper1 @r)+  , \_ -> pure ()+  , \_ -> pure ()+  , \_ -> pure ()+  )++genConstrXFold+  :: forall r bst sig m+   . (Has (State (IntMap [Int]) :+: State [Int] :+: Writer (Seq C.Constraint) :+: Error (ProtocolError r bst)) sig m, Enum r)+  => XFold m (GenConst r) r bst+genConstrXFold =+  ( \(((is, os), (from, to), index), _) -> do+      let ifrom = fromEnum from+          ito = fromEnum to+          from' = is !! ifrom --- is+          to' = is !! ito ------- is+          deleteIndexFromTo ks =+            fmap snd $ filter (\(idx, _) -> idx /= ifrom && idx /= ito) $ zip [0 ..] ks+          deleteIndexFrom ks =+            fmap snd $ filter (\(idx, _) -> idx /= ifrom) $ zip [0 ..] ks++      when (index == 0) $ do+        branchSts <- get @[Int]+        tellSeq $ map (uncurry C.Constraint) $ zip (deleteIndexFrom branchSts) (deleteIndexFrom is)++      tellSeq $+        C.Constraint from' to'+          : zipWith C.Constraint (deleteIndexFromTo is) (deleteIndexFromTo os)+  , \((is, i), lb) ->+      gets (IntMap.lookup @[Int] i) >>= \case+        Just _ -> throwError @(ProtocolError r bst) (DefLabelMultTimes lb)+        Nothing -> modify (IntMap.insert i is)+  , \(is, _) -> do+      put is+      pure (restoreWrapper @[Int])+  , \_ -> pure ()+  , \((xs, i), gt) -> do+      gets (IntMap.lookup i) >>= \case+        Nothing -> throwError @(ProtocolError r bst) (LabelUndefined gt)+        Just ls -> tellSeq $ zipWith C.Constraint xs ls+  , \(xs) -> tellSeq $ zipWith C.Constraint xs (cycle [-1])+  )++replXTraverse :: (Monad m) => C.SubMap -> XTraverse m (GenConst r) (GenConst r) r bst+replXTraverse sbm =+  ( \(((a, b), (from, to), i), _) ->+      pure ((replaceList sbm a, replaceList sbm b), (from, to), i)+  , \((xs, i), _) -> pure (replaceList sbm xs, i)+  , \(a, _) -> pure (replaceList sbm a, id)+  , \_ -> pure ()+  , \((xs, i), _) -> pure (replaceList sbm xs, i)+  , \xs -> pure (replaceList sbm xs)+  )++verifyProtXFold+  :: forall r bst sig m+   . (Has (State (IntMap (r, r)) :+: Error (ProtocolError r bst)) sig m, Enum r, Eq r)+  => XFold m (GenConst r) r bst+verifyProtXFold =+  ( \(((is, _), ft@(from, _to), _), _) -> do+      let from' = is !! fromEnum from+      res <- gets @(IntMap (r, r)) (IntMap.lookup from')+      case res of+        Nothing -> modify (IntMap.insert from' ft)+        Just ft1 -> when (ft1 /= ft) (throwError @(ProtocolError r bst) AStateOnlyBeUsedForTheSamePair)+  , \_ -> pure ()+  , \_ -> pure id+  , \_ -> pure ()+  , \_ -> pure ()+  , \_ -> pure ()+  )++collectBranchDynValXFold :: (Has (State (Set Int)) sig m, Enum r) => XFold m (GenConst r) r bst+collectBranchDynValXFold =+  ( \_ -> pure ()+  , \_ -> pure ()+  , \(ls, (r, _)) -> do+      let ls' = map snd $ filter (\(i, _) -> i /= fromEnum r) $ zip [0 ..] ls+      modify (`Set.union` (Set.fromList ls'))+      pure id+  , \_ -> pure ()+  , \_ -> pure ()+  , \_ -> pure ()+  )++genT+  :: forall bst sig m+   . (Has (Reader (Set Int) :+: State bst) sig m)+  => (bst -> Int -> T bst) -> Int -> m (T bst)+genT fun i = do+  dynSet <- ask @(Set Int)+  if i == -1+    then pure (TEnd)+    else+      if Set.member i dynSet+        then do+          bst <- get+          pure (fun bst i)+        else pure $ TNum i++genMsgTXTraverse+  :: forall r bst sig m+   . (Has (Reader (Set Int) :+: State bst) sig m, Enum r, Eq r, Bounded r)+  => XTraverse m (GenConst r) (MsgT r bst) r bst+genMsgTXTraverse =+  ( \(((is, _), (from, to), vi), _) -> do+      is' <- forM (zip rRange is) $+        \(key, i) -> genT @bst (\bst1 i1 -> if key == from then BstList i1 bst1 else TAny i1) i+      pure (is', (from, to), vi)+  , \((ls, idx), _) -> do+      ls' <- mapM (genT (const TAny)) ls+      pure (ls', idx)+  , \(ls, (r, _)) -> do+      ls' <- mapM (\(idx, v) -> genT (if idx == fromEnum r then const TNum else (const TAny)) v) (zip [0 ..] ls)+      pure (ls', restoreWrapper @bst)+  , \(_, (bst, _)) -> put bst+  , \((is, i), _) -> do+      is' <- mapM (genT @bst (const TAny)) is+      pure (is', i)+  , \ls -> pure $ fmap (const TEnd) ls+  )++getFirstXV :: Protocol (MsgT r bst) r bst -> [T bst]+getFirstXV = \case+  Msg (xv, _, _) _ _ _ _ :> _ -> xv+  Label (xv, _) _ :> _ -> xv+  Branch xv _ _ -> xv+  Goto (xv, _) _ -> xv+  Terminal xv -> xv++genMsgT1XTraverse :: (Monad m, Enum r) => XTraverse m (MsgT r bst) (MsgT1 r bst) r bst+genMsgT1XTraverse =+  ( \((is, (from, to), i), (_, _, _, _, prot)) -> do+      let os = getFirstXV prot+          from' = fromEnum from+          to' = fromEnum to+      pure ((is !! from', os !! from', os !! to'), (from, to), i)+  , \(a, _) -> pure a+  , \(a, _) -> pure (a, id)+  , \(a, _) -> pure a+  , \(a, _) -> pure a+  , \a -> pure a+  )++data PipleResult r bst = PipleResult+  { msgT :: Protocol (MsgT r bst) r bst+  , msgT1 :: Protocol (MsgT1 r bst) r bst+  , dnySet :: Set Int+  , stBound :: (Int, Int)+  }++reRank :: Set Int -> Int -> IntMap Int+reRank branchValSet maxSize =+  let allSet = Set.insert 0 branchValSet+      restList = [i | i <- [0 .. maxSize], i `Set.notMember` allSet]+   in IntMap.fromList $ zip (Set.toList allSet ++ restList) [0 ..]++piple'+  :: forall r bst sig m+   . ( Has (Error (ProtocolError r bst)) sig m+     , Enum r+     , Bounded r+     , Eq r+     , Ord r+     )+  => (Tracer r bst -> m ())+  -> Protocol Creat r bst+  -> m (PipleResult r bst)+piple' trace prot0 = do+  trace (TracerProtocolCreat prot0)+  (brSet, (maxSzie, (_, idxProt))) <-+    runState @(Set Int) Set.empty+      . runState @Int 0+      . runState @Index (Index 100)+      $ (xtraverse addIdxXTraverse prot0)+  trace (TracerProtocolIdx idxProt)+  trace (TracerReRank (reRank brSet maxSzie))+  idxProt1 <- xtraverse (reRankXTraverse (reRank brSet maxSzie)) idxProt+  trace (TracerProtocolIdx idxProt1)+  prot1 <- xtraverse addNumsXTraverse idxProt1+  trace (TracerProtocolAddNum prot1)+  prot2 <- xtraverse toGenConstrXTraverse prot1+  trace (TracerProtocolGenConst prot2)+  void+    . runState @(Map r CurrSt) (Map.fromList $ zip (rRange @r) (cycle [Decide]))+    . runState @r (error internalError)+    $ xfold checkProtXFold prot2+  (constraintList, _) <-+    runWriter @(Seq C.Constraint)+      . runState @(IntMap [Int]) (IntMap.empty)+      . runState @[Int] (error internalError)+      $ xfold genConstrXFold prot2+  trace (TracerConstraints constraintList)+  let (sbm, stBound) = compressSubMap $ C.constrToSubMap $ toList constraintList+  trace (TracerSubMap sbm)+  prot3 <- xtraverse (replXTraverse sbm) prot2+  trace (TracerProtocolGenConstN prot3)+  verifyResult <- fst <$> runState @(IntMap (r, r)) (IntMap.empty) (xfold verifyProtXFold prot3)+  trace (TracerVerifyResult verifyResult)+  dnys <- fst <$> runState @((Set Int)) (Set.empty) (xfold collectBranchDynValXFold prot3)+  trace (TracerCollectBranchDynVal dnys)+  prot4 <-+    fmap snd+      . runReader @(Set Int) dnys+      . runState @bst (error internalError)+      $ (xtraverse genMsgTXTraverse prot3)+  trace (TracerProtocolMsgT prot4)+  prot5 <- xtraverse genMsgT1XTraverse prot4+  trace (TracerProtocolMsgT1 prot5)+  pure (PipleResult prot4 prot5 dnys stBound)++piple+  :: forall r bst+   . (Enum r, Bounded r, Eq r, Ord r)+  => Protocol Creat r bst+  -> Either+      (ProtocolError r bst)+      (PipleResult r bst)+piple protocol =+  run $ runError @(ProtocolError r bst) $ (piple' (const (pure ())) protocol)++pipleWithTracer+  :: forall r bst+   . (Enum r, Bounded r, Eq r, Ord r)+  => Protocol Creat r bst+  -> ( Seq (Tracer r bst)+     , Either+        (ProtocolError r bst)+        (PipleResult r bst)+     )+pipleWithTracer protocol =+  run+    . runWriter @(Seq (Tracer r bst))+    . runError @(ProtocolError r bst)+    $ (piple' (\w -> tell @(Seq (Tracer r bst)) (Seq.singleton w)) protocol)++genDocXFold+  :: forall r bst ann sig m+   . ( Has (Writer [Doc ann]) sig m+     , Show r+     , Show bst+     )+  => String -> String -> XFold m (MsgT1 r bst) r bst+genDocXFold rName protName =+  ( \( ((sendStart, sendEnd, recEnd), (from, to), _)+      , (cons, args, _, _, _)+      ) -> do+        tell @[Doc ann]+          [ pretty cons+              <+> "::"+              <+> pretty (L.intercalate "->" args)+              <+> (if null args then emptyDoc else "->")+              <+> "Msg"+              <+> pretty rName+              <+> pretty (protName <> "St")+              <+> parens (pretty $ show sendStart)+              <+> (pretty $ '\'' : show (from, sendEnd))+              <+> (pretty $ '\'' : show (to, recEnd))+          ]+  , \_ -> pure ()+  , \_ -> pure (id)+  , \_ -> pure ()+  , \_ -> pure ()+  , \_ -> pure ()+  )++genDoc :: forall r bst ann. (Show r, Show bst) => String -> String -> Protocol (MsgT1 r bst) r bst -> [Doc ann]+genDoc rName protName prot =+  fst $ run $ runWriter @[Doc ann] (xfold (genDocXFold @r @bst @ann rName protName) prot)++genGraph :: (Enum r, Bounded r, Show bst, Ord r, Show r) => StrFillEnv -> PipleResult r bst -> String+genGraph sfe PipleResult{msgT} = runRender sfe (stMsgT sfe) msgT

@@ -1,411 +0,0 @@-{-# LANGUAGE AllowAmbiguousTypes #-}-{-# LANGUAGE ConstraintKinds #-}-{-# LANGUAGE DeriveFunctor #-}-{-# LANGUAGE EmptyCase #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE GeneralizedNewtypeDeriving #-}-{-# LANGUAGE LambdaCase #-}-{-# LANGUAGE MultiWayIf #-}-{-# LANGUAGE OverloadedStrings #-}-{-# LANGUAGE PatternSynonyms #-}-{-# LANGUAGE RankNTypes #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeAbstractions #-}-{-# LANGUAGE TypeApplications #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE UndecidableInstances #-}-{-# LANGUAGE NoFieldSelectors #-}--module TypedSession.State.Piple where--import Control.Algebra ((:+:))-import Control.Carrier.Error.Either (runError)-import Control.Carrier.Fresh.Strict-import Control.Carrier.Reader (runReader)-import Control.Carrier.State.Strict-import Control.Carrier.Writer.Strict (runWriter)-import Control.Effect.Error-import Control.Effect.Reader-import Control.Effect.Writer-import Control.Monad-import Data.Foldable (Foldable (toList), for_)-import Data.IntMap (IntMap)-import qualified Data.IntMap as IntMap-import qualified Data.List as L-import Data.Map (Map)-import qualified Data.Map as Map-import Data.Sequence (Seq)-import qualified Data.Sequence as Seq-import Data.Set (Set)-import qualified Data.Set as Set-import Prettyprinter-import qualified TypedSession.State.Constraint as C-import TypedSession.State.Render-import TypedSession.State.Type-import TypedSession.State.Utils----------------------------newtype Index = Index Int deriving (Show, Eq, Ord, Num)--addIdxXTraverse-  :: forall r bst sig m-   . ( Has (State Int :+: State Index :+: State (Set Int) :+: Error (ProtocolError r bst)) sig m-     , Enum r-     , Bounded r-     , Ord r-     )-  => XTraverse m Creat Idx r bst-addIdxXTraverse =-  ( \_ -> do-      inputIdx <- get @Int-      modify @Int (+ 1)-      Index idx <- get @Index-      modify @Index (+ 1)-      outputInx <- get @Int-      pure (inputIdx, outputInx, idx)-  , const get-  , \(_, _) -> do-      inputIdx <- get @Int-      modify (Set.insert inputIdx)-      pure (inputIdx, id)-  , \_ -> do-      put (Index 0)-      modify @Int (+ 1)-  , const get-  , const get-  )--reRankXTraverse :: (Monad m) => IntMap Int -> XTraverse m Idx Idx r bst-reRankXTraverse sbm =-  ( \((a, b, idx), _) -> pure (replaceVal sbm a, replaceVal sbm b, idx)-  , \(xs, _) -> pure (replaceVal sbm xs)-  , \(a, _) -> pure (replaceVal sbm a, id)-  , \_ -> pure ()-  , \(xs, _) -> pure (replaceVal sbm xs)-  , \xs -> pure (replaceVal sbm xs)-  )--addNumsXTraverse-  :: forall r bst sig m-   . ( Has (Error (ProtocolError r bst)) sig m-     , Enum r-     , Bounded r-     , Ord r-     )-  => XTraverse m Idx AddNums r bst-addNumsXTraverse =-  let mkNums i =-        let sized = fromEnum (maxBound @r) + 1-         in fmap (\x -> i * sized + fromEnum x) (rRange @r)-   in ( \((va, vb, idx), _) -> pure (mkNums va, mkNums vb, idx)-      , \(va, _) -> pure $ mkNums va-      , \(va, _) -> pure (mkNums va, id)-      , \_ -> pure ()-      , \(va, _) -> pure $ mkNums va-      , \va -> pure $ mkNums va-      )--toGenConstrXTraverse :: (Monad m) => XTraverse m AddNums (GenConst r) r bst-toGenConstrXTraverse =-  ( \((a, b, i), (_, _, from, to, _)) -> pure ((a, b), (from, to), i)-  , \(is, (i, _)) -> pure (is, i)-  , \(xv, _) -> pure (xv, id)-  , \_ -> pure ()-  , \(xs, i) -> pure (xs, i)-  , \xv -> pure xv-  )--data CurrSt = Decide | Undecide deriving (Show, Eq, Ord)--getRCurrSt :: forall r sig m. (Has (State (Map r CurrSt)) sig m, Ord r) => r -> m CurrSt-getRCurrSt r =-  gets @(Map r CurrSt) (Map.lookup r) >>= \case-    Nothing -> error "np"-    Just v -> pure v--restoreWrapper1 :: forall r sig m a. (Has (State (Map r CurrSt) :+: State r) sig m) => m a -> m a-restoreWrapper1 m = do-  s1 <- get @(Map r CurrSt)-  s2 <- get @r-  a <- m-  put s1-  put s2-  pure a--checkProtXFold-  :: forall r bst sig m-   . (Has (State (Map r CurrSt) :+: State r :+: Error (ProtocolError r bst)) sig m, Eq r, Ord r, Enum r, Bounded r)-  => XFold m (GenConst r) r bst-checkProtXFold =-  ( \((_, (from, to), idx), (msgName, _, _, _, prot)) -> do-      when (idx == 0) $ do-        r1 <- get @r-        if from == r1-          then pure ()-          else throwError @(ProtocolError r bst) (BranchFirstMsgMustHaveTheSameSender r1 msgName from)-      fromCurrSt <- getRCurrSt from-      when (fromCurrSt == Undecide) (throwError @(ProtocolError r bst) (UndecideStateCanNotSendMsg msgName))-      modify (Map.insert to Decide)-      case prot of-        Terminal _ -> do-          vals <- gets @(Map r CurrSt) Map.elems-          when (any (/= Decide) vals) (throwError @(ProtocolError r bst) (TerminalNeedAllRoleDecide msgName))-        _ -> pure ()-  , \_ -> pure ()-  , \(_, (r1, ls)) -> do-      r1CurrSt <- getRCurrSt r1-      when (r1CurrSt == Undecide) (throwError @(ProtocolError r bst) (UndecideStateCanNotStartBranch ls))-      for_ [r | r <- rRange, r /= r1] $ \r -> modify (Map.insert r Undecide)-      when (length ls < 1) (throwError @(ProtocolError r bst) BranchAtLeastOneBranch)-      put r1-      pure (restoreWrapper1 @r)-  , \_ -> pure ()-  , \_ -> pure ()-  , \_ -> pure ()-  )--genConstrXFold-  :: forall r bst sig m-   . (Has (State (IntMap [Int]) :+: State [Int] :+: Writer (Seq C.Constraint) :+: Error (ProtocolError r bst)) sig m, Enum r)-  => XFold m (GenConst r) r bst-genConstrXFold =-  ( \(((is, os), (from, to), index), _) -> do-      let ifrom = fromEnum from-          ito = fromEnum to-          from' = is !! ifrom --- is-          to' = is !! ito ------- is-          deleteIndexFromTo ks =-            fmap snd $ filter (\(idx, _) -> idx /= ifrom && idx /= ito) $ zip [0 ..] ks-          deleteIndexFrom ks =-            fmap snd $ filter (\(idx, _) -> idx /= ifrom) $ zip [0 ..] ks--      when (index == 0) $ do-        branchSts <- get @[Int]-        tellSeq $ map (uncurry C.Constraint) $ zip (deleteIndexFrom branchSts) (deleteIndexFrom is)--      tellSeq $-        C.Constraint from' to'-          : zipWith C.Constraint (deleteIndexFromTo is) (deleteIndexFromTo os)-  , \((is, i), lb) ->-      gets (IntMap.lookup @[Int] i) >>= \case-        Just _ -> throwError @(ProtocolError r bst) (DefLabelMultTimes lb)-        Nothing -> modify (IntMap.insert i is)-  , \(is, _) -> do-      put is-      pure (restoreWrapper @[Int])-  , \_ -> pure ()-  , \((xs, i), gt) -> do-      gets (IntMap.lookup i) >>= \case-        Nothing -> throwError @(ProtocolError r bst) (LabelUndefined gt)-        Just ls -> tellSeq $ zipWith C.Constraint xs ls-  , \(xs) -> tellSeq $ zipWith C.Constraint xs (cycle [-1])-  )--replXTraverse :: (Monad m) => C.SubMap -> XTraverse m (GenConst r) (GenConst r) r bst-replXTraverse sbm =-  ( \(((a, b), (from, to), i), _) ->-      pure ((replaceList sbm a, replaceList sbm b), (from, to), i)-  , \((xs, i), _) -> pure (replaceList sbm xs, i)-  , \(a, _) -> pure (replaceList sbm a, id)-  , \_ -> pure ()-  , \((xs, i), _) -> pure (replaceList sbm xs, i)-  , \xs -> pure (replaceList sbm xs)-  )--collectBranchDynValXFold :: (Has (State (Set Int)) sig m, Enum r) => XFold m (GenConst r) r bst-collectBranchDynValXFold =-  ( \_ -> pure ()-  , \_ -> pure ()-  , \(ls, (r, _)) -> do-      let ls' = map snd $ filter (\(i, _) -> i /= fromEnum r) $ zip [0 ..] ls-      modify (`Set.union` (Set.fromList ls'))-      pure id-  , \_ -> pure ()-  , \_ -> pure ()-  , \_ -> pure ()-  )--genT-  :: forall bst sig m-   . (Has (Reader (Set Int) :+: State bst) sig m)-  => (bst -> Int -> T bst) -> Int -> m (T bst)-genT fun i = do-  dynSet <- ask @(Set Int)-  if i == -1-    then pure (TEnd)-    else-      if Set.member i dynSet-        then do-          bst <- get-          pure (fun bst i)-        else pure $ TNum i--genMsgTXTraverse-  :: forall r bst sig m-   . (Has (Reader (Set Int) :+: State bst) sig m, Enum r, Eq r, Bounded r)-  => XTraverse m (GenConst r) (MsgT r bst) r bst-genMsgTXTraverse =-  ( \(((is, _), (from, to), vi), _) -> do-      is' <- forM (zip rRange is) $-        \(key, i) -> genT @bst (\bst1 i1 -> if key == from then BstList i1 bst1 else TAny i1) i-      pure (is', (from, to), vi)-  , \((ls, idx), _) -> do-      ls' <- mapM (genT (const TAny)) ls-      pure (ls', idx)-  , \(ls, (r, _)) -> do-      ls' <- mapM (\(idx, v) -> genT (if idx == fromEnum r then const TNum else (const TAny)) v) (zip [0 ..] ls)-      pure (ls', restoreWrapper @bst)-  , \(_, (bst, _)) -> put bst-  , \((is, i), _) -> do-      is' <- mapM (genT @bst (const TAny)) is-      pure (is', i)-  , \ls -> pure $ fmap (const TEnd) ls-  )--getFirstXV :: Protocol (MsgT r bst) r bst -> [T bst]-getFirstXV = \case-  Msg (xv, _, _) _ _ _ _ :> _ -> xv-  Label (xv, _) _ :> _ -> xv-  Branch xv _ _ -> xv-  Goto (xv, _) _ -> xv-  Terminal xv -> xv--genMsgT1XTraverse :: (Monad m, Enum r) => XTraverse m (MsgT r bst) (MsgT1 r bst) r bst-genMsgT1XTraverse =-  ( \((is, (from, to), i), (_, _, _, _, prot)) -> do-      let os = getFirstXV prot-          from' = fromEnum from-          to' = fromEnum to-      pure ((is !! from', os !! from', os !! to'), (from, to), i)-  , \(a, _) -> pure a-  , \(a, _) -> pure (a, id)-  , \(a, _) -> pure a-  , \(a, _) -> pure a-  , \a -> pure a-  )--data PipleResult r bst = PipleResult-  { msgT :: Protocol (MsgT r bst) r bst-  , msgT1 :: Protocol (MsgT1 r bst) r bst-  , dnySet :: Set Int-  , stBound :: (Int, Int)-  }--reRank :: Set Int -> Int -> IntMap Int-reRank branchValSet maxSize =-  let allSet = Set.insert 0 branchValSet-      restList = [i | i <- [0 .. maxSize], i `Set.notMember` allSet]-   in IntMap.fromList $ zip (Set.toList allSet ++ restList) [0 ..]--piple'-  :: forall r bst sig m-   . ( Has (Error (ProtocolError r bst)) sig m-     , Enum r-     , Bounded r-     , Eq r-     , Ord r-     )-  => (Tracer r bst -> m ())-  -> Protocol Creat r bst-  -> m (PipleResult r bst)-piple' trace prot0 = do-  trace (TracerProtocolCreat prot0)-  (brSet, (maxSzie, (_, idxProt))) <--    runState @(Set Int) Set.empty-      . runState @Int 0-      . runState @Index (Index 100)-      $ (xtraverse addIdxXTraverse prot0)-  trace (TracerProtocolIdx idxProt)-  trace (TracerReRank (reRank brSet maxSzie))-  idxProt1 <- xtraverse (reRankXTraverse (reRank brSet maxSzie)) idxProt-  trace (TracerProtocolIdx idxProt1)-  prot1 <- xtraverse addNumsXTraverse idxProt1-  trace (TracerProtocolAddNum prot1)-  prot2 <- xtraverse toGenConstrXTraverse prot1-  trace (TracerProtocolGenConst prot2)-  void-    . runState @(Map r CurrSt) (Map.fromList $ zip (rRange @r) (cycle [Decide]))-    . runState @r undefined-    $ xfold checkProtXFold prot2-  (constraintList, _) <--    runWriter @(Seq C.Constraint)-      . runState @(IntMap [Int]) (IntMap.empty)-      . runState @[Int] undefined-      $ xfold genConstrXFold prot2-  trace (TracerConstraints constraintList)-  let (sbm, stBound) = compressSubMap $ C.constrToSubMap $ toList constraintList-  trace (TracerSubMap sbm)-  prot3 <- xtraverse (replXTraverse sbm) prot2-  trace (TracerProtocolGenConstN prot3)-  dnys <- fst <$> runState @((Set Int)) (Set.empty) (xfold collectBranchDynValXFold prot3)-  trace (TracerCollectBranchDynVal dnys)-  prot4 <--    fmap snd-      . runReader @(Set Int) dnys-      . runState @bst undefined-      $ (xtraverse genMsgTXTraverse prot3)-  trace (TracerProtocolMsgT prot4)-  prot5 <- xtraverse genMsgT1XTraverse prot4-  trace (TracerProtocolMsgT1 prot5)-  pure (PipleResult prot4 prot5 dnys stBound)--piple-  :: forall r bst-   . (Enum r, Bounded r, Eq r, Ord r)-  => Protocol Creat r bst-  -> Either-      (ProtocolError r bst)-      (PipleResult r bst)-piple protocol =-  run $ runError @(ProtocolError r bst) $ (piple' (const (pure ())) protocol)--pipleWithTracer-  :: forall r bst-   . (Enum r, Bounded r, Eq r, Ord r)-  => Protocol Creat r bst-  -> ( Seq (Tracer r bst)-     , Either-        (ProtocolError r bst)-        (PipleResult r bst)-     )-pipleWithTracer protocol =-  run-    . runWriter @(Seq (Tracer r bst))-    . runError @(ProtocolError r bst)-    $ (piple' (\w -> tell @(Seq (Tracer r bst)) (Seq.singleton w)) protocol)--genDocXFold-  :: forall r bst ann sig m-   . ( Has (Writer [Doc ann]) sig m-     , Show r-     , Show bst-     )-  => String -> String -> XFold m (MsgT1 r bst) r bst-genDocXFold rName protName =-  ( \( ((sendStart, sendEnd, recEnd), (from, to), _)-      , (cons, args, _, _, _)-      ) -> do-        tell @[Doc ann]-          [ pretty cons-              <+> "::"-              <+> pretty (L.intercalate "->" args)-              <+> (if null args then emptyDoc else "->")-              <+> "Msg"-              <+> pretty rName-              <+> pretty (protName <> "St")-              <+> parens (pretty $ show sendStart)-              <+> (pretty $ '\'' : show (from, sendEnd))-              <+> (pretty $ '\'' : show (to, recEnd))-          ]-  , \_ -> pure ()-  , \_ -> pure (id)-  , \_ -> pure ()-  , \_ -> pure ()-  , \_ -> pure ()-  )--genDoc :: forall r bst ann. (Show r, Show bst) => String -> String -> Protocol (MsgT1 r bst) r bst -> [Doc ann]-genDoc rName protName prot =-  fst $ run $ runWriter @[Doc ann] (xfold (genDocXFold @r @bst @ann rName protName) prot)

@@ -17,11 +17,7 @@ import Control.Effect.State import Control.Effect.Writer import Control.Monad (when)-import Data.IntMap (IntMap) import qualified Data.List as L-import Data.Sequence (Seq)-import Data.Set (Set)-import qualified TypedSession.State.Constraint as C import TypedSession.State.Type import TypedSession.State.Utils @@ -140,18 +136,6 @@       tell [header]       (xfold (renderXFold sfe xst) prot) -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)-  | TracerCollectBranchDynVal (Set Int)-  | TracerProtocolMsgT (Protocol (MsgT r bst) r bst)-  | TracerProtocolMsgT1 (Protocol (MsgT1 r bst) r bst)  traceWrapper :: String -> String -> String traceWrapper desc st =@@ -212,6 +196,7 @@     TracerConstraints p -> traceWrapper "Constrains" $ show p     TracerSubMap p -> traceWrapper "SubMap" $ show p     TracerProtocolGenConstN p -> traceWrapper "GenConstN" $ show p+    TracerVerifyResult m -> traceWrapper "VerifyResult Map" $ show m     TracerCollectBranchDynVal dvs -> traceWrapper "CollectBranchDynVal" $ show dvs     TracerProtocolMsgT p -> traceWrapper "MsgT" $ show p     TracerProtocolMsgT1 p -> traceWrapper "MsgT1" $ show p

@@ -17,9 +17,13 @@ module TypedSession.State.Type where  import Control.Monad+import Data.IntMap (IntMap) import Data.Kind (Constraint, Type)+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@@ -132,6 +136,7 @@   | UndecideStateCanNotStartBranch [BranchSt (GenConst r) r bst]   | TerminalNeedAllRoleDecide String   | BranchAtLeastOneBranch+  | AStateOnlyBeUsedForTheSamePair  instance (Show r, Show bst) => Show (ProtocolError r bst) where   show = \case@@ -148,6 +153,24 @@     UndecideStateCanNotStartBranch brs -> "Undecide State can't start branch! " <> show brs     TerminalNeedAllRoleDecide msgName -> "Msg " <> msgName <> ", Terminal need all role decide!"     BranchAtLeastOneBranch -> "Branch at least one branch!"+    AStateOnlyBeUsedForTheSamePair -> "A state can only be used for the same pair of communicators." ++ internalError++internalError :: String+internalError = "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)  ------------------------ 

@@ -74,4 +74,4 @@ replaceList sbm ls = fmap (\k -> fromMaybe k $ IntMap.lookup k sbm) ls  replaceVal :: IntMap Int -> Int -> Int-replaceVal sbm k = fromMaybe (error "np") $ IntMap.lookup k sbm+replaceVal sbm k = fromMaybe (error internalError) $ IntMap.lookup k sbm

@@ -5,9 +5,8 @@ module Main (main) where  import Text.RawString.QQ (r)-import TypedSession.State.GenDoc (genGraph) import TypedSession.State.Parser (runProtocolParser)-import TypedSession.State.Piple (pipleWithTracer)+import TypedSession.State.Pipeline (genGraph, pipleWithTracer) import TypedSession.State.Render (StrFillEnv (StrFillEnv))  main :: IO ()@@ -125,6 +124,8 @@ --   Msg <(([1,1,2],[2,-1,2]),(Client,Server),0)> Stop [] Client Server --   Msg <(([2,-1,2],[-1,-1,-1]),(Client,Counter),1)> CStop [] Client Counter --   Terminal [-1,-1,-1]+-- ,--------------------VerifyResult Map-----------------+-- fromList [(1,(Client,Server)),(2,(Client,Counter)),(3,(Server,Client))] -- ,--------------------CollectBranchDynVal----------------- -- fromList [1,2] -- ,--------------------MsgT-----------------@@ -451,6 +452,8 @@ --   Msg <(([2,2,1],[1,0,1]),(Seller,Buyer),0)> NoBook [] Seller Buyer --   Msg <(([1,0,1],[0,0,1]),(Buyer,Buyer2),1)> SellerNoBook [] Buyer Buyer2 --   Goto ([0,0,1],0) 0+-- ,--------------------VerifyResult Map-----------------+-- fromList [(0,(Buyer,Seller)),(1,(Buyer,Buyer2)),(2,(Seller,Buyer)),(5,(Buyer,Seller)),(6,(Buyer2,Buyer)),(9,(Buyer,Buyer2)),(10,(Seller,Buyer)),(11,(Seller,Buyer))] -- ,--------------------CollectBranchDynVal----------------- -- fromList [1,2,5,6,9] -- ,--------------------MsgT-----------------

@@ -20,7 +20,7 @@ -- PVP summary:     +-+------- breaking API changes --                  | | +----- non-breaking API additions --                  | | | +--- code changes with no API change-version:            0.1.0.2+version:            0.2.0.0  -- A short (one-line) description of the package. synopsis: Automatically generate status for typed-session.@@ -60,9 +60,7 @@      -- Modules exported by the library.     exposed-modules:  TypedSession.State.Constraint-                    , TypedSession.State.Piple-                    , TypedSession.State.Pattern-                    , TypedSession.State.GenDoc+                    , TypedSession.State.Pipeline                     , TypedSession.State.Type                     , TypedSession.State.Utils                     , TypedSession.State.Render