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

instance
  ( SpecRep (PParamsHKD Identity era) ~ Agda.PParams
  , SpecTranslate ctx (PParamsHKD Identity era)
  , Inject ctx (Set (Credential 'DRepRole (EraCrypto 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
..} = do
    Set (Credential 'DRepRole (EraCrypto era))
delegatees <- forall b ctx. Inject ctx b => SpecTransM ctx b
askCtx @(Set (Credential 'DRepRole (EraCrypto era)))
    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) c.
KeyHash r c -> Hash (ADDRHASH c) (VerKeyDSIGN (DSIGN c))
unKeyHash) Map
  (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era))
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 (EraCrypto era))
delegatees

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 (r :: KeyRole) c.
KeyHash r 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 (r :: KeyRole) c.
KeyHash r 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)