{-# LANGUAGE DataKinds #-}
{-# 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.BasicFunctors
import           Data.SOP.Counting (Exactly (..))
import           Data.SOP.Dict (Dict (..))
import           Data.SOP.Index
import qualified Data.SOP.InPairs as InPairs
import           Data.SOP.Strict
import           Ouroboros.Consensus.Block
import           Ouroboros.Consensus.Config
import           Ouroboros.Consensus.HardFork.Combinator
import qualified Ouroboros.Consensus.HardFork.Combinator.State as State
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 ((.:))

{-------------------------------------------------------------------------------
  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' :: forall (f :: * -> *) a b x (xs :: [*]).
(Inject f, CanHardFork xs, Coercible a (f x),
 Coercible b (f (HardForkBlock xs))) =>
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
forall a b. Coercible a b => a -> b
coerce (f (HardForkBlock xs) -> b)
-> (a -> f (HardForkBlock xs)) -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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
forall a b. Coercible a b => a -> b
coerce

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

injectNestedCtxt_ ::
     forall f x xs a.
     Index xs x
  -> NestedCtxt_ x f a
  -> NestedCtxt_ (HardForkBlock xs) f a
injectNestedCtxt_ :: 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 = case Index xs x
idx of
    Index xs x
IZ      -> NestedCtxt_ x f a -> NestedCtxt_ (HardForkBlock (x : xs1)) f a
forall x (a :: * -> *) b (xs1 :: [*]).
NestedCtxt_ x a b -> NestedCtxt_ (HardForkBlock (x : xs1)) a b
NCZ NestedCtxt_ x f a
nc
    IS Index xs1 x
idx' -> NestedCtxt_ (HardForkBlock xs1) f a
-> NestedCtxt_ (HardForkBlock (y : xs1)) f a
forall (xs1 :: [*]) (a :: * -> *) b x.
NestedCtxt_ (HardForkBlock xs1) a b
-> NestedCtxt_ (HardForkBlock (x : xs1)) a b
NCS (Index xs1 x
-> NestedCtxt_ x f a -> NestedCtxt_ (HardForkBlock xs1) f a
forall (f :: * -> *) x (xs :: [*]) a.
Index xs x
-> NestedCtxt_ x f a -> NestedCtxt_ (HardForkBlock xs) f a
injectNestedCtxt_ Index xs1 x
idx' NestedCtxt_ x f a
nc)

injectQuery ::
     forall x xs result.
     Index xs x
  -> BlockQuery x result
  -> QueryIfCurrent xs result
injectQuery :: forall x (xs :: [*]) result.
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 : xs1) result
forall x b (xs :: [*]). BlockQuery x b -> QueryIfCurrent (x : xs) b
QZ BlockQuery x result
q
    IS Index xs1 x
idx' -> QueryIfCurrent xs1 result -> QueryIfCurrent (y : xs1) result
forall (xs :: [*]) b x.
QueryIfCurrent xs b -> QueryIfCurrent (x : xs) b
QS (Index xs1 x -> BlockQuery x result -> QueryIfCurrent xs1 result
forall x (xs :: [*]) result.
Index xs x -> BlockQuery x result -> QueryIfCurrent xs result
injectQuery Index xs1 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 :: forall (f :: * -> *) x (xs :: [*]).
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 :: forall (xs' :: [*]).
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 {k} (f :: k -> *) (x :: k) (g :: k -> *) (xs1 :: [k]).
f x -> Telescope g f (x : xs1)
TZ (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 xs1 x
idx') =
        K Past x
-> Telescope (K Past) (Current f) xs
-> Telescope (K Past) (Current f) (x : xs)
forall {k} (g :: k -> *) (x :: k) (f :: k -> *) (xs1 :: [k]).
g x -> Telescope g f xs1 -> Telescope g f (x : xs1)
TS (Past -> K Past x
forall k a (b :: k). a -> K a b
K 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 xs1 x
idx')
    go (ExactlyCons Bound
_ Exactly xs Bound
ExactlyNil) (IS Index xs1 x
idx') = case Index xs1 x
idx' of {}
    go Exactly xs' Bound
ExactlyNil Index xs' x
idx' = case Index xs' x
idx' of {}

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

instance Inject I where
  inject :: forall x (xs :: [*]).
CanHardFork xs =>
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 {k} (f :: k -> *) a b (x :: k) (xs :: [k]).
(Coercible a (f x), Coercible b (NS f xs)) =>
Proxy f -> Index xs x -> a -> b
injectNS' (forall {k} (t :: k). Proxy t
forall (t :: * -> *). Proxy t
Proxy @I)

instance Inject Header where
  inject :: forall x (xs :: [*]).
CanHardFork xs =>
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 {k} (f :: k -> *) a b (x :: k) (xs :: [k]).
(Coercible a (f x), Coercible b (NS f xs)) =>
Proxy f -> Index xs x -> a -> b
injectNS' (forall {k} (t :: k). Proxy t
forall (t :: * -> *). Proxy t
Proxy @Header)

instance Inject SerialisedHeader where
  inject :: forall x (xs :: [*]).
CanHardFork xs =>
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 a b c. (a -> b) -> (a, c) -> (b, c)
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 :: forall x (xs :: [*]).
CanHardFork xs =>
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 (forall {k} (t :: k). Proxy t
forall (t :: * -> Constraint). Proxy t
Proxy @SingleEraBlock) Index xs x
idx of
      Dict SingleEraBlock x
Dict ->
          HeaderHash (HardForkBlock xs) -> WrapHeaderHash (HardForkBlock xs)
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
forall (proxy :: * -> *).
proxy x -> HeaderHash x -> ShortByteString
toShortRawHash (forall t. Proxy t
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 :: forall x (xs :: [*]).
CanHardFork xs =>
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 {k} (f :: k -> *) a b (x :: k) (xs :: [k]).
(Coercible a (f x), Coercible b (NS f xs)) =>
Proxy f -> Index xs x -> a -> b
injectNS' (forall {k} (t :: k). Proxy t
forall (t :: * -> *). Proxy t
Proxy @GenTx)

instance Inject WrapGenTxId where
  inject :: forall x (xs :: [*]).
CanHardFork xs =>
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 {k} (f :: k -> *) a b (x :: k) (xs :: [k]).
(Coercible a (f x), Coercible b (NS f xs)) =>
Proxy f -> Index xs x -> a -> b
injectNS' (forall {k} (t :: k). Proxy t
forall (t :: * -> *). Proxy t
Proxy @WrapGenTxId)

instance Inject WrapApplyTxErr where
  inject :: forall x (xs :: [*]).
CanHardFork xs =>
Exactly xs Bound
-> Index xs x
-> WrapApplyTxErr x
-> WrapApplyTxErr (HardForkBlock xs)
inject Exactly xs Bound
_ =
      (ApplyTxErr (HardForkBlock xs) -> WrapApplyTxErr (HardForkBlock xs)
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 {k} (f :: k -> *) a b (x :: k) (xs :: [k]).
(Coercible a (f x), Coercible b (NS f xs)) =>
Proxy f -> Index xs x -> a -> b
injectNS' (forall {k} (t :: k). Proxy t
forall (t :: * -> *). Proxy t
Proxy @WrapApplyTxErr)

instance Inject (SomeSecond BlockQuery) where
  inject :: forall x (xs :: [*]).
CanHardFork xs =>
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) (Either (MismatchEraInfo xs) b)
-> SomeSecond BlockQuery (HardForkBlock xs)
forall {k1} {k2} (f :: k1 -> k2 -> *) (a :: k1) (b :: k2).
f a b -> SomeSecond f a
SomeSecond (QueryIfCurrent xs b
-> BlockQuery (HardForkBlock xs) (Either (MismatchEraInfo xs) b)
forall (xs :: [*]) result.
QueryIfCurrent xs result
-> BlockQuery
     (HardForkBlock xs) (Either (MismatchEraInfo 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 :: forall x (xs :: [*]).
CanHardFork xs =>
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 {k} (f :: k -> *) a b (x :: k) (xs :: [k]).
(Coercible a (f x), Coercible b (NS f xs)) =>
Proxy f -> Index xs x -> a -> b
injectNS' (forall {k} (t :: k). Proxy t
forall (t :: * -> *). Proxy t
Proxy @AnnTip)

instance Inject LedgerState where
  inject :: forall x (xs :: [*]).
CanHardFork xs =>
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 :: forall x (xs :: [*]).
CanHardFork xs =>
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)
forall a b. Coercible a b => a -> b
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 :: forall x (xs :: [*]).
CanHardFork xs =>
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)
headerStateTip :: WithOrigin (AnnTip x)
headerStateChainDep :: ChainDepState (BlockProtocol x)
headerStateTip :: forall blk. HeaderState blk -> WithOrigin (AnnTip blk)
headerStateChainDep :: forall blk. HeaderState blk -> ChainDepState (BlockProtocol blk)
..} = HeaderState {
        headerStateTip :: WithOrigin (AnnTip (HardForkBlock xs))
headerStateTip      = Exactly xs Bound
-> Index xs x -> AnnTip x -> AnnTip (HardForkBlock xs)
forall x (xs :: [*]).
CanHardFork xs =>
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 x (xs :: [*]).
CanHardFork xs =>
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 :: forall x (xs :: [*]).
CanHardFork xs =>
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
ledgerState :: LedgerState x
headerState :: HeaderState x
ledgerState :: forall blk. ExtLedgerState blk -> LedgerState blk
headerState :: forall blk. ExtLedgerState blk -> HeaderState blk
..} = ExtLedgerState {
        ledgerState :: LedgerState (HardForkBlock xs)
ledgerState = Exactly xs Bound
-> Index xs x -> LedgerState x -> LedgerState (HardForkBlock xs)
forall x (xs :: [*]).
CanHardFork xs =>
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 x (xs :: [*]).
CanHardFork xs =>
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 :: forall x (xs :: [*]).
CanHardFork (x : xs) =>
TopLevelConfig (HardForkBlock (x : xs))
-> ExtLedgerState x -> ExtLedgerState (HardForkBlock (x : xs))
injectInitialExtLedgerState TopLevelConfig (HardForkBlock (x : xs))
cfg ExtLedgerState x
extLedgerState0 =
    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 (xs :: [*]) (f :: * -> *).
SListIN NP xs =>
(forall a. f a) -> NP f 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