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

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

import Cardano.Ledger.BaseTypes (Inject)
import Cardano.Ledger.Coin (Coin)
import Cardano.Ledger.Conway
import Cardano.Ledger.Conway.TxCert
import Cardano.Ledger.Crypto (StandardCrypto)
import Constrained (lit)
import Data.Bifunctor (Bifunctor (..))
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.Constrained.Conway

instance
  ( IsConwayUniv fn
  , Inject (ConwayCertExecContext Conway) (Map (DepositPurpose StandardCrypto) Coin)
  ) =>
  ExecSpecRule fn "GOVCERT" Conway
  where
  type ExecContext fn "GOVCERT" Conway = ConwayCertExecContext Conway

  environmentSpec :: HasCallStack =>
ExecContext fn "GOVCERT" Conway
-> Specification fn (ExecEnvironment fn "GOVCERT" Conway)
environmentSpec ExecContext fn "GOVCERT" Conway
_ctx = forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
Specification fn (ConwayGovCertEnv Conway)
govCertEnvSpec

  stateSpec :: HasCallStack =>
ExecContext fn "GOVCERT" Conway
-> ExecEnvironment fn "GOVCERT" Conway
-> Specification fn (ExecState fn "GOVCERT" Conway)
stateSpec ExecContext fn "GOVCERT" Conway
ctx ExecEnvironment fn "GOVCERT" Conway
_env = forall (fn :: [*] -> * -> *) era.
(IsConwayUniv fn, EraSpecDeleg era) =>
Term fn (Set (Credential 'DRepRole (EraCrypto era)))
-> Specification fn (CertState era)
certStateSpec (forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit forall a b. (a -> b) -> a -> b
$ forall era.
ConwayCertExecContext era
-> Set (Credential 'DRepRole (EraCrypto era))
ccecDelegatees ExecContext fn "GOVCERT" Conway
ctx)

  signalSpec :: HasCallStack =>
ExecContext fn "GOVCERT" Conway
-> ExecEnvironment fn "GOVCERT" Conway
-> ExecState fn "GOVCERT" Conway
-> Specification fn (ExecSignal fn "GOVCERT" Conway)
signalSpec ExecContext fn "GOVCERT" Conway
_ctx = forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
ConwayGovCertEnv Conway
-> CertState Conway
-> Specification fn (ConwayGovCert StandardCrypto)
govCertSpec

  classOf :: ExecSignal fn "GOVCERT" Conway -> Maybe String
classOf = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c. ConwayGovCert c -> String
nameGovCert

  runAgdaRule :: HasCallStack =>
SpecRep (ExecEnvironment fn "GOVCERT" Conway)
-> SpecRep (ExecState fn "GOVCERT" Conway)
-> SpecRep (ExecSignal fn "GOVCERT" Conway)
-> Either
     (NonEmpty (SpecRep (PredicateFailure (EraRule "GOVCERT" Conway))))
     (SpecRep (ExecState fn "GOVCERT" Conway))
runAgdaRule SpecRep (ExecEnvironment fn "GOVCERT" Conway)
env (Agda.MkCertState DState
dState PState
pState GState
vState) SpecRep (ExecSignal fn "GOVCERT" Conway)
sig =
    forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap
      (\T_String_6
e -> String -> OpaqueErrorString
OpaqueErrorString (T_String_6 -> String
T.unpack T_String_6
e) forall a. a -> [a] -> NonEmpty a
NE.:| [])
      (DState -> PState -> GState -> CertState
Agda.MkCertState DState
dState PState
pState)
      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
-> GState -> DCert -> T_ComputationResult_46 T_String_6 GState
Agda.govCertStep SpecRep (ExecEnvironment fn "GOVCERT" Conway)
env GState
vState SpecRep (ExecSignal fn "GOVCERT" Conway)
sig

nameGovCert :: ConwayGovCert c -> String
nameGovCert :: forall c. ConwayGovCert c -> String
nameGovCert (ConwayRegDRep {}) = String
"ConwayRegDRep"
nameGovCert (ConwayUnRegDRep {}) = String
"ConwayUnRegDRep"
nameGovCert (ConwayUpdateDRep {}) = String
"ConwayUpdateDRep"
nameGovCert (ConwayAuthCommitteeHotKey {}) = String
"ConwayAuthCommitteeHotKey"
nameGovCert (ConwayResignCommitteeColdKey {}) = String
"ConwayResignCommitteeColdKey"