{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Cardano.Ledger.Dijkstra.Rules.Cert (
  DijkstraCERT,
) where

import Cardano.Ledger.BaseTypes (ShelleyBase, StrictMaybe (..))
import Cardano.Ledger.Conway.Rules (
  CertEnv (..),
  ConwayCertEvent,
  ConwayCertPredFailure (..),
  ConwayDelegEnv (..),
  ConwayDelegPredFailure,
  ConwayGovCertEnv (..),
  ConwayGovCertPredFailure,
 )
import Cardano.Ledger.Conway.TxCert
import Cardano.Ledger.Dijkstra.Core
import Cardano.Ledger.Dijkstra.Era
import Cardano.Ledger.Dijkstra.Rules.GovCert (DijkstraGovCertPredFailure)
import Cardano.Ledger.Dijkstra.State
import Cardano.Ledger.Dijkstra.TxCert
import Cardano.Ledger.Shelley.Rules (PoolEnv (..), ShelleyPoolPredFailure)
import Control.State.Transition.Extended
import Data.Void (absurd)
import Lens.Micro ((&), (.~), (^.))

type instance EraRuleFailure "CERT" DijkstraEra = ConwayCertPredFailure DijkstraEra

type instance EraRuleEvent "CERT" DijkstraEra = ConwayCertEvent DijkstraEra

instance InjectRuleFailure "CERT" ConwayCertPredFailure DijkstraEra

instance InjectRuleFailure "CERT" ConwayDelegPredFailure DijkstraEra where
  injectFailure :: ConwayDelegPredFailure DijkstraEra
-> EraRuleFailure "CERT" DijkstraEra
injectFailure = PredicateFailure (EraRule "DELEG" DijkstraEra)
-> ConwayCertPredFailure DijkstraEra
ConwayDelegPredFailure DijkstraEra
-> EraRuleFailure "CERT" DijkstraEra
forall era.
PredicateFailure (EraRule "DELEG" era) -> ConwayCertPredFailure era
DelegFailure

instance InjectRuleFailure "CERT" ShelleyPoolPredFailure DijkstraEra where
  injectFailure :: ShelleyPoolPredFailure DijkstraEra
-> EraRuleFailure "CERT" DijkstraEra
injectFailure = PredicateFailure (EraRule "POOL" DijkstraEra)
-> ConwayCertPredFailure DijkstraEra
ShelleyPoolPredFailure DijkstraEra
-> EraRuleFailure "CERT" DijkstraEra
forall era.
PredicateFailure (EraRule "POOL" era) -> ConwayCertPredFailure era
PoolFailure

instance InjectRuleFailure "CERT" DijkstraGovCertPredFailure DijkstraEra where
  injectFailure :: DijkstraGovCertPredFailure DijkstraEra
-> EraRuleFailure "CERT" DijkstraEra
injectFailure = PredicateFailure (EraRule "GOVCERT" DijkstraEra)
-> ConwayCertPredFailure DijkstraEra
DijkstraGovCertPredFailure DijkstraEra
-> EraRuleFailure "CERT" DijkstraEra
forall era.
PredicateFailure (EraRule "GOVCERT" era)
-> ConwayCertPredFailure era
GovCertFailure

instance InjectRuleFailure "CERT" ConwayGovCertPredFailure DijkstraEra where
  injectFailure :: ConwayGovCertPredFailure DijkstraEra
-> EraRuleFailure "CERT" DijkstraEra
injectFailure = PredicateFailure (EraRule "GOVCERT" DijkstraEra)
-> ConwayCertPredFailure DijkstraEra
DijkstraGovCertPredFailure DijkstraEra
-> ConwayCertPredFailure DijkstraEra
forall era.
PredicateFailure (EraRule "GOVCERT" era)
-> ConwayCertPredFailure era
GovCertFailure (DijkstraGovCertPredFailure DijkstraEra
 -> ConwayCertPredFailure DijkstraEra)
-> (ConwayGovCertPredFailure DijkstraEra
    -> DijkstraGovCertPredFailure DijkstraEra)
-> ConwayGovCertPredFailure DijkstraEra
-> ConwayCertPredFailure DijkstraEra
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConwayGovCertPredFailure DijkstraEra
-> EraRuleFailure "GOVCERT" DijkstraEra
ConwayGovCertPredFailure DijkstraEra
-> DijkstraGovCertPredFailure DijkstraEra
forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure

instance
  ( Era era
  , State (EraRule "DELEG" era) ~ CertState era
  , State (EraRule "POOL" era) ~ PState era
  , State (EraRule "GOVCERT" era) ~ CertState era
  , Environment (EraRule "DELEG" era) ~ ConwayDelegEnv era
  , Environment (EraRule "POOL" era) ~ PoolEnv era
  , Environment (EraRule "GOVCERT" era) ~ ConwayGovCertEnv era
  , Signal (EraRule "DELEG" era) ~ ConwayDelegCert
  , Signal (EraRule "POOL" era) ~ PoolCert
  , Signal (EraRule "GOVCERT" era) ~ ConwayGovCert
  , Embed (EraRule "DELEG" era) (DijkstraCERT era)
  , Embed (EraRule "POOL" era) (DijkstraCERT era)
  , Embed (EraRule "GOVCERT" era) (DijkstraCERT era)
  , TxCert era ~ DijkstraTxCert era
  , EraCertState era
  ) =>
  STS (DijkstraCERT era)
  where
  type State (DijkstraCERT era) = CertState era
  type Signal (DijkstraCERT era) = TxCert era
  type Environment (DijkstraCERT era) = CertEnv era
  type BaseM (DijkstraCERT era) = ShelleyBase
  type PredicateFailure (DijkstraCERT era) = ConwayCertPredFailure era
  type Event (DijkstraCERT era) = ConwayCertEvent era

  transitionRules :: [TransitionRule (DijkstraCERT era)]
transitionRules = [forall era.
(State (EraRule "DELEG" era) ~ CertState era,
 State (EraRule "POOL" era) ~ PState era,
 State (EraRule "GOVCERT" era) ~ CertState era,
 Environment (EraRule "DELEG" era) ~ ConwayDelegEnv era,
 Environment (EraRule "POOL" era) ~ PoolEnv era,
 Environment (EraRule "GOVCERT" era) ~ ConwayGovCertEnv era,
 Signal (EraRule "DELEG" era) ~ ConwayDelegCert,
 Signal (EraRule "POOL" era) ~ PoolCert,
 Signal (EraRule "GOVCERT" era) ~ ConwayGovCert,
 Embed (EraRule "DELEG" era) (DijkstraCERT era),
 Embed (EraRule "POOL" era) (DijkstraCERT era),
 Embed (EraRule "GOVCERT" era) (DijkstraCERT era),
 TxCert era ~ DijkstraTxCert era, EraCertState era) =>
TransitionRule (DijkstraCERT era)
certTransition @era]

certTransition ::
  forall era.
  ( State (EraRule "DELEG" era) ~ CertState era
  , State (EraRule "POOL" era) ~ PState era
  , State (EraRule "GOVCERT" era) ~ CertState era
  , Environment (EraRule "DELEG" era) ~ ConwayDelegEnv era
  , Environment (EraRule "POOL" era) ~ PoolEnv era
  , Environment (EraRule "GOVCERT" era) ~ ConwayGovCertEnv era
  , Signal (EraRule "DELEG" era) ~ ConwayDelegCert
  , Signal (EraRule "POOL" era) ~ PoolCert
  , Signal (EraRule "GOVCERT" era) ~ ConwayGovCert
  , Embed (EraRule "DELEG" era) (DijkstraCERT era)
  , Embed (EraRule "POOL" era) (DijkstraCERT era)
  , Embed (EraRule "GOVCERT" era) (DijkstraCERT era)
  , TxCert era ~ DijkstraTxCert era
  , EraCertState era
  ) =>
  TransitionRule (DijkstraCERT era)
certTransition :: forall era.
(State (EraRule "DELEG" era) ~ CertState era,
 State (EraRule "POOL" era) ~ PState era,
 State (EraRule "GOVCERT" era) ~ CertState era,
 Environment (EraRule "DELEG" era) ~ ConwayDelegEnv era,
 Environment (EraRule "POOL" era) ~ PoolEnv era,
 Environment (EraRule "GOVCERT" era) ~ ConwayGovCertEnv era,
 Signal (EraRule "DELEG" era) ~ ConwayDelegCert,
 Signal (EraRule "POOL" era) ~ PoolCert,
 Signal (EraRule "GOVCERT" era) ~ ConwayGovCert,
 Embed (EraRule "DELEG" era) (DijkstraCERT era),
 Embed (EraRule "POOL" era) (DijkstraCERT era),
 Embed (EraRule "GOVCERT" era) (DijkstraCERT era),
 TxCert era ~ DijkstraTxCert era, EraCertState era) =>
TransitionRule (DijkstraCERT era)
certTransition = do
  TRC (CertEnv pp currentEpoch committee committeeProposals, certState, c) <- Rule
  (DijkstraCERT era)
  'Transition
  (RuleContext 'Transition (DijkstraCERT era))
F (Clause (DijkstraCERT era) 'Transition) (TRC (DijkstraCERT era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
  let
    certPState = CertState era
State (DijkstraCERT 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 ->
      let conwayDelegCert :: ConwayDelegCert
conwayDelegCert = case DijkstraDelegCert
delegCert of
            DijkstraRegCert Credential Staking
cred Coin
coin -> Credential Staking -> StrictMaybe Coin -> ConwayDelegCert
ConwayRegCert Credential Staking
cred (Coin -> StrictMaybe Coin
forall a. a -> StrictMaybe a
SJust Coin
coin)
            DijkstraUnRegCert Credential Staking
cred Coin
coin -> Credential Staking -> StrictMaybe Coin -> ConwayDelegCert
ConwayUnRegCert Credential Staking
cred (Coin -> StrictMaybe Coin
forall a. a -> StrictMaybe a
SJust Coin
coin)
            DijkstraDelegCert Credential Staking
cred Delegatee
d -> Credential Staking -> Delegatee -> ConwayDelegCert
ConwayDelegCert Credential Staking
cred Delegatee
d
            DijkstraRegDelegCert Credential Staking
sc Delegatee
d Coin
coin -> Credential Staking -> Delegatee -> Coin -> ConwayDelegCert
ConwayRegDelegCert Credential Staking
sc Delegatee
d Coin
coin
       in forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @(EraRule "DELEG" era) (RuleContext 'Transition (EraRule "DELEG" era)
 -> Rule
      (DijkstraCERT era) 'Transition (State (EraRule "DELEG" era)))
-> RuleContext 'Transition (EraRule "DELEG" era)
-> Rule
     (DijkstraCERT era) 'Transition (State (EraRule "DELEG" era))
forall a b. (a -> b) -> a -> b
$
            (Environment (EraRule "DELEG" era), State (EraRule "DELEG" era),
 Signal (EraRule "DELEG" era))
-> TRC (EraRule "DELEG" 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
ConwayDelegEnv PParams era
pp Map (KeyHash StakePool) StakePoolState
pools, State (EraRule "DELEG" era)
State (DijkstraCERT era)
certState, ConwayDelegCert
Signal (EraRule "DELEG" era)
conwayDelegCert)
    DijkstraTxCertPool PoolCert
poolCert -> do
      newPState <- forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @(EraRule "POOL" era) (RuleContext 'Transition (EraRule "POOL" era)
 -> Rule
      (DijkstraCERT era) 'Transition (State (EraRule "POOL" era)))
-> RuleContext 'Transition (EraRule "POOL" era)
-> Rule (DijkstraCERT era) 'Transition (State (EraRule "POOL" era))
forall a b. (a -> b) -> a -> b
$ (Environment (EraRule "POOL" era), State (EraRule "POOL" era),
 Signal (EraRule "POOL" era))
-> TRC (EraRule "POOL" era)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (EpochNo -> PParams era -> PoolEnv era
forall era. EpochNo -> PParams era -> PoolEnv era
PoolEnv EpochNo
currentEpoch PParams era
pp, PState era
State (EraRule "POOL" era)
certPState, PoolCert
Signal (EraRule "POOL" 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 "GOVCERT" era) (RuleContext 'Transition (EraRule "GOVCERT" era)
 -> Rule
      (DijkstraCERT era) 'Transition (State (EraRule "GOVCERT" era)))
-> RuleContext 'Transition (EraRule "GOVCERT" era)
-> Rule
     (DijkstraCERT era) 'Transition (State (EraRule "GOVCERT" era))
forall a b. (a -> b) -> a -> b
$
        (Environment (EraRule "GOVCERT" era),
 State (EraRule "GOVCERT" era), Signal (EraRule "GOVCERT" era))
-> TRC (EraRule "GOVCERT" 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
ConwayGovCertEnv PParams era
pp EpochNo
currentEpoch StrictMaybe (Committee era)
committee Map (GovPurposeId 'CommitteePurpose) (GovActionState era)
committeeProposals, State (EraRule "GOVCERT" era)
State (DijkstraCERT era)
certState, ConwayGovCert
Signal (EraRule "GOVCERT" era)
govCert)

instance
  ( Era era
  , STS (DijkstraGOVCERT era)
  , PredicateFailure (EraRule "GOVCERT" era) ~ DijkstraGovCertPredFailure era
  ) =>
  Embed (DijkstraGOVCERT era) (DijkstraCERT era)
  where
  wrapFailed :: PredicateFailure (DijkstraGOVCERT era)
-> PredicateFailure (DijkstraCERT era)
wrapFailed = PredicateFailure (EraRule "GOVCERT" era)
-> ConwayCertPredFailure era
PredicateFailure (DijkstraGOVCERT era)
-> PredicateFailure (DijkstraCERT era)
forall era.
PredicateFailure (EraRule "GOVCERT" era)
-> ConwayCertPredFailure era
GovCertFailure
  wrapEvent :: Event (DijkstraGOVCERT era) -> Event (DijkstraCERT era)
wrapEvent = Void -> ConwayCertEvent era
Event (DijkstraGOVCERT era) -> Event (DijkstraCERT era)
forall a. Void -> a
absurd