{-# 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
(ShelleyUpecPredFailure era -> ShelleyUpecPredFailure era -> Bool)
-> (ShelleyUpecPredFailure era
    -> ShelleyUpecPredFailure era -> Bool)
-> Eq (ShelleyUpecPredFailure era)
forall era.
ShelleyUpecPredFailure era -> ShelleyUpecPredFailure era -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall era.
ShelleyUpecPredFailure era -> ShelleyUpecPredFailure era -> Bool
== :: ShelleyUpecPredFailure era -> ShelleyUpecPredFailure era -> Bool
$c/= :: forall era.
ShelleyUpecPredFailure era -> ShelleyUpecPredFailure era -> Bool
/= :: ShelleyUpecPredFailure era -> ShelleyUpecPredFailure era -> Bool
Eq, Int -> ShelleyUpecPredFailure era -> ShowS
[ShelleyUpecPredFailure era] -> ShowS
ShelleyUpecPredFailure era -> String
(Int -> ShelleyUpecPredFailure era -> ShowS)
-> (ShelleyUpecPredFailure era -> String)
-> ([ShelleyUpecPredFailure era] -> ShowS)
-> Show (ShelleyUpecPredFailure era)
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
$cshowsPrec :: forall era. Int -> ShelleyUpecPredFailure era -> ShowS
showsPrec :: Int -> ShelleyUpecPredFailure era -> ShowS
$cshow :: forall era. ShelleyUpecPredFailure era -> String
show :: ShelleyUpecPredFailure era -> String
$cshowList :: forall era. [ShelleyUpecPredFailure era] -> ShowS
showList :: [ShelleyUpecPredFailure era] -> ShowS
Show, (forall x.
 ShelleyUpecPredFailure era -> Rep (ShelleyUpecPredFailure era) x)
-> (forall x.
    Rep (ShelleyUpecPredFailure era) x -> ShelleyUpecPredFailure era)
-> Generic (ShelleyUpecPredFailure era)
forall x.
Rep (ShelleyUpecPredFailure era) x -> ShelleyUpecPredFailure era
forall x.
ShelleyUpecPredFailure era -> Rep (ShelleyUpecPredFailure era) x
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
$cfrom :: forall era x.
ShelleyUpecPredFailure era -> Rep (ShelleyUpecPredFailure era) x
from :: forall x.
ShelleyUpecPredFailure era -> Rep (ShelleyUpecPredFailure era) x
$cto :: forall era x.
Rep (ShelleyUpecPredFailure era) x -> ShelleyUpecPredFailure era
to :: forall x.
Rep (ShelleyUpecPredFailure era) x -> ShelleyUpecPredFailure era
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)
_
            ) <-
          Rule
  (ShelleyUPEC era)
  'Transition
  (RuleContext 'Transition (ShelleyUPEC era))
F (Clause (ShelleyUPEC era) 'Transition) (TRC (ShelleyUPEC era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext

        let utxoState :: UTxOState era
utxoState = LedgerState era -> UTxOState era
forall era. LedgerState era -> UTxOState era
lsUTxOState Environment (ShelleyUPEC era)
LedgerState era
ls
            ppNew :: PParams era
ppNew = GovState era -> PParams era
forall era. EraGov era => GovState era -> PParams era
nextEpochPParams GovState era
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) (RuleContext 'Transition (ShelleyNEWPP era)
 -> Rule (ShelleyUPEC era) 'Transition (State (ShelleyNEWPP era)))
-> RuleContext 'Transition (ShelleyNEWPP era)
-> Rule (ShelleyUPEC era) 'Transition (State (ShelleyNEWPP era))
forall a b. (a -> b) -> a -> b
$
            (Environment (ShelleyNEWPP era), State (ShelleyNEWPP era),
 Signal (ShelleyNEWPP era))
-> TRC (ShelleyNEWPP era)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (CertState era -> UTxOState era -> NewppEnv era
forall era. CertState era -> UTxOState era -> NewppEnv era
NewppEnv (LedgerState era -> CertState era
forall era. LedgerState era -> CertState era
lsCertState Environment (ShelleyUPEC era)
LedgerState era
ls) UTxOState era
utxoState, PParams era -> ShelleyGovState era -> ShelleyNewppState era
forall era.
PParams era -> ShelleyGovState era -> ShelleyNewppState era
NewppState PParams era
pp ShelleyGovState era
ppupState, PParams era
Signal (ShelleyNEWPP era)
ppNew)
        UpecState era
-> F (Clause (ShelleyUPEC era) 'Transition) (UpecState era)
forall a. a -> F (Clause (ShelleyUPEC era) 'Transition) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UpecState era
 -> F (Clause (ShelleyUPEC era) 'Transition) (UpecState era))
-> UpecState era
-> F (Clause (ShelleyUPEC era) 'Transition) (UpecState era)
forall a b. (a -> b) -> a -> b
$! PParams era -> ShelleyGovState era -> UpecState era
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 = PredicateFailure (ShelleyNEWPP era)
-> PredicateFailure (ShelleyUPEC era)
PredicateFailure (ShelleyNEWPP era) -> ShelleyUpecPredFailure era
forall era.
PredicateFailure (ShelleyNEWPP era) -> ShelleyUpecPredFailure era
NewPpFailure