{-# LANGUAGE DataKinds #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

module Ouroboros.Consensus.HardFork.Combinator.State.Infra
  ( -- * Initialization
    initHardForkState

    -- * Lifting 'Telescope' operations
  , fromTZ
  , match
  , sequence
  , tip

    -- * Situated
  , Situated (..)
  , situate

    -- * Aligning
  , align

    -- * EpochInfo/Summary
  , reconstructSummary
  ) where

import Data.Functor.Product
import Data.SOP.BasicFunctors
import Data.SOP.Constraint
import Data.SOP.Counting
import Data.SOP.InPairs (InPairs, Requiring (..))
import qualified Data.SOP.InPairs as InPairs
import Data.SOP.Match (Mismatch)
import qualified Data.SOP.Match as Match
import Data.SOP.NonEmpty
import Data.SOP.Strict
import Data.SOP.Telescope (Extend (..), Telescope (..))
import qualified Data.SOP.Telescope as Telescope
import Ouroboros.Consensus.Block
import Ouroboros.Consensus.HardFork.Combinator.Abstract.SingleEraBlock
import Ouroboros.Consensus.HardFork.Combinator.State.Lift
import Ouroboros.Consensus.HardFork.Combinator.State.Types
import Ouroboros.Consensus.HardFork.History
  ( Bound (..)
  , EraEnd (..)
  , EraParams (..)
  , EraSummary (..)
  , SafeZone (..)
  )
import qualified Ouroboros.Consensus.HardFork.History as History
import Prelude hiding (sequence)

{-------------------------------------------------------------------------------
  Initialization
-------------------------------------------------------------------------------}

initHardForkState :: f x -> HardForkState f (x ': xs)
initHardForkState :: forall (f :: * -> *) x (xs :: [*]). f x -> HardForkState f (x : xs)
initHardForkState f x
st =
  Telescope (K Past) (Current f) (x : xs) -> HardForkState f (x : xs)
forall (f :: * -> *) (xs :: [*]).
Telescope (K Past) (Current f) xs -> HardForkState f xs
HardForkState (Telescope (K Past) (Current f) (x : xs)
 -> HardForkState f (x : xs))
-> Telescope (K Past) (Current f) (x : xs)
-> HardForkState f (x : xs)
forall a b. (a -> b) -> a -> b
$
    Current f x -> Telescope (K Past) (Current f) (x : xs)
forall {k} (f :: k -> *) (x :: k) (g :: k -> *) (xs1 :: [k]).
f x -> Telescope g f (x : xs1)
TZ (Current f x -> Telescope (K Past) (Current f) (x : xs))
-> Current f x -> Telescope (K Past) (Current f) (x : xs)
forall a b. (a -> b) -> a -> b
$
      Current
        { currentStart :: Bound
currentStart = Bound
History.initBound
        , currentState :: f x
currentState = f x
st
        }

{-------------------------------------------------------------------------------
  Lift telescope operations
-------------------------------------------------------------------------------}

tip :: SListI xs => HardForkState f xs -> NS f xs
tip :: forall (xs :: [*]) (f :: * -> *).
SListI xs =>
HardForkState f xs -> NS f xs
tip (HardForkState Telescope (K Past) (Current f) xs
st) = (forall a. Current f a -> f a) -> NS (Current f) xs -> NS 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 f a -> f a
forall a. Current f a -> f a
forall (f :: * -> *) blk. Current f blk -> f blk
currentState (NS (Current f) xs -> NS f xs) -> NS (Current f) xs -> NS f xs
forall a b. (a -> b) -> a -> b
$ Telescope (K Past) (Current f) xs -> NS (Current f) xs
forall {k} (g :: k -> *) (f :: k -> *) (xs :: [k]).
Telescope g f xs -> NS f xs
Telescope.tip Telescope (K Past) (Current f) xs
st

match ::
  SListI xs =>
  NS h xs ->
  HardForkState f xs ->
  Either (Mismatch h (Current f) xs) (HardForkState (Product h f) xs)
match :: forall (xs :: [*]) (h :: * -> *) (f :: * -> *).
SListI xs =>
NS h xs
-> HardForkState f xs
-> Either
     (Mismatch h (Current f) xs) (HardForkState (Product h f) xs)
match NS h xs
ns (HardForkState Telescope (K Past) (Current f) xs
t) =
  Telescope (K Past) (Current (Product h f)) xs
-> HardForkState (Product h f) xs
forall (f :: * -> *) (xs :: [*]).
Telescope (K Past) (Current f) xs -> HardForkState f xs
HardForkState (Telescope (K Past) (Current (Product h f)) xs
 -> HardForkState (Product h f) xs)
-> (Telescope (K Past) (Product h (Current f)) xs
    -> Telescope (K Past) (Current (Product h f)) xs)
-> Telescope (K Past) (Product h (Current f)) xs
-> HardForkState (Product h f) xs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. Product h (Current f) a -> Current (Product h f) a)
-> Telescope (K Past) (Product h (Current f)) xs
-> Telescope (K Past) (Current (Product h 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 Product h (Current f) a -> Current (Product h f) a
forall a. Product h (Current f) a -> Current (Product h f) a
forall (h :: * -> *) (f :: * -> *) blk.
Product h (Current f) blk -> Current (Product h f) blk
distrib (Telescope (K Past) (Product h (Current f)) xs
 -> HardForkState (Product h f) xs)
-> Either
     (Mismatch h (Current f) xs)
     (Telescope (K Past) (Product h (Current f)) xs)
-> Either
     (Mismatch h (Current f) xs) (HardForkState (Product h f) xs)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NS h xs
-> Telescope (K Past) (Current f) xs
-> Either
     (Mismatch h (Current f) xs)
     (Telescope (K Past) (Product h (Current f)) xs)
forall {k} (h :: k -> *) (xs :: [k]) (g :: k -> *) (f :: k -> *).
NS h xs
-> Telescope g f xs
-> Either (Mismatch h f xs) (Telescope g (Product h f) xs)
Match.matchTelescope NS h xs
ns Telescope (K Past) (Current f) xs
t
 where
  distrib :: Product h (Current f) blk -> Current (Product h f) blk
  distrib :: forall (h :: * -> *) (f :: * -> *) blk.
Product h (Current f) blk -> Current (Product h f) blk
distrib (Pair h blk
x (Current Bound
start f blk
y)) =
    Bound -> Product h f blk -> Current (Product h f) blk
forall (f :: * -> *) blk. Bound -> f blk -> Current f blk
Current Bound
start (h blk -> f blk -> Product h f blk
forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair h blk
x f blk
y)

sequence ::
  forall f m xs.
  (SListI xs, Functor m) =>
  HardForkState (m :.: f) xs -> m (HardForkState f xs)
sequence :: forall (f :: * -> *) (m :: * -> *) (xs :: [*]).
(SListI xs, Functor m) =>
HardForkState (m :.: f) xs -> m (HardForkState f xs)
sequence = \(HardForkState Telescope (K Past) (Current (m :.: f)) xs
st) ->
  Telescope (K Past) (Current f) xs -> HardForkState f xs
forall (f :: * -> *) (xs :: [*]).
Telescope (K Past) (Current f) xs -> HardForkState f xs
HardForkState
    (Telescope (K Past) (Current f) xs -> HardForkState f xs)
-> m (Telescope (K Past) (Current f) xs) -> m (HardForkState f xs)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f 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 ((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
distrib Telescope (K Past) (Current (m :.: f)) xs
st)
 where
  distrib :: Current (m :.: f) blk -> (m :.: Current f) blk
  distrib :: forall a. Current (m :.: f) a -> (:.:) m (Current f) a
distrib (Current Bound
start (:.:) m f blk
st) =
    m (Current f blk) -> (:.:) m (Current f) blk
forall l k (f :: l -> *) (g :: k -> l) (p :: k).
f (g p) -> (:.:) f g p
Comp (m (Current f blk) -> (:.:) m (Current f) blk)
-> m (Current f blk) -> (:.:) m (Current f) blk
forall a b. (a -> b) -> a -> b
$
      Bound -> f blk -> Current f blk
forall (f :: * -> *) blk. Bound -> f blk -> Current f blk
Current Bound
start (f blk -> Current f blk) -> m (f blk) -> m (Current f blk)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (:.:) m f blk -> m (f blk)
forall {l} {k} (f :: l -> *) (g :: k -> l) (p :: k).
(:.:) f g p -> f (g p)
unComp (:.:) m f blk
st

fromTZ :: HardForkState f '[blk] -> f blk
fromTZ :: forall (f :: * -> *) blk. HardForkState f '[blk] -> f blk
fromTZ = Current f blk -> f blk
forall (f :: * -> *) blk. Current f blk -> f blk
currentState (Current f blk -> f blk)
-> (HardForkState f '[blk] -> Current f blk)
-> HardForkState f '[blk]
-> f blk
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Telescope (K Past) (Current f) '[blk] -> Current f blk
forall {k} (g :: k -> *) (f :: k -> *) (x :: k).
Telescope g f '[x] -> f x
Telescope.fromTZ (Telescope (K Past) (Current f) '[blk] -> Current f blk)
-> (HardForkState f '[blk]
    -> Telescope (K Past) (Current f) '[blk])
-> HardForkState f '[blk]
-> Current f blk
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HardForkState f '[blk] -> Telescope (K Past) (Current f) '[blk]
forall (f :: * -> *) (xs :: [*]).
HardForkState f xs -> Telescope (K Past) (Current f) xs
getHardForkState

{-------------------------------------------------------------------------------
  Situated
-------------------------------------------------------------------------------}

-- | A @h@ situated in time
data Situated h f xs where
  SituatedCurrent :: Current f x -> h x -> Situated h f (x ': xs)
  SituatedNext :: Current f x -> h y -> Situated h f (x ': y ': xs)
  SituatedFuture :: Current f x -> NS h xs -> Situated h f (x ': y ': xs)
  SituatedPast :: K Past x -> h x -> Situated h f (x ': xs)
  SituatedShift :: Situated h f xs -> Situated h f (x ': xs)

situate :: NS h xs -> HardForkState f xs -> Situated h f xs
situate :: forall (h :: * -> *) (xs :: [*]) (f :: * -> *).
NS h xs -> HardForkState f xs -> Situated h f xs
situate NS h xs
ns = NS h xs -> Telescope (K Past) (Current f) xs -> Situated h f xs
forall (h :: * -> *) (xs' :: [*]) (f :: * -> *).
NS h xs' -> Telescope (K Past) (Current f) xs' -> Situated h f xs'
go NS h xs
ns (Telescope (K Past) (Current f) xs -> Situated h f xs)
-> (HardForkState f xs -> Telescope (K Past) (Current f) xs)
-> HardForkState f xs
-> Situated h f xs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HardForkState f xs -> Telescope (K Past) (Current f) xs
forall (f :: * -> *) (xs :: [*]).
HardForkState f xs -> Telescope (K Past) (Current f) xs
getHardForkState
 where
  go ::
    NS h xs' ->
    Telescope (K Past) (Current f) xs' ->
    Situated h f xs'
  go :: forall (h :: * -> *) (xs' :: [*]) (f :: * -> *).
NS h xs' -> Telescope (K Past) (Current f) xs' -> Situated h f xs'
go (Z h x
era) (TZ Current f x
cur) = Current f x -> h x -> Situated h f (x : xs1)
forall (f :: * -> *) xs (h :: * -> *) (x :: [*]).
Current f xs -> h xs -> Situated h f (xs : x)
SituatedCurrent Current f x
cur h x
h x
era
  go (S (Z h x
era)) (TZ Current f x
cur) = Current f x -> h x -> Situated h f (x : x : xs1)
forall (f :: * -> *) xs (h :: * -> *) x (y :: [*]).
Current f xs -> h x -> Situated h f (xs : x : y)
SituatedNext Current f x
cur h x
era
  go (S (S NS h xs1
era)) (TZ Current f x
cur) = Current f x -> NS h xs1 -> Situated h f (x : x : xs1)
forall (f :: * -> *) xs (h :: * -> *) (x :: [*]) y.
Current f xs -> NS h x -> Situated h f (xs : y : x)
SituatedFuture Current f x
cur NS h xs1
era
  go (Z h x
era) (TS K Past x
past Telescope (K Past) (Current f) xs1
_) = K Past x -> h x -> Situated h f (x : xs1)
forall xs (h :: * -> *) (f :: * -> *) (x :: [*]).
K Past xs -> h xs -> Situated h f (xs : x)
SituatedPast K Past x
past h x
h x
era
  go (S NS h xs1
era) (TS K Past x
_ Telescope (K Past) (Current f) xs1
st) = Situated h f xs1 -> Situated h f (x : xs1)
forall (h :: * -> *) (f :: * -> *) (xs :: [*]) x.
Situated h f xs -> Situated h f (x : xs)
SituatedShift (Situated h f xs1 -> Situated h f (x : xs1))
-> Situated h f xs1 -> Situated h f (x : xs1)
forall a b. (a -> b) -> a -> b
$ NS h xs1 -> Telescope (K Past) (Current f) xs1 -> Situated h f xs1
forall (h :: * -> *) (xs' :: [*]) (f :: * -> *).
NS h xs' -> Telescope (K Past) (Current f) xs' -> Situated h f xs'
go NS h xs1
era Telescope (K Past) (Current f) xs1
Telescope (K Past) (Current f) xs1
st

{-------------------------------------------------------------------------------
  Aligning
-------------------------------------------------------------------------------}

align ::
  forall xs f f' f''.
  All SingleEraBlock xs =>
  InPairs (Translate f) xs ->
  NP (f' -.-> f -.-> f'') xs ->
  -- | State we are aligning with
  HardForkState f' xs ->
  -- | State we are aligning
  HardForkState f xs ->
  HardForkState f'' xs
align :: forall (xs :: [*]) (f :: * -> *) (f' :: * -> *) (f'' :: * -> *).
All SingleEraBlock xs =>
InPairs (Translate f) xs
-> NP (f' -.-> (f -.-> f'')) xs
-> HardForkState f' xs
-> HardForkState f xs
-> HardForkState f'' xs
align InPairs (Translate f) xs
fs NP (f' -.-> (f -.-> f'')) xs
updTip (HardForkState Telescope (K Past) (Current f') xs
alignWith) (HardForkState Telescope (K Past) (Current f) xs
toAlign) =
  Telescope (K Past) (Current f'') xs -> HardForkState f'' xs
forall (f :: * -> *) (xs :: [*]).
Telescope (K Past) (Current f) xs -> HardForkState f xs
HardForkState (Telescope (K Past) (Current f'') xs -> HardForkState f'' xs)
-> (I (Telescope (K Past) (Current f'') xs)
    -> Telescope (K Past) (Current f'') xs)
-> I (Telescope (K Past) (Current f'') xs)
-> HardForkState f'' xs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. I (Telescope (K Past) (Current f'') xs)
-> Telescope (K Past) (Current f'') xs
forall a. I a -> a
unI (I (Telescope (K Past) (Current f'') xs) -> HardForkState f'' xs)
-> I (Telescope (K Past) (Current f'') xs) -> HardForkState f'' xs
forall a b. (a -> b) -> a -> b
$
    InPairs (Requiring (K Past) (Extend I (K Past) (Current f))) xs
-> NP (Current f' -.-> (Current f -.-> Current f'')) xs
-> Telescope (K Past) (Current f') xs
-> Telescope (K Past) (Current f) xs
-> I (Telescope (K Past) (Current f'') xs)
forall {k} (m :: * -> *) (g' :: k -> *) (g :: k -> *) (f :: k -> *)
       (xs :: [k]) (f' :: k -> *) (f'' :: k -> *).
(Monad m, HasCallStack) =>
InPairs (Requiring g' (Extend m g f)) xs
-> NP (f' -.-> (f -.-> f'')) xs
-> Telescope g' f' xs
-> Telescope g f xs
-> m (Telescope g f'' xs)
Telescope.alignExtend
      ( (forall x y.
 Translate f x y
 -> Requiring (K Past) (Extend I (K Past) (Current f)) x y)
-> InPairs (Translate f) xs
-> InPairs (Requiring (K Past) (Extend I (K Past) (Current f))) xs
forall {k} (xs :: [k]) (f :: k -> k -> *) (g :: k -> k -> *).
SListI xs =>
(forall (x :: k) (y :: k). f x y -> g x y)
-> InPairs f xs -> InPairs g xs
InPairs.hmap
          ( \Translate f x y
f -> (K Past x -> Extend I (K Past) (Current f) x y)
-> Requiring (K Past) (Extend I (K Past) (Current f)) x y
forall {k} {k1} (h :: k -> *) (f :: k -> k1 -> *) (x :: k)
       (y :: k1).
(h x -> f x y) -> Requiring h f x y
Require ((K Past x -> Extend I (K Past) (Current f) x y)
 -> Requiring (K Past) (Extend I (K Past) (Current f)) x y)
-> (K Past x -> Extend I (K Past) (Current f) x y)
-> Requiring (K Past) (Extend I (K Past) (Current f)) x y
forall a b. (a -> b) -> a -> b
$
              \K Past x
past -> (Current f x -> I (K Past x, Current f y))
-> Extend I (K Past) (Current f) x y
forall {k} (m :: * -> *) (g :: k -> *) (f :: k -> *) (x :: k)
       (y :: k).
(f x -> m (g x, f y)) -> Extend m g f x y
Extend ((Current f x -> I (K Past x, Current f y))
 -> Extend I (K Past) (Current f) x y)
-> (Current f x -> I (K Past x, Current f y))
-> Extend I (K Past) (Current f) x y
forall a b. (a -> b) -> a -> b
$
                \Current f x
cur ->
                  (K Past x, Current f y) -> I (K Past x, Current f y)
forall a. a -> I a
I ((K Past x, Current f y) -> I (K Past x, Current f y))
-> (K Past x, Current f y) -> I (K Past x, Current f y)
forall a b. (a -> b) -> a -> b
$
                    Translate f x y
-> K Past x -> Current f x -> (K Past x, Current f y)
forall blk blk'.
Translate f blk blk'
-> K Past blk -> Current f blk -> (K Past blk, Current f blk')
newCurrent Translate f x y
f K Past x
past Current f x
cur
          )
          InPairs (Translate f) xs
fs
      )
      ((forall a.
 (-.->) f' (f -.-> f'') a
 -> (-.->) (Current f') (Current f -.-> Current f'') a)
-> NP (f' -.-> (f -.-> f'')) xs
-> NP (Current f' -.-> (Current f -.-> 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 f' a -> Current f a -> Current f'' a)
-> (-.->) (Current f') (Current f -.-> Current f'') a
forall {k} (f :: k -> *) (a :: k) (f' :: k -> *) (f'' :: k -> *).
(f a -> f' a -> f'' a) -> (-.->) f (f' -.-> f'') a
fn_2 ((Current f' a -> Current f a -> Current f'' a)
 -> (-.->) (Current f') (Current f -.-> Current f'') a)
-> ((-.->) f' (f -.-> f'') a
    -> Current f' a -> Current f a -> Current f'' a)
-> (-.->) f' (f -.-> f'') a
-> (-.->) (Current f') (Current f -.-> Current f'') a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (-.->) f' (f -.-> f'') a
-> Current f' a -> Current f a -> Current f'' a
forall blk.
(-.->) f' (f -.-> f'') blk
-> Current f' blk -> Current f blk -> Current f'' blk
liftUpdTip) NP (f' -.-> (f -.-> f'')) xs
updTip)
      Telescope (K Past) (Current f') xs
alignWith
      Telescope (K Past) (Current f) xs
toAlign
 where
  liftUpdTip ::
    (f' -.-> f -.-> f'') blk ->
    Current f' blk ->
    Current f blk ->
    Current f'' blk
  liftUpdTip :: forall blk.
(-.->) f' (f -.-> f'') blk
-> Current f' blk -> Current f blk -> Current f'' blk
liftUpdTip (-.->) f' (f -.-> f'') blk
f = (f blk -> f'' blk) -> Current f blk -> Current f'' blk
forall (f :: * -> *) blk (f' :: * -> *).
(f blk -> f' blk) -> Current f blk -> Current f' blk
lift ((f blk -> f'' blk) -> Current f blk -> Current f'' blk)
-> (Current f' blk -> f blk -> f'' blk)
-> Current f' blk
-> Current f blk
-> Current f'' blk
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (-.->) f f'' blk -> f blk -> f'' blk
forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
(-.->) f g a -> f a -> g a
apFn ((-.->) f f'' blk -> f blk -> f'' blk)
-> (Current f' blk -> (-.->) f f'' blk)
-> Current f' blk
-> f blk
-> f'' blk
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (-.->) f' (f -.-> f'') blk -> f' blk -> (-.->) f f'' blk
forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
(-.->) f g a -> f a -> g a
apFn (-.->) f' (f -.-> f'') blk
f (f' blk -> (-.->) f f'' blk)
-> (Current f' blk -> f' blk) -> Current f' blk -> (-.->) f f'' blk
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Current f' blk -> f' blk
forall (f :: * -> *) blk. Current f blk -> f blk
currentState

  newCurrent ::
    Translate f blk blk' ->
    K Past blk ->
    Current f blk ->
    (K Past blk, Current f blk')
  newCurrent :: forall blk blk'.
Translate f blk blk'
-> K Past blk -> Current f blk -> (K Past blk, Current f blk')
newCurrent Translate f blk blk'
f (K Past
past) Current f blk
curF =
    ( Past -> K Past blk
forall k a (b :: k). a -> K a b
K
        Past
          { pastStart :: Bound
pastStart = Current f blk -> Bound
forall (f :: * -> *) blk. Current f blk -> Bound
currentStart Current f blk
curF
          , pastEnd :: Bound
pastEnd = Bound
curEnd
          }
    , Current
        { currentStart :: Bound
currentStart = Bound
curEnd
        , currentState :: f blk'
currentState =
            Translate f blk blk' -> EpochNo -> f blk -> f blk'
forall (f :: * -> *) x y. Translate f x y -> EpochNo -> f x -> f y
translateWith
              Translate f blk blk'
f
              (Bound -> EpochNo
boundEpoch Bound
curEnd)
              (Current f blk -> f blk
forall (f :: * -> *) blk. Current f blk -> f blk
currentState Current f blk
curF)
        }
    )
   where
    curEnd :: Bound
    curEnd :: Bound
curEnd = Past -> Bound
pastEnd Past
past

{-------------------------------------------------------------------------------
  Summary/EpochInfo
-------------------------------------------------------------------------------}

reconstructSummary ::
  History.Shape xs ->
  -- | At the tip
  TransitionInfo ->
  HardForkState f xs ->
  History.Summary xs
reconstructSummary :: forall (xs :: [*]) (f :: * -> *).
Shape xs -> TransitionInfo -> HardForkState f xs -> Summary xs
reconstructSummary (History.Shape Exactly xs EraParams
shape) TransitionInfo
transition (HardForkState Telescope (K Past) (Current f) xs
st) =
  NonEmpty xs EraSummary -> Summary xs
forall (xs :: [*]). NonEmpty xs EraSummary -> Summary xs
History.Summary (NonEmpty xs EraSummary -> Summary xs)
-> NonEmpty xs EraSummary -> Summary xs
forall a b. (a -> b) -> a -> b
$ Exactly xs EraParams
-> Telescope (K Past) (Current f) xs -> NonEmpty xs EraSummary
forall (xs' :: [*]) (f :: * -> *).
Exactly xs' EraParams
-> Telescope (K Past) (Current f) xs' -> NonEmpty xs' EraSummary
go Exactly xs EraParams
shape Telescope (K Past) (Current f) xs
st
 where
  go ::
    Exactly xs' EraParams ->
    Telescope (K Past) (Current f) xs' ->
    NonEmpty xs' EraSummary
  go :: forall (xs' :: [*]) (f :: * -> *).
Exactly xs' EraParams
-> Telescope (K Past) (Current f) xs' -> NonEmpty xs' EraSummary
go Exactly xs' EraParams
ExactlyNil Telescope (K Past) (Current f) xs'
t = case Telescope (K Past) (Current f) xs'
t of {}
  go (ExactlyCons EraParams
params Exactly xs EraParams
ss) (TS (K Past{Bound
pastStart :: Past -> Bound
pastEnd :: Past -> Bound
pastStart :: Bound
pastEnd :: Bound
..}) Telescope (K Past) (Current f) xs1
t) =
    EraSummary
-> NonEmpty xs EraSummary -> NonEmpty (x : xs) EraSummary
forall a (xs1 :: [*]) x.
a -> NonEmpty xs1 a -> NonEmpty (x : xs1) a
NonEmptyCons (Bound -> EraEnd -> EraParams -> EraSummary
EraSummary Bound
pastStart (Bound -> EraEnd
EraEnd Bound
pastEnd) EraParams
params) (NonEmpty xs EraSummary -> NonEmpty (x : xs) EraSummary)
-> NonEmpty xs EraSummary -> NonEmpty (x : xs) EraSummary
forall a b. (a -> b) -> a -> b
$ Exactly xs EraParams
-> Telescope (K Past) (Current f) xs -> NonEmpty xs EraSummary
forall (xs' :: [*]) (f :: * -> *).
Exactly xs' EraParams
-> Telescope (K Past) (Current f) xs' -> NonEmpty xs' EraSummary
go Exactly xs EraParams
ss Telescope (K Past) (Current f) xs
Telescope (K Past) (Current f) xs1
t
  go (ExactlyCons EraParams
params Exactly xs EraParams
ss) (TZ Current{f x
Bound
currentStart :: forall (f :: * -> *) blk. Current f blk -> Bound
currentState :: forall (f :: * -> *) blk. Current f blk -> f blk
currentStart :: Bound
currentState :: f x
..}) =
    case TransitionInfo
transition of
      TransitionKnown EpochNo
epoch ->
        -- We haven't reached the next era yet, but the transition is
        -- already known. The safe zone applies from the start of the
        -- next era.
        let currentEnd :: Bound
currentEnd = HasCallStack => EraParams -> Bound -> EpochNo -> Bound
EraParams -> Bound -> EpochNo -> Bound
History.mkUpperBound EraParams
params Bound
currentStart EpochNo
epoch
            nextStart :: Bound
nextStart = Bound
currentEnd
         in case Exactly xs EraParams
ss of
              ExactlyCons EraParams
nextParams Exactly xs EraParams
_ ->
                EraSummary
-> NonEmpty (x : xs) EraSummary -> NonEmpty (x : x : xs) EraSummary
forall a (xs1 :: [*]) x.
a -> NonEmpty xs1 a -> NonEmpty (x : xs1) a
NonEmptyCons
                  EraSummary
                    { eraStart :: Bound
eraStart = Bound
currentStart
                    , eraParams :: EraParams
eraParams = EraParams
params
                    , eraEnd :: EraEnd
eraEnd = Bound -> EraEnd
EraEnd Bound
currentEnd
                    }
                  (NonEmpty (x : xs) EraSummary -> NonEmpty (x : x : xs) EraSummary)
-> NonEmpty (x : xs) EraSummary -> NonEmpty (x : x : xs) EraSummary
forall a b. (a -> b) -> a -> b
$ EraSummary -> NonEmpty (x : xs) EraSummary
forall a x (xs1 :: [*]). a -> NonEmpty (x : xs1) a
NonEmptyOne
                    EraSummary
                      { eraStart :: Bound
eraStart = Bound
nextStart
                      , eraParams :: EraParams
eraParams = EraParams
nextParams
                      , eraEnd :: EraEnd
eraEnd =
                          EraParams -> Bound -> SlotNo -> EraEnd
applySafeZone
                            EraParams
nextParams
                            Bound
nextStart
                            (Bound -> SlotNo
boundSlot Bound
nextStart)
                      }
              Exactly xs EraParams
ExactlyNil ->
                -- HOWEVER, this code doesn't know what that next era is! This
                -- can arise when a node has not updated its code despite an
                -- imminent hard fork.
                --
                -- In the specific case of 'ShelleyBlock' and 'CardanoBlock', a
                -- lot would have to go wrong in the PR review process for
                -- 'TransitionKnown' to arise during the last known era in the
                -- code. The 'ShelleyBlock' 'singleEraTransition' method leads
                -- to 'TransitionKnown' here only based on the
                -- 'shelleyTriggerHardFork' field of its ledger config, which is
                -- statically set by a quite obvious pattern in
                -- 'protocolInfoCardano', which is passed concrete arguments by
                -- a similarly obvious pattern in
                -- 'mkSomeConsensusProtocolCardano' defined in the
                -- @cardano-node@ repo.
                EraSummary -> NonEmpty '[x] EraSummary
forall a x (xs1 :: [*]). a -> NonEmpty (x : xs1) a
NonEmptyOne
                  EraSummary
                    { eraStart :: Bound
eraStart = Bound
currentStart
                    , eraParams :: EraParams
eraParams = EraParams
params
                    , eraEnd :: EraEnd
eraEnd = Bound -> EraEnd
EraEnd Bound
currentEnd
                    }
      TransitionUnknown WithOrigin SlotNo
ledgerTip ->
        EraSummary -> NonEmpty (x : xs) EraSummary
forall a x (xs1 :: [*]). a -> NonEmpty (x : xs1) a
NonEmptyOne (EraSummary -> NonEmpty (x : xs) EraSummary)
-> EraSummary -> NonEmpty (x : xs) EraSummary
forall a b. (a -> b) -> a -> b
$
          EraSummary
            { eraStart :: Bound
eraStart = Bound
currentStart
            , eraParams :: EraParams
eraParams = EraParams
params
            , eraEnd :: EraEnd
eraEnd =
                EraParams -> Bound -> SlotNo -> EraEnd
applySafeZone
                  EraParams
params
                  Bound
currentStart
                  -- Even if the safe zone is 0, the first slot at
                  -- which the next era could begin is the /next/
                  (WithOrigin SlotNo -> SlotNo
next WithOrigin SlotNo
ledgerTip)
            }
      -- 'TransitionImpossible' is used in one of two cases: we are in the
      -- final era this chain will ever have (handled by the corresponding
      -- 'UnsafeIndefiniteSafeZone' case within 'applySafeZone' below) or
      -- this era is a future era that hasn't begun yet, in which case the
      -- safe zone must start at the beginning of this era.
      TransitionInfo
TransitionImpossible ->
        EraSummary -> NonEmpty (x : xs) EraSummary
forall a x (xs1 :: [*]). a -> NonEmpty (x : xs1) a
NonEmptyOne (EraSummary -> NonEmpty (x : xs) EraSummary)
-> EraSummary -> NonEmpty (x : xs) EraSummary
forall a b. (a -> b) -> a -> b
$
          EraSummary
            { eraStart :: Bound
eraStart = Bound
currentStart
            , eraParams :: EraParams
eraParams = EraParams
params
            , eraEnd :: EraEnd
eraEnd =
                EraParams -> Bound -> SlotNo -> EraEnd
applySafeZone
                  EraParams
params
                  Bound
currentStart
                  (Bound -> SlotNo
boundSlot Bound
currentStart)
            }

  -- Apply safe zone from the specified 'SlotNo'
  --
  -- All arguments must be referring to or in the same era.
  applySafeZone :: EraParams -> Bound -> SlotNo -> EraEnd
  applySafeZone :: EraParams -> Bound -> SlotNo -> EraEnd
applySafeZone params :: EraParams
params@EraParams{EpochSize
SlotLength
GenesisWindow
SafeZone
eraEpochSize :: EpochSize
eraSlotLength :: SlotLength
eraSafeZone :: SafeZone
eraGenesisWin :: GenesisWindow
eraGenesisWin :: EraParams -> GenesisWindow
eraSafeZone :: EraParams -> SafeZone
eraSlotLength :: EraParams -> SlotLength
eraEpochSize :: EraParams -> EpochSize
..} Bound
start =
    case SafeZone
eraSafeZone of
      SafeZone
UnsafeIndefiniteSafeZone ->
        EraEnd -> SlotNo -> EraEnd
forall a b. a -> b -> a
const EraEnd
EraUnbounded
      StandardSafeZone Word64
safeFromTip ->
        Bound -> EraEnd
EraEnd
          (Bound -> EraEnd) -> (SlotNo -> Bound) -> SlotNo -> EraEnd
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HasCallStack => EraParams -> Bound -> EpochNo -> Bound
EraParams -> Bound -> EpochNo -> Bound
History.mkUpperBound EraParams
params Bound
start
          (EpochNo -> Bound) -> (SlotNo -> EpochNo) -> SlotNo -> Bound
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EraParams -> Bound -> SlotNo -> EpochNo
History.slotToEpochBound EraParams
params Bound
start
          (SlotNo -> EpochNo) -> (SlotNo -> SlotNo) -> SlotNo -> EpochNo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word64 -> SlotNo -> SlotNo
History.addSlots Word64
safeFromTip

  next :: WithOrigin SlotNo -> SlotNo
  next :: WithOrigin SlotNo -> SlotNo
next WithOrigin SlotNo
Origin = Word64 -> SlotNo
SlotNo Word64
0
  next (NotOrigin SlotNo
s) = SlotNo -> SlotNo
forall a. Enum a => a -> a
succ SlotNo
s