{-# 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.FingerTree.Strict (Measured (..))
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 => Measured BlockMeasure (HardForkBlock xs) where
  measure :: HardForkBlock xs -> BlockMeasure
measure = HardForkBlock xs -> BlockMeasure
forall b. HasHeader b => b -> BlockMeasure
blockMeasure

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 (xs :: [*]) 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.
 Injection WrapTipInfo xs a
 -> AnnTip a -> K (AnnTip (HardForkBlock xs)) a)
-> Prod NS (Injection WrapTipInfo xs) xs
-> NS AnnTip xs
-> NS (K (AnnTip (HardForkBlock xs))) xs
forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
       (f' :: k -> *) (f'' :: k -> *).
(SListIN (Prod h) xs, HAp h, HAp (Prod h)) =>
(forall (a :: k). f a -> f' a -> f'' a)
-> Prod h f xs -> h f' xs -> h f'' xs
hzipWith forall (xs :: [*]) blk.
(-.->) WrapTipInfo (K (NS WrapTipInfo xs)) blk
-> AnnTip blk -> K (AnnTip (HardForkBlock xs)) blk
forall a.
Injection WrapTipInfo xs a
-> AnnTip a -> K (AnnTip (HardForkBlock xs)) a
undistrib Prod NS (Injection WrapTipInfo xs) xs
forall k (xs :: [k]) (f :: k -> *).
SListI xs =>
NP (Injection f xs) xs
injections
  where
    undistrib :: (WrapTipInfo -.-> K (NS WrapTipInfo xs)) blk
              -> AnnTip blk
              -> K (AnnTip (HardForkBlock xs)) blk
    undistrib :: (-.->) WrapTipInfo (K (NS WrapTipInfo xs)) blk
-> AnnTip blk -> K (AnnTip (HardForkBlock xs)) blk
undistrib (-.->) WrapTipInfo (K (NS WrapTipInfo xs)) blk
inj 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)
-> NS WrapTipInfo xs -> OneEraTipInfo xs
forall a b. (a -> b) -> a -> b
$ K (NS WrapTipInfo xs) blk -> NS WrapTipInfo xs
forall k a (b :: k). K a b -> a
unK (K (NS WrapTipInfo xs) blk -> NS WrapTipInfo xs)
-> (TipInfo blk -> K (NS WrapTipInfo xs) blk)
-> TipInfo blk
-> NS WrapTipInfo xs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (-.->) WrapTipInfo (K (NS WrapTipInfo xs)) blk
-> WrapTipInfo blk -> K (NS WrapTipInfo xs) blk
forall k (f :: k -> *) (g :: k -> *) (a :: k).
(-.->) f g a -> f a -> g a
apFn (-.->) WrapTipInfo (K (NS WrapTipInfo xs)) blk
inj (WrapTipInfo blk -> K (NS WrapTipInfo xs) blk)
-> (TipInfo blk -> WrapTipInfo blk)
-> TipInfo blk
-> K (NS WrapTipInfo xs) blk
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TipInfo blk -> WrapTipInfo blk
forall blk. TipInfo blk -> WrapTipInfo blk
WrapTipInfo (TipInfo blk -> NS WrapTipInfo xs)
-> TipInfo blk -> NS WrapTipInfo 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 (xs :: [*]) (proxy :: [*] -> *).
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 (xs :: [*]) (proxy :: [*] -> *).
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