{-# LANGUAGE DataKinds                #-}
{-# LANGUAGE DeriveAnyClass           #-}
{-# LANGUAGE DeriveGeneric            #-}
{-# LANGUAGE DeriveTraversable        #-}
{-# LANGUAGE EmptyCase                #-}
{-# LANGUAGE FlexibleInstances        #-}
{-# LANGUAGE GADTs                    #-}
{-# LANGUAGE PolyKinds                #-}
{-# LANGUAGE QuantifiedConstraints    #-}
{-# LANGUAGE RankNTypes               #-}
{-# LANGUAGE ScopedTypeVariables      #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# 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.Singletons

import Network.TypedProtocol.Core
import Network.TypedProtocol.Stateful.Codec (AnyMessage (..))

import Control.DeepSeq
import GHC.Generics
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.
--
type LocalStateQuery :: Type           -- ^ block
                     -> Type           -- ^ point
                     -> (Type -> Type) -- ^ query
                     -> Type
data LocalStateQuery block point query 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 :: forall block point query (result :: Type). 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)
      ]


-- | Singletons for 'LocalStateQuery' state types.
--
type SingLocalStateQuery :: forall (block :: Type) (point :: Type) (query :: Type -> Type).
                            LocalStateQuery block point query
                         -> Type
data SingLocalStateQuery k where
    SingIdle      :: SingLocalStateQuery StIdle
    SingAcquiring :: SingLocalStateQuery StAcquiring
    SingAcquired  :: SingLocalStateQuery StAcquired
    SingQuerying  :: forall (block :: Type) (point :: Type) (query :: Type -> Type) (result :: Type).
                     SingLocalStateQuery (StQuerying result
                                            :: LocalStateQuery block point query)
    SingDone      :: SingLocalStateQuery StDone

instance StateTokenI StIdle              where stateToken :: StateToken 'StIdle
stateToken = StateToken 'StIdle
SingLocalStateQuery 'StIdle
forall {block} {point} {query :: * -> *}.
SingLocalStateQuery 'StIdle
SingIdle
instance StateTokenI StAcquiring         where stateToken :: StateToken 'StAcquiring
stateToken = StateToken 'StAcquiring
SingLocalStateQuery 'StAcquiring
forall {block} {point} {query :: * -> *}.
SingLocalStateQuery 'StAcquiring
SingAcquiring
instance StateTokenI StAcquired          where stateToken :: StateToken 'StAcquired
stateToken = StateToken 'StAcquired
SingLocalStateQuery 'StAcquired
forall {block} {point} {query :: * -> *}.
SingLocalStateQuery 'StAcquired
SingAcquired
instance StateTokenI (StQuerying (result :: Type))
                                         where stateToken :: StateToken ('StQuerying result)
stateToken = StateToken ('StQuerying result)
SingLocalStateQuery ('StQuerying result)
forall block point (query :: * -> *) result.
SingLocalStateQuery ('StQuerying result)
SingQuerying
instance StateTokenI StDone              where stateToken :: StateToken 'StDone
stateToken = StateToken 'StDone
SingLocalStateQuery 'StDone
forall {block} {point} {query :: * -> *}.
SingLocalStateQuery 'StDone
SingDone


instance (forall result. Show (query result))
      => Show (SingLocalStateQuery (k :: LocalStateQuery block point query)) where
    show :: SingLocalStateQuery k -> String
show SingLocalStateQuery k
SingIdle      = String
"SingIdle"
    show SingLocalStateQuery k
SingAcquiring = String
"SingAcuiring"
    show SingLocalStateQuery k
SingAcquired  = String
"SingAcquired"
    show SingLocalStateQuery k
SingQuerying  = String
"SingQuerying"
    show SingLocalStateQuery k
SingDone      = String
"SingDone"


data Target point = -- | The tip of the volatile chain
                    --
                    -- Cannot fail to be acquired.
                    VolatileTip
                  | -- | A specified point
                    --
                    -- Fails to be acquired if the point is not between
                    -- 'VolatileTip' and 'ImmutableTip' (inclusive).
                    SpecificPoint point
                    -- | The tip of the immutable chain
                    --
                    -- Cannot fail to be acquired.
                    --
                    -- Requires at least 'NodeToClientV_16'.
                  | ImmutableTip
  deriving (Target point -> Target point -> Bool
(Target point -> Target point -> Bool)
-> (Target point -> Target point -> Bool) -> Eq (Target point)
forall point. Eq point => Target point -> Target point -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall point. Eq point => Target point -> Target point -> Bool
== :: Target point -> Target point -> Bool
$c/= :: forall point. Eq point => Target point -> Target point -> Bool
/= :: Target point -> Target point -> Bool
Eq, (forall m. Monoid m => Target m -> m)
-> (forall m a. Monoid m => (a -> m) -> Target a -> m)
-> (forall m a. Monoid m => (a -> m) -> Target a -> m)
-> (forall a b. (a -> b -> b) -> b -> Target a -> b)
-> (forall a b. (a -> b -> b) -> b -> Target a -> b)
-> (forall b a. (b -> a -> b) -> b -> Target a -> b)
-> (forall b a. (b -> a -> b) -> b -> Target a -> b)
-> (forall a. (a -> a -> a) -> Target a -> a)
-> (forall a. (a -> a -> a) -> Target a -> a)
-> (forall a. Target a -> [a])
-> (forall a. Target a -> Bool)
-> (forall a. Target a -> Int)
-> (forall a. Eq a => a -> Target a -> Bool)
-> (forall a. Ord a => Target a -> a)
-> (forall a. Ord a => Target a -> a)
-> (forall a. Num a => Target a -> a)
-> (forall a. Num a => Target a -> a)
-> Foldable Target
forall a. Eq a => a -> Target a -> Bool
forall a. Num a => Target a -> a
forall a. Ord a => Target a -> a
forall m. Monoid m => Target m -> m
forall a. Target a -> Bool
forall a. Target a -> Int
forall a. Target a -> [a]
forall a. (a -> a -> a) -> Target a -> a
forall m a. Monoid m => (a -> m) -> Target a -> m
forall b a. (b -> a -> b) -> b -> Target a -> b
forall a b. (a -> b -> b) -> b -> Target a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall m. Monoid m => Target m -> m
fold :: forall m. Monoid m => Target m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Target a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Target a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Target a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> Target a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> Target a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Target a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Target a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Target a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Target a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Target a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Target a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> Target a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> Target a -> a
foldr1 :: forall a. (a -> a -> a) -> Target a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Target a -> a
foldl1 :: forall a. (a -> a -> a) -> Target a -> a
$ctoList :: forall a. Target a -> [a]
toList :: forall a. Target a -> [a]
$cnull :: forall a. Target a -> Bool
null :: forall a. Target a -> Bool
$clength :: forall a. Target a -> Int
length :: forall a. Target a -> Int
$celem :: forall a. Eq a => a -> Target a -> Bool
elem :: forall a. Eq a => a -> Target a -> Bool
$cmaximum :: forall a. Ord a => Target a -> a
maximum :: forall a. Ord a => Target a -> a
$cminimum :: forall a. Ord a => Target a -> a
minimum :: forall a. Ord a => Target a -> a
$csum :: forall a. Num a => Target a -> a
sum :: forall a. Num a => Target a -> a
$cproduct :: forall a. Num a => Target a -> a
product :: forall a. Num a => Target a -> a
Foldable, (forall a b. (a -> b) -> Target a -> Target b)
-> (forall a b. a -> Target b -> Target a) -> Functor Target
forall a b. a -> Target b -> Target a
forall a b. (a -> b) -> Target a -> Target b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> Target a -> Target b
fmap :: forall a b. (a -> b) -> Target a -> Target b
$c<$ :: forall a b. a -> Target b -> Target a
<$ :: forall a b. a -> Target b -> Target a
Functor, (forall x. Target point -> Rep (Target point) x)
-> (forall x. Rep (Target point) x -> Target point)
-> Generic (Target point)
forall x. Rep (Target point) x -> Target point
forall x. Target point -> Rep (Target point) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall point x. Rep (Target point) x -> Target point
forall point x. Target point -> Rep (Target point) x
$cfrom :: forall point x. Target point -> Rep (Target point) x
from :: forall x. Target point -> Rep (Target point) x
$cto :: forall point x. Rep (Target point) x -> Target point
to :: forall x. Rep (Target point) x -> Target point
Generic, Eq (Target point)
Eq (Target point) =>
(Target point -> Target point -> Ordering)
-> (Target point -> Target point -> Bool)
-> (Target point -> Target point -> Bool)
-> (Target point -> Target point -> Bool)
-> (Target point -> Target point -> Bool)
-> (Target point -> Target point -> Target point)
-> (Target point -> Target point -> Target point)
-> Ord (Target point)
Target point -> Target point -> Bool
Target point -> Target point -> Ordering
Target point -> Target point -> Target point
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall point. Ord point => Eq (Target point)
forall point. Ord point => Target point -> Target point -> Bool
forall point. Ord point => Target point -> Target point -> Ordering
forall point.
Ord point =>
Target point -> Target point -> Target point
$ccompare :: forall point. Ord point => Target point -> Target point -> Ordering
compare :: Target point -> Target point -> Ordering
$c< :: forall point. Ord point => Target point -> Target point -> Bool
< :: Target point -> Target point -> Bool
$c<= :: forall point. Ord point => Target point -> Target point -> Bool
<= :: Target point -> Target point -> Bool
$c> :: forall point. Ord point => Target point -> Target point -> Bool
> :: Target point -> Target point -> Bool
$c>= :: forall point. Ord point => Target point -> Target point -> Bool
>= :: Target point -> Target point -> Bool
$cmax :: forall point.
Ord point =>
Target point -> Target point -> Target point
max :: Target point -> Target point -> Target point
$cmin :: forall point.
Ord point =>
Target point -> Target point -> Target point
min :: Target point -> Target point -> Target point
Ord, Int -> Target point -> ShowS
[Target point] -> ShowS
Target point -> String
(Int -> Target point -> ShowS)
-> (Target point -> String)
-> ([Target point] -> ShowS)
-> Show (Target point)
forall point. Show point => Int -> Target point -> ShowS
forall point. Show point => [Target point] -> ShowS
forall point. Show point => Target point -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall point. Show point => Int -> Target point -> ShowS
showsPrec :: Int -> Target point -> ShowS
$cshow :: forall point. Show point => Target point -> String
show :: Target point -> String
$cshowList :: forall point. Show point => [Target point] -> ShowS
showList :: [Target point] -> ShowS
Show, Functor Target
Foldable Target
(Functor Target, Foldable Target) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> Target a -> f (Target b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    Target (f a) -> f (Target a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Target a -> m (Target b))
-> (forall (m :: * -> *) a.
    Monad m =>
    Target (m a) -> m (Target a))
-> Traversable Target
forall (t :: * -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => Target (m a) -> m (Target a)
forall (f :: * -> *) a.
Applicative f =>
Target (f a) -> f (Target a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Target a -> m (Target b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Target a -> f (Target b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Target a -> f (Target b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Target a -> f (Target b)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
Target (f a) -> f (Target a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Target (f a) -> f (Target a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Target a -> m (Target b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Target a -> m (Target b)
$csequence :: forall (m :: * -> *) a. Monad m => Target (m a) -> m (Target a)
sequence :: forall (m :: * -> *) a. Monad m => Target (m a) -> m (Target a)
Traversable, Target point -> ()
(Target point -> ()) -> NFData (Target point)
forall point. NFData point => Target point -> ()
forall a. (a -> ()) -> NFData a
$crnf :: forall point. NFData point => Target point -> ()
rnf :: Target point -> ()
NFData)

instance Protocol (LocalStateQuery (block :: Type) (point :: Type) (query :: Type -> Type)) 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 'Target' ledger state on the server's
    -- chain be made available to query, and waits for confirmation or failure.
    --
    MsgAcquire
      :: Target 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
      :: 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 moving 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.
    --
    MsgReAcquire
      :: Target point
      -> Message (LocalStateQuery block point query) StAcquired StAcquiring

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


  type StateAgency StIdle              = ClientAgency
  type StateAgency StAcquired          = ClientAgency
  type StateAgency StAcquiring         = ServerAgency
  type StateAgency (StQuerying result) = ServerAgency
  type StateAgency StDone              = NobodyAgency

  type StateToken = SingLocalStateQuery


instance ( forall result. NFData (query result)
         , NFData point
         )
         => NFData (Message (LocalStateQuery block point query) from to) where
  rnf :: Message (LocalStateQuery block point query) from to -> ()
rnf (MsgAcquire Target point
mbPoint)   = Target point -> ()
forall a. NFData a => a -> ()
rnf Target point
mbPoint
  rnf Message (LocalStateQuery block point query) from to
R:MessageLocalStateQueryfromto block point query from to
MsgAcquired            = ()
  rnf (MsgFailure AcquireFailure
af)        = AcquireFailure -> ()
forall a. NFData a => a -> ()
rnf AcquireFailure
af
  rnf (MsgQuery query result
qr)          = query result -> ()
forall a. NFData a => a -> ()
rnf query result
qr
  rnf (MsgResult result
r)          = result -> ()
forall a. a -> ()
rwhnf result
r
  rnf Message (LocalStateQuery block point query) from to
R:MessageLocalStateQueryfromto block point query from to
MsgRelease             = ()
  rnf (MsgReAcquire Target point
mbPoint) = Target point -> ()
forall a. NFData a => a -> ()
rnf Target point
mbPoint
  rnf Message (LocalStateQuery block point query) from to
R:MessageLocalStateQueryfromto block point query from to
MsgDone                = ()

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
$c== :: AcquireFailure -> AcquireFailure -> Bool
== :: AcquireFailure -> AcquireFailure -> Bool
$c/= :: AcquireFailure -> AcquireFailure -> Bool
/= :: 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
$csucc :: AcquireFailure -> AcquireFailure
succ :: AcquireFailure -> AcquireFailure
$cpred :: AcquireFailure -> AcquireFailure
pred :: AcquireFailure -> AcquireFailure
$ctoEnum :: Int -> AcquireFailure
toEnum :: Int -> AcquireFailure
$cfromEnum :: AcquireFailure -> Int
fromEnum :: AcquireFailure -> Int
$cenumFrom :: AcquireFailure -> [AcquireFailure]
enumFrom :: AcquireFailure -> [AcquireFailure]
$cenumFromThen :: AcquireFailure -> AcquireFailure -> [AcquireFailure]
enumFromThen :: AcquireFailure -> AcquireFailure -> [AcquireFailure]
$cenumFromTo :: AcquireFailure -> AcquireFailure -> [AcquireFailure]
enumFromTo :: AcquireFailure -> AcquireFailure -> [AcquireFailure]
$cenumFromThenTo :: AcquireFailure
-> AcquireFailure -> AcquireFailure -> [AcquireFailure]
enumFromThenTo :: AcquireFailure
-> AcquireFailure -> 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
$cshowsPrec :: Int -> AcquireFailure -> ShowS
showsPrec :: Int -> AcquireFailure -> ShowS
$cshow :: AcquireFailure -> String
show :: AcquireFailure -> String
$cshowList :: [AcquireFailure] -> ShowS
showList :: [AcquireFailure] -> ShowS
Show, (forall x. AcquireFailure -> Rep AcquireFailure x)
-> (forall x. Rep AcquireFailure x -> AcquireFailure)
-> Generic AcquireFailure
forall x. Rep AcquireFailure x -> AcquireFailure
forall x. AcquireFailure -> Rep AcquireFailure x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. AcquireFailure -> Rep AcquireFailure x
from :: forall x. AcquireFailure -> Rep AcquireFailure x
$cto :: forall x. Rep AcquireFailure x -> AcquireFailure
to :: forall x. Rep AcquireFailure x -> AcquireFailure
Generic, AcquireFailure -> ()
(AcquireFailure -> ()) -> NFData AcquireFailure
forall a. (a -> ()) -> NFData a
$crnf :: AcquireFailure -> ()
rnf :: AcquireFailure -> ()
NFData)


-- | 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 (AnyMessage (LocalStateQuery block point query) State) where
  showsPrec :: Int
-> AnyMessage (LocalStateQuery block point query) State -> ShowS
showsPrec Int
p AnyMessage (LocalStateQuery block point query) State
msg = case AnyMessage (LocalStateQuery block point query) State
msg of
      AnyMessage State st
_f (MsgAcquire Target point
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 -> Target point -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 Target point
pt
      AnyMessage State st
_f Message (LocalStateQuery block point query) st st'
R:MessageLocalStateQueryfromto block point query st st'
MsgAcquired ->
        String -> ShowS
showString String
"MsgAcquired"
      AnyMessage State st
_f (MsgFailure AcquireFailure
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
      AnyMessage State st
_f (MsgQuery query result
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
      AnyMessage (StateQuerying query result
query) (MsgResult result
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 result. query result -> result -> String
forall (query :: * -> *) result.
ShowQuery query =>
query result -> result -> String
showResult query result
query result
result
result))
      AnyMessage State st
_f Message (LocalStateQuery block point query) st st'
R:MessageLocalStateQueryfromto block point query st st'
MsgRelease ->
        String -> ShowS
showString String
"MsgRelease"
      AnyMessage State st
_f (MsgReAcquire Target point
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 -> Target point -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 Target point
pt
      AnyMessage State st
_f Message (LocalStateQuery block point query) st st'
R:MessageLocalStateQueryfromto block point query st st'
MsgDone ->
        String -> ShowS
showString String
"MsgDone"


type State :: LocalStateQuery block point query -> Type
data State st where
    StateIdle      :: State StIdle
    StateAcquiring :: State StAcquiring
    StateAcquired  :: State StAcquired
    StateQuerying  :: query result
                    -> State (StQuerying result :: LocalStateQuery block point query)
    StateDone      :: State StDone

instance Show (State st) where
    show :: State st -> String
show State st
StateIdle         = String
"StateIdle"
    show State st
StateAcquiring    = String
"StateAcquiring"
    show State st
StateAcquired     = String
"StateAcquired"
    show (StateQuerying query result
_) = String
"StateQuerying *"
    show State st
StateDone         = String
"StateDone"