{-# 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]

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