{-# 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.Keys
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 ()
import Test.Cardano.Ledger.Conway.TreeDiff

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 SlotNo
_ 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 ShelleyPoolPredFailure era
e = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> OpaqueErrorString
OpaqueErrorString forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ forall a. ToExpr a => a -> Expr
toExpr ShelleyPoolPredFailure era
e

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 (EraCrypto era)) Coin
Map
  (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era))
Map (KeyHash 'StakePool (EraCrypto era)) EpochNo
psStakePoolParams :: forall era.
PState era
-> Map
     (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era))
psFutureStakePoolParams :: forall era.
PState era
-> Map
     (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era))
psRetiring :: forall era.
PState era -> Map (KeyHash 'StakePool (EraCrypto era)) EpochNo
psDeposits :: forall era.
PState era -> Map (KeyHash 'StakePool (EraCrypto era)) Coin
psDeposits :: Map (KeyHash 'StakePool (EraCrypto era)) Coin
psRetiring :: Map (KeyHash 'StakePool (EraCrypto era)) EpochNo
psFutureStakePoolParams :: Map
  (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era))
psStakePoolParams :: Map
  (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era))
..} =
    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 (discriminator :: KeyRole) c.
KeyHash discriminator c
-> Hash (ADDRHASH c) (VerKeyDSIGN (DSIGN c))
unKeyHash) Map
  (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era))
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 (discriminator :: KeyRole) c.
KeyHash discriminator c
-> Hash (ADDRHASH c) (VerKeyDSIGN (DSIGN c))
unKeyHash) Map (KeyHash 'StakePool (EraCrypto era)) EpochNo
psRetiring)

instance SpecTranslate ctx (PoolCert c) where
  type SpecRep (PoolCert c) = Agda.DCert

  toSpecRep :: PoolCert c -> SpecTransM ctx (SpecRep (PoolCert c))
toSpecRep (RegPool p :: PoolParams c
p@PoolParams {ppId :: forall c. PoolParams c -> KeyHash 'StakePool c
ppId = KeyHash Hash (ADDRHASH c) (VerKeyDSIGN (DSIGN c))
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 c) (VerKeyDSIGN (DSIGN c))
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 c
p
  toSpecRep (RetirePool (KeyHash Hash (ADDRHASH c) (VerKeyDSIGN (DSIGN c))
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 c) (VerKeyDSIGN (DSIGN c))
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