{-# 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 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 (..),
  unComputationResult_,
 )
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway ()
import Test.Cardano.Ledger.Conway.ImpTest ()

instance ExecSpecRule "EPOCH" ConwayEra where
  translateInputs :: HasCallStack =>
TRC (EraRule "EPOCH" ConwayEra)
-> SpecTransM
     ConwayEra
     (ExecContext "EPOCH" ConwayEra)
     (SpecTRC "EPOCH" ConwayEra)
translateInputs (TRC (Environment (EraRule "EPOCH" ConwayEra)
env, State (EraRule "EPOCH" ConwayEra)
st, Signal (EraRule "EPOCH" ConwayEra)
sig)) =
    () -> EpochState -> Integer -> SpecTRC "EPOCH" ConwayEra
SpecEnvironment "EPOCH" ConwayEra
-> SpecState "EPOCH" ConwayEra
-> SpecSignal "EPOCH" ConwayEra
-> SpecTRC "EPOCH" ConwayEra
forall (rule :: Symbol) era.
SpecEnvironment rule era
-> SpecState rule era -> SpecSignal rule era -> SpecTRC rule era
SpecTRC (() -> EpochState -> Integer -> SpecTRC "EPOCH" ConwayEra)
-> SpecTransM ConwayEra () ()
-> SpecTransM
     ConwayEra () (EpochState -> Integer -> SpecTRC "EPOCH" ConwayEra)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ()
-> SpecTransM
     ConwayEra (SpecContext ConwayEra ()) (SpecRep ConwayEra ())
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep ()
Environment (EraRule "EPOCH" ConwayEra)
env SpecTransM
  ConwayEra () (EpochState -> Integer -> SpecTRC "EPOCH" ConwayEra)
-> SpecTransM ConwayEra () EpochState
-> SpecTransM ConwayEra () (Integer -> SpecTRC "EPOCH" ConwayEra)
forall a b.
SpecTransM ConwayEra () (a -> b)
-> SpecTransM ConwayEra () a -> SpecTransM ConwayEra () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> EpochState ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (EpochState ConwayEra))
     (SpecRep ConwayEra (EpochState ConwayEra))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep State (EraRule "EPOCH" ConwayEra)
EpochState ConwayEra
st SpecTransM ConwayEra () (Integer -> SpecTRC "EPOCH" ConwayEra)
-> SpecTransM ConwayEra () Integer
-> SpecTransM ConwayEra () (SpecTRC "EPOCH" ConwayEra)
forall a b.
SpecTransM ConwayEra () (a -> b)
-> SpecTransM ConwayEra () a -> SpecTransM ConwayEra () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> EpochNo
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra EpochNo)
     (SpecRep ConwayEra EpochNo)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep EpochNo
Signal (EraRule "EPOCH" ConwayEra)
sig

  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