{-# LANGUAGE AllowAmbiguousTypes #-}
{-# 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.Ledger () where

import Cardano.Ledger.BaseTypes (Inject)
import Cardano.Ledger.Conway (ConwayEra)
import Cardano.Ledger.Conway.Core (
  AllegraEraTxBody (..),
  AlonzoEraTx (..),
  AlonzoEraTxBody (..),
  BabbageEraTxBody (..),
  ConwayEraTxBody (..),
  EraPParams (..),
  EraTx (..),
  EraTxBody (..),
  ScriptHash,
  TxLevel (..),
  txIdTx,
 )
import Cardano.Ledger.Conway.Rules (EnactState)
import Cardano.Ledger.Shelley.Rules (LedgerEnv (..))
import Cardano.Ledger.Shelley.State (ChainAccountState (..))
import Cardano.Ledger.TxIn (TxId)
import Data.Functor.Identity (Identity)
import Data.Maybe.Strict (StrictMaybe)
import Lens.Micro ((^.))
import qualified MAlonzo.Code.Ledger.Foreign.API as Agda
import Test.Cardano.Ledger.Conformance (askCtx, withCtx)
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base (
  SpecTranslate (..),
 )
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Cert ()

instance
  ( EraPParams era
  , SpecTranslate ctx (PParamsHKD Identity era)
  , SpecRep (PParamsHKD Identity era) ~ Agda.PParams
  , Inject ctx (StrictMaybe ScriptHash)
  , Inject ctx (EnactState era)
  ) =>
  SpecTranslate ctx (LedgerEnv era)
  where
  type SpecRep (LedgerEnv era) = Agda.LEnv

  toSpecRep :: LedgerEnv era -> SpecTransM ctx (SpecRep (LedgerEnv era))
toSpecRep LedgerEnv {Maybe EpochNo
PParams era
ChainAccountState
TxIx
SlotNo
ledgerSlotNo :: SlotNo
ledgerEpochNo :: Maybe EpochNo
ledgerIx :: TxIx
ledgerPp :: PParams era
ledgerAccount :: ChainAccountState
ledgerAccount :: forall era. LedgerEnv era -> ChainAccountState
ledgerPp :: forall era. LedgerEnv era -> PParams era
ledgerIx :: forall era. LedgerEnv era -> TxIx
ledgerEpochNo :: forall era. LedgerEnv era -> Maybe EpochNo
ledgerSlotNo :: forall era. LedgerEnv era -> SlotNo
..} = do
    policyHash <- forall b ctx. Inject ctx b => SpecTransM ctx b
askCtx @(StrictMaybe ScriptHash)
    enactState <- askCtx @(EnactState era)
    Agda.MkLEnv
      <$> toSpecRep ledgerSlotNo
      <*> toSpecRep policyHash
      <*> toSpecRep ledgerPp
      <*> toSpecRep enactState
      <*> toSpecRep (casTreasury ledgerAccount)

instance
  Inject ctx TxId =>
  SpecTranslate ctx (TxBody TopTx ConwayEra)
  where
  type SpecRep (TxBody TopTx ConwayEra) = Agda.TxBody

  toSpecRep :: TxBody TopTx ConwayEra
-> SpecTransM ctx (SpecRep (TxBody TopTx ConwayEra))
toSpecRep TxBody TopTx ConwayEra
txb = do
    txId <- forall b ctx. Inject ctx b => SpecTransM ctx b
askCtx @TxId
    Agda.MkTxBody
      <$> toSpecRep (txb ^. inputsTxBodyL)
      <*> toSpecRep (txb ^. referenceInputsTxBodyL)
      <*> toSpecRep (txb ^. collateralInputsTxBodyL)
      <*> (Agda.MkHSMap . zip [0 ..] <$> toSpecRep (txb ^. outputsTxBodyL))
      <*> toSpecRep txId
      <*> toSpecRep (txb ^. certsTxBodyL)
      <*> toSpecRep (txb ^. feeTxBodyL)
      <*> toSpecRep (txb ^. withdrawalsTxBodyL)
      <*> toSpecRep (txb ^. vldtTxBodyL)
      <*> toSpecRep (txb ^. auxDataHashTxBodyL)
      <*> toSpecRep (txb ^. treasuryDonationTxBodyL)
      <*> toSpecRep (txb ^. votingProceduresTxBodyL)
      <*> toSpecRep (txb ^. proposalProceduresTxBodyL)
      <*> toSpecRep (txb ^. networkIdTxBodyL)
      <*> toSpecRep (txb ^. currentTreasuryValueTxBodyL)
      <*> pure 0
      <*> toSpecRep (txb ^. reqSignerHashesTxBodyL)
      -- The script integrity hash is computed using @const 0@ on the Agda
      -- side (@Hashable-ScriptIntegrity = record { hash = λ x → 0 }@).
      -- Until a proper hash function is used in Agda, we emulate the same
      -- behavior here.
      --
      -- The following PR documents the discrepancy on the Agda side:
      -- https://github.com/IntersectMBO/formal-ledger-specifications/issues/1086
      <*> fmap (fmap (const 0)) (toSpecRep (txb ^. scriptIntegrityHashTxBodyL))

instance SpecTranslate ctx (Tx TopTx ConwayEra) where
  type SpecRep (Tx TopTx ConwayEra) = Agda.Tx

  toSpecRep :: Tx TopTx ConwayEra -> SpecTransM ctx (SpecRep (Tx TopTx ConwayEra))
toSpecRep Tx TopTx ConwayEra
tx =
    TxBody -> TxWitnesses -> Integer -> Bool -> Maybe Integer -> Tx
Agda.MkTx
      (TxBody -> TxWitnesses -> Integer -> Bool -> Maybe Integer -> Tx)
-> SpecTransM ctx TxBody
-> SpecTransM
     ctx (TxWitnesses -> Integer -> Bool -> Maybe Integer -> Tx)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TxId -> SpecTransM TxId TxBody -> SpecTransM ctx TxBody
forall ctx a ctx'. ctx -> SpecTransM ctx a -> SpecTransM ctx' a
withCtx (Tx TopTx ConwayEra -> TxId
forall era (l :: TxLevel). EraTx era => Tx l era -> TxId
txIdTx Tx TopTx ConwayEra
tx) (TxBody TopTx ConwayEra
-> SpecTransM TxId (SpecRep (TxBody TopTx ConwayEra))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (Tx TopTx ConwayEra
tx Tx TopTx ConwayEra
-> Getting
     (TxBody TopTx ConwayEra)
     (Tx TopTx ConwayEra)
     (TxBody TopTx ConwayEra)
-> TxBody TopTx ConwayEra
forall s a. s -> Getting a s a -> a
^. Getting
  (TxBody TopTx ConwayEra)
  (Tx TopTx ConwayEra)
  (TxBody TopTx ConwayEra)
forall era (l :: TxLevel).
EraTx era =>
Lens' (Tx l era) (TxBody l era)
forall (l :: TxLevel). Lens' (Tx l ConwayEra) (TxBody l ConwayEra)
bodyTxL))
      SpecTransM
  ctx (TxWitnesses -> Integer -> Bool -> Maybe Integer -> Tx)
-> SpecTransM ctx TxWitnesses
-> SpecTransM ctx (Integer -> Bool -> Maybe Integer -> Tx)
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
<*> AlonzoTxWits ConwayEra
-> SpecTransM ctx (SpecRep (AlonzoTxWits ConwayEra))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (Tx TopTx ConwayEra
tx Tx TopTx ConwayEra
-> Getting
     (AlonzoTxWits ConwayEra)
     (Tx TopTx ConwayEra)
     (AlonzoTxWits ConwayEra)
-> AlonzoTxWits ConwayEra
forall s a. s -> Getting a s a -> a
^. (TxWits ConwayEra
 -> Const (AlonzoTxWits ConwayEra) (TxWits ConwayEra))
-> Tx TopTx ConwayEra
-> Const (AlonzoTxWits ConwayEra) (Tx TopTx ConwayEra)
Getting
  (AlonzoTxWits ConwayEra)
  (Tx TopTx ConwayEra)
  (AlonzoTxWits ConwayEra)
forall era (l :: TxLevel).
EraTx era =>
Lens' (Tx l era) (TxWits era)
forall (l :: TxLevel). Lens' (Tx l ConwayEra) (TxWits ConwayEra)
witsTxL)
      SpecTransM ctx (Integer -> Bool -> Maybe Integer -> Tx)
-> SpecTransM ctx Integer
-> SpecTransM ctx (Bool -> Maybe Integer -> Tx)
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
<*> Word32 -> SpecTransM ctx (SpecRep Word32)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (Tx TopTx ConwayEra
tx Tx TopTx ConwayEra
-> Getting Word32 (Tx TopTx ConwayEra) Word32 -> Word32
forall s a. s -> Getting a s a -> a
^. Getting Word32 (Tx TopTx ConwayEra) Word32
forall era (l :: TxLevel).
(EraTx era, HasCallStack) =>
SimpleGetter (Tx l era) Word32
SimpleGetter (Tx TopTx ConwayEra) Word32
forall (l :: TxLevel).
HasCallStack =>
SimpleGetter (Tx l ConwayEra) Word32
sizeTxF)
      SpecTransM ctx (Bool -> Maybe Integer -> Tx)
-> SpecTransM ctx Bool -> SpecTransM ctx (Maybe Integer -> Tx)
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
<*> IsValid -> SpecTransM ctx (SpecRep IsValid)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (Tx TopTx ConwayEra
tx Tx TopTx ConwayEra
-> Getting IsValid (Tx TopTx ConwayEra) IsValid -> IsValid
forall s a. s -> Getting a s a -> a
^. Getting IsValid (Tx TopTx ConwayEra) IsValid
forall era. AlonzoEraTx era => Lens' (Tx TopTx era) IsValid
Lens' (Tx TopTx ConwayEra) IsValid
isValidTxL)
      SpecTransM ctx (Maybe Integer -> Tx)
-> SpecTransM ctx (Maybe Integer) -> SpecTransM ctx Tx
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 (AlonzoTxAuxData ConwayEra)
-> SpecTransM
     ctx (SpecRep (StrictMaybe (AlonzoTxAuxData ConwayEra)))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (Tx TopTx ConwayEra
tx Tx TopTx ConwayEra
-> Getting
     (StrictMaybe (AlonzoTxAuxData ConwayEra))
     (Tx TopTx ConwayEra)
     (StrictMaybe (AlonzoTxAuxData ConwayEra))
-> StrictMaybe (AlonzoTxAuxData ConwayEra)
forall s a. s -> Getting a s a -> a
^. (StrictMaybe (TxAuxData ConwayEra)
 -> Const
      (StrictMaybe (AlonzoTxAuxData ConwayEra))
      (StrictMaybe (TxAuxData ConwayEra)))
-> Tx TopTx ConwayEra
-> Const
     (StrictMaybe (AlonzoTxAuxData ConwayEra)) (Tx TopTx ConwayEra)
Getting
  (StrictMaybe (AlonzoTxAuxData ConwayEra))
  (Tx TopTx ConwayEra)
  (StrictMaybe (AlonzoTxAuxData ConwayEra))
forall era (l :: TxLevel).
EraTx era =>
Lens' (Tx l era) (StrictMaybe (TxAuxData era))
forall (l :: TxLevel).
Lens' (Tx l ConwayEra) (StrictMaybe (TxAuxData ConwayEra))
auxDataTxL)