{-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -Wno-orphans #-} module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Pool where import Cardano.Ledger.Conway import Cardano.Ledger.Core (PoolCert (..)) import qualified MAlonzo.Code.Ledger.Foreign.API as Agda import Test.Cardano.Ledger.Conformance import Test.Cardano.Ledger.Conformance.ExecSpecRule.Core () import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base () import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Pool () import Test.Cardano.Ledger.Constrained.Conway import Test.Cardano.Ledger.Constrained.Conway.WitnessUniverse instance ExecSpecRule "POOL" ConwayEra where type ExecContext "POOL" ConwayEra = WitUniv ConwayEra environmentSpec :: HasCallStack => ExecContext "POOL" ConwayEra -> Specification (ExecEnvironment "POOL" ConwayEra) environmentSpec ExecContext "POOL" ConwayEra ctx = forall era. EraSpecPParams era => WitUniv era -> Specification (PoolEnv era) poolEnvSpec ExecContext "POOL" ConwayEra ctx stateSpec :: HasCallStack => ExecContext "POOL" ConwayEra -> ExecEnvironment "POOL" ConwayEra -> Specification (ExecState "POOL" ConwayEra) stateSpec ExecContext "POOL" ConwayEra ctx ExecEnvironment "POOL" ConwayEra _ = forall era. Era era => WitUniv era -> Specification (PState era) pStateSpec ExecContext "POOL" ConwayEra ctx signalSpec :: HasCallStack => ExecContext "POOL" ConwayEra -> ExecEnvironment "POOL" ConwayEra -> ExecState "POOL" ConwayEra -> Specification (ExecSignal "POOL" ConwayEra) signalSpec ExecContext "POOL" ConwayEra wituniv ExecEnvironment "POOL" ConwayEra env ExecState "POOL" ConwayEra st = forall era. EraSpecPParams era => WitUniv era -> PoolEnv era -> PState era -> Specification PoolCert poolCertSpec @ConwayEra ExecContext "POOL" ConwayEra wituniv ExecEnvironment "POOL" ConwayEra env ExecState "POOL" ConwayEra st runAgdaRule :: HasCallStack => SpecRep (ExecEnvironment "POOL" ConwayEra) -> SpecRep (ExecState "POOL" ConwayEra) -> SpecRep (ExecSignal "POOL" ConwayEra) -> Either OpaqueErrorString (SpecRep (ExecState "POOL" ConwayEra)) runAgdaRule SpecRep (ExecEnvironment "POOL" ConwayEra) env SpecRep (ExecState "POOL" ConwayEra) st SpecRep (ExecSignal "POOL" ConwayEra) sig = forall a. ComputationResult Text a -> Either OpaqueErrorString a unComputationResult forall a b. (a -> b) -> a -> b $ PParams -> PState -> DCert -> T_ComputationResult_46 Text PState Agda.poolStep SpecRep (ExecEnvironment "POOL" ConwayEra) env SpecRep (ExecState "POOL" ConwayEra) st SpecRep (ExecSignal "POOL" ConwayEra) sig classOf :: ExecSignal "POOL" ConwayEra -> Maybe String classOf = forall a. a -> Maybe a Just forall b c a. (b -> c) -> (a -> b) -> a -> c . PoolCert -> String namePoolCert namePoolCert :: PoolCert -> String namePoolCert :: PoolCert -> String namePoolCert RegPool {} = String "RegPool" namePoolCert RetirePool {} = String "RetirePool"