{-# 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.BaseTypes (
  ShelleyBase,
 )
import Cardano.Ledger.Binary (
  DecCBOR (..),
  EncCBOR (..),
 )
import Cardano.Ledger.Conway.Core
import Cardano.Ledger.Conway.Governance
import Cardano.Ledger.Conway.State
import Cardano.Ledger.Dijkstra.Era (
  DijkstraEra,
  DijkstraSUBCERT,
  DijkstraSUBCERTS,
  DijkstraSUBDELEG,
  DijkstraSUBGOV,
  DijkstraSUBGOVCERT,
  DijkstraSUBLEDGER,
  DijkstraSUBLEDGERS,
  DijkstraSUBPOOL,
  DijkstraSUBUTXO,
  DijkstraSUBUTXOS,
  DijkstraSUBUTXOW,
 )
import Cardano.Ledger.Dijkstra.Rules.SubLedger (DijkstraSubLedgerPredFailure (..))
import Cardano.Ledger.Dijkstra.Rules.SubPool (DijkstraSubPoolEvent, DijkstraSubPoolPredFailure (..))
import Cardano.Ledger.Dijkstra.TxCert
import Cardano.Ledger.Shelley.LedgerState
import Cardano.Ledger.Shelley.Rules (LedgerEnv, PoolEvent, ShelleyPoolPredFailure)
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) = LedgerEnv 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
  ( EraTx era
  , ConwayEraTxBody era
  , ConwayEraGov era
  , ConwayEraCertState era
  , EraPlutusContext era
  , EraRule "SUBLEDGER" era ~ DijkstraSUBLEDGER era
  , EraRule "SUBGOV" era ~ DijkstraSUBGOV era
  , EraRule "SUBUTXO" era ~ DijkstraSUBUTXO era
  , EraRule "SUBUTXOS" era ~ DijkstraSUBUTXOS 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
  , TxCert era ~ DijkstraTxCert 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