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

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

import Cardano.Ledger.Conway (ConwayEra)
import qualified MAlonzo.Code.Ledger.Foreign.API as Agda
import Test.Cardano.Ledger.Conformance (ExecSpecRule (..), runFromAgdaFunction)
import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base (externalFunctions)
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Cert ()
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Utxo ()
import Test.Cardano.Ledger.Constrained.Conway (UtxoExecContext (..))
import Test.Cardano.Ledger.Generic.Instances ()

instance ExecSpecRule "UTXO" ConwayEra where
  type ExecContext "UTXO" ConwayEra = UtxoExecContext ConwayEra

  runAgdaRule :: HasCallStack =>
SpecTRC "UTXO" ConwayEra
-> Either Text (SpecState "UTXO" ConwayEra)
runAgdaRule = (SpecEnvironment "UTXO" ConwayEra
 -> SpecState "UTXO" ConwayEra
 -> SpecSignal "UTXO" ConwayEra
 -> ComputationResult Text (SpecState "UTXO" ConwayEra))
-> SpecTRC "UTXO" ConwayEra
-> Either Text (SpecState "UTXO" 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 (T_ExternalFunctions_8
-> UTxOEnv
-> UTxOState
-> Tx
-> T_ComputationResult_44 Text UTxOState
Agda.utxoStep T_ExternalFunctions_8
externalFunctions)