{-# 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.BasicFunctors
import           Data.SOP.Constraint
import           Data.SOP.Index
import qualified Data.SOP.Match as Match
import           Data.SOP.Strict
import           Data.Typeable (Typeable)
import           Data.Word
import           NoThunks.Class (NoThunks)
import           Ouroboros.Consensus.Block
import           Ouroboros.Consensus.HardFork.Combinator.Abstract
import           Ouroboros.Consensus.HardFork.Combinator.AcrossEras
import           Ouroboros.Consensus.HardFork.Combinator.Basics
import           Ouroboros.Consensus.HeaderValidation
import           Ouroboros.Consensus.TypeFamilyWrappers
import           Ouroboros.Consensus.Util (ShowProxy, (.:))

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

newtype instance Header (HardForkBlock xs) = HardForkHeader {
      forall (xs :: [*]). 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
$cshowsPrec :: forall (xs :: [*]).
CanHardFork xs =>
Int -> Header (HardForkBlock xs) -> ShowS
showsPrec :: Int -> Header (HardForkBlock xs) -> ShowS
$cshow :: forall (xs :: [*]).
CanHardFork xs =>
Header (HardForkBlock xs) -> String
show :: Header (HardForkBlock xs) -> String
$cshowList :: forall (xs :: [*]).
CanHardFork xs =>
[Header (HardForkBlock xs)] -> ShowS
showList :: [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
$cnoThunks :: forall (xs :: [*]).
CanHardFork xs =>
Context -> Header (HardForkBlock xs) -> IO (Maybe ThunkInfo)
noThunks :: Context -> Header (HardForkBlock xs) -> IO (Maybe ThunkInfo)
$cwNoThunks :: forall (xs :: [*]).
CanHardFork xs =>
Context -> Header (HardForkBlock xs) -> IO (Maybe ThunkInfo)
wNoThunks :: Context -> Header (HardForkBlock xs) -> IO (Maybe ThunkInfo)
$cshowTypeOf :: forall (xs :: [*]).
CanHardFork xs =>
Proxy (Header (HardForkBlock xs)) -> String
showTypeOf :: Proxy (Header (HardForkBlock xs)) -> String
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 (xs :: [*]) a.
SListIN NS xs =>
NS (K a) xs -> CollapseTo NS a
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 Product Header I a -> K Bool a
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 :: forall blk. GetHeader blk => 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
NS (K (Maybe EpochNo)) xs -> CollapseTo NS (Maybe EpochNo)
forall (xs :: [*]) a.
SListIN NS xs =>
NS (K a) xs -> CollapseTo NS a
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))
NS (K (HeaderFields (Header (HardForkBlock xs)))) xs
-> CollapseTo NS (HeaderFields (Header (HardForkBlock xs)))
forall (xs :: [*]) a.
SListIN NS xs =>
NS (K a) xs -> CollapseTo NS a
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 :: forall blk.
SingleEraBlock blk =>
Header blk -> HeaderFields (Header (HardForkBlock xs))
getOne Header blk
hdr = 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
forall (proxy :: * -> *).
proxy blk -> HeaderHash blk -> ShortByteString
toShortRawHash (forall t. Proxy t
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{BlockNo
SlotNo
HeaderHash (Header blk)
headerFieldHash :: forall k (b :: k). HeaderFields b -> HeaderHash b
headerFieldHash :: HeaderHash (Header blk)
headerFieldSlot :: forall k (b :: k). HeaderFields b -> SlotNo
headerFieldSlot :: SlotNo
headerFieldBlockNo :: forall k (b :: k). HeaderFields b -> BlockNo
headerFieldBlockNo :: BlockNo
..} = 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)
NS (K (ChainHash (HardForkBlock xs))) xs
-> CollapseTo NS (ChainHash (HardForkBlock xs))
forall (xs :: [*]) a.
SListIN NS xs =>
NS (K a) xs -> CollapseTo NS a
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 :: forall blk.
SingleEraBlock blk =>
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 {k} (b :: k). ChainHash b
GenesisHash
            BlockHash HeaderHash blk
h -> HeaderHash (HardForkBlock xs) -> ChainHash (HardForkBlock xs)
forall {k} (b :: k). 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
forall (proxy :: * -> *).
proxy blk -> HeaderHash blk -> ShortByteString
toShortRawHash (forall t. Proxy t
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 :: forall a b.
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 :: forall (xs' :: [*]) a b.
All SingleEraBlock xs' =>
NestedCtxt_ (HardForkBlock xs') Header a
-> NestedCtxt_ (HardForkBlock xs') Header b -> Maybe (a :~: b)
go (NCZ NestedCtxt_ x Header a
ctxt) (NCZ NestedCtxt_ x Header b
ctxt') = NestedCtxt_ x Header a -> NestedCtxt_ x Header b -> Maybe (a :~: b)
forall a b.
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 NestedCtxt_ (HardForkBlock xs) Header a
ctxt) (NCS NestedCtxt_ (HardForkBlock xs) Header b
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 :: forall (xs' :: [*]).
All SingleEraBlock xs' =>
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 xs') a
-> a -> DepPair (NestedCtxt Header (HardForkBlock xs'))
forall (f :: * -> *) a. f a -> a -> DepPair f
DepPair (NestedCtxt_ (HardForkBlock xs') Header a
-> NestedCtxt Header (HardForkBlock xs') a
forall (f :: * -> *) blk a.
NestedCtxt_ blk f a -> NestedCtxt f blk a
NestedCtxt (NestedCtxt_ x Header a
-> NestedCtxt_ (HardForkBlock (x : xs1)) Header a
forall xs (f :: * -> *) a (x :: [*]).
NestedCtxt_ xs f a -> NestedCtxt_ (HardForkBlock (xs : x)) f a
NCZ NestedCtxt_ x Header a
ctxt)) a
x'
      go (S NS Header xs1
x) = case NS Header xs1 -> DepPair (NestedCtxt Header (HardForkBlock xs1))
forall (xs' :: [*]).
All SingleEraBlock xs' =>
NS Header xs' -> DepPair (NestedCtxt Header (HardForkBlock xs'))
go NS Header xs1
x of
                   DepPair (NestedCtxt NestedCtxt_ (HardForkBlock xs1) Header a
ctxt) a
x' ->
                     NestedCtxt Header (HardForkBlock xs') a
-> a -> DepPair (NestedCtxt Header (HardForkBlock xs'))
forall (f :: * -> *) a. f a -> a -> DepPair f
DepPair (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 xs1) Header a
-> NestedCtxt_ (HardForkBlock (x : xs1)) Header a
forall (xs :: [*]) (f :: * -> *) a x.
NestedCtxt_ (HardForkBlock xs) f a
-> NestedCtxt_ (HardForkBlock (x : xs)) f a
NCS NestedCtxt_ (HardForkBlock xs1) 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 :: forall (xs' :: [*]) a.
All SingleEraBlock xs' =>
NestedCtxt Header (HardForkBlock xs') a -> a -> NS Header xs'
go (NestedCtxt (NCZ NestedCtxt_ x Header a
ctxt)) a
x = Header x -> NS Header (x : xs)
forall {k} (f :: k -> *) (x :: k) (xs1 :: [k]).
f x -> NS f (x : xs1)
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 NestedCtxt_ (HardForkBlock xs) Header a
ctxt)) a
x = NS Header xs -> NS Header (x : xs)
forall {k} (f :: k -> *) (xs1 :: [k]) (x :: k).
NS f xs1 -> NS f (x : xs1)
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 :: forall (proxy :: * -> *).
proxy (HardForkBlock xs)
-> HeaderHash (HardForkBlock xs) -> ShortByteString
toShortRawHash   proxy (HardForkBlock xs)
_ = HeaderHash (HardForkBlock xs) -> ShortByteString
OneEraHash xs -> ShortByteString
forall k (xs :: [k]). OneEraHash xs -> ShortByteString
getOneEraHash
  fromShortRawHash :: forall (proxy :: * -> *).
proxy (HardForkBlock xs)
-> ShortByteString -> HeaderHash (HardForkBlock xs)
fromShortRawHash proxy (HardForkBlock xs)
_ = ShortByteString -> HeaderHash (HardForkBlock xs)
ShortByteString -> OneEraHash xs
forall k (xs :: [k]). ShortByteString -> OneEraHash xs
OneEraHash
  hashSize :: forall (proxy :: * -> *). 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
forall (c :: * -> Constraint) (xs :: [*])
       (proxy :: (* -> Constraint) -> *) (f :: * -> *).
AllN NP c xs =>
proxy c -> (forall a. c a => f a) -> NP f xs
hcpure Proxy SingleEraBlock
proxySingle K Word32 a
forall a. SingleEraBlock a => K Word32 a
hashSizeOne

      hashSizeOne :: forall blk. SingleEraBlock blk => K Word32 blk
      hashSizeOne :: forall a. SingleEraBlock a => K Word32 a
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
forall (proxy :: * -> *). proxy blk -> Word32
hashSize (forall t. Proxy t
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 :: forall (proxy :: * -> *).
proxy (HardForkBlock xs)
-> TipInfo (HardForkBlock xs) -> HeaderHash (HardForkBlock xs)
tipInfoHash proxy (HardForkBlock xs)
_ =
        NS (K (OneEraHash xs)) xs -> CollapseTo NS (OneEraHash xs)
NS (K (OneEraHash xs)) xs -> OneEraHash xs
forall (xs :: [*]) a.
SListIN NS xs =>
NS (K a) xs -> CollapseTo NS a
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 :: forall blk. SingleEraBlock blk => 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
forall (proxy :: * -> *).
proxy blk -> HeaderHash blk -> ShortByteString
toShortRawHash (forall t. Proxy t
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
forall (proxy :: * -> *).
proxy blk -> TipInfo blk -> HeaderHash blk
tipInfoHash    (forall t. Proxy t
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 :: forall (xs :: [*]).
SListI xs =>
AnnTip (HardForkBlock xs) -> NS AnnTip xs
distribAnnTip AnnTip{BlockNo
SlotNo
TipInfo (HardForkBlock xs)
annTipSlotNo :: SlotNo
annTipBlockNo :: BlockNo
annTipInfo :: TipInfo (HardForkBlock xs)
annTipSlotNo :: forall blk. AnnTip blk -> SlotNo
annTipBlockNo :: forall blk. AnnTip blk -> BlockNo
annTipInfo :: forall blk. AnnTip blk -> TipInfo blk
..} =
    (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 WrapTipInfo a -> AnnTip a
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 :: forall a. WrapTipInfo a -> AnnTip a
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 :: forall (xs :: [*]).
SListI xs =>
NS AnnTip xs -> AnnTip (HardForkBlock xs)
undistribAnnTip = NS (K (AnnTip (HardForkBlock xs))) xs
-> CollapseTo NS (AnnTip (HardForkBlock xs))
NS (K (AnnTip (HardForkBlock xs))) xs -> AnnTip (HardForkBlock xs)
forall (xs :: [*]) a.
SListIN NS xs =>
NS (K a) xs -> CollapseTo NS a
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 Index xs a -> AnnTip a -> K (AnnTip (HardForkBlock xs)) a
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 :: forall (xs :: [*]) blk.
Index xs blk -> AnnTip blk -> K (AnnTip (HardForkBlock xs)) blk
undistrib Index xs blk
index AnnTip{BlockNo
SlotNo
TipInfo blk
annTipSlotNo :: forall blk. AnnTip blk -> SlotNo
annTipBlockNo :: forall blk. AnnTip blk -> BlockNo
annTipInfo :: forall blk. AnnTip blk -> TipInfo blk
annTipSlotNo :: SlotNo
annTipBlockNo :: BlockNo
annTipInfo :: TipInfo blk
..} = 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 -> TipInfo (HardForkBlock xs)
NS WrapTipInfo xs -> OneEraTipInfo xs
forall (xs :: [*]). NS WrapTipInfo xs -> OneEraTipInfo xs
OneEraTipInfo (NS WrapTipInfo xs -> TipInfo (HardForkBlock xs))
-> (TipInfo blk -> NS WrapTipInfo xs)
-> TipInfo blk
-> TipInfo (HardForkBlock 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 -> TipInfo (HardForkBlock xs))
-> TipInfo blk -> TipInfo (HardForkBlock xs)
forall a b. (a -> b) -> a -> b
$ TipInfo blk
annTipInfo)

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

instance CanHardFork xs => BasicEnvelopeValidation (HardForkBlock xs) where
  expectedFirstBlockNo :: forall (proxy :: * -> *). 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
forall (proxy :: [*] -> *). proxy xs -> ProofNonEmpty xs
isNonEmpty (forall (t :: [*]). Proxy t
forall {k} (t :: k). Proxy t
Proxy @xs) of
        ProofNonEmpty Proxy x
p Proxy xs1
_ -> Proxy x -> BlockNo
forall blk (proxy :: * -> *).
BasicEnvelopeValidation blk =>
proxy blk -> BlockNo
forall (proxy :: * -> *). proxy x -> 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
forall (proxy :: [*] -> *). proxy xs -> ProofNonEmpty xs
isNonEmpty (forall (t :: [*]). Proxy t
forall {k} (t :: k). Proxy t
Proxy @xs) of
        ProofNonEmpty Proxy x
p Proxy xs1
_ -> 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 :: forall (proxy :: * -> *).
proxy (HardForkBlock xs)
-> TipInfo (HardForkBlock xs)
-> TipInfo (HardForkBlock xs)
-> BlockNo
-> BlockNo
expectedNextBlockNo proxy (HardForkBlock xs)
_ (OneEraTipInfo NS WrapTipInfo xs
oldTip) (OneEraTipInfo NS WrapTipInfo xs
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 (xs :: [*]) a.
SListIN NS xs =>
NS (K a) xs -> CollapseTo NS a
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 Product WrapTipInfo WrapTipInfo a -> K BlockNo a
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 :: forall a.
SingleEraBlock a =>
Product WrapTipInfo WrapTipInfo a -> K BlockNo a
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
forall (proxy :: * -> *).
proxy blk -> TipInfo blk -> TipInfo blk -> BlockNo -> BlockNo
expectedNextBlockNo (forall t. Proxy t
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 :: forall (proxy :: * -> *).
proxy (HardForkBlock xs)
-> TipInfo (HardForkBlock xs)
-> TipInfo (HardForkBlock xs)
-> SlotNo
-> SlotNo
minimumNextSlotNo proxy (HardForkBlock xs)
_ (OneEraTipInfo NS WrapTipInfo xs
oldTip) (OneEraTipInfo NS WrapTipInfo xs
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 (xs :: [*]) a.
SListIN NS xs =>
NS (K a) xs -> CollapseTo NS a
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 Product WrapTipInfo WrapTipInfo a -> K SlotNo a
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 :: forall a.
SingleEraBlock a =>
Product WrapTipInfo WrapTipInfo a -> K SlotNo a
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
forall (proxy :: * -> *).
proxy blk -> TipInfo blk -> TipInfo blk -> SlotNo -> SlotNo
minimumNextSlotNo (forall t. Proxy t
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 (xs :: [*]) a.
SListIN NS xs =>
NS (K a) xs -> CollapseTo NS a
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 (forall {k} (t :: k). Proxy t
forall (t :: * -> Constraint). Proxy t
Proxy @Eq) (\(Pair I a
x I a
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 (xs :: [*]) a.
SListIN NS xs =>
NS (K a) xs -> CollapseTo NS a
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
                          (forall {k} (t :: k). Proxy t
forall (t :: * -> Constraint). Proxy t
Proxy @(Compose Eq Header))
                          (\(Pair Header a
x Header a
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