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

module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Pool where

import Cardano.Ledger.Conway
import Cardano.Ledger.Core (PoolCert (..))
import Data.Bifunctor (first)
import qualified Data.List.NonEmpty as NE
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.Pool ()
import Test.Cardano.Ledger.Constrained.Conway

instance IsConwayUniv fn => ExecSpecRule fn "POOL" Conway where
  environmentSpec :: HasCallStack =>
ExecContext fn "POOL" Conway
-> Specification fn (ExecEnvironment fn "POOL" Conway)
environmentSpec ExecContext fn "POOL" Conway
_ = forall (fn :: [*] -> * -> *) era.
(EraSpecPParams era, IsConwayUniv fn) =>
Specification fn (PoolEnv era)
poolEnvSpec

  stateSpec :: HasCallStack =>
ExecContext fn "POOL" Conway
-> ExecEnvironment fn "POOL" Conway
-> Specification fn (ExecState fn "POOL" Conway)
stateSpec ExecContext fn "POOL" Conway
_ ExecEnvironment fn "POOL" Conway
_ = forall (fn :: [*] -> * -> *) era.
(Era era, IsConwayUniv fn) =>
Specification fn (PState era)
pStateSpec

  signalSpec :: HasCallStack =>
ExecContext fn "POOL" Conway
-> ExecEnvironment fn "POOL" Conway
-> ExecState fn "POOL" Conway
-> Specification fn (ExecSignal fn "POOL" Conway)
signalSpec ExecContext fn "POOL" Conway
_ ExecEnvironment fn "POOL" Conway
env ExecState fn "POOL" Conway
st = forall (fn :: [*] -> * -> *) era.
(EraSpecPParams era, IsConwayUniv fn) =>
PoolEnv era
-> PState era -> Specification fn (PoolCert (EraCrypto era))
poolCertSpec ExecEnvironment fn "POOL" Conway
env ExecState fn "POOL" Conway
st

  runAgdaRule :: HasCallStack =>
SpecRep (ExecEnvironment fn "POOL" Conway)
-> SpecRep (ExecState fn "POOL" Conway)
-> SpecRep (ExecSignal fn "POOL" Conway)
-> Either
     (NonEmpty (SpecRep (PredicateFailure (EraRule "POOL" Conway))))
     (SpecRep (ExecState fn "POOL" Conway))
runAgdaRule SpecRep (ExecEnvironment fn "POOL" Conway)
env SpecRep (ExecState fn "POOL" Conway)
st SpecRep (ExecSignal fn "POOL" 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
$ PParams
-> PState -> DCert -> T_ComputationResult_46 T_String_6 PState
Agda.poolStep SpecRep (ExecEnvironment fn "POOL" Conway)
env SpecRep (ExecState fn "POOL" Conway)
st SpecRep (ExecSignal fn "POOL" Conway)
sig

  classOf :: ExecSignal fn "POOL" Conway -> Maybe String
classOf = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c. PoolCert c -> String
namePoolCert

namePoolCert :: PoolCert c -> String
namePoolCert :: forall c. PoolCert c -> String
namePoolCert RegPool {} = String
"RegPool"
namePoolCert RetirePool {} = String
"RetirePool"