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

module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.NewEpoch () 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 "NEWEPOCH" ConwayEra where
  type ExecContext "NEWEPOCH" ConwayEra = [GovActionState ConwayEra]

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