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

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

import Cardano.Ledger.Conway
import Cardano.Ledger.Conway.TxCert (ConwayTxCert (..))
import Constrained.API
import qualified MAlonzo.Code.Ledger.Foreign.API 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
import Test.Cardano.Ledger.Constrained.Conway.WitnessUniverse

instance ExecSpecRule "CERT" ConwayEra where
  type ExecContext "CERT" ConwayEra = (WitUniv ConwayEra, ConwayCertExecContext ConwayEra)

  genExecContext :: HasCallStack => Gen (ExecContext "CERT" ConwayEra)
genExecContext = do
    WitUniv ConwayEra
univ <- forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv @ConwayEra Int
300
    ConwayCertExecContext ConwayEra
ccec <- forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec (forall era.
Era era =>
WitUniv era -> Integer -> Specification (ConwayCertExecContext era)
conwayCertExecContextSpec WitUniv ConwayEra
univ Integer
5)
    forall (f :: * -> *) a. Applicative f => a -> f a
pure (WitUniv ConwayEra
univ, ConwayCertExecContext ConwayEra
ccec)

  environmentSpec :: HasCallStack =>
ExecContext "CERT" ConwayEra
-> Specification (ExecEnvironment "CERT" ConwayEra)
environmentSpec (WitUniv ConwayEra
univ, ConwayCertExecContext ConwayEra
_) = forall era.
EraSpecPParams era =>
WitUniv era -> Specification (CertEnv era)
certEnvSpec @ConwayEra WitUniv ConwayEra
univ

  stateSpec :: HasCallStack =>
ExecContext "CERT" ConwayEra
-> ExecEnvironment "CERT" ConwayEra
-> Specification (ExecState "CERT" ConwayEra)
stateSpec (WitUniv ConwayEra
univ, ConwayCertExecContext ConwayEra
ccec) ExecEnvironment "CERT" ConwayEra
_ =
    forall era.
EraSpecCert era =>
WitUniv era
-> Set (Credential 'DRepRole)
-> Map RewardAccount Coin
-> Specification (CertState era)
certStateSpec @ConwayEra WitUniv ConwayEra
univ (forall era. ConwayCertExecContext era -> Set (Credential 'DRepRole)
ccecDelegatees ConwayCertExecContext ConwayEra
ccec) (forall era. ConwayCertExecContext era -> Map RewardAccount Coin
ccecWithdrawals ConwayCertExecContext ConwayEra
ccec)

  signalSpec :: HasCallStack =>
ExecContext "CERT" ConwayEra
-> ExecEnvironment "CERT" ConwayEra
-> ExecState "CERT" ConwayEra
-> Specification (ExecSignal "CERT" ConwayEra)
signalSpec (WitUniv ConwayEra
univ, ConwayCertExecContext ConwayEra
_) ExecEnvironment "CERT" ConwayEra
env ExecState "CERT" ConwayEra
state = forall era.
(era ~ ConwayEra) =>
WitUniv era
-> CertEnv era -> CertState era -> Specification (ConwayTxCert era)
conwayTxCertSpec @ConwayEra WitUniv ConwayEra
univ ExecEnvironment "CERT" ConwayEra
env ExecState "CERT" ConwayEra
state

  runAgdaRule :: HasCallStack =>
SpecRep (ExecEnvironment "CERT" ConwayEra)
-> SpecRep (ExecState "CERT" ConwayEra)
-> SpecRep (ExecSignal "CERT" ConwayEra)
-> Either OpaqueErrorString (SpecRep (ExecState "CERT" ConwayEra))
runAgdaRule SpecRep (ExecEnvironment "CERT" ConwayEra)
env SpecRep (ExecState "CERT" ConwayEra)
st SpecRep (ExecSignal "CERT" ConwayEra)
sig =
    forall a. ComputationResult Text a -> Either OpaqueErrorString a
unComputationResult forall a b. (a -> b) -> a -> b
$
      CertEnv
-> CertState -> DCert -> T_ComputationResult_46 Text CertState
Agda.certStep SpecRep (ExecEnvironment "CERT" ConwayEra)
env SpecRep (ExecState "CERT" ConwayEra)
st SpecRep (ExecSignal "CERT" ConwayEra)
sig

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

nameTxCert :: ConwayTxCert ConwayEra -> String
nameTxCert :: ConwayTxCert ConwayEra -> String
nameTxCert (ConwayTxCertDeleg ConwayDelegCert
x) = ConwayDelegCert -> String
nameDelegCert ConwayDelegCert
x
nameTxCert (ConwayTxCertPool PoolCert
x) = PoolCert -> String
namePoolCert PoolCert
x
nameTxCert (ConwayTxCertGov ConwayGovCert
x) = ConwayGovCert -> String
nameGovCert ConwayGovCert
x