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

module Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Certs () where

import Cardano.Ledger.Coin
import Cardano.Ledger.Conway (ConwayEra)
import Cardano.Ledger.Conway.Core
import Cardano.Ledger.Conway.Governance
import qualified Cardano.Ledger.Conway.Rules as Conway
import Data.Map (keysSet)
import Data.Map.Strict (Map)
import qualified MAlonzo.Code.Ledger.Conway.Foreign.API as Agda
import Test.Cardano.Ledger.Conformance.SpecTranslate.Base (
  SpecTranslate (..),
  askSpecTransM,
  toSpecRepMap,
  withCtxSpecTransM,
 )
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Deleg ()
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Pool ()

instance SpecTranslate ConwayEra (Conway.CertsEnv ConwayEra) where
  type SpecRep ConwayEra (Conway.CertsEnv ConwayEra) = Agda.CertEnv
  type
    SpecContext ConwayEra (Conway.CertsEnv ConwayEra) =
      (VotingProcedures ConwayEra, Map AccountAddress Coin)
  toSpecRep :: CertsEnv ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (CertsEnv ConwayEra))
     (SpecRep ConwayEra (CertsEnv ConwayEra))
toSpecRep Conway.CertsEnv {Map (GovPurposeId 'CommitteePurpose) (GovActionState ConwayEra)
StrictMaybe (Committee ConwayEra)
Tx TopTx ConwayEra
PParams ConwayEra
EpochNo
certsTx :: Tx TopTx ConwayEra
certsPParams :: PParams ConwayEra
certsCurrentEpoch :: EpochNo
certsCurrentCommittee :: StrictMaybe (Committee ConwayEra)
certsCommitteeProposals :: Map (GovPurposeId 'CommitteePurpose) (GovActionState ConwayEra)
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, withdrawals) <- SpecTransM
  ConwayEra
  (VotingProcedures ConwayEra, Map AccountAddress Coin)
  (VotingProcedures ConwayEra, Map AccountAddress Coin)
forall era ctx. SpecTransM era ctx ctx
askSpecTransM
    let ccColdCreds = (Committee ConwayEra -> Set (Credential ColdCommitteeRole))
-> StrictMaybe (Committee ConwayEra)
-> 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 ConwayEra
    -> Map (Credential ColdCommitteeRole) EpochNo)
-> Committee ConwayEra
-> Set (Credential ColdCommitteeRole)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Committee ConwayEra -> Map (Credential ColdCommitteeRole) EpochNo
forall era.
Committee era -> Map (Credential ColdCommitteeRole) EpochNo
committeeMembers) StrictMaybe (Committee ConwayEra)
certsCurrentCommittee
    withCtxSpecTransM () $
      Agda.MkCertEnv
        <$> toSpecRep certsCurrentEpoch
        <*> toSpecRep certsPParams
        <*> toSpecRep votes
        <*> toSpecRepMap withdrawals
        <*> toSpecRep ccColdCreds