{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

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

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

instance ExecSpecRule "LEDGERS" ConwayEra where
  type ExecContext "LEDGERS" ConwayEra = EnactState ConwayEra

  runAgdaRule :: HasCallStack =>
SpecTRC "LEDGERS" ConwayEra
-> Either Text (SpecState "LEDGERS" ConwayEra)
runAgdaRule = (SpecEnvironment "LEDGERS" ConwayEra
 -> SpecState "LEDGERS" ConwayEra
 -> SpecSignal "LEDGERS" ConwayEra
 -> ComputationResult Text (SpecState "LEDGERS" ConwayEra))
-> SpecTRC "LEDGERS" ConwayEra
-> Either Text (SpecState "LEDGERS" ConwayEra)
forall (rule :: Symbol) era.
(SpecEnvironment rule era
 -> SpecState rule era
 -> SpecSignal rule era
 -> ComputationResult Text (SpecState rule era))
-> SpecTRC rule era -> Either Text (SpecState rule era)
runFromAgdaFunction LEnv -> LState -> [Tx] -> T_ComputationResult_44 Text LState
SpecEnvironment "LEDGERS" ConwayEra
-> SpecState "LEDGERS" ConwayEra
-> SpecSignal "LEDGERS" ConwayEra
-> ComputationResult Text (SpecState "LEDGERS" ConwayEra)
Agda.ledgersStep