--  This part of the code comes from typed-protocols, I modified a few things.
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE NumericUnderscores #-}
{-# 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.

-}
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
import Unsafe.Coerce (unsafeCoerce)

{- |
Contains two functions sendMsg, recvMsg.
runPeerWithDriver uses them to send and receive Msg.
-}
data Driver role' ps m
  = Driver
  { forall role' ps (m :: * -> *).
Driver role' ps m
-> 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 ()
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 ()
  , forall role' ps (m :: * -> *).
Driver role' ps m
-> forall (st' :: ps).
   SingToInt ps =>
   Sing st' -> m (AnyMsg role' ps)
recvMsg
      :: forall (st' :: ps)
       . (SingToInt ps)
      => Sing st'
      -> m (AnyMsg role' ps)
  , forall role' ps (m :: * -> *). Driver role' ps m -> [m ()]
terminalDecodeThreads :: [m ()]
  }

{- |
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 :: 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{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 ()
sendMsg :: forall role' ps (m :: * -> *).
Driver role' ps m
-> 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 ()
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 ()
sendMsg, forall (st' :: ps). SingToInt ps => Sing st' -> m (AnyMsg role' ps)
recvMsg :: forall role' ps (m :: * -> *).
Driver role' ps m
-> forall (st' :: ps).
   SingToInt ps =>
   Sing st' -> m (AnyMsg role' ps)
recvMsg :: forall (st' :: ps). SingToInt ps => Sing st' -> m (AnyMsg role' ps)
recvMsg, [m ()]
terminalDecodeThreads :: forall role' ps (m :: * -> *). Driver role' ps m -> [m ()]
terminalDecodeThreads :: [m ()]
terminalDecodeThreads} Peer role' ps r m (At a (Done r)) st
peer = do
  a <- Peer role' ps r m (At a (Done r)) st -> m a
forall (st' :: ps). Peer role' ps r m (At a (Done r)) st' -> m a
go Peer role' ps r m (At a (Done r)) st
peer
  sequence_ terminalDecodeThreads
  pure a
 where
  go
    :: forall st'
     . Peer role' ps r m (At a (Done r)) st'
    -> m a
  go :: forall (st' :: ps). Peer role' ps r m (At a (Done r)) st' -> m a
go (IReturn (At a
a)) = a -> m a
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
a
  go (LiftM m (Peer role' ps r m (At a (Done r)) st')
k) = m (Peer role' ps r m (At a (Done r)) st')
k m (Peer role' ps r m (At a (Done r)) st')
-> (Peer role' ps r m (At a (Done r)) st' -> m a) -> m a
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Peer role' ps r m (At a (Done r)) st' -> m a
forall (st' :: ps). Peer role' ps r m (At a (Done r)) st' -> m a
go
  go (Yield (Msg role' ps st' r sps recv rps
msg :: Msg role' ps st' r sps recv rps) Peer role' ps r m (At a (Done r)) sps
k) = do
    Sing recv -> Msg role' ps st' r sps recv rps -> m ()
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 ()
sendMsg (forall (a :: role'). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @recv) Msg role' ps st' r sps recv rps
msg
    Peer role' ps r m (At a (Done r)) sps -> m a
forall (st' :: ps). Peer role' ps r m (At a (Done r)) st' -> m a
go Peer role' ps r m (At a (Done r)) sps
k
  go (Await (Msg role' ps st' send sps r ~> Peer role' ps r m (At a (Done r))
k :: (Msg role' ps st' send sps r I.~> Peer role' ps r m ia))) = do
    AnyMsg msg <- Sing st' -> m (AnyMsg role' ps)
forall (st' :: ps). SingToInt ps => Sing st' -> m (AnyMsg role' ps)
recvMsg (forall (a :: ps). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @st')
    go (k $ unsafeCoerce 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 :: TraceSendRecv role' ps -> String
show (TraceSendMsg AnyMsg role' ps
msg) = String
"Send " String -> ShowS
forall a. [a] -> [a] -> [a]
++ AnyMsg role' ps -> String
forall a. Show a => a -> String
show AnyMsg role' ps
msg
  show (TraceRecvMsg AnyMsg role' ps
msg) = String
"Recv " String -> ShowS
forall a. [a] -> [a] -> [a]
++ AnyMsg role' ps -> String
forall a. Show a => a -> String
show AnyMsg role' ps
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 :: forall (m :: * -> *) a. Monad m => a -> m ()
nullTracer a
_ = () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

{- |
ConnChannels aggregates the multiple connect channels together.
-}
type ConnChannels role' m bytes = [(SomeRole role', Channel m bytes)]

data NotConnect role' = NotConnect role'
  deriving (Int -> NotConnect role' -> ShowS
[NotConnect role'] -> ShowS
NotConnect role' -> String
(Int -> NotConnect role' -> ShowS)
-> (NotConnect role' -> String)
-> ([NotConnect role'] -> ShowS)
-> Show (NotConnect role')
forall role'. Show role' => Int -> NotConnect role' -> ShowS
forall role'. Show role' => [NotConnect role'] -> ShowS
forall role'. Show role' => NotConnect role' -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall role'. Show role' => Int -> NotConnect role' -> ShowS
showsPrec :: Int -> NotConnect role' -> ShowS
$cshow :: forall role'. Show role' => NotConnect role' -> String
show :: NotConnect role' -> String
$cshowList :: forall role'. Show role' => [NotConnect role'] -> ShowS
showList :: [NotConnect role'] -> ShowS
Show)

instance (Show role', Typeable role') => Exception (NotConnect role')

data SomeRole role' = forall (r :: role'). (SingToInt role') => SomeRole (Sing r)

{- |

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. `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:

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 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)
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)
driverSimple
  Tracer role' ps n
tracer
  Encode{forall (send :: role') (recv :: role') (st :: ps) (st' :: ps)
       (st'' :: ps).
Msg role' ps st send st' recv st'' -> bytes
encode :: forall (send :: role') (recv :: role') (st :: ps) (st' :: ps)
       (st'' :: ps).
Msg role' ps st send st' recv st'' -> bytes
encode :: forall role' ps bytes.
Encode role' ps bytes
-> forall (send :: role') (recv :: role') (st :: ps) (st' :: ps)
          (st'' :: ps).
   Msg role' ps st send st' recv st'' -> bytes
encode}
  Decode role' ps failure bytes
decodeV
  ConnChannels role' n bytes
connChannels
  forall a. n a -> m a
liftFun = do
    msgCache <- IntMap (AnyMsg role' ps) -> n (TVar n (IntMap (AnyMsg role' ps)))
forall a. a -> n (TVar n a)
forall (m :: * -> *) a. MonadSTM m => a -> m (TVar m a)
newTVarIO IntMap (AnyMsg role' ps)
forall a. IntMap a
IntMap.empty
    ths <- for connChannels $ \(SomeRole role'
_, Channel n bytes
channel) -> n () -> n (ThreadId n)
forall (m :: * -> *). MonadFork m => m () -> m (ThreadId m)
forkIO (n () -> n (ThreadId n)) -> n () -> n (ThreadId n)
forall a b. (a -> b) -> a -> b
$ Maybe bytes
-> Decode role' ps failure bytes
-> Channel n bytes
-> TVar n (IntMap (AnyMsg role' ps))
-> n ()
forall failure (n :: * -> *) bytes role' ps.
(Exception failure, MonadDelay n, MonadSTM n, MonadThrow n) =>
Maybe bytes
-> Decode role' ps failure bytes
-> Channel n bytes
-> MsgCache role' ps n
-> n ()
decodeLoop Maybe bytes
forall a. Maybe a
Nothing Decode role' ps failure bytes
decodeV Channel n bytes
channel TVar n (IntMap (AnyMsg role' ps))
msgCache
    let terminalDecodeThreads = (ThreadId n -> m ()) -> [ThreadId n] -> [m ()]
forall a b. (a -> b) -> [a] -> [b]
map (\ThreadId n
tid -> n () -> m ()
forall a. n a -> m a
liftFun (n () -> m ()) -> n () -> m ()
forall a b. (a -> b) -> a -> b
$ ThreadId n -> n ()
forall (m :: * -> *). MonadFork m => ThreadId m -> m ()
killThread ThreadId n
tid) [ThreadId n]
ths
    pure $ Driver{sendMsg, recvMsg = recvMsg' msgCache, terminalDecodeThreads}
   where
    sendMap :: IntMap (bytes -> n ())
sendMap = [(Int, bytes -> n ())] -> IntMap (bytes -> n ())
forall a. [(Int, a)] -> IntMap a
IntMap.fromList ([(Int, bytes -> n ())] -> IntMap (bytes -> n ()))
-> [(Int, bytes -> n ())] -> IntMap (bytes -> n ())
forall a b. (a -> b) -> a -> b
$ ((SomeRole role', Channel n bytes) -> (Int, bytes -> n ()))
-> ConnChannels role' n bytes -> [(Int, bytes -> n ())]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(SomeRole Sing r
r, Channel n bytes
c) -> (Sing r -> Int
forall (r :: role'). Sing r -> Int
forall s (r :: s). SingToInt s => Sing r -> Int
singToInt Sing r
r, Channel n bytes -> bytes -> n ()
forall (m :: * -> *) bytes. Channel m bytes -> bytes -> m ()
send Channel n bytes
c)) ConnChannels role' n bytes
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 :: 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 ()
sendMsg Sing recv
role Msg role' ps from send st recv st1
msg = n () -> m ()
forall a. n a -> m a
liftFun (n () -> m ()) -> n () -> m ()
forall a b. (a -> b) -> a -> b
$ do
      let recvKey :: Int
recvKey = Sing recv -> Int
forall (r :: role'). Sing r -> Int
forall s (r :: s). SingToInt s => Sing r -> Int
singToInt Sing recv
role
      case Int -> IntMap (bytes -> n ()) -> Maybe (bytes -> n ())
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
recvKey IntMap (bytes -> n ())
sendMap of
        Maybe (bytes -> n ())
Nothing -> do
          let recvRole :: role'
recvRole = forall a. Enum a => Int -> a
toEnum @role' Int
recvKey
          NotConnect role' -> n ()
forall e a. Exception e => e -> n a
forall (m :: * -> *) e a. (MonadThrow m, Exception e) => e -> m a
throwIO (role' -> NotConnect role'
forall role'. role' -> NotConnect role'
NotConnect role'
recvRole)
        Just bytes -> n ()
sendFun -> bytes -> n ()
sendFun (Msg role' ps from send st recv st1 -> bytes
forall (send :: role') (recv :: role') (st :: ps) (st' :: ps)
       (st'' :: ps).
Msg role' ps st send st' recv st'' -> bytes
encode Msg role' ps from send st recv st1
msg)
      Tracer role' ps n
tracer (AnyMsg role' ps -> TraceSendRecv role' ps
forall role' ps. AnyMsg role' ps -> TraceSendRecv role' ps
TraceSendMsg (Msg role' ps from send st recv st1 -> AnyMsg role' ps
forall role' (recv :: role') ps (st :: ps) (send :: role')
       (st' :: ps) (st'' :: ps).
(SingI recv, SingI st, SingToInt role', SingToInt ps) =>
Msg role' ps st send st' recv st'' -> AnyMsg role' ps
AnyMsg Msg role' ps from send st recv st1
msg))

    recvMsg'
      :: forall (st' :: ps)
       . (SingToInt ps)
      => MsgCache role' ps n
      -> Sing st'
      -> m (AnyMsg role' ps)
    recvMsg' :: forall (st' :: ps).
SingToInt ps =>
TVar n (IntMap (AnyMsg role' ps))
-> Sing st' -> m (AnyMsg role' ps)
recvMsg' TVar n (IntMap (AnyMsg role' ps))
msgCache Sing st'
sst' = do
      let singInt :: Int
singInt = Sing st' -> Int
forall (r :: ps). Sing r -> Int
forall s (r :: s). SingToInt s => Sing r -> Int
singToInt Sing st'
sst'
      n (AnyMsg role' ps) -> m (AnyMsg role' ps)
forall a. n a -> m a
liftFun (n (AnyMsg role' ps) -> m (AnyMsg role' ps))
-> n (AnyMsg role' ps) -> m (AnyMsg role' ps)
forall a b. (a -> b) -> a -> b
$ do
        anyMsg <- STM n (AnyMsg role' ps) -> n (AnyMsg role' ps)
forall a. HasCallStack => STM n a -> n a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (STM n (AnyMsg role' ps) -> n (AnyMsg role' ps))
-> STM n (AnyMsg role' ps) -> n (AnyMsg role' ps)
forall a b. (a -> b) -> a -> b
$ do
          agencyMsg <- TVar n (IntMap (AnyMsg role' ps))
-> STM n (IntMap (AnyMsg role' ps))
forall a. TVar n a -> STM n a
forall (m :: * -> *) a. MonadSTM m => TVar m a -> STM m a
readTVar TVar n (IntMap (AnyMsg role' ps))
msgCache
          case IntMap.lookup singInt agencyMsg of
            Maybe (AnyMsg role' ps)
Nothing -> STM n (AnyMsg role' ps)
forall a. STM n a
forall (m :: * -> *) a. MonadSTM m => STM m a
retry
            Just AnyMsg role' ps
v -> do
              TVar n (IntMap (AnyMsg role' ps))
-> IntMap (AnyMsg role' ps) -> STM n ()
forall a. TVar n a -> a -> STM n ()
forall (m :: * -> *) a. MonadSTM m => TVar m a -> a -> STM m ()
writeTVar TVar n (IntMap (AnyMsg role' ps))
msgCache (Int -> IntMap (AnyMsg role' ps) -> IntMap (AnyMsg role' ps)
forall a. Int -> IntMap a -> IntMap a
IntMap.delete Int
singInt IntMap (AnyMsg role' ps)
agencyMsg)
              AnyMsg role' ps -> STM n (AnyMsg role' ps)
forall a. a -> STM n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure AnyMsg role' ps
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, MonadDelay n, MonadSTM n, MonadThrow n)
  => Maybe bytes
  -> Decode role' ps failure bytes
  -> Channel n bytes
  -> MsgCache role' ps n
  -> n ()
decodeLoop :: forall failure (n :: * -> *) bytes role' ps.
(Exception failure, MonadDelay n, MonadSTM n, MonadThrow n) =>
Maybe bytes
-> Decode role' ps failure bytes
-> Channel n bytes
-> MsgCache role' ps n
-> n ()
decodeLoop Maybe bytes
mbt d :: Decode role' ps failure bytes
d@Decode{DecodeStep bytes failure (AnyMsg role' ps)
decode :: DecodeStep bytes failure (AnyMsg role' ps)
decode :: forall role' ps failure bytes.
Decode role' ps failure bytes
-> DecodeStep bytes failure (AnyMsg role' ps)
decode} Channel n bytes
channel MsgCache role' ps n
tvar = do
  result <- Channel n bytes
-> Maybe bytes
-> DecodeStep bytes failure (AnyMsg role' ps)
-> n (Either failure (AnyMsg role' ps, Maybe bytes))
forall (m :: * -> *) bytes failure a.
Monad m =>
Channel m bytes
-> Maybe bytes
-> DecodeStep bytes failure a
-> m (Either failure (a, Maybe bytes))
runDecoderWithChannel Channel n bytes
channel Maybe bytes
mbt DecodeStep bytes failure (AnyMsg role' ps)
decode
  case result of
    Right (AnyMsg Msg role' ps st send st' recv st''
msg, Maybe bytes
mbt') -> do
      let agencyInt :: Int
agencyInt = Sing st -> Int
forall (r :: ps). Sing r -> Int
forall s (r :: s). SingToInt s => Sing r -> Int
singToInt (Sing st -> Int) -> Sing st -> Int
forall a b. (a -> b) -> a -> b
$ Msg role' ps st send st' recv st'' -> Sing st
forall role' ps (st :: ps) (send :: role') (recv :: role')
       (st' :: ps) (st'' :: ps).
(SingI recv, SingI st) =>
Msg role' ps st send st' recv st'' -> Sing st
msgFromStSing Msg role' ps st send st' recv st''
msg
      STM n () -> n ()
forall a. HasCallStack => STM n a -> n a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (STM n () -> n ()) -> STM n () -> n ()
forall a b. (a -> b) -> a -> b
$ do
        agencyMsg <- MsgCache role' ps n -> STM n (IntMap (AnyMsg role' ps))
forall a. TVar n a -> STM n a
forall (m :: * -> *) a. MonadSTM m => TVar m a -> STM m a
readTVar MsgCache role' ps n
tvar
        case IntMap.lookup agencyInt agencyMsg of
          Maybe (AnyMsg role' ps)
Nothing -> MsgCache role' ps n -> IntMap (AnyMsg role' ps) -> STM n ()
forall a. TVar n a -> a -> STM n ()
forall (m :: * -> *) a. MonadSTM m => TVar m a -> a -> STM m ()
writeTVar MsgCache role' ps n
tvar (Int
-> AnyMsg role' ps
-> IntMap (AnyMsg role' ps)
-> IntMap (AnyMsg role' ps)
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
agencyInt (Msg role' ps st send st' recv st'' -> AnyMsg role' ps
forall role' (recv :: role') ps (st :: ps) (send :: role')
       (st' :: ps) (st'' :: ps).
(SingI recv, SingI st, SingToInt role', SingToInt ps) =>
Msg role' ps st send st' recv st'' -> AnyMsg role' ps
AnyMsg Msg role' ps st send st' recv st''
msg) IntMap (AnyMsg role' ps)
agencyMsg)
          Just AnyMsg role' ps
_v -> STM n ()
forall a. STM n a
forall (m :: * -> *) a. MonadSTM m => STM m a
retry
      Maybe bytes
-> Decode role' ps failure bytes
-> Channel n bytes
-> MsgCache role' ps n
-> n ()
forall failure (n :: * -> *) bytes role' ps.
(Exception failure, MonadDelay n, MonadSTM n, MonadThrow n) =>
Maybe bytes
-> Decode role' ps failure bytes
-> Channel n bytes
-> MsgCache role' ps n
-> n ()
decodeLoop Maybe bytes
mbt' Decode role' ps failure bytes
d Channel n bytes
channel MsgCache role' ps n
tvar
    Left failure
failure -> do
      Int -> n ()
forall (m :: * -> *). MonadDelay m => Int -> m ()
threadDelay Int
1_000_000
      failure -> n ()
forall e a. Exception e => e -> n a
forall (m :: * -> *) e a. (MonadThrow m, Exception e) => e -> m a
throwIO failure
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 :: 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 role' ps n
tracer IntMap (MsgCache role' ps n)
allMsgCache (SomeRole Sing r
r) forall a. n a -> m a
liftFun =
  Driver{Sing recv -> Msg role' ps st send st' recv st'' -> m ()
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 ()
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 ()
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 ()
sendMsg, recvMsg :: forall (st' :: ps). SingToInt ps => Sing st' -> m (AnyMsg role' ps)
recvMsg = MsgCache role' ps n -> Sing st' -> m (AnyMsg role' ps)
forall (st' :: ps).
SingToInt ps =>
MsgCache role' ps n -> Sing st' -> m (AnyMsg role' ps)
recvMsg' (IntMap (MsgCache role' ps n)
allMsgCache IntMap (MsgCache role' ps n) -> Int -> MsgCache role' ps n
forall a. IntMap a -> Int -> a
IntMap.! (Sing r -> Int
forall (r :: role'). Sing r -> Int
forall s (r :: s). SingToInt s => Sing r -> Int
singToInt Sing r
r)), terminalDecodeThreads :: [m ()]
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 :: 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 ()
sendMsg Sing recv
role Msg role' ps from send st recv st1
msg = n () -> m ()
forall a. n a -> m a
liftFun (n () -> m ()) -> n () -> m ()
forall a b. (a -> b) -> a -> b
$ do
    let recvKey :: Int
recvKey = Sing recv -> Int
forall (r :: role'). Sing r -> Int
forall s (r :: s). SingToInt s => Sing r -> Int
singToInt Sing recv
role
    case Int -> IntMap (MsgCache role' ps n) -> Maybe (MsgCache role' ps n)
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup (Sing recv -> Int
forall (r :: role'). Sing r -> Int
forall s (r :: s). SingToInt s => Sing r -> Int
singToInt Sing recv
role) IntMap (MsgCache role' ps n)
allMsgCache of
      Maybe (MsgCache role' ps n)
Nothing -> do
        let recvRole :: role'
recvRole = forall a. Enum a => Int -> a
toEnum @role' Int
recvKey
        NotConnect role' -> n ()
forall e a. Exception e => e -> n a
forall (m :: * -> *) e a. (MonadThrow m, Exception e) => e -> m a
throwIO (role' -> NotConnect role'
forall role'. role' -> NotConnect role'
NotConnect role'
recvRole)
      Just MsgCache role' ps n
ttvar -> STM n () -> n ()
forall a. HasCallStack => STM n a -> n a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (STM n () -> n ()) -> STM n () -> n ()
forall a b. (a -> b) -> a -> b
$ do
        agencyMsg <- MsgCache role' ps n -> STM n (IntMap (AnyMsg role' ps))
forall a. TVar n a -> STM n a
forall (m :: * -> *) a. MonadSTM m => TVar m a -> STM m a
readTVar MsgCache role' ps n
ttvar
        let singInt = Sing from -> Int
forall (r :: ps). Sing r -> Int
forall s (r :: s). SingToInt s => Sing r -> Int
singToInt (forall (a :: ps). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @from)
        case IntMap.lookup singInt agencyMsg of
          Maybe (AnyMsg role' ps)
Nothing -> MsgCache role' ps n -> IntMap (AnyMsg role' ps) -> STM n ()
forall a. TVar n a -> a -> STM n ()
forall (m :: * -> *) a. MonadSTM m => TVar m a -> a -> STM m ()
writeTVar MsgCache role' ps n
ttvar (Int
-> AnyMsg role' ps
-> IntMap (AnyMsg role' ps)
-> IntMap (AnyMsg role' ps)
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
singInt (Msg role' ps from send st recv st1 -> AnyMsg role' ps
forall role' (recv :: role') ps (st :: ps) (send :: role')
       (st' :: ps) (st'' :: ps).
(SingI recv, SingI st, SingToInt role', SingToInt ps) =>
Msg role' ps st send st' recv st'' -> AnyMsg role' ps
AnyMsg Msg role' ps from send st recv st1
msg) IntMap (AnyMsg role' ps)
agencyMsg)
          Just AnyMsg role' ps
_v -> STM n ()
forall a. STM n a
forall (m :: * -> *) a. MonadSTM m => STM m a
retry
    Tracer role' ps n
tracer (AnyMsg role' ps -> TraceSendRecv role' ps
forall role' ps. AnyMsg role' ps -> TraceSendRecv role' ps
TraceSendMsg (Msg role' ps from send st recv st1 -> AnyMsg role' ps
forall role' (recv :: role') ps (st :: ps) (send :: role')
       (st' :: ps) (st'' :: ps).
(SingI recv, SingI st, SingToInt role', SingToInt ps) =>
Msg role' ps st send st' recv st'' -> AnyMsg role' ps
AnyMsg Msg role' ps from send st recv st1
msg))

  recvMsg'
    :: forall (st' :: ps)
     . (SingToInt ps)
    => MsgCache role' ps n
    -> Sing st'
    -> m (AnyMsg role' ps)
  recvMsg' :: forall (st' :: ps).
SingToInt ps =>
MsgCache role' ps n -> Sing st' -> m (AnyMsg role' ps)
recvMsg' MsgCache role' ps n
msgCache Sing st'
sst' = do
    let singInt :: Int
singInt = Sing st' -> Int
forall (r :: ps). Sing r -> Int
forall s (r :: s). SingToInt s => Sing r -> Int
singToInt Sing st'
sst'
    n (AnyMsg role' ps) -> m (AnyMsg role' ps)
forall a. n a -> m a
liftFun (n (AnyMsg role' ps) -> m (AnyMsg role' ps))
-> n (AnyMsg role' ps) -> m (AnyMsg role' ps)
forall a b. (a -> b) -> a -> b
$ do
      anyMsg <- STM n (AnyMsg role' ps) -> n (AnyMsg role' ps)
forall a. HasCallStack => STM n a -> n a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (STM n (AnyMsg role' ps) -> n (AnyMsg role' ps))
-> STM n (AnyMsg role' ps) -> n (AnyMsg role' ps)
forall a b. (a -> b) -> a -> b
$ do
        agencyMsg <- MsgCache role' ps n -> STM n (IntMap (AnyMsg role' ps))
forall a. TVar n a -> STM n a
forall (m :: * -> *) a. MonadSTM m => TVar m a -> STM m a
readTVar MsgCache role' ps n
msgCache
        case IntMap.lookup singInt agencyMsg of
          Maybe (AnyMsg role' ps)
Nothing -> STM n (AnyMsg role' ps)
forall a. STM n a
forall (m :: * -> *) a. MonadSTM m => STM m a
retry
          Just AnyMsg role' ps
v -> do
            MsgCache role' ps n -> IntMap (AnyMsg role' ps) -> STM n ()
forall a. TVar n a -> a -> STM n ()
forall (m :: * -> *) a. MonadSTM m => TVar m a -> a -> STM m ()
writeTVar MsgCache role' ps n
msgCache (Int -> IntMap (AnyMsg role' ps) -> IntMap (AnyMsg role' ps)
forall a. Int -> IntMap a -> IntMap a
IntMap.delete Int
singInt IntMap (AnyMsg role' ps)
agencyMsg)
            AnyMsg role' ps -> STM n (AnyMsg role' ps)
forall a. a -> STM n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure AnyMsg role' ps
v
      tracer (TraceRecvMsg (anyMsg))
      pure anyMsg