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

module Ouroboros.Network.Protocol.LocalStateQuery.Codec
  ( LocalStateQueryVersion (..)
  , codecLocalStateQuery
  , codecLocalStateQueryId
  , Some (..)
  ) 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.Kind (Type)
import Data.Singletons.Decide
import Formatting (formatToString, (%+))
import Formatting qualified as F

import Network.TypedProtocol.Codec (CodecFailure (..), DecodeStep (..),
           SomeMessage (..))
import Network.TypedProtocol.Core
import Network.TypedProtocol.Stateful.Codec qualified as Stateful
import Network.TypedProtocol.Stateful.Codec.CBOR qualified as Stateful

import Ouroboros.Network.Protocol.LocalStateQuery.Type


data Some (f :: k -> Type) where
    Some :: f a -> Some f

codecLocalStateQuery
  :: forall block point query m.
     ( MonadST m
     , ShowQuery query
     )
  => LocalStateQueryVersion
     -- ^ eg whether to allow 'ImmutableTip' in @'MsgAcquire'
  -> (point -> CBOR.Encoding)
  -> (forall s . CBOR.Decoder s point)
  -> (forall result . query result -> CBOR.Encoding)
  -> (forall s . CBOR.Decoder s (Some query))
  -> (forall result . query result -> result -> CBOR.Encoding)
  -> (forall result . query result -> forall s . CBOR.Decoder s result)
  -> Stateful.Codec (LocalStateQuery block point query) CBOR.DeserialiseFailure State m ByteString
codecLocalStateQuery :: forall block point (query :: * -> *) (m :: * -> *).
(MonadST m, ShowQuery query) =>
LocalStateQueryVersion
-> (point -> Encoding)
-> (forall s. Decoder s point)
-> (forall result. query result -> Encoding)
-> (forall s. Decoder s (Some query))
-> (forall result. query result -> result -> Encoding)
-> (forall result. query result -> forall s. Decoder s result)
-> Codec
     (LocalStateQuery block point query)
     DeserialiseFailure
     State
     m
     ByteString
codecLocalStateQuery LocalStateQueryVersion
version
                     point -> Encoding
encodePoint  forall s. Decoder s point
decodePoint
                     forall result. query result -> Encoding
encodeQuery  forall s. Decoder s (Some query)
decodeQuery
                     forall result. query result -> result -> Encoding
encodeResult forall result. query result -> forall s. Decoder s result
decodeResult =
    (forall (st :: LocalStateQuery block point query)
        (st' :: LocalStateQuery block point query).
 (StateTokenI st, ActiveState st) =>
 State st
 -> Message (LocalStateQuery block point query) st st' -> Encoding)
-> (forall (st :: LocalStateQuery block point query) s.
    ActiveState st =>
    StateToken st -> State st -> Decoder s (SomeMessage st))
-> Codec
     (LocalStateQuery block point query)
     DeserialiseFailure
     State
     m
     ByteString
forall ps (f :: ps -> *) (m :: * -> *).
MonadST m =>
(forall (st :: ps) (st' :: ps).
 (StateTokenI st, ActiveState st) =>
 f st -> Message ps st st' -> Encoding)
-> (forall (st :: ps) s.
    ActiveState st =>
    StateToken st -> f st -> Decoder s (SomeMessage st))
-> Codec ps DeserialiseFailure f m ByteString
Stateful.mkCodecCborLazyBS State st
-> Message (LocalStateQuery block point query) st st' -> Encoding
forall (st :: LocalStateQuery block point query)
       (st' :: LocalStateQuery block point query).
(StateTokenI st, ActiveState st) =>
State st
-> Message (LocalStateQuery block point query) st st' -> Encoding
forall (st :: LocalStateQuery block point query)
       (st' :: LocalStateQuery block point query).
State st
-> Message (LocalStateQuery block point query) st st' -> Encoding
encode StateToken st -> State st -> Decoder s (SomeMessage st)
forall s (st :: LocalStateQuery block point query).
ActiveState st =>
StateToken st -> State st -> Decoder s (SomeMessage st)
forall (st :: LocalStateQuery block point query) s.
ActiveState st =>
StateToken st -> State st -> Decoder s (SomeMessage st)
decode
  where
    canAcquireImmutable :: Bool
canAcquireImmutable = LocalStateQueryVersion
version LocalStateQueryVersion -> LocalStateQueryVersion -> Bool
forall a. Ord a => a -> a -> Bool
>= LocalStateQueryVersion
LocalStateQuery_V2

    encodeFailure :: AcquireFailure -> CBOR.Encoding
    encodeFailure :: AcquireFailure -> Encoding
encodeFailure AcquireFailure
AcquireFailurePointTooOld     = Word8 -> Encoding
CBOR.encodeWord8 Word8
0
    encodeFailure AcquireFailure
AcquireFailurePointNotOnChain = Word8 -> Encoding
CBOR.encodeWord8 Word8
1

    decodeFailure :: forall s. CBOR.Decoder s AcquireFailure
    decodeFailure :: forall s. Decoder s AcquireFailure
decodeFailure = do
      tag <- Decoder s Word8
forall s. Decoder s Word8
CBOR.decodeWord8
      case tag of
        Word8
0 -> AcquireFailure -> Decoder s AcquireFailure
forall a. a -> Decoder s a
forall (m :: * -> *) a. Monad m => a -> m a
return AcquireFailure
AcquireFailurePointTooOld
        Word8
1 -> AcquireFailure -> Decoder s AcquireFailure
forall a. a -> Decoder s a
forall (m :: * -> *) a. Monad m => a -> m a
return AcquireFailure
AcquireFailurePointNotOnChain
        Word8
_ -> String -> Decoder s AcquireFailure
forall a. String -> Decoder s a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Decoder s AcquireFailure)
-> String -> Decoder s AcquireFailure
forall a b. (a -> b) -> a -> b
$ String
"decodeFailure: invalid tag " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Word8 -> String
forall a. Show a => a -> String
show Word8
tag

    encode :: forall (st  :: LocalStateQuery block point query)
                     (st' :: LocalStateQuery block point query).
              State st
           -> Message (LocalStateQuery block point query) st st'
           -> CBOR.Encoding
    encode :: forall (st :: LocalStateQuery block point query)
       (st' :: LocalStateQuery block point query).
State st
-> Message (LocalStateQuery block point query) st st' -> Encoding
encode State st
_ (MsgAcquire (SpecificPoint point
pt)) =
        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
<> point -> Encoding
encodePoint point
pt

    encode State st
_ (MsgAcquire Target point
VolatileTip) =
        Word -> Encoding
CBOR.encodeListLen Word
1
     Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word -> Encoding
CBOR.encodeWord Word
8

    encode State st
_ (MsgAcquire Target point
ImmutableTip)
      | Bool
canAcquireImmutable =
        Word -> Encoding
CBOR.encodeListLen Word
1
     Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word -> Encoding
CBOR.encodeWord Word
10
      | Bool
otherwise =
      String -> Encoding
forall a. HasCallStack => String -> a
error (String -> Encoding) -> String -> Encoding
forall a b. (a -> b) -> a -> b
$ String
"encodeFailure: local state query: acquiring the immutable tip "
           String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"must be conditional on negotiating v16 of the node-to-client "
           String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"protocol"

    encode State st
_ Message (LocalStateQuery block point query) st st'
R:MessageLocalStateQueryfromto block point query st st'
MsgAcquired =
        Word -> Encoding
CBOR.encodeListLen Word
1
     Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word -> Encoding
CBOR.encodeWord Word
1

    encode State st
_ (MsgFailure AcquireFailure
failure) =
        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
<> AcquireFailure -> Encoding
encodeFailure AcquireFailure
failure

    encode State st
_ (MsgQuery query result
query) =
        Word -> Encoding
CBOR.encodeListLen Word
2
     Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word -> Encoding
CBOR.encodeWord Word
3
     Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> query result -> Encoding
forall result. query result -> Encoding
encodeQuery query result
query

    encode (StateQuerying query result
query) (MsgResult result
result) =
        Word -> Encoding
CBOR.encodeListLen Word
2
     Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word -> Encoding
CBOR.encodeWord Word
4
     Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> query result -> result -> Encoding
forall result. query result -> result -> Encoding
encodeResult query result
query result
result
result

    encode State st
_ Message (LocalStateQuery block point query) st st'
R:MessageLocalStateQueryfromto block point query st st'
MsgRelease =
        Word -> Encoding
CBOR.encodeListLen Word
1
     Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word -> Encoding
CBOR.encodeWord Word
5

    encode State st
_ (MsgReAcquire (SpecificPoint point
pt)) =
        Word -> Encoding
CBOR.encodeListLen Word
2
     Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word -> Encoding
CBOR.encodeWord Word
6
     Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> point -> Encoding
encodePoint point
pt

    encode State st
_ (MsgReAcquire Target point
VolatileTip) =
        Word -> Encoding
CBOR.encodeListLen Word
1
     Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word -> Encoding
CBOR.encodeWord Word
9

    encode State st
_ (MsgReAcquire Target point
ImmutableTip)
      | Bool
canAcquireImmutable =
        Word -> Encoding
CBOR.encodeListLen Word
1
     Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word -> Encoding
CBOR.encodeWord Word
11
      | Bool
otherwise =
      String -> Encoding
forall a. HasCallStack => String -> a
error (String -> Encoding) -> String -> Encoding
forall a b. (a -> b) -> a -> b
$ String
"encodeFailure: local state query: re-acquiring the immutable "
           String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"tip must be conditional on negotiating v16 of the "
           String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"node-to-client protocol"

    encode State st
_ Message (LocalStateQuery block point query) st st'
R:MessageLocalStateQueryfromto block point query st st'
MsgDone =
        Word -> Encoding
CBOR.encodeListLen Word
1
     Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word -> Encoding
CBOR.encodeWord Word
7

    decode :: forall s (st :: LocalStateQuery block point query).
              ActiveState st
           => StateToken st
           -> State st
           -> CBOR.Decoder s (SomeMessage st)
    decode :: forall s (st :: LocalStateQuery block point query).
ActiveState st =>
StateToken st -> State st -> Decoder s (SomeMessage st)
decode StateToken st
stok State st
f = do
      len <- Decoder s Int
forall s. Decoder s Int
CBOR.decodeListLen
      key <- CBOR.decodeWord
      case (stok, f, len, key) of
        (SingLocalStateQuery st
SingIdle, State st
_, Int
2, Word
0) -> do
          pt <- Decoder s point
forall s. Decoder s point
decodePoint
          return (SomeMessage (MsgAcquire (SpecificPoint pt)))

        (SingLocalStateQuery st
SingIdle, State st
_, Int
1, Word
8) -> do
          SomeMessage st -> Decoder s (SomeMessage st)
forall a. a -> Decoder s a
forall (m :: * -> *) a. Monad m => a -> m a
return (Message (LocalStateQuery block point query) st 'StAcquiring
-> SomeMessage st
forall ps (st :: ps) (st' :: ps).
(StateTokenI st, StateTokenI st', ActiveState st) =>
Message ps st st' -> SomeMessage st
SomeMessage (Target point
-> Message (LocalStateQuery block point query) 'StIdle 'StAcquiring
forall point block (query :: * -> *).
Target point
-> Message (LocalStateQuery block point query) 'StIdle 'StAcquiring
MsgAcquire Target point
forall point. Target point
VolatileTip))

        (SingLocalStateQuery st
SingIdle, State st
_, Int
1, Word
10) -> do
          SomeMessage st -> Decoder s (SomeMessage st)
forall a. a -> Decoder s a
forall (m :: * -> *) a. Monad m => a -> m a
return (Message (LocalStateQuery block point query) st 'StAcquiring
-> SomeMessage st
forall ps (st :: ps) (st' :: ps).
(StateTokenI st, StateTokenI st', ActiveState st) =>
Message ps st st' -> SomeMessage st
SomeMessage (Target point
-> Message (LocalStateQuery block point query) 'StIdle 'StAcquiring
forall point block (query :: * -> *).
Target point
-> Message (LocalStateQuery block point query) 'StIdle 'StAcquiring
MsgAcquire Target point
forall point. Target point
ImmutableTip))

        (SingLocalStateQuery st
SingAcquiring, State st
_, Int
1, Word
1) ->
          SomeMessage st -> Decoder s (SomeMessage st)
forall a. a -> Decoder s a
forall (m :: * -> *) a. Monad m => a -> m a
return (Message (LocalStateQuery block point query) st 'StAcquired
-> SomeMessage st
forall ps (st :: ps) (st' :: ps).
(StateTokenI st, StateTokenI st', ActiveState st) =>
Message ps st st' -> SomeMessage st
SomeMessage Message (LocalStateQuery block point query) st 'StAcquired
Message
  (LocalStateQuery block point query) 'StAcquiring 'StAcquired
forall block point (query :: * -> *).
Message
  (LocalStateQuery block point query) 'StAcquiring 'StAcquired
MsgAcquired)

        (SingLocalStateQuery st
SingAcquiring, State st
_, Int
2, Word
2) -> do
          failure <- Decoder s AcquireFailure
forall s. Decoder s AcquireFailure
decodeFailure
          return (SomeMessage (MsgFailure failure))

        (SingLocalStateQuery st
SingAcquired, State st
_, Int
2, Word
3) -> do
          Some query <- Decoder s (Some query)
forall s. Decoder s (Some query)
decodeQuery
          return (SomeMessage (MsgQuery query))

        (SingLocalStateQuery st
SingQuerying, StateQuerying query result
query, Int
2, Word
4) -> do
          result <- query result -> forall s. Decoder s result
forall result. query result -> forall s. Decoder s result
decodeResult query result
query
          return (SomeMessage (MsgResult result))

        (SingLocalStateQuery st
SingAcquired, State st
_, Int
1, Word
5) ->
          SomeMessage st -> Decoder s (SomeMessage st)
forall a. a -> Decoder s a
forall (m :: * -> *) a. Monad m => a -> m a
return (Message (LocalStateQuery block point query) st 'StIdle
-> SomeMessage st
forall ps (st :: ps) (st' :: ps).
(StateTokenI st, StateTokenI st', ActiveState st) =>
Message ps st st' -> SomeMessage st
SomeMessage Message (LocalStateQuery block point query) st 'StIdle
Message (LocalStateQuery block point query) 'StAcquired 'StIdle
forall block point (query :: * -> *).
Message (LocalStateQuery block point query) 'StAcquired 'StIdle
MsgRelease)

        (SingLocalStateQuery st
SingAcquired, State st
_, Int
2, Word
6) -> do
          pt <- Decoder s point
forall s. Decoder s point
decodePoint
          return (SomeMessage (MsgReAcquire (SpecificPoint pt)))

        (SingLocalStateQuery st
SingAcquired, State st
_, Int
1, Word
9) -> do
          SomeMessage st -> Decoder s (SomeMessage st)
forall a. a -> Decoder s a
forall (m :: * -> *) a. Monad m => a -> m a
return (Message (LocalStateQuery block point query) st 'StAcquiring
-> SomeMessage st
forall ps (st :: ps) (st' :: ps).
(StateTokenI st, StateTokenI st', ActiveState st) =>
Message ps st st' -> SomeMessage st
SomeMessage (Target point
-> Message
     (LocalStateQuery block point query) 'StAcquired 'StAcquiring
forall point block (query :: * -> *).
Target point
-> Message
     (LocalStateQuery block point query) 'StAcquired 'StAcquiring
MsgReAcquire Target point
forall point. Target point
VolatileTip))

        (SingLocalStateQuery st
SingAcquired, State st
_, Int
1, Word
11) -> do
          SomeMessage st -> Decoder s (SomeMessage st)
forall a. a -> Decoder s a
forall (m :: * -> *) a. Monad m => a -> m a
return (Message (LocalStateQuery block point query) st 'StAcquiring
-> SomeMessage st
forall ps (st :: ps) (st' :: ps).
(StateTokenI st, StateTokenI st', ActiveState st) =>
Message ps st st' -> SomeMessage st
SomeMessage (Target point
-> Message
     (LocalStateQuery block point query) 'StAcquired 'StAcquiring
forall point block (query :: * -> *).
Target point
-> Message
     (LocalStateQuery block point query) 'StAcquired 'StAcquiring
MsgReAcquire Target point
forall point. Target point
ImmutableTip))

        (SingLocalStateQuery st
SingIdle, State st
_, Int
1, Word
7) ->
          SomeMessage st -> Decoder s (SomeMessage st)
forall a. a -> Decoder s a
forall (m :: * -> *) a. Monad m => a -> m a
return (Message (LocalStateQuery block point query) st 'StDone
-> SomeMessage st
forall ps (st :: ps) (st' :: ps).
(StateTokenI st, StateTokenI st', ActiveState st) =>
Message ps st st' -> SomeMessage st
SomeMessage Message (LocalStateQuery block point query) st 'StDone
Message (LocalStateQuery block point query) 'StIdle 'StDone
forall block point (query :: * -> *).
Message (LocalStateQuery block point query) 'StIdle 'StDone
MsgDone)

        --
        -- failures per protocol state
        --

        (SingLocalStateQuery st
SingIdle, State st
_, Int
_, Word
_) ->
          String -> Decoder s (SomeMessage st)
forall a. String -> Decoder s a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (Format
  String
  (ActiveAgency' st (StateAgency st)
   -> SingLocalStateQuery st -> Word -> Int -> String)
-> ActiveAgency' st (StateAgency st)
-> SingLocalStateQuery st
-> Word
-> Int
-> String
forall a. Format String a -> a
formatToString Format
  String
  (ActiveAgency' st (StateAgency st)
   -> StateToken st -> Word -> Int -> String)
Format
  String
  (ActiveAgency' st (StateAgency st)
   -> SingLocalStateQuery st -> Word -> Int -> String)
forall (st :: LocalStateQuery block point query) r.
Format r (ActiveAgency st -> StateToken st -> Word -> Int -> r)
fmterr (ActiveAgency' st 'ClientAgency
ActiveAgency' st (StateAgency st)
forall {ps} (st :: ps) (agency :: Agency).
IsActiveState st agency =>
ActiveAgency' st agency
activeAgency :: ActiveAgency st) StateToken st
SingLocalStateQuery st
stok Word
key Int
len)
        (SingLocalStateQuery st
SingAcquired, State st
_, Int
_, Word
_) ->
          String -> Decoder s (SomeMessage st)
forall a. String -> Decoder s a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (Format
  String
  (ActiveAgency' st (StateAgency st)
   -> SingLocalStateQuery st -> Word -> Int -> String)
-> ActiveAgency' st (StateAgency st)
-> SingLocalStateQuery st
-> Word
-> Int
-> String
forall a. Format String a -> a
formatToString Format
  String
  (ActiveAgency' st (StateAgency st)
   -> StateToken st -> Word -> Int -> String)
Format
  String
  (ActiveAgency' st (StateAgency st)
   -> SingLocalStateQuery st -> Word -> Int -> String)
forall (st :: LocalStateQuery block point query) r.
Format r (ActiveAgency st -> StateToken st -> Word -> Int -> r)
fmterr (ActiveAgency' st 'ClientAgency
ActiveAgency' st (StateAgency st)
forall {ps} (st :: ps) (agency :: Agency).
IsActiveState st agency =>
ActiveAgency' st agency
activeAgency :: ActiveAgency st) StateToken st
SingLocalStateQuery st
stok Word
key Int
len)
        (SingLocalStateQuery st
SingAcquiring, State st
_, Int
_, Word
_) ->
          String -> Decoder s (SomeMessage st)
forall a. String -> Decoder s a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (Format
  String
  (ActiveAgency' st (StateAgency st)
   -> SingLocalStateQuery st -> Word -> Int -> String)
-> ActiveAgency' st (StateAgency st)
-> SingLocalStateQuery st
-> Word
-> Int
-> String
forall a. Format String a -> a
formatToString Format
  String
  (ActiveAgency' st (StateAgency st)
   -> StateToken st -> Word -> Int -> String)
Format
  String
  (ActiveAgency' st (StateAgency st)
   -> SingLocalStateQuery st -> Word -> Int -> String)
forall (st :: LocalStateQuery block point query) r.
Format r (ActiveAgency st -> StateToken st -> Word -> Int -> r)
fmterr (ActiveAgency' st 'ServerAgency
ActiveAgency' st (StateAgency st)
forall {ps} (st :: ps) (agency :: Agency).
IsActiveState st agency =>
ActiveAgency' st agency
activeAgency :: ActiveAgency st) StateToken st
SingLocalStateQuery st
stok Word
key Int
len)
        (SingQuerying {}, State st
_, Int
_, Word
_) ->
          String -> Decoder s (SomeMessage st)
forall a. String -> Decoder s a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (Format
  String
  (ActiveAgency' st (StateAgency st)
   -> SingLocalStateQuery st -> Word -> Int -> String)
-> ActiveAgency' st (StateAgency st)
-> SingLocalStateQuery st
-> Word
-> Int
-> String
forall a. Format String a -> a
formatToString Format
  String
  (ActiveAgency' st (StateAgency st)
   -> StateToken st -> Word -> Int -> String)
Format
  String
  (ActiveAgency' st (StateAgency st)
   -> SingLocalStateQuery st -> Word -> Int -> String)
forall (st :: LocalStateQuery block point query) r.
Format r (ActiveAgency st -> StateToken st -> Word -> Int -> r)
fmterr (ActiveAgency' st 'ServerAgency
ActiveAgency' st (StateAgency st)
forall {ps} (st :: ps) (agency :: Agency).
IsActiveState st agency =>
ActiveAgency' st agency
activeAgency :: ActiveAgency st) StateToken st
SingLocalStateQuery st
stok Word
key Int
len)

        (SingLocalStateQuery st
SingDone, State st
_, 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

    fmterr :: forall (st :: LocalStateQuery block point query) r.
              F.Format r (ActiveAgency st -> StateToken st -> Word -> Int -> r)
    fmterr :: forall (st :: LocalStateQuery block point query) r.
Format r (ActiveAgency st -> StateToken st -> Word -> Int -> r)
fmterr = Format
  (ActiveAgency' st (StateAgency st)
   -> SingLocalStateQuery st -> Word -> Int -> r)
  (ActiveAgency' st (StateAgency st)
   -> SingLocalStateQuery st -> Word -> Int -> r)
"codecLocalStateQuery"
          Format
  (ActiveAgency' st (StateAgency st)
   -> SingLocalStateQuery st -> Word -> Int -> r)
  (ActiveAgency' st (StateAgency st)
   -> SingLocalStateQuery st -> Word -> Int -> r)
-> Format
     r
     (ActiveAgency' st (StateAgency st)
      -> SingLocalStateQuery st -> Word -> Int -> r)
-> Format
     r
     (ActiveAgency' st (StateAgency st)
      -> SingLocalStateQuery st -> Word -> Int -> r)
forall r a r'. Format r a -> Format r' r -> Format r' a
%+ Format
  (Word -> Int -> r)
  (ActiveAgency' st (StateAgency st)
   -> SingLocalStateQuery st -> Word -> Int -> r)
-> Format
     (Word -> Int -> r)
     (ActiveAgency' st (StateAgency st)
      -> SingLocalStateQuery st -> Word -> Int -> r)
forall r a. Format r a -> Format r a
F.parenthesised (Format
  (SingLocalStateQuery st -> Word -> Int -> r)
  (ActiveAgency' st (StateAgency st)
   -> SingLocalStateQuery st -> Word -> Int -> r)
forall a r. Show a => Format r (a -> r)
F.shown Format
  (SingLocalStateQuery st -> Word -> Int -> r)
  (ActiveAgency' st (StateAgency st)
   -> SingLocalStateQuery st -> Word -> Int -> r)
-> Format
     (Word -> Int -> r) (SingLocalStateQuery st -> Word -> Int -> r)
-> Format
     (Word -> Int -> r)
     (ActiveAgency' st (StateAgency st)
      -> SingLocalStateQuery st -> Word -> Int -> r)
forall r a r'. Format r a -> Format r' r -> Format r' a
F.% Format
  (SingLocalStateQuery st -> Word -> Int -> r)
  (SingLocalStateQuery st -> Word -> Int -> r)
"," Format
  (SingLocalStateQuery st -> Word -> Int -> r)
  (SingLocalStateQuery st -> Word -> Int -> r)
-> Format
     (Word -> Int -> r) (SingLocalStateQuery st -> Word -> Int -> r)
-> Format
     (Word -> Int -> r) (SingLocalStateQuery st -> Word -> Int -> r)
forall r a r'. Format r a -> Format r' r -> Format r' a
%+ Format
  (Word -> Int -> r) (SingLocalStateQuery st -> Word -> Int -> r)
forall a r. Show a => Format r (a -> r)
F.shown)
          Format
  (Word -> Int -> r)
  (ActiveAgency' st (StateAgency st)
   -> SingLocalStateQuery st -> Word -> Int -> r)
-> Format r (Word -> Int -> r)
-> Format
     r
     (ActiveAgency' st (StateAgency st)
      -> SingLocalStateQuery st -> Word -> Int -> r)
forall r a r'. Format r a -> Format r' r -> Format r' a
%+ Format (Word -> Int -> r) (Word -> Int -> r)
"unexpected key"
          Format (Word -> Int -> r) (Word -> Int -> r)
-> Format r (Word -> Int -> r) -> Format r (Word -> Int -> r)
forall r a r'. Format r a -> Format r' r -> Format r' a
%+ Format r (Word -> Int -> r) -> Format r (Word -> Int -> r)
forall r a. Format r a -> Format r a
F.parenthesised (Format (Int -> r) (Word -> Int -> r)
forall a r. Integral a => Format r (a -> r)
F.int Format (Int -> r) (Word -> Int -> r)
-> Format r (Int -> r) -> Format r (Word -> Int -> r)
forall r a r'. Format r a -> Format r' r -> Format r' a
F.% Format (Int -> r) (Int -> r)
"," Format (Int -> r) (Int -> r)
-> Format r (Int -> r) -> Format r (Int -> r)
forall r a r'. Format r a -> Format r' r -> Format r' a
%+ Format r (Int -> r)
forall a r. Integral a => Format r (a -> r)
F.int)


-- | An identity 'Codec' for the 'LocalStateQuery' protocol. It does not do
-- any serialisation. It keeps the typed messages, wrapped in 'AnyMessage'.
--
codecLocalStateQueryId
  :: forall (block :: Type) (point :: Type) (query :: Type -> Type) m.
     Monad m
     => (forall (result1 :: Type) (result2 :: Type).
          query result1
       -> query result2
       -> Maybe (result1 :~: result2)
     )
  -> Stateful.Codec (LocalStateQuery block point query)
                    CodecFailure State m
                    (Stateful.AnyMessage (LocalStateQuery block point query) State)
codecLocalStateQueryId :: forall block point (query :: * -> *) (m :: * -> *).
Monad m =>
(forall result1 result2.
 query result1 -> query result2 -> Maybe (result1 :~: result2))
-> Codec
     (LocalStateQuery block point query)
     CodecFailure
     State
     m
     (AnyMessage (LocalStateQuery block point query) State)
codecLocalStateQueryId forall result1 result2.
query result1 -> query result2 -> Maybe (result1 :~: result2)
eqQuery =
   Stateful.Codec { State st
-> Message (LocalStateQuery block point query) st st'
-> AnyMessage (LocalStateQuery block point query) State
forall (st :: LocalStateQuery block point query)
       (st' :: LocalStateQuery block point query).
(ActiveState st, StateTokenI st) =>
State st
-> Message (LocalStateQuery block point query) st st'
-> AnyMessage (LocalStateQuery block point query) State
forall (st :: LocalStateQuery block point query)
       (st' :: LocalStateQuery block point query).
(StateTokenI st, ActiveState st) =>
State st
-> Message (LocalStateQuery block point query) st st'
-> AnyMessage (LocalStateQuery block point query) State
encode :: forall (st :: LocalStateQuery block point query)
       (st' :: LocalStateQuery block point query).
(ActiveState st, StateTokenI st) =>
State st
-> Message (LocalStateQuery block point query) st st'
-> AnyMessage (LocalStateQuery block point query) State
encode :: forall (st :: LocalStateQuery block point query)
       (st' :: LocalStateQuery block point query).
(StateTokenI st, ActiveState st) =>
State st
-> Message (LocalStateQuery block point query) st st'
-> AnyMessage (LocalStateQuery block point query) State
Stateful.encode, StateToken st
-> State st
-> m (DecodeStep
        (AnyMessage (LocalStateQuery block point query) State)
        CodecFailure
        m
        (SomeMessage st))
forall (st :: LocalStateQuery block point query).
ActiveState st =>
StateToken st
-> State st
-> m (DecodeStep
        (AnyMessage (LocalStateQuery block point query) State)
        CodecFailure
        m
        (SomeMessage st))
decode :: forall (st :: LocalStateQuery block point query).
ActiveState st =>
StateToken st
-> State st
-> m (DecodeStep
        (AnyMessage (LocalStateQuery block point query) State)
        CodecFailure
        m
        (SomeMessage st))
decode :: forall (st :: LocalStateQuery block point query).
ActiveState st =>
StateToken st
-> State st
-> m (DecodeStep
        (AnyMessage (LocalStateQuery block point query) State)
        CodecFailure
        m
        (SomeMessage st))
Stateful.decode }
 where
   encode :: forall st st'.
             ActiveState st
          => StateTokenI st
          => State st
          -> Message (LocalStateQuery block point query) st st'
          -> Stateful.AnyMessage (LocalStateQuery block point query) State
   encode :: forall (st :: LocalStateQuery block point query)
       (st' :: LocalStateQuery block point query).
(ActiveState st, StateTokenI st) =>
State st
-> Message (LocalStateQuery block point query) st st'
-> AnyMessage (LocalStateQuery block point query) State
encode = State st
-> Message (LocalStateQuery block point query) st st'
-> AnyMessage (LocalStateQuery block point query) State
forall ps (f :: ps -> *) (st :: ps) (st' :: ps).
(StateTokenI st, ActiveState st) =>
f st -> Message ps st st' -> AnyMessage ps f
Stateful.AnyMessage

   decode :: forall (st :: LocalStateQuery block point query).
             ActiveState st
          => StateToken st
          -> State st
          -> m (DecodeStep (Stateful.AnyMessage (LocalStateQuery block point query) State)
                           CodecFailure m (SomeMessage st))
   decode :: forall (st :: LocalStateQuery block point query).
ActiveState st =>
StateToken st
-> State st
-> m (DecodeStep
        (AnyMessage (LocalStateQuery block point query) State)
        CodecFailure
        m
        (SomeMessage st))
decode StateToken st
stok State st
f = DecodeStep
  (AnyMessage (LocalStateQuery block point query) State)
  CodecFailure
  m
  (SomeMessage st)
-> m (DecodeStep
        (AnyMessage (LocalStateQuery block point query) State)
        CodecFailure
        m
        (SomeMessage st))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (DecodeStep
   (AnyMessage (LocalStateQuery block point query) State)
   CodecFailure
   m
   (SomeMessage st)
 -> m (DecodeStep
         (AnyMessage (LocalStateQuery block point query) State)
         CodecFailure
         m
         (SomeMessage st)))
-> DecodeStep
     (AnyMessage (LocalStateQuery block point query) State)
     CodecFailure
     m
     (SomeMessage st)
-> m (DecodeStep
        (AnyMessage (LocalStateQuery block point query) State)
        CodecFailure
        m
        (SomeMessage st))
forall a b. (a -> b) -> a -> b
$ (Maybe (AnyMessage (LocalStateQuery block point query) State)
 -> m (DecodeStep
         (AnyMessage (LocalStateQuery block point query) State)
         CodecFailure
         m
         (SomeMessage st)))
-> DecodeStep
     (AnyMessage (LocalStateQuery block point query) State)
     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 (LocalStateQuery block point query) State)
  -> m (DecodeStep
          (AnyMessage (LocalStateQuery block point query) State)
          CodecFailure
          m
          (SomeMessage st)))
 -> DecodeStep
      (AnyMessage (LocalStateQuery block point query) State)
      CodecFailure
      m
      (SomeMessage st))
-> (Maybe (AnyMessage (LocalStateQuery block point query) State)
    -> m (DecodeStep
            (AnyMessage (LocalStateQuery block point query) State)
            CodecFailure
            m
            (SomeMessage st)))
-> DecodeStep
     (AnyMessage (LocalStateQuery block point query) State)
     CodecFailure
     m
     (SomeMessage st)
forall a b. (a -> b) -> a -> b
$ \Maybe (AnyMessage (LocalStateQuery block point query) State)
bytes ->
     DecodeStep
  (AnyMessage (LocalStateQuery block point query) State)
  CodecFailure
  m
  (SomeMessage st)
-> m (DecodeStep
        (AnyMessage (LocalStateQuery block point query) State)
        CodecFailure
        m
        (SomeMessage st))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (DecodeStep
   (AnyMessage (LocalStateQuery block point query) State)
   CodecFailure
   m
   (SomeMessage st)
 -> m (DecodeStep
         (AnyMessage (LocalStateQuery block point query) State)
         CodecFailure
         m
         (SomeMessage st)))
-> DecodeStep
     (AnyMessage (LocalStateQuery block point query) State)
     CodecFailure
     m
     (SomeMessage st)
-> m (DecodeStep
        (AnyMessage (LocalStateQuery block point query) State)
        CodecFailure
        m
        (SomeMessage st))
forall a b. (a -> b) -> a -> b
$ case (StateToken st
SingLocalStateQuery st
stok, State st
f, Maybe (AnyMessage (LocalStateQuery block point query) State)
bytes) of
       (SingLocalStateQuery st
SingIdle,       State st
_, Just (Stateful.AnyMessage State st
_ msg :: Message (LocalStateQuery block point query) st st'
msg@(MsgAcquire{})))   -> SomeMessage st
-> Maybe (AnyMessage (LocalStateQuery block point query) State)
-> DecodeStep
     (AnyMessage (LocalStateQuery block point query) State)
     CodecFailure
     m
     (SomeMessage st)
forall bytes failure (m :: * -> *) a.
a -> Maybe bytes -> DecodeStep bytes failure m a
DecodeDone (Message (LocalStateQuery block point query) st st'
-> SomeMessage st
forall ps (st :: ps) (st' :: ps).
(StateTokenI st, StateTokenI st', ActiveState st) =>
Message ps st st' -> SomeMessage st
SomeMessage Message (LocalStateQuery block point query) st st'
Message (LocalStateQuery block point query) st st'
msg) Maybe (AnyMessage (LocalStateQuery block point query) State)
forall a. Maybe a
Nothing
       (SingLocalStateQuery st
SingIdle,       State st
_, Just (Stateful.AnyMessage State st
_ msg :: Message (LocalStateQuery block point query) st st'
msg@(MsgDone{})))      -> SomeMessage st
-> Maybe (AnyMessage (LocalStateQuery block point query) State)
-> DecodeStep
     (AnyMessage (LocalStateQuery block point query) State)
     CodecFailure
     m
     (SomeMessage st)
forall bytes failure (m :: * -> *) a.
a -> Maybe bytes -> DecodeStep bytes failure m a
DecodeDone (Message (LocalStateQuery block point query) st st'
-> SomeMessage st
forall ps (st :: ps) (st' :: ps).
(StateTokenI st, StateTokenI st', ActiveState st) =>
Message ps st st' -> SomeMessage st
SomeMessage Message (LocalStateQuery block point query) st st'
Message (LocalStateQuery block point query) st st'
msg) Maybe (AnyMessage (LocalStateQuery block point query) State)
forall a. Maybe a
Nothing
       (SingLocalStateQuery st
SingAcquired,   State st
_, Just (Stateful.AnyMessage State st
_ msg :: Message (LocalStateQuery block point query) st st'
msg@(MsgQuery{})))     -> SomeMessage st
-> Maybe (AnyMessage (LocalStateQuery block point query) State)
-> DecodeStep
     (AnyMessage (LocalStateQuery block point query) State)
     CodecFailure
     m
     (SomeMessage st)
forall bytes failure (m :: * -> *) a.
a -> Maybe bytes -> DecodeStep bytes failure m a
DecodeDone (Message (LocalStateQuery block point query) st st'
-> SomeMessage st
forall ps (st :: ps) (st' :: ps).
(StateTokenI st, StateTokenI st', ActiveState st) =>
Message ps st st' -> SomeMessage st
SomeMessage Message (LocalStateQuery block point query) st st'
Message (LocalStateQuery block point query) st st'
msg) Maybe (AnyMessage (LocalStateQuery block point query) State)
forall a. Maybe a
Nothing
       (SingLocalStateQuery st
SingAcquired,   State st
_, Just (Stateful.AnyMessage State st
_ msg :: Message (LocalStateQuery block point query) st st'
msg@(MsgReAcquire{}))) -> SomeMessage st
-> Maybe (AnyMessage (LocalStateQuery block point query) State)
-> DecodeStep
     (AnyMessage (LocalStateQuery block point query) State)
     CodecFailure
     m
     (SomeMessage st)
forall bytes failure (m :: * -> *) a.
a -> Maybe bytes -> DecodeStep bytes failure m a
DecodeDone (Message (LocalStateQuery block point query) st st'
-> SomeMessage st
forall ps (st :: ps) (st' :: ps).
(StateTokenI st, StateTokenI st', ActiveState st) =>
Message ps st st' -> SomeMessage st
SomeMessage Message (LocalStateQuery block point query) st st'
Message (LocalStateQuery block point query) st st'
msg) Maybe (AnyMessage (LocalStateQuery block point query) State)
forall a. Maybe a
Nothing
       (SingLocalStateQuery st
SingAcquired,   State st
_, Just (Stateful.AnyMessage State st
_ msg :: Message (LocalStateQuery block point query) st st'
msg@(MsgRelease{})))   -> SomeMessage st
-> Maybe (AnyMessage (LocalStateQuery block point query) State)
-> DecodeStep
     (AnyMessage (LocalStateQuery block point query) State)
     CodecFailure
     m
     (SomeMessage st)
forall bytes failure (m :: * -> *) a.
a -> Maybe bytes -> DecodeStep bytes failure m a
DecodeDone (Message (LocalStateQuery block point query) st st'
-> SomeMessage st
forall ps (st :: ps) (st' :: ps).
(StateTokenI st, StateTokenI st', ActiveState st) =>
Message ps st st' -> SomeMessage st
SomeMessage Message (LocalStateQuery block point query) st st'
Message (LocalStateQuery block point query) st st'
msg) Maybe (AnyMessage (LocalStateQuery block point query) State)
forall a. Maybe a
Nothing
       (SingLocalStateQuery st
SingAcquiring,  State st
_, Just (Stateful.AnyMessage State st
_ msg :: Message (LocalStateQuery block point query) st st'
msg@(MsgAcquired{})))  -> SomeMessage st
-> Maybe (AnyMessage (LocalStateQuery block point query) State)
-> DecodeStep
     (AnyMessage (LocalStateQuery block point query) State)
     CodecFailure
     m
     (SomeMessage st)
forall bytes failure (m :: * -> *) a.
a -> Maybe bytes -> DecodeStep bytes failure m a
DecodeDone (Message (LocalStateQuery block point query) st st'
-> SomeMessage st
forall ps (st :: ps) (st' :: ps).
(StateTokenI st, StateTokenI st', ActiveState st) =>
Message ps st st' -> SomeMessage st
SomeMessage Message (LocalStateQuery block point query) st st'
Message (LocalStateQuery block point query) st st'
msg) Maybe (AnyMessage (LocalStateQuery block point query) State)
forall a. Maybe a
Nothing
       (SingLocalStateQuery st
SingAcquiring,  State st
_, Just (Stateful.AnyMessage State st
_ msg :: Message (LocalStateQuery block point query) st st'
msg@(MsgFailure{})))   -> SomeMessage st
-> Maybe (AnyMessage (LocalStateQuery block point query) State)
-> DecodeStep
     (AnyMessage (LocalStateQuery block point query) State)
     CodecFailure
     m
     (SomeMessage st)
forall bytes failure (m :: * -> *) a.
a -> Maybe bytes -> DecodeStep bytes failure m a
DecodeDone (Message (LocalStateQuery block point query) st st'
-> SomeMessage st
forall ps (st :: ps) (st' :: ps).
(StateTokenI st, StateTokenI st', ActiveState st) =>
Message ps st st' -> SomeMessage st
SomeMessage Message (LocalStateQuery block point query) st st'
Message (LocalStateQuery block point query) st st'
msg) Maybe (AnyMessage (LocalStateQuery block point query) State)
forall a. Maybe a
Nothing
       (SingLocalStateQuery st
SingQuerying,  StateQuerying query result
q, Just (Stateful.AnyMessage (StateQuerying query result
q') msg :: Message (LocalStateQuery block point query) st st'
msg@(MsgResult result
_)))
            |  Just result :~: result
Refl <- query result
q query result -> query result -> Maybe (result :~: result)
forall result1 result2.
query result1 -> query result2 -> Maybe (result1 :~: result2)
`eqQuery` query result
q'
            -> SomeMessage st
-> Maybe (AnyMessage (LocalStateQuery block point query) State)
-> DecodeStep
     (AnyMessage (LocalStateQuery block point query) State)
     CodecFailure
     m
     (SomeMessage st)
forall bytes failure (m :: * -> *) a.
a -> Maybe bytes -> DecodeStep bytes failure m a
DecodeDone (Message (LocalStateQuery block point query) st st'
-> SomeMessage st
forall ps (st :: ps) (st' :: ps).
(StateTokenI st, StateTokenI st', ActiveState st) =>
Message ps st st' -> SomeMessage st
SomeMessage Message (LocalStateQuery block point query) st st'
Message (LocalStateQuery block point query) st st'
msg) Maybe (AnyMessage (LocalStateQuery block point query) State)
forall a. Maybe a
Nothing
       (SingLocalStateQuery st
SingDone, State st
_, Maybe (AnyMessage (LocalStateQuery block point query) State)
_) -> 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
       (SingLocalStateQuery st
_, State st
_, Maybe (AnyMessage (LocalStateQuery block point query) State)
Nothing) -> CodecFailure
-> DecodeStep
     (AnyMessage (LocalStateQuery block point query) State)
     CodecFailure
     m
     (SomeMessage st)
forall bytes failure (m :: * -> *) a.
failure -> DecodeStep bytes failure m a
DecodeFail CodecFailure
CodecFailureOutOfInput
       (SingLocalStateQuery st
_, State st
_, Maybe (AnyMessage (LocalStateQuery block point query) State)
_)       -> CodecFailure
-> DecodeStep
     (AnyMessage (LocalStateQuery block point query) State)
     CodecFailure
     m
     (SomeMessage st)
forall bytes failure (m :: * -> *) a.
failure -> DecodeStep bytes failure m a
DecodeFail (String -> CodecFailure
CodecFailure String
failmsg)

   failmsg :: String
failmsg = String
"codecLocalStateQueryId: no matching message"