{-# 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.CertState
import Cardano.Ledger.Core
import Cardano.Ledger.PoolParams
import Cardano.Ledger.Shelley.Rules
import Data.Map.Strict (mapKeys)
import qualified Lib 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) = 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 = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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) PoolParams
Map (KeyHash 'StakePool) EpochNo
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
psDeposits :: Map (KeyHash 'StakePool) Coin
psRetiring :: Map (KeyHash 'StakePool) EpochNo
psFutureStakePoolParams :: Map (KeyHash 'StakePool) PoolParams
psStakePoolParams :: Map (KeyHash 'StakePool) PoolParams
..} =
    HSMap Integer PoolParams -> HSMap Integer Integer -> PState
Agda.MkPState
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
mapKeys (forall a b. Hash a b -> Integer
hashToInteger forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (r :: KeyRole).
KeyHash r -> Hash ADDRHASH (VerKeyDSIGN DSIGN)
unKeyHash) Map (KeyHash 'StakePool) PoolParams
psStakePoolParams)
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
mapKeys (forall a b. Hash a b -> Integer
hashToInteger forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (r :: KeyRole).
KeyHash r -> Hash ADDRHASH (VerKeyDSIGN DSIGN)
unKeyHash) 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
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Hash ADDRHASH (VerKeyDSIGN DSIGN)
ppHash
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Hash ADDRHASH (VerKeyDSIGN DSIGN)
ppHash
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep EpochNo
e