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

module Shelley.Spec.Ledger.STS.Snap
  ( SNAP,
    PredicateFailure,
    SnapPredicateFailure,
  )
where

import Cardano.Ledger.Shelley (ShelleyBased)
import Control.State.Transition
  ( STS (..),
    TRC (..),
    TransitionRule,
    judgmentContext,
  )
import GHC.Generics (Generic)
import NoThunks.Class (NoThunks (..))
import Shelley.Spec.Ledger.BaseTypes
import Shelley.Spec.Ledger.EpochBoundary
import Shelley.Spec.Ledger.LedgerState
  ( DPState (..),
    LedgerState (..),
    UTxOState (..),
    stakeDistr,
  )

data SNAP era

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

instance NoThunks (SnapPredicateFailure era)

instance ShelleyBased era => STS (SNAP era) where
  type State (SNAP era) = SnapShots era
  type Signal (SNAP era) = ()
  type Environment (SNAP era) = LedgerState era
  type BaseM (SNAP era) = ShelleyBase
  type PredicateFailure (SNAP era) = SnapPredicateFailure era
  initialRules :: [InitialRule (SNAP era)]
initialRules = [SnapShots era -> F (Clause (SNAP era) 'Initial) (SnapShots era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure SnapShots era
forall era. SnapShots era
emptySnapShots]
  transitionRules :: [TransitionRule (SNAP era)]
transitionRules = [TransitionRule (SNAP era)
forall era. ShelleyBased era => TransitionRule (SNAP era)
snapTransition]

snapTransition ::
  ShelleyBased era =>
  TransitionRule (SNAP era)
snapTransition :: TransitionRule (SNAP era)
snapTransition = do
  TRC (Environment (SNAP era)
lstate, State (SNAP era)
s, Signal (SNAP era)
_) <- F (Clause (SNAP era) 'Transition) (TRC (SNAP era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext

  let LedgerState (UTxOState UTxO era
utxo Coin
_ Coin
fees PPUPState era
_) (DPState DState era
dstate PState era
pstate) = Environment (SNAP era)
LedgerState era
lstate
      stake :: SnapShot era
stake = UTxO era -> DState era -> PState era -> SnapShot era
forall era.
ShelleyBased era =>
UTxO era -> DState era -> PState era -> SnapShot era
stakeDistr UTxO era
utxo DState era
dstate PState era
pstate
  SnapShots era -> F (Clause (SNAP era) 'Transition) (SnapShots era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SnapShots era
 -> F (Clause (SNAP era) 'Transition) (SnapShots era))
-> SnapShots era
-> F (Clause (SNAP era) 'Transition) (SnapShots era)
forall a b. (a -> b) -> a -> b
$
    State (SNAP era)
SnapShots era
s
      { $sel:_pstakeMark:SnapShots :: SnapShot era
_pstakeMark = SnapShot era
stake,
        $sel:_pstakeSet:SnapShots :: SnapShot era
_pstakeSet = SnapShots era -> SnapShot era
forall era. SnapShots era -> SnapShot era
_pstakeMark State (SNAP era)
SnapShots era
s,
        $sel:_pstakeGo:SnapShots :: SnapShot era
_pstakeGo = SnapShots era -> SnapShot era
forall era. SnapShots era -> SnapShot era
_pstakeSet State (SNAP era)
SnapShots era
s,
        $sel:_feeSS:SnapShots :: Coin
_feeSS = Coin
fees
      }