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

instance SpecTranslate ConwayEra (Shelley.ShelleyLedgersEnv ConwayEra) where
  type SpecRep ConwayEra (Shelley.ShelleyLedgersEnv ConwayEra) = Agda.LEnv
  type SpecContext ConwayEra (Shelley.ShelleyLedgersEnv ConwayEra) = EnactState ConwayEra

  toSpecRep :: ShelleyLedgersEnv ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (ShelleyLedgersEnv ConwayEra))
     (SpecRep ConwayEra (ShelleyLedgersEnv ConwayEra))
toSpecRep Shelley.LedgersEnv {PParams ConwayEra
ChainAccountState
EpochNo
SlotNo
ledgersSlotNo :: SlotNo
ledgersEpochNo :: EpochNo
ledgersPp :: PParams ConwayEra
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 <- SpecTransM ConwayEra (EnactState ConwayEra) (EnactState ConwayEra)
forall era ctx. SpecTransM era ctx ctx
askSpecTransM
    let
      guardrailsScriptHash = Constitution ConwayEra -> StrictMaybe ScriptHash
forall era. Constitution era -> StrictMaybe ScriptHash
constitutionGuardrailsScriptHash (Constitution ConwayEra -> StrictMaybe ScriptHash)
-> Constitution ConwayEra -> StrictMaybe ScriptHash
forall a b. (a -> b) -> a -> b
$ EnactState ConwayEra -> Constitution ConwayEra
forall era. EnactState era -> Constitution era
ensConstitution EnactState ConwayEra
enactState
    withCtxSpecTransM () $
      Agda.MkLEnv
        <$> toSpecRep ledgersSlotNo
        <*> toSpecRep guardrailsScriptHash
        <*> toSpecRep ledgersPp
        <*> toSpecRep enactState
        <*> toSpecRep (casTreasury ledgersAccount)