{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_GHC -Wno-orphans #-}

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

import Cardano.Crypto.Leios
import Cardano.Ledger.BaseTypes
import Cardano.Ledger.Coin
import Cardano.Ledger.Conway.Core
import Cardano.Ledger.Conway.Governance
import Cardano.Ledger.Conway.State
import Cardano.Ledger.Dijkstra (DijkstraEra)
import Cardano.Ledger.Rewards (rewardAmount)
import Cardano.Ledger.Shelley.LedgerState
import Data.Foldable (Foldable (..))
import qualified Data.Map.Strict as Map
import qualified Data.VMap as VMap
import qualified Data.Vector.Strict as V
import Lens.Micro
import qualified MAlonzo.Code.Ledger.Dijkstra.Foreign.API as Agda
import Test.Cardano.Ledger.Conformance.SpecTranslate.Base (
  SpecTranslate (..),
  askSpecTransM,
  toSpecRepMap,
  withCtxSpecTransM,
 )
import Test.Cardano.Ledger.Conformance.SpecTranslate.Core (verkeyToInteger)
import Test.Cardano.Ledger.Conformance.SpecTranslate.Dijkstra.Deleg ()
import Test.Cardano.Ledger.Conformance.SpecTranslate.Dijkstra.GovCert ()
import Test.Cardano.Ledger.Conformance.SpecTranslate.Dijkstra.Ledger ()
import Test.Cardano.Ledger.Conformance.SpecTranslate.Dijkstra.Pool ()
import Test.Cardano.Ledger.Shelley.Utils (runShelleyBase)

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

  type SpecContext DijkstraEra (EpochState DijkstraEra) = Network

  toSpecRep :: EpochState DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (EpochState DijkstraEra))
     (SpecRep DijkstraEra (EpochState DijkstraEra))
toSpecRep (EpochState {esLState :: forall era. EpochState era -> LedgerState era
esLState = esLState :: LedgerState DijkstraEra
esLState@LedgerState {UTxOState DijkstraEra
lsUTxOState :: UTxOState DijkstraEra
lsUTxOState :: forall era. LedgerState era -> UTxOState era
lsUTxOState}, ChainAccountState
SnapShots DijkstraEra
NonMyopic
esChainAccountState :: ChainAccountState
esSnapshots :: SnapShots DijkstraEra
esNonMyopic :: NonMyopic
esNonMyopic :: forall era. EpochState era -> NonMyopic
esSnapshots :: forall era. EpochState era -> SnapShots era
esChainAccountState :: forall era. EpochState era -> ChainAccountState
..}) = do
    netId <- SpecTransM DijkstraEra Network Network
forall era ctx. SpecTransM era ctx ctx
askSpecTransM
    withCtxSpecTransM () $
      Agda.MkEpochState
        <$> toSpecRep esChainAccountState
        <*> toSpecRep esSnapshots
        <*> withCtxSpecTransM netId (toSpecRep esLState)
        <*> toSpecRep enactState
        <*> withCtxSpecTransM govActions (toSpecRep ratifyState)
    where
      enactState :: EnactState DijkstraEra
enactState = GovState DijkstraEra -> EnactState DijkstraEra
forall era. ConwayEraGov era => GovState era -> EnactState era
mkEnactState (GovState DijkstraEra -> EnactState DijkstraEra)
-> GovState DijkstraEra -> EnactState DijkstraEra
forall a b. (a -> b) -> a -> b
$ UTxOState DijkstraEra -> GovState DijkstraEra
forall era. UTxOState era -> GovState era
utxosGovState UTxOState DijkstraEra
lsUTxOState
      ratifyState :: RatifyState DijkstraEra
ratifyState = ConwayGovState DijkstraEra -> RatifyState DijkstraEra
forall era.
(ConwayEraAccounts era, EraStake era) =>
ConwayGovState era -> RatifyState era
getRatifyState (ConwayGovState DijkstraEra -> RatifyState DijkstraEra)
-> ConwayGovState DijkstraEra -> RatifyState DijkstraEra
forall a b. (a -> b) -> a -> b
$ UTxOState DijkstraEra -> GovState DijkstraEra
forall era. UTxOState era -> GovState era
utxosGovState UTxOState DijkstraEra
lsUTxOState
      govActions :: [GovActionState DijkstraEra]
govActions = OMap GovActionId (GovActionState DijkstraEra)
-> [GovActionState DijkstraEra]
forall a. OMap GovActionId a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (OMap GovActionId (GovActionState DijkstraEra)
 -> [GovActionState DijkstraEra])
-> OMap GovActionId (GovActionState DijkstraEra)
-> [GovActionState DijkstraEra]
forall a b. (a -> b) -> a -> b
$ UTxOState DijkstraEra
lsUTxOState UTxOState DijkstraEra
-> Getting
     (OMap GovActionId (GovActionState DijkstraEra))
     (UTxOState DijkstraEra)
     (OMap GovActionId (GovActionState DijkstraEra))
-> OMap GovActionId (GovActionState DijkstraEra)
forall s a. s -> Getting a s a -> a
^. (GovState DijkstraEra
 -> Const
      (OMap GovActionId (GovActionState DijkstraEra))
      (GovState DijkstraEra))
-> UTxOState DijkstraEra
-> Const
     (OMap GovActionId (GovActionState DijkstraEra))
     (UTxOState DijkstraEra)
(ConwayGovState DijkstraEra
 -> Const
      (OMap GovActionId (GovActionState DijkstraEra))
      (ConwayGovState DijkstraEra))
-> UTxOState DijkstraEra
-> Const
     (OMap GovActionId (GovActionState DijkstraEra))
     (UTxOState DijkstraEra)
forall era (f :: * -> *).
Functor f =>
(GovState era -> f (GovState era))
-> UTxOState era -> f (UTxOState era)
utxosGovStateL ((ConwayGovState DijkstraEra
  -> Const
       (OMap GovActionId (GovActionState DijkstraEra))
       (ConwayGovState DijkstraEra))
 -> UTxOState DijkstraEra
 -> Const
      (OMap GovActionId (GovActionState DijkstraEra))
      (UTxOState DijkstraEra))
-> ((OMap GovActionId (GovActionState DijkstraEra)
     -> Const
          (OMap GovActionId (GovActionState DijkstraEra))
          (OMap GovActionId (GovActionState DijkstraEra)))
    -> ConwayGovState DijkstraEra
    -> Const
         (OMap GovActionId (GovActionState DijkstraEra))
         (ConwayGovState DijkstraEra))
-> Getting
     (OMap GovActionId (GovActionState DijkstraEra))
     (UTxOState DijkstraEra)
     (OMap GovActionId (GovActionState DijkstraEra))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Proposals DijkstraEra
 -> Const
      (OMap GovActionId (GovActionState DijkstraEra))
      (Proposals DijkstraEra))
-> GovState DijkstraEra
-> Const
     (OMap GovActionId (GovActionState DijkstraEra))
     (GovState DijkstraEra)
(Proposals DijkstraEra
 -> Const
      (OMap GovActionId (GovActionState DijkstraEra))
      (Proposals DijkstraEra))
-> ConwayGovState DijkstraEra
-> Const
     (OMap GovActionId (GovActionState DijkstraEra))
     (ConwayGovState DijkstraEra)
forall era.
ConwayEraGov era =>
Lens' (GovState era) (Proposals era)
Lens' (GovState DijkstraEra) (Proposals DijkstraEra)
proposalsGovStateL ((Proposals DijkstraEra
  -> Const
       (OMap GovActionId (GovActionState DijkstraEra))
       (Proposals DijkstraEra))
 -> ConwayGovState DijkstraEra
 -> Const
      (OMap GovActionId (GovActionState DijkstraEra))
      (ConwayGovState DijkstraEra))
-> ((OMap GovActionId (GovActionState DijkstraEra)
     -> Const
          (OMap GovActionId (GovActionState DijkstraEra))
          (OMap GovActionId (GovActionState DijkstraEra)))
    -> Proposals DijkstraEra
    -> Const
         (OMap GovActionId (GovActionState DijkstraEra))
         (Proposals DijkstraEra))
-> (OMap GovActionId (GovActionState DijkstraEra)
    -> Const
         (OMap GovActionId (GovActionState DijkstraEra))
         (OMap GovActionId (GovActionState DijkstraEra)))
-> ConwayGovState DijkstraEra
-> Const
     (OMap GovActionId (GovActionState DijkstraEra))
     (ConwayGovState DijkstraEra)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (OMap GovActionId (GovActionState DijkstraEra)
 -> Const
      (OMap GovActionId (GovActionState DijkstraEra))
      (OMap GovActionId (GovActionState DijkstraEra)))
-> Proposals DijkstraEra
-> Const
     (OMap GovActionId (GovActionState DijkstraEra))
     (Proposals DijkstraEra)
forall era (f :: * -> *).
Functor f =>
(OMap GovActionId (GovActionState era)
 -> f (OMap GovActionId (GovActionState era)))
-> Proposals era -> f (Proposals era)
pPropsL

instance SpecTranslate DijkstraEra (SnapShots DijkstraEra) where
  type SpecRep DijkstraEra (SnapShots DijkstraEra) = Agda.Snapshots

  toSpecRep :: SnapShots DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (SnapShots DijkstraEra))
     (SpecRep DijkstraEra (SnapShots DijkstraEra))
toSpecRep (SnapShots {GoSnapShot
MarkSnapShot
SetSnapShot
Coin
ssStakeMark :: MarkSnapShot
ssStakeSet :: SetSnapShot
ssStakeGo :: GoSnapShot
ssFee :: Coin
ssFee :: forall era. SnapShots era -> Coin
ssStakeGo :: forall era. SnapShots era -> GoSnapShot
ssStakeMark :: forall era. SnapShots era -> MarkSnapShot
ssStakeSet :: forall era. SnapShots era -> SetSnapShot
..}) =
    Snapshot -> Snapshot -> Snapshot -> Integer -> Snapshots
Agda.MkSnapshots
      (Snapshot -> Snapshot -> Snapshot -> Integer -> Snapshots)
-> SpecTransM DijkstraEra () Snapshot
-> SpecTransM
     DijkstraEra () (Snapshot -> Snapshot -> Integer -> Snapshots)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SnapShot
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra SnapShot)
     (SpecRep DijkstraEra SnapShot)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep (MarkSnapShot -> SnapShot
msSnapShot MarkSnapShot
ssStakeMark)
      SpecTransM
  DijkstraEra () (Snapshot -> Snapshot -> Integer -> Snapshots)
-> SpecTransM DijkstraEra () Snapshot
-> SpecTransM DijkstraEra () (Snapshot -> Integer -> Snapshots)
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
<*> SnapShot
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra SnapShot)
     (SpecRep DijkstraEra SnapShot)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep (SetSnapShot -> SnapShot
ssSnapShot SetSnapShot
ssStakeSet)
      SpecTransM DijkstraEra () (Snapshot -> Integer -> Snapshots)
-> SpecTransM DijkstraEra () Snapshot
-> SpecTransM DijkstraEra () (Integer -> Snapshots)
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
<*> SnapShot
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra SnapShot)
     (SpecRep DijkstraEra SnapShot)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep (GoSnapShot -> SnapShot
gsSnapShot GoSnapShot
ssStakeGo)
      SpecTransM DijkstraEra () (Integer -> Snapshots)
-> SpecTransM DijkstraEra () Integer
-> SpecTransM DijkstraEra () Snapshots
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
ssFee

instance SpecTranslate DijkstraEra SnapShot where
  type SpecRep DijkstraEra SnapShot = Agda.Snapshot

  toSpecRep :: SnapShot
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra SnapShot)
     (SpecRep DijkstraEra SnapShot)
toSpecRep (SnapShot {ActiveStake
NonZero Coin
VMap VB VB (KeyHash StakePool) StakePoolSnapShot
ssActiveStake :: ActiveStake
ssTotalActiveStake :: NonZero Coin
ssStakePoolsSnapShot :: VMap VB VB (KeyHash StakePool) StakePoolSnapShot
ssActiveStake :: SnapShot -> ActiveStake
ssStakePoolsSnapShot :: SnapShot -> VMap VB VB (KeyHash StakePool) StakePoolSnapShot
ssTotalActiveStake :: SnapShot -> NonZero Coin
..}) =
    HSMap Credential Integer
-> HSMap Credential Integer
-> HSMap Integer StakePoolState
-> Snapshot
Agda.MkSnapshot
      (HSMap Credential Integer
 -> HSMap Credential Integer
 -> HSMap Integer StakePoolState
 -> Snapshot)
-> SpecTransM DijkstraEra () (HSMap Credential Integer)
-> SpecTransM
     DijkstraEra
     ()
     (HSMap Credential Integer
      -> HSMap Integer StakePoolState -> Snapshot)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Stake
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra Stake)
     (SpecRep DijkstraEra Stake)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep (VMap VB VP (Credential Staking) (CompactForm Coin) -> Stake
Stake (VMap VB VP (Credential Staking) (CompactForm Coin) -> Stake)
-> VMap VB VP (Credential Staking) (CompactForm Coin) -> Stake
forall a b. (a -> b) -> a -> b
$ Map (Credential Staking) (CompactForm Coin)
-> VMap VB VP (Credential Staking) (CompactForm Coin)
forall (kv :: * -> *) k (vv :: * -> *) v.
(Vector kv k, Vector vv v) =>
Map k v -> VMap kv vv k v
VMap.fromMap (Map (Credential Staking) (CompactForm Coin)
 -> VMap VB VP (Credential Staking) (CompactForm Coin))
-> Map (Credential Staking) (CompactForm Coin)
-> VMap VB VP (Credential Staking) (CompactForm Coin)
forall a b. (a -> b) -> a -> b
$ (StakeWithDelegation -> CompactForm Coin)
-> Map (Credential Staking) StakeWithDelegation
-> Map (Credential Staking) (CompactForm Coin)
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (NonZero (CompactForm Coin) -> CompactForm Coin
forall a. NonZero a -> a
unNonZero (NonZero (CompactForm Coin) -> CompactForm Coin)
-> (StakeWithDelegation -> NonZero (CompactForm Coin))
-> StakeWithDelegation
-> CompactForm Coin
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StakeWithDelegation -> NonZero (CompactForm Coin)
swdStake) Map (Credential Staking) StakeWithDelegation
activeStakeMap)
      SpecTransM
  DijkstraEra
  ()
  (HSMap Credential Integer
   -> HSMap Integer StakePoolState -> Snapshot)
-> SpecTransM DijkstraEra () (HSMap Credential Integer)
-> SpecTransM
     DijkstraEra () (HSMap Integer StakePoolState -> Snapshot)
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 ((StakeWithDelegation -> KeyHash StakePool)
-> Map (Credential Staking) StakeWithDelegation
-> Map (Credential Staking) (KeyHash StakePool)
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map StakeWithDelegation -> KeyHash StakePool
swdDelegation Map (Credential Staking) StakeWithDelegation
activeStakeMap)
      SpecTransM
  DijkstraEra () (HSMap Integer StakePoolState -> Snapshot)
-> SpecTransM DijkstraEra () (HSMap Integer StakePoolState)
-> SpecTransM DijkstraEra () Snapshot
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 (KeyHash StakePool) StakePoolSnapShot
-> SpecTransM
     DijkstraEra
     ()
     (HSMap
        (SpecRep DijkstraEra (KeyHash StakePool))
        (SpecRep DijkstraEra StakePoolSnapShot))
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 (VMap VB VB (KeyHash StakePool) StakePoolSnapShot
-> Map (KeyHash StakePool) StakePoolSnapShot
forall (kv :: * -> *) k (vv :: * -> *) v.
(Vector kv k, Vector vv v) =>
VMap kv vv k v -> Map k v
VMap.toMap VMap VB VB (KeyHash StakePool) StakePoolSnapShot
ssStakePoolsSnapShot)
    where
      activeStakeMap :: Map (Credential Staking) StakeWithDelegation
activeStakeMap = VMap VB VS (Credential Staking) StakeWithDelegation
-> Map (Credential Staking) StakeWithDelegation
forall (kv :: * -> *) k (vv :: * -> *) v.
(Vector kv k, Vector vv v) =>
VMap kv vv k v -> Map k v
VMap.toMap (VMap VB VS (Credential Staking) StakeWithDelegation
 -> Map (Credential Staking) StakeWithDelegation)
-> VMap VB VS (Credential Staking) StakeWithDelegation
-> Map (Credential Staking) StakeWithDelegation
forall a b. (a -> b) -> a -> b
$ ActiveStake -> VMap VB VS (Credential Staking) StakeWithDelegation
unActiveStake ActiveStake
ssActiveStake

instance SpecTranslate DijkstraEra StakePoolSnapShot where
  type SpecRep DijkstraEra StakePoolSnapShot = Agda.StakePoolState

  toSpecRep :: StakePoolSnapShot
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra StakePoolSnapShot)
     (SpecRep DijkstraEra StakePoolSnapShot)
toSpecRep StakePoolSnapShot {Int
Rational
Set (KeyHash Staking)
StrictMaybe BlsKeyState
AccountId
VRFVerKeyHash StakePoolVRF
Coin
CompactForm Coin
UnitInterval
spssStake :: CompactForm Coin
spssStakeRatio :: Rational
spssSelfDelegatedOwners :: Set (KeyHash Staking)
spssSelfDelegatedOwnersStake :: Coin
spssVrf :: VRFVerKeyHash StakePoolVRF
spssBlsKey :: StrictMaybe BlsKeyState
spssPledge :: Coin
spssCost :: Coin
spssMargin :: UnitInterval
spssNumDelegators :: Int
spssAccountId :: AccountId
spssAccountId :: StakePoolSnapShot -> AccountId
spssBlsKey :: StakePoolSnapShot -> StrictMaybe BlsKeyState
spssCost :: StakePoolSnapShot -> Coin
spssMargin :: StakePoolSnapShot -> UnitInterval
spssNumDelegators :: StakePoolSnapShot -> Int
spssPledge :: StakePoolSnapShot -> Coin
spssSelfDelegatedOwners :: StakePoolSnapShot -> Set (KeyHash Staking)
spssSelfDelegatedOwnersStake :: StakePoolSnapShot -> Coin
spssStake :: StakePoolSnapShot -> CompactForm Coin
spssStakeRatio :: StakePoolSnapShot -> Rational
spssVrf :: StakePoolSnapShot -> VRFVerKeyHash StakePoolVRF
..} =
    HSSet Integer
-> Integer
-> Rational
-> Integer
-> RewardAddress
-> Integer
-> Maybe (Integer, Integer)
-> StakePoolState
Agda.StakePoolState
      (HSSet Integer
 -> Integer
 -> Rational
 -> Integer
 -> RewardAddress
 -> Integer
 -> Maybe (Integer, Integer)
 -> StakePoolState)
-> SpecTransM DijkstraEra () (HSSet Integer)
-> SpecTransM
     DijkstraEra
     ()
     (Integer
      -> Rational
      -> Integer
      -> RewardAddress
      -> Integer
      -> Maybe (Integer, Integer)
      -> StakePoolState)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set (KeyHash Staking)
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (Set (KeyHash Staking)))
     (SpecRep DijkstraEra (Set (KeyHash Staking)))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep Set (KeyHash Staking)
spssSelfDelegatedOwners
      SpecTransM
  DijkstraEra
  ()
  (Integer
   -> Rational
   -> Integer
   -> RewardAddress
   -> Integer
   -> Maybe (Integer, Integer)
   -> StakePoolState)
-> SpecTransM DijkstraEra () Integer
-> SpecTransM
     DijkstraEra
     ()
     (Rational
      -> Integer
      -> RewardAddress
      -> Integer
      -> Maybe (Integer, Integer)
      -> StakePoolState)
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
spssCost
      SpecTransM
  DijkstraEra
  ()
  (Rational
   -> Integer
   -> RewardAddress
   -> Integer
   -> Maybe (Integer, Integer)
   -> StakePoolState)
-> SpecTransM DijkstraEra () Rational
-> SpecTransM
     DijkstraEra
     ()
     (Integer
      -> RewardAddress
      -> Integer
      -> Maybe (Integer, Integer)
      -> StakePoolState)
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
<*> UnitInterval
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra UnitInterval)
     (SpecRep DijkstraEra UnitInterval)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep UnitInterval
spssMargin
      SpecTransM
  DijkstraEra
  ()
  (Integer
   -> RewardAddress
   -> Integer
   -> Maybe (Integer, Integer)
   -> StakePoolState)
-> SpecTransM DijkstraEra () Integer
-> SpecTransM
     DijkstraEra
     ()
     (RewardAddress
      -> Integer -> Maybe (Integer, Integer) -> StakePoolState)
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
spssPledge
      SpecTransM
  DijkstraEra
  ()
  (RewardAddress
   -> Integer -> Maybe (Integer, Integer) -> StakePoolState)
-> SpecTransM DijkstraEra () RewardAddress
-> SpecTransM
     DijkstraEra
     ()
     (Integer -> Maybe (Integer, Integer) -> StakePoolState)
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 -> Credential -> RewardAddress
Agda.RewardAddress (Integer -> Credential -> RewardAddress)
-> SpecTransM DijkstraEra () Integer
-> SpecTransM DijkstraEra () (Credential -> RewardAddress)
forall (f :: * -> *) a b. Functor 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 SpecTransM DijkstraEra () (Credential -> RewardAddress)
-> SpecTransM DijkstraEra () Credential
-> SpecTransM DijkstraEra () RewardAddress
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
<*> 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 (AccountId -> Credential Staking
unAccountId AccountId
spssAccountId))
      SpecTransM
  DijkstraEra
  ()
  (Integer -> Maybe (Integer, Integer) -> StakePoolState)
-> SpecTransM DijkstraEra () Integer
-> SpecTransM
     DijkstraEra () (Maybe (Integer, Integer) -> StakePoolState)
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
<*> VRFVerKeyHash StakePoolVRF
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (VRFVerKeyHash StakePoolVRF))
     (SpecRep DijkstraEra (VRFVerKeyHash StakePoolVRF))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep VRFVerKeyHash StakePoolVRF
spssVrf
      SpecTransM
  DijkstraEra () (Maybe (Integer, Integer) -> StakePoolState)
-> SpecTransM DijkstraEra () (Maybe (Integer, Integer))
-> SpecTransM DijkstraEra () StakePoolState
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
<*> StrictMaybe BlsKeyState
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (StrictMaybe BlsKeyState))
     (SpecRep DijkstraEra (StrictMaybe BlsKeyState))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep StrictMaybe BlsKeyState
spssBlsKey

instance SpecTranslate DijkstraEra Stake where
  type SpecRep DijkstraEra Stake = Agda.HSMap Agda.Credential Agda.Coin

  toSpecRep :: Stake
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra Stake)
     (SpecRep DijkstraEra Stake)
toSpecRep (Stake VMap VB VP (Credential Staking) (CompactForm Coin)
stake) = Map (Credential Staking) (CompactForm Coin)
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra Stake)
     (HSMap
        (SpecRep DijkstraEra (Credential Staking))
        (SpecRep DijkstraEra (CompactForm 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 (Map (Credential Staking) (CompactForm Coin)
 -> SpecTransM
      DijkstraEra
      (SpecContext DijkstraEra Stake)
      (HSMap
         (SpecRep DijkstraEra (Credential Staking))
         (SpecRep DijkstraEra (CompactForm Coin))))
-> Map (Credential Staking) (CompactForm Coin)
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra Stake)
     (HSMap
        (SpecRep DijkstraEra (Credential Staking))
        (SpecRep DijkstraEra (CompactForm Coin)))
forall a b. (a -> b) -> a -> b
$ VMap VB VP (Credential Staking) (CompactForm Coin)
-> Map (Credential Staking) (CompactForm Coin)
forall (kv :: * -> *) k (vv :: * -> *) v.
(Vector kv k, Vector vv v) =>
VMap kv vv k v -> Map k v
VMap.toMap VMap VB VP (Credential Staking) (CompactForm Coin)
stake

instance SpecTranslate DijkstraEra ChainAccountState where
  type SpecRep DijkstraEra ChainAccountState = Agda.Acnt

  toSpecRep :: ChainAccountState
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra ChainAccountState)
     (SpecRep DijkstraEra ChainAccountState)
toSpecRep (ChainAccountState {Coin
casTreasury :: Coin
casReserves :: Coin
casReserves :: ChainAccountState -> Coin
casTreasury :: ChainAccountState -> Coin
..}) =
    Integer -> Integer -> Acnt
Agda.MkAcnt
      (Integer -> Integer -> Acnt)
-> SpecTransM DijkstraEra () Integer
-> SpecTransM DijkstraEra () (Integer -> Acnt)
forall (f :: * -> *) a b. Functor 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
casTreasury
      SpecTransM DijkstraEra () (Integer -> Acnt)
-> SpecTransM DijkstraEra () Integer
-> SpecTransM DijkstraEra () Acnt
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
casReserves

instance SpecTranslate DijkstraEra DeltaCoin where
  type SpecRep DijkstraEra DeltaCoin = Integer

  toSpecRep :: DeltaCoin
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra DeltaCoin)
     (SpecRep DijkstraEra DeltaCoin)
toSpecRep (DeltaCoin Integer
x) = Integer -> SpecTransM DijkstraEra () Integer
forall a. a -> SpecTransM DijkstraEra () a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Integer
x

instance SpecTranslate DijkstraEra PulsingRewUpdate where
  type SpecRep DijkstraEra PulsingRewUpdate = Agda.RewardUpdate

  toSpecRep :: PulsingRewUpdate
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra PulsingRewUpdate)
     (SpecRep DijkstraEra PulsingRewUpdate)
toSpecRep PulsingRewUpdate
x =
    Integer
-> Integer -> Integer -> HSMap Credential Integer -> RewardUpdate
Agda.MkRewardUpdate
      (Integer
 -> Integer -> Integer -> HSMap Credential Integer -> RewardUpdate)
-> SpecTransM DijkstraEra () Integer
-> SpecTransM
     DijkstraEra
     ()
     (Integer -> Integer -> HSMap Credential Integer -> RewardUpdate)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DeltaCoin
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra DeltaCoin)
     (SpecRep DijkstraEra DeltaCoin)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep DeltaCoin
deltaT
      SpecTransM
  DijkstraEra
  ()
  (Integer -> Integer -> HSMap Credential Integer -> RewardUpdate)
-> SpecTransM DijkstraEra () Integer
-> SpecTransM
     DijkstraEra
     ()
     (Integer -> HSMap Credential Integer -> RewardUpdate)
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
<*> DeltaCoin
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra DeltaCoin)
     (SpecRep DijkstraEra DeltaCoin)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep DeltaCoin
deltaR
      SpecTransM
  DijkstraEra
  ()
  (Integer -> HSMap Credential Integer -> RewardUpdate)
-> SpecTransM DijkstraEra () Integer
-> SpecTransM
     DijkstraEra () (HSMap Credential Integer -> RewardUpdate)
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
<*> DeltaCoin
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra DeltaCoin)
     (SpecRep DijkstraEra DeltaCoin)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep DeltaCoin
deltaF
      SpecTransM
  DijkstraEra () (HSMap Credential Integer -> RewardUpdate)
-> SpecTransM DijkstraEra () (HSMap Credential Integer)
-> SpecTransM DijkstraEra () RewardUpdate
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 Map (Credential Staking) Coin
rwds
    where
      (RewardUpdate {RewardEvent
DeltaCoin
NonMyopic
deltaT :: DeltaCoin
deltaR :: DeltaCoin
deltaF :: DeltaCoin
rs :: RewardEvent
nonMyopic :: NonMyopic
nonMyopic :: RewardUpdate -> NonMyopic
deltaF :: RewardUpdate -> DeltaCoin
rs :: RewardUpdate -> RewardEvent
deltaR :: RewardUpdate -> DeltaCoin
deltaT :: RewardUpdate -> DeltaCoin
..}, RewardEvent
_) = ShelleyBase (RewardUpdate, RewardEvent)
-> (RewardUpdate, RewardEvent)
forall a. ShelleyBase a -> a
runShelleyBase (ShelleyBase (RewardUpdate, RewardEvent)
 -> (RewardUpdate, RewardEvent))
-> ShelleyBase (RewardUpdate, RewardEvent)
-> (RewardUpdate, RewardEvent)
forall a b. (a -> b) -> a -> b
$ PulsingRewUpdate -> ShelleyBase (RewardUpdate, RewardEvent)
completeRupd PulsingRewUpdate
x
      rwds :: Map (Credential Staking) Coin
rwds = (Reward -> Coin) -> Set Reward -> Coin
forall m a. Monoid m => (a -> m) -> Set a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Reward -> Coin
rewardAmount (Set Reward -> Coin)
-> RewardEvent -> Map (Credential Staking) Coin
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RewardEvent
rs

instance SpecTranslate DijkstraEra Weight where
  type SpecRep DijkstraEra Weight = Agda.Rational

  toSpecRep :: Rational
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra Rational)
     (SpecRep DijkstraEra Rational)
toSpecRep = Rational -> SpecTransM DijkstraEra () Rational
Rational
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra Rational)
     (SpecRep DijkstraEra Rational)
forall a. a -> SpecTransM DijkstraEra () a
forall (f :: * -> *) a. Applicative f => a -> f a
pure

instance SpecTranslate DijkstraEra LeiosVerificationKey where
  type SpecRep DijkstraEra LeiosVerificationKey = Integer

  toSpecRep :: LeiosVerificationKey
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra LeiosVerificationKey)
     (SpecRep DijkstraEra LeiosVerificationKey)
toSpecRep = Integer -> SpecTransM DijkstraEra () Integer
forall a. a -> SpecTransM DijkstraEra () a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> SpecTransM DijkstraEra () Integer)
-> (LeiosVerificationKey -> Integer)
-> LeiosVerificationKey
-> SpecTransM DijkstraEra () Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LeiosVerificationKey -> Integer
forall v. DSIGNAlgorithm v => VerKeyDSIGN v -> Integer
verkeyToInteger

instance SpecTranslate DijkstraEra LeiosSeat where
  type SpecRep DijkstraEra LeiosSeat = Agda.LeiosSeat

  toSpecRep :: LeiosSeat
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra LeiosSeat)
     (SpecRep DijkstraEra LeiosSeat)
toSpecRep (LeiosSeat {Rational
StrictMaybe LeiosVerificationKey
seatWeight :: Rational
seatVKey :: StrictMaybe LeiosVerificationKey
seatVKey :: LeiosSeat -> StrictMaybe LeiosVerificationKey
seatWeight :: LeiosSeat -> Rational
..}) = Integer -> Rational -> Maybe Integer -> LeiosSeat
Agda.MkLeiosSeat Integer
0 (Rational -> Maybe Integer -> LeiosSeat)
-> SpecTransM DijkstraEra () Rational
-> SpecTransM DijkstraEra () (Maybe Integer -> LeiosSeat)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Rational
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra Rational)
     (SpecRep DijkstraEra Rational)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep Rational
seatWeight SpecTransM DijkstraEra () (Maybe Integer -> LeiosSeat)
-> SpecTransM DijkstraEra () (Maybe Integer)
-> SpecTransM DijkstraEra () LeiosSeat
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
<*> StrictMaybe LeiosVerificationKey
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (StrictMaybe LeiosVerificationKey))
     (SpecRep DijkstraEra (StrictMaybe LeiosVerificationKey))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep StrictMaybe LeiosVerificationKey
seatVKey

instance SpecTranslate DijkstraEra LeiosCommittee where
  type SpecRep DijkstraEra LeiosCommittee = [Agda.LeiosSeat]

  toSpecRep :: LeiosCommittee
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra LeiosCommittee)
     (SpecRep DijkstraEra LeiosCommittee)
toSpecRep = (LeiosSeat -> SpecTransM DijkstraEra () LeiosSeat)
-> [LeiosSeat] -> SpecTransM DijkstraEra () [LeiosSeat]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM LeiosSeat -> SpecTransM DijkstraEra () LeiosSeat
LeiosSeat
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra LeiosSeat)
     (SpecRep DijkstraEra LeiosSeat)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep ([LeiosSeat] -> SpecTransM DijkstraEra () [LeiosSeat])
-> (LeiosCommittee -> [LeiosSeat])
-> LeiosCommittee
-> SpecTransM DijkstraEra () [LeiosSeat]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vector LeiosSeat -> [LeiosSeat]
forall a. Vector a -> [a]
V.toList (Vector LeiosSeat -> [LeiosSeat])
-> (LeiosCommittee -> Vector LeiosSeat)
-> LeiosCommittee
-> [LeiosSeat]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LeiosCommittee -> Vector LeiosSeat
leiosCommitteeSeats

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

  type SpecContext DijkstraEra (NewEpochState DijkstraEra) = Network
  toSpecRep :: NewEpochState DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (NewEpochState DijkstraEra))
     (SpecRep DijkstraEra (NewEpochState DijkstraEra))
toSpecRep nes :: NewEpochState DijkstraEra
nes@(NewEpochState {StrictMaybe PulsingRewUpdate
EpochNo
BlocksMade
StashedAVVMAddresses DijkstraEra
EpochState DijkstraEra
nesEL :: EpochNo
nesBprev :: BlocksMade
nesBcur :: BlocksMade
nesEs :: EpochState DijkstraEra
nesRu :: StrictMaybe PulsingRewUpdate
stashedAVVMAddresses :: StashedAVVMAddresses DijkstraEra
stashedAVVMAddresses :: forall era. NewEpochState era -> StashedAVVMAddresses era
nesRu :: forall era. NewEpochState era -> StrictMaybe PulsingRewUpdate
nesEs :: forall era. NewEpochState era -> EpochState era
nesBcur :: forall era. NewEpochState era -> BlocksMade
nesBprev :: forall era. NewEpochState era -> BlocksMade
nesEL :: forall era. NewEpochState era -> EpochNo
..}) = do
    netId <- SpecTransM DijkstraEra Network Network
forall era ctx. SpecTransM era ctx ctx
askSpecTransM
    withCtxSpecTransM () $
      Agda.MkNewEpochState
        <$> toSpecRep nesEL
        <*> toSpecRep nesBprev
        <*> toSpecRep nesBcur
        <*> withCtxSpecTransM netId (toSpecRep nesEs)
        <*> toSpecRep nesRu
        <*> (filterZeroEntries <$> toSpecRep (nes ^. nesStakePoolDistrG))
        <*> toSpecRep go
    where
      go :: LeiosCommittee
go = SetSnapShot -> LeiosCommittee
ssLeiosCommittee (SetSnapShot -> LeiosCommittee)
-> (EpochState DijkstraEra -> SetSnapShot)
-> EpochState DijkstraEra
-> LeiosCommittee
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SnapShots DijkstraEra -> SetSnapShot
forall era. SnapShots era -> SetSnapShot
ssStakeSet (SnapShots DijkstraEra -> SetSnapShot)
-> (EpochState DijkstraEra -> SnapShots DijkstraEra)
-> EpochState DijkstraEra
-> SetSnapShot
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EpochState DijkstraEra -> SnapShots DijkstraEra
forall era. EpochState era -> SnapShots era
esSnapshots (EpochState DijkstraEra -> LeiosCommittee)
-> EpochState DijkstraEra -> LeiosCommittee
forall a b. (a -> b) -> a -> b
$ EpochState DijkstraEra
nesEs
      -- The specification does not include zero entries in general
      -- while the implementation might. So we filter them out here for the sake
      -- of comparing results.
      --
      -- The discrepancy is discussed here:
      -- https://github.com/IntersectMBO/cardano-ledger/issues/5306
      filterZeroEntries :: HSMap k b -> HSMap k b
filterZeroEntries (Agda.MkHSMap [(k, b)]
lst) =
        [(k, b)] -> HSMap k b
forall k v. [(k, v)] -> HSMap k v
Agda.MkHSMap ([(k, b)] -> HSMap k b) -> [(k, b)] -> HSMap k b
forall a b. (a -> b) -> a -> b
$ ((k, b) -> Bool) -> [(k, b)] -> [(k, b)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((b -> b -> Bool
forall a. Eq a => a -> a -> Bool
/= b
0) (b -> Bool) -> ((k, b) -> b) -> (k, b) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (k, b) -> b
forall a b. (a, b) -> b
snd) [(k, b)]
lst