{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE FlexibleInstances   #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE PolyKinds           #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving  #-}
{-# LANGUAGE TypeFamilies        #-}

-- | The type of the chain synchronisation protocol.
--
-- Since we are using a typed protocol framework this is in some sense /the/
-- definition of the protocol: what is allowed and what is not allowed.
--
module Ouroboros.Network.Protocol.ChainSync.Type where

import Data.Singletons

import Network.TypedProtocol.Core

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


-- | A kind to identify our protocol, and the types of the states in the state
-- transition diagram of the protocol.
--
data ChainSync header point tip where

  -- | Both client and server are idle. The client can send a request and
  -- the server is waiting for a request.
  StIdle      :: ChainSync header point tip

  -- | The client has sent a next update request. The client is now waiting
  -- for a response, and the server is busy getting ready to send a response.
  -- There are two possibilities here, since the server can send a reply
  -- immediately or it can send an initial await message followed later by
  -- the normal reply.
  StNext      :: StNextKind -> ChainSync header point tip

  -- | The client has sent an intersection request. The client is now waiting
  -- for a response, and the server is busy getting ready to send a response.
  StIntersect :: ChainSync header point tip

  -- | Both the client and server are in the terminal state. They're done.
  StDone      :: ChainSync header point tip


instance (ShowProxy header, ShowProxy tip)
      => ShowProxy (ChainSync header point tip) where
    showProxy :: Proxy (ChainSync header point tip) -> String
showProxy Proxy (ChainSync header point tip)
_ = [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
      [ String
"ChainSync ("
      , Proxy header -> String
forall {k} (p :: k). ShowProxy p => Proxy p -> String
showProxy (Proxy header
forall {k} (t :: k). Proxy t
Proxy :: Proxy header)
      , String
") ("
      , Proxy tip -> String
forall {k} (p :: k). ShowProxy p => Proxy p -> String
showProxy (Proxy tip
forall {k} (t :: k). Proxy t
Proxy :: Proxy tip)
      , String
")"
      ]


-- | Singletons for 'ChainSync' state types.
--
data SingChainSync (k :: ChainSync header point tip) where
    SingIdle      :: SingChainSync StIdle
    SingNext      :: SingNextKind k
                  -> SingChainSync (StNext k)
    SingIntersect :: SingChainSync StIntersect
    SingDone      :: SingChainSync StDone

deriving instance Show (SingChainSync k)

instance StateTokenI StIdle      where stateToken :: StateToken 'StIdle
stateToken = StateToken 'StIdle
SingChainSync 'StIdle
forall {k} {k} {k} {header :: k} {point :: k} {tip :: k}.
SingChainSync 'StIdle
SingIdle
instance SingI k =>
         StateTokenI (StNext k)  where stateToken :: StateToken ('StNext k)
stateToken = SingNextKind k -> SingChainSync ('StNext k)
forall {k} {k} {k} {header :: k} {point :: k} {tip :: k}
       (k :: StNextKind).
SingNextKind k -> SingChainSync ('StNext k)
SingNext Sing k
SingNextKind k
forall {k} (a :: k). SingI a => Sing a
sing
instance StateTokenI StIntersect where stateToken :: StateToken 'StIntersect
stateToken = StateToken 'StIntersect
SingChainSync 'StIntersect
forall {k} {k} {k} {header :: k} {point :: k} {tip :: k}.
SingChainSync 'StIntersect
SingIntersect
instance StateTokenI StDone      where stateToken :: StateToken 'StDone
stateToken = StateToken 'StDone
SingChainSync 'StDone
forall {k} {k} {k} {header :: k} {point :: k} {tip :: k}.
SingChainSync 'StDone
SingDone


-- | Sub-cases of the 'StNext' state. This is needed since the server can
-- either send one reply back, or two.
--
data StNextKind where
  -- | The server can reply or send an await msg.
  StCanAwait  :: StNextKind
  -- | The server must now reply, having already sent an await message.
  StMustReply :: StNextKind


data SingNextKind (k :: StNextKind) where
  SingCanAwait  :: SingNextKind StCanAwait
  SingMustReply :: SingNextKind StMustReply

deriving instance Show (SingNextKind k)

type instance Sing = SingNextKind
instance SingI StCanAwait  where sing :: Sing 'StCanAwait
sing = Sing 'StCanAwait
SingNextKind 'StCanAwait
SingCanAwait
instance SingI StMustReply where sing :: Sing 'StMustReply
sing = Sing 'StMustReply
SingNextKind 'StMustReply
SingMustReply

instance Protocol (ChainSync header point tip) where

  -- | The messages in the chain sync protocol.
  --
  -- In this protocol the consumer always initiates things and the producer
  -- replies.
  --
  data Message (ChainSync header point tip) from to where

    -- | Request the next update from the producer. The response can be a roll
    -- forward, a roll back or wait.
    --
    MsgRequestNext :: Message (ChainSync header point tip)
                              StIdle (StNext StCanAwait)

    -- | Acknowledge the request but require the consumer to wait for the next
    -- update. This means that the consumer is synced with the producer, and
    -- the producer is waiting for its own chain state to change.
    --
    MsgAwaitReply :: Message (ChainSync header point tip)
                             (StNext StCanAwait) (StNext StMustReply)

    -- | Tell the consumer to extend their chain with the given header.
    --
    -- The message also tells the consumer about the head point of the producer.
    --
    MsgRollForward :: header -> tip
                   -> Message (ChainSync header point tip)
                              (StNext any) StIdle

    -- | Tell the consumer to roll back to a given point on their chain.
    --
    -- The message also tells the consumer about the head point of the producer.
    --
    MsgRollBackward :: point -> tip
                    -> Message (ChainSync header point tip)
                               (StNext any) StIdle

    -- | Ask the producer to try to find an improved intersection point between
    -- the consumer and producer's chains. The consumer sends a sequence of
    -- points and it is up to the producer to find the first intersection point
    -- on its chain and send it back to the consumer.  The list of points should
    -- be ordered by the preference, e.g. highest slot number to lowest.
    --
    MsgFindIntersect :: [point]
                     -> Message (ChainSync header point tip)
                                StIdle StIntersect

    -- | The reply to the consumer about an intersection found.
    -- The consumer can decide weather to send more points.
    --
    -- The message also tells the consumer about the head point of the producer.
    --
    MsgIntersectFound  :: point -> tip
                       -> Message (ChainSync header point tip)
                                  StIntersect StIdle

    -- | The reply to the consumer that no intersection was found: none of the
    -- points the consumer supplied are on the producer chain.
    --
    -- The message also tells the consumer about the head point of the producer.
    --
    MsgIntersectNotFound :: tip
                         -> Message (ChainSync header point tip)
                                    StIntersect StIdle

    -- | Terminating messages
    --
    MsgDone :: Message (ChainSync header point tip)
                       StIdle StDone

  -- | We have to explain to the framework what our states mean, in terms of
  -- which party has agency in each state.
  --
  -- Idle states are where it is for the client to send a message,
  -- busy states are where the server is expected to send a reply.
  --
  type StateAgency StIdle      = ClientAgency
  type StateAgency (StNext _)  = ServerAgency
  type StateAgency StIntersect = ServerAgency
  type StateAgency StDone      = NobodyAgency

  type StateToken = SingChainSync

instance ( NFData header
         , NFData point
         , NFData tip
         ) => NFData (Message (ChainSync header point tip) from to) where
  rnf :: Message (ChainSync header point tip) from to -> ()
rnf Message (ChainSync header point tip) from to
R:MessageChainSyncfromto (*) (*) (*) header point tip from to
MsgRequestNext           = ()
  rnf Message (ChainSync header point tip) from to
R:MessageChainSyncfromto (*) (*) (*) header point tip from to
MsgAwaitReply            = ()
  rnf (MsgRollForward header
h tip
t)     = header -> ()
forall a. NFData a => a -> ()
rnf header
h () -> () -> ()
forall a b. a -> b -> b
`seq` tip -> ()
forall a. NFData a => a -> ()
rnf tip
t
  rnf (MsgRollBackward point
p tip
t)    = point -> ()
forall a. NFData a => a -> ()
rnf point
p () -> () -> ()
forall a b. a -> b -> b
`seq` tip -> ()
forall a. NFData a => a -> ()
rnf tip
t
  rnf (MsgFindIntersect [point]
ps)    = [point] -> ()
forall a. NFData a => a -> ()
rnf [point]
ps
  rnf (MsgIntersectFound point
p tip
t)  = point -> ()
forall a. NFData a => a -> ()
rnf point
p () -> () -> ()
forall a b. a -> b -> b
`seq` tip -> ()
forall a. NFData a => a -> ()
rnf tip
t
  rnf (MsgIntersectNotFound tip
t) = tip -> ()
forall a. NFData a => a -> ()
rnf tip
t
  rnf Message (ChainSync header point tip) from to
R:MessageChainSyncfromto (*) (*) (*) header point tip from to
MsgDone                  = ()

data TokNextKind (k :: StNextKind) where
  TokCanAwait  :: TokNextKind StCanAwait
  TokMustReply :: TokNextKind StMustReply

instance NFData (TokNextKind k) where
  rnf :: TokNextKind k -> ()
rnf TokNextKind k
TokCanAwait  = ()
  rnf TokNextKind k
TokMustReply = ()

instance (Show header, Show point, Show tip)
      => Show (Message (ChainSync header point tip) from to) where
  show :: Message (ChainSync header point tip) from to -> String
show Message (ChainSync header point tip) from to
R:MessageChainSyncfromto (*) (*) (*) header point tip from to
MsgRequestNext             = String
"MsgRequestNext"
  show Message (ChainSync header point tip) from to
R:MessageChainSyncfromto (*) (*) (*) header point tip from to
MsgAwaitReply              = String
"MsgAwaitReply"
  show (MsgRollForward header
h tip
tip)     = String
"MsgRollForward "
                                  String -> ShowS
forall a. [a] -> [a] -> [a]
++ header -> String
forall a. Show a => a -> String
show header
h
                                  String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" "
                                  String -> ShowS
forall a. [a] -> [a] -> [a]
++ tip -> String
forall a. Show a => a -> String
show tip
tip
  show (MsgRollBackward point
p tip
tip)    = String
"MsgRollBackward "
                                  String -> ShowS
forall a. [a] -> [a] -> [a]
++ point -> String
forall a. Show a => a -> String
show point
p
                                  String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" "
                                  String -> ShowS
forall a. [a] -> [a] -> [a]
++ tip -> String
forall a. Show a => a -> String
show tip
tip
  show (MsgFindIntersect [point]
ps)      = String
"MsgFindIntersect " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [point] -> String
forall a. Show a => a -> String
show [point]
ps
  show (MsgIntersectFound point
p tip
tip)  = String
"MsgIntersectFound "
                                  String -> ShowS
forall a. [a] -> [a] -> [a]
++ point -> String
forall a. Show a => a -> String
show point
p
                                  String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" "
                                  String -> ShowS
forall a. [a] -> [a] -> [a]
++ tip -> String
forall a. Show a => a -> String
show tip
tip
  show (MsgIntersectNotFound tip
tip) = String
"MsgIntersectNotFound "
                                  String -> ShowS
forall a. [a] -> [a] -> [a]
++ tip -> String
forall a. Show a => a -> String
show tip
tip
  show MsgDone{}                  = String
"MsgDone"