{-# 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
ensPrevGovActionIds :: forall era. EnactState era -> GovRelation StrictMaybe
ensWithdrawals :: forall era. EnactState era -> Map (Credential Staking) Coin
ensTreasury :: forall era. EnactState era -> Coin
ensPrevPParams :: forall era. EnactState era -> PParams era
ensCurPParams :: forall era. EnactState era -> PParams era
ensConstitution :: forall era. EnactState era -> Constitution era
ensCommittee :: forall era. EnactState era -> StrictMaybe (Committee era)
..}, sig :: Signal (EraRule "ENACT" ConwayEra)
sig@EnactSignal {GovAction ConwayEra
GovActionId
esGovActionId :: GovActionId
esGovAction :: GovAction ConwayEra
esGovAction :: forall era. EnactSignal era -> GovAction era
esGovActionId :: forall era. EnactSignal era -> GovActionId
..})) =
    ()
-> 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
      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
      agdaSig <- toSpecRep sig
      treasury <- toSpecRep ensTreasury
      gaId <- toSpecRep esGovActionId
      curEpoch <- toSpecRep ctx
      pure $
        SpecTRC
          (Agda.MkEnactEnv gaId treasury curEpoch)
          agdaSt
          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