{-# 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.Rules (Identity, ShelleyLedgersEnv (..), ShelleyLedgersPredFailure)
import Cardano.Ledger.Shelley.State (ChainAccountState (..))
import Control.State.Transition.Extended (STS (..))
import qualified MAlonzo.Code.Ledger.Foreign.API as Agda
import Test.Cardano.Ledger.Conformance (
  OpaqueErrorString (..),
  SpecTranslate (..),
  askCtx,
  showOpaqueErrorString,
 )
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base ()
import Test.Cardano.Ledger.Conway.TreeDiff (ToExpr)

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
ledgersSlotNo :: forall era. ShelleyLedgersEnv era -> SlotNo
ledgersEpochNo :: forall era. ShelleyLedgersEnv era -> EpochNo
ledgersPp :: forall era. ShelleyLedgersEnv era -> PParams era
ledgersAccount :: forall era. ShelleyLedgersEnv era -> ChainAccountState
..} = do
    EnactState era
enactState <- forall b ctx. Inject ctx b => SpecTransM ctx b
askCtx @(EnactState era)
    let
      pPolicy :: StrictMaybe ScriptHash
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
    Integer
-> Maybe Integer -> PParams -> EnactState -> Integer -> LEnv
Agda.MkLEnv
      (Integer
 -> Maybe Integer -> PParams -> EnactState -> Integer -> LEnv)
-> SpecTransM ctx Integer
-> SpecTransM
     ctx (Maybe Integer -> PParams -> EnactState -> Integer -> LEnv)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SlotNo -> SpecTransM ctx (SpecRep SlotNo)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep SlotNo
ledgersSlotNo
      SpecTransM
  ctx (Maybe Integer -> PParams -> EnactState -> Integer -> LEnv)
-> SpecTransM ctx (Maybe Integer)
-> SpecTransM ctx (PParams -> EnactState -> Integer -> LEnv)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StrictMaybe ScriptHash
-> SpecTransM ctx (SpecRep (StrictMaybe ScriptHash))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep StrictMaybe ScriptHash
pPolicy
      SpecTransM ctx (PParams -> EnactState -> Integer -> LEnv)
-> SpecTransM ctx PParams
-> SpecTransM ctx (EnactState -> Integer -> LEnv)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> PParams era -> SpecTransM ctx (SpecRep (PParams era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep PParams era
ledgersPp
      SpecTransM ctx (EnactState -> Integer -> LEnv)
-> SpecTransM ctx EnactState -> SpecTransM ctx (Integer -> LEnv)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> EnactState era -> SpecTransM ctx (SpecRep (EnactState era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep EnactState era
enactState
      SpecTransM ctx (Integer -> LEnv)
-> SpecTransM ctx Integer -> SpecTransM ctx LEnv
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Coin -> SpecTransM ctx (SpecRep Coin)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (ChainAccountState -> Coin
casTreasury ChainAccountState
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 = OpaqueErrorString -> SpecTransM ctx OpaqueErrorString
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (OpaqueErrorString -> SpecTransM ctx OpaqueErrorString)
-> (ShelleyLedgersPredFailure era -> OpaqueErrorString)
-> ShelleyLedgersPredFailure era
-> SpecTransM ctx OpaqueErrorString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShelleyLedgersPredFailure era -> OpaqueErrorString
forall a. ToExpr a => a -> OpaqueErrorString
showOpaqueErrorString