typed-session 0.1.1.0 → 0.1.2.0
raw patch · 5 files changed
+242/−267 lines, 5 filesdep ~template-haskelldep ~typed-session-state-algorithmPVP: major bump suggested
API removals or changes: PVP suggests a major version bump
Dependency ranges changed: template-haskell, typed-session-state-algorithm
API changes (from Hackage documentation)
- TypedSession.TH: addS :: Name -> Name
+ TypedSession.Core: liftConstructor :: forall (m :: Type -> Type) k ia (st' :: k) role' (r :: role') (st :: k). Applicative m => ia st' -> Peer role' k r m ia st
- TypedSession.TH: protDecsAndMsgDecs :: (Show r, Show bst) => String -> Name -> Name -> PipleResult r bst -> Q [Dec]
+ TypedSession.TH: protDecsAndMsgDecs :: (Show r, Show bst) => String -> Name -> Name -> PipeResult r bst -> Q [Dec]
Files
- src/TypedSession/Core.hs +4/−1
- src/TypedSession/TH.hs +186/−165
- test/Book3/Peer.hs +20/−37
- test/Book3/Protocol.hs +29/−61
- typed-session.cabal +3/−3
src/TypedSession/Core.hs view
@@ -247,8 +247,11 @@ await = Await ireturn {- |-Lift any m to Peer role' ps r m, which is an application of LiftM. +Lift any m to Peer role' ps r m, which is an application of LiftM. Note that the state of `ts` has not changed. -} liftm :: (Functor m) => m a -> Peer role' ps r m (At a ts) ts liftm m = LiftM (returnAt <$> m)++liftConstructor :: (Applicative m) => ia st' -> Peer role' k r m ia st+liftConstructor a = LiftM $ pure $ ireturn a
src/TypedSession/TH.hs view
@@ -4,6 +4,7 @@ {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MagicHash #-} {-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-}@@ -17,14 +18,17 @@ import Control.Monad (forM) import Data.Either (fromRight)+import Data.IFunctor (Sing, SingI (..)) import Data.Kind import qualified Data.Set as Set+import GHC.Exts (DataToTag (..), Int (..)) import Language.Haskell.TH hiding (Type) import qualified Language.Haskell.TH as TH import Language.Haskell.TH.Quote-import TypedSession.State.GenDoc+import TypedSession.Core (SingToInt (..))+import qualified TypedSession.Core as TSC import TypedSession.State.Parser (runProtocolParser)-import TypedSession.State.Piple (PipleResult (..), piple)+import TypedSession.State.Pipeline (PipeResult (..), genGraph, pipe) import TypedSession.State.Render import TypedSession.State.Type (BranchSt (..), Creat, MsgOrLabel (..), MsgT1, Protocol (..), ProtocolError, T (..)) @@ -33,46 +37,51 @@ res <- reify name case res of TyConI (DataD [] dName [] Nothing cons _) -> do- a <- newName "a"- x <- newName "x"- pure $- [ DataD- []- (addS dName)- [KindedTV a BndrReq (ConT dName)]- Nothing- [GadtC [addS n] [] (AppT (ConT (addS dName)) (PromotedT n)) | NormalC n [] <- cons]- []- , TySynInstD (TySynEqn Nothing (ConT (mkName "Data.IFunctor.Sing")) (ConT (addS dName)))- ]- ++ [ InstanceD- Nothing- []- (AppT (ConT $ mkName "Data.IFunctor.SingI") (PromotedT n))- [FunD (mkName "sing") [Clause [] (NormalB (ConE (addS n))) []]]- | NormalC n [] <- cons- ]- ++ [ InstanceD- Nothing- []- (AppT (ConT (mkName "TypedSession.Core.SingToInt")) (ConT name))- [ FunD- (mkName "singToInt")- [Clause [VarP x] (NormalB (AppE (ConE (mkName "I#")) (AppE (VarE $ mkName "dataToTag#") (VarE x)))) []]- ]- ]- _ -> error "np"+ aVar <- newName "a"+ xVar <- newName "x"+ let+ addPerfixS :: Name -> Name+ addPerfixS vname =+ let n = (nameBase vname)+ in mkName ("S" <> n) -addS :: Name -> Name-addS name =- let n = (nameBase name)- in mkName ("S" <> n)+ roleSingleton =+ [ DataD+ []+ (addPerfixS dName)+ [KindedTV aVar BndrReq (ConT dName)]+ Nothing+ [GadtC [addPerfixS n] [] (AppT (ConT (addPerfixS dName)) (PromotedT n)) | NormalC n [] <- cons]+ []+ ]+ singToSRole = [TySynInstD (TySynEqn Nothing (ConT ''Sing) (ConT (addPerfixS dName)))]+ instanceSingI =+ [ InstanceD+ Nothing+ []+ (AppT (ConT ''SingI) (PromotedT n))+ [FunD 'sing [Clause [] (NormalB (ConE (addPerfixS n))) []]]+ | NormalC n [] <- cons+ ]+ instanceSingToInt =+ [ InstanceD+ Nothing+ []+ (AppT (ConT ''SingToInt) (ConT name))+ [ FunD+ 'singToInt+ [Clause [VarP xVar] (NormalB (AppE (ConE 'I#) (AppE (VarE 'dataToTag#) (VarE xVar)))) []]+ ]+ ]+ pure $ roleSingleton ++ singToSRole ++ instanceSingI ++ instanceSingToInt+ _ -> error $ "Name: " ++ show name ++ " is not a data constructor" -protDecsAndMsgDecs :: forall r bst. (Show r, Show bst) => String -> Name -> Name -> PipleResult r bst -> Q [Dec]-protDecsAndMsgDecs protN roleName bstName PipleResult{msgT1, dnySet, stBound = (fromVal, toVal)} = do- sVar <- newName "s"+protDecsAndMsgDecs :: forall r bst. (Show r, Show bst) => String -> Name -> Name -> PipeResult r bst -> Q [Dec]+protDecsAndMsgDecs protN roleName bstName PipeResult{msgT1, dnySet, stBound = (fromVal, toVal), branchResultTypeInfo} = do let protName = mkName protN protSName = mkName ("S" <> protN)+ mkSiName i = mkName $ "S" <> show i+ mkSSiName i = mkName $ "SS" <> show i genConstr i = if i == -1 then NormalC (mkName "End") []@@ -80,10 +89,30 @@ if i `Set.member` dnySet then NormalC- (mkName $ "S" <> show i)+ (mkSiName i) [(Bang NoSourceUnpackedness NoSourceStrictness, ConT bstName)]- else NormalC (mkName $ "S" <> show i) []- genSConstr i =+ else NormalC (mkSiName i) []+ -- generate protocol data type+ dataProt = [DataD [] protName [] Nothing [genConstr i | i <- [fromVal .. toVal]] []]++ let tAnyToType :: Name -> T bst -> TH.Type+ tAnyToType s = \case+ TNum i -> PromotedT (mkSiName i)+ BstList i bst -> AppT (PromotedT (mkSiName i)) (PromotedT (mkName (show bst)))+ TAny i -> AppT (PromotedT (mkSiName i)) (VarT s)+ TEnd -> PromotedT $ mkName "End"+ mkArgs args =+ [ ( Bang NoSourceUnpackedness NoSourceStrictness+ , case ag of+ [] -> error "np"+ (x : xs) -> foldl' AppT (ConT (mkName x)) (map (ConT . mkName) xs)+ )+ | ag <- args+ ]++ sVar <- newName "s"+ aVar <- newName "a"+ let genSConstr i = if i == -1 then GadtC [mkName "SEnd"] [] (AppT (ConT protSName) (PromotedT (mkName "End")))@@ -94,79 +123,68 @@ [KindedTV sVar SpecifiedSpec (ConT bstName)] [] ( GadtC- [mkName $ "SS" <> show i]+ [mkSSiName i] []- (AppT (ConT protSName) (AppT (PromotedT $ mkName $ "S" <> show i) (VarT sVar)))+ (AppT (ConT protSName) (AppT (PromotedT $ mkSiName i) (VarT sVar))) ) else- GadtC [mkName $ "SS" <> show i] [] (AppT (ConT protSName) (PromotedT $ mkName $ "S" <> show i))+ GadtC [mkSSiName i] [] (AppT (ConT protSName) (PromotedT $ mkSiName i))+ -- generate protocol singleton data type+ dataSingletonProt = [DataD [] protSName [KindedTV aVar BndrReq (ConT protName)] Nothing [genSConstr i | i <- [fromVal .. toVal]] []] - isTAny :: T bst -> Bool- isTAny = \case- TAny _ -> True- _ -> False+ -- generate type family Sing to Singleton protocol+ let singSingletonProt = [TySynInstD (TySynEqn Nothing (ConT ''Sing) (ConT protSName))] - mkInstanceMsg :: Name -> Protocol (MsgT1 r bst) r bst -> Q [Con]- mkInstanceMsg s = \case- Msg ((a, b, c), (from, to), _) constr args _ _ :> prots -> do- let tAnyToType :: T bst -> TH.Type- tAnyToType = \case- TNum i -> PromotedT (mkName $ "S" <> show i)- BstList i bst -> AppT (PromotedT (mkName $ "S" <> show i)) (PromotedT (mkName (show bst)))- TAny i -> AppT (PromotedT (mkName $ "S" <> show i)) (VarT s)- TEnd -> PromotedT $ mkName "End"+ aVar1 <- newName "a"+ let branchResultDatas =+ [ DataD+ []+ dataName+ [KindedTV aVar1 BndrReq (ConT protName)]+ Nothing+ [ GadtC [constrName] (mkArgs args) (AppT (ConT dataName) (tAnyToType (mkName "s") t))+ | (bst, args, t) <- constrs+ , let constrName = mkName ("BranchSt_" <> show bst)+ ]+ []+ | (name, constrs) <- branchResultTypeInfo+ , let dataName = mkName name+ ] - let mkTName =- ( AppT- ( AppT- ( AppT- ( AppT- ( AppT- (ConT $ mkName "Msg")- (ConT roleName)- )- (ConT protName)- )- (tAnyToType a)- )- (AppT (AppT (PromotedTupleT 2) (PromotedT (mkName (show from)))) (tAnyToType b))- )- (AppT (AppT (PromotedTupleT 2) (PromotedT (mkName (show to)))) (tAnyToType c))+ s1 <- newName "s1"+ -- generate instance SingI+ let instanceSingI =+ [ InstanceD+ Nothing+ []+ ( AppT+ (ConT ''SingI)+ ( if i == -1+ then PromotedT (mkName "End")+ else+ if i `Set.member` dnySet+ then SigT (AppT (PromotedT (mkSiName i)) (VarT s1)) (ConT protName)+ else PromotedT (mkSiName i) )- let val =- let gadtc =- GadtC- [mkName constr]- [ ( Bang NoSourceUnpackedness NoSourceStrictness- , case words ag of- [] -> error "np"- (x : xs) -> foldl' AppT (ConT (mkName x)) (map (ConT . mkName) xs)- )- | ag <- args- ]- mkTName- in if any isTAny [a, b, c]- then- ForallC- [KindedTV s SpecifiedSpec (ConT bstName)]- []- gadtc- else gadtc- res <- mkInstanceMsg s prots- pure (val : res)- Label _ _ :> prots -> mkInstanceMsg s prots- Branch _ _ ls -> do- ls' <- forM ls $ \(BranchSt _ _ prot) -> mkInstanceMsg s prot- pure $ concat ls'- _ -> pure []+ )+ [FunD 'sing [Clause [] (NormalB (ConE (mkName $ "S" <> (if i == -1 then "End" else ("S" <> show i))))) []]]+ | i <- [fromVal .. toVal]+ ] - a <- newName "a"- s1 <- newName "s1"- x <- newName "x"+ xVar <- newName "x"+ -- generate instance SingToInt+ let instanceSingToInt =+ [ InstanceD+ Nothing+ []+ (AppT (ConT ''SingToInt) (ConT protName))+ [ FunD 'singToInt [Clause [VarP xVar] (NormalB (AppE (ConE 'I#) (AppE (VarE 'dataToTag#) (VarE xVar)))) []]+ ]+ ] - -- make instance Done- res <- reify roleName- instDoneDesc <- case res of+ -- make instance type family Done+ roleRes <- reify roleName+ instDoneDesc <- case roleRes of TyConI (DataD [] _ [] Nothing cons _) -> do pure [ TySynInstD@@ -177,55 +195,56 @@ ) | NormalC n [] <- cons ]- _ -> error "np"+ _ -> error $ "Name: " ++ show roleName ++ " is not a data constructor" - -- make instance msg- ss <- newName "s"- instMsgDesc <- mkInstanceMsg ss (msgT1)+ let typeListT :: [TH.Type] -> TH.Type+ typeListT = foldl1 AppT + isTAny :: T bst -> Bool+ isTAny = \case+ TAny _ -> True+ _ -> False++ mkDataInstanceMsg :: Name -> Protocol (MsgT1 r bst) r bst -> Q [Con]+ mkDataInstanceMsg s = \case+ Msg ((a, b, c), (from, to), _) constr args _ _ :> prots -> do+ let mkTName =+ typeListT+ [ ConT ''TSC.Msg+ , ConT roleName+ , ConT protName+ , tAnyToType s a+ , typeListT [PromotedTupleT 2, PromotedT (mkName (show from)), tAnyToType s b]+ , typeListT [PromotedTupleT 2, PromotedT (mkName (show to)), tAnyToType s c]+ ]+ let val =+ let gadtc =+ GadtC+ [mkName constr]+ (mkArgs args)+ mkTName+ in if any isTAny [a, b, c]+ then ForallC [KindedTV s SpecifiedSpec (ConT bstName)] [] gadtc+ else gadtc+ vals <- mkDataInstanceMsg s prots+ pure (val : vals)+ Label _ _ :> prots -> mkDataInstanceMsg s prots+ Branch _ _ _ ls -> do+ ls' <- forM ls $ \(BranchSt _ _ _ prot) -> mkDataInstanceMsg s prot+ pure $ concat ls'+ _ -> pure []++ -- make data instance Msg+ ssVar <- newName "s"+ instMsgDesc <- mkDataInstanceMsg ssVar (msgT1) fromVar <- newName "from" sendVar <- newName "send" recvVar <- newName "recv"- pure $- [ DataD [] protName [] Nothing [genConstr i | i <- [fromVal .. toVal]] []- ]- ++ [DataD [] protSName [KindedTV a BndrReq (ConT protName)] Nothing [genSConstr i | i <- [fromVal .. toVal]] []]- ++ [TySynInstD (TySynEqn Nothing (ConT (mkName "Data.IFunctor.Sing")) (ConT protSName))]- ++ [ InstanceD- Nothing- []- ( AppT- (ConT $ mkName "Data.IFunctor.SingI")- ( if i == -1- then PromotedT (mkName "End")- else- if i `Set.member` dnySet- then SigT (AppT (PromotedT (mkName ("S" <> show i))) (VarT s1)) (ConT protName)- else PromotedT (mkName ("S" <> show i))- )- )- [ FunD- (mkName "sing")- [Clause [] (NormalB (ConE (mkName $ "S" <> (if i == -1 then "End" else ("S" <> show i))))) []]- ]- | i <- [fromVal .. toVal]- ]- ++ [ InstanceD- Nothing- []- (AppT (ConT (mkName "TypedSession.Core.SingToInt")) (ConT protName))- [ FunD- (mkName "singToInt")- [Clause [VarP x] (NormalB (AppE (ConE (mkName "I#")) (AppE (VarE $ mkName "dataToTag#") (VarE x)))) []]- ]- ]- ++ [ InstanceD+ let instanceMsg =+ [ InstanceD Nothing []- ( AppT- (AppT (ConT (mkName "TypedSession.Core.Protocol")) (ConT roleName))- (ConT protName)- )+ (AppT (AppT (ConT ''TSC.Protocol) (ConT roleName)) (ConT protName)) ( instDoneDesc ++ let ct1 = (AppT (AppT (TupleT 2) (ConT roleName)) (ConT protName)) in [ DataInstD@@ -236,29 +255,31 @@ , KindedTV recvVar () ct1 ] )- ( AppT- ( AppT- ( AppT- ( AppT- ( AppT- (ConT $ mkName "Msg")- (ConT roleName)- )- (ConT protName)- )- (SigT (VarT fromVar) (ConT protName))- )- (SigT (VarT sendVar) ct1)- )- (SigT (VarT recvVar) ct1)+ ( typeListT+ [ ConT ''TSC.Msg+ , ConT roleName+ , ConT protName+ , (SigT (VarT fromVar) (ConT protName))+ , (SigT (VarT sendVar) ct1)+ , (SigT (VarT recvVar) ct1)+ ] ) Nothing instMsgDesc [] ] )- ]+ ] + pure $+ dataProt+ ++ dataSingletonProt+ ++ singSingletonProt+ ++ branchResultDatas+ ++ instanceSingI+ ++ instanceSingToInt+ ++ instanceMsg+ protocol :: forall r bst . ( Enum r@@ -281,10 +302,10 @@ parseOrThrow :: String -> Q [Dec] parseOrThrow st = case runProtocolParser @r @bst st of Left e -> fail (show e)- Right protCreat -> case piple protCreat of+ Right protCreat -> case pipe protCreat of Left e -> fail (show e) Right pipResult -> do- let graphStr = genGraph @r @bst defaultStrFilEnv pipResult+ let graphStr = genGraph @r @bst pipResult runIO $ do writeFile (protN <> ".prot") graphStr putStrLn graphStr
test/Book3/Peer.hs view
@@ -19,9 +19,8 @@ import Book3.Type import Control.Algebra (Has) import Control.Effect.Random (Random, uniform)-import Data.IFunctor (At (..), ireturn, returnAt)+import Data.IFunctor (At (..), returnAt) import qualified Data.IFunctor as I-import Data.Kind import TypedSession.Core budget :: Int@@ -29,34 +28,26 @@ type Date = Int -data CheckPriceResult :: Book -> Type where- Yes :: CheckPriceResult (S5 Enough)- No :: CheckPriceResult (S5 NotEnough)- checkPrice :: (Has Random sig m) => Int -> Int- -> Peer BookRole Book Buyer m CheckPriceResult S8+ -> Peer BookRole Book Buyer m EnoughOrNotEnough S8 checkPrice _i _h = I.do At b <- liftm $ uniform @Bool if b- then LiftM $ pure (ireturn Yes)- else LiftM $ pure (ireturn No)--data OT :: Book -> Type where- OTOne :: OT (S5 One)- OTTwo :: OT (S1 Two)+ then liftConstructor BranchSt_Enough+ else liftConstructor BranchSt_NotEnough choiceOT :: (Has Random sig m) => Int- -> Peer BookRole Book Buyer m OT S4+ -> Peer BookRole Book Buyer m OneOrTwo S4 choiceOT _i = I.do At b <- liftm $ uniform @Bool if b- then LiftM $ pure $ ireturn OTOne- else LiftM $ pure $ ireturn OTTwo+ then liftConstructor BranchSt_One+ else liftConstructor BranchSt_Two buyerPeer :: (Has Random sig m)@@ -69,12 +60,12 @@ returnAt Nothing Recv (Price i) -> I.do choiceOT i I.>>= \case- OTOne -> I.do+ BranchSt_One -> I.do yield OneAccept Recv (OneDate d) <- await yield (OneSuccess d) returnAt $ Just d- OTTwo -> f1+ BranchSt_Two -> f1 where f1 :: (Has Random sig m)@@ -87,29 +78,25 @@ returnAt Nothing Recv (SupportVal h) -> I.do checkPrice 10 h I.>>= \case- Yes -> I.do+ BranchSt_Enough -> I.do yield TwoAccept Recv (TwoDate d) <- await yield (TwoSuccess d) returnAt (Just d)- No -> I.do+ BranchSt_NotEnough -> I.do yield TwoNotBuy1 yield TwoFailed returnAt Nothing -data BuySupp :: Book -> Type where- BNS :: BuySupp (S6 NotSupport)- BS :: BuySupp (S6 Support)- choiceB :: (Has Random sig m) => Int- -> Peer BookRole Book Buyer2 m BuySupp S7+ -> Peer BookRole Book Buyer2 m SupportOrNotSupport S7 choiceB _i = I.do At b <- liftm $ uniform @Bool if b- then LiftM $ pure $ ireturn BNS- else LiftM $ pure $ ireturn BS+ then liftConstructor BranchSt_Support+ else liftConstructor BranchSt_NotSupport buyer2Peer :: (Has Random sig m)@@ -120,19 +107,15 @@ Recv (OneSuccess d) -> returnAt (Just d) Recv (PriceToBuyer2 i) -> I.do choiceB i I.>>= \case- BNS -> I.do+ BranchSt_NotSupport -> I.do yield NotSupport1 returnAt Nothing- BS -> I.do+ BranchSt_Support -> I.do yield (SupportVal (i `div` 2)) await I.>>= \case Recv (TwoSuccess d) -> returnAt $ Just d Recv TwoFailed -> returnAt Nothing -data FindBookResult :: Book -> Type where- NotFound' :: FindBookResult (S2 NotFound)- Found' :: FindBookResult (S2 Found)- findBook :: (Has Random sig m) => String@@ -140,8 +123,8 @@ findBook _st = I.do At b <- liftm $ uniform @Bool if b- then LiftM $ pure (ireturn Found')- else LiftM $ pure (ireturn NotFound')+ then liftConstructor BranchSt_Found+ else liftConstructor BranchSt_NotFound sellerPeer :: (Has Random sig m)@@ -149,8 +132,8 @@ sellerPeer = I.do Recv (Title st) <- await findBook st I.>>= \case- NotFound' -> yield NoBook- Found' -> I.do+ BranchSt_NotFound -> yield NoBook+ BranchSt_Found -> I.do yield (Price 30) await I.>>= \case Recv OneAccept -> yield (OneDate 100)
test/Book3/Protocol.hs view
@@ -11,50 +11,49 @@ {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# OPTIONS_GHC -Wno-orphans #-}+{-# OPTIONS_GHC -ddump-splices #-} module Book3.Protocol where import Book3.Type -import Data.IFunctor (Sing, SingI (sing))-import GHC.Exts (Int (..), dataToTag#) import TypedSession.Codec import TypedSession.Core [bookProtocol| Label 0- Msg "Title" ["String"] Buyer Seller- Branch Seller {- BranchSt NotFound- Msg "NoBook" [] Seller Buyer- Msg "SellerNoBook" [] Buyer Buyer2+ Msg Title [String] Buyer Seller+ Branch Seller FindBookResult {+ BranchSt NotFound []+ Msg NoBook [] Seller Buyer+ Msg SellerNoBook [] Buyer Buyer2 Terminal- BranchSt Found - Msg "Price" ["Int"] Seller Buyer- Branch Buyer {- BranchSt One - Msg "OneAccept" [] Buyer Seller- Msg "OneDate" ["Int"] Seller Buyer- Msg "OneSuccess" ["Int"] Buyer Buyer2+ BranchSt Found []+ Msg Price [Int] Seller Buyer+ Branch Buyer OneOrTwo {+ BranchSt One []+ Msg OneAccept [] Buyer Seller+ Msg OneDate [Int] Seller Buyer+ Msg OneSuccess [Int] Buyer Buyer2 Terminal- BranchSt Two - Msg "PriceToBuyer2" ["Int"] Buyer Buyer2- Branch Buyer2 {- BranchSt NotSupport - Msg "NotSupport1" [] Buyer2 Buyer- Msg "TwoNotBuy" [] Buyer Seller+ BranchSt Two []+ Msg PriceToBuyer2 [Int] Buyer Buyer2+ Branch Buyer2 SupportOrNotSupport {+ BranchSt NotSupport []+ Msg NotSupport1 [] Buyer2 Buyer+ Msg TwoNotBuy [] Buyer Seller Terminal- 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+ BranchSt Support []+ Msg SupportVal [Int] Buyer2 Buyer+ Branch Buyer EnoughOrNotEnough {+ BranchSt Enough []+ Msg TwoAccept [] Buyer Seller+ Msg TwoDate [Int] Seller Buyer+ Msg TwoSuccess [Int] Buyer Buyer2 Terminal- BranchSt NotEnough - Msg "TwoNotBuy1" [] Buyer Seller- Msg "TwoFailed" [] Buyer Buyer2+ BranchSt NotEnough []+ Msg TwoNotBuy1 [] Buyer Seller+ Msg TwoFailed [] Buyer Buyer2 Terminal } }@@ -62,37 +61,6 @@ } |]--{-------------------------------------------------Buyer-------------------------Seller------------------------Buyer2-LABEL 0 S0 S0 S1 s- Title S0-> ->S0 S1 s- [Branch Seller] S2 s S3 S1 s- NoBook S2 s<- <-{S2 NotFound} S1 s- SellerNoBook S1 NotFound-> End ->S1 s- Terminal End End End- Price S2 s<- <-{S2 Found} S1 s- [Branch Buyer] S4 S5 s S1 s- OneAccept {S5 One}-> ->S5 s S1 s- OneDate S10<- <-S10 S1 s- OneSuccess S1 One-> End ->S1 s- Terminal End End End- 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 End- Terminal End End End- SupportVal S6 s<- S5 s <-{S6 Support}- [Branch Buyer] S8 S5 s S9 s- TwoAccept {S5 Enough}-> ->S5 s S9 s- TwoDate S11<- <-S11 S9 s- TwoSuccess S9 Enough-> End ->S9 s- Terminal End End End- TwoNotBuy1 {S5 NotEnough}-> ->S5 s S9 s- TwoFailed S9 NotEnough-> End ->S9 s- Terminal End End End---} encodeMsg :: Encode BookRole Book (AnyMsg BookRole Book) encodeMsg = Encode $ \x -> case x of
typed-session.cabal view
@@ -20,7 +20,7 @@ -- PVP summary: +-+------- breaking API changes -- | | +----- non-breaking API additions -- | | | +--- code changes with no API change-version: 0.1.1.0+version: 0.1.2.0 -- A short (one-line) description of the package. synopsis: typed session framework@@ -78,8 +78,8 @@ build-depends: base >= 4.20.0 && < 4.21 , containers >= 0.7 && < 0.8 , io-classes >= 1.5.0 && < 1.6- , template-haskell- , typed-session-state-algorithm+ , template-haskell >= 2.22.0 && < 2.23+ , typed-session-state-algorithm >= 0.4.0 && < 0.5 -- Directories containing source files. hs-source-dirs: src