{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE KindSignatures      #-}
{-# LANGUAGE NamedFieldPuns      #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Ouroboros.Network.Protocol.LocalStateQuery.Server
  ( -- * Protocol type for the server
    -- | The protocol states from the point of view of the server.
    LocalStateQueryServer (..)
  , ServerStIdle (..)
  , ServerStAcquiring (..)
  , ServerStAcquired (..)
  , ServerStQuerying (..)
    -- * Execution as a typed protocol
  , localStateQueryServerPeer
  ) where

import           Data.Kind (Type)
import           Network.TypedProtocol.Core

import           Ouroboros.Network.Protocol.LocalStateQuery.Type


newtype LocalStateQueryServer block point (query :: Type -> Type) m a = LocalStateQueryServer {
      LocalStateQueryServer block point query m a
-> m (ServerStIdle block point query m a)
runLocalStateQueryServer :: m (ServerStIdle block point query m a)
    }

-- | In the 'StIdle' protocol state, the server does not have agency. Instead
-- it is waiting for:
--
--  * a request to acquire a state
--  * a termination messge
--
-- It must be prepared to handle either.
--
data ServerStIdle block point query m a = ServerStIdle {
       ServerStIdle block point query m a
-> Maybe point -> m (ServerStAcquiring block point query m a)
recvMsgAcquire :: Maybe point
                      -> m (ServerStAcquiring block point query m a),

       ServerStIdle block point query m a -> m a
recvMsgDone    :: m a
     }

-- | In the 'StAcquiring' protocol state, the server has agency and must send
-- either:
--
--  * acquired
--  * failure to acquire
--
data ServerStAcquiring block point query m a where
  SendMsgAcquired :: ServerStAcquired  block point query m a
                  -> ServerStAcquiring block point query m a

  SendMsgFailure  :: AcquireFailure
                  -> ServerStIdle      block point query m a
                  -> ServerStAcquiring block point query m a

-- | In the 'StAcquired' protocol state, the server does not have agency.
-- Instead it is waiting for:
--
--  * a query
--  * a request to (re)acquire another state
--  * a release of the current state
--
-- It must be prepared to handle either.
--
data ServerStAcquired block point query m a = ServerStAcquired {
      ServerStAcquired block point query m a
-> forall result.
   query result -> m (ServerStQuerying block point query m a result)
recvMsgQuery     :: forall result.
                          query result
                       -> m (ServerStQuerying  block point query m a result),

      ServerStAcquired block point query m a
-> Maybe point -> m (ServerStAcquiring block point query m a)
recvMsgReAcquire :: Maybe point
                       -> m (ServerStAcquiring block point query m a),

      ServerStAcquired block point query m a
-> m (ServerStIdle block point query m a)
recvMsgRelease   :: m (ServerStIdle      block point query m a)
    }

-- | In the 'StQuerying' protocol state, the server has agency and must send:
--
--  * a result
--
data ServerStQuerying block point query m a result where
  SendMsgResult :: result
                -> ServerStAcquired block point query m a
                -> ServerStQuerying block point query m a result

-- | Interpret a 'LocalStateQueryServer' action sequence as a 'Peer' on the server
-- side of the 'LocalStateQuery' protocol.
--
localStateQueryServerPeer
  :: forall block point (query :: Type -> Type) m a.
     Monad m
  => LocalStateQueryServer block point query m a
  -> Peer (LocalStateQuery block point query) AsServer StIdle m a
localStateQueryServerPeer :: LocalStateQueryServer block point query m a
-> Peer (LocalStateQuery block point query) 'AsServer 'StIdle m a
localStateQueryServerPeer (LocalStateQueryServer m (ServerStIdle block point query m a)
handler) =
    m (Peer (LocalStateQuery block point query) 'AsServer 'StIdle m a)
-> Peer (LocalStateQuery block point query) 'AsServer 'StIdle m a
forall (m :: * -> *) ps (pr :: PeerRole) (st :: ps) a.
m (Peer ps pr st m a) -> Peer ps pr st m a
Effect (m (Peer (LocalStateQuery block point query) 'AsServer 'StIdle m a)
 -> Peer (LocalStateQuery block point query) 'AsServer 'StIdle m a)
-> m (Peer
        (LocalStateQuery block point query) 'AsServer 'StIdle m a)
-> Peer (LocalStateQuery block point query) 'AsServer 'StIdle m a
forall a b. (a -> b) -> a -> b
$ ServerStIdle block point query m a
-> Peer (LocalStateQuery block point query) 'AsServer 'StIdle m a
handleStIdle (ServerStIdle block point query m a
 -> Peer (LocalStateQuery block point query) 'AsServer 'StIdle m a)
-> m (ServerStIdle block point query m a)
-> m (Peer
        (LocalStateQuery block point query) 'AsServer 'StIdle m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (ServerStIdle block point query m a)
handler
  where
    handleStIdle
      :: ServerStIdle block point query m a
      -> Peer (LocalStateQuery block point query) AsServer StIdle m a
    handleStIdle :: ServerStIdle block point query m a
-> Peer (LocalStateQuery block point query) 'AsServer 'StIdle m a
handleStIdle ServerStIdle{Maybe point -> m (ServerStAcquiring block point query m a)
recvMsgAcquire :: Maybe point -> m (ServerStAcquiring block point query m a)
recvMsgAcquire :: forall block point (query :: * -> *) (m :: * -> *) a.
ServerStIdle block point query m a
-> Maybe point -> m (ServerStAcquiring block point query m a)
recvMsgAcquire, m a
recvMsgDone :: m a
recvMsgDone :: forall block point (query :: * -> *) (m :: * -> *) a.
ServerStIdle block point query m a -> m a
recvMsgDone} =
      TheyHaveAgency 'AsServer 'StIdle
-> (forall (st' :: LocalStateQuery block point query).
    Message (LocalStateQuery block point query) 'StIdle st'
    -> Peer (LocalStateQuery block point query) 'AsServer st' m a)
-> Peer (LocalStateQuery block point query) 'AsServer 'StIdle m a
forall (pr :: PeerRole) ps (st :: ps) (m :: * -> *) a.
TheyHaveAgency pr st
-> (forall (st' :: ps). Message ps st st' -> Peer ps pr st' m a)
-> Peer ps pr st m a
Await (ClientHasAgency 'StIdle -> PeerHasAgency 'AsClient 'StIdle
forall ps (st :: ps).
ClientHasAgency st -> PeerHasAgency 'AsClient st
ClientAgency ClientHasAgency 'StIdle
forall k k (block :: k) (point :: k) (query :: * -> *).
ClientHasAgency 'StIdle
TokIdle) ((forall (st' :: LocalStateQuery block point query).
  Message (LocalStateQuery block point query) 'StIdle st'
  -> Peer (LocalStateQuery block point query) 'AsServer st' m a)
 -> Peer (LocalStateQuery block point query) 'AsServer 'StIdle m a)
-> (forall (st' :: LocalStateQuery block point query).
    Message (LocalStateQuery block point query) 'StIdle st'
    -> Peer (LocalStateQuery block point query) 'AsServer st' m a)
-> Peer (LocalStateQuery block point query) 'AsServer 'StIdle m a
forall a b. (a -> b) -> a -> b
$ \Message (LocalStateQuery block point query) 'StIdle st'
req -> case Message (LocalStateQuery block point query) 'StIdle st'
req of
        MsgAcquire pt -> m (Peer
     (LocalStateQuery block point query) 'AsServer 'StAcquiring m a)
-> Peer
     (LocalStateQuery block point query) 'AsServer 'StAcquiring m a
forall (m :: * -> *) ps (pr :: PeerRole) (st :: ps) a.
m (Peer ps pr st m a) -> Peer ps pr st m a
Effect (m (Peer
      (LocalStateQuery block point query) 'AsServer 'StAcquiring m a)
 -> Peer
      (LocalStateQuery block point query) 'AsServer 'StAcquiring m a)
-> m (Peer
        (LocalStateQuery block point query) 'AsServer 'StAcquiring m a)
-> Peer
     (LocalStateQuery block point query) 'AsServer 'StAcquiring m a
forall a b. (a -> b) -> a -> b
$
          ServerStAcquiring block point query m a
-> Peer
     (LocalStateQuery block point query) 'AsServer 'StAcquiring m a
handleStAcquiring (ServerStAcquiring block point query m a
 -> Peer
      (LocalStateQuery block point query) 'AsServer 'StAcquiring m a)
-> m (ServerStAcquiring block point query m a)
-> m (Peer
        (LocalStateQuery block point query) 'AsServer 'StAcquiring m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe point -> m (ServerStAcquiring block point query m a)
recvMsgAcquire Maybe point
Maybe point
pt
        Message (LocalStateQuery block point query) 'StIdle st'
MsgDone       -> m (Peer (LocalStateQuery block point query) 'AsServer 'StDone m a)
-> Peer (LocalStateQuery block point query) 'AsServer 'StDone m a
forall (m :: * -> *) ps (pr :: PeerRole) (st :: ps) a.
m (Peer ps pr st m a) -> Peer ps pr st m a
Effect (m (Peer (LocalStateQuery block point query) 'AsServer 'StDone m a)
 -> Peer (LocalStateQuery block point query) 'AsServer 'StDone m a)
-> m (Peer
        (LocalStateQuery block point query) 'AsServer 'StDone m a)
-> Peer (LocalStateQuery block point query) 'AsServer 'StDone m a
forall a b. (a -> b) -> a -> b
$
          NobodyHasAgency 'StDone
-> a
-> Peer (LocalStateQuery block point query) 'AsServer 'StDone m a
forall ps (st :: ps) a (pr :: PeerRole) (m :: * -> *).
NobodyHasAgency st -> a -> Peer ps pr st m a
Done NobodyHasAgency 'StDone
forall k k (block :: k) (point :: k) (query :: * -> *).
NobodyHasAgency 'StDone
TokDone (a
 -> Peer (LocalStateQuery block point query) 'AsServer 'StDone m a)
-> m a
-> m (Peer
        (LocalStateQuery block point query) 'AsServer 'StDone m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m a
recvMsgDone

    handleStAcquiring
      :: ServerStAcquiring block point query m a
      -> Peer (LocalStateQuery block point query) AsServer StAcquiring m a
    handleStAcquiring :: ServerStAcquiring block point query m a
-> Peer
     (LocalStateQuery block point query) 'AsServer 'StAcquiring m a
handleStAcquiring ServerStAcquiring block point query m a
req = case ServerStAcquiring block point query m a
req of
      SendMsgAcquired ServerStAcquired block point query m a
stAcquired    ->
        WeHaveAgency 'AsServer 'StAcquiring
-> Message
     (LocalStateQuery block point query) 'StAcquiring 'StAcquired
-> Peer
     (LocalStateQuery block point query) 'AsServer 'StAcquired m a
-> Peer
     (LocalStateQuery block point query) 'AsServer 'StAcquiring m a
forall (pr :: PeerRole) ps (st :: ps) (st' :: ps) (m :: * -> *) a.
WeHaveAgency pr st
-> Message ps st st' -> Peer ps pr st' m a -> Peer ps pr st m a
Yield (ServerHasAgency 'StAcquiring -> WeHaveAgency 'AsServer 'StAcquiring
forall ps (st :: ps).
ServerHasAgency st -> PeerHasAgency 'AsServer st
ServerAgency ServerHasAgency 'StAcquiring
forall k k (block :: k) (point :: k) (query :: * -> *).
ServerHasAgency 'StAcquiring
TokAcquiring)
              Message
  (LocalStateQuery block point query) 'StAcquiring 'StAcquired
forall k k (block :: k) (point :: k) (query :: * -> *).
Message
  (LocalStateQuery block point query) 'StAcquiring 'StAcquired
MsgAcquired
              (ServerStAcquired block point query m a
-> Peer
     (LocalStateQuery block point query) 'AsServer 'StAcquired m a
handleStAcquired ServerStAcquired block point query m a
stAcquired)
      SendMsgFailure AcquireFailure
failure ServerStIdle block point query m a
stIdle ->
        WeHaveAgency 'AsServer 'StAcquiring
-> Message (LocalStateQuery block point query) 'StAcquiring 'StIdle
-> Peer (LocalStateQuery block point query) 'AsServer 'StIdle m a
-> Peer
     (LocalStateQuery block point query) 'AsServer 'StAcquiring m a
forall (pr :: PeerRole) ps (st :: ps) (st' :: ps) (m :: * -> *) a.
WeHaveAgency pr st
-> Message ps st st' -> Peer ps pr st' m a -> Peer ps pr st m a
Yield (ServerHasAgency 'StAcquiring -> WeHaveAgency 'AsServer 'StAcquiring
forall ps (st :: ps).
ServerHasAgency st -> PeerHasAgency 'AsServer st
ServerAgency ServerHasAgency 'StAcquiring
forall k k (block :: k) (point :: k) (query :: * -> *).
ServerHasAgency 'StAcquiring
TokAcquiring)
              (AcquireFailure
-> Message (LocalStateQuery block point query) 'StAcquiring 'StIdle
forall k k (block :: k) (point :: k) (query :: * -> *).
AcquireFailure
-> Message (LocalStateQuery block point query) 'StAcquiring 'StIdle
MsgFailure AcquireFailure
failure)
              (ServerStIdle block point query m a
-> Peer (LocalStateQuery block point query) 'AsServer 'StIdle m a
handleStIdle ServerStIdle block point query m a
stIdle)

    handleStAcquired
      :: ServerStAcquired block point query m a
      -> Peer (LocalStateQuery block point query) AsServer StAcquired m a
    handleStAcquired :: ServerStAcquired block point query m a
-> Peer
     (LocalStateQuery block point query) 'AsServer 'StAcquired m a
handleStAcquired ServerStAcquired{forall result.
query result -> m (ServerStQuerying block point query m a result)
recvMsgQuery :: forall result.
query result -> m (ServerStQuerying block point query m a result)
recvMsgQuery :: forall block point (query :: * -> *) (m :: * -> *) a.
ServerStAcquired block point query m a
-> forall result.
   query result -> m (ServerStQuerying block point query m a result)
recvMsgQuery, Maybe point -> m (ServerStAcquiring block point query m a)
recvMsgReAcquire :: Maybe point -> m (ServerStAcquiring block point query m a)
recvMsgReAcquire :: forall block point (query :: * -> *) (m :: * -> *) a.
ServerStAcquired block point query m a
-> Maybe point -> m (ServerStAcquiring block point query m a)
recvMsgReAcquire, m (ServerStIdle block point query m a)
recvMsgRelease :: m (ServerStIdle block point query m a)
recvMsgRelease :: forall block point (query :: * -> *) (m :: * -> *) a.
ServerStAcquired block point query m a
-> m (ServerStIdle block point query m a)
recvMsgRelease} =
      TheyHaveAgency 'AsServer 'StAcquired
-> (forall (st' :: LocalStateQuery block point query).
    Message (LocalStateQuery block point query) 'StAcquired st'
    -> Peer (LocalStateQuery block point query) 'AsServer st' m a)
-> Peer
     (LocalStateQuery block point query) 'AsServer 'StAcquired m a
forall (pr :: PeerRole) ps (st :: ps) (m :: * -> *) a.
TheyHaveAgency pr st
-> (forall (st' :: ps). Message ps st st' -> Peer ps pr st' m a)
-> Peer ps pr st m a
Await (ClientHasAgency 'StAcquired -> PeerHasAgency 'AsClient 'StAcquired
forall ps (st :: ps).
ClientHasAgency st -> PeerHasAgency 'AsClient st
ClientAgency ClientHasAgency 'StAcquired
forall k k (block :: k) (point :: k) (query :: * -> *).
ClientHasAgency 'StAcquired
TokAcquired) ((forall (st' :: LocalStateQuery block point query).
  Message (LocalStateQuery block point query) 'StAcquired st'
  -> Peer (LocalStateQuery block point query) 'AsServer st' m a)
 -> Peer
      (LocalStateQuery block point query) 'AsServer 'StAcquired m a)
-> (forall (st' :: LocalStateQuery block point query).
    Message (LocalStateQuery block point query) 'StAcquired st'
    -> Peer (LocalStateQuery block point query) 'AsServer st' m a)
-> Peer
     (LocalStateQuery block point query) 'AsServer 'StAcquired m a
forall a b. (a -> b) -> a -> b
$ \Message (LocalStateQuery block point query) 'StAcquired st'
req -> case Message (LocalStateQuery block point query) 'StAcquired st'
req of
        MsgQuery query  -> m (Peer
     (LocalStateQuery block point query)
     'AsServer
     ('StQuerying result)
     m
     a)
-> Peer
     (LocalStateQuery block point query)
     'AsServer
     ('StQuerying result)
     m
     a
forall (m :: * -> *) ps (pr :: PeerRole) (st :: ps) a.
m (Peer ps pr st m a) -> Peer ps pr st m a
Effect (m (Peer
      (LocalStateQuery block point query)
      'AsServer
      ('StQuerying result)
      m
      a)
 -> Peer
      (LocalStateQuery block point query)
      'AsServer
      ('StQuerying result)
      m
      a)
-> m (Peer
        (LocalStateQuery block point query)
        'AsServer
        ('StQuerying result)
        m
        a)
-> Peer
     (LocalStateQuery block point query)
     'AsServer
     ('StQuerying result)
     m
     a
forall a b. (a -> b) -> a -> b
$ query result
-> ServerStQuerying block point query m a result
-> Peer
     (LocalStateQuery block point query)
     'AsServer
     ('StQuerying result)
     m
     a
forall result.
query result
-> ServerStQuerying block point query m a result
-> Peer
     (LocalStateQuery block point query)
     'AsServer
     ('StQuerying result)
     m
     a
handleStQuerying query result
query (ServerStQuerying block point query m a result
 -> Peer
      (LocalStateQuery block point query)
      'AsServer
      ('StQuerying result)
      m
      a)
-> m (ServerStQuerying block point query m a result)
-> m (Peer
        (LocalStateQuery block point query)
        'AsServer
        ('StQuerying result)
        m
        a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> query result -> m (ServerStQuerying block point query m a result)
forall result.
query result -> m (ServerStQuerying block point query m a result)
recvMsgQuery query result
query
        MsgReAcquire pt -> m (Peer
     (LocalStateQuery block point query) 'AsServer 'StAcquiring m a)
-> Peer
     (LocalStateQuery block point query) 'AsServer 'StAcquiring m a
forall (m :: * -> *) ps (pr :: PeerRole) (st :: ps) a.
m (Peer ps pr st m a) -> Peer ps pr st m a
Effect (m (Peer
      (LocalStateQuery block point query) 'AsServer 'StAcquiring m a)
 -> Peer
      (LocalStateQuery block point query) 'AsServer 'StAcquiring m a)
-> m (Peer
        (LocalStateQuery block point query) 'AsServer 'StAcquiring m a)
-> Peer
     (LocalStateQuery block point query) 'AsServer 'StAcquiring m a
forall a b. (a -> b) -> a -> b
$ ServerStAcquiring block point query m a
-> Peer
     (LocalStateQuery block point query) 'AsServer 'StAcquiring m a
handleStAcquiring      (ServerStAcquiring block point query m a
 -> Peer
      (LocalStateQuery block point query) 'AsServer 'StAcquiring m a)
-> m (ServerStAcquiring block point query m a)
-> m (Peer
        (LocalStateQuery block point query) 'AsServer 'StAcquiring m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe point -> m (ServerStAcquiring block point query m a)
recvMsgReAcquire Maybe point
Maybe point
pt
        Message (LocalStateQuery block point query) 'StAcquired st'
MsgRelease      -> m (Peer (LocalStateQuery block point query) 'AsServer 'StIdle m a)
-> Peer (LocalStateQuery block point query) 'AsServer 'StIdle m a
forall (m :: * -> *) ps (pr :: PeerRole) (st :: ps) a.
m (Peer ps pr st m a) -> Peer ps pr st m a
Effect (m (Peer (LocalStateQuery block point query) 'AsServer 'StIdle m a)
 -> Peer (LocalStateQuery block point query) 'AsServer 'StIdle m a)
-> m (Peer
        (LocalStateQuery block point query) 'AsServer 'StIdle m a)
-> Peer (LocalStateQuery block point query) 'AsServer 'StIdle m a
forall a b. (a -> b) -> a -> b
$ ServerStIdle block point query m a
-> Peer (LocalStateQuery block point query) 'AsServer 'StIdle m a
handleStIdle           (ServerStIdle block point query m a
 -> Peer (LocalStateQuery block point query) 'AsServer 'StIdle m a)
-> m (ServerStIdle block point query m a)
-> m (Peer
        (LocalStateQuery block point query) 'AsServer 'StIdle m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (ServerStIdle block point query m a)
recvMsgRelease

    handleStQuerying
      :: query result
      -> ServerStQuerying block point query m a result
      -> Peer (LocalStateQuery block point query) AsServer (StQuerying result) m a
    handleStQuerying :: query result
-> ServerStQuerying block point query m a result
-> Peer
     (LocalStateQuery block point query)
     'AsServer
     ('StQuerying result)
     m
     a
handleStQuerying query result
query (SendMsgResult result
result ServerStAcquired block point query m a
stAcquired) =
      WeHaveAgency 'AsServer ('StQuerying result)
-> Message
     (LocalStateQuery block point query)
     ('StQuerying result)
     'StAcquired
-> Peer
     (LocalStateQuery block point query) 'AsServer 'StAcquired m a
-> Peer
     (LocalStateQuery block point query)
     'AsServer
     ('StQuerying result)
     m
     a
forall (pr :: PeerRole) ps (st :: ps) (st' :: ps) (m :: * -> *) a.
WeHaveAgency pr st
-> Message ps st st' -> Peer ps pr st' m a -> Peer ps pr st m a
Yield (ServerHasAgency ('StQuerying result)
-> WeHaveAgency 'AsServer ('StQuerying result)
forall ps (st :: ps).
ServerHasAgency st -> PeerHasAgency 'AsServer st
ServerAgency (query result -> ServerHasAgency ('StQuerying result)
forall k k (query :: * -> *) result (block :: k) (point :: k).
query result -> ServerHasAgency ('StQuerying result)
TokQuerying query result
query))
            (query result
-> result
-> Message
     (LocalStateQuery block point query)
     ('StQuerying result)
     'StAcquired
forall k k (query :: * -> *) result (block :: k) (point :: k).
query result
-> result
-> Message
     (LocalStateQuery block point query)
     ('StQuerying result)
     'StAcquired
MsgResult query result
query result
result)
            (ServerStAcquired block point query m a
-> Peer
     (LocalStateQuery block point query) 'AsServer 'StAcquired m a
handleStAcquired ServerStAcquired block point query m a
stAcquired)