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

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

import Cardano.Ledger.Conway
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.Conway.ImpTest ()

instance ExecSpecRule "POOL" ConwayEra where
  runAgdaRule :: HasCallStack =>
SpecTRC "POOL" ConwayEra
-> Either Text (SpecState "POOL" ConwayEra)
runAgdaRule = (SpecEnvironment "POOL" ConwayEra
 -> SpecState "POOL" ConwayEra
 -> SpecSignal "POOL" ConwayEra
 -> ComputationResult Text (SpecState "POOL" ConwayEra))
-> SpecTRC "POOL" ConwayEra
-> Either Text (SpecState "POOL" ConwayEra)
forall (rule :: Symbol) era.
(SpecEnvironment rule era
 -> SpecState rule era
 -> SpecSignal rule era
 -> ComputationResult Text (SpecState rule era))
-> SpecTRC rule era -> Either Text (SpecState rule era)
runFromAgdaFunction PParams -> PState -> DCert -> T_ComputationResult_44 Text PState
SpecEnvironment "POOL" ConwayEra
-> SpecState "POOL" ConwayEra
-> SpecSignal "POOL" ConwayEra
-> ComputationResult Text (SpecState "POOL" ConwayEra)
Agda.poolStep