{-# 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.Core (EraPParams (..))
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.Foreign.API as Agda
import Test.Cardano.Ledger.Conformance (
  SpecTranslate (..),
  askSpecTransM,
  withCtxSpecTransM,
 )
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base ()

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

  toSpecRep :: ShelleyLedgersEnv era
-> SpecTransM
     (SpecContext (ShelleyLedgersEnv era))
     (SpecRep (ShelleyLedgersEnv era))
toSpecRep Shelley.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 <- SpecTransM (EnactState era) (EnactState era)
forall ctx. SpecTransM ctx ctx
askSpecTransM
    let
      guardrailsScriptHash = Constitution era -> StrictMaybe ScriptHash
forall era. Constitution era -> StrictMaybe ScriptHash
constitutionGuardrailsScriptHash (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
    withCtxSpecTransM () $
      Agda.MkLEnv
        <$> toSpecRep ledgersSlotNo
        <*> toSpecRep guardrailsScriptHash
        <*> toSpecRep ledgersPp
        <*> toSpecRep enactState
        <*> toSpecRep (casTreasury ledgersAccount)