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

module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.GovCert () where

import Cardano.Ledger.Conway (ConwayEra)
import Control.State.Transition.Extended (TRC (..))
import qualified MAlonzo.Code.Ledger.Conway.Foreign.API as Agda
import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Cert (ConwayCertExecContext (..))
import Test.Cardano.Ledger.Conformance.ExecSpecRule.Core (
  ExecSpecRule (..),
  SpecTRC (..),
 )
import Test.Cardano.Ledger.Conformance.SpecTranslate.Base (
  SpecTranslate (..),
  askSpecTransM,
  unComputationResult,
  withCtxSpecTransM,
 )

instance ExecSpecRule "GOVCERT" ConwayEra where
  type ExecContext "GOVCERT" ConwayEra = ConwayCertExecContext ConwayEra

  translateInputs :: HasCallStack =>
TRC (EraRule "GOVCERT" ConwayEra)
-> SpecTransM
     ConwayEra
     (ExecContext "GOVCERT" ConwayEra)
     (SpecTRC "GOVCERT" ConwayEra)
translateInputs (TRC (Environment (EraRule "GOVCERT" ConwayEra)
env, State (EraRule "GOVCERT" ConwayEra)
st, Signal (EraRule "GOVCERT" ConwayEra)
sig)) = do
    ConwayCertExecContext {..} <- SpecTransM
  ConwayEra
  (ConwayCertExecContext ConwayEra)
  (ConwayCertExecContext ConwayEra)
forall era ctx. SpecTransM era ctx ctx
askSpecTransM
    agdaEnv <- withCtxSpecTransM (ccecVotes, ccecWithdrawals) $ toSpecRep env
    agdaSt <- withCtxSpecTransM () $ toSpecRep st
    agdaSig <- withCtxSpecTransM () $ toSpecRep sig
    pure $ SpecTRC agdaEnv agdaSt agdaSig

  runAgdaRule :: HasCallStack =>
SpecTRC "GOVCERT" ConwayEra
-> Either Text (SpecState "GOVCERT" ConwayEra)
runAgdaRule (SpecTRC SpecEnvironment "GOVCERT" ConwayEra
env SpecState "GOVCERT" ConwayEra
st SpecSignal "GOVCERT" ConwayEra
sig) =
    ComputationResult Text CertState -> Either Text CertState
forall a. ComputationResult Text a -> Either Text a
unComputationResult (ComputationResult Text CertState -> Either Text CertState)
-> ComputationResult Text CertState -> Either Text CertState
forall a b. (a -> b) -> a -> b
$
      CertEnv -> CertState -> DCert -> ComputationResult Text CertState
Agda.govCertStep CertEnv
SpecEnvironment "GOVCERT" ConwayEra
env CertState
SpecState "GOVCERT" ConwayEra
st DCert
SpecSignal "GOVCERT" ConwayEra
sig