{-# 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.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 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.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
NonMyopic
esChainAccountState :: ChainAccountState
esSnapshots :: SnapShots
esNonMyopic :: NonMyopic
esNonMyopic :: forall era. EpochState era -> NonMyopic
esSnapshots :: forall era. EpochState era -> SnapShots
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 where
  type SpecRep DijkstraEra SnapShots = Agda.Snapshots

  toSpecRep :: SnapShots
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra SnapShots)
     (SpecRep DijkstraEra SnapShots)
toSpecRep (SnapShots {PoolDistr
SnapShot
Coin
ssStakeMark :: SnapShot
ssStakeMarkPoolDistr :: PoolDistr
ssStakeSet :: SnapShot
ssStakeGo :: SnapShot
ssFee :: Coin
ssFee :: SnapShots -> Coin
ssStakeGo :: SnapShots -> SnapShot
ssStakeMark :: SnapShots -> SnapShot
ssStakeMarkPoolDistr :: SnapShots -> PoolDistr
ssStakeSet :: SnapShots -> SnapShot
..}) =
    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 SnapShot
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 SnapShot
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 SnapShot
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 StakePoolParams
-> Snapshot
Agda.MkSnapshot
      (HSMap Credential Integer
 -> HSMap Credential Integer
 -> HSMap Integer StakePoolParams
 -> Snapshot)
-> SpecTransM DijkstraEra () (HSMap Credential Integer)
-> SpecTransM
     DijkstraEra
     ()
     (HSMap Credential Integer
      -> HSMap Integer StakePoolParams -> 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 StakePoolParams -> Snapshot)
-> SpecTransM DijkstraEra () (HSMap Credential Integer)
-> SpecTransM
     DijkstraEra () (HSMap Integer StakePoolParams -> 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 StakePoolParams -> Snapshot)
-> SpecTransM DijkstraEra () (HSMap Integer StakePoolParams)
-> 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.StakePoolParams

  toSpecRep :: StakePoolSnapShot
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra StakePoolSnapShot)
     (SpecRep DijkstraEra StakePoolSnapShot)
toSpecRep StakePoolSnapShot {Int
Rational
Set (KeyHash Staking)
AccountId
VRFVerKeyHash StakePoolVRF
Coin
CompactForm Coin
UnitInterval
spssStake :: CompactForm Coin
spssStakeRatio :: Rational
spssSelfDelegatedOwners :: Set (KeyHash Staking)
spssSelfDelegatedOwnersStake :: Coin
spssVrf :: VRFVerKeyHash StakePoolVRF
spssPledge :: Coin
spssCost :: Coin
spssMargin :: UnitInterval
spssNumDelegators :: Int
spssAccountId :: AccountId
spssAccountId :: StakePoolSnapShot -> AccountId
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 -> Credential -> StakePoolParams
Agda.StakePoolParams
      (HSSet Integer
 -> Integer -> Rational -> Integer -> Credential -> StakePoolParams)
-> SpecTransM DijkstraEra () (HSSet Integer)
-> SpecTransM
     DijkstraEra
     ()
     (Integer -> Rational -> Integer -> Credential -> StakePoolParams)
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 -> Credential -> StakePoolParams)
-> SpecTransM DijkstraEra () Integer
-> SpecTransM
     DijkstraEra
     ()
     (Rational -> Integer -> Credential -> StakePoolParams)
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 -> Credential -> StakePoolParams)
-> SpecTransM DijkstraEra () Rational
-> SpecTransM
     DijkstraEra () (Integer -> Credential -> StakePoolParams)
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 -> Credential -> StakePoolParams)
-> SpecTransM DijkstraEra () Integer
-> SpecTransM DijkstraEra () (Credential -> StakePoolParams)
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 () (Credential -> StakePoolParams)
-> SpecTransM DijkstraEra () Credential
-> SpecTransM DijkstraEra () StakePoolParams
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)

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 (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 (NewEpochState {StrictMaybe PulsingRewUpdate
PoolDistr
EpochNo
BlocksMade
StashedAVVMAddresses DijkstraEra
EpochState DijkstraEra
nesEL :: EpochNo
nesBprev :: BlocksMade
nesBcur :: BlocksMade
nesEs :: EpochState DijkstraEra
nesRu :: StrictMaybe PulsingRewUpdate
nesPd :: PoolDistr
stashedAVVMAddresses :: StashedAVVMAddresses DijkstraEra
stashedAVVMAddresses :: forall era. NewEpochState era -> StashedAVVMAddresses era
nesPd :: forall era. NewEpochState era -> PoolDistr
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 nesPd)
    where
      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