{-# 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
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
import Test.Cardano.Ledger.Constrained.Conway.WitnessUniverse

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

  genExecContext :: HasCallStack => Gen (ExecContext fn "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 (fn :: [*] -> * -> *) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec @ConwayFn (forall (fn :: [*] -> * -> *) era.
(Reflect era, IsConwayUniv fn) =>
WitUniv era
-> Integer -> Specification fn (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 fn "CERT" ConwayEra
-> Specification fn (ExecEnvironment fn "CERT" ConwayEra)
environmentSpec (WitUniv ConwayEra
univ, ConwayCertExecContext ConwayEra
_) = forall (fn :: [*] -> * -> *) era.
(EraSpecPParams era, IsConwayUniv fn) =>
WitUniv era -> Specification fn (CertEnv era)
certEnvSpec @fn @ConwayEra WitUniv ConwayEra
univ

  stateSpec :: HasCallStack =>
ExecContext fn "CERT" ConwayEra
-> ExecEnvironment fn "CERT" ConwayEra
-> Specification fn (ExecState fn "CERT" ConwayEra)
stateSpec (WitUniv ConwayEra
univ, ConwayCertExecContext ConwayEra
ccec) ExecEnvironment fn "CERT" ConwayEra
_ =
    forall era (fn :: [*] -> * -> *).
EraSpecCert era fn =>
WitUniv era
-> Set (Credential 'DRepRole)
-> Map RewardAccount Coin
-> Specification fn (CertState era)
certStateSpec @ConwayEra @fn 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 fn "CERT" ConwayEra
-> ExecEnvironment fn "CERT" ConwayEra
-> ExecState fn "CERT" ConwayEra
-> Specification fn (ExecSignal fn "CERT" ConwayEra)
signalSpec (WitUniv ConwayEra
univ, ConwayCertExecContext ConwayEra
_) ExecEnvironment fn "CERT" ConwayEra
env ExecState fn "CERT" ConwayEra
state = forall (fn :: [*] -> * -> *) era.
(IsConwayUniv fn, era ~ ConwayEra) =>
WitUniv era
-> CertEnv era
-> CertState era
-> Specification fn (ConwayTxCert era)
conwayTxCertSpec @fn @ConwayEra WitUniv ConwayEra
univ ExecEnvironment fn "CERT" ConwayEra
env ExecState fn "CERT" ConwayEra
state

  runAgdaRule :: HasCallStack =>
SpecRep (ExecEnvironment fn "CERT" ConwayEra)
-> SpecRep (ExecState fn "CERT" ConwayEra)
-> SpecRep (ExecSignal fn "CERT" ConwayEra)
-> Either
     OpaqueErrorString (SpecRep (ExecState fn "CERT" ConwayEra))
runAgdaRule SpecRep (ExecEnvironment fn "CERT" ConwayEra)
env SpecRep (ExecState fn "CERT" ConwayEra)
st SpecRep (ExecSignal fn "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 fn "CERT" ConwayEra)
env SpecRep (ExecState fn "CERT" ConwayEra)
st SpecRep (ExecSignal fn "CERT" ConwayEra)
sig

  classOf :: ExecSignal fn "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