{-# 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,
  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
ledgerSlotNo :: forall era. LedgerEnv era -> SlotNo
ledgerEpochNo :: forall era. LedgerEnv era -> Maybe EpochNo
ledgerIx :: forall era. LedgerEnv era -> TxIx
ledgerPp :: forall era. LedgerEnv era -> PParams era
ledgerAccount :: forall era. LedgerEnv era -> ChainAccountState
..} = do
    StrictMaybe ScriptHash
policyHash <- forall b ctx. Inject ctx b => SpecTransM ctx b
askCtx @(StrictMaybe ScriptHash)
    EnactState era
enactState <- forall b ctx. Inject ctx b => SpecTransM ctx b
askCtx @(EnactState era)
    Integer
-> Maybe Integer -> PParams -> EnactState -> Integer -> LEnv
Agda.MkLEnv
      (Integer
 -> Maybe Integer -> PParams -> EnactState -> Integer -> LEnv)
-> SpecTransM ctx Integer
-> SpecTransM
     ctx (Maybe Integer -> PParams -> EnactState -> Integer -> LEnv)
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 SlotNo
ledgerSlotNo
      SpecTransM
  ctx (Maybe Integer -> PParams -> EnactState -> Integer -> LEnv)
-> SpecTransM ctx (Maybe Integer)
-> SpecTransM ctx (PParams -> EnactState -> Integer -> LEnv)
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 ScriptHash
-> SpecTransM ctx (SpecRep (StrictMaybe ScriptHash))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep StrictMaybe ScriptHash
policyHash
      SpecTransM ctx (PParams -> EnactState -> Integer -> LEnv)
-> SpecTransM ctx PParams
-> SpecTransM ctx (EnactState -> Integer -> LEnv)
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 PParams era
ledgerPp
      SpecTransM ctx (EnactState -> Integer -> LEnv)
-> SpecTransM ctx EnactState -> SpecTransM ctx (Integer -> LEnv)
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
<*> EnactState era -> SpecTransM ctx (SpecRep (EnactState era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep EnactState era
enactState
      SpecTransM ctx (Integer -> LEnv)
-> SpecTransM ctx Integer -> SpecTransM ctx LEnv
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 (ChainAccountState -> Coin
casTreasury ChainAccountState
ledgerAccount)

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

  toSpecRep :: TxBody ConwayEra -> SpecTransM ctx (SpecRep (TxBody ConwayEra))
toSpecRep TxBody ConwayEra
txb = do
    TxId
txId <- forall b ctx. Inject ctx b => SpecTransM ctx b
askCtx @TxId
    HSSet (Integer, Integer)
-> HSSet (Integer, Integer)
-> HSSet (Integer, Integer)
-> HSMap
     Integer
     (Either BaseAddr BootstrapAddr,
      (Integer,
       (Maybe (Either Integer Integer),
        Maybe (Either HSTimelock HSPlutusScript))))
-> Integer
-> [DCert]
-> Integer
-> HSMap RwdAddr Integer
-> (Maybe Integer, Maybe Integer)
-> Maybe Integer
-> Integer
-> [GovVote]
-> [GovProposal]
-> Maybe Integer
-> Maybe Integer
-> Integer
-> HSSet Integer
-> Maybe Integer
-> TxBody
Agda.MkTxBody
      (HSSet (Integer, Integer)
 -> HSSet (Integer, Integer)
 -> HSSet (Integer, Integer)
 -> HSMap
      Integer
      (Either BaseAddr BootstrapAddr,
       (Integer,
        (Maybe (Either Integer Integer),
         Maybe (Either HSTimelock HSPlutusScript))))
 -> Integer
 -> [DCert]
 -> Integer
 -> HSMap RwdAddr Integer
 -> (Maybe Integer, Maybe Integer)
 -> Maybe Integer
 -> Integer
 -> [GovVote]
 -> [GovProposal]
 -> Maybe Integer
 -> Maybe Integer
 -> Integer
 -> HSSet Integer
 -> Maybe Integer
 -> TxBody)
-> SpecTransM ctx (HSSet (Integer, Integer))
-> SpecTransM
     ctx
     (HSSet (Integer, Integer)
      -> HSSet (Integer, Integer)
      -> HSMap
           Integer
           (Either BaseAddr BootstrapAddr,
            (Integer,
             (Maybe (Either Integer Integer),
              Maybe (Either HSTimelock HSPlutusScript))))
      -> Integer
      -> [DCert]
      -> Integer
      -> HSMap RwdAddr Integer
      -> (Maybe Integer, Maybe Integer)
      -> Maybe Integer
      -> Integer
      -> [GovVote]
      -> [GovProposal]
      -> Maybe Integer
      -> Maybe Integer
      -> Integer
      -> HSSet Integer
      -> Maybe Integer
      -> TxBody)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set TxIn -> SpecTransM ctx (SpecRep (Set TxIn))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (TxBody ConwayEra
txb TxBody ConwayEra
-> Getting (Set TxIn) (TxBody ConwayEra) (Set TxIn) -> Set TxIn
forall s a. s -> Getting a s a -> a
^. Getting (Set TxIn) (TxBody ConwayEra) (Set TxIn)
forall era. EraTxBody era => Lens' (TxBody era) (Set TxIn)
Lens' (TxBody ConwayEra) (Set TxIn)
inputsTxBodyL)
      SpecTransM
  ctx
  (HSSet (Integer, Integer)
   -> HSSet (Integer, Integer)
   -> HSMap
        Integer
        (Either BaseAddr BootstrapAddr,
         (Integer,
          (Maybe (Either Integer Integer),
           Maybe (Either HSTimelock HSPlutusScript))))
   -> Integer
   -> [DCert]
   -> Integer
   -> HSMap RwdAddr Integer
   -> (Maybe Integer, Maybe Integer)
   -> Maybe Integer
   -> Integer
   -> [GovVote]
   -> [GovProposal]
   -> Maybe Integer
   -> Maybe Integer
   -> Integer
   -> HSSet Integer
   -> Maybe Integer
   -> TxBody)
-> SpecTransM ctx (HSSet (Integer, Integer))
-> SpecTransM
     ctx
     (HSSet (Integer, Integer)
      -> HSMap
           Integer
           (Either BaseAddr BootstrapAddr,
            (Integer,
             (Maybe (Either Integer Integer),
              Maybe (Either HSTimelock HSPlutusScript))))
      -> Integer
      -> [DCert]
      -> Integer
      -> HSMap RwdAddr Integer
      -> (Maybe Integer, Maybe Integer)
      -> Maybe Integer
      -> Integer
      -> [GovVote]
      -> [GovProposal]
      -> Maybe Integer
      -> Maybe Integer
      -> Integer
      -> HSSet Integer
      -> Maybe Integer
      -> TxBody)
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
<*> Set TxIn -> SpecTransM ctx (SpecRep (Set TxIn))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (TxBody ConwayEra
txb TxBody ConwayEra
-> Getting (Set TxIn) (TxBody ConwayEra) (Set TxIn) -> Set TxIn
forall s a. s -> Getting a s a -> a
^. Getting (Set TxIn) (TxBody ConwayEra) (Set TxIn)
forall era. BabbageEraTxBody era => Lens' (TxBody era) (Set TxIn)
Lens' (TxBody ConwayEra) (Set TxIn)
referenceInputsTxBodyL)
      SpecTransM
  ctx
  (HSSet (Integer, Integer)
   -> HSMap
        Integer
        (Either BaseAddr BootstrapAddr,
         (Integer,
          (Maybe (Either Integer Integer),
           Maybe (Either HSTimelock HSPlutusScript))))
   -> Integer
   -> [DCert]
   -> Integer
   -> HSMap RwdAddr Integer
   -> (Maybe Integer, Maybe Integer)
   -> Maybe Integer
   -> Integer
   -> [GovVote]
   -> [GovProposal]
   -> Maybe Integer
   -> Maybe Integer
   -> Integer
   -> HSSet Integer
   -> Maybe Integer
   -> TxBody)
-> SpecTransM ctx (HSSet (Integer, Integer))
-> SpecTransM
     ctx
     (HSMap
        Integer
        (Either BaseAddr BootstrapAddr,
         (Integer,
          (Maybe (Either Integer Integer),
           Maybe (Either HSTimelock HSPlutusScript))))
      -> Integer
      -> [DCert]
      -> Integer
      -> HSMap RwdAddr Integer
      -> (Maybe Integer, Maybe Integer)
      -> Maybe Integer
      -> Integer
      -> [GovVote]
      -> [GovProposal]
      -> Maybe Integer
      -> Maybe Integer
      -> Integer
      -> HSSet Integer
      -> Maybe Integer
      -> TxBody)
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
<*> Set TxIn -> SpecTransM ctx (SpecRep (Set TxIn))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (TxBody ConwayEra
txb TxBody ConwayEra
-> Getting (Set TxIn) (TxBody ConwayEra) (Set TxIn) -> Set TxIn
forall s a. s -> Getting a s a -> a
^. Getting (Set TxIn) (TxBody ConwayEra) (Set TxIn)
forall era. AlonzoEraTxBody era => Lens' (TxBody era) (Set TxIn)
Lens' (TxBody ConwayEra) (Set TxIn)
collateralInputsTxBodyL)
      SpecTransM
  ctx
  (HSMap
     Integer
     (Either BaseAddr BootstrapAddr,
      (Integer,
       (Maybe (Either Integer Integer),
        Maybe (Either HSTimelock HSPlutusScript))))
   -> Integer
   -> [DCert]
   -> Integer
   -> HSMap RwdAddr Integer
   -> (Maybe Integer, Maybe Integer)
   -> Maybe Integer
   -> Integer
   -> [GovVote]
   -> [GovProposal]
   -> Maybe Integer
   -> Maybe Integer
   -> Integer
   -> HSSet Integer
   -> Maybe Integer
   -> TxBody)
-> SpecTransM
     ctx
     (HSMap
        Integer
        (Either BaseAddr BootstrapAddr,
         (Integer,
          (Maybe (Either Integer Integer),
           Maybe (Either HSTimelock HSPlutusScript)))))
-> SpecTransM
     ctx
     (Integer
      -> [DCert]
      -> Integer
      -> HSMap RwdAddr Integer
      -> (Maybe Integer, Maybe Integer)
      -> Maybe Integer
      -> Integer
      -> [GovVote]
      -> [GovProposal]
      -> Maybe Integer
      -> Maybe Integer
      -> Integer
      -> HSSet Integer
      -> Maybe Integer
      -> TxBody)
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
<*> ([(Integer,
  (Either BaseAddr BootstrapAddr,
   (Integer,
    (Maybe (Either Integer Integer),
     Maybe (Either HSTimelock HSPlutusScript)))))]
-> HSMap
     Integer
     (Either BaseAddr BootstrapAddr,
      (Integer,
       (Maybe (Either Integer Integer),
        Maybe (Either HSTimelock HSPlutusScript))))
forall k v. [(k, v)] -> HSMap k v
Agda.MkHSMap ([(Integer,
   (Either BaseAddr BootstrapAddr,
    (Integer,
     (Maybe (Either Integer Integer),
      Maybe (Either HSTimelock HSPlutusScript)))))]
 -> HSMap
      Integer
      (Either BaseAddr BootstrapAddr,
       (Integer,
        (Maybe (Either Integer Integer),
         Maybe (Either HSTimelock HSPlutusScript)))))
-> ([(Either BaseAddr BootstrapAddr,
      (Integer,
       (Maybe (Either Integer Integer),
        Maybe (Either HSTimelock HSPlutusScript))))]
    -> [(Integer,
         (Either BaseAddr BootstrapAddr,
          (Integer,
           (Maybe (Either Integer Integer),
            Maybe (Either HSTimelock HSPlutusScript)))))])
-> [(Either BaseAddr BootstrapAddr,
     (Integer,
      (Maybe (Either Integer Integer),
       Maybe (Either HSTimelock HSPlutusScript))))]
-> HSMap
     Integer
     (Either BaseAddr BootstrapAddr,
      (Integer,
       (Maybe (Either Integer Integer),
        Maybe (Either HSTimelock HSPlutusScript))))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Integer]
-> [(Either BaseAddr BootstrapAddr,
     (Integer,
      (Maybe (Either Integer Integer),
       Maybe (Either HSTimelock HSPlutusScript))))]
-> [(Integer,
     (Either BaseAddr BootstrapAddr,
      (Integer,
       (Maybe (Either Integer Integer),
        Maybe (Either HSTimelock HSPlutusScript)))))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Integer
0 ..] ([(Either BaseAddr BootstrapAddr,
   (Integer,
    (Maybe (Either Integer Integer),
     Maybe (Either HSTimelock HSPlutusScript))))]
 -> HSMap
      Integer
      (Either BaseAddr BootstrapAddr,
       (Integer,
        (Maybe (Either Integer Integer),
         Maybe (Either HSTimelock HSPlutusScript)))))
-> SpecTransM
     ctx
     [(Either BaseAddr BootstrapAddr,
       (Integer,
        (Maybe (Either Integer Integer),
         Maybe (Either HSTimelock HSPlutusScript))))]
-> SpecTransM
     ctx
     (HSMap
        Integer
        (Either BaseAddr BootstrapAddr,
         (Integer,
          (Maybe (Either Integer Integer),
           Maybe (Either HSTimelock HSPlutusScript)))))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StrictSeq (BabbageTxOut ConwayEra)
-> SpecTransM ctx (SpecRep (StrictSeq (BabbageTxOut ConwayEra)))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (TxBody ConwayEra
txb TxBody ConwayEra
-> Getting
     (StrictSeq (BabbageTxOut ConwayEra))
     (TxBody ConwayEra)
     (StrictSeq (BabbageTxOut ConwayEra))
-> StrictSeq (BabbageTxOut ConwayEra)
forall s a. s -> Getting a s a -> a
^. (StrictSeq (TxOut ConwayEra)
 -> Const
      (StrictSeq (BabbageTxOut ConwayEra)) (StrictSeq (TxOut ConwayEra)))
-> TxBody ConwayEra
-> Const (StrictSeq (BabbageTxOut ConwayEra)) (TxBody ConwayEra)
Getting
  (StrictSeq (BabbageTxOut ConwayEra))
  (TxBody ConwayEra)
  (StrictSeq (BabbageTxOut ConwayEra))
forall era.
EraTxBody era =>
Lens' (TxBody era) (StrictSeq (TxOut era))
Lens' (TxBody ConwayEra) (StrictSeq (TxOut ConwayEra))
outputsTxBodyL))
      SpecTransM
  ctx
  (Integer
   -> [DCert]
   -> Integer
   -> HSMap RwdAddr Integer
   -> (Maybe Integer, Maybe Integer)
   -> Maybe Integer
   -> Integer
   -> [GovVote]
   -> [GovProposal]
   -> Maybe Integer
   -> Maybe Integer
   -> Integer
   -> HSSet Integer
   -> Maybe Integer
   -> TxBody)
-> SpecTransM ctx Integer
-> SpecTransM
     ctx
     ([DCert]
      -> Integer
      -> HSMap RwdAddr Integer
      -> (Maybe Integer, Maybe Integer)
      -> Maybe Integer
      -> Integer
      -> [GovVote]
      -> [GovProposal]
      -> Maybe Integer
      -> Maybe Integer
      -> Integer
      -> HSSet Integer
      -> Maybe Integer
      -> TxBody)
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
<*> TxId -> SpecTransM ctx (SpecRep TxId)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep TxId
txId
      SpecTransM
  ctx
  ([DCert]
   -> Integer
   -> HSMap RwdAddr Integer
   -> (Maybe Integer, Maybe Integer)
   -> Maybe Integer
   -> Integer
   -> [GovVote]
   -> [GovProposal]
   -> Maybe Integer
   -> Maybe Integer
   -> Integer
   -> HSSet Integer
   -> Maybe Integer
   -> TxBody)
-> SpecTransM ctx [DCert]
-> SpecTransM
     ctx
     (Integer
      -> HSMap RwdAddr Integer
      -> (Maybe Integer, Maybe Integer)
      -> Maybe Integer
      -> Integer
      -> [GovVote]
      -> [GovProposal]
      -> Maybe Integer
      -> Maybe Integer
      -> Integer
      -> HSSet Integer
      -> Maybe Integer
      -> TxBody)
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
<*> StrictSeq (ConwayTxCert ConwayEra)
-> SpecTransM ctx (SpecRep (StrictSeq (ConwayTxCert ConwayEra)))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (TxBody ConwayEra
txb TxBody ConwayEra
-> Getting
     (StrictSeq (ConwayTxCert ConwayEra))
     (TxBody ConwayEra)
     (StrictSeq (ConwayTxCert ConwayEra))
-> StrictSeq (ConwayTxCert ConwayEra)
forall s a. s -> Getting a s a -> a
^. (StrictSeq (TxCert ConwayEra)
 -> Const
      (StrictSeq (ConwayTxCert ConwayEra))
      (StrictSeq (TxCert ConwayEra)))
-> TxBody ConwayEra
-> Const (StrictSeq (ConwayTxCert ConwayEra)) (TxBody ConwayEra)
Getting
  (StrictSeq (ConwayTxCert ConwayEra))
  (TxBody ConwayEra)
  (StrictSeq (ConwayTxCert ConwayEra))
forall era.
EraTxBody era =>
Lens' (TxBody era) (StrictSeq (TxCert era))
Lens' (TxBody ConwayEra) (StrictSeq (TxCert ConwayEra))
certsTxBodyL)
      SpecTransM
  ctx
  (Integer
   -> HSMap RwdAddr Integer
   -> (Maybe Integer, Maybe Integer)
   -> Maybe Integer
   -> Integer
   -> [GovVote]
   -> [GovProposal]
   -> Maybe Integer
   -> Maybe Integer
   -> Integer
   -> HSSet Integer
   -> Maybe Integer
   -> TxBody)
-> SpecTransM ctx Integer
-> SpecTransM
     ctx
     (HSMap RwdAddr Integer
      -> (Maybe Integer, Maybe Integer)
      -> Maybe Integer
      -> Integer
      -> [GovVote]
      -> [GovProposal]
      -> Maybe Integer
      -> Maybe Integer
      -> Integer
      -> HSSet Integer
      -> Maybe Integer
      -> TxBody)
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 (TxBody ConwayEra
txb TxBody ConwayEra -> Getting Coin (TxBody ConwayEra) Coin -> Coin
forall s a. s -> Getting a s a -> a
^. Getting Coin (TxBody ConwayEra) Coin
forall era. EraTxBody era => Lens' (TxBody era) Coin
Lens' (TxBody ConwayEra) Coin
feeTxBodyL)
      SpecTransM
  ctx
  (HSMap RwdAddr Integer
   -> (Maybe Integer, Maybe Integer)
   -> Maybe Integer
   -> Integer
   -> [GovVote]
   -> [GovProposal]
   -> Maybe Integer
   -> Maybe Integer
   -> Integer
   -> HSSet Integer
   -> Maybe Integer
   -> TxBody)
-> SpecTransM ctx (HSMap RwdAddr Integer)
-> SpecTransM
     ctx
     ((Maybe Integer, Maybe Integer)
      -> Maybe Integer
      -> Integer
      -> [GovVote]
      -> [GovProposal]
      -> Maybe Integer
      -> Maybe Integer
      -> Integer
      -> HSSet Integer
      -> Maybe Integer
      -> TxBody)
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
<*> Withdrawals -> SpecTransM ctx (SpecRep Withdrawals)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (TxBody ConwayEra
txb TxBody ConwayEra
-> Getting Withdrawals (TxBody ConwayEra) Withdrawals
-> Withdrawals
forall s a. s -> Getting a s a -> a
^. Getting Withdrawals (TxBody ConwayEra) Withdrawals
forall era. EraTxBody era => Lens' (TxBody era) Withdrawals
Lens' (TxBody ConwayEra) Withdrawals
withdrawalsTxBodyL)
      SpecTransM
  ctx
  ((Maybe Integer, Maybe Integer)
   -> Maybe Integer
   -> Integer
   -> [GovVote]
   -> [GovProposal]
   -> Maybe Integer
   -> Maybe Integer
   -> Integer
   -> HSSet Integer
   -> Maybe Integer
   -> TxBody)
-> SpecTransM ctx (Maybe Integer, Maybe Integer)
-> SpecTransM
     ctx
     (Maybe Integer
      -> Integer
      -> [GovVote]
      -> [GovProposal]
      -> Maybe Integer
      -> Maybe Integer
      -> Integer
      -> HSSet Integer
      -> Maybe Integer
      -> TxBody)
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
<*> ValidityInterval -> SpecTransM ctx (SpecRep ValidityInterval)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (TxBody ConwayEra
txb TxBody ConwayEra
-> Getting ValidityInterval (TxBody ConwayEra) ValidityInterval
-> ValidityInterval
forall s a. s -> Getting a s a -> a
^. Getting ValidityInterval (TxBody ConwayEra) ValidityInterval
forall era.
AllegraEraTxBody era =>
Lens' (TxBody era) ValidityInterval
Lens' (TxBody ConwayEra) ValidityInterval
vldtTxBodyL)
      SpecTransM
  ctx
  (Maybe Integer
   -> Integer
   -> [GovVote]
   -> [GovProposal]
   -> Maybe Integer
   -> Maybe Integer
   -> Integer
   -> HSSet Integer
   -> Maybe Integer
   -> TxBody)
-> SpecTransM ctx (Maybe Integer)
-> SpecTransM
     ctx
     (Integer
      -> [GovVote]
      -> [GovProposal]
      -> Maybe Integer
      -> Maybe Integer
      -> Integer
      -> HSSet Integer
      -> Maybe Integer
      -> TxBody)
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 TxAuxDataHash
-> SpecTransM ctx (SpecRep (StrictMaybe TxAuxDataHash))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (TxBody ConwayEra
txb TxBody ConwayEra
-> Getting
     (StrictMaybe TxAuxDataHash)
     (TxBody ConwayEra)
     (StrictMaybe TxAuxDataHash)
-> StrictMaybe TxAuxDataHash
forall s a. s -> Getting a s a -> a
^. Getting
  (StrictMaybe TxAuxDataHash)
  (TxBody ConwayEra)
  (StrictMaybe TxAuxDataHash)
forall era.
EraTxBody era =>
Lens' (TxBody era) (StrictMaybe TxAuxDataHash)
Lens' (TxBody ConwayEra) (StrictMaybe TxAuxDataHash)
auxDataHashTxBodyL)
      SpecTransM
  ctx
  (Integer
   -> [GovVote]
   -> [GovProposal]
   -> Maybe Integer
   -> Maybe Integer
   -> Integer
   -> HSSet Integer
   -> Maybe Integer
   -> TxBody)
-> SpecTransM ctx Integer
-> SpecTransM
     ctx
     ([GovVote]
      -> [GovProposal]
      -> Maybe Integer
      -> Maybe Integer
      -> Integer
      -> HSSet Integer
      -> Maybe Integer
      -> TxBody)
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 (TxBody ConwayEra
txb TxBody ConwayEra -> Getting Coin (TxBody ConwayEra) Coin -> Coin
forall s a. s -> Getting a s a -> a
^. Getting Coin (TxBody ConwayEra) Coin
forall era. ConwayEraTxBody era => Lens' (TxBody era) Coin
Lens' (TxBody ConwayEra) Coin
treasuryDonationTxBodyL)
      SpecTransM
  ctx
  ([GovVote]
   -> [GovProposal]
   -> Maybe Integer
   -> Maybe Integer
   -> Integer
   -> HSSet Integer
   -> Maybe Integer
   -> TxBody)
-> SpecTransM ctx [GovVote]
-> SpecTransM
     ctx
     ([GovProposal]
      -> Maybe Integer
      -> Maybe Integer
      -> Integer
      -> HSSet Integer
      -> Maybe Integer
      -> TxBody)
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
<*> VotingProcedures ConwayEra
-> SpecTransM ctx (SpecRep (VotingProcedures ConwayEra))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (TxBody ConwayEra
txb TxBody ConwayEra
-> Getting
     (VotingProcedures ConwayEra)
     (TxBody ConwayEra)
     (VotingProcedures ConwayEra)
-> VotingProcedures ConwayEra
forall s a. s -> Getting a s a -> a
^. Getting
  (VotingProcedures ConwayEra)
  (TxBody ConwayEra)
  (VotingProcedures ConwayEra)
forall era.
ConwayEraTxBody era =>
Lens' (TxBody era) (VotingProcedures era)
Lens' (TxBody ConwayEra) (VotingProcedures ConwayEra)
votingProceduresTxBodyL)
      SpecTransM
  ctx
  ([GovProposal]
   -> Maybe Integer
   -> Maybe Integer
   -> Integer
   -> HSSet Integer
   -> Maybe Integer
   -> TxBody)
-> SpecTransM ctx [GovProposal]
-> SpecTransM
     ctx
     (Maybe Integer
      -> Maybe Integer
      -> Integer
      -> HSSet Integer
      -> Maybe Integer
      -> TxBody)
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
<*> OSet (ProposalProcedure ConwayEra)
-> SpecTransM ctx (SpecRep (OSet (ProposalProcedure ConwayEra)))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (TxBody ConwayEra
txb TxBody ConwayEra
-> Getting
     (OSet (ProposalProcedure ConwayEra))
     (TxBody ConwayEra)
     (OSet (ProposalProcedure ConwayEra))
-> OSet (ProposalProcedure ConwayEra)
forall s a. s -> Getting a s a -> a
^. Getting
  (OSet (ProposalProcedure ConwayEra))
  (TxBody ConwayEra)
  (OSet (ProposalProcedure ConwayEra))
forall era.
ConwayEraTxBody era =>
Lens' (TxBody era) (OSet (ProposalProcedure era))
Lens' (TxBody ConwayEra) (OSet (ProposalProcedure ConwayEra))
proposalProceduresTxBodyL)
      SpecTransM
  ctx
  (Maybe Integer
   -> Maybe Integer
   -> Integer
   -> HSSet Integer
   -> Maybe Integer
   -> TxBody)
-> SpecTransM ctx (Maybe Integer)
-> SpecTransM
     ctx
     (Maybe Integer
      -> Integer -> HSSet Integer -> Maybe Integer -> TxBody)
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 Network
-> SpecTransM ctx (SpecRep (StrictMaybe Network))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (TxBody ConwayEra
txb TxBody ConwayEra
-> Getting
     (StrictMaybe Network) (TxBody ConwayEra) (StrictMaybe Network)
-> StrictMaybe Network
forall s a. s -> Getting a s a -> a
^. Getting
  (StrictMaybe Network) (TxBody ConwayEra) (StrictMaybe Network)
forall era.
AlonzoEraTxBody era =>
Lens' (TxBody era) (StrictMaybe Network)
Lens' (TxBody ConwayEra) (StrictMaybe Network)
networkIdTxBodyL)
      SpecTransM
  ctx
  (Maybe Integer
   -> Integer -> HSSet Integer -> Maybe Integer -> TxBody)
-> SpecTransM ctx (Maybe Integer)
-> SpecTransM
     ctx (Integer -> HSSet Integer -> Maybe Integer -> TxBody)
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 Coin -> SpecTransM ctx (SpecRep (StrictMaybe Coin))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (TxBody ConwayEra
txb TxBody ConwayEra
-> Getting (StrictMaybe Coin) (TxBody ConwayEra) (StrictMaybe Coin)
-> StrictMaybe Coin
forall s a. s -> Getting a s a -> a
^. Getting (StrictMaybe Coin) (TxBody ConwayEra) (StrictMaybe Coin)
forall era.
ConwayEraTxBody era =>
Lens' (TxBody era) (StrictMaybe Coin)
Lens' (TxBody ConwayEra) (StrictMaybe Coin)
currentTreasuryValueTxBodyL)
      SpecTransM
  ctx (Integer -> HSSet Integer -> Maybe Integer -> TxBody)
-> SpecTransM ctx Integer
-> SpecTransM ctx (HSSet Integer -> Maybe Integer -> TxBody)
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
<*> Integer -> SpecTransM ctx Integer
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Integer
0
      SpecTransM ctx (HSSet Integer -> Maybe Integer -> TxBody)
-> SpecTransM ctx (HSSet Integer)
-> SpecTransM ctx (Maybe Integer -> TxBody)
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
<*> Set (KeyHash 'Witness)
-> SpecTransM ctx (SpecRep (Set (KeyHash 'Witness)))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (TxBody ConwayEra
txb TxBody ConwayEra
-> Getting
     (Set (KeyHash 'Witness))
     (TxBody ConwayEra)
     (Set (KeyHash 'Witness))
-> Set (KeyHash 'Witness)
forall s a. s -> Getting a s a -> a
^. Getting
  (Set (KeyHash 'Witness))
  (TxBody ConwayEra)
  (Set (KeyHash 'Witness))
forall era.
(AlonzoEraTxBody era, AtMostEra "Conway" era) =>
Lens' (TxBody era) (Set (KeyHash 'Witness))
Lens' (TxBody ConwayEra) (Set (KeyHash 'Witness))
reqSignerHashesTxBodyL)
      SpecTransM ctx (Maybe Integer -> TxBody)
-> SpecTransM ctx (Maybe Integer) -> SpecTransM ctx TxBody
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 ScriptIntegrityHash
-> SpecTransM ctx (SpecRep (StrictMaybe ScriptIntegrityHash))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (TxBody ConwayEra
txb TxBody ConwayEra
-> Getting
     (StrictMaybe ScriptIntegrityHash)
     (TxBody ConwayEra)
     (StrictMaybe ScriptIntegrityHash)
-> StrictMaybe ScriptIntegrityHash
forall s a. s -> Getting a s a -> a
^. Getting
  (StrictMaybe ScriptIntegrityHash)
  (TxBody ConwayEra)
  (StrictMaybe ScriptIntegrityHash)
forall era.
AlonzoEraTxBody era =>
Lens' (TxBody era) (StrictMaybe ScriptIntegrityHash)
Lens' (TxBody ConwayEra) (StrictMaybe ScriptIntegrityHash)
scriptIntegrityHashTxBodyL)

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

  toSpecRep :: Tx ConwayEra -> SpecTransM ctx (SpecRep (Tx ConwayEra))
toSpecRep Tx 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 ConwayEra -> TxId
forall era. EraTx era => Tx era -> TxId
txIdTx Tx ConwayEra
tx) (TxBody ConwayEra -> SpecTransM TxId (SpecRep (TxBody ConwayEra))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (Tx ConwayEra
tx Tx ConwayEra
-> Getting (TxBody ConwayEra) (Tx ConwayEra) (TxBody ConwayEra)
-> TxBody ConwayEra
forall s a. s -> Getting a s a -> a
^. Getting (TxBody ConwayEra) (Tx ConwayEra) (TxBody ConwayEra)
forall era. EraTx era => Lens' (Tx era) (TxBody era)
Lens' (Tx ConwayEra) (TxBody 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 ConwayEra
tx Tx ConwayEra
-> Getting
     (AlonzoTxWits ConwayEra) (Tx ConwayEra) (AlonzoTxWits ConwayEra)
-> AlonzoTxWits ConwayEra
forall s a. s -> Getting a s a -> a
^. (TxWits ConwayEra
 -> Const (AlonzoTxWits ConwayEra) (TxWits ConwayEra))
-> Tx ConwayEra -> Const (AlonzoTxWits ConwayEra) (Tx ConwayEra)
Getting
  (AlonzoTxWits ConwayEra) (Tx ConwayEra) (AlonzoTxWits ConwayEra)
forall era. EraTx era => Lens' (Tx era) (TxWits era)
Lens' (Tx 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 ConwayEra
tx Tx ConwayEra -> Getting Word32 (Tx ConwayEra) Word32 -> Word32
forall s a. s -> Getting a s a -> a
^. Getting Word32 (Tx ConwayEra) Word32
forall era.
(EraTx era, HasCallStack) =>
SimpleGetter (Tx era) Word32
SimpleGetter (Tx 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 ConwayEra
tx Tx ConwayEra -> Getting IsValid (Tx ConwayEra) IsValid -> IsValid
forall s a. s -> Getting a s a -> a
^. Getting IsValid (Tx ConwayEra) IsValid
forall era. AlonzoEraTx era => Lens' (Tx era) IsValid
Lens' (Tx 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 ConwayEra
tx Tx ConwayEra
-> Getting
     (StrictMaybe (AlonzoTxAuxData ConwayEra))
     (Tx 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 ConwayEra
-> Const (StrictMaybe (AlonzoTxAuxData ConwayEra)) (Tx ConwayEra)
Getting
  (StrictMaybe (AlonzoTxAuxData ConwayEra))
  (Tx ConwayEra)
  (StrictMaybe (AlonzoTxAuxData ConwayEra))
forall era.
EraTx era =>
Lens' (Tx era) (StrictMaybe (TxAuxData era))
Lens' (Tx ConwayEra) (StrictMaybe (TxAuxData ConwayEra))
auxDataTxL)