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

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

import Cardano.Ledger.Conway (ConwayEra)
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.Conway.Base (externalFunctions)
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Cert ()
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Utxo ()
import Test.Cardano.Ledger.Constrained.Conway (UtxoExecContext (..))
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)