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

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

import Cardano.Ledger.Conway (ConwayEra)
import Data.Bifunctor (Bifunctor (..))
import qualified MAlonzo.Code.Ledger.Foreign.API as Agda
import Test.Cardano.Ledger.Conformance (ExecSpecRule (..), SpecTRC (..), unComputationResult)
import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Cert (ConwayCertExecContext)

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

  runAgdaRule :: HasCallStack =>
SpecTRC "GOVCERT" ConwayEra
-> Either Text (SpecState "GOVCERT" ConwayEra)
runAgdaRule (SpecTRC SpecEnvironment "GOVCERT" ConwayEra
env (Agda.MkCertState DState
dState PState
pState GState
vState) SpecSignal "GOVCERT" ConwayEra
sig) =
    (GState -> CertState)
-> Either Text GState -> Either Text CertState
forall b c a. (b -> c) -> Either a b -> Either a c
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (DState -> PState -> GState -> CertState
Agda.MkCertState DState
dState PState
pState) (Either Text GState -> Either Text (SpecState "GOVCERT" ConwayEra))
-> (T_ComputationResult_44 Text GState -> Either Text GState)
-> T_ComputationResult_44 Text GState
-> Either Text (SpecState "GOVCERT" ConwayEra)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. T_ComputationResult_44 Text GState -> Either Text GState
forall a. ComputationResult Text a -> Either Text a
unComputationResult (T_ComputationResult_44 Text GState
 -> Either Text (SpecState "GOVCERT" ConwayEra))
-> T_ComputationResult_44 Text GState
-> Either Text (SpecState "GOVCERT" ConwayEra)
forall a b. (a -> b) -> a -> b
$
      CertEnv -> GState -> DCert -> T_ComputationResult_44 Text GState
Agda.govCertStep CertEnv
SpecEnvironment "GOVCERT" ConwayEra
env GState
vState DCert
SpecSignal "GOVCERT" ConwayEra
sig