{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NumericUnderscores #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# 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 (ConwayEra)
import qualified Cardano.Ledger.Shelley.Rules as Shelley
import qualified MAlonzo.Code.Ledger.Conway.Foreign.API as Agda
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base (SpecTranslate (..))
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Cert ()

instance SpecTranslate ConwayEra (Shelley.UtxoEnv ConwayEra) where
  type SpecRep ConwayEra (Shelley.UtxoEnv ConwayEra) = Agda.UTxOEnv

  toSpecRep :: UtxoEnv ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (UtxoEnv ConwayEra))
     (SpecRep ConwayEra (UtxoEnv ConwayEra))
toSpecRep UtxoEnv ConwayEra
x =
    Integer -> PParams -> Integer -> UTxOEnv
Agda.MkUTxOEnv
      (Integer -> PParams -> Integer -> UTxOEnv)
-> SpecTransM ConwayEra () Integer
-> SpecTransM ConwayEra () (PParams -> Integer -> UTxOEnv)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SlotNo
-> SpecTransM
     ConwayEra (SpecContext ConwayEra SlotNo) (SpecRep ConwayEra SlotNo)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep (UtxoEnv ConwayEra -> SlotNo
forall era. UtxoEnv era -> SlotNo
Shelley.ueSlot UtxoEnv ConwayEra
x)
      SpecTransM ConwayEra () (PParams -> Integer -> UTxOEnv)
-> SpecTransM ConwayEra () PParams
-> SpecTransM ConwayEra () (Integer -> UTxOEnv)
forall a b.
SpecTransM ConwayEra () (a -> b)
-> SpecTransM ConwayEra () a -> SpecTransM ConwayEra () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> PParams ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (PParams ConwayEra))
     (SpecRep ConwayEra (PParams ConwayEra))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep (UtxoEnv ConwayEra -> PParams ConwayEra
forall era. UtxoEnv era -> PParams era
Shelley.uePParams UtxoEnv ConwayEra
x)
      SpecTransM ConwayEra () (Integer -> UTxOEnv)
-> SpecTransM ConwayEra () Integer
-> SpecTransM ConwayEra () UTxOEnv
forall a b.
SpecTransM ConwayEra () (a -> b)
-> SpecTransM ConwayEra () a -> SpecTransM ConwayEra () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Coin
-> SpecTransM
     ConwayEra (SpecContext ConwayEra Coin) (SpecRep ConwayEra Coin)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep (Integer -> Coin
Coin Integer
10_000_000) -- TODO: Fix generating types