{-# 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 MAlonzo.Code.Ledger.Foreign.API 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 ExecSpecRule "POOL" ConwayEra where
  type ExecContext "POOL" ConwayEra = WitUniv ConwayEra
  environmentSpec :: HasCallStack =>
ExecContext "POOL" ConwayEra
-> Specification (ExecEnvironment "POOL" ConwayEra)
environmentSpec ExecContext "POOL" ConwayEra
ctx = forall era.
EraSpecPParams era =>
WitUniv era -> Specification (PoolEnv era)
poolEnvSpec ExecContext "POOL" ConwayEra
ctx

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

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

  runAgdaRule :: HasCallStack =>
SpecRep (ExecEnvironment "POOL" ConwayEra)
-> SpecRep (ExecState "POOL" ConwayEra)
-> SpecRep (ExecSignal "POOL" ConwayEra)
-> Either OpaqueErrorString (SpecRep (ExecState "POOL" ConwayEra))
runAgdaRule SpecRep (ExecEnvironment "POOL" ConwayEra)
env SpecRep (ExecState "POOL" ConwayEra)
st SpecRep (ExecSignal "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 "POOL" ConwayEra)
env SpecRep (ExecState "POOL" ConwayEra)
st SpecRep (ExecSignal "POOL" ConwayEra)
sig

  classOf :: ExecSignal "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"