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

module Cardano.Ledger.Dijkstra.Rules.SubUtxos (
  DijkstraSUBUTXOS,
  DijkstraSubUtxosEvent (..),
  DijkstraSubUtxosPredFailure (..),
) 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.Rules (ConwayUtxosEvent, ConwayUtxosPredFailure)
import Cardano.Ledger.Dijkstra.Era (
  DijkstraEra,
  DijkstraSUBUTXOS,
 )
import Cardano.Ledger.Shelley.LedgerState (UTxOState)
import Cardano.Ledger.Shelley.Rules (UtxoEnv)
import Control.DeepSeq (NFData)
import Control.State.Transition.Extended (
  BaseM,
  Environment,
  Event,
  PredicateFailure,
  STS,
  Signal,
  State,
  TRC (TRC),
  TransitionRule,
  judgmentContext,
  transitionRules,
 )
import GHC.Generics (Generic)
import NoThunks.Class (NoThunks (..))

newtype DijkstraSubUtxosPredFailure era = DijkstraSubUtxosPredFailure (ConwayUtxosPredFailure era)
  deriving ((forall x.
 DijkstraSubUtxosPredFailure era
 -> Rep (DijkstraSubUtxosPredFailure era) x)
-> (forall x.
    Rep (DijkstraSubUtxosPredFailure era) x
    -> DijkstraSubUtxosPredFailure era)
-> Generic (DijkstraSubUtxosPredFailure era)
forall x.
Rep (DijkstraSubUtxosPredFailure era) x
-> DijkstraSubUtxosPredFailure era
forall x.
DijkstraSubUtxosPredFailure era
-> Rep (DijkstraSubUtxosPredFailure era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (DijkstraSubUtxosPredFailure era) x
-> DijkstraSubUtxosPredFailure era
forall era x.
DijkstraSubUtxosPredFailure era
-> Rep (DijkstraSubUtxosPredFailure era) x
$cfrom :: forall era x.
DijkstraSubUtxosPredFailure era
-> Rep (DijkstraSubUtxosPredFailure era) x
from :: forall x.
DijkstraSubUtxosPredFailure era
-> Rep (DijkstraSubUtxosPredFailure era) x
$cto :: forall era x.
Rep (DijkstraSubUtxosPredFailure era) x
-> DijkstraSubUtxosPredFailure era
to :: forall x.
Rep (DijkstraSubUtxosPredFailure era) x
-> DijkstraSubUtxosPredFailure era
Generic)

deriving newtype instance
  Eq (ConwayUtxosPredFailure era) =>
  Eq (DijkstraSubUtxosPredFailure era)

deriving newtype instance
  Show (ConwayUtxosPredFailure era) =>
  Show (DijkstraSubUtxosPredFailure era)

instance
  NoThunks (ConwayUtxosPredFailure era) =>
  NoThunks (DijkstraSubUtxosPredFailure era)

instance NFData (ConwayUtxosPredFailure era) => NFData (DijkstraSubUtxosPredFailure era)

deriving newtype instance
  EncCBOR (ConwayUtxosPredFailure era) =>
  EncCBOR (DijkstraSubUtxosPredFailure era)

deriving newtype instance
  (Era era, DecCBOR (ConwayUtxosPredFailure era)) =>
  DecCBOR (DijkstraSubUtxosPredFailure era)

type instance EraRuleFailure "SUBUTXOS" DijkstraEra = DijkstraSubUtxosPredFailure DijkstraEra

type instance EraRuleEvent "SUBUTXOS" DijkstraEra = DijkstraSubUtxosEvent DijkstraEra

instance InjectRuleFailure "SUBUTXOS" DijkstraSubUtxosPredFailure DijkstraEra

newtype DijkstraSubUtxosEvent era = DijkstraSubUtxosEvent (ConwayUtxosEvent era)
  deriving ((forall x.
 DijkstraSubUtxosEvent era -> Rep (DijkstraSubUtxosEvent era) x)
-> (forall x.
    Rep (DijkstraSubUtxosEvent era) x -> DijkstraSubUtxosEvent era)
-> Generic (DijkstraSubUtxosEvent era)
forall x.
Rep (DijkstraSubUtxosEvent era) x -> DijkstraSubUtxosEvent era
forall x.
DijkstraSubUtxosEvent era -> Rep (DijkstraSubUtxosEvent era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (DijkstraSubUtxosEvent era) x -> DijkstraSubUtxosEvent era
forall era x.
DijkstraSubUtxosEvent era -> Rep (DijkstraSubUtxosEvent era) x
$cfrom :: forall era x.
DijkstraSubUtxosEvent era -> Rep (DijkstraSubUtxosEvent era) x
from :: forall x.
DijkstraSubUtxosEvent era -> Rep (DijkstraSubUtxosEvent era) x
$cto :: forall era x.
Rep (DijkstraSubUtxosEvent era) x -> DijkstraSubUtxosEvent era
to :: forall x.
Rep (DijkstraSubUtxosEvent era) x -> DijkstraSubUtxosEvent era
Generic)

deriving instance Eq (ConwayUtxosEvent era) => Eq (DijkstraSubUtxosEvent era)

instance NFData (ConwayUtxosEvent era) => NFData (DijkstraSubUtxosEvent era)

instance InjectRuleEvent "SUBUTXOS" DijkstraSubUtxosEvent DijkstraEra

instance
  ( ConwayEraGov era
  , ConwayEraTxBody era
  , EraPlutusContext era
  , EraRule "SUBUTXOS" era ~ DijkstraSUBUTXOS era
  ) =>
  STS (DijkstraSUBUTXOS era)
  where
  type State (DijkstraSUBUTXOS era) = UTxOState era
  type Signal (DijkstraSUBUTXOS era) = Tx SubTx era
  type Environment (DijkstraSUBUTXOS era) = UtxoEnv era
  type BaseM (DijkstraSUBUTXOS era) = ShelleyBase
  type PredicateFailure (DijkstraSUBUTXOS era) = DijkstraSubUtxosPredFailure era
  type Event (DijkstraSUBUTXOS era) = DijkstraSubUtxosEvent era

  transitionRules :: [TransitionRule (DijkstraSUBUTXOS era)]
transitionRules = [forall era. TransitionRule (EraRule "SUBUTXOS" era)
dijkstraSubUtxosTransition @era]

dijkstraSubUtxosTransition :: TransitionRule (EraRule "SUBUTXOS" era)
dijkstraSubUtxosTransition :: forall era. TransitionRule (EraRule "SUBUTXOS" era)
dijkstraSubUtxosTransition = do
  TRC (_, st, _) <- Rule
  (EraRule "SUBUTXOS" era)
  'Transition
  (RuleContext 'Transition (EraRule "SUBUTXOS" era))
F (Clause (EraRule "SUBUTXOS" era) 'Transition)
  (TRC (EraRule "SUBUTXOS" era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
  pure st