{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE CPP #-}
{-# 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 #-}
#if __GLASGOW_HASKELL__ >= 910
-- See https://gitlab.haskell.org/ghc/ghc/-/issues/27342
{-# OPTIONS_GHC -fno-spec-eval #-}
#endif

module Cardano.Ledger.Dijkstra.Rules.SubLedgers (
  SUBLEDGERS,
  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,
  SUBLEDGER,
  SUBLEDGERS,
 )
import Cardano.Ledger.Dijkstra.Rules.SubLedger (
  DijkstraSubLedgerEvent,
  DijkstraSubLedgerPredFailure (..),
  SubLedgerEnv (..),
 )
import Cardano.Ledger.Dijkstra.Rules.SubPool (DijkstraSubPoolEvent, DijkstraSubPoolPredFailure (..))
import Cardano.Ledger.Shelley.LedgerState
import qualified Cardano.Ledger.Shelley.Rules as Shelley
import Control.DeepSeq (NFData)
import Control.Monad (foldM)
import Control.State.Transition.Extended
import GHC.Generics (Generic)

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
  Ord (PredicateFailure (EraRule "SUBLEDGER" era)) => Ord (DijkstraSubLedgersPredFailure era)

deriving stock instance
  Show (PredicateFailure (EraRule "SUBLEDGER" era)) => Show (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 ~ SUBLEDGERS era
  , EraRule "SUBLEDGER" era ~ SUBLEDGER era
  , Embed (EraRule "SUBLEDGER" era) (SUBLEDGERS era)
  , InjectRuleEvent "SUBPOOL" Shelley.PoolEvent era
  , InjectRuleEvent "SUBPOOL" DijkstraSubPoolEvent era
  , InjectRuleFailure "SUBPOOL" Shelley.ShelleyPoolPredFailure era
  , InjectRuleFailure "SUBPOOL" DijkstraSubPoolPredFailure era
  ) =>
  STS (SUBLEDGERS era)
  where
  type State (SUBLEDGERS era) = LedgerState era
  type Signal (SUBLEDGERS era) = [StAnnTx SubTx era]
  type Environment (SUBLEDGERS era) = SubLedgerEnv era
  type BaseM (SUBLEDGERS era) = ShelleyBase
  type PredicateFailure (SUBLEDGERS era) = DijkstraSubLedgersPredFailure era
  type Event (SUBLEDGERS era) = DijkstraSubLedgersEvent era

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

dijkstraSubLedgersTransition ::
  forall era.
  ( EraRule "SUBLEDGERS" era ~ SUBLEDGERS era
  , EraRule "SUBLEDGER" era ~ SUBLEDGER era
  , Embed (EraRule "SUBLEDGER" era) (SUBLEDGERS era)
  ) =>
  TransitionRule (EraRule "SUBLEDGERS" era)
dijkstraSubLedgersTransition :: forall era.
(EraRule "SUBLEDGERS" era ~ SUBLEDGERS era,
 EraRule "SUBLEDGER" era ~ SUBLEDGER era,
 Embed (EraRule "SUBLEDGER" era) (SUBLEDGERS era)) =>
TransitionRule (EraRule "SUBLEDGERS" era)
dijkstraSubLedgersTransition = do
  TRC (env, ledgerState, subTxs) <- Rule
  (SUBLEDGERS era)
  'Transition
  (RuleContext 'Transition (SUBLEDGERS era))
F (Clause (SUBLEDGERS era) 'Transition) (TRC (SUBLEDGERS era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
  foldM
    ( \LedgerState era
ls StAnnTx 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
      (SUBLEDGERS era) 'Transition (State (EraRule "SUBLEDGER" era)))
-> RuleContext 'Transition (EraRule "SUBLEDGER" era)
-> Rule
     (SUBLEDGERS era) 'Transition (State (EraRule "SUBLEDGER" era))
forall a b. (a -> b) -> a -> b
$ (Environment (SUBLEDGER era), State (SUBLEDGER era),
 Signal (SUBLEDGER era))
-> TRC (SUBLEDGER era)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment (SUBLEDGER era)
Environment (SUBLEDGERS era)
env, State (SUBLEDGER era)
LedgerState era
ls, StAnnTx SubTx era
Signal (SUBLEDGER era)
subTx)
    )
    ledgerState
    subTxs

instance
  ( STS (SUBLEDGER era)
  , PredicateFailure (EraRule "SUBLEDGER" era) ~ DijkstraSubLedgerPredFailure era
  , Event (EraRule "SUBLEDGER" era) ~ DijkstraSubLedgerEvent era
  ) =>
  Embed (SUBLEDGER era) (SUBLEDGERS era)
  where
  wrapFailed :: PredicateFailure (SUBLEDGER era)
-> PredicateFailure (SUBLEDGERS era)
wrapFailed = PredicateFailure (EraRule "SUBLEDGER" era)
-> DijkstraSubLedgersPredFailure era
PredicateFailure (SUBLEDGER era)
-> PredicateFailure (SUBLEDGERS era)
forall era.
PredicateFailure (EraRule "SUBLEDGER" era)
-> DijkstraSubLedgersPredFailure era
SubLedgerFailure
  wrapEvent :: Event (SUBLEDGER era) -> Event (SUBLEDGERS era)
wrapEvent = Event (EraRule "SUBLEDGER" era) -> DijkstraSubLedgersEvent era
Event (SUBLEDGER era) -> Event (SUBLEDGERS era)
forall era.
Event (EraRule "SUBLEDGER" era) -> DijkstraSubLedgersEvent era
SubLedgerEvent