{-# 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.Core (EraTx (..))
import Cardano.Ledger.Conway.TxCert (ConwayTxCert)
import Cardano.Ledger.Conway.UTxO (getConwayWitsVKeyNeeded)
import Cardano.Ledger.Shelley.LedgerState (UTxOState (..))
import Cardano.Ledger.TxIn (TxId)
import Control.State.Transition.Extended (TRC (..))
import Data.Bifunctor (Bifunctor (..))
import Data.Coerce (coerce)
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 (..),
  runFromAgdaFunction,
  runSpecTransM,
 )
import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base (externalFunctions)
import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Utxo ()
import Test.Cardano.Ledger.Constrained.Conway (
  UtxoExecContext,
 )
import Test.Cardano.Ledger.Conway.TreeDiff (showExpr)
import Test.Cardano.Ledger.Shelley.Utils (runSTS)

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

  runAgdaRule :: HasCallStack =>
SpecTRC "UTXOW" ConwayEra
-> Either Text (SpecState "UTXOW" ConwayEra)
runAgdaRule = (SpecEnvironment "UTXOW" ConwayEra
 -> SpecState "UTXOW" ConwayEra
 -> SpecSignal "UTXOW" ConwayEra
 -> ComputationResult Text (SpecState "UTXOW" ConwayEra))
-> SpecTRC "UTXOW" ConwayEra
-> Either Text (SpecState "UTXOW" ConwayEra)
forall (rule :: Symbol) era.
(SpecEnvironment rule era
 -> SpecState rule era
 -> SpecSignal rule era
 -> ComputationResult Text (SpecState rule era))
-> SpecTRC rule era -> Either Text (SpecState rule era)
runFromAgdaFunction (T_ExternalFunctions_8
-> UTxOEnv
-> UTxOState
-> Tx
-> T_ComputationResult_44 Text UTxOState
Agda.utxowStep T_ExternalFunctions_8
externalFunctions)

  extraInfo :: HasCallStack =>
Globals
-> ExecContext "UTXOW" ConwayEra
-> TRC (EraRule "UTXOW" ConwayEra)
-> Either
     Text
     (State (EraRule "UTXOW" ConwayEra),
      [Event (EraRule "UTXOW" ConwayEra)])
-> Doc AnsiStyle
extraInfo Globals
globals ExecContext "UTXOW" ConwayEra
ctx trc :: TRC (EraRule "UTXOW" ConwayEra)
trc@(TRC (Environment (EraRule "UTXOW" ConwayEra)
env, State (EraRule "UTXOW" ConwayEra)
st, Signal (EraRule "UTXOW" ConwayEra)
sig)) Either
  Text
  (State (EraRule "UTXOW" ConwayEra),
   [Event (EraRule "UTXOW" ConwayEra)])
_ =
    let
      result :: String
result =
        (Text -> String) -> (Text -> String) -> Either Text Text -> String
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Text -> String
forall a. Show a => a -> String
show Text -> String
T.unpack (Either Text Text -> String)
-> (SpecTransM (UtxoExecContext ConwayEra) Text
    -> Either Text Text)
-> SpecTransM (UtxoExecContext ConwayEra) Text
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UtxoExecContext ConwayEra
-> SpecTransM (UtxoExecContext ConwayEra) Text -> Either Text Text
forall ctx a. ctx -> SpecTransM ctx a -> Either Text a
runSpecTransM UtxoExecContext ConwayEra
ExecContext "UTXOW" ConwayEra
ctx (SpecTransM (UtxoExecContext ConwayEra) Text -> String)
-> SpecTransM (UtxoExecContext ConwayEra) Text -> String
forall a b. (a -> b) -> a -> b
$
          T_ExternalFunctions_8 -> UTxOEnv -> UTxOState -> Tx -> Text
Agda.utxowDebug T_ExternalFunctions_8
externalFunctions
            (UTxOEnv -> UTxOState -> Tx -> Text)
-> SpecTransM (UtxoExecContext ConwayEra) UTxOEnv
-> SpecTransM (UtxoExecContext ConwayEra) (UTxOState -> Tx -> Text)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UtxoEnv ConwayEra
-> SpecTransM
     (UtxoExecContext ConwayEra) (SpecRep (UtxoEnv ConwayEra))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep UtxoEnv ConwayEra
Environment (EraRule "UTXOW" ConwayEra)
env
            SpecTransM (UtxoExecContext ConwayEra) (UTxOState -> Tx -> Text)
-> SpecTransM (UtxoExecContext ConwayEra) UTxOState
-> SpecTransM (UtxoExecContext ConwayEra) (Tx -> Text)
forall a b.
SpecTransM (UtxoExecContext ConwayEra) (a -> b)
-> SpecTransM (UtxoExecContext ConwayEra) a
-> SpecTransM (UtxoExecContext ConwayEra) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> UTxOState ConwayEra
-> SpecTransM
     (UtxoExecContext ConwayEra) (SpecRep (UTxOState ConwayEra))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep State (EraRule "UTXOW" ConwayEra)
UTxOState ConwayEra
st
            SpecTransM (UtxoExecContext ConwayEra) (Tx -> Text)
-> SpecTransM (UtxoExecContext ConwayEra) Tx
-> SpecTransM (UtxoExecContext ConwayEra) Text
forall a b.
SpecTransM (UtxoExecContext ConwayEra) (a -> b)
-> SpecTransM (UtxoExecContext ConwayEra) a
-> SpecTransM (UtxoExecContext ConwayEra) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Tx ConwayEra
-> SpecTransM (UtxoExecContext ConwayEra) (SpecRep (Tx ConwayEra))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Tx ConwayEra
Signal (EraRule "UTXOW" ConwayEra)
sig
      stFinal :: Either
  Text
  (State (EraRule "UTXO" ConwayEra),
   [Event (EraRule "UTXO" ConwayEra)])
stFinal = (NonEmpty (PredicateFailure (EraRule "UTXO" ConwayEra)) -> Text)
-> Either
     (NonEmpty (PredicateFailure (EraRule "UTXO" ConwayEra)))
     (State (EraRule "UTXO" ConwayEra),
      [Event (EraRule "UTXO" ConwayEra)])
-> Either
     Text
     (State (EraRule "UTXO" ConwayEra),
      [Event (EraRule "UTXO" ConwayEra)])
forall a b c. (a -> b) -> Either a c -> Either b c
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (String -> Text
T.pack (String -> Text)
-> (NonEmpty (ConwayUtxoPredFailure ConwayEra) -> String)
-> NonEmpty (ConwayUtxoPredFailure ConwayEra)
-> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty (ConwayUtxoPredFailure ConwayEra) -> String
forall a. Show a => a -> String
show) (Either
   (NonEmpty (PredicateFailure (EraRule "UTXO" ConwayEra)))
   (State (EraRule "UTXO" ConwayEra),
    [Event (EraRule "UTXO" ConwayEra)])
 -> Either
      Text
      (State (EraRule "UTXO" ConwayEra),
       [Event (EraRule "UTXO" ConwayEra)]))
-> Either
     (NonEmpty (PredicateFailure (EraRule "UTXO" ConwayEra)))
     (State (EraRule "UTXO" ConwayEra),
      [Event (EraRule "UTXO" ConwayEra)])
-> Either
     Text
     (State (EraRule "UTXO" ConwayEra),
      [Event (EraRule "UTXO" ConwayEra)])
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 "UTXO" ConwayEra)
Environment (EraRule "UTXOW" ConwayEra)
env State (EraRule "UTXO" ConwayEra)
State (EraRule "UTXOW" ConwayEra)
st Signal (EraRule "UTXO" ConwayEra)
Signal (EraRule "UTXOW" ConwayEra)
sig
      utxoInfo :: Doc AnsiStyle
utxoInfo = forall (rule :: Symbol) era.
(ExecSpecRule rule era, HasCallStack) =>
Globals
-> ExecContext rule era
-> TRC (EraRule rule era)
-> Either
     Text (State (EraRule rule era), [Event (EraRule rule era)])
-> Doc AnsiStyle
extraInfo @"UTXO" @ConwayEra Globals
globals ExecContext "UTXO" ConwayEra
ExecContext "UTXOW" ConwayEra
ctx (TRC (ConwayUTXOW ConwayEra) -> TRC (ConwayUTXO ConwayEra)
forall a b. Coercible a b => a -> b
coerce TRC (EraRule "UTXOW" ConwayEra)
TRC (ConwayUTXOW ConwayEra)
trc) Either
  Text
  (State (EraRule "UTXO" ConwayEra),
   [Event (EraRule "UTXO" ConwayEra)])
stFinal
     in
      [Doc AnsiStyle] -> Doc AnsiStyle
forall ann. [Doc ann] -> Doc ann
PP.vcat
        [ Doc AnsiStyle
"UTXOW"
        , Doc AnsiStyle
"Impl:"
        , Doc AnsiStyle
"witsVKeyNeeded"
        , String -> Doc AnsiStyle
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty (String -> Doc AnsiStyle)
-> (Set (KeyHash 'Witness) -> String)
-> Set (KeyHash 'Witness)
-> Doc AnsiStyle
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set (KeyHash 'Witness) -> String
forall a. ToExpr a => a -> String
showExpr (Set (KeyHash 'Witness) -> Doc AnsiStyle)
-> Set (KeyHash 'Witness) -> Doc AnsiStyle
forall a b. (a -> b) -> a -> b
$
            forall era.
(EraTx era, ConwayEraTxBody era) =>
UTxO era -> TxBody era -> Set (KeyHash 'Witness)
getConwayWitsVKeyNeeded @ConwayEra (UTxOState ConwayEra -> UTxO ConwayEra
forall era. UTxOState era -> UTxO era
utxosUtxo State (EraRule "UTXOW" ConwayEra)
UTxOState ConwayEra
st) (Tx ConwayEra
Signal (EraRule "UTXOW" ConwayEra)
sig Tx ConwayEra
-> Getting (TxBody ConwayEra) (Tx ConwayEra) (TxBody ConwayEra)
-> TxBody ConwayEra
forall s a. s -> Getting a s a -> a
^. Getting (TxBody ConwayEra) (Tx ConwayEra) (TxBody ConwayEra)
forall era. EraTx era => Lens' (Tx era) (TxBody era)
Lens' (Tx ConwayEra) (TxBody ConwayEra)
bodyTxL)
        , Doc AnsiStyle
"witsVKeyHashes"
        , Doc AnsiStyle
"Spec:"
        , String -> Doc AnsiStyle
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty String
result
        , Doc AnsiStyle
forall a. Monoid a => a
mempty
        , Doc AnsiStyle
"UTXO"
        , Doc AnsiStyle
utxoInfo
        ]