{-# 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.SubUtxo (
  DijkstraSUBUTXO,
  DijkstraSubUtxoPredFailure (..),
) 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,
  DijkstraSUBUTXO,
  DijkstraSUBUTXOS,
 )
import Cardano.Ledger.Dijkstra.Rules.SubUtxos (DijkstraSubUtxosPredFailure)
import Cardano.Ledger.Shelley.LedgerState (UTxOState)
import Cardano.Ledger.Shelley.Rules (UtxoEnv)
import Control.DeepSeq (NFData)
import Control.State.Transition.Extended
import Data.Void (Void, absurd)
import GHC.Generics (Generic)
import NoThunks.Class (NoThunks (..))

data DijkstraSubUtxoPredFailure era
  = SubUtxosFailure (PredicateFailure (EraRule "SUBUTXOS" era))
  deriving ((forall x.
 DijkstraSubUtxoPredFailure era
 -> Rep (DijkstraSubUtxoPredFailure era) x)
-> (forall x.
    Rep (DijkstraSubUtxoPredFailure era) x
    -> DijkstraSubUtxoPredFailure era)
-> Generic (DijkstraSubUtxoPredFailure era)
forall x.
Rep (DijkstraSubUtxoPredFailure era) x
-> DijkstraSubUtxoPredFailure era
forall x.
DijkstraSubUtxoPredFailure era
-> Rep (DijkstraSubUtxoPredFailure era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (DijkstraSubUtxoPredFailure era) x
-> DijkstraSubUtxoPredFailure era
forall era x.
DijkstraSubUtxoPredFailure era
-> Rep (DijkstraSubUtxoPredFailure era) x
$cfrom :: forall era x.
DijkstraSubUtxoPredFailure era
-> Rep (DijkstraSubUtxoPredFailure era) x
from :: forall x.
DijkstraSubUtxoPredFailure era
-> Rep (DijkstraSubUtxoPredFailure era) x
$cto :: forall era x.
Rep (DijkstraSubUtxoPredFailure era) x
-> DijkstraSubUtxoPredFailure era
to :: forall x.
Rep (DijkstraSubUtxoPredFailure era) x
-> DijkstraSubUtxoPredFailure era
Generic)

deriving stock instance
  Eq (PredicateFailure (EraRule "SUBUTXOS" era)) => Eq (DijkstraSubUtxoPredFailure era)

deriving stock instance
  Show (PredicateFailure (EraRule "SUBUTXOS" era)) => Show (DijkstraSubUtxoPredFailure era)

instance
  NoThunks (PredicateFailure (EraRule "SUBUTXOS" era)) =>
  NoThunks (DijkstraSubUtxoPredFailure era)

instance
  NFData (PredicateFailure (EraRule "SUBUTXOS" era)) =>
  NFData (DijkstraSubUtxoPredFailure era)

instance
  ( Era era
  , EncCBOR (PredicateFailure (EraRule "SUBUTXOS" era))
  ) =>
  EncCBOR (DijkstraSubUtxoPredFailure era)
  where
  encCBOR :: DijkstraSubUtxoPredFailure era -> Encoding
encCBOR (SubUtxosFailure PredicateFailure (EraRule "SUBUTXOS" era)
e) = PredicateFailure (EraRule "SUBUTXOS" era) -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR PredicateFailure (EraRule "SUBUTXOS" era)
e

instance
  ( Era era
  , DecCBOR (PredicateFailure (EraRule "SUBUTXOS" era))
  ) =>
  DecCBOR (DijkstraSubUtxoPredFailure era)
  where
  decCBOR :: forall s. Decoder s (DijkstraSubUtxoPredFailure era)
decCBOR = PredicateFailure (EraRule "SUBUTXOS" era)
-> DijkstraSubUtxoPredFailure era
forall era.
PredicateFailure (EraRule "SUBUTXOS" era)
-> DijkstraSubUtxoPredFailure era
SubUtxosFailure (PredicateFailure (EraRule "SUBUTXOS" era)
 -> DijkstraSubUtxoPredFailure era)
-> Decoder s (PredicateFailure (EraRule "SUBUTXOS" era))
-> Decoder s (DijkstraSubUtxoPredFailure era)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Decoder s (PredicateFailure (EraRule "SUBUTXOS" era))
forall s. Decoder s (PredicateFailure (EraRule "SUBUTXOS" era))
forall a s. DecCBOR a => Decoder s a
decCBOR

type instance EraRuleFailure "SUBUTXO" DijkstraEra = DijkstraSubUtxoPredFailure DijkstraEra

type instance EraRuleEvent "SUBUTXO" DijkstraEra = VoidEraRule "SUBUTXO" DijkstraEra

instance InjectRuleFailure "SUBUTXO" DijkstraSubUtxoPredFailure DijkstraEra

instance InjectRuleFailure "SUBUTXO" DijkstraSubUtxosPredFailure DijkstraEra where
  injectFailure :: DijkstraSubUtxosPredFailure DijkstraEra
-> EraRuleFailure "SUBUTXO" DijkstraEra
injectFailure = PredicateFailure (EraRule "SUBUTXOS" DijkstraEra)
-> DijkstraSubUtxoPredFailure DijkstraEra
DijkstraSubUtxosPredFailure DijkstraEra
-> EraRuleFailure "SUBUTXO" DijkstraEra
forall era.
PredicateFailure (EraRule "SUBUTXOS" era)
-> DijkstraSubUtxoPredFailure era
SubUtxosFailure

instance
  ( ConwayEraGov era
  , EraRule "SUBUTXO" era ~ DijkstraSUBUTXO era
  , EraRule "SUBUTXOS" era ~ DijkstraSUBUTXOS era
  , Embed (EraRule "SUBUTXOS" era) (DijkstraSUBUTXO era)
  ) =>
  STS (DijkstraSUBUTXO era)
  where
  type State (DijkstraSUBUTXO era) = UTxOState era
  type Signal (DijkstraSUBUTXO era) = Tx SubTx era
  type Environment (DijkstraSUBUTXO era) = UtxoEnv era
  type BaseM (DijkstraSUBUTXO era) = ShelleyBase
  type PredicateFailure (DijkstraSUBUTXO era) = DijkstraSubUtxoPredFailure era
  type Event (DijkstraSUBUTXO era) = Void

  transitionRules :: [TransitionRule (DijkstraSUBUTXO era)]
transitionRules = [forall era.
(EraRule "SUBUTXO" era ~ DijkstraSUBUTXO era,
 EraRule "SUBUTXOS" era ~ DijkstraSUBUTXOS era,
 Embed (EraRule "SUBUTXOS" era) (DijkstraSUBUTXO era)) =>
TransitionRule (EraRule "SUBUTXO" era)
dijkstraSubUtxoTransition @era]

dijkstraSubUtxoTransition ::
  forall era.
  ( EraRule "SUBUTXO" era ~ DijkstraSUBUTXO era
  , EraRule "SUBUTXOS" era ~ DijkstraSUBUTXOS era
  , Embed (EraRule "SUBUTXOS" era) (DijkstraSUBUTXO era)
  ) =>
  TransitionRule (EraRule "SUBUTXO" era)
dijkstraSubUtxoTransition :: forall era.
(EraRule "SUBUTXO" era ~ DijkstraSUBUTXO era,
 EraRule "SUBUTXOS" era ~ DijkstraSUBUTXOS era,
 Embed (EraRule "SUBUTXOS" era) (DijkstraSUBUTXO era)) =>
TransitionRule (EraRule "SUBUTXO" era)
dijkstraSubUtxoTransition = do
  TRC (env, state, signal) <- Rule
  (DijkstraSUBUTXO era)
  'Transition
  (RuleContext 'Transition (DijkstraSUBUTXO era))
F (Clause (DijkstraSUBUTXO era) 'Transition)
  (TRC (DijkstraSUBUTXO era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
  trans @(EraRule "SUBUTXOS" era) $
    TRC (env, state, signal)

instance
  ( ConwayEraGov era
  , EraRule "SUBUTXOS" era ~ DijkstraSUBUTXOS era
  ) =>
  Embed (DijkstraSUBUTXOS era) (DijkstraSUBUTXO era)
  where
  wrapFailed :: PredicateFailure (DijkstraSUBUTXOS era)
-> PredicateFailure (DijkstraSUBUTXO era)
wrapFailed = PredicateFailure (EraRule "SUBUTXOS" era)
-> DijkstraSubUtxoPredFailure era
PredicateFailure (DijkstraSUBUTXOS era)
-> PredicateFailure (DijkstraSUBUTXO era)
forall era.
PredicateFailure (EraRule "SUBUTXOS" era)
-> DijkstraSubUtxoPredFailure era
SubUtxosFailure
  wrapEvent :: Event (DijkstraSUBUTXOS era) -> Event (DijkstraSUBUTXO era)
wrapEvent = Void -> Void
Event (DijkstraSUBUTXOS era) -> Event (DijkstraSUBUTXO era)
forall a. Void -> a
absurd