{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE EmptyDataDeriving #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeFamilies #-}

module Shelley.Spec.Ledger.STS.Rupd
  ( RUPD,
    RupdEnv (..),
    PredicateFailure,
    RupdPredicateFailure,
  )
where

import Control.Monad.Trans.Reader (asks)
import Control.State.Transition
  ( STS (..),
    TRC (..),
    TransitionRule,
    judgmentContext,
    liftSTS,
  )
import Data.Functor ((<&>))
import Data.Typeable (Typeable)
import GHC.Generics (Generic)
import NoThunks.Class (NoThunks (..))
import Shelley.Spec.Ledger.BaseTypes
  ( ShelleyBase,
    StrictMaybe (..),
    epochInfo,
    maxLovelaceSupply,
    randomnessStabilisationWindow,
  )
import Shelley.Spec.Ledger.Coin (Coin (..))
import Shelley.Spec.Ledger.EpochBoundary (BlocksMade)
import Shelley.Spec.Ledger.LedgerState (EpochState, RewardUpdate, createRUpd)
import Shelley.Spec.Ledger.Slot
  ( Duration (..),
    SlotNo,
    epochInfoEpoch,
    epochInfoFirst,
    epochInfoSize,
    (+*),
  )

data RUPD era

data RupdEnv era
  = RupdEnv (BlocksMade era) (EpochState era)

data RupdPredicateFailure era -- No predicate failures
  deriving (Int -> RupdPredicateFailure era -> ShowS
[RupdPredicateFailure era] -> ShowS
RupdPredicateFailure era -> String
(Int -> RupdPredicateFailure era -> ShowS)
-> (RupdPredicateFailure era -> String)
-> ([RupdPredicateFailure era] -> ShowS)
-> Show (RupdPredicateFailure era)
forall era. Int -> RupdPredicateFailure era -> ShowS
forall era. [RupdPredicateFailure era] -> ShowS
forall era. RupdPredicateFailure era -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [RupdPredicateFailure era] -> ShowS
$cshowList :: forall era. [RupdPredicateFailure era] -> ShowS
show :: RupdPredicateFailure era -> String
$cshow :: forall era. RupdPredicateFailure era -> String
showsPrec :: Int -> RupdPredicateFailure era -> ShowS
$cshowsPrec :: forall era. Int -> RupdPredicateFailure era -> ShowS
Show, RupdPredicateFailure era -> RupdPredicateFailure era -> Bool
(RupdPredicateFailure era -> RupdPredicateFailure era -> Bool)
-> (RupdPredicateFailure era -> RupdPredicateFailure era -> Bool)
-> Eq (RupdPredicateFailure era)
forall era.
RupdPredicateFailure era -> RupdPredicateFailure era -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: RupdPredicateFailure era -> RupdPredicateFailure era -> Bool
$c/= :: forall era.
RupdPredicateFailure era -> RupdPredicateFailure era -> Bool
== :: RupdPredicateFailure era -> RupdPredicateFailure era -> Bool
$c== :: forall era.
RupdPredicateFailure era -> RupdPredicateFailure era -> Bool
Eq, (forall x.
 RupdPredicateFailure era -> Rep (RupdPredicateFailure era) x)
-> (forall x.
    Rep (RupdPredicateFailure era) x -> RupdPredicateFailure era)
-> Generic (RupdPredicateFailure era)
forall x.
Rep (RupdPredicateFailure era) x -> RupdPredicateFailure era
forall x.
RupdPredicateFailure era -> Rep (RupdPredicateFailure era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (RupdPredicateFailure era) x -> RupdPredicateFailure era
forall era x.
RupdPredicateFailure era -> Rep (RupdPredicateFailure era) x
$cto :: forall era x.
Rep (RupdPredicateFailure era) x -> RupdPredicateFailure era
$cfrom :: forall era x.
RupdPredicateFailure era -> Rep (RupdPredicateFailure era) x
Generic)

instance NoThunks (RupdPredicateFailure era)

instance Typeable era => STS (RUPD era) where
  type State (RUPD era) = StrictMaybe (RewardUpdate era)
  type Signal (RUPD era) = SlotNo
  type Environment (RUPD era) = RupdEnv era
  type BaseM (RUPD era) = ShelleyBase
  type PredicateFailure (RUPD era) = RupdPredicateFailure era

  initialRules :: [InitialRule (RUPD era)]
initialRules = [StrictMaybe (RewardUpdate era)
-> F (Clause (RUPD era) 'Initial) (StrictMaybe (RewardUpdate era))
forall (f :: * -> *) a. Applicative f => a -> f a
pure StrictMaybe (RewardUpdate era)
forall a. StrictMaybe a
SNothing]
  transitionRules :: [TransitionRule (RUPD era)]
transitionRules = [TransitionRule (RUPD era)
forall era. Typeable era => TransitionRule (RUPD era)
rupdTransition]

rupdTransition :: Typeable era => TransitionRule (RUPD era)
rupdTransition :: TransitionRule (RUPD era)
rupdTransition = do
  TRC (RupdEnv b es, State (RUPD era)
ru, Signal (RUPD era)
s) <- F (Clause (RUPD era) 'Transition) (TRC (RUPD era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
  (EpochSize
slotsPerEpoch, SlotNo
slot, Word64
maxLL) <- BaseM (RUPD era) (EpochSize, SlotNo, Word64)
-> Rule (RUPD era) 'Transition (EpochSize, SlotNo, Word64)
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM (RUPD era) (EpochSize, SlotNo, Word64)
 -> Rule (RUPD era) 'Transition (EpochSize, SlotNo, Word64))
-> BaseM (RUPD era) (EpochSize, SlotNo, Word64)
-> Rule (RUPD era) 'Transition (EpochSize, SlotNo, Word64)
forall a b. (a -> b) -> a -> b
$ do
    EpochInfo Identity
ei <- (Globals -> EpochInfo Identity)
-> ReaderT Globals Identity (EpochInfo Identity)
forall (m :: * -> *) r a. Monad m => (r -> a) -> ReaderT r m a
asks Globals -> EpochInfo Identity
epochInfo
    Word64
sr <- (Globals -> Word64) -> ReaderT Globals Identity Word64
forall (m :: * -> *) r a. Monad m => (r -> a) -> ReaderT r m a
asks Globals -> Word64
randomnessStabilisationWindow
    EpochNo
e <- HasCallStack => EpochInfo Identity -> SlotNo -> ShelleyBase EpochNo
EpochInfo Identity -> SlotNo -> ShelleyBase EpochNo
epochInfoEpoch EpochInfo Identity
ei SlotNo
Signal (RUPD era)
s
    EpochSize
slotsPerEpoch <- HasCallStack =>
EpochInfo Identity -> EpochNo -> ShelleyBase EpochSize
EpochInfo Identity -> EpochNo -> ShelleyBase EpochSize
epochInfoSize EpochInfo Identity
ei EpochNo
e
    SlotNo
slot <- HasCallStack => EpochInfo Identity -> EpochNo -> ShelleyBase SlotNo
EpochInfo Identity -> EpochNo -> ShelleyBase SlotNo
epochInfoFirst EpochInfo Identity
ei EpochNo
e ShelleyBase SlotNo -> (SlotNo -> SlotNo) -> ShelleyBase SlotNo
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (SlotNo -> Duration -> SlotNo
+* (Word64 -> Duration
Duration Word64
sr))
    Word64
maxLL <- (Globals -> Word64) -> ReaderT Globals Identity Word64
forall (m :: * -> *) r a. Monad m => (r -> a) -> ReaderT r m a
asks Globals -> Word64
maxLovelaceSupply
    (EpochSize, SlotNo, Word64)
-> ReaderT Globals Identity (EpochSize, SlotNo, Word64)
forall (m :: * -> *) a. Monad m => a -> m a
return (EpochSize
slotsPerEpoch, SlotNo
slot, Word64
maxLL)
  if SlotNo
Signal (RUPD era)
s SlotNo -> SlotNo -> Bool
forall a. Ord a => a -> a -> Bool
<= SlotNo
slot
    then StrictMaybe (RewardUpdate era)
-> F (Clause (RUPD era) 'Transition)
     (StrictMaybe (RewardUpdate era))
forall (f :: * -> *) a. Applicative f => a -> f a
pure State (RUPD era)
StrictMaybe (RewardUpdate era)
ru
    else case State (RUPD era)
ru of
      State (RUPD era)
SNothing ->
        RewardUpdate era -> StrictMaybe (RewardUpdate era)
forall a. a -> StrictMaybe a
SJust
          (RewardUpdate era -> StrictMaybe (RewardUpdate era))
-> F (Clause (RUPD era) 'Transition) (RewardUpdate era)
-> F (Clause (RUPD era) 'Transition)
     (StrictMaybe (RewardUpdate era))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ( BaseM (RUPD era) (RewardUpdate era)
-> F (Clause (RUPD era) 'Transition) (RewardUpdate era)
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM (RUPD era) (RewardUpdate era)
 -> F (Clause (RUPD era) 'Transition) (RewardUpdate era))
-> BaseM (RUPD era) (RewardUpdate era)
-> F (Clause (RUPD era) 'Transition) (RewardUpdate era)
forall a b. (a -> b) -> a -> b
$
                  EpochSize
-> BlocksMade era
-> EpochState era
-> Coin
-> ShelleyBase (RewardUpdate era)
forall era.
EpochSize
-> BlocksMade era
-> EpochState era
-> Coin
-> ShelleyBase (RewardUpdate era)
createRUpd
                    EpochSize
slotsPerEpoch
                    BlocksMade era
b
                    EpochState era
es
                    (Integer -> Coin
Coin (Integer -> Coin) -> Integer -> Coin
forall a b. (a -> b) -> a -> b
$ Word64 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
maxLL)
              )
      SJust _ -> StrictMaybe (RewardUpdate era)
-> F (Clause (RUPD era) 'Transition)
     (StrictMaybe (RewardUpdate era))
forall (f :: * -> *) a. Applicative f => a -> f a
pure State (RUPD era)
StrictMaybe (RewardUpdate era)
ru