{-# 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 Constrained.API (Specification (..)) import qualified MAlonzo.Code.Ledger.Foreign.API as Agda import Test.Cardano.Ledger.Conformance ( ExecSpecRule (..), unComputationResult, ) import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway () instance ExecSpecRule "LEDGERS" ConwayEra where type ExecContext "LEDGERS" ConwayEra = EnactState ConwayEra environmentSpec :: HasCallStack => ExecContext "LEDGERS" ConwayEra -> Specification (ExecEnvironment "LEDGERS" ConwayEra) environmentSpec ExecContext "LEDGERS" ConwayEra _ = forall a. Specification a TrueSpec stateSpec :: HasCallStack => ExecContext "LEDGERS" ConwayEra -> ExecEnvironment "LEDGERS" ConwayEra -> Specification (ExecState "LEDGERS" ConwayEra) stateSpec ExecContext "LEDGERS" ConwayEra _ ExecEnvironment "LEDGERS" ConwayEra _ = forall a. Specification a TrueSpec signalSpec :: HasCallStack => ExecContext "LEDGERS" ConwayEra -> ExecEnvironment "LEDGERS" ConwayEra -> ExecState "LEDGERS" ConwayEra -> Specification (ExecSignal "LEDGERS" ConwayEra) signalSpec ExecContext "LEDGERS" ConwayEra _ ExecEnvironment "LEDGERS" ConwayEra _ ExecState "LEDGERS" ConwayEra _ = forall a. Specification a TrueSpec runAgdaRule :: HasCallStack => SpecRep (ExecEnvironment "LEDGERS" ConwayEra) -> SpecRep (ExecState "LEDGERS" ConwayEra) -> SpecRep (ExecSignal "LEDGERS" ConwayEra) -> Either OpaqueErrorString (SpecRep (ExecState "LEDGERS" ConwayEra)) runAgdaRule SpecRep (ExecEnvironment "LEDGERS" ConwayEra) env SpecRep (ExecState "LEDGERS" ConwayEra) st SpecRep (ExecSignal "LEDGERS" ConwayEra) sig = forall a. ComputationResult Text a -> Either OpaqueErrorString a unComputationResult forall a b. (a -> b) -> a -> b $ LEnv -> LState -> [Tx] -> T_ComputationResult_46 Text LState Agda.ledgersStep SpecRep (ExecEnvironment "LEDGERS" ConwayEra) env SpecRep (ExecState "LEDGERS" ConwayEra) st SpecRep (ExecSignal "LEDGERS" ConwayEra) sig