{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE EmptyDataDeriving #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}
#if __GLASGOW_HASKELL__ >= 910
-- See https://gitlab.haskell.org/ghc/ghc/-/issues/27342
{-# OPTIONS_GHC -fno-spec-eval #-}
#endif

module Cardano.Ledger.Dijkstra.Rules.SubCert (
  SUBCERT,
  DijkstraSubCertPredFailure (..),
  DijkstraSubCertEvent (..),
) where

import Cardano.Ledger.BaseTypes (
  ShelleyBase,
 )
import Cardano.Ledger.Binary (
  DecCBOR (..),
  EncCBOR (..),
 )
import Cardano.Ledger.Binary.Coders
import Cardano.Ledger.Conway.Core
import Cardano.Ledger.Conway.Governance (ConwayEraGov)
import qualified Cardano.Ledger.Conway.Rules as Conway
import Cardano.Ledger.Conway.State
import Cardano.Ledger.Dijkstra.Era (
  DijkstraEra,
  SUBCERT,
  SUBDELEG,
  SUBGOVCERT,
  SUBPOOL,
 )
import Cardano.Ledger.Dijkstra.Rules.GovCert (DijkstraGovCertPredFailure)
import Cardano.Ledger.Dijkstra.Rules.SubDeleg (DijkstraSubDelegPredFailure)
import Cardano.Ledger.Dijkstra.Rules.SubGovCert (DijkstraSubGovCertPredFailure)
import Cardano.Ledger.Dijkstra.Rules.SubPool (DijkstraSubPoolEvent, DijkstraSubPoolPredFailure)
import Cardano.Ledger.Dijkstra.TxCert
import qualified Cardano.Ledger.Shelley.Rules as Shelley
import Control.DeepSeq (NFData)
import Control.State.Transition.Extended
import Data.Void (absurd)
import GHC.Generics (Generic)
import Lens.Micro

data DijkstraSubCertPredFailure era
  = SubDelegFailure (PredicateFailure (EraRule "SUBDELEG" era))
  | SubPoolFailure (PredicateFailure (EraRule "SUBPOOL" era))
  | SubGovCertFailure (PredicateFailure (EraRule "SUBGOVCERT" era))
  deriving ((forall x.
 DijkstraSubCertPredFailure era
 -> Rep (DijkstraSubCertPredFailure era) x)
-> (forall x.
    Rep (DijkstraSubCertPredFailure era) x
    -> DijkstraSubCertPredFailure era)
-> Generic (DijkstraSubCertPredFailure era)
forall x.
Rep (DijkstraSubCertPredFailure era) x
-> DijkstraSubCertPredFailure era
forall x.
DijkstraSubCertPredFailure era
-> Rep (DijkstraSubCertPredFailure era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (DijkstraSubCertPredFailure era) x
-> DijkstraSubCertPredFailure era
forall era x.
DijkstraSubCertPredFailure era
-> Rep (DijkstraSubCertPredFailure era) x
$cfrom :: forall era x.
DijkstraSubCertPredFailure era
-> Rep (DijkstraSubCertPredFailure era) x
from :: forall x.
DijkstraSubCertPredFailure era
-> Rep (DijkstraSubCertPredFailure era) x
$cto :: forall era x.
Rep (DijkstraSubCertPredFailure era) x
-> DijkstraSubCertPredFailure era
to :: forall x.
Rep (DijkstraSubCertPredFailure era) x
-> DijkstraSubCertPredFailure era
Generic)

deriving stock instance
  ( Eq (PredicateFailure (EraRule "SUBDELEG" era))
  , Eq (PredicateFailure (EraRule "SUBPOOL" era))
  , Eq (PredicateFailure (EraRule "SUBGOVCERT" era))
  ) =>
  Eq (DijkstraSubCertPredFailure era)

deriving stock instance
  ( Ord (PredicateFailure (EraRule "SUBDELEG" era))
  , Ord (PredicateFailure (EraRule "SUBPOOL" era))
  , Ord (PredicateFailure (EraRule "SUBGOVCERT" era))
  ) =>
  Ord (DijkstraSubCertPredFailure era)

deriving stock instance
  ( Show (PredicateFailure (EraRule "SUBDELEG" era))
  , Show (PredicateFailure (EraRule "SUBPOOL" era))
  , Show (PredicateFailure (EraRule "SUBGOVCERT" era))
  ) =>
  Show (DijkstraSubCertPredFailure era)

instance
  ( NFData (PredicateFailure (EraRule "SUBDELEG" era))
  , NFData (PredicateFailure (EraRule "SUBPOOL" era))
  , NFData (PredicateFailure (EraRule "SUBGOVCERT" era))
  ) =>
  NFData (DijkstraSubCertPredFailure era)

instance
  ( Era era
  , EncCBOR (PredicateFailure (EraRule "SUBDELEG" era))
  , EncCBOR (PredicateFailure (EraRule "SUBPOOL" era))
  , EncCBOR (PredicateFailure (EraRule "SUBGOVCERT" era))
  ) =>
  EncCBOR (DijkstraSubCertPredFailure era)
  where
  encCBOR :: DijkstraSubCertPredFailure era -> Encoding
encCBOR =
    Encode Open (DijkstraSubCertPredFailure era) -> Encoding
forall (w :: Wrapped) t. Encode w t -> Encoding
encode (Encode Open (DijkstraSubCertPredFailure era) -> Encoding)
-> (DijkstraSubCertPredFailure era
    -> Encode Open (DijkstraSubCertPredFailure era))
-> DijkstraSubCertPredFailure era
-> Encoding
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
      SubDelegFailure PredicateFailure (EraRule "SUBDELEG" era)
x -> (PredicateFailure (EraRule "SUBDELEG" era)
 -> DijkstraSubCertPredFailure era)
-> Word
-> Encode
     Open
     (PredicateFailure (EraRule "SUBDELEG" era)
      -> DijkstraSubCertPredFailure era)
forall t. t -> Word -> Encode Open t
Sum (forall era.
PredicateFailure (EraRule "SUBDELEG" era)
-> DijkstraSubCertPredFailure era
SubDelegFailure @era) Word
1 Encode
  Open
  (PredicateFailure (EraRule "SUBDELEG" era)
   -> DijkstraSubCertPredFailure era)
-> Encode
     (Closed Dense) (PredicateFailure (EraRule "SUBDELEG" era))
-> Encode Open (DijkstraSubCertPredFailure era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode (Closed r) a -> Encode w t
!> PredicateFailure (EraRule "SUBDELEG" era)
-> Encode
     (Closed Dense) (PredicateFailure (EraRule "SUBDELEG" era))
forall t. EncCBOR t => t -> Encode (Closed Dense) t
To PredicateFailure (EraRule "SUBDELEG" era)
x
      SubPoolFailure PredicateFailure (EraRule "SUBPOOL" era)
x -> (PredicateFailure (EraRule "SUBPOOL" era)
 -> DijkstraSubCertPredFailure era)
-> Word
-> Encode
     Open
     (PredicateFailure (EraRule "SUBPOOL" era)
      -> DijkstraSubCertPredFailure era)
forall t. t -> Word -> Encode Open t
Sum (forall era.
PredicateFailure (EraRule "SUBPOOL" era)
-> DijkstraSubCertPredFailure era
SubPoolFailure @era) Word
2 Encode
  Open
  (PredicateFailure (EraRule "SUBPOOL" era)
   -> DijkstraSubCertPredFailure era)
-> Encode (Closed Dense) (PredicateFailure (EraRule "SUBPOOL" era))
-> Encode Open (DijkstraSubCertPredFailure era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode (Closed r) a -> Encode w t
!> PredicateFailure (EraRule "SUBPOOL" era)
-> Encode (Closed Dense) (PredicateFailure (EraRule "SUBPOOL" era))
forall t. EncCBOR t => t -> Encode (Closed Dense) t
To PredicateFailure (EraRule "SUBPOOL" era)
x
      SubGovCertFailure PredicateFailure (EraRule "SUBGOVCERT" era)
x -> (PredicateFailure (EraRule "SUBGOVCERT" era)
 -> DijkstraSubCertPredFailure era)
-> Word
-> Encode
     Open
     (PredicateFailure (EraRule "SUBGOVCERT" era)
      -> DijkstraSubCertPredFailure era)
forall t. t -> Word -> Encode Open t
Sum (forall era.
PredicateFailure (EraRule "SUBGOVCERT" era)
-> DijkstraSubCertPredFailure era
SubGovCertFailure @era) Word
3 Encode
  Open
  (PredicateFailure (EraRule "SUBGOVCERT" era)
   -> DijkstraSubCertPredFailure era)
-> Encode
     (Closed Dense) (PredicateFailure (EraRule "SUBGOVCERT" era))
-> Encode Open (DijkstraSubCertPredFailure era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode (Closed r) a -> Encode w t
!> PredicateFailure (EraRule "SUBGOVCERT" era)
-> Encode
     (Closed Dense) (PredicateFailure (EraRule "SUBGOVCERT" era))
forall t. EncCBOR t => t -> Encode (Closed Dense) t
To PredicateFailure (EraRule "SUBGOVCERT" era)
x

instance
  ( Era era
  , DecCBOR (PredicateFailure (EraRule "SUBDELEG" era))
  , DecCBOR (PredicateFailure (EraRule "SUBPOOL" era))
  , DecCBOR (PredicateFailure (EraRule "SUBGOVCERT" era))
  ) =>
  DecCBOR (DijkstraSubCertPredFailure era)
  where
  decCBOR :: forall s. Decoder s (DijkstraSubCertPredFailure era)
decCBOR =
    Decode (Closed Dense) (DijkstraSubCertPredFailure era)
-> Decoder s (DijkstraSubCertPredFailure era)
forall t (w :: Wrapped) s. Typeable t => Decode w t -> Decoder s t
decode (Decode (Closed Dense) (DijkstraSubCertPredFailure era)
 -> Decoder s (DijkstraSubCertPredFailure era))
-> Decode (Closed Dense) (DijkstraSubCertPredFailure era)
-> Decoder s (DijkstraSubCertPredFailure era)
forall a b. (a -> b) -> a -> b
$ Text
-> (Word -> Decode Open (DijkstraSubCertPredFailure era))
-> Decode (Closed Dense) (DijkstraSubCertPredFailure era)
forall t.
Text -> (Word -> Decode Open t) -> Decode (Closed Dense) t
Summands Text
"DijkstraSubCertPredFailure" ((Word -> Decode Open (DijkstraSubCertPredFailure era))
 -> Decode (Closed Dense) (DijkstraSubCertPredFailure era))
-> (Word -> Decode Open (DijkstraSubCertPredFailure era))
-> Decode (Closed Dense) (DijkstraSubCertPredFailure era)
forall a b. (a -> b) -> a -> b
$ \case
      Word
1 -> (PredicateFailure (EraRule "SUBDELEG" era)
 -> DijkstraSubCertPredFailure era)
-> Decode
     Open
     (PredicateFailure (EraRule "SUBDELEG" era)
      -> DijkstraSubCertPredFailure era)
forall t. t -> Decode Open t
SumD PredicateFailure (EraRule "SUBDELEG" era)
-> DijkstraSubCertPredFailure era
forall era.
PredicateFailure (EraRule "SUBDELEG" era)
-> DijkstraSubCertPredFailure era
SubDelegFailure Decode
  Open
  (PredicateFailure (EraRule "SUBDELEG" era)
   -> DijkstraSubCertPredFailure era)
-> Decode
     (Closed (ZonkAny 0)) (PredicateFailure (EraRule "SUBDELEG" era))
-> Decode Open (DijkstraSubCertPredFailure era)
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode (Closed w) a -> Decode w1 t
<! Decode
  (Closed (ZonkAny 0)) (PredicateFailure (EraRule "SUBDELEG" era))
forall t (w :: Wrapped). DecCBOR t => Decode w t
From
      Word
2 -> (PredicateFailure (EraRule "SUBPOOL" era)
 -> DijkstraSubCertPredFailure era)
-> Decode
     Open
     (PredicateFailure (EraRule "SUBPOOL" era)
      -> DijkstraSubCertPredFailure era)
forall t. t -> Decode Open t
SumD PredicateFailure (EraRule "SUBPOOL" era)
-> DijkstraSubCertPredFailure era
forall era.
PredicateFailure (EraRule "SUBPOOL" era)
-> DijkstraSubCertPredFailure era
SubPoolFailure Decode
  Open
  (PredicateFailure (EraRule "SUBPOOL" era)
   -> DijkstraSubCertPredFailure era)
-> Decode
     (Closed (ZonkAny 1)) (PredicateFailure (EraRule "SUBPOOL" era))
-> Decode Open (DijkstraSubCertPredFailure era)
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode (Closed w) a -> Decode w1 t
<! Decode
  (Closed (ZonkAny 1)) (PredicateFailure (EraRule "SUBPOOL" era))
forall t (w :: Wrapped). DecCBOR t => Decode w t
From
      Word
3 -> (PredicateFailure (EraRule "SUBGOVCERT" era)
 -> DijkstraSubCertPredFailure era)
-> Decode
     Open
     (PredicateFailure (EraRule "SUBGOVCERT" era)
      -> DijkstraSubCertPredFailure era)
forall t. t -> Decode Open t
SumD PredicateFailure (EraRule "SUBGOVCERT" era)
-> DijkstraSubCertPredFailure era
forall era.
PredicateFailure (EraRule "SUBGOVCERT" era)
-> DijkstraSubCertPredFailure era
SubGovCertFailure Decode
  Open
  (PredicateFailure (EraRule "SUBGOVCERT" era)
   -> DijkstraSubCertPredFailure era)
-> Decode
     (Closed (ZonkAny 2)) (PredicateFailure (EraRule "SUBGOVCERT" era))
-> Decode Open (DijkstraSubCertPredFailure era)
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode (Closed w) a -> Decode w1 t
<! Decode
  (Closed (ZonkAny 2)) (PredicateFailure (EraRule "SUBGOVCERT" era))
forall t (w :: Wrapped). DecCBOR t => Decode w t
From
      Word
n -> Word -> Decode Open (DijkstraSubCertPredFailure era)
forall (w :: Wrapped) t. Word -> Decode w t
Invalid Word
n

type instance EraRuleFailure "SUBCERT" DijkstraEra = DijkstraSubCertPredFailure DijkstraEra

type instance EraRuleEvent "SUBCERT" DijkstraEra = DijkstraSubCertEvent DijkstraEra

instance InjectRuleFailure "SUBCERT" DijkstraSubCertPredFailure DijkstraEra

instance InjectRuleFailure "SUBCERT" DijkstraSubDelegPredFailure DijkstraEra where
  injectFailure :: DijkstraSubDelegPredFailure DijkstraEra
-> EraRuleFailure "SUBCERT" DijkstraEra
injectFailure = PredicateFailure (EraRule "SUBDELEG" DijkstraEra)
-> DijkstraSubCertPredFailure DijkstraEra
DijkstraSubDelegPredFailure DijkstraEra
-> EraRuleFailure "SUBCERT" DijkstraEra
forall era.
PredicateFailure (EraRule "SUBDELEG" era)
-> DijkstraSubCertPredFailure era
SubDelegFailure

instance InjectRuleFailure "SUBCERT" DijkstraSubPoolPredFailure DijkstraEra where
  injectFailure :: DijkstraSubPoolPredFailure DijkstraEra
-> EraRuleFailure "SUBCERT" DijkstraEra
injectFailure = PredicateFailure (EraRule "SUBPOOL" DijkstraEra)
-> DijkstraSubCertPredFailure DijkstraEra
DijkstraSubPoolPredFailure DijkstraEra
-> EraRuleFailure "SUBCERT" DijkstraEra
forall era.
PredicateFailure (EraRule "SUBPOOL" era)
-> DijkstraSubCertPredFailure era
SubPoolFailure

instance InjectRuleFailure "SUBCERT" DijkstraSubGovCertPredFailure DijkstraEra where
  injectFailure :: DijkstraSubGovCertPredFailure DijkstraEra
-> EraRuleFailure "SUBCERT" DijkstraEra
injectFailure = PredicateFailure (EraRule "SUBGOVCERT" DijkstraEra)
-> DijkstraSubCertPredFailure DijkstraEra
DijkstraSubGovCertPredFailure DijkstraEra
-> EraRuleFailure "SUBCERT" DijkstraEra
forall era.
PredicateFailure (EraRule "SUBGOVCERT" era)
-> DijkstraSubCertPredFailure era
SubGovCertFailure

instance InjectRuleFailure "SUBCERT" Conway.ConwayCertPredFailure DijkstraEra where
  injectFailure :: ConwayCertPredFailure DijkstraEra
-> EraRuleFailure "SUBCERT" DijkstraEra
injectFailure = ConwayCertPredFailure DijkstraEra
-> EraRuleFailure "SUBCERT" DijkstraEra
ConwayCertPredFailure DijkstraEra
-> DijkstraSubCertPredFailure DijkstraEra
forall era.
(InjectRuleFailure "SUBDELEG" ConwayDelegPredFailure era,
 PredicateFailure (EraRule "DELEG" era)
 ~ ConwayDelegPredFailure era,
 InjectRuleFailure "SUBPOOL" ShelleyPoolPredFailure era,
 PredicateFailure (EraRule "POOL" era) ~ ShelleyPoolPredFailure era,
 InjectRuleFailure "SUBGOVCERT" DijkstraGovCertPredFailure era,
 PredicateFailure (EraRule "GOVCERT" era)
 ~ DijkstraGovCertPredFailure era) =>
ConwayCertPredFailure era -> DijkstraSubCertPredFailure era
conwayToDijkstraSubCertPredFailure

instance InjectRuleEvent "SUBCERT" DijkstraSubCertEvent DijkstraEra

newtype DijkstraSubCertEvent era = SubPoolEvent (Event (EraRule "SUBPOOL" era))
  deriving ((forall x.
 DijkstraSubCertEvent era -> Rep (DijkstraSubCertEvent era) x)
-> (forall x.
    Rep (DijkstraSubCertEvent era) x -> DijkstraSubCertEvent era)
-> Generic (DijkstraSubCertEvent era)
forall x.
Rep (DijkstraSubCertEvent era) x -> DijkstraSubCertEvent era
forall x.
DijkstraSubCertEvent era -> Rep (DijkstraSubCertEvent era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (DijkstraSubCertEvent era) x -> DijkstraSubCertEvent era
forall era x.
DijkstraSubCertEvent era -> Rep (DijkstraSubCertEvent era) x
$cfrom :: forall era x.
DijkstraSubCertEvent era -> Rep (DijkstraSubCertEvent era) x
from :: forall x.
DijkstraSubCertEvent era -> Rep (DijkstraSubCertEvent era) x
$cto :: forall era x.
Rep (DijkstraSubCertEvent era) x -> DijkstraSubCertEvent era
to :: forall x.
Rep (DijkstraSubCertEvent era) x -> DijkstraSubCertEvent era
Generic)

deriving instance Eq (Event (EraRule "SUBPOOL" era)) => Eq (DijkstraSubCertEvent era)

instance NFData (Event (EraRule "SUBPOOL" era)) => NFData (DijkstraSubCertEvent era)

instance
  ( ConwayEraGov era
  , ConwayEraCertState era
  , EraRule "SUBCERT" era ~ SUBCERT era
  , EraRule "SUBDELEG" era ~ SUBDELEG era
  , EraRule "SUBPOOL" era ~ SUBPOOL era
  , EraRule "SUBGOVCERT" era ~ SUBGOVCERT era
  , Embed (EraRule "SUBDELEG" era) (SUBCERT era)
  , Embed (EraRule "SUBPOOL" era) (SUBCERT era)
  , Embed (EraRule "SUBGOVCERT" era) (SUBCERT era)
  , TxCert era ~ DijkstraTxCert era
  ) =>
  STS (SUBCERT era)
  where
  type State (SUBCERT era) = CertState era
  type Signal (SUBCERT era) = TxCert era
  type Environment (SUBCERT era) = Conway.CertEnv era
  type BaseM (SUBCERT era) = ShelleyBase
  type PredicateFailure (SUBCERT era) = DijkstraSubCertPredFailure era
  type Event (SUBCERT era) = DijkstraSubCertEvent era

  transitionRules :: [TransitionRule (SUBCERT era)]
transitionRules = [forall era.
(ConwayEraCertState era, EraRule "SUBCERT" era ~ SUBCERT era,
 EraRule "SUBDELEG" era ~ SUBDELEG era,
 EraRule "SUBPOOL" era ~ SUBPOOL era,
 EraRule "SUBGOVCERT" era ~ SUBGOVCERT era,
 Embed (EraRule "SUBDELEG" era) (SUBCERT era),
 Embed (EraRule "SUBPOOL" era) (SUBCERT era),
 Embed (EraRule "SUBGOVCERT" era) (SUBCERT era),
 TxCert era ~ DijkstraTxCert era) =>
TransitionRule (EraRule "SUBCERT" era)
dijkstraSubCertTransition @era]

dijkstraSubCertTransition ::
  forall era.
  ( ConwayEraCertState era
  , EraRule "SUBCERT" era ~ SUBCERT era
  , EraRule "SUBDELEG" era ~ SUBDELEG era
  , EraRule "SUBPOOL" era ~ SUBPOOL era
  , EraRule "SUBGOVCERT" era ~ SUBGOVCERT era
  , Embed (EraRule "SUBDELEG" era) (SUBCERT era)
  , Embed (EraRule "SUBPOOL" era) (SUBCERT era)
  , Embed (EraRule "SUBGOVCERT" era) (SUBCERT era)
  , TxCert era ~ DijkstraTxCert era
  ) =>
  TransitionRule (EraRule "SUBCERT" era)
dijkstraSubCertTransition :: forall era.
(ConwayEraCertState era, EraRule "SUBCERT" era ~ SUBCERT era,
 EraRule "SUBDELEG" era ~ SUBDELEG era,
 EraRule "SUBPOOL" era ~ SUBPOOL era,
 EraRule "SUBGOVCERT" era ~ SUBGOVCERT era,
 Embed (EraRule "SUBDELEG" era) (SUBCERT era),
 Embed (EraRule "SUBPOOL" era) (SUBCERT era),
 Embed (EraRule "SUBGOVCERT" era) (SUBCERT era),
 TxCert era ~ DijkstraTxCert era) =>
TransitionRule (EraRule "SUBCERT" era)
dijkstraSubCertTransition = do
  TRC (Conway.CertEnv pp currentEpoch committee committeeProposals, certState, c) <- Rule
  (SUBCERT era) 'Transition (RuleContext 'Transition (SUBCERT era))
F (Clause (SUBCERT era) 'Transition) (TRC (SUBCERT era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
  let
    certPState = CertState era
State (SUBCERT era)
certState CertState era
-> Getting (PState era) (CertState era) (PState era) -> PState era
forall s a. s -> Getting a s a -> a
^. Getting (PState era) (CertState era) (PState era)
forall era. EraCertState era => Lens' (CertState era) (PState era)
Lens' (CertState era) (PState era)
certPStateL
    pools = PState era -> Map (KeyHash StakePool) StakePoolState
forall era. PState era -> Map (KeyHash StakePool) StakePoolState
psStakePools PState era
certPState
  case c of
    DijkstraTxCertDeleg DijkstraDelegCert
delegCert ->
      forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @(EraRule "SUBDELEG" era) (RuleContext 'Transition (EraRule "SUBDELEG" era)
 -> Rule (SUBCERT era) 'Transition (State (EraRule "SUBDELEG" era)))
-> RuleContext 'Transition (EraRule "SUBDELEG" era)
-> Rule (SUBCERT era) 'Transition (State (EraRule "SUBDELEG" era))
forall a b. (a -> b) -> a -> b
$
        (Environment (SUBDELEG era), State (SUBDELEG era),
 Signal (SUBDELEG era))
-> TRC (SUBDELEG era)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (PParams era
-> Map (KeyHash StakePool) StakePoolState -> ConwayDelegEnv era
forall era.
PParams era
-> Map (KeyHash StakePool) StakePoolState -> ConwayDelegEnv era
Conway.ConwayDelegEnv PParams era
pp Map (KeyHash StakePool) StakePoolState
pools, State (SUBDELEG era)
State (SUBCERT era)
certState, DijkstraDelegCert -> ConwayDelegCert
dijkstraToConwayDelegCert DijkstraDelegCert
delegCert)
    DijkstraTxCertPool PoolCert
poolCert -> do
      newPState <-
        forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @(EraRule "SUBPOOL" era) (RuleContext 'Transition (EraRule "SUBPOOL" era)
 -> Rule (SUBCERT era) 'Transition (State (EraRule "SUBPOOL" era)))
-> RuleContext 'Transition (EraRule "SUBPOOL" era)
-> Rule (SUBCERT era) 'Transition (State (EraRule "SUBPOOL" era))
forall a b. (a -> b) -> a -> b
$ (Environment (SUBPOOL era), State (SUBPOOL era),
 Signal (SUBPOOL era))
-> TRC (SUBPOOL era)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (EpochNo -> PParams era -> PoolEnv era
forall era. EpochNo -> PParams era -> PoolEnv era
Shelley.PoolEnv EpochNo
currentEpoch PParams era
pp, PState era
State (SUBPOOL era)
certPState, PoolCert
Signal (SUBPOOL era)
poolCert)
      pure $ certState & certPStateL .~ newPState
    DijkstraTxCertGov ConwayGovCert
govCert -> do
      forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @(EraRule "SUBGOVCERT" era) (RuleContext 'Transition (EraRule "SUBGOVCERT" era)
 -> Rule
      (SUBCERT era) 'Transition (State (EraRule "SUBGOVCERT" era)))
-> RuleContext 'Transition (EraRule "SUBGOVCERT" era)
-> Rule
     (SUBCERT era) 'Transition (State (EraRule "SUBGOVCERT" era))
forall a b. (a -> b) -> a -> b
$
        (Environment (SUBGOVCERT era), State (SUBGOVCERT era),
 Signal (SUBGOVCERT era))
-> TRC (SUBGOVCERT era)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (PParams era
-> EpochNo
-> StrictMaybe (Committee era)
-> Map (GovPurposeId 'CommitteePurpose) (GovActionState era)
-> ConwayGovCertEnv era
forall era.
PParams era
-> EpochNo
-> StrictMaybe (Committee era)
-> Map (GovPurposeId 'CommitteePurpose) (GovActionState era)
-> ConwayGovCertEnv era
Conway.ConwayGovCertEnv PParams era
pp EpochNo
currentEpoch StrictMaybe (Committee era)
committee Map (GovPurposeId 'CommitteePurpose) (GovActionState era)
committeeProposals, State (SUBGOVCERT era)
State (SUBCERT era)
certState, ConwayGovCert
Signal (SUBGOVCERT era)
govCert)

instance
  ( STS (SUBDELEG era)
  , PredicateFailure (EraRule "SUBDELEG" era) ~ DijkstraSubDelegPredFailure era
  ) =>
  Embed (SUBDELEG era) (SUBCERT era)
  where
  wrapFailed :: PredicateFailure (SUBDELEG era) -> PredicateFailure (SUBCERT era)
wrapFailed = PredicateFailure (EraRule "SUBDELEG" era)
-> DijkstraSubCertPredFailure era
PredicateFailure (SUBDELEG era) -> PredicateFailure (SUBCERT era)
forall era.
PredicateFailure (EraRule "SUBDELEG" era)
-> DijkstraSubCertPredFailure era
SubDelegFailure
  wrapEvent :: Event (SUBDELEG era) -> Event (SUBCERT era)
wrapEvent = Void -> DijkstraSubCertEvent era
Event (SUBDELEG era) -> Event (SUBCERT era)
forall a. Void -> a
absurd

instance
  ( STS (SUBPOOL era)
  , PredicateFailure (EraRule "SUBPOOL" era) ~ DijkstraSubPoolPredFailure era
  , Event (EraRule "SUBPOOL" era) ~ DijkstraSubPoolEvent era
  ) =>
  Embed (SUBPOOL era) (SUBCERT era)
  where
  wrapFailed :: PredicateFailure (SUBPOOL era) -> PredicateFailure (SUBCERT era)
wrapFailed = PredicateFailure (EraRule "SUBPOOL" era)
-> DijkstraSubCertPredFailure era
PredicateFailure (SUBPOOL era) -> PredicateFailure (SUBCERT era)
forall era.
PredicateFailure (EraRule "SUBPOOL" era)
-> DijkstraSubCertPredFailure era
SubPoolFailure
  wrapEvent :: Event (SUBPOOL era) -> Event (SUBCERT era)
wrapEvent = Event (EraRule "SUBPOOL" era) -> DijkstraSubCertEvent era
Event (SUBPOOL era) -> Event (SUBCERT era)
forall era.
Event (EraRule "SUBPOOL" era) -> DijkstraSubCertEvent era
SubPoolEvent

instance
  ( Era era
  , STS (SUBGOVCERT era)
  , PredicateFailure (EraRule "SUBGOVCERT" era) ~ DijkstraSubGovCertPredFailure era
  ) =>
  Embed (SUBGOVCERT era) (SUBCERT era)
  where
  wrapFailed :: PredicateFailure (SUBGOVCERT era) -> PredicateFailure (SUBCERT era)
wrapFailed = PredicateFailure (EraRule "SUBGOVCERT" era)
-> DijkstraSubCertPredFailure era
PredicateFailure (SUBGOVCERT era) -> PredicateFailure (SUBCERT era)
forall era.
PredicateFailure (EraRule "SUBGOVCERT" era)
-> DijkstraSubCertPredFailure era
SubGovCertFailure
  wrapEvent :: Event (SUBGOVCERT era) -> Event (SUBCERT era)
wrapEvent = Void -> DijkstraSubCertEvent era
Event (SUBGOVCERT era) -> Event (SUBCERT era)
forall a. Void -> a
absurd

conwayToDijkstraSubCertPredFailure ::
  forall era.
  ( InjectRuleFailure "SUBDELEG" Conway.ConwayDelegPredFailure era
  , PredicateFailure (EraRule "DELEG" era) ~ Conway.ConwayDelegPredFailure era
  , InjectRuleFailure "SUBPOOL" Shelley.ShelleyPoolPredFailure era
  , PredicateFailure (EraRule "POOL" era) ~ Shelley.ShelleyPoolPredFailure era
  , InjectRuleFailure "SUBGOVCERT" DijkstraGovCertPredFailure era
  , PredicateFailure (EraRule "GOVCERT" era) ~ DijkstraGovCertPredFailure era
  ) =>
  Conway.ConwayCertPredFailure era -> DijkstraSubCertPredFailure era
conwayToDijkstraSubCertPredFailure :: forall era.
(InjectRuleFailure "SUBDELEG" ConwayDelegPredFailure era,
 PredicateFailure (EraRule "DELEG" era)
 ~ ConwayDelegPredFailure era,
 InjectRuleFailure "SUBPOOL" ShelleyPoolPredFailure era,
 PredicateFailure (EraRule "POOL" era) ~ ShelleyPoolPredFailure era,
 InjectRuleFailure "SUBGOVCERT" DijkstraGovCertPredFailure era,
 PredicateFailure (EraRule "GOVCERT" era)
 ~ DijkstraGovCertPredFailure era) =>
ConwayCertPredFailure era -> DijkstraSubCertPredFailure era
conwayToDijkstraSubCertPredFailure = \case
  Conway.DelegFailure PredicateFailure (EraRule "DELEG" era)
f -> PredicateFailure (EraRule "SUBDELEG" era)
-> DijkstraSubCertPredFailure era
forall era.
PredicateFailure (EraRule "SUBDELEG" era)
-> DijkstraSubCertPredFailure era
SubDelegFailure (forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure @"SUBDELEG" PredicateFailure (EraRule "DELEG" era)
ConwayDelegPredFailure era
f)
  Conway.PoolFailure PredicateFailure (EraRule "POOL" era)
f -> PredicateFailure (EraRule "SUBPOOL" era)
-> DijkstraSubCertPredFailure era
forall era.
PredicateFailure (EraRule "SUBPOOL" era)
-> DijkstraSubCertPredFailure era
SubPoolFailure (forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure @"SUBPOOL" PredicateFailure (EraRule "POOL" era)
ShelleyPoolPredFailure era
f)
  Conway.GovCertFailure PredicateFailure (EraRule "GOVCERT" era)
f -> PredicateFailure (EraRule "SUBGOVCERT" era)
-> DijkstraSubCertPredFailure era
forall era.
PredicateFailure (EraRule "SUBGOVCERT" era)
-> DijkstraSubCertPredFailure era
SubGovCertFailure (forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure @"SUBGOVCERT" PredicateFailure (EraRule "GOVCERT" era)
DijkstraGovCertPredFailure era
f)