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

module Cardano.Ledger.Shelley.Rules.Epoch (
  ShelleyEPOCH,
  ShelleyEpochEvent (..),
  PredicateFailure,
) where

import Cardano.Ledger.BaseTypes (ShelleyBase)
import Cardano.Ledger.Shelley.Core
import Cardano.Ledger.Shelley.Era (ShelleyEPOCH)
import Cardano.Ledger.Shelley.LedgerState (
  EpochState,
  LedgerState,
  UTxOState (utxosDeposited, utxosGovState),
  curPParamsEpochStateL,
  esChainAccountState,
  esLState,
  esLStateL,
  esNonMyopic,
  esSnapshots,
  lsCertState,
  lsCertStateL,
  lsUTxOState,
  lsUTxOStateL,
  totalObligation,
  utxosGovStateL,
  pattern EpochState,
 )
import Cardano.Ledger.Shelley.LedgerState.Types (prevPParamsEpochStateL)
import Cardano.Ledger.Shelley.Rewards ()
import Cardano.Ledger.Shelley.Rules.PoolReap (
  ShelleyPOOLREAP,
  ShelleyPoolreapEvent,
  ShelleyPoolreapState (..),
 )
import Cardano.Ledger.Shelley.Rules.Snap (
  ShelleySNAP,
  SnapEnv (..),
  SnapEvent,
 )
import Cardano.Ledger.Shelley.Rules.Upec (ShelleyUPEC, UpecState (..))
import Cardano.Ledger.Slot (EpochNo)
import Cardano.Ledger.State
import Control.DeepSeq (NFData)
import Control.State.Transition (
  Embed (..),
  STS (..),
  TRC (..),
  TransitionRule,
  judgmentContext,
  trans,
 )
import Data.Default (Default)
import Data.Void (Void)
import GHC.Generics (Generic)
import Lens.Micro

data ShelleyEpochEvent era
  = PoolReapEvent (Event (EraRule "POOLREAP" era))
  | SnapEvent (Event (EraRule "SNAP" era))
  | UpecEvent (Event (EraRule "UPEC" era))
  deriving ((forall x. ShelleyEpochEvent era -> Rep (ShelleyEpochEvent era) x)
-> (forall x.
    Rep (ShelleyEpochEvent era) x -> ShelleyEpochEvent era)
-> Generic (ShelleyEpochEvent era)
forall x. Rep (ShelleyEpochEvent era) x -> ShelleyEpochEvent era
forall x. ShelleyEpochEvent era -> Rep (ShelleyEpochEvent era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (ShelleyEpochEvent era) x -> ShelleyEpochEvent era
forall era x.
ShelleyEpochEvent era -> Rep (ShelleyEpochEvent era) x
$cfrom :: forall era x.
ShelleyEpochEvent era -> Rep (ShelleyEpochEvent era) x
from :: forall x. ShelleyEpochEvent era -> Rep (ShelleyEpochEvent era) x
$cto :: forall era x.
Rep (ShelleyEpochEvent era) x -> ShelleyEpochEvent era
to :: forall x. Rep (ShelleyEpochEvent era) x -> ShelleyEpochEvent era
Generic)

deriving instance
  ( Eq (Event (EraRule "POOLREAP" era))
  , Eq (Event (EraRule "SNAP" era))
  , Eq (Event (EraRule "UPEC" era))
  ) =>
  Eq (ShelleyEpochEvent era)

instance
  ( NFData (Event (EraRule "POOLREAP" era))
  , NFData (Event (EraRule "SNAP" era))
  , NFData (Event (EraRule "UPEC" era))
  ) =>
  NFData (ShelleyEpochEvent era)

instance
  ( EraTxOut era
  , EraGov era
  , EraStake era
  , EraCertState era
  , GovState era ~ ShelleyGovState era
  , Embed (EraRule "SNAP" era) (ShelleyEPOCH era)
  , Environment (EraRule "SNAP" era) ~ SnapEnv era
  , State (EraRule "SNAP" era) ~ SnapShots
  , Signal (EraRule "SNAP" era) ~ ()
  , Embed (EraRule "POOLREAP" era) (ShelleyEPOCH era)
  , Environment (EraRule "POOLREAP" era) ~ ()
  , State (EraRule "POOLREAP" era) ~ ShelleyPoolreapState era
  , Signal (EraRule "POOLREAP" era) ~ EpochNo
  , Embed (EraRule "UPEC" era) (ShelleyEPOCH era)
  , Environment (EraRule "UPEC" era) ~ LedgerState era
  , State (EraRule "UPEC" era) ~ UpecState era
  , Signal (EraRule "UPEC" era) ~ ()
  , Default (PParams era)
  ) =>
  STS (ShelleyEPOCH era)
  where
  type State (ShelleyEPOCH era) = EpochState era
  type Signal (ShelleyEPOCH era) = EpochNo
  type Environment (ShelleyEPOCH era) = ()
  type BaseM (ShelleyEPOCH era) = ShelleyBase
  type PredicateFailure (ShelleyEPOCH era) = Void
  type Event (ShelleyEPOCH era) = ShelleyEpochEvent era
  transitionRules :: [TransitionRule (ShelleyEPOCH era)]
transitionRules = [TransitionRule (ShelleyEPOCH era)
forall era.
(Embed (EraRule "SNAP" era) (ShelleyEPOCH era),
 Environment (EraRule "SNAP" era) ~ SnapEnv era,
 State (EraRule "SNAP" era) ~ SnapShots,
 Signal (EraRule "SNAP" era) ~ (),
 Embed (EraRule "POOLREAP" era) (ShelleyEPOCH era),
 Environment (EraRule "POOLREAP" era) ~ (),
 State (EraRule "POOLREAP" era) ~ ShelleyPoolreapState era,
 Signal (EraRule "POOLREAP" era) ~ EpochNo,
 Embed (EraRule "UPEC" era) (ShelleyEPOCH era),
 Environment (EraRule "UPEC" era) ~ LedgerState era,
 State (EraRule "UPEC" era) ~ UpecState era,
 Signal (EraRule "UPEC" era) ~ (),
 GovState era ~ ShelleyGovState era, EraGov era,
 EraCertState era) =>
TransitionRule (ShelleyEPOCH era)
epochTransition]

epochTransition ::
  forall era.
  ( Embed (EraRule "SNAP" era) (ShelleyEPOCH era)
  , Environment (EraRule "SNAP" era) ~ SnapEnv era
  , State (EraRule "SNAP" era) ~ SnapShots
  , Signal (EraRule "SNAP" era) ~ ()
  , Embed (EraRule "POOLREAP" era) (ShelleyEPOCH era)
  , Environment (EraRule "POOLREAP" era) ~ ()
  , State (EraRule "POOLREAP" era) ~ ShelleyPoolreapState era
  , Signal (EraRule "POOLREAP" era) ~ EpochNo
  , Embed (EraRule "UPEC" era) (ShelleyEPOCH era)
  , Environment (EraRule "UPEC" era) ~ LedgerState era
  , State (EraRule "UPEC" era) ~ UpecState era
  , Signal (EraRule "UPEC" era) ~ ()
  , GovState era ~ ShelleyGovState era
  , EraGov era
  , EraCertState era
  ) =>
  TransitionRule (ShelleyEPOCH era)
epochTransition :: forall era.
(Embed (EraRule "SNAP" era) (ShelleyEPOCH era),
 Environment (EraRule "SNAP" era) ~ SnapEnv era,
 State (EraRule "SNAP" era) ~ SnapShots,
 Signal (EraRule "SNAP" era) ~ (),
 Embed (EraRule "POOLREAP" era) (ShelleyEPOCH era),
 Environment (EraRule "POOLREAP" era) ~ (),
 State (EraRule "POOLREAP" era) ~ ShelleyPoolreapState era,
 Signal (EraRule "POOLREAP" era) ~ EpochNo,
 Embed (EraRule "UPEC" era) (ShelleyEPOCH era),
 Environment (EraRule "UPEC" era) ~ LedgerState era,
 State (EraRule "UPEC" era) ~ UpecState era,
 Signal (EraRule "UPEC" era) ~ (),
 GovState era ~ ShelleyGovState era, EraGov era,
 EraCertState era) =>
TransitionRule (ShelleyEPOCH era)
epochTransition = do
  TRC
    ( _
      , es@EpochState
          { esChainAccountState = chainAccountState
          , esSnapshots = ss
          , esLState = ls
          , esNonMyopic = nm
          }
      , e
      ) <-
    Rule
  (ShelleyEPOCH era)
  'Transition
  (RuleContext 'Transition (ShelleyEPOCH era))
F (Clause (ShelleyEPOCH era) 'Transition) (TRC (ShelleyEPOCH era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
  let pp = State (ShelleyEPOCH era)
EpochState era
es EpochState era
-> Getting (PParams era) (EpochState era) (PParams era)
-> PParams era
forall s a. s -> Getting a s a -> a
^. Getting (PParams era) (EpochState era) (PParams era)
forall era. EraGov era => Lens' (EpochState era) (PParams era)
Lens' (EpochState era) (PParams era)
curPParamsEpochStateL
      utxoSt = LedgerState era -> UTxOState era
forall era. LedgerState era -> UTxOState era
lsUTxOState LedgerState era
ls
      certState = LedgerState era
ls LedgerState era
-> Getting (CertState era) (LedgerState era) (CertState era)
-> CertState era
forall s a. s -> Getting a s a -> a
^. Getting (CertState era) (LedgerState era) (CertState era)
forall era (f :: * -> *).
Functor f =>
(CertState era -> f (CertState era))
-> LedgerState era -> f (LedgerState era)
lsCertStateL
  ss' <-
    trans @(EraRule "SNAP" era) $ TRC (SnapEnv ls pp, ss, ())

  PoolreapState utxoSt' chainAccountState' adjustedCertState <-
    trans @(EraRule "POOLREAP" era) $
      TRC ((), PoolreapState utxoSt chainAccountState certState, e)

  let ls' = LedgerState era
ls {lsUTxOState = utxoSt', lsCertState = adjustedCertState}

  UpecState pp' ppupSt' <-
    trans @(EraRule "UPEC" era) $
      TRC (ls', UpecState pp (utxosGovState utxoSt'), ())
  let utxoSt'' = UTxOState era
utxoSt' {utxosGovState = ppupSt'}

  let
    -- At the epoch boundary refunds are made, so we need to change what
    -- the utxosDeposited field is. The other two places where deposits are
    -- kept (dsUnified of DState and psDeposits of PState) are adjusted by
    -- the rules, So we can recompute the utxosDeposited field using adjustedCertState
    -- since we have the invariant that: obligationCertState dpstate == utxosDeposited utxostate
    oblgNew = CertState era -> GovState era -> Coin
forall era.
(EraGov era, EraCertState era) =>
CertState era -> GovState era -> Coin
totalObligation CertState era
adjustedCertState (UTxOState era
utxoSt'' UTxOState era
-> Getting
     (ShelleyGovState era) (UTxOState era) (ShelleyGovState era)
-> ShelleyGovState era
forall s a. s -> Getting a s a -> a
^. (GovState era -> Const (ShelleyGovState era) (GovState era))
-> UTxOState era -> Const (ShelleyGovState era) (UTxOState era)
Getting (ShelleyGovState era) (UTxOState era) (ShelleyGovState era)
forall era (f :: * -> *).
Functor f =>
(GovState era -> f (GovState era))
-> UTxOState era -> f (UTxOState era)
utxosGovStateL)
    utxoSt''' = UTxOState era
utxoSt'' {utxosDeposited = oblgNew}
  pure $
    EpochState chainAccountState' ls' ss' nm
      & esLStateL . lsUTxOStateL .~ utxoSt'''
      & prevPParamsEpochStateL .~ pp
      & curPParamsEpochStateL .~ pp'

instance
  ( EraTxOut era
  , EraStake era
  , Event (EraRule "SNAP" era) ~ SnapEvent era
  , EraCertState era
  ) =>
  Embed (ShelleySNAP era) (ShelleyEPOCH era)
  where
  wrapFailed :: PredicateFailure (ShelleySNAP era)
-> PredicateFailure (ShelleyEPOCH era)
wrapFailed = \case {}
  wrapEvent :: Event (ShelleySNAP era) -> Event (ShelleyEPOCH era)
wrapEvent = Event (EraRule "SNAP" era) -> ShelleyEpochEvent era
Event (ShelleySNAP era) -> Event (ShelleyEPOCH era)
forall era. Event (EraRule "SNAP" era) -> ShelleyEpochEvent era
SnapEvent

instance
  ( Era era
  , STS (ShelleyPOOLREAP era)
  , Event (EraRule "POOLREAP" era) ~ ShelleyPoolreapEvent era
  ) =>
  Embed (ShelleyPOOLREAP era) (ShelleyEPOCH era)
  where
  wrapFailed :: PredicateFailure (ShelleyPOOLREAP era)
-> PredicateFailure (ShelleyEPOCH era)
wrapFailed = \case {}
  wrapEvent :: Event (ShelleyPOOLREAP era) -> Event (ShelleyEPOCH era)
wrapEvent = Event (EraRule "POOLREAP" era) -> ShelleyEpochEvent era
Event (ShelleyPOOLREAP era) -> Event (ShelleyEPOCH era)
forall era. Event (EraRule "POOLREAP" era) -> ShelleyEpochEvent era
PoolReapEvent

instance
  ( Era era
  , STS (ShelleyUPEC era)
  , Event (EraRule "UPEC" era) ~ Void
  ) =>
  Embed (ShelleyUPEC era) (ShelleyEPOCH era)
  where
  wrapFailed :: PredicateFailure (ShelleyUPEC era)
-> PredicateFailure (ShelleyEPOCH era)
wrapFailed = \case {}
  wrapEvent :: Event (ShelleyUPEC era) -> Event (ShelleyEPOCH era)
wrapEvent = Event (EraRule "UPEC" era) -> ShelleyEpochEvent era
Event (ShelleyUPEC era) -> Event (ShelleyEPOCH era)
forall era. Event (EraRule "UPEC" era) -> ShelleyEpochEvent era
UpecEvent