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

module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Cert (nameTxCert) where

import Cardano.Ledger.Address (RewardAccount)
import Cardano.Ledger.BaseTypes (Inject)
import Cardano.Ledger.Coin (Coin)
import Cardano.Ledger.Conway
import Cardano.Ledger.Conway.TxCert (ConwayTxCert (..))
import Cardano.Ledger.Crypto (StandardCrypto)
import Data.Bifunctor (first)
import qualified Data.List.NonEmpty as NE
import Data.Map.Strict (Map)
import qualified Data.Text as T
import qualified Lib as Agda
import Test.Cardano.Ledger.Conformance
import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base
import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Deleg (nameDelegCert)
import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.GovCert (nameGovCert)
import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Pool (namePoolCert)
import Test.Cardano.Ledger.Constrained.Conway

instance
  ( IsConwayUniv fn
  , Inject (ConwayCertExecContext Conway) (Map (RewardAccount StandardCrypto) Coin)
  ) =>
  ExecSpecRule fn "CERT" Conway
  where
  type ExecContext fn "CERT" Conway = ConwayCertExecContext Conway
  environmentSpec :: HasCallStack =>
ExecContext fn "CERT" Conway
-> Specification fn (ExecEnvironment fn "CERT" Conway)
environmentSpec ExecContext fn "CERT" Conway
_ = forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
Specification fn (CertEnv Conway)
certEnvSpec
  stateSpec :: HasCallStack =>
ExecContext fn "CERT" Conway
-> ExecEnvironment fn "CERT" Conway
-> Specification fn (ExecState fn "CERT" Conway)
stateSpec ExecContext fn "CERT" Conway
_ ExecEnvironment fn "CERT" Conway
_ = forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
Specification fn (CertState Conway)
certStateSpec
  signalSpec :: HasCallStack =>
ExecContext fn "CERT" Conway
-> ExecEnvironment fn "CERT" Conway
-> ExecState fn "CERT" Conway
-> Specification fn (ExecSignal fn "CERT" Conway)
signalSpec ExecContext fn "CERT" Conway
_ = forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
CertEnv Conway
-> CertState Conway -> Specification fn (ConwayTxCert Conway)
txCertSpec
  runAgdaRule :: HasCallStack =>
SpecRep (ExecEnvironment fn "CERT" Conway)
-> SpecRep (ExecState fn "CERT" Conway)
-> SpecRep (ExecSignal fn "CERT" Conway)
-> Either
     (NonEmpty (SpecRep (PredicateFailure (EraRule "CERT" Conway))))
     (SpecRep (ExecState fn "CERT" Conway))
runAgdaRule SpecRep (ExecEnvironment fn "CERT" Conway)
env SpecRep (ExecState fn "CERT" Conway)
st SpecRep (ExecSignal fn "CERT" Conway)
sig =
    forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (\T_String_6
e -> String -> OpaqueErrorString
OpaqueErrorString (T_String_6 -> String
T.unpack T_String_6
e) forall a. a -> [a] -> NonEmpty a
NE.:| [])
      forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e a. ComputationResult e a -> Either e a
computationResultToEither
      forall a b. (a -> b) -> a -> b
$ CertEnv
-> CertState
-> DCert
-> T_ComputationResult_48 T_String_6 CertState
Agda.certStep SpecRep (ExecEnvironment fn "CERT" Conway)
env SpecRep (ExecState fn "CERT" Conway)
st SpecRep (ExecSignal fn "CERT" Conway)
sig

  classOf :: ExecSignal fn "CERT" Conway -> Maybe String
classOf = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConwayTxCert Conway -> String
nameTxCert

nameTxCert :: ConwayTxCert Conway -> String
nameTxCert :: ConwayTxCert Conway -> String
nameTxCert (ConwayTxCertDeleg ConwayDelegCert (EraCrypto Conway)
x) = forall c. ConwayDelegCert c -> String
nameDelegCert ConwayDelegCert (EraCrypto Conway)
x
nameTxCert (ConwayTxCertPool PoolCert (EraCrypto Conway)
x) = forall c. PoolCert c -> String
namePoolCert PoolCert (EraCrypto Conway)
x
nameTxCert (ConwayTxCertGov ConwayGovCert (EraCrypto Conway)
x) = forall c. ConwayGovCert c -> String
nameGovCert ConwayGovCert (EraCrypto Conway)
x