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

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

import Cardano.Ledger.Compactible (fromCompact)
import Cardano.Ledger.Conway.State
import Cardano.Ledger.Conway.TxCert (
  getDRepDelegatee,
  getStakePoolDelegatee,
 )
import Cardano.Ledger.Core
import Cardano.Ledger.Dijkstra (DijkstraEra)
import Cardano.Ledger.Dijkstra.TxCert (DijkstraDelegCert (..))
import qualified Data.Map.Strict as Map
import Lens.Micro
import Lens.Micro.Extras (view)
import qualified MAlonzo.Code.Ledger.Dijkstra.Foreign.API as Agda
import Test.Cardano.Ledger.Conformance.SpecTranslate.Base
import Test.Cardano.Ledger.Conformance.SpecTranslate.Dijkstra.Base ()
import Test.Cardano.Ledger.Conformance.Utils (hashToInteger)

instance SpecTranslate DijkstraEra DijkstraDelegCert where
  type SpecRep DijkstraEra DijkstraDelegCert = Agda.DCert

  toSpecRep :: DijkstraDelegCert
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra DijkstraDelegCert)
     (SpecRep DijkstraEra DijkstraDelegCert)
toSpecRep (DijkstraRegCert Credential Staking
c Coin
d) =
    Credential -> Maybe VDeleg -> Maybe Integer -> Integer -> DCert
Agda.Delegate
      (Credential -> Maybe VDeleg -> Maybe Integer -> Integer -> DCert)
-> SpecTransM DijkstraEra () Credential
-> SpecTransM
     DijkstraEra () (Maybe VDeleg -> Maybe Integer -> Integer -> DCert)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Credential Staking
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (Credential Staking))
     (SpecRep DijkstraEra (Credential Staking))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep Credential Staking
c
      SpecTransM
  DijkstraEra () (Maybe VDeleg -> Maybe Integer -> Integer -> DCert)
-> SpecTransM DijkstraEra () (Maybe VDeleg)
-> SpecTransM DijkstraEra () (Maybe Integer -> Integer -> DCert)
forall a b.
SpecTransM DijkstraEra () (a -> b)
-> SpecTransM DijkstraEra () a -> SpecTransM DijkstraEra () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe VDeleg -> SpecTransM DijkstraEra () (Maybe VDeleg)
forall a. a -> SpecTransM DijkstraEra () a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe VDeleg
forall a. Maybe a
Nothing
      SpecTransM DijkstraEra () (Maybe Integer -> Integer -> DCert)
-> SpecTransM DijkstraEra () (Maybe Integer)
-> SpecTransM DijkstraEra () (Integer -> DCert)
forall a b.
SpecTransM DijkstraEra () (a -> b)
-> SpecTransM DijkstraEra () a -> SpecTransM DijkstraEra () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe Integer -> SpecTransM DijkstraEra () (Maybe Integer)
forall a. a -> SpecTransM DijkstraEra () a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Integer
forall a. Maybe a
Nothing
      SpecTransM DijkstraEra () (Integer -> DCert)
-> SpecTransM DijkstraEra () Integer
-> SpecTransM DijkstraEra () DCert
forall a b.
SpecTransM DijkstraEra () (a -> b)
-> SpecTransM DijkstraEra () a -> SpecTransM DijkstraEra () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Coin
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra Coin)
     (SpecRep DijkstraEra Coin)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep Coin
d
  toSpecRep (DijkstraUnRegCert Credential Staking
c Coin
d) =
    Credential -> Maybe Integer -> DCert
Agda.Dereg
      (Credential -> Maybe Integer -> DCert)
-> SpecTransM DijkstraEra () Credential
-> SpecTransM DijkstraEra () (Maybe Integer -> DCert)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Credential Staking
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (Credential Staking))
     (SpecRep DijkstraEra (Credential Staking))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep Credential Staking
c
      SpecTransM DijkstraEra () (Maybe Integer -> DCert)
-> SpecTransM DijkstraEra () (Maybe Integer)
-> SpecTransM DijkstraEra () DCert
forall a b.
SpecTransM DijkstraEra () (a -> b)
-> SpecTransM DijkstraEra () a -> SpecTransM DijkstraEra () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe Coin
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (Maybe Coin))
     (SpecRep DijkstraEra (Maybe Coin))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep (Coin -> Maybe Coin
forall a. a -> Maybe a
Just Coin
d)
  toSpecRep (DijkstraDelegCert Credential Staking
c Delegatee
d) =
    Credential -> Maybe VDeleg -> Maybe Integer -> Integer -> DCert
Agda.Delegate
      (Credential -> Maybe VDeleg -> Maybe Integer -> Integer -> DCert)
-> SpecTransM DijkstraEra () Credential
-> SpecTransM
     DijkstraEra () (Maybe VDeleg -> Maybe Integer -> Integer -> DCert)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Credential Staking
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (Credential Staking))
     (SpecRep DijkstraEra (Credential Staking))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep Credential Staking
c
      SpecTransM
  DijkstraEra () (Maybe VDeleg -> Maybe Integer -> Integer -> DCert)
-> SpecTransM DijkstraEra () (Maybe VDeleg)
-> SpecTransM DijkstraEra () (Maybe Integer -> Integer -> DCert)
forall a b.
SpecTransM DijkstraEra () (a -> b)
-> SpecTransM DijkstraEra () a -> SpecTransM DijkstraEra () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe DRep
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (Maybe DRep))
     (SpecRep DijkstraEra (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 DijkstraEra () (Maybe Integer -> Integer -> DCert)
-> SpecTransM DijkstraEra () (Maybe Integer)
-> SpecTransM DijkstraEra () (Integer -> DCert)
forall a b.
SpecTransM DijkstraEra () (a -> b)
-> SpecTransM DijkstraEra () a -> SpecTransM DijkstraEra () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe Integer
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (Maybe Integer))
     (SpecRep DijkstraEra (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 DijkstraEra () (Integer -> DCert)
-> SpecTransM DijkstraEra () Integer
-> SpecTransM DijkstraEra () DCert
forall a b.
SpecTransM DijkstraEra () (a -> b)
-> SpecTransM DijkstraEra () a -> SpecTransM DijkstraEra () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Integer -> SpecTransM DijkstraEra () Integer
forall a. a -> SpecTransM DijkstraEra () a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Integer
0
  toSpecRep (DijkstraRegDelegCert Credential Staking
s Delegatee
d Coin
c) =
    Credential -> Maybe VDeleg -> Maybe Integer -> Integer -> DCert
Agda.Delegate
      (Credential -> Maybe VDeleg -> Maybe Integer -> Integer -> DCert)
-> SpecTransM DijkstraEra () Credential
-> SpecTransM
     DijkstraEra () (Maybe VDeleg -> Maybe Integer -> Integer -> DCert)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Credential Staking
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (Credential Staking))
     (SpecRep DijkstraEra (Credential Staking))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep Credential Staking
s
      SpecTransM
  DijkstraEra () (Maybe VDeleg -> Maybe Integer -> Integer -> DCert)
-> SpecTransM DijkstraEra () (Maybe VDeleg)
-> SpecTransM DijkstraEra () (Maybe Integer -> Integer -> DCert)
forall a b.
SpecTransM DijkstraEra () (a -> b)
-> SpecTransM DijkstraEra () a -> SpecTransM DijkstraEra () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe DRep
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (Maybe DRep))
     (SpecRep DijkstraEra (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 DijkstraEra () (Maybe Integer -> Integer -> DCert)
-> SpecTransM DijkstraEra () (Maybe Integer)
-> SpecTransM DijkstraEra () (Integer -> DCert)
forall a b.
SpecTransM DijkstraEra () (a -> b)
-> SpecTransM DijkstraEra () a -> SpecTransM DijkstraEra () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe Integer
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (Maybe Integer))
     (SpecRep DijkstraEra (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 DijkstraEra () (Integer -> DCert)
-> SpecTransM DijkstraEra () Integer
-> SpecTransM DijkstraEra () DCert
forall a b.
SpecTransM DijkstraEra () (a -> b)
-> SpecTransM DijkstraEra () a -> SpecTransM DijkstraEra () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Coin
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra Coin)
     (SpecRep DijkstraEra Coin)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep Coin
c

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

  toSpecRep :: DState DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (DState DijkstraEra))
     (SpecRep DijkstraEra (DState DijkstraEra))
toSpecRep DState DijkstraEra
dState =
    HSMap Credential VDeleg
-> HSMap Credential Integer
-> HSMap Credential Integer
-> HSMap Credential Integer
-> DState
Agda.MkDState
      (HSMap Credential VDeleg
 -> HSMap Credential Integer
 -> HSMap Credential Integer
 -> HSMap Credential Integer
 -> DState)
-> SpecTransM DijkstraEra () (HSMap Credential VDeleg)
-> SpecTransM
     DijkstraEra
     ()
     (HSMap Credential Integer
      -> HSMap Credential Integer -> HSMap Credential Integer -> DState)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map (Credential Staking) DRep
-> SpecTransM
     DijkstraEra
     ()
     (HSMap
        (SpecRep DijkstraEra (Credential Staking))
        (SpecRep DijkstraEra 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 DijkstraEra -> Maybe DRep)
-> Map (Credential Staking) (AccountState DijkstraEra)
-> Map (Credential Staking) DRep
forall a b k. (a -> Maybe b) -> Map k a -> Map k b
Map.mapMaybe (Getting (Maybe DRep) (AccountState DijkstraEra) (Maybe DRep)
-> AccountState DijkstraEra -> Maybe DRep
forall a s. Getting a s a -> s -> a
view Getting (Maybe DRep) (AccountState DijkstraEra) (Maybe DRep)
forall era.
ConwayEraAccounts era =>
Lens' (AccountState era) (Maybe DRep)
Lens' (AccountState DijkstraEra) (Maybe DRep)
dRepDelegationAccountStateL) Map (Credential Staking) (AccountState DijkstraEra)
accountsMap)
      SpecTransM
  DijkstraEra
  ()
  (HSMap Credential Integer
   -> HSMap Credential Integer -> HSMap Credential Integer -> DState)
-> SpecTransM DijkstraEra () (HSMap Credential Integer)
-> SpecTransM
     DijkstraEra
     ()
     (HSMap Credential Integer -> HSMap Credential Integer -> DState)
forall a b.
SpecTransM DijkstraEra () (a -> b)
-> SpecTransM DijkstraEra () a -> SpecTransM DijkstraEra () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Map (Credential Staking) (KeyHash StakePool)
-> SpecTransM
     DijkstraEra
     ()
     (HSMap
        (SpecRep DijkstraEra (Credential Staking))
        (SpecRep DijkstraEra (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 DijkstraEra -> Maybe (KeyHash StakePool))
-> Map (Credential Staking) (AccountState DijkstraEra)
-> 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 DijkstraEra)
  (Maybe (KeyHash StakePool))
-> AccountState DijkstraEra -> Maybe (KeyHash StakePool)
forall a s. Getting a s a -> s -> a
view Getting
  (Maybe (KeyHash StakePool))
  (AccountState DijkstraEra)
  (Maybe (KeyHash StakePool))
forall era.
EraAccounts era =>
Lens' (AccountState era) (Maybe (KeyHash StakePool))
Lens' (AccountState DijkstraEra) (Maybe (KeyHash StakePool))
stakePoolDelegationAccountStateL) Map (Credential Staking) (AccountState DijkstraEra)
accountsMap)
      SpecTransM
  DijkstraEra
  ()
  (HSMap Credential Integer -> HSMap Credential Integer -> DState)
-> SpecTransM DijkstraEra () (HSMap Credential Integer)
-> SpecTransM DijkstraEra () (HSMap Credential Integer -> DState)
forall a b.
SpecTransM DijkstraEra () (a -> b)
-> SpecTransM DijkstraEra () a -> SpecTransM DijkstraEra () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Map (Credential Staking) Coin
-> SpecTransM
     DijkstraEra
     ()
     (HSMap
        (SpecRep DijkstraEra (Credential Staking))
        (SpecRep DijkstraEra 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 DijkstraEra -> Coin)
-> Map (Credential Staking) (AccountState DijkstraEra)
-> 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 DijkstraEra -> CompactForm Coin)
-> AccountState DijkstraEra
-> Coin
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting
  (CompactForm Coin) (AccountState DijkstraEra) (CompactForm Coin)
-> AccountState DijkstraEra -> CompactForm Coin
forall a s. Getting a s a -> s -> a
view Getting
  (CompactForm Coin) (AccountState DijkstraEra) (CompactForm Coin)
forall era.
EraAccounts era =>
Lens' (AccountState era) (CompactForm Coin)
Lens' (AccountState DijkstraEra) (CompactForm Coin)
balanceAccountStateL) Map (Credential Staking) (AccountState DijkstraEra)
accountsMap)
      SpecTransM DijkstraEra () (HSMap Credential Integer -> DState)
-> SpecTransM DijkstraEra () (HSMap Credential Integer)
-> SpecTransM DijkstraEra () DState
forall a b.
SpecTransM DijkstraEra () (a -> b)
-> SpecTransM DijkstraEra () a -> SpecTransM DijkstraEra () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Map (Credential Staking) Coin
-> SpecTransM
     DijkstraEra
     ()
     (HSMap
        (SpecRep DijkstraEra (Credential Staking))
        (SpecRep DijkstraEra 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 DijkstraEra -> Coin)
-> Map (Credential Staking) (AccountState DijkstraEra)
-> 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 DijkstraEra -> CompactForm Coin)
-> AccountState DijkstraEra
-> Coin
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting
  (CompactForm Coin) (AccountState DijkstraEra) (CompactForm Coin)
-> AccountState DijkstraEra -> CompactForm Coin
forall a s. Getting a s a -> s -> a
view Getting
  (CompactForm Coin) (AccountState DijkstraEra) (CompactForm Coin)
forall era.
EraAccounts era =>
Lens' (AccountState era) (CompactForm Coin)
Lens' (AccountState DijkstraEra) (CompactForm Coin)
depositAccountStateL) Map (Credential Staking) (AccountState DijkstraEra)
accountsMap)
    where
      accountsMap :: Map (Credential Staking) (AccountState DijkstraEra)
accountsMap = DState DijkstraEra
dState DState DijkstraEra
-> Getting
     (Map (Credential Staking) (AccountState DijkstraEra))
     (DState DijkstraEra)
     (Map (Credential Staking) (AccountState DijkstraEra))
-> Map (Credential Staking) (AccountState DijkstraEra)
forall s a. s -> Getting a s a -> a
^. (Accounts DijkstraEra
 -> Const
      (Map (Credential Staking) (AccountState DijkstraEra))
      (Accounts DijkstraEra))
-> DState DijkstraEra
-> Const
     (Map (Credential Staking) (AccountState DijkstraEra))
     (DState DijkstraEra)
(ConwayAccounts DijkstraEra
 -> Const
      (Map (Credential Staking) (AccountState DijkstraEra))
      (ConwayAccounts DijkstraEra))
-> DState DijkstraEra
-> Const
     (Map (Credential Staking) (AccountState DijkstraEra))
     (DState DijkstraEra)
forall era. Lens' (DState era) (Accounts era)
forall (t :: * -> *) era.
CanSetAccounts t =>
Lens' (t era) (Accounts era)
accountsL ((ConwayAccounts DijkstraEra
  -> Const
       (Map (Credential Staking) (AccountState DijkstraEra))
       (ConwayAccounts DijkstraEra))
 -> DState DijkstraEra
 -> Const
      (Map (Credential Staking) (AccountState DijkstraEra))
      (DState DijkstraEra))
-> ((Map (Credential Staking) (AccountState DijkstraEra)
     -> Const
          (Map (Credential Staking) (AccountState DijkstraEra))
          (Map (Credential Staking) (AccountState DijkstraEra)))
    -> ConwayAccounts DijkstraEra
    -> Const
         (Map (Credential Staking) (AccountState DijkstraEra))
         (ConwayAccounts DijkstraEra))
-> Getting
     (Map (Credential Staking) (AccountState DijkstraEra))
     (DState DijkstraEra)
     (Map (Credential Staking) (AccountState DijkstraEra))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map (Credential Staking) (AccountState DijkstraEra)
 -> Const
      (Map (Credential Staking) (AccountState DijkstraEra))
      (Map (Credential Staking) (AccountState DijkstraEra)))
-> Accounts DijkstraEra
-> Const
     (Map (Credential Staking) (AccountState DijkstraEra))
     (Accounts DijkstraEra)
(Map (Credential Staking) (AccountState DijkstraEra)
 -> Const
      (Map (Credential Staking) (AccountState DijkstraEra))
      (Map (Credential Staking) (AccountState DijkstraEra)))
-> ConwayAccounts DijkstraEra
-> Const
     (Map (Credential Staking) (AccountState DijkstraEra))
     (ConwayAccounts DijkstraEra)
forall era.
EraAccounts era =>
Lens' (Accounts era) (Map (Credential Staking) (AccountState era))
Lens'
  (Accounts DijkstraEra)
  (Map (Credential Staking) (AccountState DijkstraEra))
accountsMapL