{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE EmptyCase             #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE UndecidableInstances  #-}

-- | The type of the local ledger state query protocol.
--
-- This is used by local clients (like wallets and CLI tools) to query the
-- ledger state of a local node.
--
module Ouroboros.Network.Protocol.LocalStateQuery.Type where

import           Data.Kind (Type)
import           Data.Proxy (Proxy (..))

import           Network.TypedProtocol.Core

import           Ouroboros.Network.Util.ShowProxy (ShowProxy (..))


-- | The kind of the local state query protocol, and the types of
-- the states in the protocol state machine.
--
-- It is parametrised over the type of block (for points), the type of queries
-- and query results.
--
data LocalStateQuery block point (query :: Type -> Type) where

  -- | The client has agency. It can ask to acquire a state or terminate.
  --
  -- There is no timeout in this state.
  --
  StIdle :: LocalStateQuery block point query

  -- | The server has agency. it must acquire the state at the requested point
  -- or report a failure.
  --
  -- There is a timeout in this state.
  --
  StAcquiring :: LocalStateQuery block point query

  -- | The client has agency. It can request queries against the current state,
  -- or it can release the state.
  --
  StAcquired :: LocalStateQuery block point query

  -- | The server has agency. It must respond with the query result.
  --
  StQuerying :: result -> LocalStateQuery block point query

  -- | Nobody has agency. The terminal state.
  --
  StDone :: LocalStateQuery block point query

instance ( ShowProxy block
         , ShowProxy query
         ) => ShowProxy (LocalStateQuery block point query) where
    showProxy :: Proxy (LocalStateQuery block point query) -> String
showProxy Proxy (LocalStateQuery block point query)
_ = [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
      [ String
"LocalStateQuery "
      , Proxy block -> String
forall k (p :: k). ShowProxy p => Proxy p -> String
showProxy (Proxy block
forall k (t :: k). Proxy t
Proxy :: Proxy block)
      , String
" "
      , Proxy query -> String
forall k (p :: k). ShowProxy p => Proxy p -> String
showProxy (Proxy query
forall k (t :: k). Proxy t
Proxy :: Proxy query)
      ]

instance Protocol (LocalStateQuery block point query) where

  -- | The messages in the state query protocol.
  --
  -- The pattern of use is to
  --
  data Message (LocalStateQuery block point query) from to where

    -- | The client requests that the state as of a particular recent point on
    -- the server's chain (within K of the tip) be made available to query,
    -- and waits for confirmation or failure.
    --
    -- From 'NodeToClient_V8' onwards if the point is not specified, current tip
    -- will be acquired.  For previous versions of the protocol 'point' must be
    -- given.
    --
    MsgAcquire
      :: Maybe point
      -> Message (LocalStateQuery block point query) StIdle StAcquiring

    -- | The server can confirm that it has the state at the requested point.
    --
    MsgAcquired
      :: Message (LocalStateQuery block point query) StAcquiring StAcquired

    -- | The server can report that it cannot obtain the state for the
    -- requested point.
    --
    MsgFailure
      :: AcquireFailure
      -> Message (LocalStateQuery block point query) StAcquiring StIdle

    -- | The client can perform queries on the current acquired state.
    --
    MsgQuery
      :: query result
      -> Message (LocalStateQuery block point query) StAcquired (StQuerying result)

    -- | The server must reply with the queries.
    --
    MsgResult
      :: query result
         -- ^ The query will not be sent across the network, it is solely used
         -- as evidence that @result@ is a valid type index of @query@.
      -> result
      -> Message (LocalStateQuery block point query) (StQuerying result) StAcquired

    -- | The client can instruct the server to release the state. This lets
    -- the server free resources.
    --
    MsgRelease
      :: Message (LocalStateQuery block point query) StAcquired StIdle

    -- | This is like 'MsgAcquire' but for when the client already has a
    -- state. By moveing to another state directly without a 'MsgRelease' it
    -- enables optimisations on the server side (e.g. moving to the state for
    -- the immediate next block).
    --
    -- Note that failure to re-acquire is equivalent to 'MsgRelease',
    -- rather than keeping the exiting acquired state.
    --
    -- From 'NodeToClient_V8' onwards if the point is not specified, current tip
    -- will be acquired.  For previous versions of the protocol 'point' must be
    -- given.
    --
    MsgReAcquire
      :: Maybe point
      -> Message (LocalStateQuery block point query) StAcquired StAcquiring

    -- | The client can terminate the protocol.
    --
    MsgDone
      :: Message (LocalStateQuery block point query) StIdle StDone


  data ClientHasAgency st where
    TokIdle      :: ClientHasAgency StIdle
    TokAcquired  :: ClientHasAgency StAcquired

  data ServerHasAgency st where
    TokAcquiring  :: ServerHasAgency StAcquiring
    TokQuerying   :: query result
                  -> ServerHasAgency (StQuerying result :: LocalStateQuery block point query)

  data NobodyHasAgency st where
    TokDone  :: NobodyHasAgency StDone

  exclusionLemma_ClientAndServerHaveAgency :: ClientHasAgency st -> ServerHasAgency st -> Void
exclusionLemma_ClientAndServerHaveAgency ClientHasAgency st
TokIdle     ServerHasAgency st
tok = case ServerHasAgency st
tok of {}
  exclusionLemma_ClientAndServerHaveAgency ClientHasAgency st
TokAcquired ServerHasAgency st
tok = case ServerHasAgency st
tok of {}

  exclusionLemma_NobodyAndClientHaveAgency :: NobodyHasAgency st -> ClientHasAgency st -> Void
exclusionLemma_NobodyAndClientHaveAgency NobodyHasAgency st
TokDone ClientHasAgency st
tok = case ClientHasAgency st
tok of {}

  exclusionLemma_NobodyAndServerHaveAgency :: NobodyHasAgency st -> ServerHasAgency st -> Void
exclusionLemma_NobodyAndServerHaveAgency NobodyHasAgency st
TokDone ServerHasAgency st
tok = case ServerHasAgency st
tok of {}


data AcquireFailure = AcquireFailurePointTooOld
                    | AcquireFailurePointNotOnChain
  deriving (AcquireFailure -> AcquireFailure -> Bool
(AcquireFailure -> AcquireFailure -> Bool)
-> (AcquireFailure -> AcquireFailure -> Bool) -> Eq AcquireFailure
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: AcquireFailure -> AcquireFailure -> Bool
$c/= :: AcquireFailure -> AcquireFailure -> Bool
== :: AcquireFailure -> AcquireFailure -> Bool
$c== :: AcquireFailure -> AcquireFailure -> Bool
Eq, Int -> AcquireFailure
AcquireFailure -> Int
AcquireFailure -> [AcquireFailure]
AcquireFailure -> AcquireFailure
AcquireFailure -> AcquireFailure -> [AcquireFailure]
AcquireFailure
-> AcquireFailure -> AcquireFailure -> [AcquireFailure]
(AcquireFailure -> AcquireFailure)
-> (AcquireFailure -> AcquireFailure)
-> (Int -> AcquireFailure)
-> (AcquireFailure -> Int)
-> (AcquireFailure -> [AcquireFailure])
-> (AcquireFailure -> AcquireFailure -> [AcquireFailure])
-> (AcquireFailure -> AcquireFailure -> [AcquireFailure])
-> (AcquireFailure
    -> AcquireFailure -> AcquireFailure -> [AcquireFailure])
-> Enum AcquireFailure
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: AcquireFailure
-> AcquireFailure -> AcquireFailure -> [AcquireFailure]
$cenumFromThenTo :: AcquireFailure
-> AcquireFailure -> AcquireFailure -> [AcquireFailure]
enumFromTo :: AcquireFailure -> AcquireFailure -> [AcquireFailure]
$cenumFromTo :: AcquireFailure -> AcquireFailure -> [AcquireFailure]
enumFromThen :: AcquireFailure -> AcquireFailure -> [AcquireFailure]
$cenumFromThen :: AcquireFailure -> AcquireFailure -> [AcquireFailure]
enumFrom :: AcquireFailure -> [AcquireFailure]
$cenumFrom :: AcquireFailure -> [AcquireFailure]
fromEnum :: AcquireFailure -> Int
$cfromEnum :: AcquireFailure -> Int
toEnum :: Int -> AcquireFailure
$ctoEnum :: Int -> AcquireFailure
pred :: AcquireFailure -> AcquireFailure
$cpred :: AcquireFailure -> AcquireFailure
succ :: AcquireFailure -> AcquireFailure
$csucc :: AcquireFailure -> AcquireFailure
Enum, Int -> AcquireFailure -> ShowS
[AcquireFailure] -> ShowS
AcquireFailure -> String
(Int -> AcquireFailure -> ShowS)
-> (AcquireFailure -> String)
-> ([AcquireFailure] -> ShowS)
-> Show AcquireFailure
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [AcquireFailure] -> ShowS
$cshowList :: [AcquireFailure] -> ShowS
show :: AcquireFailure -> String
$cshow :: AcquireFailure -> String
showsPrec :: Int -> AcquireFailure -> ShowS
$cshowsPrec :: Int -> AcquireFailure -> ShowS
Show)

instance Show (ClientHasAgency (st :: LocalStateQuery block point query)) where
  show :: ClientHasAgency st -> String
show ClientHasAgency st
TokIdle     = String
"TokIdle"
  show ClientHasAgency st
TokAcquired = String
"TokAcquired"

instance (forall result. Show (query result))
    => Show (ServerHasAgency (st :: LocalStateQuery block point query)) where
  show :: ServerHasAgency st -> String
show ServerHasAgency st
TokAcquiring        = String
"TokAcquiring"
  show (TokQuerying query) = String
"TokQuerying " String -> ShowS
forall a. [a] -> [a] -> [a]
++ query result -> String
forall a. Show a => a -> String
show query result
query

-- | To implement 'Show' for:
--
-- > ('Message' ('LocalStateQuery' block query) st st')
--
-- we need a way to print the @query@ GADT and its type index, @result@. This
-- class contain the method we need to provide this 'Show' instance.
--
-- We use a type class for this, as this 'Show' constraint propagates to a lot
-- of places.
class (forall result. Show (query result)) => ShowQuery query where
    showResult :: forall result. query result -> result -> String

instance (ShowQuery query, Show point)
      => Show (Message (LocalStateQuery block point query) st st') where
  showsPrec :: Int -> Message (LocalStateQuery block point query) st st' -> ShowS
showsPrec Int
p Message (LocalStateQuery block point query) st st'
msg = case Message (LocalStateQuery block point query) st st'
msg of
      MsgAcquire pt -> Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
11) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
        String -> ShowS
showString String
"MsgAcquire " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
        Int -> Maybe point -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 Maybe point
pt
      Message (LocalStateQuery block point query) st st'
MsgAcquired ->
        String -> ShowS
showString String
"MsgAcquired"
      MsgFailure failure -> Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
11) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
        String -> ShowS
showString String
"MsgFailure " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
        Int -> AcquireFailure -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 AcquireFailure
failure
      MsgQuery query -> Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
11) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
        String -> ShowS
showString String
"MsgQuery " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
        Int -> query result -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 query result
query
      MsgResult query result -> Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
11) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
        String -> ShowS
showString String
"MsgResult " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
        Bool -> ShowS -> ShowS
showParen Bool
True (String -> ShowS
showString (query result -> result -> String
forall (query :: * -> *) result.
ShowQuery query =>
query result -> result -> String
showResult query result
query result
result))
      Message (LocalStateQuery block point query) st st'
MsgRelease ->
        String -> ShowS
showString String
"MsgRelease"
      MsgReAcquire pt -> Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
11) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
        String -> ShowS
showString String
"MsgReAcquire " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
        Int -> Maybe point -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 Maybe point
pt
      Message (LocalStateQuery block point query) st st'
MsgDone ->
        String -> ShowS
showString String
"MsgDone"