typed-session-state-algorithm 0.4.2.3 → 0.5.0.0
raw patch · 6 files changed
+82/−76 lines, 6 files
Files
- src/TypedSession/State/Pipeline.hs +22/−13
- src/TypedSession/State/Render.hs +1/−1
- src/TypedSession/State/Type.hs +2/−2
- src/TypedSession/State/Utils.hs +9/−12
- test/Main.hs +47/−47
- typed-session-state-algorithm.cabal +1/−1
src/TypedSession/State/Pipeline.hs view
@@ -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
src/TypedSession/State/Render.hs view
@@ -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
src/TypedSession/State/Type.hs view
@@ -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
src/TypedSession/State/Utils.hs view
@@ -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
test/Main.hs view
@@ -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) -}
typed-session-state-algorithm.cabal view
@@ -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.