{-# LANGUAGE DataKinds #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Enact () where

import Cardano.Ledger.BaseTypes (EpochNo)
import Cardano.Ledger.Conway (ConwayEra)
import Cardano.Ledger.Conway.Governance (EnactState (..))
import Cardano.Ledger.Conway.Rules (EnactSignal (..))
import Control.State.Transition.Extended (TRC (..))
import qualified MAlonzo.Code.Ledger.Foreign.API as Agda
import Test.Cardano.Ledger.Conformance (
  ExecSpecRule (..),
  SpecTRC (..),
  SpecTranslate (..),
  runSpecTransM,
  unComputationResult,
 )
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway ()
import Test.Cardano.Ledger.Conway.ImpTest ()

instance ExecSpecRule "ENACT" ConwayEra where
  type ExecContext "ENACT" ConwayEra = EpochNo
  type SpecEnvironment "ENACT" ConwayEra = Agda.EnactEnv

  translateInputs :: HasCallStack =>
ExecContext "ENACT" ConwayEra
-> TRC (EraRule "ENACT" ConwayEra)
-> Either Text (SpecTRC "ENACT" ConwayEra)
translateInputs ExecContext "ENACT" ConwayEra
ctx (TRC (Environment (EraRule "ENACT" ConwayEra)
_, st :: State (EraRule "ENACT" ConwayEra)
st@EnactState {Map (Credential 'Staking) Coin
StrictMaybe (Committee ConwayEra)
PParams ConwayEra
Constitution ConwayEra
GovRelation StrictMaybe
Coin
ensCommittee :: StrictMaybe (Committee ConwayEra)
ensConstitution :: Constitution ConwayEra
ensCurPParams :: PParams ConwayEra
ensPrevPParams :: PParams ConwayEra
ensTreasury :: Coin
ensWithdrawals :: Map (Credential 'Staking) Coin
ensPrevGovActionIds :: GovRelation StrictMaybe
ensCommittee :: forall era. EnactState era -> StrictMaybe (Committee era)
ensConstitution :: forall era. EnactState era -> Constitution era
ensCurPParams :: forall era. EnactState era -> PParams era
ensPrevPParams :: forall era. EnactState era -> PParams era
ensTreasury :: forall era. EnactState era -> Coin
ensWithdrawals :: forall era. EnactState era -> Map (Credential 'Staking) Coin
ensPrevGovActionIds :: forall era. EnactState era -> GovRelation StrictMaybe
..}, sig :: Signal (EraRule "ENACT" ConwayEra)
sig@EnactSignal {GovAction ConwayEra
GovActionId
esGovActionId :: GovActionId
esGovAction :: GovAction ConwayEra
esGovActionId :: forall era. EnactSignal era -> GovActionId
esGovAction :: forall era. EnactSignal era -> GovAction era
..})) =
    ()
-> SpecTransM () (SpecTRC "ENACT" ConwayEra)
-> Either Text (SpecTRC "ENACT" ConwayEra)
forall ctx a. ctx -> SpecTransM ctx a -> Either Text a
runSpecTransM () (SpecTransM () (SpecTRC "ENACT" ConwayEra)
 -> Either Text (SpecTRC "ENACT" ConwayEra))
-> SpecTransM () (SpecTRC "ENACT" ConwayEra)
-> Either Text (SpecTRC "ENACT" ConwayEra)
forall a b. (a -> b) -> a -> b
$ do
      SpecRep (EnactState ConwayEra)
agdaSt <- EnactState ConwayEra
-> SpecTransM () (SpecRep (EnactState ConwayEra))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep EnactState ConwayEra
State (EraRule "ENACT" ConwayEra)
st
      SpecRep (EnactSignal ConwayEra)
agdaSig <- EnactSignal ConwayEra
-> SpecTransM () (SpecRep (EnactSignal ConwayEra))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep EnactSignal ConwayEra
Signal (EraRule "ENACT" ConwayEra)
sig
      Integer
treasury <- Coin -> SpecTransM () (SpecRep Coin)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Coin
ensTreasury
      (Integer, Integer)
gaId <- GovActionId -> SpecTransM () (SpecRep GovActionId)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep GovActionId
esGovActionId
      Integer
curEpoch <- EpochNo -> SpecTransM () (SpecRep EpochNo)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep EpochNo
ExecContext "ENACT" ConwayEra
ctx
      SpecTRC "ENACT" ConwayEra
-> SpecTransM () (SpecTRC "ENACT" ConwayEra)
forall a. a -> SpecTransM () a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SpecTRC "ENACT" ConwayEra
 -> SpecTransM () (SpecTRC "ENACT" ConwayEra))
-> SpecTRC "ENACT" ConwayEra
-> SpecTransM () (SpecTRC "ENACT" ConwayEra)
forall a b. (a -> b) -> a -> b
$
        SpecEnvironment "ENACT" ConwayEra
-> SpecState "ENACT" ConwayEra
-> SpecSignal "ENACT" ConwayEra
-> SpecTRC "ENACT" ConwayEra
forall (rule :: Symbol) era.
SpecEnvironment rule era
-> SpecState rule era -> SpecSignal rule era -> SpecTRC rule era
SpecTRC
          ((Integer, Integer) -> Integer -> Integer -> EnactEnv
Agda.MkEnactEnv (Integer, Integer)
gaId Integer
treasury Integer
curEpoch)
          SpecRep (EnactState ConwayEra)
SpecState "ENACT" ConwayEra
agdaSt
          SpecRep (EnactSignal ConwayEra)
SpecSignal "ENACT" ConwayEra
agdaSig

  runAgdaRule :: HasCallStack =>
SpecTRC "ENACT" ConwayEra
-> Either Text (SpecState "ENACT" ConwayEra)
runAgdaRule (SpecTRC SpecEnvironment "ENACT" ConwayEra
env SpecState "ENACT" ConwayEra
st SpecSignal "ENACT" ConwayEra
sig) = ComputationResult Text EnactState -> Either Text EnactState
forall a. ComputationResult Text a -> Either Text a
unComputationResult (ComputationResult Text EnactState -> Either Text EnactState)
-> ComputationResult Text EnactState -> Either Text EnactState
forall a b. (a -> b) -> a -> b
$ EnactEnv
-> EnactState -> GovAction -> ComputationResult Text EnactState
Agda.enactStep EnactEnv
SpecEnvironment "ENACT" ConwayEra
env EnactState
SpecState "ENACT" ConwayEra
st GovAction
SpecSignal "ENACT" ConwayEra
sig