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

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

import Cardano.Ledger.BaseTypes (Network)
import Cardano.Ledger.Conway.Governance
import qualified Cardano.Ledger.Conway.Rules as Conway
import Cardano.Ledger.Dijkstra (DijkstraEra)
import Cardano.Ledger.Dijkstra.Core (
  AllegraEraTxBody (..),
  AlonzoEraTx (..),
  AlonzoEraTxBody (..),
  BabbageEraTxBody (..),
  ConwayEraTxBody (..),
  EraTx (..),
  EraTxBody (..),
  ScriptHash,
  SubTx,
  TopTx,
  TxLevel (..),
  txIdTx,
  txStAnnTxG,
 )
import Cardano.Ledger.Dijkstra.Tx (DijkstraStAnnTx)
import Cardano.Ledger.Dijkstra.TxBody (DijkstraEraTxBody (..))
import Cardano.Ledger.Shelley.LedgerState
import qualified Cardano.Ledger.Shelley.Rules as Shelley
import Cardano.Ledger.Shelley.State (ChainAccountState (..))
import Cardano.Ledger.TxIn (TxId)
import Data.Foldable (toList)
import qualified Data.Map.Strict as Map
import Data.Maybe.Strict (StrictMaybe)
import qualified Data.OMap.Strict as OMap
import Lens.Micro ((^.))
import qualified MAlonzo.Code.Ledger.Dijkstra.Foreign.API as Agda
import Test.Cardano.Ledger.Conformance (toSpecRepTuple)
import Test.Cardano.Ledger.Conformance.SpecTranslate.Base (
  SpecTranslate (..),
  askSpecTransM,
  withCtxSpecTransM,
 )
import Test.Cardano.Ledger.Conformance.SpecTranslate.Dijkstra.Base ()
import Test.Cardano.Ledger.Conformance.SpecTranslate.Dijkstra.Cert ()
import Test.Cardano.Ledger.Conformance.SpecTranslate.Dijkstra.Utxo ()

instance SpecTranslate DijkstraEra (Shelley.LedgerEnv DijkstraEra) where
  type SpecRep DijkstraEra (Shelley.LedgerEnv DijkstraEra) = Agda.LedgerEnv
  type
    SpecContext DijkstraEra (Shelley.LedgerEnv DijkstraEra) =
      (StrictMaybe ScriptHash, Conway.EnactState DijkstraEra)

  toSpecRep :: LedgerEnv DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (LedgerEnv DijkstraEra))
     (SpecRep DijkstraEra (LedgerEnv DijkstraEra))
toSpecRep Shelley.LedgerEnv {Maybe EpochNo
PParams DijkstraEra
ChainAccountState
TxIx
SlotNo
ledgerSlotNo :: SlotNo
ledgerEpochNo :: Maybe EpochNo
ledgerIx :: TxIx
ledgerPp :: PParams DijkstraEra
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, enactState) <- SpecTransM
  DijkstraEra
  (StrictMaybe ScriptHash, EnactState DijkstraEra)
  (StrictMaybe ScriptHash, EnactState DijkstraEra)
forall era ctx. SpecTransM era ctx ctx
askSpecTransM
    withCtxSpecTransM () $
      Agda.MkLedgerEnv
        <$> toSpecRep ledgerSlotNo
        <*> toSpecRep policyHash
        <*> toSpecRep ledgerPp
        <*> toSpecRep enactState
        <*> toSpecRep (casTreasury ledgerAccount)

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

  type SpecContext DijkstraEra (LedgerState DijkstraEra) = Network

  toSpecRep :: LedgerState DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (LedgerState DijkstraEra))
     (SpecRep DijkstraEra (LedgerState DijkstraEra))
toSpecRep (LedgerState {CertState DijkstraEra
UTxOState DijkstraEra
lsUTxOState :: UTxOState DijkstraEra
lsCertState :: CertState DijkstraEra
lsCertState :: forall era. LedgerState era -> CertState era
lsUTxOState :: forall era. LedgerState era -> UTxOState era
..}) =
    UTxOState
-> [((Integer, Integer), GovActionState)]
-> CertState
-> LedgerState
Agda.MkLedgerState
      (UTxOState
 -> [((Integer, Integer), GovActionState)]
 -> CertState
 -> LedgerState)
-> SpecTransM DijkstraEra Network UTxOState
-> SpecTransM
     DijkstraEra
     Network
     ([((Integer, Integer), GovActionState)]
      -> CertState -> LedgerState)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ()
-> SpecTransM DijkstraEra () UTxOState
-> SpecTransM DijkstraEra Network UTxOState
forall ctx era a ctx'.
ctx -> SpecTransM era ctx a -> SpecTransM era ctx' a
withCtxSpecTransM () (UTxOState DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (UTxOState DijkstraEra))
     (SpecRep DijkstraEra (UTxOState DijkstraEra))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep UTxOState DijkstraEra
lsUTxOState)
      SpecTransM
  DijkstraEra
  Network
  ([((Integer, Integer), GovActionState)]
   -> CertState -> LedgerState)
-> SpecTransM
     DijkstraEra Network [((Integer, Integer), GovActionState)]
-> SpecTransM DijkstraEra Network (CertState -> LedgerState)
forall a b.
SpecTransM DijkstraEra Network (a -> b)
-> SpecTransM DijkstraEra Network a
-> SpecTransM DijkstraEra Network b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ()
-> SpecTransM DijkstraEra () [((Integer, Integer), GovActionState)]
-> SpecTransM
     DijkstraEra Network [((Integer, Integer), GovActionState)]
forall ctx era a ctx'.
ctx -> SpecTransM era ctx a -> SpecTransM era ctx' a
withCtxSpecTransM () (Proposals DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (Proposals DijkstraEra))
     (SpecRep DijkstraEra (Proposals DijkstraEra))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep (UTxOState DijkstraEra -> GovState DijkstraEra
forall era. UTxOState era -> GovState era
utxosGovState UTxOState DijkstraEra
lsUTxOState ConwayGovState DijkstraEra
-> Getting
     (Proposals DijkstraEra)
     (ConwayGovState DijkstraEra)
     (Proposals DijkstraEra)
-> Proposals DijkstraEra
forall s a. s -> Getting a s a -> a
^. (Proposals DijkstraEra
 -> Const (Proposals DijkstraEra) (Proposals DijkstraEra))
-> GovState DijkstraEra
-> Const (Proposals DijkstraEra) (GovState DijkstraEra)
Getting
  (Proposals DijkstraEra)
  (ConwayGovState DijkstraEra)
  (Proposals DijkstraEra)
forall era.
ConwayEraGov era =>
Lens' (GovState era) (Proposals era)
Lens' (GovState DijkstraEra) (Proposals DijkstraEra)
proposalsGovStateL))
      SpecTransM DijkstraEra Network (CertState -> LedgerState)
-> SpecTransM DijkstraEra Network CertState
-> SpecTransM DijkstraEra Network LedgerState
forall a b.
SpecTransM DijkstraEra Network (a -> b)
-> SpecTransM DijkstraEra Network a
-> SpecTransM DijkstraEra Network b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ConwayCertState DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (ConwayCertState DijkstraEra))
     (SpecRep DijkstraEra (ConwayCertState DijkstraEra))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep CertState DijkstraEra
ConwayCertState DijkstraEra
lsCertState

instance SpecTranslate DijkstraEra (TxBody TopTx DijkstraEra) where
  type SpecRep DijkstraEra (TxBody TopTx DijkstraEra) = Agda.TxBodyTop
  type SpecContext DijkstraEra (TxBody TopTx DijkstraEra) = TxId

  toSpecRep :: TxBody TopTx DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (TxBody TopTx DijkstraEra))
     (SpecRep DijkstraEra (TxBody TopTx DijkstraEra))
toSpecRep TxBody TopTx DijkstraEra
txb = do
    txId <- SpecTransM DijkstraEra TxId TxId
forall era ctx. SpecTransM era ctx ctx
askSpecTransM
    withCtxSpecTransM () $
      Agda.MkTxBodyTop
        <$> 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
        <*> fmap (fmap (const 0)) (toSpecRep (txb ^. scriptIntegrityHashTxBodyL))
        <*> traverse toSpecRep (toList $ OMap.toMap $ txb ^. subTransactionsTxBodyL)
        <*> (Agda.MkHSSet <$> toSpecRep (txb ^. guardsTxBodyL))
        <*> toSpecRep (txb ^. directDepositsTxBodyL)
        <*> toSpecRep (txb ^. accountBalanceIntervalsTxBodyL)

instance SpecTranslate DijkstraEra (TxBody SubTx DijkstraEra) where
  type SpecRep DijkstraEra (TxBody SubTx DijkstraEra) = Agda.TxBodySub
  type SpecContext DijkstraEra (TxBody SubTx DijkstraEra) = TxId

  toSpecRep :: TxBody SubTx DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (TxBody SubTx DijkstraEra))
     (SpecRep DijkstraEra (TxBody SubTx DijkstraEra))
toSpecRep TxBody SubTx DijkstraEra
txb = do
    txId <- SpecTransM DijkstraEra TxId TxId
forall era ctx. SpecTransM era ctx ctx
askSpecTransM
    withCtxSpecTransM () $
      Agda.MkTxBodySub
        <$> toSpecRep (txb ^. inputsTxBodyL)
        <*> toSpecRep (txb ^. referenceInputsTxBodyL)
        <*> (Agda.MkHSMap . zip [0 ..] <$> toSpecRep (txb ^. outputsTxBodyL))
        <*> toSpecRep txId
        <*> toSpecRep (txb ^. certsTxBodyL)
        <*> 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
        <*> fmap (fmap (const 0)) (toSpecRep (txb ^. scriptIntegrityHashTxBodyL))
        <*> (Agda.MkHSSet <$> toSpecRep (txb ^. guardsTxBodyL))
        <*> (Agda.MkHSSet <$> traverse toSpecRepTuple (Map.toList $ txb ^. requiredTopLevelGuardsL))
        <*> toSpecRep (txb ^. directDepositsTxBodyL)
        <*> toSpecRep (txb ^. accountBalanceIntervalsTxBodyL)

instance SpecTranslate DijkstraEra (Tx TopTx DijkstraEra) where
  type SpecRep DijkstraEra (Tx TopTx DijkstraEra) = Agda.TxTop

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

instance SpecTranslate DijkstraEra (Tx SubTx DijkstraEra) where
  type SpecRep DijkstraEra (Tx SubTx DijkstraEra) = Agda.TxSub

  toSpecRep :: Tx SubTx DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (Tx SubTx DijkstraEra))
     (SpecRep DijkstraEra (Tx SubTx DijkstraEra))
toSpecRep Tx SubTx DijkstraEra
tx =
    TxBodySub -> TxWitnesses -> Integer -> () -> Maybe Integer -> TxSub
Agda.MkTxSub
      (TxBodySub
 -> TxWitnesses -> Integer -> () -> Maybe Integer -> TxSub)
-> SpecTransM DijkstraEra () TxBodySub
-> SpecTransM
     DijkstraEra
     ()
     (TxWitnesses -> Integer -> () -> Maybe Integer -> TxSub)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TxId
-> SpecTransM DijkstraEra TxId TxBodySub
-> SpecTransM DijkstraEra () TxBodySub
forall ctx era a ctx'.
ctx -> SpecTransM era ctx a -> SpecTransM era ctx' a
withCtxSpecTransM (Tx SubTx DijkstraEra -> TxId
forall era (l :: TxLevel). EraTx era => Tx l era -> TxId
txIdTx Tx SubTx DijkstraEra
tx) (TxBody SubTx DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (TxBody SubTx DijkstraEra))
     (SpecRep DijkstraEra (TxBody SubTx DijkstraEra))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep (Tx SubTx DijkstraEra
tx Tx SubTx DijkstraEra
-> Getting
     (TxBody SubTx DijkstraEra)
     (Tx SubTx DijkstraEra)
     (TxBody SubTx DijkstraEra)
-> TxBody SubTx DijkstraEra
forall s a. s -> Getting a s a -> a
^. Getting
  (TxBody SubTx DijkstraEra)
  (Tx SubTx DijkstraEra)
  (TxBody SubTx DijkstraEra)
forall era (l :: TxLevel).
EraTx era =>
Lens' (Tx l era) (TxBody l era)
forall (l :: TxLevel).
Lens' (Tx l DijkstraEra) (TxBody l DijkstraEra)
bodyTxL))
      SpecTransM
  DijkstraEra
  ()
  (TxWitnesses -> Integer -> () -> Maybe Integer -> TxSub)
-> SpecTransM DijkstraEra () TxWitnesses
-> SpecTransM
     DijkstraEra () (Integer -> () -> Maybe Integer -> TxSub)
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
<*> AlonzoTxWits DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (AlonzoTxWits DijkstraEra))
     (SpecRep DijkstraEra (AlonzoTxWits DijkstraEra))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep (Tx SubTx DijkstraEra
tx Tx SubTx DijkstraEra
-> Getting
     (AlonzoTxWits DijkstraEra)
     (Tx SubTx DijkstraEra)
     (AlonzoTxWits DijkstraEra)
-> AlonzoTxWits DijkstraEra
forall s a. s -> Getting a s a -> a
^. (TxWits DijkstraEra
 -> Const (AlonzoTxWits DijkstraEra) (TxWits DijkstraEra))
-> Tx SubTx DijkstraEra
-> Const (AlonzoTxWits DijkstraEra) (Tx SubTx DijkstraEra)
Getting
  (AlonzoTxWits DijkstraEra)
  (Tx SubTx DijkstraEra)
  (AlonzoTxWits DijkstraEra)
forall era (l :: TxLevel).
EraTx era =>
Lens' (Tx l era) (TxWits era)
forall (l :: TxLevel).
Lens' (Tx l DijkstraEra) (TxWits DijkstraEra)
witsTxL)
      SpecTransM DijkstraEra () (Integer -> () -> Maybe Integer -> TxSub)
-> SpecTransM DijkstraEra () Integer
-> SpecTransM DijkstraEra () (() -> Maybe Integer -> TxSub)
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
<*> Word32
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra Word32)
     (SpecRep DijkstraEra Word32)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep (Tx SubTx DijkstraEra
tx Tx SubTx DijkstraEra
-> Getting Word32 (Tx SubTx DijkstraEra) Word32 -> Word32
forall s a. s -> Getting a s a -> a
^. Getting Word32 (Tx SubTx DijkstraEra) Word32
forall era (l :: TxLevel).
(EraTx era, HasCallStack) =>
SimpleGetter (Tx l era) Word32
SimpleGetter (Tx SubTx DijkstraEra) Word32
forall (l :: TxLevel).
HasCallStack =>
SimpleGetter (Tx l DijkstraEra) Word32
sizeTxF)
      SpecTransM DijkstraEra () (() -> Maybe Integer -> TxSub)
-> SpecTransM DijkstraEra () ()
-> SpecTransM DijkstraEra () (Maybe Integer -> TxSub)
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
<*> () -> SpecTransM DijkstraEra () ()
forall a. a -> SpecTransM DijkstraEra () a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
      SpecTransM DijkstraEra () (Maybe Integer -> TxSub)
-> SpecTransM DijkstraEra () (Maybe Integer)
-> SpecTransM DijkstraEra () TxSub
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
<*> StrictMaybe (AlonzoTxAuxData DijkstraEra)
-> SpecTransM
     DijkstraEra
     (SpecContext
        DijkstraEra (StrictMaybe (AlonzoTxAuxData DijkstraEra)))
     (SpecRep DijkstraEra (StrictMaybe (AlonzoTxAuxData DijkstraEra)))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep (Tx SubTx DijkstraEra
tx Tx SubTx DijkstraEra
-> Getting
     (StrictMaybe (AlonzoTxAuxData DijkstraEra))
     (Tx SubTx DijkstraEra)
     (StrictMaybe (AlonzoTxAuxData DijkstraEra))
-> StrictMaybe (AlonzoTxAuxData DijkstraEra)
forall s a. s -> Getting a s a -> a
^. (StrictMaybe (TxAuxData DijkstraEra)
 -> Const
      (StrictMaybe (AlonzoTxAuxData DijkstraEra))
      (StrictMaybe (TxAuxData DijkstraEra)))
-> Tx SubTx DijkstraEra
-> Const
     (StrictMaybe (AlonzoTxAuxData DijkstraEra)) (Tx SubTx DijkstraEra)
Getting
  (StrictMaybe (AlonzoTxAuxData DijkstraEra))
  (Tx SubTx DijkstraEra)
  (StrictMaybe (AlonzoTxAuxData DijkstraEra))
forall era (l :: TxLevel).
EraTx era =>
Lens' (Tx l era) (StrictMaybe (TxAuxData era))
forall (l :: TxLevel).
Lens' (Tx l DijkstraEra) (StrictMaybe (TxAuxData DijkstraEra))
auxDataTxL)

instance SpecTranslate DijkstraEra (DijkstraStAnnTx TopTx DijkstraEra) where
  type SpecRep DijkstraEra (DijkstraStAnnTx TopTx DijkstraEra) = Agda.TxTop

  toSpecRep :: DijkstraStAnnTx TopTx DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (DijkstraStAnnTx TopTx DijkstraEra))
     (SpecRep DijkstraEra (DijkstraStAnnTx TopTx DijkstraEra))
toSpecRep DijkstraStAnnTx TopTx DijkstraEra
stAnnTx = Tx TopTx DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (Tx TopTx DijkstraEra))
     (SpecRep DijkstraEra (Tx TopTx DijkstraEra))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep (DijkstraStAnnTx TopTx DijkstraEra
stAnnTx DijkstraStAnnTx TopTx DijkstraEra
-> Getting
     (Tx TopTx DijkstraEra)
     (DijkstraStAnnTx TopTx DijkstraEra)
     (Tx TopTx DijkstraEra)
-> Tx TopTx DijkstraEra
forall s a. s -> Getting a s a -> a
^. forall era (l :: TxLevel).
EraTx era =>
SimpleGetter (StAnnTx l era) (Tx l era)
txStAnnTxG @DijkstraEra)