{-# 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 (..))
import Cardano.Ledger.Conway.Governance (Constitution (..), EnactState (..))
import Cardano.Ledger.Shelley.Rules (Identity, ShelleyLedgersEnv (..))
import Cardano.Ledger.Shelley.State (ChainAccountState (..))
import qualified MAlonzo.Code.Ledger.Foreign.API as Agda
import Test.Cardano.Ledger.Conformance (
  SpecTranslate (..),
  askCtx,
 )
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base ()

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