{-# 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.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.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
    => InjectionIndex 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 -> InjectionIndex 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 -> 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) =>
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.
     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 xs' x
idx' -> QueryIfCurrent xs' result -> QueryIfCurrent (x' : xs') result
forall (xs :: [*]) b x.
QueryIfCurrent xs b -> QueryIfCurrent (x : xs) b
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.
     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 =>
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 =>
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 =>
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 =>
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 =>
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 =>
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 =>
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 =>
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 (SomeSecond BlockQuery) where
  inject :: forall x (xs :: [*]).
CanHardFork xs =>
InjectionIndex xs x
-> SomeSecond BlockQuery x
-> SomeSecond BlockQuery (HardForkBlock xs)
inject InjectionIndex xs x
iidx (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))
    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 =>
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 LedgerState where
  inject :: forall x (xs :: [*]).
CanHardFork xs =>
InjectionIndex xs x
-> LedgerState x -> LedgerState (HardForkBlock xs)
inject = HardForkState LedgerState xs -> LedgerState (HardForkBlock xs)
forall (xs :: [*]).
HardForkState LedgerState xs -> LedgerState (HardForkBlock xs)
HardForkLedgerState (HardForkState LedgerState xs -> LedgerState (HardForkBlock xs))
-> (InjectionIndex xs x
    -> LedgerState x -> HardForkState LedgerState xs)
-> InjectionIndex xs x
-> LedgerState x
-> LedgerState (HardForkBlock xs)
forall y z x0 x1. (y -> z) -> (x0 -> x1 -> y) -> x0 -> x1 -> z
.: InjectionIndex xs x
-> LedgerState x -> HardForkState LedgerState xs
forall (f :: * -> *) x (xs :: [*]).
InjectionIndex xs x -> f x -> HardForkState f xs
injectHardForkState

instance Inject WrapChainDepState where
  inject :: forall x (xs :: [*]).
CanHardFork 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 =>
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)
headerStateTip :: forall blk. HeaderState blk -> WithOrigin (AnnTip blk)
headerStateChainDep :: forall blk. HeaderState blk -> ChainDepState (BlockProtocol blk)
..} = HeaderState {
        headerStateTip :: WithOrigin (AnnTip (HardForkBlock xs))
headerStateTip      = InjectionIndex xs x -> AnnTip x -> AnnTip (HardForkBlock xs)
forall x (xs :: [*]).
CanHardFork xs =>
InjectionIndex xs x -> AnnTip x -> AnnTip (HardForkBlock xs)
forall (f :: * -> *) x (xs :: [*]).
(Inject f, CanHardFork 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 =>
InjectionIndex xs x
-> WrapChainDepState x -> WrapChainDepState (HardForkBlock xs)
forall (f :: * -> *) x (xs :: [*]).
(Inject f, CanHardFork 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 ExtLedgerState where
  inject :: forall x (xs :: [*]).
CanHardFork xs =>
InjectionIndex xs x
-> ExtLedgerState x -> ExtLedgerState (HardForkBlock xs)
inject InjectionIndex xs x
iidx 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 = InjectionIndex xs x
-> LedgerState x -> LedgerState (HardForkBlock xs)
forall x (xs :: [*]).
CanHardFork xs =>
InjectionIndex xs x
-> LedgerState x -> LedgerState (HardForkBlock xs)
forall (f :: * -> *) x (xs :: [*]).
(Inject f, CanHardFork xs) =>
InjectionIndex xs x -> f x -> f (HardForkBlock xs)
inject InjectionIndex xs x
iidx LedgerState x
ledgerState
      , headerState :: HeaderState (HardForkBlock xs)
headerState = InjectionIndex xs x
-> HeaderState x -> HeaderState (HardForkBlock xs)
forall x (xs :: [*]).
CanHardFork xs =>
InjectionIndex xs x
-> HeaderState x -> HeaderState (HardForkBlock xs)
forall (f :: * -> *) x (xs :: [*]).
(Inject f, CanHardFork 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)
  => 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