{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}

module Ouroboros.Consensus.HardFork.Combinator.State.Types (
    -- * Main types
    Current (..)
  , HardForkState (..)
  , Past (..)
  , sequenceHardForkState
    -- * Supporting types
  , CrossEraForecaster (..)
  , TransitionInfo (..)
  , Translate (..)
  ) where

import           Control.Monad.Except
import           Data.SOP.BasicFunctors
import           Data.SOP.Constraint
import           Data.SOP.Strict
import           Data.SOP.Telescope (Telescope)
import qualified Data.SOP.Telescope as Telescope
import           GHC.Generics (Generic)
import           NoThunks.Class (NoThunks (..))
import           Ouroboros.Consensus.Block
import           Ouroboros.Consensus.Forecast
import           Ouroboros.Consensus.HardFork.History (Bound)
import           Prelude

{-------------------------------------------------------------------------------
  Types
-------------------------------------------------------------------------------}

-- | Generic hard fork state
--
-- This is used both for the consensus state and the ledger state.
--
-- By using a telescope with @f ~ LedgerState@, we will keep track of 'Past'
-- information for eras before the current one:
--
-- > TZ currentByronState
-- > TZ pastByronState $ TZ currentShelleyState
-- > TZ pastByronState $ TS pastShelleyState $ TZ currentAllegraState
-- > ...
--
-- These are some intuitions on how the Telescope operations behave for this
-- type:
--
-- = @extend@
--
-- Suppose we have a telescope containing the ledger state. The "how to extend"
-- argument would take, say, the final Byron state to the initial Shelley state;
-- and "where to extend from" argument would indicate when we want to extend:
-- when the current slot number has gone past the end of the Byron era.
--
-- = @retract@
--
-- Suppose we have a telescope containing the consensus state. When we rewind
-- the consensus state, we might cross a hard fork transition point. So we first
-- /retract/ the telescope /to/ the era containing the slot number that we want
-- to rewind to, and only then call 'rewindChainDepState' on that era. Of course,
-- retraction may fail (we might not /have/ past consensus state to rewind to
-- anymore); this failure would require a choice for a particular monad @m@.
--
-- = @align@
--
-- Suppose we have one telescope containing the already-ticked ledger state, and
-- another telescope containing the consensus state. Since the ledger state has
-- already been ticked, it might have been advanced to the next era. If this
-- happens, we should then align the consensus state with the ledger state,
-- moving /it/ also to the next era, before we can do the consensus header
-- validation check. Note that in this particular example, the ledger state will
-- always be ahead of the consensus state, never behind; 'alignExtend' can be
-- used in this case.
newtype HardForkState f xs = HardForkState {
      forall (f :: * -> *) (xs :: [*]).
HardForkState f xs -> Telescope (K Past) (Current f) xs
getHardForkState :: Telescope (K Past) (Current f) xs
    }

-- | Information about the current era
data Current f blk = Current {
      forall (f :: * -> *) blk. Current f blk -> Bound
currentStart :: !Bound
    , forall (f :: * -> *) blk. Current f blk -> f blk
currentState :: !(f blk)
    }
  deriving ((forall x. Current f blk -> Rep (Current f blk) x)
-> (forall x. Rep (Current f blk) x -> Current f blk)
-> Generic (Current f blk)
forall x. Rep (Current f blk) x -> Current f blk
forall x. Current f blk -> Rep (Current f blk) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (f :: * -> *) blk x. Rep (Current f blk) x -> Current f blk
forall (f :: * -> *) blk x. Current f blk -> Rep (Current f blk) x
$cfrom :: forall (f :: * -> *) blk x. Current f blk -> Rep (Current f blk) x
from :: forall x. Current f blk -> Rep (Current f blk) x
$cto :: forall (f :: * -> *) blk x. Rep (Current f blk) x -> Current f blk
to :: forall x. Rep (Current f blk) x -> Current f blk
Generic)

-- | Information about a past era
data Past = Past {
      Past -> Bound
pastStart :: !Bound
    , Past -> Bound
pastEnd   :: !Bound
    }
  deriving (Past -> Past -> Bool
(Past -> Past -> Bool) -> (Past -> Past -> Bool) -> Eq Past
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Past -> Past -> Bool
== :: Past -> Past -> Bool
$c/= :: Past -> Past -> Bool
/= :: Past -> Past -> Bool
Eq, Int -> Past -> ShowS
[Past] -> ShowS
Past -> String
(Int -> Past -> ShowS)
-> (Past -> String) -> ([Past] -> ShowS) -> Show Past
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Past -> ShowS
showsPrec :: Int -> Past -> ShowS
$cshow :: Past -> String
show :: Past -> String
$cshowList :: [Past] -> ShowS
showList :: [Past] -> ShowS
Show, (forall x. Past -> Rep Past x)
-> (forall x. Rep Past x -> Past) -> Generic Past
forall x. Rep Past x -> Past
forall x. Past -> Rep Past x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Past -> Rep Past x
from :: forall x. Past -> Rep Past x
$cto :: forall x. Rep Past x -> Past
to :: forall x. Rep Past x -> Past
Generic, Context -> Past -> IO (Maybe ThunkInfo)
Proxy Past -> String
(Context -> Past -> IO (Maybe ThunkInfo))
-> (Context -> Past -> IO (Maybe ThunkInfo))
-> (Proxy Past -> String)
-> NoThunks Past
forall a.
(Context -> a -> IO (Maybe ThunkInfo))
-> (Context -> a -> IO (Maybe ThunkInfo))
-> (Proxy a -> String)
-> NoThunks a
$cnoThunks :: Context -> Past -> IO (Maybe ThunkInfo)
noThunks :: Context -> Past -> IO (Maybe ThunkInfo)
$cwNoThunks :: Context -> Past -> IO (Maybe ThunkInfo)
wNoThunks :: Context -> Past -> IO (Maybe ThunkInfo)
$cshowTypeOf :: Proxy Past -> String
showTypeOf :: Proxy Past -> String
NoThunks)

-- | Thin wrapper around 'Telescope.sequence'
sequenceHardForkState :: forall m f xs. (All Top xs, Functor m)
                      => HardForkState (m :.: f) xs -> m (HardForkState f xs)
sequenceHardForkState :: forall (m :: * -> *) (f :: * -> *) (xs :: [*]).
(All Top xs, Functor m) =>
HardForkState (m :.: f) xs -> m (HardForkState f xs)
sequenceHardForkState (HardForkState Telescope (K Past) (Current (m :.: f)) xs
tel) =
      (Telescope (K Past) (Current f) xs -> HardForkState f xs)
-> m (Telescope (K Past) (Current f) xs) -> m (HardForkState f xs)
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Telescope (K Past) (Current f) xs -> HardForkState f xs
forall (f :: * -> *) (xs :: [*]).
Telescope (K Past) (Current f) xs -> HardForkState f xs
HardForkState
    (m (Telescope (K Past) (Current f) xs) -> m (HardForkState f xs))
-> m (Telescope (K Past) (Current f) xs) -> m (HardForkState f xs)
forall a b. (a -> b) -> a -> b
$ Telescope (K Past) (m :.: Current f) xs
-> m (Telescope (K Past) (Current f) xs)
forall {k} (m :: * -> *) (g :: k -> *) (f :: k -> *) (xs :: [k]).
Functor m =>
Telescope g (m :.: f) xs -> m (Telescope g f xs)
Telescope.sequence
    (Telescope (K Past) (m :.: Current f) xs
 -> m (Telescope (K Past) (Current f) xs))
-> Telescope (K Past) (m :.: Current f) xs
-> m (Telescope (K Past) (Current f) xs)
forall a b. (a -> b) -> a -> b
$ (forall a. Current (m :.: f) a -> (:.:) m (Current f) a)
-> Telescope (K Past) (Current (m :.: f)) xs
-> Telescope (K Past) (m :.: Current f) xs
forall {k} {l} (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
       (f' :: k -> *).
(SListIN (Prod h) xs, HAp h) =>
(forall (a :: k). f a -> f' a) -> h f xs -> h f' xs
hmap Current (m :.: f) a -> (:.:) m (Current f) a
forall a. Current (m :.: f) a -> (:.:) m (Current f) a
sequenceCurrent Telescope (K Past) (Current (m :.: f)) xs
tel
  where
    sequenceCurrent :: Current (m :.: f) a -> (m :.: Current f) a
    sequenceCurrent :: forall a. Current (m :.: f) a -> (:.:) m (Current f) a
sequenceCurrent (Current Bound
start (:.:) m f a
state) =
      m (Current f a) -> (:.:) m (Current f) a
forall l k (f :: l -> *) (g :: k -> l) (p :: k).
f (g p) -> (:.:) f g p
Comp (m (Current f a) -> (:.:) m (Current f) a)
-> m (Current f a) -> (:.:) m (Current f) a
forall a b. (a -> b) -> a -> b
$ Bound -> f a -> Current f a
forall (f :: * -> *) blk. Bound -> f blk -> Current f blk
Current Bound
start (f a -> Current f a) -> m (f a) -> m (Current f a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (:.:) m f a -> m (f a)
forall {l} {k} (f :: l -> *) (g :: k -> l) (p :: k).
(:.:) f g p -> f (g p)
unComp (:.:) m f a
state

{-------------------------------------------------------------------------------
  Supporting types
-------------------------------------------------------------------------------}

-- | Translate @f x@ to @f y@ across an era transition
--
-- Typically @f@ will be 'LedgerState' or 'WrapChainDepState'.
newtype Translate f x y = Translate {
      forall (f :: * -> *) x y. Translate f x y -> EpochNo -> f x -> f y
translateWith :: EpochNo -> f x -> f y
    }

-- | Forecast a @view y@ from a @state x@ across an era transition.
--
-- In addition to the 'Bound' of the transition, this is also told the
-- 'SlotNo' we're constructing a forecast for. This enables the translation
-- function to take into account any scheduled changes that the final ledger
-- view in the preceding era might have.
newtype CrossEraForecaster state view x y = CrossEraForecaster {
      forall (state :: * -> *) (view :: * -> *) x y.
CrossEraForecaster state view x y
-> Bound
-> SlotNo
-> state x
-> Except OutsideForecastRange (view y)
crossEraForecastWith ::
           Bound    -- 'Bound' of the transition (start of the new era)
        -> SlotNo   -- 'SlotNo' we're constructing a forecast for
        -> state x
        -> Except OutsideForecastRange (view y)
    }

-- | Knowledge in a particular era of the transition to the next era
data TransitionInfo =
    -- | No transition is yet known for this era
    -- We instead record the ledger tip (which must be in /this/ era)
    --
    -- NOTE: If we are forecasting, this will be set to the slot number of the
    -- (past) ledger state in which the forecast was created. This means that
    -- when we construct an 'EpochInfo' using a 'HardForkLedgerView', the
    -- range of that 'EpochInfo' will extend a safe zone from that /past/
    -- ledger state.
    TransitionUnknown !(WithOrigin SlotNo)

    -- | Transition to the next era is known to happen at this 'EpochNo'
  | TransitionKnown !EpochNo

    -- | The transition is impossible
    --
    -- This can be due to one of two reasons:
    --
    -- * We are in the final era
    -- * This era has not actually begun yet (we are forecasting). In this case,
    --   we cannot look past the safe zone of this era and hence, by definition,
    --   the transition to the /next/ era cannot happen.
  | TransitionImpossible
  deriving (Int -> TransitionInfo -> ShowS
[TransitionInfo] -> ShowS
TransitionInfo -> String
(Int -> TransitionInfo -> ShowS)
-> (TransitionInfo -> String)
-> ([TransitionInfo] -> ShowS)
-> Show TransitionInfo
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> TransitionInfo -> ShowS
showsPrec :: Int -> TransitionInfo -> ShowS
$cshow :: TransitionInfo -> String
show :: TransitionInfo -> String
$cshowList :: [TransitionInfo] -> ShowS
showList :: [TransitionInfo] -> ShowS
Show, (forall x. TransitionInfo -> Rep TransitionInfo x)
-> (forall x. Rep TransitionInfo x -> TransitionInfo)
-> Generic TransitionInfo
forall x. Rep TransitionInfo x -> TransitionInfo
forall x. TransitionInfo -> Rep TransitionInfo x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. TransitionInfo -> Rep TransitionInfo x
from :: forall x. TransitionInfo -> Rep TransitionInfo x
$cto :: forall x. Rep TransitionInfo x -> TransitionInfo
to :: forall x. Rep TransitionInfo x -> TransitionInfo
Generic, Context -> TransitionInfo -> IO (Maybe ThunkInfo)
Proxy TransitionInfo -> String
(Context -> TransitionInfo -> IO (Maybe ThunkInfo))
-> (Context -> TransitionInfo -> IO (Maybe ThunkInfo))
-> (Proxy TransitionInfo -> String)
-> NoThunks TransitionInfo
forall a.
(Context -> a -> IO (Maybe ThunkInfo))
-> (Context -> a -> IO (Maybe ThunkInfo))
-> (Proxy a -> String)
-> NoThunks a
$cnoThunks :: Context -> TransitionInfo -> IO (Maybe ThunkInfo)
noThunks :: Context -> TransitionInfo -> IO (Maybe ThunkInfo)
$cwNoThunks :: Context -> TransitionInfo -> IO (Maybe ThunkInfo)
wNoThunks :: Context -> TransitionInfo -> IO (Maybe ThunkInfo)
$cshowTypeOf :: Proxy TransitionInfo -> String
showTypeOf :: Proxy TransitionInfo -> String
NoThunks)