{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE EmptyDataDeriving #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Cardano.Ledger.Dijkstra.Rules.SubLedgers (
  DijkstraSUBLEDGERS,
  DijkstraSubLedgersPredFailure (..),
  DijkstraSubLedgersEvent (..),
) where

import Cardano.Ledger.Alonzo.Plutus.Context (EraPlutusContext)
import Cardano.Ledger.Alonzo.Rules (AlonzoUtxowPredFailure)
import Cardano.Ledger.Alonzo.UTxO (AlonzoEraUTxO, AlonzoScriptsNeeded)
import Cardano.Ledger.Babbage.Rules (BabbageUtxowPredFailure)
import Cardano.Ledger.BaseTypes (
  ShelleyBase,
 )
import Cardano.Ledger.Binary (
  DecCBOR (..),
  EncCBOR (..),
 )
import Cardano.Ledger.Conway.Core
import Cardano.Ledger.Conway.Governance
import Cardano.Ledger.Conway.Rules (
  ConwayDelegPredFailure,
  ConwayGovCertPredFailure,
  ConwayGovEvent,
  ConwayGovPredFailure,
  ConwayLedgerPredFailure,
 )
import Cardano.Ledger.Conway.State
import Cardano.Ledger.Dijkstra.Era (
  DijkstraEra,
  DijkstraSUBCERT,
  DijkstraSUBCERTS,
  DijkstraSUBDELEG,
  DijkstraSUBGOV,
  DijkstraSUBGOVCERT,
  DijkstraSUBLEDGER,
  DijkstraSUBLEDGERS,
  DijkstraSUBPOOL,
  DijkstraSUBUTXO,
  DijkstraSUBUTXOW,
 )
import Cardano.Ledger.Dijkstra.Rules.SubDeleg (DijkstraSubDelegPredFailure)
import Cardano.Ledger.Dijkstra.Rules.SubGov (DijkstraSubGovEvent, DijkstraSubGovPredFailure (..))
import Cardano.Ledger.Dijkstra.Rules.SubGovCert (DijkstraSubGovCertPredFailure)
import Cardano.Ledger.Dijkstra.Rules.SubLedger (
  DijkstraSubLedgerPredFailure (..),
  SubLedgerEnv (..),
 )
import Cardano.Ledger.Dijkstra.Rules.SubPool (DijkstraSubPoolEvent, DijkstraSubPoolPredFailure (..))
import Cardano.Ledger.Dijkstra.TxCert
import Cardano.Ledger.Shelley.LedgerState
import Cardano.Ledger.Shelley.Rules (
  PoolEvent,
  ShelleyPoolPredFailure,
  ShelleyUtxowPredFailure,
 )
import Cardano.Ledger.TxIn (TxId)
import Control.DeepSeq (NFData)
import Control.Monad (foldM)
import Control.State.Transition.Extended
import Data.OMap.Strict (OMap)
import GHC.Generics (Generic)
import NoThunks.Class (NoThunks (..))

newtype DijkstraSubLedgersPredFailure era
  = SubLedgerFailure (PredicateFailure (EraRule "SUBLEDGER" era))
  deriving ((forall x.
 DijkstraSubLedgersPredFailure era
 -> Rep (DijkstraSubLedgersPredFailure era) x)
-> (forall x.
    Rep (DijkstraSubLedgersPredFailure era) x
    -> DijkstraSubLedgersPredFailure era)
-> Generic (DijkstraSubLedgersPredFailure era)
forall x.
Rep (DijkstraSubLedgersPredFailure era) x
-> DijkstraSubLedgersPredFailure era
forall x.
DijkstraSubLedgersPredFailure era
-> Rep (DijkstraSubLedgersPredFailure era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (DijkstraSubLedgersPredFailure era) x
-> DijkstraSubLedgersPredFailure era
forall era x.
DijkstraSubLedgersPredFailure era
-> Rep (DijkstraSubLedgersPredFailure era) x
$cfrom :: forall era x.
DijkstraSubLedgersPredFailure era
-> Rep (DijkstraSubLedgersPredFailure era) x
from :: forall x.
DijkstraSubLedgersPredFailure era
-> Rep (DijkstraSubLedgersPredFailure era) x
$cto :: forall era x.
Rep (DijkstraSubLedgersPredFailure era) x
-> DijkstraSubLedgersPredFailure era
to :: forall x.
Rep (DijkstraSubLedgersPredFailure era) x
-> DijkstraSubLedgersPredFailure era
Generic)

deriving stock instance
  Eq (PredicateFailure (EraRule "SUBLEDGER" era)) => Eq (DijkstraSubLedgersPredFailure era)

deriving stock instance
  Show (PredicateFailure (EraRule "SUBLEDGER" era)) => Show (DijkstraSubLedgersPredFailure era)

instance
  NoThunks (PredicateFailure (EraRule "SUBLEDGER" era)) =>
  NoThunks (DijkstraSubLedgersPredFailure era)

instance NFData (PredicateFailure (EraRule "SUBLEDGER" era)) => NFData (DijkstraSubLedgersPredFailure era)

instance
  ( Era era
  , EncCBOR (PredicateFailure (EraRule "SUBLEDGER" era))
  ) =>
  EncCBOR (DijkstraSubLedgersPredFailure era)
  where
  encCBOR :: DijkstraSubLedgersPredFailure era -> Encoding
encCBOR (SubLedgerFailure PredicateFailure (EraRule "SUBLEDGER" era)
e) = PredicateFailure (EraRule "SUBLEDGER" era) -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR PredicateFailure (EraRule "SUBLEDGER" era)
e

instance
  ( Era era
  , DecCBOR (PredicateFailure (EraRule "SUBLEDGER" era))
  ) =>
  DecCBOR (DijkstraSubLedgersPredFailure era)
  where
  decCBOR :: forall s. Decoder s (DijkstraSubLedgersPredFailure era)
decCBOR = PredicateFailure (EraRule "SUBLEDGER" era)
-> DijkstraSubLedgersPredFailure era
forall era.
PredicateFailure (EraRule "SUBLEDGER" era)
-> DijkstraSubLedgersPredFailure era
SubLedgerFailure (PredicateFailure (EraRule "SUBLEDGER" era)
 -> DijkstraSubLedgersPredFailure era)
-> Decoder s (PredicateFailure (EraRule "SUBLEDGER" era))
-> Decoder s (DijkstraSubLedgersPredFailure era)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Decoder s (PredicateFailure (EraRule "SUBLEDGER" era))
forall s. Decoder s (PredicateFailure (EraRule "SUBLEDGER" era))
forall a s. DecCBOR a => Decoder s a
decCBOR

type instance EraRuleFailure "SUBLEDGERS" DijkstraEra = DijkstraSubLedgersPredFailure DijkstraEra

type instance EraRuleEvent "SUBLEDGERS" DijkstraEra = DijkstraSubLedgersEvent DijkstraEra

instance InjectRuleFailure "SUBLEDGERS" DijkstraSubLedgersPredFailure DijkstraEra

instance InjectRuleFailure "SUBLEDGERS" DijkstraSubLedgerPredFailure DijkstraEra where
  injectFailure :: DijkstraSubLedgerPredFailure DijkstraEra
-> EraRuleFailure "SUBLEDGERS" DijkstraEra
injectFailure = PredicateFailure (EraRule "SUBLEDGER" DijkstraEra)
-> DijkstraSubLedgersPredFailure DijkstraEra
DijkstraSubLedgerPredFailure DijkstraEra
-> EraRuleFailure "SUBLEDGERS" DijkstraEra
forall era.
PredicateFailure (EraRule "SUBLEDGER" era)
-> DijkstraSubLedgersPredFailure era
SubLedgerFailure

instance InjectRuleEvent "SUBLEDGERS" DijkstraSubLedgersEvent DijkstraEra

newtype DijkstraSubLedgersEvent era
  = SubLedgerEvent (Event (EraRule "SUBLEDGER" era))
  deriving ((forall x.
 DijkstraSubLedgersEvent era -> Rep (DijkstraSubLedgersEvent era) x)
-> (forall x.
    Rep (DijkstraSubLedgersEvent era) x -> DijkstraSubLedgersEvent era)
-> Generic (DijkstraSubLedgersEvent era)
forall x.
Rep (DijkstraSubLedgersEvent era) x -> DijkstraSubLedgersEvent era
forall x.
DijkstraSubLedgersEvent era -> Rep (DijkstraSubLedgersEvent era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (DijkstraSubLedgersEvent era) x -> DijkstraSubLedgersEvent era
forall era x.
DijkstraSubLedgersEvent era -> Rep (DijkstraSubLedgersEvent era) x
$cfrom :: forall era x.
DijkstraSubLedgersEvent era -> Rep (DijkstraSubLedgersEvent era) x
from :: forall x.
DijkstraSubLedgersEvent era -> Rep (DijkstraSubLedgersEvent era) x
$cto :: forall era x.
Rep (DijkstraSubLedgersEvent era) x -> DijkstraSubLedgersEvent era
to :: forall x.
Rep (DijkstraSubLedgersEvent era) x -> DijkstraSubLedgersEvent era
Generic)

deriving instance Eq (Event (EraRule "SUBLEDGER" era)) => Eq (DijkstraSubLedgersEvent era)

instance NFData (Event (EraRule "SUBLEDGER" era)) => NFData (DijkstraSubLedgersEvent era)

instance
  ( ConwayEraGov era
  , ConwayEraCertState era
  , EraPlutusContext era
  , EraRule "SUBLEDGERS" era ~ DijkstraSUBLEDGERS era
  , EraRule "SUBLEDGER" era ~ DijkstraSUBLEDGER era
  , Embed (EraRule "SUBLEDGER" era) (DijkstraSUBLEDGERS era)
  , InjectRuleEvent "SUBPOOL" PoolEvent era
  , InjectRuleEvent "SUBPOOL" DijkstraSubPoolEvent era
  , InjectRuleFailure "SUBPOOL" ShelleyPoolPredFailure era
  , InjectRuleFailure "SUBPOOL" DijkstraSubPoolPredFailure era
  ) =>
  STS (DijkstraSUBLEDGERS era)
  where
  type State (DijkstraSUBLEDGERS era) = LedgerState era
  type Signal (DijkstraSUBLEDGERS era) = OMap TxId (Tx SubTx era)
  type Environment (DijkstraSUBLEDGERS era) = SubLedgerEnv era
  type BaseM (DijkstraSUBLEDGERS era) = ShelleyBase
  type PredicateFailure (DijkstraSUBLEDGERS era) = DijkstraSubLedgersPredFailure era
  type Event (DijkstraSUBLEDGERS era) = DijkstraSubLedgersEvent era

  transitionRules :: [TransitionRule (DijkstraSUBLEDGERS era)]
transitionRules = [forall era.
(EraRule "SUBLEDGERS" era ~ DijkstraSUBLEDGERS era,
 EraRule "SUBLEDGER" era ~ DijkstraSUBLEDGER era,
 Embed (EraRule "SUBLEDGER" era) (DijkstraSUBLEDGERS era)) =>
TransitionRule (EraRule "SUBLEDGERS" era)
dijkstraSubLedgersTransition @era]

dijkstraSubLedgersTransition ::
  forall era.
  ( EraRule "SUBLEDGERS" era ~ DijkstraSUBLEDGERS era
  , EraRule "SUBLEDGER" era ~ DijkstraSUBLEDGER era
  , Embed (EraRule "SUBLEDGER" era) (DijkstraSUBLEDGERS era)
  ) =>
  TransitionRule (EraRule "SUBLEDGERS" era)
dijkstraSubLedgersTransition :: forall era.
(EraRule "SUBLEDGERS" era ~ DijkstraSUBLEDGERS era,
 EraRule "SUBLEDGER" era ~ DijkstraSUBLEDGER era,
 Embed (EraRule "SUBLEDGER" era) (DijkstraSUBLEDGERS era)) =>
TransitionRule (EraRule "SUBLEDGERS" era)
dijkstraSubLedgersTransition = do
  TRC (env, ledgerState, subTxs) <- Rule
  (DijkstraSUBLEDGERS era)
  'Transition
  (RuleContext 'Transition (DijkstraSUBLEDGERS era))
F (Clause (DijkstraSUBLEDGERS era) 'Transition)
  (TRC (DijkstraSUBLEDGERS era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
  foldM
    ( \LedgerState era
ls Tx SubTx era
subTx ->
        forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @(EraRule "SUBLEDGER" era) (RuleContext 'Transition (EraRule "SUBLEDGER" era)
 -> Rule
      (DijkstraSUBLEDGERS era)
      'Transition
      (State (EraRule "SUBLEDGER" era)))
-> RuleContext 'Transition (EraRule "SUBLEDGER" era)
-> Rule
     (DijkstraSUBLEDGERS era)
     'Transition
     (State (EraRule "SUBLEDGER" era))
forall a b. (a -> b) -> a -> b
$ (Environment (DijkstraSUBLEDGER era),
 State (DijkstraSUBLEDGER era), Signal (DijkstraSUBLEDGER era))
-> TRC (DijkstraSUBLEDGER era)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment (DijkstraSUBLEDGER era)
Environment (DijkstraSUBLEDGERS era)
env, State (DijkstraSUBLEDGER era)
LedgerState era
ls, Tx SubTx era
Signal (DijkstraSUBLEDGER era)
subTx)
    )
    ledgerState
    subTxs

instance
  ( AlonzoEraTx era
  , AlonzoEraUTxO era
  , ConwayEraTxBody era
  , ConwayEraGov era
  , ConwayEraCertState era
  , ConwayEraPParams era
  , ConwayEraTxCert era
  , EraPlutusContext era
  , EraRule "SUBLEDGER" era ~ DijkstraSUBLEDGER era
  , EraRule "SUBGOV" era ~ DijkstraSUBGOV era
  , EraRule "SUBUTXO" era ~ DijkstraSUBUTXO era
  , EraRule "SUBUTXOW" era ~ DijkstraSUBUTXOW era
  , EraRule "SUBCERTS" era ~ DijkstraSUBCERTS era
  , EraRule "SUBCERT" era ~ DijkstraSUBCERT era
  , EraRule "SUBDELEG" era ~ DijkstraSUBDELEG era
  , EraRule "SUBPOOL" era ~ DijkstraSUBPOOL era
  , EraRule "SUBGOVCERT" era ~ DijkstraSUBGOVCERT era
  , InjectRuleEvent "SUBPOOL" PoolEvent era
  , InjectRuleEvent "SUBPOOL" DijkstraSubPoolEvent era
  , InjectRuleFailure "SUBPOOL" ShelleyPoolPredFailure era
  , InjectRuleFailure "SUBPOOL" DijkstraSubPoolPredFailure era
  , InjectRuleFailure "SUBGOVCERT" DijkstraSubGovCertPredFailure era
  , InjectRuleFailure "SUBGOVCERT" ConwayGovCertPredFailure era
  , InjectRuleFailure "SUBDELEG" ConwayDelegPredFailure era
  , InjectRuleFailure "SUBDELEG" DijkstraSubDelegPredFailure era
  , InjectRuleEvent "SUBGOV" DijkstraSubGovEvent era
  , InjectRuleEvent "SUBGOV" ConwayGovEvent era
  , InjectRuleFailure "SUBGOV" DijkstraSubGovPredFailure era
  , InjectRuleFailure "SUBGOV" ConwayGovPredFailure era
  , InjectRuleFailure "SUBLEDGER" ConwayLedgerPredFailure era
  , InjectRuleFailure "SUBUTXOW" AlonzoUtxowPredFailure era
  , InjectRuleFailure "SUBUTXOW" ShelleyUtxowPredFailure era
  , InjectRuleFailure "SUBUTXOW" BabbageUtxowPredFailure era
  , TxCert era ~ DijkstraTxCert era
  , ScriptsNeeded era ~ AlonzoScriptsNeeded era
  ) =>
  Embed (DijkstraSUBLEDGER era) (DijkstraSUBLEDGERS era)
  where
  wrapFailed :: PredicateFailure (DijkstraSUBLEDGER era)
-> PredicateFailure (DijkstraSUBLEDGERS era)
wrapFailed = PredicateFailure (EraRule "SUBLEDGER" era)
-> DijkstraSubLedgersPredFailure era
PredicateFailure (DijkstraSUBLEDGER era)
-> PredicateFailure (DijkstraSUBLEDGERS era)
forall era.
PredicateFailure (EraRule "SUBLEDGER" era)
-> DijkstraSubLedgersPredFailure era
SubLedgerFailure
  wrapEvent :: Event (DijkstraSUBLEDGER era) -> Event (DijkstraSUBLEDGERS era)
wrapEvent = Event (EraRule "SUBLEDGER" era) -> DijkstraSubLedgersEvent era
Event (DijkstraSUBLEDGER era) -> Event (DijkstraSUBLEDGERS era)
forall era.
Event (EraRule "SUBLEDGER" era) -> DijkstraSubLedgersEvent era
SubLedgerEvent