module Hydra.Network.Ouroboros.Type where

import Hydra.Prelude

import Cardano.Binary qualified as CBOR
import Codec.CBOR.Read qualified as CBOR
import GHC.Show (Show (show))
import Network.TypedProtocol (PeerHasAgency (ClientAgency), Protocol (..))
import Network.TypedProtocol.Codec (Codec)
import Network.TypedProtocol.Codec.CBOR (mkCodecCborLazyBS)
import Network.TypedProtocol.Core (PeerRole)
import Network.TypedProtocol.Driver (SomeMessage (SomeMessage))
import Ouroboros.Consensus.Util (ShowProxy (..))

-- | TODO explain Protocol
--
-- It is used both as a type level tag for the protocol and as the kind of the
-- types of the states in the protocol state machine. That is @FireForget@ is a
-- kind, and @StIdle@ is a type of that kind.
data FireForget msg where
  StIdle :: FireForget msg
  StDone :: FireForget msg

instance ShowProxy (FireForget msg) where
  showProxy :: Proxy (FireForget msg) -> String
showProxy Proxy (FireForget msg)
_ = String
"FireForget"

instance Protocol (FireForget msg) where
  -- The actual messages in our protocol.
  --
  -- Messages define the possible transitions between the protocol's state as defined
  -- by `FireForget`. In this particular case things are extremely simple: The protocol
  -- handles `Msg` containing some payload until terminated by `MsgDone`.
  data Message (FireForget msg) from to where
    MsgSend :: msg -> Message (FireForget msg) 'StIdle 'StIdle
    MsgDone :: Message (FireForget msg) 'StIdle 'StDone

  -- We have to explain to the framework what our states mean, in terms of
  -- who is expected to send and receive in the different states.
  --
  -- Idle states are where it is for the client to send a message.
  data ClientHasAgency st where
    TokIdle :: ClientHasAgency 'StIdle

  -- In our protocol the server is always receiving, thus in no state the server
  -- has agency.
  data ServerHasAgency st

  -- In the done state neither client nor server can send messages.
  data NobodyHasAgency st where
    TokDone :: NobodyHasAgency 'StDone

  exclusionLemma_ClientAndServerHaveAgency :: forall (st :: FireForget msg).
ClientHasAgency st -> ServerHasAgency st -> Void
exclusionLemma_ClientAndServerHaveAgency ClientHasAgency st
R:ClientHasAgencyFireForgetst k msg st
TokIdle ServerHasAgency st
tok = case ServerHasAgency st
tok of {}
  exclusionLemma_NobodyAndClientHaveAgency :: forall (st :: FireForget msg).
NobodyHasAgency st -> ClientHasAgency st -> Void
exclusionLemma_NobodyAndClientHaveAgency NobodyHasAgency st
R:NobodyHasAgencyFireForgetst k msg st
TokDone ClientHasAgency st
tok = case ClientHasAgency st
tok of {}
  exclusionLemma_NobodyAndServerHaveAgency :: forall (st :: FireForget msg).
NobodyHasAgency st -> ServerHasAgency st -> Void
exclusionLemma_NobodyAndServerHaveAgency NobodyHasAgency st
R:NobodyHasAgencyFireForgetst k msg st
TokDone ServerHasAgency st
tok = case ServerHasAgency st
tok of {}

deriving stock instance Show msg => Show (Message (FireForget msg) from to)

deriving stock instance Eq msg => Eq (Message (FireForget msg) from to)

instance Show (ClientHasAgency (st :: FireForget msg)) where
  show :: ClientHasAgency st -> String
show ClientHasAgency st
R:ClientHasAgencyFireForgetst k msg st
TokIdle = String
"TokIdle"

instance Show (ServerHasAgency (st :: FireForget msg)) where
  show :: ServerHasAgency st -> String
show ServerHasAgency st
_ = Text -> String
forall a t. (HasCallStack, IsText t) => t -> a
error Text
"absurd"

codecFireForget ::
  forall a m.
  ( MonadST m
  , ToCBOR a
  , FromCBOR a
  ) =>
  Codec (FireForget a) CBOR.DeserialiseFailure m LByteString
codecFireForget :: forall a (m :: * -> *).
(MonadST m, ToCBOR a, FromCBOR a) =>
Codec (FireForget a) DeserialiseFailure m LByteString
codecFireForget = (forall (pr :: PeerRole) (st :: FireForget a)
        (st' :: FireForget a).
 PeerHasAgency pr st -> Message (FireForget a) st st' -> Encoding)
-> (forall (pr :: PeerRole) (st :: FireForget a) s.
    PeerHasAgency pr st -> Decoder s (SomeMessage st))
-> Codec (FireForget a) DeserialiseFailure m LByteString
forall ps (m :: * -> *).
MonadST m =>
(forall (pr :: PeerRole) (st :: ps) (st' :: ps).
 PeerHasAgency pr st -> Message ps st st' -> Encoding)
-> (forall (pr :: PeerRole) (st :: ps) s.
    PeerHasAgency pr st -> Decoder s (SomeMessage st))
-> Codec ps DeserialiseFailure m LByteString
mkCodecCborLazyBS PeerHasAgency pr st -> Message (FireForget a) st st' -> Encoding
forall (pr :: PeerRole) (st :: FireForget a) (st' :: FireForget a).
PeerHasAgency pr st -> Message (FireForget a) st st' -> Encoding
encodeMsg PeerHasAgency pr st -> Decoder s (SomeMessage st)
forall (pr :: PeerRole) s (st :: FireForget a).
PeerHasAgency pr st -> Decoder s (SomeMessage st)
forall (pr :: PeerRole) (st :: FireForget a) s.
PeerHasAgency pr st -> Decoder s (SomeMessage st)
decodeMsg
 where
  encodeMsg ::
    forall (pr :: PeerRole) st st'.
    PeerHasAgency pr st ->
    Message (FireForget a) st st' ->
    CBOR.Encoding
  encodeMsg :: forall (pr :: PeerRole) (st :: FireForget a) (st' :: FireForget a).
PeerHasAgency pr st -> Message (FireForget a) st st' -> Encoding
encodeMsg (ClientAgency ClientHasAgency st
R:ClientHasAgencyFireForgetst (*) a st
TokIdle) Message (FireForget a) st st'
R:MessageFireForgetfromto (*) a st st'
MsgDone = Word -> Encoding
CBOR.encodeWord Word
0
  encodeMsg (ClientAgency ClientHasAgency st
R:ClientHasAgencyFireForgetst (*) a st
TokIdle) (MsgSend msg
msg) = Word -> Encoding
CBOR.encodeWord Word
1 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> msg -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR msg
msg

  decodeMsg ::
    forall (pr :: PeerRole) s (st :: FireForget a).
    PeerHasAgency pr st ->
    CBOR.Decoder s (SomeMessage st)
  decodeMsg :: forall (pr :: PeerRole) s (st :: FireForget a).
PeerHasAgency pr st -> Decoder s (SomeMessage st)
decodeMsg PeerHasAgency pr st
stok = do
    Word
key <- Decoder s Word
forall s. Decoder s Word
CBOR.decodeWord
    case (PeerHasAgency pr st
stok, Word
key) of
      (ClientAgency ClientHasAgency st
R:ClientHasAgencyFireForgetst (*) a st
TokIdle, Word
0) ->
        SomeMessage st -> Decoder s (SomeMessage st)
forall a. a -> Decoder s a
forall (m :: * -> *) a. Monad m => a -> m a
return (SomeMessage st -> Decoder s (SomeMessage st))
-> SomeMessage st -> Decoder s (SomeMessage st)
forall a b. (a -> b) -> a -> b
$ Message (FireForget a) st 'StDone -> SomeMessage st
forall ps (st :: ps) (st' :: ps).
Message ps st st' -> SomeMessage st
SomeMessage Message (FireForget a) st 'StDone
Message (FireForget a) 'StIdle 'StDone
forall {k} (msg :: k). Message (FireForget msg) 'StIdle 'StDone
MsgDone
      (ClientAgency ClientHasAgency st
R:ClientHasAgencyFireForgetst (*) a st
TokIdle, Word
1) -> do
        Message (FireForget a) st 'StIdle -> SomeMessage st
forall ps (st :: ps) (st' :: ps).
Message ps st st' -> SomeMessage st
SomeMessage (Message (FireForget a) st 'StIdle -> SomeMessage st)
-> (a -> Message (FireForget a) st 'StIdle) -> a -> SomeMessage st
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Message (FireForget a) st 'StIdle
a -> Message (FireForget a) 'StIdle 'StIdle
forall msg. msg -> Message (FireForget msg) 'StIdle 'StIdle
MsgSend (a -> SomeMessage st) -> Decoder s a -> Decoder s (SomeMessage st)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Decoder s a
forall s. Decoder s a
forall a s. FromCBOR a => Decoder s a
fromCBOR
      (ClientAgency ClientHasAgency st
R:ClientHasAgencyFireForgetst (*) a st
TokIdle, Word
_) ->
        String -> Decoder s (SomeMessage st)
forall a. String -> Decoder s a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"codecFireForget.StIdle: unexpected key"