{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}

module Ouroboros.Consensus.HardFork.Combinator.Embed.Nary (
    Inject (..)
  , InjectionIndex (InjectionIndex)
  , inject'
    -- * Defaults
  , injectHardForkState
  , injectNestedCtxt_
  , injectQuery
    -- * Initial 'ExtLedgerState'
  , injectInitialExtLedgerState
    -- * Convenience
  , forgetInjectionIndex
  , oracularInjectionIndex
  ) where

import           Data.Bifunctor (first)
import           Data.Coerce (Coercible, coerce)
import           Data.SOP.BasicFunctors
import           Data.SOP.Constraint
import           Data.SOP.Counting (Exactly (..))
import           Data.SOP.Dict (Dict (..))
import           Data.SOP.Functors (Flip (..))
import           Data.SOP.Index
import qualified Data.SOP.InPairs as InPairs
import           Data.SOP.Strict
import qualified Data.SOP.Telescope as Telescope
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.Basics
import           Ouroboros.Consensus.Ledger.Extended (ExtLedgerState (..))
import           Ouroboros.Consensus.Ledger.Query
import           Ouroboros.Consensus.Ledger.Tables.Utils
import           Ouroboros.Consensus.Storage.Serialisation
import           Ouroboros.Consensus.TypeFamilyWrappers

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

class Inject f where
  inject ::
       forall x xs. (CanHardFork xs, HasCanonicalTxIn xs, HasHardForkTxOut xs)
    => InjectionIndex xs x
    -> f x
    -> f (HardForkBlock xs)

inject' ::
     forall f a b x xs.
     ( Inject f
     , CanHardFork xs
     , HasCanonicalTxIn xs
     , HasHardForkTxOut xs
     , Coercible a (f x)
     , Coercible b (f (HardForkBlock xs))
     )
  => Proxy f -> InjectionIndex xs x -> a -> b
inject' :: forall (f :: * -> *) a b x (xs :: [*]).
(Inject f, CanHardFork xs, HasCanonicalTxIn xs,
 HasHardForkTxOut xs, Coercible a (f x),
 Coercible b (f (HardForkBlock xs))) =>
Proxy f -> InjectionIndex xs x -> a -> b
inject' Proxy f
_ InjectionIndex xs x
iidx = 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, HasCanonicalTxIn xs,
 HasHardForkTxOut xs) =>
InjectionIndex xs x -> f x -> f (HardForkBlock xs)
inject @f InjectionIndex xs x
iidx (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

{-------------------------------------------------------------------------------
  InjectionIndex
-------------------------------------------------------------------------------}

-- | This data type is isomorphic to an 'Index' that additionally provides a
-- 'History.Bound' for every era up to and including that index, but none of
-- the subsequent eras.
newtype InjectionIndex xs x =
    InjectionIndex (Telescope (K History.Bound) (State.Current ((:~:) x)) xs)

-- | Many instances of 'Inject' do not need the 'History.Bound's, eg those that
-- do not construct 'HardForkState's
forgetInjectionIndex :: SListI xs => InjectionIndex xs x -> Index xs x
forgetInjectionIndex :: forall (xs :: [*]) x.
SListI xs =>
InjectionIndex xs x -> Index xs x
forgetInjectionIndex (InjectionIndex Telescope (K Bound) (Current ((:~:) x)) xs
tele) =
  NS ((:~:) x) xs -> Index xs x
forall {k} (xs :: [k]) (x :: k). NS ((:~:) x) xs -> Index xs x
Index (NS ((:~:) x) xs -> Index xs x) -> NS ((:~:) x) xs -> Index xs x
forall a b. (a -> b) -> a -> b
$ (forall a. Current ((:~:) x) a -> x :~: a)
-> NS (Current ((:~:) x)) xs -> NS ((:~:) 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 Current ((:~:) x) a -> x :~: a
forall a. Current ((:~:) x) a -> x :~: a
forall (f :: * -> *) blk. Current f blk -> f blk
State.currentState (NS (Current ((:~:) x)) xs -> NS ((:~:) x) xs)
-> NS (Current ((:~:) x)) xs -> NS ((:~:) x) xs
forall a b. (a -> b) -> a -> b
$ Telescope (K Bound) (Current ((:~:) x)) xs
-> NS (Current ((:~:) x)) xs
forall {k} (g :: k -> *) (f :: k -> *) (xs :: [k]).
Telescope g f xs -> NS f xs
Telescope.tip Telescope (K Bound) (Current ((:~:) x)) xs
tele

-- | Build an 'InjectionIndex' from oracular 'History.Bound's and an 'Index'
--
-- This bounds data is oracular, since the later eras in @xs@ might have not
-- yet started. However, it can be known in test code.
--
-- INVARIANT: the result is completely independent of the 'history.Bound's for
-- eras /after/ the given 'Index'.
oracularInjectionIndex ::
     SListI xs
  => Exactly xs History.Bound
  -> Index xs x
  -> InjectionIndex xs x
oracularInjectionIndex :: forall (xs :: [*]) x.
SListI xs =>
Exactly xs Bound -> Index xs x -> InjectionIndex xs x
oracularInjectionIndex (Exactly NP (K Bound) xs
np) (Index NS ((:~:) x) xs
idx) =
  Telescope (K Bound) (Current ((:~:) x)) xs -> InjectionIndex xs x
forall (xs :: [*]) x.
Telescope (K Bound) (Current ((:~:) x)) xs -> InjectionIndex xs x
InjectionIndex
    (Telescope (K Bound) (Current ((:~:) x)) xs -> InjectionIndex xs x)
-> Telescope (K Bound) (Current ((:~:) x)) xs
-> InjectionIndex xs x
forall a b. (a -> b) -> a -> b
$ (forall x. K Bound x -> K () x -> K Bound x)
-> (forall x. K Bound x -> (x :~: x) -> Current ((:~:) x) x)
-> NP (K Bound) xs
-> Telescope (K ()) ((:~:) x) xs
-> Telescope (K Bound) (Current ((:~:) x)) xs
forall {k} (xs :: [k]) (h :: k -> *) (g :: k -> *) (g' :: k -> *)
       (f :: k -> *) (f' :: k -> *).
SListI xs =>
(forall (x :: k). h x -> g x -> g' x)
-> (forall (x :: k). h x -> f x -> f' x)
-> NP h xs
-> Telescope g f xs
-> Telescope g' f' xs
Telescope.bihzipWith
      (\K Bound x
x (K ()) -> K Bound x
x)
      (\(K Bound
start) x :~: x
Refl -> State.Current { currentStart :: Bound
currentStart = Bound
start, currentState :: x :~: x
currentState = x :~: x
forall {k} (a :: k). a :~: a
Refl })
      NP (K Bound) xs
np
    (Telescope (K ()) ((:~:) x) xs
 -> Telescope (K Bound) (Current ((:~:) x)) xs)
-> Telescope (K ()) ((:~:) x) xs
-> Telescope (K Bound) (Current ((:~:) x)) xs
forall a b. (a -> b) -> a -> b
$ NS ((:~:) x) xs -> Telescope (K ()) ((:~:) x) xs
forall {k} (f :: k -> *) (xs :: [k]).
NS f xs -> Telescope (K ()) f xs
Telescope.fromTip NS ((:~:) x) xs
idx

-- | NOT EXPORTED
--
-- The first bound in a telescope. This is used in an inductive alternative
-- within 'injectHardForkState', since the end of one era is the start of the
-- next.
firstBound :: InjectionIndex xs x -> History.Bound
firstBound :: forall (xs :: [*]) x. InjectionIndex xs x -> Bound
firstBound (InjectionIndex Telescope (K Bound) (Current ((:~:) x)) xs
tele) = case Telescope (K Bound) (Current ((:~:) x)) xs
tele of
    TZ State.Current {currentStart :: forall (f :: * -> *) blk. Current f blk -> Bound
currentStart = Bound
start} -> Bound
start
    TS (K Bound
start) Telescope (K Bound) (Current ((:~:) x)) xs1
_tele'                     -> Bound
start

{-------------------------------------------------------------------------------
  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 xs' x
idx' -> NestedCtxt_ (HardForkBlock xs') f a
-> NestedCtxt_ (HardForkBlock (x' : xs')) f a
forall (xs1 :: [*]) (a :: * -> *) b x.
NestedCtxt_ (HardForkBlock xs1) a b
-> NestedCtxt_ (HardForkBlock (x : xs1)) a b
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 fp.
     Index xs x
  -> BlockQuery x fp      result
  -> QueryIfCurrent xs fp result
injectQuery :: forall x (xs :: [*]) result (fp :: QueryFootprint).
Index xs x -> BlockQuery x fp result -> QueryIfCurrent xs fp result
injectQuery Index xs x
idx BlockQuery x fp result
q = case Index xs x
idx of
    Index xs x
IZ      -> BlockQuery x fp result -> QueryIfCurrent (x : xs1) fp result
forall x (footprint :: QueryFootprint) result (xs1 :: [*]).
BlockQuery x footprint result
-> QueryIfCurrent (x : xs1) footprint result
QZ BlockQuery x fp result
q
    IS Index xs' x
idx' -> QueryIfCurrent xs' fp result -> QueryIfCurrent (x' : xs') fp result
forall (xs1 :: [*]) (footprint :: QueryFootprint) result x.
QueryIfCurrent xs1 footprint result
-> QueryIfCurrent (x : xs1) footprint result
QS (Index xs' x
-> BlockQuery x fp result -> QueryIfCurrent xs' fp result
forall x (xs :: [*]) result (fp :: QueryFootprint).
Index xs x -> BlockQuery x fp result -> QueryIfCurrent xs fp result
injectQuery Index xs' x
idx' BlockQuery x fp result
q)

injectHardForkState ::
     forall f x xs.
     InjectionIndex xs x
  -> f x
  -> HardForkState f xs
injectHardForkState :: forall (f :: * -> *) x (xs :: [*]).
InjectionIndex xs x -> f x -> HardForkState f xs
injectHardForkState InjectionIndex xs x
iidx 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
$ InjectionIndex xs x -> Telescope (K Past) (Current f) xs
forall (xs' :: [*]).
InjectionIndex xs' x -> Telescope (K Past) (Current f) xs'
go InjectionIndex xs x
iidx
  where
    go ::
         InjectionIndex xs' x
      -> Telescope (K State.Past) (State.Current f) xs'
    go :: forall (xs' :: [*]).
InjectionIndex xs' x -> Telescope (K Past) (Current f) xs'
go (InjectionIndex (TZ current :: Current ((:~:) x) x
current@State.Current { currentState :: forall (f :: * -> *) blk. Current f blk -> f blk
currentState = x :~: x
Refl })) =
        Current f x -> Telescope (K Past) (Current f) (x : xs1)
forall {k} (f :: k -> *) (x :: k) (g :: k -> *) (xs1 :: [k]).
f x -> Telescope g f (x : xs1)
TZ
          Current ((:~:) x) x
current { State.currentState = x }
    go (InjectionIndex (TS (K Bound
start) Telescope (K Bound) (Current ((:~:) x)) xs1
tele)) =
        K Past x
-> Telescope (K Past) (Current f) xs1
-> Telescope (K Past) (Current f) (x : xs1)
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   = InjectionIndex xs1 x -> Bound
forall (xs :: [*]) x. InjectionIndex xs x -> Bound
firstBound (Telescope (K Bound) (Current ((:~:) x)) xs1 -> InjectionIndex xs1 x
forall (xs :: [*]) x.
Telescope (K Bound) (Current ((:~:) x)) xs -> InjectionIndex xs x
InjectionIndex Telescope (K Bound) (Current ((:~:) x)) xs1
tele)
            }
          )
          (InjectionIndex xs1 x -> Telescope (K Past) (Current f) xs1
forall (xs' :: [*]).
InjectionIndex xs' x -> Telescope (K Past) (Current f) xs'
go (Telescope (K Bound) (Current ((:~:) x)) xs1 -> InjectionIndex xs1 x
forall (xs :: [*]) x.
Telescope (K Bound) (Current ((:~:) x)) xs -> InjectionIndex xs x
InjectionIndex Telescope (K Bound) (Current ((:~:) x)) xs1
tele))

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

instance Inject I where
  inject :: forall x (xs :: [*]).
(CanHardFork xs, HasCanonicalTxIn xs, HasHardForkTxOut xs) =>
InjectionIndex xs x -> I x -> I (HardForkBlock xs)
inject = Proxy I -> Index xs x -> I x -> I (HardForkBlock xs)
forall {k} (f :: k -> *) a b (x :: k) (xs :: [k]).
(All Top xs, 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) (Index xs x -> I x -> I (HardForkBlock xs))
-> (InjectionIndex xs x -> Index xs x)
-> InjectionIndex xs x
-> I x
-> I (HardForkBlock xs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InjectionIndex xs x -> Index xs x
forall (xs :: [*]) x.
SListI xs =>
InjectionIndex xs x -> Index xs x
forgetInjectionIndex

instance Inject (K a) where
  inject :: forall x (xs :: [*]).
(CanHardFork xs, HasCanonicalTxIn xs, HasHardForkTxOut xs) =>
InjectionIndex xs x -> K a x -> K a (HardForkBlock xs)
inject InjectionIndex xs x
_ (K a
a) = a -> K a (HardForkBlock xs)
forall k a (b :: k). a -> K a b
K a
a

instance Inject Header where
  inject :: forall x (xs :: [*]).
(CanHardFork xs, HasCanonicalTxIn xs, HasHardForkTxOut xs) =>
InjectionIndex xs x -> Header x -> Header (HardForkBlock xs)
inject = Proxy Header -> Index xs x -> Header x -> Header (HardForkBlock xs)
forall {k} (f :: k -> *) a b (x :: k) (xs :: [k]).
(All Top xs, 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) (Index xs x -> Header x -> Header (HardForkBlock xs))
-> (InjectionIndex xs x -> Index xs x)
-> InjectionIndex xs x
-> Header x
-> Header (HardForkBlock xs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InjectionIndex xs x -> Index xs x
forall (xs :: [*]) x.
SListI xs =>
InjectionIndex xs x -> Index xs x
forgetInjectionIndex

instance Inject SerialisedHeader where
  inject :: forall x (xs :: [*]).
(CanHardFork xs, HasCanonicalTxIn xs, HasHardForkTxOut xs) =>
InjectionIndex xs x
-> SerialisedHeader x -> SerialisedHeader (HardForkBlock xs)
inject InjectionIndex xs x
iidx =
        (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
    where
      idx :: Index xs x
idx = InjectionIndex xs x -> Index xs x
forall (xs :: [*]) x.
SListI xs =>
InjectionIndex xs x -> Index xs x
forgetInjectionIndex InjectionIndex xs x
iidx

instance Inject WrapHeaderHash where
  inject :: forall x (xs :: [*]).
(CanHardFork xs, HasCanonicalTxIn xs, HasHardForkTxOut xs) =>
InjectionIndex xs x
-> WrapHeaderHash x -> WrapHeaderHash (HardForkBlock xs)
inject (InjectionIndex xs x
iidx :: InjectionIndex 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
    where
      idx :: Index xs x
idx = InjectionIndex xs x -> Index xs x
forall (xs :: [*]) x.
SListI xs =>
InjectionIndex xs x -> Index xs x
forgetInjectionIndex InjectionIndex xs x
iidx

instance Inject GenTx where
  inject :: forall x (xs :: [*]).
(CanHardFork xs, HasCanonicalTxIn xs, HasHardForkTxOut xs) =>
InjectionIndex xs x -> GenTx x -> GenTx (HardForkBlock xs)
inject = Proxy GenTx -> Index xs x -> GenTx x -> GenTx (HardForkBlock xs)
forall {k} (f :: k -> *) a b (x :: k) (xs :: [k]).
(All Top xs, 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) (Index xs x -> GenTx x -> GenTx (HardForkBlock xs))
-> (InjectionIndex xs x -> Index xs x)
-> InjectionIndex xs x
-> GenTx x
-> GenTx (HardForkBlock xs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InjectionIndex xs x -> Index xs x
forall (xs :: [*]) x.
SListI xs =>
InjectionIndex xs x -> Index xs x
forgetInjectionIndex

instance Inject WrapGenTxId where
  inject :: forall x (xs :: [*]).
(CanHardFork xs, HasCanonicalTxIn xs, HasHardForkTxOut xs) =>
InjectionIndex xs x
-> WrapGenTxId x -> WrapGenTxId (HardForkBlock xs)
inject = Proxy WrapGenTxId
-> Index xs x -> WrapGenTxId x -> WrapGenTxId (HardForkBlock xs)
forall {k} (f :: k -> *) a b (x :: k) (xs :: [k]).
(All Top xs, 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) (Index xs x -> WrapGenTxId x -> WrapGenTxId (HardForkBlock xs))
-> (InjectionIndex xs x -> Index xs x)
-> InjectionIndex xs x
-> WrapGenTxId x
-> WrapGenTxId (HardForkBlock xs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InjectionIndex xs x -> Index xs x
forall (xs :: [*]) x.
SListI xs =>
InjectionIndex xs x -> Index xs x
forgetInjectionIndex

instance Inject WrapApplyTxErr where
  inject :: forall x (xs :: [*]).
(CanHardFork xs, HasCanonicalTxIn xs, HasHardForkTxOut xs) =>
InjectionIndex xs x
-> WrapApplyTxErr x -> WrapApplyTxErr (HardForkBlock xs)
inject =
      (   (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]).
(All Top xs, 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)
      )
    (Index xs x
 -> WrapApplyTxErr x -> WrapApplyTxErr (HardForkBlock xs))
-> (InjectionIndex xs x -> Index xs x)
-> InjectionIndex xs x
-> WrapApplyTxErr x
-> WrapApplyTxErr (HardForkBlock xs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InjectionIndex xs x -> Index xs x
forall (xs :: [*]) x.
SListI xs =>
InjectionIndex xs x -> Index xs x
forgetInjectionIndex

instance Inject (SomeBlockQuery :.: BlockQuery) where
  inject :: forall x (xs :: [*]).
(CanHardFork xs, HasCanonicalTxIn xs, HasHardForkTxOut xs) =>
InjectionIndex xs x
-> (:.:) SomeBlockQuery BlockQuery x
-> (:.:) SomeBlockQuery BlockQuery (HardForkBlock xs)
inject InjectionIndex xs x
iidx (Comp (SomeBlockQuery BlockQuery x footprint result
q)) =
      SomeBlockQuery (BlockQuery (HardForkBlock xs))
-> (:.:) SomeBlockQuery BlockQuery (HardForkBlock xs)
forall l k (f :: l -> *) (g :: k -> l) (p :: k).
f (g p) -> (:.:) f g p
Comp (SomeBlockQuery (BlockQuery (HardForkBlock xs))
 -> (:.:) SomeBlockQuery BlockQuery (HardForkBlock xs))
-> SomeBlockQuery (BlockQuery (HardForkBlock xs))
-> (:.:) SomeBlockQuery BlockQuery (HardForkBlock xs)
forall a b. (a -> b) -> a -> b
$ BlockQuery
  (HardForkBlock xs) footprint (Either (MismatchEraInfo xs) result)
-> SomeBlockQuery (BlockQuery (HardForkBlock xs))
forall (q :: QueryFootprint -> * -> *)
       (footprint :: QueryFootprint) result.
SingI footprint =>
q footprint result -> SomeBlockQuery q
SomeBlockQuery (QueryIfCurrent xs footprint result
-> BlockQuery
     (HardForkBlock xs) footprint (Either (MismatchEraInfo xs) result)
forall (xs :: [*]) (footprint :: QueryFootprint) result1.
QueryIfCurrent xs footprint result1
-> BlockQuery
     (HardForkBlock xs) footprint (Either (MismatchEraInfo xs) result1)
QueryIfCurrent (Index xs x
-> BlockQuery x footprint result
-> QueryIfCurrent xs footprint result
forall x (xs :: [*]) result (fp :: QueryFootprint).
Index xs x -> BlockQuery x fp result -> QueryIfCurrent xs fp result
injectQuery Index xs x
idx BlockQuery x footprint result
q))
    where
      idx :: Index xs x
idx = InjectionIndex xs x -> Index xs x
forall (xs :: [*]) x.
SListI xs =>
InjectionIndex xs x -> Index xs x
forgetInjectionIndex InjectionIndex xs x
iidx

instance Inject AnnTip where
  inject :: forall x (xs :: [*]).
(CanHardFork xs, HasCanonicalTxIn xs, HasHardForkTxOut xs) =>
InjectionIndex xs x -> AnnTip x -> AnnTip (HardForkBlock xs)
inject =
      (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]).
(All Top xs, 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)) (Index xs x -> AnnTip x -> AnnTip (HardForkBlock xs))
-> (InjectionIndex xs x -> Index xs x)
-> InjectionIndex xs x
-> AnnTip x
-> AnnTip (HardForkBlock xs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InjectionIndex xs x -> Index xs x
forall (xs :: [*]) x.
SListI xs =>
InjectionIndex xs x -> Index xs x
forgetInjectionIndex

instance Inject (Flip LedgerState mk) where
  inject :: forall x (xs :: [*]).
(CanHardFork xs, HasCanonicalTxIn xs, HasHardForkTxOut xs) =>
InjectionIndex xs x
-> Flip LedgerState mk x -> Flip LedgerState mk (HardForkBlock xs)
inject InjectionIndex xs x
iidx =
      LedgerState (HardForkBlock xs) mk
-> Flip LedgerState mk (HardForkBlock xs)
forall x y (f :: x -> y -> *) (x1 :: y) (y1 :: x).
f y1 x1 -> Flip f x1 y1
Flip (LedgerState (HardForkBlock xs) mk
 -> Flip LedgerState mk (HardForkBlock xs))
-> (Flip LedgerState mk x -> LedgerState (HardForkBlock xs) mk)
-> Flip LedgerState mk x
-> Flip LedgerState mk (HardForkBlock xs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HardForkState (Flip LedgerState mk) xs
-> LedgerState (HardForkBlock xs) mk
forall (xs :: [*]) (mk :: * -> * -> *).
HardForkState (Flip LedgerState mk) xs
-> LedgerState (HardForkBlock xs) mk
HardForkLedgerState (HardForkState (Flip LedgerState mk) xs
 -> LedgerState (HardForkBlock xs) mk)
-> (Flip LedgerState mk x
    -> HardForkState (Flip LedgerState mk) xs)
-> Flip LedgerState mk x
-> LedgerState (HardForkBlock xs) mk
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InjectionIndex xs x
-> Flip LedgerState mk x -> HardForkState (Flip LedgerState mk) xs
forall (f :: * -> *) x (xs :: [*]).
InjectionIndex xs x -> f x -> HardForkState f xs
injectHardForkState InjectionIndex xs x
iidx

instance Inject WrapChainDepState where
  inject :: forall x (xs :: [*]).
(CanHardFork xs, HasCanonicalTxIn xs, HasHardForkTxOut xs) =>
InjectionIndex xs x
-> WrapChainDepState x -> WrapChainDepState (HardForkBlock xs)
inject = HardForkState WrapChainDepState xs
-> WrapChainDepState (HardForkBlock xs)
forall a b. Coercible a b => a -> b
coerce (HardForkState WrapChainDepState xs
 -> WrapChainDepState (HardForkBlock xs))
-> (InjectionIndex xs x
    -> WrapChainDepState x -> HardForkState WrapChainDepState xs)
-> InjectionIndex xs x
-> WrapChainDepState x
-> WrapChainDepState (HardForkBlock xs)
forall y z x0 x1. (y -> z) -> (x0 -> x1 -> y) -> x0 -> x1 -> z
.: InjectionIndex xs x
-> WrapChainDepState x -> HardForkState WrapChainDepState xs
forall (f :: * -> *) x (xs :: [*]).
InjectionIndex xs x -> f x -> HardForkState f xs
injectHardForkState

instance Inject HeaderState where
  inject :: forall x (xs :: [*]).
(CanHardFork xs, HasCanonicalTxIn xs, HasHardForkTxOut xs) =>
InjectionIndex xs x
-> HeaderState x -> HeaderState (HardForkBlock xs)
inject InjectionIndex xs x
iidx HeaderState {WithOrigin (AnnTip x)
ChainDepState (BlockProtocol x)
headerStateTip :: WithOrigin (AnnTip x)
headerStateChainDep :: ChainDepState (BlockProtocol x)
headerStateChainDep :: forall blk. HeaderState blk -> ChainDepState (BlockProtocol blk)
headerStateTip :: forall blk. HeaderState blk -> WithOrigin (AnnTip blk)
..} = HeaderState {
        headerStateTip :: WithOrigin (AnnTip (HardForkBlock xs))
headerStateTip      = InjectionIndex xs x -> AnnTip x -> AnnTip (HardForkBlock xs)
forall x (xs :: [*]).
(CanHardFork xs, HasCanonicalTxIn xs, HasHardForkTxOut xs) =>
InjectionIndex xs x -> AnnTip x -> AnnTip (HardForkBlock xs)
forall (f :: * -> *) x (xs :: [*]).
(Inject f, CanHardFork xs, HasCanonicalTxIn xs,
 HasHardForkTxOut xs) =>
InjectionIndex xs x -> f x -> f (HardForkBlock xs)
inject InjectionIndex xs x
iidx (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
$ InjectionIndex xs x
-> WrapChainDepState x -> WrapChainDepState (HardForkBlock xs)
forall x (xs :: [*]).
(CanHardFork xs, HasCanonicalTxIn xs, HasHardForkTxOut xs) =>
InjectionIndex xs x
-> WrapChainDepState x -> WrapChainDepState (HardForkBlock xs)
forall (f :: * -> *) x (xs :: [*]).
(Inject f, CanHardFork xs, HasCanonicalTxIn xs,
 HasHardForkTxOut xs) =>
InjectionIndex xs x -> f x -> f (HardForkBlock xs)
inject InjectionIndex xs x
iidx
                            (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 (Flip ExtLedgerState mk) where
  inject :: forall x (xs :: [*]).
(CanHardFork xs, HasCanonicalTxIn xs, HasHardForkTxOut xs) =>
InjectionIndex xs x
-> Flip ExtLedgerState mk x
-> Flip ExtLedgerState mk (HardForkBlock xs)
inject InjectionIndex xs x
iidx (Flip ExtLedgerState {LedgerState x mk
HeaderState x
ledgerState :: LedgerState x mk
headerState :: HeaderState x
headerState :: forall blk (mk :: * -> * -> *).
ExtLedgerState blk mk -> HeaderState blk
ledgerState :: forall blk (mk :: * -> * -> *).
ExtLedgerState blk mk -> LedgerState blk mk
..}) = ExtLedgerState (HardForkBlock xs) mk
-> Flip ExtLedgerState mk (HardForkBlock xs)
forall x y (f :: x -> y -> *) (x1 :: y) (y1 :: x).
f y1 x1 -> Flip f x1 y1
Flip (ExtLedgerState (HardForkBlock xs) mk
 -> Flip ExtLedgerState mk (HardForkBlock xs))
-> ExtLedgerState (HardForkBlock xs) mk
-> Flip ExtLedgerState mk (HardForkBlock xs)
forall a b. (a -> b) -> a -> b
$ ExtLedgerState {
        ledgerState :: LedgerState (HardForkBlock xs) mk
ledgerState = Flip LedgerState mk (HardForkBlock xs)
-> LedgerState (HardForkBlock xs) mk
forall x1 y1 (f :: x1 -> y1 -> *) (x2 :: y1) (y2 :: x1).
Flip f x2 y2 -> f y2 x2
unFlip (Flip LedgerState mk (HardForkBlock xs)
 -> LedgerState (HardForkBlock xs) mk)
-> Flip LedgerState mk (HardForkBlock xs)
-> LedgerState (HardForkBlock xs) mk
forall a b. (a -> b) -> a -> b
$ InjectionIndex xs x
-> Flip LedgerState mk x -> Flip LedgerState mk (HardForkBlock xs)
forall x (xs :: [*]).
(CanHardFork xs, HasCanonicalTxIn xs, HasHardForkTxOut xs) =>
InjectionIndex xs x
-> Flip LedgerState mk x -> Flip LedgerState mk (HardForkBlock xs)
forall (f :: * -> *) x (xs :: [*]).
(Inject f, CanHardFork xs, HasCanonicalTxIn xs,
 HasHardForkTxOut xs) =>
InjectionIndex xs x -> f x -> f (HardForkBlock xs)
inject InjectionIndex xs x
iidx (LedgerState x mk -> Flip LedgerState mk x
forall x y (f :: x -> y -> *) (x1 :: y) (y1 :: x).
f y1 x1 -> Flip f x1 y1
Flip LedgerState x mk
ledgerState)
      , headerState :: HeaderState (HardForkBlock xs)
headerState = InjectionIndex xs x
-> HeaderState x -> HeaderState (HardForkBlock xs)
forall x (xs :: [*]).
(CanHardFork xs, HasCanonicalTxIn xs, HasHardForkTxOut xs) =>
InjectionIndex xs x
-> HeaderState x -> HeaderState (HardForkBlock xs)
forall (f :: * -> *) x (xs :: [*]).
(Inject f, CanHardFork xs, HasCanonicalTxIn xs,
 HasHardForkTxOut xs) =>
InjectionIndex xs x -> f x -> f (HardForkBlock xs)
inject InjectionIndex xs x
iidx 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@.
--
-- Note: this function is an /alternative/ to the 'Inject' class above. It does
-- not rely on that class.
injectInitialExtLedgerState ::
     forall x xs. (CanHardFork (x ': xs), HasLedgerTables (LedgerState (HardForkBlock (x : xs))))
  => TopLevelConfig (HardForkBlock (x ': xs))
  -> ExtLedgerState x ValuesMK
  -> ExtLedgerState (HardForkBlock (x ': xs)) ValuesMK
injectInitialExtLedgerState :: forall x (xs :: [*]).
(CanHardFork (x : xs),
 HasLedgerTables (LedgerState (HardForkBlock (x : xs)))) =>
TopLevelConfig (HardForkBlock (x : xs))
-> ExtLedgerState x ValuesMK
-> ExtLedgerState (HardForkBlock (x : xs)) ValuesMK
injectInitialExtLedgerState TopLevelConfig (HardForkBlock (x : xs))
cfg ExtLedgerState x ValuesMK
extLedgerState0 =
    ExtLedgerState {
        ledgerState :: LedgerState (HardForkBlock (x : xs)) ValuesMK
ledgerState = LedgerState (HardForkBlock (x : xs)) ValuesMK
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 (Flip LedgerState ValuesMK) (x : xs)
-> EpochInfo (Except PastHorizonException)
forall (xs :: [*]) (mk :: * -> * -> *).
All SingleEraBlock xs =>
HardForkLedgerConfig xs
-> HardForkState (Flip LedgerState mk) 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)) ValuesMK
-> HardForkState (Flip LedgerState ValuesMK) (x : xs)
forall (xs :: [*]) (mk :: * -> * -> *).
LedgerState (HardForkBlock xs) mk
-> HardForkState (Flip LedgerState mk) xs
hardForkLedgerStatePerEra LedgerState (HardForkBlock (x : xs)) ValuesMK
targetEraLedgerState))
          TopLevelConfig (HardForkBlock (x : xs))
cfg

    targetEraLedgerState :: LedgerState (HardForkBlock (x ': xs)) ValuesMK
    targetEraLedgerState :: LedgerState (HardForkBlock (x : xs)) ValuesMK
targetEraLedgerState = LedgerState (HardForkBlock (x : xs)) ValuesMK
-> LedgerState (HardForkBlock (x : xs)) DiffMK
-> LedgerState (HardForkBlock (x : xs)) ValuesMK
forall (l :: LedgerStateKind) (l' :: LedgerStateKind).
(SameUtxoTypes l l', HasLedgerTables l, HasLedgerTables l') =>
l ValuesMK -> l' DiffMK -> l' ValuesMK
applyDiffs LedgerState (HardForkBlock (x : xs)) ValuesMK
st LedgerState (HardForkBlock (x : xs)) DiffMK
st'
      where
        st :: LedgerState (HardForkBlock (x ': xs)) ValuesMK
        st :: LedgerState (HardForkBlock (x : xs)) ValuesMK
st = HardForkState (Flip LedgerState ValuesMK) (x : xs)
-> LedgerState (HardForkBlock (x : xs)) ValuesMK
forall (xs :: [*]) (mk :: * -> * -> *).
HardForkState (Flip LedgerState mk) xs
-> LedgerState (HardForkBlock xs) mk
HardForkLedgerState (HardForkState (Flip LedgerState ValuesMK) (x : xs)
 -> LedgerState (HardForkBlock (x : xs)) ValuesMK)
-> (ExtLedgerState x ValuesMK
    -> HardForkState (Flip LedgerState ValuesMK) (x : xs))
-> ExtLedgerState x ValuesMK
-> LedgerState (HardForkBlock (x : xs)) ValuesMK
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Flip LedgerState ValuesMK x
-> HardForkState (Flip LedgerState ValuesMK) (x : xs)
forall (f :: * -> *) x (xs :: [*]). f x -> HardForkState f (x : xs)
initHardForkState (Flip LedgerState ValuesMK x
 -> HardForkState (Flip LedgerState ValuesMK) (x : xs))
-> (ExtLedgerState x ValuesMK -> Flip LedgerState ValuesMK x)
-> ExtLedgerState x ValuesMK
-> HardForkState (Flip LedgerState ValuesMK) (x : xs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LedgerState x ValuesMK -> Flip LedgerState ValuesMK x
forall x y (f :: x -> y -> *) (x1 :: y) (y1 :: x).
f y1 x1 -> Flip f x1 y1
Flip (LedgerState x ValuesMK -> Flip LedgerState ValuesMK x)
-> (ExtLedgerState x ValuesMK -> LedgerState x ValuesMK)
-> ExtLedgerState x ValuesMK
-> Flip LedgerState ValuesMK x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExtLedgerState x ValuesMK -> LedgerState x ValuesMK
forall blk (mk :: * -> * -> *).
ExtLedgerState blk mk -> LedgerState blk mk
ledgerState (ExtLedgerState x ValuesMK
 -> LedgerState (HardForkBlock (x : xs)) ValuesMK)
-> ExtLedgerState x ValuesMK
-> LedgerState (HardForkBlock (x : xs)) ValuesMK
forall a b. (a -> b) -> a -> b
$ ExtLedgerState x ValuesMK
extLedgerState0
        st' :: LedgerState (HardForkBlock (x : xs)) DiffMK
st' = HardForkState (Flip LedgerState DiffMK) (x : xs)
-> LedgerState (HardForkBlock (x : xs)) DiffMK
forall (xs :: [*]) (mk :: * -> * -> *).
HardForkState (Flip LedgerState mk) xs
-> LedgerState (HardForkBlock xs) mk
HardForkLedgerState
                -- We can immediately extend it to the right slot, executing any
                -- scheduled hard forks in the first slot
                  (HardForkLedgerConfig (x : xs)
-> SlotNo
-> HardForkState (Flip LedgerState EmptyMK) (x : xs)
-> HardForkState (Flip LedgerState DiffMK) (x : xs)
forall (xs :: [*]).
CanHardFork xs =>
HardForkLedgerConfig xs
-> SlotNo
-> HardForkState (Flip LedgerState EmptyMK) xs
-> HardForkState (Flip LedgerState DiffMK) 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)
                      (Flip LedgerState EmptyMK x
-> HardForkState (Flip LedgerState EmptyMK) (x : xs)
forall (f :: * -> *) x (xs :: [*]). f x -> HardForkState f (x : xs)
initHardForkState (Flip LedgerState EmptyMK x
 -> HardForkState (Flip LedgerState EmptyMK) (x : xs))
-> Flip LedgerState EmptyMK x
-> HardForkState (Flip LedgerState EmptyMK) (x : xs)
forall a b. (a -> b) -> a -> b
$ LedgerState x EmptyMK -> Flip LedgerState EmptyMK x
forall x y (f :: x -> y -> *) (x1 :: y) (y1 :: x).
f y1 x1 -> Flip f x1 y1
Flip (LedgerState x EmptyMK -> Flip LedgerState EmptyMK x)
-> LedgerState x EmptyMK -> Flip LedgerState EmptyMK x
forall a b. (a -> b) -> a -> b
$ LedgerState x ValuesMK -> LedgerState x EmptyMK
forall (l :: LedgerStateKind) (mk :: * -> * -> *).
HasLedgerTables l =>
l mk -> l EmptyMK
forgetLedgerTables (LedgerState x ValuesMK -> LedgerState x EmptyMK)
-> LedgerState x ValuesMK -> LedgerState x EmptyMK
forall a b. (a -> b) -> a -> b
$ ExtLedgerState x ValuesMK -> LedgerState x ValuesMK
forall blk (mk :: * -> * -> *).
ExtLedgerState blk mk -> LedgerState blk mk
ledgerState ExtLedgerState x ValuesMK
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 ValuesMK -> HeaderState x
forall blk (mk :: * -> * -> *).
ExtLedgerState blk mk -> HeaderState blk
headerState ExtLedgerState x ValuesMK
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
     (Flip LedgerState ValuesMK
      -.-> (WrapChainDepState -.-> WrapChainDepState))
     (x : xs)
-> HardForkState (Flip LedgerState ValuesMK) (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.
 (-.->)
   (Flip LedgerState ValuesMK)
   (WrapChainDepState -.-> WrapChainDepState)
   a)
-> NP
     (Flip LedgerState ValuesMK
      -.-> (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 ((Flip LedgerState ValuesMK a
 -> WrapChainDepState a -> WrapChainDepState a)
-> (-.->)
     (Flip LedgerState ValuesMK)
     (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 (\Flip LedgerState ValuesMK a
_ WrapChainDepState a
st -> WrapChainDepState a
st)))
          (LedgerState (HardForkBlock (x : xs)) ValuesMK
-> HardForkState (Flip LedgerState ValuesMK) (x : xs)
forall (xs :: [*]) (mk :: * -> * -> *).
LedgerState (HardForkBlock xs) mk
-> HardForkState (Flip LedgerState mk) xs
hardForkLedgerStatePerEra LedgerState (HardForkBlock (x : xs)) ValuesMK
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