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

module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Deleg (nameDelegCert) where

import Cardano.Ledger.Conway
import Cardano.Ledger.Conway.TxCert (ConwayDelegCert (..))
import Cardano.Ledger.Credential (Credential)
import Cardano.Ledger.Crypto (StandardCrypto)
import Cardano.Ledger.Keys (KeyRole (..))
import Constrained (lit)
import Data.Bifunctor (bimap)
import qualified Data.List.NonEmpty as NE
import Data.Set (Set)
import qualified Data.Text as T
import qualified Lib as Agda
import Test.Cardano.Ledger.Conformance
import Test.Cardano.Ledger.Conformance.ExecSpecRule.Core ()
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base ()
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Cert ()
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Deleg ()
import Test.Cardano.Ledger.Constrained.Conway

instance IsConwayUniv fn => ExecSpecRule fn "DELEG" Conway where
  type ExecContext fn "DELEG" Conway = Set (Credential 'DRepRole StandardCrypto)

  environmentSpec :: HasCallStack =>
ExecContext fn "DELEG" Conway
-> Specification fn (ExecEnvironment fn "DELEG" Conway)
environmentSpec ExecContext fn "DELEG" Conway
_ = forall era (fn :: [*] -> * -> *).
(EraSpecPParams era, IsConwayUniv fn) =>
Specification fn (ConwayDelegEnv era)
delegEnvSpec

  stateSpec :: HasCallStack =>
ExecContext fn "DELEG" Conway
-> ExecEnvironment fn "DELEG" Conway
-> Specification fn (ExecState fn "DELEG" Conway)
stateSpec ExecContext fn "DELEG" Conway
ctx ExecEnvironment fn "DELEG" Conway
_ = 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 ExecContext fn "DELEG" Conway
ctx)

  signalSpec :: HasCallStack =>
ExecContext fn "DELEG" Conway
-> ExecEnvironment fn "DELEG" Conway
-> ExecState fn "DELEG" Conway
-> Specification fn (ExecSignal fn "DELEG" Conway)
signalSpec ExecContext fn "DELEG" Conway
_ = forall (fn :: [*] -> * -> *) era.
(EraPParams era, IsConwayUniv fn) =>
ConwayDelegEnv era
-> CertState era
-> Specification fn (ConwayDelegCert (EraCrypto era))
conwayDelegCertSpec

  runAgdaRule :: HasCallStack =>
SpecRep (ExecEnvironment fn "DELEG" Conway)
-> SpecRep (ExecState fn "DELEG" Conway)
-> SpecRep (ExecSignal fn "DELEG" Conway)
-> Either
     (NonEmpty (SpecRep (PredicateFailure (EraRule "DELEG" Conway))))
     (SpecRep (ExecState fn "DELEG" Conway))
runAgdaRule SpecRep (ExecEnvironment fn "DELEG" Conway)
env (Agda.MkCertState DState
dState PState
pState GState
vState) SpecRep (ExecSignal fn "DELEG" 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
dState' -> DState -> PState -> GState -> CertState
Agda.MkCertState DState
dState' PState
pState GState
vState)
      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
$ DelegEnv
-> DState -> DCert -> T_ComputationResult_46 T_String_6 DState
Agda.delegStep SpecRep (ExecEnvironment fn "DELEG" Conway)
env DState
dState SpecRep (ExecSignal fn "DELEG" Conway)
sig

  classOf :: ExecSignal fn "DELEG" Conway -> Maybe String
classOf = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c. ConwayDelegCert c -> String
nameDelegCert

nameDelegCert :: ConwayDelegCert c -> String
nameDelegCert :: forall c. ConwayDelegCert c -> String
nameDelegCert ConwayRegCert {} = String
"RegKey"
nameDelegCert ConwayUnRegCert {} = String
"UnRegKey"
nameDelegCert ConwayDelegCert {} = String
"DelegateWithKey"
nameDelegCert ConwayRegDelegCert {} = String
"RegK&DelegateWithKey"