{-# 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