{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Ouroboros.Consensus.HardFork.Combinator.State (
module X
, getTip
, recover
, epochInfoLedger
, epochInfoPrecomputedTransitionInfo
, mostRecentTransitionInfo
, reconstructSummaryLedger
, extendToSlot
) where
import Prelude hiding (sequence)
import Control.Monad (guard)
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 :: 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
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 a (xs :: [a]) (proxy :: [a] -> *).
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 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 : 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
}
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
epochInfoLedger :: All SingleEraBlock xs
=> HardForkLedgerConfig xs
-> HardForkState LedgerState xs
-> EpochInfo (Except PastHorizonException)
epochInfoLedger :: 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
epochInfoPrecomputedTransitionInfo ::
History.Shape xs
-> TransitionInfo
-> HardForkState f xs
-> EpochInfo (Except PastHorizonException)
epochInfoPrecomputedTransitionInfo :: 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
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 (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
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