{-# 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.SubUtxow (
  DijkstraSUBUTXOW,
  DijkstraSubUtxowPredFailure (..),
) 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,
  DijkstraSUBUTXOW,
 )
import Cardano.Ledger.Dijkstra.Rules.SubUtxo (
  DijkstraSubUtxoPredFailure,
 )
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 DijkstraSubUtxowPredFailure era
  = SubUtxoFailure (PredicateFailure (EraRule "SUBUTXO" era))
  deriving ((forall x.
 DijkstraSubUtxowPredFailure era
 -> Rep (DijkstraSubUtxowPredFailure era) x)
-> (forall x.
    Rep (DijkstraSubUtxowPredFailure era) x
    -> DijkstraSubUtxowPredFailure era)
-> Generic (DijkstraSubUtxowPredFailure era)
forall x.
Rep (DijkstraSubUtxowPredFailure era) x
-> DijkstraSubUtxowPredFailure era
forall x.
DijkstraSubUtxowPredFailure era
-> Rep (DijkstraSubUtxowPredFailure era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (DijkstraSubUtxowPredFailure era) x
-> DijkstraSubUtxowPredFailure era
forall era x.
DijkstraSubUtxowPredFailure era
-> Rep (DijkstraSubUtxowPredFailure era) x
$cfrom :: forall era x.
DijkstraSubUtxowPredFailure era
-> Rep (DijkstraSubUtxowPredFailure era) x
from :: forall x.
DijkstraSubUtxowPredFailure era
-> Rep (DijkstraSubUtxowPredFailure era) x
$cto :: forall era x.
Rep (DijkstraSubUtxowPredFailure era) x
-> DijkstraSubUtxowPredFailure era
to :: forall x.
Rep (DijkstraSubUtxowPredFailure era) x
-> DijkstraSubUtxowPredFailure era
Generic)

deriving stock instance
  Eq (PredicateFailure (EraRule "SUBUTXO" era)) => Eq (DijkstraSubUtxowPredFailure era)

deriving stock instance
  Show (PredicateFailure (EraRule "SUBUTXO" era)) => Show (DijkstraSubUtxowPredFailure era)

instance
  NoThunks (PredicateFailure (EraRule "SUBUTXO" era)) =>
  NoThunks (DijkstraSubUtxowPredFailure era)

instance
  NFData (PredicateFailure (EraRule "SUBUTXO" era)) =>
  NFData (DijkstraSubUtxowPredFailure era)

instance
  ( Era era
  , EncCBOR (PredicateFailure (EraRule "SUBUTXO" era))
  ) =>
  EncCBOR (DijkstraSubUtxowPredFailure era)
  where
  encCBOR :: DijkstraSubUtxowPredFailure era -> Encoding
encCBOR (SubUtxoFailure PredicateFailure (EraRule "SUBUTXO" era)
e) = PredicateFailure (EraRule "SUBUTXO" era) -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR PredicateFailure (EraRule "SUBUTXO" era)
e

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

type instance EraRuleFailure "SUBUTXOW" DijkstraEra = DijkstraSubUtxowPredFailure DijkstraEra

type instance EraRuleEvent "SUBUTXOW" DijkstraEra = VoidEraRule "SUBUTXOW" DijkstraEra

instance InjectRuleFailure "SUBUTXOW" DijkstraSubUtxowPredFailure DijkstraEra

instance InjectRuleFailure "SUBUTXOW" DijkstraSubUtxoPredFailure DijkstraEra where
  injectFailure :: DijkstraSubUtxoPredFailure DijkstraEra
-> EraRuleFailure "SUBUTXOW" DijkstraEra
injectFailure = PredicateFailure (EraRule "SUBUTXO" DijkstraEra)
-> DijkstraSubUtxowPredFailure DijkstraEra
DijkstraSubUtxoPredFailure DijkstraEra
-> EraRuleFailure "SUBUTXOW" DijkstraEra
forall era.
PredicateFailure (EraRule "SUBUTXO" era)
-> DijkstraSubUtxowPredFailure era
SubUtxoFailure

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

  transitionRules :: [TransitionRule (DijkstraSUBUTXOW era)]
transitionRules = [forall era.
(EraRule "SUBUTXO" era ~ DijkstraSUBUTXO era,
 EraRule "SUBUTXOW" era ~ DijkstraSUBUTXOW era,
 Embed (EraRule "SUBUTXO" era) (DijkstraSUBUTXOW era)) =>
TransitionRule (EraRule "SUBUTXOW" era)
dijkstraSubUtxowTransition @era]

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

instance
  ( ConwayEraGov era
  , EraRule "SUBUTXO" era ~ DijkstraSUBUTXO era
  , EraRule "SUBUTXOS" era ~ DijkstraSUBUTXOS era
  , EraRule "SUBUTXOW" era ~ DijkstraSUBUTXOW era
  ) =>
  Embed (DijkstraSUBUTXO era) (DijkstraSUBUTXOW era)
  where
  wrapFailed :: PredicateFailure (DijkstraSUBUTXO era)
-> PredicateFailure (DijkstraSUBUTXOW era)
wrapFailed = PredicateFailure (EraRule "SUBUTXO" era)
-> DijkstraSubUtxowPredFailure era
PredicateFailure (DijkstraSUBUTXO era)
-> PredicateFailure (DijkstraSUBUTXOW era)
forall era.
PredicateFailure (EraRule "SUBUTXO" era)
-> DijkstraSubUtxowPredFailure era
SubUtxoFailure
  wrapEvent :: Event (DijkstraSUBUTXO era) -> Event (DijkstraSUBUTXOW era)
wrapEvent = Void -> Void
Event (DijkstraSUBUTXO era) -> Event (DijkstraSUBUTXOW era)
forall a. Void -> a
absurd