{-# 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.Shelley.Rules
import Cardano.Ledger.State
import qualified Data.Map.Strict as Map
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 (PState era) where
  type SpecRep (PState era) = Agda.PState

  toSpecRep :: PState era -> SpecTransM ctx (SpecRep (PState era))
toSpecRep PState {Map (KeyHash 'StakePool) StakePoolState
Map (KeyHash 'StakePool) EpochNo
Map (VRFVerKeyHash 'StakePoolVRF) (NonZero Word64)
psVRFKeyHashes :: Map (VRFVerKeyHash 'StakePoolVRF) (NonZero Word64)
psStakePools :: Map (KeyHash 'StakePool) StakePoolState
psFutureStakePools :: Map (KeyHash 'StakePool) StakePoolState
psRetiring :: Map (KeyHash 'StakePool) EpochNo
psVRFKeyHashes :: forall era.
PState era -> Map (VRFVerKeyHash 'StakePoolVRF) (NonZero Word64)
psStakePools :: forall era. PState era -> Map (KeyHash 'StakePool) StakePoolState
psFutureStakePools :: forall era. PState era -> Map (KeyHash 'StakePool) StakePoolState
psRetiring :: forall era. PState era -> Map (KeyHash 'StakePool) EpochNo
..} =
    HSMap Integer StakePoolParams -> HSMap Integer Integer -> PState
Agda.MkPState
      (HSMap Integer StakePoolParams -> HSMap Integer Integer -> PState)
-> SpecTransM ctx (HSMap Integer StakePoolParams)
-> 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 ((KeyHash 'StakePool -> StakePoolState -> PoolParams)
-> Map (KeyHash 'StakePool) StakePoolState
-> Map (KeyHash 'StakePool) PoolParams
forall k a b. (k -> a -> b) -> Map k a -> Map k b
Map.mapWithKey KeyHash 'StakePool -> StakePoolState -> PoolParams
stakePoolStateToPoolParams Map (KeyHash 'StakePool) StakePoolState
psStakePools)
      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 -> StakePoolParams -> DCert
Agda.Regpool
      (Integer -> StakePoolParams -> DCert)
-> SpecTransM ctx Integer
-> SpecTransM ctx (StakePoolParams -> 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 (StakePoolParams -> DCert)
-> SpecTransM ctx StakePoolParams -> 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