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

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

import Cardano.Ledger.Conway (ConwayEra)
import Cardano.Ledger.Conway.Governance (EnactState)
import Control.State.Transition.Extended (TRC (..))
import qualified MAlonzo.Code.Ledger.Conway.Foreign.API as Agda
import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base (
  externalFunctions,
 )
import Test.Cardano.Ledger.Conformance.ExecSpecRule.Core (
  ExecSpecRule (..),
  SpecTRC (..),
  runFromAgdaFunction,
 )
import Test.Cardano.Ledger.Conformance.SpecTranslate.Base (
  SpecTranslate (..),
  withCtxSpecTransM,
 )
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway ()
import Test.Cardano.Ledger.Conway.ImpTest ()

instance ExecSpecRule "LEDGERS" ConwayEra where
  type ExecContext "LEDGERS" ConwayEra = EnactState ConwayEra

  translateInputs :: HasCallStack =>
TRC (EraRule "LEDGERS" ConwayEra)
-> SpecTransM
     ConwayEra
     (ExecContext "LEDGERS" ConwayEra)
     (SpecTRC "LEDGERS" ConwayEra)
translateInputs (TRC (Environment (EraRule "LEDGERS" ConwayEra)
env, State (EraRule "LEDGERS" ConwayEra)
st, Signal (EraRule "LEDGERS" ConwayEra)
sig)) = do
    agdaEnv <- ShelleyLedgersEnv ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (ShelleyLedgersEnv ConwayEra))
     (SpecRep ConwayEra (ShelleyLedgersEnv ConwayEra))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep ShelleyLedgersEnv ConwayEra
Environment (EraRule "LEDGERS" ConwayEra)
env
    agdaSt <- withCtxSpecTransM () $ toSpecRep st
    agdaSig <- withCtxSpecTransM () $ toSpecRep sig
    pure $ SpecTRC agdaEnv agdaSt agdaSig

  runAgdaRule :: HasCallStack =>
SpecTRC "LEDGERS" ConwayEra
-> Either Text (SpecState "LEDGERS" ConwayEra)
runAgdaRule = (SpecEnvironment "LEDGERS" ConwayEra
 -> SpecState "LEDGERS" ConwayEra
 -> SpecSignal "LEDGERS" ConwayEra
 -> ComputationResult Text (SpecState "LEDGERS" ConwayEra))
-> SpecTRC "LEDGERS" ConwayEra
-> Either Text (SpecState "LEDGERS" 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
-> LEnv -> LState -> [Tx] -> T_HSComputationResult_110 Text LState
Agda.ledgersStep T_ExternalFunctions_8
externalFunctions)