{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE FlexibleContexts    #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE NamedFieldPuns      #-}
{-# LANGUAGE PolyKinds           #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications    #-}
{-# LANGUAGE TypeFamilies        #-}
{-# LANGUAGE TypeOperators       #-}

module Ouroboros.Network.Protocol.LocalTxSubmission.Codec
  ( codecLocalTxSubmission
  , anncodecLocalTxSubmission
  , anncodecLocalTxSubmission'
  , codecLocalTxSubmissionId
  , WithBytes (..)
  ) where

import Control.Monad.Class.MonadST

import Codec.CBOR.Decoding qualified as CBOR
import Codec.CBOR.Encoding qualified as CBOR
import Codec.CBOR.Read qualified as CBOR
import Data.ByteString.Lazy (ByteString)
import Data.Constraint
import Data.Functor.Identity
import Data.Kind (Type)
import Data.Type.Equality
import Text.Printf

import Network.TypedProtocol.Codec.CBOR

import Ouroboros.Network.Protocol.Codec.Utils (WithByteSpan (..),
           WithBytes (..), encodeWithBytes)
import Ouroboros.Network.Protocol.Codec.Utils qualified as Utils
import Ouroboros.Network.Protocol.LocalTxSubmission.Type


anncodecLocalTxSubmission
  :: forall tx reject m.
     MonadST m
  => (forall s . CBOR.Decoder s (ByteString -> tx))
  -- ^ decode transaction
  -> (reject -> CBOR.Encoding)
  -> (forall s. CBOR.Decoder s reject)
  -> AnnotatedCodec (LocalTxSubmission (WithBytes tx) reject) CBOR.DeserialiseFailure m ByteString
anncodecLocalTxSubmission :: forall tx reject (m :: * -> *).
MonadST m =>
(forall s. Decoder s (ByteString -> tx))
-> (reject -> Encoding)
-> (forall s. Decoder s reject)
-> AnnotatedCodec
     (LocalTxSubmission (WithBytes tx) reject)
     DeserialiseFailure
     m
     ByteString
anncodecLocalTxSubmission              forall s. Decoder s (ByteString -> tx)
decodeTx
                          reject -> Encoding
encodeReject forall s. Decoder s reject
decodeReject
    =
    (ByteString -> tx -> WithBytes tx)
-> (WithBytes tx -> Encoding)
-> (forall s. Decoder s (ByteString -> tx))
-> (reject -> Encoding)
-> (forall s. Decoder s reject)
-> AnnotatedCodec
     (LocalTxSubmission (WithBytes tx) reject)
     DeserialiseFailure
     m
     ByteString
forall tx reject txWithBytes (m :: * -> *).
MonadST m =>
(ByteString -> tx -> txWithBytes)
-> (txWithBytes -> Encoding)
-> (forall s. Decoder s (ByteString -> tx))
-> (reject -> Encoding)
-> (forall s. Decoder s reject)
-> AnnotatedCodec
     (LocalTxSubmission txWithBytes reject)
     DeserialiseFailure
     m
     ByteString
anncodecLocalTxSubmission' ByteString -> tx -> WithBytes tx
forall a. ByteString -> a -> WithBytes a
WithBytes WithBytes tx -> Encoding
encodeTx     Decoder s (ByteString -> tx)
forall s. Decoder s (ByteString -> tx)
decodeTx
                                         reject -> Encoding
encodeReject Decoder s reject
forall s. Decoder s reject
decodeReject
  where
    encodeTx :: WithBytes tx -> CBOR.Encoding
    encodeTx :: WithBytes tx -> Encoding
encodeTx = WithBytes tx -> Encoding
forall a. WithBytes a -> Encoding
encodeWithBytes


anncodecLocalTxSubmission'
  :: forall tx reject txWithBytes m.
     MonadST m
  => (ByteString -> tx -> txWithBytes)
  -> (txWithBytes -> CBOR.Encoding)
  -- ^ encode 'tx'
  -> (forall s. CBOR.Decoder s (ByteString -> tx))
  -- ^ decode 'tx'
  -> (reject -> CBOR.Encoding)
  -- ^ encode rejection reason
  -> (forall s. CBOR.Decoder s reject)
  -- ^ decode rejection reason
  -> AnnotatedCodec (LocalTxSubmission txWithBytes reject) CBOR.DeserialiseFailure m ByteString
anncodecLocalTxSubmission' :: forall tx reject txWithBytes (m :: * -> *).
MonadST m =>
(ByteString -> tx -> txWithBytes)
-> (txWithBytes -> Encoding)
-> (forall s. Decoder s (ByteString -> tx))
-> (reject -> Encoding)
-> (forall s. Decoder s reject)
-> AnnotatedCodec
     (LocalTxSubmission txWithBytes reject)
     DeserialiseFailure
     m
     ByteString
anncodecLocalTxSubmission' ByteString -> tx -> txWithBytes
mkWithBytes txWithBytes -> Encoding
encodeTx     forall s. Decoder s (ByteString -> tx)
decodeTx
                                       reject -> Encoding
encodeReject forall s. Decoder s reject
decodeReject
    =
    (forall (st :: LocalTxSubmission txWithBytes reject)
        (st' :: LocalTxSubmission txWithBytes reject).
 (StateTokenI st, ActiveState st) =>
 Message (LocalTxSubmission txWithBytes reject) st st' -> Encoding)
-> (forall (st :: LocalTxSubmission txWithBytes reject) s.
    ActiveState st =>
    StateToken st -> Decoder s (Annotator ByteString st))
-> CodecF
     (LocalTxSubmission txWithBytes reject)
     DeserialiseFailure
     m
     (Annotator ByteString)
     ByteString
forall ps (m :: * -> *) (f :: ps -> *).
MonadST m =>
(forall (st :: ps) (st' :: ps).
 (StateTokenI st, ActiveState st) =>
 Message ps st st' -> Encoding)
-> (forall (st :: ps) s.
    ActiveState st =>
    StateToken st -> Decoder s (f st))
-> CodecF ps DeserialiseFailure m f ByteString
mkCodecCborLazyBS
      ((txWithBytes -> Encoding)
-> (reject -> Encoding)
-> Message (LocalTxSubmission txWithBytes reject) st st'
-> Encoding
forall tx reject (st :: LocalTxSubmission tx reject)
       (st' :: LocalTxSubmission tx reject).
(tx -> Encoding)
-> (reject -> Encoding)
-> Message (LocalTxSubmission tx reject) st st'
-> Encoding
encodeLocalTxSubmission txWithBytes -> Encoding
encodeTx reject -> Encoding
encodeReject)
      StateToken st -> Decoder s (Annotator ByteString st)
StateToken st -> forall s. Decoder s (Annotator ByteString st)
forall (st :: LocalTxSubmission txWithBytes reject).
ActiveState st =>
StateToken st -> forall s. Decoder s (Annotator ByteString st)
forall (st :: LocalTxSubmission txWithBytes reject) s.
ActiveState st =>
StateToken st -> Decoder s (Annotator ByteString st)
decode
  where
    decode :: forall (st :: LocalTxSubmission txWithBytes reject).
              ActiveState st
           => StateToken st
           -> forall s. CBOR.Decoder s (Annotator ByteString st)
    decode :: forall (st :: LocalTxSubmission txWithBytes reject).
ActiveState st =>
StateToken st -> forall s. Decoder s (Annotator ByteString st)
decode =
      forall tx txWithBytes (withByteSpan :: * -> *) bytes reject
       (st :: LocalTxSubmission txWithBytes reject) s.
ActiveState st =>
(bytes -> withByteSpan (bytes -> tx) -> txWithBytes)
-> (forall a s'. Decoder s' a -> Decoder s' (withByteSpan a))
-> (forall s'. Decoder s' (bytes -> tx))
-> (forall s'. Decoder s' reject)
-> StateToken st
-> Decoder s (Annotator bytes st)
decodeLocalTxSubmission @tx
                              @txWithBytes
                              @WithByteSpan
                              @ByteString
                              @reject
                              ByteString -> WithByteSpan (ByteString -> tx) -> txWithBytes
mkWithBytes'
                              Decoder s' a -> Decoder s' (WithByteSpan a)
forall s a. Decoder s a -> Decoder s (WithByteSpan a)
forall a s'. Decoder s' a -> Decoder s' (WithByteSpan a)
Utils.decodeWithByteSpan
                              Decoder s' (ByteString -> tx)
forall s. Decoder s (ByteString -> tx)
decodeTx Decoder s' reject
forall s. Decoder s reject
decodeReject

    mkWithBytes' :: ByteString
                 -> WithByteSpan (ByteString -> tx)
                 -> txWithBytes
    mkWithBytes' :: ByteString -> WithByteSpan (ByteString -> tx) -> txWithBytes
mkWithBytes' ByteString
bytes (WithByteSpan (ByteString -> tx
fn, ByteOffset
start, ByteOffset
end)) =
      ByteString -> tx -> txWithBytes
mkWithBytes (ByteOffset -> ByteOffset -> ByteString -> ByteString
Utils.bytesBetweenOffsets ByteOffset
start ByteOffset
end ByteString
bytes) (ByteString -> tx
fn ByteString
bytes)


encodeLocalTxSubmission
  :: forall tx reject (st :: LocalTxSubmission tx reject) (st' :: LocalTxSubmission tx reject).
     (tx -> CBOR.Encoding)
  -> (reject -> CBOR.Encoding)
  -> Message (LocalTxSubmission tx reject) st st'
  -> CBOR.Encoding
encodeLocalTxSubmission :: forall tx reject (st :: LocalTxSubmission tx reject)
       (st' :: LocalTxSubmission tx reject).
(tx -> Encoding)
-> (reject -> Encoding)
-> Message (LocalTxSubmission tx reject) st st'
-> Encoding
encodeLocalTxSubmission tx -> Encoding
encodeTx reject -> Encoding
encodeReject = Message (LocalTxSubmission tx reject) st st' -> Encoding
forall (st0 :: LocalTxSubmission tx reject)
       (st1 :: LocalTxSubmission tx reject).
Message (LocalTxSubmission tx reject) st0 st1 -> Encoding
encode
  where
    encode :: forall st0 st1.
              Message (LocalTxSubmission tx reject) st0 st1
           -> CBOR.Encoding
    encode :: forall (st0 :: LocalTxSubmission tx reject)
       (st1 :: LocalTxSubmission tx reject).
Message (LocalTxSubmission tx reject) st0 st1 -> Encoding
encode (MsgSubmitTx tx
tx) =
        Word -> Encoding
CBOR.encodeListLen Word
2
     Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word -> Encoding
CBOR.encodeWord Word
0
     Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> tx -> Encoding
encodeTx tx
tx

    encode Message (LocalTxSubmission tx reject) st0 st1
R:MessageLocalTxSubmissionfromto tx reject st0 st1
MsgAcceptTx =
        Word -> Encoding
CBOR.encodeListLen Word
1
     Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word -> Encoding
CBOR.encodeWord Word
1

    encode (MsgRejectTx reject
reject) =
        Word -> Encoding
CBOR.encodeListLen Word
2
     Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word -> Encoding
CBOR.encodeWord Word
2
     Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> reject -> Encoding
encodeReject reject
reject

    encode Message (LocalTxSubmission tx reject) st0 st1
R:MessageLocalTxSubmissionfromto tx reject st0 st1
MsgDone =
        Word -> Encoding
CBOR.encodeListLen Word
1
     Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word -> Encoding
CBOR.encodeWord Word
3


decodeLocalTxSubmission
  :: forall (tx           :: Type)
            (txWithBytes  :: Type)
            (withByteSpan :: Type -> Type)
            (bytes        :: Type)
            (reject       :: Type)
            (st           :: LocalTxSubmission txWithBytes reject)
            s.
     ActiveState st
  => (bytes -> withByteSpan (bytes -> tx) -> txWithBytes)
  -> (forall a s'. CBOR.Decoder s' a -> CBOR.Decoder s' (withByteSpan a))
  -> (forall s'. CBOR.Decoder s' (bytes -> tx))
  -- ^ decode transaction
  -> (forall s'. CBOR.Decoder s' reject)
  -- ^ decode rejection reason
  -> StateToken st
  -> CBOR.Decoder s (Annotator bytes st)
decodeLocalTxSubmission :: forall tx txWithBytes (withByteSpan :: * -> *) bytes reject
       (st :: LocalTxSubmission txWithBytes reject) s.
ActiveState st =>
(bytes -> withByteSpan (bytes -> tx) -> txWithBytes)
-> (forall a s'. Decoder s' a -> Decoder s' (withByteSpan a))
-> (forall s'. Decoder s' (bytes -> tx))
-> (forall s'. Decoder s' reject)
-> StateToken st
-> Decoder s (Annotator bytes st)
decodeLocalTxSubmission bytes -> withByteSpan (bytes -> tx) -> txWithBytes
mkWithBytes forall a s'. Decoder s' a -> Decoder s' (withByteSpan a)
decodeWithByteSpan forall s'. Decoder s' (bytes -> tx)
decodeTx forall s'. Decoder s' reject
decodeReject StateToken st
stok
  = do
  len <- Decoder s Int
forall s. Decoder s Int
CBOR.decodeListLen
  key <- CBOR.decodeWord
  case (stok, len, key) of
    (SingLocalTxSubmission st
SingIdle, Int
2, Word
0) -> do
      tx <- Decoder s (bytes -> tx) -> Decoder s (withByteSpan (bytes -> tx))
forall a s'. Decoder s' a -> Decoder s' (withByteSpan a)
decodeWithByteSpan Decoder s (bytes -> tx)
forall s'. Decoder s' (bytes -> tx)
decodeTx
      return (Annotator $ \bytes
bytes -> Message (LocalTxSubmission txWithBytes reject) st 'StBusy
-> SomeMessage st
forall ps (st :: ps) (st' :: ps).
(StateTokenI st, StateTokenI st', ActiveState st) =>
Message ps st st' -> SomeMessage st
SomeMessage (txWithBytes
-> Message (LocalTxSubmission txWithBytes reject) 'StIdle 'StBusy
forall tx reject.
tx -> Message (LocalTxSubmission tx reject) 'StIdle 'StBusy
MsgSubmitTx (txWithBytes
 -> Message (LocalTxSubmission txWithBytes reject) 'StIdle 'StBusy)
-> txWithBytes
-> Message (LocalTxSubmission txWithBytes reject) 'StIdle 'StBusy
forall a b. (a -> b) -> a -> b
$ bytes -> withByteSpan (bytes -> tx) -> txWithBytes
mkWithBytes bytes
bytes withByteSpan (bytes -> tx)
tx))

    (SingLocalTxSubmission st
SingBusy, Int
1, Word
1) ->
      Annotator bytes st -> Decoder s (Annotator bytes st)
forall a. a -> Decoder s a
forall (m :: * -> *) a. Monad m => a -> m a
return ((bytes -> SomeMessage st) -> Annotator bytes st
forall {ps} bytes (st :: ps).
(bytes -> SomeMessage st) -> Annotator bytes st
Annotator ((bytes -> SomeMessage st) -> Annotator bytes st)
-> (bytes -> SomeMessage st) -> Annotator bytes st
forall a b. (a -> b) -> a -> b
$ \bytes
_ -> Message (LocalTxSubmission txWithBytes reject) st 'StIdle
-> SomeMessage st
forall ps (st :: ps) (st' :: ps).
(StateTokenI st, StateTokenI st', ActiveState st) =>
Message ps st st' -> SomeMessage st
SomeMessage Message (LocalTxSubmission txWithBytes reject) st 'StIdle
Message (LocalTxSubmission txWithBytes reject) 'StBusy 'StIdle
forall tx reject.
Message (LocalTxSubmission tx reject) 'StBusy 'StIdle
MsgAcceptTx)

    (SingLocalTxSubmission st
SingBusy, Int
2, Word
2) -> do
      reject <- Decoder s reject
forall s'. Decoder s' reject
decodeReject
      return (Annotator $ \bytes
_ -> Message (LocalTxSubmission txWithBytes reject) st 'StIdle
-> SomeMessage st
forall ps (st :: ps) (st' :: ps).
(StateTokenI st, StateTokenI st', ActiveState st) =>
Message ps st st' -> SomeMessage st
SomeMessage (reject
-> Message (LocalTxSubmission txWithBytes reject) 'StBusy 'StIdle
forall reject tx.
reject -> Message (LocalTxSubmission tx reject) 'StBusy 'StIdle
MsgRejectTx reject
reject))

    (SingLocalTxSubmission st
SingIdle, Int
1, Word
3) ->
      Annotator bytes st -> Decoder s (Annotator bytes st)
forall a. a -> Decoder s a
forall (m :: * -> *) a. Monad m => a -> m a
return ((bytes -> SomeMessage st) -> Annotator bytes st
forall {ps} bytes (st :: ps).
(bytes -> SomeMessage st) -> Annotator bytes st
Annotator ((bytes -> SomeMessage st) -> Annotator bytes st)
-> (bytes -> SomeMessage st) -> Annotator bytes st
forall a b. (a -> b) -> a -> b
$ \bytes
_ -> Message (LocalTxSubmission txWithBytes reject) st 'StDone
-> SomeMessage st
forall ps (st :: ps) (st' :: ps).
(StateTokenI st, StateTokenI st', ActiveState st) =>
Message ps st st' -> SomeMessage st
SomeMessage Message (LocalTxSubmission txWithBytes reject) st 'StDone
Message (LocalTxSubmission txWithBytes reject) 'StIdle 'StDone
forall tx reject.
Message (LocalTxSubmission tx reject) 'StIdle 'StDone
MsgDone)

    (SingLocalTxSubmission st
SingDone, Int
_, Word
_) -> StateToken 'StDone -> forall a. a
forall ps (st :: ps).
(StateAgency st ~ 'NobodyAgency, ActiveState st) =>
StateToken st -> forall a. a
notActiveState StateToken st
StateToken 'StDone
stok

    (SingLocalTxSubmission st
_, Int
_, Word
_) -> String -> Decoder s (Annotator bytes st)
forall a. String -> Decoder s a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> String -> String -> Word -> Int -> String
forall r. PrintfType r => String -> r
printf String
"codecLocalTxSubmission (%s, %s) unexpected key (%d, %d)"
                              (ActiveAgency' st (StateAgency st) -> String
forall a. Show a => a -> String
show (ActiveAgency' st (StateAgency st)
forall {ps} (st :: ps) (agency :: Agency).
IsActiveState st agency =>
ActiveAgency' st agency
activeAgency :: ActiveAgency st)) (SingLocalTxSubmission st -> String
forall a. Show a => a -> String
show StateToken st
SingLocalTxSubmission st
stok) Word
key Int
len)

--
-- Map protocol state & messages from `LocalTxSubmission (Identity tx) reject` to
-- `LocalTxSubmission tx reject`
--

type family FromIdentity (st :: LocalTxSubmission (Identity tx) reject) :: LocalTxSubmission tx reject where
  FromIdentity StIdle        = StIdle
  FromIdentity StBusy        = StBusy
  FromIdentity StDone        = StDone

type family ToIdentity (st :: LocalTxSubmission tx reject) :: LocalTxSubmission (Identity tx) reject where
  ToIdentity StIdle        = StIdle
  ToIdentity StBusy        = StBusy
  ToIdentity StDone        = StDone

singToIdentity
  :: forall tx reject (st :: LocalTxSubmission tx reject).
     StateToken st
  -> StateToken (ToIdentity st)
singToIdentity :: forall tx reject (st :: LocalTxSubmission tx reject).
StateToken st -> StateToken (ToIdentity st)
singToIdentity StateToken st
SingLocalTxSubmission st
SingIdle = StateToken (ToIdentity st)
SingLocalTxSubmission 'StIdle
forall {tx} {rejct}. SingLocalTxSubmission 'StIdle
SingIdle
singToIdentity StateToken st
SingLocalTxSubmission st
SingBusy = StateToken (ToIdentity st)
SingLocalTxSubmission 'StBusy
forall {tx} {rejct}. SingLocalTxSubmission 'StBusy
SingBusy
singToIdentity StateToken st
SingLocalTxSubmission st
SingDone = StateToken (ToIdentity st)
SingLocalTxSubmission 'StDone
forall {tx} {rejct}. SingLocalTxSubmission 'StDone
SingDone

--
-- Proofs
--

-- | A proof that `FromIdentity` is a left inverse of `ToIdentity`.
--
proof_FromTo
  :: forall tx reject (st :: LocalTxSubmission tx reject).
     StateToken st
  -> FromIdentity (ToIdentity st) :~: st
proof_FromTo :: forall tx reject (st :: LocalTxSubmission tx reject).
StateToken st -> FromIdentity (ToIdentity st) :~: st
proof_FromTo StateToken st
SingLocalTxSubmission st
SingIdle = st :~: st
FromIdentity (ToIdentity st) :~: st
forall {k} (a :: k). a :~: a
Refl
proof_FromTo StateToken st
SingLocalTxSubmission st
SingBusy = st :~: st
FromIdentity (ToIdentity st) :~: st
forall {k} (a :: k). a :~: a
Refl
proof_FromTo StateToken st
SingLocalTxSubmission st
SingDone = st :~: st
FromIdentity (ToIdentity st) :~: st
forall {k} (a :: k). a :~: a
Refl
{-# INLINE proof_FromTo #-}

-- | A proof that `ActiveState` constraint is preserved by `ToIdentity`.
--
proof_activeState
  :: forall tx reject (st :: LocalTxSubmission tx reject).
     StateToken st
  -> Dict (ActiveState st)
  -> Dict (ActiveState (ToIdentity st))
proof_activeState :: forall tx reject (st :: LocalTxSubmission tx reject).
StateToken st
-> Dict (ActiveState st) -> Dict (ActiveState (ToIdentity st))
proof_activeState StateToken st
SingLocalTxSubmission st
SingIdle      Dict (ActiveState st)
Dict = Dict (IsActiveState 'StIdle 'ClientAgency)
Dict (IsActiveState (ToIdentity st) (StateAgency (ToIdentity st)))
forall (a :: Constraint). a => Dict a
Dict
proof_activeState StateToken st
SingLocalTxSubmission st
SingBusy      Dict (ActiveState st)
Dict = Dict (IsActiveState 'StBusy 'ServerAgency)
Dict (IsActiveState (ToIdentity st) (StateAgency (ToIdentity st)))
forall (a :: Constraint). a => Dict a
Dict
proof_activeState sing :: StateToken st
sing@StateToken st
SingLocalTxSubmission st
SingDone Dict (ActiveState st)
Dict = StateToken 'StDone -> forall a. a
forall ps (st :: ps).
(StateAgency st ~ 'NobodyAgency, ActiveState st) =>
StateToken st -> forall a. a
notActiveState StateToken st
StateToken 'StDone
sing
{-# INLINE proof_activeState #-}

msgFromIdentity
  :: forall tx reject (st :: LocalTxSubmission (Identity tx) reject).
     SomeMessage st
  -> SomeMessage (FromIdentity st)
msgFromIdentity :: forall tx reject (st :: LocalTxSubmission (Identity tx) reject).
SomeMessage st -> SomeMessage (FromIdentity st)
msgFromIdentity (SomeMessage (MsgSubmitTx Identity tx
tx))
              =  Message (LocalTxSubmission tx reject) 'StIdle 'StBusy
-> SomeMessage 'StIdle
forall ps (st :: ps) (st' :: ps).
(StateTokenI st, StateTokenI st', ActiveState st) =>
Message ps st st' -> SomeMessage st
SomeMessage (tx -> Message (LocalTxSubmission tx reject) 'StIdle 'StBusy
forall tx reject.
tx -> Message (LocalTxSubmission tx reject) 'StIdle 'StBusy
MsgSubmitTx (Identity tx -> tx
forall a. Identity a -> a
runIdentity Identity tx
tx))
msgFromIdentity (SomeMessage Message (LocalTxSubmission (Identity tx) reject) st st'
R:MessageLocalTxSubmissionfromto (Identity tx) reject st st'
MsgAcceptTx)
              =  Message (LocalTxSubmission tx reject) 'StBusy 'StIdle
-> SomeMessage 'StBusy
forall ps (st :: ps) (st' :: ps).
(StateTokenI st, StateTokenI st', ActiveState st) =>
Message ps st st' -> SomeMessage st
SomeMessage Message (LocalTxSubmission tx reject) 'StBusy 'StIdle
forall tx reject.
Message (LocalTxSubmission tx reject) 'StBusy 'StIdle
MsgAcceptTx
msgFromIdentity (SomeMessage (MsgRejectTx reject
reject))
              =  Message (LocalTxSubmission tx reject) 'StBusy 'StIdle
-> SomeMessage 'StBusy
forall ps (st :: ps) (st' :: ps).
(StateTokenI st, StateTokenI st', ActiveState st) =>
Message ps st st' -> SomeMessage st
SomeMessage (reject -> Message (LocalTxSubmission tx reject) 'StBusy 'StIdle
forall reject tx.
reject -> Message (LocalTxSubmission tx reject) 'StBusy 'StIdle
MsgRejectTx reject
reject)
msgFromIdentity (SomeMessage Message (LocalTxSubmission (Identity tx) reject) st st'
R:MessageLocalTxSubmissionfromto (Identity tx) reject st st'
MsgDone)
              =  Message (LocalTxSubmission tx reject) 'StIdle 'StDone
-> SomeMessage 'StIdle
forall ps (st :: ps) (st' :: ps).
(StateTokenI st, StateTokenI st', ActiveState st) =>
Message ps st st' -> SomeMessage st
SomeMessage Message (LocalTxSubmission tx reject) 'StIdle 'StDone
forall tx reject.
Message (LocalTxSubmission tx reject) 'StIdle 'StDone
MsgDone
{-# INLINE msgFromIdentity #-}

codecLocalTxSubmission
  :: forall tx reject m.
     MonadST m
  => (tx -> CBOR.Encoding)
  -- ^ encode transaction
  -> (forall s . CBOR.Decoder s tx)
  -- ^ decode transaction
  -> (reject -> CBOR.Encoding)
  -> (forall s . CBOR.Decoder s reject)
  -> Codec (LocalTxSubmission tx reject) CBOR.DeserialiseFailure m ByteString
codecLocalTxSubmission :: forall tx reject (m :: * -> *).
MonadST m =>
(tx -> Encoding)
-> (forall s. Decoder s tx)
-> (reject -> Encoding)
-> (forall s. Decoder s reject)
-> Codec
     (LocalTxSubmission tx reject) DeserialiseFailure m ByteString
codecLocalTxSubmission tx -> Encoding
encodeTx     forall s. Decoder s tx
decodeTx
                       reject -> Encoding
encodeReject forall s. Decoder s reject
decodeReject
  = (forall (st :: LocalTxSubmission tx reject)
        (st' :: LocalTxSubmission tx reject).
 (StateTokenI st, ActiveState st) =>
 Message (LocalTxSubmission tx reject) st st' -> Encoding)
-> (forall (st :: LocalTxSubmission tx reject) s.
    ActiveState st =>
    StateToken st -> Decoder s (SomeMessage st))
-> CodecF
     (LocalTxSubmission tx reject)
     DeserialiseFailure
     m
     SomeMessage
     ByteString
forall ps (m :: * -> *) (f :: ps -> *).
MonadST m =>
(forall (st :: ps) (st' :: ps).
 (StateTokenI st, ActiveState st) =>
 Message ps st st' -> Encoding)
-> (forall (st :: ps) s.
    ActiveState st =>
    StateToken st -> Decoder s (f st))
-> CodecF ps DeserialiseFailure m f ByteString
mkCodecCborLazyBS
      ((tx -> Encoding)
-> (reject -> Encoding)
-> Message (LocalTxSubmission tx reject) st st'
-> Encoding
forall tx reject (st :: LocalTxSubmission tx reject)
       (st' :: LocalTxSubmission tx reject).
(tx -> Encoding)
-> (reject -> Encoding)
-> Message (LocalTxSubmission tx reject) st st'
-> Encoding
encodeLocalTxSubmission tx -> Encoding
encodeTx reject -> Encoding
encodeReject)
      StateToken st -> Decoder s (SomeMessage st)
forall (st :: LocalTxSubmission tx reject) s.
ActiveState st =>
StateToken st -> Decoder s (SomeMessage st)
decode
  where
    decode :: forall (st :: LocalTxSubmission tx reject) s.
                         ActiveState st
                      => StateToken st
                      -> CBOR.Decoder s (SomeMessage st)
    decode :: forall (st :: LocalTxSubmission tx reject) s.
ActiveState st =>
StateToken st -> Decoder s (SomeMessage st)
decode StateToken st
sing =
      case StateToken st -> FromIdentity (ToIdentity st) :~: st
forall tx reject (st :: LocalTxSubmission tx reject).
StateToken st -> FromIdentity (ToIdentity st) :~: st
proof_FromTo StateToken st
sing of { FromIdentity (ToIdentity st) :~: st
Refl ->
        case StateToken st
-> Dict (ActiveState st) -> Dict (ActiveState (ToIdentity st))
forall tx reject (st :: LocalTxSubmission tx reject).
StateToken st
-> Dict (ActiveState st) -> Dict (ActiveState (ToIdentity st))
proof_activeState StateToken st
sing Dict (ActiveState st)
forall (a :: Constraint). a => Dict a
Dict of { Dict (ActiveState (ToIdentity st))
Dict ->
          SomeMessage (ToIdentity st) -> SomeMessage st
SomeMessage (ToIdentity st)
-> SomeMessage (FromIdentity (ToIdentity st))
forall tx reject (st :: LocalTxSubmission (Identity tx) reject).
SomeMessage st -> SomeMessage (FromIdentity st)
msgFromIdentity (SomeMessage (ToIdentity st) -> SomeMessage st)
-> Decoder s (SomeMessage (ToIdentity st))
-> Decoder s (SomeMessage st)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateToken (ToIdentity st)
-> forall s. Decoder s (SomeMessage (ToIdentity st))
forall (st :: LocalTxSubmission (Identity tx) reject).
ActiveState st =>
StateToken st -> forall s. Decoder s (SomeMessage st)
decode' (StateToken st -> StateToken (ToIdentity st)
forall tx reject (st :: LocalTxSubmission tx reject).
StateToken st -> StateToken (ToIdentity st)
singToIdentity StateToken st
sing)
        }
      }

    decode' :: forall (st :: LocalTxSubmission (Identity tx) reject).
              ActiveState st
           => StateToken st
           -> forall s. CBOR.Decoder s (SomeMessage st)
    decode' :: forall (st :: LocalTxSubmission (Identity tx) reject).
ActiveState st =>
StateToken st -> forall s. Decoder s (SomeMessage st)
decode' StateToken st
stok =
      Annotator () st -> SomeMessage st
forall {ps} (st :: ps). Annotator () st -> SomeMessage st
mapAnnotator (Annotator () st -> SomeMessage st)
-> Decoder s (Annotator () st) -> Decoder s (SomeMessage st)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
        forall tx txWithBytes (withByteSpan :: * -> *) bytes reject
       (st :: LocalTxSubmission txWithBytes reject) s.
ActiveState st =>
(bytes -> withByteSpan (bytes -> tx) -> txWithBytes)
-> (forall a s'. Decoder s' a -> Decoder s' (withByteSpan a))
-> (forall s'. Decoder s' (bytes -> tx))
-> (forall s'. Decoder s' reject)
-> StateToken st
-> Decoder s (Annotator bytes st)
decodeLocalTxSubmission @tx            -- tx without bytes
                                @(Identity tx) -- tx with bytes
                                @Identity      -- withByteSpan functor
                                @()            -- bytes
                                @reject
                                () -> Identity (() -> tx) -> Identity tx
forall a. () -> Identity (() -> a) -> Identity a
mkWithBytes
                                Decoder s' a -> Decoder s' (Identity a)
forall s a. Decoder s a -> Decoder s (Identity a)
forall a s'. Decoder s' a -> Decoder s' (Identity a)
decodeWithByteSpan
                                (tx -> () -> tx
forall a b. a -> b -> a
const (tx -> () -> tx) -> Decoder s' tx -> Decoder s' (() -> tx)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Decoder s' tx
forall s. Decoder s tx
decodeTx)
                                Decoder s' reject
forall s. Decoder s reject
decodeReject
                                StateToken st
stok

    mapAnnotator :: Annotator () st -> SomeMessage st
    mapAnnotator :: forall {ps} (st :: ps). Annotator () st -> SomeMessage st
mapAnnotator Annotator { () -> SomeMessage st
runAnnotator :: () -> SomeMessage st
runAnnotator :: forall {ps} bytes (st :: ps).
Annotator bytes st -> bytes -> SomeMessage st
runAnnotator } = () -> SomeMessage st
runAnnotator ()

    mkWithBytes :: forall a. () -> Identity (() -> a) -> Identity a
    mkWithBytes :: forall a. () -> Identity (() -> a) -> Identity a
mkWithBytes ()
_ (Identity () -> a
f) = a -> Identity a
forall a. a -> Identity a
Identity (() -> a
f ())

    decodeWithByteSpan :: CBOR.Decoder s a -> CBOR.Decoder s (Identity a)
    decodeWithByteSpan :: forall s a. Decoder s a -> Decoder s (Identity a)
decodeWithByteSpan = (a -> Identity a) -> Decoder s a -> Decoder s (Identity a)
forall a b. (a -> b) -> Decoder s a -> Decoder s b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Identity a
forall a. a -> Identity a
Identity


codecLocalTxSubmissionId
  :: forall tx reject m.
     Monad m
  => Codec (LocalTxSubmission tx reject)
            CodecFailure m
           (AnyMessage (LocalTxSubmission tx reject))
codecLocalTxSubmissionId :: forall tx reject (m :: * -> *).
Monad m =>
Codec
  (LocalTxSubmission tx reject)
  CodecFailure
  m
  (AnyMessage (LocalTxSubmission tx reject))
codecLocalTxSubmissionId =
    (forall (st :: LocalTxSubmission tx reject)
        (st' :: LocalTxSubmission tx reject).
 (StateTokenI st, ActiveState st) =>
 Message (LocalTxSubmission tx reject) st st'
 -> AnyMessage (LocalTxSubmission tx reject))
-> (forall (st :: LocalTxSubmission tx reject).
    ActiveState st =>
    StateToken st
    -> m (DecodeStep
            (AnyMessage (LocalTxSubmission tx reject))
            CodecFailure
            m
            (SomeMessage st)))
-> CodecF
     (LocalTxSubmission tx reject)
     CodecFailure
     m
     SomeMessage
     (AnyMessage (LocalTxSubmission tx reject))
forall ps failure (m :: * -> *) (f :: ps -> *) bytes.
(forall (st :: ps) (st' :: ps).
 (StateTokenI st, ActiveState st) =>
 Message ps st st' -> bytes)
-> (forall (st :: ps).
    ActiveState st =>
    StateToken st -> m (DecodeStep bytes failure m (f st)))
-> CodecF ps failure m f bytes
Codec Message (LocalTxSubmission tx reject) st st'
-> AnyMessage (LocalTxSubmission tx reject)
forall (st :: LocalTxSubmission tx reject)
       (st' :: LocalTxSubmission tx reject).
(ActiveState st, StateTokenI st) =>
Message (LocalTxSubmission tx reject) st st'
-> AnyMessage (LocalTxSubmission tx reject)
forall (st :: LocalTxSubmission tx reject)
       (st' :: LocalTxSubmission tx reject).
(StateTokenI st, ActiveState st) =>
Message (LocalTxSubmission tx reject) st st'
-> AnyMessage (LocalTxSubmission tx reject)
encode StateToken st
-> m (DecodeStep
        (AnyMessage (LocalTxSubmission tx reject))
        CodecFailure
        m
        (SomeMessage st))
forall (st :: LocalTxSubmission tx reject).
ActiveState st =>
StateToken st
-> m (DecodeStep
        (AnyMessage (LocalTxSubmission tx reject))
        CodecFailure
        m
        (SomeMessage st))
decode
  where
    encode :: forall st st'.
              ActiveState st
           => StateTokenI st
           => Message (LocalTxSubmission tx reject) st st'
           -> AnyMessage (LocalTxSubmission tx reject)
    encode :: forall (st :: LocalTxSubmission tx reject)
       (st' :: LocalTxSubmission tx reject).
(ActiveState st, StateTokenI st) =>
Message (LocalTxSubmission tx reject) st st'
-> AnyMessage (LocalTxSubmission tx reject)
encode = Message (LocalTxSubmission tx reject) st st'
-> AnyMessage (LocalTxSubmission tx reject)
forall ps (st :: ps) (st' :: ps).
(StateTokenI st, ActiveState st) =>
Message ps st st' -> AnyMessage ps
AnyMessage

    decode :: forall (st :: LocalTxSubmission tx reject).
              ActiveState st
           => StateToken st
           -> m (DecodeStep (AnyMessage (LocalTxSubmission tx reject))
                            CodecFailure m (SomeMessage st))
    decode :: forall (st :: LocalTxSubmission tx reject).
ActiveState st =>
StateToken st
-> m (DecodeStep
        (AnyMessage (LocalTxSubmission tx reject))
        CodecFailure
        m
        (SomeMessage st))
decode StateToken st
stok = DecodeStep
  (AnyMessage (LocalTxSubmission tx reject))
  CodecFailure
  m
  (SomeMessage st)
-> m (DecodeStep
        (AnyMessage (LocalTxSubmission tx reject))
        CodecFailure
        m
        (SomeMessage st))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (DecodeStep
   (AnyMessage (LocalTxSubmission tx reject))
   CodecFailure
   m
   (SomeMessage st)
 -> m (DecodeStep
         (AnyMessage (LocalTxSubmission tx reject))
         CodecFailure
         m
         (SomeMessage st)))
-> DecodeStep
     (AnyMessage (LocalTxSubmission tx reject))
     CodecFailure
     m
     (SomeMessage st)
-> m (DecodeStep
        (AnyMessage (LocalTxSubmission tx reject))
        CodecFailure
        m
        (SomeMessage st))
forall a b. (a -> b) -> a -> b
$ (Maybe (AnyMessage (LocalTxSubmission tx reject))
 -> m (DecodeStep
         (AnyMessage (LocalTxSubmission tx reject))
         CodecFailure
         m
         (SomeMessage st)))
-> DecodeStep
     (AnyMessage (LocalTxSubmission tx reject))
     CodecFailure
     m
     (SomeMessage st)
forall bytes failure (m :: * -> *) a.
(Maybe bytes -> m (DecodeStep bytes failure m a))
-> DecodeStep bytes failure m a
DecodePartial ((Maybe (AnyMessage (LocalTxSubmission tx reject))
  -> m (DecodeStep
          (AnyMessage (LocalTxSubmission tx reject))
          CodecFailure
          m
          (SomeMessage st)))
 -> DecodeStep
      (AnyMessage (LocalTxSubmission tx reject))
      CodecFailure
      m
      (SomeMessage st))
-> (Maybe (AnyMessage (LocalTxSubmission tx reject))
    -> m (DecodeStep
            (AnyMessage (LocalTxSubmission tx reject))
            CodecFailure
            m
            (SomeMessage st)))
-> DecodeStep
     (AnyMessage (LocalTxSubmission tx reject))
     CodecFailure
     m
     (SomeMessage st)
forall a b. (a -> b) -> a -> b
$ \Maybe (AnyMessage (LocalTxSubmission tx reject))
bytes -> case (StateToken st
SingLocalTxSubmission st
stok, Maybe (AnyMessage (LocalTxSubmission tx reject))
bytes) of
      (SingLocalTxSubmission st
SingIdle, Just (AnyMessage msg :: Message (LocalTxSubmission tx reject) st st'
msg@(MsgSubmitTx{}))) -> Message (LocalTxSubmission tx reject) st st'
-> m (DecodeStep
        (AnyMessage (LocalTxSubmission tx reject))
        CodecFailure
        m
        (SomeMessage st))
forall {ps} {m :: * -> *} {st :: ps} {st' :: ps} {bytes} {failure}
       {m :: * -> *}.
(Monad m, StateTokenI st, StateTokenI st',
 IsActiveState st (StateAgency st)) =>
Message ps st st'
-> m (DecodeStep bytes failure m (SomeMessage st))
res Message (LocalTxSubmission tx reject) st st'
Message (LocalTxSubmission tx reject) st st'
msg
      (SingLocalTxSubmission st
SingBusy, Just (AnyMessage msg :: Message (LocalTxSubmission tx reject) st st'
msg@(MsgAcceptTx{}))) -> Message (LocalTxSubmission tx reject) st st'
-> m (DecodeStep
        (AnyMessage (LocalTxSubmission tx reject))
        CodecFailure
        m
        (SomeMessage st))
forall {ps} {m :: * -> *} {st :: ps} {st' :: ps} {bytes} {failure}
       {m :: * -> *}.
(Monad m, StateTokenI st, StateTokenI st',
 IsActiveState st (StateAgency st)) =>
Message ps st st'
-> m (DecodeStep bytes failure m (SomeMessage st))
res Message (LocalTxSubmission tx reject) st st'
Message (LocalTxSubmission tx reject) st st'
msg
      (SingLocalTxSubmission st
SingBusy, Just (AnyMessage msg :: Message (LocalTxSubmission tx reject) st st'
msg@(MsgRejectTx{}))) -> Message (LocalTxSubmission tx reject) st st'
-> m (DecodeStep
        (AnyMessage (LocalTxSubmission tx reject))
        CodecFailure
        m
        (SomeMessage st))
forall {ps} {m :: * -> *} {st :: ps} {st' :: ps} {bytes} {failure}
       {m :: * -> *}.
(Monad m, StateTokenI st, StateTokenI st',
 IsActiveState st (StateAgency st)) =>
Message ps st st'
-> m (DecodeStep bytes failure m (SomeMessage st))
res Message (LocalTxSubmission tx reject) st st'
Message (LocalTxSubmission tx reject) st st'
msg
      (SingLocalTxSubmission st
SingIdle, Just (AnyMessage msg :: Message (LocalTxSubmission tx reject) st st'
msg@(MsgDone{})))     -> Message (LocalTxSubmission tx reject) st st'
-> m (DecodeStep
        (AnyMessage (LocalTxSubmission tx reject))
        CodecFailure
        m
        (SomeMessage st))
forall {ps} {m :: * -> *} {st :: ps} {st' :: ps} {bytes} {failure}
       {m :: * -> *}.
(Monad m, StateTokenI st, StateTokenI st',
 IsActiveState st (StateAgency st)) =>
Message ps st st'
-> m (DecodeStep bytes failure m (SomeMessage st))
res Message (LocalTxSubmission tx reject) st st'
Message (LocalTxSubmission tx reject) st st'
msg
      (SingLocalTxSubmission st
SingDone, Maybe (AnyMessage (LocalTxSubmission tx reject))
_)                                     -> StateToken 'StDone -> forall a. a
forall ps (st :: ps).
(StateAgency st ~ 'NobodyAgency, ActiveState st) =>
StateToken st -> forall a. a
notActiveState StateToken st
StateToken 'StDone
stok
      (SingLocalTxSubmission st
_, Maybe (AnyMessage (LocalTxSubmission tx reject))
Nothing) -> DecodeStep
  (AnyMessage (LocalTxSubmission tx reject))
  CodecFailure
  m
  (SomeMessage st)
-> m (DecodeStep
        (AnyMessage (LocalTxSubmission tx reject))
        CodecFailure
        m
        (SomeMessage st))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (CodecFailure
-> DecodeStep
     (AnyMessage (LocalTxSubmission tx reject))
     CodecFailure
     m
     (SomeMessage st)
forall bytes failure (m :: * -> *) a.
failure -> DecodeStep bytes failure m a
DecodeFail CodecFailure
CodecFailureOutOfInput)
      (SingLocalTxSubmission st
_, Maybe (AnyMessage (LocalTxSubmission tx reject))
_)       -> DecodeStep
  (AnyMessage (LocalTxSubmission tx reject))
  CodecFailure
  m
  (SomeMessage st)
-> m (DecodeStep
        (AnyMessage (LocalTxSubmission tx reject))
        CodecFailure
        m
        (SomeMessage st))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (CodecFailure
-> DecodeStep
     (AnyMessage (LocalTxSubmission tx reject))
     CodecFailure
     m
     (SomeMessage st)
forall bytes failure (m :: * -> *) a.
failure -> DecodeStep bytes failure m a
DecodeFail (String -> CodecFailure
CodecFailure String
failmsg))
    res :: Message ps st st'
-> m (DecodeStep bytes failure m (SomeMessage st))
res Message ps st st'
msg = DecodeStep bytes failure m (SomeMessage st)
-> m (DecodeStep bytes failure m (SomeMessage st))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SomeMessage st
-> Maybe bytes -> DecodeStep bytes failure m (SomeMessage st)
forall bytes failure (m :: * -> *) a.
a -> Maybe bytes -> DecodeStep bytes failure m a
DecodeDone (Message ps st st' -> SomeMessage st
forall ps (st :: ps) (st' :: ps).
(StateTokenI st, StateTokenI st', ActiveState st) =>
Message ps st st' -> SomeMessage st
SomeMessage Message ps st st'
msg) Maybe bytes
forall a. Maybe a
Nothing)
    failmsg :: String
failmsg = String
"codecLocalTxSubmissionId: no matching message"