{-# 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 Cardano.Ledger.Conway.UTxO (getConwayWitsVKeyNeeded)
import Cardano.Ledger.Core (EraTx (..))
import Cardano.Ledger.Shelley.LedgerState (UTxOState (..))
import Data.Bifunctor (Bifunctor (..))
import qualified Data.Text as T
import Lens.Micro ((^.))
import qualified MAlonzo.Code.Ledger.Foreign.API 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 (
  UtxoExecContext,
  utxoEnvSpec,
  utxoStateSpec,
  utxoTxSpec,
 )
import qualified Test.Cardano.Ledger.Generic.PrettyCore as PP
import Test.Cardano.Ledger.Shelley.Utils (runSTS)
import Test.Cardano.Ledger.TreeDiff (showExpr)

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

  genExecContext :: HasCallStack => Gen (ExecContext "UTXOW" ConwayEra)
genExecContext = Gen (UtxoExecContext ConwayEra)
genUtxoExecContext
  environmentSpec :: HasCallStack =>
ExecContext "UTXOW" ConwayEra
-> Specification (ExecEnvironment "UTXOW" ConwayEra)
environmentSpec = UtxoExecContext ConwayEra -> Specification (UtxoEnv ConwayEra)
utxoEnvSpec
  stateSpec :: HasCallStack =>
ExecContext "UTXOW" ConwayEra
-> ExecEnvironment "UTXOW" ConwayEra
-> Specification (ExecState "UTXOW" ConwayEra)
stateSpec = UtxoExecContext ConwayEra
-> UtxoEnv ConwayEra -> Specification (UTxOState ConwayEra)
utxoStateSpec
  signalSpec :: HasCallStack =>
ExecContext "UTXOW" ConwayEra
-> ExecEnvironment "UTXOW" ConwayEra
-> ExecState "UTXOW" ConwayEra
-> Specification (ExecSignal "UTXOW" ConwayEra)
signalSpec ExecContext "UTXOW" ConwayEra
ctx ExecEnvironment "UTXOW" ConwayEra
_ ExecState "UTXOW" ConwayEra
_ = forall era.
HasSpec (AlonzoTx era) =>
UtxoExecContext era -> Specification (AlonzoTx era)
utxoTxSpec ExecContext "UTXOW" ConwayEra
ctx
  runAgdaRule :: HasCallStack =>
SpecRep (ExecEnvironment "UTXOW" ConwayEra)
-> SpecRep (ExecState "UTXOW" ConwayEra)
-> SpecRep (ExecSignal "UTXOW" ConwayEra)
-> Either OpaqueErrorString (SpecRep (ExecState "UTXOW" ConwayEra))
runAgdaRule SpecRep (ExecEnvironment "UTXOW" ConwayEra)
env SpecRep (ExecState "UTXOW" ConwayEra)
st SpecRep (ExecSignal "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 "UTXOW" ConwayEra)
env SpecRep (ExecState "UTXOW" ConwayEra)
st SpecRep (ExecSignal "UTXOW" ConwayEra)
sig
  extraInfo :: HasCallStack =>
Globals
-> ExecContext "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 "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 "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 (rule :: Symbol) era.
(ExecSpecRule rule era, HasCallStack) =>
Globals
-> ExecContext 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 @"UTXO" @ConwayEra Globals
globals ExecContext "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"
        , Doc AnsiStyle
"Impl:"
        , Doc AnsiStyle
"witsVKeyNeeded"
        , forall a. String -> Doc a
PP.ppString forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. ToExpr a => a -> String
showExpr forall a b. (a -> b) -> a -> b
$
            forall era.
(EraTx era, ConwayEraTxBody era) =>
UTxO era -> TxBody era -> Set (KeyHash 'Witness)
getConwayWitsVKeyNeeded @ConwayEra (forall era. UTxOState era -> UTxO era
utxosUtxo State (EraRule "UTXOW" ConwayEra)
st) (Signal (EraRule "UTXOW" ConwayEra)
sig forall s a. s -> Getting a s a -> a
^. forall era. EraTx era => Lens' (Tx era) (TxBody era)
bodyTxL)
        , Doc AnsiStyle
"witsVKeyHashes"
        , Doc AnsiStyle
"Spec:"
        , forall a. String -> Doc a
PP.ppString String
result
        , forall a. Monoid a => a
mempty
        , Doc AnsiStyle
"UTXO"
        , Doc AnsiStyle
utxoInfo
        ]