{-# 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.Ledgers () where

import Cardano.Ledger.BaseTypes (Inject)
import Cardano.Ledger.Conway.Core (EraPParams (..), EraRule)
import Cardano.Ledger.Conway.Governance (Constitution (..), EnactState (..))
import Cardano.Ledger.Shelley.LedgerState (AccountState (..))
import Cardano.Ledger.Shelley.Rules (Identity, ShelleyLedgersEnv (..), ShelleyLedgersPredFailure)
import Control.State.Transition.Extended (STS (..))
import qualified Lib as Agda
import Test.Cardano.Ledger.Conformance (OpaqueErrorString (..), SpecTranslate (..), askCtx)
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base ()
import Test.Cardano.Ledger.Conway.TreeDiff (ToExpr, showExpr)

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

  toSpecRep :: ShelleyLedgersEnv era
-> SpecTransM ctx (SpecRep (ShelleyLedgersEnv era))
toSpecRep LedgersEnv {PParams era
EpochNo
SlotNo
AccountState
ledgersSlotNo :: forall era. ShelleyLedgersEnv era -> SlotNo
ledgersEpochNo :: forall era. ShelleyLedgersEnv era -> EpochNo
ledgersPp :: forall era. ShelleyLedgersEnv era -> PParams era
ledgersAccount :: forall era. ShelleyLedgersEnv era -> AccountState
ledgersAccount :: AccountState
ledgersPp :: PParams era
ledgersEpochNo :: EpochNo
ledgersSlotNo :: SlotNo
..} = do
    EnactState era
enactState <- forall b ctx. Inject ctx b => SpecTransM ctx b
askCtx @(EnactState era)
    let
      pPolicy :: StrictMaybe (ScriptHash (EraCrypto era))
pPolicy = forall era.
Constitution era -> StrictMaybe (ScriptHash (EraCrypto era))
constitutionScript forall a b. (a -> b) -> a -> b
$ forall era. EnactState era -> Constitution era
ensConstitution EnactState era
enactState
    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
ledgersSlotNo
      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))
pPolicy
      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
ledgersPp
      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
ledgersAccount)

instance
  ToExpr (PredicateFailure (EraRule "LEDGER" era)) =>
  SpecTranslate ctx (ShelleyLedgersPredFailure era)
  where
  type SpecRep (ShelleyLedgersPredFailure era) = OpaqueErrorString

  toSpecRep :: ShelleyLedgersPredFailure era
-> SpecTransM ctx (SpecRep (ShelleyLedgersPredFailure era))
toSpecRep = 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. ToExpr a => a -> String
showExpr