{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -Wno-orphans #-} module Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Pool where import Cardano.Ledger.Core import Cardano.Ledger.PoolParams import Cardano.Ledger.Shelley.Rules import Cardano.Ledger.State import qualified MAlonzo.Code.Ledger.Foreign.API as Agda import Test.Cardano.Ledger.Conformance import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base () instance ( SpecRep (PParamsHKD Identity era) ~ Agda.PParams , SpecTranslate ctx (PParamsHKD Identity era) ) => SpecTranslate ctx (PoolEnv era) where type SpecRep (PoolEnv era) = Agda.PParams toSpecRep :: PoolEnv era -> SpecTransM ctx (SpecRep (PoolEnv era)) toSpecRep (PoolEnv EpochNo _ PParams era pp) = PParams era -> SpecTransM ctx (SpecRep (PParams era)) forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep PParams era pp instance SpecTranslate ctx (ShelleyPoolPredFailure era) where type SpecRep (ShelleyPoolPredFailure era) = OpaqueErrorString toSpecRep :: ShelleyPoolPredFailure era -> SpecTransM ctx (SpecRep (ShelleyPoolPredFailure era)) toSpecRep = OpaqueErrorString -> SpecTransM ctx OpaqueErrorString forall a. a -> SpecTransM ctx a forall (f :: * -> *) a. Applicative f => a -> f a pure (OpaqueErrorString -> SpecTransM ctx OpaqueErrorString) -> (ShelleyPoolPredFailure era -> OpaqueErrorString) -> ShelleyPoolPredFailure era -> SpecTransM ctx OpaqueErrorString forall b c a. (b -> c) -> (a -> b) -> a -> c . ShelleyPoolPredFailure era -> OpaqueErrorString forall a. ToExpr a => a -> OpaqueErrorString showOpaqueErrorString instance SpecTranslate ctx (PState era) where type SpecRep (PState era) = Agda.PState toSpecRep :: PState era -> SpecTransM ctx (SpecRep (PState era)) toSpecRep PState {Map (KeyHash 'StakePool) Coin Map (KeyHash 'StakePool) EpochNo Map (KeyHash 'StakePool) PoolParams psStakePoolParams :: Map (KeyHash 'StakePool) PoolParams psFutureStakePoolParams :: Map (KeyHash 'StakePool) PoolParams psRetiring :: Map (KeyHash 'StakePool) EpochNo psDeposits :: Map (KeyHash 'StakePool) Coin psStakePoolParams :: forall era. PState era -> Map (KeyHash 'StakePool) PoolParams psFutureStakePoolParams :: forall era. PState era -> Map (KeyHash 'StakePool) PoolParams psRetiring :: forall era. PState era -> Map (KeyHash 'StakePool) EpochNo psDeposits :: forall era. PState era -> Map (KeyHash 'StakePool) Coin ..} = HSMap Integer PoolParams -> HSMap Integer Integer -> PState Agda.MkPState (HSMap Integer PoolParams -> HSMap Integer Integer -> PState) -> SpecTransM ctx (HSMap Integer PoolParams) -> SpecTransM ctx (HSMap Integer Integer -> PState) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> Map (KeyHash 'StakePool) PoolParams -> SpecTransM ctx (SpecRep (Map (KeyHash 'StakePool) PoolParams)) forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep Map (KeyHash 'StakePool) PoolParams psStakePoolParams SpecTransM ctx (HSMap Integer Integer -> PState) -> SpecTransM ctx (HSMap Integer Integer) -> SpecTransM ctx PState forall a b. SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b <*> Map (KeyHash 'StakePool) EpochNo -> SpecTransM ctx (SpecRep (Map (KeyHash 'StakePool) EpochNo)) forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep Map (KeyHash 'StakePool) EpochNo psRetiring instance SpecTranslate ctx PoolCert where type SpecRep PoolCert = Agda.DCert toSpecRep :: PoolCert -> SpecTransM ctx (SpecRep PoolCert) toSpecRep (RegPool p :: PoolParams p@PoolParams {ppId :: PoolParams -> KeyHash 'StakePool ppId = KeyHash Hash ADDRHASH (VerKeyDSIGN DSIGN) ppHash}) = Integer -> PoolParams -> DCert Agda.Regpool (Integer -> PoolParams -> DCert) -> SpecTransM ctx Integer -> SpecTransM ctx (PoolParams -> DCert) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> Hash ADDRHASH (VerKeyDSIGN DSIGN) -> SpecTransM ctx (SpecRep (Hash ADDRHASH (VerKeyDSIGN DSIGN))) forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep Hash ADDRHASH (VerKeyDSIGN DSIGN) ppHash SpecTransM ctx (PoolParams -> DCert) -> SpecTransM ctx PoolParams -> SpecTransM ctx DCert forall a b. SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b <*> PoolParams -> SpecTransM ctx (SpecRep PoolParams) forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep PoolParams p toSpecRep (RetirePool (KeyHash Hash ADDRHASH (VerKeyDSIGN DSIGN) ppHash) EpochNo e) = Integer -> Integer -> DCert Agda.Retirepool (Integer -> Integer -> DCert) -> SpecTransM ctx Integer -> SpecTransM ctx (Integer -> DCert) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> Hash ADDRHASH (VerKeyDSIGN DSIGN) -> SpecTransM ctx (SpecRep (Hash ADDRHASH (VerKeyDSIGN DSIGN))) forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep Hash ADDRHASH (VerKeyDSIGN DSIGN) ppHash SpecTransM ctx (Integer -> DCert) -> SpecTransM ctx Integer -> SpecTransM ctx DCert forall a b. SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b <*> EpochNo -> SpecTransM ctx (SpecRep EpochNo) forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep EpochNo e