typed-session-state-algorithm 0.3.0.0 → 0.3.0.1
raw patch · 5 files changed
+179/−228 lines, 5 files
Files
- src/TypedSession/State/Pipeline.hs +7/−45
- src/TypedSession/State/Render.hs +126/−140
- src/TypedSession/State/Utils.hs +3/−0
- test/Main.hs +42/−42
- typed-session-state-algorithm.cabal +1/−1
src/TypedSession/State/Pipeline.hs view
@@ -34,21 +34,17 @@ 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@@ -306,7 +302,7 @@ , \a -> pure a ) -data PipleResult r bst = PipleResult+data PipeResult r bst = PipeResult { msgT :: Protocol (MsgT r bst) r bst , msgT1 :: Protocol (MsgT1 r bst) r bst , dnySet :: Set Int@@ -329,7 +325,7 @@ ) => (Tracer r bst -> m ()) -> Protocol Creat r bst- -> m (PipleResult r bst)+ -> m (PipeResult r bst) pipe' trace prot0 = do trace (TracerProtocolCreat prot0) (brSet, (maxSzie, (_, idxProt))) <-@@ -371,7 +367,7 @@ trace (TracerProtocolMsgT prot4) prot5 <- xtraverse genMsgT1XTraverse prot4 trace (TracerProtocolMsgT1 prot5)- pure (PipleResult prot4 prot5 dnys stBound)+ pure (PipeResult prot4 prot5 dnys stBound) pipe :: forall r bst@@ -379,7 +375,7 @@ => Protocol Creat r bst -> Either (ProtocolError r bst)- (PipleResult r bst)+ (PipeResult r bst) pipe protocol = run $ runError @(ProtocolError r bst) $ (pipe' (const (pure ())) protocol) @@ -390,7 +386,7 @@ -> ( Seq (Tracer r bst) , Either (ProtocolError r bst)- (PipleResult r bst)+ (PipeResult r bst) ) pipeWithTracer protocol = run@@ -398,39 +394,5 @@ . runError @(ProtocolError r bst) $ (pipe' (\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+genGraph :: (Enum r, Bounded r, Show bst, Ord r, Show r) => PipeResult r bst -> String+genGraph PipeResult{msgT} = runRender msgT
src/TypedSession/State/Render.hs view
@@ -1,178 +1,164 @@ {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE MultiWayIf #-} {-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE NoFieldSelectors #-} module TypedSession.State.Render where import Control.Algebra ((:+:))+import Control.Carrier.Reader (runReader) import Control.Carrier.State.Strict (runState) import Control.Carrier.Writer.Strict (runWriter)+import Control.Effect.Reader import Control.Effect.State import Control.Effect.Writer import Control.Monad (when)-import qualified Data.List as L+import Data.Semigroup (Max (..))+import Data.Traversable (for) import TypedSession.State.Type import TypedSession.State.Utils--data StringFill- = CenterFill Int Char String- | LeftAlign Int Char String- deriving (Show)--runCenterFill :: String -> StringFill -> String-runCenterFill startSt (CenterFill centerPoint c st) =- let stlen = length st- hlen = stlen `div` 2- rplen = (centerPoint - length startSt) - if odd stlen then hlen + 1 else hlen- rpSt = replicate rplen c- in startSt ++ rpSt ++ st-runCenterFill startSt v@(LeftAlign leftAlignPoint c st) =- if leftAlignPoint < length startSt- then error $ "np: " ++ startSt ++ " " ++ show v- else- let repLen = leftAlignPoint - length startSt - 1- fillSt = replicate repLen c- in startSt ++ fillSt ++ st--getPoint :: StringFill -> Int-getPoint = \case- CenterFill cp _ _ -> cp- LeftAlign lp _ _ -> lp--runCenterFills :: [StringFill] -> String-runCenterFills ls =- let ls' = L.sortOn getPoint ls- in foldl' runCenterFill "" ls'+import qualified Data.List as L --- width :: Int--- width = 30+data RenderProt --- leftWidth :: Int--- leftWidth = 20+type instance XMsg RenderProt = (String, [String])+type instance XLabel RenderProt = (String, [String])+type instance XBranch RenderProt = (String, [String])+type instance XBranchSt RenderProt = ()+type instance XGoto RenderProt = (String, [String])+type instance XTerminal RenderProt = (String, [String]) -data StrFillEnv = StrFillEnv- { width :: Int- , leftWidth :: Int- }- deriving (Show)+parensWarapper :: String -> String+parensWarapper st = "{" <> st <> "}" -defaultStrFilEnv :: StrFillEnv-defaultStrFilEnv = StrFillEnv 30 20+newtype LV = LV Int+ deriving (Show, Eq, Ord, Num, Bounded) -reSt :: StrFillEnv -> String -> String-reSt StrFillEnv{width} st =- let st' = words st- in case st' of- [] -> error "np"- (x : _) ->- let lv = width - 6- in if length x >= lv- then take (lv - 2) x <> ".."- else x+newtype RV = RV Int+ deriving (Show, Eq, Ord, Num, Bounded) ----------------------------------------------type XStringFill eta r bst =- ( XMsg eta -> ([StringFill], Bool)- , XLabel eta -> [StringFill]- , XBranch eta -> [StringFill]- , XBranchSt eta -> [StringFill]- , XGoto eta -> [StringFill]- , XTerminal eta -> [StringFill]- )+mkLeftStr :: (Has (State Int :+: Writer (Max LV)) sig m) => String -> m String+mkLeftStr str = do+ indent <- get @Int+ let str' = replicate (indent * 2 + 3) ' ' <> str+ tell (Max $ LV $ length str')+ pure str' -renderXFold- :: forall r eta bst sig m- . ( Has (Writer [[StringFill]] :+: State Int) sig m- , ForallX Show eta+render1XTraverse+ :: forall r bst sig m+ . ( Has (State Int :+: Writer (Max LV) :+: Writer (Max RV)) sig m+ , Show bst , Enum r , Bounded r+ , Eq r+ , Ord r , Show r- , Show bst )- => StrFillEnv -> XStringFill eta r bst -> XFold m eta r bst-renderXFold sfe (xmsg, xlabel, xbranch, _xbranchst, xgoto, xterminal) =- ( \(xv, (con, _, _, _, _)) -> do- indentVal <- get @Int- let va = [LeftAlign (indentVal * 2 + 3) ' ' (reSt sfe con)]- (xv', isFirst) = xmsg xv- when isFirst (modify @Int (+ 1))- tell [va ++ xv']- , \(xv, i) -> tell [[LeftAlign 1 ' ' ("LABEL " ++ show i)] ++ xlabel xv]- , \(xv, (r, _)) -> do- indentVal <- get @Int- modify @Int (+ 1)- tell [[LeftAlign (indentVal * 2 + 3) ' ' ("[Branch " ++ show r ++ "]")] ++ xbranch xv]- pure (restoreWrapper @Int)- , \(_, (_, _)) -> pure ()- , \(xv, i) -> do- indentVal <- get @Int- tell [[LeftAlign (indentVal * 2 + 3) ' ' ("Goto " ++ show i)] ++ xgoto xv]- , \xv -> do- indentVal <- get @Int- tell [[LeftAlign (indentVal * 2 + 3) ' ' "Terminal"] ++ xterminal xv]+ => XTraverse m (MsgT r bst) RenderProt r bst+render1XTraverse =+ ( \((ts, (from, to), idx), (constr, args, _, _, _)) -> do+ nst <- mkLeftStr (constr <> " [" <> L.intercalate "," args <> "]")+ when (idx == 0) (modify @Int (+ 1))+ ts' <- for (zip (rRange @r) ts) $ \(r, t) -> do+ let sht =+ if+ | idx == 0 && r == from -> parensWarapper $ show t+ | otherwise -> show t+ sht' =+ if+ | r == from ->+ if+ | from > to -> "<- " <> sht+ | otherwise -> sht <> " ->"+ | r == to ->+ if+ | from > to -> sht <> " <-"+ | otherwise -> "-> " <> sht+ | otherwise -> sht+ tell $ Max $ RV (length sht')+ pure sht'+ pure (nst, ts')+ , \((ts, i), _) -> pure ("Label " <> show i, map show ts)+ , \(ts, (r, _)) -> do+ nst <- mkLeftStr $ "[Branch " <> show r <> "]"+ pure ((nst, map show ts), restoreWrapper @Int)+ , \_ -> pure ()+ , \((ts, i), _) -> do+ nst <- mkLeftStr $ "Goto " <> show i+ pure (nst, map show ts)+ , \ts -> do+ nst <- mkLeftStr "Terminal"+ pure (nst, map show ts) ) -runRender- :: forall r eta bst- . (ForallX Show eta, Show bst, Enum r, Bounded r, Show r)- => StrFillEnv -> XStringFill eta r bst -> Protocol eta r bst -> String-runRender sfe@(StrFillEnv{width, leftWidth}) xst prot =- unlines- . fmap runCenterFills- . fst- . run- . runWriter @[[StringFill]]- . runState @Int 0- $ do- let header =- [CenterFill ((fromEnum r + 1) * width + leftWidth) '-' (show r) | r <- rRange @r]- tell [header]- (xfold (renderXFold sfe xst) prot)--foo :: (Ord a) => a -> a -> [Char] -> a -> [Char]-foo from to str i =- if- | i == from ->- if from > to- then "<-" ++ str- else str ++ "->"- | i == to ->- if from > to- then str ++ "<-"- else "->" ++ str- | otherwise -> str--rtops :: (Enum r) => StrFillEnv -> r -> Int-rtops StrFillEnv{width, leftWidth} = ((+ leftWidth) . (width *) . (+ 1) . fromEnum)+fillStr :: Char -> Int -> String -> String+fillStr c i st =+ let len = length st+ in case compare len i of+ EQ -> st+ LT -> st <> replicate (i - len) c+ GT -> error "np" -rRange :: forall r. (Enum r, Bounded r) => [r]-rRange = [minBound @r .. maxBound]+mkLine+ :: forall r sig m+ . ( Has (Reader (LV, RV) :+: Writer [String]) sig m+ , Enum r+ , Bounded r+ )+ => (String, [String]) -> m ()+mkLine (ls, rs) = do+ (LV maxLv, RV maxRv) <- ask+ let+ leftMaxPos = maxLv + 3+ rightMaxPos = maxRv + 2+ tell [fillStr ' ' leftMaxPos ls <> concatMap (fillStr ' ' rightMaxPos) rs] -too :: forall r a. (Show a, Enum r, Bounded r) => StrFillEnv -> [a] -> [StringFill]-too sfe xs = [CenterFill ps ' ' (show v) | (v, ps) <- zip xs $ fmap (rtops sfe) (rRange @r)]+render2XTraverse+ :: forall r bst sig m+ . ( Has (Reader (LV, RV) :+: Writer [String]) sig m+ , Enum r+ , Bounded r+ )+ => XFold m RenderProt r bst+render2XTraverse =+ ( \(vs, _) -> mkLine @r vs+ , \(vs, _) -> mkLine @r vs+ , \(vs, _) -> do+ mkLine @r vs+ pure id+ , \_ -> pure ()+ , \(vs, _) -> mkLine @r vs+ , \vs -> mkLine @r vs+ ) -stMsgT :: forall r bst. (Show bst, Ord r, Enum r, Bounded r) => StrFillEnv -> XStringFill (MsgT r bst) r bst-stMsgT sfe =- let- in ( \(ls, (from, to), idx) ->- ( [ CenterFill ps ' ' $ foo from to ((if (i, idx) == (from, 0) then parensWarapper else id) $ show v) i- | (i, (ps, v)) <- zip (rRange @r) $ zip (fmap (rtops sfe) (rRange @r)) ls- ]- , idx == 0- )- , \(xs, _) -> too @r sfe xs- , \xs -> too @r sfe xs- , \_ -> []- , \(xs, _) -> too @r sfe xs- , \xs -> too @r sfe xs- )+runRender1+ :: (Enum r, Bounded r, Ord r, Show bst, Show r)+ => Protocol (MsgT r bst) r bst+ -> (Max LV, (Max RV, (Int, Protocol RenderProt r bst)))+runRender1 prot =+ run+ . runWriter @(Max LV)+ . runWriter @(Max RV)+ . runState @Int 0+ $ xtraverse render1XTraverse prot -parensWarapper :: String -> String-parensWarapper st = "{" <> st <> "}"+runRender :: forall r bst. (Enum r, Bounded r, Ord r, Show bst, Show r) => Protocol (MsgT r bst) r bst -> String+runRender prot =+ let (Max lv@(LV maxLv), (Max rv@(RV maxRv), (_, prot1))) = runRender1 prot+ header = replicate (maxLv + 3) '-' <> concatMap (fillStr '-' (maxRv + 2)) [show r | r <- rRange @r]+ in unlines+ . fst+ . run+ . runReader (lv, rv)+ . runWriter @[String]+ $ do+ tell [header]+ xfold render2XTraverse prot1
src/TypedSession/State/Utils.hs view
@@ -75,3 +75,6 @@ replaceVal :: IntMap Int -> Int -> Int replaceVal sbm k = fromMaybe (error internalError) $ IntMap.lookup k sbm++rRange :: forall r. (Enum r, Bounded r) => [r]+rRange = [minBound @r .. maxBound]
test/Main.hs view
@@ -6,8 +6,8 @@ import Text.RawString.QQ (r) import TypedSession.State.Parser (runProtocolParser)-import TypedSession.State.Pipeline (genGraph, pipeWithTracer)-import TypedSession.State.Render (StrFillEnv (StrFillEnv))+import TypedSession.State.Pipeline (PipeResult (..), genGraph, pipeWithTracer)+import TypedSession.State.Render main :: IO () main = putStrLn "Test suite not yet implemented."@@ -41,7 +41,7 @@ let (lq, res) = pipeWithTracer a in case res of Left e -> show e- Right ppResult -> show lq <> "\n" <> genGraph (StrFillEnv 20 20) ppResult+ Right ppResult -> show lq <> "\n" <> genGraph ppResult -- >>> error r1 -- fromList [--------------------Creat-----------------@@ -155,16 +155,16 @@ -- Msg <((S2 SFalse,End,End),(Client,Counter),1)> CStop [] Client Counter -- Terminal [End,End,End] -- ]--- -------------------------------------Client--------------Server-------------Counter--- LABEL 0 S0 S1 s S2 s--- [Branch Client] S0 S1 s S2 s--- AddOne {S2 STrue}-> S1 s ->S2 s--- Ping S1 STrue-> ->S1 s S2 s--- Pong S3<- <-S3 S2 s--- Goto 0 S0 S1 s S2 s--- Stop {S1 SFalse}-> ->S1 s S2 s--- CStop S2 SFalse-> End ->S2 s--- Terminal End End End+-- ---------------------Client----------Server----------Counter---------+-- Label 0 S0 S1 s S2 s +-- [Branch Client] S0 S1 s S2 s +-- AddOne {S2 STrue} -> S1 s -> S2 s +-- Ping S1 STrue -> -> S1 s S2 s +-- Pong S3 <- <- S3 S2 s +-- Goto 0 S0 S1 s S2 s +-- Stop {S1 SFalse} -> -> S1 s S2 s +-- CStop S2 SFalse -> End -> S2 s +-- Terminal End End End data Role = Buyer@@ -231,9 +231,9 @@ let (seqList, res) = pipeWithTracer a in case res of Left e -> show e- Right ppResult ->+ Right PipeResult{msgT} -> let st = show seqList- in st <> "\n" <> genGraph (StrFillEnv 20 20) ppResult+ in st <> "\n" <> runRender msgT -- >>> error r2 -- fromList [--------------------Creat-----------------@@ -527,30 +527,30 @@ -- Msg <((S1 NotFound,S0,S1 s),(Buyer,Buyer2),1)> SellerNoBook [] Buyer Buyer2 -- Goto ([S0,S0,S1 s],0) 0 -- ]--- -------------------------------------Buyer---------------Seller--------------Buyer2--- LABEL 0 S0 S0 S1 s--- Title S0-> ->S0 S1 s--- [Branch Seller] S2 s S3 S1 s--- Price S2 s<- <-{S2 Found} S1 s--- [Branch Buyer] S4 S5 s S1 s--- PriceToBuyer2 {S1 Two}-> S5 s ->S1 s--- [Branch Buyer2] S6 s S5 s S7--- NotSupport1 S6 s<- S5 s <-{S6 NotSupport}--- TwoNotBuy S5 NotSupport-> ->S5 s S1 s--- Goto 0 S0 S0 S1 s--- SupportVal S6 s<- S5 s <-{S6 Support}--- [Branch Buyer] S8 S5 s S9 s--- TwoAccept {S5 Enough}-> ->S5 s S9 s--- TwoDate S10<- <-S10 S9 s--- TwoSuccess S9 Enough-> S0 ->S9 s--- Goto 0 S0 S0 S1 s--- TwoNotBuy1 {S5 NotEnough}-> ->S5 s S9 s--- TwoFailed S9 NotEnough-> End ->S9 s--- Terminal End End End--- OneAccept {S5 One}-> ->S5 s S1 s--- OneDate S11<- <-S11 S1 s--- OneSuccess S1 One-> S0 ->S1 s--- Goto 0 S0 S0 S1 s--- NoBook S2 s<- <-{S2 NotFound} S1 s--- SellerNoBook S1 NotFound-> S0 ->S1 s--- Goto 0 S0 S0 S1 s+-- ------------------------------Buyer---------------Seller--------------Buyer2--------------+-- Label 0 S0 S0 S1 s +-- Title [String] S0 -> -> S0 S1 s +-- [Branch Seller] S2 s S3 S1 s +-- Price [Int] S2 s <- <- {S2 Found} S1 s +-- [Branch Buyer] S4 S5 s S1 s +-- PriceToBuyer2 [Int] {S1 Two} -> S5 s -> S1 s +-- [Branch Buyer2] S6 s S5 s S7 +-- NotSupport1 [] S6 s <- S5 s <- {S6 NotSupport} +-- TwoNotBuy [] S5 NotSupport -> -> S5 s S1 s +-- Goto 0 S0 S0 S1 s +-- SupportVal [Int] S6 s <- S5 s <- {S6 Support} +-- [Branch Buyer] S8 S5 s S9 s +-- TwoAccept [] {S5 Enough} -> -> S5 s S9 s +-- TwoDate [Int] S10 <- <- S10 S9 s +-- TwoSuccess [Int] S9 Enough -> S0 -> S9 s +-- Goto 0 S0 S0 S1 s +-- TwoNotBuy1 [] {S5 NotEnough} -> -> S5 s S9 s +-- TwoFailed [] S9 NotEnough -> End -> S9 s +-- Terminal End End End +-- OneAccept [] {S5 One} -> -> S5 s S1 s +-- OneDate [Int] S11 <- <- S11 S1 s +-- OneSuccess [Int] S1 One -> S0 -> S1 s +-- Goto 0 S0 S0 S1 s +-- NoBook [] S2 s <- <- {S2 NotFound} S1 s +-- SellerNoBook [] S1 NotFound -> S0 -> S1 s +-- Goto 0 S0 S0 S1 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.3.0.0+version: 0.3.0.1 -- A short (one-line) description of the package. synopsis: Automatically generate status for typed-session.