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

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

import Cardano.Ledger.Conway (Conway, ConwayEra)
import Cardano.Ledger.Conway.TxCert (ConwayTxCert)
import Cardano.Ledger.Crypto (StandardCrypto)
import Data.Bifunctor (Bifunctor (..))
import qualified Data.List.NonEmpty as NE
import qualified Data.Text as T
import qualified Lib as Agda
import Test.Cardano.Ledger.Conformance (
  ExecSpecRule (..),
  OpaqueErrorString (..),
  SpecTranslate,
  computationResultToEither,
 )
import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Utxo (genUtxoExecContext)
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base (ConwayTxBodyTransContext)
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Utxow ()
import Test.Cardano.Ledger.Constrained.Conway (
  IsConwayUniv,
  UtxoExecContext,
  utxoEnvSpec,
  utxoStateSpec,
  utxoTxSpec,
 )

instance
  ( IsConwayUniv fn
  , SpecTranslate (ConwayTxBodyTransContext StandardCrypto) (ConwayTxCert (ConwayEra StandardCrypto))
  ) =>
  ExecSpecRule fn "UTXOW" Conway
  where
  type ExecContext fn "UTXOW" Conway = UtxoExecContext Conway

  genExecContext :: HasCallStack =>
Gen (ExecContext fn "UTXOW" (ConwayEra StandardCrypto))
genExecContext = Gen (UtxoExecContext (ConwayEra StandardCrypto))
genUtxoExecContext
  environmentSpec :: HasCallStack =>
ExecContext fn "UTXOW" (ConwayEra StandardCrypto)
-> Specification
     fn (ExecEnvironment fn "UTXOW" (ConwayEra StandardCrypto))
environmentSpec = forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
UtxoExecContext (ConwayEra StandardCrypto)
-> Specification fn (UtxoEnv (ConwayEra StandardCrypto))
utxoEnvSpec
  stateSpec :: HasCallStack =>
ExecContext fn "UTXOW" (ConwayEra StandardCrypto)
-> ExecEnvironment fn "UTXOW" (ConwayEra StandardCrypto)
-> Specification
     fn (ExecState fn "UTXOW" (ConwayEra StandardCrypto))
stateSpec = forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
UtxoExecContext (ConwayEra StandardCrypto)
-> UtxoEnv (ConwayEra StandardCrypto)
-> Specification fn (UTxOState (ConwayEra StandardCrypto))
utxoStateSpec
  signalSpec :: HasCallStack =>
ExecContext fn "UTXOW" (ConwayEra StandardCrypto)
-> ExecEnvironment fn "UTXOW" (ConwayEra StandardCrypto)
-> ExecState fn "UTXOW" (ConwayEra StandardCrypto)
-> Specification
     fn (ExecSignal fn "UTXOW" (ConwayEra StandardCrypto))
signalSpec ExecContext fn "UTXOW" (ConwayEra StandardCrypto)
ctx ExecEnvironment fn "UTXOW" (ConwayEra StandardCrypto)
_ ExecState fn "UTXOW" (ConwayEra StandardCrypto)
_ = forall (fn :: [*] -> * -> *) era.
(IsConwayUniv fn, HasSpec fn (AlonzoTx era)) =>
UtxoExecContext era -> Specification fn (AlonzoTx era)
utxoTxSpec ExecContext fn "UTXOW" (ConwayEra StandardCrypto)
ctx
  runAgdaRule :: HasCallStack =>
SpecRep (ExecEnvironment fn "UTXOW" (ConwayEra StandardCrypto))
-> SpecRep (ExecState fn "UTXOW" (ConwayEra StandardCrypto))
-> SpecRep (ExecSignal fn "UTXOW" (ConwayEra StandardCrypto))
-> Either
     (NonEmpty
        (SpecRep
           (PredicateFailure (EraRule "UTXOW" (ConwayEra StandardCrypto)))))
     (SpecRep (ExecState fn "UTXOW" (ConwayEra StandardCrypto)))
runAgdaRule SpecRep (ExecEnvironment fn "UTXOW" (ConwayEra StandardCrypto))
env SpecRep (ExecState fn "UTXOW" (ConwayEra StandardCrypto))
st SpecRep (ExecSignal fn "UTXOW" (ConwayEra StandardCrypto))
sig =
    forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (\T_String_6
e -> String -> OpaqueErrorString
OpaqueErrorString (T_String_6 -> String
T.unpack T_String_6
e) forall a. a -> [a] -> NonEmpty a
NE.:| [])
      forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e a. ComputationResult e a -> Either e a
computationResultToEither
      forall a b. (a -> b) -> a -> b
$ UTxOEnv
-> UTxOState -> Tx -> T_ComputationResult_48 T_String_6 UTxOState
Agda.utxowStep SpecRep (ExecEnvironment fn "UTXOW" (ConwayEra StandardCrypto))
env SpecRep (ExecState fn "UTXOW" (ConwayEra StandardCrypto))
st SpecRep (ExecSignal fn "UTXOW" (ConwayEra StandardCrypto))
sig