{-# 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.Stateful.Peer.Server

import Ouroboros.Network.Protocol.LocalStateQuery.Type


newtype LocalStateQueryServer block point (query :: Type -> Type) m a = LocalStateQueryServer {
      forall block point (query :: * -> *) (m :: * -> *) a.
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 {
       forall block point (query :: * -> *) (m :: * -> *) a.
ServerStIdle block point query m a
-> Target point -> m (ServerStAcquiring block point query m a)
recvMsgAcquire :: Target point
                      -> m (ServerStAcquiring block point query m a),

       forall 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 {
      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     :: forall result.
                          query result
                       -> m (ServerStQuerying  block point query m a result),

      forall block point (query :: * -> *) (m :: * -> *) a.
ServerStAcquired block point query m a
-> Target point -> m (ServerStAcquiring block point query m a)
recvMsgReAcquire :: Target point
                       -> m (ServerStAcquiring block point query m a),

      forall 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
  -> Server (LocalStateQuery block point query) StIdle State m a
localStateQueryServerPeer :: forall block point (query :: * -> *) (m :: * -> *) a.
Monad m =>
LocalStateQueryServer block point query m a
-> Server (LocalStateQuery block point query) 'StIdle State m a
localStateQueryServerPeer (LocalStateQueryServer m (ServerStIdle block point query m a)
handler) =
    m (Server (LocalStateQuery block point query) 'StIdle State m a)
-> Server (LocalStateQuery block point query) 'StIdle State m a
forall ps (st :: ps) (f :: ps -> *) (m :: * -> *) a.
m (Server ps st f m a) -> Server ps st f m a
Effect (m (Server (LocalStateQuery block point query) 'StIdle State m a)
 -> Server (LocalStateQuery block point query) 'StIdle State m a)
-> m (Server (LocalStateQuery block point query) 'StIdle State m a)
-> Server (LocalStateQuery block point query) 'StIdle State m a
forall a b. (a -> b) -> a -> b
$ ServerStIdle block point query m a
-> Server (LocalStateQuery block point query) 'StIdle State m a
handleStIdle (ServerStIdle block point query m a
 -> Server (LocalStateQuery block point query) 'StIdle State m a)
-> m (ServerStIdle block point query m a)
-> m (Server (LocalStateQuery block point query) 'StIdle State 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
      -> Server (LocalStateQuery block point query) StIdle State m a
    handleStIdle :: ServerStIdle block point query m a
-> Server (LocalStateQuery block point query) 'StIdle State m a
handleStIdle ServerStIdle{Target point -> m (ServerStAcquiring block point query m a)
recvMsgAcquire :: forall block point (query :: * -> *) (m :: * -> *) a.
ServerStIdle block point query m a
-> Target point -> m (ServerStAcquiring block point query m a)
recvMsgAcquire :: Target point -> m (ServerStAcquiring block point query m a)
recvMsgAcquire, m a
recvMsgDone :: forall block point (query :: * -> *) (m :: * -> *) a.
ServerStIdle block point query m a -> m a
recvMsgDone :: m a
recvMsgDone} =
      (forall (st' :: LocalStateQuery block point query).
 State 'StIdle
 -> Message (LocalStateQuery block point query) 'StIdle st'
 -> (Server (LocalStateQuery block point query) st' State m a,
     State st'))
-> Server (LocalStateQuery block point query) 'StIdle State m a
forall ps (st :: ps) (f :: ps -> *) (m :: * -> *) a.
(StateTokenI st, StateAgency st ~ 'ClientAgency) =>
(forall (st' :: ps).
 f st -> Message ps st st' -> (Server ps st' f m a, f st'))
-> Server ps st f m a
Await ((forall (st' :: LocalStateQuery block point query).
  State 'StIdle
  -> Message (LocalStateQuery block point query) 'StIdle st'
  -> (Server (LocalStateQuery block point query) st' State m a,
      State st'))
 -> Server (LocalStateQuery block point query) 'StIdle State m a)
-> (forall (st' :: LocalStateQuery block point query).
    State 'StIdle
    -> Message (LocalStateQuery block point query) 'StIdle st'
    -> (Server (LocalStateQuery block point query) st' State m a,
        State st'))
-> Server (LocalStateQuery block point query) 'StIdle State m a
forall a b. (a -> b) -> a -> b
$ \State 'StIdle
_ Message (LocalStateQuery block point query) 'StIdle st'
req -> case Message (LocalStateQuery block point query) 'StIdle st'
req of
        MsgAcquire Target point
pt -> ( m (Server (LocalStateQuery block point query) st' State m a)
-> Server (LocalStateQuery block point query) st' State m a
forall ps (st :: ps) (f :: ps -> *) (m :: * -> *) a.
m (Server ps st f m a) -> Server ps st f m a
Effect (m (Server (LocalStateQuery block point query) st' State m a)
 -> Server (LocalStateQuery block point query) st' State m a)
-> m (Server (LocalStateQuery block point query) st' State m a)
-> Server (LocalStateQuery block point query) st' State m a
forall a b. (a -> b) -> a -> b
$ ServerStAcquiring block point query m a
-> Server (LocalStateQuery block point query) st' State m a
ServerStAcquiring block point query m a
-> Server
     (LocalStateQuery block point query) 'StAcquiring State m a
handleStAcquiring (ServerStAcquiring block point query m a
 -> Server (LocalStateQuery block point query) st' State m a)
-> m (ServerStAcquiring block point query m a)
-> m (Server (LocalStateQuery block point query) st' State m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Target point -> m (ServerStAcquiring block point query m a)
recvMsgAcquire Target point
pt
                         , State st'
State 'StAcquiring
forall {block} {point} {query :: * -> *}. State 'StAcquiring
StateAcquiring
                         )
        Message (LocalStateQuery block point query) 'StIdle st'
R:MessageLocalStateQueryfromto block point query 'StIdle st'
MsgDone -> ( m (Server (LocalStateQuery block point query) st' State m a)
-> Server (LocalStateQuery block point query) st' State m a
forall ps (st :: ps) (f :: ps -> *) (m :: * -> *) a.
m (Server ps st f m a) -> Server ps st f m a
Effect (m (Server (LocalStateQuery block point query) st' State m a)
 -> Server (LocalStateQuery block point query) st' State m a)
-> m (Server (LocalStateQuery block point query) st' State m a)
-> Server (LocalStateQuery block point query) st' State m a
forall a b. (a -> b) -> a -> b
$ a -> Server (LocalStateQuery block point query) st' State m a
forall ps (st :: ps) (f :: ps -> *) (m :: * -> *) a.
(StateTokenI st, StateAgency st ~ 'NobodyAgency) =>
a -> Server ps st f m a
Done (a -> Server (LocalStateQuery block point query) st' State m a)
-> m a
-> m (Server (LocalStateQuery block point query) st' State m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m a
recvMsgDone
                   , State st'
State 'StDone
forall {block} {point} {query :: * -> *}. State 'StDone
StateDone
                   )

    handleStAcquiring
      :: ServerStAcquiring block point query m a
      -> Server (LocalStateQuery block point query) StAcquiring State m a
    handleStAcquiring :: ServerStAcquiring block point query m a
-> Server
     (LocalStateQuery block point query) 'StAcquiring State 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    ->
        State 'StAcquiring
-> State 'StAcquired
-> Message
     (LocalStateQuery block point query) 'StAcquiring 'StAcquired
-> Server (LocalStateQuery block point query) 'StAcquired State m a
-> Server
     (LocalStateQuery block point query) 'StAcquiring State m a
forall ps (st :: ps) (f :: ps -> *) (m :: * -> *) a (st' :: ps).
(StateTokenI st, StateTokenI st',
 StateAgency st ~ 'ServerAgency) =>
f st
-> f st'
-> Message ps st st'
-> Server ps st' f m a
-> Server ps st f m a
Yield State 'StAcquiring
forall {block} {point} {query :: * -> *}. State 'StAcquiring
StateAcquiring State 'StAcquired
forall {block} {point} {query :: * -> *}. State 'StAcquired
StateAcquired
              Message
  (LocalStateQuery block point query) 'StAcquiring 'StAcquired
forall block point (query :: * -> *).
Message
  (LocalStateQuery block point query) 'StAcquiring 'StAcquired
MsgAcquired
              (ServerStAcquired block point query m a
-> Server (LocalStateQuery block point query) 'StAcquired State m a
handleStAcquired ServerStAcquired block point query m a
stAcquired)
      SendMsgFailure AcquireFailure
failure ServerStIdle block point query m a
stIdle ->
        State 'StAcquiring
-> State 'StIdle
-> Message (LocalStateQuery block point query) 'StAcquiring 'StIdle
-> Server (LocalStateQuery block point query) 'StIdle State m a
-> Server
     (LocalStateQuery block point query) 'StAcquiring State m a
forall ps (st :: ps) (f :: ps -> *) (m :: * -> *) a (st' :: ps).
(StateTokenI st, StateTokenI st',
 StateAgency st ~ 'ServerAgency) =>
f st
-> f st'
-> Message ps st st'
-> Server ps st' f m a
-> Server ps st f m a
Yield State 'StAcquiring
forall {block} {point} {query :: * -> *}. State 'StAcquiring
StateAcquiring State 'StIdle
forall {block} {point} {query :: * -> *}. State 'StIdle
StateIdle
              (AcquireFailure
-> Message (LocalStateQuery block point query) 'StAcquiring 'StIdle
forall block point (query :: * -> *).
AcquireFailure
-> Message (LocalStateQuery block point query) 'StAcquiring 'StIdle
MsgFailure AcquireFailure
failure)
              (ServerStIdle block point query m a
-> Server (LocalStateQuery block point query) 'StIdle State m a
handleStIdle ServerStIdle block point query m a
stIdle)

    handleStAcquired
      :: ServerStAcquired block point query m a
      -> Server (LocalStateQuery block point query) StAcquired State m a
    handleStAcquired :: ServerStAcquired block point query m a
-> Server (LocalStateQuery block point query) 'StAcquired State m a
handleStAcquired ServerStAcquired{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 :: forall result.
query result -> m (ServerStQuerying block point query m a result)
recvMsgQuery, Target point -> m (ServerStAcquiring block point query m a)
recvMsgReAcquire :: forall block point (query :: * -> *) (m :: * -> *) a.
ServerStAcquired block point query m a
-> Target point -> m (ServerStAcquiring block point query m a)
recvMsgReAcquire :: Target point -> m (ServerStAcquiring block point query m a)
recvMsgReAcquire, 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 :: m (ServerStIdle block point query m a)
recvMsgRelease} =
      (forall (st' :: LocalStateQuery block point query).
 State 'StAcquired
 -> Message (LocalStateQuery block point query) 'StAcquired st'
 -> (Server (LocalStateQuery block point query) st' State m a,
     State st'))
-> Server (LocalStateQuery block point query) 'StAcquired State m a
forall ps (st :: ps) (f :: ps -> *) (m :: * -> *) a.
(StateTokenI st, StateAgency st ~ 'ClientAgency) =>
(forall (st' :: ps).
 f st -> Message ps st st' -> (Server ps st' f m a, f st'))
-> Server ps st f m a
Await ((forall (st' :: LocalStateQuery block point query).
  State 'StAcquired
  -> Message (LocalStateQuery block point query) 'StAcquired st'
  -> (Server (LocalStateQuery block point query) st' State m a,
      State st'))
 -> Server
      (LocalStateQuery block point query) 'StAcquired State m a)
-> (forall (st' :: LocalStateQuery block point query).
    State 'StAcquired
    -> Message (LocalStateQuery block point query) 'StAcquired st'
    -> (Server (LocalStateQuery block point query) st' State m a,
        State st'))
-> Server (LocalStateQuery block point query) 'StAcquired State m a
forall a b. (a -> b) -> a -> b
$ \State 'StAcquired
_ Message (LocalStateQuery block point query) 'StAcquired st'
req -> case Message (LocalStateQuery block point query) 'StAcquired st'
req of
        MsgQuery query result
query  -> ( m (Server (LocalStateQuery block point query) st' State m a)
-> Server (LocalStateQuery block point query) st' State m a
forall ps (st :: ps) (f :: ps -> *) (m :: * -> *) a.
m (Server ps st f m a) -> Server ps st f m a
Effect (m (Server (LocalStateQuery block point query) st' State m a)
 -> Server (LocalStateQuery block point query) st' State m a)
-> m (Server (LocalStateQuery block point query) st' State m a)
-> Server (LocalStateQuery block point query) st' State m a
forall a b. (a -> b) -> a -> b
$ query result
-> ServerStQuerying block point query m a result
-> Server
     (LocalStateQuery block point query) ('StQuerying result) State m a
forall result.
query result
-> ServerStQuerying block point query m a result
-> Server
     (LocalStateQuery block point query) ('StQuerying result) State m a
handleStQuerying query result
query (ServerStQuerying block point query m a result
 -> Server (LocalStateQuery block point query) st' State m a)
-> m (ServerStQuerying block point query m a result)
-> m (Server (LocalStateQuery block point query) st' State 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
                           , query result -> State ('StQuerying result)
forall (query :: * -> *) result block point.
query result -> State ('StQuerying result)
StateQuerying query result
query
                           )
        MsgReAcquire Target point
pt -> ( m (Server (LocalStateQuery block point query) st' State m a)
-> Server (LocalStateQuery block point query) st' State m a
forall ps (st :: ps) (f :: ps -> *) (m :: * -> *) a.
m (Server ps st f m a) -> Server ps st f m a
Effect (m (Server (LocalStateQuery block point query) st' State m a)
 -> Server (LocalStateQuery block point query) st' State m a)
-> m (Server (LocalStateQuery block point query) st' State m a)
-> Server (LocalStateQuery block point query) st' State m a
forall a b. (a -> b) -> a -> b
$ ServerStAcquiring block point query m a
-> Server (LocalStateQuery block point query) st' State m a
ServerStAcquiring block point query m a
-> Server
     (LocalStateQuery block point query) 'StAcquiring State m a
handleStAcquiring      (ServerStAcquiring block point query m a
 -> Server (LocalStateQuery block point query) st' State m a)
-> m (ServerStAcquiring block point query m a)
-> m (Server (LocalStateQuery block point query) st' State m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Target point -> m (ServerStAcquiring block point query m a)
recvMsgReAcquire Target point
pt
                           , State st'
State 'StAcquiring
forall {block} {point} {query :: * -> *}. State 'StAcquiring
StateAcquiring
                           )
        Message (LocalStateQuery block point query) 'StAcquired st'
R:MessageLocalStateQueryfromto block point query 'StAcquired st'
MsgRelease      -> ( m (Server (LocalStateQuery block point query) st' State m a)
-> Server (LocalStateQuery block point query) st' State m a
forall ps (st :: ps) (f :: ps -> *) (m :: * -> *) a.
m (Server ps st f m a) -> Server ps st f m a
Effect (m (Server (LocalStateQuery block point query) st' State m a)
 -> Server (LocalStateQuery block point query) st' State m a)
-> m (Server (LocalStateQuery block point query) st' State m a)
-> Server (LocalStateQuery block point query) st' State m a
forall a b. (a -> b) -> a -> b
$ ServerStIdle block point query m a
-> Server (LocalStateQuery block point query) st' State m a
ServerStIdle block point query m a
-> Server (LocalStateQuery block point query) 'StIdle State m a
handleStIdle           (ServerStIdle block point query m a
 -> Server (LocalStateQuery block point query) st' State m a)
-> m (ServerStIdle block point query m a)
-> m (Server (LocalStateQuery block point query) st' State m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (ServerStIdle block point query m a)
recvMsgRelease
                           , State st'
State 'StIdle
forall {block} {point} {query :: * -> *}. State 'StIdle
StateIdle
                           )

    handleStQuerying
      :: query result
      -> ServerStQuerying block point query m a result
      -> Server (LocalStateQuery block point query) (StQuerying result) State m a
    handleStQuerying :: forall result.
query result
-> ServerStQuerying block point query m a result
-> Server
     (LocalStateQuery block point query) ('StQuerying result) State m a
handleStQuerying query result
query (SendMsgResult result
result ServerStAcquired block point query m a
stAcquired) =
      State ('StQuerying result)
-> State 'StAcquired
-> Message
     (LocalStateQuery block point query)
     ('StQuerying result)
     'StAcquired
-> Server (LocalStateQuery block point query) 'StAcquired State m a
-> Server
     (LocalStateQuery block point query) ('StQuerying result) State m a
forall ps (st :: ps) (f :: ps -> *) (m :: * -> *) a (st' :: ps).
(StateTokenI st, StateTokenI st',
 StateAgency st ~ 'ServerAgency) =>
f st
-> f st'
-> Message ps st st'
-> Server ps st' f m a
-> Server ps st f m a
Yield (query result -> State ('StQuerying result)
forall (query :: * -> *) result block point.
query result -> State ('StQuerying result)
StateQuerying query result
query) State 'StAcquired
forall {block} {point} {query :: * -> *}. State 'StAcquired
StateAcquired
            (result
-> Message
     (LocalStateQuery block point query)
     ('StQuerying result)
     'StAcquired
forall result block point (query :: * -> *).
result
-> Message
     (LocalStateQuery block point query)
     ('StQuerying result)
     'StAcquired
MsgResult result
result)
            (ServerStAcquired block point query m a
-> Server (LocalStateQuery block point query) 'StAcquired State m a
handleStAcquired ServerStAcquired block point query m a
stAcquired)