{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeData #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableSuperClasses #-}

module Cardano.Ledger.Core.TxLevel (
  TxLevel (..),
  STxTopLevel (..),
  withSTxTopLevelM,
  STxBothLevels (..),
  withSTxBothLevels,
  EraTxLevel (..),
  HasEraTxLevel (..),
  asSTxTopLevel,
  mkSTxTopLevelM,
  withTopTxLevelOnly,
  asSTxBothLevels,
  mkSTxBothLevelsM,
  withBothTxLevels,
) where

import Cardano.Ledger.Core.Era (Era (..))
import Control.Monad.Trans.Class (lift)
import Control.Monad.Trans.Fail.String
import Data.Functor.Identity (Identity (..), runIdentity)
import Data.Kind (Type)
import Data.Typeable
import GHC.Stack

type data TxLevel = TopTx | SubTx

data STxTopLevel (l :: TxLevel) era where
  STopTxOnly :: STxTopLevel TopTx era

withSTxTopLevelM ::
  forall l era a m. (Typeable l, Era era, MonadFail m) => (STxTopLevel l era -> m a) -> m a
withSTxTopLevelM :: forall (l :: TxLevel) era a (m :: * -> *).
(Typeable l, Era era, MonadFail m) =>
(STxTopLevel l era -> m a) -> m a
withSTxTopLevelM STxTopLevel l era -> m a
f =
  case forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
forall (a :: TxLevel) (b :: TxLevel).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @l @TopTx of
    Just l :~: TopTx
Refl -> STxTopLevel l era -> m a
f STxTopLevel l era
STxTopLevel TopTx era
forall era. STxTopLevel TopTx era
STopTxOnly
    Maybe (l :~: TopTx)
Nothing -> String -> m a
forall a. String -> m a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> m a) -> String -> m a
forall a b. (a -> b) -> a -> b
$ String
"SubTx level is not supported in the " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> forall era. Era era => String
eraName @era String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" era"

data STxBothLevels (l :: TxLevel) era where
  STopTx :: STxBothLevels TopTx era
  SSubTx :: STxBothLevels SubTx era

withSTxBothLevels :: forall l era a. (Typeable l, HasCallStack) => (STxBothLevels l era -> a) -> a
withSTxBothLevels :: forall (l :: TxLevel) era a.
(Typeable l, HasCallStack) =>
(STxBothLevels l era -> a) -> a
withSTxBothLevels STxBothLevels l era -> a
f =
  case forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
forall (a :: TxLevel) (b :: TxLevel).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @l @TopTx of
    Just l :~: TopTx
Refl -> STxBothLevels l era -> a
f STxBothLevels l era
STxBothLevels TopTx era
forall era. STxBothLevels TopTx era
STopTx
    Maybe (l :~: TopTx)
Nothing -> case forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
forall (a :: TxLevel) (b :: TxLevel).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @l @SubTx of
      Just l :~: SubTx
Refl -> STxBothLevels l era -> a
f STxBothLevels l era
STxBothLevels SubTx era
forall era. STxBothLevels SubTx era
SSubTx
      Maybe (l :~: SubTx)
Nothing -> String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ String
"Impossible: Unrecognized TxLevel: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> TypeRep -> String
forall a. Show a => a -> String
show (Proxy l -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {k} (t :: k). Proxy t
forall (t :: TxLevel). Proxy t
Proxy @l))

class Era era => EraTxLevel era where
  -- | Supported transaction level as a singleton. One of these two should be used:
  --
  -- * `STxTopLevel` - for eras up to and including Conway, that do not support nested transactions.
  -- * `STxBothLevels` - for Dijkstra onwards that do support nested transactions.
  type STxLevel (l :: TxLevel) era = (r :: Type) | r -> era

  type STxLevel l era = STxBothLevels l era

-- | Type class for data families that have different definition depending on the level. Currently
-- it is only `Cardano.Ledger.Core.Tx` and `Cardano.Ledger.Core.TxBody` that have this distinction.
class EraTxLevel era => HasEraTxLevel (t :: TxLevel -> Type -> Type) era where
  toSTxLevel :: t l era -> STxLevel l era

mkSTxTopLevelM ::
  forall (l :: TxLevel) t m era.
  (Typeable l, Monad m, HasEraTxLevel t era, STxLevel l era ~ STxTopLevel l era) =>
  m (t TopTx era) -> m (t l era)
mkSTxTopLevelM :: forall (l :: TxLevel) (t :: TxLevel -> * -> *) (m :: * -> *) era.
(Typeable l, Monad m, HasEraTxLevel t era,
 STxLevel l era ~ STxTopLevel l era) =>
m (t TopTx era) -> m (t l era)
mkSTxTopLevelM m (t TopTx era)
mkTopTx = do
  (Either String (t l era) -> t l era)
-> m (Either String (t l era)) -> m (t l era)
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((String -> t l era)
-> (t l era -> t l era) -> Either String (t l era) -> t l era
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either String -> t l era
forall a. HasCallStack => String -> a
error t l era -> t l era
forall a. a -> a
id) (m (Either String (t l era)) -> m (t l era))
-> m (Either String (t l era)) -> m (t l era)
forall a b. (a -> b) -> a -> b
$ FailT m (t l era) -> m (Either String (t l era))
forall (m :: * -> *) a.
Functor m =>
FailT m a -> m (Either String a)
runFailT (FailT m (t l era) -> m (Either String (t l era)))
-> FailT m (t l era) -> m (Either String (t l era))
forall a b. (a -> b) -> a -> b
$ forall (l :: TxLevel) era a (m :: * -> *).
(Typeable l, Era era, MonadFail m) =>
(STxTopLevel l era -> m a) -> m a
withSTxTopLevelM @l @era ((STxTopLevel l era -> FailT m (t l era)) -> FailT m (t l era))
-> (STxTopLevel l era -> FailT m (t l era)) -> FailT m (t l era)
forall a b. (a -> b) -> a -> b
$ \STxTopLevel l era
level ->
    case STxTopLevel l era
level of
      STxTopLevel l era
STopTxOnly -> do
        res <- m (t TopTx era) -> FailT String m (t TopTx era)
forall (m :: * -> *) a. Monad m => m a -> FailT String m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m (t TopTx era)
mkTopTx
        -- Here we tell the compiler that we only expect top level transactions in this function and
        -- any attempt to construct a sub transaction level will result in a compiler error,
        -- instead of a trigger of `fail` in `MonadFail`, as `withSTxTopLevelM` would normally do.
        let _level = STxTopLevel l era -> STxTopLevel l era -> STxTopLevel l era
forall a. a -> a -> a
asTypeOf (t TopTx era -> STxLevel TopTx era
forall (l :: TxLevel). t l era -> STxLevel l era
forall (t :: TxLevel -> * -> *) era (l :: TxLevel).
HasEraTxLevel t era =>
t l era -> STxLevel l era
toSTxLevel t TopTx era
res) STxTopLevel l era
level
        pure res

asSTxTopLevel ::
  forall (l :: TxLevel) t era.
  (Typeable l, HasEraTxLevel t era, STxLevel l era ~ STxTopLevel l era) =>
  t TopTx era -> t l era
asSTxTopLevel :: forall (l :: TxLevel) (t :: TxLevel -> * -> *) era.
(Typeable l, HasEraTxLevel t era,
 STxLevel l era ~ STxTopLevel l era) =>
t TopTx era -> t l era
asSTxTopLevel = Identity (t l era) -> t l era
forall a. Identity a -> a
runIdentity (Identity (t l era) -> t l era)
-> (t TopTx era -> Identity (t l era)) -> t TopTx era -> t l era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Identity (t TopTx era) -> Identity (t l era)
forall (l :: TxLevel) (t :: TxLevel -> * -> *) (m :: * -> *) era.
(Typeable l, Monad m, HasEraTxLevel t era,
 STxLevel l era ~ STxTopLevel l era) =>
m (t TopTx era) -> m (t l era)
mkSTxTopLevelM (Identity (t TopTx era) -> Identity (t l era))
-> (t TopTx era -> Identity (t TopTx era))
-> t TopTx era
-> Identity (t l era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t TopTx era -> Identity (t TopTx era)
forall a. a -> Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure

withTopTxLevelOnly ::
  (HasEraTxLevel t era, STxLevel l era ~ STxTopLevel l era) =>
  t l era -> (t TopTx era -> a) -> a
withTopTxLevelOnly :: forall (t :: TxLevel -> * -> *) era (l :: TxLevel) a.
(HasEraTxLevel t era, STxLevel l era ~ STxTopLevel l era) =>
t l era -> (t TopTx era -> a) -> a
withTopTxLevelOnly t l era
t t TopTx era -> a
f =
  case t l era -> STxLevel l era
forall (l :: TxLevel). t l era -> STxLevel l era
forall (t :: TxLevel -> * -> *) era (l :: TxLevel).
HasEraTxLevel t era =>
t l era -> STxLevel l era
toSTxLevel t l era
t of
    STxLevel l era
STxTopLevel l era
STopTxOnly -> t TopTx era -> a
f t l era
t TopTx era
t

mkSTxBothLevelsM ::
  forall (l :: TxLevel) t m era.
  (Typeable l, Monad m, HasEraTxLevel t era, STxLevel l era ~ STxBothLevels l era) =>
  m (t TopTx era) -> m (t SubTx era) -> m (t l era)
mkSTxBothLevelsM :: forall (l :: TxLevel) (t :: TxLevel -> * -> *) (m :: * -> *) era.
(Typeable l, Monad m, HasEraTxLevel t era,
 STxLevel l era ~ STxBothLevels l era) =>
m (t TopTx era) -> m (t SubTx era) -> m (t l era)
mkSTxBothLevelsM m (t TopTx era)
mkTopTx m (t SubTx era)
mkSubTx =
  forall (l :: TxLevel) era a.
(Typeable l, HasCallStack) =>
(STxBothLevels l era -> a) -> a
withSTxBothLevels @l ((STxBothLevels l era -> m (t l era)) -> m (t l era))
-> (STxBothLevels l era -> m (t l era)) -> m (t l era)
forall a b. (a -> b) -> a -> b
$ \STxBothLevels l era
level -> do
    res <- case STxBothLevels l era
level of
      STxBothLevels l era
STopTx -> m (t l era)
m (t TopTx era)
mkTopTx
      STxBothLevels l era
SSubTx -> m (t l era)
m (t SubTx era)
mkSubTx
    -- Tell the compiler that we expect only `STxBothLevels` in this action
    let _level = STxBothLevels l era -> STxBothLevels l era -> STxBothLevels l era
forall a. a -> a -> a
asTypeOf (t l era -> STxLevel l era
forall (l :: TxLevel). t l era -> STxLevel l era
forall (t :: TxLevel -> * -> *) era (l :: TxLevel).
HasEraTxLevel t era =>
t l era -> STxLevel l era
toSTxLevel t l era
res) STxBothLevels l era
level
    pure res

asSTxBothLevels ::
  forall (l :: TxLevel) t era.
  (Typeable l, HasEraTxLevel t era, STxLevel l era ~ STxBothLevels l era) =>
  t TopTx era -> t SubTx era -> t l era
asSTxBothLevels :: forall (l :: TxLevel) (t :: TxLevel -> * -> *) era.
(Typeable l, HasEraTxLevel t era,
 STxLevel l era ~ STxBothLevels l era) =>
t TopTx era -> t SubTx era -> t l era
asSTxBothLevels t TopTx era
mkTopTx t SubTx era
mkSubTx = Identity (t l era) -> t l era
forall a. Identity a -> a
runIdentity (Identity (t l era) -> t l era) -> Identity (t l era) -> t l era
forall a b. (a -> b) -> a -> b
$ Identity (t TopTx era)
-> Identity (t SubTx era) -> Identity (t l era)
forall (l :: TxLevel) (t :: TxLevel -> * -> *) (m :: * -> *) era.
(Typeable l, Monad m, HasEraTxLevel t era,
 STxLevel l era ~ STxBothLevels l era) =>
m (t TopTx era) -> m (t SubTx era) -> m (t l era)
mkSTxBothLevelsM (t TopTx era -> Identity (t TopTx era)
forall a. a -> Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure t TopTx era
mkTopTx) (t SubTx era -> Identity (t SubTx era)
forall a. a -> Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure t SubTx era
mkSubTx)

withBothTxLevels ::
  (HasEraTxLevel t era, STxLevel l era ~ STxBothLevels l era) =>
  t l era -> (t TopTx era -> a) -> (t SubTx era -> a) -> a
withBothTxLevels :: forall (t :: TxLevel -> * -> *) era (l :: TxLevel) a.
(HasEraTxLevel t era, STxLevel l era ~ STxBothLevels l era) =>
t l era -> (t TopTx era -> a) -> (t SubTx era -> a) -> a
withBothTxLevels t l era
t t TopTx era -> a
fTop t SubTx era -> a
fSub =
  case t l era -> STxLevel l era
forall (l :: TxLevel). t l era -> STxLevel l era
forall (t :: TxLevel -> * -> *) era (l :: TxLevel).
HasEraTxLevel t era =>
t l era -> STxLevel l era
toSTxLevel t l era
t of
    STxLevel l era
STxBothLevels l era
STopTx -> t TopTx era -> a
fTop t l era
t TopTx era
t
    STxLevel l era
STxBothLevels l era
SSubTx -> t SubTx era -> a
fSub t l era
t SubTx era
t