{-# 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 (Specification (..))
import qualified Lib as Agda
import Test.Cardano.Ledger.Conformance (
  ExecSpecRule (..),
  unComputationResult,
 )
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway ()
import Test.Cardano.Ledger.Constrained.Conway (IsConwayUniv)

instance IsConwayUniv fn => ExecSpecRule fn "LEDGERS" ConwayEra where
  type ExecContext fn "LEDGERS" ConwayEra = EnactState ConwayEra

  environmentSpec :: HasCallStack =>
ExecContext fn "LEDGERS" ConwayEra
-> Specification fn (ExecEnvironment fn "LEDGERS" ConwayEra)
environmentSpec ExecContext fn "LEDGERS" ConwayEra
_ = forall (fn :: [*] -> * -> *) a. Specification fn a
TrueSpec
  stateSpec :: HasCallStack =>
ExecContext fn "LEDGERS" ConwayEra
-> ExecEnvironment fn "LEDGERS" ConwayEra
-> Specification fn (ExecState fn "LEDGERS" ConwayEra)
stateSpec ExecContext fn "LEDGERS" ConwayEra
_ ExecEnvironment fn "LEDGERS" ConwayEra
_ = forall (fn :: [*] -> * -> *) a. Specification fn a
TrueSpec
  signalSpec :: HasCallStack =>
ExecContext fn "LEDGERS" ConwayEra
-> ExecEnvironment fn "LEDGERS" ConwayEra
-> ExecState fn "LEDGERS" ConwayEra
-> Specification fn (ExecSignal fn "LEDGERS" ConwayEra)
signalSpec ExecContext fn "LEDGERS" ConwayEra
_ ExecEnvironment fn "LEDGERS" ConwayEra
_ ExecState fn "LEDGERS" ConwayEra
_ = forall (fn :: [*] -> * -> *) a. Specification fn a
TrueSpec
  runAgdaRule :: HasCallStack =>
SpecRep (ExecEnvironment fn "LEDGERS" ConwayEra)
-> SpecRep (ExecState fn "LEDGERS" ConwayEra)
-> SpecRep (ExecSignal fn "LEDGERS" ConwayEra)
-> Either
     OpaqueErrorString (SpecRep (ExecState fn "LEDGERS" ConwayEra))
runAgdaRule SpecRep (ExecEnvironment fn "LEDGERS" ConwayEra)
env SpecRep (ExecState fn "LEDGERS" ConwayEra)
st SpecRep (ExecSignal fn "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 fn "LEDGERS" ConwayEra)
env SpecRep (ExecState fn "LEDGERS" ConwayEra)
st SpecRep (ExecSignal fn "LEDGERS" ConwayEra)
sig