{-# 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.CertState (CertState)
import Cardano.Ledger.Conway.Core
import Cardano.Ledger.Conway.Governance
import Cardano.Ledger.Conway.Rules
import Data.Functor.Identity (Identity)
import qualified Lib 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
  ) =>
  SpecTranslate ctx (GovEnv era)
  where
  type SpecRep (GovEnv era) = Agda.GovEnv

  toSpecRep :: GovEnv era -> SpecTransM ctx (SpecRep (GovEnv era))
toSpecRep GovEnv {PParams era
StrictMaybe ScriptHash
TxId
CertState era
EpochNo
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
geCertState :: CertState era
gePPolicy :: StrictMaybe ScriptHash
gePParams :: PParams era
geEpoch :: EpochNo
geTxId :: TxId
..} = do
    EnactState era
enactState <- forall b ctx. Inject ctx b => SpecTransM ctx b
askCtx @(EnactState era)
    Integer
-> Integer
-> PParams
-> Maybe Integer
-> EnactState
-> CertState
-> GovEnv
Agda.MkGovEnv
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep TxId
geTxId
      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 EpochNo
geEpoch
      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
gePParams
      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 StrictMaybe ScriptHash
gePPolicy
      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 EnactState era
enactState
      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 CertState era
geCertState

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 :: forall era. GovSignal era -> VotingProcedures era
gsVotingProcedures :: VotingProcedures era
gsVotingProcedures, OSet (ProposalProcedure era)
gsProposalProcedures :: forall era. GovSignal era -> OSet (ProposalProcedure era)
gsProposalProcedures :: OSet (ProposalProcedure era)
gsProposalProcedures} = do
    [GovVote]
votingProcedures <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep VotingProcedures era
gsVotingProcedures
    [GovProposal]
proposalProcedures <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep OSet (ProposalProcedure era)
gsProposalProcedures
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
      forall a. Monoid a => [a] -> a
mconcat
        [ forall a b. a -> Either a b
Left forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [GovVote]
votingProcedures
        , forall a b. b -> Either a b
Right forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [GovProposal]
proposalProcedures
        ]