{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE EmptyCase           #-}
{-# LANGUAGE FlexibleContexts    #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE LambdaCase          #-}
{-# 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           Prelude hiding (sequence)

import           Data.Functor.Product
import           Data.SOP.Strict hiding (shape)

import           Ouroboros.Consensus.Block
import           Ouroboros.Consensus.HardFork.History (Bound (..), EraEnd (..),
                     EraParams (..), EraSummary (..), SafeZone (..))
import qualified Ouroboros.Consensus.HardFork.History as History
import           Ouroboros.Consensus.Util.Counting

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.Combinator.Util.InPairs (InPairs,
                     Requiring (..))
import qualified Ouroboros.Consensus.HardFork.Combinator.Util.InPairs as InPairs
import           Ouroboros.Consensus.HardFork.Combinator.Util.Match (Mismatch)
import qualified Ouroboros.Consensus.HardFork.Combinator.Util.Match as Match
import           Ouroboros.Consensus.HardFork.Combinator.Util.Telescope
                     (Extend (..), Telescope (..))
import qualified Ouroboros.Consensus.HardFork.Combinator.Util.Telescope as Telescope

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

initHardForkState :: f x -> HardForkState f (x ': xs)
initHardForkState :: 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 a (f :: a -> *) (x :: a) (g :: a -> *) (xs :: [a]).
f x -> Telescope g f (x : xs)
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 :: forall (f :: * -> *) blk. Bound -> f blk -> Current f blk
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 :: 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 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 :: 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 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 :: 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 :: 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 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 :: Current (m :.: f) blk -> (:.:) m (Current f) blk
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 :: 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 :: 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 :: 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 : xs)
forall (f :: * -> *) x (h :: * -> *) (xs :: [*]).
Current f x -> h x -> Situated h f (x : xs)
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 : xs)
forall (f :: * -> *) x (h :: * -> *) y (x :: [*]).
Current f x -> h y -> Situated h f (x : y : x)
SituatedNext    Current f x
cur h x
era
    go (S (S NS h xs
era)) (TZ Current f x
cur)    = Current f x -> NS h xs -> Situated h f (x : x : xs)
forall (f :: * -> *) x (h :: * -> *) (xs :: [*]) y.
Current f x -> NS h xs -> Situated h f (x : y : xs)
SituatedFuture  Current f x
cur NS h xs
era
    go (Z    h x
era)  (TS K Past x
past Telescope (K Past) (Current f) xs
_) = K Past x -> h x -> Situated h f (x : xs)
forall x (h :: * -> *) (f :: * -> *) (xs :: [*]).
K Past x -> h x -> Situated h f (x : xs)
SituatedPast   K Past x
past h x
h x
era
    go (S    NS h xs
era)  (TS K Past x
_ Telescope (K Past) (Current f) xs
st)   = Situated h f xs -> Situated h f (x : xs)
forall (h :: * -> *) (f :: * -> *) (xs :: [*]) x.
Situated h f xs -> Situated h f (x : xs)
SituatedShift (Situated h f xs -> Situated h f (x : xs))
-> Situated h f xs -> Situated h f (x : xs)
forall a b. (a -> b) -> a -> b
$ 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
era Telescope (K Past) (Current f) xs
Telescope (K Past) (Current f) xs
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 :: 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 k (h :: k -> *) (f :: k -> k -> *) (x :: k) (y :: k).
(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 :: (-.->) 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 :: 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 :: Bound -> Bound -> Past
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 :: forall (f :: * -> *) blk. Bound -> f blk -> Current f blk
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 :: 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 :: 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
pastEnd :: Bound
pastStart :: Bound
pastEnd :: Past -> Bound
pastStart :: Past -> Bound
..}) Telescope (K Past) (Current f) xs
t) =
        EraSummary
-> NonEmpty xs EraSummary -> NonEmpty (x : xs) EraSummary
forall a (xs :: [*]) x. a -> NonEmpty xs a -> NonEmpty (x : xs) 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) xs
t
    go (ExactlyCons EraParams
params Exactly xs EraParams
ss) (TZ Current{f x
Bound
currentState :: f x
currentStart :: Bound
currentState :: forall (f :: * -> *) blk. Current f blk -> f blk
currentStart :: forall (f :: * -> *) blk. Current f blk -> Bound
..}) =
        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 (xs :: [*]) x. a -> NonEmpty xs a -> NonEmpty (x : xs) a
NonEmptyCons EraSummary :: Bound -> EraEnd -> EraParams -> EraSummary
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 (xs :: [*]). a -> NonEmpty (x : xs) a
NonEmptyOne EraSummary :: Bound -> EraEnd -> EraParams -> EraSummary
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 (xs :: [*]). a -> NonEmpty (x : xs) a
NonEmptyOne EraSummary :: Bound -> EraEnd -> EraParams -> EraSummary
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 (xs :: [*]). a -> NonEmpty (x : xs) a
NonEmptyOne (EraSummary -> NonEmpty (x : xs) EraSummary)
-> EraSummary -> NonEmpty (x : xs) EraSummary
forall a b. (a -> b) -> a -> b
$ EraSummary :: Bound -> EraEnd -> EraParams -> EraSummary
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 (xs :: [*]). a -> NonEmpty (x : xs) a
NonEmptyOne (EraSummary -> NonEmpty (x : xs) EraSummary)
-> EraSummary -> NonEmpty (x : xs) EraSummary
forall a b. (a -> b) -> a -> b
$ EraSummary :: Bound -> EraEnd -> EraParams -> EraSummary
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{SlotLength
EpochSize
SafeZone
eraSafeZone :: EraParams -> SafeZone
eraSlotLength :: EraParams -> SlotLength
eraEpochSize :: EraParams -> EpochSize
eraSafeZone :: SafeZone
eraSlotLength :: SlotLength
eraEpochSize :: 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