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

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

import Cardano.Ledger.Conway (ConwayEra)
import qualified Cardano.Ledger.Conway.Rules as Conway
import Cardano.Ledger.State
import qualified Data.Map.Strict as Map
import Lens.Micro ((^.))
import qualified MAlonzo.Code.Ledger.Conway.Foreign.API as Agda
import Test.Cardano.Ledger.Conformance.SpecTranslate.Base
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base ()
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Cert ()

instance SpecTranslate ConwayEra (Conway.GovEnv ConwayEra) where
  type SpecRep ConwayEra (Conway.GovEnv ConwayEra) = Agda.GovEnv
  type SpecContext ConwayEra (Conway.GovEnv ConwayEra) = Conway.EnactState ConwayEra

  toSpecRep :: GovEnv ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (GovEnv ConwayEra))
     (SpecRep ConwayEra (GovEnv ConwayEra))
toSpecRep Conway.GovEnv {StrictMaybe ScriptHash
StrictMaybe (Committee ConwayEra)
PParams ConwayEra
CertState ConwayEra
TxId
EpochNo
geTxId :: TxId
geEpoch :: EpochNo
gePParams :: PParams ConwayEra
geGuardrailsScriptHash :: StrictMaybe ScriptHash
geCertState :: CertState ConwayEra
geCommittee :: StrictMaybe (Committee ConwayEra)
geCommittee :: forall era. GovEnv era -> StrictMaybe (Committee era)
geCertState :: forall era. GovEnv era -> CertState era
geGuardrailsScriptHash :: 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 <- SpecTransM ConwayEra (EnactState ConwayEra) (EnactState ConwayEra)
forall era ctx. SpecTransM era ctx ctx
askSpecTransM
    let rewardAccounts = Map (Credential Staking) (AccountState ConwayEra)
-> Set (Credential Staking)
forall k a. Map k a -> Set k
Map.keysSet (Map (Credential Staking) (AccountState ConwayEra)
 -> Set (Credential Staking))
-> Map (Credential Staking) (AccountState ConwayEra)
-> Set (Credential Staking)
forall a b. (a -> b) -> a -> b
$ CertState ConwayEra
ConwayCertState ConwayEra
geCertState ConwayCertState ConwayEra
-> Getting
     (Map (Credential Staking) (AccountState ConwayEra))
     (ConwayCertState ConwayEra)
     (Map (Credential Staking) (AccountState ConwayEra))
-> Map (Credential Staking) (AccountState ConwayEra)
forall s a. s -> Getting a s a -> a
^. (DState ConwayEra
 -> Const
      (Map (Credential Staking) (AccountState ConwayEra))
      (DState ConwayEra))
-> CertState ConwayEra
-> Const
     (Map (Credential Staking) (AccountState ConwayEra))
     (CertState ConwayEra)
(DState ConwayEra
 -> Const
      (Map (Credential Staking) (AccountState ConwayEra))
      (DState ConwayEra))
-> ConwayCertState ConwayEra
-> Const
     (Map (Credential Staking) (AccountState ConwayEra))
     (ConwayCertState ConwayEra)
forall era. EraCertState era => Lens' (CertState era) (DState era)
Lens' (CertState ConwayEra) (DState ConwayEra)
certDStateL ((DState ConwayEra
  -> Const
       (Map (Credential Staking) (AccountState ConwayEra))
       (DState ConwayEra))
 -> ConwayCertState ConwayEra
 -> Const
      (Map (Credential Staking) (AccountState ConwayEra))
      (ConwayCertState ConwayEra))
-> ((Map (Credential Staking) (AccountState ConwayEra)
     -> Const
          (Map (Credential Staking) (AccountState ConwayEra))
          (Map (Credential Staking) (AccountState ConwayEra)))
    -> DState ConwayEra
    -> Const
         (Map (Credential Staking) (AccountState ConwayEra))
         (DState ConwayEra))
-> Getting
     (Map (Credential Staking) (AccountState ConwayEra))
     (ConwayCertState ConwayEra)
     (Map (Credential Staking) (AccountState ConwayEra))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Accounts ConwayEra
 -> Const
      (Map (Credential Staking) (AccountState ConwayEra))
      (Accounts ConwayEra))
-> DState ConwayEra
-> Const
     (Map (Credential Staking) (AccountState ConwayEra))
     (DState ConwayEra)
(ConwayAccounts ConwayEra
 -> Const
      (Map (Credential Staking) (AccountState ConwayEra))
      (ConwayAccounts ConwayEra))
-> DState ConwayEra
-> Const
     (Map (Credential Staking) (AccountState ConwayEra))
     (DState ConwayEra)
forall era. Lens' (DState era) (Accounts era)
forall (t :: * -> *) era.
CanSetAccounts t =>
Lens' (t era) (Accounts era)
accountsL ((ConwayAccounts ConwayEra
  -> Const
       (Map (Credential Staking) (AccountState ConwayEra))
       (ConwayAccounts ConwayEra))
 -> DState ConwayEra
 -> Const
      (Map (Credential Staking) (AccountState ConwayEra))
      (DState ConwayEra))
-> ((Map (Credential Staking) (AccountState ConwayEra)
     -> Const
          (Map (Credential Staking) (AccountState ConwayEra))
          (Map (Credential Staking) (AccountState ConwayEra)))
    -> ConwayAccounts ConwayEra
    -> Const
         (Map (Credential Staking) (AccountState ConwayEra))
         (ConwayAccounts ConwayEra))
-> (Map (Credential Staking) (AccountState ConwayEra)
    -> Const
         (Map (Credential Staking) (AccountState ConwayEra))
         (Map (Credential Staking) (AccountState ConwayEra)))
-> DState ConwayEra
-> Const
     (Map (Credential Staking) (AccountState ConwayEra))
     (DState ConwayEra)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map (Credential Staking) (AccountState ConwayEra)
 -> Const
      (Map (Credential Staking) (AccountState ConwayEra))
      (Map (Credential Staking) (AccountState ConwayEra)))
-> Accounts ConwayEra
-> Const
     (Map (Credential Staking) (AccountState ConwayEra))
     (Accounts ConwayEra)
(Map (Credential Staking) (AccountState ConwayEra)
 -> Const
      (Map (Credential Staking) (AccountState ConwayEra))
      (Map (Credential Staking) (AccountState ConwayEra)))
-> ConwayAccounts ConwayEra
-> Const
     (Map (Credential Staking) (AccountState ConwayEra))
     (ConwayAccounts ConwayEra)
forall era.
EraAccounts era =>
Lens' (Accounts era) (Map (Credential Staking) (AccountState era))
Lens'
  (Accounts ConwayEra)
  (Map (Credential Staking) (AccountState ConwayEra))
accountsMapL
    withCtxSpecTransM () $
      Agda.MkGovEnv
        <$> toSpecRep geTxId
        <*> toSpecRep geEpoch
        <*> toSpecRep gePParams
        <*> toSpecRep geGuardrailsScriptHash
        <*> toSpecRep enactState
        <*> toSpecRep geCertState
        <*> toSpecRep rewardAccounts

instance SpecTranslate ConwayEra (Conway.GovSignal ConwayEra) where
  type SpecRep ConwayEra (Conway.GovSignal ConwayEra) = [Either Agda.GovVote Agda.GovProposal]

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