{-# 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 (ConwayEra)
import qualified Cardano.Ledger.Conway.Rules as Conway
import Cardano.Ledger.Conway.State
import Cardano.Ledger.Conway.TxCert (
  ConwayDelegCert (..),
  getDRepDelegatee,
  getStakePoolDelegatee,
 )
import Cardano.Ledger.Core
import Cardano.Ledger.Credential (Credential)
import qualified Data.Map.Strict as Map
import Data.Set (Set)
import Lens.Micro
import Lens.Micro.Extras (view)
import qualified MAlonzo.Code.Ledger.Conway.Foreign.API as Agda
import Test.Cardano.Ledger.Conformance (
  hashToInteger,
 )
import Test.Cardano.Ledger.Conformance.SpecTranslate.Base
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base ()

instance SpecTranslate ConwayEra (Conway.ConwayDelegEnv ConwayEra) where
  type SpecRep ConwayEra (Conway.ConwayDelegEnv ConwayEra) = Agda.DelegEnv
  type SpecContext ConwayEra (Conway.ConwayDelegEnv ConwayEra) = Set (Credential DRepRole)

  toSpecRep :: ConwayDelegEnv ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (ConwayDelegEnv ConwayEra))
     (SpecRep ConwayEra (ConwayDelegEnv ConwayEra))
toSpecRep Conway.ConwayDelegEnv {Map (KeyHash StakePool) StakePoolState
PParams ConwayEra
cdePParams :: PParams ConwayEra
cdePools :: Map (KeyHash StakePool) StakePoolState
cdePools :: forall era.
ConwayDelegEnv era -> Map (KeyHash StakePool) StakePoolState
cdePParams :: forall era. ConwayDelegEnv era -> PParams era
..} = do
    delegatees <- SpecTransM
  ConwayEra (Set (Credential DRepRole)) (Set (Credential DRepRole))
forall era ctx. SpecTransM era ctx ctx
askSpecTransM
    withCtxSpecTransM () $
      Agda.MkDelegEnv
        <$> toSpecRep cdePParams
        <*> ( toSpecRepMap
                ( Map.mapKeys (hashToInteger . unKeyHash) $
                    Map.mapWithKey (stakePoolStateToStakePoolParams Testnet) cdePools
                )
            )
        <*> toSpecRep delegatees

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

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

instance SpecTranslate ConwayEra (DState ConwayEra) where
  type SpecRep ConwayEra (DState ConwayEra) = Agda.DState

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