{-# 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 qualified Cardano.Ledger.Conway.Rules as Conway
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 (PParamsHKD Identity era)
  , SpecContext (PParamsHKD Identity era) ~ ()
  , EraPParams era
  , SpecRep (PParamsHKD Identity era) ~ Agda.PParams
  , SpecTranslate (CertState era)
  , SpecContext (CertState era) ~ ()
  , SpecRep (CertState era) ~ Agda.CertState
  , EraCertState era
  ) =>
  SpecTranslate (Conway.GovEnv era)
  where
  type SpecRep (Conway.GovEnv era) = Agda.GovEnv
  type SpecContext (Conway.GovEnv era) = EnactState era

  toSpecRep :: GovEnv era
-> SpecTransM (SpecContext (GovEnv era)) (SpecRep (GovEnv era))
toSpecRep Conway.GovEnv {StrictMaybe ScriptHash
StrictMaybe (Committee era)
PParams era
CertState era
TxId
EpochNo
geTxId :: TxId
geEpoch :: EpochNo
gePParams :: PParams era
geGuardrailsScriptHash :: StrictMaybe ScriptHash
geCertState :: CertState era
geCommittee :: StrictMaybe (Committee era)
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 (EnactState era) (EnactState era)
forall ctx. SpecTransM ctx ctx
askSpecTransM
    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
    withCtxSpecTransM () $
      Agda.MkGovEnv
        <$> toSpecRep geTxId
        <*> toSpecRep geEpoch
        <*> toSpecRep gePParams
        <*> toSpecRep geGuardrailsScriptHash
        <*> toSpecRep enactState
        <*> toSpecRep geCertState
        <*> toSpecRep rewardAccounts

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

  toSpecRep :: GovSignal era
-> SpecTransM
     (SpecContext (GovSignal era)) (SpecRep (GovSignal era))
toSpecRep Conway.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
     (SpecContext (VotingProcedures era))
     (SpecRep (VotingProcedures era))
forall a.
SpecTranslate a =>
a -> SpecTransM (SpecContext a) (SpecRep a)
toSpecRep VotingProcedures era
gsVotingProcedures
    proposalProcedures <- toSpecRep gsProposalProcedures
    pure $
      mconcat
        [ Left <$> votingProcedures
        , Right <$> proposalProcedures
        ]