{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NumericUnderscores #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Utxo () where

import Cardano.Ledger.Coin (Coin (..))
import Cardano.Ledger.Conway.Core (EraPParams (..), EraRule, PParams, Value)
import Cardano.Ledger.Conway.Rules (ConwayUtxoPredFailure)
import Cardano.Ledger.Core (EraTxOut (..))
import Cardano.Ledger.Shelley.Rules (UtxoEnv (..))
import Control.State.Transition.Extended (STS (..))
import Data.Functor.Identity (Identity)
import qualified MAlonzo.Code.Ledger.Foreign.API as Agda
import Test.Cardano.Ledger.Conformance (OpaqueErrorString (..), showOpaqueErrorString)
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base (SpecTranslate (..))
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Cert ()
import Test.Cardano.Ledger.Conway.TreeDiff (ToExpr (..))

instance
  ( SpecRep (PParams era) ~ Agda.PParams
  , SpecTranslate ctx (PParamsHKD Identity era)
  ) =>
  SpecTranslate ctx (UtxoEnv era)
  where
  type SpecRep (UtxoEnv era) = Agda.UTxOEnv

  toSpecRep :: UtxoEnv era -> SpecTransM ctx (SpecRep (UtxoEnv era))
toSpecRep UtxoEnv era
x =
    Integer -> PParams -> Integer -> UTxOEnv
Agda.MkUTxOEnv
      (Integer -> PParams -> Integer -> UTxOEnv)
-> SpecTransM ctx Integer
-> SpecTransM ctx (PParams -> Integer -> UTxOEnv)
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 (UtxoEnv era -> SlotNo
forall era. UtxoEnv era -> SlotNo
ueSlot UtxoEnv era
x)
      SpecTransM ctx (PParams -> Integer -> UTxOEnv)
-> SpecTransM ctx PParams -> SpecTransM ctx (Integer -> UTxOEnv)
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 (UtxoEnv era -> PParams era
forall era. UtxoEnv era -> PParams era
uePParams UtxoEnv era
x)
      SpecTransM ctx (Integer -> UTxOEnv)
-> SpecTransM ctx Integer -> SpecTransM ctx UTxOEnv
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 (Integer -> Coin
Coin Integer
10_000_000) -- TODO: Fix generating types

instance
  ( ToExpr (Value era)
  , ToExpr (TxOut era)
  , ToExpr (PredicateFailure (EraRule "UTXOS" era))
  ) =>
  SpecTranslate ctx (ConwayUtxoPredFailure era)
  where
  type SpecRep (ConwayUtxoPredFailure era) = OpaqueErrorString

  toSpecRep :: ConwayUtxoPredFailure era
-> SpecTransM ctx (SpecRep (ConwayUtxoPredFailure 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)
-> (ConwayUtxoPredFailure era -> OpaqueErrorString)
-> ConwayUtxoPredFailure era
-> SpecTransM ctx OpaqueErrorString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConwayUtxoPredFailure era -> OpaqueErrorString
forall a. ToExpr a => a -> OpaqueErrorString
showOpaqueErrorString