diff --git a/src/TypedSession/State/Pipeline.hs b/src/TypedSession/State/Pipeline.hs --- a/src/TypedSession/State/Pipeline.hs +++ b/src/TypedSession/State/Pipeline.hs @@ -7,6 +7,7 @@ {-# LANGUAGE LambdaCase #-} {-# LANGUAGE MultiWayIf #-} {-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE NumericUnderscores #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE RankNTypes #-} @@ -205,15 +206,23 @@ , \(xs) -> tellSeq $ zipWith C.Constraint xs (cycle [-1]) ) -replXTraverse :: (Monad m) => C.SubMap -> XTraverse m (GenConst r) (GenConst r) r bst +replXTraverse :: (Has (State (Set Int)) sig 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) + ( \(((a, b), (from, to), i), _) -> do + a' <- replaceList sbm a + b' <- replaceList sbm b + pure ((a', b'), (from, to), i) + , \((xs, i), _) -> do + xs' <- replaceList sbm xs + pure (xs', i) + , \(a, _) -> do + a' <- replaceList sbm a + pure (a', id) , \_ -> pure () - , \((xs, i), _) -> pure (replaceList sbm xs, i) - , \xs -> pure (replaceList sbm xs) + , \((xs, i), _) -> do + xs' <- replaceList sbm xs + pure (xs', i) + , \xs -> replaceList sbm xs ) verifyProtXFold @@ -322,7 +331,7 @@ { msgT :: Protocol (MsgT r bst) r bst , msgT1 :: Protocol (MsgT1 r bst) r bst , dnySet :: Set Int - , stBound :: (Int, Int) + , stList :: [Int] , branchResultTypeInfo :: [(String, [(bst, [[String]], T bst)])] , branchFunList :: [(r, String, T bst)] , allMsgBATypes :: [(String, [T bst], [T bst])] @@ -374,7 +383,7 @@ idxProt <- fmap (snd . snd) . runState @Int 0 - . runState @Index (Index 100) + . runState @Index (Index 1_000_000) $ (xtraverse addIdxXTraverse prot0) trace (TracerProtocolIdx idxProt) prot1 <- xtraverse addNumsXTraverse idxProt @@ -391,9 +400,9 @@ . 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 + let sbm = C.constrToSubMap $ toList constraintList + (stSet, prot3) <- runState (Set.singleton (-1)) $ xtraverse (replXTraverse sbm) prot2 + trace (TracerSubMapAndStList (sbm, stSet)) trace (TracerProtocolGenConstN prot3) verifyResult <- fst <$> runState @(IntMap (r, r)) (IntMap.empty) (xfold verifyProtXFold prot3) trace (TracerVerifyResult verifyResult) @@ -414,7 +423,7 @@ . runState @(Map String [(bst, [[String]], T bst)]) Map.empty $ xfold genBranchResultTIXFold prot5 trace (TracerBranchResultTI bfl branchTIMap) - pure (PipeResult prot4 prot5 dnys stBound (Map.toList branchTIMap) bfl allMsgBAs) + pure (PipeResult prot4 prot5 dnys (Set.toList stSet) (Map.toList branchTIMap) bfl allMsgBAs) pipe :: forall r bst diff --git a/src/TypedSession/State/Render.hs b/src/TypedSession/State/Render.hs --- a/src/TypedSession/State/Render.hs +++ b/src/TypedSession/State/Render.hs @@ -66,6 +66,7 @@ => XTraverse m (MsgT r bst) RenderProt r bst render1XTraverse = ( \((ts, (from, to), idx), (constr, args, _, _, _)) -> do + when (idx == 0) (modify @Int (+ 1)) nst <- mkLeftStr (constr <> " [" <> L.intercalate "," (fmap (L.intercalate " ") args) <> "]") ts' <- for (zip (rRange @r) ts) $ \(r, t) -> do let sht = parensWarapper $ show t @@ -76,7 +77,6 @@ | otherwise -> " " <> sht tell $ Max $ RV (length sht') pure sht' - when (idx == 0) (modify @Int (+ 1)) pure (nst, ts') , \((ts, i), _) -> pure ("Label " <> show i, mkStrs ts) , \(ts, (r, st, _)) -> do diff --git a/src/TypedSession/State/Type.hs b/src/TypedSession/State/Type.hs --- a/src/TypedSession/State/Type.hs +++ b/src/TypedSession/State/Type.hs @@ -169,7 +169,7 @@ | TracerProtocolAddNum (Protocol AddNums r bst) | TracerProtocolGenConst (Protocol (GenConst r) r bst) | TracerConstraints (Seq C.Constraint) - | TracerSubMap C.SubMap + | TracerSubMapAndStList (C.SubMap, Set Int) | TracerProtocolGenConstN (Protocol (GenConst r) r bst) | TracerVerifyResult (IntMap (r, r)) | TracerCollectBranchDynVal (Set Int) @@ -189,7 +189,7 @@ TracerProtocolAddNum p -> traceWrapper "AddNum" $ show p TracerProtocolGenConst p -> traceWrapper "GenConst" $ show p TracerConstraints p -> traceWrapper "Constrains" $ show p - TracerSubMap p -> traceWrapper "SubMap" $ show p + TracerSubMapAndStList p -> traceWrapper "SubMapAndStList" $ show p TracerProtocolGenConstN p -> traceWrapper "GenConstN" $ show p TracerVerifyResult m -> traceWrapper "VerifyResult Map" $ show m TracerCollectBranchDynVal dvs -> traceWrapper "CollectBranchDynVal" $ show dvs diff --git a/src/TypedSession/State/Utils.hs b/src/TypedSession/State/Utils.hs --- a/src/TypedSession/State/Utils.hs +++ b/src/TypedSession/State/Utils.hs @@ -26,6 +26,9 @@ import Data.Maybe (fromJust, fromMaybe) import Data.Sequence (Seq) import qualified Data.Sequence as Seq +import Data.Set (Set) +import qualified Data.Set as Set +import Data.Traversable (for) import qualified TypedSession.State.Constraint as C import TypedSession.State.Type import Prelude hiding (traverse) @@ -60,18 +63,12 @@ tellSeq :: (Has (Writer (Seq a)) sig m) => [a] -> m () tellSeq ls = tell (Seq.fromList ls) -compressSubMap :: C.SubMap -> (C.SubMap, (Int, Int)) -compressSubMap sbm' = - let (minKey, maxKey) = (fst $ IntMap.findMin sbm', fst $ IntMap.findMax sbm') - list = [minKey .. maxKey] - (keys, vals) = (list, fmap (\k -> fromMaybe k $ IntMap.lookup k sbm') list) - minVal = minimum vals - tmap = IntMap.fromList $ zip (L.nub $ L.sort vals) [minVal, minVal + 1 ..] - vals' = fmap (\k -> fromJust $ IntMap.lookup k tmap) vals - in (IntMap.fromList $ zip keys vals', (-1, maximum vals')) - -replaceList :: C.SubMap -> [Int] -> [Int] -replaceList sbm ls = fmap (\k -> fromMaybe k $ IntMap.lookup k sbm) ls +replaceList :: (Has (State (Set Int)) sig m) => C.SubMap -> [Int] -> m [Int] +replaceList sbm ls = do + for ls $ \k -> do + let newVal = fromMaybe k $ IntMap.lookup k sbm + modify (Set.insert newVal) + pure newVal replaceVal :: IntMap Int -> Int -> Int replaceVal sbm k = fromMaybe (error internalError) $ IntMap.lookup k sbm diff --git a/test/Main.hs b/test/Main.hs --- a/test/Main.hs +++ b/test/Main.hs @@ -45,18 +45,18 @@ {- >>> error r1 ----------------------------------------------Client--------------Server--------------Counter------------- -Label 0 (S0) (S1 s) (S2 s) - [Branch Client ContinueOrFinish] (S0) (S1 s) (S2 s) - * BranchSt_Continue [] - AddOne [Maybe Int,Int,Either String Int] Send (S2 Continue) (S1 s) Recv (S2 s) - Ping [Int,Int,Int] Send (S1 Continue) Recv (S1 s) (S2 s) - Pong [] Recv (S3) Send (S3) (S2 s) - Goto 0 (S0) (S1 s) (S2 s) - * BranchSt_Finish [] - Stop [] Send (S1 Finish) Recv (S1 s) (S2 s) - CStop [] Send (S2 Finish) (End) Recv (S2 s) - Terminal (End) (End) (End) +-----------------------------------------------Client--------------Server--------------Counter------------- +Label 0 (S0) (S1 s) (S2 s) + [Branch Client ContinueOrFinish] (S0) (S1 s) (S2 s) + * BranchSt_Continue [] + AddOne [Maybe Int,Int,Either String Int] Send (S2 Continue) (S1 s) Recv (S2 s) + Ping [Int,Int,Int] Send (S1 Continue) Recv (S1 s) (S2 s) + Pong [] Recv (S9) Send (S9) (S2 s) + Goto 0 (S0) (S1 s) (S2 s) + * BranchSt_Finish [] + Stop [] Send (S1 Finish) Recv (S1 s) (S2 s) + CStop [] Send (S2 Finish) (End) Recv (S2 s) + Terminal (End) (End) (End) -} @@ -131,40 +131,40 @@ {- >>> error r2 ---------------------------------------------Buyer-----------------Seller----------------Buyer2---------------- -Label 0 (S0) (S0) (S1 s) - Title [String] Send (S0) Recv (S0) (S1 s) - [Branch Seller FindBookResult] (S2 s) (S3) (S1 s) - * BranchSt_Found [] - Price [Int] Recv (S2 s) Send (S2 Found) (S1 s) - [Branch Buyer OneOrTwo] (S4) (S5 s) (S1 s) - * BranchSt_Two [] - PriceToBuyer2 [Int] Send (S1 Two) (S5 s) Recv (S1 s) - [Branch Buyer2 SupportOrNotSupport] (S6 s) (S5 s) (S7) - * BranchSt_NotSupport [] - NotSupport1 [] Recv (S6 s) (S5 s) Send (S6 NotSupport) - TwoNotBuy [] Send (S5 NotSupport) Recv (S5 s) (S1 s) - Goto 0 (S0) (S0) (S1 s) - * BranchSt_Support [] - SupportVal [Int] Recv (S6 s) (S5 s) Send (S6 Support) - [Branch Buyer EnoughOrNotEnough] (S8) (S5 s) (S9 s) - * BranchSt_Enough [] - TwoAccept [] Send (S5 Enough) Recv (S5 s) (S9 s) - TwoDate [Int] Recv (S10) Send (S10) (S9 s) - TwoSuccess [Int] Send (S9 Enough) (S0) Recv (S9 s) - Goto 0 (S0) (S0) (S1 s) - * BranchSt_NotEnough [] - TwoNotBuy1 [] Send (S5 NotEnough) Recv (S5 s) (S9 s) - TwoFailed [] Send (S9 NotEnough) (End) Recv (S9 s) - Terminal (End) (End) (End) - * BranchSt_One [] - OneAccept [] Send (S5 One) Recv (S5 s) (S1 s) - OneDate [Int] Recv (S11) Send (S11) (S1 s) - OneSuccess [Int] Send (S1 One) (S0) Recv (S1 s) - Goto 0 (S0) (S0) (S1 s) - * BranchSt_NotFound [] - NoBook [] Recv (S2 s) Send (S2 NotFound) (S1 s) - SellerNoBook [] Send (S1 NotFound) (S0) Recv (S1 s) - Goto 0 (S0) (S0) (S1 s) +--------------------------------------------Buyer------------------Seller-----------------Buyer2----------------- +Label 0 (S0) (S0) (S2 s) + Title [String] Send (S0) Recv (S0) (S2 s) + [Branch Seller FindBookResult] (S3 s) (S4) (S2 s) + * BranchSt_Found [] + Price [Int] Recv (S3 s) Send (S3 Found) (S2 s) + [Branch Buyer OneOrTwo] (S9) (S10 s) (S2 s) + * BranchSt_Two [] + PriceToBuyer2 [Int] Send (S2 Two) (S10 s) Recv (S2 s) + [Branch Buyer2 SupportOrNotSupport] (S15 s) (S10 s) (S17) + * BranchSt_NotSupport [] + NotSupport1 [] Recv (S15 s) (S10 s) Send (S15 NotSupport) + TwoNotBuy [] Send (S10 NotSupport) Recv (S10 s) (S2 s) + Goto 0 (S0) (S0) (S2 s) + * BranchSt_Support [] + SupportVal [Int] Recv (S15 s) (S10 s) Send (S15 Support) + [Branch Buyer EnoughOrNotEnough] (S30) (S10 s) (S32 s) + * BranchSt_Enough [] + TwoAccept [] Send (S10 Enough) Recv (S10 s) (S32 s) + TwoDate [Int] Recv (S36) Send (S36) (S32 s) + TwoSuccess [Int] Send (S32 Enough) (S0) Recv (S32 s) + Goto 0 (S0) (S0) (S2 s) + * BranchSt_NotEnough [] + TwoNotBuy1 [] Send (S10 NotEnough) Recv (S10 s) (S32 s) + TwoFailed [] Send (S32 NotEnough) (End) Recv (S32 s) + Terminal (End) (End) (End) + * BranchSt_One [] + OneAccept [] Send (S10 One) Recv (S10 s) (S2 s) + OneDate [Int] Recv (S57) Send (S57) (S2 s) + OneSuccess [Int] Send (S2 One) (S0) Recv (S2 s) + Goto 0 (S0) (S0) (S2 s) + * BranchSt_NotFound [] + NoBook [] Recv (S3 s) Send (S3 NotFound) (S2 s) + SellerNoBook [] Send (S2 NotFound) (S0) Recv (S2 s) + Goto 0 (S0) (S0) (S2 s) -} diff --git a/typed-session-state-algorithm.cabal b/typed-session-state-algorithm.cabal --- a/typed-session-state-algorithm.cabal +++ b/typed-session-state-algorithm.cabal @@ -20,7 +20,7 @@ -- PVP summary: +-+------- breaking API changes -- | | +----- non-breaking API additions -- | | | +--- code changes with no API change -version: 0.4.2.3 +version: 0.5.0.0 -- A short (one-line) description of the package. synopsis: Automatically generate status for typed-session.