{-# 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.Certs () where

import Cardano.Ledger.Address (RewardAccount)
import Cardano.Ledger.BaseTypes
import Cardano.Ledger.Coin
import Cardano.Ledger.Conway.Core
import Cardano.Ledger.Conway.Governance
import Cardano.Ledger.Conway.Rules
import Data.Functor.Identity (Identity)
import Data.Map (keysSet)
import Data.Map.Strict (Map)
import qualified MAlonzo.Code.Ledger.Foreign.API as Agda
import Test.Cardano.Ledger.Conformance
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Deleg ()
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Pool ()

instance
  ( SpecTranslate ctx (PParamsHKD Identity era)
  , SpecRep (PParamsHKD Identity era) ~ Agda.PParams
  , Inject ctx (VotingProcedures era)
  , Inject ctx (Map RewardAccount Coin)
  ) =>
  SpecTranslate ctx (CertsEnv era)
  where
  type SpecRep (CertsEnv era) = Agda.CertEnv
  toSpecRep :: CertsEnv era -> SpecTransM ctx (SpecRep (CertsEnv era))
toSpecRep CertsEnv {Map (GovPurposeId 'CommitteePurpose) (GovActionState era)
StrictMaybe (Committee era)
Tx TopTx era
PParams era
EpochNo
certsTx :: Tx TopTx era
certsPParams :: PParams era
certsCurrentEpoch :: EpochNo
certsCurrentCommittee :: StrictMaybe (Committee era)
certsCommitteeProposals :: Map (GovPurposeId 'CommitteePurpose) (GovActionState era)
certsCommitteeProposals :: forall era.
CertsEnv era
-> Map (GovPurposeId 'CommitteePurpose) (GovActionState era)
certsCurrentCommittee :: forall era. CertsEnv era -> StrictMaybe (Committee era)
certsCurrentEpoch :: forall era. CertsEnv era -> EpochNo
certsPParams :: forall era. CertsEnv era -> PParams era
certsTx :: forall era. CertsEnv era -> Tx TopTx era
..} = do
    votes <- forall b ctx. Inject ctx b => SpecTransM ctx b
askCtx @(VotingProcedures era)
    withdrawals <- askCtx @(Map RewardAccount Coin)
    let ccColdCreds = (Committee era -> Set (Credential ColdCommitteeRole))
-> StrictMaybe (Committee era)
-> Set (Credential ColdCommitteeRole)
forall m a. Monoid m => (a -> m) -> StrictMaybe a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (Map (Credential ColdCommitteeRole) EpochNo
-> Set (Credential ColdCommitteeRole)
forall k a. Map k a -> Set k
keysSet (Map (Credential ColdCommitteeRole) EpochNo
 -> Set (Credential ColdCommitteeRole))
-> (Committee era -> Map (Credential ColdCommitteeRole) EpochNo)
-> Committee era
-> Set (Credential ColdCommitteeRole)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Committee era -> Map (Credential ColdCommitteeRole) EpochNo
forall era.
Committee era -> Map (Credential ColdCommitteeRole) EpochNo
committeeMembers) StrictMaybe (Committee era)
certsCurrentCommittee
    Agda.MkCertEnv
      <$> toSpecRep certsCurrentEpoch
      <*> toSpecRep certsPParams
      <*> toSpecRep votes
      <*> toSpecRep withdrawals
      <*> toSpecRep ccColdCreds