{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# 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 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
import Test.Cardano.Ledger.Constrained.Conway.WitnessUniverse

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

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

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

  runAgdaRule :: HasCallStack =>
SpecRep (ExecEnvironment fn "POOL" ConwayEra)
-> SpecRep (ExecState fn "POOL" ConwayEra)
-> SpecRep (ExecSignal fn "POOL" ConwayEra)
-> Either
     OpaqueErrorString (SpecRep (ExecState fn "POOL" ConwayEra))
runAgdaRule SpecRep (ExecEnvironment fn "POOL" ConwayEra)
env SpecRep (ExecState fn "POOL" ConwayEra)
st SpecRep (ExecSignal fn "POOL" ConwayEra)
sig = forall a. ComputationResult Text a -> Either OpaqueErrorString a
unComputationResult forall a b. (a -> b) -> a -> b
$ PParams -> PState -> DCert -> T_ComputationResult_46 Text PState
Agda.poolStep SpecRep (ExecEnvironment fn "POOL" ConwayEra)
env SpecRep (ExecState fn "POOL" ConwayEra)
st SpecRep (ExecSignal fn "POOL" ConwayEra)
sig

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

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