{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# 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
  , epochInfoLedger
  , epochInfoPrecomputedTransitionInfo
  , mostRecentTransitionInfo
  , reconstructSummaryLedger
    -- * Ledger specific functionality
  , extendToSlot
  ) where

import           Control.Monad (guard)
import           Data.Functor.Product
import           Data.Proxy
import           Data.SOP.BasicFunctors
import           Data.SOP.Constraint
import           Data.SOP.Counting (getExactly)
import           Data.SOP.InPairs (InPairs, Requiring (..))
import qualified Data.SOP.InPairs as InPairs
import           Data.SOP.Strict
import           Data.SOP.Telescope (Extend (..), ScanNext (..), Telescope)
import qualified Data.SOP.Telescope as Telescope
import           Ouroboros.Consensus.Block
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.State.Infra as X
import           Ouroboros.Consensus.HardFork.Combinator.State.Instances as X ()
import           Ouroboros.Consensus.HardFork.Combinator.State.Types as X
import           Ouroboros.Consensus.HardFork.Combinator.Translation
import qualified Ouroboros.Consensus.HardFork.History as History
import           Ouroboros.Consensus.Ledger.Abstract hiding (getTip)
import           Ouroboros.Consensus.Util ((.:))
import           Prelude hiding (sequence)

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

getTip :: forall f xs. CanHardFork xs
       => (forall blk. SingleEraBlock blk => f blk -> Point blk)
       -> HardForkState f xs -> Point (HardForkBlock xs)
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
getLedgerTip =
      NS (K (Point (HardForkBlock xs))) xs -> Point (HardForkBlock xs)
NS (K (Point (HardForkBlock xs))) xs
-> CollapseTo NS (Point (HardForkBlock xs))
forall (xs :: [*]) a.
SListIN NS xs =>
NS (K a) xs -> CollapseTo NS a
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 :: forall blk.
SingleEraBlock blk =>
Point blk -> Point (HardForkBlock xs)
injPoint Point blk
GenesisPoint     = Point (HardForkBlock xs)
forall {k} (block :: k). Point block
GenesisPoint
    injPoint (BlockPoint SlotNo
s HeaderHash blk
h) = SlotNo -> HeaderHash (HardForkBlock xs) -> Point (HardForkBlock xs)
forall {k} (block :: k). 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
forall (proxy :: * -> *).
proxy blk -> HeaderHash blk -> ShortByteString
toShortRawHash (forall t. Proxy t
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 :: forall (f :: * -> *) (xs :: [*]).
CanHardFork xs =>
Telescope (K Past) f xs -> HardForkState f xs
recover =
    case Proxy xs -> ProofNonEmpty xs
forall {a} (xs :: [a]) (proxy :: [a] -> *).
IsNonEmpty xs =>
proxy xs -> ProofNonEmpty xs
forall (proxy :: [*] -> *). proxy xs -> ProofNonEmpty xs
isNonEmpty (forall (t :: [*]). Proxy t
forall {k} (t :: k). Proxy t
Proxy @xs) of
      ProofNonEmpty {} ->
          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)
-> (Telescope (K Past) f xs -> Telescope (K Past) (Current f) xs)
-> Telescope (K Past) f xs
-> HardForkState f 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) xs
-> Telescope (K Past) (Current f) 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 K Bound x
_ K Past x
past) -> K Past x
past)
            Product (K Bound) f x -> Current f x
forall x. Product (K Bound) f x -> Current f x
recoverCurrent
        (Telescope (Product (K Bound) (K Past)) (Product (K Bound) f) xs
 -> Telescope (K Past) (Current f) xs)
-> (Telescope (K Past) f xs
    -> Telescope (Product (K Bound) (K Past)) (Product (K Bound) f) xs)
-> Telescope (K Past) f xs
-> Telescope (K Past) (Current f) xs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InPairs (ScanNext (K Bound) (K Past)) (x : xs1)
-> K Bound x
-> Telescope (K Past) f (x : xs1)
-> Telescope
     (Product (K Bound) (K Past)) (Product (K Bound) f) (x : xs1)
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 : xs1)
forall {k} (xs :: [k]) (f :: k -> k -> *).
(SListI xs, IsNonEmpty xs) =>
(forall (x :: k) (y :: k). 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 : xs1))
-> (forall x y. ScanNext (K Bound) (K Past) x y)
-> InPairs (ScanNext (K Bound) (K Past)) (x : xs1)
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 :: forall x. Product (K Bound) f x -> Current f x
recoverCurrent (Pair (K Bound
prevEnd) f blk
st) = 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 :: forall (xs :: [*]).
All SingleEraBlock xs =>
HardForkLedgerConfig xs
-> HardForkState LedgerState xs -> TransitionInfo
mostRecentTransitionInfo HardForkLedgerConfig{Shape xs
PerEraLedgerConfig xs
hardForkLedgerConfigShape :: Shape xs
hardForkLedgerConfigPerEra :: PerEraLedgerConfig xs
hardForkLedgerConfigShape :: forall (xs :: [*]). HardForkLedgerConfig xs -> Shape xs
hardForkLedgerConfigPerEra :: forall (xs :: [*]).
HardForkLedgerConfig xs -> PerEraLedgerConfig xs
..} HardForkState LedgerState xs
st =
    NS (K TransitionInfo) xs -> CollapseTo NS TransitionInfo
forall (xs :: [*]) a.
SListIN NS xs =>
NS (K a) xs -> CollapseTo NS a
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
        WrapPartialLedgerConfig a
-> K EraParams a -> Current LedgerState a -> K TransitionInfo a
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 :: forall a.
SingleEraBlock a =>
WrapPartialLedgerConfig a
-> K EraParams a -> Current LedgerState a -> K TransitionInfo a
getTransition WrapPartialLedgerConfig blk
cfg (K EraParams
eraParams) Current{LedgerState blk
Bound
currentStart :: forall (f :: * -> *) blk. Current f blk -> Bound
currentState :: forall (f :: * -> *) blk. Current f blk -> f blk
currentStart :: Bound
currentState :: LedgerState blk
..} = 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 :: forall (xs :: [*]).
All SingleEraBlock xs =>
HardForkLedgerConfig xs
-> HardForkState LedgerState xs -> Summary xs
reconstructSummaryLedger cfg :: HardForkLedgerConfig xs
cfg@HardForkLedgerConfig{Shape xs
PerEraLedgerConfig xs
hardForkLedgerConfigShape :: forall (xs :: [*]). HardForkLedgerConfig xs -> Shape xs
hardForkLedgerConfigPerEra :: forall (xs :: [*]).
HardForkLedgerConfig xs -> PerEraLedgerConfig xs
hardForkLedgerConfigShape :: Shape xs
hardForkLedgerConfigPerEra :: PerEraLedgerConfig 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 (Except PastHorizonException)
epochInfoLedger :: forall (xs :: [*]).
All SingleEraBlock xs =>
HardForkLedgerConfig xs
-> HardForkState LedgerState xs
-> EpochInfo (Except PastHorizonException)
epochInfoLedger HardForkLedgerConfig xs
cfg HardForkState LedgerState xs
st =
    Summary xs -> EpochInfo (Except PastHorizonException)
forall (xs :: [*]).
Summary xs -> EpochInfo (Except PastHorizonException)
History.summaryToEpochInfo (Summary xs -> EpochInfo (Except PastHorizonException))
-> Summary xs -> EpochInfo (Except PastHorizonException)
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'
--
-- The transition and state arguments are acquired either from a ticked ledger
-- state or a ledger view.
epochInfoPrecomputedTransitionInfo ::
     History.Shape xs
  -> TransitionInfo
  -> HardForkState f xs
  -> EpochInfo (Except PastHorizonException)
epochInfoPrecomputedTransitionInfo :: forall (xs :: [*]) (f :: * -> *).
Shape xs
-> TransitionInfo
-> HardForkState f xs
-> EpochInfo (Except PastHorizonException)
epochInfoPrecomputedTransitionInfo Shape xs
shape TransitionInfo
transition HardForkState f xs
st =
    Summary xs -> EpochInfo (Except PastHorizonException)
forall (xs :: [*]).
Summary xs -> EpochInfo (Except PastHorizonException)
History.summaryToEpochInfo (Summary xs -> EpochInfo (Except PastHorizonException))
-> Summary xs -> EpochInfo (Except PastHorizonException)
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 :: forall (xs :: [*]).
CanHardFork xs =>
HardForkLedgerConfig xs
-> SlotNo
-> HardForkState LedgerState xs
-> HardForkState LedgerState xs
extendToSlot ledgerCfg :: HardForkLedgerConfig xs
ledgerCfg@HardForkLedgerConfig{Shape xs
PerEraLedgerConfig xs
hardForkLedgerConfigShape :: forall (xs :: [*]). HardForkLedgerConfig xs -> Shape xs
hardForkLedgerConfigPerEra :: forall (xs :: [*]).
HardForkLedgerConfig xs -> PerEraLedgerConfig xs
hardForkLedgerConfigShape :: Shape xs
hardForkLedgerConfigPerEra :: PerEraLedgerConfig 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} {k1} (h :: k -> *) (f :: k -> k1 -> *) (x :: k)
       (y :: k1).
(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 (Except PastHorizonException)
-> WrapPartialLedgerConfig a -> WrapLedgerConfig a
forall blk.
HasPartialLedgerConfig blk =>
EpochInfo (Except PastHorizonException)
-> WrapPartialLedgerConfig blk -> WrapLedgerConfig blk
completeLedgerConfig'' EpochInfo (Except PastHorizonException)
ei) NP WrapPartialLedgerConfig xs
pcfgs
    ei :: EpochInfo (Except PastHorizonException)
ei    = HardForkLedgerConfig xs
-> HardForkState LedgerState xs
-> EpochInfo (Except PastHorizonException)
forall (xs :: [*]).
All SingleEraBlock xs =>
HardForkLedgerConfig xs
-> HardForkState LedgerState xs
-> EpochInfo (Except PastHorizonException)
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 :: forall blk.
SingleEraBlock blk =>
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 a. a -> Maybe a
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 :: forall blk blk'.
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 {
              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 {
              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