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

module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Ledgers () where

import Cardano.Ledger.Conway (ConwayEra)
import Cardano.Ledger.Conway.Governance (EnactState)
import Constrained.API (Specification (..))
import qualified MAlonzo.Code.Ledger.Foreign.API as Agda
import Test.Cardano.Ledger.Conformance (
  ExecSpecRule (..),
  unComputationResult,
 )
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway ()

instance ExecSpecRule "LEDGERS" ConwayEra where
  type ExecContext "LEDGERS" ConwayEra = EnactState ConwayEra

  environmentSpec :: HasCallStack =>
ExecContext "LEDGERS" ConwayEra
-> Specification (ExecEnvironment "LEDGERS" ConwayEra)
environmentSpec ExecContext "LEDGERS" ConwayEra
_ = forall a. Specification a
TrueSpec
  stateSpec :: HasCallStack =>
ExecContext "LEDGERS" ConwayEra
-> ExecEnvironment "LEDGERS" ConwayEra
-> Specification (ExecState "LEDGERS" ConwayEra)
stateSpec ExecContext "LEDGERS" ConwayEra
_ ExecEnvironment "LEDGERS" ConwayEra
_ = forall a. Specification a
TrueSpec
  signalSpec :: HasCallStack =>
ExecContext "LEDGERS" ConwayEra
-> ExecEnvironment "LEDGERS" ConwayEra
-> ExecState "LEDGERS" ConwayEra
-> Specification (ExecSignal "LEDGERS" ConwayEra)
signalSpec ExecContext "LEDGERS" ConwayEra
_ ExecEnvironment "LEDGERS" ConwayEra
_ ExecState "LEDGERS" ConwayEra
_ = forall a. Specification a
TrueSpec
  runAgdaRule :: HasCallStack =>
SpecRep (ExecEnvironment "LEDGERS" ConwayEra)
-> SpecRep (ExecState "LEDGERS" ConwayEra)
-> SpecRep (ExecSignal "LEDGERS" ConwayEra)
-> Either
     OpaqueErrorString (SpecRep (ExecState "LEDGERS" ConwayEra))
runAgdaRule SpecRep (ExecEnvironment "LEDGERS" ConwayEra)
env SpecRep (ExecState "LEDGERS" ConwayEra)
st SpecRep (ExecSignal "LEDGERS" ConwayEra)
sig = forall a. ComputationResult Text a -> Either OpaqueErrorString a
unComputationResult forall a b. (a -> b) -> a -> b
$ LEnv -> LState -> [Tx] -> T_ComputationResult_46 Text LState
Agda.ledgersStep SpecRep (ExecEnvironment "LEDGERS" ConwayEra)
env SpecRep (ExecState "LEDGERS" ConwayEra)
st SpecRep (ExecSignal "LEDGERS" ConwayEra)
sig