packages feed

typed-session 0.2.0.1 → 0.3.0.0

raw patch · 6 files changed

+233/−102 lines, 6 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

- TypedSession.Driver: type SendMap (role' :: k) (m :: Type -> Type) bytes = IntMap bytes -> m ()
+ TypedSession.Driver: NotConnect :: role' -> NotConnect role'
+ TypedSession.Driver: SomeRole :: Sing r -> SomeRole role'
+ TypedSession.Driver: [terminalDecodeThreads] :: Driver role' ps (m :: Type -> Type) -> [m ()]
+ TypedSession.Driver: data NotConnect role'
+ TypedSession.Driver: data SomeRole role'
+ TypedSession.Driver: instance (GHC.Internal.Show.Show role', GHC.Internal.Data.Typeable.Internal.Typeable role') => GHC.Internal.Exception.Type.Exception (TypedSession.Driver.NotConnect role')
+ TypedSession.Driver: instance GHC.Internal.Show.Show role' => GHC.Internal.Show.Show (TypedSession.Driver.NotConnect role')
+ TypedSession.Driver: localDriverSimple :: forall role' ps m n. (Monad m, Monad n, MonadSTM n, Enum role', MonadThrow n, Show role', Typeable role') => Tracer role' ps n -> IntMap (MsgCache role' ps n) -> SomeRole role' -> (forall a. () => n a -> m a) -> Driver role' ps m
+ TypedSession.Driver: type ConnChannels role' (m :: Type -> Type) bytes = [(SomeRole role', Channel m bytes)]
- TypedSession.Core: type MsgCache role' ps = IntMap AnyMsg role' ps
+ TypedSession.Core: type MsgCache role' ps (n :: Type -> Type) = TVar n IntMap AnyMsg role' ps
- TypedSession.Driver: Driver :: (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 ()) -> (forall (st' :: ps). SingToInt ps => Sing st' -> m (AnyMsg role' ps)) -> Driver role' ps (m :: Type -> Type)
+ TypedSession.Driver: Driver :: (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 ()) -> (forall (st' :: ps). SingToInt ps => Sing st' -> m (AnyMsg role' ps)) -> [m ()] -> Driver role' ps (m :: Type -> Type)
- TypedSession.Driver: decodeLoop :: (Exception failure, MonadDelay n, MonadSTM n, MonadThrow n) => Tracer role' ps n -> Maybe bytes -> Decode role' ps failure bytes -> Channel n bytes -> TVar n (MsgCache role' ps) -> n ()
+ TypedSession.Driver: decodeLoop :: (Exception failure, MonadDelay n, MonadSTM n, MonadThrow n) => Maybe bytes -> Decode role' ps failure bytes -> Channel n bytes -> MsgCache role' ps n -> n ()
- TypedSession.Driver: 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
+ TypedSession.Driver: driverSimple :: forall role' ps failure bytes m n. (Monad m, Monad n, MonadSTM n, MonadFork n, MonadDelay n, MonadThrow n, SingToInt role', Enum role', Show role', Typeable role', Exception failure) => Tracer role' ps n -> Encode role' ps bytes -> Decode role' ps failure bytes -> ConnChannels role' n bytes -> (forall a. () => n a -> m a) -> n (Driver role' ps m)

Files

src/TypedSession/Core.hs view
@@ -14,6 +14,7 @@  module TypedSession.Core where +import Control.Concurrent.Class.MonadSTM (MonadSTM (..)) import Data.IFunctor import Data.IntMap (IntMap) import Data.Kind@@ -125,7 +126,7 @@ 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)+type MsgCache role' ps n = TVar n (IntMap (AnyMsg role' ps))  {- | Packaging of Msg, shielding part of the type information, mainly used for serialization.
src/TypedSession/Driver.hs view
@@ -25,18 +25,19 @@  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.MonadFork (MonadFork (killThread), forkIO) import Control.Monad.Class.MonadThrow (MonadThrow, throwIO) import Control.Monad.Class.MonadTimer (MonadDelay, threadDelay)+import Data.Data (Typeable) import Data.IFunctor (At (..), Sing, SingI (sing)) import qualified Data.IFunctor as I import Data.IntMap (IntMap) import qualified Data.IntMap as IntMap+import Data.Traversable (for) import GHC.Exception (Exception) import TypedSession.Codec import TypedSession.Core@@ -63,6 +64,7 @@        . (SingToInt ps)       => Sing st'       -> m (AnyMsg role' ps)+  , terminalDecodeThreads :: [m ()]   }  {- |@@ -76,8 +78,10 @@   => Driver role' ps m   -> Peer role' ps r m (At a (Done r)) st   -> m a-runPeerWithDriver Driver{sendMsg, recvMsg} =-  go+runPeerWithDriver Driver{sendMsg, recvMsg, terminalDecodeThreads} peer = do+  a <- go peer+  sequence_ terminalDecodeThreads+  pure a  where   go     :: forall st'@@ -115,19 +119,26 @@ 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.+ConnChannels aggregates the multiple connect channels together. -}-type SendMap role' m bytes = IntMap (bytes -> m ())+type ConnChannels role' m bytes = [(SomeRole role', Channel m bytes)] +data NotConnect role' = NotConnect role'+  deriving (Show)++instance (Show role', Typeable role') => Exception (NotConnect role')++data SomeRole role' = forall (r :: role'). (SingToInt role') => SomeRole (Sing r)+ {- | -Build Driver through SendMap and MsgCache.+Build Driver through ConnChannels. 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.+3. `Decode role' ps failure bytes` bytes decode function, converts bytes into Msg.+4. `forall a. n a -> m a` This is a bit complicated, I will explain it in detail below.  I see Peer as three layers: @@ -136,53 +147,74 @@ 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+  :: forall role' ps failure bytes m n    . ( Monad m      , Monad n      , MonadSTM n+     , MonadFork n+     , MonadDelay n+     , MonadThrow n+     , SingToInt role'+     , Enum role'+     , Show role'+     , Typeable role'+     , Exception failure      )   => Tracer role' ps n   -> Encode role' ps bytes-  -> SendMap role' n bytes-  -> TVar n (MsgCache role' ps)+  -> Decode role' ps failure bytes+  -> ConnChannels role' n bytes   -> (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))+  -> n (Driver role' ps m)+driverSimple+  tracer+  Encode{encode}+  decodeV+  connChannels+  liftFun = do+    msgCache <- newTVarIO IntMap.empty+    ths <- for connChannels $ \(_, channel) -> forkIO $ decodeLoop Nothing decodeV channel msgCache+    let terminalDecodeThreads = map (\tid -> liftFun $ killThread tid) ths+    pure $ Driver{sendMsg, recvMsg = recvMsg' msgCache, terminalDecodeThreads}+   where+    sendMap = IntMap.fromList $ fmap (\(SomeRole r, c) -> (singToInt r, send c)) connChannels+    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+      let recvKey = singToInt role+      case IntMap.lookup recvKey sendMap of+        Nothing -> do+          let recvRole = toEnum @role' recvKey+          throwIO (NotConnect recvRole)+        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+    recvMsg'+      :: forall (st' :: ps)+       . (SingToInt ps)+      => MsgCache role' ps n+      -> Sing st'+      -> m (AnyMsg role' ps)+    recvMsg' msgCache sst' = do+      let singInt = singToInt sst'+      liftFun $ do+        anyMsg <- atomically $ do+          agencyMsg <- readTVar msgCache+          case IntMap.lookup singInt agencyMsg of+            Nothing -> retry+            Just v -> do+              writeTVar msgCache (IntMap.delete singInt agencyMsg)+              pure v+        tracer (TraceRecvMsg (anyMsg))+        pure anyMsg  {- | decode loop, usually in a separate thread.@@ -199,13 +231,12 @@ -} decodeLoop   :: (Exception failure, MonadDelay n, MonadSTM n, MonadThrow n)-  => Tracer role' ps n-  -> Maybe bytes+  => Maybe bytes   -> Decode role' ps failure bytes   -> Channel n bytes-  -> TVar n (MsgCache role' ps)+  -> MsgCache role' ps n   -> n ()-decodeLoop tracer mbt d@Decode{decode} channel tvar = do+decodeLoop mbt d@Decode{decode} channel tvar = do   result <- runDecoderWithChannel channel mbt decode   case result of     Right (AnyMsg msg, mbt') -> do@@ -215,7 +246,68 @@         case IntMap.lookup agencyInt agencyMsg of           Nothing -> writeTVar tvar (IntMap.insert agencyInt (AnyMsg msg) agencyMsg)           Just _v -> retry-      decodeLoop tracer mbt' d channel tvar+      decodeLoop mbt' d channel tvar     Left failure -> do       threadDelay 1_000_000       throwIO failure++localDriverSimple+  :: forall role' ps m n+   . ( Monad m+     , Monad n+     , MonadSTM n+     , Enum role'+     , MonadThrow n+     , Show role'+     , Typeable role'+     )+  => Tracer role' ps n+  -> IntMap (MsgCache role' ps n)+  -> SomeRole role'+  -> (forall a. n a -> m a)+  -> Driver role' ps m+localDriverSimple tracer allMsgCache (SomeRole r) liftFun =+  Driver{sendMsg, recvMsg = recvMsg' (allMsgCache IntMap.! (singToInt r)), terminalDecodeThreads = []}+ 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+    let recvKey = singToInt role+    case IntMap.lookup (singToInt role) allMsgCache of+      Nothing -> do+        let recvRole = toEnum @role' recvKey+        throwIO (NotConnect recvRole)+      Just ttvar -> atomically $ do+        agencyMsg <- readTVar ttvar+        let singInt = singToInt (sing @from)+        case IntMap.lookup singInt agencyMsg of+          Nothing -> writeTVar ttvar (IntMap.insert singInt (AnyMsg msg) agencyMsg)+          Just _v -> retry+    tracer (TraceSendMsg (AnyMsg msg))++  recvMsg'+    :: forall (st' :: ps)+     . (SingToInt ps)+    => MsgCache role' ps n+    -> Sing st'+    -> m (AnyMsg role' ps)+  recvMsg' msgCache sst' = do+    let singInt = singToInt sst'+    liftFun $ do+      anyMsg <- atomically $ do+        agencyMsg <- readTVar msgCache+        case IntMap.lookup singInt agencyMsg of+          Nothing -> retry+          Just v -> do+            writeTVar msgCache (IntMap.delete singInt agencyMsg)+            pure v+      tracer (TraceRecvMsg (anyMsg))+      pure anyMsg
test/Book3/Main.hs view
@@ -25,13 +25,12 @@ 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 Control.Monad.IOSim-import qualified Data.IntMap as IntMap import System.Random (StdGen, split) import TypedSession.Codec import TypedSession.Core import TypedSession.Driver-import Control.Monad.Class.MonadTimer (MonadDelay)  mvarsAsChannel   :: (MonadSTM m)@@ -62,36 +61,32 @@   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 -      sellerBuyerChannel = mvarsAsChannel @n sellerTMVar buyerTMVar--      buyer2BuyerChannel = mvarsAsChannel @n buyer2TMVar buyerTMVar--      sendFun bufferWrite x = atomically @n (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 sendM-      buyer2Driver = driverSimple (myTracer "buyer2 :") encodeMsg sendToRole buyer2Tvar sendM-      sellerDriver = driverSimple (myTracer "seller :") encodeMsg sendToRole sellerTvar sendM-  -- 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+  buyerDriver <-+    driverSimple+      (myTracer "buyer :")+      encodeMsg+      (Decode decodeMsg)+      [ (SomeRole SSeller, mvarsAsChannel buyerTMVar sellerTMVar)+      , (SomeRole SBuyer2, mvarsAsChannel buyerTMVar buyer2TMVar)+      ]+      sendM -  -- fork seller decode thread, buyer -> seller-  forkIO $ decodeLoop (myTracer "seller :") Nothing (Decode decodeMsg) sellerBuyerChannel sellerTvar+  buyer2Driver <-+    driverSimple+      (myTracer "buyer2 :")+      encodeMsg+      (Decode decodeMsg)+      [(SomeRole SBuyer, mvarsAsChannel buyer2TMVar buyerTMVar)]+      sendM -  -- fork buyer2 decode thread, buyer -> buyer2-  forkIO $ decodeLoop (myTracer "buyer2 :") Nothing (Decode decodeMsg) buyer2BuyerChannel buyer2Tvar+  sellerDriver <-+    driverSimple+      (myTracer "seller :")+      encodeMsg+      (Decode decodeMsg)+      [(SomeRole SBuyer, mvarsAsChannel sellerTMVar buyerTMVar)]+      sendM    let (g0, g1) = split g       (g2, g3) = split g0
test/Book3/Peer.hs view
@@ -12,16 +12,25 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# OPTIONS_GHC -Wno-unused-do-bind #-}  module Book3.Peer where  import Book3.Protocol import Book3.Type-import Control.Algebra (Has)-import Control.Effect.Random (Random, uniform)-import Data.IFunctor (At (..), returnAt)+import Control.Carrier.Lift+import Control.Carrier.Random.Gen+import Control.Carrier.State.Strict (runState)+import Control.Effect.State+import Control.Monad+import Data.IFunctor (At (..), SingI (..), returnAt) import qualified Data.IFunctor as I+import Data.IntMap (IntMap)+import qualified Data.IntMap as IntMap+import System.Random (StdGen, mkStdGen, randomIO) import TypedSession.Core+import Unsafe.Coerce (unsafeCoerce)  budget :: Int budget = 16@@ -135,3 +144,52 @@         TwoNotBuy -> returnAt ()         TwoAccept -> yield (TwoDate 100)         TwoNotBuy1 -> returnAt ()++-- data AnyPeer role' ps m where+--   AnyPeer :: Peer role' ps r m (At () (Done r)) st -> AnyPeer role' ps m++-- runAnyPeers+--   :: forall n role' ps sig m+--    . ( SingToInt role'+--      , Has (State (IntMap (AnyPeer role' ps n))) sig m+--      )+--   => (forall a. n a -> m a) -> m ()+-- runAnyPeers liftFun = do+--   im <- get @(IntMap (AnyPeer role' ps n))+--   case IntMap.keys im of+--     [] -> pure ()+--     keys -> do+--       forM_ keys $ \key -> do+--         gets @(IntMap (AnyPeer role' ps n)) (IntMap.lookup key) >>= \case+--           Nothing -> error "np"+--           Just (AnyPeer peer) -> case peer of+--             IReturn (At ()) -> do+--               modify @(IntMap (AnyPeer role' ps n)) (IntMap.delete key)+--             LiftM fm -> do+--               np <- liftFun fm+--               modify @(IntMap (AnyPeer role' ps n)) (IntMap.insert key (AnyPeer np))+--             Yield (msg :: Msg role' ps st send sps recv rps) cont -> do+--               let recvKey = (singToInt $ sing @recv)+--               gets @(IntMap (AnyPeer role' ps n)) (IntMap.lookup recvKey) >>= \case+--                 Nothing -> error "np"+--                 Just (AnyPeer recvPeer) -> case recvPeer of+--                   Await scont -> do+--                     let nS = scont (unsafeCoerce msg)+--                     modify @(IntMap (AnyPeer role' ps n)) (IntMap.insert recvKey (AnyPeer nS))+--                   _ -> error "np"+--               modify @(IntMap (AnyPeer role' ps n)) (IntMap.insert key (AnyPeer cont))+--             Await{} -> pure ()+--       runAnyPeers @n @role' @ps liftFun++-- runAP = do+--   i <- randomIO @Int+--   runRandom (mkStdGen i)+--     $ runM @(RandomC StdGen IO)+--     $ runState+--       ( IntMap.fromList+--           [ (singToInt SBuyer, AnyPeer (buyerPeer @_ @(RandomC StdGen IO) I.>> returnAt ()))+--           , (singToInt SBuyer2, AnyPeer (buyer2Peer @_ @(RandomC StdGen IO) I.>> returnAt ()))+--           , (singToInt SSeller, AnyPeer (sellerPeer @_ @(RandomC StdGen IO) I.>> returnAt ()))+--           ]+--       )+--     $ (runAnyPeers @(RandomC StdGen IO) @BookRole @Book sendM)
test/Book3/Protocol.hs view
@@ -112,18 +112,3 @@     TwoSuccess d -> "TwoSuccess " <> show d     TwoNotBuy1 -> "TwoNotBuy1"     TwoFailed -> "TwoFailed"--type Start s = Maybe s-type Start1  = Int--$( do - x <- reify ''Start - y <- reify ''Start1- runIO $ do -  putStrLn "--------------------------------------------"-  putStrLn $ show x-  putStrLn $ show y-  putStrLn "--------------------------------------------"- pure []--  )
typed-session.cabal view
@@ -20,7 +20,7 @@ -- PVP summary:     +-+------- breaking API changes --                  | | +----- non-breaking API additions --                  | | | +--- code changes with no API change-version:            0.2.0.1+version:            0.3.0.0  -- A short (one-line) description of the package. synopsis: typed session framework