{-# 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 :: [*] -> * -> *).
IsConwayUniv fn =>
Specification fn (PoolEnv Conway)
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 :: [*] -> * -> *).
IsConwayUniv fn =>
Specification fn (PState Conway)
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 :: [*] -> * -> *).
IsConwayUniv fn =>
PoolEnv Conway
-> PState Conway -> Specification fn (PoolCert StandardCrypto)
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_48 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"