{-# 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 = WitUniv ConwayEra -> Specification (PoolEnv ConwayEra)
forall era.
EraSpecPParams era =>
WitUniv era -> Specification (PoolEnv era)
poolEnvSpec WitUniv ConwayEra
ExecContext "POOL" ConwayEra
ctx

  stateSpec :: HasCallStack =>
ExecContext "POOL" ConwayEra
-> ExecEnvironment "POOL" ConwayEra
-> Specification (ExecState "POOL" ConwayEra)
stateSpec ExecContext "POOL" ConwayEra
ctx ExecEnvironment "POOL" ConwayEra
_ = WitUniv ConwayEra -> Specification (PState ConwayEra)
forall era. Era era => WitUniv era -> Specification (PState era)
pStateSpec WitUniv ConwayEra
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 WitUniv ConwayEra
ExecContext "POOL" ConwayEra
wituniv PoolEnv ConwayEra
ExecEnvironment "POOL" ConwayEra
env PState ConwayEra
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 = ComputationResult Text PState -> Either OpaqueErrorString PState
forall a. ComputationResult Text a -> Either OpaqueErrorString a
unComputationResult (ComputationResult Text PState -> Either OpaqueErrorString PState)
-> ComputationResult Text PState -> Either OpaqueErrorString PState
forall a b. (a -> b) -> a -> b
$ PParams -> PState -> DCert -> ComputationResult Text PState
Agda.poolStep PParams
SpecRep (ExecEnvironment "POOL" ConwayEra)
env PState
SpecRep (ExecState "POOL" ConwayEra)
st DCert
SpecRep (ExecSignal "POOL" ConwayEra)
sig

  classOf :: ExecSignal "POOL" ConwayEra -> Maybe String
classOf = String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String)
-> (PoolCert -> String) -> PoolCert -> Maybe String
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"