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

module Cardano.Ledger.Dijkstra.Rules.SubUtxos (
  DijkstraSUBUTXOS,
  DijkstraSubUtxosPredFailure (..),
) 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.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 Data.Typeable (Typeable)
import Data.Void (Void)
import GHC.Generics (Generic)
import NoThunks.Class (NoThunks (..))

data DijkstraSubUtxosPredFailure era = DijkstraSubUtxosPredFailure
  deriving (Int -> DijkstraSubUtxosPredFailure era -> ShowS
[DijkstraSubUtxosPredFailure era] -> ShowS
DijkstraSubUtxosPredFailure era -> String
(Int -> DijkstraSubUtxosPredFailure era -> ShowS)
-> (DijkstraSubUtxosPredFailure era -> String)
-> ([DijkstraSubUtxosPredFailure era] -> ShowS)
-> Show (DijkstraSubUtxosPredFailure era)
forall era. Int -> DijkstraSubUtxosPredFailure era -> ShowS
forall era. [DijkstraSubUtxosPredFailure era] -> ShowS
forall era. DijkstraSubUtxosPredFailure era -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall era. Int -> DijkstraSubUtxosPredFailure era -> ShowS
showsPrec :: Int -> DijkstraSubUtxosPredFailure era -> ShowS
$cshow :: forall era. DijkstraSubUtxosPredFailure era -> String
show :: DijkstraSubUtxosPredFailure era -> String
$cshowList :: forall era. [DijkstraSubUtxosPredFailure era] -> ShowS
showList :: [DijkstraSubUtxosPredFailure era] -> ShowS
Show, DijkstraSubUtxosPredFailure era
-> DijkstraSubUtxosPredFailure era -> Bool
(DijkstraSubUtxosPredFailure era
 -> DijkstraSubUtxosPredFailure era -> Bool)
-> (DijkstraSubUtxosPredFailure era
    -> DijkstraSubUtxosPredFailure era -> Bool)
-> Eq (DijkstraSubUtxosPredFailure era)
forall era.
DijkstraSubUtxosPredFailure era
-> DijkstraSubUtxosPredFailure era -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall era.
DijkstraSubUtxosPredFailure era
-> DijkstraSubUtxosPredFailure era -> Bool
== :: DijkstraSubUtxosPredFailure era
-> DijkstraSubUtxosPredFailure era -> Bool
$c/= :: forall era.
DijkstraSubUtxosPredFailure era
-> DijkstraSubUtxosPredFailure era -> Bool
/= :: DijkstraSubUtxosPredFailure era
-> DijkstraSubUtxosPredFailure era -> Bool
Eq, (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)

instance NoThunks (DijkstraSubUtxosPredFailure era)

instance NFData (DijkstraSubUtxosPredFailure era)

instance Era era => EncCBOR (DijkstraSubUtxosPredFailure era) where
  encCBOR :: DijkstraSubUtxosPredFailure era -> Encoding
encCBOR DijkstraSubUtxosPredFailure era
_ = () -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR ()

instance Typeable era => DecCBOR (DijkstraSubUtxosPredFailure era) where
  decCBOR :: forall s. Decoder s (DijkstraSubUtxosPredFailure era)
decCBOR = forall a s. DecCBOR a => Decoder s a
decCBOR @() Decoder s ()
-> Decoder s (DijkstraSubUtxosPredFailure era)
-> Decoder s (DijkstraSubUtxosPredFailure era)
forall a b. Decoder s a -> Decoder s b -> Decoder s b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> DijkstraSubUtxosPredFailure era
-> Decoder s (DijkstraSubUtxosPredFailure era)
forall a. a -> Decoder s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DijkstraSubUtxosPredFailure era
forall era. DijkstraSubUtxosPredFailure era
DijkstraSubUtxosPredFailure

type instance EraRuleFailure "SUBUTXOS" DijkstraEra = DijkstraSubUtxosPredFailure DijkstraEra

type instance EraRuleEvent "SUBUTXOS" DijkstraEra = VoidEraRule "SUBUTXOS" DijkstraEra

instance InjectRuleFailure "SUBUTXOS" DijkstraSubUtxosPredFailure DijkstraEra

instance
  ( ConwayEraGov 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) = Void

  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