{-# 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 qualified Cardano.Ledger.Conway.Rules as Conway
import Control.State.Transition.Extended (TRC (..))
import qualified MAlonzo.Code.Ledger.Conway.Foreign.API as Agda
import Test.Cardano.Ledger.Conformance.ExecSpecRule.Core (
  ExecSpecRule (..),
  SpecTRC (..),
 )
import Test.Cardano.Ledger.Conformance.SpecTranslate.Base (
  SpecTranslate (..),
  askSpecTransM,
  unComputationResult,
  withCtxSpecTransM,
 )
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 =>
TRC (EraRule "ENACT" ConwayEra)
-> SpecTransM
     ConwayEra
     (ExecContext "ENACT" ConwayEra)
     (SpecTRC "ENACT" ConwayEra)
translateInputs (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@Conway.EnactSignal {GovAction ConwayEra
GovActionId
esGovActionId :: GovActionId
esGovAction :: GovAction ConwayEra
esGovAction :: forall era. EnactSignal era -> GovAction era
esGovActionId :: forall era. EnactSignal era -> GovActionId
..})) = do
    epochNo <- SpecTransM ConwayEra EpochNo EpochNo
forall era ctx. SpecTransM era ctx ctx
askSpecTransM
    withCtxSpecTransM () $ do
      agdaSt <- toSpecRep st
      agdaSig <- toSpecRep sig
      treasury <- toSpecRep ensTreasury
      gaId <- toSpecRep esGovActionId
      curEpoch <- toSpecRep epochNo
      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