{-# 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 (..),
) where

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.TxCert
import Cardano.Ledger.Shelley.LedgerState
import Cardano.Ledger.Shelley.Rules (LedgerEnv)
import Cardano.Ledger.TxIn (TxId)
import Control.DeepSeq (NFData)
import Control.Monad (foldM)
import Control.State.Transition.Extended
import Data.OMap.Strict (OMap)
import Data.Void (Void, absurd)
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 = VoidEraRule "SUBLEDGERS" 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
  ( ConwayEraGov era
  , ConwayEraCertState era
  , EraRule "SUBLEDGERS" era ~ DijkstraSUBLEDGERS era
  , EraRule "SUBLEDGER" era ~ DijkstraSUBLEDGER era
  , Embed (EraRule "SUBLEDGER" era) (DijkstraSUBLEDGERS 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) = Void

  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
  , 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
  , 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 = Void -> Void
Event (DijkstraSUBLEDGER era) -> Event (DijkstraSUBLEDGERS era)
forall a. Void -> a
absurd