{-# 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
      -> HardForkState f'  xs -- ^ State we are aligning with
      -> HardForkState f   xs -- ^ State we are aligning
      -> 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
                   -> TransitionInfo         -- ^ At the tip
                   -> 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
eraEpochSize :: EraParams -> EpochSize
eraSlotLength :: EraParams -> SlotLength
eraSafeZone :: EraParams -> SafeZone
eraGenesisWin :: EraParams -> GenesisWindow
..} 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