typed-session 0.1.3.0 → 0.2.0.0

raw patch · 12 files changed

+102/−1149 lines, 12 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• CHANGELOG.md +2/−0
• src/TypedSession/Codec.hs +1/−1
• src/TypedSession/Core.hs +30/−25
• src/TypedSession/Driver.hs +6/−6
• src/TypedSession/TH.hs +31/−24
• test/Book.hs +0/−232
• test/Book1.hs +0/−281
• test/Book2.hs +0/−342
• test/Book3/Peer.hs +30/−35
• test/Book3/Protocol.hs +0/−1
• test/PingPong.hs +0/−196
• typed-session.cabal +2/−6

@@ -1,4 +1,6 @@ # Revision history for typed-session+## 0.2.0.0+* Remove data Recv  ## 0.1.1.0 * add protocol TH

@@ -21,7 +21,7 @@ newtype Encode role' ps bytes = Encode   { encode       :: forall (send :: role') (recv :: role') (st :: ps) (st' :: ps) (st'' :: ps)-       . Msg role' ps st '(send, st') '(recv, st'')+       . Msg role' ps st send st' recv st''       -> bytes   } 

@@ -72,15 +72,25 @@ Describe the state of each role when it terminates.  @-data Msg role' ps (from :: ps) (sendAndSt :: (role', ps)) (recvAndSt :: (role', ps))+data+  Msg+    role'+    ps+    (fromSt :: ps)+    (sender :: role')+    (senderNewSt :: ps)+    (receiver :: role')+    (receiverNewSt :: ps) @ * role': the type of the role. * ps: the type of the state machine.-* ​​from: when sending a message, the sender is in this state,+* ​​fromSt: when sending a message, the sender is in this state, where the receiver may be in this state, or a more generalized state related to this state. For example, the sender is in state (S1 [True]), and the receiver is in state (S1 s).-* sendAndSt: the role that sends the message and the state of the role after sending the message.-* recvAndSt: the role that receives the message and the state of the role after receiving the message.+* sender: the role that sends the message+* senderNewSt: the state of the role after sending the message+* receiver: the role that receives the message+* receiverNewSt: the state of the role after receiving the message  There are two principles to follow when designing the state of Msg: @@ -101,20 +111,15 @@ -} class (SingToInt role', SingToInt ps) => Protocol role' ps where   type Done (sr :: role') :: ps-  data Msg role' ps (from :: ps) (sendAndSt :: (role', ps)) (recvAndSt :: (role', ps))--{- |-Package Msg and extract the required type.--@-Msg  role' ps from '(send, sps) '(recv,     rps)-Recv role' ps                     recv from rps-@--}-data Recv role' ps recv from to where-  Recv-    :: Msg role' ps from '(send, sps) '(recv, rps)-    -> Recv role' ps recv from rps+  data+    Msg+      role'+      ps+      (fromSt :: ps)+      (sender :: role')+      (senderNewSt :: ps)+      (receiver :: role')+      (receiverNewSt :: ps)  {- | Messages received from the outside are placed in MsgCache. When interpreting@@ -132,13 +137,13 @@        , SingToInt role'        , SingToInt ps        )-    => Msg role' ps st '(send, st') '(recv, st'')+    => Msg role' ps st send st' recv st''     -> AnyMsg role' ps  msgFromStSing   :: forall role' ps st send recv st' st''    . (SingI recv, SingI st)-  => Msg role' ps st '(send, st') '(recv, st'')+  => Msg role' ps st send st' recv st''   -> Sing st msgFromStSing _ = sing @st @@ -178,7 +183,7 @@      , SingI from      , SingToInt ps      )-  => (Recv role' ps recv from ~> Peer role' ps recv m ia)+  => (Msg role' ps from send sps recv ~> Peer role' ps recv m ia)   -> Peer role' ps recv m ia from @ @@ -194,7 +199,7 @@        , SingI from        , SingToInt ps        )-    => Msg role' ps from '(send, sps) '(recv, rps)+    => Msg role' ps from send sps recv rps     -> Peer role' ps send m ia sps     -> Peer role' ps send m ia from   Await@@ -202,7 +207,7 @@        , SingI from        , SingToInt ps        )-    => (Recv role' ps recv from ~> Peer role' ps recv m ia)+    => (Msg role' ps from send sps recv ~> Peer role' ps recv m ia)     -> Peer role' ps recv m ia from  instance (Functor m) => IMonadFail (Peer role' ps r m) where@@ -232,7 +237,7 @@      , SingI from      , SingToInt ps      )-  => Msg role' ps from '(send, sps) '(recv, rps)+  => Msg role' ps from send sps recv rps   -> Peer role' ps send m (At () sps) from yield msg = Yield msg (returnAt ()) @@ -245,7 +250,7 @@      , SingI from      , SingToInt ps      )-  => Peer role' ps recv m (Recv role' ps recv from) from+  => Peer role' ps recv m (Msg role' ps from send sps recv) from await = Await ireturn  {- |

@@ -3,6 +3,7 @@ {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE NumericUnderscores #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-}@@ -10,7 +11,6 @@ {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -Wno-unused-do-bind #-}-{-# LANGUAGE NumericUnderscores #-}  {- | Schematic diagram of the communication structure of three roles through typed-session:@@ -56,7 +56,7 @@          , SingToInt role'          )       => Sing recv-      -> Msg role' ps st '(send, st') '(recv, st'')+      -> Msg role' ps st send st' recv st''       -> m ()   , recvMsg       :: forall (st' :: ps)@@ -85,12 +85,12 @@     -> m a   go (IReturn (At a)) = pure a   go (LiftM k) = k >>= go-  go (Yield (msg :: Msg role' ps (st' :: ps) '(r, sps) '(recv :: role', rps)) k) = do+  go (Yield (msg :: Msg role' ps st' r sps recv rps) k) = do     sendMsg (sing @recv) msg     go k-  go (Await (k :: (Recv role' ps r st' I.~> Peer role' ps r m ia))) = do+  go (Await (k :: (Msg role' ps st' send sps r I.~> Peer role' ps r m ia))) = do     AnyMsg msg <- recvMsg (sing @st')-    go (k $ unsafeCoerce (Recv msg))+    go (k $ unsafeCoerce msg)  {- | A wrapper around AnyMsg that represents sending and receiving Msg.@@ -158,7 +158,7 @@        , SingToInt role'        )     => Sing recv-    -> Msg role' ps from '(send, st) '(recv, st1)+    -> Msg role' ps from send st recv st1     -> m ()   sendMsg role msg = liftFun $ do     case IntMap.lookup (singToInt role) sendMap of

@@ -231,8 +231,10 @@                   , 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]+                  , PromotedT (mkName (show from))+                  , tAnyToType s b+                  , PromotedT (mkName (show to))+                  , tAnyToType s c                   ]           let val =                 let gadtc =@@ -256,35 +258,40 @@   instMsgDesc <- mkDataInstanceMsg ssVar (msgT1)   fromVar <- newName "from"   sendVar <- newName "send"+  sendNewStVar <- newName "sendNewSt"   recvVar <- newName "recv"+  receiverNewStVar <- newName "receiverNewSt"   let instanceMsg =         [ InstanceD             Nothing             []             (AppT (AppT (ConT ''TSC.Protocol) (ConT roleName)) (ConT protName))             ( instDoneDesc-                ++ let ct1 = (AppT (AppT (TupleT 2) (ConT roleName)) (ConT protName))-                    in [ DataInstD-                          []-                          ( Just-                              [ KindedTV fromVar () (ConT protName)-                              , KindedTV sendVar () ct1-                              , KindedTV 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-                          []-                       ]+                ++ [ DataInstD+                      []+                      ( Just+                          [ KindedTV fromVar () (ConT protName)+                          , KindedTV sendVar () (ConT roleName)+                          , KindedTV sendNewStVar () (ConT protName)+                          , KindedTV recvVar () (ConT roleName)+                          , KindedTV receiverNewStVar () (ConT protName)+                          ]+                      )+                      ( typeListT+                          [ ConT ''TSC.Msg+                          , ConT roleName+                          , ConT protName+                          , (SigT (VarT fromVar) (ConT protName))+                          , (SigT (VarT sendVar) (ConT roleName))+                          , (SigT (VarT sendNewStVar) (ConT protName))+                          , (SigT (VarT recvVar) (ConT roleName))+                          , (SigT (VarT receiverNewStVar) (ConT protName))+                          ]+                      )+                      Nothing+                      instMsgDesc+                      []+                   ]             )         ] 

@@ -1,232 +0,0 @@-{-# LANGUAGE AllowAmbiguousTypes #-}-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE LambdaCase #-}-{-# LANGUAGE MagicHash #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE NamedFieldPuns #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE QualifiedDo #-}-{-# LANGUAGE RankNTypes #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeApplications #-}-{-# LANGUAGE TypeFamilies #-}-{-# OPTIONS_GHC -Wno-unused-do-bind #-}--module Book where--import Control.Concurrent.Class.MonadSTM-import Control.Monad-import Control.Monad.Class.MonadFork (MonadFork, forkIO)-import Control.Monad.Class.MonadSay-import Control.Monad.Class.MonadThrow (MonadThrow)-import Data.IFunctor (At (..), Sing, SingI, ireturn, returnAt)-import qualified Data.IFunctor as I-import qualified Data.IntMap as IntMap-import Data.Kind-import GHC.Exts (dataToTag#)-import GHC.Int (Int (I#))-import TypedSession.Codec-import TypedSession.Core-import TypedSession.Driver-import Control.Monad.Class.MonadTimer (MonadDelay)--{------------------------------------------------------------------------------    Buyer                                                      Seller-    :S0                                                        :S0-     <                     Title String  ->                     >-    :S1                                                        :S1-     <                     <-  Price Int                         >-    :S12 s                                                     :S12 s--   ----------------------------------------------------------------------   |:S12 EnoughBudget                                          :S12 s-   | <                  Afford ->                               >-   |:S3                                                        :S3-   | <                  <- Data Int                             >-   |:End                                                       :End-   -----------------------------------------------------------------------   ----------------------------------------------------------------------   |:S12 NotEnoughBuget                                        :S12 s-   | <                  NotBuy ->                               >-   |:End                                                       :End-   ---------------------------------------------------------------------- -}--data Role = Buyer | Seller-  deriving (Show, Eq, Ord)--data SRole :: Role -> Type where-  SBuyer :: SRole Buyer-  SSeller :: SRole Seller--type instance Sing = SRole--instance SingI Buyer where-  sing = SBuyer--instance SingI Seller where-  sing = SSeller--data BudgetSt-  = EnoughBudget-  | NotEnoughBuget--data BookSt-  = S0-  | S1-  | S12 BudgetSt-  | S3-  | End--data SBookSt :: BookSt -> Type where-  SS0 :: SBookSt S0-  SS1 :: SBookSt S1-  SS12 :: SBookSt (S12 (s :: BudgetSt))-  SS3 :: SBookSt S3-  SEnd :: SBookSt End--type instance Sing = SBookSt--instance SingI S0 where-  sing = SS0--instance SingI S1 where-  sing = SS1--instance SingI (S12 s) where-  sing = SS12--instance SingI S3 where-  sing = SS3--instance SingI End where-  sing = SEnd--type Date = Int--instance SingToInt Role where-  singToInt x = I# (dataToTag# x)--instance SingToInt BookSt where-  singToInt x = I# (dataToTag# x)--instance Protocol Role BookSt where-  type Done Buyer = End-  type Done Seller = End--  data Msg Role BookSt from send recv where-    Title :: String -> Msg Role BookSt S0 '(Buyer, S1) '(Seller, S1)-    Price :: Int -> Msg Role BookSt S1 '(Seller, S12 s) '(Buyer, S12 s)-    Afford :: Msg Role BookSt (S12 EnoughBudget) '(Buyer, S3) '(Seller, S3)-    Date :: Date -> Msg Role BookSt S3 '(Seller, End) '(Buyer, End)-    NotBuy :: Msg Role BookSt (S12 NotEnoughBuget) '(Buyer, End) '(Seller, End)--encodeMsg :: Encode Role BookSt (AnyMsg Role BookSt)-encodeMsg = Encode $ \x -> case x of-  Title{} -> AnyMsg x-  Price{} -> AnyMsg x-  Afford{} -> AnyMsg x-  Date{} -> AnyMsg x-  NotBuy{} -> AnyMsg x--decodeMsg-  :: DecodeStep-      (AnyMsg Role BookSt)-      CodecFailure-      (AnyMsg Role BookSt)-decodeMsg =-  DecodePartial $ \case-    Nothing -> DecodeFail (CodecFailure "expected more data")-    Just anyMsg -> DecodeDone anyMsg Nothing--budget :: Int-budget = 100--data CheckPriceResult :: BookSt -> Type where-  Yes :: CheckPriceResult (S12 EnoughBudget)-  No :: CheckPriceResult (S12 NotEnoughBuget)--checkPrice :: (Monad m) => Int -> Peer Role BookSt Buyer m CheckPriceResult (S12 s)-checkPrice i =-  if i <= budget-    then LiftM $ pure (ireturn Yes)-    else LiftM $ pure (ireturn No)--buyerPeer-  :: (Monad m) => Peer Role BookSt Buyer m (At (Maybe Date) (Done Buyer)) S0-buyerPeer = I.do-  yield (Title "haskell book")-  Recv (Price i) <- await-  res <- checkPrice i-  case res of-    Yes -> I.do-      yield Afford-      Recv (Date d) <- await-      returnAt (Just d)-    No -> I.do-      yield NotBuy-      returnAt Nothing--sellerPeer :: (Functor m) => Peer Role BookSt Seller m (At () (Done Seller)) S0-sellerPeer = I.do-  Recv (Title _name) <- await-  yield (Price 30)-  Recv msg <- await-  case msg of-    Afford -> I.do-      yield (Date 100)-    NotBuy -> I.do-      returnAt ()--mvarsAsChannel-  :: (MonadSTM m)-  => TMVar m a-  -> TMVar m a-  -> Channel m a-mvarsAsChannel bufferRead bufferWrite =-  Channel{send, recv}- where-  send x = atomically (putTMVar bufferWrite x)-  recv = atomically (Just <$> takeTMVar bufferRead)--myTracer :: (MonadSay m) => String -> Tracer Role BookSt m-myTracer st v = say (st <> show v)--instance Show (AnyMsg Role BookSt) where-  show (AnyMsg msg) = case msg of-    Title st -> "Title " <> show st-    Price i -> "Price " <> show i-    Afford -> "Afford"-    Date i -> "Date " <> show i-    NotBuy -> "NotBuy"--runAll :: forall m. (Monad m, MonadDelay m, MonadSTM m, MonadSay m, MonadFork m, MonadThrow m) => m ()-runAll = do-  buyerTMVar <- newEmptyTMVarIO @m @(AnyMsg Role BookSt)-  sellerTMVar <- newEmptyTMVarIO @m @(AnyMsg Role BookSt)-  let buyerChannel = mvarsAsChannel @m buyerTMVar sellerTMVar-      sellerChannel = mvarsAsChannel @m sellerTMVar buyerTMVar-      sendFun bufferWrite x = atomically (putTMVar bufferWrite x)-      sendToRole =-        IntMap.fromList-          [ (singToInt SSeller, sendFun sellerTMVar)-          , (singToInt SBuyer, sendFun buyerTMVar)-          ]-  buyerTvar <- newTVarIO IntMap.empty-  sellerTvar <- newTVarIO IntMap.empty-  let buyerDriver = driverSimple (myTracer "buyer") encodeMsg sendToRole buyerTvar id-      sellerDriver = driverSimple (myTracer "seller") encodeMsg sendToRole sellerTvar id-  -- fork buyer decode thread, seller -> buyer-  forkIO $ decodeLoop (myTracer "buyer") Nothing (Decode decodeMsg) buyerChannel buyerTvar-  -- fork seller decode thread, buyer -> seller-  forkIO $ decodeLoop (myTracer "seller") Nothing (Decode decodeMsg) sellerChannel sellerTvar-  -- fork seller Peer thread-  forkIO $ void $ runPeerWithDriver sellerDriver sellerPeer-  -- run buyer Peer-  void $ runPeerWithDriver buyerDriver buyerPeer

@@ -1,281 +0,0 @@-{-# LANGUAGE AllowAmbiguousTypes #-}-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE LambdaCase #-}-{-# LANGUAGE MagicHash #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE NamedFieldPuns #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE QualifiedDo #-}-{-# LANGUAGE RankNTypes #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeApplications #-}-{-# LANGUAGE TypeFamilies #-}-{-# OPTIONS_GHC -Wno-unused-do-bind #-}--module Book1 where--import Control.Concurrent.Class.MonadSTM-import Control.Monad-import Control.Monad.Class.MonadFork (MonadFork, forkIO)-import Control.Monad.Class.MonadSay-import Control.Monad.Class.MonadThrow (MonadThrow)-import Data.IFunctor (At (..), Sing, SingI, ireturn, returnAt)-import qualified Data.IFunctor as I-import qualified Data.IntMap as IntMap-import Data.Kind-import GHC.Exts (dataToTag#)-import GHC.Int (Int (I#))-import TypedSession.Codec-import TypedSession.Core-import TypedSession.Driver-import Control.Monad.Class.MonadTimer (MonadDelay)--{---------------------------------------------------------------------------------------------------    Buyer                                                      Seller                  Buyer2-    :S0                                                        :S0-     <                     Title String  ->                     >-    :S1                                                        :S1-     <                     <-  Price Int                         >-    :S11                                                       :S12 s                  :S11-     <                                  PriceToBuyer2 Int ->                            >-    :S110                                                                              :S110-     <                                  <- HalfPrice  Int                               >-    :S12 s                                                                             :End--   ----------------------------------------------------------------------   |:S12 EnoughBudget                                          :S12 s-   | <                  Afford ->                               >-   |:S3                                                        :S3-   | <                  <- Data Int                             >-   |:End                                                       :End-   -----------------------------------------------------------------------   ----------------------------------------------------------------------   |:S12  NotEnoughBuget                                       :S12-   | <                  NotBuy ->                               >-   |:End                                                       :End-   -----------------------------------------------------------------------}--data Role = Buyer | Seller | Buyer2-  deriving (Show, Eq, Ord)--data SRole :: Role -> Type where-  SBuyer :: SRole Buyer-  SBuyer2 :: SRole Buyer2-  SSeller :: SRole Seller--type instance Sing = SRole--instance SingI Buyer where-  sing = SBuyer--instance SingI Buyer2 where-  sing = SBuyer2--instance SingI Seller where-  sing = SSeller--data BudgetSt-  = EnoughBudget-  | NotEnoughBuget--data BookSt-  = S0-  | S1-  | S11-  | S110-  | S12 BudgetSt-  | S3-  | End--data SBookSt :: BookSt -> Type where-  SS0 :: SBookSt S0-  SS1 :: SBookSt S1-  SS11 :: SBookSt S11-  SS110 :: SBookSt S110-  SS12 :: SBookSt (S12 (s :: BudgetSt))-  SS3 :: SBookSt S3-  SEnd :: SBookSt End--type instance Sing = SBookSt--instance SingI S0 where-  sing = SS0--instance SingI S1 where-  sing = SS1--instance SingI S11 where-  sing = SS11--instance SingI S110 where-  sing = SS110--instance SingI (S12 s) where-  sing = SS12--instance SingI S3 where-  sing = SS3--instance SingI End where-  sing = SEnd--type Date = Int--instance SingToInt Role where-  singToInt x = I# (dataToTag# x)--instance SingToInt BookSt where-  singToInt x = I# (dataToTag# x)--instance Protocol Role BookSt where-  type Done Buyer = End-  type Done Seller = End-  type Done Buyer2 = End-  data Msg Role BookSt from send recv where-    Title :: String -> Msg Role BookSt S0 '(Buyer, S1) '(Seller, S1)-    Price :: Int -> Msg Role BookSt S1 '(Seller, S12 s) '(Buyer, S11)-    PriceToB2 :: Int -> Msg Role BookSt S11 '(Buyer, S110) '(Buyer2, S110)-    HalfPrice :: Int -> Msg Role BookSt S110 '(Buyer2, End) '(Buyer, S12 s)-    Afford :: Msg Role BookSt (S12 EnoughBudget) '(Buyer, S3) '(Seller, S3)-    Date :: Date -> Msg Role BookSt S3 '(Seller, End) '(Buyer, End)-    NotBuy :: Msg Role BookSt (S12 NotEnoughBuget) '(Buyer, End) '(Seller, End)--encodeMsg :: Encode Role BookSt (AnyMsg Role BookSt)-encodeMsg = Encode $ \x -> case x of-  Title{} -> AnyMsg x-  Price{} -> AnyMsg x-  PriceToB2{} -> AnyMsg x-  HalfPrice{} -> AnyMsg x-  Afford{} -> AnyMsg x-  Date{} -> AnyMsg x-  NotBuy{} -> AnyMsg x--decodeMsg-  :: DecodeStep-      (AnyMsg Role BookSt)-      CodecFailure-      (AnyMsg Role BookSt)-decodeMsg =-  DecodePartial $ \case-    Nothing -> DecodeFail (CodecFailure "expected more data")-    Just anyMsg -> DecodeDone anyMsg Nothing--budget :: Int-budget = 16--data CheckPriceResult :: BookSt -> Type where-  Yes :: CheckPriceResult (S12 EnoughBudget)-  No :: CheckPriceResult (S12 NotEnoughBuget)--checkPrice :: (Monad m) => Int -> Int -> Peer Role BookSt Buyer m CheckPriceResult (S12 s)-checkPrice i h =-  if i <= budget + h-    then LiftM $ pure (ireturn Yes)-    else LiftM $ pure (ireturn No)--buyerPeer-  :: (Monad m) => Peer Role BookSt Buyer m (At (Maybe Date) (Done Buyer)) S0-buyerPeer = I.do-  yield (Title "haskell book")-  Recv (Price i) <- await-  yield (PriceToB2 i)-  Recv (HalfPrice hv) <- await-  res <- checkPrice i hv-  case res of-    Yes -> I.do-      yield Afford-      Recv (Date d) <- await-      returnAt (Just d)-    No -> I.do-      yield NotBuy-      returnAt Nothing--buyer2Peer-  :: (Monad m) => Peer Role BookSt Buyer2 m (At () (Done Buyer2)) S11-buyer2Peer = I.do-  Recv (PriceToB2 i) <- await-  yield (HalfPrice (i `div` 2))--sellerPeer :: (Monad m) => Peer Role BookSt Seller m (At () (Done Seller)) S0-sellerPeer = I.do-  Recv (Title _name) <- await-  yield (Price 30)-  Recv msg <- await-  case msg of-    Afford -> yield (Date 100)-    NotBuy -> returnAt ()--mvarsAsChannel-  :: (MonadSTM m)-  => TMVar m a-  -> TMVar m a-  -> Channel m a-mvarsAsChannel bufferRead bufferWrite =-  Channel{send, recv}- where-  send x = atomically (putTMVar bufferWrite x)-  recv = atomically (Just <$> takeTMVar bufferRead)--myTracer :: (MonadSay m) => String -> Tracer Role BookSt m-myTracer st v = say (st <> show v)--instance Show (AnyMsg Role BookSt) where-  show (AnyMsg msg) = case msg of-    Title st -> "Title " <> show st-    Price i -> "Price " <> show i-    PriceToB2 i -> "PriceToB2 " <> show i-    HalfPrice i -> "HalfPrice " <> show i-    Afford -> "Afford"-    Date i -> "Date " <> show i-    NotBuy -> "NotBuy"--runAll :: forall m. (Monad m, MonadDelay m, MonadSTM m, MonadSay m, MonadFork m, MonadThrow m) => m ()-runAll = do-  buyerTMVar <- newEmptyTMVarIO @m @(AnyMsg Role BookSt)-  buyer2TMVar <- newEmptyTMVarIO @m @(AnyMsg Role BookSt)-  sellerTMVar <- newEmptyTMVarIO @m @(AnyMsg Role BookSt)-  let buyerSellerChannel = mvarsAsChannel @m buyerTMVar sellerTMVar-      buyerBuyer2Channel = mvarsAsChannel @m buyerTMVar buyer2TMVar--      sellerBuyerChannel = mvarsAsChannel @m sellerTMVar buyerTMVar--      buyer2BuyerChannel = mvarsAsChannel @m buyer2TMVar buyerTMVar--      sendFun bufferWrite x = atomically (putTMVar bufferWrite x)-      sendToRole =-        IntMap.fromList-          [ (singToInt SSeller, sendFun sellerTMVar)-          , (singToInt SBuyer, sendFun buyerTMVar)-          , (singToInt SBuyer2, sendFun buyer2TMVar)-          ]-  buyerTvar <- newTVarIO IntMap.empty-  buyer2Tvar <- newTVarIO IntMap.empty-  sellerTvar <- newTVarIO IntMap.empty-  let buyerDriver = driverSimple (myTracer "buyer") encodeMsg sendToRole buyerTvar id-      buyer2Driver = driverSimple (myTracer "buyer2") encodeMsg sendToRole buyer2Tvar id-      sellerDriver = driverSimple (myTracer "seller") encodeMsg sendToRole sellerTvar id-  -- fork buyer decode thread, seller -> buyer-  forkIO $ decodeLoop (myTracer "buyer") Nothing (Decode decodeMsg) buyerSellerChannel buyerTvar-  -- fork buyer decode thread, buyer2 -> buyer-  forkIO $ decodeLoop (myTracer "buyer") Nothing (Decode decodeMsg) buyerBuyer2Channel buyerTvar--  -- fork seller decode thread, buyer -> seller-  forkIO $ decodeLoop (myTracer "seller") Nothing (Decode decodeMsg) sellerBuyerChannel sellerTvar--  -- fork buyer2 decode thread, buyer -> buyer2-  forkIO $ decodeLoop (myTracer "buyer2") Nothing (Decode decodeMsg) buyer2BuyerChannel buyer2Tvar--  -- fork seller Peer thread-  forkIO $ void $ runPeerWithDriver sellerDriver sellerPeer--  -- fork buyer2 Peer thread-  forkIO $ void $ runPeerWithDriver buyer2Driver buyer2Peer-  -- run buyer Peer-  void $ runPeerWithDriver buyerDriver buyerPeer

@@ -1,342 +0,0 @@-{-# LANGUAGE AllowAmbiguousTypes #-}-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE LambdaCase #-}-{-# LANGUAGE MagicHash #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE NamedFieldPuns #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE QualifiedDo #-}-{-# LANGUAGE RankNTypes #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeApplications #-}-{-# LANGUAGE TypeFamilies #-}-{-# OPTIONS_GHC -Wno-unused-do-bind #-}--module Book2 where--import Control.Concurrent.Class.MonadSTM-import Control.Monad-import Control.Monad.Class.MonadFork (MonadFork, forkIO)-import Control.Monad.Class.MonadSay-import Control.Monad.Class.MonadThrow (MonadThrow)-import Control.Monad.Class.MonadTimer (MonadDelay)-import Data.IFunctor (At (..), Sing, SingI, ireturn, returnAt)-import qualified Data.IFunctor as I-import qualified Data.IntMap as IntMap-import Data.Kind-import GHC.Exts (dataToTag#)-import GHC.Int (Int (I#))-import TypedSession.Codec-import TypedSession.Core-import TypedSession.Driver--{--------------------Buyer---------------Seller--------------Buyer2------------------                   S0                  S0                 S1 s-       Title       |        --->       |-                  S2 s                S2 s                S1 s-    ------------------------------BookNotFound-------------------------------                  S2 s          S2 BookNotFound           S1 s-    BookNotFoun    |        <---       |-            S1 BookNotFound           End                 S1 s-  SellerNotFoundB  |                  --->                 |-                  End                 End                 End-                                    Terminal--    -------------------------------BookFound---------------------------------                  S2 s            S2 BookFound            S1 s-       Price       |        <---       |-              S1 BookFound            S3 s                S1 s-   PriceToBuyer2   |                  --->                 |-                   S4                 S3 s                 S4-     HalfPrice     |                  <---                 |-                  S3 s                S3 s                S5 s-        --------------------------EnoughBudget---------------------------            S3 EnoughBudget           S3 s                S5 s-       Afford      |        --->       |-                   S6                  S6                 S5 s-        Data       |        <---       |-            S5 EnoughBudget           End                 S5 s-      Success      |                  --->                 |-                  End                 End                 End-                                    Terminal--        ------------------------NotEnoughBudget--------------------------           S3 NotEnoughBudget         S3 s                S5 s-       NotBuy      |        --->       |-           S5 NotEnoughBudget         End                 S5 s-       Failed      |                  --->                 |-                  End                 End                 End-                                    Terminal--}--data Role = Buyer | Seller | Buyer2-  deriving (Show, Eq, Ord)--data SRole :: Role -> Type where-  SBuyer :: SRole Buyer-  SBuyer2 :: SRole Buyer2-  SSeller :: SRole Seller--type instance Sing = SRole--instance SingI Buyer where-  sing = SBuyer--instance SingI Buyer2 where-  sing = SBuyer2--instance SingI Seller where-  sing = SSeller--data FindBook-  = BookNotFound-  | BookFound--data BudgetSt-  = EnoughBudget-  | NotEnoughBuget--data BookSt-  = S0-  | S1 FindBook-  | S2 FindBook-  | S3 BudgetSt-  | S4-  | S5 BudgetSt-  | S6-  | End--data SBookSt :: BookSt -> Type where-  SS0 :: SBookSt S0-  SS1 :: SBookSt (S1 (s :: FindBook))-  SS2 :: SBookSt (S2 (s :: FindBook))-  SS3 :: SBookSt (S3 (s :: BudgetSt))-  SS4 :: SBookSt S4-  SS5 :: SBookSt (S5 (s :: BudgetSt))-  SS6 :: SBookSt S6-  SEnd :: SBookSt End--type instance Sing = SBookSt--instance SingI S0 where-  sing = SS0--instance SingI (S1 s) where-  sing = SS1--instance SingI (S2 s) where-  sing = SS2--instance SingI (S3 s) where-  sing = SS3--instance SingI S4 where-  sing = SS4--instance SingI (S5 s) where-  sing = SS5--instance SingI S6 where-  sing = SS6--instance SingI End where-  sing = SEnd--type Date = Int--instance SingToInt Role where-  singToInt x = I# (dataToTag# x)--instance SingToInt BookSt where-  singToInt x = I# (dataToTag# x)--instance Protocol Role BookSt where-  type Done Buyer = End-  type Done Seller = End-  type Done Buyer2 = End-  data Msg Role BookSt from send recv where-    Title :: String -> Msg Role BookSt S0 '(Buyer, S2 s) '(Seller, S2 s)-    Price :: Int -> Msg Role BookSt (S2 BookFound) '(Seller, S3 s) '(Buyer, S1 BookFound)-    PriceToB2 :: Int -> Msg Role BookSt (S1 BookFound) '(Buyer, S4) '(Buyer2, S4)-    HalfPrice :: Int -> Msg Role BookSt S4 '(Buyer2, S5 s) '(Buyer, S3 s)-    Afford :: Msg Role BookSt (S3 EnoughBudget) '(Buyer, S6) '(Seller, S6)-    Date :: Date -> Msg Role BookSt S6 '(Seller, End) '(Buyer, S5 EnoughBudget)-    Success :: Int -> Msg Role BookSt (S5 EnoughBudget) '(Buyer, End) '(Buyer2, End)-    NotBuy :: Msg Role BookSt (S3 NotEnoughBuget) '(Buyer, S5 NotEnoughBuget) '(Seller, End)-    Failed :: Msg Role BookSt (S5 NotEnoughBuget) '(Buyer, End) '(Buyer2, End)-    BookNotFoun :: Msg Role BookSt (S2 BookNotFound) '(Seller, End) '(Buyer, S1 BookNotFound)-    SellerNotFoundBook :: Msg Role BookSt (S1 BookNotFound) '(Buyer, End) '(Buyer2, End)--encodeMsg :: Encode Role BookSt (AnyMsg Role BookSt)-encodeMsg = Encode $ \x -> case x of-  Title{} -> AnyMsg x-  Price{} -> AnyMsg x-  PriceToB2{} -> AnyMsg x-  HalfPrice{} -> AnyMsg x-  Afford{} -> AnyMsg x-  Date{} -> AnyMsg x-  Success{} -> AnyMsg x-  NotBuy{} -> AnyMsg x-  Failed{} -> AnyMsg x-  BookNotFoun{} -> AnyMsg x-  SellerNotFoundBook{} -> AnyMsg x--decodeMsg-  :: DecodeStep-      (AnyMsg Role BookSt)-      CodecFailure-      (AnyMsg Role BookSt)-decodeMsg =-  DecodePartial $ \case-    Nothing -> DecodeFail (CodecFailure "expected more data")-    Just anyMsg -> DecodeDone anyMsg Nothing--budget :: Int-budget = 16--data CheckPriceResult :: BookSt -> Type where-  Yes :: CheckPriceResult (S3 EnoughBudget)-  No :: CheckPriceResult (S3 NotEnoughBuget)--checkPrice :: (Monad m) => Int -> Int -> Peer Role BookSt Buyer m CheckPriceResult (S3 s)-checkPrice i h =-  if i <= budget + h-    then LiftM $ pure (ireturn Yes)-    else LiftM $ pure (ireturn No)--buyerPeer-  :: (Monad m) => Peer Role BookSt Buyer m (At (Maybe Date) (Done Buyer)) S0-buyerPeer = I.do-  yield (Title "haskell book")-  Recv msg <- await-  case msg of-    BookNotFoun -> I.do-      yield SellerNotFoundBook-      returnAt Nothing-    Price i -> I.do-      yield (PriceToB2 i)-      Recv (HalfPrice hv) <- await-      res <- checkPrice i hv-      case res of-        Yes -> I.do-          yield Afford-          Recv (Date d) <- await-          yield (Success d)-          returnAt (Just d)-        No -> I.do-          yield NotBuy-          yield Failed-          returnAt Nothing--buyer2Peer-  :: (Monad m) => Peer Role BookSt Buyer2 m (At () (Done Buyer2)) (S1 s)-buyer2Peer = I.do-  Recv msg' <- await-  case msg' of-    SellerNotFoundBook -> returnAt ()-    PriceToB2 i -> I.do-      yield (HalfPrice (i `div` 2))-      Recv msg <- await-      case msg of-        Success _ -> returnAt ()-        Failed -> returnAt ()--data FindBookResult :: BookSt -> Type where-  Found :: FindBookResult (S2 BookFound)-  NotFound :: FindBookResult (S2 BookNotFound)--findBook :: (Monad m) => String -> Peer Role BookSt Seller m FindBookResult (S2 s)-findBook st =-  if st /= ""-    then LiftM $ pure (ireturn Found)-    else LiftM $ pure (ireturn NotFound)--sellerPeer :: (Monad m) => Peer Role BookSt Seller m (At () (Done Seller)) S0-sellerPeer = I.do-  Recv (Title name) <- await-  res <- findBook name-  case res of-    Found -> I.do-      yield (Price 30)-      Recv msg <- await-      case msg of-        Afford -> yield (Date 100)-        NotBuy -> returnAt ()-    NotFound -> yield BookNotFoun--mvarsAsChannel-  :: (MonadSTM m)-  => TMVar m a-  -> TMVar m a-  -> Channel m a-mvarsAsChannel bufferRead bufferWrite =-  Channel{send, recv}- where-  send x = atomically (putTMVar bufferWrite x)-  recv = atomically (Just <$> takeTMVar bufferRead)--myTracer :: (MonadSay m) => String -> Tracer Role BookSt m-myTracer st v = say (st <> show v)--instance Show (AnyMsg Role BookSt) where-  show (AnyMsg msg) = case msg of-    Title st -> "Title " <> show st-    Price i -> "Price " <> show i-    PriceToB2 i -> "PriceToB2 " <> show i-    HalfPrice i -> "HalfPrice " <> show i-    Afford -> "Afford"-    Date i -> "Date " <> show i-    NotBuy -> "NotBuy"-    Success i -> "Success " <> show i-    Failed -> "Failed"-    BookNotFoun -> "BookNotFound"-    SellerNotFoundBook -> "SellerNotFoundBook"--runAll :: forall m. (Monad m, MonadDelay m, MonadSTM m, MonadSay m, MonadFork m, MonadThrow m) => m ()-runAll = do-  buyerTMVar <- newEmptyTMVarIO @m @(AnyMsg Role BookSt)-  buyer2TMVar <- newEmptyTMVarIO @m @(AnyMsg Role BookSt)-  sellerTMVar <- newEmptyTMVarIO @m @(AnyMsg Role BookSt)-  let buyerSellerChannel = mvarsAsChannel @m buyerTMVar sellerTMVar-      buyerBuyer2Channel = mvarsAsChannel @m buyerTMVar buyer2TMVar--      sellerBuyerChannel = mvarsAsChannel @m sellerTMVar buyerTMVar--      buyer2BuyerChannel = mvarsAsChannel @m buyer2TMVar buyerTMVar--      sendFun bufferWrite x = atomically (putTMVar bufferWrite x)-      sendToRole =-        IntMap.fromList-          [ (singToInt SSeller, sendFun sellerTMVar)-          , (singToInt SBuyer, sendFun buyerTMVar)-          , (singToInt SBuyer2, sendFun buyer2TMVar)-          ]-  buyerTvar <- newTVarIO IntMap.empty-  buyer2Tvar <- newTVarIO IntMap.empty-  sellerTvar <- newTVarIO IntMap.empty-  let buyerDriver = driverSimple (myTracer "buyer") encodeMsg sendToRole buyerTvar id-      buyer2Driver = driverSimple (myTracer "buyer2") encodeMsg sendToRole buyer2Tvar id-      sellerDriver = driverSimple (myTracer "seller") encodeMsg sendToRole sellerTvar id-  -- fork buyer decode thread, seller -> buyer-  forkIO $ decodeLoop (myTracer "buyer") Nothing (Decode decodeMsg) buyerSellerChannel buyerTvar-  -- fork buyer decode thread, buyer2 -> buyer-  forkIO $ decodeLoop (myTracer "buyer") Nothing (Decode decodeMsg) buyerBuyer2Channel buyerTvar--  -- fork seller decode thread, buyer -> seller-  forkIO $ decodeLoop (myTracer "seller") Nothing (Decode decodeMsg) sellerBuyerChannel sellerTvar--  -- fork buyer2 decode thread, buyer -> buyer2-  forkIO $ decodeLoop (myTracer "buyer2") Nothing (Decode decodeMsg) buyer2BuyerChannel buyer2Tvar--  -- fork seller Peer thread-  forkIO $ void $ runPeerWithDriver sellerDriver sellerPeer--  -- fork buyer2 Peer thread-  forkIO $ void $ runPeerWithDriver buyer2Driver buyer2Peer-  -- run buyer Peer-  void $ runPeerWithDriver buyerDriver buyerPeer

@@ -55,38 +55,33 @@ buyerPeer = I.do   yield (Title "haskell book")   await I.>>= \case-    Recv NoBook -> I.do+    NoBook -> I.do       yield SellerNoBook       returnAt Nothing-    Recv (Price i) -> I.do+    Price i -> I.do       choiceOT i I.>>= \case         BranchSt_One -> I.do           yield OneAccept-          Recv (OneDate d) <- await+          OneDate d <- await           yield (OneSuccess d)           returnAt $ Just d-        BranchSt_Two -> f1- where-  f1-    :: (Has Random sig m)-    => Peer BookRole Book 'Buyer m (At (Maybe Date) (Done Buyer)) ('S1 'Two)-  f1 = I.do-    yield (PriceToBuyer2 300)-    await I.>>= \case-      Recv NotSupport1 -> I.do-        yield TwoNotBuy-        returnAt Nothing-      Recv (SupportVal h) -> I.do-        checkPrice 10 h I.>>= \case-          BranchSt_Enough -> I.do-            yield TwoAccept-            Recv (TwoDate d) <- await-            yield (TwoSuccess d)-            returnAt (Just d)-          BranchSt_NotEnough -> I.do-            yield TwoNotBuy1-            yield TwoFailed-            returnAt Nothing+        BranchSt_Two -> I.do+          yield (PriceToBuyer2 (i `div` 2))+          await I.>>= \case+            NotSupport1 -> I.do+              yield TwoNotBuy+              returnAt Nothing+            SupportVal h -> I.do+              checkPrice 10 h I.>>= \case+                BranchSt_Enough -> I.do+                  yield TwoAccept+                  TwoDate d <- await+                  yield (TwoSuccess d)+                  returnAt (Just d)+                BranchSt_NotEnough -> I.do+                  yield TwoNotBuy1+                  yield TwoFailed+                  returnAt Nothing  choiceB   :: (Has Random sig m)@@ -103,9 +98,9 @@   => Peer BookRole Book Buyer2 m (At (Maybe Date) (Done Buyer2)) (S1 s) buyer2Peer = I.do   await I.>>= \case-    Recv SellerNoBook -> returnAt Nothing-    Recv (OneSuccess d) -> returnAt (Just d)-    Recv (PriceToBuyer2 i) -> I.do+    SellerNoBook -> returnAt Nothing+    (OneSuccess d) -> returnAt (Just d)+    (PriceToBuyer2 i) -> I.do       choiceB i I.>>= \case         BranchSt_NotSupport -> I.do           yield NotSupport1@@ -113,8 +108,8 @@         BranchSt_Support -> I.do           yield (SupportVal (i `div` 2))           await I.>>= \case-            Recv (TwoSuccess d) -> returnAt $ Just d-            Recv TwoFailed -> returnAt Nothing+            TwoSuccess d -> returnAt $ Just d+            TwoFailed -> returnAt Nothing  findBook   :: (Has Random sig m)@@ -130,13 +125,13 @@   :: (Has Random sig m)   => Peer BookRole Book Seller m (At () (Done Seller)) S0 sellerPeer = I.do-  Recv (Title st) <- await+  (Title st) <- await   findBook st I.>>= \case     BranchSt_NotFound -> yield NoBook     BranchSt_Found -> I.do       yield (Price 30)       await I.>>= \case-        Recv OneAccept -> yield (OneDate 100)-        Recv TwoNotBuy -> returnAt ()-        Recv TwoAccept -> yield (TwoDate 100)-        Recv TwoNotBuy1 -> returnAt ()+        OneAccept -> yield (OneDate 100)+        TwoNotBuy -> returnAt ()+        TwoAccept -> yield (TwoDate 100)+        TwoNotBuy1 -> returnAt ()

@@ -17,7 +17,6 @@  import Book3.Type -import Language.Haskell.TH hiding (Type) import TypedSession.Codec import TypedSession.Core 

@@ -1,196 +0,0 @@-{-# LANGUAGE AllowAmbiguousTypes #-}-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE LambdaCase #-}-{-# LANGUAGE MagicHash #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE NamedFieldPuns #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE QualifiedDo #-}-{-# LANGUAGE RankNTypes #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeApplications #-}-{-# LANGUAGE TypeFamilies #-}-{-# OPTIONS_GHC -Wno-unused-do-bind #-}--module PingPong where--import Control.Concurrent.Class.MonadSTM-import Control.Monad-import Control.Monad.Class.MonadFork (MonadFork, forkIO)-import Control.Monad.Class.MonadSay-import Control.Monad.Class.MonadThrow (MonadThrow)-import Control.Monad.Class.MonadTimer (MonadDelay)-import Data.IFunctor (At (..), Sing, SingI, ireturn, returnAt)-import qualified Data.IFunctor as I-import qualified Data.IntMap as IntMap-import Data.Kind-import GHC.Exts (dataToTag#)-import GHC.Int (Int (I#))-import TypedSession.Codec-import TypedSession.Core-import TypedSession.Driver--{------------------------------------------------------------------------------   Client                               Server-    :S0 s                                 :S0 s-  ------------------------------------------------------------------------  | :S0 True                           :S0 s-  |             Ping    ->-  | :S1                                :S1-  |             <- Pong-  | :S0 s                               :S0 s-  -------------------------------------------------------------------------  ------------------------------------------------------------------------  |  :S0 False                          :S0 s-  |               Stop    ->-  |  :End                               :End-  ------------------------------------------------------------------------ -}--data Role = Client | Server-  deriving (Show, Eq, Ord)--data SRole :: Role -> Type where-  SClient :: SRole Client-  SServer :: SRole Server--type instance Sing = SRole--instance SingI Client where-  sing = SClient--instance SingI Server where-  sing = SServer--data PingPong-  = S0 Bool-  | S1-  | End--data SPingPong :: PingPong -> Type where-  SS0 :: SPingPong (S0 b)-  SS1 :: SPingPong S1-  SEnd :: SPingPong End--type instance Sing = SPingPong--instance SingI (S0 b) where-  sing = SS0--instance SingI S1 where-  sing = SS1--instance SingI End where-  sing = SEnd--instance SingToInt Role where-  singToInt x = I# (dataToTag# x)--instance SingToInt PingPong where-  singToInt x = I# (dataToTag# x)--instance Protocol Role PingPong where-  type Done Client = End-  type Done Server = End-  data Msg Role PingPong from send recv where-    Ping :: Int -> Msg Role PingPong (S0 True) '(Client, S1) '(Server, S1)-    Pong :: Int -> Msg Role PingPong S1 '(Server, S0 s) '(Client, S0 s)-    Stop :: Msg Role PingPong (S0 False) '(Client, End) '(Server, End)--encodeMsg :: Encode Role PingPong (AnyMsg Role PingPong)-encodeMsg = Encode $ \x -> case x of-  Ping{} -> AnyMsg x-  Pong{} -> AnyMsg x-  Stop{} -> AnyMsg x--decodeMsg-  :: DecodeStep-      (AnyMsg Role PingPong)-      CodecFailure-      (AnyMsg Role PingPong)-decodeMsg =-  DecodePartial $ \case-    Nothing -> DecodeFail (CodecFailure "expected more data")-    Just anyMsg -> DecodeDone anyMsg Nothing--data Choice :: PingPong -> Type where-  ST :: Choice (S0 True)-  SF :: Choice (S0 False)--choice :: (Monad m) => Int -> Peer Role PingPong Client m Choice (S0 s)-choice i =-  if i <= 5-    then LiftM $ pure (ireturn ST)-    else LiftM $ pure (ireturn SF)--clientPeer-  :: (Monad m) => Int -> Peer Role PingPong Client m (At () (Done Client)) (S0 s)-clientPeer i = I.do-  res <- choice i-  case res of-    ST -> I.do-      yield (Ping i)-      Recv (Pong i') <- await-      clientPeer i'-    SF -> yield Stop--serverPeer-  :: (Monad m) => Peer Role PingPong Server m (At () (Done Server)) (S0 s)-serverPeer = I.do-  Recv msg <- await-  case msg of-    Ping i -> I.do-      yield (Pong (i + 1))-      serverPeer-    Stop -> returnAt ()--mvarsAsChannel-  :: (MonadSTM m)-  => TMVar m a-  -> TMVar m a-  -> Channel m a-mvarsAsChannel bufferRead bufferWrite =-  Channel{send, recv}- where-  send x = atomically (putTMVar bufferWrite x)-  recv = atomically (Just <$> takeTMVar bufferRead)--myTracer :: (MonadSay m) => String -> Tracer Role PingPong m-myTracer st v = say (st <> show v)--instance Show (AnyMsg Role PingPong) where-  show (AnyMsg msg) = case msg of-    Ping i -> "Ping " <> show i-    Pong i -> "Pong " <> show i-    Stop -> "Stop"--runAll :: forall m. (Monad m, MonadDelay m, MonadSTM m, MonadSay m, MonadFork m, MonadThrow m) => m ()-runAll = do-  clientTMVar <- newEmptyTMVarIO @m @(AnyMsg Role PingPong)-  serverTMVar <- newEmptyTMVarIO @m @(AnyMsg Role PingPong)-  let clientChannel = mvarsAsChannel @m clientTMVar serverTMVar-      serverChannel = mvarsAsChannel @m serverTMVar clientTMVar-      sendFun bufferWrite x = atomically (putTMVar bufferWrite x)-      sendToRole =-        IntMap.fromList-          [ (singToInt SServer, sendFun serverTMVar)-          , (singToInt SClient, sendFun clientTMVar)-          ]-  clientTvar <- newTVarIO IntMap.empty-  serverTvar <- newTVarIO IntMap.empty-  let clientDriver = driverSimple (myTracer "client: ") encodeMsg sendToRole clientTvar id-      serverDriver = driverSimple (myTracer "server: ") encodeMsg sendToRole serverTvar id-  -- fork client decode thread-  forkIO $ decodeLoop (myTracer "client: ") Nothing (Decode decodeMsg) clientChannel clientTvar-  -- fork server decode thread-  forkIO $ decodeLoop (myTracer "server: ") Nothing (Decode decodeMsg) serverChannel serverTvar-  -- fork server Peer thread-  forkIO $ void $ runPeerWithDriver serverDriver serverPeer-  -- run client Peer-  void $ runPeerWithDriver clientDriver (clientPeer 0)

@@ -20,7 +20,7 @@ -- PVP summary:     +-+------- breaking API changes --                  | | +----- non-breaking API additions --                  | | | +--- code changes with no API change-version:            0.1.3.0+version:            0.2.0.0  -- A short (one-line) description of the package. synopsis: typed session framework@@ -95,14 +95,10 @@     default-language: Haskell2010      -- Modules included in this executable, other than Main.-    other-modules: Book-                 , Book1-                 , Book2-                 , Book3.Type+    other-modules: Book3.Type                  , Book3.Protocol                  , Book3.Peer                  , Book3.Main-                 , PingPong      -- LANGUAGE extensions used by modules in this package.     -- other-extensions: