{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Deleg () where

import Cardano.Ledger.BaseTypes
import Cardano.Ledger.Conway.Rules (
  ConwayDelegEnv (..),
  ConwayDelegPredFailure,
 )
import Cardano.Ledger.Conway.TxCert (
  ConwayDelegCert (..),
  getStakePoolDelegatee,
  getVoteDelegatee,
 )
import Cardano.Ledger.Core
import Cardano.Ledger.Credential (Credential)
import Cardano.Ledger.Shelley.LedgerState (DState (..))
import Cardano.Ledger.Shelley.Rules
import qualified Cardano.Ledger.UMap as UMap
import qualified Data.Map.Strict as Map
import Data.Set (Set)
import qualified Lib as Agda
import Test.Cardano.Ledger.Conformance (
  hashToInteger,
 )
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base
import Test.Cardano.Ledger.Conformance.SpecTranslate.Core

instance
  ( SpecRep (PParamsHKD Identity era) ~ Agda.PParams
  , SpecTranslate ctx (PParamsHKD Identity era)
  , Inject ctx (Set (Credential 'DRepRole))
  ) =>
  SpecTranslate ctx (ConwayDelegEnv era)
  where
  type SpecRep (ConwayDelegEnv era) = Agda.DelegEnv

  toSpecRep :: ConwayDelegEnv era -> SpecTransM ctx (SpecRep (ConwayDelegEnv era))
toSpecRep ConwayDelegEnv {Map (KeyHash 'StakePool) PoolParams
PParams era
cdePParams :: forall era. ConwayDelegEnv era -> PParams era
cdePools :: forall era.
ConwayDelegEnv era -> Map (KeyHash 'StakePool) PoolParams
cdePools :: Map (KeyHash 'StakePool) PoolParams
cdePParams :: PParams era
..} = do
    Set (Credential 'DRepRole)
delegatees <- forall b ctx. Inject ctx b => SpecTransM ctx b
askCtx @(Set (Credential 'DRepRole))
    PParams -> HSMap Integer PoolParams -> HSSet Credential -> DelegEnv
Agda.MkDelegEnv
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep PParams era
cdePParams
      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
Map.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
cdePools)
      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 Set (Credential 'DRepRole)
delegatees

instance SpecTranslate ctx ConwayDelegCert where
  type SpecRep ConwayDelegCert = Agda.DCert

  toSpecRep :: ConwayDelegCert -> SpecTransM ctx (SpecRep ConwayDelegCert)
toSpecRep (ConwayRegCert StakeCredential
c StrictMaybe Coin
d) =
    Credential -> Integer -> DCert
Agda.Reg
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep StakeCredential
c
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a b. a -> (b -> a) -> StrictMaybe b -> a
strictMaybe (forall (f :: * -> *) a. Applicative f => a -> f a
pure Integer
0) forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep StrictMaybe Coin
d
  toSpecRep (ConwayUnRegCert StakeCredential
c StrictMaybe Coin
d) =
    Credential -> Integer -> DCert
Agda.Dereg
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep StakeCredential
c
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a b. a -> (b -> a) -> StrictMaybe b -> a
strictMaybe (forall (f :: * -> *) a. Applicative f => a -> f a
pure Integer
0) forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep StrictMaybe Coin
d
  toSpecRep (ConwayDelegCert StakeCredential
c Delegatee
d) =
    Credential -> Maybe VDeleg -> Maybe Integer -> Integer -> DCert
Agda.Delegate
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep StakeCredential
c
      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 (Delegatee -> Maybe DRep
getVoteDelegatee Delegatee
d)
      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 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Delegatee -> Maybe (KeyHash 'StakePool)
getStakePoolDelegatee Delegatee
d)
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure Integer
0
  toSpecRep (ConwayRegDelegCert StakeCredential
s Delegatee
d Coin
c) =
    Credential -> Maybe VDeleg -> Maybe Integer -> Integer -> DCert
Agda.Delegate
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep StakeCredential
s
      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 (Delegatee -> Maybe DRep
getVoteDelegatee Delegatee
d)
      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 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Delegatee -> Maybe (KeyHash 'StakePool)
getStakePoolDelegatee Delegatee
d)
      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 Coin
c

instance SpecTranslate ctx (ConwayDelegPredFailure era) where
  type SpecRep (ConwayDelegPredFailure era) = OpaqueErrorString

  toSpecRep :: ConwayDelegPredFailure era
-> SpecTransM ctx (SpecRep (ConwayDelegPredFailure 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 (DState era) where
  type SpecRep (DState era) = Agda.DState

  toSpecRep :: DState era -> SpecTransM ctx (SpecRep (DState era))
toSpecRep DState {Map FutureGenDeleg GenDelegPair
InstantaneousRewards
UMap
GenDelegs
dsUnified :: forall era. DState era -> UMap
dsFutureGenDelegs :: forall era. DState era -> Map FutureGenDeleg GenDelegPair
dsGenDelegs :: forall era. DState era -> GenDelegs
dsIRewards :: forall era. DState era -> InstantaneousRewards
dsIRewards :: InstantaneousRewards
dsGenDelegs :: GenDelegs
dsFutureGenDelegs :: Map FutureGenDeleg GenDelegPair
dsUnified :: UMap
..} =
    HSMap Credential VDeleg
-> HSMap Credential Integer
-> HSMap Credential Integer
-> HSMap DepositPurpose Integer
-> DState
Agda.MkDState
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (UMap -> Map StakeCredential DRep
UMap.dRepMap UMap
dsUnified)
      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 (UMap -> Map StakeCredential (KeyHash 'StakePool)
UMap.sPoolMap UMap
dsUnified)
      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 (UMap -> Map StakeCredential Coin
UMap.rewardMap UMap
dsUnified)
      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 Map DepositPurpose Coin
deposits
    where
      deposits :: Map DepositPurpose Coin
deposits =
        forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys StakeCredential -> DepositPurpose
CredentialDeposit (UMap -> Map StakeCredential Coin
UMap.depositMap UMap
dsUnified)