{-# 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 (..), PParams)
import Cardano.Ledger.Shelley.Rules (UtxoEnv (..))
import Data.Functor.Identity (Identity)
import qualified MAlonzo.Code.Ledger.Foreign.API as Agda
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base (SpecTranslate (..))
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Cert ()

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