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

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

import Cardano.Ledger.BaseTypes
import Cardano.Ledger.Conway.Core
import Cardano.Ledger.Conway.Governance
import Cardano.Ledger.Conway.Rules
import Cardano.Ledger.State
import Data.Functor.Identity (Identity)
import qualified Data.Map.Strict as Map
import Lens.Micro ((^.))
import qualified MAlonzo.Code.Ledger.Foreign.API as Agda
import Test.Cardano.Ledger.Conformance.SpecTranslate.Base
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base ()

instance
  ( SpecTranslate ctx (PParamsHKD Identity era)
  , Inject ctx (EnactState era)
  , EraPParams era
  , SpecRep (PParamsHKD Identity era) ~ Agda.PParams
  , SpecTranslate ctx (CertState era)
  , SpecRep (CertState era) ~ Agda.CertState
  , EraCertState era
  ) =>
  SpecTranslate ctx (GovEnv era)
  where
  type SpecRep (GovEnv era) = Agda.GovEnv

  toSpecRep :: GovEnv era -> SpecTransM ctx (SpecRep (GovEnv era))
toSpecRep GovEnv {StrictMaybe ScriptHash
StrictMaybe (Committee era)
PParams era
CertState era
TxId
EpochNo
geTxId :: TxId
geEpoch :: EpochNo
gePParams :: PParams era
gePPolicy :: StrictMaybe ScriptHash
geCertState :: CertState era
geCommittee :: StrictMaybe (Committee era)
geCommittee :: forall era. GovEnv era -> StrictMaybe (Committee era)
geCertState :: forall era. GovEnv era -> CertState era
gePPolicy :: forall era. GovEnv era -> StrictMaybe ScriptHash
gePParams :: forall era. GovEnv era -> PParams era
geEpoch :: forall era. GovEnv era -> EpochNo
geTxId :: forall era. GovEnv era -> TxId
..} = do
    enactState <- forall b ctx. Inject ctx b => SpecTransM ctx b
askCtx @(EnactState era)
    let rewardAccounts = Map (Credential Staking) (AccountState era)
-> Set (Credential Staking)
forall k a. Map k a -> Set k
Map.keysSet (Map (Credential Staking) (AccountState era)
 -> Set (Credential Staking))
-> Map (Credential Staking) (AccountState era)
-> Set (Credential Staking)
forall a b. (a -> b) -> a -> b
$ CertState era
geCertState CertState era
-> Getting
     (Map (Credential Staking) (AccountState era))
     (CertState era)
     (Map (Credential Staking) (AccountState era))
-> Map (Credential Staking) (AccountState era)
forall s a. s -> Getting a s a -> a
^. (DState era
 -> Const
      (Map (Credential Staking) (AccountState era)) (DState era))
-> CertState era
-> Const
     (Map (Credential Staking) (AccountState era)) (CertState era)
forall era. EraCertState era => Lens' (CertState era) (DState era)
Lens' (CertState era) (DState era)
certDStateL ((DState era
  -> Const
       (Map (Credential Staking) (AccountState era)) (DState era))
 -> CertState era
 -> Const
      (Map (Credential Staking) (AccountState era)) (CertState era))
-> ((Map (Credential Staking) (AccountState era)
     -> Const
          (Map (Credential Staking) (AccountState era))
          (Map (Credential Staking) (AccountState era)))
    -> DState era
    -> Const
         (Map (Credential Staking) (AccountState era)) (DState era))
-> Getting
     (Map (Credential Staking) (AccountState era))
     (CertState era)
     (Map (Credential Staking) (AccountState era))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Accounts era
 -> Const
      (Map (Credential Staking) (AccountState era)) (Accounts era))
-> DState era
-> Const (Map (Credential Staking) (AccountState era)) (DState era)
forall era. Lens' (DState era) (Accounts era)
forall (t :: * -> *) era.
CanSetAccounts t =>
Lens' (t era) (Accounts era)
accountsL ((Accounts era
  -> Const
       (Map (Credential Staking) (AccountState era)) (Accounts era))
 -> DState era
 -> Const
      (Map (Credential Staking) (AccountState era)) (DState era))
-> ((Map (Credential Staking) (AccountState era)
     -> Const
          (Map (Credential Staking) (AccountState era))
          (Map (Credential Staking) (AccountState era)))
    -> Accounts era
    -> Const
         (Map (Credential Staking) (AccountState era)) (Accounts era))
-> (Map (Credential Staking) (AccountState era)
    -> Const
         (Map (Credential Staking) (AccountState era))
         (Map (Credential Staking) (AccountState era)))
-> DState era
-> Const (Map (Credential Staking) (AccountState era)) (DState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map (Credential Staking) (AccountState era)
 -> Const
      (Map (Credential Staking) (AccountState era))
      (Map (Credential Staking) (AccountState era)))
-> Accounts era
-> Const
     (Map (Credential Staking) (AccountState era)) (Accounts era)
forall era.
EraAccounts era =>
Lens' (Accounts era) (Map (Credential Staking) (AccountState era))
Lens' (Accounts era) (Map (Credential Staking) (AccountState era))
accountsMapL
    Agda.MkGovEnv
      <$> toSpecRep geTxId
      <*> toSpecRep geEpoch
      <*> toSpecRep gePParams
      <*> toSpecRep gePPolicy
      <*> toSpecRep enactState
      <*> toSpecRep geCertState
      <*> toSpecRep rewardAccounts

instance
  ( EraPParams era
  , SpecTranslate ctx (PParamsHKD StrictMaybe era)
  , SpecRep (PParamsHKD StrictMaybe era) ~ Agda.PParamsUpdate
  ) =>
  SpecTranslate ctx (GovSignal era)
  where
  type SpecRep (GovSignal era) = [Either Agda.GovVote Agda.GovProposal]

  toSpecRep :: GovSignal era -> SpecTransM ctx (SpecRep (GovSignal era))
toSpecRep GovSignal {VotingProcedures era
gsVotingProcedures :: VotingProcedures era
gsVotingProcedures :: forall era. GovSignal era -> VotingProcedures era
gsVotingProcedures, OSet (ProposalProcedure era)
gsProposalProcedures :: OSet (ProposalProcedure era)
gsProposalProcedures :: forall era. GovSignal era -> OSet (ProposalProcedure era)
gsProposalProcedures} = do
    votingProcedures <- VotingProcedures era
-> SpecTransM ctx (SpecRep (VotingProcedures era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep VotingProcedures era
gsVotingProcedures
    proposalProcedures <- toSpecRep gsProposalProcedures
    pure $
      mconcat
        [ Left <$> votingProcedures
        , Right <$> proposalProcedures
        ]