{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Ouroboros.Consensus.HardFork.Combinator.InjectTxs (
InjectPolyTx (..)
, cannotInjectPolyTx
, matchPolyTx
, matchPolyTxsNS
, InjectTx
, cannotInjectTx
, matchTx
, pattern InjectTx
, InjectValidatedTx
, cannotInjectValidatedTx
, matchValidatedTx
, matchValidatedTxsNS
, pattern InjectValidatedTx
) where
import Data.Bifunctor
import Data.Functor.Product
import Data.SOP.Strict
import Ouroboros.Consensus.HardFork.Combinator.State.Types
import Ouroboros.Consensus.HardFork.Combinator.Util.InPairs
(InPairs (..))
import Ouroboros.Consensus.HardFork.Combinator.Util.Match
import Ouroboros.Consensus.HardFork.Combinator.Util.Telescope
(Telescope (..))
import qualified Ouroboros.Consensus.HardFork.Combinator.Util.Telescope as Telescope
import Ouroboros.Consensus.Ledger.SupportsMempool
import Ouroboros.Consensus.TypeFamilyWrappers
import Ouroboros.Consensus.Util (pairFst)
data InjectPolyTx tx blk blk' = InjectPolyTx {
InjectPolyTx tx blk blk' -> tx blk -> Maybe (tx blk')
injectTxWith :: tx blk -> Maybe (tx blk')
}
cannotInjectPolyTx :: InjectPolyTx tx blk blk'
cannotInjectPolyTx :: 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
matchPolyTx' ::
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)
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 :: 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) (x : xs)
-> Either (Mismatch tx f xs) (Telescope g (Product tx f) (x : xs))
forall a b. b -> Either a b
Right (Telescope g (Product tx f) (x : xs)
-> Either (Mismatch tx f xs) (Telescope g (Product tx f) (x : xs)))
-> Telescope g (Product tx f) (x : xs)
-> Either (Mismatch tx f xs) (Telescope g (Product tx f) (x : xs))
forall a b. (a -> b) -> a -> b
$ Product tx f x -> Telescope g (Product tx f) (x : xs)
forall a (f :: a -> *) (x :: a) (g :: a -> *) (xs :: [a]).
f x -> Telescope g f (x : xs)
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 xs
x) (TS g x
g Telescope g f xs
f) = (Mismatch tx f (y : zs) -> Mismatch tx f (x : y : zs))
-> (Telescope g (Product tx f) (y : zs)
-> Telescope g (Product tx f) (x : y : zs))
-> Either
(Mismatch tx f (y : zs)) (Telescope g (Product tx f) (y : zs))
-> Either
(Mismatch tx f (x : y : zs))
(Telescope g (Product tx f) (x : y : zs))
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 (x : y : zs)
forall a (f :: a -> *) (g :: a -> *) (xs :: [a]) (x :: a).
Mismatch f g xs -> Mismatch f g (x : xs)
MS (g x
-> Telescope g (Product tx f) (y : zs)
-> Telescope g (Product tx f) (x : y : zs)
forall a (g :: a -> *) (x :: a) (f :: a -> *) (xs :: [a]).
g x -> Telescope g f xs -> Telescope g f (x : xs)
TS g x
g) (Either
(Mismatch tx f (y : zs)) (Telescope g (Product tx f) (y : zs))
-> Either
(Mismatch tx f (x : y : zs))
(Telescope g (Product tx f) (x : y : zs)))
-> Either
(Mismatch tx f (y : zs)) (Telescope g (Product tx f) (y : zs))
-> Either
(Mismatch tx f (x : y : zs))
(Telescope g (Product tx f) (x : y : zs))
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 xs
NS tx (y : zs)
x Telescope g f xs
Telescope g f (y : zs)
f
go InPairs (InjectPolyTx tx) xs
_ (S NS tx xs
x) (TZ f x
f) = Mismatch tx f (x : xs)
-> Either (Mismatch tx f (x : xs)) (Telescope g (Product tx f) xs)
forall a b. a -> Either a b
Left (Mismatch tx f (x : xs)
-> Either (Mismatch tx f (x : xs)) (Telescope g (Product tx f) xs))
-> Mismatch tx f (x : xs)
-> Either (Mismatch tx f (x : xs)) (Telescope g (Product tx f) xs)
forall a b. (a -> b) -> a -> b
$ NS tx xs -> f x -> Mismatch tx f (x : xs)
forall a (f :: a -> *) (xs :: [a]) (g :: a -> *) (x :: a).
NS f xs -> g x -> Mismatch f g (x : xs)
MR NS tx xs
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 xs
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 (x : xs)
-> Either (Mismatch tx f (x : xs)) (Telescope g (Product tx f) xs)
forall a b. a -> Either a b
Left (Mismatch tx f (x : xs)
-> Either (Mismatch tx f (x : xs)) (Telescope g (Product tx f) xs))
-> Mismatch tx f (x : xs)
-> Either (Mismatch tx f (x : xs)) (Telescope g (Product tx f) xs)
forall a b. (a -> b) -> a -> b
$ tx x -> NS f xs -> Mismatch tx f (x : xs)
forall a (f :: a -> *) (x :: a) (g :: a -> *) (xs :: [a]).
f x -> NS g xs -> Mismatch f g (x : xs)
ML tx x
x (Telescope g f xs -> NS f xs
forall k (g :: k -> *) (f :: k -> *) (xs :: [k]).
Telescope g f xs -> NS f xs
Telescope.tip Telescope g f xs
f)
Just tx y
x' -> (Mismatch tx f (y : zs) -> Mismatch tx f (x : y : zs))
-> (Telescope g (Product tx f) (y : zs)
-> Telescope g (Product tx f) (x : y : zs))
-> Either
(Mismatch tx f (y : zs)) (Telescope g (Product tx f) (y : zs))
-> Either
(Mismatch tx f (x : y : zs))
(Telescope g (Product tx f) (x : y : zs))
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 (x : y : zs)
forall a (f :: a -> *) (g :: a -> *) (xs :: [a]) (x :: a).
Mismatch f g xs -> Mismatch f g (x : xs)
MS (g x
-> Telescope g (Product tx f) (y : zs)
-> Telescope g (Product tx f) (x : y : zs)
forall a (g :: a -> *) (x :: a) (f :: a -> *) (xs :: [a]).
g x -> Telescope g f xs -> Telescope g f (x : xs)
TS g x
g) (Either
(Mismatch tx f (y : zs)) (Telescope g (Product tx f) (y : zs))
-> Either
(Mismatch tx f (x : y : zs))
(Telescope g (Product tx f) (x : y : zs)))
-> Either
(Mismatch tx f (y : zs)) (Telescope g (Product tx f) (y : zs))
-> Either
(Mismatch tx f (x : y : zs))
(Telescope g (Product tx f) (x : y : zs))
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 a (f :: a -> *) (x :: a) (xs :: [a]). f x -> NS f (x : xs)
Z tx y
x') Telescope g f xs
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 :: 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 (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 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 :: Product tx (Current f) blk -> Current (Product tx f) blk
distrib (Pair tx blk
tx' Current{f blk
Bound
currentState :: forall (f :: * -> *) blk. Current f blk -> f blk
currentStart :: forall (f :: * -> *) blk. Current f blk -> Bound
currentState :: f blk
currentStart :: Bound
..}) = Current :: forall (f :: * -> *) blk. Bound -> f blk -> Current 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
}
matchPolyTxNS ::
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)
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 :: 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) (x : xs)
-> Either (Mismatch tx f xs) (NS (Product tx f) (x : xs))
forall a b. b -> Either a b
Right (NS (Product tx f) (x : xs)
-> Either (Mismatch tx f xs) (NS (Product tx f) (x : xs)))
-> NS (Product tx f) (x : xs)
-> Either (Mismatch tx f xs) (NS (Product tx f) (x : xs))
forall a b. (a -> b) -> a -> b
$ Product tx f x -> NS (Product tx f) (x : xs)
forall a (f :: a -> *) (x :: a) (xs :: [a]). f x -> NS f (x : xs)
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 xs
x) (S NS f xs
f) = (Mismatch tx f (y : zs) -> Mismatch tx f (x : y : zs))
-> (NS (Product tx f) (y : zs) -> NS (Product tx f) (x : y : zs))
-> Either (Mismatch tx f (y : zs)) (NS (Product tx f) (y : zs))
-> Either
(Mismatch tx f (x : y : zs)) (NS (Product tx f) (x : y : zs))
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 (x : y : zs)
forall a (f :: a -> *) (g :: a -> *) (xs :: [a]) (x :: a).
Mismatch f g xs -> Mismatch f g (x : xs)
MS NS (Product tx f) (y : zs) -> NS (Product tx f) (x : y : zs)
forall a (f :: a -> *) (xs :: [a]) (x :: a).
NS f xs -> NS f (x : xs)
S (Either (Mismatch tx f (y : zs)) (NS (Product tx f) (y : zs))
-> Either
(Mismatch tx f (x : y : zs)) (NS (Product tx f) (x : y : zs)))
-> Either (Mismatch tx f (y : zs)) (NS (Product tx f) (y : zs))
-> Either
(Mismatch tx f (x : y : zs)) (NS (Product tx f) (x : y : zs))
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 xs
NS tx (y : zs)
x NS f xs
NS f (y : zs)
f
go InPairs (InjectPolyTx tx) xs
_ (S NS tx xs
x) (Z f x
f) = Mismatch tx f (x : xs)
-> Either (Mismatch tx f (x : xs)) (NS (Product tx f) xs)
forall a b. a -> Either a b
Left (Mismatch tx f (x : xs)
-> Either (Mismatch tx f (x : xs)) (NS (Product tx f) xs))
-> Mismatch tx f (x : xs)
-> Either (Mismatch tx f (x : xs)) (NS (Product tx f) xs)
forall a b. (a -> b) -> a -> b
$ NS tx xs -> f x -> Mismatch tx f (x : xs)
forall a (f :: a -> *) (xs :: [a]) (g :: a -> *) (x :: a).
NS f xs -> g x -> Mismatch f g (x : xs)
MR NS tx xs
x f x
f
go (PCons InjectPolyTx tx x y
i InPairs (InjectPolyTx tx) (y : zs)
is) (Z tx x
x) (S NS f xs
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 (x : xs)
-> Either (Mismatch tx f (x : xs)) (NS (Product tx f) xs)
forall a b. a -> Either a b
Left (Mismatch tx f (x : xs)
-> Either (Mismatch tx f (x : xs)) (NS (Product tx f) xs))
-> Mismatch tx f (x : xs)
-> Either (Mismatch tx f (x : xs)) (NS (Product tx f) xs)
forall a b. (a -> b) -> a -> b
$ tx x -> NS f xs -> Mismatch tx f (x : xs)
forall a (f :: a -> *) (x :: a) (g :: a -> *) (xs :: [a]).
f x -> NS g xs -> Mismatch f g (x : xs)
ML tx x
x NS f xs
f
Just tx y
x' -> (Mismatch tx f (y : zs) -> Mismatch tx f (x : y : zs))
-> (NS (Product tx f) (y : zs) -> NS (Product tx f) (x : y : zs))
-> Either (Mismatch tx f (y : zs)) (NS (Product tx f) (y : zs))
-> Either
(Mismatch tx f (x : y : zs)) (NS (Product tx f) (x : y : zs))
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 (x : y : zs)
forall a (f :: a -> *) (g :: a -> *) (xs :: [a]) (x :: a).
Mismatch f g xs -> Mismatch f g (x : xs)
MS NS (Product tx f) (y : zs) -> NS (Product tx f) (x : y : zs)
forall a (f :: a -> *) (xs :: [a]) (x :: a).
NS f xs -> NS f (x : xs)
S (Either (Mismatch tx f (y : zs)) (NS (Product tx f) (y : zs))
-> Either
(Mismatch tx f (x : y : zs)) (NS (Product tx f) (x : y : zs)))
-> Either (Mismatch tx f (y : zs)) (NS (Product tx f) (y : zs))
-> Either
(Mismatch tx f (x : y : zs)) (NS (Product tx f) (x : y : zs))
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 a (f :: a -> *) (x :: a) (xs :: [a]). f x -> NS f (x : xs)
Z tx y
x') NS f xs
NS f (y : zs)
f
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
-> 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 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 (Pair f (Comp 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))
type InjectTx = InjectPolyTx GenTx
pattern InjectTx :: (GenTx blk -> Maybe (GenTx blk')) -> InjectTx blk blk'
pattern $bInjectTx :: (GenTx blk -> Maybe (GenTx blk')) -> InjectTx blk blk'
$mInjectTx :: forall r blk blk'.
InjectTx blk blk'
-> ((GenTx blk -> Maybe (GenTx blk')) -> r) -> (Void# -> r) -> r
InjectTx f = InjectPolyTx f
cannotInjectTx :: InjectTx blk blk'
cannotInjectTx :: InjectTx blk blk'
cannotInjectTx = InjectTx blk blk'
forall (tx :: * -> *) blk blk'. InjectPolyTx tx blk blk'
cannotInjectPolyTx
matchTx ::
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)
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
pattern InjectValidatedTx ::
(WrapValidatedGenTx blk -> Maybe (WrapValidatedGenTx blk'))
-> InjectValidatedTx blk blk'
pattern $bInjectValidatedTx :: (WrapValidatedGenTx blk -> Maybe (WrapValidatedGenTx blk'))
-> InjectValidatedTx blk blk'
$mInjectValidatedTx :: forall r blk blk'.
InjectValidatedTx blk blk'
-> ((WrapValidatedGenTx blk -> Maybe (WrapValidatedGenTx blk'))
-> r)
-> (Void# -> r)
-> r
InjectValidatedTx f = InjectPolyTx f
cannotInjectValidatedTx :: InjectValidatedTx blk blk'
cannotInjectValidatedTx :: InjectValidatedTx blk blk'
cannotInjectValidatedTx = InjectValidatedTx blk blk'
forall (tx :: * -> *) blk blk'. InjectPolyTx tx blk blk'
cannotInjectPolyTx
matchValidatedTx ::
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)
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
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)
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