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

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

import Cardano.Ledger.Conway (ConwayEra)
import Cardano.Ledger.Conway.TxCert (ConwayTxCert)
import Data.Bifunctor (Bifunctor (..))
import qualified Data.Text as T
import qualified Lib as Agda
import qualified Prettyprinter as PP
import Test.Cardano.Ledger.Conformance (
  ExecSpecRule (..),
  SpecTranslate,
  runSpecTransM,
  showOpaqueErrorString,
  toSpecRep,
  unComputationResult,
 )
import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base (externalFunctions)
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,
 )
import qualified Test.Cardano.Ledger.Generic.PrettyCore as PP
import Test.Cardano.Ledger.Shelley.Utils (runSTS)

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

  genExecContext :: HasCallStack => Gen (ExecContext fn "UTXOW" ConwayEra)
genExecContext = Gen (UtxoExecContext ConwayEra)
genUtxoExecContext
  environmentSpec :: HasCallStack =>
ExecContext fn "UTXOW" ConwayEra
-> Specification fn (ExecEnvironment fn "UTXOW" ConwayEra)
environmentSpec = forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
UtxoExecContext ConwayEra -> Specification fn (UtxoEnv ConwayEra)
utxoEnvSpec
  stateSpec :: HasCallStack =>
ExecContext fn "UTXOW" ConwayEra
-> ExecEnvironment fn "UTXOW" ConwayEra
-> Specification fn (ExecState fn "UTXOW" ConwayEra)
stateSpec = forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
UtxoExecContext ConwayEra
-> UtxoEnv ConwayEra -> Specification fn (UTxOState ConwayEra)
utxoStateSpec
  signalSpec :: HasCallStack =>
ExecContext fn "UTXOW" ConwayEra
-> ExecEnvironment fn "UTXOW" ConwayEra
-> ExecState fn "UTXOW" ConwayEra
-> Specification fn (ExecSignal fn "UTXOW" ConwayEra)
signalSpec ExecContext fn "UTXOW" ConwayEra
ctx ExecEnvironment fn "UTXOW" ConwayEra
_ ExecState fn "UTXOW" ConwayEra
_ = forall (fn :: [*] -> * -> *) era.
(IsConwayUniv fn, HasSpec fn (AlonzoTx era)) =>
UtxoExecContext era -> Specification fn (AlonzoTx era)
utxoTxSpec ExecContext fn "UTXOW" ConwayEra
ctx
  runAgdaRule :: HasCallStack =>
SpecRep (ExecEnvironment fn "UTXOW" ConwayEra)
-> SpecRep (ExecState fn "UTXOW" ConwayEra)
-> SpecRep (ExecSignal fn "UTXOW" ConwayEra)
-> Either
     OpaqueErrorString (SpecRep (ExecState fn "UTXOW" ConwayEra))
runAgdaRule SpecRep (ExecEnvironment fn "UTXOW" ConwayEra)
env SpecRep (ExecState fn "UTXOW" ConwayEra)
st SpecRep (ExecSignal fn "UTXOW" ConwayEra)
sig =
    forall a. ComputationResult Text a -> Either OpaqueErrorString a
unComputationResult forall a b. (a -> b) -> a -> b
$ T_ExternalFunctions_8
-> UTxOEnv
-> UTxOState
-> Tx
-> T_ComputationResult_46 Text UTxOState
Agda.utxowStep T_ExternalFunctions_8
externalFunctions SpecRep (ExecEnvironment fn "UTXOW" ConwayEra)
env SpecRep (ExecState fn "UTXOW" ConwayEra)
st SpecRep (ExecSignal fn "UTXOW" ConwayEra)
sig
  extraInfo :: HasCallStack =>
Globals
-> ExecContext fn "UTXOW" ConwayEra
-> Environment (EraRule "UTXOW" ConwayEra)
-> State (EraRule "UTXOW" ConwayEra)
-> Signal (EraRule "UTXOW" ConwayEra)
-> Either
     OpaqueErrorString
     (State (EraRule "UTXOW" ConwayEra),
      [Event (EraRule "UTXOW" ConwayEra)])
-> Doc AnsiStyle
extraInfo Globals
globals ExecContext fn "UTXOW" ConwayEra
ctx Environment (EraRule "UTXOW" ConwayEra)
env State (EraRule "UTXOW" ConwayEra)
st Signal (EraRule "UTXOW" ConwayEra)
sig Either
  OpaqueErrorString
  (State (EraRule "UTXOW" ConwayEra),
   [Event (EraRule "UTXOW" ConwayEra)])
_ =
    let
      result :: String
result =
        forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall a. Show a => a -> String
show Text -> String
T.unpack forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ctx a. ctx -> SpecTransM ctx a -> Either Text a
runSpecTransM ExecContext fn "UTXOW" ConwayEra
ctx forall a b. (a -> b) -> a -> b
$
          T_ExternalFunctions_8 -> UTxOEnv -> UTxOState -> Tx -> Text
Agda.utxowDebug T_ExternalFunctions_8
externalFunctions
            forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Environment (EraRule "UTXOW" ConwayEra)
env
            forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep State (EraRule "UTXOW" ConwayEra)
st
            forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Signal (EraRule "UTXOW" ConwayEra)
sig
      stFinal :: Either
  OpaqueErrorString
  (State (EraRule "UTXO" ConwayEra),
   [Event (EraRule "UTXO" ConwayEra)])
stFinal = forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first forall a. ToExpr a => a -> OpaqueErrorString
showOpaqueErrorString forall a b. (a -> b) -> a -> b
$ forall (rule :: Symbol) era.
(BaseM (EraRule rule era) ~ ShelleyBase, STS (EraRule rule era)) =>
Globals
-> Environment (EraRule rule era)
-> State (EraRule rule era)
-> Signal (EraRule rule era)
-> Either
     (NonEmpty (PredicateFailure (EraRule rule era)))
     (State (EraRule rule era), [Event (EraRule rule era)])
runSTS @"UTXO" @ConwayEra Globals
globals Environment (EraRule "UTXOW" ConwayEra)
env State (EraRule "UTXOW" ConwayEra)
st Signal (EraRule "UTXOW" ConwayEra)
sig
      utxoInfo :: Doc AnsiStyle
utxoInfo = forall (fn :: [*] -> * -> *) (rule :: Symbol) era.
(ExecSpecRule fn rule era, HasCallStack) =>
Globals
-> ExecContext fn rule era
-> Environment (EraRule rule era)
-> State (EraRule rule era)
-> Signal (EraRule rule era)
-> Either
     OpaqueErrorString
     (State (EraRule rule era), [Event (EraRule rule era)])
-> Doc AnsiStyle
extraInfo @fn @"UTXO" @ConwayEra Globals
globals ExecContext fn "UTXOW" ConwayEra
ctx Environment (EraRule "UTXOW" ConwayEra)
env State (EraRule "UTXOW" ConwayEra)
st Signal (EraRule "UTXOW" ConwayEra)
sig Either
  OpaqueErrorString
  (State (EraRule "UTXO" ConwayEra),
   [Event (EraRule "UTXO" ConwayEra)])
stFinal
     in
      forall ann. [Doc ann] -> Doc ann
PP.vcat
        [ Doc AnsiStyle
"UTXOW"
        , forall a. String -> Doc a
PP.ppString String
result
        , forall a. Monoid a => a
mempty
        , Doc AnsiStyle
"UTXO"
        , Doc AnsiStyle
utxoInfo
        ]