{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE KindSignatures      #-}
{-# LANGUAGE NamedFieldPuns      #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Ouroboros.Network.Protocol.LocalStateQuery.Client
  ( -- * Protocol type for the client
    -- | The protocol states from the point of view of the client.
    LocalStateQueryClient (..)
  , ClientStIdle (..)
  , ClientStAcquiring (..)
  , ClientStAcquired (..)
  , ClientStQuerying (..)
    -- * Execution as a typed protocol
  , localStateQueryClientPeer
    -- * Utilities
  , mapLocalStateQueryClient
  , Some (..)
  ) where

import Data.Kind (Type)

import Network.TypedProtocol.Stateful.Peer.Client

import Ouroboros.Network.Protocol.LocalStateQuery.Codec (Some (..))
import Ouroboros.Network.Protocol.LocalStateQuery.Type


newtype LocalStateQueryClient block point (query :: Type -> Type) m a =
    LocalStateQueryClient {
      forall block point (query :: * -> *) (m :: * -> *) a.
LocalStateQueryClient block point query m a
-> m (ClientStIdle block point query m a)
runLocalStateQueryClient :: m (ClientStIdle block point query m a)
    }

-- | In the 'StIdle' protocol state, the client has agency and must send:
--
--  * a request to acquire a state
--  * a termination messge
--
data ClientStIdle block point query (m :: Type -> Type) a where
  SendMsgAcquire :: Target point
                 -> ClientStAcquiring block point query m a
                 -> ClientStIdle      block point query m a

  SendMsgDone    :: a
                 -> ClientStIdle      block point query m a

-- | In the 'StAcquiring' protocol state, the client does not have agency.
-- Instead it is waiting for:
--
--  * acquired
--  * failure to acquire
--
-- It must be prepared to handle either.
--
data ClientStAcquiring block point query m a = ClientStAcquiring {
      forall block point (query :: * -> *) (m :: * -> *) a.
ClientStAcquiring block point query m a
-> m (ClientStAcquired block point query m a)
recvMsgAcquired :: m (ClientStAcquired block point query m a),

      forall block point (query :: * -> *) (m :: * -> *) a.
ClientStAcquiring block point query m a
-> AcquireFailure -> m (ClientStIdle block point query m a)
recvMsgFailure  :: AcquireFailure
                      -> m (ClientStIdle  block point query m a)
    }

-- | In the 'StAcquired' protocol state, the client has agency and must send:
--
--  * a query
--  * a request to (re)acquire another state
--  * a release of the current state
--
data ClientStAcquired block point query m a where
  SendMsgQuery     :: query result
                   -> ClientStQuerying block point query m a result
                   -> ClientStAcquired block point query m a

  SendMsgReAcquire :: Target point
                   -> ClientStAcquiring block point query m a
                   -> ClientStAcquired  block point query m a

  SendMsgRelease   :: m (ClientStIdle   block point query m a)
                   -> ClientStAcquired  block point query m a

-- | In the 'StQuerying' protocol state, the client does not have agency.
-- Instead it is waiting for:
--
--  * a result
--
data ClientStQuerying block point query m a result = ClientStQuerying {
      forall block point (query :: * -> *) (m :: * -> *) a result.
ClientStQuerying block point query m a result
-> result -> m (ClientStAcquired block point query m a)
recvMsgResult :: result -> m (ClientStAcquired block point query m a)
    }

-- | Transform a 'LocalStateQueryClient' by mapping over the query and query
-- result values.
--
-- Note the direction of the individual mapping functions corresponds to
-- whether the types are used as protocol inputs or outputs.
--
mapLocalStateQueryClient :: forall block block' point point' query query' m a.
                            Functor m
                         => (point -> point')
                         -> (forall result. query result -> Some query')
                         -> (forall result result'.
                                    query result
                                 -> query' result'
                                 -> result' -> result)
                         -> LocalStateQueryClient block  point  query  m a
                         -> LocalStateQueryClient block' point' query' m a
mapLocalStateQueryClient :: forall block block' point point' (query :: * -> *)
       (query' :: * -> *) (m :: * -> *) a.
Functor m =>
(point -> point')
-> (forall result. query result -> Some query')
-> (forall result result'.
    query result -> query' result' -> result' -> result)
-> LocalStateQueryClient block point query m a
-> LocalStateQueryClient block' point' query' m a
mapLocalStateQueryClient point -> point'
fpoint forall result. query result -> Some query'
fquery forall result result'.
query result -> query' result' -> result' -> result
fresult =
    \(LocalStateQueryClient m (ClientStIdle block point query m a)
c) -> m (ClientStIdle block' point' query' m a)
-> LocalStateQueryClient block' point' query' m a
forall block point (query :: * -> *) (m :: * -> *) a.
m (ClientStIdle block point query m a)
-> LocalStateQueryClient block point query m a
LocalStateQueryClient ((ClientStIdle block point query m a
 -> ClientStIdle block' point' query' m a)
-> m (ClientStIdle block point query m a)
-> m (ClientStIdle block' point' query' m a)
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ClientStIdle block point query m a
-> ClientStIdle block' point' query' m a
goIdle m (ClientStIdle block point query m a)
c)
  where
    goIdle :: ClientStIdle block  point  query  m a
           -> ClientStIdle block' point' query' m a
    goIdle :: ClientStIdle block point query m a
-> ClientStIdle block' point' query' m a
goIdle (SendMsgAcquire Target point
tgt ClientStAcquiring block point query m a
k) =
      Target point'
-> ClientStAcquiring block' point' query' m a
-> ClientStIdle block' point' query' m a
forall point block (query :: * -> *) (m :: * -> *) a.
Target point
-> ClientStAcquiring block point query m a
-> ClientStIdle block point query m a
SendMsgAcquire (point -> point'
fpoint (point -> point') -> Target point -> Target point'
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Target point
tgt) (ClientStAcquiring block point query m a
-> ClientStAcquiring block' point' query' m a
goAcquiring ClientStAcquiring block point query m a
k)

    goIdle (SendMsgDone a
a) = a -> ClientStIdle block' point' query' m a
forall a block point (query :: * -> *) (m :: * -> *).
a -> ClientStIdle block point query m a
SendMsgDone a
a

    goAcquiring :: ClientStAcquiring block  point  query  m a
                -> ClientStAcquiring block' point' query' m a
    goAcquiring :: ClientStAcquiring block point query m a
-> ClientStAcquiring block' point' query' m a
goAcquiring ClientStAcquiring { m (ClientStAcquired block point query m a)
recvMsgAcquired :: forall block point (query :: * -> *) (m :: * -> *) a.
ClientStAcquiring block point query m a
-> m (ClientStAcquired block point query m a)
recvMsgAcquired :: m (ClientStAcquired block point query m a)
recvMsgAcquired, AcquireFailure -> m (ClientStIdle block point query m a)
recvMsgFailure :: forall block point (query :: * -> *) (m :: * -> *) a.
ClientStAcquiring block point query m a
-> AcquireFailure -> m (ClientStIdle block point query m a)
recvMsgFailure :: AcquireFailure -> m (ClientStIdle block point query m a)
recvMsgFailure } =
      ClientStAcquiring {
        recvMsgAcquired :: m (ClientStAcquired block' point' query' m a)
recvMsgAcquired = ClientStAcquired block point query m a
-> ClientStAcquired block' point' query' m a
goAcquired (ClientStAcquired block point query m a
 -> ClientStAcquired block' point' query' m a)
-> m (ClientStAcquired block point query m a)
-> m (ClientStAcquired block' point' query' m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (ClientStAcquired block point query m a)
recvMsgAcquired,
        recvMsgFailure :: AcquireFailure -> m (ClientStIdle block' point' query' m a)
recvMsgFailure  = \AcquireFailure
failure -> (ClientStIdle block point query m a
 -> ClientStIdle block' point' query' m a)
-> m (ClientStIdle block point query m a)
-> m (ClientStIdle block' point' query' m a)
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ClientStIdle block point query m a
-> ClientStIdle block' point' query' m a
goIdle (AcquireFailure -> m (ClientStIdle block point query m a)
recvMsgFailure AcquireFailure
failure)
      }

    goAcquired :: ClientStAcquired block  point  query  m a
               -> ClientStAcquired block' point' query' m a
    goAcquired :: ClientStAcquired block point query m a
-> ClientStAcquired block' point' query' m a
goAcquired (SendMsgQuery     query result
q  ClientStQuerying block point query m a result
k) = case query result -> Some query'
forall result. query result -> Some query'
fquery query result
q of
                                           Some query' a
q' -> query' a
-> ClientStQuerying block' point' query' m a a
-> ClientStAcquired block' point' query' m a
forall (query :: * -> *) result block point (m :: * -> *) a.
query result
-> ClientStQuerying block point query m a result
-> ClientStAcquired block point query m a
SendMsgQuery query' a
q' (query result
-> query' a
-> ClientStQuerying block point query m a result
-> ClientStQuerying block' point' query' m a a
forall result result'.
query result
-> query' result'
-> ClientStQuerying block point query m a result
-> ClientStQuerying block' point' query' m a result'
goQuerying query result
q query' a
q' ClientStQuerying block point query m a result
k)
    goAcquired (SendMsgReAcquire Target point
tgt ClientStAcquiring block point query m a
k) = Target point'
-> ClientStAcquiring block' point' query' m a
-> ClientStAcquired block' point' query' m a
forall point block (query :: * -> *) (m :: * -> *) a.
Target point
-> ClientStAcquiring block point query m a
-> ClientStAcquired block point query m a
SendMsgReAcquire (point -> point'
fpoint (point -> point') -> Target point -> Target point'
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Target point
tgt) (ClientStAcquiring block point query m a
-> ClientStAcquiring block' point' query' m a
goAcquiring ClientStAcquiring block point query m a
k)
    goAcquired (SendMsgRelease       m (ClientStIdle block point query m a)
k) = m (ClientStIdle block' point' query' m a)
-> ClientStAcquired block' point' query' m a
forall (m :: * -> *) block point (query :: * -> *) a.
m (ClientStIdle block point query m a)
-> ClientStAcquired block point query m a
SendMsgRelease ((ClientStIdle block point query m a
 -> ClientStIdle block' point' query' m a)
-> m (ClientStIdle block point query m a)
-> m (ClientStIdle block' point' query' m a)
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ClientStIdle block point query m a
-> ClientStIdle block' point' query' m a
goIdle m (ClientStIdle block point query m a)
k)

    goQuerying :: forall result result'.
                  query  result
               -> query' result'
               -> ClientStQuerying block  point  query  m a result
               -> ClientStQuerying block' point' query' m a result'
    goQuerying :: forall result result'.
query result
-> query' result'
-> ClientStQuerying block point query m a result
-> ClientStQuerying block' point' query' m a result'
goQuerying query result
q query' result'
q' ClientStQuerying {result -> m (ClientStAcquired block point query m a)
recvMsgResult :: forall block point (query :: * -> *) (m :: * -> *) a result.
ClientStQuerying block point query m a result
-> result -> m (ClientStAcquired block point query m a)
recvMsgResult :: result -> m (ClientStAcquired block point query m a)
recvMsgResult} =
      ClientStQuerying {
        recvMsgResult :: result' -> m (ClientStAcquired block' point' query' m a)
recvMsgResult = \result'
result' ->
          let result :: result
              result :: result
result = query result -> query' result' -> result' -> result
forall result result'.
query result -> query' result' -> result' -> result
fresult query result
q query' result'
q' result'
result' in
          (ClientStAcquired block point query m a
 -> ClientStAcquired block' point' query' m a)
-> m (ClientStAcquired block point query m a)
-> m (ClientStAcquired block' point' query' m a)
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ClientStAcquired block point query m a
-> ClientStAcquired block' point' query' m a
goAcquired (result -> m (ClientStAcquired block point query m a)
recvMsgResult result
result)
      }


-- | Interpret a 'LocalStateQueryClient' action sequence as a 'Peer' on the
-- client side of the 'LocalStateQuery' protocol.
--
localStateQueryClientPeer
  :: forall block point (query :: Type -> Type) m a.
     Monad m
  => LocalStateQueryClient block point query m a
  -> Client (LocalStateQuery block point query) StIdle State m a
localStateQueryClientPeer :: forall block point (query :: * -> *) (m :: * -> *) a.
Monad m =>
LocalStateQueryClient block point query m a
-> Client (LocalStateQuery block point query) 'StIdle State m a
localStateQueryClientPeer (LocalStateQueryClient m (ClientStIdle block point query m a)
handler) =
    m (Client (LocalStateQuery block point query) 'StIdle State m a)
-> Client (LocalStateQuery block point query) 'StIdle State m a
forall ps (st :: ps) (f :: ps -> *) (m :: * -> *) a.
m (Client ps st f m a) -> Client ps st f m a
Effect (m (Client (LocalStateQuery block point query) 'StIdle State m a)
 -> Client (LocalStateQuery block point query) 'StIdle State m a)
-> m (Client (LocalStateQuery block point query) 'StIdle State m a)
-> Client (LocalStateQuery block point query) 'StIdle State m a
forall a b. (a -> b) -> a -> b
$ ClientStIdle block point query m a
-> Client (LocalStateQuery block point query) 'StIdle State m a
handleStIdle (ClientStIdle block point query m a
 -> Client (LocalStateQuery block point query) 'StIdle State m a)
-> m (ClientStIdle block point query m a)
-> m (Client (LocalStateQuery block point query) 'StIdle State m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (ClientStIdle block point query m a)
handler
  where
    handleStIdle
      :: ClientStIdle block point query m a
      -> Client (LocalStateQuery block point query) StIdle State m a
    handleStIdle :: ClientStIdle block point query m a
-> Client (LocalStateQuery block point query) 'StIdle State m a
handleStIdle ClientStIdle block point query m a
req = case ClientStIdle block point query m a
req of
      SendMsgAcquire Target point
tgt ClientStAcquiring block point query m a
stAcquiring ->
        State 'StIdle
-> State 'StAcquiring
-> Message (LocalStateQuery block point query) 'StIdle 'StAcquiring
-> Client
     (LocalStateQuery block point query) 'StAcquiring State m a
-> Client (LocalStateQuery block point query) 'StIdle State m a
forall ps (st :: ps) (f :: ps -> *) (m :: * -> *) a (st' :: ps).
(StateTokenI st, StateTokenI st',
 StateAgency st ~ 'ClientAgency) =>
f st
-> f st'
-> Message ps st st'
-> Client ps st' f m a
-> Client ps st f m a
Yield State 'StIdle
forall {block} {point} {query :: * -> *}. State 'StIdle
StateIdle State 'StAcquiring
forall {block} {point} {query :: * -> *}. State 'StAcquiring
StateAcquiring
              (Target point
-> Message (LocalStateQuery block point query) 'StIdle 'StAcquiring
forall point block (query :: * -> *).
Target point
-> Message (LocalStateQuery block point query) 'StIdle 'StAcquiring
MsgAcquire Target point
tgt)
              (ClientStAcquiring block point query m a
-> Client
     (LocalStateQuery block point query) 'StAcquiring State m a
handleStAcquiring ClientStAcquiring block point query m a
stAcquiring)
      SendMsgDone a
a ->
        State 'StIdle
-> State 'StDone
-> Message (LocalStateQuery block point query) 'StIdle 'StDone
-> Client (LocalStateQuery block point query) 'StDone State m a
-> Client (LocalStateQuery block point query) 'StIdle State m a
forall ps (st :: ps) (f :: ps -> *) (m :: * -> *) a (st' :: ps).
(StateTokenI st, StateTokenI st',
 StateAgency st ~ 'ClientAgency) =>
f st
-> f st'
-> Message ps st st'
-> Client ps st' f m a
-> Client ps st f m a
Yield State 'StIdle
forall {block} {point} {query :: * -> *}. State 'StIdle
StateIdle State 'StDone
forall {block} {point} {query :: * -> *}. State 'StDone
StateDone Message (LocalStateQuery block point query) 'StIdle 'StDone
forall block point (query :: * -> *).
Message (LocalStateQuery block point query) 'StIdle 'StDone
MsgDone (a -> Client (LocalStateQuery block point query) 'StDone State m a
forall ps (st :: ps) (f :: ps -> *) (m :: * -> *) a.
(StateTokenI st, StateAgency st ~ 'NobodyAgency) =>
a -> Client ps st f m a
Done a
a)

    handleStAcquiring
      :: ClientStAcquiring block point query m a
      -> Client (LocalStateQuery block point query) StAcquiring State m a
    handleStAcquiring :: ClientStAcquiring block point query m a
-> Client
     (LocalStateQuery block point query) 'StAcquiring State m a
handleStAcquiring ClientStAcquiring{m (ClientStAcquired block point query m a)
recvMsgAcquired :: forall block point (query :: * -> *) (m :: * -> *) a.
ClientStAcquiring block point query m a
-> m (ClientStAcquired block point query m a)
recvMsgAcquired :: m (ClientStAcquired block point query m a)
recvMsgAcquired, AcquireFailure -> m (ClientStIdle block point query m a)
recvMsgFailure :: forall block point (query :: * -> *) (m :: * -> *) a.
ClientStAcquiring block point query m a
-> AcquireFailure -> m (ClientStIdle block point query m a)
recvMsgFailure :: AcquireFailure -> m (ClientStIdle block point query m a)
recvMsgFailure} =
      (forall (st' :: LocalStateQuery block point query).
 State 'StAcquiring
 -> Message (LocalStateQuery block point query) 'StAcquiring st'
 -> (Client (LocalStateQuery block point query) st' State m a,
     State st'))
-> Client
     (LocalStateQuery block point query) 'StAcquiring State m a
forall ps (st :: ps) (f :: ps -> *) (m :: * -> *) a.
(StateTokenI st, StateAgency st ~ 'ServerAgency) =>
(forall (st' :: ps).
 f st -> Message ps st st' -> (Client ps st' f m a, f st'))
-> Client ps st f m a
Await ((forall (st' :: LocalStateQuery block point query).
  State 'StAcquiring
  -> Message (LocalStateQuery block point query) 'StAcquiring st'
  -> (Client (LocalStateQuery block point query) st' State m a,
      State st'))
 -> Client
      (LocalStateQuery block point query) 'StAcquiring State m a)
-> (forall (st' :: LocalStateQuery block point query).
    State 'StAcquiring
    -> Message (LocalStateQuery block point query) 'StAcquiring st'
    -> (Client (LocalStateQuery block point query) st' State m a,
        State st'))
-> Client
     (LocalStateQuery block point query) 'StAcquiring State m a
forall a b. (a -> b) -> a -> b
$ \State 'StAcquiring
_ Message (LocalStateQuery block point query) 'StAcquiring st'
req -> case Message (LocalStateQuery block point query) 'StAcquiring st'
req of
        Message (LocalStateQuery block point query) 'StAcquiring st'
R:MessageLocalStateQueryfromto block point query 'StAcquiring st'
MsgAcquired        -> ( m (Client (LocalStateQuery block point query) st' State m a)
-> Client (LocalStateQuery block point query) st' State m a
forall ps (st :: ps) (f :: ps -> *) (m :: * -> *) a.
m (Client ps st f m a) -> Client ps st f m a
Effect (m (Client (LocalStateQuery block point query) st' State m a)
 -> Client (LocalStateQuery block point query) st' State m a)
-> m (Client (LocalStateQuery block point query) st' State m a)
-> Client (LocalStateQuery block point query) st' State m a
forall a b. (a -> b) -> a -> b
$ ClientStAcquired block point query m a
-> Client (LocalStateQuery block point query) st' State m a
ClientStAcquired block point query m a
-> Client (LocalStateQuery block point query) 'StAcquired State m a
handleStAcquired (ClientStAcquired block point query m a
 -> Client (LocalStateQuery block point query) st' State m a)
-> m (ClientStAcquired block point query m a)
-> m (Client (LocalStateQuery block point query) st' State m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (ClientStAcquired block point query m a)
recvMsgAcquired
                              , State st'
State 'StAcquired
forall {block} {point} {query :: * -> *}. State 'StAcquired
StateAcquired
                              )
        MsgFailure AcquireFailure
failure -> ( m (Client (LocalStateQuery block point query) st' State m a)
-> Client (LocalStateQuery block point query) st' State m a
forall ps (st :: ps) (f :: ps -> *) (m :: * -> *) a.
m (Client ps st f m a) -> Client ps st f m a
Effect (m (Client (LocalStateQuery block point query) st' State m a)
 -> Client (LocalStateQuery block point query) st' State m a)
-> m (Client (LocalStateQuery block point query) st' State m a)
-> Client (LocalStateQuery block point query) st' State m a
forall a b. (a -> b) -> a -> b
$ ClientStIdle block point query m a
-> Client (LocalStateQuery block point query) st' State m a
ClientStIdle block point query m a
-> Client (LocalStateQuery block point query) 'StIdle State m a
handleStIdle (ClientStIdle block point query m a
 -> Client (LocalStateQuery block point query) st' State m a)
-> m (ClientStIdle block point query m a)
-> m (Client (LocalStateQuery block point query) st' State m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AcquireFailure -> m (ClientStIdle block point query m a)
recvMsgFailure AcquireFailure
failure
                              , State st'
State 'StIdle
forall {block} {point} {query :: * -> *}. State 'StIdle
StateIdle
                              )

    handleStAcquired
      :: ClientStAcquired block point query m a
      -> Client (LocalStateQuery block point query) StAcquired State m a
    handleStAcquired :: ClientStAcquired block point query m a
-> Client (LocalStateQuery block point query) 'StAcquired State m a
handleStAcquired ClientStAcquired block point query m a
req = case ClientStAcquired block point query m a
req of
      SendMsgQuery query result
query ClientStQuerying block point query m a result
stQuerying ->
        State 'StAcquired
-> State ('StQuerying result)
-> Message
     (LocalStateQuery block point query)
     'StAcquired
     ('StQuerying result)
-> Client
     (LocalStateQuery block point query) ('StQuerying result) State m a
-> Client (LocalStateQuery block point query) 'StAcquired State m a
forall ps (st :: ps) (f :: ps -> *) (m :: * -> *) a (st' :: ps).
(StateTokenI st, StateTokenI st',
 StateAgency st ~ 'ClientAgency) =>
f st
-> f st'
-> Message ps st st'
-> Client ps st' f m a
-> Client ps st f m a
Yield State 'StAcquired
forall {block} {point} {query :: * -> *}. State 'StAcquired
StateAcquired (query result -> State ('StQuerying result)
forall (query :: * -> *) result block point.
query result -> State ('StQuerying result)
StateQuerying query result
query)
              (query result
-> Message
     (LocalStateQuery block point query)
     'StAcquired
     ('StQuerying result)
forall (query :: * -> *) result block point.
query result
-> Message
     (LocalStateQuery block point query)
     'StAcquired
     ('StQuerying result)
MsgQuery query result
query)
              (query result
-> ClientStQuerying block point query m a result
-> Client
     (LocalStateQuery block point query) ('StQuerying result) State m a
forall result.
query result
-> ClientStQuerying block point query m a result
-> Client
     (LocalStateQuery block point query) ('StQuerying result) State m a
handleStQuerying query result
query ClientStQuerying block point query m a result
stQuerying)
      SendMsgReAcquire Target point
tgt ClientStAcquiring block point query m a
stAcquiring ->
        State 'StAcquired
-> State 'StAcquiring
-> Message
     (LocalStateQuery block point query) 'StAcquired 'StAcquiring
-> Client
     (LocalStateQuery block point query) 'StAcquiring State m a
-> Client (LocalStateQuery block point query) 'StAcquired State m a
forall ps (st :: ps) (f :: ps -> *) (m :: * -> *) a (st' :: ps).
(StateTokenI st, StateTokenI st',
 StateAgency st ~ 'ClientAgency) =>
f st
-> f st'
-> Message ps st st'
-> Client ps st' f m a
-> Client ps st f m a
Yield State 'StAcquired
forall {block} {point} {query :: * -> *}. State 'StAcquired
StateAcquired State 'StAcquiring
forall {block} {point} {query :: * -> *}. State 'StAcquiring
StateAcquiring
              (Target point
-> Message
     (LocalStateQuery block point query) 'StAcquired 'StAcquiring
forall point block (query :: * -> *).
Target point
-> Message
     (LocalStateQuery block point query) 'StAcquired 'StAcquiring
MsgReAcquire Target point
tgt)
              (ClientStAcquiring block point query m a
-> Client
     (LocalStateQuery block point query) 'StAcquiring State m a
handleStAcquiring ClientStAcquiring block point query m a
stAcquiring)
      SendMsgRelease m (ClientStIdle block point query m a)
stIdle ->
        State 'StAcquired
-> State 'StIdle
-> Message (LocalStateQuery block point query) 'StAcquired 'StIdle
-> Client (LocalStateQuery block point query) 'StIdle State m a
-> Client (LocalStateQuery block point query) 'StAcquired State m a
forall ps (st :: ps) (f :: ps -> *) (m :: * -> *) a (st' :: ps).
(StateTokenI st, StateTokenI st',
 StateAgency st ~ 'ClientAgency) =>
f st
-> f st'
-> Message ps st st'
-> Client ps st' f m a
-> Client ps st f m a
Yield State 'StAcquired
forall {block} {point} {query :: * -> *}. State 'StAcquired
StateAcquired State 'StIdle
forall {block} {point} {query :: * -> *}. State 'StIdle
StateIdle
              Message (LocalStateQuery block point query) 'StAcquired 'StIdle
forall block point (query :: * -> *).
Message (LocalStateQuery block point query) 'StAcquired 'StIdle
MsgRelease
              (m (Client (LocalStateQuery block point query) 'StIdle State m a)
-> Client (LocalStateQuery block point query) 'StIdle State m a
forall ps (st :: ps) (f :: ps -> *) (m :: * -> *) a.
m (Client ps st f m a) -> Client ps st f m a
Effect (ClientStIdle block point query m a
-> Client (LocalStateQuery block point query) 'StIdle State m a
handleStIdle (ClientStIdle block point query m a
 -> Client (LocalStateQuery block point query) 'StIdle State m a)
-> m (ClientStIdle block point query m a)
-> m (Client (LocalStateQuery block point query) 'StIdle State m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (ClientStIdle block point query m a)
stIdle))

    handleStQuerying
      :: query result
      -> ClientStQuerying block point query m a result
      -> Client (LocalStateQuery block point query) (StQuerying result) State m a
    handleStQuerying :: forall result.
query result
-> ClientStQuerying block point query m a result
-> Client
     (LocalStateQuery block point query) ('StQuerying result) State m a
handleStQuerying query result
_ ClientStQuerying{result -> m (ClientStAcquired block point query m a)
recvMsgResult :: forall block point (query :: * -> *) (m :: * -> *) a result.
ClientStQuerying block point query m a result
-> result -> m (ClientStAcquired block point query m a)
recvMsgResult :: result -> m (ClientStAcquired block point query m a)
recvMsgResult} =
      (forall (st' :: LocalStateQuery block point query).
 State ('StQuerying result)
 -> Message
      (LocalStateQuery block point query) ('StQuerying result) st'
 -> (Client (LocalStateQuery block point query) st' State m a,
     State st'))
-> Client
     (LocalStateQuery block point query) ('StQuerying result) State m a
forall ps (st :: ps) (f :: ps -> *) (m :: * -> *) a.
(StateTokenI st, StateAgency st ~ 'ServerAgency) =>
(forall (st' :: ps).
 f st -> Message ps st st' -> (Client ps st' f m a, f st'))
-> Client ps st f m a
Await ((forall (st' :: LocalStateQuery block point query).
  State ('StQuerying result)
  -> Message
       (LocalStateQuery block point query) ('StQuerying result) st'
  -> (Client (LocalStateQuery block point query) st' State m a,
      State st'))
 -> Client
      (LocalStateQuery block point query) ('StQuerying result) State m a)
-> (forall (st' :: LocalStateQuery block point query).
    State ('StQuerying result)
    -> Message
         (LocalStateQuery block point query) ('StQuerying result) st'
    -> (Client (LocalStateQuery block point query) st' State m a,
        State st'))
-> Client
     (LocalStateQuery block point query) ('StQuerying result) State m a
forall a b. (a -> b) -> a -> b
$ \State ('StQuerying result)
_ Message
  (LocalStateQuery block point query) ('StQuerying result) st'
req -> case Message
  (LocalStateQuery block point query) ('StQuerying result) st'
req of
        MsgResult result
result -> ( m (Client (LocalStateQuery block point query) st' State m a)
-> Client (LocalStateQuery block point query) st' State m a
forall ps (st :: ps) (f :: ps -> *) (m :: * -> *) a.
m (Client ps st f m a) -> Client ps st f m a
Effect (ClientStAcquired block point query m a
-> Client (LocalStateQuery block point query) st' State m a
ClientStAcquired block point query m a
-> Client (LocalStateQuery block point query) 'StAcquired State m a
handleStAcquired (ClientStAcquired block point query m a
 -> Client (LocalStateQuery block point query) st' State m a)
-> m (ClientStAcquired block point query m a)
-> m (Client (LocalStateQuery block point query) st' State m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> result -> m (ClientStAcquired block point query m a)
recvMsgResult result
result
result)
                            , State st'
State 'StAcquired
forall {block} {point} {query :: * -> *}. State 'StAcquired
StateAcquired
                            )