{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

module Cardano.Ledger.Shelley.Rules.Ledgers
  ( LEDGERS,
    LedgersEnv (..),
    LedgersPredicateFailure (..),
    LedgersEvent (..),
    PredicateFailure,
  )
where

import Cardano.Binary (FromCBOR (..), ToCBOR (..))
import Cardano.Ledger.BaseTypes (ShelleyBase)
import qualified Cardano.Ledger.Core as Core
import Cardano.Ledger.Era
import Cardano.Ledger.Keys (DSignable, Hash)
import Cardano.Ledger.Shelley.LedgerState (AccountState, LedgerState)
import Cardano.Ledger.Shelley.Rules.Ledger
  ( LEDGER,
    LedgerEnv (..),
    LedgerEvent,
    LedgerPredicateFailure,
  )
import Cardano.Ledger.Shelley.TxBody (EraIndependentTxBody)
import Cardano.Ledger.Slot (SlotNo)
import Control.Monad (foldM)
import Control.State.Transition
  ( Embed (..),
    STS (..),
    TRC (..),
    TransitionRule,
    judgmentContext,
    trans,
  )
import Data.Default.Class (Default)
import Data.Foldable (toList)
import Data.Sequence (Seq)
import GHC.Generics (Generic)
import NoThunks.Class (NoThunks (..))

data LEDGERS era

data LedgersEnv era = LedgersEnv
  { LedgersEnv era -> SlotNo
ledgersSlotNo :: SlotNo,
    LedgersEnv era -> PParams era
ledgersPp :: Core.PParams era,
    LedgersEnv era -> AccountState
ledgersAccount :: AccountState
  }

newtype LedgersPredicateFailure era
  = LedgerFailure (PredicateFailure (Core.EraRule "LEDGER" era)) -- Subtransition Failures
  deriving ((forall x.
 LedgersPredicateFailure era -> Rep (LedgersPredicateFailure era) x)
-> (forall x.
    Rep (LedgersPredicateFailure era) x -> LedgersPredicateFailure era)
-> Generic (LedgersPredicateFailure era)
forall x.
Rep (LedgersPredicateFailure era) x -> LedgersPredicateFailure era
forall x.
LedgersPredicateFailure era -> Rep (LedgersPredicateFailure era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (LedgersPredicateFailure era) x -> LedgersPredicateFailure era
forall era x.
LedgersPredicateFailure era -> Rep (LedgersPredicateFailure era) x
$cto :: forall era x.
Rep (LedgersPredicateFailure era) x -> LedgersPredicateFailure era
$cfrom :: forall era x.
LedgersPredicateFailure era -> Rep (LedgersPredicateFailure era) x
Generic)

newtype LedgersEvent era
  = LedgerEvent (Event (Core.EraRule "LEDGER" era))

deriving stock instance
  ( Era era,
    Show (PredicateFailure (Core.EraRule "LEDGER" era))
  ) =>
  Show (LedgersPredicateFailure era)

deriving stock instance
  ( Era era,
    Eq (PredicateFailure (Core.EraRule "LEDGER" era))
  ) =>
  Eq (LedgersPredicateFailure era)

instance
  ( Era era,
    NoThunks (PredicateFailure (Core.EraRule "LEDGER" era))
  ) =>
  NoThunks (LedgersPredicateFailure era)

instance
  ( Era era,
    ToCBOR (PredicateFailure (Core.EraRule "LEDGER" era))
  ) =>
  ToCBOR (LedgersPredicateFailure era)
  where
  toCBOR :: LedgersPredicateFailure era -> Encoding
toCBOR (LedgerFailure PredicateFailure (EraRule "LEDGER" era)
e) = PredicateFailure (EraRule "LEDGER" era) -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR PredicateFailure (EraRule "LEDGER" era)
e

instance
  ( Era era,
    FromCBOR (PredicateFailure (Core.EraRule "LEDGER" era))
  ) =>
  FromCBOR (LedgersPredicateFailure era)
  where
  fromCBOR :: Decoder s (LedgersPredicateFailure era)
fromCBOR = PredicateFailure (EraRule "LEDGER" era)
-> LedgersPredicateFailure era
forall era.
PredicateFailure (EraRule "LEDGER" era)
-> LedgersPredicateFailure era
LedgerFailure (PredicateFailure (EraRule "LEDGER" era)
 -> LedgersPredicateFailure era)
-> Decoder s (PredicateFailure (EraRule "LEDGER" era))
-> Decoder s (LedgersPredicateFailure era)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Decoder s (PredicateFailure (EraRule "LEDGER" era))
forall a s. FromCBOR a => Decoder s a
fromCBOR

instance
  ( Era era,
    Embed (Core.EraRule "LEDGER" era) (LEDGERS era),
    Environment (Core.EraRule "LEDGER" era) ~ LedgerEnv era,
    State (Core.EraRule "LEDGER" era) ~ LedgerState era,
    Signal (Core.EraRule "LEDGER" era) ~ Core.Tx era,
    DSignable (Crypto era) (Hash (Crypto era) EraIndependentTxBody),
    Default (LedgerState era)
  ) =>
  STS (LEDGERS era)
  where
  type State (LEDGERS era) = LedgerState era
  type Signal (LEDGERS era) = Seq (Core.Tx era)
  type Environment (LEDGERS era) = LedgersEnv era
  type BaseM (LEDGERS era) = ShelleyBase
  type PredicateFailure (LEDGERS era) = LedgersPredicateFailure era
  type Event (LEDGERS era) = LedgersEvent era

  transitionRules :: [TransitionRule (LEDGERS era)]
transitionRules = [TransitionRule (LEDGERS era)
forall era.
(Embed (EraRule "LEDGER" era) (LEDGERS era),
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 Signal (EraRule "LEDGER" era) ~ Tx era) =>
TransitionRule (LEDGERS era)
ledgersTransition]

ledgersTransition ::
  forall era.
  ( Embed (Core.EraRule "LEDGER" era) (LEDGERS era),
    Environment (Core.EraRule "LEDGER" era) ~ LedgerEnv era,
    State (Core.EraRule "LEDGER" era) ~ LedgerState era,
    Signal (Core.EraRule "LEDGER" era) ~ Core.Tx era
  ) =>
  TransitionRule (LEDGERS era)
ledgersTransition :: TransitionRule (LEDGERS era)
ledgersTransition = do
  TRC (LedgersEnv slot pp account, State (LEDGERS era)
ls, Signal (LEDGERS era)
txwits) <- F (Clause (LEDGERS era) 'Transition) (TRC (LEDGERS era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
  (LedgerState era
 -> (TxIx, Tx era)
 -> F (Clause (LEDGERS era) 'Transition) (LedgerState era))
-> LedgerState era
-> [(TxIx, Tx era)]
-> F (Clause (LEDGERS era) 'Transition) (LedgerState era)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM
    ( \ !LedgerState era
ls' (TxIx
ix, Tx era
tx) ->
        forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
forall super (rtype :: RuleType).
Embed (EraRule "LEDGER" era) super =>
RuleContext rtype (EraRule "LEDGER" era)
-> Rule super rtype (State (EraRule "LEDGER" era))
trans @(Core.EraRule "LEDGER" era) (RuleContext 'Transition (EraRule "LEDGER" era)
 -> Rule (LEDGERS era) 'Transition (State (EraRule "LEDGER" era)))
-> RuleContext 'Transition (EraRule "LEDGER" era)
-> Rule (LEDGERS era) 'Transition (State (EraRule "LEDGER" era))
forall a b. (a -> b) -> a -> b
$
          (Environment (EraRule "LEDGER" era), State (EraRule "LEDGER" era),
 Signal (EraRule "LEDGER" era))
-> TRC (EraRule "LEDGER" era)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (SlotNo -> TxIx -> PParams era -> AccountState -> LedgerEnv era
forall era.
SlotNo -> TxIx -> PParams era -> AccountState -> LedgerEnv era
LedgerEnv SlotNo
slot TxIx
ix PParams era
pp AccountState
account, State (EraRule "LEDGER" era)
LedgerState era
ls', Tx era
Signal (EraRule "LEDGER" era)
tx)
    )
    State (LEDGERS era)
LedgerState era
ls
    ([(TxIx, Tx era)]
 -> F (Clause (LEDGERS era) 'Transition) (LedgerState era))
-> [(TxIx, Tx era)]
-> F (Clause (LEDGERS era) 'Transition) (LedgerState era)
forall a b. (a -> b) -> a -> b
$ [TxIx] -> [Tx era] -> [(TxIx, Tx era)]
forall a b. [a] -> [b] -> [(a, b)]
zip [TxIx
forall a. Bounded a => a
minBound ..] ([Tx era] -> [(TxIx, Tx era)]) -> [Tx era] -> [(TxIx, Tx era)]
forall a b. (a -> b) -> a -> b
$ Seq (Tx era) -> [Tx era]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Seq (Tx era)
Signal (LEDGERS era)
txwits

instance
  ( Era era,
    STS (LEDGER era),
    PredicateFailure (Core.EraRule "LEDGER" era) ~ LedgerPredicateFailure era,
    Event (Core.EraRule "LEDGER" era) ~ LedgerEvent era
  ) =>
  Embed (LEDGER era) (LEDGERS era)
  where
  wrapFailed :: PredicateFailure (LEDGER era) -> PredicateFailure (LEDGERS era)
wrapFailed = PredicateFailure (LEDGER era) -> PredicateFailure (LEDGERS era)
forall era.
PredicateFailure (EraRule "LEDGER" era)
-> LedgersPredicateFailure era
LedgerFailure
  wrapEvent :: Event (LEDGER era) -> Event (LEDGERS era)
wrapEvent = Event (LEDGER era) -> Event (LEDGERS era)
forall era. Event (EraRule "LEDGER" era) -> LedgersEvent era
LedgerEvent