{-# LANGUAGE DataKinds                  #-}
{-# LANGUAGE FlexibleContexts           #-}
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE GADTs                      #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses      #-}
{-# LANGUAGE RankNTypes                 #-}
{-# LANGUAGE RecordWildCards            #-}
{-# LANGUAGE ScopedTypeVariables        #-}
{-# LANGUAGE StandaloneDeriving         #-}
{-# LANGUAGE TypeApplications           #-}
{-# LANGUAGE TypeFamilies               #-}
{-# LANGUAGE TypeOperators              #-}
{-# LANGUAGE UndecidableInstances       #-}

{-# OPTIONS_GHC -Wno-orphans #-}

module Ouroboros.Consensus.HardFork.Combinator.Block (
    -- * Type family instances
    Header (..)
  , NestedCtxt_ (..)
    -- * AnnTip
  , distribAnnTip
  , undistribAnnTip
  ) where

import           Data.Function (on)
import           Data.Functor.Product
import           Data.Kind (Type)
import           Data.SOP.Strict
import           Data.Typeable (Typeable)
import           Data.Word
import           NoThunks.Class (NoThunks)

import           Ouroboros.Consensus.Block
import           Ouroboros.Consensus.HeaderValidation
import           Ouroboros.Consensus.TypeFamilyWrappers
import           Ouroboros.Consensus.Util (ShowProxy, (.:))
import           Ouroboros.Consensus.Util.SOP

import           Ouroboros.Consensus.HardFork.Combinator.Abstract
import           Ouroboros.Consensus.HardFork.Combinator.AcrossEras
import           Ouroboros.Consensus.HardFork.Combinator.Basics
import qualified Ouroboros.Consensus.HardFork.Combinator.Util.Match as Match

{-------------------------------------------------------------------------------
  GetHeader
-------------------------------------------------------------------------------}

newtype instance Header (HardForkBlock xs) = HardForkHeader {
      Header (HardForkBlock xs) -> OneEraHeader xs
getHardForkHeader :: OneEraHeader xs
    }
  deriving (Int -> Header (HardForkBlock xs) -> ShowS
[Header (HardForkBlock xs)] -> ShowS
Header (HardForkBlock xs) -> String
(Int -> Header (HardForkBlock xs) -> ShowS)
-> (Header (HardForkBlock xs) -> String)
-> ([Header (HardForkBlock xs)] -> ShowS)
-> Show (Header (HardForkBlock xs))
forall (xs :: [*]).
CanHardFork xs =>
Int -> Header (HardForkBlock xs) -> ShowS
forall (xs :: [*]).
CanHardFork xs =>
[Header (HardForkBlock xs)] -> ShowS
forall (xs :: [*]).
CanHardFork xs =>
Header (HardForkBlock xs) -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Header (HardForkBlock xs)] -> ShowS
$cshowList :: forall (xs :: [*]).
CanHardFork xs =>
[Header (HardForkBlock xs)] -> ShowS
show :: Header (HardForkBlock xs) -> String
$cshow :: forall (xs :: [*]).
CanHardFork xs =>
Header (HardForkBlock xs) -> String
showsPrec :: Int -> Header (HardForkBlock xs) -> ShowS
$cshowsPrec :: forall (xs :: [*]).
CanHardFork xs =>
Int -> Header (HardForkBlock xs) -> ShowS
Show, Context -> Header (HardForkBlock xs) -> IO (Maybe ThunkInfo)
Proxy (Header (HardForkBlock xs)) -> String
(Context -> Header (HardForkBlock xs) -> IO (Maybe ThunkInfo))
-> (Context -> Header (HardForkBlock xs) -> IO (Maybe ThunkInfo))
-> (Proxy (Header (HardForkBlock xs)) -> String)
-> NoThunks (Header (HardForkBlock xs))
forall (xs :: [*]).
CanHardFork xs =>
Context -> Header (HardForkBlock xs) -> IO (Maybe ThunkInfo)
forall (xs :: [*]).
CanHardFork xs =>
Proxy (Header (HardForkBlock xs)) -> String
forall a.
(Context -> a -> IO (Maybe ThunkInfo))
-> (Context -> a -> IO (Maybe ThunkInfo))
-> (Proxy a -> String)
-> NoThunks a
showTypeOf :: Proxy (Header (HardForkBlock xs)) -> String
$cshowTypeOf :: forall (xs :: [*]).
CanHardFork xs =>
Proxy (Header (HardForkBlock xs)) -> String
wNoThunks :: Context -> Header (HardForkBlock xs) -> IO (Maybe ThunkInfo)
$cwNoThunks :: forall (xs :: [*]).
CanHardFork xs =>
Context -> Header (HardForkBlock xs) -> IO (Maybe ThunkInfo)
noThunks :: Context -> Header (HardForkBlock xs) -> IO (Maybe ThunkInfo)
$cnoThunks :: forall (xs :: [*]).
CanHardFork xs =>
Context -> Header (HardForkBlock xs) -> IO (Maybe ThunkInfo)
NoThunks)

instance Typeable xs => ShowProxy (Header (HardForkBlock xs)) where

instance CanHardFork xs => GetHeader (HardForkBlock xs) where
  getHeader :: HardForkBlock xs -> Header (HardForkBlock xs)
getHeader = OneEraHeader xs -> Header (HardForkBlock xs)
forall (xs :: [*]). OneEraHeader xs -> Header (HardForkBlock xs)
HardForkHeader (OneEraHeader xs -> Header (HardForkBlock xs))
-> (HardForkBlock xs -> OneEraHeader xs)
-> HardForkBlock xs
-> Header (HardForkBlock xs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OneEraBlock xs -> OneEraHeader xs
forall (xs :: [*]).
CanHardFork xs =>
OneEraBlock xs -> OneEraHeader xs
oneEraBlockHeader (OneEraBlock xs -> OneEraHeader xs)
-> (HardForkBlock xs -> OneEraBlock xs)
-> HardForkBlock xs
-> OneEraHeader xs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HardForkBlock xs -> OneEraBlock xs
forall (xs :: [*]). HardForkBlock xs -> OneEraBlock xs
getHardForkBlock

  blockMatchesHeader :: Header (HardForkBlock xs) -> HardForkBlock xs -> Bool
blockMatchesHeader = \Header (HardForkBlock xs)
hdr HardForkBlock xs
blk ->
      case NS Header xs
-> NS I xs
-> Either (Mismatch Header I xs) (NS (Product Header I) xs)
forall k (f :: k -> *) (xs :: [k]) (g :: k -> *).
NS f xs
-> NS g xs -> Either (Mismatch f g xs) (NS (Product f g) xs)
Match.matchNS
             (OneEraHeader xs -> NS Header xs
forall (xs :: [*]). OneEraHeader xs -> NS Header xs
getOneEraHeader (Header (HardForkBlock xs) -> OneEraHeader xs
forall (xs :: [*]). Header (HardForkBlock xs) -> OneEraHeader xs
getHardForkHeader Header (HardForkBlock xs)
hdr))
             (OneEraBlock xs -> NS I xs
forall (xs :: [*]). OneEraBlock xs -> NS I xs
getOneEraBlock  (HardForkBlock xs -> OneEraBlock xs
forall (xs :: [*]). HardForkBlock xs -> OneEraBlock xs
getHardForkBlock  HardForkBlock xs
blk)) of
        Left Mismatch Header I xs
_          -> Bool
False
        Right NS (Product Header I) xs
hdrAndBlk ->
          NS (K Bool) xs -> CollapseTo NS Bool
forall k l (h :: (k -> *) -> l -> *) (xs :: l) a.
(HCollapse h, SListIN h xs) =>
h (K a) xs -> CollapseTo h a
hcollapse (NS (K Bool) xs -> CollapseTo NS Bool)
-> NS (K Bool) xs -> CollapseTo NS Bool
forall a b. (a -> b) -> a -> b
$ Proxy SingleEraBlock
-> (forall a. SingleEraBlock a => Product Header I a -> K Bool a)
-> NS (Product Header I) xs
-> NS (K Bool) xs
forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *)
       (f' :: k -> *).
(AllN (Prod h) c xs, HAp h) =>
proxy c
-> (forall (a :: k). c a => f a -> f' a) -> h f xs -> h f' xs
hcliftA Proxy SingleEraBlock
proxySingle forall blk. GetHeader blk => Product Header I blk -> K Bool blk
forall a. SingleEraBlock a => Product Header I a -> K Bool a
matchesSingle NS (Product Header I) xs
hdrAndBlk
    where
      matchesSingle :: GetHeader blk => Product Header I blk -> K Bool blk
      matchesSingle :: Product Header I blk -> K Bool blk
matchesSingle (Pair Header blk
hdr (I blk
blk)) = Bool -> K Bool blk
forall k a (b :: k). a -> K a b
K (Header blk -> blk -> Bool
forall blk. GetHeader blk => Header blk -> blk -> Bool
blockMatchesHeader Header blk
hdr blk
blk)

  headerIsEBB :: Header (HardForkBlock xs) -> Maybe EpochNo
headerIsEBB =
        NS (K (Maybe EpochNo)) xs -> Maybe EpochNo
forall k l (h :: (k -> *) -> l -> *) (xs :: l) a.
(HCollapse h, SListIN h xs) =>
h (K a) xs -> CollapseTo h a
hcollapse
      (NS (K (Maybe EpochNo)) xs -> Maybe EpochNo)
-> (Header (HardForkBlock xs) -> NS (K (Maybe EpochNo)) xs)
-> Header (HardForkBlock xs)
-> Maybe EpochNo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy SingleEraBlock
-> (forall a. SingleEraBlock a => Header a -> K (Maybe EpochNo) a)
-> NS Header xs
-> NS (K (Maybe EpochNo)) xs
forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *)
       (f' :: k -> *).
(AllN (Prod h) c xs, HAp h) =>
proxy c
-> (forall (a :: k). c a => f a -> f' a) -> h f xs -> h f' xs
hcmap Proxy SingleEraBlock
proxySingle (Maybe EpochNo -> K (Maybe EpochNo) a
forall k a (b :: k). a -> K a b
K (Maybe EpochNo -> K (Maybe EpochNo) a)
-> (Header a -> Maybe EpochNo) -> Header a -> K (Maybe EpochNo) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Header a -> Maybe EpochNo
forall blk. GetHeader blk => Header blk -> Maybe EpochNo
headerIsEBB)
      (NS Header xs -> NS (K (Maybe EpochNo)) xs)
-> (Header (HardForkBlock xs) -> NS Header xs)
-> Header (HardForkBlock xs)
-> NS (K (Maybe EpochNo)) xs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OneEraHeader xs -> NS Header xs
forall (xs :: [*]). OneEraHeader xs -> NS Header xs
getOneEraHeader
      (OneEraHeader xs -> NS Header xs)
-> (Header (HardForkBlock xs) -> OneEraHeader xs)
-> Header (HardForkBlock xs)
-> NS Header xs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Header (HardForkBlock xs) -> OneEraHeader xs
forall (xs :: [*]). Header (HardForkBlock xs) -> OneEraHeader xs
getHardForkHeader

{-------------------------------------------------------------------------------
  HasHeader
-------------------------------------------------------------------------------}

instance CanHardFork xs => StandardHash (HardForkBlock xs)

instance CanHardFork xs => HasHeader (HardForkBlock xs) where
  getHeaderFields :: HardForkBlock xs -> HeaderFields (HardForkBlock xs)
getHeaderFields = HardForkBlock xs -> HeaderFields (HardForkBlock xs)
forall blk. GetHeader blk => blk -> HeaderFields blk
getBlockHeaderFields

instance CanHardFork xs => HasHeader (Header (HardForkBlock xs)) where
  getHeaderFields :: Header (HardForkBlock xs)
-> HeaderFields (Header (HardForkBlock xs))
getHeaderFields =
        NS (K (HeaderFields (Header (HardForkBlock xs)))) xs
-> HeaderFields (Header (HardForkBlock xs))
forall k l (h :: (k -> *) -> l -> *) (xs :: l) a.
(HCollapse h, SListIN h xs) =>
h (K a) xs -> CollapseTo h a
hcollapse
      (NS (K (HeaderFields (Header (HardForkBlock xs)))) xs
 -> HeaderFields (Header (HardForkBlock xs)))
-> (Header (HardForkBlock xs)
    -> NS (K (HeaderFields (Header (HardForkBlock xs)))) xs)
-> Header (HardForkBlock xs)
-> HeaderFields (Header (HardForkBlock xs))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy SingleEraBlock
-> (forall a.
    SingleEraBlock a =>
    Header a -> K (HeaderFields (Header (HardForkBlock xs))) a)
-> NS Header xs
-> NS (K (HeaderFields (Header (HardForkBlock xs)))) xs
forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *)
       (f' :: k -> *).
(AllN (Prod h) c xs, HAp h) =>
proxy c
-> (forall (a :: k). c a => f a -> f' a) -> h f xs -> h f' xs
hcmap Proxy SingleEraBlock
proxySingle (HeaderFields (Header (HardForkBlock xs))
-> K (HeaderFields (Header (HardForkBlock xs))) a
forall k a (b :: k). a -> K a b
K (HeaderFields (Header (HardForkBlock xs))
 -> K (HeaderFields (Header (HardForkBlock xs))) a)
-> (Header a -> HeaderFields (Header (HardForkBlock xs)))
-> Header a
-> K (HeaderFields (Header (HardForkBlock xs))) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Header a -> HeaderFields (Header (HardForkBlock xs))
forall blk.
SingleEraBlock blk =>
Header blk -> HeaderFields (Header (HardForkBlock xs))
getOne)
      (NS Header xs
 -> NS (K (HeaderFields (Header (HardForkBlock xs)))) xs)
-> (Header (HardForkBlock xs) -> NS Header xs)
-> Header (HardForkBlock xs)
-> NS (K (HeaderFields (Header (HardForkBlock xs)))) xs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OneEraHeader xs -> NS Header xs
forall (xs :: [*]). OneEraHeader xs -> NS Header xs
getOneEraHeader
      (OneEraHeader xs -> NS Header xs)
-> (Header (HardForkBlock xs) -> OneEraHeader xs)
-> Header (HardForkBlock xs)
-> NS Header xs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Header (HardForkBlock xs) -> OneEraHeader xs
forall (xs :: [*]). Header (HardForkBlock xs) -> OneEraHeader xs
getHardForkHeader
    where
      getOne :: forall blk. SingleEraBlock blk
             => Header blk -> HeaderFields (Header (HardForkBlock xs))
      getOne :: Header blk -> HeaderFields (Header (HardForkBlock xs))
getOne Header blk
hdr = HeaderFields :: forall b. SlotNo -> BlockNo -> HeaderHash b -> HeaderFields b
HeaderFields {
            headerFieldHash :: HeaderHash (Header (HardForkBlock xs))
headerFieldHash    = ShortByteString -> OneEraHash xs
forall k (xs :: [k]). ShortByteString -> OneEraHash xs
OneEraHash (ShortByteString -> OneEraHash xs)
-> ShortByteString -> OneEraHash xs
forall a b. (a -> b) -> a -> b
$
                                   Proxy blk -> HeaderHash blk -> ShortByteString
forall blk (proxy :: * -> *).
ConvertRawHash blk =>
proxy blk -> HeaderHash blk -> ShortByteString
toShortRawHash (Proxy blk
forall k (t :: k). Proxy t
Proxy @blk) HeaderHash blk
HeaderHash (Header blk)
headerFieldHash
          , headerFieldSlot :: SlotNo
headerFieldSlot    = SlotNo
headerFieldSlot
          , headerFieldBlockNo :: BlockNo
headerFieldBlockNo = BlockNo
headerFieldBlockNo
          }
        where
          HeaderFields{SlotNo
BlockNo
HeaderHash (Header blk)
headerFieldBlockNo :: BlockNo
headerFieldBlockNo :: forall b. HeaderFields b -> BlockNo
headerFieldSlot :: SlotNo
headerFieldSlot :: forall b. HeaderFields b -> SlotNo
headerFieldHash :: HeaderHash (Header blk)
headerFieldHash :: forall b. HeaderFields b -> HeaderHash b
..} = Header blk -> HeaderFields (Header blk)
forall b. HasHeader b => b -> HeaderFields b
getHeaderFields Header blk
hdr

instance CanHardFork xs => GetPrevHash (HardForkBlock xs) where
  headerPrevHash :: Header (HardForkBlock xs) -> ChainHash (HardForkBlock xs)
headerPrevHash =
        NS (K (ChainHash (HardForkBlock xs))) xs
-> ChainHash (HardForkBlock xs)
forall k l (h :: (k -> *) -> l -> *) (xs :: l) a.
(HCollapse h, SListIN h xs) =>
h (K a) xs -> CollapseTo h a
hcollapse
      (NS (K (ChainHash (HardForkBlock xs))) xs
 -> ChainHash (HardForkBlock xs))
-> (Header (HardForkBlock xs)
    -> NS (K (ChainHash (HardForkBlock xs))) xs)
-> Header (HardForkBlock xs)
-> ChainHash (HardForkBlock xs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy SingleEraBlock
-> (forall a.
    SingleEraBlock a =>
    Header a -> K (ChainHash (HardForkBlock xs)) a)
-> NS Header xs
-> NS (K (ChainHash (HardForkBlock xs))) xs
forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *)
       (f' :: k -> *).
(AllN (Prod h) c xs, HAp h) =>
proxy c
-> (forall (a :: k). c a => f a -> f' a) -> h f xs -> h f' xs
hcmap Proxy SingleEraBlock
proxySingle (ChainHash (HardForkBlock xs) -> K (ChainHash (HardForkBlock xs)) a
forall k a (b :: k). a -> K a b
K (ChainHash (HardForkBlock xs)
 -> K (ChainHash (HardForkBlock xs)) a)
-> (Header a -> ChainHash (HardForkBlock xs))
-> Header a
-> K (ChainHash (HardForkBlock xs)) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Header a -> ChainHash (HardForkBlock xs)
forall blk.
SingleEraBlock blk =>
Header blk -> ChainHash (HardForkBlock xs)
getOnePrev)
      (NS Header xs -> NS (K (ChainHash (HardForkBlock xs))) xs)
-> (Header (HardForkBlock xs) -> NS Header xs)
-> Header (HardForkBlock xs)
-> NS (K (ChainHash (HardForkBlock xs))) xs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OneEraHeader xs -> NS Header xs
forall (xs :: [*]). OneEraHeader xs -> NS Header xs
getOneEraHeader
      (OneEraHeader xs -> NS Header xs)
-> (Header (HardForkBlock xs) -> OneEraHeader xs)
-> Header (HardForkBlock xs)
-> NS Header xs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Header (HardForkBlock xs) -> OneEraHeader xs
forall (xs :: [*]). Header (HardForkBlock xs) -> OneEraHeader xs
getHardForkHeader
    where
      getOnePrev :: forall blk. SingleEraBlock blk
                 => Header blk -> ChainHash (HardForkBlock xs)
      getOnePrev :: Header blk -> ChainHash (HardForkBlock xs)
getOnePrev Header blk
hdr =
          case Header blk -> ChainHash blk
forall blk. GetPrevHash blk => Header blk -> ChainHash blk
headerPrevHash Header blk
hdr of
            ChainHash blk
GenesisHash -> ChainHash (HardForkBlock xs)
forall b. ChainHash b
GenesisHash
            BlockHash HeaderHash blk
h -> HeaderHash (HardForkBlock xs) -> ChainHash (HardForkBlock xs)
forall b. HeaderHash b -> ChainHash b
BlockHash (ShortByteString -> OneEraHash xs
forall k (xs :: [k]). ShortByteString -> OneEraHash xs
OneEraHash (ShortByteString -> OneEraHash xs)
-> ShortByteString -> OneEraHash xs
forall a b. (a -> b) -> a -> b
$ Proxy blk -> HeaderHash blk -> ShortByteString
forall blk (proxy :: * -> *).
ConvertRawHash blk =>
proxy blk -> HeaderHash blk -> ShortByteString
toShortRawHash (Proxy blk
forall k (t :: k). Proxy t
Proxy @blk) HeaderHash blk
h)

{-------------------------------------------------------------------------------
  NestedContent
-------------------------------------------------------------------------------}

data instance NestedCtxt_ (HardForkBlock xs) :: (Type -> Type) -> (Type -> Type) where
    NCZ :: !(NestedCtxt_ x                  f a) -> NestedCtxt_ (HardForkBlock (x ': xs)) f a
    NCS :: !(NestedCtxt_ (HardForkBlock xs) f a) -> NestedCtxt_ (HardForkBlock (x ': xs)) f a

deriving instance All SingleEraBlock xs => Show (NestedCtxt_ (HardForkBlock xs) Header a)

instance CanHardFork xs => SameDepIndex (NestedCtxt_ (HardForkBlock xs) Header) where
  sameDepIndex :: NestedCtxt_ (HardForkBlock xs) Header a
-> NestedCtxt_ (HardForkBlock xs) Header b -> Maybe (a :~: b)
sameDepIndex = NestedCtxt_ (HardForkBlock xs) Header a
-> NestedCtxt_ (HardForkBlock xs) Header b -> Maybe (a :~: b)
forall (xs' :: [*]) a b.
All SingleEraBlock xs' =>
NestedCtxt_ (HardForkBlock xs') Header a
-> NestedCtxt_ (HardForkBlock xs') Header b -> Maybe (a :~: b)
go
    where
      go :: All SingleEraBlock xs'
         => NestedCtxt_ (HardForkBlock xs') Header a
         -> NestedCtxt_ (HardForkBlock xs') Header b
         -> Maybe (a :~: b)
      go :: NestedCtxt_ (HardForkBlock xs') Header a
-> NestedCtxt_ (HardForkBlock xs') Header b -> Maybe (a :~: b)
go (NCZ ctxt) (NCZ ctxt') = NestedCtxt_ x Header a -> NestedCtxt_ x Header b -> Maybe (a :~: b)
forall (f :: * -> *) a b.
SameDepIndex f =>
f a -> f b -> Maybe (a :~: b)
sameDepIndex NestedCtxt_ x Header a
ctxt NestedCtxt_ x Header b
NestedCtxt_ x Header b
ctxt'
      go (NCS ctxt) (NCS ctxt') = NestedCtxt_ (HardForkBlock xs) Header a
-> NestedCtxt_ (HardForkBlock xs) Header b -> Maybe (a :~: b)
forall (xs' :: [*]) a b.
All SingleEraBlock xs' =>
NestedCtxt_ (HardForkBlock xs') Header a
-> NestedCtxt_ (HardForkBlock xs') Header b -> Maybe (a :~: b)
go NestedCtxt_ (HardForkBlock xs) Header a
ctxt NestedCtxt_ (HardForkBlock xs) Header b
NestedCtxt_ (HardForkBlock xs) Header b
ctxt'
      go NestedCtxt_ (HardForkBlock xs') Header a
_          NestedCtxt_ (HardForkBlock xs') Header b
_           = Maybe (a :~: b)
forall a. Maybe a
Nothing

instance CanHardFork xs => HasNestedContent Header (HardForkBlock xs) where
  unnest :: Header (HardForkBlock xs)
-> DepPair (NestedCtxt Header (HardForkBlock xs))
unnest =
      NS Header xs -> DepPair (NestedCtxt Header (HardForkBlock xs))
forall (xs' :: [*]).
All SingleEraBlock xs' =>
NS Header xs' -> DepPair (NestedCtxt Header (HardForkBlock xs'))
go (NS Header xs -> DepPair (NestedCtxt Header (HardForkBlock xs)))
-> (Header (HardForkBlock xs) -> NS Header xs)
-> Header (HardForkBlock xs)
-> DepPair (NestedCtxt Header (HardForkBlock xs))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OneEraHeader xs -> NS Header xs
forall (xs :: [*]). OneEraHeader xs -> NS Header xs
getOneEraHeader (OneEraHeader xs -> NS Header xs)
-> (Header (HardForkBlock xs) -> OneEraHeader xs)
-> Header (HardForkBlock xs)
-> NS Header xs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Header (HardForkBlock xs) -> OneEraHeader xs
forall (xs :: [*]). Header (HardForkBlock xs) -> OneEraHeader xs
getHardForkHeader
    where
      go :: All SingleEraBlock xs'
         => NS Header xs' -> DepPair (NestedCtxt Header (HardForkBlock xs'))
      go :: NS Header xs' -> DepPair (NestedCtxt Header (HardForkBlock xs'))
go (Z Header x
x) = case Header x -> DepPair (NestedCtxt Header x)
forall (f :: * -> *) blk.
HasNestedContent f blk =>
f blk -> DepPair (NestedCtxt f blk)
unnest Header x
x of
                   DepPair (NestedCtxt NestedCtxt_ x Header a
ctxt) a
x' ->
                     NestedCtxt Header (HardForkBlock (x : xs)) a
-> a -> DepPair (NestedCtxt Header (HardForkBlock (x : xs)))
forall (f :: * -> *) a. f a -> a -> DepPair f
DepPair (NestedCtxt_ (HardForkBlock (x : xs)) Header a
-> NestedCtxt Header (HardForkBlock (x : xs)) a
forall (f :: * -> *) blk a.
NestedCtxt_ blk f a -> NestedCtxt f blk a
NestedCtxt (NestedCtxt_ x Header a
-> NestedCtxt_ (HardForkBlock (x : xs)) Header a
forall x (f :: * -> *) a (xs :: [*]).
NestedCtxt_ x f a -> NestedCtxt_ (HardForkBlock (x : xs)) f a
NCZ NestedCtxt_ x Header a
ctxt)) a
x'
      go (S NS Header xs
x) = case NS Header xs -> DepPair (NestedCtxt Header (HardForkBlock xs))
forall (xs' :: [*]).
All SingleEraBlock xs' =>
NS Header xs' -> DepPair (NestedCtxt Header (HardForkBlock xs'))
go NS Header xs
x of
                   DepPair (NestedCtxt NestedCtxt_ (HardForkBlock xs) Header a
ctxt) a
x' ->
                     NestedCtxt Header (HardForkBlock (x : xs)) a
-> a -> DepPair (NestedCtxt Header (HardForkBlock (x : xs)))
forall (f :: * -> *) a. f a -> a -> DepPair f
DepPair (NestedCtxt_ (HardForkBlock (x : xs)) Header a
-> NestedCtxt Header (HardForkBlock (x : xs)) a
forall (f :: * -> *) blk a.
NestedCtxt_ blk f a -> NestedCtxt f blk a
NestedCtxt (NestedCtxt_ (HardForkBlock xs) Header a
-> NestedCtxt_ (HardForkBlock (x : xs)) Header a
forall (xs :: [*]) (f :: * -> *) a x.
NestedCtxt_ (HardForkBlock xs) f a
-> NestedCtxt_ (HardForkBlock (x : xs)) f a
NCS NestedCtxt_ (HardForkBlock xs) Header a
ctxt)) a
x'

  nest :: DepPair (NestedCtxt Header (HardForkBlock xs))
-> Header (HardForkBlock xs)
nest = \(DepPair NestedCtxt Header (HardForkBlock xs) a
ctxt a
hdr) ->
      OneEraHeader xs -> Header (HardForkBlock xs)
forall (xs :: [*]). OneEraHeader xs -> Header (HardForkBlock xs)
HardForkHeader (OneEraHeader xs -> Header (HardForkBlock xs))
-> (NS Header xs -> OneEraHeader xs)
-> NS Header xs
-> Header (HardForkBlock xs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NS Header xs -> OneEraHeader xs
forall (xs :: [*]). NS Header xs -> OneEraHeader xs
OneEraHeader (NS Header xs -> Header (HardForkBlock xs))
-> NS Header xs -> Header (HardForkBlock xs)
forall a b. (a -> b) -> a -> b
$ NestedCtxt Header (HardForkBlock xs) a -> a -> NS Header xs
forall (xs' :: [*]) a.
All SingleEraBlock xs' =>
NestedCtxt Header (HardForkBlock xs') a -> a -> NS Header xs'
go NestedCtxt Header (HardForkBlock xs) a
ctxt a
hdr
    where
      go :: All SingleEraBlock xs'
         => NestedCtxt Header (HardForkBlock xs') a -> a -> NS Header xs'
      go :: NestedCtxt Header (HardForkBlock xs') a -> a -> NS Header xs'
go (NestedCtxt (NCZ ctxt)) a
x = Header x -> NS Header (x : xs)
forall a (f :: a -> *) (x :: a) (xs :: [a]). f x -> NS f (x : xs)
Z (DepPair (NestedCtxt Header x) -> Header x
forall (f :: * -> *) blk.
HasNestedContent f blk =>
DepPair (NestedCtxt f blk) -> f blk
nest (NestedCtxt Header x a -> a -> DepPair (NestedCtxt Header x)
forall (f :: * -> *) a. f a -> a -> DepPair f
DepPair (NestedCtxt_ x Header a -> NestedCtxt Header x a
forall (f :: * -> *) blk a.
NestedCtxt_ blk f a -> NestedCtxt f blk a
NestedCtxt NestedCtxt_ x Header a
ctxt) a
x))
      go (NestedCtxt (NCS ctxt)) a
x = NS Header xs -> NS Header (x : xs)
forall a (f :: a -> *) (xs :: [a]) (x :: a).
NS f xs -> NS f (x : xs)
S (NestedCtxt Header (HardForkBlock xs) a -> a -> NS Header xs
forall (xs' :: [*]) a.
All SingleEraBlock xs' =>
NestedCtxt Header (HardForkBlock xs') a -> a -> NS Header xs'
go (NestedCtxt_ (HardForkBlock xs) Header a
-> NestedCtxt Header (HardForkBlock xs) a
forall (f :: * -> *) blk a.
NestedCtxt_ blk f a -> NestedCtxt f blk a
NestedCtxt NestedCtxt_ (HardForkBlock xs) Header a
ctxt) a
x)

{-------------------------------------------------------------------------------
  ConvertRawHash
-------------------------------------------------------------------------------}

instance CanHardFork xs => ConvertRawHash (HardForkBlock xs) where
  toShortRawHash :: proxy (HardForkBlock xs)
-> HeaderHash (HardForkBlock xs) -> ShortByteString
toShortRawHash   proxy (HardForkBlock xs)
_ = HeaderHash (HardForkBlock xs) -> ShortByteString
forall k (xs :: [k]). OneEraHash xs -> ShortByteString
getOneEraHash
  fromShortRawHash :: proxy (HardForkBlock xs)
-> ShortByteString -> HeaderHash (HardForkBlock xs)
fromShortRawHash proxy (HardForkBlock xs)
_ = ShortByteString -> HeaderHash (HardForkBlock xs)
forall k (xs :: [k]). ShortByteString -> OneEraHash xs
OneEraHash
  hashSize :: proxy (HardForkBlock xs) -> Word32
hashSize         proxy (HardForkBlock xs)
_ = NP (K Word32) xs -> Word32
forall k (xs :: [k]) a.
(IsNonEmpty xs, Eq a, SListI xs, HasCallStack) =>
NP (K a) xs -> a
getSameValue NP (K Word32) xs
hashSizes
    where
      hashSizes :: NP (K Word32) xs
      hashSizes :: NP (K Word32) xs
hashSizes = Proxy SingleEraBlock
-> (forall a. SingleEraBlock a => K Word32 a) -> NP (K Word32) xs
forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *).
(HPure h, AllN h c xs) =>
proxy c -> (forall (a :: k). c a => f a) -> h f xs
hcpure Proxy SingleEraBlock
proxySingle forall a. SingleEraBlock a => K Word32 a
hashSizeOne

      hashSizeOne :: forall blk. SingleEraBlock blk => K Word32 blk
      hashSizeOne :: K Word32 blk
hashSizeOne = Word32 -> K Word32 blk
forall k a (b :: k). a -> K a b
K (Word32 -> K Word32 blk) -> Word32 -> K Word32 blk
forall a b. (a -> b) -> a -> b
$ Proxy blk -> Word32
forall blk (proxy :: * -> *).
ConvertRawHash blk =>
proxy blk -> Word32
hashSize (Proxy blk
forall k (t :: k). Proxy t
Proxy @blk)

{-------------------------------------------------------------------------------
  HasAnnTip
-------------------------------------------------------------------------------}

instance CanHardFork xs => HasAnnTip (HardForkBlock xs) where
  type TipInfo (HardForkBlock xs) = OneEraTipInfo xs

  getTipInfo :: Header (HardForkBlock xs) -> TipInfo (HardForkBlock xs)
getTipInfo =
        NS WrapTipInfo xs -> OneEraTipInfo xs
forall (xs :: [*]). NS WrapTipInfo xs -> OneEraTipInfo xs
OneEraTipInfo
      (NS WrapTipInfo xs -> OneEraTipInfo xs)
-> (Header (HardForkBlock xs) -> NS WrapTipInfo xs)
-> Header (HardForkBlock xs)
-> OneEraTipInfo xs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy SingleEraBlock
-> (forall a. SingleEraBlock a => Header a -> WrapTipInfo a)
-> NS Header xs
-> NS WrapTipInfo xs
forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *)
       (f' :: k -> *).
(AllN (Prod h) c xs, HAp h) =>
proxy c
-> (forall (a :: k). c a => f a -> f' a) -> h f xs -> h f' xs
hcmap Proxy SingleEraBlock
proxySingle (TipInfo a -> WrapTipInfo a
forall blk. TipInfo blk -> WrapTipInfo blk
WrapTipInfo (TipInfo a -> WrapTipInfo a)
-> (Header a -> TipInfo a) -> Header a -> WrapTipInfo a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Header a -> TipInfo a
forall blk. HasAnnTip blk => Header blk -> TipInfo blk
getTipInfo)
      (NS Header xs -> NS WrapTipInfo xs)
-> (Header (HardForkBlock xs) -> NS Header xs)
-> Header (HardForkBlock xs)
-> NS WrapTipInfo xs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OneEraHeader xs -> NS Header xs
forall (xs :: [*]). OneEraHeader xs -> NS Header xs
getOneEraHeader
      (OneEraHeader xs -> NS Header xs)
-> (Header (HardForkBlock xs) -> OneEraHeader xs)
-> Header (HardForkBlock xs)
-> NS Header xs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Header (HardForkBlock xs) -> OneEraHeader xs
forall (xs :: [*]). Header (HardForkBlock xs) -> OneEraHeader xs
getHardForkHeader

  tipInfoHash :: proxy (HardForkBlock xs)
-> TipInfo (HardForkBlock xs) -> HeaderHash (HardForkBlock xs)
tipInfoHash proxy (HardForkBlock xs)
_ =
        NS (K (OneEraHash xs)) xs -> OneEraHash xs
forall k l (h :: (k -> *) -> l -> *) (xs :: l) a.
(HCollapse h, SListIN h xs) =>
h (K a) xs -> CollapseTo h a
hcollapse
      (NS (K (OneEraHash xs)) xs -> OneEraHash xs)
-> (OneEraTipInfo xs -> NS (K (OneEraHash xs)) xs)
-> OneEraTipInfo xs
-> OneEraHash xs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy SingleEraBlock
-> (forall a.
    SingleEraBlock a =>
    WrapTipInfo a -> K (OneEraHash xs) a)
-> NS WrapTipInfo xs
-> NS (K (OneEraHash xs)) xs
forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *)
       (f' :: k -> *).
(AllN (Prod h) c xs, HAp h) =>
proxy c
-> (forall (a :: k). c a => f a -> f' a) -> h f xs -> h f' xs
hcmap Proxy SingleEraBlock
proxySingle (OneEraHash xs -> K (OneEraHash xs) a
forall k a (b :: k). a -> K a b
K (OneEraHash xs -> K (OneEraHash xs) a)
-> (WrapTipInfo a -> OneEraHash xs)
-> WrapTipInfo a
-> K (OneEraHash xs) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WrapTipInfo a -> OneEraHash xs
forall blk. SingleEraBlock blk => WrapTipInfo blk -> OneEraHash xs
tipInfoOne)
      (NS WrapTipInfo xs -> NS (K (OneEraHash xs)) xs)
-> (OneEraTipInfo xs -> NS WrapTipInfo xs)
-> OneEraTipInfo xs
-> NS (K (OneEraHash xs)) xs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OneEraTipInfo xs -> NS WrapTipInfo xs
forall (xs :: [*]). OneEraTipInfo xs -> NS WrapTipInfo xs
getOneEraTipInfo
    where
      tipInfoOne :: forall blk. SingleEraBlock blk
                 => WrapTipInfo blk -> OneEraHash xs
      tipInfoOne :: WrapTipInfo blk -> OneEraHash xs
tipInfoOne = ShortByteString -> OneEraHash xs
forall k (xs :: [k]). ShortByteString -> OneEraHash xs
OneEraHash
                 (ShortByteString -> OneEraHash xs)
-> (WrapTipInfo blk -> ShortByteString)
-> WrapTipInfo blk
-> OneEraHash xs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy blk -> HeaderHash blk -> ShortByteString
forall blk (proxy :: * -> *).
ConvertRawHash blk =>
proxy blk -> HeaderHash blk -> ShortByteString
toShortRawHash (Proxy blk
forall k (t :: k). Proxy t
Proxy @blk)
                 (HeaderHash blk -> ShortByteString)
-> (WrapTipInfo blk -> HeaderHash blk)
-> WrapTipInfo blk
-> ShortByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy blk -> TipInfo blk -> HeaderHash blk
forall blk (proxy :: * -> *).
HasAnnTip blk =>
proxy blk -> TipInfo blk -> HeaderHash blk
tipInfoHash    (Proxy blk
forall k (t :: k). Proxy t
Proxy @blk)
                 (TipInfo blk -> HeaderHash blk)
-> (WrapTipInfo blk -> TipInfo blk)
-> WrapTipInfo blk
-> HeaderHash blk
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WrapTipInfo blk -> TipInfo blk
forall blk. WrapTipInfo blk -> TipInfo blk
unwrapTipInfo

distribAnnTip :: SListI xs => AnnTip (HardForkBlock xs) -> NS AnnTip xs
distribAnnTip :: AnnTip (HardForkBlock xs) -> NS AnnTip xs
distribAnnTip AnnTip{SlotNo
BlockNo
TipInfo (HardForkBlock xs)
annTipInfo :: forall blk. AnnTip blk -> TipInfo blk
annTipBlockNo :: forall blk. AnnTip blk -> BlockNo
annTipSlotNo :: forall blk. AnnTip blk -> SlotNo
annTipInfo :: TipInfo (HardForkBlock xs)
annTipBlockNo :: BlockNo
annTipSlotNo :: SlotNo
..} =
    (forall a. WrapTipInfo a -> AnnTip a)
-> NS WrapTipInfo xs -> NS AnnTip 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 forall a. WrapTipInfo a -> AnnTip a
distrib (OneEraTipInfo xs -> NS WrapTipInfo xs
forall (xs :: [*]). OneEraTipInfo xs -> NS WrapTipInfo xs
getOneEraTipInfo TipInfo (HardForkBlock xs)
OneEraTipInfo xs
annTipInfo)
  where
    distrib :: WrapTipInfo blk -> AnnTip blk
    distrib :: WrapTipInfo blk -> AnnTip blk
distrib (WrapTipInfo TipInfo blk
info) =
        SlotNo -> BlockNo -> TipInfo blk -> AnnTip blk
forall blk. SlotNo -> BlockNo -> TipInfo blk -> AnnTip blk
AnnTip SlotNo
annTipSlotNo BlockNo
annTipBlockNo TipInfo blk
info

undistribAnnTip :: SListI xs => NS AnnTip xs -> AnnTip (HardForkBlock xs)
undistribAnnTip :: NS AnnTip xs -> AnnTip (HardForkBlock xs)
undistribAnnTip = NS (K (AnnTip (HardForkBlock xs))) xs -> AnnTip (HardForkBlock xs)
forall k l (h :: (k -> *) -> l -> *) (xs :: l) a.
(HCollapse h, SListIN h xs) =>
h (K a) xs -> CollapseTo h a
hcollapse (NS (K (AnnTip (HardForkBlock xs))) xs
 -> AnnTip (HardForkBlock xs))
-> (NS AnnTip xs -> NS (K (AnnTip (HardForkBlock xs))) xs)
-> NS AnnTip xs
-> AnnTip (HardForkBlock xs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a.
 Index xs a -> AnnTip a -> K (AnnTip (HardForkBlock xs)) a)
-> NS AnnTip xs -> NS (K (AnnTip (HardForkBlock xs))) xs
forall k (h :: (k -> *) -> [k] -> *) (xs :: [k]) (f1 :: k -> *)
       (f2 :: k -> *).
(HAp h, SListI xs, Prod h ~ NP) =>
(forall (a :: k). Index xs a -> f1 a -> f2 a) -> h f1 xs -> h f2 xs
himap forall (xs :: [*]) blk.
Index xs blk -> AnnTip blk -> K (AnnTip (HardForkBlock xs)) blk
forall a. Index xs a -> AnnTip a -> K (AnnTip (HardForkBlock xs)) a
undistrib
  where
    undistrib :: Index xs blk
              -> AnnTip blk
              -> K (AnnTip (HardForkBlock xs)) blk
    undistrib :: Index xs blk -> AnnTip blk -> K (AnnTip (HardForkBlock xs)) blk
undistrib Index xs blk
index AnnTip{SlotNo
BlockNo
TipInfo blk
annTipInfo :: TipInfo blk
annTipBlockNo :: BlockNo
annTipSlotNo :: SlotNo
annTipInfo :: forall blk. AnnTip blk -> TipInfo blk
annTipBlockNo :: forall blk. AnnTip blk -> BlockNo
annTipSlotNo :: forall blk. AnnTip blk -> SlotNo
..} = AnnTip (HardForkBlock xs) -> K (AnnTip (HardForkBlock xs)) blk
forall k a (b :: k). a -> K a b
K (AnnTip (HardForkBlock xs) -> K (AnnTip (HardForkBlock xs)) blk)
-> AnnTip (HardForkBlock xs) -> K (AnnTip (HardForkBlock xs)) blk
forall a b. (a -> b) -> a -> b
$
        SlotNo
-> BlockNo
-> TipInfo (HardForkBlock xs)
-> AnnTip (HardForkBlock xs)
forall blk. SlotNo -> BlockNo -> TipInfo blk -> AnnTip blk
AnnTip SlotNo
annTipSlotNo
               BlockNo
annTipBlockNo
               (NS WrapTipInfo xs -> OneEraTipInfo xs
forall (xs :: [*]). NS WrapTipInfo xs -> OneEraTipInfo xs
OneEraTipInfo (NS WrapTipInfo xs -> OneEraTipInfo xs)
-> (TipInfo blk -> NS WrapTipInfo xs)
-> TipInfo blk
-> OneEraTipInfo xs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index xs blk -> WrapTipInfo blk -> NS WrapTipInfo xs
forall k (f :: k -> *) (x :: k) (xs :: [k]).
Index xs x -> f x -> NS f xs
injectNS Index xs blk
index (WrapTipInfo blk -> NS WrapTipInfo xs)
-> (TipInfo blk -> WrapTipInfo blk)
-> TipInfo blk
-> NS WrapTipInfo xs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TipInfo blk -> WrapTipInfo blk
forall blk. TipInfo blk -> WrapTipInfo blk
WrapTipInfo (TipInfo blk -> OneEraTipInfo xs)
-> TipInfo blk -> OneEraTipInfo xs
forall a b. (a -> b) -> a -> b
$ TipInfo blk
annTipInfo)

{-------------------------------------------------------------------------------
  BasicEnvelopeValidation
-------------------------------------------------------------------------------}

instance CanHardFork xs => BasicEnvelopeValidation (HardForkBlock xs) where
  expectedFirstBlockNo :: proxy (HardForkBlock xs) -> BlockNo
expectedFirstBlockNo proxy (HardForkBlock xs)
_ =
      case Proxy xs -> ProofNonEmpty xs
forall a (xs :: [a]) (proxy :: [a] -> *).
IsNonEmpty xs =>
proxy xs -> ProofNonEmpty xs
isNonEmpty (Proxy xs
forall k (t :: k). Proxy t
Proxy @xs) of
        ProofNonEmpty Proxy x
p Proxy xs
_ -> Proxy x -> BlockNo
forall blk (proxy :: * -> *).
BasicEnvelopeValidation blk =>
proxy blk -> BlockNo
expectedFirstBlockNo Proxy x
p

  minimumPossibleSlotNo :: Proxy (HardForkBlock xs) -> SlotNo
minimumPossibleSlotNo Proxy (HardForkBlock xs)
_ =
      case Proxy xs -> ProofNonEmpty xs
forall a (xs :: [a]) (proxy :: [a] -> *).
IsNonEmpty xs =>
proxy xs -> ProofNonEmpty xs
isNonEmpty (Proxy xs
forall k (t :: k). Proxy t
Proxy @xs) of
        ProofNonEmpty Proxy x
p Proxy xs
_ -> Proxy x -> SlotNo
forall blk. BasicEnvelopeValidation blk => Proxy blk -> SlotNo
minimumPossibleSlotNo Proxy x
p

  -- TODO: If the block is from a different era as the current tip, we just
  -- expect @succ b@. This may not be sufficient: if we ever transition /to/
  -- an era with EBBs, this is not correct.
  expectedNextBlockNo :: proxy (HardForkBlock xs)
-> TipInfo (HardForkBlock xs)
-> TipInfo (HardForkBlock xs)
-> BlockNo
-> BlockNo
expectedNextBlockNo proxy (HardForkBlock xs)
_ (OneEraTipInfo oldTip) (OneEraTipInfo newBlock) BlockNo
b =
      case NS WrapTipInfo xs
-> NS WrapTipInfo xs
-> Either
     (Mismatch WrapTipInfo WrapTipInfo xs)
     (NS (Product WrapTipInfo WrapTipInfo) xs)
forall k (f :: k -> *) (xs :: [k]) (g :: k -> *).
NS f xs
-> NS g xs -> Either (Mismatch f g xs) (NS (Product f g) xs)
Match.matchNS NS WrapTipInfo xs
oldTip NS WrapTipInfo xs
newBlock of
        Right NS (Product WrapTipInfo WrapTipInfo) xs
matched  -> NS (K BlockNo) xs -> CollapseTo NS BlockNo
forall k l (h :: (k -> *) -> l -> *) (xs :: l) a.
(HCollapse h, SListIN h xs) =>
h (K a) xs -> CollapseTo h a
hcollapse (NS (K BlockNo) xs -> CollapseTo NS BlockNo)
-> NS (K BlockNo) xs -> CollapseTo NS BlockNo
forall a b. (a -> b) -> a -> b
$ Proxy SingleEraBlock
-> (forall a.
    SingleEraBlock a =>
    Product WrapTipInfo WrapTipInfo a -> K BlockNo a)
-> NS (Product WrapTipInfo WrapTipInfo) xs
-> NS (K BlockNo) xs
forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *)
       (f' :: k -> *).
(AllN (Prod h) c xs, HAp h) =>
proxy c
-> (forall (a :: k). c a => f a -> f' a) -> h f xs -> h f' xs
hcmap Proxy SingleEraBlock
proxySingle forall a.
SingleEraBlock a =>
Product WrapTipInfo WrapTipInfo a -> K BlockNo a
aux NS (Product WrapTipInfo WrapTipInfo) xs
matched
        Left Mismatch WrapTipInfo WrapTipInfo xs
_mismatch -> BlockNo -> BlockNo
forall a. Enum a => a -> a
succ BlockNo
b
    where
      aux :: forall blk. SingleEraBlock blk
          => Product WrapTipInfo WrapTipInfo blk
          -> K BlockNo blk
      aux :: Product WrapTipInfo WrapTipInfo blk -> K BlockNo blk
aux (Pair (WrapTipInfo TipInfo blk
old) (WrapTipInfo TipInfo blk
new)) = BlockNo -> K BlockNo blk
forall k a (b :: k). a -> K a b
K (BlockNo -> K BlockNo blk) -> BlockNo -> K BlockNo blk
forall a b. (a -> b) -> a -> b
$
          Proxy blk -> TipInfo blk -> TipInfo blk -> BlockNo -> BlockNo
forall blk (proxy :: * -> *).
BasicEnvelopeValidation blk =>
proxy blk -> TipInfo blk -> TipInfo blk -> BlockNo -> BlockNo
expectedNextBlockNo (Proxy blk
forall k (t :: k). Proxy t
Proxy @blk) TipInfo blk
old TipInfo blk
new BlockNo
b

  -- TODO: If the block is from a different era as the current tip, we just
  -- expect @succ s@. This may not be sufficient: if we ever transition /to/
  -- an era with EBBs, this is not correct.
  minimumNextSlotNo :: proxy (HardForkBlock xs)
-> TipInfo (HardForkBlock xs)
-> TipInfo (HardForkBlock xs)
-> SlotNo
-> SlotNo
minimumNextSlotNo proxy (HardForkBlock xs)
_ (OneEraTipInfo oldTip) (OneEraTipInfo newBlock) SlotNo
s =
      case NS WrapTipInfo xs
-> NS WrapTipInfo xs
-> Either
     (Mismatch WrapTipInfo WrapTipInfo xs)
     (NS (Product WrapTipInfo WrapTipInfo) xs)
forall k (f :: k -> *) (xs :: [k]) (g :: k -> *).
NS f xs
-> NS g xs -> Either (Mismatch f g xs) (NS (Product f g) xs)
Match.matchNS NS WrapTipInfo xs
oldTip NS WrapTipInfo xs
newBlock of
        Right NS (Product WrapTipInfo WrapTipInfo) xs
matched  -> NS (K SlotNo) xs -> CollapseTo NS SlotNo
forall k l (h :: (k -> *) -> l -> *) (xs :: l) a.
(HCollapse h, SListIN h xs) =>
h (K a) xs -> CollapseTo h a
hcollapse (NS (K SlotNo) xs -> CollapseTo NS SlotNo)
-> NS (K SlotNo) xs -> CollapseTo NS SlotNo
forall a b. (a -> b) -> a -> b
$ Proxy SingleEraBlock
-> (forall a.
    SingleEraBlock a =>
    Product WrapTipInfo WrapTipInfo a -> K SlotNo a)
-> NS (Product WrapTipInfo WrapTipInfo) xs
-> NS (K SlotNo) xs
forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *)
       (f' :: k -> *).
(AllN (Prod h) c xs, HAp h) =>
proxy c
-> (forall (a :: k). c a => f a -> f' a) -> h f xs -> h f' xs
hcmap Proxy SingleEraBlock
proxySingle forall a.
SingleEraBlock a =>
Product WrapTipInfo WrapTipInfo a -> K SlotNo a
aux NS (Product WrapTipInfo WrapTipInfo) xs
matched
        Left Mismatch WrapTipInfo WrapTipInfo xs
_mismatch -> SlotNo -> SlotNo
forall a. Enum a => a -> a
succ SlotNo
s
    where
      aux :: forall blk. SingleEraBlock blk
          => Product WrapTipInfo WrapTipInfo blk
          -> K SlotNo blk
      aux :: Product WrapTipInfo WrapTipInfo blk -> K SlotNo blk
aux (Pair (WrapTipInfo TipInfo blk
old) (WrapTipInfo TipInfo blk
new)) = SlotNo -> K SlotNo blk
forall k a (b :: k). a -> K a b
K (SlotNo -> K SlotNo blk) -> SlotNo -> K SlotNo blk
forall a b. (a -> b) -> a -> b
$
          Proxy blk -> TipInfo blk -> TipInfo blk -> SlotNo -> SlotNo
forall blk (proxy :: * -> *).
BasicEnvelopeValidation blk =>
proxy blk -> TipInfo blk -> TipInfo blk -> SlotNo -> SlotNo
minimumNextSlotNo (Proxy blk
forall k (t :: k). Proxy t
Proxy @blk) TipInfo blk
old TipInfo blk
new SlotNo
s

{-------------------------------------------------------------------------------
  Other instances (primarily for the benefit of tests)
-------------------------------------------------------------------------------}

instance All Eq xs => Eq (HardForkBlock xs) where
  == :: HardForkBlock xs -> HardForkBlock xs -> Bool
(==) = (Either (Mismatch I I xs) (NS (Product I I) xs) -> Bool
aux (Either (Mismatch I I xs) (NS (Product I I) xs) -> Bool)
-> (NS I xs
    -> NS I xs -> Either (Mismatch I I xs) (NS (Product I I) xs))
-> NS I xs
-> NS I xs
-> Bool
forall y z x0 x1. (y -> z) -> (x0 -> x1 -> y) -> x0 -> x1 -> z
.: NS I xs
-> NS I xs -> Either (Mismatch I I xs) (NS (Product I I) xs)
forall k (f :: k -> *) (xs :: [k]) (g :: k -> *).
NS f xs
-> NS g xs -> Either (Mismatch f g xs) (NS (Product f g) xs)
Match.matchNS) (NS I xs -> NS I xs -> Bool)
-> (HardForkBlock xs -> NS I xs)
-> HardForkBlock xs
-> HardForkBlock xs
-> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (OneEraBlock xs -> NS I xs
forall (xs :: [*]). OneEraBlock xs -> NS I xs
getOneEraBlock (OneEraBlock xs -> NS I xs)
-> (HardForkBlock xs -> OneEraBlock xs)
-> HardForkBlock xs
-> NS I xs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HardForkBlock xs -> OneEraBlock xs
forall (xs :: [*]). HardForkBlock xs -> OneEraBlock xs
getHardForkBlock)
    where
      aux :: Either (Match.Mismatch I I xs) (NS (Product I I) xs) -> Bool
      aux :: Either (Mismatch I I xs) (NS (Product I I) xs) -> Bool
aux (Left  Mismatch I I xs
_) = Bool
False
      aux (Right NS (Product I I) xs
m) = NS (K Bool) xs -> CollapseTo NS Bool
forall k l (h :: (k -> *) -> l -> *) (xs :: l) a.
(HCollapse h, SListIN h xs) =>
h (K a) xs -> CollapseTo h a
hcollapse (NS (K Bool) xs -> CollapseTo NS Bool)
-> NS (K Bool) xs -> CollapseTo NS Bool
forall a b. (a -> b) -> a -> b
$
                        Proxy Eq
-> (forall a. Eq a => Product I I a -> K Bool a)
-> NS (Product I I) xs
-> NS (K Bool) xs
forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *)
       (f' :: k -> *).
(AllN (Prod h) c xs, HAp h) =>
proxy c
-> (forall (a :: k). c a => f a -> f' a) -> h f xs -> h f' xs
hcmap (Proxy Eq
forall k (t :: k). Proxy t
Proxy @Eq) (\(Pair x y) -> Bool -> K Bool a
forall k a (b :: k). a -> K a b
K (Bool -> K Bool a) -> Bool -> K Bool a
forall a b. (a -> b) -> a -> b
$ I a
x I a -> I a -> Bool
forall a. Eq a => a -> a -> Bool
== I a
y) NS (Product I I) xs
m

instance All (Compose Eq Header) xs => Eq (Header (HardForkBlock xs)) where
  == :: Header (HardForkBlock xs) -> Header (HardForkBlock xs) -> Bool
(==) = (Either (Mismatch Header Header xs) (NS (Product Header Header) xs)
-> Bool
aux (Either (Mismatch Header Header xs) (NS (Product Header Header) xs)
 -> Bool)
-> (NS Header xs
    -> NS Header xs
    -> Either
         (Mismatch Header Header xs) (NS (Product Header Header) xs))
-> NS Header xs
-> NS Header xs
-> Bool
forall y z x0 x1. (y -> z) -> (x0 -> x1 -> y) -> x0 -> x1 -> z
.: NS Header xs
-> NS Header xs
-> Either
     (Mismatch Header Header xs) (NS (Product Header Header) xs)
forall k (f :: k -> *) (xs :: [k]) (g :: k -> *).
NS f xs
-> NS g xs -> Either (Mismatch f g xs) (NS (Product f g) xs)
Match.matchNS) (NS Header xs -> NS Header xs -> Bool)
-> (Header (HardForkBlock xs) -> NS Header xs)
-> Header (HardForkBlock xs)
-> Header (HardForkBlock xs)
-> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (OneEraHeader xs -> NS Header xs
forall (xs :: [*]). OneEraHeader xs -> NS Header xs
getOneEraHeader (OneEraHeader xs -> NS Header xs)
-> (Header (HardForkBlock xs) -> OneEraHeader xs)
-> Header (HardForkBlock xs)
-> NS Header xs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Header (HardForkBlock xs) -> OneEraHeader xs
forall (xs :: [*]). Header (HardForkBlock xs) -> OneEraHeader xs
getHardForkHeader)
    where
      aux :: Either (Match.Mismatch Header Header xs) (NS (Product Header Header) xs)
          -> Bool
      aux :: Either (Mismatch Header Header xs) (NS (Product Header Header) xs)
-> Bool
aux (Left  Mismatch Header Header xs
_) = Bool
False
      aux (Right NS (Product Header Header) xs
m) = NS (K Bool) xs -> CollapseTo NS Bool
forall k l (h :: (k -> *) -> l -> *) (xs :: l) a.
(HCollapse h, SListIN h xs) =>
h (K a) xs -> CollapseTo h a
hcollapse (NS (K Bool) xs -> CollapseTo NS Bool)
-> NS (K Bool) xs -> CollapseTo NS Bool
forall a b. (a -> b) -> a -> b
$
                        Proxy (Compose Eq Header)
-> (forall a.
    Compose Eq Header a =>
    Product Header Header a -> K Bool a)
-> NS (Product Header Header) xs
-> NS (K Bool) xs
forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *)
       (f' :: k -> *).
(AllN (Prod h) c xs, HAp h) =>
proxy c
-> (forall (a :: k). c a => f a -> f' a) -> h f xs -> h f' xs
hcmap
                          (Proxy (Compose Eq Header)
forall k (t :: k). Proxy t
Proxy @(Compose Eq Header))
                          (\(Pair x y) -> Bool -> K Bool a
forall k a (b :: k). a -> K a b
K (Bool -> K Bool a) -> Bool -> K Bool a
forall a b. (a -> b) -> a -> b
$ Header a
x Header a -> Header a -> Bool
forall a. Eq a => a -> a -> Bool
== Header a
y)
                          NS (Product Header Header) xs
m