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

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

  toSpecRep :: ConwayDelegEnv era -> SpecTransM ctx (SpecRep (ConwayDelegEnv era))
toSpecRep ConwayDelegEnv {Map
  (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era))
PParams era
cdePParams :: forall era. ConwayDelegEnv era -> PParams era
cdePools :: forall era.
ConwayDelegEnv era
-> Map
     (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era))
cdePools :: Map
  (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era))
cdePParams :: PParams era
..} =
    PParams -> HSMap Integer PoolParams -> 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 (discriminator :: KeyRole) c.
KeyHash discriminator c
-> Hash (ADDRHASH c) (VerKeyDSIGN (DSIGN c))
unKeyHash) Map
  (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era))
cdePools)

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

  toSpecRep :: ConwayDelegCert c -> SpecTransM ctx (SpecRep (ConwayDelegCert c))
toSpecRep (ConwayRegCert StakeCredential c
c StrictMaybe Coin
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
c
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing
      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
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
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
c Delegatee c
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
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 (forall c. Delegatee c -> Maybe (DRep c)
getVoteDelegatee Delegatee c
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 (discriminator :: KeyRole) c.
KeyHash discriminator c
-> Hash (ADDRHASH c) (VerKeyDSIGN (DSIGN c))
unKeyHash forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall c. Delegatee c -> Maybe (KeyHash 'StakePool c)
getStakePoolDelegatee Delegatee c
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 c
s Delegatee c
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 c
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 (forall c. Delegatee c -> Maybe (DRep c)
getVoteDelegatee Delegatee c
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 (discriminator :: KeyRole) c.
KeyHash discriminator c
-> Hash (ADDRHASH c) (VerKeyDSIGN (DSIGN c))
unKeyHash forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall c. Delegatee c -> Maybe (KeyHash 'StakePool c)
getStakePoolDelegatee Delegatee c
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 ConwayDelegPredFailure 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 ConwayDelegPredFailure era
e

instance SpecTranslate ctx (DState era) where
  type SpecRep (DState era) = Agda.DState

  toSpecRep :: DState era -> SpecTransM ctx (SpecRep (DState era))
toSpecRep DState {Map (FutureGenDeleg (EraCrypto era)) (GenDelegPair (EraCrypto era))
InstantaneousRewards (EraCrypto era)
UMap (EraCrypto era)
GenDelegs (EraCrypto era)
dsUnified :: forall era. DState era -> UMap (EraCrypto era)
dsFutureGenDelegs :: forall era.
DState era
-> Map
     (FutureGenDeleg (EraCrypto era)) (GenDelegPair (EraCrypto era))
dsGenDelegs :: forall era. DState era -> GenDelegs (EraCrypto era)
dsIRewards :: forall era. DState era -> InstantaneousRewards (EraCrypto era)
dsIRewards :: InstantaneousRewards (EraCrypto era)
dsGenDelegs :: GenDelegs (EraCrypto era)
dsFutureGenDelegs :: Map (FutureGenDeleg (EraCrypto era)) (GenDelegPair (EraCrypto era))
dsUnified :: UMap (EraCrypto era)
..} =
    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 (forall c. UMap c -> Map (Credential 'Staking c) (DRep c)
UMap.dRepMap UMap (EraCrypto era)
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 (forall c.
UMap c -> Map (Credential 'Staking c) (KeyHash 'StakePool c)
UMap.sPoolMap UMap (EraCrypto era)
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 (forall c. UMap c -> Map (Credential 'Staking c) Coin
UMap.rewardMap UMap (EraCrypto era)
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 (EraCrypto era)) Coin
deposits
    where
      deposits :: Map (DepositPurpose (EraCrypto era)) Coin
deposits =
        forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys forall c. Credential 'Staking c -> DepositPurpose c
CredentialDeposit (forall c. UMap c -> Map (Credential 'Staking c) Coin
UMap.depositMap UMap (EraCrypto era)
dsUnified)