{-# LANGUAGE DataKinds                #-}
{-# LANGUAGE FlexibleInstances        #-}
{-# LANGUAGE OverloadedStrings        #-}
{-# LANGUAGE PolyKinds                #-}
{-# LANGUAGE StandaloneDeriving       #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeData                 #-}
{-# LANGUAGE TypeFamilies             #-}


-- | Defines types for the local message notification protocol
--
module DMQ.Protocol.LocalMsgNotification.Type
  ( module DMQ.Protocol.LocalMsgNotification.Type
  , module Network.TypedProtocol.Core
    -- re-exports
  , StBlockingStyle (..)
  , BlockingReplyList (..)
  , SingBlockingStyle (..)
  ) where

import Data.Aeson
import Data.Foldable qualified as Foldable
import Data.Kind
import Data.Singletons

import Network.TypedProtocol.Codec (AnyMessage (..))
import Network.TypedProtocol.Core

import Ouroboros.Network.Protocol.TxSubmission2.Type (BlockingReplyList (..),
           SingBlockingStyle (..), StBlockingStyle (..))
import Ouroboros.Network.Util.ShowProxy

-- | There are some constraints of the protocol that are not captured in the
-- types of the messages, but are documented with the messages. Violation
-- of these constraints is also a protocol error. The constraints are intended
-- to ensure that implementations are able to work in bounded space.
--
instance Protocol (LocalMsgNotification msg) where
  -- | The messages in the protocol.
  --
  -- There are two ways to ask for messages, blocking and
  -- non-blocking
  --
  data Message (LocalMsgNotification msg) from to where

    -- | Request a list of messages from the server,
    --
    -- * The blocking case is used when the server has announced it has no
    --   further messages to provide, and otherwise the non-blocking request
    --   must be used.
    --
    -- TODO: this request should have the max number of messages that shall
    -- be returned?
    MsgRequest
      :: forall blocking msg.
         SingI blocking
      => SingBlockingStyle blocking
      -> Message (LocalMsgNotification msg) StIdle (StBusy blocking)

    -- | Reply with a list of messages, along with a flag indicating
    -- whether the server has more messages that it can provide.
    --
    MsgReply
      :: forall blocking msg.
         BlockingReplyList blocking msg
      -> HasMore
      -> Message (LocalMsgNotification msg) (StBusy blocking) StIdle

    -- | The client can terminate the exchange when it has the agency
    --
    MsgClientDone
      :: Message (LocalMsgNotification msg) StIdle StDone

  type StateAgency  (StBusy blocking)  = ServerAgency
  type StateAgency  StIdle  = ClientAgency
  type StateAgency  StDone  = NobodyAgency

  type StateToken = SingMsgNotification

deriving instance (Eq msg) =>
                  Eq (Message (LocalMsgNotification msg) from to)

deriving instance (Show msg) =>
                  Show (Message (LocalMsgNotification msg) from to)


-- | The kind of the local message notification protocol, and the types of
-- the states in the protocol state machine.
--
-- It is parameterised over the type of messages
--
type LocalMsgNotification :: Type -> Type
type data LocalMsgNotification msg where
  StIdle :: LocalMsgNotification msg
  StBusy :: StBlockingStyle -> LocalMsgNotification msg
  StDone :: LocalMsgNotification msg

instance ( ShowProxy msg
         ) => ShowProxy (LocalMsgNotification msg) where
    showProxy :: Proxy (LocalMsgNotification msg) -> String
showProxy Proxy (LocalMsgNotification msg)
_ =
      String
"LocalMsgNotification " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Proxy msg -> String
forall {k} (p :: k). ShowProxy p => Proxy p -> String
showProxy (Proxy msg
forall {k} (t :: k). Proxy t
Proxy :: Proxy msg)


-- | a singleton witness for protocol state
--
type SingMsgNotification :: LocalMsgNotification msg
                         -> Type
data SingMsgNotification k where
    SingIdle  :: SingMsgNotification  StIdle
    SingBusy  :: SingBlockingStyle blocking
              -> SingMsgNotification (StBusy blocking)
    SingDone  :: SingMsgNotification  StDone

deriving instance Show (SingMsgNotification k)

instance StateTokenI StIdle where stateToken :: StateToken StIdle
stateToken = StateToken StIdle
SingMsgNotification StIdle
forall {msg}. SingMsgNotification StIdle
SingIdle
instance SingI blocking => StateTokenI (StBusy blocking) where
  stateToken :: StateToken (StBusy blocking)
stateToken = SingBlockingStyle blocking -> SingMsgNotification (StBusy blocking)
forall {msg} (blocking :: StBlockingStyle).
SingBlockingStyle blocking -> SingMsgNotification (StBusy blocking)
SingBusy Sing blocking
SingBlockingStyle blocking
forall {k} (a :: k). SingI a => Sing a
sing
instance StateTokenI StDone where stateToken :: StateToken StDone
stateToken = StateToken StDone
SingMsgNotification StDone
forall {msg}. SingMsgNotification StDone
SingDone


-- | A boolean-like to indicate whether the server has more messages
-- that it can provide.
--
data HasMore = HasMore | DoesNotHaveMore
  deriving (HasMore -> HasMore -> Bool
(HasMore -> HasMore -> Bool)
-> (HasMore -> HasMore -> Bool) -> Eq HasMore
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: HasMore -> HasMore -> Bool
== :: HasMore -> HasMore -> Bool
$c/= :: HasMore -> HasMore -> Bool
/= :: HasMore -> HasMore -> Bool
Eq, Int -> HasMore -> ShowS
[HasMore] -> ShowS
HasMore -> String
(Int -> HasMore -> ShowS)
-> (HasMore -> String) -> ([HasMore] -> ShowS) -> Show HasMore
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> HasMore -> ShowS
showsPrec :: Int -> HasMore -> ShowS
$cshow :: HasMore -> String
show :: HasMore -> String
$cshowList :: [HasMore] -> ShowS
showList :: [HasMore] -> ShowS
Show)

instance ToJSON sig => ToJSON (AnyMessage (LocalMsgNotification sig)) where
  toJSON :: AnyMessage (LocalMsgNotification sig) -> Value
toJSON (AnyMessage Message (LocalMsgNotification sig) st st'
msg) = case Message (LocalMsgNotification sig) st st'
msg of
    MsgRequest SingBlockingStyle blocking
blockingStyle ->
      [Pair] -> Value
object [ Key
"type" Key -> Value -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= Text -> Value
String Text
"MsgRequest"
             , Key
"blockingStyle" Key -> String -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= SingBlockingStyle blocking -> String
forall a. Show a => a -> String
show SingBlockingStyle blocking
blockingStyle
             ]
    MsgReply BlockingReplyList blocking sig
msgs HasMore
hasMore ->
      [Pair] -> Value
object [ Key
"type" Key -> Value -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= Text -> Value
String Text
"MsgReply"
             , Key
"msgs" Key -> [sig] -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= BlockingReplyList blocking sig -> [sig]
forall a. BlockingReplyList blocking a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Foldable.toList BlockingReplyList blocking sig
msgs
             , Key
"hasMore" Key -> Bool -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= case HasMore
hasMore of
                  HasMore
HasMore         -> Bool
True
                  HasMore
DoesNotHaveMore -> Bool
False
             ]
    Message (LocalMsgNotification sig) st st'
R:MessageLocalMsgNotificationfromto sig st st'
MsgClientDone ->
      [Pair] -> Value
object [ Key
"type" Key -> Value -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= Text -> Value
String Text
"MsgClientDone"
             ]