{-# 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 #-}
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)
, forall era. UpecState era -> ShelleyGovState era
usGovState :: !(ShelleyGovState era)
}
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