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

-- | Epoch change registration.
--
-- The rules of this module determine how the update subsystem of the ledger
-- handles the epoch transitions.
module Cardano.Ledger.Shelley.Rules.Upec (
  ShelleyUPEC,
  UpecState (..),
  ShelleyUpecPredFailure (..),
) where

import Cardano.Ledger.BaseTypes (ShelleyBase)
import Cardano.Ledger.Core
import Cardano.Ledger.Shelley.Era (ShelleyUPEC)
import Cardano.Ledger.Shelley.Governance
import Cardano.Ledger.Shelley.LedgerState (
  LedgerState,
  lsCertState,
  lsUTxOState,
 )
import Cardano.Ledger.Shelley.Rules.Newpp (
  NewppEnv (..),
  ShelleyNEWPP,
  ShelleyNewppState (..),
 )
import Control.DeepSeq (NFData)
import Control.State.Transition (
  Embed (..),
  STS (..),
  TRC (..),
  judgmentContext,
  trans,
 )
import Data.Default (Default)
import GHC.Generics (Generic)
import NoThunks.Class (NoThunks (..))

data UpecState era = UpecState
  { forall era. UpecState era -> PParams era
usCurPParams :: !(PParams era)
  -- ^ Current protocol parameters.
  , forall era. UpecState era -> ShelleyGovState era
usGovState :: !(ShelleyGovState era)
  -- ^ State of the protocol update transition system.
  }

deriving stock instance
  (Show (PParams era), Show (PParamsUpdate era)) =>
  Show (UpecState era)

newtype ShelleyUpecPredFailure era
  = NewPpFailure (PredicateFailure (ShelleyNEWPP era))
  deriving (ShelleyUpecPredFailure era -> ShelleyUpecPredFailure era -> Bool
forall era.
ShelleyUpecPredFailure era -> ShelleyUpecPredFailure era -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ShelleyUpecPredFailure era -> ShelleyUpecPredFailure era -> Bool
$c/= :: forall era.
ShelleyUpecPredFailure era -> ShelleyUpecPredFailure era -> Bool
== :: ShelleyUpecPredFailure era -> ShelleyUpecPredFailure era -> Bool
$c== :: forall era.
ShelleyUpecPredFailure era -> ShelleyUpecPredFailure era -> Bool
Eq, Int -> ShelleyUpecPredFailure era -> ShowS
forall era. Int -> ShelleyUpecPredFailure era -> ShowS
forall era. [ShelleyUpecPredFailure era] -> ShowS
forall era. ShelleyUpecPredFailure era -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ShelleyUpecPredFailure era] -> ShowS
$cshowList :: forall era. [ShelleyUpecPredFailure era] -> ShowS
show :: ShelleyUpecPredFailure era -> String
$cshow :: forall era. ShelleyUpecPredFailure era -> String
showsPrec :: Int -> ShelleyUpecPredFailure era -> ShowS
$cshowsPrec :: forall era. Int -> ShelleyUpecPredFailure era -> ShowS
Show, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (ShelleyUpecPredFailure era) x -> ShelleyUpecPredFailure era
forall era x.
ShelleyUpecPredFailure era -> Rep (ShelleyUpecPredFailure era) x
$cto :: forall era x.
Rep (ShelleyUpecPredFailure era) x -> ShelleyUpecPredFailure era
$cfrom :: forall era x.
ShelleyUpecPredFailure era -> Rep (ShelleyUpecPredFailure era) x
Generic)

instance NoThunks (ShelleyUpecPredFailure era)

instance NFData (ShelleyUpecPredFailure era)

instance
  ( EraGov era
  , Default (PParams era)
  , GovState era ~ ShelleyGovState era
  , ProtVerAtMost era 8
  ) =>
  STS (ShelleyUPEC era)
  where
  type State (ShelleyUPEC era) = UpecState era
  type Signal (ShelleyUPEC era) = ()
  type Environment (ShelleyUPEC era) = LedgerState era
  type BaseM (ShelleyUPEC era) = ShelleyBase
  type PredicateFailure (ShelleyUPEC era) = ShelleyUpecPredFailure era
  initialRules :: [InitialRule (ShelleyUPEC era)]
initialRules = []
  transitionRules :: [TransitionRule (ShelleyUPEC era)]
transitionRules =
    [ do
        TRC
          ( Environment (ShelleyUPEC era)
ls
            , UpecState PParams era
pp ShelleyGovState era
ppupState
            , Signal (ShelleyUPEC era)
_
            ) <-
          forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext

        let utxoState :: UTxOState era
utxoState = forall era. LedgerState era -> UTxOState era
lsUTxOState Environment (ShelleyUPEC era)
ls
            ppNew :: PParams era
ppNew = forall era. EraGov era => GovState era -> PParams era
nextEpochPParams ShelleyGovState era
ppupState
        NewppState PParams era
pp' ShelleyGovState era
ppupState' <-
          forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @(ShelleyNEWPP era) forall a b. (a -> b) -> a -> b
$
            forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (forall era. CertState era -> UTxOState era -> NewppEnv era
NewppEnv (forall era. LedgerState era -> CertState era
lsCertState Environment (ShelleyUPEC era)
ls) UTxOState era
utxoState, forall era.
PParams era -> ShelleyGovState era -> ShelleyNewppState era
NewppState PParams era
pp ShelleyGovState era
ppupState, PParams era
ppNew)
        forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! forall era. PParams era -> ShelleyGovState era -> UpecState era
UpecState PParams era
pp' ShelleyGovState era
ppupState'
    ]

instance
  (Era era, STS (ShelleyNEWPP era)) =>
  Embed (ShelleyNEWPP era) (ShelleyUPEC era)
  where
  wrapFailed :: PredicateFailure (ShelleyNEWPP era)
-> PredicateFailure (ShelleyUPEC era)
wrapFailed = forall era.
PredicateFailure (ShelleyNEWPP era) -> ShelleyUpecPredFailure era
NewPpFailure