{-# LANGUAGE DataKinds                #-}
{-# LANGUAGE DisambiguateRecordFields #-}
{-# LANGUAGE EmptyCase                #-}
{-# LANGUAGE FlexibleContexts         #-}
{-# LANGUAGE FlexibleInstances        #-}
{-# LANGUAGE GADTs                    #-}
{-# LANGUAGE RecordWildCards          #-}
{-# LANGUAGE ScopedTypeVariables      #-}
{-# LANGUAGE TypeApplications         #-}
{-# LANGUAGE TypeOperators            #-}
module Ouroboros.Consensus.HardFork.Combinator.Embed.Nary (
    Inject (..)
  , inject'
    -- * Defaults
  , injectHardForkState
  , injectNestedCtxt_
  , injectQuery
    -- * Initial 'ExtLedgerState'
  , injectInitialExtLedgerState
  ) where

import           Data.Bifunctor (first)
import           Data.Coerce (Coercible, coerce)
import           Data.SOP.Dict (Dict (..))
import           Data.SOP.Strict

import           Ouroboros.Consensus.Block
import           Ouroboros.Consensus.Config
import qualified Ouroboros.Consensus.HardFork.History as History
import           Ouroboros.Consensus.HeaderValidation (AnnTip, HeaderState (..),
                     genesisHeaderState)
import           Ouroboros.Consensus.Ledger.Extended (ExtLedgerState (..))
import           Ouroboros.Consensus.Storage.Serialisation
import           Ouroboros.Consensus.TypeFamilyWrappers
import           Ouroboros.Consensus.Util ((.:))
import           Ouroboros.Consensus.Util.Counting (Exactly (..))
import           Ouroboros.Consensus.Util.SOP

import           Ouroboros.Consensus.HardFork.Combinator
import qualified Ouroboros.Consensus.HardFork.Combinator.State as State
import qualified Ouroboros.Consensus.HardFork.Combinator.Util.InPairs as InPairs

{-------------------------------------------------------------------------------
  Injection for a single block into a HardForkBlock
-------------------------------------------------------------------------------}

class Inject f where
  inject ::
       forall x xs. CanHardFork xs
    => Exactly xs History.Bound
       -- ^ Start bound of each era
    -> Index xs x
    -> f x
    -> f (HardForkBlock xs)

inject' ::
     forall f a b x xs.
     ( Inject f
     , CanHardFork xs
     , Coercible a (f x)
     , Coercible b (f (HardForkBlock xs))
     )
  => Proxy f -> Exactly xs History.Bound -> Index xs x -> a -> b
inject' :: Proxy f -> Exactly xs Bound -> Index xs x -> a -> b
inject' Proxy f
_ Exactly xs Bound
startBounds Index xs x
idx = f (HardForkBlock xs) -> b
coerce (f (HardForkBlock xs) -> b)
-> (a -> f (HardForkBlock xs)) -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Exactly xs Bound -> Index xs x -> f x -> f (HardForkBlock xs)
forall (f :: * -> *) x (xs :: [*]).
(Inject f, CanHardFork xs) =>
Exactly xs Bound -> Index xs x -> f x -> f (HardForkBlock xs)
inject @f Exactly xs Bound
startBounds Index xs x
idx (f x -> f (HardForkBlock xs))
-> (a -> f x) -> a -> f (HardForkBlock xs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> f x
coerce

{-------------------------------------------------------------------------------
  Defaults (to ease implementation)
-------------------------------------------------------------------------------}

injectNestedCtxt_ ::
     forall f x xs a.
     Index xs x
  -> NestedCtxt_ x f a
  -> NestedCtxt_ (HardForkBlock xs) f a
injectNestedCtxt_ :: Index xs x
-> NestedCtxt_ x f a -> NestedCtxt_ (HardForkBlock xs) f a
injectNestedCtxt_ Index xs x
idx NestedCtxt_ x f a
nc = case Index xs x
idx of
    Index xs x
IZ      -> NestedCtxt_ x f a -> NestedCtxt_ (HardForkBlock (x : xs)) f a
forall x (f :: * -> *) a (xs :: [*]).
NestedCtxt_ x f a -> NestedCtxt_ (HardForkBlock (x : xs)) f a
NCZ NestedCtxt_ x f a
nc
    IS Index xs x
idx' -> NestedCtxt_ (HardForkBlock xs) f a
-> NestedCtxt_ (HardForkBlock (y : xs)) f a
forall (xs :: [*]) (f :: * -> *) a x.
NestedCtxt_ (HardForkBlock xs) f a
-> NestedCtxt_ (HardForkBlock (x : xs)) f a
NCS (Index xs x
-> NestedCtxt_ x f a -> NestedCtxt_ (HardForkBlock xs) f a
forall (f :: * -> *) x (xs :: [*]) a.
Index xs x
-> NestedCtxt_ x f a -> NestedCtxt_ (HardForkBlock xs) f a
injectNestedCtxt_ Index xs x
idx' NestedCtxt_ x f a
nc)

injectQuery ::
     forall x xs result.
     Index xs x
  -> BlockQuery x result
  -> QueryIfCurrent xs result
injectQuery :: Index xs x -> BlockQuery x result -> QueryIfCurrent xs result
injectQuery Index xs x
idx BlockQuery x result
q = case Index xs x
idx of
    Index xs x
IZ      -> BlockQuery x result -> QueryIfCurrent (x : xs) result
forall x result (xs :: [*]).
BlockQuery x result -> QueryIfCurrent (x : xs) result
QZ BlockQuery x result
q
    IS Index xs x
idx' -> QueryIfCurrent xs result -> QueryIfCurrent (y : xs) result
forall (xs :: [*]) result x.
QueryIfCurrent xs result -> QueryIfCurrent (x : xs) result
QS (Index xs x -> BlockQuery x result -> QueryIfCurrent xs result
forall x (xs :: [*]) result.
Index xs x -> BlockQuery x result -> QueryIfCurrent xs result
injectQuery Index xs x
idx' BlockQuery x result
q)

injectHardForkState ::
     forall f x xs.
     Exactly xs History.Bound
     -- ^ Start bound of each era
  -> Index xs x
  -> f x
  -> HardForkState f xs
injectHardForkState :: Exactly xs Bound -> Index xs x -> f x -> HardForkState f xs
injectHardForkState Exactly xs Bound
startBounds Index xs x
idx f x
x =
    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) (Current f) xs -> HardForkState f xs
forall a b. (a -> b) -> a -> b
$ Exactly xs Bound -> Index xs x -> Telescope (K Past) (Current f) xs
forall (xs' :: [*]).
Exactly xs' Bound
-> Index xs' x -> Telescope (K Past) (Current f) xs'
go Exactly xs Bound
startBounds Index xs x
idx
  where
    go ::
         Exactly xs' History.Bound
      -> Index xs' x
      -> Telescope (K State.Past) (State.Current f) xs'
    go :: Exactly xs' Bound
-> Index xs' x -> Telescope (K Past) (Current f) xs'
go (ExactlyCons Bound
start Exactly xs Bound
_) Index xs' x
IZ =
        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 :: forall (f :: * -> *) blk. Bound -> f blk -> Current f blk
State.Current { currentStart :: Bound
currentStart = Bound
start, currentState :: f x
currentState = f x
x })
    go (ExactlyCons Bound
start startBounds' :: Exactly xs Bound
startBounds'@(ExactlyCons Bound
nextStart Exactly xs Bound
_)) (IS Index xs x
idx') =
        K Past x
-> Telescope (K Past) (Current f) xs
-> Telescope (K Past) (Current f) (x : xs)
forall a (g :: a -> *) (x :: a) (f :: a -> *) (xs :: [a]).
g x -> Telescope g f xs -> Telescope g f (x : xs)
TS (Past -> K Past x
forall k a (b :: k). a -> K a b
K Past :: Bound -> Bound -> Past
State.Past { pastStart :: Bound
pastStart = Bound
start, pastEnd :: Bound
pastEnd = Bound
nextStart })
           (Exactly xs Bound -> Index xs x -> Telescope (K Past) (Current f) xs
forall (xs' :: [*]).
Exactly xs' Bound
-> Index xs' x -> Telescope (K Past) (Current f) xs'
go Exactly xs Bound
startBounds' Index xs x
Index xs x
idx')
    go (ExactlyCons Bound
_ Exactly xs Bound
ExactlyNil) (IS Index xs x
idx') = case Index xs x
idx' of {}

{-------------------------------------------------------------------------------
  Instances
-------------------------------------------------------------------------------}

instance Inject I where
  inject :: Exactly xs Bound -> Index xs x -> I x -> I (HardForkBlock xs)
inject Exactly xs Bound
_ = Proxy I -> Index xs x -> I x -> I (HardForkBlock xs)
forall a1 (f :: a1 -> *) a2 b (x :: a1) (xs :: [a1]).
(Coercible a2 (f x), Coercible b (NS f xs)) =>
Proxy f -> Index xs x -> a2 -> b
injectNS' (Proxy I
forall k (t :: k). Proxy t
Proxy @I)

instance Inject Header where
  inject :: Exactly xs Bound
-> Index xs x -> Header x -> Header (HardForkBlock xs)
inject Exactly xs Bound
_ = Proxy Header -> Index xs x -> Header x -> Header (HardForkBlock xs)
forall a1 (f :: a1 -> *) a2 b (x :: a1) (xs :: [a1]).
(Coercible a2 (f x), Coercible b (NS f xs)) =>
Proxy f -> Index xs x -> a2 -> b
injectNS' (Proxy Header
forall k (t :: k). Proxy t
Proxy @Header)

instance Inject SerialisedHeader where
  inject :: Exactly xs Bound
-> Index xs x
-> SerialisedHeader x
-> SerialisedHeader (HardForkBlock xs)
inject Exactly xs Bound
_ Index xs x
idx =
        (SomeSecond (NestedCtxt Header) (HardForkBlock xs), ByteString)
-> SerialisedHeader (HardForkBlock xs)
forall blk.
(SomeSecond (NestedCtxt Header) blk, ByteString)
-> SerialisedHeader blk
serialisedHeaderFromPair
      ((SomeSecond (NestedCtxt Header) (HardForkBlock xs), ByteString)
 -> SerialisedHeader (HardForkBlock xs))
-> (SerialisedHeader x
    -> (SomeSecond (NestedCtxt Header) (HardForkBlock xs), ByteString))
-> SerialisedHeader x
-> SerialisedHeader (HardForkBlock xs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SomeSecond (NestedCtxt Header) x
 -> SomeSecond (NestedCtxt Header) (HardForkBlock xs))
-> (SomeSecond (NestedCtxt Header) x, ByteString)
-> (SomeSecond (NestedCtxt Header) (HardForkBlock xs), ByteString)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first ((forall a.
 NestedCtxt_ x Header a -> NestedCtxt_ (HardForkBlock xs) Header a)
-> SomeSecond (NestedCtxt Header) x
-> SomeSecond (NestedCtxt Header) (HardForkBlock xs)
forall blk (f :: * -> *) blk' (f' :: * -> *).
(forall a. NestedCtxt_ blk f a -> NestedCtxt_ blk' f' a)
-> SomeSecond (NestedCtxt f) blk -> SomeSecond (NestedCtxt f') blk'
mapSomeNestedCtxt (Index xs x
-> NestedCtxt_ x Header a
-> NestedCtxt_ (HardForkBlock xs) Header a
forall (f :: * -> *) x (xs :: [*]) a.
Index xs x
-> NestedCtxt_ x f a -> NestedCtxt_ (HardForkBlock xs) f a
injectNestedCtxt_ Index xs x
idx))
      ((SomeSecond (NestedCtxt Header) x, ByteString)
 -> (SomeSecond (NestedCtxt Header) (HardForkBlock xs), ByteString))
-> (SerialisedHeader x
    -> (SomeSecond (NestedCtxt Header) x, ByteString))
-> SerialisedHeader x
-> (SomeSecond (NestedCtxt Header) (HardForkBlock xs), ByteString)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SerialisedHeader x
-> (SomeSecond (NestedCtxt Header) x, ByteString)
forall blk.
SerialisedHeader blk
-> (SomeSecond (NestedCtxt Header) blk, ByteString)
serialisedHeaderToPair

instance Inject WrapHeaderHash where
  inject :: Exactly xs Bound
-> Index xs x
-> WrapHeaderHash x
-> WrapHeaderHash (HardForkBlock xs)
inject Exactly xs Bound
_ (Index xs x
idx :: Index xs x) =
    case Proxy SingleEraBlock -> Index xs x -> Dict SingleEraBlock x
forall k (c :: k -> Constraint) (xs :: [k]) (x :: k).
All c xs =>
Proxy c -> Index xs x -> Dict c x
dictIndexAll (Proxy SingleEraBlock
forall k (t :: k). Proxy t
Proxy @SingleEraBlock) Index xs x
idx of
      Dict SingleEraBlock x
Dict ->
          OneEraHash xs -> WrapHeaderHash (HardForkBlock xs)
forall blk. HeaderHash blk -> WrapHeaderHash blk
WrapHeaderHash
        (OneEraHash xs -> WrapHeaderHash (HardForkBlock xs))
-> (WrapHeaderHash x -> OneEraHash xs)
-> WrapHeaderHash x
-> WrapHeaderHash (HardForkBlock xs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShortByteString -> OneEraHash xs
forall k (xs :: [k]). ShortByteString -> OneEraHash xs
OneEraHash
        (ShortByteString -> OneEraHash xs)
-> (WrapHeaderHash x -> ShortByteString)
-> WrapHeaderHash x
-> OneEraHash xs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy x -> HeaderHash x -> ShortByteString
forall blk (proxy :: * -> *).
ConvertRawHash blk =>
proxy blk -> HeaderHash blk -> ShortByteString
toShortRawHash (Proxy x
forall k (t :: k). Proxy t
Proxy @x)
        (HeaderHash x -> ShortByteString)
-> (WrapHeaderHash x -> HeaderHash x)
-> WrapHeaderHash x
-> ShortByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WrapHeaderHash x -> HeaderHash x
forall blk. WrapHeaderHash blk -> HeaderHash blk
unwrapHeaderHash

instance Inject GenTx where
  inject :: Exactly xs Bound
-> Index xs x -> GenTx x -> GenTx (HardForkBlock xs)
inject Exactly xs Bound
_ = Proxy GenTx -> Index xs x -> GenTx x -> GenTx (HardForkBlock xs)
forall a1 (f :: a1 -> *) a2 b (x :: a1) (xs :: [a1]).
(Coercible a2 (f x), Coercible b (NS f xs)) =>
Proxy f -> Index xs x -> a2 -> b
injectNS' (Proxy GenTx
forall k (t :: k). Proxy t
Proxy @GenTx)

instance Inject WrapGenTxId where
  inject :: Exactly xs Bound
-> Index xs x -> WrapGenTxId x -> WrapGenTxId (HardForkBlock xs)
inject Exactly xs Bound
_ = Proxy WrapGenTxId
-> Index xs x -> WrapGenTxId x -> WrapGenTxId (HardForkBlock xs)
forall a1 (f :: a1 -> *) a2 b (x :: a1) (xs :: [a1]).
(Coercible a2 (f x), Coercible b (NS f xs)) =>
Proxy f -> Index xs x -> a2 -> b
injectNS' (Proxy WrapGenTxId
forall k (t :: k). Proxy t
Proxy @WrapGenTxId)

instance Inject WrapApplyTxErr where
  inject :: Exactly xs Bound
-> Index xs x
-> WrapApplyTxErr x
-> WrapApplyTxErr (HardForkBlock xs)
inject Exactly xs Bound
_ =
      (HardForkApplyTxErr xs -> WrapApplyTxErr (HardForkBlock xs)
forall blk. ApplyTxErr blk -> WrapApplyTxErr blk
WrapApplyTxErr (HardForkApplyTxErr xs -> WrapApplyTxErr (HardForkBlock xs))
-> (OneEraApplyTxErr xs -> HardForkApplyTxErr xs)
-> OneEraApplyTxErr xs
-> WrapApplyTxErr (HardForkBlock xs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OneEraApplyTxErr xs -> HardForkApplyTxErr xs
forall (xs :: [*]). OneEraApplyTxErr xs -> HardForkApplyTxErr xs
HardForkApplyTxErrFromEra)
        (OneEraApplyTxErr xs -> WrapApplyTxErr (HardForkBlock xs))
-> (Index xs x -> WrapApplyTxErr x -> OneEraApplyTxErr xs)
-> Index xs x
-> WrapApplyTxErr x
-> WrapApplyTxErr (HardForkBlock xs)
forall y z x0 x1. (y -> z) -> (x0 -> x1 -> y) -> x0 -> x1 -> z
.: Proxy WrapApplyTxErr
-> Index xs x -> WrapApplyTxErr x -> OneEraApplyTxErr xs
forall a1 (f :: a1 -> *) a2 b (x :: a1) (xs :: [a1]).
(Coercible a2 (f x), Coercible b (NS f xs)) =>
Proxy f -> Index xs x -> a2 -> b
injectNS' (Proxy WrapApplyTxErr
forall k (t :: k). Proxy t
Proxy @WrapApplyTxErr)

instance Inject (SomeSecond BlockQuery) where
  inject :: Exactly xs Bound
-> Index xs x
-> SomeSecond BlockQuery x
-> SomeSecond BlockQuery (HardForkBlock xs)
inject Exactly xs Bound
_ Index xs x
idx (SomeSecond BlockQuery x b
q) = BlockQuery (HardForkBlock xs) (HardForkQueryResult xs b)
-> SomeSecond BlockQuery (HardForkBlock xs)
forall (f :: * -> * -> *) a b. f a b -> SomeSecond f a
SomeSecond (QueryIfCurrent xs b
-> BlockQuery (HardForkBlock xs) (HardForkQueryResult xs b)
forall (xs :: [*]) result.
QueryIfCurrent xs result
-> BlockQuery (HardForkBlock xs) (HardForkQueryResult xs result)
QueryIfCurrent (Index xs x -> BlockQuery x b -> QueryIfCurrent xs b
forall x (xs :: [*]) result.
Index xs x -> BlockQuery x result -> QueryIfCurrent xs result
injectQuery Index xs x
idx BlockQuery x b
q))

instance Inject AnnTip where
  inject :: Exactly xs Bound
-> Index xs x -> AnnTip x -> AnnTip (HardForkBlock xs)
inject Exactly xs Bound
_ = NS AnnTip xs -> AnnTip (HardForkBlock xs)
forall (xs :: [*]).
SListI xs =>
NS AnnTip xs -> AnnTip (HardForkBlock xs)
undistribAnnTip (NS AnnTip xs -> AnnTip (HardForkBlock xs))
-> (Index xs x -> AnnTip x -> NS AnnTip xs)
-> Index xs x
-> AnnTip x
-> AnnTip (HardForkBlock xs)
forall y z x0 x1. (y -> z) -> (x0 -> x1 -> y) -> x0 -> x1 -> z
.: Proxy AnnTip -> Index xs x -> AnnTip x -> NS AnnTip xs
forall a1 (f :: a1 -> *) a2 b (x :: a1) (xs :: [a1]).
(Coercible a2 (f x), Coercible b (NS f xs)) =>
Proxy f -> Index xs x -> a2 -> b
injectNS' (Proxy AnnTip
forall k (t :: k). Proxy t
Proxy @AnnTip)

instance Inject LedgerState where
  inject :: Exactly xs Bound
-> Index xs x -> LedgerState x -> LedgerState (HardForkBlock xs)
inject Exactly xs Bound
startBounds Index xs x
idx =
      HardForkState LedgerState xs -> LedgerState (HardForkBlock xs)
forall (xs :: [*]).
HardForkState LedgerState xs -> LedgerState (HardForkBlock xs)
HardForkLedgerState (HardForkState LedgerState xs -> LedgerState (HardForkBlock xs))
-> (LedgerState x -> HardForkState LedgerState xs)
-> LedgerState x
-> LedgerState (HardForkBlock xs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Exactly xs Bound
-> Index xs x -> LedgerState x -> HardForkState LedgerState xs
forall (f :: * -> *) x (xs :: [*]).
Exactly xs Bound -> Index xs x -> f x -> HardForkState f xs
injectHardForkState Exactly xs Bound
startBounds Index xs x
idx

instance Inject WrapChainDepState where
  inject :: Exactly xs Bound
-> Index xs x
-> WrapChainDepState x
-> WrapChainDepState (HardForkBlock xs)
inject Exactly xs Bound
startBounds Index xs x
idx =
      HardForkState WrapChainDepState xs
-> WrapChainDepState (HardForkBlock xs)
coerce (HardForkState WrapChainDepState xs
 -> WrapChainDepState (HardForkBlock xs))
-> (WrapChainDepState x -> HardForkState WrapChainDepState xs)
-> WrapChainDepState x
-> WrapChainDepState (HardForkBlock xs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Exactly xs Bound
-> Index xs x
-> WrapChainDepState x
-> HardForkState WrapChainDepState xs
forall (f :: * -> *) x (xs :: [*]).
Exactly xs Bound -> Index xs x -> f x -> HardForkState f xs
injectHardForkState Exactly xs Bound
startBounds Index xs x
idx

instance Inject HeaderState where
  inject :: Exactly xs Bound
-> Index xs x -> HeaderState x -> HeaderState (HardForkBlock xs)
inject Exactly xs Bound
startBounds Index xs x
idx HeaderState {WithOrigin (AnnTip x)
ChainDepState (BlockProtocol x)
headerStateChainDep :: forall blk. HeaderState blk -> ChainDepState (BlockProtocol blk)
headerStateTip :: forall blk. HeaderState blk -> WithOrigin (AnnTip blk)
headerStateChainDep :: ChainDepState (BlockProtocol x)
headerStateTip :: WithOrigin (AnnTip x)
..} = HeaderState :: forall blk.
WithOrigin (AnnTip blk)
-> ChainDepState (BlockProtocol blk) -> HeaderState blk
HeaderState {
        headerStateTip :: WithOrigin (AnnTip (HardForkBlock xs))
headerStateTip      = Exactly xs Bound
-> Index xs x -> AnnTip x -> AnnTip (HardForkBlock xs)
forall (f :: * -> *) x (xs :: [*]).
(Inject f, CanHardFork xs) =>
Exactly xs Bound -> Index xs x -> f x -> f (HardForkBlock xs)
inject Exactly xs Bound
startBounds Index xs x
idx (AnnTip x -> AnnTip (HardForkBlock xs))
-> WithOrigin (AnnTip x) -> WithOrigin (AnnTip (HardForkBlock xs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> WithOrigin (AnnTip x)
headerStateTip
      , headerStateChainDep :: ChainDepState (BlockProtocol (HardForkBlock xs))
headerStateChainDep = WrapChainDepState (HardForkBlock xs)
-> ChainDepState (BlockProtocol (HardForkBlock xs))
forall blk.
WrapChainDepState blk -> ChainDepState (BlockProtocol blk)
unwrapChainDepState
                            (WrapChainDepState (HardForkBlock xs)
 -> ChainDepState (BlockProtocol (HardForkBlock xs)))
-> WrapChainDepState (HardForkBlock xs)
-> ChainDepState (BlockProtocol (HardForkBlock xs))
forall a b. (a -> b) -> a -> b
$ Exactly xs Bound
-> Index xs x
-> WrapChainDepState x
-> WrapChainDepState (HardForkBlock xs)
forall (f :: * -> *) x (xs :: [*]).
(Inject f, CanHardFork xs) =>
Exactly xs Bound -> Index xs x -> f x -> f (HardForkBlock xs)
inject Exactly xs Bound
startBounds Index xs x
idx
                            (WrapChainDepState x -> WrapChainDepState (HardForkBlock xs))
-> WrapChainDepState x -> WrapChainDepState (HardForkBlock xs)
forall a b. (a -> b) -> a -> b
$ ChainDepState (BlockProtocol x) -> WrapChainDepState x
forall blk.
ChainDepState (BlockProtocol blk) -> WrapChainDepState blk
WrapChainDepState ChainDepState (BlockProtocol x)
headerStateChainDep
      }

instance Inject ExtLedgerState where
  inject :: Exactly xs Bound
-> Index xs x
-> ExtLedgerState x
-> ExtLedgerState (HardForkBlock xs)
inject Exactly xs Bound
startBounds Index xs x
idx ExtLedgerState {LedgerState x
HeaderState x
headerState :: forall blk. ExtLedgerState blk -> HeaderState blk
ledgerState :: forall blk. ExtLedgerState blk -> LedgerState blk
headerState :: HeaderState x
ledgerState :: LedgerState x
..} = ExtLedgerState :: forall blk.
LedgerState blk -> HeaderState blk -> ExtLedgerState blk
ExtLedgerState {
        ledgerState :: LedgerState (HardForkBlock xs)
ledgerState = Exactly xs Bound
-> Index xs x -> LedgerState x -> LedgerState (HardForkBlock xs)
forall (f :: * -> *) x (xs :: [*]).
(Inject f, CanHardFork xs) =>
Exactly xs Bound -> Index xs x -> f x -> f (HardForkBlock xs)
inject Exactly xs Bound
startBounds Index xs x
idx LedgerState x
ledgerState
      , headerState :: HeaderState (HardForkBlock xs)
headerState = Exactly xs Bound
-> Index xs x -> HeaderState x -> HeaderState (HardForkBlock xs)
forall (f :: * -> *) x (xs :: [*]).
(Inject f, CanHardFork xs) =>
Exactly xs Bound -> Index xs x -> f x -> f (HardForkBlock xs)
inject Exactly xs Bound
startBounds Index xs x
idx HeaderState x
headerState
      }

{-------------------------------------------------------------------------------
  Initial ExtLedgerState
-------------------------------------------------------------------------------}

-- | Inject the first era's initial 'ExtLedgerState' and trigger any
-- translations that should take place in the very first slot.
--
-- Performs any hard forks scheduled via 'TriggerHardForkAtEpoch'.
--
-- Note: we can translate across multiple eras when computing the initial ledger
-- state, but we do not support translation across multiple eras in general;
-- extending 'applyChainTick' to translate across more than one era is not
-- problematic, but extending 'ledgerViewForecastAt' is a lot more subtle; see
-- @forecastNotFinal@.
injectInitialExtLedgerState ::
     forall x xs. CanHardFork (x ': xs)
  => TopLevelConfig (HardForkBlock (x ': xs))
  -> ExtLedgerState x
  -> ExtLedgerState (HardForkBlock (x ': xs))
injectInitialExtLedgerState :: TopLevelConfig (HardForkBlock (x : xs))
-> ExtLedgerState x -> ExtLedgerState (HardForkBlock (x : xs))
injectInitialExtLedgerState TopLevelConfig (HardForkBlock (x : xs))
cfg ExtLedgerState x
extLedgerState0 =
    ExtLedgerState :: forall blk.
LedgerState blk -> HeaderState blk -> ExtLedgerState blk
ExtLedgerState {
        ledgerState :: LedgerState (HardForkBlock (x : xs))
ledgerState = LedgerState (HardForkBlock (x : xs))
targetEraLedgerState
      , headerState :: HeaderState (HardForkBlock (x : xs))
headerState = HeaderState (HardForkBlock (x : xs))
targetEraHeaderState
      }
  where
    cfgs :: NP TopLevelConfig (x ': xs)
    cfgs :: NP TopLevelConfig (x : xs)
cfgs =
        EpochInfo (Except PastHorizonException)
-> TopLevelConfig (HardForkBlock (x : xs))
-> NP TopLevelConfig (x : xs)
forall (xs :: [*]).
All SingleEraBlock xs =>
EpochInfo (Except PastHorizonException)
-> TopLevelConfig (HardForkBlock xs) -> NP TopLevelConfig xs
distribTopLevelConfig
          (HardForkLedgerConfig (x : xs)
-> HardForkState LedgerState (x : xs)
-> EpochInfo (Except PastHorizonException)
forall (xs :: [*]).
All SingleEraBlock xs =>
HardForkLedgerConfig xs
-> HardForkState LedgerState xs
-> EpochInfo (Except PastHorizonException)
State.epochInfoLedger
             (TopLevelConfig (HardForkBlock (x : xs))
-> LedgerConfig (HardForkBlock (x : xs))
forall blk. TopLevelConfig blk -> LedgerConfig blk
configLedger TopLevelConfig (HardForkBlock (x : xs))
cfg)
             (LedgerState (HardForkBlock (x : xs))
-> HardForkState LedgerState (x : xs)
forall (xs :: [*]).
LedgerState (HardForkBlock xs) -> HardForkState LedgerState xs
hardForkLedgerStatePerEra LedgerState (HardForkBlock (x : xs))
targetEraLedgerState))
          TopLevelConfig (HardForkBlock (x : xs))
cfg

    targetEraLedgerState :: LedgerState (HardForkBlock (x ': xs))
    targetEraLedgerState :: LedgerState (HardForkBlock (x : xs))
targetEraLedgerState =
        HardForkState LedgerState (x : xs)
-> LedgerState (HardForkBlock (x : xs))
forall (xs :: [*]).
HardForkState LedgerState xs -> LedgerState (HardForkBlock xs)
HardForkLedgerState (HardForkState LedgerState (x : xs)
 -> LedgerState (HardForkBlock (x : xs)))
-> HardForkState LedgerState (x : xs)
-> LedgerState (HardForkBlock (x : xs))
forall a b. (a -> b) -> a -> b
$
          -- We can immediately extend it to the right slot, executing any
          -- scheduled hard forks in the first slot
          HardForkLedgerConfig (x : xs)
-> SlotNo
-> HardForkState LedgerState (x : xs)
-> HardForkState LedgerState (x : xs)
forall (xs :: [*]).
CanHardFork xs =>
HardForkLedgerConfig xs
-> SlotNo
-> HardForkState LedgerState xs
-> HardForkState LedgerState xs
State.extendToSlot
            (TopLevelConfig (HardForkBlock (x : xs))
-> LedgerConfig (HardForkBlock (x : xs))
forall blk. TopLevelConfig blk -> LedgerConfig blk
configLedger TopLevelConfig (HardForkBlock (x : xs))
cfg)
            (Word64 -> SlotNo
SlotNo Word64
0)
            (LedgerState x -> HardForkState LedgerState (x : xs)
forall (f :: * -> *) x (xs :: [*]). f x -> HardForkState f (x : xs)
initHardForkState (ExtLedgerState x -> LedgerState x
forall blk. ExtLedgerState blk -> LedgerState blk
ledgerState ExtLedgerState x
extLedgerState0))

    firstEraChainDepState :: HardForkChainDepState (x ': xs)
    firstEraChainDepState :: HardForkChainDepState (x : xs)
firstEraChainDepState =
        WrapChainDepState x -> HardForkChainDepState (x : xs)
forall (f :: * -> *) x (xs :: [*]). f x -> HardForkState f (x : xs)
initHardForkState (WrapChainDepState x -> HardForkChainDepState (x : xs))
-> WrapChainDepState x -> HardForkChainDepState (x : xs)
forall a b. (a -> b) -> a -> b
$
          ChainDepState (BlockProtocol x) -> WrapChainDepState x
forall blk.
ChainDepState (BlockProtocol blk) -> WrapChainDepState blk
WrapChainDepState (ChainDepState (BlockProtocol x) -> WrapChainDepState x)
-> ChainDepState (BlockProtocol x) -> WrapChainDepState x
forall a b. (a -> b) -> a -> b
$
            HeaderState x -> ChainDepState (BlockProtocol x)
forall blk. HeaderState blk -> ChainDepState (BlockProtocol blk)
headerStateChainDep (HeaderState x -> ChainDepState (BlockProtocol x))
-> HeaderState x -> ChainDepState (BlockProtocol x)
forall a b. (a -> b) -> a -> b
$
              ExtLedgerState x -> HeaderState x
forall blk. ExtLedgerState blk -> HeaderState blk
headerState ExtLedgerState x
extLedgerState0

    targetEraChainDepState :: HardForkChainDepState (x ': xs)
    targetEraChainDepState :: HardForkChainDepState (x : xs)
targetEraChainDepState =
        -- Align the 'ChainDepState' with the ledger state of the target era.
        InPairs (Translate WrapChainDepState) (x : xs)
-> NP
     (LedgerState -.-> (WrapChainDepState -.-> WrapChainDepState))
     (x : xs)
-> HardForkState LedgerState (x : xs)
-> HardForkChainDepState (x : xs)
-> HardForkChainDepState (x : xs)
forall (xs :: [*]) (f :: * -> *) (f' :: * -> *) (f'' :: * -> *).
All SingleEraBlock xs =>
InPairs (Translate f) xs
-> NP (f' -.-> (f -.-> f'')) xs
-> HardForkState f' xs
-> HardForkState f xs
-> HardForkState f'' xs
State.align
          (NP WrapConsensusConfig (x : xs)
-> InPairs
     (RequiringBoth WrapConsensusConfig (Translate WrapChainDepState))
     (x : xs)
-> InPairs (Translate WrapChainDepState) (x : xs)
forall k (h :: k -> *) (xs :: [k]) (f :: k -> k -> *).
NP h xs -> InPairs (RequiringBoth h f) xs -> InPairs f xs
InPairs.requiringBoth
            ((forall a. TopLevelConfig a -> WrapConsensusConfig a)
-> NP TopLevelConfig (x : xs) -> NP WrapConsensusConfig (x : 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 (ConsensusConfig (BlockProtocol a) -> WrapConsensusConfig a
forall blk.
ConsensusConfig (BlockProtocol blk) -> WrapConsensusConfig blk
WrapConsensusConfig (ConsensusConfig (BlockProtocol a) -> WrapConsensusConfig a)
-> (TopLevelConfig a -> ConsensusConfig (BlockProtocol a))
-> TopLevelConfig a
-> WrapConsensusConfig a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TopLevelConfig a -> ConsensusConfig (BlockProtocol a)
forall blk.
TopLevelConfig blk -> ConsensusConfig (BlockProtocol blk)
configConsensus) NP TopLevelConfig (x : xs)
cfgs)
            (EraTranslation (x : xs)
-> InPairs
     (RequiringBoth WrapConsensusConfig (Translate WrapChainDepState))
     (x : xs)
forall (xs :: [*]).
EraTranslation xs
-> InPairs
     (RequiringBoth WrapConsensusConfig (Translate WrapChainDepState))
     xs
translateChainDepState EraTranslation (x : xs)
forall (xs :: [*]). CanHardFork xs => EraTranslation xs
hardForkEraTranslation))
          ((forall a.
 (-.->) LedgerState (WrapChainDepState -.-> WrapChainDepState) a)
-> NP
     (LedgerState -.-> (WrapChainDepState -.-> WrapChainDepState))
     (x : xs)
forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *).
(HPure h, SListIN h xs) =>
(forall (a :: k). f a) -> h f xs
hpure ((LedgerState a -> WrapChainDepState a -> WrapChainDepState a)
-> (-.->) LedgerState (WrapChainDepState -.-> WrapChainDepState) a
forall k (f :: k -> *) (a :: k) (f' :: k -> *) (f'' :: k -> *).
(f a -> f' a -> f'' a) -> (-.->) f (f' -.-> f'') a
fn_2 (\LedgerState a
_ WrapChainDepState a
st -> WrapChainDepState a
st)))
          (LedgerState (HardForkBlock (x : xs))
-> HardForkState LedgerState (x : xs)
forall (xs :: [*]).
LedgerState (HardForkBlock xs) -> HardForkState LedgerState xs
hardForkLedgerStatePerEra LedgerState (HardForkBlock (x : xs))
targetEraLedgerState)
          HardForkChainDepState (x : xs)
firstEraChainDepState

    targetEraHeaderState :: HeaderState (HardForkBlock (x ': xs))
    targetEraHeaderState :: HeaderState (HardForkBlock (x : xs))
targetEraHeaderState = ChainDepState (BlockProtocol (HardForkBlock (x : xs)))
-> HeaderState (HardForkBlock (x : xs))
forall blk. ChainDepState (BlockProtocol blk) -> HeaderState blk
genesisHeaderState ChainDepState (BlockProtocol (HardForkBlock (x : xs)))
HardForkChainDepState (x : xs)
targetEraChainDepState