{-# 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 ()
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
_ = Specification (ShelleyLedgersEnv ConwayEra)
Specification (ExecEnvironment "LEDGERS" ConwayEra)
forall a. Monoid a => a
mempty
  stateSpec :: HasCallStack =>
ExecContext "LEDGERS" ConwayEra
-> ExecEnvironment "LEDGERS" ConwayEra
-> Specification (ExecState "LEDGERS" ConwayEra)
stateSpec ExecContext "LEDGERS" ConwayEra
_ ExecEnvironment "LEDGERS" ConwayEra
_ = Specification (LedgerState ConwayEra)
Specification (ExecState "LEDGERS" ConwayEra)
forall a. Monoid a => a
mempty
  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
_ = Specification (Seq (Tx ConwayEra))
Specification (ExecSignal "LEDGERS" ConwayEra)
forall a. Monoid a => a
mempty
  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 = ComputationResult Text LState -> Either OpaqueErrorString LState
forall a. ComputationResult Text a -> Either OpaqueErrorString a
unComputationResult (ComputationResult Text LState -> Either OpaqueErrorString LState)
-> ComputationResult Text LState -> Either OpaqueErrorString LState
forall a b. (a -> b) -> a -> b
$ LEnv -> LState -> [Tx] -> ComputationResult Text LState
Agda.ledgersStep LEnv
SpecRep (ExecEnvironment "LEDGERS" ConwayEra)
env LState
SpecRep (ExecState "LEDGERS" ConwayEra)
st [Tx]
SpecRep (ExecSignal "LEDGERS" ConwayEra)
sig