{-# 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 ()
import Test.Cardano.Ledger.Conway.TreeDiff

instance ToExpr (PredicateFailure (EraRule "CERT" era)) => SpecTranslate ctx (ConwayCertsPredFailure era) where
  type SpecRep (ConwayCertsPredFailure era) = OpaqueErrorString
  toSpecRep :: ConwayCertsPredFailure era
-> SpecTransM ctx (SpecRep (ConwayCertsPredFailure era))
toSpecRep = OpaqueErrorString -> SpecTransM ctx OpaqueErrorString
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (OpaqueErrorString -> SpecTransM ctx OpaqueErrorString)
-> (ConwayCertsPredFailure era -> OpaqueErrorString)
-> ConwayCertsPredFailure era
-> SpecTransM ctx OpaqueErrorString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConwayCertsPredFailure era -> OpaqueErrorString
forall a. ToExpr a => a -> OpaqueErrorString
showOpaqueErrorString

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 era) (GovActionState era)
StrictMaybe (Committee era)
Tx era
PParams era
EpochNo
certsTx :: Tx era
certsPParams :: PParams era
certsCurrentEpoch :: EpochNo
certsCurrentCommittee :: StrictMaybe (Committee era)
certsCommitteeProposals :: Map (GovPurposeId 'CommitteePurpose era) (GovActionState era)
certsTx :: forall era. CertsEnv era -> Tx era
certsPParams :: forall era. CertsEnv era -> PParams era
certsCurrentEpoch :: forall era. CertsEnv era -> EpochNo
certsCurrentCommittee :: forall era. CertsEnv era -> StrictMaybe (Committee era)
certsCommitteeProposals :: forall era.
CertsEnv era
-> Map (GovPurposeId 'CommitteePurpose era) (GovActionState era)
..} = do
    VotingProcedures era
votes <- forall b ctx. Inject ctx b => SpecTransM ctx b
askCtx @(VotingProcedures era)
    Map RewardAccount Coin
withdrawals <- forall b ctx. Inject ctx b => SpecTransM ctx b
askCtx @(Map RewardAccount Coin)
    let ccColdCreds :: Set (Credential 'ColdCommitteeRole)
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
    Integer
-> PParams
-> [GovVote]
-> HSMap RwdAddr Integer
-> HSSet Credential
-> CertEnv
Agda.MkCertEnv
      (Integer
 -> PParams
 -> [GovVote]
 -> HSMap RwdAddr Integer
 -> HSSet Credential
 -> CertEnv)
-> SpecTransM ctx Integer
-> SpecTransM
     ctx
     (PParams
      -> [GovVote]
      -> HSMap RwdAddr Integer
      -> HSSet Credential
      -> CertEnv)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> EpochNo -> SpecTransM ctx (SpecRep EpochNo)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep EpochNo
certsCurrentEpoch
      SpecTransM
  ctx
  (PParams
   -> [GovVote]
   -> HSMap RwdAddr Integer
   -> HSSet Credential
   -> CertEnv)
-> SpecTransM ctx PParams
-> SpecTransM
     ctx
     ([GovVote] -> HSMap RwdAddr Integer -> HSSet Credential -> CertEnv)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> PParams era -> SpecTransM ctx (SpecRep (PParams era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep PParams era
certsPParams
      SpecTransM
  ctx
  ([GovVote] -> HSMap RwdAddr Integer -> HSSet Credential -> CertEnv)
-> SpecTransM ctx [GovVote]
-> SpecTransM
     ctx (HSMap RwdAddr Integer -> HSSet Credential -> CertEnv)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> VotingProcedures era
-> SpecTransM ctx (SpecRep (VotingProcedures era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep VotingProcedures era
votes
      SpecTransM
  ctx (HSMap RwdAddr Integer -> HSSet Credential -> CertEnv)
-> SpecTransM ctx (HSMap RwdAddr Integer)
-> SpecTransM ctx (HSSet Credential -> CertEnv)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Map RewardAccount Coin
-> SpecTransM ctx (SpecRep (Map RewardAccount Coin))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Map RewardAccount Coin
withdrawals
      SpecTransM ctx (HSSet Credential -> CertEnv)
-> SpecTransM ctx (HSSet Credential) -> SpecTransM ctx CertEnv
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Set (Credential 'ColdCommitteeRole)
-> SpecTransM ctx (SpecRep (Set (Credential 'ColdCommitteeRole)))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Set (Credential 'ColdCommitteeRole)
ccColdCreds