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

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

import Cardano.Ledger.Conway (ConwayEra)
import Cardano.Ledger.Conway.Governance (GovActionState)
import qualified MAlonzo.Code.Ledger.Foreign.API as Agda
import Test.Cardano.Ledger.Conformance (ExecSpecRule (..), SpecTRC (..), unComputationResult_)
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway ()
import Test.Cardano.Ledger.Conway.ImpTest ()

instance ExecSpecRule "EPOCH" ConwayEra where
  type ExecContext "EPOCH" ConwayEra = [GovActionState ConwayEra]

  runAgdaRule :: HasCallStack =>
SpecTRC "EPOCH" ConwayEra
-> Either Text (SpecState "EPOCH" ConwayEra)
runAgdaRule (SpecTRC SpecEnvironment "EPOCH" ConwayEra
env SpecState "EPOCH" ConwayEra
st SpecSignal "EPOCH" ConwayEra
sig) = ComputationResult Void EpochState -> Either Text EpochState
forall a e. ComputationResult Void a -> Either e a
unComputationResult_ (ComputationResult Void EpochState -> Either Text EpochState)
-> ComputationResult Void EpochState -> Either Text EpochState
forall a b. (a -> b) -> a -> b
$ () -> EpochState -> Integer -> ComputationResult Void EpochState
Agda.epochStep ()
SpecEnvironment "EPOCH" ConwayEra
env EpochState
SpecState "EPOCH" ConwayEra
st Integer
SpecSignal "EPOCH" ConwayEra
sig