{-# 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.Coin
import Cardano.Ledger.Conway.Core
import Cardano.Ledger.Conway.Governance
import qualified Cardano.Ledger.Conway.Rules as Conway
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 (PParamsHKD Identity era)
  , SpecRep (PParamsHKD Identity era) ~ Agda.PParams
  , SpecContext (PParamsHKD Identity era) ~ ()
  ) =>
  SpecTranslate (Conway.CertsEnv era)
  where
  type SpecRep (Conway.CertsEnv era) = Agda.CertEnv
  type SpecContext (Conway.CertsEnv era) = (VotingProcedures era, Map AccountAddress Coin)
  toSpecRep :: CertsEnv era
-> SpecTransM (SpecContext (CertsEnv era)) (SpecRep (CertsEnv era))
toSpecRep Conway.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, withdrawals) <- SpecTransM
  (VotingProcedures era, Map AccountAddress Coin)
  (VotingProcedures era, Map AccountAddress Coin)
forall ctx. SpecTransM ctx ctx
askSpecTransM
    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
    withCtxSpecTransM () $
      Agda.MkCertEnv
        <$> toSpecRep certsCurrentEpoch
        <*> toSpecRep certsPParams
        <*> toSpecRep votes
        <*> toSpecRepMap withdrawals
        <*> toSpecRep ccColdCreds