{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE NamedFieldPuns        #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE TypeInType            #-}
-- @UndecidableInstances@ extension is required for defining @Show@ instance of
-- @'AnyMessage'@ and @'AnyMessageAndAgency'@.
{-# LANGUAGE UndecidableInstances  #-}

module Network.TypedProtocol.Codec
  ( -- * Defining and using Codecs
    Codec (..)
  , hoistCodec
  , isoCodec
  , mapFailureCodec
    -- ** Related types
  , PeerRole (..)
  , PeerHasAgency (..)
  , WeHaveAgency
  , TheyHaveAgency
  , SomeMessage (..)
  , CodecFailure (..)
    -- ** Incremental decoding
  , DecodeStep (..)
  , runDecoder
  , runDecoderPure
    -- ** Codec properties
  , AnyMessage (..)
  , AnyMessageAndAgency (..)
  , prop_codecM
  , prop_codec
  , prop_codec_splitsM
  , prop_codec_splits
  , prop_codec_binary_compatM
  , prop_codec_binary_compat
  , prop_codecs_compatM
  , prop_codecs_compat
  , SamePeerHasAgency (..)
  ) where

import           Control.Exception (Exception)
import           Data.Kind (Type)
import           Data.Monoid (All (..))

import           Network.TypedProtocol.Core (PeerHasAgency (..), PeerRole (..),
                     Protocol (..), TheyHaveAgency, WeHaveAgency)
import           Network.TypedProtocol.Driver (SomeMessage (..))

-- | A codec for a 'Protocol' handles the encoding and decoding of typed
-- protocol messages. This is typically used when sending protocol messages
-- over untyped channels. The codec chooses the exact encoding, for example
-- encoding in some text-based syntax, or some choice of binary format.
--
-- The codec is parametrised by:
--
-- * The protocol
-- * The peer role (client\/server)
-- * the type of decoding failures
-- * the monad in which the decoder runs
-- * the type of the encoded data (typically strings or bytes)
--
-- It is expected that typical codec implementations will be polymorphic in
-- the peer role. For example a codec for the ping\/pong protocol might have
-- type:
--
-- > codecPingPong :: forall m. Monad m => Codec PingPong String m String
--
-- A codec consists of a message encoder and a decoder.
--
-- The encoder is supplied both with the message to encode and the current
-- protocol state (matching the message). The protocol state can be either
-- a client or server state, but for either peer role it is a protocol state
-- in which the peer has agency, since those are the only states where a
-- peer needs to encode a message to be able to send it.
--
-- For example a simple text encoder for the ping\/pong protocol could be:
--
-- > encode :: WeHaveAgency pr st
-- >        -> Message PingPong st st'
-- >        -> String
-- >  encode (ClientAgency TokIdle) MsgPing = "ping\n"
-- >  encode (ClientAgency TokIdle) MsgDone = "done\n"
-- >  encode (ServerAgency TokBusy) MsgPong = "pong\n"
--
-- The decoder is also given the current protocol state and it is expected to
-- be able to decode /any/ message that is valid in that state, but /only/
-- messages that are valid in that state. Messages that are unexpected for the
-- current state should be treated like any other decoding format error.
--
-- While the current protocol state is known, the state that the message will
-- have the peer transition to is not known. For this reason the decoded
-- message is wrapped in the 'SomeMessage' constructor which hides the \"to\"
-- state.
--
-- The decoder uses an incremental decoding interface 'DecodeStep' so that
-- input can be supplied (e.g. from a Channel) bit by bit. This style of
-- decoder allows but does not require a format with message framing where the
-- decoder input matches exactly with the message boundaries.
--
-- > decode :: TheyHaveAgency pr st
-- >        -> m (DecodeStep String String m (SomeMessage st))
-- > decode stok =
-- >   decodeTerminatedFrame '\n' $ \str trailing ->
-- >     case (stok, str) of
-- >       (ServerAgency TokBusy, "pong") ->
-- >            DecodeDone (SomeMessage MsgPong) trailing
-- >       (ClientAgency TokIdle, "ping") ->
-- >            DecodeDone (SomeMessage MsgPing) trailing
-- >       (ClientAgency TokIdle, "done") ->
-- >            DecodeDone (SomeMessage MsgDone) trailing
-- >       _ -> DecodeFail ("unexpected message: " ++ str)
--
-- The main thing to note is the pattern matching on the combination of the
-- message string and the protocol state. This neatly fulfils the requirement
-- that we only return messages that are of the correct type for the given
-- protocol state.
--
-- This toy example format uses newlines @\n@ as a framing format. See
-- 'DecodeStep' for suggestions on how to use it for more realistic formats.
--
data Codec ps failure m bytes = Codec {
       Codec ps failure m bytes
-> forall (pr :: PeerRole) (st :: ps) (st' :: ps).
   PeerHasAgency pr st -> Message ps st st' -> bytes
encode :: forall (pr :: PeerRole) (st :: ps) (st' :: ps).
                 PeerHasAgency pr st
              -> Message ps st st'
              -> bytes,

       Codec ps failure m bytes
-> forall (pr :: PeerRole) (st :: ps).
   PeerHasAgency pr st
   -> m (DecodeStep bytes failure m (SomeMessage st))
decode :: forall (pr :: PeerRole) (st :: ps).
                 PeerHasAgency pr st
              -> m (DecodeStep bytes failure m (SomeMessage st))
     }

hoistCodec
  :: ( Functor n )
  => (forall x . m x -> n x)
  -> Codec ps failure m bytes
  -> Codec ps failure n bytes
hoistCodec :: (forall x. m x -> n x)
-> Codec ps failure m bytes -> Codec ps failure n bytes
hoistCodec forall x. m x -> n x
nat Codec ps failure m bytes
codec = Codec ps failure m bytes
codec
  { decode :: forall (pr :: PeerRole) (st :: ps).
PeerHasAgency pr st
-> n (DecodeStep bytes failure n (SomeMessage st))
decode = (DecodeStep bytes failure m (SomeMessage st)
 -> DecodeStep bytes failure n (SomeMessage st))
-> n (DecodeStep bytes failure m (SomeMessage st))
-> n (DecodeStep bytes failure n (SomeMessage st))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((forall x. m x -> n x)
-> DecodeStep bytes failure m (SomeMessage st)
-> DecodeStep bytes failure n (SomeMessage st)
forall (n :: * -> *) (m :: * -> *) bytes failure a.
Functor n =>
(forall x. m x -> n x)
-> DecodeStep bytes failure m a -> DecodeStep bytes failure n a
hoistDecodeStep forall x. m x -> n x
nat) (n (DecodeStep bytes failure m (SomeMessage st))
 -> n (DecodeStep bytes failure n (SomeMessage st)))
-> (PeerHasAgency pr st
    -> n (DecodeStep bytes failure m (SomeMessage st)))
-> PeerHasAgency pr st
-> n (DecodeStep bytes failure n (SomeMessage st))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m (DecodeStep bytes failure m (SomeMessage st))
-> n (DecodeStep bytes failure m (SomeMessage st))
forall x. m x -> n x
nat (m (DecodeStep bytes failure m (SomeMessage st))
 -> n (DecodeStep bytes failure m (SomeMessage st)))
-> (PeerHasAgency pr st
    -> m (DecodeStep bytes failure m (SomeMessage st)))
-> PeerHasAgency pr st
-> n (DecodeStep bytes failure m (SomeMessage st))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Codec ps failure m bytes
-> forall (pr :: PeerRole) (st :: ps).
   PeerHasAgency pr st
   -> m (DecodeStep bytes failure m (SomeMessage st))
forall ps failure (m :: * -> *) bytes.
Codec ps failure m bytes
-> forall (pr :: PeerRole) (st :: ps).
   PeerHasAgency pr st
   -> m (DecodeStep bytes failure m (SomeMessage st))
decode Codec ps failure m bytes
codec
  }

isoCodec :: Functor m
         => (bytes -> bytes')
         -> (bytes' -> bytes)
         -> Codec ps failure m bytes
         -> Codec ps failure m bytes'
isoCodec :: (bytes -> bytes')
-> (bytes' -> bytes)
-> Codec ps failure m bytes
-> Codec ps failure m bytes'
isoCodec bytes -> bytes'
f bytes' -> bytes
finv Codec {forall (pr :: PeerRole) (st :: ps) (st' :: ps).
PeerHasAgency pr st -> Message ps st st' -> bytes
encode :: forall (pr :: PeerRole) (st :: ps) (st' :: ps).
PeerHasAgency pr st -> Message ps st st' -> bytes
encode :: forall ps failure (m :: * -> *) bytes.
Codec ps failure m bytes
-> forall (pr :: PeerRole) (st :: ps) (st' :: ps).
   PeerHasAgency pr st -> Message ps st st' -> bytes
encode, forall (pr :: PeerRole) (st :: ps).
PeerHasAgency pr st
-> m (DecodeStep bytes failure m (SomeMessage st))
decode :: forall (pr :: PeerRole) (st :: ps).
PeerHasAgency pr st
-> m (DecodeStep bytes failure m (SomeMessage st))
decode :: forall ps failure (m :: * -> *) bytes.
Codec ps failure m bytes
-> forall (pr :: PeerRole) (st :: ps).
   PeerHasAgency pr st
   -> m (DecodeStep bytes failure m (SomeMessage st))
decode} = Codec :: forall ps failure (m :: * -> *) bytes.
(forall (pr :: PeerRole) (st :: ps) (st' :: ps).
 PeerHasAgency pr st -> Message ps st st' -> bytes)
-> (forall (pr :: PeerRole) (st :: ps).
    PeerHasAgency pr st
    -> m (DecodeStep bytes failure m (SomeMessage st)))
-> Codec ps failure m bytes
Codec {
      encode :: forall (pr :: PeerRole) (st :: ps) (st' :: ps).
PeerHasAgency pr st -> Message ps st st' -> bytes'
encode = \PeerHasAgency pr st
tok Message ps st st'
msg -> bytes -> bytes'
f (bytes -> bytes') -> bytes -> bytes'
forall a b. (a -> b) -> a -> b
$ PeerHasAgency pr st -> Message ps st st' -> bytes
forall (pr :: PeerRole) (st :: ps) (st' :: ps).
PeerHasAgency pr st -> Message ps st st' -> bytes
encode PeerHasAgency pr st
tok Message ps st st'
msg,
      decode :: forall (pr :: PeerRole) (st :: ps).
PeerHasAgency pr st
-> m (DecodeStep bytes' failure m (SomeMessage st))
decode = \PeerHasAgency pr st
tok -> (bytes -> bytes')
-> (bytes' -> bytes)
-> DecodeStep bytes failure m (SomeMessage st)
-> DecodeStep bytes' failure m (SomeMessage st)
forall (m :: * -> *) bytes bytes' failure a.
Functor m =>
(bytes -> bytes')
-> (bytes' -> bytes)
-> DecodeStep bytes failure m a
-> DecodeStep bytes' failure m a
isoDecodeStep bytes -> bytes'
f bytes' -> bytes
finv (DecodeStep bytes failure m (SomeMessage st)
 -> DecodeStep bytes' failure m (SomeMessage st))
-> m (DecodeStep bytes failure m (SomeMessage st))
-> m (DecodeStep bytes' failure m (SomeMessage st))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PeerHasAgency pr st
-> m (DecodeStep bytes failure m (SomeMessage st))
forall (pr :: PeerRole) (st :: ps).
PeerHasAgency pr st
-> m (DecodeStep bytes failure m (SomeMessage st))
decode PeerHasAgency pr st
tok
    }

mapFailureCodec
  :: Functor m
  => (failure -> failure')
  -> Codec ps failure  m bytes
  -> Codec ps failure' m bytes
mapFailureCodec :: (failure -> failure')
-> Codec ps failure m bytes -> Codec ps failure' m bytes
mapFailureCodec failure -> failure'
f Codec {forall (pr :: PeerRole) (st :: ps) (st' :: ps).
PeerHasAgency pr st -> Message ps st st' -> bytes
encode :: forall (pr :: PeerRole) (st :: ps) (st' :: ps).
PeerHasAgency pr st -> Message ps st st' -> bytes
encode :: forall ps failure (m :: * -> *) bytes.
Codec ps failure m bytes
-> forall (pr :: PeerRole) (st :: ps) (st' :: ps).
   PeerHasAgency pr st -> Message ps st st' -> bytes
encode, forall (pr :: PeerRole) (st :: ps).
PeerHasAgency pr st
-> m (DecodeStep bytes failure m (SomeMessage st))
decode :: forall (pr :: PeerRole) (st :: ps).
PeerHasAgency pr st
-> m (DecodeStep bytes failure m (SomeMessage st))
decode :: forall ps failure (m :: * -> *) bytes.
Codec ps failure m bytes
-> forall (pr :: PeerRole) (st :: ps).
   PeerHasAgency pr st
   -> m (DecodeStep bytes failure m (SomeMessage st))
decode} = Codec :: forall ps failure (m :: * -> *) bytes.
(forall (pr :: PeerRole) (st :: ps) (st' :: ps).
 PeerHasAgency pr st -> Message ps st st' -> bytes)
-> (forall (pr :: PeerRole) (st :: ps).
    PeerHasAgency pr st
    -> m (DecodeStep bytes failure m (SomeMessage st)))
-> Codec ps failure m bytes
Codec {
    encode :: forall (pr :: PeerRole) (st :: ps) (st' :: ps).
PeerHasAgency pr st -> Message ps st st' -> bytes
encode = forall (pr :: PeerRole) (st :: ps) (st' :: ps).
PeerHasAgency pr st -> Message ps st st' -> bytes
encode,
    decode :: forall (pr :: PeerRole) (st :: ps).
PeerHasAgency pr st
-> m (DecodeStep bytes failure' m (SomeMessage st))
decode = \PeerHasAgency pr st
tok -> (failure -> failure')
-> DecodeStep bytes failure m (SomeMessage st)
-> DecodeStep bytes failure' m (SomeMessage st)
forall (m :: * -> *) failure failure' bytes a.
Functor m =>
(failure -> failure')
-> DecodeStep bytes failure m a -> DecodeStep bytes failure' m a
mapFailureDecodeStep failure -> failure'
f (DecodeStep bytes failure m (SomeMessage st)
 -> DecodeStep bytes failure' m (SomeMessage st))
-> m (DecodeStep bytes failure m (SomeMessage st))
-> m (DecodeStep bytes failure' m (SomeMessage st))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PeerHasAgency pr st
-> m (DecodeStep bytes failure m (SomeMessage st))
forall (pr :: PeerRole) (st :: ps).
PeerHasAgency pr st
-> m (DecodeStep bytes failure m (SomeMessage st))
decode PeerHasAgency pr st
tok
  }

-- The types here are pretty fancy. The decode is polymorphic in the protocol
-- state, but only for kinds that are the same kind as the protocol state.
-- The TheyHaveAgency is a type family that resolves to a singleton, and the
-- result uses existential types to hide the unknown type of the state we're
-- transitioning to.
--
-- Both the Message and TheyHaveAgency data families are indexed on the kind ps
-- which is why it has to be a parameter here, otherwise these type functions
-- are unusable.


-- | An incremental decoder with return a value of type @a@.
--
-- This interface is not designed to be used directly for implementing
-- decoders, only for running them. In real applications it is expected to use
-- libraries for text or binary decoding and to implement appropriate wrappers
-- to match up with this incremental decoder interface.
--
-- This style of interface already closely matches that provided by libraries
-- such as @attoparsec@ for text formats, and @binary@, @cereal@ and @cborg@
-- for binary formats.
--
data DecodeStep bytes failure m a =

    -- | The decoder has consumed the available input and needs more
    -- to continue. Provide @'Just'@ if more input is available and
    -- @'Nothing'@ otherwise, and you will get a new @'DecodeStep'@.
    DecodePartial (Maybe bytes -> m (DecodeStep bytes failure m a))

    -- | The decoder has successfully finished. This provides the decoded
    -- result value plus any unused input.
  | DecodeDone a (Maybe bytes)

    -- | The decoder ran into an error. The decoder either used
    -- @'fail'@ or was not provided enough input.
  | DecodeFail failure

isoDecodeStep
  :: Functor m
  => (bytes -> bytes')
  -> (bytes' -> bytes)
  -> DecodeStep bytes failure m a
  -> DecodeStep bytes' failure m a
isoDecodeStep :: (bytes -> bytes')
-> (bytes' -> bytes)
-> DecodeStep bytes failure m a
-> DecodeStep bytes' failure m a
isoDecodeStep bytes -> bytes'
f  bytes' -> bytes
finv  (DecodePartial Maybe bytes -> m (DecodeStep bytes failure m a)
g)    = (Maybe bytes' -> m (DecodeStep bytes' failure m a))
-> DecodeStep bytes' failure m a
forall bytes failure (m :: * -> *) a.
(Maybe bytes -> m (DecodeStep bytes failure m a))
-> DecodeStep bytes failure m a
DecodePartial ((DecodeStep bytes failure m a -> DecodeStep bytes' failure m a)
-> m (DecodeStep bytes failure m a)
-> m (DecodeStep bytes' failure m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((bytes -> bytes')
-> (bytes' -> bytes)
-> DecodeStep bytes failure m a
-> DecodeStep bytes' failure m a
forall (m :: * -> *) bytes bytes' failure a.
Functor m =>
(bytes -> bytes')
-> (bytes' -> bytes)
-> DecodeStep bytes failure m a
-> DecodeStep bytes' failure m a
isoDecodeStep bytes -> bytes'
f bytes' -> bytes
finv) (m (DecodeStep bytes failure m a)
 -> m (DecodeStep bytes' failure m a))
-> (Maybe bytes' -> m (DecodeStep bytes failure m a))
-> Maybe bytes'
-> m (DecodeStep bytes' failure m a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe bytes -> m (DecodeStep bytes failure m a)
g (Maybe bytes -> m (DecodeStep bytes failure m a))
-> (Maybe bytes' -> Maybe bytes)
-> Maybe bytes'
-> m (DecodeStep bytes failure m a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (bytes' -> bytes) -> Maybe bytes' -> Maybe bytes
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap bytes' -> bytes
finv)
isoDecodeStep bytes -> bytes'
f  bytes' -> bytes
_finv (DecodeDone a
a Maybe bytes
bytes) = a -> Maybe bytes' -> DecodeStep bytes' failure m a
forall bytes failure (m :: * -> *) a.
a -> Maybe bytes -> DecodeStep bytes failure m a
DecodeDone a
a ((bytes -> bytes') -> Maybe bytes -> Maybe bytes'
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap bytes -> bytes'
f Maybe bytes
bytes)
isoDecodeStep bytes -> bytes'
_f bytes' -> bytes
_finv (DecodeFail failure
failure) = failure -> DecodeStep bytes' failure m a
forall bytes failure (m :: * -> *) a.
failure -> DecodeStep bytes failure m a
DecodeFail failure
failure

hoistDecodeStep
  :: ( Functor n )
  => (forall x . m x -> n x)
  -> DecodeStep bytes failure m a
  -> DecodeStep bytes failure n a
hoistDecodeStep :: (forall x. m x -> n x)
-> DecodeStep bytes failure m a -> DecodeStep bytes failure n a
hoistDecodeStep forall x. m x -> n x
nat DecodeStep bytes failure m a
step = case DecodeStep bytes failure m a
step of
  DecodeDone a
a Maybe bytes
mb -> a -> Maybe bytes -> DecodeStep bytes failure n a
forall bytes failure (m :: * -> *) a.
a -> Maybe bytes -> DecodeStep bytes failure m a
DecodeDone a
a Maybe bytes
mb
  DecodeFail failure
fail_AvoidNameShadow -> failure -> DecodeStep bytes failure n a
forall bytes failure (m :: * -> *) a.
failure -> DecodeStep bytes failure m a
DecodeFail failure
fail_AvoidNameShadow
  DecodePartial Maybe bytes -> m (DecodeStep bytes failure m a)
k -> (Maybe bytes -> n (DecodeStep bytes failure n a))
-> DecodeStep bytes failure n a
forall bytes failure (m :: * -> *) a.
(Maybe bytes -> m (DecodeStep bytes failure m a))
-> DecodeStep bytes failure m a
DecodePartial ((DecodeStep bytes failure m a -> DecodeStep bytes failure n a)
-> n (DecodeStep bytes failure m a)
-> n (DecodeStep bytes failure n a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((forall x. m x -> n x)
-> DecodeStep bytes failure m a -> DecodeStep bytes failure n a
forall (n :: * -> *) (m :: * -> *) bytes failure a.
Functor n =>
(forall x. m x -> n x)
-> DecodeStep bytes failure m a -> DecodeStep bytes failure n a
hoistDecodeStep forall x. m x -> n x
nat) (n (DecodeStep bytes failure m a)
 -> n (DecodeStep bytes failure n a))
-> (Maybe bytes -> n (DecodeStep bytes failure m a))
-> Maybe bytes
-> n (DecodeStep bytes failure n a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m (DecodeStep bytes failure m a)
-> n (DecodeStep bytes failure m a)
forall x. m x -> n x
nat (m (DecodeStep bytes failure m a)
 -> n (DecodeStep bytes failure m a))
-> (Maybe bytes -> m (DecodeStep bytes failure m a))
-> Maybe bytes
-> n (DecodeStep bytes failure m a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe bytes -> m (DecodeStep bytes failure m a)
k)

mapFailureDecodeStep
  :: Functor m
  => (failure -> failure')
  -> DecodeStep bytes failure  m a
  -> DecodeStep bytes failure' m a
mapFailureDecodeStep :: (failure -> failure')
-> DecodeStep bytes failure m a -> DecodeStep bytes failure' m a
mapFailureDecodeStep failure -> failure'
f DecodeStep bytes failure m a
step = case DecodeStep bytes failure m a
step of
  DecodeDone a
a Maybe bytes
mb    -> a -> Maybe bytes -> DecodeStep bytes failure' m a
forall bytes failure (m :: * -> *) a.
a -> Maybe bytes -> DecodeStep bytes failure m a
DecodeDone a
a Maybe bytes
mb
  DecodeFail failure
failure -> failure' -> DecodeStep bytes failure' m a
forall bytes failure (m :: * -> *) a.
failure -> DecodeStep bytes failure m a
DecodeFail (failure -> failure'
f failure
failure)
  DecodePartial Maybe bytes -> m (DecodeStep bytes failure m a)
k    -> (Maybe bytes -> m (DecodeStep bytes failure' m a))
-> DecodeStep bytes failure' m a
forall bytes failure (m :: * -> *) a.
(Maybe bytes -> m (DecodeStep bytes failure m a))
-> DecodeStep bytes failure m a
DecodePartial ((DecodeStep bytes failure m a -> DecodeStep bytes failure' m a)
-> m (DecodeStep bytes failure m a)
-> m (DecodeStep bytes failure' m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((failure -> failure')
-> DecodeStep bytes failure m a -> DecodeStep bytes failure' m a
forall (m :: * -> *) failure failure' bytes a.
Functor m =>
(failure -> failure')
-> DecodeStep bytes failure m a -> DecodeStep bytes failure' m a
mapFailureDecodeStep failure -> failure'
f) (m (DecodeStep bytes failure m a)
 -> m (DecodeStep bytes failure' m a))
-> (Maybe bytes -> m (DecodeStep bytes failure m a))
-> Maybe bytes
-> m (DecodeStep bytes failure' m a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe bytes -> m (DecodeStep bytes failure m a)
k)


-- | Each 'Codec' can use whatever @failure@ type is appropriate. This simple
-- exception type is provided for use by simple codecs (e.g. \"identity\") when
-- nothing more than a 'String' is needed. It is an instance of 'Exception'.
--
data CodecFailure = CodecFailureOutOfInput
                  | CodecFailure String
  deriving (CodecFailure -> CodecFailure -> Bool
(CodecFailure -> CodecFailure -> Bool)
-> (CodecFailure -> CodecFailure -> Bool) -> Eq CodecFailure
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CodecFailure -> CodecFailure -> Bool
$c/= :: CodecFailure -> CodecFailure -> Bool
== :: CodecFailure -> CodecFailure -> Bool
$c== :: CodecFailure -> CodecFailure -> Bool
Eq, Int -> CodecFailure -> ShowS
[CodecFailure] -> ShowS
CodecFailure -> String
(Int -> CodecFailure -> ShowS)
-> (CodecFailure -> String)
-> ([CodecFailure] -> ShowS)
-> Show CodecFailure
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CodecFailure] -> ShowS
$cshowList :: [CodecFailure] -> ShowS
show :: CodecFailure -> String
$cshow :: CodecFailure -> String
showsPrec :: Int -> CodecFailure -> ShowS
$cshowsPrec :: Int -> CodecFailure -> ShowS
Show)

-- safe instance with @UndecidableInstances@ in scope
instance Exception CodecFailure


--
-- Running decoders
--

-- | Run a codec incremental decoder 'DecodeStep' against a list of input.
--
-- It ignores any unused trailing data. This is useful for demos, quick
-- experiments and tests.
--
-- See also 'Network.TypedProtocol.Driver.runDecoderWithChannel'
--
runDecoder :: Monad m
           => [bytes]
           -> DecodeStep bytes failure m a
           -> m (Either failure a)
runDecoder :: [bytes] -> DecodeStep bytes failure m a -> m (Either failure a)
runDecoder [bytes]
_      (DecodeDone a
x Maybe bytes
_trailing) = Either failure a -> m (Either failure a)
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> Either failure a
forall a b. b -> Either a b
Right a
x)
runDecoder [bytes]
_      (DecodeFail failure
failure)     = Either failure a -> m (Either failure a)
forall (m :: * -> *) a. Monad m => a -> m a
return (failure -> Either failure a
forall a b. a -> Either a b
Left failure
failure)
runDecoder []     (DecodePartial Maybe bytes -> m (DecodeStep bytes failure m a)
k)        = Maybe bytes -> m (DecodeStep bytes failure m a)
k Maybe bytes
forall a. Maybe a
Nothing  m (DecodeStep bytes failure m a)
-> (DecodeStep bytes failure m a -> m (Either failure a))
-> m (Either failure a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [bytes] -> DecodeStep bytes failure m a -> m (Either failure a)
forall (m :: * -> *) bytes failure a.
Monad m =>
[bytes] -> DecodeStep bytes failure m a -> m (Either failure a)
runDecoder []
runDecoder (bytes
b:[bytes]
bs) (DecodePartial Maybe bytes -> m (DecodeStep bytes failure m a)
k)        = Maybe bytes -> m (DecodeStep bytes failure m a)
k (bytes -> Maybe bytes
forall a. a -> Maybe a
Just bytes
b) m (DecodeStep bytes failure m a)
-> (DecodeStep bytes failure m a -> m (Either failure a))
-> m (Either failure a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [bytes] -> DecodeStep bytes failure m a -> m (Either failure a)
forall (m :: * -> *) bytes failure a.
Monad m =>
[bytes] -> DecodeStep bytes failure m a -> m (Either failure a)
runDecoder [bytes]
bs


-- | A variant of 'runDecoder' that is suitable for \"pure\" monads that have
-- a run function. This includes 'ST', using 'Control.Monad.ST.runST'.
--
runDecoderPure :: Monad m
               => (forall b. m b -> b)
               -> m (DecodeStep bytes failure m a)
               -> [bytes]
               -> Either failure a
runDecoderPure :: (forall b. m b -> b)
-> m (DecodeStep bytes failure m a) -> [bytes] -> Either failure a
runDecoderPure forall b. m b -> b
runM m (DecodeStep bytes failure m a)
decoder [bytes]
bs = m (Either failure a) -> Either failure a
forall b. m b -> b
runM ([bytes] -> DecodeStep bytes failure m a -> m (Either failure a)
forall (m :: * -> *) bytes failure a.
Monad m =>
[bytes] -> DecodeStep bytes failure m a -> m (Either failure a)
runDecoder [bytes]
bs (DecodeStep bytes failure m a -> m (Either failure a))
-> m (DecodeStep bytes failure m a) -> m (Either failure a)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< m (DecodeStep bytes failure m a)
decoder)


--
-- Codec properties
--

-- | Any message for a protocol, without knowing the protocol state.
--
-- Used at least for 'Eq' instances for messages, but also as a target for an
-- identity codec `Codec ps failure m (AnyMessage ps)` .
--
data AnyMessage ps where
     AnyMessage :: Message ps st st' -> AnyMessage ps

-- requires @UndecidableInstances@ and @QuantifiedConstraints@.
instance (forall st st'. Show (Message ps st st')) => Show (AnyMessage ps) where
    show :: AnyMessage ps -> String
show (AnyMessage Message ps st st'
msg) = Message ps st st' -> String
forall a. Show a => a -> String
show Message ps st st'
msg

-- | Used to hold the 'PeerHasAgency' state token and a corresponding 'Message'.
--
-- Used where we don't know statically what the state type is, but need the
-- agency and message to match each other.
--
data AnyMessageAndAgency ps where
  AnyMessageAndAgency :: PeerHasAgency pr (st :: ps)
                      -> Message ps (st :: ps) (st' :: ps)
                      -> AnyMessageAndAgency ps

-- requires @UndecidableInstances@ and @QuantifiedConstraints@.
instance
    ( forall (st :: ps).             Show (ClientHasAgency st)
    , forall (st :: ps).             Show (ServerHasAgency st)
    , forall (st :: ps) (st' :: ps). Show (Message ps st st')
    ) => Show (AnyMessageAndAgency ps) where
  show :: AnyMessageAndAgency ps -> String
show (AnyMessageAndAgency PeerHasAgency pr st
agency Message ps st st'
msg) = (PeerHasAgency pr st, Message ps st st') -> String
forall a. Show a => a -> String
show (PeerHasAgency pr st
agency, Message ps st st'
msg)

-- | The 'Codec' round-trip property: decode after encode gives the same
-- message. Every codec must satisfy this property.
--
prop_codecM
  :: forall ps failure m bytes.
     ( Monad m
     , Eq (AnyMessage ps)
     )
  => Codec ps failure m bytes
  -> AnyMessageAndAgency ps
  -> m Bool
prop_codecM :: Codec ps failure m bytes -> AnyMessageAndAgency ps -> m Bool
prop_codecM Codec {forall (pr :: PeerRole) (st :: ps) (st' :: ps).
PeerHasAgency pr st -> Message ps st st' -> bytes
encode :: forall (pr :: PeerRole) (st :: ps) (st' :: ps).
PeerHasAgency pr st -> Message ps st st' -> bytes
encode :: forall ps failure (m :: * -> *) bytes.
Codec ps failure m bytes
-> forall (pr :: PeerRole) (st :: ps) (st' :: ps).
   PeerHasAgency pr st -> Message ps st st' -> bytes
encode, forall (pr :: PeerRole) (st :: ps).
PeerHasAgency pr st
-> m (DecodeStep bytes failure m (SomeMessage st))
decode :: forall (pr :: PeerRole) (st :: ps).
PeerHasAgency pr st
-> m (DecodeStep bytes failure m (SomeMessage st))
decode :: forall ps failure (m :: * -> *) bytes.
Codec ps failure m bytes
-> forall (pr :: PeerRole) (st :: ps).
   PeerHasAgency pr st
   -> m (DecodeStep bytes failure m (SomeMessage st))
decode} (AnyMessageAndAgency PeerHasAgency pr st
stok Message ps st st'
msg) = do
    Either failure (SomeMessage st)
r <- PeerHasAgency pr st
-> m (DecodeStep bytes failure m (SomeMessage st))
forall (pr :: PeerRole) (st :: ps).
PeerHasAgency pr st
-> m (DecodeStep bytes failure m (SomeMessage st))
decode PeerHasAgency pr st
stok m (DecodeStep bytes failure m (SomeMessage st))
-> (DecodeStep bytes failure m (SomeMessage st)
    -> m (Either failure (SomeMessage st)))
-> m (Either failure (SomeMessage st))
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [bytes]
-> DecodeStep bytes failure m (SomeMessage st)
-> m (Either failure (SomeMessage st))
forall (m :: * -> *) bytes failure a.
Monad m =>
[bytes] -> DecodeStep bytes failure m a -> m (Either failure a)
runDecoder [PeerHasAgency pr st -> Message ps st st' -> bytes
forall (pr :: PeerRole) (st :: ps) (st' :: ps).
PeerHasAgency pr st -> Message ps st st' -> bytes
encode PeerHasAgency pr st
stok Message ps st st'
msg]
    case Either failure (SomeMessage st)
r of
      Right (SomeMessage Message ps st st'
msg') -> Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> m Bool) -> Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ Message ps st st' -> AnyMessage ps
forall ps (st :: ps) (st' :: ps).
Message ps st st' -> AnyMessage ps
AnyMessage Message ps st st'
msg' AnyMessage ps -> AnyMessage ps -> Bool
forall a. Eq a => a -> a -> Bool
== Message ps st st' -> AnyMessage ps
forall ps (st :: ps) (st' :: ps).
Message ps st st' -> AnyMessage ps
AnyMessage Message ps st st'
msg
      Left failure
_                   -> Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

-- | The 'Codec' round-trip property in a pure monad.
--
prop_codec
  :: forall ps failure m bytes.
     (Monad m, Eq (AnyMessage ps))
  => (forall a. m a -> a)
  -> Codec ps failure m bytes
  -> AnyMessageAndAgency ps
  -> Bool
prop_codec :: (forall a. m a -> a)
-> Codec ps failure m bytes -> AnyMessageAndAgency ps -> Bool
prop_codec forall a. m a -> a
runM Codec ps failure m bytes
codec AnyMessageAndAgency ps
msg =
    m Bool -> Bool
forall a. m a -> a
runM (Codec ps failure m bytes -> AnyMessageAndAgency ps -> m Bool
forall ps failure (m :: * -> *) bytes.
(Monad m, Eq (AnyMessage ps)) =>
Codec ps failure m bytes -> AnyMessageAndAgency ps -> m Bool
prop_codecM Codec ps failure m bytes
codec AnyMessageAndAgency ps
msg)


-- | A variant on the codec round-trip property: given the encoding of a
-- message, check that decode always gives the same result irrespective
-- of how the chunks of input are fed to the incremental decoder.
--
-- This property guards against boundary errors in incremental decoders.
-- It is not necessary to check this for every message type, just for each
-- generic codec construction. For example given some binary serialisation
-- library one would write a generic adaptor to the codec interface. This
-- adaptor has to deal with the incremental decoding and this is what needs
-- to be checked.
--
prop_codec_splitsM
  :: forall ps failure m bytes.
     (Monad m, Eq (AnyMessage ps))
  => (bytes -> [[bytes]])   -- ^ alternative re-chunkings of serialised form
  -> Codec ps failure m bytes
  -> AnyMessageAndAgency ps
  -> m Bool
prop_codec_splitsM :: (bytes -> [[bytes]])
-> Codec ps failure m bytes -> AnyMessageAndAgency ps -> m Bool
prop_codec_splitsM bytes -> [[bytes]]
splits
                  Codec {forall (pr :: PeerRole) (st :: ps) (st' :: ps).
PeerHasAgency pr st -> Message ps st st' -> bytes
encode :: forall (pr :: PeerRole) (st :: ps) (st' :: ps).
PeerHasAgency pr st -> Message ps st st' -> bytes
encode :: forall ps failure (m :: * -> *) bytes.
Codec ps failure m bytes
-> forall (pr :: PeerRole) (st :: ps) (st' :: ps).
   PeerHasAgency pr st -> Message ps st st' -> bytes
encode, forall (pr :: PeerRole) (st :: ps).
PeerHasAgency pr st
-> m (DecodeStep bytes failure m (SomeMessage st))
decode :: forall (pr :: PeerRole) (st :: ps).
PeerHasAgency pr st
-> m (DecodeStep bytes failure m (SomeMessage st))
decode :: forall ps failure (m :: * -> *) bytes.
Codec ps failure m bytes
-> forall (pr :: PeerRole) (st :: ps).
   PeerHasAgency pr st
   -> m (DecodeStep bytes failure m (SomeMessage st))
decode} (AnyMessageAndAgency PeerHasAgency pr st
stok Message ps st st'
msg) = do
    [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool) -> m [Bool] -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [m Bool] -> m [Bool]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence
      [ do Either failure (SomeMessage st)
r <- PeerHasAgency pr st
-> m (DecodeStep bytes failure m (SomeMessage st))
forall (pr :: PeerRole) (st :: ps).
PeerHasAgency pr st
-> m (DecodeStep bytes failure m (SomeMessage st))
decode PeerHasAgency pr st
stok m (DecodeStep bytes failure m (SomeMessage st))
-> (DecodeStep bytes failure m (SomeMessage st)
    -> m (Either failure (SomeMessage st)))
-> m (Either failure (SomeMessage st))
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [bytes]
-> DecodeStep bytes failure m (SomeMessage st)
-> m (Either failure (SomeMessage st))
forall (m :: * -> *) bytes failure a.
Monad m =>
[bytes] -> DecodeStep bytes failure m a -> m (Either failure a)
runDecoder [bytes]
bytes'
           case Either failure (SomeMessage st)
r of
             Right (SomeMessage Message ps st st'
msg') -> Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> m Bool) -> Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ Message ps st st' -> AnyMessage ps
forall ps (st :: ps) (st' :: ps).
Message ps st st' -> AnyMessage ps
AnyMessage Message ps st st'
msg' AnyMessage ps -> AnyMessage ps -> Bool
forall a. Eq a => a -> a -> Bool
== Message ps st st' -> AnyMessage ps
forall ps (st :: ps) (st' :: ps).
Message ps st st' -> AnyMessage ps
AnyMessage Message ps st st'
msg
             Left failure
_                   -> Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

      | let bytes :: bytes
bytes = PeerHasAgency pr st -> Message ps st st' -> bytes
forall (pr :: PeerRole) (st :: ps) (st' :: ps).
PeerHasAgency pr st -> Message ps st st' -> bytes
encode PeerHasAgency pr st
stok Message ps st st'
msg
      , [bytes]
bytes' <- bytes -> [[bytes]]
splits bytes
bytes ]


-- | Like @'prop_codec_splitsM'@ but run in a pure monad @m@, e.g. @Identity@.
--
prop_codec_splits
  :: forall ps failure m bytes.
     (Monad m, Eq (AnyMessage ps))
  => (bytes -> [[bytes]])
  -> (forall a. m a -> a)
  -> Codec ps failure m bytes
  -> AnyMessageAndAgency ps
  -> Bool
prop_codec_splits :: (bytes -> [[bytes]])
-> (forall a. m a -> a)
-> Codec ps failure m bytes
-> AnyMessageAndAgency ps
-> Bool
prop_codec_splits bytes -> [[bytes]]
splits forall a. m a -> a
runM Codec ps failure m bytes
codec AnyMessageAndAgency ps
msg =
    m Bool -> Bool
forall a. m a -> a
runM (m Bool -> Bool) -> m Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (bytes -> [[bytes]])
-> Codec ps failure m bytes -> AnyMessageAndAgency ps -> m Bool
forall ps failure (m :: * -> *) bytes.
(Monad m, Eq (AnyMessage ps)) =>
(bytes -> [[bytes]])
-> Codec ps failure m bytes -> AnyMessageAndAgency ps -> m Bool
prop_codec_splitsM bytes -> [[bytes]]
splits Codec ps failure m bytes
codec AnyMessageAndAgency ps
msg


-- | Auxiliary definition for 'prop_codec_binary_compatM'.
--
-- Used for the existential @st :: ps@ parameter when expressing that for each
-- value of 'PeerHasAgency' for protocol A, there is a corresponding
-- 'PeerHasAgency' for protocol B of some @st :: ps@.
data SamePeerHasAgency (pr :: PeerRole) (ps :: Type) where
  SamePeerHasAgency
    :: forall (pr :: PeerRole) ps (st :: ps).
       PeerHasAgency pr st
    -> SamePeerHasAgency pr ps

-- | Binary compatibility of two protocols
--
-- We check the following property:
--
-- 1. Using codec A, we encode a message of protocol @psA@ to @bytes@.
--
-- 2. When we decode those @bytes@ using codec B, we get a message of protocol
-- @ps@B.
--
-- 3. When we encode that message again using codec B, we get @bytes@.
--
-- 4. When we decode those @bytes@ using codec A, we get the original message
-- again.
prop_codec_binary_compatM
  :: forall psA psB failure m bytes.
     ( Monad m
     , Eq (AnyMessage psA)
     )
  => Codec psA failure m bytes
  -> Codec psB failure m bytes
  -> (forall pr (stA :: psA). PeerHasAgency pr stA -> SamePeerHasAgency pr psB)
     -- ^ The states of A map directly of states of B.
  -> AnyMessageAndAgency psA
  -> m Bool
prop_codec_binary_compatM :: Codec psA failure m bytes
-> Codec psB failure m bytes
-> (forall (pr :: PeerRole) (stA :: psA).
    PeerHasAgency pr stA -> SamePeerHasAgency pr psB)
-> AnyMessageAndAgency psA
-> m Bool
prop_codec_binary_compatM
    Codec psA failure m bytes
codecA Codec psB failure m bytes
codecB forall (pr :: PeerRole) (stA :: psA).
PeerHasAgency pr stA -> SamePeerHasAgency pr psB
stokEq
    (AnyMessageAndAgency (PeerHasAgency pr st
stokA :: PeerHasAgency pr stA) Message psA st st'
msgA) =
  case PeerHasAgency pr st -> SamePeerHasAgency pr psB
forall (pr :: PeerRole) (stA :: psA).
PeerHasAgency pr stA -> SamePeerHasAgency pr psB
stokEq PeerHasAgency pr st
stokA of
    SamePeerHasAgency PeerHasAgency pr st
stokB -> do
      -- 1.
      let bytesA :: bytes
bytesA = Codec psA failure m bytes
-> PeerHasAgency pr st -> Message psA st st' -> bytes
forall ps failure (m :: * -> *) bytes.
Codec ps failure m bytes
-> forall (pr :: PeerRole) (st :: ps) (st' :: ps).
   PeerHasAgency pr st -> Message ps st st' -> bytes
encode Codec psA failure m bytes
codecA PeerHasAgency pr st
stokA Message psA st st'
msgA
      -- 2.
      Either failure (SomeMessage st)
r1 <- Codec psB failure m bytes
-> PeerHasAgency pr st
-> m (DecodeStep bytes failure m (SomeMessage st))
forall ps failure (m :: * -> *) bytes.
Codec ps failure m bytes
-> forall (pr :: PeerRole) (st :: ps).
   PeerHasAgency pr st
   -> m (DecodeStep bytes failure m (SomeMessage st))
decode Codec psB failure m bytes
codecB PeerHasAgency pr st
stokB m (DecodeStep bytes failure m (SomeMessage st))
-> (DecodeStep bytes failure m (SomeMessage st)
    -> m (Either failure (SomeMessage st)))
-> m (Either failure (SomeMessage st))
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [bytes]
-> DecodeStep bytes failure m (SomeMessage st)
-> m (Either failure (SomeMessage st))
forall (m :: * -> *) bytes failure a.
Monad m =>
[bytes] -> DecodeStep bytes failure m a -> m (Either failure a)
runDecoder [bytes
bytesA]
      case Either failure (SomeMessage st)
r1 of
        Left failure
_     -> Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
        Right (SomeMessage Message psB st st'
msgB) -> do
          -- 3.
          let bytesB :: bytes
bytesB = Codec psB failure m bytes
-> PeerHasAgency pr st -> Message psB st st' -> bytes
forall ps failure (m :: * -> *) bytes.
Codec ps failure m bytes
-> forall (pr :: PeerRole) (st :: ps) (st' :: ps).
   PeerHasAgency pr st -> Message ps st st' -> bytes
encode Codec psB failure m bytes
codecB PeerHasAgency pr st
stokB Message psB st st'
msgB
          -- 4.
          Either failure (SomeMessage st)
r2 <- Codec psA failure m bytes
-> PeerHasAgency pr st
-> m (DecodeStep bytes failure m (SomeMessage st))
forall ps failure (m :: * -> *) bytes.
Codec ps failure m bytes
-> forall (pr :: PeerRole) (st :: ps).
   PeerHasAgency pr st
   -> m (DecodeStep bytes failure m (SomeMessage st))
decode Codec psA failure m bytes
codecA PeerHasAgency pr st
stokA m (DecodeStep bytes failure m (SomeMessage st))
-> (DecodeStep bytes failure m (SomeMessage st)
    -> m (Either failure (SomeMessage st)))
-> m (Either failure (SomeMessage st))
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [bytes]
-> DecodeStep bytes failure m (SomeMessage st)
-> m (Either failure (SomeMessage st))
forall (m :: * -> *) bytes failure a.
Monad m =>
[bytes] -> DecodeStep bytes failure m a -> m (Either failure a)
runDecoder [bytes
bytesB]
          case Either failure (SomeMessage st)
r2 of
            Left failure
_                    -> Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
            Right (SomeMessage Message psA st st'
msgA') -> Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> m Bool) -> Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ Message psA st st' -> AnyMessage psA
forall ps (st :: ps) (st' :: ps).
Message ps st st' -> AnyMessage ps
AnyMessage Message psA st st'
msgA' AnyMessage psA -> AnyMessage psA -> Bool
forall a. Eq a => a -> a -> Bool
== Message psA st st' -> AnyMessage psA
forall ps (st :: ps) (st' :: ps).
Message ps st st' -> AnyMessage ps
AnyMessage Message psA st st'
msgA

-- | Like @'prop_codec_splitsM'@ but run in a pure monad @m@, e.g. @Identity@.
prop_codec_binary_compat
  :: forall psA psB failure m bytes.
     ( Monad m
     , Eq (AnyMessage psA)
     )
  => (forall a. m a -> a)
  -> Codec psA failure m bytes
  -> Codec psB failure m bytes
  -> (forall pr (stA :: psA). PeerHasAgency pr stA -> SamePeerHasAgency pr psB)
  -> AnyMessageAndAgency psA
  -> Bool
prop_codec_binary_compat :: (forall a. m a -> a)
-> Codec psA failure m bytes
-> Codec psB failure m bytes
-> (forall (pr :: PeerRole) (stA :: psA).
    PeerHasAgency pr stA -> SamePeerHasAgency pr psB)
-> AnyMessageAndAgency psA
-> Bool
prop_codec_binary_compat forall a. m a -> a
runM Codec psA failure m bytes
codecA Codec psB failure m bytes
codecB forall (pr :: PeerRole) (stA :: psA).
PeerHasAgency pr stA -> SamePeerHasAgency pr psB
stokEq AnyMessageAndAgency psA
msgA =
     m Bool -> Bool
forall a. m a -> a
runM (m Bool -> Bool) -> m Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Codec psA failure m bytes
-> Codec psB failure m bytes
-> (forall (pr :: PeerRole) (stA :: psA).
    PeerHasAgency pr stA -> SamePeerHasAgency pr psB)
-> AnyMessageAndAgency psA
-> m Bool
forall psA psB failure (m :: * -> *) bytes.
(Monad m, Eq (AnyMessage psA)) =>
Codec psA failure m bytes
-> Codec psB failure m bytes
-> (forall (pr :: PeerRole) (stA :: psA).
    PeerHasAgency pr stA -> SamePeerHasAgency pr psB)
-> AnyMessageAndAgency psA
-> m Bool
prop_codec_binary_compatM Codec psA failure m bytes
codecA Codec psB failure m bytes
codecB forall (pr :: PeerRole) (stA :: psA).
PeerHasAgency pr stA -> SamePeerHasAgency pr psB
stokEq AnyMessageAndAgency psA
msgA


-- | Compatibility between two codecs of the same protocol.  Encode a message
-- with one codec and decode it with the other one, then compare if the result
-- is the same as initial message.
--
prop_codecs_compatM
  :: forall ps failure m bytes.
     ( Monad m
     , Eq (AnyMessage ps)
     , forall a. Monoid a => Monoid (m a)
     )
  => Codec ps failure m bytes
  -> Codec ps failure m bytes
  -> AnyMessageAndAgency ps
  -> m Bool
prop_codecs_compatM :: Codec ps failure m bytes
-> Codec ps failure m bytes -> AnyMessageAndAgency ps -> m Bool
prop_codecs_compatM Codec ps failure m bytes
codecA Codec ps failure m bytes
codecB
                    (AnyMessageAndAgency PeerHasAgency pr st
stok Message ps st st'
msg) =
    All -> Bool
getAll (All -> Bool) -> m All -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do Either failure (SomeMessage st)
r <- Codec ps failure m bytes
-> PeerHasAgency pr st
-> m (DecodeStep bytes failure m (SomeMessage st))
forall ps failure (m :: * -> *) bytes.
Codec ps failure m bytes
-> forall (pr :: PeerRole) (st :: ps).
   PeerHasAgency pr st
   -> m (DecodeStep bytes failure m (SomeMessage st))
decode Codec ps failure m bytes
codecB PeerHasAgency pr st
stok m (DecodeStep bytes failure m (SomeMessage st))
-> (DecodeStep bytes failure m (SomeMessage st)
    -> m (Either failure (SomeMessage st)))
-> m (Either failure (SomeMessage st))
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [bytes]
-> DecodeStep bytes failure m (SomeMessage st)
-> m (Either failure (SomeMessage st))
forall (m :: * -> *) bytes failure a.
Monad m =>
[bytes] -> DecodeStep bytes failure m a -> m (Either failure a)
runDecoder [Codec ps failure m bytes
-> PeerHasAgency pr st -> Message ps st st' -> bytes
forall ps failure (m :: * -> *) bytes.
Codec ps failure m bytes
-> forall (pr :: PeerRole) (st :: ps) (st' :: ps).
   PeerHasAgency pr st -> Message ps st st' -> bytes
encode Codec ps failure m bytes
codecA PeerHasAgency pr st
stok Message ps st st'
msg]
                  case Either failure (SomeMessage st)
r of
                    Right (SomeMessage Message ps st st'
msg') -> All -> m All
forall (m :: * -> *) a. Monad m => a -> m a
return (All -> m All) -> All -> m All
forall a b. (a -> b) -> a -> b
$ Bool -> All
All (Bool -> All) -> Bool -> All
forall a b. (a -> b) -> a -> b
$ Message ps st st' -> AnyMessage ps
forall ps (st :: ps) (st' :: ps).
Message ps st st' -> AnyMessage ps
AnyMessage Message ps st st'
msg' AnyMessage ps -> AnyMessage ps -> Bool
forall a. Eq a => a -> a -> Bool
== Message ps st st' -> AnyMessage ps
forall ps (st :: ps) (st' :: ps).
Message ps st st' -> AnyMessage ps
AnyMessage Message ps st st'
msg
                    Left failure
_                   -> All -> m All
forall (m :: * -> *) a. Monad m => a -> m a
return (All -> m All) -> All -> m All
forall a b. (a -> b) -> a -> b
$ Bool -> All
All Bool
False
            m All -> m All -> m All
forall a. Semigroup a => a -> a -> a
<> do Either failure (SomeMessage st)
r <- Codec ps failure m bytes
-> PeerHasAgency pr st
-> m (DecodeStep bytes failure m (SomeMessage st))
forall ps failure (m :: * -> *) bytes.
Codec ps failure m bytes
-> forall (pr :: PeerRole) (st :: ps).
   PeerHasAgency pr st
   -> m (DecodeStep bytes failure m (SomeMessage st))
decode Codec ps failure m bytes
codecA PeerHasAgency pr st
stok m (DecodeStep bytes failure m (SomeMessage st))
-> (DecodeStep bytes failure m (SomeMessage st)
    -> m (Either failure (SomeMessage st)))
-> m (Either failure (SomeMessage st))
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [bytes]
-> DecodeStep bytes failure m (SomeMessage st)
-> m (Either failure (SomeMessage st))
forall (m :: * -> *) bytes failure a.
Monad m =>
[bytes] -> DecodeStep bytes failure m a -> m (Either failure a)
runDecoder [Codec ps failure m bytes
-> PeerHasAgency pr st -> Message ps st st' -> bytes
forall ps failure (m :: * -> *) bytes.
Codec ps failure m bytes
-> forall (pr :: PeerRole) (st :: ps) (st' :: ps).
   PeerHasAgency pr st -> Message ps st st' -> bytes
encode Codec ps failure m bytes
codecB PeerHasAgency pr st
stok Message ps st st'
msg]
                  case Either failure (SomeMessage st)
r of
                    Right (SomeMessage Message ps st st'
msg') -> All -> m All
forall (m :: * -> *) a. Monad m => a -> m a
return (All -> m All) -> All -> m All
forall a b. (a -> b) -> a -> b
$ Bool -> All
All (Bool -> All) -> Bool -> All
forall a b. (a -> b) -> a -> b
$ Message ps st st' -> AnyMessage ps
forall ps (st :: ps) (st' :: ps).
Message ps st st' -> AnyMessage ps
AnyMessage Message ps st st'
msg' AnyMessage ps -> AnyMessage ps -> Bool
forall a. Eq a => a -> a -> Bool
== Message ps st st' -> AnyMessage ps
forall ps (st :: ps) (st' :: ps).
Message ps st st' -> AnyMessage ps
AnyMessage Message ps st st'
msg
                    Left failure
_                   -> All -> m All
forall (m :: * -> *) a. Monad m => a -> m a
return (All -> m All) -> All -> m All
forall a b. (a -> b) -> a -> b
$ Bool -> All
All Bool
False

-- | Like @'prop_codecs_compatM'@ but run in a pure monad @m@, e.g. @Identity@.
--
prop_codecs_compat
  :: forall ps failure m bytes.
     ( Monad m
     , Eq (AnyMessage ps)
     , forall a. Monoid a => Monoid (m a)
     )
  => (forall a. m a -> a)
  -> Codec ps failure m bytes
  -> Codec ps failure m bytes
  -> AnyMessageAndAgency ps
  -> Bool
prop_codecs_compat :: (forall a. m a -> a)
-> Codec ps failure m bytes
-> Codec ps failure m bytes
-> AnyMessageAndAgency ps
-> Bool
prop_codecs_compat forall a. m a -> a
run Codec ps failure m bytes
codecA Codec ps failure m bytes
codecB AnyMessageAndAgency ps
msg =
    m Bool -> Bool
forall a. m a -> a
run (m Bool -> Bool) -> m Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Codec ps failure m bytes
-> Codec ps failure m bytes -> AnyMessageAndAgency ps -> m Bool
forall ps failure (m :: * -> *) bytes.
(Monad m, Eq (AnyMessage ps),
 forall a. Monoid a => Monoid (m a)) =>
Codec ps failure m bytes
-> Codec ps failure m bytes -> AnyMessageAndAgency ps -> m Bool
prop_codecs_compatM Codec ps failure m bytes
codecA Codec ps failure m bytes
codecB AnyMessageAndAgency ps
msg