{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Cardano.Ledger.Shelley.Rules.Ledgers (
  ShelleyLEDGERS,
  ShelleyLedgersEnv (..),
  ShelleyLedgersPredFailure (..),
  ShelleyLedgersEvent (..),
  PredicateFailure,
)
where

import Cardano.Ledger.BaseTypes (ShelleyBase)
import Cardano.Ledger.Binary (DecCBOR (..), EncCBOR (..))
import Cardano.Ledger.Core
import Cardano.Ledger.Keys (DSignable, Hash)
import Cardano.Ledger.Shelley.Era (ShelleyEra, ShelleyLEDGERS)
import Cardano.Ledger.Shelley.LedgerState (AccountState, LedgerState)
import Cardano.Ledger.Shelley.Rules.Deleg (ShelleyDelegPredFailure)
import Cardano.Ledger.Shelley.Rules.Delegs (ShelleyDelegsPredFailure)
import Cardano.Ledger.Shelley.Rules.Delpl (ShelleyDelplPredFailure)
import Cardano.Ledger.Shelley.Rules.Ledger (
  LedgerEnv (..),
  ShelleyLEDGER,
  ShelleyLedgerEvent,
  ShelleyLedgerPredFailure,
 )
import Cardano.Ledger.Shelley.Rules.Pool (ShelleyPoolPredFailure)
import Cardano.Ledger.Shelley.Rules.Ppup (ShelleyPpupPredFailure)
import Cardano.Ledger.Shelley.Rules.Utxo (ShelleyUtxoPredFailure)
import Cardano.Ledger.Shelley.Rules.Utxow (ShelleyUtxowPredFailure)
import Cardano.Ledger.Slot (SlotNo)
import Control.Monad (foldM)
import Control.State.Transition (
  Embed (..),
  STS (..),
  TRC (..),
  TransitionRule,
  judgmentContext,
  trans,
 )
import Data.Default.Class (Default)
import Data.Foldable (toList)
import Data.Sequence (Seq)
import GHC.Generics (Generic)
import NoThunks.Class (NoThunks (..))

data ShelleyLedgersEnv era = LedgersEnv
  { forall era. ShelleyLedgersEnv era -> SlotNo
ledgersSlotNo :: SlotNo
  , forall era. ShelleyLedgersEnv era -> PParams era
ledgersPp :: PParams era
  , forall era. ShelleyLedgersEnv era -> AccountState
ledgersAccount :: AccountState
  }

newtype ShelleyLedgersPredFailure era
  = LedgerFailure (PredicateFailure (EraRule "LEDGER" era)) -- Subtransition Failures
  deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (ShelleyLedgersPredFailure era) x
-> ShelleyLedgersPredFailure era
forall era x.
ShelleyLedgersPredFailure era
-> Rep (ShelleyLedgersPredFailure era) x
$cto :: forall era x.
Rep (ShelleyLedgersPredFailure era) x
-> ShelleyLedgersPredFailure era
$cfrom :: forall era x.
ShelleyLedgersPredFailure era
-> Rep (ShelleyLedgersPredFailure era) x
Generic)

type instance EraRuleFailure "LEDGERS" (ShelleyEra c) = ShelleyLedgersPredFailure (ShelleyEra c)

type instance EraRuleEvent "LEDGERS" (ShelleyEra c) = ShelleyLedgersEvent (ShelleyEra c)

instance InjectRuleFailure "LEDGERS" ShelleyLedgersPredFailure (ShelleyEra c)

instance InjectRuleFailure "LEDGERS" ShelleyLedgerPredFailure (ShelleyEra c) where
  injectFailure :: ShelleyLedgerPredFailure (ShelleyEra c)
-> EraRuleFailure "LEDGERS" (ShelleyEra c)
injectFailure = forall era.
PredicateFailure (EraRule "LEDGER" era)
-> ShelleyLedgersPredFailure era
LedgerFailure

instance InjectRuleFailure "LEDGERS" ShelleyUtxowPredFailure (ShelleyEra c) where
  injectFailure :: ShelleyUtxowPredFailure (ShelleyEra c)
-> EraRuleFailure "LEDGERS" (ShelleyEra c)
injectFailure = forall era.
PredicateFailure (EraRule "LEDGER" era)
-> ShelleyLedgersPredFailure era
LedgerFailure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure

instance InjectRuleFailure "LEDGERS" ShelleyUtxoPredFailure (ShelleyEra c) where
  injectFailure :: ShelleyUtxoPredFailure (ShelleyEra c)
-> EraRuleFailure "LEDGERS" (ShelleyEra c)
injectFailure = forall era.
PredicateFailure (EraRule "LEDGER" era)
-> ShelleyLedgersPredFailure era
LedgerFailure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure

instance InjectRuleFailure "LEDGERS" ShelleyPpupPredFailure (ShelleyEra c) where
  injectFailure :: ShelleyPpupPredFailure (ShelleyEra c)
-> EraRuleFailure "LEDGERS" (ShelleyEra c)
injectFailure = forall era.
PredicateFailure (EraRule "LEDGER" era)
-> ShelleyLedgersPredFailure era
LedgerFailure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure

instance InjectRuleFailure "LEDGERS" ShelleyDelegsPredFailure (ShelleyEra c) where
  injectFailure :: ShelleyDelegsPredFailure (ShelleyEra c)
-> EraRuleFailure "LEDGERS" (ShelleyEra c)
injectFailure = forall era.
PredicateFailure (EraRule "LEDGER" era)
-> ShelleyLedgersPredFailure era
LedgerFailure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure

instance InjectRuleFailure "LEDGERS" ShelleyDelplPredFailure (ShelleyEra c) where
  injectFailure :: ShelleyDelplPredFailure (ShelleyEra c)
-> EraRuleFailure "LEDGERS" (ShelleyEra c)
injectFailure = forall era.
PredicateFailure (EraRule "LEDGER" era)
-> ShelleyLedgersPredFailure era
LedgerFailure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure

instance InjectRuleFailure "LEDGERS" ShelleyPoolPredFailure (ShelleyEra c) where
  injectFailure :: ShelleyPoolPredFailure (ShelleyEra c)
-> EraRuleFailure "LEDGERS" (ShelleyEra c)
injectFailure = forall era.
PredicateFailure (EraRule "LEDGER" era)
-> ShelleyLedgersPredFailure era
LedgerFailure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure

instance InjectRuleFailure "LEDGERS" ShelleyDelegPredFailure (ShelleyEra c) where
  injectFailure :: ShelleyDelegPredFailure (ShelleyEra c)
-> EraRuleFailure "LEDGERS" (ShelleyEra c)
injectFailure = forall era.
PredicateFailure (EraRule "LEDGER" era)
-> ShelleyLedgersPredFailure era
LedgerFailure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure

newtype ShelleyLedgersEvent era
  = LedgerEvent (Event (EraRule "LEDGER" era))

deriving stock instance
  ( Era era
  , Show (PredicateFailure (EraRule "LEDGER" era))
  ) =>
  Show (ShelleyLedgersPredFailure era)

deriving stock instance
  ( Era era
  , Eq (PredicateFailure (EraRule "LEDGER" era))
  ) =>
  Eq (ShelleyLedgersPredFailure era)

instance
  ( Era era
  , NoThunks (PredicateFailure (EraRule "LEDGER" era))
  ) =>
  NoThunks (ShelleyLedgersPredFailure era)

instance
  ( Era era
  , EncCBOR (PredicateFailure (EraRule "LEDGER" era))
  ) =>
  EncCBOR (ShelleyLedgersPredFailure era)
  where
  encCBOR :: ShelleyLedgersPredFailure era -> Encoding
encCBOR (LedgerFailure PredicateFailure (EraRule "LEDGER" era)
e) = forall a. EncCBOR a => a -> Encoding
encCBOR PredicateFailure (EraRule "LEDGER" era)
e

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

instance
  ( Era era
  , Embed (EraRule "LEDGER" era) (ShelleyLEDGERS era)
  , Environment (EraRule "LEDGER" era) ~ LedgerEnv era
  , State (EraRule "LEDGER" era) ~ LedgerState era
  , Signal (EraRule "LEDGER" era) ~ Tx era
  , DSignable (EraCrypto era) (Hash (EraCrypto era) EraIndependentTxBody)
  , Default (LedgerState era)
  ) =>
  STS (ShelleyLEDGERS era)
  where
  type State (ShelleyLEDGERS era) = LedgerState era
  type Signal (ShelleyLEDGERS era) = Seq (Tx era)
  type Environment (ShelleyLEDGERS era) = ShelleyLedgersEnv era
  type BaseM (ShelleyLEDGERS era) = ShelleyBase
  type PredicateFailure (ShelleyLEDGERS era) = ShelleyLedgersPredFailure era
  type Event (ShelleyLEDGERS era) = ShelleyLedgersEvent era

  transitionRules :: [TransitionRule (ShelleyLEDGERS era)]
transitionRules = [forall era.
(Embed (EraRule "LEDGER" era) (ShelleyLEDGERS era),
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 Signal (EraRule "LEDGER" era) ~ Tx era) =>
TransitionRule (ShelleyLEDGERS era)
ledgersTransition]

ledgersTransition ::
  forall era.
  ( Embed (EraRule "LEDGER" era) (ShelleyLEDGERS era)
  , Environment (EraRule "LEDGER" era) ~ LedgerEnv era
  , State (EraRule "LEDGER" era) ~ LedgerState era
  , Signal (EraRule "LEDGER" era) ~ Tx era
  ) =>
  TransitionRule (ShelleyLEDGERS era)
ledgersTransition :: forall era.
(Embed (EraRule "LEDGER" era) (ShelleyLEDGERS era),
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 Signal (EraRule "LEDGER" era) ~ Tx era) =>
TransitionRule (ShelleyLEDGERS era)
ledgersTransition = do
  TRC (LedgersEnv SlotNo
slot PParams era
pp AccountState
account, State (ShelleyLEDGERS era)
ls, Signal (ShelleyLEDGERS era)
txwits) <- forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
  forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM
    ( \ !LedgerState era
ls' (TxIx
ix, Tx era
tx) ->
        forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @(EraRule "LEDGER" era) forall a b. (a -> b) -> a -> b
$
          forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (forall era.
SlotNo
-> TxIx -> PParams era -> AccountState -> Bool -> LedgerEnv era
LedgerEnv SlotNo
slot TxIx
ix PParams era
pp AccountState
account Bool
False, LedgerState era
ls', Tx era
tx)
    )
    State (ShelleyLEDGERS era)
ls
    forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip [forall a. Bounded a => a
minBound ..]
    forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Signal (ShelleyLEDGERS era)
txwits

instance
  ( Era era
  , STS (ShelleyLEDGER era)
  , PredicateFailure (EraRule "LEDGER" era) ~ ShelleyLedgerPredFailure era
  , Event (EraRule "LEDGER" era) ~ ShelleyLedgerEvent era
  ) =>
  Embed (ShelleyLEDGER era) (ShelleyLEDGERS era)
  where
  wrapFailed :: PredicateFailure (ShelleyLEDGER era)
-> PredicateFailure (ShelleyLEDGERS era)
wrapFailed = forall era.
PredicateFailure (EraRule "LEDGER" era)
-> ShelleyLedgersPredFailure era
LedgerFailure
  wrapEvent :: Event (ShelleyLEDGER era) -> Event (ShelleyLEDGERS era)
wrapEvent = forall era. Event (EraRule "LEDGER" era) -> ShelleyLedgersEvent era
LedgerEvent