{-# 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 (EraCertState (..), dsUnifiedL)
import Cardano.Ledger.UMap (umElemsL)
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.Conway.Base ()
import Test.Cardano.Ledger.Conformance.SpecTranslate.Core

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
PParams era
CertState era
TxId
EpochNo
geTxId :: TxId
geEpoch :: EpochNo
gePParams :: PParams era
gePPolicy :: StrictMaybe ScriptHash
geCertState :: CertState era
geTxId :: forall era. GovEnv era -> TxId
geEpoch :: forall era. GovEnv era -> EpochNo
gePParams :: forall era. GovEnv era -> PParams era
gePPolicy :: forall era. GovEnv era -> StrictMaybe ScriptHash
geCertState :: forall era. GovEnv era -> CertState era
..} = do
    EnactState era
enactState <- forall b ctx. Inject ctx b => SpecTransM ctx b
askCtx @(EnactState era)
    let rewardAccounts :: Set (Credential 'Staking)
rewardAccounts = Map (Credential 'Staking) UMElem -> Set (Credential 'Staking)
forall k a. Map k a -> Set k
Map.keysSet (Map (Credential 'Staking) UMElem -> Set (Credential 'Staking))
-> Map (Credential 'Staking) UMElem -> Set (Credential 'Staking)
forall a b. (a -> b) -> a -> b
$ CertState era
geCertState CertState era
-> Getting
     (Map (Credential 'Staking) UMElem)
     (CertState era)
     (Map (Credential 'Staking) UMElem)
-> Map (Credential 'Staking) UMElem
forall s a. s -> Getting a s a -> a
^. (DState era
 -> Const (Map (Credential 'Staking) UMElem) (DState era))
-> CertState era
-> Const (Map (Credential 'Staking) UMElem) (CertState era)
forall era. EraCertState era => Lens' (CertState era) (DState era)
Lens' (CertState era) (DState era)
certDStateL ((DState era
  -> Const (Map (Credential 'Staking) UMElem) (DState era))
 -> CertState era
 -> Const (Map (Credential 'Staking) UMElem) (CertState era))
-> ((Map (Credential 'Staking) UMElem
     -> Const
          (Map (Credential 'Staking) UMElem)
          (Map (Credential 'Staking) UMElem))
    -> DState era
    -> Const (Map (Credential 'Staking) UMElem) (DState era))
-> Getting
     (Map (Credential 'Staking) UMElem)
     (CertState era)
     (Map (Credential 'Staking) UMElem)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (UMap -> Const (Map (Credential 'Staking) UMElem) UMap)
-> DState era
-> Const (Map (Credential 'Staking) UMElem) (DState era)
forall era (f :: * -> *).
Functor f =>
(UMap -> f UMap) -> DState era -> f (DState era)
dsUnifiedL ((UMap -> Const (Map (Credential 'Staking) UMElem) UMap)
 -> DState era
 -> Const (Map (Credential 'Staking) UMElem) (DState era))
-> ((Map (Credential 'Staking) UMElem
     -> Const
          (Map (Credential 'Staking) UMElem)
          (Map (Credential 'Staking) UMElem))
    -> UMap -> Const (Map (Credential 'Staking) UMElem) UMap)
-> (Map (Credential 'Staking) UMElem
    -> Const
         (Map (Credential 'Staking) UMElem)
         (Map (Credential 'Staking) UMElem))
-> DState era
-> Const (Map (Credential 'Staking) UMElem) (DState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map (Credential 'Staking) UMElem
 -> Const
      (Map (Credential 'Staking) UMElem)
      (Map (Credential 'Staking) UMElem))
-> UMap -> Const (Map (Credential 'Staking) UMElem) UMap
Lens' UMap (Map (Credential 'Staking) UMElem)
umElemsL
    Integer
-> Integer
-> PParams
-> Maybe Integer
-> EnactState
-> CertState
-> HSSet Credential
-> GovEnv
Agda.MkGovEnv
      (Integer
 -> Integer
 -> PParams
 -> Maybe Integer
 -> EnactState
 -> CertState
 -> HSSet Credential
 -> GovEnv)
-> SpecTransM ctx Integer
-> SpecTransM
     ctx
     (Integer
      -> PParams
      -> Maybe Integer
      -> EnactState
      -> CertState
      -> HSSet Credential
      -> GovEnv)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TxId -> SpecTransM ctx (SpecRep TxId)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep TxId
geTxId
      SpecTransM
  ctx
  (Integer
   -> PParams
   -> Maybe Integer
   -> EnactState
   -> CertState
   -> HSSet Credential
   -> GovEnv)
-> SpecTransM ctx Integer
-> SpecTransM
     ctx
     (PParams
      -> Maybe Integer
      -> EnactState
      -> CertState
      -> HSSet Credential
      -> GovEnv)
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
<*> EpochNo -> SpecTransM ctx (SpecRep EpochNo)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep EpochNo
geEpoch
      SpecTransM
  ctx
  (PParams
   -> Maybe Integer
   -> EnactState
   -> CertState
   -> HSSet Credential
   -> GovEnv)
-> SpecTransM ctx PParams
-> SpecTransM
     ctx
     (Maybe Integer
      -> EnactState -> CertState -> HSSet Credential -> GovEnv)
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
gePParams
      SpecTransM
  ctx
  (Maybe Integer
   -> EnactState -> CertState -> HSSet Credential -> GovEnv)
-> SpecTransM ctx (Maybe Integer)
-> SpecTransM
     ctx (EnactState -> CertState -> HSSet Credential -> GovEnv)
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
<*> StrictMaybe ScriptHash
-> SpecTransM ctx (SpecRep (StrictMaybe ScriptHash))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep StrictMaybe ScriptHash
gePPolicy
      SpecTransM
  ctx (EnactState -> CertState -> HSSet Credential -> GovEnv)
-> SpecTransM ctx EnactState
-> SpecTransM ctx (CertState -> HSSet Credential -> GovEnv)
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
<*> EnactState era -> SpecTransM ctx (SpecRep (EnactState era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep EnactState era
enactState
      SpecTransM ctx (CertState -> HSSet Credential -> GovEnv)
-> SpecTransM ctx CertState
-> SpecTransM ctx (HSSet Credential -> GovEnv)
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
<*> CertState era -> SpecTransM ctx (SpecRep (CertState era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep CertState era
geCertState
      SpecTransM ctx (HSSet Credential -> GovEnv)
-> SpecTransM ctx (HSSet Credential) -> SpecTransM ctx GovEnv
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 'Staking)
-> SpecTransM ctx (SpecRep (Set (Credential 'Staking)))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Set (Credential 'Staking)
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
    [GovVote]
votingProcedures <- VotingProcedures era
-> SpecTransM ctx (SpecRep (VotingProcedures era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep VotingProcedures era
gsVotingProcedures
    [GovProposal]
proposalProcedures <- OSet (ProposalProcedure era)
-> SpecTransM ctx (SpecRep (OSet (ProposalProcedure era)))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep OSet (ProposalProcedure era)
gsProposalProcedures
    [Either GovVote GovProposal]
-> SpecTransM ctx [Either GovVote GovProposal]
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Either GovVote GovProposal]
 -> SpecTransM ctx [Either GovVote GovProposal])
-> [Either GovVote GovProposal]
-> SpecTransM ctx [Either GovVote GovProposal]
forall a b. (a -> b) -> a -> b
$
      [[Either GovVote GovProposal]] -> [Either GovVote GovProposal]
forall a. Monoid a => [a] -> a
mconcat
        [ GovVote -> Either GovVote GovProposal
forall a b. a -> Either a b
Left (GovVote -> Either GovVote GovProposal)
-> [GovVote] -> [Either GovVote GovProposal]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [GovVote]
votingProcedures
        , GovProposal -> Either GovVote GovProposal
forall a b. b -> Either a b
Right (GovProposal -> Either GovVote GovProposal)
-> [GovProposal] -> [Either GovVote GovProposal]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [GovProposal]
proposalProcedures
        ]