{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

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

import Cardano.Ledger.Dijkstra (DijkstraEra)
import Cardano.Ledger.Shelley.LedgerState (UTxOState (..))
import qualified MAlonzo.Code.Ledger.Dijkstra.Foreign.API as Agda
import Test.Cardano.Ledger.Conformance.SpecTranslate.Base (
  SpecTranslate (..),
 )
import Test.Cardano.Ledger.Conformance.SpecTranslate.Dijkstra.Base ()

instance SpecTranslate DijkstraEra (UTxOState DijkstraEra) where
  type SpecRep DijkstraEra (UTxOState DijkstraEra) = Agda.UTxOState

  toSpecRep :: UTxOState DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (UTxOState DijkstraEra))
     (SpecRep DijkstraEra (UTxOState DijkstraEra))
toSpecRep UTxOState {GovState DijkstraEra
InstantStake DijkstraEra
UTxO DijkstraEra
Coin
utxosUtxo :: UTxO DijkstraEra
utxosDeposited :: Coin
utxosFees :: Coin
utxosGovState :: GovState DijkstraEra
utxosInstantStake :: InstantStake DijkstraEra
utxosDonation :: Coin
utxosDonation :: forall era. UTxOState era -> Coin
utxosInstantStake :: forall era. UTxOState era -> InstantStake era
utxosGovState :: forall era. UTxOState era -> GovState era
utxosFees :: forall era. UTxOState era -> Coin
utxosDeposited :: forall era. UTxOState era -> Coin
utxosUtxo :: forall era. UTxOState era -> UTxO era
..} =
    HSMap
  (Integer, Integer)
  (Either BaseAddr BootstrapAddr,
   (Integer,
    (Maybe (Either Integer Integer),
     Maybe (Either HSNativeScript HSPlutusScript))))
-> Integer -> Integer -> UTxOState
Agda.MkUTxOState
      (HSMap
   (Integer, Integer)
   (Either BaseAddr BootstrapAddr,
    (Integer,
     (Maybe (Either Integer Integer),
      Maybe (Either HSNativeScript HSPlutusScript))))
 -> Integer -> Integer -> UTxOState)
-> SpecTransM
     DijkstraEra
     ()
     (HSMap
        (Integer, Integer)
        (Either BaseAddr BootstrapAddr,
         (Integer,
          (Maybe (Either Integer Integer),
           Maybe (Either HSNativeScript HSPlutusScript)))))
-> SpecTransM DijkstraEra () (Integer -> Integer -> UTxOState)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UTxO DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (UTxO DijkstraEra))
     (SpecRep DijkstraEra (UTxO DijkstraEra))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep UTxO DijkstraEra
utxosUtxo
      SpecTransM DijkstraEra () (Integer -> Integer -> UTxOState)
-> SpecTransM DijkstraEra () Integer
-> SpecTransM DijkstraEra () (Integer -> UTxOState)
forall a b.
SpecTransM DijkstraEra () (a -> b)
-> SpecTransM DijkstraEra () a -> SpecTransM DijkstraEra () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Coin
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra Coin)
     (SpecRep DijkstraEra Coin)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep Coin
utxosFees
      SpecTransM DijkstraEra () (Integer -> UTxOState)
-> SpecTransM DijkstraEra () Integer
-> SpecTransM DijkstraEra () UTxOState
forall a b.
SpecTransM DijkstraEra () (a -> b)
-> SpecTransM DijkstraEra () a -> SpecTransM DijkstraEra () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Coin
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra Coin)
     (SpecRep DijkstraEra Coin)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep Coin
utxosDonation