{-# 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.Compactible (fromCompact)
import Cardano.Ledger.Conway.Rules (
  ConwayDelegEnv (..),
 )
import Cardano.Ledger.Conway.State
import Cardano.Ledger.Conway.TxCert (
  ConwayDelegCert (..),
  getDRepDelegatee,
  getStakePoolDelegatee,
 )
import Cardano.Ledger.Core
import Cardano.Ledger.Credential (Credential)
import Cardano.Ledger.Shelley.Rules
import qualified Data.Map.Strict as Map
import Data.Set (Set)
import Lens.Micro
import qualified MAlonzo.Code.Ledger.Foreign.API 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) StakePoolState
PParams era
cdePParams :: PParams era
cdePools :: Map (KeyHash 'StakePool) StakePoolState
cdePParams :: forall era. ConwayDelegEnv era -> PParams era
cdePools :: forall era.
ConwayDelegEnv era -> Map (KeyHash 'StakePool) StakePoolState
..} = 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
      (PParams
 -> HSMap Integer PoolParams -> HSSet Credential -> DelegEnv)
-> SpecTransM ctx PParams
-> SpecTransM
     ctx (HSMap Integer PoolParams -> HSSet Credential -> DelegEnv)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PParams era -> SpecTransM ctx (SpecRep (PParams era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep PParams era
cdePParams
      SpecTransM
  ctx (HSMap Integer PoolParams -> HSSet Credential -> DelegEnv)
-> SpecTransM ctx (HSMap Integer PoolParams)
-> SpecTransM ctx (HSSet Credential -> DelegEnv)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Map Integer PoolParams
-> SpecTransM ctx (SpecRep (Map Integer PoolParams))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep
        ((KeyHash 'StakePool -> Integer)
-> Map (KeyHash 'StakePool) PoolParams -> Map Integer PoolParams
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys (Hash ADDRHASH (VerKeyDSIGN DSIGN) -> Integer
forall a b. Hash a b -> Integer
hashToInteger (Hash ADDRHASH (VerKeyDSIGN DSIGN) -> Integer)
-> (KeyHash 'StakePool -> Hash ADDRHASH (VerKeyDSIGN DSIGN))
-> KeyHash 'StakePool
-> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. KeyHash 'StakePool -> Hash ADDRHASH (VerKeyDSIGN DSIGN)
forall (r :: KeyRole).
KeyHash r -> Hash ADDRHASH (VerKeyDSIGN DSIGN)
unKeyHash) (Map (KeyHash 'StakePool) PoolParams -> Map Integer PoolParams)
-> Map (KeyHash 'StakePool) PoolParams -> Map Integer PoolParams
forall a b. (a -> b) -> a -> b
$ (KeyHash 'StakePool -> StakePoolState -> PoolParams)
-> Map (KeyHash 'StakePool) StakePoolState
-> Map (KeyHash 'StakePool) PoolParams
forall k a b. (k -> a -> b) -> Map k a -> Map k b
Map.mapWithKey KeyHash 'StakePool -> StakePoolState -> PoolParams
stakePoolStateToPoolParams Map (KeyHash 'StakePool) StakePoolState
cdePools)
      SpecTransM ctx (HSSet Credential -> DelegEnv)
-> SpecTransM ctx (HSSet Credential) -> SpecTransM ctx DelegEnv
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Set (Credential 'DRepRole)
-> SpecTransM ctx (SpecRep (Set (Credential 'DRepRole)))
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
      (Credential -> Integer -> DCert)
-> SpecTransM ctx Credential -> SpecTransM ctx (Integer -> DCert)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StakeCredential -> SpecTransM ctx (SpecRep StakeCredential)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep StakeCredential
c
      SpecTransM ctx (Integer -> DCert)
-> SpecTransM ctx Integer -> SpecTransM ctx DCert
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SpecTransM ctx Integer
-> (Coin -> SpecTransM ctx Integer)
-> StrictMaybe Coin
-> SpecTransM ctx Integer
forall a b. a -> (b -> a) -> StrictMaybe b -> a
strictMaybe (Integer -> SpecTransM ctx Integer
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Integer
0) Coin -> SpecTransM ctx Integer
Coin -> SpecTransM ctx (SpecRep Coin)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep StrictMaybe Coin
d
  toSpecRep (ConwayUnRegCert StakeCredential
c StrictMaybe Coin
d) =
    Credential -> Maybe Integer -> DCert
Agda.Dereg
      (Credential -> Maybe Integer -> DCert)
-> SpecTransM ctx Credential
-> SpecTransM ctx (Maybe Integer -> DCert)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StakeCredential -> SpecTransM ctx (SpecRep StakeCredential)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep StakeCredential
c
      SpecTransM ctx (Maybe Integer -> DCert)
-> SpecTransM ctx (Maybe Integer) -> SpecTransM ctx DCert
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StrictMaybe Coin -> SpecTransM ctx (SpecRep (StrictMaybe Coin))
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
      (Credential -> Maybe VDeleg -> Maybe Integer -> Integer -> DCert)
-> SpecTransM ctx Credential
-> SpecTransM
     ctx (Maybe VDeleg -> Maybe Integer -> Integer -> DCert)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StakeCredential -> SpecTransM ctx (SpecRep StakeCredential)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep StakeCredential
c
      SpecTransM ctx (Maybe VDeleg -> Maybe Integer -> Integer -> DCert)
-> SpecTransM ctx (Maybe VDeleg)
-> SpecTransM ctx (Maybe Integer -> Integer -> DCert)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe DRep -> SpecTransM ctx (SpecRep (Maybe DRep))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (Delegatee -> Maybe DRep
getDRepDelegatee Delegatee
d)
      SpecTransM ctx (Maybe Integer -> Integer -> DCert)
-> SpecTransM ctx (Maybe Integer)
-> SpecTransM ctx (Integer -> DCert)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe Integer -> SpecTransM ctx (SpecRep (Maybe Integer))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (Hash ADDRHASH (VerKeyDSIGN DSIGN) -> Integer
forall a b. Hash a b -> Integer
hashToInteger (Hash ADDRHASH (VerKeyDSIGN DSIGN) -> Integer)
-> (KeyHash 'StakePool -> Hash ADDRHASH (VerKeyDSIGN DSIGN))
-> KeyHash 'StakePool
-> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. KeyHash 'StakePool -> Hash ADDRHASH (VerKeyDSIGN DSIGN)
forall (r :: KeyRole).
KeyHash r -> Hash ADDRHASH (VerKeyDSIGN DSIGN)
unKeyHash (KeyHash 'StakePool -> Integer)
-> Maybe (KeyHash 'StakePool) -> Maybe Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Delegatee -> Maybe (KeyHash 'StakePool)
getStakePoolDelegatee Delegatee
d)
      SpecTransM ctx (Integer -> DCert)
-> SpecTransM ctx Integer -> SpecTransM ctx DCert
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Integer -> SpecTransM ctx Integer
forall a. a -> SpecTransM ctx a
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
      (Credential -> Maybe VDeleg -> Maybe Integer -> Integer -> DCert)
-> SpecTransM ctx Credential
-> SpecTransM
     ctx (Maybe VDeleg -> Maybe Integer -> Integer -> DCert)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StakeCredential -> SpecTransM ctx (SpecRep StakeCredential)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep StakeCredential
s
      SpecTransM ctx (Maybe VDeleg -> Maybe Integer -> Integer -> DCert)
-> SpecTransM ctx (Maybe VDeleg)
-> SpecTransM ctx (Maybe Integer -> Integer -> DCert)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe DRep -> SpecTransM ctx (SpecRep (Maybe DRep))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (Delegatee -> Maybe DRep
getDRepDelegatee Delegatee
d)
      SpecTransM ctx (Maybe Integer -> Integer -> DCert)
-> SpecTransM ctx (Maybe Integer)
-> SpecTransM ctx (Integer -> DCert)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe Integer -> SpecTransM ctx (SpecRep (Maybe Integer))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (Hash ADDRHASH (VerKeyDSIGN DSIGN) -> Integer
forall a b. Hash a b -> Integer
hashToInteger (Hash ADDRHASH (VerKeyDSIGN DSIGN) -> Integer)
-> (KeyHash 'StakePool -> Hash ADDRHASH (VerKeyDSIGN DSIGN))
-> KeyHash 'StakePool
-> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. KeyHash 'StakePool -> Hash ADDRHASH (VerKeyDSIGN DSIGN)
forall (r :: KeyRole).
KeyHash r -> Hash ADDRHASH (VerKeyDSIGN DSIGN)
unKeyHash (KeyHash 'StakePool -> Integer)
-> Maybe (KeyHash 'StakePool) -> Maybe Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Delegatee -> Maybe (KeyHash 'StakePool)
getStakePoolDelegatee Delegatee
d)
      SpecTransM ctx (Integer -> DCert)
-> SpecTransM ctx Integer -> SpecTransM ctx DCert
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Coin -> SpecTransM ctx (SpecRep Coin)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Coin
c

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

  toSpecRep :: DState era -> SpecTransM ctx (SpecRep (DState era))
toSpecRep DState era
dState =
    HSMap Credential VDeleg
-> HSMap Credential Integer
-> HSMap Credential Integer
-> HSMap DepositPurpose Integer
-> DState
Agda.MkDState
      (HSMap Credential VDeleg
 -> HSMap Credential Integer
 -> HSMap Credential Integer
 -> HSMap DepositPurpose Integer
 -> DState)
-> SpecTransM ctx (HSMap Credential VDeleg)
-> SpecTransM
     ctx
     (HSMap Credential Integer
      -> HSMap Credential Integer
      -> HSMap DepositPurpose Integer
      -> DState)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map StakeCredential DRep
-> SpecTransM ctx (SpecRep (Map StakeCredential DRep))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep ((AccountState era -> Maybe DRep)
-> Map StakeCredential (AccountState era)
-> Map StakeCredential DRep
forall a b k. (a -> Maybe b) -> Map k a -> Map k b
Map.mapMaybe (AccountState era
-> Getting (Maybe DRep) (AccountState era) (Maybe DRep)
-> Maybe DRep
forall s a. s -> Getting a s a -> a
^. Getting (Maybe DRep) (AccountState era) (Maybe DRep)
forall era.
ConwayEraAccounts era =>
Lens' (AccountState era) (Maybe DRep)
Lens' (AccountState era) (Maybe DRep)
dRepDelegationAccountStateL) Map StakeCredential (AccountState era)
accountsMap)
      SpecTransM
  ctx
  (HSMap Credential Integer
   -> HSMap Credential Integer
   -> HSMap DepositPurpose Integer
   -> DState)
-> SpecTransM ctx (HSMap Credential Integer)
-> SpecTransM
     ctx
     (HSMap Credential Integer
      -> HSMap DepositPurpose Integer -> DState)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Map StakeCredential (KeyHash 'StakePool)
-> SpecTransM
     ctx (SpecRep (Map StakeCredential (KeyHash 'StakePool)))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep ((AccountState era -> Maybe (KeyHash 'StakePool))
-> Map StakeCredential (AccountState era)
-> Map StakeCredential (KeyHash 'StakePool)
forall a b k. (a -> Maybe b) -> Map k a -> Map k b
Map.mapMaybe (AccountState era
-> Getting
     (Maybe (KeyHash 'StakePool))
     (AccountState era)
     (Maybe (KeyHash 'StakePool))
-> Maybe (KeyHash 'StakePool)
forall s a. s -> Getting a s a -> a
^. Getting
  (Maybe (KeyHash 'StakePool))
  (AccountState era)
  (Maybe (KeyHash 'StakePool))
forall era.
EraAccounts era =>
Lens' (AccountState era) (Maybe (KeyHash 'StakePool))
Lens' (AccountState era) (Maybe (KeyHash 'StakePool))
stakePoolDelegationAccountStateL) Map StakeCredential (AccountState era)
accountsMap)
      SpecTransM
  ctx
  (HSMap Credential Integer
   -> HSMap DepositPurpose Integer -> DState)
-> SpecTransM ctx (HSMap Credential Integer)
-> SpecTransM ctx (HSMap DepositPurpose Integer -> DState)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Map StakeCredential Coin
-> SpecTransM ctx (SpecRep (Map StakeCredential Coin))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep ((AccountState era -> Coin)
-> Map StakeCredential (AccountState era)
-> Map StakeCredential Coin
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (CompactForm Coin -> Coin
forall a. Compactible a => CompactForm a -> a
fromCompact (CompactForm Coin -> Coin)
-> (AccountState era -> CompactForm Coin)
-> AccountState era
-> Coin
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AccountState era
-> Getting (CompactForm Coin) (AccountState era) (CompactForm Coin)
-> CompactForm Coin
forall s a. s -> Getting a s a -> a
^. Getting (CompactForm Coin) (AccountState era) (CompactForm Coin)
forall era.
EraAccounts era =>
Lens' (AccountState era) (CompactForm Coin)
Lens' (AccountState era) (CompactForm Coin)
balanceAccountStateL)) Map StakeCredential (AccountState era)
accountsMap)
      SpecTransM ctx (HSMap DepositPurpose Integer -> DState)
-> SpecTransM ctx (HSMap DepositPurpose Integer)
-> SpecTransM ctx DState
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SpecTransM ctx (HSMap DepositPurpose Integer)
deposits
    where
      accountsMap :: Map StakeCredential (AccountState era)
accountsMap = DState era
dState DState era
-> Getting
     (Map StakeCredential (AccountState era))
     (DState era)
     (Map StakeCredential (AccountState era))
-> Map StakeCredential (AccountState era)
forall s a. s -> Getting a s a -> a
^. (Accounts era
 -> Const (Map StakeCredential (AccountState era)) (Accounts era))
-> DState era
-> Const (Map StakeCredential (AccountState era)) (DState era)
forall era. Lens' (DState era) (Accounts era)
forall (t :: * -> *) era.
CanSetAccounts t =>
Lens' (t era) (Accounts era)
accountsL ((Accounts era
  -> Const (Map StakeCredential (AccountState era)) (Accounts era))
 -> DState era
 -> Const (Map StakeCredential (AccountState era)) (DState era))
-> ((Map StakeCredential (AccountState era)
     -> Const
          (Map StakeCredential (AccountState era))
          (Map StakeCredential (AccountState era)))
    -> Accounts era
    -> Const (Map StakeCredential (AccountState era)) (Accounts era))
-> Getting
     (Map StakeCredential (AccountState era))
     (DState era)
     (Map StakeCredential (AccountState era))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map StakeCredential (AccountState era)
 -> Const
      (Map StakeCredential (AccountState era))
      (Map StakeCredential (AccountState era)))
-> Accounts era
-> Const (Map StakeCredential (AccountState era)) (Accounts era)
forall era.
EraAccounts era =>
Lens' (Accounts era) (Map StakeCredential (AccountState era))
Lens' (Accounts era) (Map StakeCredential (AccountState era))
accountsMapL
      deposits :: SpecTransM ctx (HSMap DepositPurpose Integer)
deposits = do
        let
          m :: Map StakeCredential Coin
m = (AccountState era -> Coin)
-> Map StakeCredential (AccountState era)
-> Map StakeCredential Coin
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (CompactForm Coin -> Coin
forall a. Compactible a => CompactForm a -> a
fromCompact (CompactForm Coin -> Coin)
-> (AccountState era -> CompactForm Coin)
-> AccountState era
-> Coin
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AccountState era
-> Getting (CompactForm Coin) (AccountState era) (CompactForm Coin)
-> CompactForm Coin
forall s a. s -> Getting a s a -> a
^. Getting (CompactForm Coin) (AccountState era) (CompactForm Coin)
forall era.
EraAccounts era =>
Lens' (AccountState era) (CompactForm Coin)
Lens' (AccountState era) (CompactForm Coin)
depositAccountStateL)) Map StakeCredential (AccountState era)
accountsMap
          transEntry :: (a, a) -> SpecTransM ctx (DepositPurpose, SpecRep a)
transEntry (a
cred, a
val) =
            (,)
              (DepositPurpose -> SpecRep a -> (DepositPurpose, SpecRep a))
-> SpecTransM ctx DepositPurpose
-> SpecTransM ctx (SpecRep a -> (DepositPurpose, SpecRep a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Credential -> DepositPurpose
Agda.CredentialDeposit (Credential -> DepositPurpose)
-> SpecTransM ctx Credential -> SpecTransM ctx DepositPurpose
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> SpecTransM ctx (SpecRep a)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep a
cred)
              SpecTransM ctx (SpecRep a -> (DepositPurpose, SpecRep a))
-> SpecTransM ctx (SpecRep a)
-> SpecTransM ctx (DepositPurpose, SpecRep a)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> a -> SpecTransM ctx (SpecRep a)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep a
val
        [(DepositPurpose, Integer)] -> HSMap DepositPurpose Integer
forall k v. [(k, v)] -> HSMap k v
Agda.MkHSMap ([(DepositPurpose, Integer)] -> HSMap DepositPurpose Integer)
-> SpecTransM ctx [(DepositPurpose, Integer)]
-> SpecTransM ctx (HSMap DepositPurpose Integer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((StakeCredential, Coin)
 -> SpecTransM ctx (DepositPurpose, Integer))
-> [(StakeCredential, Coin)]
-> SpecTransM ctx [(DepositPurpose, Integer)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (StakeCredential, Coin) -> SpecTransM ctx (DepositPurpose, Integer)
(StakeCredential, Coin)
-> SpecTransM ctx (DepositPurpose, SpecRep Coin)
forall {a} {ctx} {a}.
(SpecRep a ~ Credential, SpecTranslate ctx a,
 SpecTranslate ctx a) =>
(a, a) -> SpecTransM ctx (DepositPurpose, SpecRep a)
transEntry (Map StakeCredential Coin -> [(StakeCredential, Coin)]
forall k a. Map k a -> [(k, a)]
Map.toList Map StakeCredential Coin
m)