{-# LANGUAGE EmptyCase        #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs            #-}
{-# LANGUAGE RecordWildCards  #-}

module Ouroboros.Consensus.HardFork.Combinator.InjectTxs (
    InjectTx(..)
  , cannotInjectTx
  , matchTx
  ) 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

{-------------------------------------------------------------------------------
  Match a transaction with a ledger
-------------------------------------------------------------------------------}

data InjectTx blk blk' = InjectTx {
      InjectTx blk blk' -> GenTx blk -> Maybe (GenTx blk')
injectTxWith :: GenTx blk  -> Maybe (GenTx blk')
    }

cannotInjectTx :: InjectTx blk blk'
cannotInjectTx :: InjectTx blk blk'
cannotInjectTx = (GenTx blk -> Maybe (GenTx blk')) -> InjectTx blk blk'
forall blk blk'.
(GenTx blk -> Maybe (GenTx blk')) -> InjectTx blk blk'
InjectTx ((GenTx blk -> Maybe (GenTx blk')) -> InjectTx blk blk')
-> (GenTx blk -> Maybe (GenTx blk')) -> InjectTx blk blk'
forall a b. (a -> b) -> a -> b
$ Maybe (GenTx blk') -> GenTx blk -> Maybe (GenTx blk')
forall a b. a -> b -> a
const Maybe (GenTx blk')
forall a. Maybe a
Nothing

-- | Match transaction with a ledger, attempting to inject where possible
matchTx' ::
     InPairs InjectTx xs
  -> NS GenTx xs
  -> Telescope g f xs
  -> Either (Mismatch GenTx f xs)
            (Telescope g (Product GenTx f) xs)
matchTx' :: InPairs InjectTx xs
-> NS GenTx xs
-> Telescope g f xs
-> Either (Mismatch GenTx f xs) (Telescope g (Product GenTx f) xs)
matchTx' = InPairs InjectTx xs
-> NS GenTx xs
-> Telescope g f xs
-> Either (Mismatch GenTx f xs) (Telescope g (Product GenTx f) xs)
forall (xs :: [*]) (g :: * -> *) (f :: * -> *).
InPairs InjectTx xs
-> NS GenTx xs
-> Telescope g f xs
-> Either (Mismatch GenTx f xs) (Telescope g (Product GenTx f) xs)
go
  where
    go :: InPairs InjectTx xs
       -> NS GenTx xs
       -> Telescope g f xs
       -> Either (Mismatch GenTx f xs)
                 (Telescope g (Product GenTx f) xs)
    go :: InPairs InjectTx xs
-> NS GenTx xs
-> Telescope g f xs
-> Either (Mismatch GenTx f xs) (Telescope g (Product GenTx f) xs)
go InPairs InjectTx xs
_            (Z GenTx x
x) (TZ f x
f)   = Telescope g (Product GenTx f) (x : xs)
-> Either
     (Mismatch GenTx f xs) (Telescope g (Product GenTx f) (x : xs))
forall a b. b -> Either a b
Right (Telescope g (Product GenTx f) (x : xs)
 -> Either
      (Mismatch GenTx f xs) (Telescope g (Product GenTx f) (x : xs)))
-> Telescope g (Product GenTx f) (x : xs)
-> Either
     (Mismatch GenTx f xs) (Telescope g (Product GenTx f) (x : xs))
forall a b. (a -> b) -> a -> b
$ Product GenTx f x -> Telescope g (Product GenTx f) (x : xs)
forall a (f :: a -> *) (x :: a) (g :: a -> *) (xs :: [a]).
f x -> Telescope g f (x : xs)
TZ (GenTx x -> f x -> Product GenTx f x
forall k (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair GenTx x
x f x
f x
f)
    go (PCons InjectTx x y
_ InPairs InjectTx (y : zs)
is) (S NS GenTx xs
x) (TS g x
g Telescope g f xs
f) = (Mismatch GenTx f (y : zs) -> Mismatch GenTx f (x : y : zs))
-> (Telescope g (Product GenTx f) (y : zs)
    -> Telescope g (Product GenTx f) (x : y : zs))
-> Either
     (Mismatch GenTx f (y : zs))
     (Telescope g (Product GenTx f) (y : zs))
-> Either
     (Mismatch GenTx f (x : y : zs))
     (Telescope g (Product GenTx f) (x : y : zs))
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap Mismatch GenTx f (y : zs) -> Mismatch GenTx 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 GenTx f) (y : zs)
-> Telescope g (Product GenTx 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 GenTx f (y : zs))
   (Telescope g (Product GenTx f) (y : zs))
 -> Either
      (Mismatch GenTx f (x : y : zs))
      (Telescope g (Product GenTx f) (x : y : zs)))
-> Either
     (Mismatch GenTx f (y : zs))
     (Telescope g (Product GenTx f) (y : zs))
-> Either
     (Mismatch GenTx f (x : y : zs))
     (Telescope g (Product GenTx f) (x : y : zs))
forall a b. (a -> b) -> a -> b
$ InPairs InjectTx (y : zs)
-> NS GenTx (y : zs)
-> Telescope g f (y : zs)
-> Either
     (Mismatch GenTx f (y : zs))
     (Telescope g (Product GenTx f) (y : zs))
forall (xs :: [*]) (g :: * -> *) (f :: * -> *).
InPairs InjectTx xs
-> NS GenTx xs
-> Telescope g f xs
-> Either (Mismatch GenTx f xs) (Telescope g (Product GenTx f) xs)
go InPairs InjectTx (y : zs)
is NS GenTx xs
NS GenTx (y : zs)
x Telescope g f xs
Telescope g f (y : zs)
f
    go InPairs InjectTx xs
_            (S NS GenTx xs
x) (TZ f x
f)   = Mismatch GenTx f (x : xs)
-> Either
     (Mismatch GenTx f (x : xs)) (Telescope g (Product GenTx f) xs)
forall a b. a -> Either a b
Left (Mismatch GenTx f (x : xs)
 -> Either
      (Mismatch GenTx f (x : xs)) (Telescope g (Product GenTx f) xs))
-> Mismatch GenTx f (x : xs)
-> Either
     (Mismatch GenTx f (x : xs)) (Telescope g (Product GenTx f) xs)
forall a b. (a -> b) -> a -> b
$ NS GenTx xs -> f x -> Mismatch GenTx 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 GenTx xs
x f x
f
    go (PCons InjectTx x y
i InPairs InjectTx (y : zs)
is) (Z GenTx x
x) (TS g x
g Telescope g f xs
f) =
        case InjectTx x y -> GenTx x -> Maybe (GenTx y)
forall blk blk'.
InjectTx blk blk' -> GenTx blk -> Maybe (GenTx blk')
injectTxWith InjectTx x y
i GenTx x
GenTx x
x of
          Maybe (GenTx y)
Nothing -> Mismatch GenTx f (x : xs)
-> Either
     (Mismatch GenTx f (x : xs)) (Telescope g (Product GenTx f) xs)
forall a b. a -> Either a b
Left (Mismatch GenTx f (x : xs)
 -> Either
      (Mismatch GenTx f (x : xs)) (Telescope g (Product GenTx f) xs))
-> Mismatch GenTx f (x : xs)
-> Either
     (Mismatch GenTx f (x : xs)) (Telescope g (Product GenTx f) xs)
forall a b. (a -> b) -> a -> b
$ GenTx x -> NS f xs -> Mismatch GenTx f (x : xs)
forall a (f :: a -> *) (x :: a) (g :: a -> *) (xs :: [a]).
f x -> NS g xs -> Mismatch f g (x : xs)
ML GenTx 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 GenTx y
x' -> (Mismatch GenTx f (y : zs) -> Mismatch GenTx f (x : y : zs))
-> (Telescope g (Product GenTx f) (y : zs)
    -> Telescope g (Product GenTx f) (x : y : zs))
-> Either
     (Mismatch GenTx f (y : zs))
     (Telescope g (Product GenTx f) (y : zs))
-> Either
     (Mismatch GenTx f (x : y : zs))
     (Telescope g (Product GenTx f) (x : y : zs))
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap Mismatch GenTx f (y : zs) -> Mismatch GenTx 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 GenTx f) (y : zs)
-> Telescope g (Product GenTx 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 GenTx f (y : zs))
   (Telescope g (Product GenTx f) (y : zs))
 -> Either
      (Mismatch GenTx f (x : y : zs))
      (Telescope g (Product GenTx f) (x : y : zs)))
-> Either
     (Mismatch GenTx f (y : zs))
     (Telescope g (Product GenTx f) (y : zs))
-> Either
     (Mismatch GenTx f (x : y : zs))
     (Telescope g (Product GenTx f) (x : y : zs))
forall a b. (a -> b) -> a -> b
$ InPairs InjectTx (y : zs)
-> NS GenTx (y : zs)
-> Telescope g f (y : zs)
-> Either
     (Mismatch GenTx f (y : zs))
     (Telescope g (Product GenTx f) (y : zs))
forall (xs :: [*]) (g :: * -> *) (f :: * -> *).
InPairs InjectTx xs
-> NS GenTx xs
-> Telescope g f xs
-> Either (Mismatch GenTx f xs) (Telescope g (Product GenTx f) xs)
go InPairs InjectTx (y : zs)
is (GenTx y -> NS GenTx (y : zs)
forall a (f :: a -> *) (x :: a) (xs :: [a]). f x -> NS f (x : xs)
Z GenTx y
x') Telescope g f xs
Telescope g f (y : zs)
f

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
is NS GenTx xs
tx =
      (Telescope (K Past) (Product GenTx (Current f)) xs
 -> HardForkState (Product GenTx f) xs)
-> Either
     (Mismatch GenTx (Current f) xs)
     (Telescope (K Past) (Product GenTx (Current f)) xs)
-> Either
     (Mismatch GenTx (Current f) xs)
     (HardForkState (Product GenTx f) xs)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Telescope (K Past) (Current (Product GenTx f)) xs
-> HardForkState (Product GenTx f) xs
forall (f :: * -> *) (xs :: [*]).
Telescope (K Past) (Current f) xs -> HardForkState f xs
HardForkState (Telescope (K Past) (Current (Product GenTx f)) xs
 -> HardForkState (Product GenTx f) xs)
-> (Telescope (K Past) (Product GenTx (Current f)) xs
    -> Telescope (K Past) (Current (Product GenTx f)) xs)
-> Telescope (K Past) (Product GenTx (Current f)) xs
-> HardForkState (Product GenTx f) xs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a.
 Product GenTx (Current f) a -> Current (Product GenTx f) a)
-> Telescope (K Past) (Product GenTx (Current f)) xs
-> Telescope (K Past) (Current (Product GenTx 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 GenTx (Current f) a -> Current (Product GenTx f) a
forall (f :: * -> *) blk.
Product GenTx (Current f) blk -> Current (Product GenTx f) blk
distrib)
    (Either
   (Mismatch GenTx (Current f) xs)
   (Telescope (K Past) (Product GenTx (Current f)) xs)
 -> Either
      (Mismatch GenTx (Current f) xs)
      (HardForkState (Product GenTx f) xs))
-> (HardForkState f xs
    -> Either
         (Mismatch GenTx (Current f) xs)
         (Telescope (K Past) (Product GenTx (Current f)) xs))
-> HardForkState f xs
-> Either
     (Mismatch GenTx (Current f) xs)
     (HardForkState (Product GenTx f) xs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InPairs InjectTx xs
-> NS GenTx xs
-> Telescope (K Past) (Current f) xs
-> Either
     (Mismatch GenTx (Current f) xs)
     (Telescope (K Past) (Product GenTx (Current f)) xs)
forall (xs :: [*]) (g :: * -> *) (f :: * -> *).
InPairs InjectTx xs
-> NS GenTx xs
-> Telescope g f xs
-> Either (Mismatch GenTx f xs) (Telescope g (Product GenTx f) xs)
matchTx' InPairs InjectTx xs
is NS GenTx xs
tx
    (Telescope (K Past) (Current f) xs
 -> Either
      (Mismatch GenTx (Current f) xs)
      (Telescope (K Past) (Product GenTx (Current f)) xs))
-> (HardForkState f xs -> Telescope (K Past) (Current f) xs)
-> HardForkState f xs
-> Either
     (Mismatch GenTx (Current f) xs)
     (Telescope (K Past) (Product GenTx (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 GenTx (Current f) blk -> Current (Product GenTx f) blk
    distrib :: Product GenTx (Current f) blk -> Current (Product GenTx f) blk
distrib (Pair GenTx 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 GenTx f blk
currentState = GenTx blk -> f blk -> Product GenTx f blk
forall k (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair GenTx blk
tx' f blk
currentState
        }