{-# 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.Strict (Map)
import qualified Lib 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 = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> OpaqueErrorString
OpaqueErrorString forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. ToExpr a => a -> Expr
toExpr

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