{-# LANGUAGE DataKinds                #-}
{-# LANGUAGE FlexibleContexts         #-}
{-# LANGUAGE FlexibleInstances        #-}
{-# LANGUAGE GADTs                    #-}
{-# LANGUAGE NamedFieldPuns           #-}
{-# LANGUAGE PatternSynonyms          #-}
{-# LANGUAGE PolyKinds                #-}
{-# LANGUAGE QuantifiedConstraints    #-}
{-# LANGUAGE RankNTypes               #-}
{-# LANGUAGE ScopedTypeVariables      #-}
{-# LANGUAGE TypeFamilies             #-}
{-# LANGUAGE ViewPatterns             #-}
-- @UndecidableInstances@ extension is required for defining @Show@ instance of
-- @'AnyMessage'@ and @'AnyMessage'@.
{-# LANGUAGE UndecidableInstances     #-}
{-# OPTIONS_GHC -Wno-dodgy-imports #-}

-- | Stateful codec.  This module is intended to be imported qualified.
--
module Network.TypedProtocol.Stateful.Codec
  ( -- * Defining and using Codecs
    Codec (..)
  , hoistCodec
  , isoCodec
  , mapFailureCodec
  , liftCodec
    -- ** Incremental decoding
  , DecodeStep (..)
  , runDecoder
  , runDecoderPure
    -- ** Related types
    -- *** SomeMessage
  , SomeMessage (..)
    -- *** StateToken 
  , StateToken
  , StateTokenI (..)
    -- *** ActiveState
  , ActiveState
    -- *** PeerRole
  , PeerRole (..)
    -- * CodecFailure
  , CodecFailure (..)
    -- * Testing codec properties
  , AnyMessage (.., AnyMessageAndAgency)
  , showAnyMessage
  , prop_codecM
  , prop_codec
  , prop_codec_splitsM
  , prop_codec_splits
  , prop_codecs_compatM
  , prop_codecs_compat
  ) where

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

import           Network.TypedProtocol.Core
import           Network.TypedProtocol.Codec (CodecFailure (..),
                   DecodeStep (..),  SomeMessage (..), hoistDecodeStep,
                   isoDecodeStep, mapFailureDecodeStep, runDecoder,
                   runDecoderPure)
import qualified Network.TypedProtocol.Codec as TP hiding (AnyMessageAndAgency)


-- | A stateful codec.
--
data Codec ps failure (f :: ps -> Type) m bytes = Codec {
       forall ps failure (f :: ps -> *) (m :: * -> *) bytes.
Codec ps failure f m bytes
-> forall (st :: ps) (st' :: ps).
   (StateTokenI st, ActiveState st) =>
   f st -> Message ps st st' -> bytes
encode :: forall (st :: ps) (st' :: ps).
                 StateTokenI st
              => ActiveState st
              => f st
              -- local state, which contain extra context for the encoding
              -- process.
              --
              -- TODO: input-output-hk/typed-protocols#57
              -> Message ps st st'
              -- message to be encoded
              -> bytes,

       forall ps failure (f :: ps -> *) (m :: * -> *) bytes.
Codec ps failure f m bytes
-> forall (st :: ps).
   ActiveState st =>
   StateToken st
   -> f st -> m (DecodeStep bytes failure m (SomeMessage st))
decode :: forall (st :: ps).
                 ActiveState st
              => StateToken st
              -> f st
              -- local state, which can contain extra context from the
              -- previous message.
              --
              -- TODO: input-output-hk/typed-protocols#57
              -> m (DecodeStep bytes failure m (SomeMessage st))
     }

liftCodec :: TP.Codec ps failure m bytes -> Codec ps failure f m bytes
liftCodec :: forall ps failure (m :: * -> *) bytes (f :: ps -> *).
Codec ps failure m bytes -> Codec ps failure f m bytes
liftCodec Codec ps failure m bytes
codec = Codec { encode :: forall (st :: ps) (st' :: ps).
(StateTokenI st, ActiveState st) =>
f st -> Message ps st st' -> bytes
encode = \f st
_ Message ps st st'
msg -> Codec ps failure m bytes
-> forall (st :: ps) (st' :: ps).
   (StateTokenI st, ActiveState st) =>
   Message ps st st' -> bytes
forall ps failure (m :: * -> *) bytes.
Codec ps failure m bytes
-> forall (st :: ps) (st' :: ps).
   (StateTokenI st, ActiveState st) =>
   Message ps st st' -> bytes
TP.encode Codec ps failure m bytes
codec Message ps st st'
msg
                        , decode :: forall (st :: ps).
ActiveState st =>
StateToken st
-> f st -> m (DecodeStep bytes failure m (SomeMessage st))
decode = \StateToken st
stok f st
_ -> Codec ps failure m bytes
-> forall (st :: ps).
   ActiveState st =>
   StateToken st -> m (DecodeStep bytes failure m (SomeMessage st))
forall ps failure (m :: * -> *) bytes.
Codec ps failure m bytes
-> forall (st :: ps).
   ActiveState st =>
   StateToken st -> m (DecodeStep bytes failure m (SomeMessage st))
TP.decode Codec ps failure m bytes
codec StateToken st
stok
                        }

hoistCodec
  :: ( Functor n )
  => (forall x . m x -> n x)
  -> Codec ps failure f m bytes
  -> Codec ps failure f n bytes
hoistCodec :: forall (n :: * -> *) (m :: * -> *) ps failure (f :: ps -> *) bytes.
Functor n =>
(forall x. m x -> n x)
-> Codec ps failure f m bytes -> Codec ps failure f n bytes
hoistCodec forall x. m x -> n x
nat Codec ps failure f m bytes
codec = Codec ps failure f m bytes
codec
  { decode = \StateToken st
stok f st
f -> (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 a b. (a -> b) -> n a -> n b
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 m x -> n x
forall x. m x -> n x
nat) (n (DecodeStep bytes failure m (SomeMessage st))
 -> n (DecodeStep bytes failure n (SomeMessage st)))
-> (m (DecodeStep bytes failure m (SomeMessage st))
    -> n (DecodeStep bytes failure m (SomeMessage st)))
-> m (DecodeStep bytes failure m (SomeMessage 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 n (SomeMessage st)))
-> m (DecodeStep bytes failure m (SomeMessage st))
-> n (DecodeStep bytes failure n (SomeMessage st))
forall a b. (a -> b) -> a -> b
$ Codec ps failure f m bytes
-> forall (st :: ps).
   ActiveState st =>
   StateToken st
   -> f st -> m (DecodeStep bytes failure m (SomeMessage st))
forall ps failure (f :: ps -> *) (m :: * -> *) bytes.
Codec ps failure f m bytes
-> forall (st :: ps).
   ActiveState st =>
   StateToken st
   -> f st -> m (DecodeStep bytes failure m (SomeMessage st))
decode Codec ps failure f m bytes
codec StateToken st
stok f st
f
  }

isoCodec :: Functor m
         => (bytes -> bytes')
         -> (bytes' -> bytes)
         -> Codec ps failure f m bytes
         -> Codec ps failure f m bytes'
isoCodec :: forall (m :: * -> *) bytes bytes' ps failure (f :: ps -> *).
Functor m =>
(bytes -> bytes')
-> (bytes' -> bytes)
-> Codec ps failure f m bytes
-> Codec ps failure f m bytes'
isoCodec bytes -> bytes'
g bytes' -> bytes
finv Codec {forall (st :: ps) (st' :: ps).
(StateTokenI st, ActiveState st) =>
f st -> Message ps st st' -> bytes
encode :: forall ps failure (f :: ps -> *) (m :: * -> *) bytes.
Codec ps failure f m bytes
-> forall (st :: ps) (st' :: ps).
   (StateTokenI st, ActiveState st) =>
   f st -> Message ps st st' -> bytes
encode :: forall (st :: ps) (st' :: ps).
(StateTokenI st, ActiveState st) =>
f st -> Message ps st st' -> bytes
encode, forall (st :: ps).
ActiveState st =>
StateToken st
-> f st -> m (DecodeStep bytes failure m (SomeMessage st))
decode :: forall ps failure (f :: ps -> *) (m :: * -> *) bytes.
Codec ps failure f m bytes
-> forall (st :: ps).
   ActiveState st =>
   StateToken st
   -> f st -> m (DecodeStep bytes failure m (SomeMessage st))
decode :: forall (st :: ps).
ActiveState st =>
StateToken st
-> f st -> m (DecodeStep bytes failure m (SomeMessage st))
decode} = Codec {
      encode :: forall (st :: ps) (st' :: ps).
(StateTokenI st, ActiveState st) =>
f st -> Message ps st st' -> bytes'
encode = \f st
f Message ps st st'
msg -> bytes -> bytes'
g (bytes -> bytes') -> bytes -> bytes'
forall a b. (a -> b) -> a -> b
$ f st -> Message ps st st' -> bytes
forall (st :: ps) (st' :: ps).
(StateTokenI st, ActiveState st) =>
f st -> Message ps st st' -> bytes
encode f st
f Message ps st st'
msg,
      decode :: forall (st :: ps).
ActiveState st =>
StateToken st
-> f st -> m (DecodeStep bytes' failure m (SomeMessage st))
decode = \StateToken st
stok f st
f -> (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'
g 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
<$> StateToken st
-> f st -> m (DecodeStep bytes failure m (SomeMessage st))
forall (st :: ps).
ActiveState st =>
StateToken st
-> f st -> m (DecodeStep bytes failure m (SomeMessage st))
decode StateToken st
stok f st
f
    }

mapFailureCodec
  :: Functor m
  => (failure -> failure')
  -> Codec ps failure  f m bytes
  -> Codec ps failure' f m bytes
mapFailureCodec :: forall (m :: * -> *) failure failure' ps (f :: ps -> *) bytes.
Functor m =>
(failure -> failure')
-> Codec ps failure f m bytes -> Codec ps failure' f m bytes
mapFailureCodec failure -> failure'
g Codec {forall (st :: ps) (st' :: ps).
(StateTokenI st, ActiveState st) =>
f st -> Message ps st st' -> bytes
encode :: forall ps failure (f :: ps -> *) (m :: * -> *) bytes.
Codec ps failure f m bytes
-> forall (st :: ps) (st' :: ps).
   (StateTokenI st, ActiveState st) =>
   f st -> Message ps st st' -> bytes
encode :: forall (st :: ps) (st' :: ps).
(StateTokenI st, ActiveState st) =>
f st -> Message ps st st' -> bytes
encode, forall (st :: ps).
ActiveState st =>
StateToken st
-> f st -> m (DecodeStep bytes failure m (SomeMessage st))
decode :: forall ps failure (f :: ps -> *) (m :: * -> *) bytes.
Codec ps failure f m bytes
-> forall (st :: ps).
   ActiveState st =>
   StateToken st
   -> f st -> m (DecodeStep bytes failure m (SomeMessage st))
decode :: forall (st :: ps).
ActiveState st =>
StateToken st
-> f st -> m (DecodeStep bytes failure m (SomeMessage st))
decode} = Codec {
    encode :: forall (st :: ps) (st' :: ps).
(StateTokenI st, ActiveState st) =>
f st -> Message ps st st' -> bytes
encode = f st -> Message ps st st' -> bytes
forall (st :: ps) (st' :: ps).
(StateTokenI st, ActiveState st) =>
f st -> Message ps st st' -> bytes
encode,
    decode :: forall (st :: ps).
ActiveState st =>
StateToken st
-> f st -> m (DecodeStep bytes failure' m (SomeMessage st))
decode = \StateToken st
stok f st
f -> (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'
g (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
<$> StateToken st
-> f st -> m (DecodeStep bytes failure m (SomeMessage st))
forall (st :: ps).
ActiveState st =>
StateToken st
-> f st -> m (DecodeStep bytes failure m (SomeMessage st))
decode StateToken st
stok f st
f
  }


--
-- Codec properties
--

-- | Any message for a protocol, with a 'StateTokenI' constraint which gives access
-- to protocol state.
--
-- Used where we don't know statically what the state type is, but need the
-- agency and message to match each other.
--
data AnyMessage ps (f :: ps -> Type) where
  AnyMessage :: forall ps f (st :: ps) (st' :: ps).
                ( StateTokenI st
                , ActiveState st
                )
             => f st
             -- ^ local state
             -> Message ps (st :: ps) (st' :: ps)
             -- ^ protocol messsage
             -> AnyMessage ps f


-- | `showAnyMessage` is can be used to provide `Show` instance for
-- `AnyMessage` if showing `Message` is independent of the state or one accepts
-- showing only partial information included in message constructors or accepts
-- message constructors to carry `Show` instances for its arguments.  Note that
-- the proper solution is to define a custom `Show (AnyMessage ps f)` instance
-- for a protocol `ps`, which give access to the state functor `f` in scope of
-- `show`.
--
showAnyMessage :: forall ps f.
                  ( forall st st'. Show (Message ps st st')
                  , forall st. Show (f st)
                  )
               => AnyMessage ps f
               -> String
showAnyMessage :: forall ps (f :: ps -> *).
(forall (st :: ps) (st' :: ps). Show (Message ps st st'),
 forall (st :: ps). Show (f st)) =>
AnyMessage ps f -> String
showAnyMessage (AnyMessage f st
st Message ps st st'
msg) =
    [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ String
"AnyMessage "
           , f st -> String
forall a. Show a => a -> String
show f st
st
           , String
" "
           , Message ps st st' -> String
forall a. Show a => a -> String
show Message ps st st'
msg
           ]


-- | A convenient pattern synonym which unwrap 'AnyMessage' giving both the
-- singleton for the state and the message.
--
pattern AnyMessageAndAgency :: forall ps f. ()
                            => forall (st :: ps) (st' :: ps).
                               (StateTokenI st, ActiveState st)
                            => StateToken st
                            -> f st
                            -> Message ps st st'
                            -> AnyMessage ps f
pattern $bAnyMessageAndAgency :: forall ps (f :: ps -> *) (st :: ps) (st' :: ps).
(StateTokenI st, ActiveState st) =>
StateToken st -> f st -> Message ps st st' -> AnyMessage ps f
$mAnyMessageAndAgency :: forall {r} {ps} {f :: ps -> *}.
AnyMessage ps f
-> (forall {st :: ps} {st' :: ps}.
    (StateTokenI st, ActiveState st) =>
    StateToken st -> f st -> Message ps st st' -> r)
-> ((# #) -> r)
-> r
AnyMessageAndAgency stateToken f msg <- AnyMessage f (getAgency -> (msg, stateToken))
  where
    AnyMessageAndAgency StateToken st
_ f st
msg = f st -> Message ps st st' -> AnyMessage ps f
forall ps (f :: ps -> *) (st :: ps) (st' :: ps).
(StateTokenI st, ActiveState st) =>
f st -> Message ps st st' -> AnyMessage ps f
AnyMessage f st
msg
{-# COMPLETE AnyMessageAndAgency #-}

-- | Internal view pattern for 'AnyMessageAndAgency'
--
getAgency :: StateTokenI st => Message ps st st' -> (Message ps st st', StateToken st)
getAgency :: forall ps (st :: ps) (st' :: ps).
StateTokenI st =>
Message ps st st' -> (Message ps st st', StateToken st)
getAgency Message ps st st'
msg = (Message ps st st'
msg, StateToken st
forall {ps} (st :: ps). StateTokenI st => StateToken st
stateToken)


-- | The 'Codec' round-trip property: decode after encode gives the same
-- message. Every codec must satisfy this property.
--
prop_codecM
  :: forall ps failure f m bytes.
     ( Monad m
     , Eq (AnyMessage ps f)
     )
  => Codec ps failure f m bytes
  -> AnyMessage ps f
  -> m Bool
prop_codecM :: forall ps failure (f :: ps -> *) (m :: * -> *) bytes.
(Monad m, Eq (AnyMessage ps f)) =>
Codec ps failure f m bytes -> AnyMessage ps f -> m Bool
prop_codecM Codec {forall (st :: ps) (st' :: ps).
(StateTokenI st, ActiveState st) =>
f st -> Message ps st st' -> bytes
encode :: forall ps failure (f :: ps -> *) (m :: * -> *) bytes.
Codec ps failure f m bytes
-> forall (st :: ps) (st' :: ps).
   (StateTokenI st, ActiveState st) =>
   f st -> Message ps st st' -> bytes
encode :: forall (st :: ps) (st' :: ps).
(StateTokenI st, ActiveState st) =>
f st -> Message ps st st' -> bytes
encode, forall (st :: ps).
ActiveState st =>
StateToken st
-> f st -> m (DecodeStep bytes failure m (SomeMessage st))
decode :: forall ps failure (f :: ps -> *) (m :: * -> *) bytes.
Codec ps failure f m bytes
-> forall (st :: ps).
   ActiveState st =>
   StateToken st
   -> f st -> m (DecodeStep bytes failure m (SomeMessage st))
decode :: forall (st :: ps).
ActiveState st =>
StateToken st
-> f st -> m (DecodeStep bytes failure m (SomeMessage st))
decode} a :: AnyMessage ps f
a@(AnyMessage f st
f (Message ps st st'
msg :: Message ps st st')) = do
    r <- StateToken st
-> f st -> m (DecodeStep bytes failure m (SomeMessage st))
forall (st :: ps).
ActiveState st =>
StateToken st
-> f st -> m (DecodeStep bytes failure m (SomeMessage st))
decode (StateToken st
forall {ps} (st :: ps). StateTokenI st => StateToken st
stateToken :: StateToken st) f st
f m (DecodeStep bytes failure m (SomeMessage st))
-> (DecodeStep bytes failure m (SomeMessage st)
    -> m (Either failure (SomeMessage st)))
-> m (Either failure (SomeMessage st))
forall a b. m a -> (a -> m b) -> m b
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 [f st -> Message ps st st' -> bytes
forall (st :: ps) (st' :: ps).
(StateTokenI st, ActiveState st) =>
f st -> Message ps st st' -> bytes
encode f st
f Message ps st st'
msg]
    case r :: Either failure (SomeMessage st) of
      Right (SomeMessage Message ps st st'
msg') -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> m Bool) -> Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ f st -> Message ps st st' -> AnyMessage ps f
forall ps (f :: ps -> *) (st :: ps) (st' :: ps).
(StateTokenI st, ActiveState st) =>
f st -> Message ps st st' -> AnyMessage ps f
AnyMessage f st
f Message ps st st'
msg' AnyMessage ps f -> AnyMessage ps f -> Bool
forall a. Eq a => a -> a -> Bool
== AnyMessage ps f
a
      Left failure
_                   -> Bool -> m Bool
forall a. a -> m a
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 f m bytes.
     (Monad m, Eq (AnyMessage ps f))
  => (forall a. m a -> a)
  -> Codec ps failure f m bytes
  -> AnyMessage ps f
  -> Bool
prop_codec :: forall ps failure (f :: ps -> *) (m :: * -> *) bytes.
(Monad m, Eq (AnyMessage ps f)) =>
(forall a. m a -> a)
-> Codec ps failure f m bytes -> AnyMessage ps f -> Bool
prop_codec forall a. m a -> a
runM Codec ps failure f m bytes
codec AnyMessage ps f
msg =
    m Bool -> Bool
forall a. m a -> a
runM (Codec ps failure f m bytes -> AnyMessage ps f -> m Bool
forall ps failure (f :: ps -> *) (m :: * -> *) bytes.
(Monad m, Eq (AnyMessage ps f)) =>
Codec ps failure f m bytes -> AnyMessage ps f -> m Bool
prop_codecM Codec ps failure f m bytes
codec AnyMessage ps f
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 f m bytes.
     (Monad m, Eq (AnyMessage ps f))
  => (bytes -> [[bytes]])   -- ^ alternative re-chunkings of serialised form
  -> Codec ps failure f m bytes
  -> AnyMessage ps f
  -> m Bool
prop_codec_splitsM :: forall ps failure (f :: ps -> *) (m :: * -> *) bytes.
(Monad m, Eq (AnyMessage ps f)) =>
(bytes -> [[bytes]])
-> Codec ps failure f m bytes -> AnyMessage ps f -> m Bool
prop_codec_splitsM bytes -> [[bytes]]
splits
                   Codec {forall (st :: ps) (st' :: ps).
(StateTokenI st, ActiveState st) =>
f st -> Message ps st st' -> bytes
encode :: forall ps failure (f :: ps -> *) (m :: * -> *) bytes.
Codec ps failure f m bytes
-> forall (st :: ps) (st' :: ps).
   (StateTokenI st, ActiveState st) =>
   f st -> Message ps st st' -> bytes
encode :: forall (st :: ps) (st' :: ps).
(StateTokenI st, ActiveState st) =>
f st -> Message ps st st' -> bytes
encode, forall (st :: ps).
ActiveState st =>
StateToken st
-> f st -> m (DecodeStep bytes failure m (SomeMessage st))
decode :: forall ps failure (f :: ps -> *) (m :: * -> *) bytes.
Codec ps failure f m bytes
-> forall (st :: ps).
   ActiveState st =>
   StateToken st
   -> f st -> m (DecodeStep bytes failure m (SomeMessage st))
decode :: forall (st :: ps).
ActiveState st =>
StateToken st
-> f st -> m (DecodeStep bytes failure m (SomeMessage st))
decode} a :: AnyMessage ps f
a@(AnyMessage f st
f (Message ps st st'
msg :: Message ps st st')) = 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)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence
      [ do r <- StateToken st
-> f st -> m (DecodeStep bytes failure m (SomeMessage st))
forall (st :: ps).
ActiveState st =>
StateToken st
-> f st -> m (DecodeStep bytes failure m (SomeMessage st))
decode (StateToken st
forall {ps} (st :: ps). StateTokenI st => StateToken st
stateToken :: StateToken st) f st
f m (DecodeStep bytes failure m (SomeMessage st))
-> (DecodeStep bytes failure m (SomeMessage st)
    -> m (Either failure (SomeMessage st)))
-> m (Either failure (SomeMessage st))
forall a b. m a -> (a -> m b) -> m b
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 r :: Either failure (SomeMessage st) of
             Right (SomeMessage Message ps st st'
msg') -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> m Bool) -> Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ f st -> Message ps st st' -> AnyMessage ps f
forall ps (f :: ps -> *) (st :: ps) (st' :: ps).
(StateTokenI st, ActiveState st) =>
f st -> Message ps st st' -> AnyMessage ps f
AnyMessage f st
f Message ps st st'
msg' AnyMessage ps f -> AnyMessage ps f -> Bool
forall a. Eq a => a -> a -> Bool
== AnyMessage ps f
a
             Left failure
_                   -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

      | let bytes :: bytes
bytes = f st -> Message ps st st' -> bytes
forall (st :: ps) (st' :: ps).
(StateTokenI st, ActiveState st) =>
f st -> Message ps st st' -> bytes
encode f st
f 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 f m bytes.
     (Monad m, Eq (AnyMessage ps f))
  => (bytes -> [[bytes]])
  -> (forall a. m a -> a)
  -> Codec ps failure f m bytes
  -> AnyMessage ps f
  -> Bool
prop_codec_splits :: forall ps failure (f :: ps -> *) (m :: * -> *) bytes.
(Monad m, Eq (AnyMessage ps f)) =>
(bytes -> [[bytes]])
-> (forall a. m a -> a)
-> Codec ps failure f m bytes
-> AnyMessage ps f
-> Bool
prop_codec_splits bytes -> [[bytes]]
splits forall a. m a -> a
runM Codec ps failure f m bytes
codec AnyMessage ps f
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 f m bytes -> AnyMessage ps f -> m Bool
forall ps failure (f :: ps -> *) (m :: * -> *) bytes.
(Monad m, Eq (AnyMessage ps f)) =>
(bytes -> [[bytes]])
-> Codec ps failure f m bytes -> AnyMessage ps f -> m Bool
prop_codec_splitsM bytes -> [[bytes]]
splits Codec ps failure f m bytes
codec AnyMessage ps f
msg


-- | 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 f m bytes.
     ( Monad m
     , Eq (AnyMessage ps f)
     , forall a. Monoid a => Monoid (m a)
     )
  => Codec ps failure f m bytes
  -> Codec ps failure f m bytes
  -> AnyMessage ps f
  -> m Bool
prop_codecs_compatM :: forall ps failure (f :: ps -> *) (m :: * -> *) bytes.
(Monad m, Eq (AnyMessage ps f),
 forall a. Monoid a => Monoid (m a)) =>
Codec ps failure f m bytes
-> Codec ps failure f m bytes -> AnyMessage ps f -> m Bool
prop_codecs_compatM Codec ps failure f m bytes
codecA Codec ps failure f m bytes
codecB
                    a :: AnyMessage ps f
a@(AnyMessage f st
f (Message ps st st'
msg :: Message ps st st')) =
    All -> Bool
getAll (All -> Bool) -> m All -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do r <- Codec ps failure f m bytes
-> forall (st :: ps).
   ActiveState st =>
   StateToken st
   -> f st -> m (DecodeStep bytes failure m (SomeMessage st))
forall ps failure (f :: ps -> *) (m :: * -> *) bytes.
Codec ps failure f m bytes
-> forall (st :: ps).
   ActiveState st =>
   StateToken st
   -> f st -> m (DecodeStep bytes failure m (SomeMessage st))
decode Codec ps failure f m bytes
codecB (StateToken st
forall {ps} (st :: ps). StateTokenI st => StateToken st
stateToken :: StateToken st) f st
f m (DecodeStep bytes failure m (SomeMessage st))
-> (DecodeStep bytes failure m (SomeMessage st)
    -> m (Either failure (SomeMessage st)))
-> m (Either failure (SomeMessage st))
forall a b. m a -> (a -> m b) -> m b
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 f m bytes
-> forall (st :: ps) (st' :: ps).
   (StateTokenI st, ActiveState st) =>
   f st -> Message ps st st' -> bytes
forall ps failure (f :: ps -> *) (m :: * -> *) bytes.
Codec ps failure f m bytes
-> forall (st :: ps) (st' :: ps).
   (StateTokenI st, ActiveState st) =>
   f st -> Message ps st st' -> bytes
encode Codec ps failure f m bytes
codecA f st
f Message ps st st'
msg]
                  case r :: Either failure (SomeMessage st) of
                    Right (SomeMessage Message ps st st'
msg') -> All -> m All
forall a. a -> m a
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
$ f st -> Message ps st st' -> AnyMessage ps f
forall ps (f :: ps -> *) (st :: ps) (st' :: ps).
(StateTokenI st, ActiveState st) =>
f st -> Message ps st st' -> AnyMessage ps f
AnyMessage f st
f Message ps st st'
msg' AnyMessage ps f -> AnyMessage ps f -> Bool
forall a. Eq a => a -> a -> Bool
== AnyMessage ps f
a
                    Left failure
_                   -> All -> m All
forall a. a -> m a
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 r <- Codec ps failure f m bytes
-> forall (st :: ps).
   ActiveState st =>
   StateToken st
   -> f st -> m (DecodeStep bytes failure m (SomeMessage st))
forall ps failure (f :: ps -> *) (m :: * -> *) bytes.
Codec ps failure f m bytes
-> forall (st :: ps).
   ActiveState st =>
   StateToken st
   -> f st -> m (DecodeStep bytes failure m (SomeMessage st))
decode Codec ps failure f m bytes
codecA (StateToken st
forall {ps} (st :: ps). StateTokenI st => StateToken st
stateToken :: StateToken st) f st
f m (DecodeStep bytes failure m (SomeMessage st))
-> (DecodeStep bytes failure m (SomeMessage st)
    -> m (Either failure (SomeMessage st)))
-> m (Either failure (SomeMessage st))
forall a b. m a -> (a -> m b) -> m b
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 f m bytes
-> forall (st :: ps) (st' :: ps).
   (StateTokenI st, ActiveState st) =>
   f st -> Message ps st st' -> bytes
forall ps failure (f :: ps -> *) (m :: * -> *) bytes.
Codec ps failure f m bytes
-> forall (st :: ps) (st' :: ps).
   (StateTokenI st, ActiveState st) =>
   f st -> Message ps st st' -> bytes
encode Codec ps failure f m bytes
codecB f st
f Message ps st st'
msg]
                  case r :: Either failure (SomeMessage st) of
                    Right (SomeMessage Message ps st st'
msg') -> All -> m All
forall a. a -> m a
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
$ f st -> Message ps st st' -> AnyMessage ps f
forall ps (f :: ps -> *) (st :: ps) (st' :: ps).
(StateTokenI st, ActiveState st) =>
f st -> Message ps st st' -> AnyMessage ps f
AnyMessage f st
f Message ps st st'
msg' AnyMessage ps f -> AnyMessage ps f -> Bool
forall a. Eq a => a -> a -> Bool
== AnyMessage ps f
a
                    Left failure
_                   -> All -> m All
forall a. a -> m a
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 f m bytes.
     ( Monad m
     , Eq (AnyMessage ps f)
     , forall a. Monoid a => Monoid (m a)
     )
  => (forall a. m a -> a)
  -> Codec ps failure f m bytes
  -> Codec ps failure f m bytes
  -> AnyMessage ps f
  -> Bool
prop_codecs_compat :: forall ps failure (f :: ps -> *) (m :: * -> *) bytes.
(Monad m, Eq (AnyMessage ps f),
 forall a. Monoid a => Monoid (m a)) =>
(forall a. m a -> a)
-> Codec ps failure f m bytes
-> Codec ps failure f m bytes
-> AnyMessage ps f
-> Bool
prop_codecs_compat forall a. m a -> a
run Codec ps failure f m bytes
codecA Codec ps failure f m bytes
codecB AnyMessage ps f
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 f m bytes
-> Codec ps failure f m bytes -> AnyMessage ps f -> m Bool
forall ps failure (f :: ps -> *) (m :: * -> *) bytes.
(Monad m, Eq (AnyMessage ps f),
 forall a. Monoid a => Monoid (m a)) =>
Codec ps failure f m bytes
-> Codec ps failure f m bytes -> AnyMessage ps f -> m Bool
prop_codecs_compatM Codec ps failure f m bytes
codecA Codec ps failure f m bytes
codecB AnyMessage ps f
msg