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

-- | Like TICK, called only by consensus. But, ticks ledger state to a __future__ slot.
module Cardano.Ledger.Conway.Rules.Tickf (
  TICKF,
  ConwayTickfEvent (..),
) where

import Cardano.Ledger.BaseTypes (EpochNo, ShelleyBase, SlotNo)
import Cardano.Ledger.Conway.Era
import Cardano.Ledger.Core (Era, EraRule)
import Cardano.Ledger.Shelley.Governance
import Cardano.Ledger.Shelley.LedgerState
import qualified Cardano.Ledger.Shelley.Rules as Shelley
import Cardano.Ledger.State (SnapShots)
import Control.DeepSeq (NFData)
import Control.State.Transition
import Data.Void (Void)
import GHC.Generics (Generic)
import Lens.Micro ((&), (.~), (^.))

newtype ConwayTickfEvent era
  = TickfSnapEvent (Event (EraRule "SNAP" era))
  deriving ((forall x. ConwayTickfEvent era -> Rep (ConwayTickfEvent era) x)
-> (forall x. Rep (ConwayTickfEvent era) x -> ConwayTickfEvent era)
-> Generic (ConwayTickfEvent era)
forall x. Rep (ConwayTickfEvent era) x -> ConwayTickfEvent era
forall x. ConwayTickfEvent era -> Rep (ConwayTickfEvent era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x. Rep (ConwayTickfEvent era) x -> ConwayTickfEvent era
forall era x. ConwayTickfEvent era -> Rep (ConwayTickfEvent era) x
$cfrom :: forall era x. ConwayTickfEvent era -> Rep (ConwayTickfEvent era) x
from :: forall x. ConwayTickfEvent era -> Rep (ConwayTickfEvent era) x
$cto :: forall era x. Rep (ConwayTickfEvent era) x -> ConwayTickfEvent era
to :: forall x. Rep (ConwayTickfEvent era) x -> ConwayTickfEvent era
Generic)

deriving instance Eq (Event (EraRule "SNAP" era)) => Eq (ConwayTickfEvent era)

instance NFData (Event (EraRule "SNAP" era)) => NFData (ConwayTickfEvent era)

instance
  ( EraGov era
  , State (EraRule "SNAP" era) ~ SnapShots era
  , Environment (EraRule "SNAP" era) ~ Shelley.SnapEnv era
  , Signal (EraRule "SNAP" era) ~ EpochNo
  , Embed (EraRule "SNAP" era) (TICKF era)
  ) =>
  STS (TICKF era)
  where
  type State (TICKF era) = NewEpochState era
  type Signal (TICKF era) = SlotNo
  type Environment (TICKF era) = ()
  type BaseM (TICKF era) = ShelleyBase
  type PredicateFailure (TICKF era) = Void
  type Event (TICKF era) = ConwayTickfEvent era

  initialRules :: [InitialRule (TICKF era)]
initialRules = []
  transitionRules :: [TransitionRule (TICKF era)]
transitionRules = TransitionRule (TICKF era) -> [TransitionRule (TICKF era)]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TransitionRule (TICKF era) -> [TransitionRule (TICKF era)])
-> TransitionRule (TICKF era) -> [TransitionRule (TICKF era)]
forall a b. (a -> b) -> a -> b
$ do
    TRC ((), nes0, slot) <- Rule (TICKF era) 'Transition (RuleContext 'Transition (TICKF era))
F (Clause (TICKF era) 'Transition) (TRC (TICKF era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
    -- This whole function is a specialization of an inlined 'NEWEPOCH'.
    --
    -- The forecast is built entirely from the stake pool distribution in the set snapshot and
    -- the current protocol parameters, so the correctness of this rule only depends on getting
    -- these two correct.

    (curEpochNo, nes) <- liftSTS $ Shelley.solidifyNextEpochPParams nes0 slot

    if curEpochNo /= succ (nesEL nes)
      then pure nes
      else do
        let es = NewEpochState era -> EpochState era
forall era. NewEpochState era -> EpochState era
nesEs NewEpochState era
nes
            pp = 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
            ls = EpochState era -> LedgerState era
forall era. EpochState era -> LedgerState era
esLState EpochState era
es
            ss = EpochState era -> SnapShots era
forall era. EpochState era -> SnapShots era
esSnapshots EpochState era
es
            govState = NewEpochState era
nes NewEpochState era
-> Getting (GovState era) (NewEpochState era) (GovState era)
-> GovState era
forall s a. s -> Getting a s a -> a
^. Getting (GovState era) (NewEpochState era) (GovState era)
forall era (f :: * -> *).
Functor f =>
(GovState era -> f (GovState era))
-> NewEpochState era -> f (NewEpochState era)
newEpochStateGovStateL

        ss' <-
          trans @(EraRule "SNAP" era) $ TRC (Shelley.SnapEnv ls pp, ss, curEpochNo)

        pure $!
          nes
            & nesEsL . esSnapshotsL .~ ss'
            & newEpochStateGovStateL . curPParamsGovStateL .~ nextEpochPParams govState
            & newEpochStateGovStateL . prevPParamsGovStateL .~ (govState ^. curPParamsGovStateL)
            & newEpochStateGovStateL . futurePParamsGovStateL .~ NoPParamsUpdate

instance
  ( Era era
  , STS (Shelley.SNAP era)
  , Event (EraRule "SNAP" era) ~ Shelley.SnapEvent era
  ) =>
  Embed (Shelley.SNAP era) (TICKF era)
  where
  wrapFailed :: PredicateFailure (SNAP era) -> PredicateFailure (TICKF era)
wrapFailed = \case {}
  wrapEvent :: Event (SNAP era) -> Event (TICKF era)
wrapEvent = Event (EraRule "SNAP" era) -> ConwayTickfEvent era
Event (SNAP era) -> Event (TICKF era)
forall era. Event (EraRule "SNAP" era) -> ConwayTickfEvent era
TickfSnapEvent