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

module Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Ledger () where

import Cardano.Ledger.BaseTypes (Inject)
import Cardano.Ledger.Conway.Core (EraPParams (..), EraRule, ScriptHash)
import Cardano.Ledger.Conway.Rules (ConwayLedgerPredFailure, EnactState)
import Cardano.Ledger.Shelley.LedgerState (AccountState (..))
import Cardano.Ledger.Shelley.Rules (LedgerEnv (..))
import Control.State.Transition.Extended (STS (..))
import Data.Functor.Identity (Identity)
import Data.Maybe.Strict (StrictMaybe)
import qualified Lib as Agda
import Test.Cardano.Ledger.Conformance (OpaqueErrorString (..), askCtx, showOpaqueErrorString)
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base (SpecTranslate (..))
import Test.Cardano.Ledger.Conway.TreeDiff (ToExpr (..))

instance
  ( EraPParams era
  , SpecTranslate ctx (PParamsHKD Identity era)
  , SpecRep (PParamsHKD Identity era) ~ Agda.PParams
  , Inject ctx (StrictMaybe ScriptHash)
  , Inject ctx (EnactState era)
  ) =>
  SpecTranslate ctx (LedgerEnv era)
  where
  type SpecRep (LedgerEnv era) = Agda.LEnv

  toSpecRep :: LedgerEnv era -> SpecTransM ctx (SpecRep (LedgerEnv era))
toSpecRep LedgerEnv {Bool
Maybe EpochNo
PParams era
TxIx
SlotNo
AccountState
ledgerSlotNo :: forall era. LedgerEnv era -> SlotNo
ledgerEpochNo :: forall era. LedgerEnv era -> Maybe EpochNo
ledgerIx :: forall era. LedgerEnv era -> TxIx
ledgerPp :: forall era. LedgerEnv era -> PParams era
ledgerAccount :: forall era. LedgerEnv era -> AccountState
ledgerMempool :: forall era. LedgerEnv era -> Bool
ledgerMempool :: Bool
ledgerAccount :: AccountState
ledgerPp :: PParams era
ledgerIx :: TxIx
ledgerEpochNo :: Maybe EpochNo
ledgerSlotNo :: SlotNo
..} = do
    StrictMaybe ScriptHash
policyHash <- forall b ctx. Inject ctx b => SpecTransM ctx b
askCtx @(StrictMaybe ScriptHash)
    EnactState era
enactState <- forall b ctx. Inject ctx b => SpecTransM ctx b
askCtx @(EnactState era)
    Integer
-> Maybe Integer -> PParams -> EnactState -> Integer -> LEnv
Agda.MkLEnv
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep SlotNo
ledgerSlotNo
      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 StrictMaybe ScriptHash
policyHash
      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 PParams era
ledgerPp
      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 EnactState era
enactState
      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 (AccountState -> Coin
asTreasury AccountState
ledgerAccount)

instance
  ( ToExpr (PredicateFailure (EraRule "GOV" era))
  , ToExpr (PredicateFailure (EraRule "CERTS" era))
  , ToExpr (PredicateFailure (EraRule "UTXOW" era))
  ) =>
  SpecTranslate ctx (ConwayLedgerPredFailure era)
  where
  type SpecRep (ConwayLedgerPredFailure era) = OpaqueErrorString

  toSpecRep :: ConwayLedgerPredFailure era
-> SpecTransM ctx (SpecRep (ConwayLedgerPredFailure era))
toSpecRep = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. ToExpr a => a -> OpaqueErrorString
showOpaqueErrorString