{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}

-- | Infrastructure for doing chain selection across eras
module Ouroboros.Consensus.HardFork.Combinator.Protocol.ChainSel (
    AcrossEraMode (..)
  , AcrossEraSelection (..)
  , WithBlockNo (..)
  , acrossEraSelection
  , mapWithBlockNo
  ) where

import           Data.Kind (Type)
import           Data.SOP.Constraint
import           Data.SOP.Strict
import           Data.SOP.Tails (Tails (..))
import           GHC.Generics (Generic)
import           NoThunks.Class (NoThunks)
import           Ouroboros.Consensus.Block
import           Ouroboros.Consensus.HardFork.Combinator.Abstract.SingleEraBlock
import           Ouroboros.Consensus.Protocol.Abstract
import           Ouroboros.Consensus.TypeFamilyWrappers

{-------------------------------------------------------------------------------
  Configuration
-------------------------------------------------------------------------------}

data AcrossEraSelection :: Type -> Type -> Type where
  -- | Just compare block numbers
  --
  -- This is a useful default when two eras run totally different consensus
  -- protocols, and we just want to choose the longer chain.
  CompareBlockNo :: AcrossEraSelection x y

  -- | Two eras using the same 'SelectView'. In this case, we can just compare
  -- chains even across eras, as the chain ordering is fully captured by
  -- 'SelectView' and its 'ChainOrder' instance.
  --
  -- We use the 'ChainOrderConfig' of the 'SelectView' in the newer era (with
  -- the intuition that newer eras are generally "preferred") when invoking
  -- 'compareChains'. However, this choice is arbitrary; we could also make it
  -- configurable here.
  CompareSameSelectView ::
       SelectView (BlockProtocol x) ~ SelectView (BlockProtocol y)
    => AcrossEraSelection x y

{-------------------------------------------------------------------------------
  Compare two eras
-------------------------------------------------------------------------------}


-- | GADT indicating whether we are lifting 'compare' or 'preferCandidate' to
-- the HFC, together with the type of configuration we need for that and the
-- result type.
data AcrossEraMode cfg a where
  AcrossEraCompare         :: AcrossEraMode Proxy                Ordering
  AcrossEraPreferCandidate :: AcrossEraMode WrapChainOrderConfig Bool

applyAcrossEraMode ::
     ChainOrder sv
  => cfg blk
  -> (WrapChainOrderConfig blk -> ChainOrderConfig sv)
  -> AcrossEraMode cfg a
  -> sv -> sv -> a
applyAcrossEraMode :: forall sv (cfg :: * -> *) blk a.
ChainOrder sv =>
cfg blk
-> (WrapChainOrderConfig blk -> ChainOrderConfig sv)
-> AcrossEraMode cfg a
-> sv
-> sv
-> a
applyAcrossEraMode cfg blk
cfg WrapChainOrderConfig blk -> ChainOrderConfig sv
f = \case
    AcrossEraMode cfg a
AcrossEraCompare         -> sv -> sv -> a
sv -> sv -> Ordering
forall a. Ord a => a -> a -> Ordering
compare
    AcrossEraMode cfg a
AcrossEraPreferCandidate -> ChainOrderConfig sv -> sv -> sv -> Bool
forall sv. ChainOrder sv => ChainOrderConfig sv -> sv -> sv -> Bool
preferCandidate (WrapChainOrderConfig blk -> ChainOrderConfig sv
f cfg blk
WrapChainOrderConfig blk
cfg)

data FlipArgs = KeepArgs | FlipArgs

acrossEras ::
     forall blk blk' cfg a. SingleEraBlock blk
  => FlipArgs
  -> AcrossEraMode cfg a
  -> cfg                        blk'
     -- ^ The configuration corresponding to the later block/era, also see
     -- 'CompareSameSelectView'.
  -> WithBlockNo WrapSelectView blk
  -> WithBlockNo WrapSelectView blk'
  -> AcrossEraSelection blk blk'
  -> a
acrossEras :: forall blk blk' (cfg :: * -> *) a.
SingleEraBlock blk =>
FlipArgs
-> AcrossEraMode cfg a
-> cfg blk'
-> WithBlockNo WrapSelectView blk
-> WithBlockNo WrapSelectView blk'
-> AcrossEraSelection blk blk'
-> a
acrossEras FlipArgs
flipArgs AcrossEraMode cfg a
mode cfg blk'
cfg
  (WithBlockNo BlockNo
bnoL (WrapSelectView SelectView (BlockProtocol blk)
l))
  (WithBlockNo BlockNo
bnoR (WrapSelectView SelectView (BlockProtocol blk')
r)) = \case
    AcrossEraSelection blk blk'
CompareBlockNo        -> (BlockNo -> BlockNo -> a) -> BlockNo -> BlockNo -> a
forall b. (b -> b -> a) -> b -> b -> a
maybeFlip BlockNo -> BlockNo -> a
cmp BlockNo
bnoL BlockNo
bnoR
      where
        cmp :: BlockNo -> BlockNo -> a
cmp = cfg blk'
-> (WrapChainOrderConfig blk' -> ChainOrderConfig BlockNo)
-> AcrossEraMode cfg a
-> BlockNo
-> BlockNo
-> a
forall sv (cfg :: * -> *) blk a.
ChainOrder sv =>
cfg blk
-> (WrapChainOrderConfig blk -> ChainOrderConfig sv)
-> AcrossEraMode cfg a
-> sv
-> sv
-> a
applyAcrossEraMode cfg blk'
cfg (() -> WrapChainOrderConfig blk' -> ()
forall a b. a -> b -> a
const ()) AcrossEraMode cfg a
mode
    AcrossEraSelection blk blk'
CompareSameSelectView -> (SelectView (BlockProtocol blk')
 -> SelectView (BlockProtocol blk') -> a)
-> SelectView (BlockProtocol blk')
-> SelectView (BlockProtocol blk')
-> a
forall b. (b -> b -> a) -> b -> b -> a
maybeFlip SelectView (BlockProtocol blk')
-> SelectView (BlockProtocol blk') -> a
cmp SelectView (BlockProtocol blk)
SelectView (BlockProtocol blk')
l SelectView (BlockProtocol blk')
r
      where
        cmp :: SelectView (BlockProtocol blk')
-> SelectView (BlockProtocol blk') -> a
cmp = cfg blk'
-> (WrapChainOrderConfig blk'
    -> ChainOrderConfig (SelectView (BlockProtocol blk')))
-> AcrossEraMode cfg a
-> SelectView (BlockProtocol blk')
-> SelectView (BlockProtocol blk')
-> a
forall sv (cfg :: * -> *) blk a.
ChainOrder sv =>
cfg blk
-> (WrapChainOrderConfig blk -> ChainOrderConfig sv)
-> AcrossEraMode cfg a
-> sv
-> sv
-> a
applyAcrossEraMode cfg blk'
cfg (WrapChainOrderConfig blk'
-> ChainOrderConfig (SelectView (BlockProtocol blk'))
forall blk.
WrapChainOrderConfig blk
-> ChainOrderConfig (SelectView (BlockProtocol blk))
unwrapChainOrderConfig) AcrossEraMode cfg a
mode
  where
    maybeFlip :: (b -> b -> a) -> b -> b -> a
    maybeFlip :: forall b. (b -> b -> a) -> b -> b -> a
maybeFlip = case FlipArgs
flipArgs of
      FlipArgs
KeepArgs -> (b -> b -> a) -> b -> b -> a
forall a. a -> a
id
      FlipArgs
FlipArgs -> (b -> b -> a) -> b -> b -> a
forall a b c. (a -> b -> c) -> b -> a -> c
flip

acrossEraSelection ::
     forall xs cfg a.
     All SingleEraBlock              xs
  => AcrossEraMode cfg a
  -> NP cfg                          xs
  -> Tails AcrossEraSelection        xs
  -> WithBlockNo (NS WrapSelectView) xs
  -> WithBlockNo (NS WrapSelectView) xs
  -> a
acrossEraSelection :: forall (xs :: [*]) (cfg :: * -> *) a.
All SingleEraBlock xs =>
AcrossEraMode cfg a
-> NP cfg xs
-> Tails AcrossEraSelection xs
-> WithBlockNo (NS WrapSelectView) xs
-> WithBlockNo (NS WrapSelectView) xs
-> a
acrossEraSelection AcrossEraMode cfg a
mode = \NP cfg xs
cfg Tails AcrossEraSelection xs
ffs WithBlockNo (NS WrapSelectView) xs
l WithBlockNo (NS WrapSelectView) xs
r ->
    NP cfg xs
-> Tails AcrossEraSelection xs
-> (NS (WithBlockNo WrapSelectView) xs,
    NS (WithBlockNo WrapSelectView) xs)
-> a
forall (xs' :: [*]).
All SingleEraBlock xs' =>
NP cfg xs'
-> Tails AcrossEraSelection xs'
-> (NS (WithBlockNo WrapSelectView) xs',
    NS (WithBlockNo WrapSelectView) xs')
-> a
goBoth NP cfg xs
cfg Tails AcrossEraSelection xs
ffs (WithBlockNo (NS WrapSelectView) xs
-> NS (WithBlockNo WrapSelectView) xs
forall {k} (xs :: [k]) (f :: k -> *).
SListI xs =>
WithBlockNo (NS f) xs -> NS (WithBlockNo f) xs
distribBlockNo WithBlockNo (NS WrapSelectView) xs
l, WithBlockNo (NS WrapSelectView) xs
-> NS (WithBlockNo WrapSelectView) xs
forall {k} (xs :: [k]) (f :: k -> *).
SListI xs =>
WithBlockNo (NS f) xs -> NS (WithBlockNo f) xs
distribBlockNo WithBlockNo (NS WrapSelectView) xs
r)
  where
    goBoth ::
         All SingleEraBlock                xs'
      => NP cfg                            xs'
      -> Tails AcrossEraSelection          xs'
      -> ( NS (WithBlockNo WrapSelectView) xs'
         , NS (WithBlockNo WrapSelectView) xs'
         )
      -> a
    goBoth :: forall (xs' :: [*]).
All SingleEraBlock xs' =>
NP cfg xs'
-> Tails AcrossEraSelection xs'
-> (NS (WithBlockNo WrapSelectView) xs',
    NS (WithBlockNo WrapSelectView) xs')
-> a
goBoth NP cfg xs'
_             Tails AcrossEraSelection xs'
TNil            = \(NS (WithBlockNo WrapSelectView) xs'
a, NS (WithBlockNo WrapSelectView) xs'
_) -> case NS (WithBlockNo WrapSelectView) xs'
a of {}
    goBoth (cfg x
cfg :* NP cfg xs1
cfgs) (TCons NP (AcrossEraSelection x) xs1
fs Tails AcrossEraSelection xs1
ffs') = \case
        (Z WithBlockNo WrapSelectView x
a, Z WithBlockNo WrapSelectView x
b) -> WrapSelectView x -> WrapSelectView x -> a
cmp (WithBlockNo WrapSelectView x -> WrapSelectView x
forall k (f :: k -> *) (a :: k). WithBlockNo f a -> f a
dropBlockNo WithBlockNo WrapSelectView x
a) (WithBlockNo WrapSelectView x -> WrapSelectView x
forall k (f :: k -> *) (a :: k). WithBlockNo f a -> f a
dropBlockNo WithBlockNo WrapSelectView x
WithBlockNo WrapSelectView x
b)
          where
            cmp :: WrapSelectView x -> WrapSelectView x -> a
cmp = cfg x
-> (WrapChainOrderConfig x -> ChainOrderConfig (WrapSelectView x))
-> AcrossEraMode cfg a
-> WrapSelectView x
-> WrapSelectView x
-> a
forall sv (cfg :: * -> *) blk a.
ChainOrder sv =>
cfg blk
-> (WrapChainOrderConfig blk -> ChainOrderConfig sv)
-> AcrossEraMode cfg a
-> sv
-> sv
-> a
applyAcrossEraMode cfg x
cfg WrapChainOrderConfig x
-> ChainOrderConfig (SelectView (BlockProtocol x))
WrapChainOrderConfig x -> ChainOrderConfig (WrapSelectView x)
forall blk.
WrapChainOrderConfig blk
-> ChainOrderConfig (SelectView (BlockProtocol blk))
unwrapChainOrderConfig AcrossEraMode cfg a
mode
        (Z WithBlockNo WrapSelectView x
a, S NS (WithBlockNo WrapSelectView) xs1
b) -> FlipArgs
-> WithBlockNo WrapSelectView x
-> NP cfg xs1
-> NP (AcrossEraSelection x) xs1
-> NS (WithBlockNo WrapSelectView) xs1
-> a
forall x (xs' :: [*]).
(SingleEraBlock x, All SingleEraBlock xs') =>
FlipArgs
-> WithBlockNo WrapSelectView x
-> NP cfg xs'
-> NP (AcrossEraSelection x) xs'
-> NS (WithBlockNo WrapSelectView) xs'
-> a
goOne FlipArgs
KeepArgs WithBlockNo WrapSelectView x
a NP cfg xs1
cfgs NP (AcrossEraSelection x) xs1
NP (AcrossEraSelection x) xs1
fs NS (WithBlockNo WrapSelectView) xs1
NS (WithBlockNo WrapSelectView) xs1
b
        (S NS (WithBlockNo WrapSelectView) xs1
a, Z WithBlockNo WrapSelectView x
b) -> FlipArgs
-> WithBlockNo WrapSelectView x
-> NP cfg xs1
-> NP (AcrossEraSelection x) xs1
-> NS (WithBlockNo WrapSelectView) xs1
-> a
forall x (xs' :: [*]).
(SingleEraBlock x, All SingleEraBlock xs') =>
FlipArgs
-> WithBlockNo WrapSelectView x
-> NP cfg xs'
-> NP (AcrossEraSelection x) xs'
-> NS (WithBlockNo WrapSelectView) xs'
-> a
goOne FlipArgs
FlipArgs WithBlockNo WrapSelectView x
b NP cfg xs1
cfgs NP (AcrossEraSelection x) xs1
NP (AcrossEraSelection x) xs1
fs NS (WithBlockNo WrapSelectView) xs1
NS (WithBlockNo WrapSelectView) xs1
a
        (S NS (WithBlockNo WrapSelectView) xs1
a, S NS (WithBlockNo WrapSelectView) xs1
b) -> NP cfg xs1
-> Tails AcrossEraSelection xs1
-> (NS (WithBlockNo WrapSelectView) xs1,
    NS (WithBlockNo WrapSelectView) xs1)
-> a
forall (xs' :: [*]).
All SingleEraBlock xs' =>
NP cfg xs'
-> Tails AcrossEraSelection xs'
-> (NS (WithBlockNo WrapSelectView) xs',
    NS (WithBlockNo WrapSelectView) xs')
-> a
goBoth NP cfg xs1
cfgs Tails AcrossEraSelection xs1
Tails AcrossEraSelection xs1
ffs' (NS (WithBlockNo WrapSelectView) xs1
NS (WithBlockNo WrapSelectView) xs1
a, NS (WithBlockNo WrapSelectView) xs1
NS (WithBlockNo WrapSelectView) xs1
b)

    goOne ::
         forall x xs'. (SingleEraBlock x, All SingleEraBlock xs')
      => FlipArgs
      -> WithBlockNo WrapSelectView x
      -> NP cfg                          xs'
      -> NP (AcrossEraSelection     x)   xs'
      -> NS (WithBlockNo WrapSelectView) xs'
      -> a
    goOne :: forall x (xs' :: [*]).
(SingleEraBlock x, All SingleEraBlock xs') =>
FlipArgs
-> WithBlockNo WrapSelectView x
-> NP cfg xs'
-> NP (AcrossEraSelection x) xs'
-> NS (WithBlockNo WrapSelectView) xs'
-> a
goOne FlipArgs
flipArgs WithBlockNo WrapSelectView x
a = NP cfg xs'
-> NP (AcrossEraSelection x) xs'
-> NS (WithBlockNo WrapSelectView) xs'
-> a
forall (xs'' :: [*]).
All SingleEraBlock xs'' =>
NP cfg xs''
-> NP (AcrossEraSelection x) xs''
-> NS (WithBlockNo WrapSelectView) xs''
-> a
go
      where
        go :: forall xs''. All SingleEraBlock xs''
           => NP cfg                          xs''
           -> NP (AcrossEraSelection x)       xs''
           -> NS (WithBlockNo WrapSelectView) xs''
           -> a
        go :: forall (xs'' :: [*]).
All SingleEraBlock xs'' =>
NP cfg xs''
-> NP (AcrossEraSelection x) xs''
-> NS (WithBlockNo WrapSelectView) xs''
-> a
go NP cfg xs''
_             NP (AcrossEraSelection x) xs''
Nil          NS (WithBlockNo WrapSelectView) xs''
b  = case NS (WithBlockNo WrapSelectView) xs''
b of {}
        go (cfg x
cfg :* NP cfg xs1
_   ) (AcrossEraSelection x x
f :* NP (AcrossEraSelection x) xs1
_)  (Z WithBlockNo WrapSelectView x
b) = FlipArgs
-> AcrossEraMode cfg a
-> cfg x
-> WithBlockNo WrapSelectView x
-> WithBlockNo WrapSelectView x
-> AcrossEraSelection x x
-> a
forall blk blk' (cfg :: * -> *) a.
SingleEraBlock blk =>
FlipArgs
-> AcrossEraMode cfg a
-> cfg blk'
-> WithBlockNo WrapSelectView blk
-> WithBlockNo WrapSelectView blk'
-> AcrossEraSelection blk blk'
-> a
acrossEras FlipArgs
flipArgs AcrossEraMode cfg a
mode cfg x
cfg WithBlockNo WrapSelectView x
a WithBlockNo WrapSelectView x
WithBlockNo WrapSelectView x
b AcrossEraSelection x x
AcrossEraSelection x x
f
        go (cfg x
_   :* NP cfg xs1
cfgs) (AcrossEraSelection x x
_ :* NP (AcrossEraSelection x) xs1
fs) (S NS (WithBlockNo WrapSelectView) xs1
b) = NP cfg xs1
-> NP (AcrossEraSelection x) xs1
-> NS (WithBlockNo WrapSelectView) xs1
-> a
forall (xs'' :: [*]).
All SingleEraBlock xs'' =>
NP cfg xs''
-> NP (AcrossEraSelection x) xs''
-> NS (WithBlockNo WrapSelectView) xs''
-> a
go NP cfg xs1
cfgs NP (AcrossEraSelection x) xs1
NP (AcrossEraSelection x) xs1
fs NS (WithBlockNo WrapSelectView) xs1
NS (WithBlockNo WrapSelectView) xs1
b

{-------------------------------------------------------------------------------
  WithBlockNo
-------------------------------------------------------------------------------}

data WithBlockNo (f :: k -> Type) (a :: k) = WithBlockNo {
      forall k (f :: k -> *) (a :: k). WithBlockNo f a -> BlockNo
getBlockNo  :: BlockNo
    , forall k (f :: k -> *) (a :: k). WithBlockNo f a -> f a
dropBlockNo :: f a
    }
  deriving (Int -> WithBlockNo f a -> ShowS
[WithBlockNo f a] -> ShowS
WithBlockNo f a -> String
(Int -> WithBlockNo f a -> ShowS)
-> (WithBlockNo f a -> String)
-> ([WithBlockNo f a] -> ShowS)
-> Show (WithBlockNo f a)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (f :: k -> *) (a :: k).
Show (f a) =>
Int -> WithBlockNo f a -> ShowS
forall k (f :: k -> *) (a :: k).
Show (f a) =>
[WithBlockNo f a] -> ShowS
forall k (f :: k -> *) (a :: k).
Show (f a) =>
WithBlockNo f a -> String
$cshowsPrec :: forall k (f :: k -> *) (a :: k).
Show (f a) =>
Int -> WithBlockNo f a -> ShowS
showsPrec :: Int -> WithBlockNo f a -> ShowS
$cshow :: forall k (f :: k -> *) (a :: k).
Show (f a) =>
WithBlockNo f a -> String
show :: WithBlockNo f a -> String
$cshowList :: forall k (f :: k -> *) (a :: k).
Show (f a) =>
[WithBlockNo f a] -> ShowS
showList :: [WithBlockNo f a] -> ShowS
Show, WithBlockNo f a -> WithBlockNo f a -> Bool
(WithBlockNo f a -> WithBlockNo f a -> Bool)
-> (WithBlockNo f a -> WithBlockNo f a -> Bool)
-> Eq (WithBlockNo f a)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall k (f :: k -> *) (a :: k).
Eq (f a) =>
WithBlockNo f a -> WithBlockNo f a -> Bool
$c== :: forall k (f :: k -> *) (a :: k).
Eq (f a) =>
WithBlockNo f a -> WithBlockNo f a -> Bool
== :: WithBlockNo f a -> WithBlockNo f a -> Bool
$c/= :: forall k (f :: k -> *) (a :: k).
Eq (f a) =>
WithBlockNo f a -> WithBlockNo f a -> Bool
/= :: WithBlockNo f a -> WithBlockNo f a -> Bool
Eq, (forall x. WithBlockNo f a -> Rep (WithBlockNo f a) x)
-> (forall x. Rep (WithBlockNo f a) x -> WithBlockNo f a)
-> Generic (WithBlockNo f a)
forall x. Rep (WithBlockNo f a) x -> WithBlockNo f a
forall x. WithBlockNo f a -> Rep (WithBlockNo f a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall k (f :: k -> *) (a :: k) x.
Rep (WithBlockNo f a) x -> WithBlockNo f a
forall k (f :: k -> *) (a :: k) x.
WithBlockNo f a -> Rep (WithBlockNo f a) x
$cfrom :: forall k (f :: k -> *) (a :: k) x.
WithBlockNo f a -> Rep (WithBlockNo f a) x
from :: forall x. WithBlockNo f a -> Rep (WithBlockNo f a) x
$cto :: forall k (f :: k -> *) (a :: k) x.
Rep (WithBlockNo f a) x -> WithBlockNo f a
to :: forall x. Rep (WithBlockNo f a) x -> WithBlockNo f a
Generic, Context -> WithBlockNo f a -> IO (Maybe ThunkInfo)
Proxy (WithBlockNo f a) -> String
(Context -> WithBlockNo f a -> IO (Maybe ThunkInfo))
-> (Context -> WithBlockNo f a -> IO (Maybe ThunkInfo))
-> (Proxy (WithBlockNo f a) -> String)
-> NoThunks (WithBlockNo f a)
forall a.
(Context -> a -> IO (Maybe ThunkInfo))
-> (Context -> a -> IO (Maybe ThunkInfo))
-> (Proxy a -> String)
-> NoThunks a
forall k (f :: k -> *) (a :: k).
NoThunks (f a) =>
Context -> WithBlockNo f a -> IO (Maybe ThunkInfo)
forall k (f :: k -> *) (a :: k).
NoThunks (f a) =>
Proxy (WithBlockNo f a) -> String
$cnoThunks :: forall k (f :: k -> *) (a :: k).
NoThunks (f a) =>
Context -> WithBlockNo f a -> IO (Maybe ThunkInfo)
noThunks :: Context -> WithBlockNo f a -> IO (Maybe ThunkInfo)
$cwNoThunks :: forall k (f :: k -> *) (a :: k).
NoThunks (f a) =>
Context -> WithBlockNo f a -> IO (Maybe ThunkInfo)
wNoThunks :: Context -> WithBlockNo f a -> IO (Maybe ThunkInfo)
$cshowTypeOf :: forall k (f :: k -> *) (a :: k).
NoThunks (f a) =>
Proxy (WithBlockNo f a) -> String
showTypeOf :: Proxy (WithBlockNo f a) -> String
NoThunks)

mapWithBlockNo :: (f x -> g y) -> WithBlockNo f x -> WithBlockNo g y
mapWithBlockNo :: forall {k} {k} (f :: k -> *) (x :: k) (g :: k -> *) (y :: k).
(f x -> g y) -> WithBlockNo f x -> WithBlockNo g y
mapWithBlockNo f x -> g y
f (WithBlockNo BlockNo
bno f x
fx) = BlockNo -> g y -> WithBlockNo g y
forall k (f :: k -> *) (a :: k). BlockNo -> f a -> WithBlockNo f a
WithBlockNo BlockNo
bno (f x -> g y
f f x
fx)

distribBlockNo :: SListI xs => WithBlockNo (NS f) xs -> NS (WithBlockNo f) xs
distribBlockNo :: forall {k} (xs :: [k]) (f :: k -> *).
SListI xs =>
WithBlockNo (NS f) xs -> NS (WithBlockNo f) xs
distribBlockNo (WithBlockNo BlockNo
b NS f xs
ns) = (forall (a :: k). f a -> WithBlockNo f a)
-> NS f xs -> NS (WithBlockNo f) 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 (BlockNo -> f a -> WithBlockNo f a
forall k (f :: k -> *) (a :: k). BlockNo -> f a -> WithBlockNo f a
WithBlockNo BlockNo
b) NS f xs
ns