{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

-- | Injecting a transaction from one block type to another
module Ouroboros.Consensus.HardFork.Combinator.InjectTxs (
    -- * Polymorphic
    InjectPolyTx (..)
  , cannotInjectPolyTx
  , matchPolyTx
  , matchPolyTxsNS
    -- * Unvalidated transactions
  , InjectTx
  , cannotInjectTx
  , matchTx
  , pattern InjectTx
    -- * Validated transactions
  , InjectValidatedTx
  , cannotInjectValidatedTx
  , matchValidatedTx
  , matchValidatedTxsNS
  , pattern InjectValidatedTx
  ) where

import           Data.Bifunctor
import           Data.Functor.Product
import           Data.SOP.BasicFunctors
import           Data.SOP.InPairs (InPairs (..))
import           Data.SOP.Match
import           Data.SOP.Sing
import           Data.SOP.Strict
import           Data.SOP.Telescope (Telescope (..))
import qualified Data.SOP.Telescope as Telescope
import           Ouroboros.Consensus.HardFork.Combinator.State.Types
import           Ouroboros.Consensus.Ledger.SupportsMempool
import           Ouroboros.Consensus.TypeFamilyWrappers
import           Ouroboros.Consensus.Util (pairFst)

{-------------------------------------------------------------------------------
  Polymorphic definitions
-------------------------------------------------------------------------------}

-- | @tx@ is either 'GenTx' or 'WrapValidatedGenTx'
--
-- See 'InjectTx' and 'InjectValidatedTx', respectively.
data InjectPolyTx tx blk blk' = InjectPolyTx {
      forall (tx :: * -> *) blk blk'.
InjectPolyTx tx blk blk' -> tx blk -> Maybe (tx blk')
injectTxWith :: tx blk  -> Maybe (tx blk')
    }

-- | The injection that always fails
cannotInjectPolyTx :: InjectPolyTx tx blk blk'
cannotInjectPolyTx :: forall (tx :: * -> *) blk blk'. InjectPolyTx tx blk blk'
cannotInjectPolyTx = (tx blk -> Maybe (tx blk')) -> InjectPolyTx tx blk blk'
forall (tx :: * -> *) blk blk'.
(tx blk -> Maybe (tx blk')) -> InjectPolyTx tx blk blk'
InjectPolyTx ((tx blk -> Maybe (tx blk')) -> InjectPolyTx tx blk blk')
-> (tx blk -> Maybe (tx blk')) -> InjectPolyTx tx blk blk'
forall a b. (a -> b) -> a -> b
$ Maybe (tx blk') -> tx blk -> Maybe (tx blk')
forall a b. a -> b -> a
const Maybe (tx blk')
forall a. Maybe a
Nothing

-- | Match transaction with a telescope, attempting to inject where possible
matchPolyTx' ::
     InPairs (InjectPolyTx tx) xs
  -> NS tx xs
  -> Telescope g f xs
  -> Either (Mismatch tx f xs)
            (Telescope g (Product tx f) xs)
matchPolyTx' :: forall (tx :: * -> *) (xs :: [*]) (g :: * -> *) (f :: * -> *).
InPairs (InjectPolyTx tx) xs
-> NS tx xs
-> Telescope g f xs
-> Either (Mismatch tx f xs) (Telescope g (Product tx f) xs)
matchPolyTx' = InPairs (InjectPolyTx tx) xs
-> NS tx xs
-> Telescope g f xs
-> Either (Mismatch tx f xs) (Telescope g (Product tx f) xs)
forall (tx :: * -> *) (xs :: [*]) (g :: * -> *) (f :: * -> *).
InPairs (InjectPolyTx tx) xs
-> NS tx xs
-> Telescope g f xs
-> Either (Mismatch tx f xs) (Telescope g (Product tx f) xs)
go
  where
    go :: InPairs (InjectPolyTx tx) xs
       -> NS tx xs
       -> Telescope g f xs
       -> Either (Mismatch tx f xs)
                 (Telescope g (Product tx f) xs)
    go :: forall (tx :: * -> *) (xs :: [*]) (g :: * -> *) (f :: * -> *).
InPairs (InjectPolyTx tx) xs
-> NS tx xs
-> Telescope g f xs
-> Either (Mismatch tx f xs) (Telescope g (Product tx f) xs)
go InPairs (InjectPolyTx tx) xs
_            (Z tx x
x) (TZ f x
f)   = Telescope g (Product tx f) xs
-> Either (Mismatch tx f xs) (Telescope g (Product tx f) xs)
forall a b. b -> Either a b
Right (Telescope g (Product tx f) xs
 -> Either (Mismatch tx f xs) (Telescope g (Product tx f) xs))
-> Telescope g (Product tx f) xs
-> Either (Mismatch tx f xs) (Telescope g (Product tx f) xs)
forall a b. (a -> b) -> a -> b
$ Product tx f x -> Telescope g (Product tx f) (x : xs1)
forall {k} (f :: k -> *) (x :: k) (g :: k -> *) (xs1 :: [k]).
f x -> Telescope g f (x : xs1)
TZ (tx x -> f x -> Product tx f x
forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair tx x
x f x
f x
f)
    go (PCons InjectPolyTx tx x y
_ InPairs (InjectPolyTx tx) (y : zs)
is) (S NS tx xs1
x) (TS g x
g Telescope g f xs1
f) = (Mismatch tx f (y : zs) -> Mismatch tx f xs)
-> (Telescope g (Product tx f) (y : zs)
    -> Telescope g (Product tx f) xs)
-> Either
     (Mismatch tx f (y : zs)) (Telescope g (Product tx f) (y : zs))
-> Either (Mismatch tx f xs) (Telescope g (Product tx f) xs)
forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap Mismatch tx f (y : zs) -> Mismatch tx f xs
Mismatch tx f (y : zs) -> Mismatch tx f (x : y : zs)
forall {k} (f :: k -> *) (g :: k -> *) (xs1 :: [k]) (x :: k).
Mismatch f g xs1 -> Mismatch f g (x : xs1)
MS (g x
-> Telescope g (Product tx f) (y : zs)
-> Telescope g (Product tx f) (x : y : zs)
forall {k} (g :: k -> *) (x :: k) (f :: k -> *) (xs1 :: [k]).
g x -> Telescope g f xs1 -> Telescope g f (x : xs1)
TS g x
g) (Either
   (Mismatch tx f (y : zs)) (Telescope g (Product tx f) (y : zs))
 -> Either (Mismatch tx f xs) (Telescope g (Product tx f) xs))
-> Either
     (Mismatch tx f (y : zs)) (Telescope g (Product tx f) (y : zs))
-> Either (Mismatch tx f xs) (Telescope g (Product tx f) xs)
forall a b. (a -> b) -> a -> b
$ InPairs (InjectPolyTx tx) (y : zs)
-> NS tx (y : zs)
-> Telescope g f (y : zs)
-> Either
     (Mismatch tx f (y : zs)) (Telescope g (Product tx f) (y : zs))
forall (tx :: * -> *) (xs :: [*]) (g :: * -> *) (f :: * -> *).
InPairs (InjectPolyTx tx) xs
-> NS tx xs
-> Telescope g f xs
-> Either (Mismatch tx f xs) (Telescope g (Product tx f) xs)
go InPairs (InjectPolyTx tx) (y : zs)
is NS tx xs1
NS tx (y : zs)
x Telescope g f xs1
Telescope g f (y : zs)
f
    go InPairs (InjectPolyTx tx) xs
_            (S NS tx xs1
x) (TZ f x
f)   = Mismatch tx f xs
-> Either (Mismatch tx f xs) (Telescope g (Product tx f) xs)
forall a b. a -> Either a b
Left (Mismatch tx f xs
 -> Either (Mismatch tx f xs) (Telescope g (Product tx f) xs))
-> Mismatch tx f xs
-> Either (Mismatch tx f xs) (Telescope g (Product tx f) xs)
forall a b. (a -> b) -> a -> b
$ NS tx xs1 -> f x -> Mismatch tx f (x : xs1)
forall {k} (f :: k -> *) (xs1 :: [k]) (g :: k -> *) (x :: k).
NS f xs1 -> g x -> Mismatch f g (x : xs1)
MR NS tx xs1
x f x
f
    go (PCons InjectPolyTx tx x y
i InPairs (InjectPolyTx tx) (y : zs)
is) (Z tx x
x) (TS g x
g Telescope g f xs1
f) =
        case InjectPolyTx tx x y -> tx x -> Maybe (tx y)
forall (tx :: * -> *) blk blk'.
InjectPolyTx tx blk blk' -> tx blk -> Maybe (tx blk')
injectTxWith InjectPolyTx tx x y
i tx x
tx x
x of
          Maybe (tx y)
Nothing -> Mismatch tx f xs
-> Either (Mismatch tx f xs) (Telescope g (Product tx f) xs)
forall a b. a -> Either a b
Left (Mismatch tx f xs
 -> Either (Mismatch tx f xs) (Telescope g (Product tx f) xs))
-> Mismatch tx f xs
-> Either (Mismatch tx f xs) (Telescope g (Product tx f) xs)
forall a b. (a -> b) -> a -> b
$ tx x -> NS f xs1 -> Mismatch tx f (x : xs1)
forall {k} (f :: k -> *) (x :: k) (g :: k -> *) (xs1 :: [k]).
f x -> NS g xs1 -> Mismatch f g (x : xs1)
ML tx x
x (Telescope g f xs1 -> NS f xs1
forall {k} (g :: k -> *) (f :: k -> *) (xs :: [k]).
Telescope g f xs -> NS f xs
Telescope.tip Telescope g f xs1
f)
          Just tx y
x' -> (Mismatch tx f (y : zs) -> Mismatch tx f xs)
-> (Telescope g (Product tx f) (y : zs)
    -> Telescope g (Product tx f) xs)
-> Either
     (Mismatch tx f (y : zs)) (Telescope g (Product tx f) (y : zs))
-> Either (Mismatch tx f xs) (Telescope g (Product tx f) xs)
forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap Mismatch tx f (y : zs) -> Mismatch tx f xs
Mismatch tx f (y : zs) -> Mismatch tx f (x : y : zs)
forall {k} (f :: k -> *) (g :: k -> *) (xs1 :: [k]) (x :: k).
Mismatch f g xs1 -> Mismatch f g (x : xs1)
MS (g x
-> Telescope g (Product tx f) (y : zs)
-> Telescope g (Product tx f) (x : y : zs)
forall {k} (g :: k -> *) (x :: k) (f :: k -> *) (xs1 :: [k]).
g x -> Telescope g f xs1 -> Telescope g f (x : xs1)
TS g x
g) (Either
   (Mismatch tx f (y : zs)) (Telescope g (Product tx f) (y : zs))
 -> Either (Mismatch tx f xs) (Telescope g (Product tx f) xs))
-> Either
     (Mismatch tx f (y : zs)) (Telescope g (Product tx f) (y : zs))
-> Either (Mismatch tx f xs) (Telescope g (Product tx f) xs)
forall a b. (a -> b) -> a -> b
$ InPairs (InjectPolyTx tx) (y : zs)
-> NS tx (y : zs)
-> Telescope g f (y : zs)
-> Either
     (Mismatch tx f (y : zs)) (Telescope g (Product tx f) (y : zs))
forall (tx :: * -> *) (xs :: [*]) (g :: * -> *) (f :: * -> *).
InPairs (InjectPolyTx tx) xs
-> NS tx xs
-> Telescope g f xs
-> Either (Mismatch tx f xs) (Telescope g (Product tx f) xs)
go InPairs (InjectPolyTx tx) (y : zs)
is (tx y -> NS tx (y : zs)
forall {k} (f :: k -> *) (x :: k) (xs1 :: [k]).
f x -> NS f (x : xs1)
Z tx y
x') Telescope g f xs1
Telescope g f (y : zs)
f

matchPolyTx ::
     SListI xs
  => InPairs (InjectPolyTx tx) xs
  -> NS tx xs
  -> HardForkState f xs
  -> Either (Mismatch tx (Current f) xs)
            (HardForkState (Product tx f) xs)
matchPolyTx :: forall (xs :: [*]) (tx :: * -> *) (f :: * -> *).
SListI xs =>
InPairs (InjectPolyTx tx) xs
-> NS tx xs
-> HardForkState f xs
-> Either
     (Mismatch tx (Current f) xs) (HardForkState (Product tx f) xs)
matchPolyTx InPairs (InjectPolyTx tx) xs
is NS tx xs
tx =
      (Telescope (K Past) (Product tx (Current f)) xs
 -> HardForkState (Product tx f) xs)
-> Either
     (Mismatch tx (Current f) xs)
     (Telescope (K Past) (Product tx (Current f)) xs)
-> Either
     (Mismatch tx (Current f) xs) (HardForkState (Product tx f) xs)
forall a b.
(a -> b)
-> Either (Mismatch tx (Current f) xs) a
-> Either (Mismatch tx (Current f) xs) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Telescope (K Past) (Current (Product tx f)) xs
-> HardForkState (Product tx f) xs
forall (f :: * -> *) (xs :: [*]).
Telescope (K Past) (Current f) xs -> HardForkState f xs
HardForkState (Telescope (K Past) (Current (Product tx f)) xs
 -> HardForkState (Product tx f) xs)
-> (Telescope (K Past) (Product tx (Current f)) xs
    -> Telescope (K Past) (Current (Product tx f)) xs)
-> Telescope (K Past) (Product tx (Current f)) xs
-> HardForkState (Product tx f) xs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. Product tx (Current f) a -> Current (Product tx f) a)
-> Telescope (K Past) (Product tx (Current f)) xs
-> Telescope (K Past) (Current (Product tx 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 Product tx (Current f) a -> Current (Product tx f) a
forall a. Product tx (Current f) a -> Current (Product tx f) a
forall (tx :: * -> *) (f :: * -> *) blk.
Product tx (Current f) blk -> Current (Product tx f) blk
distrib)
    (Either
   (Mismatch tx (Current f) xs)
   (Telescope (K Past) (Product tx (Current f)) xs)
 -> Either
      (Mismatch tx (Current f) xs) (HardForkState (Product tx f) xs))
-> (HardForkState f xs
    -> Either
         (Mismatch tx (Current f) xs)
         (Telescope (K Past) (Product tx (Current f)) xs))
-> HardForkState f xs
-> Either
     (Mismatch tx (Current f) xs) (HardForkState (Product tx f) xs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InPairs (InjectPolyTx tx) xs
-> NS tx xs
-> Telescope (K Past) (Current f) xs
-> Either
     (Mismatch tx (Current f) xs)
     (Telescope (K Past) (Product tx (Current f)) xs)
forall (tx :: * -> *) (xs :: [*]) (g :: * -> *) (f :: * -> *).
InPairs (InjectPolyTx tx) xs
-> NS tx xs
-> Telescope g f xs
-> Either (Mismatch tx f xs) (Telescope g (Product tx f) xs)
matchPolyTx' InPairs (InjectPolyTx tx) xs
is NS tx xs
tx
    (Telescope (K Past) (Current f) xs
 -> Either
      (Mismatch tx (Current f) xs)
      (Telescope (K Past) (Product tx (Current f)) xs))
-> (HardForkState f xs -> Telescope (K Past) (Current f) xs)
-> HardForkState f xs
-> Either
     (Mismatch tx (Current f) xs)
     (Telescope (K Past) (Product tx (Current f)) xs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HardForkState f xs -> Telescope (K Past) (Current f) xs
forall (f :: * -> *) (xs :: [*]).
HardForkState f xs -> Telescope (K Past) (Current f) xs
getHardForkState
  where
    distrib :: Product tx (Current f) blk -> Current (Product tx f) blk
    distrib :: forall (tx :: * -> *) (f :: * -> *) blk.
Product tx (Current f) blk -> Current (Product tx f) blk
distrib (Pair tx blk
tx' Current{f blk
Bound
currentStart :: Bound
currentState :: f blk
currentStart :: forall (f :: * -> *) blk. Current f blk -> Bound
currentState :: forall (f :: * -> *) blk. Current f blk -> f blk
..}) = Current {
          currentStart :: Bound
currentStart = Bound
currentStart
        , currentState :: Product tx f blk
currentState = tx blk -> f blk -> Product tx f blk
forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair tx blk
tx' f blk
currentState
        }

-- | Match transaction with an 'NS', attempting to inject where possible
matchPolyTxNS ::
     InPairs (InjectPolyTx tx) xs
  -> NS tx xs
  -> NS f xs
  -> Either (Mismatch tx f xs)
            (NS (Product tx f) xs)
matchPolyTxNS :: forall (tx :: * -> *) (xs :: [*]) (f :: * -> *).
InPairs (InjectPolyTx tx) xs
-> NS tx xs
-> NS f xs
-> Either (Mismatch tx f xs) (NS (Product tx f) xs)
matchPolyTxNS = InPairs (InjectPolyTx tx) xs
-> NS tx xs
-> NS f xs
-> Either (Mismatch tx f xs) (NS (Product tx f) xs)
forall (tx :: * -> *) (xs :: [*]) (f :: * -> *).
InPairs (InjectPolyTx tx) xs
-> NS tx xs
-> NS f xs
-> Either (Mismatch tx f xs) (NS (Product tx f) xs)
go
  where
    go :: InPairs (InjectPolyTx tx) xs
       -> NS tx xs
       -> NS f xs
       -> Either (Mismatch tx f xs)
                 (NS (Product tx f) xs)
    go :: forall (tx :: * -> *) (xs :: [*]) (f :: * -> *).
InPairs (InjectPolyTx tx) xs
-> NS tx xs
-> NS f xs
-> Either (Mismatch tx f xs) (NS (Product tx f) xs)
go InPairs (InjectPolyTx tx) xs
_            (Z tx x
x) (Z f x
f) = NS (Product tx f) xs
-> Either (Mismatch tx f xs) (NS (Product tx f) xs)
forall a b. b -> Either a b
Right (NS (Product tx f) xs
 -> Either (Mismatch tx f xs) (NS (Product tx f) xs))
-> NS (Product tx f) xs
-> Either (Mismatch tx f xs) (NS (Product tx f) xs)
forall a b. (a -> b) -> a -> b
$ Product tx f x -> NS (Product tx f) (x : xs1)
forall {k} (f :: k -> *) (x :: k) (xs1 :: [k]).
f x -> NS f (x : xs1)
Z (tx x -> f x -> Product tx f x
forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair tx x
x f x
f x
f)
    go (PCons InjectPolyTx tx x y
_ InPairs (InjectPolyTx tx) (y : zs)
is) (S NS tx xs1
x) (S NS f xs1
f) = (Mismatch tx f (y : zs) -> Mismatch tx f xs)
-> (NS (Product tx f) (y : zs) -> NS (Product tx f) xs)
-> Either (Mismatch tx f (y : zs)) (NS (Product tx f) (y : zs))
-> Either (Mismatch tx f xs) (NS (Product tx f) xs)
forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap Mismatch tx f (y : zs) -> Mismatch tx f xs
Mismatch tx f (y : zs) -> Mismatch tx f (x : y : zs)
forall {k} (f :: k -> *) (g :: k -> *) (xs1 :: [k]) (x :: k).
Mismatch f g xs1 -> Mismatch f g (x : xs1)
MS NS (Product tx f) (y : zs) -> NS (Product tx f) xs
NS (Product tx f) (y : zs) -> NS (Product tx f) (x : y : zs)
forall {k} (f :: k -> *) (xs1 :: [k]) (x :: k).
NS f xs1 -> NS f (x : xs1)
S (Either (Mismatch tx f (y : zs)) (NS (Product tx f) (y : zs))
 -> Either (Mismatch tx f xs) (NS (Product tx f) xs))
-> Either (Mismatch tx f (y : zs)) (NS (Product tx f) (y : zs))
-> Either (Mismatch tx f xs) (NS (Product tx f) xs)
forall a b. (a -> b) -> a -> b
$ InPairs (InjectPolyTx tx) (y : zs)
-> NS tx (y : zs)
-> NS f (y : zs)
-> Either (Mismatch tx f (y : zs)) (NS (Product tx f) (y : zs))
forall (tx :: * -> *) (xs :: [*]) (f :: * -> *).
InPairs (InjectPolyTx tx) xs
-> NS tx xs
-> NS f xs
-> Either (Mismatch tx f xs) (NS (Product tx f) xs)
go InPairs (InjectPolyTx tx) (y : zs)
is NS tx xs1
NS tx (y : zs)
x NS f xs1
NS f (y : zs)
f
    go InPairs (InjectPolyTx tx) xs
_            (S NS tx xs1
x) (Z f x
f) = Mismatch tx f xs
-> Either (Mismatch tx f xs) (NS (Product tx f) xs)
forall a b. a -> Either a b
Left (Mismatch tx f xs
 -> Either (Mismatch tx f xs) (NS (Product tx f) xs))
-> Mismatch tx f xs
-> Either (Mismatch tx f xs) (NS (Product tx f) xs)
forall a b. (a -> b) -> a -> b
$ NS tx xs1 -> f x -> Mismatch tx f (x : xs1)
forall {k} (f :: k -> *) (xs1 :: [k]) (g :: k -> *) (x :: k).
NS f xs1 -> g x -> Mismatch f g (x : xs1)
MR NS tx xs1
x f x
f
    go (PCons InjectPolyTx tx x y
i InPairs (InjectPolyTx tx) (y : zs)
is) (Z tx x
x) (S NS f xs1
f) =
        case InjectPolyTx tx x y -> tx x -> Maybe (tx y)
forall (tx :: * -> *) blk blk'.
InjectPolyTx tx blk blk' -> tx blk -> Maybe (tx blk')
injectTxWith InjectPolyTx tx x y
i tx x
tx x
x of
          Maybe (tx y)
Nothing -> Mismatch tx f xs
-> Either (Mismatch tx f xs) (NS (Product tx f) xs)
forall a b. a -> Either a b
Left (Mismatch tx f xs
 -> Either (Mismatch tx f xs) (NS (Product tx f) xs))
-> Mismatch tx f xs
-> Either (Mismatch tx f xs) (NS (Product tx f) xs)
forall a b. (a -> b) -> a -> b
$ tx x -> NS f xs1 -> Mismatch tx f (x : xs1)
forall {k} (f :: k -> *) (x :: k) (g :: k -> *) (xs1 :: [k]).
f x -> NS g xs1 -> Mismatch f g (x : xs1)
ML tx x
x NS f xs1
f
          Just tx y
x' -> (Mismatch tx f (y : zs) -> Mismatch tx f xs)
-> (NS (Product tx f) (y : zs) -> NS (Product tx f) xs)
-> Either (Mismatch tx f (y : zs)) (NS (Product tx f) (y : zs))
-> Either (Mismatch tx f xs) (NS (Product tx f) xs)
forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap Mismatch tx f (y : zs) -> Mismatch tx f xs
Mismatch tx f (y : zs) -> Mismatch tx f (x : y : zs)
forall {k} (f :: k -> *) (g :: k -> *) (xs1 :: [k]) (x :: k).
Mismatch f g xs1 -> Mismatch f g (x : xs1)
MS NS (Product tx f) (y : zs) -> NS (Product tx f) xs
NS (Product tx f) (y : zs) -> NS (Product tx f) (x : y : zs)
forall {k} (f :: k -> *) (xs1 :: [k]) (x :: k).
NS f xs1 -> NS f (x : xs1)
S (Either (Mismatch tx f (y : zs)) (NS (Product tx f) (y : zs))
 -> Either (Mismatch tx f xs) (NS (Product tx f) xs))
-> Either (Mismatch tx f (y : zs)) (NS (Product tx f) (y : zs))
-> Either (Mismatch tx f xs) (NS (Product tx f) xs)
forall a b. (a -> b) -> a -> b
$ InPairs (InjectPolyTx tx) (y : zs)
-> NS tx (y : zs)
-> NS f (y : zs)
-> Either (Mismatch tx f (y : zs)) (NS (Product tx f) (y : zs))
forall (tx :: * -> *) (xs :: [*]) (f :: * -> *).
InPairs (InjectPolyTx tx) xs
-> NS tx xs
-> NS f xs
-> Either (Mismatch tx f xs) (NS (Product tx f) xs)
go InPairs (InjectPolyTx tx) (y : zs)
is (tx y -> NS tx (y : zs)
forall {k} (f :: k -> *) (x :: k) (xs1 :: [k]).
f x -> NS f (x : xs1)
Z tx y
x') NS f xs1
NS f (y : zs)
f

-- | Match a list of transactions with an 'NS', attempting to inject where
-- possible
matchPolyTxsNS ::
     forall tx f xs. SListI xs
  => InPairs (InjectPolyTx tx) xs
  -> NS f xs
  -> [NS tx xs]
  -> ([Mismatch tx f xs], NS (Product f ([] :.: tx)) xs)
matchPolyTxsNS :: forall (tx :: * -> *) (f :: * -> *) (xs :: [*]).
SListI xs =>
InPairs (InjectPolyTx tx) xs
-> NS f xs
-> [NS tx xs]
-> ([Mismatch tx f xs], NS (Product f ([] :.: tx)) xs)
matchPolyTxsNS InPairs (InjectPolyTx tx) xs
is NS f xs
ns = [NS tx xs] -> ([Mismatch tx f xs], NS (Product f ([] :.: tx)) xs)
go
  where
    go :: [NS tx xs]
       -> ([Mismatch tx f xs], NS (Product f ([] :.: tx)) xs)
    go :: [NS tx xs] -> ([Mismatch tx f xs], NS (Product f ([] :.: tx)) xs)
go []       = ([], (forall a. f a -> Product f ([] :.: tx) a)
-> NS f xs -> NS (Product f ([] :.: tx)) 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 (f a -> (:.:) [] tx a -> Product f ([] :.: tx) a
forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
`Pair` [tx a] -> (:.:) [] tx a
forall l k (f :: l -> *) (g :: k -> l) (p :: k).
f (g p) -> (:.:) f g p
Comp []) NS f xs
ns)
    go (NS tx xs
tx:[NS tx xs]
txs) =
      let ([Mismatch tx f xs]
mismatched, NS (Product f ([] :.: tx)) xs
matched) = [NS tx xs] -> ([Mismatch tx f xs], NS (Product f ([] :.: tx)) xs)
go [NS tx xs]
txs
      in case InPairs (InjectPolyTx tx) xs
-> NS tx xs
-> NS (Product f ([] :.: tx)) xs
-> Either
     (Mismatch tx (Product f ([] :.: tx)) xs)
     (NS (Product tx (Product f ([] :.: tx))) xs)
forall (tx :: * -> *) (xs :: [*]) (f :: * -> *).
InPairs (InjectPolyTx tx) xs
-> NS tx xs
-> NS f xs
-> Either (Mismatch tx f xs) (NS (Product tx f) xs)
matchPolyTxNS InPairs (InjectPolyTx tx) xs
is NS tx xs
tx NS (Product f ([] :.: tx)) xs
matched of
           Left  Mismatch tx (Product f ([] :.: tx)) xs
err      -> ((forall a. Product f ([] :.: tx) a -> f a)
-> Mismatch tx (Product f ([] :.: tx)) xs -> Mismatch tx 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 Product f ([] :.: tx) a -> f a
forall a. Product f ([] :.: tx) a -> f a
forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
Product f g a -> f a
pairFst Mismatch tx (Product f ([] :.: tx)) xs
err Mismatch tx f xs -> [Mismatch tx f xs] -> [Mismatch tx f xs]
forall a. a -> [a] -> [a]
: [Mismatch tx f xs]
mismatched, NS (Product f ([] :.: tx)) xs
matched)
           Right NS (Product tx (Product f ([] :.: tx))) xs
matched' -> ([Mismatch tx f xs]
mismatched, NS (Product tx (Product f ([] :.: tx))) xs
-> NS (Product f ([] :.: tx)) xs
insert NS (Product tx (Product f ([] :.: tx))) xs
matched')

    insert :: NS (Product tx (Product f ([] :.: tx))) xs
           -> NS (Product f ([] :.: tx)) xs
    insert :: NS (Product tx (Product f ([] :.: tx))) xs
-> NS (Product f ([] :.: tx)) xs
insert = (forall a.
 Product tx (Product f ([] :.: tx)) a -> Product f ([] :.: tx) a)
-> NS (Product tx (Product f ([] :.: tx))) xs
-> NS (Product f ([] :.: tx)) 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.
  Product tx (Product f ([] :.: tx)) a -> Product f ([] :.: tx) a)
 -> NS (Product tx (Product f ([] :.: tx))) xs
 -> NS (Product f ([] :.: tx)) xs)
-> (forall a.
    Product tx (Product f ([] :.: tx)) a -> Product f ([] :.: tx) a)
-> NS (Product tx (Product f ([] :.: tx))) xs
-> NS (Product f ([] :.: tx)) xs
forall a b. (a -> b) -> a -> b
$ \(Pair tx a
tx (Pair f a
f (Comp [tx a]
txs))) -> f a -> (:.:) [] tx a -> Product f ([] :.: tx) a
forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair f a
f ([tx a] -> (:.:) [] tx a
forall l k (f :: l -> *) (g :: k -> l) (p :: k).
f (g p) -> (:.:) f g p
Comp (tx a
txtx a -> [tx a] -> [tx a]
forall a. a -> [a] -> [a]
:[tx a]
txs))

{-------------------------------------------------------------------------------
  Monomorphic aliases
-------------------------------------------------------------------------------}

type InjectTx = InjectPolyTx GenTx

-- | 'InjectPolyTx' at type 'InjectTx'
pattern InjectTx :: (GenTx blk -> Maybe (GenTx blk')) -> InjectTx blk blk'
pattern $mInjectTx :: forall {r} {blk} {blk'}.
InjectTx blk blk'
-> ((GenTx blk -> Maybe (GenTx blk')) -> r) -> ((# #) -> r) -> r
$bInjectTx :: forall blk blk'.
(GenTx blk -> Maybe (GenTx blk')) -> InjectTx blk blk'
InjectTx f = InjectPolyTx f

-- | 'cannotInjectPolyTx' at type 'InjectTx'
cannotInjectTx :: InjectTx blk blk'
cannotInjectTx :: forall blk blk'. InjectTx blk blk'
cannotInjectTx = InjectPolyTx GenTx blk blk'
forall (tx :: * -> *) blk blk'. InjectPolyTx tx blk blk'
cannotInjectPolyTx

-- | 'matchPolyTx' at type 'InjectTx'
matchTx ::
     SListI xs
  => InPairs InjectTx xs
  -> NS GenTx xs
  -> HardForkState f xs
  -> Either (Mismatch GenTx (Current f) xs)
            (HardForkState (Product GenTx f) xs)
matchTx :: forall (xs :: [*]) (f :: * -> *).
SListI xs =>
InPairs InjectTx xs
-> NS GenTx xs
-> HardForkState f xs
-> Either
     (Mismatch GenTx (Current f) xs)
     (HardForkState (Product GenTx f) xs)
matchTx = InPairs InjectTx xs
-> NS GenTx xs
-> HardForkState f xs
-> Either
     (Mismatch GenTx (Current f) xs)
     (HardForkState (Product GenTx f) xs)
forall (xs :: [*]) (tx :: * -> *) (f :: * -> *).
SListI xs =>
InPairs (InjectPolyTx tx) xs
-> NS tx xs
-> HardForkState f xs
-> Either
     (Mismatch tx (Current f) xs) (HardForkState (Product tx f) xs)
matchPolyTx

-----

type InjectValidatedTx = InjectPolyTx WrapValidatedGenTx

-- | 'InjectPolyTx' at type 'InjectValidatedTx'
pattern InjectValidatedTx ::
     (WrapValidatedGenTx blk -> Maybe (WrapValidatedGenTx blk'))
  -> InjectValidatedTx blk blk'
pattern $mInjectValidatedTx :: forall {r} {blk} {blk'}.
InjectValidatedTx blk blk'
-> ((WrapValidatedGenTx blk -> Maybe (WrapValidatedGenTx blk'))
    -> r)
-> ((# #) -> r)
-> r
$bInjectValidatedTx :: forall blk blk'.
(WrapValidatedGenTx blk -> Maybe (WrapValidatedGenTx blk'))
-> InjectValidatedTx blk blk'
InjectValidatedTx f = InjectPolyTx f

-- | 'cannotInjectPolyTx' at type 'InjectValidatedTx'
cannotInjectValidatedTx :: InjectValidatedTx blk blk'
cannotInjectValidatedTx :: forall blk blk'. InjectValidatedTx blk blk'
cannotInjectValidatedTx = InjectPolyTx WrapValidatedGenTx blk blk'
forall (tx :: * -> *) blk blk'. InjectPolyTx tx blk blk'
cannotInjectPolyTx

-- | 'matchPolyTx' at type 'InjectValidatedTx'
matchValidatedTx ::
     SListI xs
  => InPairs InjectValidatedTx xs
  -> NS WrapValidatedGenTx xs
  -> HardForkState f xs
  -> Either (Mismatch WrapValidatedGenTx (Current f) xs)
            (HardForkState (Product WrapValidatedGenTx f) xs)
matchValidatedTx :: forall (xs :: [*]) (f :: * -> *).
SListI xs =>
InPairs InjectValidatedTx xs
-> NS WrapValidatedGenTx xs
-> HardForkState f xs
-> Either
     (Mismatch WrapValidatedGenTx (Current f) xs)
     (HardForkState (Product WrapValidatedGenTx f) xs)
matchValidatedTx = InPairs InjectValidatedTx xs
-> NS WrapValidatedGenTx xs
-> HardForkState f xs
-> Either
     (Mismatch WrapValidatedGenTx (Current f) xs)
     (HardForkState (Product WrapValidatedGenTx f) xs)
forall (xs :: [*]) (tx :: * -> *) (f :: * -> *).
SListI xs =>
InPairs (InjectPolyTx tx) xs
-> NS tx xs
-> HardForkState f xs
-> Either
     (Mismatch tx (Current f) xs) (HardForkState (Product tx f) xs)
matchPolyTx

-- | 'matchPolyTxsNS' at type 'InjectValidatedTx'
matchValidatedTxsNS ::
     forall f xs. SListI xs
  => InPairs InjectValidatedTx xs
  -> NS f xs
  -> [NS WrapValidatedGenTx xs]
  -> ([Mismatch WrapValidatedGenTx f xs], NS (Product f ([] :.: WrapValidatedGenTx)) xs)
matchValidatedTxsNS :: forall (f :: * -> *) (xs :: [*]).
SListI xs =>
InPairs InjectValidatedTx xs
-> NS f xs
-> [NS WrapValidatedGenTx xs]
-> ([Mismatch WrapValidatedGenTx f xs],
    NS (Product f ([] :.: WrapValidatedGenTx)) xs)
matchValidatedTxsNS = InPairs InjectValidatedTx xs
-> NS f xs
-> [NS WrapValidatedGenTx xs]
-> ([Mismatch WrapValidatedGenTx f xs],
    NS (Product f ([] :.: WrapValidatedGenTx)) xs)
forall (tx :: * -> *) (f :: * -> *) (xs :: [*]).
SListI xs =>
InPairs (InjectPolyTx tx) xs
-> NS f xs
-> [NS tx xs]
-> ([Mismatch tx f xs], NS (Product f ([] :.: tx)) xs)
matchPolyTxsNS