{-# 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 (Era (..), 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)
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 (EraCrypto era)))
  , 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
PParams era
TxIx
SlotNo
AccountState
ledgerSlotNo :: forall era. LedgerEnv era -> SlotNo
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
ledgerSlotNo :: SlotNo
..} = do
    StrictMaybe (ScriptHash (EraCrypto era))
policyHash <- forall b ctx. Inject ctx b => SpecTransM ctx b
askCtx @(StrictMaybe (ScriptHash (EraCrypto era)))
    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 (EraCrypto era))
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 ConwayLedgerPredFailure era
e = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> OpaqueErrorString
OpaqueErrorString forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ forall a. ToExpr a => a -> Expr
toExpr ConwayLedgerPredFailure era
e