typed-session-state-algorithm (empty) → 0.1.0.0
raw patch · 12 files changed
+2102/−0 lines, 12 filesdep +basedep +containersdep +fused-effects
Dependencies added: base, containers, fused-effects, megaparsec, parser-combinators, prettyprinter, raw-strings-qq, typed-session-state-algorithm
Files
- CHANGELOG.md +5/−0
- LICENSE +20/−0
- src/TypedSession/State/Constraint.hs +89/−0
- src/TypedSession/State/GenDoc.hs +199/−0
- src/TypedSession/State/Parser.hs +172/−0
- src/TypedSession/State/Pattern.hs +29/−0
- src/TypedSession/State/Piple.hs +367/−0
- src/TypedSession/State/Render.hs +217/−0
- src/TypedSession/State/Type.hs +240/−0
- src/TypedSession/State/Utils.hs +77/−0
- test/Main.hs +565/−0
- typed-session-state-algorithm.cabal +122/−0
+ CHANGELOG.md view
@@ -0,0 +1,5 @@+# Revision history for typed-session-state-algorithm++## 0.1.0.0 -- YYYY-mm-dd++* First version. Released on an unsuspecting world.
+ LICENSE view
@@ -0,0 +1,20 @@+Copyright (c) 2024 sdzx-1++Permission is hereby granted, free of charge, to any person obtaining+a copy of this software and associated documentation files (the+"Software"), to deal in the Software without restriction, including+without limitation the rights to use, copy, modify, merge, publish,+distribute, sublicense, and/or sell copies of the Software, and to+permit persons to whom the Software is furnished to do so, subject to+the following conditions:++The above copyright notice and this permission notice shall be included+in all copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.+IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY+CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,+TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE+SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ src/TypedSession/State/Constraint.hs view
@@ -0,0 +1,89 @@+module TypedSession.State.Constraint where++import Data.IntMap (IntMap)+import qualified Data.IntMap as I+import qualified Data.List as L++{- | Constraint+ 1 ~ 2 = Constraint 1 2+ 2 ~ 3 = Constraint 2 3+-}+data Constraint = Constraint Int Int+ deriving (Show, Eq, Ord)++type SubMap = IntMap Int++toTuple :: Constraint -> (Int, Int)+toTuple (Constraint b s) = (b, s)++{- | bigSwapConstr+>>> bigSwapConstr (Constraint 1 2)+Constraint 2 1+-}+bigSwapConstr :: Constraint -> Constraint+bigSwapConstr (Constraint a b)+ | a >= b = Constraint a b+ | otherwise = Constraint b a++subFun :: [Constraint] -> [Constraint]+subFun [] = []+subFun (Constraint b s : ys) = Constraint b s : subFun (replace b s ys)++replace :: Int -> Int -> [Constraint] -> [Constraint]+replace _b _s [] = []+replace b s ((Constraint b' s') : ys) =+ if b == s'+ then Constraint b' s : replace b s ys+ else Constraint b' s' : replace b s ys++{- | findNewConstraint+>>> findNewConstraint [Constraint 3 1, Constraint 4 2, Constraint 4 3]+[[Constraint 3 2]]+-}+findNewConstraint :: [Constraint] -> [[Constraint]]+findNewConstraint ls =+ let grouped = L.groupBy (\(Constraint a _) (Constraint c _) -> a == c) ls+ genCons s val = case val of+ [] -> s+ [_] -> s+ xs ->+ case L.sort $ map (snd . toTuple) xs of+ [] -> error "np"+ minVal : txs' -> map (`Constraint` minVal) txs' : s+ in foldl' genCons [] grouped++{- | stepConstraint+>>> stepConstraint [Constraint 3 1, Constraint 4 2, Constraint 4 3]+[Constraint 3 1,Constraint 4 2,Constraint 4 1]+-}+stepConstraint :: [Constraint] -> [Constraint]+stepConstraint = L.nub . subFun . L.sort . L.nub . map bigSwapConstr++{- | constraintLoop+>>> constraintLoop [Constraint 3 1, Constraint 4 2, Constraint 4 3]+[Constraint 2 1,Constraint 3 1,Constraint 4 1]++-------------------------------------------------++>>> stepConstraint [Constraint 3 1, Constraint 4 2, Constraint 4 3]+[Constraint 3 1,Constraint 4 2,Constraint 4 1]++>>> findNewConstraint [Constraint 3 1,Constraint 4 2,Constraint 4 1]+[[Constraint 2 1]]++>>> stepConstraint ([Constraint 3 1,Constraint 4 2,Constraint 4 1] <> [Constraint 2 1])+[Constraint 2 1,Constraint 3 1,Constraint 4 1]+-}+constraintLoop :: [Constraint] -> [Constraint]+constraintLoop ls =+ let ls' = stepConstraint ls+ in case findNewConstraint ls' of+ [] -> ls'+ xs -> constraintLoop (concat xs <> ls')++{- | constrToSubMap+>>> constrToSubMap [Constraint 3 1, Constraint 4 2, Constraint 4 3]+fromList [(2,1),(3,1),(4,1)]+-}+constrToSubMap :: [Constraint] -> SubMap+constrToSubMap ls = I.fromList $ map toTuple $ constraintLoop ls
+ src/TypedSession/State/GenDoc.hs view
@@ -0,0 +1,199 @@+{-# 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
+ src/TypedSession/State/Parser.hs view
@@ -0,0 +1,172 @@+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE QuasiQuotes #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# OPTIONS_GHC -Wno-unused-do-bind #-}++module TypedSession.State.Parser where++import Data.Char (isUpper)+import qualified Data.List as L+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)++{-++1. protocol name+2. role name+3. branch state (options)++-}++data ParserError+ = EmptyInput+ | TheFirstLetterNotCapitalized+ deriving (Show, Eq, Ord)++instance ShowErrorComponent ParserError where+ showErrorComponent = \case+ EmptyInput -> "Trying to parse constructor or type, but input is empty!"+ TheFirstLetterNotCapitalized -> "Try to parse constructor or type, but the first letter is not capitalized!"++type Parser = Parsec ParserError String++spaceConsumer :: Parser ()+spaceConsumer =+ L.space+ space1+ (L.skipLineComment "--")+ (L.skipBlockCommentNested "{-" "-}")++symbol :: String -> Parser String+symbol = L.symbol spaceConsumer++lexeme :: Parser a -> Parser a+lexeme = L.lexeme spaceConsumer++msg, label, branch, branchSt, goto, terminal :: Parser String+msg = symbol "Msg"+label = symbol "Label"+branch = symbol "Branch"+branchSt = symbol "BranchSt"+goto = symbol "Goto"+terminal = symbol "Terminal"++integer :: Parser Integer+integer = lexeme L.decimal++comma :: Parser String+comma = symbol ","++brackets :: Parser a -> Parser a+brackets = between (symbol "[") (symbol "]")++braces :: Parser a -> Parser a+braces = between (symbol "{") (symbol "}")++dbg :: String -> m a -> m a+dbg _ ma = ma++constrOrType :: Parser String+constrOrType = dbg "constrOrType" $ do+ st <- char '"' >> manyTill L.charLiteral (char '"')+ case st of+ [] -> customFailure EmptyInput+ (x : _) ->+ if isUpper x+ then pure st+ else customFailure TheFirstLetterNotCapitalized+ spaceConsumer+ pure st++mkParserA :: forall a. (Enum a, Bounded a, Show a) => Parser a+mkParserA = do+ let rg = [minBound @a .. maxBound]+ rg' =+ fmap snd+ . L.sortBy (\(a, _) (b, _) -> compare b a)+ $ zip (fmap (length . show) rg) rg+ a <-+ choice $ fmap (\r -> (string (show r) >> pure r)) rg'+ spaceConsumer+ pure a++parseMsg+ :: forall r+ . (Enum r, Bounded r, Show r)+ => Parser (MsgOrLabel Creat r)+parseMsg = dbg "Msg" $ do+ msg+ constr <- constrOrType+ args <- brackets (constrOrType `sepBy` comma)+ from <- mkParserA @r+ to <- mkParserA @r+ pure $ Msg constr args from to++parseLabel :: (Show r) => Parser (MsgOrLabel Creat r)+parseLabel = dbg "Label" $ do+ label+ i <- fromIntegral <$> integer+ pure $ Label i++parseGoto :: (Show bst, Show r) => Parser (Protocol Creat r bst)+parseGoto = dbg "Goto" $ do+ goto+ i <- fromIntegral <$> integer+ pure $ Goto i++parseTerminal :: (Show bst, Show r) => Parser (Protocol Creat r bst)+parseTerminal = dbg "Terminal" $ do+ terminal+ pure $ Terminal++parseBranchSt+ :: forall bst r+ . (Enum bst, Bounded bst, Show bst, Enum r, Bounded r, Show r)+ => Parser (BranchSt Creat r bst)+parseBranchSt = dbg "BranchSt" $ do+ branchSt+ bst <- mkParserA @bst+ prot <- parseProtocol @r @bst+ pure (BranchSt bst prot)++parseBranch+ :: forall r bst+ . (Enum r, Bounded r, Show r, Enum bst, Bounded bst, Show bst) => Parser (Protocol Creat r bst)+parseBranch = dbg "Branch" $ do+ branch+ r1 <- mkParserA @r+ braces $ do+ branchSts <- some (parseBranchSt @bst @r)+ pure (Branch r1 branchSts)++parseMsgOrLabel+ :: forall r bst+ . (Enum r, Bounded r, Show r, Enum bst, Bounded bst, Show bst)+ => Parser (Protocol Creat r bst)+parseMsgOrLabel = dbg "MsgOrLabel" $ do+ msgOrLabel <- choice [parseMsg @r, parseLabel]+ prot <- parseProtocol @r @bst+ pure (msgOrLabel :> prot)++parseProtocol+ :: forall r bst+ . (Enum r, Bounded r, Show r, Enum bst, Bounded bst, Show bst)+ => Parser (Protocol Creat r bst)+parseProtocol = dbg "Protocol" $ do+ choice [parseGoto, parseTerminal, parseBranch @r @bst, parseMsgOrLabel]++runProtocolParser+ :: forall r bst+ . (Enum r, Enum bst, Bounded r, Bounded bst, Show r, Show bst)+ => String+ -> Either String (Protocol Creat r bst)+runProtocolParser st =+ let res = runParser (between spaceConsumer eof $ parseProtocol @r @bst) "" st+ in case res of+ Left e -> Left $ errorBundlePretty @String @ParserError e+ Right a -> Right a
+ src/TypedSession/State/Pattern.hs view
@@ -0,0 +1,29 @@+{-# 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 ()
+ src/TypedSession/State/Piple.hs view
@@ -0,0 +1,367 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE EmptyCase #-}+{-# LANGUAGE FlexibleContexts #-}+{-# 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))+import Data.IntMap (IntMap)+import qualified Data.IntMap as IntMap+import qualified Data.List as L+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++------------------------++addIdxXTraverse+ :: forall r bst sig m+ . ( Has (State Int :+: 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)+ outputInx <- get @Int+ pure (inputIdx, outputInx)+ , const get+ , \(_, _) -> do+ inputIdx <- get @Int+ modify (Set.insert inputIdx)+ pure (inputIdx, id)+ , \_ -> modify @Int (+ 1)+ , const get+ , const get+ )++reRankXTraverse :: (Monad m) => IntMap Int -> XTraverse m Idx Idx r bst+reRankXTraverse sbm =+ ( \((a, b), _) -> pure (replaceVal sbm a, replaceVal sbm b)+ , \(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 (State Int :+: 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), _) -> do+ idx <- get @Int+ modify @Int (+ 1)+ pure (mkNums va, mkNums vb, idx)+ , \(va, _) -> pure $ mkNums va+ , \(va, (r, ls)) -> do+ let len = length ls+ -- At least two branches.+ when (len < 2) (throwError (AtLeastTwoBranches (Branch va r ls)))+ void $ runState @(Maybe r) Nothing $ forM_ ls $ \(BranchSt _ _ prot) -> do+ -- The first message of each branch must have the same receiver and sender.+ case getFirstMsgInfo prot of+ Nothing -> throwError (BranchNoMsg prot)+ Just (from, _) -> do+ when (from /= r) $+ throwError (BranchFirstMsgMustHaveTheSameSender prot)+ -- Each branch sender must send (directly or indirectly) a message to all other receivers to notify the state change.+ let receivers = L.nub $ L.sort $ r : (fmap snd $ getAllMsgInfo prot)+ when (receivers /= [minBound .. maxBound]) (throwError (BranchNotNotifyAllOtherReceivers prot))+ pure (mkNums va, id)+ , \_ -> put @Int 0+ , \(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+ )++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 (xtraverse addIdxXTraverse prot0)+ trace (TracerProtocolIdx idxProt)+ trace (TracerReRank (reRank brSet maxSzie))+ idxProt1 <- xtraverse (reRankXTraverse (reRank brSet maxSzie)) idxProt+ trace (TracerProtocolIdx idxProt1)+ prot1 <-+ fmap snd+ . runState @Int 100+ $ xtraverse addNumsXTraverse idxProt1+ trace (TracerProtocolAddNum prot1)+ prot2 <- xtraverse toGenConstrXTraverse prot1+ trace (TracerProtocolGenConst 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)
+ src/TypedSession/State/Render.hs view
@@ -0,0 +1,217 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MultiWayIf #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE NoFieldSelectors #-}++module TypedSession.State.Render where++import Control.Algebra ((:+:))+import Control.Carrier.State.Strict (runState)+import Control.Carrier.Writer.Strict (runWriter)+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++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'++-- width :: Int+-- width = 30++-- leftWidth :: Int+-- leftWidth = 20++data StrFillEnv = StrFillEnv+ { width :: Int+ , leftWidth :: Int+ }+ deriving (Show)++defaultStrFilEnv :: StrFillEnv+defaultStrFilEnv = StrFillEnv 30 20++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++--------------------------------------------+type XStringFill eta r bst =+ ( XMsg eta -> ([StringFill], Bool)+ , XLabel eta -> [StringFill]+ , XBranch eta -> [StringFill]+ , XBranchSt eta -> [StringFill]+ , XGoto eta -> [StringFill]+ , XTerminal eta -> [StringFill]+ )++renderXFold+ :: forall r eta bst sig m+ . ( Has (Writer [[StringFill]] :+: State Int) sig m+ , ForallX Show eta+ , Enum r+ , Bounded 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]+ )++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)++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 =+ "--------------------"+ ++ desc+ ++ "-----------------\n"+ ++ st+ ++ "\n"++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)++rRange :: forall r. (Enum r, Bounded r) => [r]+rRange = [minBound @r .. maxBound]++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)]++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+ )++parensWarapper :: String -> String+parensWarapper st = "{" <> st <> "}"++instance (Show r, Show bst, Enum r, Bounded r, Eq r, Ord r) => Show (Tracer r bst) where+ show = \case+ TracerProtocolCreat p -> traceWrapper "Creat" $ show p+ TracerProtocolIdx p -> traceWrapper "Idx" $ show p+ TracerReRank p -> traceWrapper "ReRank" $ show p+ TracerProtocolAddNum p -> traceWrapper "AddNum" $ show p+ TracerProtocolGenConst p -> traceWrapper "GenConst" $ show p+ TracerConstraints p -> traceWrapper "Constrains" $ show p+ TracerSubMap p -> traceWrapper "SubMap" $ show p+ TracerProtocolGenConstN p -> traceWrapper "GenConstN" $ show p+ TracerCollectBranchDynVal dvs -> traceWrapper "CollectBranchDynVal" $ show dvs+ TracerProtocolMsgT p -> traceWrapper "MsgT" $ show p+ TracerProtocolMsgT1 p -> traceWrapper "MsgT1" $ show p
+ src/TypedSession/State/Type.hs view
@@ -0,0 +1,240 @@+{-# 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.Kind (Constraint, Type)+import Prettyprinter+import Prettyprinter.Render.String (renderString)++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 (Protocol eta r bst)+ deriving (Functor)++-- | MsgOrLabel+data MsgOrLabel eta r+ = Msg (XMsg eta) String [String] r r+ | Label (XLabel eta) Int+ deriving (Functor)++infixr 5 :>++-- | Protocol+data Protocol eta r bst+ = (MsgOrLabel eta r) :> (Protocol eta r bst)+ | Branch (XBranch eta) r [BranchSt eta r bst]+ | Goto (XGoto eta) Int+ | Terminal (XTerminal eta)+ deriving (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, [BranchSt eta r bst]))+ -> m+ ( XBranch gama+ , m (Protocol gama r bst) -> m (Protocol gama r bst)+ )+ , (XBranchSt eta, (bst, 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 xt@(xmsg, xlabel, xbranch, xbranchSt, xgoto, xterminal) prot = case prot of+ msgOrLabel :> prots -> do+ res <- case msgOrLabel of+ Msg xv a b c d -> do+ xv' <- xmsg (xv, (a, b, c, d, prots))+ pure (Msg xv' a b c d)+ Label xv i -> do+ xv' <- xlabel (xv, (i, prots))+ pure (Label xv' i)+ prots' <- xtraverse xt prots+ pure (res :> prots')+ Branch xv r ls -> do+ (xv', wrapper) <- xbranch (xv, (r, ls))+ ls' <- forM ls $ \(BranchSt xbst bst prot1) -> do+ xbst' <- xbranchSt (xbst, (bst, prot1))+ prot' <- wrapper $ xtraverse xt prot1+ pure (BranchSt xbst' bst prot')+ pure (Branch xv' r ls')+ Goto xv i -> do+ xv' <- xgoto (xv, i)+ pure (Goto xv' i)+ Terminal xv -> do+ xv' <- xterminal 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, [BranchSt eta r bst])) -> m (m () -> m ())+ , (XBranchSt eta, (bst, 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 xt@(xmsg, xlabel, xbranch, xbranchst, xgoto, xterminal) prot = case prot of+ msgOrLabel :> prots -> do+ case msgOrLabel of+ Msg xv a b c d -> xmsg (xv, (a, b, c, d, prots))+ Label xv i -> xlabel (xv, i)+ xfold xt prots+ Branch xv r ls -> do+ wrapper <- xbranch (xv, (r, ls))+ forM_ ls $ \(BranchSt xbst bst prot1) -> do+ xbranchst (xbst, (bst, prot1))+ wrapper $ xfold xt prot1+ Goto xv i -> xgoto (xv, i)+ Terminal xv -> xterminal xv++-- | ProtocolError+data ProtocolError r bst+ = AtLeastTwoBranches (Protocol Idx r bst)+ | DefLabelMultTimes Int+ | LabelUndefined Int+ | BranchNoMsg (Protocol Idx r bst)+ | BranchFirstMsgMustHaveTheSameSender (Protocol Idx r bst)+ | BranchNotNotifyAllOtherReceivers (Protocol Idx r bst)++instance (Show r, Show bst) => Show (ProtocolError r bst) where+ show = \case+ AtLeastTwoBranches prot -> "At least two branches are required\n" <> show prot+ DefLabelMultTimes msgOrLabel -> "Defining Label multiple times\n" <> show msgOrLabel+ LabelUndefined prot -> "Label Undefined\n" <> show prot+ BranchNoMsg prot -> "Branch No Msg\n" <> show prot+ BranchFirstMsgMustHaveTheSameSender prot ->+ "The first message of each branch must have the same sender.\n" <> show prot+ BranchNotNotifyAllOtherReceivers prot ->+ "Each branch sender must send (directly or indirectly) a message to all other receivers to notify the state change.\n" <> show prot++------------------------++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)+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 = \case+ TNum i -> "S" ++ show i+ BstList i bst -> "S" ++ show i ++ " " ++ show bst+ TAny i -> "S" ++ show i ++ " s"+ TEnd -> "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 (BranchSt xbst bst prot) = "* BranchSt" <+> pretty (show xbst) <+> pretty (show bst) <> line <> (pretty prot)++instance (Show (XMsg eta), Show (XLabel eta), Show r) => Pretty (MsgOrLabel eta r) where+ pretty = \case+ Msg xv cst args from to ->+ hsep ["Msg", angles (pretty $ show xv), pretty cst, pretty args, pretty (show from), pretty (show to)]+ Label xv i -> hsep ["Label", pretty $ show xv, pretty i]++instance (ForallX Show eta, Show r, Show bst) => Pretty (Protocol eta r bst) where+ pretty = \case+ msgOrLabel :> prots -> pretty msgOrLabel <> line <> pretty prots+ Branch is r ls -> nest 2 $ "[Branch]" <+> pretty (show is) <+> pretty (show r) <> line <> vsep (fmap pretty ls)+ Goto xv i -> "Goto" <+> pretty (show xv) <+> pretty i+ Terminal xv -> "Terminal" <+> pretty (show xv)++-----------------------------+instance (Pretty (Protocol eta r bst), Show (XBranchSt eta), Show bst) => Show (BranchSt eta r bst) where+ show = renderString . layoutPretty defaultLayoutOptions . pretty++instance (Show (XMsg eta), Show (XLabel eta), Show r) => Show (MsgOrLabel eta r) where+ show = renderString . layoutPretty defaultLayoutOptions . pretty++instance (ForallX Show eta, Show r, Show bst) => Show (Protocol eta r bst) where+ show = renderString . layoutPretty defaultLayoutOptions . pretty
+ src/TypedSession/State/Utils.hs view
@@ -0,0 +1,77 @@+{-# 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.Utils where++import Control.Carrier.Fresh.Strict+import Control.Carrier.State.Strict+import Control.Effect.Writer+import Control.Monad+import Data.IntMap (IntMap)+import qualified Data.IntMap as IntMap+import qualified Data.List as L+import Data.Maybe (fromJust, fromMaybe)+import Data.Sequence (Seq)+import qualified Data.Sequence as Seq+import qualified TypedSession.State.Constraint as C+import TypedSession.State.Type+import Prelude hiding (traverse)++------------------------++restoreWrapper+ :: forall s sig m a+ . (Has (State s) sig m) => m a -> m a+restoreWrapper m = do+ st <- get @s+ a <- m+ put st+ pure a++getFirstMsgInfo :: Protocol eta r bst -> Maybe (r, r)+getFirstMsgInfo = \case+ msgOrLabel :> prots -> case msgOrLabel of+ Msg _ _ _ from to -> Just (from, to)+ _ -> getFirstMsgInfo prots+ _ -> Nothing++getAllMsgInfo :: Protocol eta r bst -> [(r, r)]+getAllMsgInfo = \case+ msgOrLabel :> prots -> case msgOrLabel of+ Msg _ _ _ from to -> (from, to) : getAllMsgInfo prots+ _ -> getAllMsgInfo prots+ Branch _ _ ls -> concatMap (\(BranchSt _ _ prots) -> getAllMsgInfo prots) ls+ Goto _ _ -> []+ Terminal _ -> []++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', (minimum vals', maximum vals'))++replaceList :: C.SubMap -> [Int] -> [Int]+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
+ test/Main.hs view
@@ -0,0 +1,565 @@+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE QuasiQuotes #-}+{-# LANGUAGE TypeApplications #-}++module Main (main) where++import Text.RawString.QQ (r)+import TypedSession.State.GenDoc (genGraph)+import TypedSession.State.Parser (runProtocolParser)+import TypedSession.State.Pattern+import TypedSession.State.Piple (PipleResult (..), piple, pipleWithTracer)+import TypedSession.State.Render (StrFillEnv (StrFillEnv), defaultStrFilEnv)+import TypedSession.State.Type (Creat, Protocol)++main :: IO ()+main = putStrLn "Test suite not yet implemented."++data PingPongRole = Client | Server | Counter+ deriving (Show, Read, Eq, Ord, Enum, Bounded)++data PingPongBranchSt = STrue | SFalse+ deriving (Show, Read, Eq, Ord, Enum, Bounded)++s1 =+ [r|+ + Label 0+ Branch Client {+ BranchSt STrue+ Msg "AddOne" [] Client Counter+ Msg "Ping" ["Int", "Int", "Int"] Client Server+ Msg "Pong" [] Server Client+ Goto 0+ BranchSt SFalse+ Msg "Stop" [] Client Server+ Msg "CStop" [] Client Counter+ Terminal+ }+|]++r1 = case runProtocolParser @PingPongRole @PingPongBranchSt s1 of+ Left e -> e+ Right a ->+ let (lq, res) = pipleWithTracer a+ in case res of+ Left e -> show e+ Right ppResult -> show lq <> "\n" <> genGraph (StrFillEnv 20 20) ppResult++-- >>> error r1+-- fromList [--------------------Creat-----------------+-- Label () 0+-- [Branch] () Client+-- * BranchSt () STrue+-- Msg <()> AddOne [] Client Counter+-- Msg <()> Ping [Int, Int, Int] Client Server+-- Msg <()> Pong [] Server Client+-- Goto () 0+-- * BranchSt () SFalse+-- Msg <()> Stop [] Client Server+-- Msg <()> CStop [] Client Counter+-- Terminal ()+-- ,--------------------Idx-----------------+-- Label 0 0+-- [Branch] 0 Client+-- * BranchSt () STrue+-- Msg <(1,2)> AddOne [] Client Counter+-- Msg <(2,3)> Ping [Int, Int, Int] Client Server+-- Msg <(3,4)> Pong [] Server Client+-- Goto 4 0+-- * BranchSt () SFalse+-- Msg <(5,6)> Stop [] Client Server+-- Msg <(6,7)> CStop [] Client Counter+-- Terminal 7+-- ,--------------------ReRank-----------------+-- fromList [(0,0),(1,1),(2,2),(3,3),(4,4),(5,5),(6,6),(7,7)]+-- ,--------------------Idx-----------------+-- Label 0 0+-- [Branch] 0 Client+-- * BranchSt () STrue+-- Msg <(1,2)> AddOne [] Client Counter+-- Msg <(2,3)> Ping [Int, Int, Int] Client Server+-- Msg <(3,4)> Pong [] Server Client+-- Goto 4 0+-- * BranchSt () SFalse+-- Msg <(5,6)> Stop [] Client Server+-- Msg <(6,7)> CStop [] Client Counter+-- Terminal 7+-- ,--------------------AddNum-----------------+-- Label [0,1,2] 0+-- [Branch] [0,1,2] Client+-- * BranchSt () STrue+-- Msg <([3,4,5],[6,7,8],0)> AddOne [] Client Counter+-- Msg <([6,7,8],[9,10,11],1)> Ping [Int, Int, Int] Client Server+-- Msg <([9,10,11],[12,13,14],2)> Pong [] Server Client+-- Goto [12,13,14] 0+-- * BranchSt () SFalse+-- Msg <([15,16,17],[18,19,20],0)> Stop [] Client Server+-- Msg <([18,19,20],[21,22,23],1)> CStop [] Client Counter+-- Terminal [21,22,23]+-- ,--------------------GenConst-----------------+-- Label ([0,1,2],0) 0+-- [Branch] [0,1,2] Client+-- * BranchSt () STrue+-- Msg <(([3,4,5],[6,7,8]),(Client,Counter),0)> AddOne [] Client Counter+-- Msg <(([6,7,8],[9,10,11]),(Client,Server),1)> Ping [ Int+-- , Int+-- , Int ] Client Server+-- Msg <(([9,10,11],[12,13,14]),(Server,Client),2)> Pong [] Server Client+-- Goto ([12,13,14],0) 0+-- * BranchSt () SFalse+-- Msg <(([15,16,17],[18,19,20]),(Client,Server),0)> Stop [] Client Server+-- Msg <(([18,19,20],[21,22,23]),(Client,Counter),1)> CStop [] Client Counter+-- Terminal [21,22,23]+-- ,--------------------Constrains-----------------+-- fromList [Constraint 1 4,Constraint 2 5,Constraint 3 5,Constraint 4 7,Constraint 6 7,Constraint 8 11,Constraint 10 9,Constraint 11 14,Constraint 12 0,Constraint 13 1,Constraint 14 2,Constraint 1 16,Constraint 2 17,Constraint 15 16,Constraint 17 20,Constraint 18 20,Constraint 19 22,Constraint 21 (-1),Constraint 22 (-1),Constraint 23 (-1)]+-- ,--------------------SubMap-----------------+-- fromList [(3,2),(4,1),(5,2),(6,1),(7,1),(8,2),(9,3),(10,3),(11,2),(12,0),(13,1),(14,2),(15,1),(16,1),(17,2),(18,2),(19,-1),(20,2),(21,-1),(22,-1),(23,-1)]+-- ,--------------------GenConstN-----------------+-- Label ([0,1,2],0) 0+-- [Branch] [0,1,2] Client+-- * BranchSt () STrue+-- Msg <(([2,1,2],[1,1,2]),(Client,Counter),0)> AddOne [] Client Counter+-- Msg <(([1,1,2],[3,3,2]),(Client,Server),1)> Ping [Int, Int, Int] Client Server+-- Msg <(([3,3,2],[0,1,2]),(Server,Client),2)> Pong [] Server Client+-- Goto ([0,1,2],0) 0+-- * BranchSt () SFalse+-- 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]+-- ,--------------------CollectBranchDynVal-----------------+-- fromList [1,2]+-- ,--------------------MsgT-----------------+-- Label ([S0,S1 s,S2 s],0) 0+-- [Branch] [S0,S1 s,S2 s] Client+-- * BranchSt () STrue+-- Msg <([S2 STrue,S1 s,S2 s],(Client,Counter),0)> AddOne [] Client Counter+-- Msg <([S1 STrue,S1 s,S2 s],(Client,Server),1)> Ping [ Int+-- , Int+-- , Int ] Client Server+-- Msg <([S3,S3,S2 s],(Server,Client),2)> Pong [] Server Client+-- Goto ([S0,S1 s,S2 s],0) 0+-- * BranchSt () SFalse+-- Msg <([S1 SFalse,S1 s,S2 s],(Client,Server),0)> Stop [] Client Server+-- Msg <([S2 SFalse,End,S2 s],(Client,Counter),1)> CStop [] Client Counter+-- Terminal [End,End,End]+-- ,--------------------MsgT1-----------------+-- Label ([S0,S1 s,S2 s],0) 0+-- [Branch] [S0,S1 s,S2 s] Client+-- * BranchSt () STrue+-- Msg <((S2 STrue,S1 STrue,S2 s),(Client,Counter),0)> AddOne [] Client Counter+-- Msg <((S1 STrue,S3,S3),(Client,Server),1)> Ping [Int, Int, Int] Client Server+-- Msg <((S3,S1 s,S0),(Server,Client),2)> Pong [] Server Client+-- Goto ([S0,S1 s,S2 s],0) 0+-- * BranchSt () SFalse+-- Msg <((S1 SFalse,S2 SFalse,End),(Client,Server),0)> Stop [] Client Server+-- 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+-- * BranchSt STrue+-- 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+-- * BranchSt SFalse+-- Stop {S1 SFalse}-> ->S1 s S2 s+-- CStop S2 SFalse-> End ->S2 s+-- ~ Terminal End End End++data Role+ = Buyer+ | Seller+ | Buyer2+ deriving (Show, Eq, Ord, Enum, Bounded)++data BookBranchSt+ = NotFound+ | Found+ | One+ | Two+ | Support+ | NotSupport+ | Enough+ | NotEnough+ deriving (Show, Eq, Ord, Enum, Bounded)++s2 =+ [r|+ Label 0+ Msg "Title" ["String"] Buyer Seller+ Branch Seller {+ BranchSt Found + Msg "Price" ["Int"] Seller Buyer+ Branch Buyer {+ BranchSt Two + Msg "PriceToBuyer2" ["Int"] Buyer Buyer2+ Branch Buyer2 {+ BranchSt NotSupport + Msg "NotSupport1" [] Buyer2 Buyer+ Msg "TwoNotBuy" [] Buyer Seller+ Goto 0+ BranchSt Support + Msg "SupportVal" ["Int"] Buyer2 Buyer+ Branch Buyer {+ BranchSt Enough + Msg "TwoAccept" [] Buyer Seller+ Msg "TwoDate" ["Int"] Seller Buyer+ Msg "TwoSuccess" ["Int"] Buyer Buyer2+ Goto 0+ BranchSt NotEnough + Msg "TwoNotBuy1" [] Buyer Seller+ Msg "TwoFailed" [] Buyer Buyer2+ Terminal+ }+ }+ BranchSt One + Msg "OneAccept" [] Buyer Seller+ Msg "OneDate" ["Int"] Seller Buyer+ Msg "OneSuccess" ["Int"] Buyer Buyer2+ Goto 0+ }+ BranchSt NotFound + Msg "NoBook" [] Seller Buyer+ Msg "SellerNoBook" [] Buyer Buyer2+ Goto 0+ }+|]++r2 = case runProtocolParser @Role @BookBranchSt s2 of+ Left e -> e+ Right a ->+ let (seqList, res) = pipleWithTracer a+ in case res of+ Left e -> show e+ Right ppResult ->+ let st = show seqList+ in st <> "\n" <> genGraph (StrFillEnv 20 20) ppResult++-- >>> error r2+-- fromList [--------------------Creat-----------------+-- Label () 0+-- Msg <()> Title [String] Buyer Seller+-- [Branch] () Seller+-- * BranchSt () Found+-- Msg <()> Price [Int] Seller Buyer+-- [Branch] () Buyer+-- * BranchSt () Two+-- Msg <()> PriceToBuyer2 [Int] Buyer Buyer2+-- [Branch] () Buyer2+-- * BranchSt () NotSupport+-- Msg <()> NotSupport1 [] Buyer2 Buyer+-- Msg <()> TwoNotBuy [] Buyer Seller+-- Goto () 0+-- * BranchSt () Support+-- Msg <()> SupportVal [Int] Buyer2 Buyer+-- [Branch] () Buyer+-- * BranchSt () Enough+-- Msg <()> TwoAccept [] Buyer Seller+-- Msg <()> TwoDate [Int] Seller Buyer+-- Msg <()> TwoSuccess [Int] Buyer Buyer2+-- Goto () 0+-- * BranchSt () NotEnough+-- Msg <()> TwoNotBuy1 [] Buyer Seller+-- Msg <()> TwoFailed [] Buyer Buyer2+-- Terminal ()+-- * BranchSt () One+-- Msg <()> OneAccept [] Buyer Seller+-- Msg <()> OneDate [Int] Seller Buyer+-- Msg <()> OneSuccess [Int] Buyer Buyer2+-- Goto () 0+-- * BranchSt () NotFound+-- Msg <()> NoBook [] Seller Buyer+-- Msg <()> SellerNoBook [] Buyer Buyer2+-- Goto () 0+-- ,--------------------Idx-----------------+-- Label 0 0+-- Msg <(0,1)> Title [String] Buyer Seller+-- [Branch] 1 Seller+-- * BranchSt () Found+-- Msg <(2,3)> Price [Int] Seller Buyer+-- [Branch] 3 Buyer+-- * BranchSt () Two+-- Msg <(4,5)> PriceToBuyer2 [Int] Buyer Buyer2+-- [Branch] 5 Buyer2+-- * BranchSt () NotSupport+-- Msg <(6,7)> NotSupport1 [] Buyer2 Buyer+-- Msg <(7,8)> TwoNotBuy [] Buyer Seller+-- Goto 8 0+-- * BranchSt () Support+-- Msg <(9,10)> SupportVal [Int] Buyer2 Buyer+-- [Branch] 10 Buyer+-- * BranchSt () Enough+-- Msg <(11,12)> TwoAccept [] Buyer Seller+-- Msg <(12,13)> TwoDate [Int] Seller Buyer+-- Msg <(13,14)> TwoSuccess [Int] Buyer Buyer2+-- Goto 14 0+-- * BranchSt () NotEnough+-- Msg <(15,16)> TwoNotBuy1 [] Buyer Seller+-- Msg <(16,17)> TwoFailed [] Buyer Buyer2+-- Terminal 17+-- * BranchSt () One+-- Msg <(18,19)> OneAccept [] Buyer Seller+-- Msg <(19,20)> OneDate [Int] Seller Buyer+-- Msg <(20,21)> OneSuccess [Int] Buyer Buyer2+-- Goto 21 0+-- * BranchSt () NotFound+-- Msg <(22,23)> NoBook [] Seller Buyer+-- Msg <(23,24)> SellerNoBook [] Buyer Buyer2+-- Goto 24 0+-- ,--------------------ReRank-----------------+-- fromList [(0,0),(1,1),(2,5),(3,2),(4,6),(5,3),(6,7),(7,8),(8,9),(9,10),(10,4),(11,11),(12,12),(13,13),(14,14),(15,15),(16,16),(17,17),(18,18),(19,19),(20,20),(21,21),(22,22),(23,23),(24,24)]+-- ,--------------------Idx-----------------+-- Label 0 0+-- Msg <(0,1)> Title [String] Buyer Seller+-- [Branch] 1 Seller+-- * BranchSt () Found+-- Msg <(5,2)> Price [Int] Seller Buyer+-- [Branch] 2 Buyer+-- * BranchSt () Two+-- Msg <(6,3)> PriceToBuyer2 [Int] Buyer Buyer2+-- [Branch] 3 Buyer2+-- * BranchSt () NotSupport+-- Msg <(7,8)> NotSupport1 [] Buyer2 Buyer+-- Msg <(8,9)> TwoNotBuy [] Buyer Seller+-- Goto 9 0+-- * BranchSt () Support+-- Msg <(10,4)> SupportVal [Int] Buyer2 Buyer+-- [Branch] 4 Buyer+-- * BranchSt () Enough+-- Msg <(11,12)> TwoAccept [] Buyer Seller+-- Msg <(12,13)> TwoDate [Int] Seller Buyer+-- Msg <(13,14)> TwoSuccess [Int] Buyer Buyer2+-- Goto 14 0+-- * BranchSt () NotEnough+-- Msg <(15,16)> TwoNotBuy1 [] Buyer Seller+-- Msg <(16,17)> TwoFailed [] Buyer Buyer2+-- Terminal 17+-- * BranchSt () One+-- Msg <(18,19)> OneAccept [] Buyer Seller+-- Msg <(19,20)> OneDate [Int] Seller Buyer+-- Msg <(20,21)> OneSuccess [Int] Buyer Buyer2+-- Goto 21 0+-- * BranchSt () NotFound+-- Msg <(22,23)> NoBook [] Seller Buyer+-- Msg <(23,24)> SellerNoBook [] Buyer Buyer2+-- Goto 24 0+-- ,--------------------AddNum-----------------+-- Label [0,1,2] 0+-- Msg <([0,1,2],[3,4,5],100)> Title [String] Buyer Seller+-- [Branch] [3,4,5] Seller+-- * BranchSt () Found+-- Msg <([15,16,17],[6,7,8],0)> Price [Int] Seller Buyer+-- [Branch] [6,7,8] Buyer+-- * BranchSt () Two+-- Msg <([18,19,20],[9,10,11],0)> PriceToBuyer2 [Int] Buyer Buyer2+-- [Branch] [9,10,11] Buyer2+-- * BranchSt () NotSupport+-- Msg <([21,22,23],[24,25,26],0)> NotSupport1 [] Buyer2 Buyer+-- Msg <([24,25,26],[27,28,29],1)> TwoNotBuy [] Buyer Seller+-- Goto [27,28,29] 0+-- * BranchSt () Support+-- Msg <([30,31,32],[12,13,14],0)> SupportVal [Int] Buyer2 Buyer+-- [Branch] [12,13,14] Buyer+-- * BranchSt () Enough+-- Msg <([33,34,35],[36,37,38],0)> TwoAccept [] Buyer Seller+-- Msg <([36,37,38],[39,40,41],1)> TwoDate [Int] Seller Buyer+-- Msg <([39,40,41],[42,43,44],2)> TwoSuccess [Int] Buyer Buyer2+-- Goto [42,43,44] 0+-- * BranchSt () NotEnough+-- Msg <([45,46,47],[48,49,50],0)> TwoNotBuy1 [] Buyer Seller+-- Msg <([48,49,50],[51,52,53],1)> TwoFailed [] Buyer Buyer2+-- Terminal [51,52,53]+-- * BranchSt () One+-- Msg <([54,55,56],[57,58,59],0)> OneAccept [] Buyer Seller+-- Msg <([57,58,59],[60,61,62],1)> OneDate [Int] Seller Buyer+-- Msg <([60,61,62],[63,64,65],2)> OneSuccess [Int] Buyer Buyer2+-- Goto [63,64,65] 0+-- * BranchSt () NotFound+-- Msg <([66,67,68],[69,70,71],0)> NoBook [] Seller Buyer+-- Msg <([69,70,71],[72,73,74],1)> SellerNoBook [] Buyer Buyer2+-- Goto [72,73,74] 0+-- ,--------------------GenConst-----------------+-- Label ([0,1,2],0) 0+-- Msg <(([0,1,2],[3,4,5]),(Buyer,Seller),100)> Title [String] Buyer Seller+-- [Branch] [3,4,5] Seller+-- * BranchSt () Found+-- Msg <(([15,16,17],[6,7,8]),(Seller,Buyer),0)> Price [Int] Seller Buyer+-- [Branch] [6,7,8] Buyer+-- * BranchSt () Two+-- Msg <(([18,19,20],[9,10,11]),(Buyer,Buyer2),0)> PriceToBuyer2 [ Int ] Buyer Buyer2+-- [Branch] [9,10,11] Buyer2+-- * BranchSt () NotSupport+-- Msg <(([21,22,23],[24,25,26]),(Buyer2,Buyer),0)> NotSupport1 [ ] Buyer2 Buyer+-- Msg <(([24,25,26],[27,28,29]),(Buyer,Seller),1)> TwoNotBuy [] Buyer Seller+-- Goto ([27,28,29],0) 0+-- * BranchSt () Support+-- Msg <(([30,31,32],[12,13,14]),(Buyer2,Buyer),0)> SupportVal [ Int ] Buyer2 Buyer+-- [Branch] [12,13,14] Buyer+-- * BranchSt () Enough+-- Msg <(([33,34,35],[36,37,38]),(Buyer,Seller),0)> TwoAccept [ ] Buyer Seller+-- Msg <(([36,37,38],[39,40,41]),(Seller,Buyer),1)> TwoDate [ Int ] Seller Buyer+-- Msg <(([39,40,41],[42,43,44]),(Buyer,Buyer2),2)> TwoSuccess [ Int ] Buyer Buyer2+-- Goto ([42,43,44],0) 0+-- * BranchSt () NotEnough+-- Msg <(([45,46,47],[48,49,50]),(Buyer,Seller),0)> TwoNotBuy1 [ ] Buyer Seller+-- Msg <(([48,49,50],[51,52,53]),(Buyer,Buyer2),1)> TwoFailed [ ] Buyer Buyer2+-- Terminal [51,52,53]+-- * BranchSt () One+-- Msg <(([54,55,56],[57,58,59]),(Buyer,Seller),0)> OneAccept [] Buyer Seller+-- Msg <(([57,58,59],[60,61,62]),(Seller,Buyer),1)> OneDate [Int] Seller Buyer+-- Msg <(([60,61,62],[63,64,65]),(Buyer,Buyer2),2)> OneSuccess [ Int ] Buyer Buyer2+-- Goto ([63,64,65],0) 0+-- * BranchSt () NotFound+-- Msg <(([66,67,68],[69,70,71]),(Seller,Buyer),0)> NoBook [] Seller Buyer+-- Msg <(([69,70,71],[72,73,74]),(Buyer,Buyer2),1)> SellerNoBook [] Buyer Buyer2+-- Goto ([72,73,74],0) 0+-- ,--------------------Constrains-----------------+-- fromList [Constraint 0 1,Constraint 2 5,Constraint 3 15,Constraint 5 17,Constraint 16 15,Constraint 17 8,Constraint 7 19,Constraint 8 20,Constraint 18 20,Constraint 19 10,Constraint 9 21,Constraint 10 22,Constraint 23 21,Constraint 22 25,Constraint 24 25,Constraint 26 29,Constraint 27 0,Constraint 28 1,Constraint 29 2,Constraint 9 30,Constraint 10 31,Constraint 32 30,Constraint 31 13,Constraint 13 34,Constraint 14 35,Constraint 33 34,Constraint 35 38,Constraint 37 36,Constraint 38 41,Constraint 39 41,Constraint 40 43,Constraint 42 0,Constraint 43 1,Constraint 44 2,Constraint 13 46,Constraint 14 47,Constraint 45 46,Constraint 47 50,Constraint 48 50,Constraint 49 52,Constraint 51 (-1),Constraint 52 (-1),Constraint 53 (-1),Constraint 7 55,Constraint 8 56,Constraint 54 55,Constraint 56 59,Constraint 58 57,Constraint 59 62,Constraint 60 62,Constraint 61 64,Constraint 63 0,Constraint 64 1,Constraint 65 2,Constraint 3 66,Constraint 5 68,Constraint 67 66,Constraint 68 71,Constraint 69 71,Constraint 70 73,Constraint 72 0,Constraint 73 1,Constraint 74 2]+-- ,--------------------SubMap-----------------+-- fromList [(1,0),(2,1),(3,2),(4,3),(5,1),(6,4),(7,5),(8,1),(9,6),(10,5),(11,7),(12,8),(13,5),(14,9),(15,2),(16,2),(17,1),(18,1),(19,5),(20,1),(21,6),(22,5),(23,6),(24,5),(25,5),(26,1),(27,0),(28,0),(29,1),(30,6),(31,5),(32,6),(33,5),(34,5),(35,9),(36,10),(37,10),(38,9),(39,9),(40,0),(41,9),(42,0),(43,0),(44,1),(45,5),(46,5),(47,9),(48,9),(49,-1),(50,9),(51,-1),(52,-1),(53,-1),(54,5),(55,5),(56,1),(57,11),(58,11),(59,1),(60,1),(61,0),(62,1),(63,0),(64,0),(65,1),(66,2),(67,2),(68,1),(69,1),(70,0),(71,1),(72,0),(73,0),(74,1)]+-- ,--------------------GenConstN-----------------+-- Label ([0,0,1],0) 0+-- Msg <(([0,0,1],[2,3,1]),(Buyer,Seller),100)> Title [String] Buyer Seller+-- [Branch] [2,3,1] Seller+-- * BranchSt () Found+-- Msg <(([2,2,1],[4,5,1]),(Seller,Buyer),0)> Price [Int] Seller Buyer+-- [Branch] [4,5,1] Buyer+-- * BranchSt () Two+-- Msg <(([1,5,1],[6,5,7]),(Buyer,Buyer2),0)> PriceToBuyer2 [Int] Buyer Buyer2+-- [Branch] [6,5,7] Buyer2+-- * BranchSt () NotSupport+-- Msg <(([6,5,6],[5,5,1]),(Buyer2,Buyer),0)> NotSupport1 [] Buyer2 Buyer+-- Msg <(([5,5,1],[0,0,1]),(Buyer,Seller),1)> TwoNotBuy [] Buyer Seller+-- Goto ([0,0,1],0) 0+-- * BranchSt () Support+-- Msg <(([6,5,6],[8,5,9]),(Buyer2,Buyer),0)> SupportVal [Int] Buyer2 Buyer+-- [Branch] [8,5,9] Buyer+-- * BranchSt () Enough+-- Msg <(([5,5,9],[10,10,9]),(Buyer,Seller),0)> TwoAccept [] Buyer Seller+-- Msg <(([10,10,9],[9,0,9]),(Seller,Buyer),1)> TwoDate [Int] Seller Buyer+-- Msg <(([9,0,9],[0,0,1]),(Buyer,Buyer2),2)> TwoSuccess [Int] Buyer Buyer2+-- Goto ([0,0,1],0) 0+-- * BranchSt () NotEnough+-- Msg <(([5,5,9],[9,-1,9]),(Buyer,Seller),0)> TwoNotBuy1 [] Buyer Seller+-- Msg <(([9,-1,9],[-1,-1,-1]),(Buyer,Buyer2),1)> TwoFailed [] Buyer Buyer2+-- Terminal [-1,-1,-1]+-- * BranchSt () One+-- Msg <(([5,5,1],[11,11,1]),(Buyer,Seller),0)> OneAccept [] Buyer Seller+-- Msg <(([11,11,1],[1,0,1]),(Seller,Buyer),1)> OneDate [Int] Seller Buyer+-- Msg <(([1,0,1],[0,0,1]),(Buyer,Buyer2),2)> OneSuccess [Int] Buyer Buyer2+-- Goto ([0,0,1],0) 0+-- * BranchSt () NotFound+-- 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+-- ,--------------------CollectBranchDynVal-----------------+-- fromList [1,2,5,6,9]+-- ,--------------------MsgT-----------------+-- Label ([S0,S0,S1 s],0) 0+-- Msg <([S0,S0,S1 s],(Buyer,Seller),100)> Title [String] Buyer Seller+-- [Branch] [S2 s,S3,S1 s] Seller+-- * BranchSt () Found+-- Msg <([S2 s,S2 Found,S1 s],(Seller,Buyer),0)> Price [Int] Seller Buyer+-- [Branch] [S4,S5 s,S1 s] Buyer+-- * BranchSt () Two+-- Msg <([S1 Two,S5 s,S1 s],(Buyer,Buyer2),0)> PriceToBuyer2 [Int] Buyer Buyer2+-- [Branch] [S6 s,S5 s,S7] Buyer2+-- * BranchSt () NotSupport+-- Msg <([S6 s,S5 s,S6 NotSupport],(Buyer2,Buyer),0)> NotSupport1 [ ] Buyer2 Buyer+-- Msg <([S5 NotSupport,S5 s,S1 s],(Buyer,Seller),1)> TwoNotBuy [ ] Buyer Seller+-- Goto ([S0,S0,S1 s],0) 0+-- * BranchSt () Support+-- Msg <([S6 s,S5 s,S6 Support],(Buyer2,Buyer),0)> SupportVal [ Int ] Buyer2 Buyer+-- [Branch] [S8,S5 s,S9 s] Buyer+-- * BranchSt () Enough+-- Msg <([S5 Enough,S5 s,S9 s],(Buyer,Seller),0)> TwoAccept [] Buyer Seller+-- Msg <([S10,S10,S9 s],(Seller,Buyer),1)> TwoDate [Int] Seller Buyer+-- Msg <([S9 Enough,S0,S9 s],(Buyer,Buyer2),2)> TwoSuccess [ Int ] Buyer Buyer2+-- Goto ([S0,S0,S1 s],0) 0+-- * BranchSt () NotEnough+-- Msg <([S5 NotEnough,S5 s,S9 s],(Buyer,Seller),0)> TwoNotBuy1 [ ] Buyer Seller+-- Msg <([S9 NotEnough,End,S9 s],(Buyer,Buyer2),1)> TwoFailed [ ] Buyer Buyer2+-- Terminal [End,End,End]+-- * BranchSt () One+-- Msg <([S5 One,S5 s,S1 s],(Buyer,Seller),0)> OneAccept [] Buyer Seller+-- Msg <([S11,S11,S1 s],(Seller,Buyer),1)> OneDate [Int] Seller Buyer+-- Msg <([S1 One,S0,S1 s],(Buyer,Buyer2),2)> OneSuccess [Int] Buyer Buyer2+-- Goto ([S0,S0,S1 s],0) 0+-- * BranchSt () NotFound+-- Msg <([S2 s,S2 NotFound,S1 s],(Seller,Buyer),0)> NoBook [] Seller Buyer+-- Msg <([S1 NotFound,S0,S1 s],(Buyer,Buyer2),1)> SellerNoBook [] Buyer Buyer2+-- Goto ([S0,S0,S1 s],0) 0+-- ,--------------------MsgT1-----------------+-- Label ([S0,S0,S1 s],0) 0+-- Msg <((S0,S2 s,S3),(Buyer,Seller),100)> Title [String] Buyer Seller+-- [Branch] [S2 s,S3,S1 s] Seller+-- * BranchSt () Found+-- Msg <((S2 Found,S5 s,S4),(Seller,Buyer),0)> Price [Int] Seller Buyer+-- [Branch] [S4,S5 s,S1 s] Buyer+-- * BranchSt () Two+-- Msg <((S1 Two,S6 s,S7),(Buyer,Buyer2),0)> PriceToBuyer2 [Int] Buyer Buyer2+-- [Branch] [S6 s,S5 s,S7] Buyer2+-- * BranchSt () NotSupport+-- Msg <((S6 NotSupport,S1 s,S5 NotSupport),(Buyer2,Buyer),0)> NotSupport1 [ ] Buyer2 Buyer+-- Msg <((S5 NotSupport,S0,S0),(Buyer,Seller),1)> TwoNotBuy [] Buyer Seller+-- Goto ([S0,S0,S1 s],0) 0+-- * BranchSt () Support+-- Msg <((S6 Support,S9 s,S8),(Buyer2,Buyer),0)> SupportVal [ Int ] Buyer2 Buyer+-- [Branch] [S8,S5 s,S9 s] Buyer+-- * BranchSt () Enough+-- Msg <((S5 Enough,S10,S10),(Buyer,Seller),0)> TwoAccept [] Buyer Seller+-- Msg <((S10,S0,S9 Enough),(Seller,Buyer),1)> TwoDate [Int] Seller Buyer+-- Msg <((S9 Enough,S0,S1 s),(Buyer,Buyer2),2)> TwoSuccess [ Int ] Buyer Buyer2+-- Goto ([S0,S0,S1 s],0) 0+-- * BranchSt () NotEnough+-- Msg <((S5 NotEnough,S9 NotEnough,End),(Buyer,Seller),0)> TwoNotBuy1 [ ] Buyer Seller+-- Msg <((S9 NotEnough,End,End),(Buyer,Buyer2),1)> TwoFailed [ ] Buyer Buyer2+-- Terminal [End,End,End]+-- * BranchSt () One+-- Msg <((S5 One,S11,S11),(Buyer,Seller),0)> OneAccept [] Buyer Seller+-- Msg <((S11,S0,S1 One),(Seller,Buyer),1)> OneDate [Int] Seller Buyer+-- Msg <((S1 One,S0,S1 s),(Buyer,Buyer2),2)> OneSuccess [Int] Buyer Buyer2+-- Goto ([S0,S0,S1 s],0) 0+-- * BranchSt () NotFound+-- Msg <((S2 NotFound,S0,S1 NotFound),(Seller,Buyer),0)> NoBook [] Seller Buyer+-- 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+-- * BranchSt Found+-- Price S2 s<- <-{S2 Found} S1 s+-- [Branch Buyer] S4 S5 s S1 s+-- * BranchSt Two+-- PriceToBuyer2 {S1 Two}-> S5 s ->S1 s+-- [Branch Buyer2] S6 s S5 s S7+-- * BranchSt NotSupport+-- NotSupport1 S6 s<- S5 s <-{S6 NotSupport}+-- TwoNotBuy S5 NotSupport-> ->S5 s S1 s+-- Goto 0 S0 S0 S1 s+-- * BranchSt Support+-- SupportVal S6 s<- S5 s <-{S6 Support}+-- [Branch Buyer] S8 S5 s S9 s+-- * BranchSt Enough+-- TwoAccept {S5 Enough}-> ->S5 s S9 s+-- TwoDate S10<- <-S10 S9 s+-- TwoSuccess S9 Enough-> S0 ->S9 s+-- Goto 0 S0 S0 S1 s+-- * BranchSt NotEnough+-- TwoNotBuy1 {S5 NotEnough}-> ->S5 s S9 s+-- TwoFailed S9 NotEnough-> End ->S9 s+-- ~ Terminal End End End+-- * BranchSt One+-- OneAccept {S5 One}-> ->S5 s S1 s+-- OneDate S11<- <-S11 S1 s+-- OneSuccess S1 One-> S0 ->S1 s+-- Goto 0 S0 S0 S1 s+-- * BranchSt NotFound+-- 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
@@ -0,0 +1,122 @@+cabal-version: 3.0+-- The cabal-version field refers to the version of the .cabal specification,+-- and can be different from the cabal-install (the tool) version and the+-- Cabal (the library) version you are using. As such, the Cabal (the library)+-- version used must be equal or greater than the version stated in this field.+-- Starting from the specification version 2.2, the cabal-version field must be+-- the first thing in the cabal file.++-- Initial package description 'typed-session-state-algorithm' generated by+-- 'cabal init'. For further documentation, see:+-- http://haskell.org/cabal/users-guide/+--+-- The name of the package.+name: typed-session-state-algorithm++-- The package version.+-- See the Haskell package versioning policy (PVP) for standards+-- guiding when and how versions should be incremented.+-- https://pvp.haskell.org+-- PVP summary: +-+------- breaking API changes+-- | | +----- non-breaking API additions+-- | | | +--- code changes with no API change+version: 0.1.0.0++-- A short (one-line) description of the package.+synopsis: Automatically generate status for typed-session.++-- A longer description of the package.+description: Consider the communication process as a state machine, and this lib will generate the required states.++-- The license under which the package is released.+license: MIT++-- The file containing the license text.+license-file: LICENSE++-- The package author(s).+author: sdzx-1++-- An email address to which users can send suggestions, bug reports, and patches.+maintainer: shangdizhixia1993@163.com++category: Algorithm+-- A copyright notice.+-- copyright:+build-type: Simple++-- Extra doc files to be distributed with the package, such as a CHANGELOG or a README.+extra-doc-files: CHANGELOG.md++-- Extra source files to be distributed with the package, such as examples, or a tutorial module.+-- extra-source-files:++common warnings+ ghc-options: -Wall++library+ -- Import common warning flags.+ import: warnings++ -- Modules exported by the library.+ exposed-modules: TypedSession.State.Constraint+ , TypedSession.State.Piple+ , TypedSession.State.Pattern+ , TypedSession.State.GenDoc+ , TypedSession.State.Type+ , TypedSession.State.Utils+ , TypedSession.State.Render+ , TypedSession.State.Parser++ -- Modules included in this library but not exported.+ -- other-modules:++ -- LANGUAGE extensions used by modules in this package.+ -- other-extensions:++ -- Other library packages from which modules are imported.+ build-depends: base >= 4.20.0 && < 4.21,+ containers >= 0.7 && < 0.8,+ fused-effects >= 1.1.2 && < 1.2,+ megaparsec >= 9.6.1 && < 9.7,+ parser-combinators >= 1.3.0 && < 1.4,+ prettyprinter >= 1.7.1 && < 1.8,+++ -- Directories containing source files.+ hs-source-dirs: src++ -- Base language which the package is written in.+ default-language: Haskell2010++test-suite typed-session-state-algorithm-test+ -- Import common warning flags.+ import: warnings++ -- Base language which the package is written in.+ default-language: Haskell2010++ -- Modules included in this executable, other than Main.+ -- other-modules:++ -- LANGUAGE extensions used by modules in this package.+ -- other-extensions:++ -- The interface type and version of the test suite.+ type: exitcode-stdio-1.0++ -- Directories containing source files.+ hs-source-dirs: test++ -- The entrypoint to the test suite.+ main-is: Main.hs++ -- Test dependencies.+ build-depends:+ base >=4.17.2.1+ , typed-session-state-algorithm+ , raw-strings-qq++source-repository head+ type: git+ location: https://github.com/sdzx-1/typed-session-state-algorithm