typed-session 0.1.0.0 → 0.1.1.0

raw patch · 17 files changed

+1053/−820 lines, 17 filesdep +template-haskelldep +typed-session-state-algorithmPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: template-haskell, typed-session-state-algorithm

API changes (from Hackage documentation)

Files

• CHANGELOG.md +3/−0
• src/TypedProtocol/Codec.hs +0/−72
• src/TypedProtocol/Core.hs +0/−254
• src/TypedProtocol/Driver.hs +0/−216
• src/TypedSession/Codec.hs +72/−0
• src/TypedSession/Core.hs +254/−0
• src/TypedSession/Driver.hs +217/−0
• src/TypedSession/TH.hs +293/−0
• test/Book.hs +3/−3
• test/Book1.hs +3/−3
• test/Book2.hs +3/−3
• test/Book3/Main.hs +9/−8
• test/Book3/Peer.hs +25/−25
• test/Book3/Protocol.hs +143/−0
• test/Book3/Type.hs +15/−228
• test/PingPong.hs +3/−3
• typed-session.cabal +10/−5

@@ -1,3 +1,6 @@ # Revision history for typed-session +## 0.1.1.0+* add protocol TH+ ## 0.1.0.0-- 2024-8-6

@@ -1,72 +0,0 @@---  This part of the code comes from typed-protocols, I modified a few things.-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE NamedFieldPuns #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE QuantifiedConstraints #-}-{-# LANGUAGE RankNTypes #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE UndecidableInstances #-}--module TypedProtocol.Codec where--import Control.Exception (Exception)-import TypedProtocol.Core--{- |-Function to encode Msg into bytes.--}-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'')-      -> bytes-  }--{- |-Incremental decoding function.--}-newtype Decode role' ps failure bytes = Decode-  { decode :: DecodeStep bytes failure (AnyMsg role' ps)-  }--{- |-Generic incremental decoder constructor, you need to convert specific incremental decoders to it.--}-data DecodeStep bytes failure a-  = DecodePartial (Maybe bytes -> (DecodeStep bytes failure a))-  | DecodeDone a (Maybe bytes)-  | DecodeFail failure--data CodecFailure-  = CodecFailureOutOfInput-  | CodecFailure String-  deriving (Eq, Show)--instance Exception CodecFailure--{- |-Bottom functions for sending and receiving bytes.--}-data Channel m bytes = Channel-  { send :: bytes -> m ()-  , recv :: m (Maybe bytes)-  }--{- |-Generic incremental decoding function.--}-runDecoderWithChannel-  :: (Monad m)-  => Channel m bytes-  -> Maybe bytes-  -> DecodeStep bytes failure a-  -> m (Either failure (a, Maybe bytes))-runDecoderWithChannel Channel{recv} = go- where-  go _ (DecodeDone x trailing) = return (Right (x, trailing))-  go _ (DecodeFail failure) = return (Left failure)-  go Nothing (DecodePartial k) = recv >>= pure . k >>= go Nothing-  go (Just trailing) (DecodePartial k) = (pure . k) (Just trailing) >>= go Nothing

@@ -1,254 +0,0 @@-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE LambdaCase #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE RankNTypes #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeApplications #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeOperators #-}--module TypedProtocol.Core where--import Data.IFunctor-import Data.IntMap (IntMap)-import Data.Kind--{- |--typed-session is a communication framework.-The messages received from the outside will be placed in MsgCache.-When interpreting the Peer, (Sing (r :: s)) will be generated according to the Peer's status.-SingToInt can convert Sing (r :: s) to Int.-Depending on this Int value, the required Msg is finally found from MsgCache.--In the process of multi-role communication, a message cache structure like MsgCache is needed.--Consider the following scenario--@-s1   s1   s2       Initial state--------------a -> b             a sends message MsgA to b--------------s3   s2   s2       State after sending--------------     b <- c        c sends message MsgC to b--------------s3   s4   s5       State after sending-@--For b, due to the influence of network transmission, it cannot guarantee that it can receive MsgA first and then MsgC.-If it receives MsgC first, it will directly put it in MsgCache and continue to wait until-MsgA arrives, then it will start to process MsgA first and then MsgC.--In general, dataToTag# is used directly here.--Example:--@-instance SingToInt Role where-  singToInt x = I# (dataToTag# x)--instance SingToInt PingPong where-  singToInt x = I# (dataToTag# x)-@--}-class SingToInt s where-  singToInt :: Sing (r :: s) -> Int--{- |--Describes the type class of Msg. The core of typed-session.--@-type Done (sr :: role') :: ps-@--Describe the state of each role when it terminates.--@-data Msg role' ps (from :: ps) (sendAndSt :: (role', ps)) (recvAndSt :: (role', 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,-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.--There are two principles to follow when designing the state of Msg:--1. When sending a message, the sender and receiver must be in the same state. Here the receiver may be in a more generalized state related to the state.-For example, the sender is in state (S1 [True]), and the receiver is in state (S1 s).--2. The same state can only be used for the same pair of receiver and sender.--For example, in the following example, state s1 is used for both (a -> b) and (b -> c), which is wrong.--@-s1   s1   s1-a -> b-s2   s1   s1-     b -> c-s2   s4   s5-@--}-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--{- |-Messages received from the outside are placed in MsgCache. When interpreting-Peer will use the Msg in MsgCache.--}-type MsgCache role' ps = IntMap (AnyMsg role' ps)--{- |-Packaging of Msg, shielding part of the type information, mainly used for serialization.--}-data AnyMsg role' ps where-  AnyMsg-    :: ( SingI recv-       , SingI st-       , SingToInt role'-       , SingToInt ps-       )-    => 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'')-  -> Sing st-msgFromStSing _ = sing @st--{- |-Core Ast, all we do is build this Ast and then interpret it.--@-IReturn :: ia st -> Peer role' ps r m ia st-@-IReturn indicates the termination of the continuation.--@-LiftM :: m (Peer role' ps r m ia st') -> Peer role' ps r m ia st-@--Liftm can transform state st to any state st'.-It looks a bit strange, as if it is a constructor that is not constrained by the Msg type.-Be careful when using it, it is a type breakpoint.-But some state transition functions need it, which can make the code more flexible.-Be very careful when using it!--@-Yield-  :: ( SingI recv-     , SingI from-     , SingToInt ps-     )-  => Msg role' ps from '(send, sps) '(recv, rps)-  -> Peer role' ps send m ia sps-  -> Peer role' ps send m ia from-@-Yield represents sending a message. Note that the Peer status changes from `from` to `sps`.--@-Await-  :: ( SingI recv-     , SingI from-     , SingToInt ps-     )-  => (Recv role' ps recv from ~> Peer role' ps recv m ia)-  -> Peer role' ps recv m ia from-@--Await represents receiving messages.-Different messages will lead to different states.-The state is passed to the next behavior through (~>).--}-data Peer role' ps (r :: role') (m :: Type -> Type) (ia :: ps -> Type) (st :: ps) where-  IReturn :: ia st -> Peer role' ps r m ia st-  LiftM :: m (Peer role' ps r m ia st') -> Peer role' ps r m ia st-  Yield-    :: ( SingI recv-       , SingI from-       , SingToInt ps-       )-    => Msg role' ps from '(send, sps) '(recv, rps)-    -> Peer role' ps send m ia sps-    -> Peer role' ps send m ia from-  Await-    :: ( SingI recv-       , SingI from-       , SingToInt ps-       )-    => (Recv role' ps recv from ~> Peer role' ps recv m ia)-    -> Peer role' ps recv m ia from--instance (Functor m) => IMonadFail (Peer role' ps r m) where-  fail = error--instance (Functor m) => IFunctor (Peer role' ps r m) where-  imap f = \case-    IReturn ia -> IReturn (f ia)-    LiftM f' -> LiftM (fmap (imap f) f')-    Yield ms cont -> Yield ms (imap f cont)-    Await cont -> Await (imap f . cont)--instance (Functor m) => IMonad (Peer role' ps r m) where-  ireturn = IReturn-  ibind f = \case-    IReturn ia -> (f ia)-    LiftM f' -> LiftM (fmap (ibind f) f')-    Yield ms cont -> Yield ms (ibind f cont)-    Await cont -> Await (ibind f . cont)--{- |-Send a message, the Peer status changes from `from` to `sps`.--}-yield-  :: ( Functor m-     , SingI recv-     , SingI from-     , SingToInt ps-     )-  => Msg role' ps from '(send, sps) '(recv, rps)-  -> Peer role' ps send m (At () sps) from-yield msg = Yield msg (returnAt ())--{- |-Receiving Messages.--}-await-  :: ( Functor m-     , SingI recv-     , SingI from-     , SingToInt ps-     )-  => Peer role' ps recv m (Recv role' ps recv from) from-await = Await ireturn--{- |-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)

@@ -1,216 +0,0 @@---  This part of the code comes from typed-protocols, I modified a few things.-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE NamedFieldPuns #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE RankNTypes #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeApplications #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE UndecidableInstances #-}-{-# OPTIONS_GHC -Wno-unused-do-bind #-}--{- |-Schematic diagram of the communication structure of three roles through typed-session:-![fm](data/fm.png)--Some explanations for this diagram:--1. Roles are connected through channels, and there are many types of channels, such as channels established through TCP or channels established through TMVar.--2. Each role has a Peer thread, in which the Peer runs.--3. Each role has one or more decode threads, and the decoded Msgs are placed in the MsgCache.--4. SendMap aggregates the send functions of multiple Channels together.-When sending a message, the send function of the receiver is searched from SendMap.--}-module TypedProtocol.Driver where--import Control.Concurrent.Class.MonadSTM-import Control.Monad.Class.MonadThrow (MonadThrow, throwIO)-import Data.IFunctor (At (..), Sing, SingI (sing))-import qualified Data.IFunctor as I-import Data.IntMap (IntMap)-import qualified Data.IntMap as IntMap-import GHC.Exception (Exception)-import TypedProtocol.Codec-import TypedProtocol.Core-import Unsafe.Coerce (unsafeCoerce)--{- |-Contains two functions sendMsg, recvMsg.-runPeerWithDriver uses them to send and receive Msg.--}-data Driver role' ps m-  = Driver-  { sendMsg-      :: forall (send :: role') (recv :: role') (st :: ps) (st' :: ps) (st'' :: ps)-       . ( SingI recv-         , SingI st-         , SingToInt ps-         , SingToInt role'-         )-      => Sing recv-      -> Msg role' ps st '(send, st') '(recv, st'')-      -> m ()-  , recvMsg-      :: forall (st' :: ps)-       . (SingToInt ps)-      => Sing st'-      -> m (AnyMsg role' ps)-  }--{- |-Interpret Peer.--}-runPeerWithDriver-  :: forall role' ps (r :: role') (st :: ps) m a-   . ( Monad m-     , (SingToInt role')-     )-  => Driver role' ps m-  -> Peer role' ps r m (At a (Done r)) st-  -> m a-runPeerWithDriver Driver{sendMsg, recvMsg} =-  go- where-  go-    :: forall st'-     . Peer role' ps r m (At a (Done r)) st'-    -> 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-    sendMsg (sing @recv) msg-    go k-  go (Await (k :: (Recv role' ps r st' I.~> Peer role' ps r m ia))) = do-    AnyMsg msg <- recvMsg (sing @st')-    go (k $ unsafeCoerce (Recv msg))--{- |-A wrapper around AnyMsg that represents sending and receiving Msg.--}-data TraceSendRecv role' ps where-  TraceSendMsg :: AnyMsg role' ps -> TraceSendRecv role' ps-  TraceRecvMsg :: AnyMsg role' ps -> TraceSendRecv role' ps--instance (Show (AnyMsg role' ps)) => Show (TraceSendRecv role' ps) where-  show (TraceSendMsg msg) = "Send " ++ show msg-  show (TraceRecvMsg msg) = "Recv " ++ show msg--{- |-Similar to the log function, used to print received or sent messages.--}-type Tracer role' ps m = TraceSendRecv role' ps -> m ()--{- |-The default trace function. It simply ignores everything.--}-nullTracer :: (Monad m) => a -> m ()-nullTracer _ = pure ()--{- |-SendMap aggregates the send functions of multiple Channels together.-When sending a message, the send function of the receiver is found from SendMap.--}-type SendMap role' m bytes = IntMap (bytes -> m ())--{- |--Build Driver through SendMap and MsgCache.-Here we need some help from other functions:--1. `Tracer role' ps n` is similar to the log function, used to print received or sent messages.-2. `Encode role' ps` bytes encoding function, converts Msg into bytes.-3. `forall a. n a -> m a` This is a bit complicated, I will explain it in detail below.--I see Peer as three layers:--1. `Peer` upper layer, meets the requirements of McBride Indexed Monad, uses do syntax construction, has semantic checks, and is interpreted to the second layer m through runPeerWithDriver.-2. `m` middle layer, describes the business requirements in this layer, and converts the received Msg into specific business actions.-3. `n` bottom layer, responsible for receiving and sending bytes. It can have multiple options such as IO or IOSim. Using IOSim can easily test the code.--}-driverSimple-  :: forall role' ps bytes m n-   . ( Monad m-     , Monad n-     , MonadSTM n-     )-  => Tracer role' ps n-  -> Encode role' ps bytes-  -> SendMap role' n bytes-  -> TVar n (MsgCache role' ps)-  -> (forall a. n a -> m a)-  -> Driver role' ps m-driverSimple tracer Encode{encode} sendMap tvar liftFun =-  Driver{sendMsg, recvMsg}- where-  sendMsg-    :: forall (send :: role') (recv :: role') (from :: ps) (st :: ps) (st1 :: ps)-     . ( SingI recv-       , SingI from-       , SingToInt ps-       , SingToInt role'-       )-    => Sing recv-    -> Msg role' ps from '(send, st) '(recv, st1)-    -> m ()-  sendMsg role msg = liftFun $ do-    case IntMap.lookup (singToInt role) sendMap of-      Nothing -> error "np"-      Just sendFun -> sendFun (encode msg)-    tracer (TraceSendMsg (AnyMsg msg))--  recvMsg-    :: forall (st' :: ps)-     . (SingToInt ps)-    => Sing st'-    -> m (AnyMsg role' ps)-  recvMsg sst' = do-    let singInt = singToInt sst'-    liftFun $ do-      anyMsg <- atomically $ do-        agencyMsg <- readTVar tvar-        case IntMap.lookup singInt agencyMsg of-          Nothing -> retry-          Just v -> do-            writeTVar tvar (IntMap.delete singInt agencyMsg)-            pure v-      tracer (TraceRecvMsg (anyMsg))-      pure anyMsg--{- |-decode loop, usually in a separate thread.--The decoded Msg is placed in MsgCache.--@-data Msg role' ps (from :: ps) (sendAndSt :: (role', ps)) (recvAndSt :: (role', ps))-@-Note that when placing a new Msg in MsgCache, if a Msg with the same `from` already exists in MsgCache, the decoding process will be blocked,-until that Msg is consumed before placing the new Msg in MsgCache.--This usually happens when the efficiency of Msg generation is greater than the efficiency of consumption.--}-decodeLoop-  :: (Exception failure, MonadSTM n, MonadThrow n)-  => Tracer role' ps n-  -> Maybe bytes-  -> Decode role' ps failure bytes-  -> Channel n bytes-  -> TVar n (MsgCache role' ps)-  -> n ()-decodeLoop tracer mbt d@Decode{decode} channel tvar = do-  result <- runDecoderWithChannel channel mbt decode-  case result of-    Right (AnyMsg msg, mbt') -> do-      let agencyInt = singToInt $ msgFromStSing msg-      atomically $ do-        agencyMsg <- readTVar tvar-        case IntMap.lookup agencyInt agencyMsg of-          Nothing -> writeTVar tvar (IntMap.insert agencyInt (AnyMsg msg) agencyMsg)-          Just _v -> retry-      decodeLoop tracer mbt' d channel tvar-    Left failure -> throwIO failure

@@ -0,0 +1,72 @@+--  This part of the code comes from typed-protocols, I modified a few things.+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-}++module TypedSession.Codec where++import Control.Exception (Exception)+import TypedSession.Core++{- |+Function to encode Msg into bytes.+-}+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'')+      -> bytes+  }++{- |+Incremental decoding function.+-}+newtype Decode role' ps failure bytes = Decode+  { decode :: DecodeStep bytes failure (AnyMsg role' ps)+  }++{- |+Generic incremental decoder constructor, you need to convert specific incremental decoders to it.+-}+data DecodeStep bytes failure a+  = DecodePartial (Maybe bytes -> (DecodeStep bytes failure a))+  | DecodeDone a (Maybe bytes)+  | DecodeFail failure++data CodecFailure+  = CodecFailureOutOfInput+  | CodecFailure String+  deriving (Eq, Show)++instance Exception CodecFailure++{- |+Bottom functions for sending and receiving bytes.+-}+data Channel m bytes = Channel+  { send :: bytes -> m ()+  , recv :: m (Maybe bytes)+  }++{- |+Generic incremental decoding function.+-}+runDecoderWithChannel+  :: (Monad m)+  => Channel m bytes+  -> Maybe bytes+  -> DecodeStep bytes failure a+  -> m (Either failure (a, Maybe bytes))+runDecoderWithChannel Channel{recv} = go+ where+  go _ (DecodeDone x trailing) = return (Right (x, trailing))+  go _ (DecodeFail failure) = return (Left failure)+  go Nothing (DecodePartial k) = recv >>= pure . k >>= go Nothing+  go (Just trailing) (DecodePartial k) = (pure . k) (Just trailing) >>= go Nothing

@@ -0,0 +1,254 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}++module TypedSession.Core where++import Data.IFunctor+import Data.IntMap (IntMap)+import Data.Kind++{- |++typed-session is a communication framework.+The messages received from the outside will be placed in MsgCache.+When interpreting the Peer, (Sing (r :: s)) will be generated according to the Peer's status.+SingToInt can convert Sing (r :: s) to Int.+Depending on this Int value, the required Msg is finally found from MsgCache.++In the process of multi-role communication, a message cache structure like MsgCache is needed.++Consider the following scenario++@+s1   s1   s2       Initial state+------------+a -> b             a sends message MsgA to b+------------+s3   s2   s2       State after sending+------------+     b <- c        c sends message MsgC to b+------------+s3   s4   s5       State after sending+@++For b, due to the influence of network transmission, it cannot guarantee that it can receive MsgA first and then MsgC.+If it receives MsgC first, it will directly put it in MsgCache and continue to wait until+MsgA arrives, then it will start to process MsgA first and then MsgC.++In general, dataToTag# is used directly here.++Example:++@+instance SingToInt Role where+  singToInt x = I# (dataToTag# x)++instance SingToInt PingPong where+  singToInt x = I# (dataToTag# x)+@+-}+class SingToInt s where+  singToInt :: Sing (r :: s) -> Int++{- |++Describes the type class of Msg. The core of typed-session.++@+type Done (sr :: role') :: ps+@++Describe the state of each role when it terminates.++@+data Msg role' ps (from :: ps) (sendAndSt :: (role', ps)) (recvAndSt :: (role', 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,+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.++There are two principles to follow when designing the state of Msg:++1. When sending a message, the sender and receiver must be in the same state. Here the receiver may be in a more generalized state related to the state.+For example, the sender is in state (S1 [True]), and the receiver is in state (S1 s).++2. The same state can only be used for the same pair of receiver and sender.++For example, in the following example, state s1 is used for both (a -> b) and (b -> c), which is wrong.++@+s1   s1   s1+a -> b+s2   s1   s1+     b -> c+s2   s4   s5+@+-}+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++{- |+Messages received from the outside are placed in MsgCache. When interpreting+Peer will use the Msg in MsgCache.+-}+type MsgCache role' ps = IntMap (AnyMsg role' ps)++{- |+Packaging of Msg, shielding part of the type information, mainly used for serialization.+-}+data AnyMsg role' ps where+  AnyMsg+    :: ( SingI recv+       , SingI st+       , SingToInt role'+       , SingToInt ps+       )+    => 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'')+  -> Sing st+msgFromStSing _ = sing @st++{- |+Core Ast, all we do is build this Ast and then interpret it.++@+IReturn :: ia st -> Peer role' ps r m ia st+@+IReturn indicates the termination of the continuation.++@+LiftM :: m (Peer role' ps r m ia st') -> Peer role' ps r m ia st+@++Liftm can transform state st to any state st'.+It looks a bit strange, as if it is a constructor that is not constrained by the Msg type.+Be careful when using it, it is a type breakpoint.+But some state transition functions need it, which can make the code more flexible.+Be very careful when using it!++@+Yield+  :: ( SingI recv+     , SingI from+     , SingToInt ps+     )+  => Msg role' ps from '(send, sps) '(recv, rps)+  -> Peer role' ps send m ia sps+  -> Peer role' ps send m ia from+@+Yield represents sending a message. Note that the Peer status changes from `from` to `sps`.++@+Await+  :: ( SingI recv+     , SingI from+     , SingToInt ps+     )+  => (Recv role' ps recv from ~> Peer role' ps recv m ia)+  -> Peer role' ps recv m ia from+@++Await represents receiving messages.+Different messages will lead to different states.+The state is passed to the next behavior through (~>).+-}+data Peer role' ps (r :: role') (m :: Type -> Type) (ia :: ps -> Type) (st :: ps) where+  IReturn :: ia st -> Peer role' ps r m ia st+  LiftM :: m (Peer role' ps r m ia st') -> Peer role' ps r m ia st+  Yield+    :: ( SingI recv+       , SingI from+       , SingToInt ps+       )+    => Msg role' ps from '(send, sps) '(recv, rps)+    -> Peer role' ps send m ia sps+    -> Peer role' ps send m ia from+  Await+    :: ( SingI recv+       , SingI from+       , SingToInt ps+       )+    => (Recv role' ps recv from ~> Peer role' ps recv m ia)+    -> Peer role' ps recv m ia from++instance (Functor m) => IMonadFail (Peer role' ps r m) where+  fail = error++instance (Functor m) => IFunctor (Peer role' ps r m) where+  imap f = \case+    IReturn ia -> IReturn (f ia)+    LiftM f' -> LiftM (fmap (imap f) f')+    Yield ms cont -> Yield ms (imap f cont)+    Await cont -> Await (imap f . cont)++instance (Functor m) => IMonad (Peer role' ps r m) where+  ireturn = IReturn+  ibind f = \case+    IReturn ia -> (f ia)+    LiftM f' -> LiftM (fmap (ibind f) f')+    Yield ms cont -> Yield ms (ibind f cont)+    Await cont -> Await (ibind f . cont)++{- |+Send a message, the Peer status changes from `from` to `sps`.+-}+yield+  :: ( Functor m+     , SingI recv+     , SingI from+     , SingToInt ps+     )+  => Msg role' ps from '(send, sps) '(recv, rps)+  -> Peer role' ps send m (At () sps) from+yield msg = Yield msg (returnAt ())++{- |+Receiving Messages.+-}+await+  :: ( Functor m+     , SingI recv+     , SingI from+     , SingToInt ps+     )+  => Peer role' ps recv m (Recv role' ps recv from) from+await = Await ireturn++{- |+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)

@@ -0,0 +1,217 @@+--  This part of the code comes from typed-protocols, I modified a few things.+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -Wno-unused-do-bind #-}++{- |+Schematic diagram of the communication structure of three roles through typed-session:++<<data/fm.png>>++Some explanations for this diagram:++1. Roles are connected through channels, and there are many types of channels, such as channels established through TCP or channels established through TMVar.++2. Each role has a Peer thread, in which the Peer runs.++3. Each role has one or more decode threads, and the decoded Msgs are placed in the MsgCache.++4. SendMap aggregates the send functions of multiple Channels together.+When sending a message, the send function of the receiver is searched from SendMap.+-}+module TypedSession.Driver where++import Control.Concurrent.Class.MonadSTM+import Control.Monad.Class.MonadThrow (MonadThrow, throwIO)+import Data.IFunctor (At (..), Sing, SingI (sing))+import qualified Data.IFunctor as I+import Data.IntMap (IntMap)+import qualified Data.IntMap as IntMap+import GHC.Exception (Exception)+import TypedSession.Codec+import TypedSession.Core+import Unsafe.Coerce (unsafeCoerce)++{- |+Contains two functions sendMsg, recvMsg.+runPeerWithDriver uses them to send and receive Msg.+-}+data Driver role' ps m+  = Driver+  { sendMsg+      :: forall (send :: role') (recv :: role') (st :: ps) (st' :: ps) (st'' :: ps)+       . ( SingI recv+         , SingI st+         , SingToInt ps+         , SingToInt role'+         )+      => Sing recv+      -> Msg role' ps st '(send, st') '(recv, st'')+      -> m ()+  , recvMsg+      :: forall (st' :: ps)+       . (SingToInt ps)+      => Sing st'+      -> m (AnyMsg role' ps)+  }++{- |+Interpret Peer.+-}+runPeerWithDriver+  :: forall role' ps (r :: role') (st :: ps) m a+   . ( Monad m+     , (SingToInt role')+     )+  => Driver role' ps m+  -> Peer role' ps r m (At a (Done r)) st+  -> m a+runPeerWithDriver Driver{sendMsg, recvMsg} =+  go+ where+  go+    :: forall st'+     . Peer role' ps r m (At a (Done r)) st'+    -> 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+    sendMsg (sing @recv) msg+    go k+  go (Await (k :: (Recv role' ps r st' I.~> Peer role' ps r m ia))) = do+    AnyMsg msg <- recvMsg (sing @st')+    go (k $ unsafeCoerce (Recv msg))++{- |+A wrapper around AnyMsg that represents sending and receiving Msg.+-}+data TraceSendRecv role' ps where+  TraceSendMsg :: AnyMsg role' ps -> TraceSendRecv role' ps+  TraceRecvMsg :: AnyMsg role' ps -> TraceSendRecv role' ps++instance (Show (AnyMsg role' ps)) => Show (TraceSendRecv role' ps) where+  show (TraceSendMsg msg) = "Send " ++ show msg+  show (TraceRecvMsg msg) = "Recv " ++ show msg++{- |+Similar to the log function, used to print received or sent messages.+-}+type Tracer role' ps m = TraceSendRecv role' ps -> m ()++{- |+The default trace function. It simply ignores everything.+-}+nullTracer :: (Monad m) => a -> m ()+nullTracer _ = pure ()++{- |+SendMap aggregates the send functions of multiple Channels together.+When sending a message, the send function of the receiver is found from SendMap.+-}+type SendMap role' m bytes = IntMap (bytes -> m ())++{- |++Build Driver through SendMap and MsgCache.+Here we need some help from other functions:++1. `Tracer role' ps n` is similar to the log function, used to print received or sent messages.+2. `Encode role' ps` bytes encoding function, converts Msg into bytes.+3. `forall a. n a -> m a` This is a bit complicated, I will explain it in detail below.++I see Peer as three layers:++1. `Peer` upper layer, meets the requirements of McBride Indexed Monad, uses do syntax construction, has semantic checks, and is interpreted to the second layer m through runPeerWithDriver.+2. `m` middle layer, describes the business requirements in this layer, and converts the received Msg into specific business actions.+3. `n` bottom layer, responsible for receiving and sending bytes. It can have multiple options such as IO or IOSim. Using IOSim can easily test the code.+-}+driverSimple+  :: forall role' ps bytes m n+   . ( Monad m+     , Monad n+     , MonadSTM n+     )+  => Tracer role' ps n+  -> Encode role' ps bytes+  -> SendMap role' n bytes+  -> TVar n (MsgCache role' ps)+  -> (forall a. n a -> m a)+  -> Driver role' ps m+driverSimple tracer Encode{encode} sendMap tvar liftFun =+  Driver{sendMsg, recvMsg}+ where+  sendMsg+    :: forall (send :: role') (recv :: role') (from :: ps) (st :: ps) (st1 :: ps)+     . ( SingI recv+       , SingI from+       , SingToInt ps+       , SingToInt role'+       )+    => Sing recv+    -> Msg role' ps from '(send, st) '(recv, st1)+    -> m ()+  sendMsg role msg = liftFun $ do+    case IntMap.lookup (singToInt role) sendMap of+      Nothing -> error "np"+      Just sendFun -> sendFun (encode msg)+    tracer (TraceSendMsg (AnyMsg msg))++  recvMsg+    :: forall (st' :: ps)+     . (SingToInt ps)+    => Sing st'+    -> m (AnyMsg role' ps)+  recvMsg sst' = do+    let singInt = singToInt sst'+    liftFun $ do+      anyMsg <- atomically $ do+        agencyMsg <- readTVar tvar+        case IntMap.lookup singInt agencyMsg of+          Nothing -> retry+          Just v -> do+            writeTVar tvar (IntMap.delete singInt agencyMsg)+            pure v+      tracer (TraceRecvMsg (anyMsg))+      pure anyMsg++{- |+decode loop, usually in a separate thread.++The decoded Msg is placed in MsgCache.++@+data Msg role' ps (from :: ps) (sendAndSt :: (role', ps)) (recvAndSt :: (role', ps))+@+Note that when placing a new Msg in MsgCache, if a Msg with the same `from` already exists in MsgCache, the decoding process will be blocked,+until that Msg is consumed before placing the new Msg in MsgCache.++This usually happens when the efficiency of Msg generation is greater than the efficiency of consumption.+-}+decodeLoop+  :: (Exception failure, MonadSTM n, MonadThrow n)+  => Tracer role' ps n+  -> Maybe bytes+  -> Decode role' ps failure bytes+  -> Channel n bytes+  -> TVar n (MsgCache role' ps)+  -> n ()+decodeLoop tracer mbt d@Decode{decode} channel tvar = do+  result <- runDecoderWithChannel channel mbt decode+  case result of+    Right (AnyMsg msg, mbt') -> do+      let agencyInt = singToInt $ msgFromStSing msg+      atomically $ do+        agencyMsg <- readTVar tvar+        case IntMap.lookup agencyInt agencyMsg of+          Nothing -> writeTVar tvar (IntMap.insert agencyInt (AnyMsg msg) agencyMsg)+          Just _v -> retry+      decodeLoop tracer mbt' d channel tvar+    Left failure -> throwIO failure

@@ -0,0 +1,293 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeApplications #-}+{-# OPTIONS_GHC -Wno-unused-imports #-}+{-# OPTIONS_GHC -split-sections #-}++module TypedSession.TH where++import Control.Monad (forM)+import Data.Either (fromRight)+import Data.Kind+import qualified Data.Set as Set+import Language.Haskell.TH hiding (Type)+import qualified Language.Haskell.TH as TH+import Language.Haskell.TH.Quote+import TypedSession.State.GenDoc+import TypedSession.State.Parser (runProtocolParser)+import TypedSession.State.Piple (PipleResult (..), piple)+import TypedSession.State.Render+import TypedSession.State.Type (BranchSt (..), Creat, MsgOrLabel (..), MsgT1, Protocol (..), ProtocolError, T (..))++roleDecs :: Name -> Q [Dec]+roleDecs name = do+  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"++addS :: Name -> Name+addS name =+  let n = (nameBase name)+   in mkName ("S" <> n)++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"+  let protName = mkName protN+      protSName = mkName ("S" <> protN)+      genConstr i =+        if i == -1+          then NormalC (mkName "End") []+          else+            if i `Set.member` dnySet+              then+                NormalC+                  (mkName $ "S" <> show i)+                  [(Bang NoSourceUnpackedness NoSourceStrictness, ConT bstName)]+              else NormalC (mkName $ "S" <> show i) []+      genSConstr i =+        if i == -1+          then+            GadtC [mkName "SEnd"] [] (AppT (ConT protSName) (PromotedT (mkName "End")))+          else+            if i `Set.member` dnySet+              then+                ForallC+                  [KindedTV sVar SpecifiedSpec (ConT bstName)]+                  []+                  ( GadtC+                      [mkName $ "SS" <> show i]+                      []+                      (AppT (ConT protSName) (AppT (PromotedT $ mkName $ "S" <> show i) (VarT sVar)))+                  )+              else+                GadtC [mkName $ "SS" <> show i] [] (AppT (ConT protSName) (PromotedT $ mkName $ "S" <> show i))++      isTAny :: T bst -> Bool+      isTAny = \case+        TAny _ -> True+        _ -> False++      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"++          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))+                )+          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 []++  a <- newName "a"+  s1 <- newName "s1"+  x <- newName "x"++  -- make instance Done+  res <- reify roleName+  instDoneDesc <- case res of+    TyConI (DataD [] _ [] Nothing cons _) -> do+      pure+        [ TySynInstD+            ( TySynEqn+                Nothing+                (AppT (ConT (mkName "Done")) (PromotedT n))+                (PromotedT (mkName "End"))+            )+        | NormalC n [] <- cons+        ]+    _ -> error "np"++  -- make instance msg+  ss <- newName "s"+  instMsgDesc <- mkInstanceMsg ss (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+            Nothing+            []+            ( AppT+                (AppT (ConT (mkName "TypedSession.Core.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+                              ]+                          )+                          ( 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)+                          )+                          Nothing+                          instMsgDesc+                          []+                       ]+            )+         ]++protocol+  :: forall r bst+   . ( Enum r+     , Bounded r+     , Show r+     , Enum bst+     , Bounded bst+     , Show bst+     , Ord r+     )+  => String -> Name -> Name -> QuasiQuoter+protocol protN roleName bstName =+  QuasiQuoter+    { quoteExp = const $ fail "No protocol parse for exp"+    , quotePat = const $ fail "No protocol parse for pat"+    , quoteType = const $ fail "No protocol parser for type"+    , quoteDec = parseOrThrow+    }+ where+  parseOrThrow :: String -> Q [Dec]+  parseOrThrow st = case runProtocolParser @r @bst st of+    Left e -> fail (show e)+    Right protCreat -> case piple protCreat of+      Left e -> fail (show e)+      Right pipResult -> do+        let graphStr = genGraph @r @bst defaultStrFilEnv pipResult+        runIO $ do+          writeFile (protN <> ".prot") graphStr+          putStrLn graphStr+        d1 <- roleDecs roleName+        d2 <- protDecsAndMsgDecs protN roleName bstName pipResult+        pure (d1 ++ d2)

@@ -28,9 +28,9 @@ import Data.Kind import GHC.Exts (dataToTag#) import GHC.Int (Int (I#))-import TypedProtocol.Codec-import TypedProtocol.Core-import TypedProtocol.Driver+import TypedSession.Codec+import TypedSession.Core+import TypedSession.Driver  {- 

@@ -28,9 +28,9 @@ import Data.Kind import GHC.Exts (dataToTag#) import GHC.Int (Int (I#))-import TypedProtocol.Codec-import TypedProtocol.Core-import TypedProtocol.Driver+import TypedSession.Codec+import TypedSession.Core+import TypedSession.Driver  {- 

@@ -28,9 +28,9 @@ import Data.Kind import GHC.Exts (dataToTag#) import GHC.Int (Int (I#))-import TypedProtocol.Codec-import TypedProtocol.Core-import TypedProtocol.Driver+import TypedSession.Codec+import TypedSession.Core+import TypedSession.Driver  {- 

@@ -16,6 +16,7 @@ module Book3.Main where  import Book3.Peer+import Book3.Protocol import Book3.Type import Control.Carrier.Random.Gen (runRandom) import Control.Concurrent.Class.MonadSTM@@ -24,12 +25,12 @@ import Control.Monad.Class.MonadFork (MonadFork, forkIO) import Control.Monad.Class.MonadSay import Control.Monad.Class.MonadThrow (MonadThrow)+import Control.Monad.IOSim import qualified Data.IntMap as IntMap import System.Random (StdGen, split)-import TypedProtocol.Codec-import TypedProtocol.Core-import TypedProtocol.Driver-import Control.Monad.IOSim+import TypedSession.Codec+import TypedSession.Core+import TypedSession.Driver  mvarsAsChannel   :: (MonadSTM m)@@ -42,7 +43,7 @@   send x = atomically (putTMVar bufferWrite x)   recv = atomically (Just <$> takeTMVar bufferRead) -myTracer :: (MonadSay m) => String -> Tracer Role BookSt m+myTracer :: (MonadSay m) => String -> Tracer BookRole Book m myTracer st v = say (st <> show v)  runAll@@ -56,9 +57,9 @@   => StdGen   -> n () runAll g = do-  buyerTMVar <- newEmptyTMVarIO @n @(AnyMsg Role BookSt)-  buyer2TMVar <- newEmptyTMVarIO @n @(AnyMsg Role BookSt)-  sellerTMVar <- newEmptyTMVarIO @n @(AnyMsg Role BookSt)+  buyerTMVar <- newEmptyTMVarIO @n @(AnyMsg BookRole Book)+  buyer2TMVar <- newEmptyTMVarIO @n @(AnyMsg BookRole Book)+  sellerTMVar <- newEmptyTMVarIO @n @(AnyMsg BookRole Book)   let buyerSellerChannel = mvarsAsChannel @n buyerTMVar sellerTMVar       buyerBuyer2Channel = mvarsAsChannel @n buyerTMVar buyer2TMVar 

@@ -15,40 +15,43 @@  module Book3.Peer where +import Book3.Protocol import Book3.Type import Control.Algebra (Has) import Control.Effect.Random (Random, uniform) import Data.IFunctor (At (..), ireturn, returnAt) import qualified Data.IFunctor as I import Data.Kind-import TypedProtocol.Core+import TypedSession.Core  budget :: Int budget = 16 -data CheckPriceResult :: BookSt -> Type where-  Yes :: CheckPriceResult (S3 [Enough, Support, Two, Found])-  No :: CheckPriceResult (S3 [NotEnough, Support, Two, Found])+type Date = Int +data CheckPriceResult :: Book -> Type where+  Yes :: CheckPriceResult (S5 Enough)+  No :: CheckPriceResult (S5 NotEnough)+ checkPrice   :: (Has Random sig m)   => Int   -> Int-  -> Peer Role BookSt Buyer m CheckPriceResult (S3 s)+  -> Peer BookRole Book Buyer m CheckPriceResult 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 :: BookSt -> Type where-  OTOne :: OT (S1 [One, Found])-  OTTwo :: OT (S1 [Two, Found])+data OT :: Book -> Type where+  OTOne :: OT (S5 One)+  OTTwo :: OT (S1 Two)  choiceOT   :: (Has Random sig m)   => Int-  -> Peer Role BookSt Buyer m OT (S1 s)+  -> Peer BookRole Book Buyer m OT S4 choiceOT _i = I.do   At b <- liftm $ uniform @Bool   if b@@ -57,7 +60,7 @@  buyerPeer   :: (Has Random sig m)-  => Peer Role BookSt Buyer m (At (Maybe Date) (Done Buyer)) S0+  => Peer BookRole Book Buyer m (At (Maybe Date) (Done Buyer)) S0 buyerPeer = I.do   yield (Title "haskell book")   await I.>>= \case@@ -67,7 +70,6 @@     Recv (Price i) -> I.do       choiceOT i I.>>= \case         OTOne -> I.do-          yield OneAfford           yield OneAccept           Recv (OneDate d) <- await           yield (OneSuccess d)@@ -76,7 +78,7 @@  where   f1     :: (Has Random sig m)-    => Peer Role BookSt 'Buyer m (At (Maybe Date) (Done Buyer)) ('S1 '[ 'Two, 'Found])+    => Peer BookRole Book 'Buyer m (At (Maybe Date) (Done Buyer)) ('S1 'Two)   f1 = I.do     yield (PriceToBuyer2 300)     await I.>>= \case@@ -95,14 +97,14 @@             yield TwoFailed             returnAt Nothing -data BuySupp :: BookSt -> Type where-  BNS :: BuySupp (S6 '[NotSupport, Two, Found])-  BS :: BuySupp (S6 '[Support, Two, Found])+data BuySupp :: Book -> Type where+  BNS :: BuySupp (S6 NotSupport)+  BS :: BuySupp (S6 Support)  choiceB   :: (Has Random sig m)   => Int-  -> Peer Role BookSt Buyer2 m BuySupp (S6 s)+  -> Peer BookRole Book Buyer2 m BuySupp S7 choiceB _i = I.do   At b <- liftm $ uniform @Bool   if b@@ -111,13 +113,11 @@  buyer2Peer   :: (Has Random sig m)-  => Peer Role BookSt Buyer2 m (At (Maybe Date) (Done Buyer2)) (S1 s)+  => Peer BookRole Book Buyer2 m (At (Maybe Date) (Done Buyer2)) (S1 s) buyer2Peer = I.do   await I.>>= \case     Recv SellerNoBook -> returnAt Nothing-    Recv OneAfford -> I.do-      Recv (OneSuccess d) <- await-      returnAt (Just d)+    Recv (OneSuccess d) -> returnAt (Just d)     Recv (PriceToBuyer2 i) -> I.do       choiceB i I.>>= \case         BNS -> I.do@@ -129,14 +129,14 @@             Recv (TwoSuccess d) -> returnAt $ Just d             Recv TwoFailed -> returnAt Nothing -data FindBookResult :: BookSt -> Type where-  NotFound' :: FindBookResult (S2 '[NotFound])-  Found' :: FindBookResult (S2 '[Found])+data FindBookResult :: Book -> Type where+  NotFound' :: FindBookResult (S2 NotFound)+  Found' :: FindBookResult (S2 Found)  findBook   :: (Has Random sig m)   => String-  -> Peer Role BookSt Seller m FindBookResult (S2 s)+  -> Peer BookRole Book Seller m FindBookResult S3 findBook _st = I.do   At b <- liftm $ uniform @Bool   if b@@ -145,7 +145,7 @@  sellerPeer   :: (Has Random sig m)-  => Peer Role BookSt Seller m (At () (Done Seller)) S0+  => Peer BookRole Book Seller m (At () (Done Seller)) S0 sellerPeer = I.do   Recv (Title st) <- await   findBook st I.>>= \case

@@ -0,0 +1,143 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MagicHash #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE QuasiQuotes #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# OPTIONS_GHC -Wno-orphans #-}++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+               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+              Terminal+            BranchSt Two +              Msg "PriceToBuyer2" ["Int"] Buyer Buyer2+              Branch Buyer2 {+                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+                      Terminal+                    BranchSt NotEnough +                      Msg "TwoNotBuy1" [] Buyer Seller+                      Msg "TwoFailed" [] Buyer Buyer2+                      Terminal +                }+              }+          }+        }++|]++{-+-----------------------------------------------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+  Title{} -> AnyMsg x+  NoBook{} -> AnyMsg x+  SellerNoBook{} -> AnyMsg x+  Price{} -> AnyMsg x+  OneAccept{} -> AnyMsg x+  OneDate{} -> AnyMsg x+  OneSuccess{} -> AnyMsg x+  PriceToBuyer2{} -> AnyMsg x+  NotSupport1{} -> AnyMsg x+  TwoNotBuy{} -> AnyMsg x+  SupportVal{} -> AnyMsg x+  TwoAccept{} -> AnyMsg x+  TwoDate{} -> AnyMsg x+  TwoSuccess{} -> AnyMsg x+  TwoNotBuy1{} -> AnyMsg x+  TwoFailed{} -> AnyMsg x++decodeMsg+  :: DecodeStep+      (AnyMsg BookRole Book)+      CodecFailure+      (AnyMsg BookRole Book)+decodeMsg =+  DecodePartial $ \case+    Nothing -> DecodeFail (CodecFailure "expected more data")+    Just anyMsg -> DecodeDone anyMsg Nothing++instance Show (AnyMsg BookRole Book) where+  show (AnyMsg msg) = case msg of+    Title st -> "Title " <> show st+    NoBook -> "NoBook"+    SellerNoBook -> "SellerNoBook"+    Price i -> "Price " <> show i+    OneAccept -> "OneAccept"+    OneDate d -> "OneDate " <> show d+    OneSuccess d -> "OneSuccess" <> show d+    PriceToBuyer2 i -> "PriceToBuyer2 " <> show i+    NotSupport1 -> "NotSupport1"+    TwoNotBuy -> "TwoNotBuy"+    SupportVal v -> "SupportVal " <> show v+    TwoAccept -> "TwoAccept"+    TwoDate d -> "TwoDate " <> show d+    TwoSuccess d -> "TwoSuccess " <> show d+    TwoNotBuy1 -> "TwoNotBuy1"+    TwoFailed -> "TwoFailed"

@@ -10,101 +10,17 @@ {-# LANGUAGE QualifiedDo #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-}  module Book3.Type where -import Data.IFunctor (Sing, SingI)-import qualified Data.IFunctor as I-import Data.Kind-import GHC.Exts (dataToTag#)-import GHC.Int (Int (I#))-import TypedProtocol.Codec-import TypedProtocol.Core--{-----------------------------Buyer-------------------------Seller------------------------Buyer2----------------------------                             S0                            S0                          (S1 s)-            Title            |            ----->           |-                           (S2 s)                        (S2 s)                        (S1 s)-    ---------------------------------------------------[NotFound]----------------------------------------------------                           (S2 s)                   (S2 [NotFound])                    (S1 s)-            NoBook           |            <-----           |-                      (S1 [NotFound])                     End                          (S1 s)-         SellerNoBook        |                           ----->                          |-                            End                           End                           End-                                                        Terminal--    ----------------------------------------------------[Found]------------------------------------------------------                           (S2 s)                     (S2 [Found])                     (S1 s)-            Price            |            <-----           |-                           (S1 s)                        (S3 s)                        (S1 s)-        ----------------------------------------------[One,Found]------------------------------------------------                      (S1 [One,Found])                   (S3 s)                        (S1 s)-          OneAfford          |                           ----->                          |-                      (S3 [One,Found])                   (S3 s)                          S4-          OneAccept          |            ----->           |-                             S5                            S5                            S4-           OneDate           |            <-----           |-                             S4                           End                            S4-          OneSuccess         |                           ----->                          |-                            End                           End                           End-                                                        Terminal--        ----------------------------------------------[Two,Found]------------------------------------------------                      (S1 [Two,Found])                   (S3 s)                        (S1 s)-        PriceToBuyer2        |                           ----->                          |-                           (S6 s)                        (S3 s)                        (S6 s)-            -------------------------------------[NotSupport,Two,Found]--------------------------------------                           (S6 s)                        (S3 s)             (S6 [NotSupport,Two,Found])-          NotSupport1        |                           <-----                          |-                (S3 [NotSupport,Two,Found])              (S3 s)                         End-          TwoNotBuy          |            ----->           |-                            End                           End                           End-                                                        Terminal--            --------------------------------------[Support,Two,Found]----------------------------------------                           (S6 s)                        (S3 s)               (S6 [Support,Two,Found])-          SupportVal         |                           <-----                          |-                           (S3 s)                        (S3 s)                        (S7 s)-                -------------------------------[Enough,Support,Two,Found]--------------------------------              (S3 [Enough,Support,Two,Found])            (S3 s)                        (S7 s)-          TwoAccept          |            ----->           |-                             S8                            S8                          (S7 s)-           TwoDate           |            <-----           |-              (S7 [Enough,Support,Two,Found])             End                          (S7 s)-          TwoSuccess         |                           ----->                          |-                            End                           End                           End-                                                        Terminal--                -----------------------------[NotEnough,Support,Two,Found]-------------------------------             (S3 [NotEnough,Support,Two,Found])          (S3 s)                        (S7 s)-          TwoNotBuy1         |            ----->           |-             (S7 [NotEnough,Support,Two,Found])           End                          (S7 s)-          TwoFailed          |                           ----->                          |-                            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+import Language.Haskell.TH.Quote (QuasiQuoter)+import TypedSession.TH (protocol) -instance SingI Seller where-  sing = SSeller+data BookRole = Buyer | Seller | Buyer2+  deriving (Show, Eq, Ord, Enum, Bounded)  data BookBranchSt   = NotFound@@ -115,142 +31,13 @@   | NotSupport   | Enough   | NotEnough-  deriving (Show)--data BookSt-  = S0-  | S1 [BookBranchSt]-  | S2 [BookBranchSt]-  | S3 [BookBranchSt]-  | S4-  | S5-  | S6 [BookBranchSt]-  | S7 [BookBranchSt]-  | S8-  | End--data SBookSt :: BookSt -> Type where-  SS0 :: SBookSt S0-  SS1 :: SBookSt (S1 s)-  SS2 :: SBookSt (S2 s)-  SS3 :: SBookSt (S3 s)-  SS4 :: SBookSt S4-  SS5 :: SBookSt S5-  SS6 :: SBookSt (S6 s)-  SS7 :: SBookSt (S7 s)-  SS8 :: SBookSt S8-  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 where-  sing = SS5--instance SingI (S6 s) where-  sing = SS6--instance SingI (S7 s) where-  sing = SS7--instance SingI S8 where-  sing = SS8--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)-    NoBook :: Msg Role BookSt (S2 '[NotFound]) '(Seller, End) '(Buyer, S1 '[NotFound])-    SellerNoBook :: Msg Role BookSt (S1 '[NotFound]) '(Buyer, End) '(Buyer2, End)-    Price :: Int -> Msg Role BookSt (S2 '[Found]) '(Seller, S3 s) '(Buyer, S1 s)-    OneAfford :: Msg Role BookSt (S1 '[One, Found]) '(Buyer, S3 '[One, Found]) '(Buyer2, S4)-    OneAccept :: Msg Role BookSt (S3 '[One, Found]) '(Buyer, S5) '(Seller, S5)-    OneDate :: Date -> Msg Role BookSt S5 '(Seller, End) '(Buyer, S4)-    OneSuccess :: Date -> Msg Role BookSt S4 '(Buyer, End) '(Buyer2, End)-    PriceToBuyer2 :: Int -> Msg Role BookSt (S1 '[Two, Found]) '(Buyer, S6 s) '(Buyer2, S6 s)-    NotSupport1 :: Msg Role BookSt (S6 '[NotSupport, Two, Found]) '(Buyer2, End) '(Buyer, S3 '[NotSupport, Two, Found])-    TwoNotBuy :: Msg Role BookSt (S3 '[NotSupport, Two, Found]) '(Buyer, End) '(Seller, End)-    SupportVal :: Int -> Msg Role BookSt (S6 '[Support, Two, Found]) '(Buyer2, S7 s) '(Buyer, S3 s)-    TwoAccept :: Msg Role BookSt (S3 '[Enough, Support, Two, Found]) '(Buyer, S8) '(Seller, S8)-    TwoDate :: Date -> Msg Role BookSt S8 '(Seller, End) '(Buyer, S7 '[Enough, Support, Two, Found])-    TwoSuccess :: Date -> Msg Role BookSt (S7 '[Enough, Support, Two, Found]) '(Buyer, End) '(Buyer2, End)-    TwoNotBuy1 :: Msg Role BookSt (S3 '[NotEnough, Support, Two, Found]) '(Buyer, S7 '[NotEnough, Support, Two, Found]) '(Seller, End)-    TwoFailed :: Msg Role BookSt (S7 '[NotEnough, Support, Two, Found]) '(Buyer, End) '(Buyer2, End)--encodeMsg :: Encode Role BookSt (AnyMsg Role BookSt)-encodeMsg = Encode $ \x -> case x of-  Title{} -> AnyMsg x-  NoBook{} -> AnyMsg x-  SellerNoBook{} -> AnyMsg x-  Price{} -> AnyMsg x-  OneAfford{} -> AnyMsg x-  OneAccept{} -> AnyMsg x-  OneDate{} -> AnyMsg x-  OneSuccess{} -> AnyMsg x-  PriceToBuyer2{} -> AnyMsg x-  NotSupport1{} -> AnyMsg x-  TwoNotBuy{} -> AnyMsg x-  SupportVal{} -> AnyMsg x-  TwoAccept{} -> AnyMsg x-  TwoDate{} -> AnyMsg x-  TwoSuccess{} -> AnyMsg x-  TwoNotBuy1{} -> AnyMsg x-  TwoFailed{} -> 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+  deriving (Show, Eq, Ord, Enum, Bounded) -instance Show (AnyMsg Role BookSt) where-  show (AnyMsg msg) = case msg of-    Title st -> "Title " <> show st-    NoBook -> "NoBook"-    SellerNoBook -> "SellerNoBook"-    Price i -> "Price " <> show i-    OneAfford -> "OneAfford"-    OneAccept -> "OneAccept"-    OneDate d -> "OneDate " <> show d-    OneSuccess d -> "OneSuccess" <> show d-    PriceToBuyer2 i -> "PriceToBuyer2 " <> show i-    NotSupport1 -> "NotSupport1"-    TwoNotBuy -> "TwoNotBuy"-    SupportVal v -> "SupportVal " <> show v-    TwoAccept -> "TwoAccept"-    TwoDate d -> "TwoDate " <> show d-    TwoSuccess d -> "TwoSuccess " <> show d-    TwoNotBuy1 -> "TwoNotBuy1"-    TwoFailed -> "TwoFailed"+bookProtocol :: QuasiQuoter+bookProtocol =+  protocol+    @BookRole+    @BookBranchSt+    "Book"+    ''BookRole+    ''BookBranchSt

@@ -28,9 +28,9 @@ import Data.Kind import GHC.Exts (dataToTag#) import GHC.Int (Int (I#))-import TypedProtocol.Codec-import TypedProtocol.Core-import TypedProtocol.Driver+import TypedSession.Codec+import TypedSession.Core+import TypedSession.Driver  {- 

@@ -20,7 +20,7 @@ -- PVP summary:     +-+------- breaking API changes --                  | | +----- non-breaking API additions --                  | | | +--- code changes with no API change-version:            0.1.0.0+version:            0.1.1.0  -- A short (one-line) description of the package. synopsis: typed session framework@@ -63,9 +63,10 @@      -- Modules exported by the library.     exposed-modules: Data.IFunctor-                   , TypedProtocol.Core-                   , TypedProtocol.Codec-                   , TypedProtocol.Driver+                   , TypedSession.Core+                   , TypedSession.Codec+                   , TypedSession.Driver+                   , TypedSession.TH      -- Modules included in this library but not exported.     -- other-modules:@@ -77,6 +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      -- Directories containing source files.     hs-source-dirs:   src@@ -96,6 +99,7 @@                  , Book1                  , Book2                  , Book3.Type+                 , Book3.Protocol                  , Book3.Peer                  , Book3.Main                  , PingPong@@ -121,7 +125,8 @@         io-sim,         random,         fused-effects,-        fused-effects-random+        fused-effects-random,+        template-haskell     ghc-options:  -Werror=inaccessible-code -threaded  source-repository head