{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE FlexibleContexts     #-}
{-# LANGUAGE GADTs                #-}
{-# LANGUAGE NamedFieldPuns       #-}
{-# LANGUAGE RankNTypes           #-}
{-# LANGUAGE RecordWildCards      #-}
{-# LANGUAGE ScopedTypeVariables  #-}
{-# LANGUAGE TypeApplications     #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}

-- | Intended for qualified import
--
-- > import Ouroboros.Consensus.HardFork.Combinator.State (HardForkState(..))
-- > import qualified Ouroboros.Consensus.HardFork.Combinator.State as State
module Ouroboros.Consensus.HardFork.Combinator.State (
    module X
    -- * Support for defining instances
  , getTip
    -- * Serialisation support
  , recover
    -- * EpochInfo
  , mostRecentTransitionInfo
  , reconstructSummaryLedger
  , epochInfoLedger
  , epochInfoPrecomputedTransitionInfo
    -- * Ledger specific functionality
  , extendToSlot
  ) where

import           Prelude hiding (sequence)

import           Control.Monad (guard)
import           Data.Functor.Identity
import           Data.Functor.Product
import           Data.Proxy
import           Data.SOP.Strict hiding (shape)

import           Ouroboros.Consensus.Block
import qualified Ouroboros.Consensus.HardFork.History as History
import           Ouroboros.Consensus.Ledger.Abstract hiding (getTip)
import           Ouroboros.Consensus.Util ((.:))
import           Ouroboros.Consensus.Util.Counting (getExactly)

import           Ouroboros.Consensus.HardFork.Combinator.Abstract
import           Ouroboros.Consensus.HardFork.Combinator.AcrossEras
import           Ouroboros.Consensus.HardFork.Combinator.Basics
import           Ouroboros.Consensus.HardFork.Combinator.PartialConfig
import           Ouroboros.Consensus.HardFork.Combinator.Translation
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.Telescope
                     (Extend (..), ScanNext (..), Telescope)
import qualified Ouroboros.Consensus.HardFork.Combinator.Util.Telescope as Telescope

import           Ouroboros.Consensus.HardFork.Combinator.State.Infra as X
import           Ouroboros.Consensus.HardFork.Combinator.State.Instances as X ()
import           Ouroboros.Consensus.HardFork.Combinator.State.Types as X

{-------------------------------------------------------------------------------
  GetTip
-------------------------------------------------------------------------------}

getTip :: forall f xs. CanHardFork xs
       => (forall blk. SingleEraBlock blk => f blk -> Point blk)
       -> HardForkState f xs -> Point (HardForkBlock xs)
getTip :: (forall blk. SingleEraBlock blk => f blk -> Point blk)
-> HardForkState f xs -> Point (HardForkBlock xs)
getTip forall blk. SingleEraBlock blk => f blk -> Point blk
getLedgerTip =
      NS (K (Point (HardForkBlock xs))) xs -> Point (HardForkBlock xs)
forall k l (h :: (k -> *) -> l -> *) (xs :: l) a.
(HCollapse h, SListIN h xs) =>
h (K a) xs -> CollapseTo h a
hcollapse
    (NS (K (Point (HardForkBlock xs))) xs -> Point (HardForkBlock xs))
-> (HardForkState f xs -> NS (K (Point (HardForkBlock xs))) xs)
-> HardForkState f xs
-> Point (HardForkBlock xs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy SingleEraBlock
-> (forall a.
    SingleEraBlock a =>
    f a -> K (Point (HardForkBlock xs)) a)
-> NS f xs
-> NS (K (Point (HardForkBlock xs))) xs
forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *)
       (f' :: k -> *).
(AllN (Prod h) c xs, HAp h) =>
proxy c
-> (forall (a :: k). c a => f a -> f' a) -> h f xs -> h f' xs
hcmap Proxy SingleEraBlock
proxySingle (Point (HardForkBlock xs) -> K (Point (HardForkBlock xs)) a
forall k a (b :: k). a -> K a b
K (Point (HardForkBlock xs) -> K (Point (HardForkBlock xs)) a)
-> (f a -> Point (HardForkBlock xs))
-> f a
-> K (Point (HardForkBlock xs)) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Point a -> Point (HardForkBlock xs)
forall blk.
SingleEraBlock blk =>
Point blk -> Point (HardForkBlock xs)
injPoint (Point a -> Point (HardForkBlock xs))
-> (f a -> Point a) -> f a -> Point (HardForkBlock xs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> Point a
forall blk. SingleEraBlock blk => f blk -> Point blk
getLedgerTip)
    (NS f xs -> NS (K (Point (HardForkBlock xs))) xs)
-> (HardForkState f xs -> NS f xs)
-> HardForkState f xs
-> NS (K (Point (HardForkBlock xs))) xs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HardForkState f xs -> NS f xs
forall (xs :: [*]) (f :: * -> *).
SListI xs =>
HardForkState f xs -> NS f xs
tip
  where
    injPoint :: forall blk. SingleEraBlock blk
             => Point blk -> Point (HardForkBlock xs)
    injPoint :: Point blk -> Point (HardForkBlock xs)
injPoint Point blk
GenesisPoint     = Point (HardForkBlock xs)
forall block. Point block
GenesisPoint
    injPoint (BlockPoint SlotNo
s HeaderHash blk
h) = SlotNo -> HeaderHash (HardForkBlock xs) -> Point (HardForkBlock xs)
forall block. SlotNo -> HeaderHash block -> Point block
BlockPoint SlotNo
s (HeaderHash (HardForkBlock xs) -> Point (HardForkBlock xs))
-> HeaderHash (HardForkBlock xs) -> Point (HardForkBlock xs)
forall a b. (a -> b) -> a -> b
$ ShortByteString -> OneEraHash xs
forall k (xs :: [k]). ShortByteString -> OneEraHash xs
OneEraHash (ShortByteString -> OneEraHash xs)
-> ShortByteString -> OneEraHash xs
forall a b. (a -> b) -> a -> b
$
                                  Proxy blk -> HeaderHash blk -> ShortByteString
forall blk (proxy :: * -> *).
ConvertRawHash blk =>
proxy blk -> HeaderHash blk -> ShortByteString
toShortRawHash (Proxy blk
forall k (t :: k). Proxy t
Proxy @blk) HeaderHash blk
h

{-------------------------------------------------------------------------------
  Recovery
-------------------------------------------------------------------------------}

-- | Recover 'HardForkState' from partial information
--
-- The primary goal of this is to make sure that for the /current/ state we
-- really only need to store the underlying @f@. It is not strictly essential
-- that this is possible but it helps with the unary hardfork case, and it may
-- in general help with binary compatibility.
recover :: forall f xs. CanHardFork xs
        => Telescope (K Past) f xs -> HardForkState f xs
recover :: Telescope (K Past) f xs -> HardForkState f xs
recover =
    case Proxy xs -> ProofNonEmpty xs
forall (xs :: [*]) (proxy :: [*] -> *).
IsNonEmpty xs =>
proxy xs -> ProofNonEmpty xs
isNonEmpty (Proxy xs
forall k (t :: k). Proxy t
Proxy @xs) of
      ProofNonEmpty {} ->
          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) f (x : xs)
    -> Telescope (K Past) (Current f) (x : xs))
-> Telescope (K Past) f (x : xs)
-> HardForkState f (x : xs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall x. Product (K Bound) (K Past) x -> K Past x)
-> (forall x. Product (K Bound) f x -> Current f x)
-> Telescope
     (Product (K Bound) (K Past)) (Product (K Bound) f) (x : xs)
-> Telescope (K Past) (Current f) (x : xs)
forall k (xs :: [k]) (g :: k -> *) (g' :: k -> *) (f :: k -> *)
       (f' :: k -> *).
SListI xs =>
(forall (x :: k). g x -> g' x)
-> (forall (x :: k). f x -> f' x)
-> Telescope g f xs
-> Telescope g' f' xs
Telescope.bihmap
            (\(Pair _ past) -> K Past x
past)
            forall x. Product (K Bound) f x -> Current f x
recoverCurrent
        (Telescope
   (Product (K Bound) (K Past)) (Product (K Bound) f) (x : xs)
 -> Telescope (K Past) (Current f) (x : xs))
-> (Telescope (K Past) f (x : xs)
    -> Telescope
         (Product (K Bound) (K Past)) (Product (K Bound) f) (x : xs))
-> Telescope (K Past) f (x : xs)
-> Telescope (K Past) (Current f) (x : xs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InPairs (ScanNext (K Bound) (K Past)) (x : xs)
-> K Bound x
-> Telescope (K Past) f (x : xs)
-> Telescope
     (Product (K Bound) (K Past)) (Product (K Bound) f) (x : xs)
forall a (h :: a -> *) (g :: a -> *) (x :: a) (xs :: [a])
       (f :: a -> *).
InPairs (ScanNext h g) (x : xs)
-> h x
-> Telescope g f (x : xs)
-> Telescope (Product h g) (Product h f) (x : xs)
Telescope.scanl
            ((forall x y. ScanNext (K Bound) (K Past) x y)
-> InPairs (ScanNext (K Bound) (K Past)) (x : xs)
forall (xs :: [*]) (f :: * -> * -> *).
(SListI xs, IsNonEmpty xs) =>
(forall x y. f x y) -> InPairs f xs
InPairs.hpure ((forall x y. ScanNext (K Bound) (K Past) x y)
 -> InPairs (ScanNext (K Bound) (K Past)) (x : xs))
-> (forall x y. ScanNext (K Bound) (K Past) x y)
-> InPairs (ScanNext (K Bound) (K Past)) (x : xs)
forall a b. (a -> b) -> a -> b
$ (K Bound x -> K Past x -> K Bound y)
-> ScanNext (K Bound) (K Past) x y
forall k (h :: k -> *) (g :: k -> *) (x :: k) (y :: k).
(h x -> g x -> h y) -> ScanNext h g x y
ScanNext ((K Bound x -> K Past x -> K Bound y)
 -> ScanNext (K Bound) (K Past) x y)
-> (K Bound x -> K Past x -> K Bound y)
-> ScanNext (K Bound) (K Past) x y
forall a b. (a -> b) -> a -> b
$ (K Past x -> K Bound y) -> K Bound x -> K Past x -> K Bound y
forall a b. a -> b -> a
const ((K Past x -> K Bound y) -> K Bound x -> K Past x -> K Bound y)
-> (K Past x -> K Bound y) -> K Bound x -> K Past x -> K Bound y
forall a b. (a -> b) -> a -> b
$ Bound -> K Bound y
forall k a (b :: k). a -> K a b
K (Bound -> K Bound y)
-> (K Past x -> Bound) -> K Past x -> K Bound y
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Past -> Bound
pastEnd (Past -> Bound) -> (K Past x -> Past) -> K Past x -> Bound
forall b c a. (b -> c) -> (a -> b) -> a -> c
. K Past x -> Past
forall k a (b :: k). K a b -> a
unK)
            (Bound -> K Bound x
forall k a (b :: k). a -> K a b
K Bound
History.initBound)
  where
    recoverCurrent :: Product (K History.Bound) f blk -> Current f blk
    recoverCurrent :: Product (K Bound) f blk -> Current f blk
recoverCurrent (Pair (K Bound
prevEnd) f blk
st) = Current :: forall (f :: * -> *) blk. Bound -> f blk -> Current f blk
Current {
          currentStart :: Bound
currentStart = Bound
prevEnd
        , currentState :: f blk
currentState = f blk
st
        }

{-------------------------------------------------------------------------------
  Reconstruct EpochInfo
-------------------------------------------------------------------------------}

mostRecentTransitionInfo :: All SingleEraBlock xs
                         => HardForkLedgerConfig xs
                         -> HardForkState LedgerState xs
                         -> TransitionInfo
mostRecentTransitionInfo :: HardForkLedgerConfig xs
-> HardForkState LedgerState xs -> TransitionInfo
mostRecentTransitionInfo HardForkLedgerConfig{Shape xs
PerEraLedgerConfig xs
hardForkLedgerConfigPerEra :: forall (xs :: [*]).
HardForkLedgerConfig xs -> PerEraLedgerConfig xs
hardForkLedgerConfigShape :: forall (xs :: [*]). HardForkLedgerConfig xs -> Shape xs
hardForkLedgerConfigPerEra :: PerEraLedgerConfig xs
hardForkLedgerConfigShape :: Shape xs
..} HardForkState LedgerState xs
st =
    NS (K TransitionInfo) xs -> CollapseTo NS TransitionInfo
forall k l (h :: (k -> *) -> l -> *) (xs :: l) a.
(HCollapse h, SListIN h xs) =>
h (K a) xs -> CollapseTo h a
hcollapse (NS (K TransitionInfo) xs -> CollapseTo NS TransitionInfo)
-> NS (K TransitionInfo) xs -> CollapseTo NS TransitionInfo
forall a b. (a -> b) -> a -> b
$
      Proxy SingleEraBlock
-> (forall a.
    SingleEraBlock a =>
    WrapPartialLedgerConfig a
    -> K EraParams a -> Current LedgerState a -> K TransitionInfo a)
-> Prod NS WrapPartialLedgerConfig xs
-> Prod NS (K EraParams) xs
-> NS (Current LedgerState) xs
-> NS (K TransitionInfo) xs
forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *)
       (f' :: k -> *) (f'' :: k -> *) (f''' :: k -> *).
(AllN (Prod h) c xs, HAp h, HAp (Prod h)) =>
proxy c
-> (forall (a :: k). c a => f a -> f' a -> f'' a -> f''' a)
-> Prod h f xs
-> Prod h f' xs
-> h f'' xs
-> h f''' xs
hczipWith3
        Proxy SingleEraBlock
proxySingle
        forall a.
SingleEraBlock a =>
WrapPartialLedgerConfig a
-> K EraParams a -> Current LedgerState a -> K TransitionInfo a
getTransition
        Prod NS WrapPartialLedgerConfig xs
NP WrapPartialLedgerConfig xs
cfgs
        (Exactly xs EraParams -> NP (K EraParams) xs
forall (xs :: [*]) a. Exactly xs a -> NP (K a) xs
getExactly (Shape xs -> Exactly xs EraParams
forall (xs :: [*]). Shape xs -> Exactly xs EraParams
History.getShape Shape xs
hardForkLedgerConfigShape))
        (Telescope (K Past) (Current LedgerState) xs
-> NS (Current LedgerState) xs
forall k (g :: k -> *) (f :: k -> *) (xs :: [k]).
Telescope g f xs -> NS f xs
Telescope.tip (HardForkState LedgerState xs
-> Telescope (K Past) (Current LedgerState) xs
forall (f :: * -> *) (xs :: [*]).
HardForkState f xs -> Telescope (K Past) (Current f) xs
getHardForkState HardForkState LedgerState xs
st))
  where
    cfgs :: NP WrapPartialLedgerConfig xs
cfgs = PerEraLedgerConfig xs -> NP WrapPartialLedgerConfig xs
forall (xs :: [*]).
PerEraLedgerConfig xs -> NP WrapPartialLedgerConfig xs
getPerEraLedgerConfig PerEraLedgerConfig xs
hardForkLedgerConfigPerEra

    getTransition :: SingleEraBlock          blk
                  => WrapPartialLedgerConfig blk
                  -> K History.EraParams     blk
                  -> Current LedgerState     blk
                  -> K TransitionInfo        blk
    getTransition :: WrapPartialLedgerConfig blk
-> K EraParams blk
-> Current LedgerState blk
-> K TransitionInfo blk
getTransition WrapPartialLedgerConfig blk
cfg (K EraParams
eraParams) Current{LedgerState blk
Bound
currentState :: LedgerState blk
currentStart :: Bound
currentState :: forall (f :: * -> *) blk. Current f blk -> f blk
currentStart :: forall (f :: * -> *) blk. Current f blk -> Bound
..} = TransitionInfo -> K TransitionInfo blk
forall k a (b :: k). a -> K a b
K (TransitionInfo -> K TransitionInfo blk)
-> TransitionInfo -> K TransitionInfo blk
forall a b. (a -> b) -> a -> b
$
        case WrapPartialLedgerConfig blk
-> EraParams -> Bound -> LedgerState blk -> Maybe EpochNo
forall blk.
SingleEraBlock blk =>
WrapPartialLedgerConfig blk
-> EraParams -> Bound -> LedgerState blk -> Maybe EpochNo
singleEraTransition' WrapPartialLedgerConfig blk
cfg EraParams
eraParams Bound
currentStart LedgerState blk
currentState of
          Maybe EpochNo
Nothing -> WithOrigin SlotNo -> TransitionInfo
TransitionUnknown (LedgerState blk -> WithOrigin SlotNo
forall blk.
UpdateLedger blk =>
LedgerState blk -> WithOrigin SlotNo
ledgerTipSlot LedgerState blk
currentState)
          Just EpochNo
e  -> EpochNo -> TransitionInfo
TransitionKnown EpochNo
e

reconstructSummaryLedger :: All SingleEraBlock xs
                         => HardForkLedgerConfig xs
                         -> HardForkState LedgerState xs
                         -> History.Summary xs
reconstructSummaryLedger :: HardForkLedgerConfig xs
-> HardForkState LedgerState xs -> Summary xs
reconstructSummaryLedger cfg :: HardForkLedgerConfig xs
cfg@HardForkLedgerConfig{Shape xs
PerEraLedgerConfig xs
hardForkLedgerConfigPerEra :: PerEraLedgerConfig xs
hardForkLedgerConfigShape :: Shape xs
hardForkLedgerConfigPerEra :: forall (xs :: [*]).
HardForkLedgerConfig xs -> PerEraLedgerConfig xs
hardForkLedgerConfigShape :: forall (xs :: [*]). HardForkLedgerConfig xs -> Shape xs
..} HardForkState LedgerState xs
st =
    Shape xs
-> TransitionInfo -> HardForkState LedgerState xs -> Summary xs
forall (xs :: [*]) (f :: * -> *).
Shape xs -> TransitionInfo -> HardForkState f xs -> Summary xs
reconstructSummary
      Shape xs
hardForkLedgerConfigShape
      (HardForkLedgerConfig xs
-> HardForkState LedgerState xs -> TransitionInfo
forall (xs :: [*]).
All SingleEraBlock xs =>
HardForkLedgerConfig xs
-> HardForkState LedgerState xs -> TransitionInfo
mostRecentTransitionInfo HardForkLedgerConfig xs
cfg HardForkState LedgerState xs
st)
      HardForkState LedgerState xs
st

-- | Construct 'EpochInfo' from the ledger state
--
-- NOTE: The resulting 'EpochInfo' is a snapshot only, with a limited range.
-- It should not be stored.
epochInfoLedger :: All SingleEraBlock xs
                => HardForkLedgerConfig xs
                -> HardForkState LedgerState xs
                -> EpochInfo Identity
epochInfoLedger :: HardForkLedgerConfig xs
-> HardForkState LedgerState xs -> EpochInfo Identity
epochInfoLedger HardForkLedgerConfig xs
cfg HardForkState LedgerState xs
st =
    Summary xs -> EpochInfo Identity
forall (xs :: [*]). Summary xs -> EpochInfo Identity
History.snapshotEpochInfo (Summary xs -> EpochInfo Identity)
-> Summary xs -> EpochInfo Identity
forall a b. (a -> b) -> a -> b
$
      HardForkLedgerConfig xs
-> HardForkState LedgerState xs -> Summary xs
forall (xs :: [*]).
All SingleEraBlock xs =>
HardForkLedgerConfig xs
-> HardForkState LedgerState xs -> Summary xs
reconstructSummaryLedger HardForkLedgerConfig xs
cfg HardForkState LedgerState xs
st

-- | Construct 'EpochInfo' given precomputed 'TransitionInfo'
epochInfoPrecomputedTransitionInfo ::
     History.Shape xs
  -> TransitionInfo
  -> HardForkState f xs
  -> EpochInfo Identity
epochInfoPrecomputedTransitionInfo :: Shape xs
-> TransitionInfo -> HardForkState f xs -> EpochInfo Identity
epochInfoPrecomputedTransitionInfo Shape xs
shape TransitionInfo
transition HardForkState f xs
st =
    Summary xs -> EpochInfo Identity
forall (xs :: [*]). Summary xs -> EpochInfo Identity
History.snapshotEpochInfo (Summary xs -> EpochInfo Identity)
-> Summary xs -> EpochInfo Identity
forall a b. (a -> b) -> a -> b
$
      Shape xs -> TransitionInfo -> HardForkState f xs -> Summary xs
forall (xs :: [*]) (f :: * -> *).
Shape xs -> TransitionInfo -> HardForkState f xs -> Summary xs
reconstructSummary Shape xs
shape TransitionInfo
transition HardForkState f xs
st

{-------------------------------------------------------------------------------
  Extending
-------------------------------------------------------------------------------}

-- | Extend the telescope until the specified slot is within the era at the tip
extendToSlot :: forall xs. CanHardFork xs
             => HardForkLedgerConfig xs
             -> SlotNo
             -> HardForkState LedgerState xs -> HardForkState LedgerState xs
extendToSlot :: HardForkLedgerConfig xs
-> SlotNo
-> HardForkState LedgerState xs
-> HardForkState LedgerState xs
extendToSlot ledgerCfg :: HardForkLedgerConfig xs
ledgerCfg@HardForkLedgerConfig{Shape xs
PerEraLedgerConfig xs
hardForkLedgerConfigPerEra :: PerEraLedgerConfig xs
hardForkLedgerConfigShape :: Shape xs
hardForkLedgerConfigPerEra :: forall (xs :: [*]).
HardForkLedgerConfig xs -> PerEraLedgerConfig xs
hardForkLedgerConfigShape :: forall (xs :: [*]). HardForkLedgerConfig xs -> Shape xs
..} SlotNo
slot ledgerSt :: HardForkState LedgerState xs
ledgerSt@(HardForkState Telescope (K Past) (Current LedgerState) xs
st) =
      Telescope (K Past) (Current LedgerState) xs
-> HardForkState LedgerState xs
forall (f :: * -> *) (xs :: [*]).
Telescope (K Past) (Current f) xs -> HardForkState f xs
HardForkState (Telescope (K Past) (Current LedgerState) xs
 -> HardForkState LedgerState xs)
-> (Telescope (K Past) (Current LedgerState) xs
    -> Telescope (K Past) (Current LedgerState) xs)
-> Telescope (K Past) (Current LedgerState) xs
-> HardForkState LedgerState xs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. I (Telescope (K Past) (Current LedgerState) xs)
-> Telescope (K Past) (Current LedgerState) xs
forall a. I a -> a
unI
    (I (Telescope (K Past) (Current LedgerState) xs)
 -> Telescope (K Past) (Current LedgerState) xs)
-> (Telescope (K Past) (Current LedgerState) xs
    -> I (Telescope (K Past) (Current LedgerState) xs))
-> Telescope (K Past) (Current LedgerState) xs
-> Telescope (K Past) (Current LedgerState) xs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InPairs
  (Requiring (K Bound) (Extend I (K Past) (Current LedgerState))) xs
-> NP (Current LedgerState -.-> (Maybe :.: K Bound)) xs
-> Telescope (K Past) (Current LedgerState) xs
-> I (Telescope (K Past) (Current LedgerState) xs)
forall k (m :: * -> *) (h :: k -> *) (g :: k -> *) (f :: k -> *)
       (xs :: [k]).
Monad m =>
InPairs (Requiring h (Extend m g f)) xs
-> NP (f -.-> (Maybe :.: h)) xs
-> Telescope g f xs
-> m (Telescope g f xs)
Telescope.extend
        ( (forall x y.
 Translate LedgerState x y
 -> Requiring
      (K Bound) (Extend I (K Past) (Current LedgerState)) x y)
-> InPairs (Translate LedgerState) xs
-> InPairs
     (Requiring (K Bound) (Extend I (K Past) (Current LedgerState))) 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 LedgerState x y
f -> (K Bound x -> Extend I (K Past) (Current LedgerState) x y)
-> Requiring
     (K Bound) (Extend I (K Past) (Current LedgerState)) 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 Bound x -> Extend I (K Past) (Current LedgerState) x y)
 -> Requiring
      (K Bound) (Extend I (K Past) (Current LedgerState)) x y)
-> (K Bound x -> Extend I (K Past) (Current LedgerState) x y)
-> Requiring
     (K Bound) (Extend I (K Past) (Current LedgerState)) x y
forall a b. (a -> b) -> a -> b
$ \(K Bound
t)
                           -> (Current LedgerState x -> I (K Past x, Current LedgerState y))
-> Extend I (K Past) (Current LedgerState) 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 LedgerState x -> I (K Past x, Current LedgerState y))
 -> Extend I (K Past) (Current LedgerState) x y)
-> (Current LedgerState x -> I (K Past x, Current LedgerState y))
-> Extend I (K Past) (Current LedgerState) x y
forall a b. (a -> b) -> a -> b
$ \Current LedgerState x
cur
                           -> (K Past x, Current LedgerState y)
-> I (K Past x, Current LedgerState y)
forall a. a -> I a
I ((K Past x, Current LedgerState y)
 -> I (K Past x, Current LedgerState y))
-> (K Past x, Current LedgerState y)
-> I (K Past x, Current LedgerState y)
forall a b. (a -> b) -> a -> b
$ Translate LedgerState x y
-> Bound
-> Current LedgerState x
-> (K Past x, Current LedgerState y)
forall blk blk'.
Translate LedgerState blk blk'
-> Bound
-> Current LedgerState blk
-> (K Past blk, Current LedgerState blk')
howExtend Translate LedgerState x y
f Bound
t Current LedgerState x
cur)
        (InPairs (Translate LedgerState) xs
 -> InPairs
      (Requiring (K Bound) (Extend I (K Past) (Current LedgerState))) xs)
-> InPairs (Translate LedgerState) xs
-> InPairs
     (Requiring (K Bound) (Extend I (K Past) (Current LedgerState))) xs
forall a b. (a -> b) -> a -> b
$ InPairs (Translate LedgerState) xs
translate
        )
        (Proxy SingleEraBlock
-> (forall a.
    SingleEraBlock a =>
    WrapPartialLedgerConfig a
    -> K EraParams a
    -> (-.->) (Current LedgerState) (Maybe :.: K Bound) a)
-> Prod NP WrapPartialLedgerConfig xs
-> NP (K EraParams) xs
-> NP (Current LedgerState -.-> (Maybe :.: K Bound)) xs
forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *)
       (f' :: k -> *) (f'' :: k -> *).
(AllN (Prod h) c xs, HAp h, HAp (Prod h)) =>
proxy c
-> (forall (a :: k). c a => f a -> f' a -> f'' a)
-> Prod h f xs
-> h f' xs
-> h f'' xs
hczipWith
           Proxy SingleEraBlock
proxySingle
           ((Current LedgerState a -> (:.:) Maybe (K Bound) a)
-> (-.->) (Current LedgerState) (Maybe :.: K Bound) a
forall k (f :: k -> *) (a :: k) (f' :: k -> *).
(f a -> f' a) -> (-.->) f f' a
fn ((Current LedgerState a -> (:.:) Maybe (K Bound) a)
 -> (-.->) (Current LedgerState) (Maybe :.: K Bound) a)
-> (WrapPartialLedgerConfig a
    -> K EraParams a
    -> Current LedgerState a
    -> (:.:) Maybe (K Bound) a)
-> WrapPartialLedgerConfig a
-> K EraParams a
-> (-.->) (Current LedgerState) (Maybe :.: K Bound) a
forall y z x0 x1. (y -> z) -> (x0 -> x1 -> y) -> x0 -> x1 -> z
.: WrapPartialLedgerConfig a
-> K EraParams a
-> Current LedgerState a
-> (:.:) Maybe (K Bound) a
forall blk.
SingleEraBlock blk =>
WrapPartialLedgerConfig blk
-> K EraParams blk
-> Current LedgerState blk
-> (:.:) Maybe (K Bound) blk
whenExtend)
           Prod NP WrapPartialLedgerConfig xs
NP WrapPartialLedgerConfig xs
pcfgs
           (Exactly xs EraParams -> NP (K EraParams) xs
forall (xs :: [*]) a. Exactly xs a -> NP (K a) xs
getExactly (Shape xs -> Exactly xs EraParams
forall (xs :: [*]). Shape xs -> Exactly xs EraParams
History.getShape Shape xs
hardForkLedgerConfigShape)))
    (Telescope (K Past) (Current LedgerState) xs
 -> HardForkState LedgerState xs)
-> Telescope (K Past) (Current LedgerState) xs
-> HardForkState LedgerState xs
forall a b. (a -> b) -> a -> b
$ Telescope (K Past) (Current LedgerState) xs
st
  where
    pcfgs :: NP WrapPartialLedgerConfig xs
pcfgs = PerEraLedgerConfig xs -> NP WrapPartialLedgerConfig xs
forall (xs :: [*]).
PerEraLedgerConfig xs -> NP WrapPartialLedgerConfig xs
getPerEraLedgerConfig PerEraLedgerConfig xs
hardForkLedgerConfigPerEra
    cfgs :: NP WrapLedgerConfig xs
cfgs  = Proxy SingleEraBlock
-> (forall a.
    SingleEraBlock a =>
    WrapPartialLedgerConfig a -> WrapLedgerConfig a)
-> NP WrapPartialLedgerConfig xs
-> NP WrapLedgerConfig xs
forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *)
       (f' :: k -> *).
(AllN (Prod h) c xs, HAp h) =>
proxy c
-> (forall (a :: k). c a => f a -> f' a) -> h f xs -> h f' xs
hcmap Proxy SingleEraBlock
proxySingle (EpochInfo Identity
-> WrapPartialLedgerConfig a -> WrapLedgerConfig a
forall blk.
HasPartialLedgerConfig blk =>
EpochInfo Identity
-> WrapPartialLedgerConfig blk -> WrapLedgerConfig blk
completeLedgerConfig'' EpochInfo Identity
ei) NP WrapPartialLedgerConfig xs
pcfgs
    ei :: EpochInfo Identity
ei    = HardForkLedgerConfig xs
-> HardForkState LedgerState xs -> EpochInfo Identity
forall (xs :: [*]).
All SingleEraBlock xs =>
HardForkLedgerConfig xs
-> HardForkState LedgerState xs -> EpochInfo Identity
epochInfoLedger HardForkLedgerConfig xs
ledgerCfg HardForkState LedgerState xs
ledgerSt

    -- Return the end of this era if we should transition to the next
    whenExtend :: SingleEraBlock              blk
               => WrapPartialLedgerConfig     blk
               -> K History.EraParams         blk
               -> Current LedgerState         blk
               -> (Maybe :.: K History.Bound) blk
    whenExtend :: WrapPartialLedgerConfig blk
-> K EraParams blk
-> Current LedgerState blk
-> (:.:) Maybe (K Bound) blk
whenExtend WrapPartialLedgerConfig blk
pcfg (K EraParams
eraParams) Current LedgerState blk
cur = Maybe (K Bound blk) -> (:.:) Maybe (K Bound) blk
forall l k (f :: l -> *) (g :: k -> l) (p :: k).
f (g p) -> (:.:) f g p
Comp (Maybe (K Bound blk) -> (:.:) Maybe (K Bound) blk)
-> Maybe (K Bound blk) -> (:.:) Maybe (K Bound) blk
forall a b. (a -> b) -> a -> b
$ Bound -> K Bound blk
forall k a (b :: k). a -> K a b
K (Bound -> K Bound blk) -> Maybe Bound -> Maybe (K Bound blk)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
        EpochNo
transition <- WrapPartialLedgerConfig blk
-> EraParams -> Bound -> LedgerState blk -> Maybe EpochNo
forall blk.
SingleEraBlock blk =>
WrapPartialLedgerConfig blk
-> EraParams -> Bound -> LedgerState blk -> Maybe EpochNo
singleEraTransition'
                        WrapPartialLedgerConfig blk
pcfg
                        EraParams
eraParams
                        (Current LedgerState blk -> Bound
forall (f :: * -> *) blk. Current f blk -> Bound
currentStart Current LedgerState blk
cur)
                        (Current LedgerState blk -> LedgerState blk
forall (f :: * -> *) blk. Current f blk -> f blk
currentState Current LedgerState blk
cur)
        let endBound :: Bound
endBound = HasCallStack => EraParams -> Bound -> EpochNo -> Bound
EraParams -> Bound -> EpochNo -> Bound
History.mkUpperBound
                         EraParams
eraParams
                         (Current LedgerState blk -> Bound
forall (f :: * -> *) blk. Current f blk -> Bound
currentStart Current LedgerState blk
cur)
                         EpochNo
transition
        Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (SlotNo
slot SlotNo -> SlotNo -> Bool
forall a. Ord a => a -> a -> Bool
>= Bound -> SlotNo
History.boundSlot Bound
endBound)
        Bound -> Maybe Bound
forall (m :: * -> *) a. Monad m => a -> m a
return Bound
endBound

    howExtend :: Translate LedgerState blk blk'
              -> History.Bound
              -> Current LedgerState blk
              -> (K Past blk, Current LedgerState blk')
    howExtend :: Translate LedgerState blk blk'
-> Bound
-> Current LedgerState blk
-> (K Past blk, Current LedgerState blk')
howExtend Translate LedgerState blk blk'
f Bound
currentEnd Current LedgerState blk
cur = (
          Past -> K Past blk
forall k a (b :: k). a -> K a b
K Past :: Bound -> Bound -> Past
Past {
              pastStart :: Bound
pastStart    = Current LedgerState blk -> Bound
forall (f :: * -> *) blk. Current f blk -> Bound
currentStart Current LedgerState blk
cur
            , pastEnd :: Bound
pastEnd      = Bound
currentEnd
            }
        , Current :: forall (f :: * -> *) blk. Bound -> f blk -> Current f blk
Current {
              currentStart :: Bound
currentStart = Bound
currentEnd
            , currentState :: LedgerState blk'
currentState = Translate LedgerState blk blk'
-> EpochNo -> LedgerState blk -> LedgerState blk'
forall (f :: * -> *) x y. Translate f x y -> EpochNo -> f x -> f y
translateWith Translate LedgerState blk blk'
f
                               (Bound -> EpochNo
History.boundEpoch Bound
currentEnd)
                               (Current LedgerState blk -> LedgerState blk
forall (f :: * -> *) blk. Current f blk -> f blk
currentState Current LedgerState blk
cur)
            }
        )

    translate :: InPairs (Translate LedgerState) xs
    translate :: InPairs (Translate LedgerState) xs
translate = NP WrapLedgerConfig xs
-> InPairs
     (RequiringBoth WrapLedgerConfig (Translate LedgerState)) xs
-> InPairs (Translate LedgerState) xs
forall k (h :: k -> *) (xs :: [k]) (f :: k -> k -> *).
NP h xs -> InPairs (RequiringBoth h f) xs -> InPairs f xs
InPairs.requiringBoth NP WrapLedgerConfig xs
cfgs (InPairs
   (RequiringBoth WrapLedgerConfig (Translate LedgerState)) xs
 -> InPairs (Translate LedgerState) xs)
-> InPairs
     (RequiringBoth WrapLedgerConfig (Translate LedgerState)) xs
-> InPairs (Translate LedgerState) xs
forall a b. (a -> b) -> a -> b
$
                  EraTranslation xs
-> InPairs
     (RequiringBoth WrapLedgerConfig (Translate LedgerState)) xs
forall (xs :: [*]).
EraTranslation xs
-> InPairs
     (RequiringBoth WrapLedgerConfig (Translate LedgerState)) xs
translateLedgerState EraTranslation xs
forall (xs :: [*]). CanHardFork xs => EraTranslation xs
hardForkEraTranslation