{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

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

import Cardano.Ledger.Alonzo.Tx
import Cardano.Ledger.Binary (EncCBOR (..))
import Cardano.Ledger.Conway (ConwayEra)
import Cardano.Ledger.MempoolTx.Internal (MempoolTx (UnsafeMkMempoolTx))
import Cardano.Ledger.Shelley.Rules (utxoEnvCertStateL)
import Control.State.Transition.Extended (TRC (..))
import Lens.Micro.Extras (view)
import qualified MAlonzo.Code.Ledger.Conway.Foreign.API as Agda
import Test.Cardano.Ledger.Conformance (
  ExecSpecRule (..),
  SpecTRC (..),
  SpecTranslate (..),
  runFromAgdaFunction,
  withCtxSpecTransM,
  withSpecTransM,
 )
import Test.Cardano.Ledger.Conformance.ExecSpecRule.Base (externalFunctions)
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway ()
import Test.Cardano.Ledger.Constrained.Conway (UtxoExecContext (..))
import Test.Cardano.Ledger.Conway.ImpTest ()
import Test.Cardano.Ledger.Generic.Instances ()

instance ExecSpecRule "UTXO" ConwayEra where
  type ExecContext "UTXO" ConwayEra = UtxoExecContext ConwayEra

  translateInputs :: HasCallStack =>
TRC (EraRule "UTXO" ConwayEra)
-> SpecTransM
     ConwayEra (ExecContext "UTXO" ConwayEra) (SpecTRC "UTXO" ConwayEra)
translateInputs (TRC (Environment (EraRule "UTXO" ConwayEra)
env, State (EraRule "UTXO" ConwayEra)
st, Signal (EraRule "UTXO" ConwayEra)
sig)) = do
    agdaEnv <- ()
-> SpecTransM ConwayEra () (SpecRep ConwayEra (UtxoEnv ConwayEra))
-> SpecTransM
     ConwayEra
     (UtxoExecContext ConwayEra)
     (SpecRep ConwayEra (UtxoEnv ConwayEra))
forall ctx era a ctx'.
ctx -> SpecTransM era ctx a -> SpecTransM era ctx' a
withCtxSpecTransM () (SpecTransM ConwayEra () (SpecRep ConwayEra (UtxoEnv ConwayEra))
 -> SpecTransM
      ConwayEra
      (UtxoExecContext ConwayEra)
      (SpecRep ConwayEra (UtxoEnv ConwayEra)))
-> SpecTransM ConwayEra () (SpecRep ConwayEra (UtxoEnv ConwayEra))
-> SpecTransM
     ConwayEra
     (UtxoExecContext ConwayEra)
     (SpecRep ConwayEra (UtxoEnv ConwayEra))
forall a b. (a -> b) -> a -> b
$ UtxoEnv ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (UtxoEnv ConwayEra))
     (SpecRep ConwayEra (UtxoEnv ConwayEra))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep UtxoEnv ConwayEra
Environment (EraRule "UTXO" ConwayEra)
env
    agdaSt <- withSpecTransM (view utxoEnvCertStateL . uecUtxoEnv) $ toSpecRep st
    agdaSig <- withCtxSpecTransM () $ toSpecRep sig
    pure $ SpecTRC agdaEnv agdaSt agdaSig

  translateOutput :: TRC (EraRule "UTXO" ConwayEra)
-> State (EraRule "UTXO" ConwayEra)
-> SpecTransM
     ConwayEra
     (ExecContext "UTXO" ConwayEra)
     (SpecState "UTXO" ConwayEra)
translateOutput TRC (EraRule "UTXO" ConwayEra)
_ =
    (UtxoExecContext ConwayEra -> ConwayCertState ConwayEra)
-> SpecTransM ConwayEra (ConwayCertState ConwayEra) UTxOState
-> SpecTransM ConwayEra (UtxoExecContext ConwayEra) UTxOState
forall ctx ctx' era a.
(ctx -> ctx') -> SpecTransM era ctx' a -> SpecTransM era ctx a
withSpecTransM (Getting
  (ConwayCertState ConwayEra)
  (UtxoEnv ConwayEra)
  (ConwayCertState ConwayEra)
-> UtxoEnv ConwayEra -> ConwayCertState ConwayEra
forall a s. Getting a s a -> s -> a
view (CertState ConwayEra
 -> Const (ConwayCertState ConwayEra) (CertState ConwayEra))
-> UtxoEnv ConwayEra
-> Const (ConwayCertState ConwayEra) (UtxoEnv ConwayEra)
Getting
  (ConwayCertState ConwayEra)
  (UtxoEnv ConwayEra)
  (ConwayCertState ConwayEra)
forall era (f :: * -> *).
Functor f =>
(CertState era -> f (CertState era))
-> UtxoEnv era -> f (UtxoEnv era)
utxoEnvCertStateL (UtxoEnv ConwayEra -> ConwayCertState ConwayEra)
-> (UtxoExecContext ConwayEra -> UtxoEnv ConwayEra)
-> UtxoExecContext ConwayEra
-> ConwayCertState ConwayEra
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UtxoExecContext ConwayEra -> UtxoEnv ConwayEra
forall era. UtxoExecContext era -> UtxoEnv era
uecUtxoEnv) (SpecTransM ConwayEra (ConwayCertState ConwayEra) UTxOState
 -> SpecTransM ConwayEra (UtxoExecContext ConwayEra) UTxOState)
-> (UTxOState ConwayEra
    -> SpecTransM ConwayEra (ConwayCertState ConwayEra) UTxOState)
-> UTxOState ConwayEra
-> SpecTransM ConwayEra (UtxoExecContext ConwayEra) UTxOState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UTxOState ConwayEra
-> SpecTransM ConwayEra (ConwayCertState ConwayEra) UTxOState
UTxOState ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (UTxOState ConwayEra))
     (SpecRep ConwayEra (UTxOState ConwayEra))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep

  runAgdaRule :: HasCallStack =>
SpecTRC "UTXO" ConwayEra
-> Either Text (SpecState "UTXO" ConwayEra)
runAgdaRule = (SpecEnvironment "UTXO" ConwayEra
 -> SpecState "UTXO" ConwayEra
 -> SpecSignal "UTXO" ConwayEra
 -> ComputationResult Text (SpecState "UTXO" ConwayEra))
-> SpecTRC "UTXO" ConwayEra
-> Either Text (SpecState "UTXO" 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_HSComputationResult_110 Text UTxOState
Agda.utxoStep T_ExternalFunctions_8
externalFunctions)

-- | The transaction is serialized in its mempool format.
instance EncCBOR (MempoolTx era) => EncCBOR (AlonzoStAnnTx l era) where
  encCBOR :: AlonzoStAnnTx l era -> Encoding
encCBOR AlonzoStAnnTx {Tx TopTx era
asatTx :: Tx TopTx era
asatTx :: forall era. AlonzoStAnnTx TopTx era -> Tx TopTx era
asatTx} = MempoolTx era -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR (Tx TopTx era -> MempoolTx era
forall era. Tx TopTx era -> MempoolTx era
UnsafeMkMempoolTx Tx TopTx era
asatTx)