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

module Test.Cardano.Ledger.Conformance.ExecSpecRule.Dijkstra.Ledger (DijkstraLedgerExecContext (..)) where

import Cardano.Ledger.Alonzo.Plutus.Context (ContextError)
import Cardano.Ledger.Alonzo.Scripts (AsItem)
import Cardano.Ledger.Alonzo.Tx (AlonzoEraTx)
import Cardano.Ledger.BaseTypes (Globals (networkId), Network, StrictMaybe)
import Cardano.Ledger.Binary (EncCBOR (..))
import Cardano.Ledger.Binary.Coders (Encode (..), encode, (!>))
import Cardano.Ledger.Conway.Core (
  EraPParams (..),
  EraTx (..),
  EraTxAuxData (..),
  EraTxBody (..),
  EraTxOut (..),
  EraTxWits (..),
  PlutusPurpose,
  ScriptHash,
  SubTx,
  TxCert,
  TxLevel (..),
 )
import Cardano.Ledger.Conway.Governance
import qualified Cardano.Ledger.Conway.Rules as Conway
import Cardano.Ledger.Dijkstra (DijkstraEra)
import Cardano.Ledger.Dijkstra.Tx (DijkstraStAnnTx (..))
import Cardano.Ledger.Shelley.LedgerState
import qualified Cardano.Ledger.Shelley.Rules as Shelley
import Cardano.Ledger.State (ScriptsNeeded, ScriptsProvided)
import Control.DeepSeq (deepseq, rnf)
import Control.State.Transition.Extended (TRC (..))
import Data.Functor.Identity (Identity)
import qualified Data.TreeDiff.OMap as OMap
import GHC.Generics (Generic)
import Lens.Micro
import qualified MAlonzo.Code.Ledger.Dijkstra.Foreign.API as Agda
import qualified Test.Cardano.Ledger.Binary.TreeDiff as TD
import Test.Cardano.Ledger.Common (NFData, ToExpr (..))
import Test.Cardano.Ledger.Conformance (withSpecTransM)
import Test.Cardano.Ledger.Conformance.ExecSpecRule.Core (
  ExecSpecRule (..),
  ExecSpecTopLevelRule (..),
  SpecTRC (..),
  runFromAgdaFunction,
 )
import Test.Cardano.Ledger.Conformance.SpecTranslate.Base (
  SpecTranslate (..),
  askSpecTransM,
  withCtxSpecTransM,
 )
import Test.Cardano.Ledger.Conformance.SpecTranslate.Dijkstra ()
import Test.Cardano.Ledger.Constrained.Conway (UtxoExecContext (..))
import Test.Cardano.Ledger.Dijkstra.Arbitrary ()
import Test.Cardano.Ledger.Dijkstra.ImpTest ()

data DijkstraLedgerExecContext era
  = DijkstraLedgerExecContext
  { forall era. DijkstraLedgerExecContext era -> StrictMaybe ScriptHash
dlecGuardrailsScriptHash :: StrictMaybe ScriptHash
  , forall era. DijkstraLedgerExecContext era -> EnactState era
dlecEnactState :: Conway.EnactState era
  , forall era. DijkstraLedgerExecContext era -> UtxoExecContext era
dlecUtxoExecContext :: UtxoExecContext era
  , forall era. DijkstraLedgerExecContext era -> Network
dlecNetworkId :: Network
  }
  deriving ((forall x.
 DijkstraLedgerExecContext era
 -> Rep (DijkstraLedgerExecContext era) x)
-> (forall x.
    Rep (DijkstraLedgerExecContext era) x
    -> DijkstraLedgerExecContext era)
-> Generic (DijkstraLedgerExecContext era)
forall x.
Rep (DijkstraLedgerExecContext era) x
-> DijkstraLedgerExecContext era
forall x.
DijkstraLedgerExecContext era
-> Rep (DijkstraLedgerExecContext era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (DijkstraLedgerExecContext era) x
-> DijkstraLedgerExecContext era
forall era x.
DijkstraLedgerExecContext era
-> Rep (DijkstraLedgerExecContext era) x
$cfrom :: forall era x.
DijkstraLedgerExecContext era
-> Rep (DijkstraLedgerExecContext era) x
from :: forall x.
DijkstraLedgerExecContext era
-> Rep (DijkstraLedgerExecContext era) x
$cto :: forall era x.
Rep (DijkstraLedgerExecContext era) x
-> DijkstraLedgerExecContext era
to :: forall x.
Rep (DijkstraLedgerExecContext era) x
-> DijkstraLedgerExecContext era
Generic)

instance
  ( EraPParams era
  , EraTx era
  , NFData (TxWits era)
  , NFData (TxAuxData era)
  , EraCertState era
  ) =>
  NFData (DijkstraLedgerExecContext era)

instance
  ( EraTx era
  , ToExpr (Tx TopTx era)
  , ToExpr (TxOut era)
  , ToExpr (TxBody TopTx era)
  , ToExpr (TxWits era)
  , ToExpr (TxAuxData era)
  , ToExpr (PParamsHKD Identity era)
  , EraCertState era
  , ToExpr (CertState era)
  ) =>
  ToExpr (DijkstraLedgerExecContext era)

instance
  ( EraPParams era
  , EraCertState era
  , EncCBOR (TxOut era)
  , EncCBOR (Tx TopTx era)
  ) =>
  EncCBOR (DijkstraLedgerExecContext era)
  where
  encCBOR :: DijkstraLedgerExecContext era -> Encoding
encCBOR DijkstraLedgerExecContext {StrictMaybe ScriptHash
EnactState era
Network
UtxoExecContext era
dlecGuardrailsScriptHash :: forall era. DijkstraLedgerExecContext era -> StrictMaybe ScriptHash
dlecEnactState :: forall era. DijkstraLedgerExecContext era -> EnactState era
dlecUtxoExecContext :: forall era. DijkstraLedgerExecContext era -> UtxoExecContext era
dlecNetworkId :: forall era. DijkstraLedgerExecContext era -> Network
dlecGuardrailsScriptHash :: StrictMaybe ScriptHash
dlecEnactState :: EnactState era
dlecUtxoExecContext :: UtxoExecContext era
dlecNetworkId :: Network
..} =
    Encode (Closed Dense) (DijkstraLedgerExecContext era) -> Encoding
forall (w :: Wrapped) t. Encode w t -> Encoding
encode (Encode (Closed Dense) (DijkstraLedgerExecContext era) -> Encoding)
-> Encode (Closed Dense) (DijkstraLedgerExecContext era)
-> Encoding
forall a b. (a -> b) -> a -> b
$
      (StrictMaybe ScriptHash
 -> EnactState era
 -> UtxoExecContext era
 -> Network
 -> DijkstraLedgerExecContext era)
-> Encode
     (Closed Dense)
     (StrictMaybe ScriptHash
      -> EnactState era
      -> UtxoExecContext era
      -> Network
      -> DijkstraLedgerExecContext era)
forall t. t -> Encode (Closed Dense) t
Rec StrictMaybe ScriptHash
-> EnactState era
-> UtxoExecContext era
-> Network
-> DijkstraLedgerExecContext era
forall era.
StrictMaybe ScriptHash
-> EnactState era
-> UtxoExecContext era
-> Network
-> DijkstraLedgerExecContext era
DijkstraLedgerExecContext
        Encode
  (Closed Dense)
  (StrictMaybe ScriptHash
   -> EnactState era
   -> UtxoExecContext era
   -> Network
   -> DijkstraLedgerExecContext era)
-> Encode (Closed Dense) (StrictMaybe ScriptHash)
-> Encode
     (Closed Dense)
     (EnactState era
      -> UtxoExecContext era -> Network -> DijkstraLedgerExecContext era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode (Closed r) a -> Encode w t
!> StrictMaybe ScriptHash
-> Encode (Closed Dense) (StrictMaybe ScriptHash)
forall t. EncCBOR t => t -> Encode (Closed Dense) t
To StrictMaybe ScriptHash
dlecGuardrailsScriptHash
        Encode
  (Closed Dense)
  (EnactState era
   -> UtxoExecContext era -> Network -> DijkstraLedgerExecContext era)
-> Encode (Closed Dense) (EnactState era)
-> Encode
     (Closed Dense)
     (UtxoExecContext era -> Network -> DijkstraLedgerExecContext era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode (Closed r) a -> Encode w t
!> EnactState era -> Encode (Closed Dense) (EnactState era)
forall t. EncCBOR t => t -> Encode (Closed Dense) t
To EnactState era
dlecEnactState
        Encode
  (Closed Dense)
  (UtxoExecContext era -> Network -> DijkstraLedgerExecContext era)
-> Encode (Closed Dense) (UtxoExecContext era)
-> Encode (Closed Dense) (Network -> DijkstraLedgerExecContext era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode (Closed r) a -> Encode w t
!> UtxoExecContext era -> Encode (Closed Dense) (UtxoExecContext era)
forall t. EncCBOR t => t -> Encode (Closed Dense) t
To UtxoExecContext era
dlecUtxoExecContext
        Encode (Closed Dense) (Network -> DijkstraLedgerExecContext era)
-> Encode (Closed Dense) Network
-> Encode (Closed Dense) (DijkstraLedgerExecContext era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode (Closed r) a -> Encode w t
!> Network -> Encode (Closed Dense) Network
forall t. EncCBOR t => t -> Encode (Closed Dense) t
To Network
dlecNetworkId

-- | Note: 'TxInfoResult' is forced only to WHNF since it contains thunks/functions
-- (via 'PlutusTxInfoResult') that cannot be fully evaluated.
instance
  ( AlonzoEraTx era
  , NFData (Tx TopTx era)
  , NFData (Tx SubTx era)
  , NFData (ScriptsNeeded era)
  , NFData (ScriptsProvided era)
  , NFData (ContextError era)
  ) =>
  NFData (DijkstraStAnnTx TopTx era)
  where
  rnf :: DijkstraStAnnTx TopTx era -> ()
rnf stAnnTx :: DijkstraStAnnTx TopTx era
stAnnTx@(DijkstraStAnnTopTx Tx TopTx era
_ ProtVer
_ ScriptsNeeded era
_ ScriptsProvided era
_ Bool
_ Set Language
_ Either (NonEmpty (CollectError era)) [PlutusWithContext]
_ [DijkstraStAnnTx SubTx era]
_) =
    let DijkstraStAnnTopTx {Bool
[DijkstraStAnnTx SubTx era]
Either (NonEmpty (CollectError era)) [PlutusWithContext]
Set Language
Tx TopTx era
ScriptsNeeded era
ScriptsProvided era
ProtVer
dsattTx :: Tx TopTx era
dsattProtocolVersion :: ProtVer
dsattScriptsNeeded :: ScriptsNeeded era
dsattScriptsProvided :: ScriptsProvided era
dsattPlutusLegacyMode :: Bool
dsattPlutusLanguagesUsed :: Set Language
dsattPlutusScriptsWithContext :: Either (NonEmpty (CollectError era)) [PlutusWithContext]
dsattSubTransactions :: [DijkstraStAnnTx SubTx era]
dsattSubTransactions :: forall era.
DijkstraStAnnTx TopTx era -> [DijkstraStAnnTx SubTx era]
dsattPlutusScriptsWithContext :: forall era.
DijkstraStAnnTx TopTx era
-> Either (NonEmpty (CollectError era)) [PlutusWithContext]
dsattPlutusLanguagesUsed :: forall era. DijkstraStAnnTx TopTx era -> Set Language
dsattPlutusLegacyMode :: forall era. DijkstraStAnnTx TopTx era -> Bool
dsattScriptsProvided :: forall era. DijkstraStAnnTx TopTx era -> ScriptsProvided era
dsattScriptsNeeded :: forall era. DijkstraStAnnTx TopTx era -> ScriptsNeeded era
dsattProtocolVersion :: forall era. DijkstraStAnnTx TopTx era -> ProtVer
dsattTx :: forall era. DijkstraStAnnTx TopTx era -> Tx TopTx era
..} = DijkstraStAnnTx TopTx era
stAnnTx
     in Tx TopTx era
dsattTx Tx TopTx era -> () -> ()
forall a b. NFData a => a -> b -> b
`deepseq`
          ProtVer
dsattProtocolVersion ProtVer -> () -> ()
forall a b. NFData a => a -> b -> b
`deepseq`
            ScriptsNeeded era
dsattScriptsNeeded ScriptsNeeded era -> () -> ()
forall a b. NFData a => a -> b -> b
`deepseq`
              ScriptsProvided era
dsattScriptsProvided ScriptsProvided era -> () -> ()
forall a b. NFData a => a -> b -> b
`deepseq`
                Bool
dsattPlutusLegacyMode Bool -> () -> ()
forall a b. NFData a => a -> b -> b
`deepseq`
                  Set Language
dsattPlutusLanguagesUsed Set Language -> () -> ()
forall a b. NFData a => a -> b -> b
`deepseq`
                    Either (NonEmpty (CollectError era)) [PlutusWithContext]
dsattPlutusScriptsWithContext Either (NonEmpty (CollectError era)) [PlutusWithContext]
-> () -> ()
forall a b. NFData a => a -> b -> b
`deepseq`
                      [DijkstraStAnnTx SubTx era] -> ()
forall a. NFData a => a -> ()
rnf [DijkstraStAnnTx SubTx era]
dsattSubTransactions

instance
  ( AlonzoEraTx era
  , NFData (Tx SubTx era)
  , NFData (ScriptsNeeded era)
  , NFData (ScriptsProvided era)
  , NFData (ContextError era)
  ) =>
  NFData (DijkstraStAnnTx SubTx era)
  where
  rnf :: DijkstraStAnnTx SubTx era -> ()
rnf stAnnTx :: DijkstraStAnnTx SubTx era
stAnnTx@(DijkstraStAnnSubTx Tx SubTx era
_ ScriptsNeeded era
_ ScriptsProvided era
_ TxInfoResult era
_ Set Language
_ Either (NonEmpty (CollectError era)) [PlutusWithContext]
_) =
    let DijkstraStAnnSubTx {Either (NonEmpty (CollectError era)) [PlutusWithContext]
Set Language
Tx SubTx era
ScriptsNeeded era
ScriptsProvided era
TxInfoResult era
dsastTx :: Tx SubTx era
dsastScriptsNeeded :: ScriptsNeeded era
dsastScriptsProvided :: ScriptsProvided era
dsastTxInfoResult :: TxInfoResult era
dsastPlutusLanguagesUsed :: Set Language
dsastPlutusScriptsWithContext :: Either (NonEmpty (CollectError era)) [PlutusWithContext]
dsastPlutusScriptsWithContext :: forall era.
DijkstraStAnnTx SubTx era
-> Either (NonEmpty (CollectError era)) [PlutusWithContext]
dsastPlutusLanguagesUsed :: forall era. DijkstraStAnnTx SubTx era -> Set Language
dsastTxInfoResult :: forall era. DijkstraStAnnTx SubTx era -> TxInfoResult era
dsastScriptsProvided :: forall era. DijkstraStAnnTx SubTx era -> ScriptsProvided era
dsastScriptsNeeded :: forall era. DijkstraStAnnTx SubTx era -> ScriptsNeeded era
dsastTx :: forall era. DijkstraStAnnTx SubTx era -> Tx SubTx era
..} = DijkstraStAnnTx SubTx era
stAnnTx
     in Tx SubTx era
dsastTx Tx SubTx era -> () -> ()
forall a b. NFData a => a -> b -> b
`deepseq`
          ScriptsNeeded era
dsastScriptsNeeded ScriptsNeeded era -> () -> ()
forall a b. NFData a => a -> b -> b
`deepseq`
            ScriptsProvided era
dsastScriptsProvided ScriptsProvided era -> () -> ()
forall a b. NFData a => a -> b -> b
`deepseq`
              TxInfoResult era
dsastTxInfoResult TxInfoResult era -> () -> ()
forall a b. a -> b -> b
`seq`
                Set Language
dsastPlutusLanguagesUsed Set Language -> () -> ()
forall a b. NFData a => a -> b -> b
`deepseq`
                  Either (NonEmpty (CollectError era)) [PlutusWithContext] -> ()
forall a. NFData a => a -> ()
rnf Either (NonEmpty (CollectError era)) [PlutusWithContext]
dsastPlutusScriptsWithContext

instance EncCBOR (Tx TopTx era) => EncCBOR (DijkstraStAnnTx TopTx era) where
  encCBOR :: DijkstraStAnnTx TopTx era -> Encoding
encCBOR DijkstraStAnnTopTx {Tx TopTx era
dsattTx :: forall era. DijkstraStAnnTx TopTx era -> Tx TopTx era
dsattTx :: Tx TopTx era
dsattTx} = Tx TopTx era -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR Tx TopTx era
dsattTx

instance
  ( ToExpr (Tx TopTx era)
  , ToExpr (Tx SubTx era)
  , ToExpr (ScriptsNeeded era)
  , ToExpr (ScriptsProvided era)
  , ToExpr (ContextError era)
  , ToExpr (PlutusPurpose AsItem era)
  , ToExpr (TxCert era)
  ) =>
  ToExpr (DijkstraStAnnTx TopTx era)
  where
  toExpr :: DijkstraStAnnTx TopTx era -> Expr
toExpr stAnnTx :: DijkstraStAnnTx TopTx era
stAnnTx@(DijkstraStAnnTopTx Tx TopTx era
_ ProtVer
_ ScriptsNeeded era
_ ScriptsProvided era
_ Bool
_ Set Language
_ Either (NonEmpty (CollectError era)) [PlutusWithContext]
_ [DijkstraStAnnTx SubTx era]
_) =
    let DijkstraStAnnTopTx {Bool
[DijkstraStAnnTx SubTx era]
Either (NonEmpty (CollectError era)) [PlutusWithContext]
Set Language
Tx TopTx era
ScriptsNeeded era
ScriptsProvided era
ProtVer
dsattSubTransactions :: forall era.
DijkstraStAnnTx TopTx era -> [DijkstraStAnnTx SubTx era]
dsattPlutusScriptsWithContext :: forall era.
DijkstraStAnnTx TopTx era
-> Either (NonEmpty (CollectError era)) [PlutusWithContext]
dsattPlutusLanguagesUsed :: forall era. DijkstraStAnnTx TopTx era -> Set Language
dsattPlutusLegacyMode :: forall era. DijkstraStAnnTx TopTx era -> Bool
dsattScriptsProvided :: forall era. DijkstraStAnnTx TopTx era -> ScriptsProvided era
dsattScriptsNeeded :: forall era. DijkstraStAnnTx TopTx era -> ScriptsNeeded era
dsattProtocolVersion :: forall era. DijkstraStAnnTx TopTx era -> ProtVer
dsattTx :: forall era. DijkstraStAnnTx TopTx era -> Tx TopTx era
dsattTx :: Tx TopTx era
dsattProtocolVersion :: ProtVer
dsattScriptsNeeded :: ScriptsNeeded era
dsattScriptsProvided :: ScriptsProvided era
dsattPlutusLegacyMode :: Bool
dsattPlutusLanguagesUsed :: Set Language
dsattPlutusScriptsWithContext :: Either (NonEmpty (CollectError era)) [PlutusWithContext]
dsattSubTransactions :: [DijkstraStAnnTx SubTx era]
..} = DijkstraStAnnTx TopTx era
stAnnTx
     in FieldName -> OMap FieldName Expr -> Expr
TD.Rec FieldName
"DijkstraStAnnTopTx" (OMap FieldName Expr -> Expr) -> OMap FieldName Expr -> Expr
forall a b. (a -> b) -> a -> b
$
          [(FieldName, Expr)] -> OMap FieldName Expr
forall k v. Ord k => [(k, v)] -> OMap k v
OMap.fromList
            [ (FieldName
"dsattTx", Tx TopTx era -> Expr
forall a. ToExpr a => a -> Expr
toExpr Tx TopTx era
dsattTx)
            , (FieldName
"dsattProtocolVersion", ProtVer -> Expr
forall a. ToExpr a => a -> Expr
toExpr ProtVer
dsattProtocolVersion)
            , (FieldName
"dsattScriptsNeeded", ScriptsNeeded era -> Expr
forall a. ToExpr a => a -> Expr
toExpr ScriptsNeeded era
dsattScriptsNeeded)
            , (FieldName
"dsattScriptsProvided", ScriptsProvided era -> Expr
forall a. ToExpr a => a -> Expr
toExpr ScriptsProvided era
dsattScriptsProvided)
            , (FieldName
"dsattPlutusLegacyMode", Bool -> Expr
forall a. ToExpr a => a -> Expr
toExpr Bool
dsattPlutusLegacyMode)
            , (FieldName
"dsattPlutusLanguagesUsed", Set Language -> Expr
forall a. ToExpr a => a -> Expr
toExpr Set Language
dsattPlutusLanguagesUsed)
            , (FieldName
"dsattPlutusScriptsWithContext", Either (NonEmpty (CollectError era)) [PlutusWithContext] -> Expr
forall a. ToExpr a => a -> Expr
toExpr Either (NonEmpty (CollectError era)) [PlutusWithContext]
dsattPlutusScriptsWithContext)
            , (FieldName
"dsattSubTransactions", [DijkstraStAnnTx SubTx era] -> Expr
forall a. ToExpr a => a -> Expr
toExpr [DijkstraStAnnTx SubTx era]
dsattSubTransactions)
            ]

-- | Note: 'dsastTxInfoResult' renders as a placeholder since 'TxInfoResult'
-- contains functions that cannot be turned into 'Expr'.
instance
  ( ToExpr (Tx SubTx era)
  , ToExpr (ScriptsNeeded era)
  , ToExpr (ScriptsProvided era)
  , ToExpr (ContextError era)
  , ToExpr (PlutusPurpose AsItem era)
  , ToExpr (TxCert era)
  ) =>
  ToExpr (DijkstraStAnnTx SubTx era)
  where
  toExpr :: DijkstraStAnnTx SubTx era -> Expr
toExpr stAnnTx :: DijkstraStAnnTx SubTx era
stAnnTx@(DijkstraStAnnSubTx Tx SubTx era
_ ScriptsNeeded era
_ ScriptsProvided era
_ TxInfoResult era
_ Set Language
_ Either (NonEmpty (CollectError era)) [PlutusWithContext]
_) =
    let DijkstraStAnnSubTx {Either (NonEmpty (CollectError era)) [PlutusWithContext]
Set Language
Tx SubTx era
ScriptsNeeded era
ScriptsProvided era
TxInfoResult era
dsastPlutusScriptsWithContext :: forall era.
DijkstraStAnnTx SubTx era
-> Either (NonEmpty (CollectError era)) [PlutusWithContext]
dsastPlutusLanguagesUsed :: forall era. DijkstraStAnnTx SubTx era -> Set Language
dsastTxInfoResult :: forall era. DijkstraStAnnTx SubTx era -> TxInfoResult era
dsastScriptsProvided :: forall era. DijkstraStAnnTx SubTx era -> ScriptsProvided era
dsastScriptsNeeded :: forall era. DijkstraStAnnTx SubTx era -> ScriptsNeeded era
dsastTx :: forall era. DijkstraStAnnTx SubTx era -> Tx SubTx era
dsastTx :: Tx SubTx era
dsastScriptsNeeded :: ScriptsNeeded era
dsastScriptsProvided :: ScriptsProvided era
dsastTxInfoResult :: TxInfoResult era
dsastPlutusLanguagesUsed :: Set Language
dsastPlutusScriptsWithContext :: Either (NonEmpty (CollectError era)) [PlutusWithContext]
..} = DijkstraStAnnTx SubTx era
stAnnTx
     in FieldName -> OMap FieldName Expr -> Expr
TD.Rec FieldName
"DijkstraStAnnSubTx" (OMap FieldName Expr -> Expr) -> OMap FieldName Expr -> Expr
forall a b. (a -> b) -> a -> b
$
          [(FieldName, Expr)] -> OMap FieldName Expr
forall k v. Ord k => [(k, v)] -> OMap k v
OMap.fromList
            [ (FieldName
"dsastTx", Tx SubTx era -> Expr
forall a. ToExpr a => a -> Expr
toExpr Tx SubTx era
dsastTx)
            , (FieldName
"dsastScriptsNeeded", ScriptsNeeded era -> Expr
forall a. ToExpr a => a -> Expr
toExpr ScriptsNeeded era
dsastScriptsNeeded)
            , (FieldName
"dsastScriptsProvided", ScriptsProvided era -> Expr
forall a. ToExpr a => a -> Expr
toExpr ScriptsProvided era
dsastScriptsProvided)
            , (FieldName
"dsastTxInfoResult", FieldName -> [Expr] -> Expr
TD.App FieldName
"<TxInfoResult>" [])
            , (FieldName
"dsastPlutusLanguagesUsed", Set Language -> Expr
forall a. ToExpr a => a -> Expr
toExpr Set Language
dsastPlutusLanguagesUsed)
            , (FieldName
"dsastPlutusScriptsWithContext", Either (NonEmpty (CollectError era)) [PlutusWithContext] -> Expr
forall a. ToExpr a => a -> Expr
toExpr Either (NonEmpty (CollectError era)) [PlutusWithContext]
dsastPlutusScriptsWithContext)
            ]

instance ExecSpecRule "LEDGER" DijkstraEra where
  type ExecContext "LEDGER" DijkstraEra = DijkstraLedgerExecContext DijkstraEra

  translateInputs :: HasCallStack =>
TRC (EraRule "LEDGER" DijkstraEra)
-> SpecTransM
     DijkstraEra
     (ExecContext "LEDGER" DijkstraEra)
     (SpecTRC "LEDGER" DijkstraEra)
translateInputs (TRC (Environment (EraRule "LEDGER" DijkstraEra)
env, State (EraRule "LEDGER" DijkstraEra)
st, Signal (EraRule "LEDGER" DijkstraEra)
sig)) = do
    DijkstraLedgerExecContext {..} <- SpecTransM
  DijkstraEra
  (DijkstraLedgerExecContext DijkstraEra)
  (DijkstraLedgerExecContext DijkstraEra)
forall era ctx. SpecTransM era ctx ctx
askSpecTransM
    agdaEnv <- withCtxSpecTransM (dlecGuardrailsScriptHash, dlecEnactState) $ toSpecRep env
    agdaSt <- withCtxSpecTransM dlecNetworkId $ toSpecRep st
    agdaSig <- withCtxSpecTransM () $ toSpecRep sig
    pure $ SpecTRC agdaEnv agdaSt agdaSig

  translateOutput :: TRC (EraRule "LEDGER" DijkstraEra)
-> State (EraRule "LEDGER" DijkstraEra)
-> SpecTransM
     DijkstraEra
     (ExecContext "LEDGER" DijkstraEra)
     (SpecState "LEDGER" DijkstraEra)
translateOutput TRC (EraRule "LEDGER" DijkstraEra)
_ = (DijkstraLedgerExecContext DijkstraEra -> Network)
-> SpecTransM DijkstraEra Network LedgerState
-> SpecTransM
     DijkstraEra (DijkstraLedgerExecContext DijkstraEra) LedgerState
forall ctx ctx' era a.
(ctx -> ctx') -> SpecTransM era ctx' a -> SpecTransM era ctx a
withSpecTransM DijkstraLedgerExecContext DijkstraEra -> Network
forall era. DijkstraLedgerExecContext era -> Network
dlecNetworkId (SpecTransM DijkstraEra Network LedgerState
 -> SpecTransM
      DijkstraEra (DijkstraLedgerExecContext DijkstraEra) LedgerState)
-> (LedgerState DijkstraEra
    -> SpecTransM DijkstraEra Network LedgerState)
-> LedgerState DijkstraEra
-> SpecTransM
     DijkstraEra (DijkstraLedgerExecContext DijkstraEra) LedgerState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LedgerState DijkstraEra
-> SpecTransM DijkstraEra Network LedgerState
LedgerState DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (LedgerState DijkstraEra))
     (SpecRep DijkstraEra (LedgerState DijkstraEra))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep

  runAgdaRule :: HasCallStack =>
SpecTRC "LEDGER" DijkstraEra
-> Either Text (SpecState "LEDGER" DijkstraEra)
runAgdaRule = (SpecEnvironment "LEDGER" DijkstraEra
 -> SpecState "LEDGER" DijkstraEra
 -> SpecSignal "LEDGER" DijkstraEra
 -> ComputationResult Text (SpecState "LEDGER" DijkstraEra))
-> SpecTRC "LEDGER" DijkstraEra
-> Either Text (SpecState "LEDGER" DijkstraEra)
forall (rule :: Symbol) era.
(SpecEnvironment rule era
 -> SpecState rule era
 -> SpecSignal rule era
 -> ComputationResult Text (SpecState rule era))
-> SpecTRC rule era -> Either Text (SpecState rule era)
runFromAgdaFunction LedgerEnv
-> LedgerState
-> TxTop
-> T_HSComputationResult_110 Text LedgerState
SpecEnvironment "LEDGER" DijkstraEra
-> SpecState "LEDGER" DijkstraEra
-> SpecSignal "LEDGER" DijkstraEra
-> ComputationResult Text (SpecState "LEDGER" DijkstraEra)
Agda.ledgerStep

instance ExecSpecTopLevelRule "LEDGER" DijkstraEra where
  mkRuleExecContext :: Globals
-> TRC (EraRule "LEDGER" DijkstraEra)
-> ExecContext "LEDGER" DijkstraEra
mkRuleExecContext Globals
globals (TRC (Environment (EraRule "LEDGER" DijkstraEra)
env, State (EraRule "LEDGER" DijkstraEra)
state, Signal (EraRule "LEDGER" DijkstraEra)
signal)) =
    DijkstraLedgerExecContext
      { dlecGuardrailsScriptHash :: StrictMaybe ScriptHash
dlecGuardrailsScriptHash =
          State (EraRule "LEDGER" DijkstraEra)
LedgerState DijkstraEra
state LedgerState DijkstraEra
-> Getting
     (StrictMaybe ScriptHash)
     (LedgerState DijkstraEra)
     (StrictMaybe ScriptHash)
-> StrictMaybe ScriptHash
forall s a. s -> Getting a s a -> a
^. (UTxOState DijkstraEra
 -> Const (StrictMaybe ScriptHash) (UTxOState DijkstraEra))
-> LedgerState DijkstraEra
-> Const (StrictMaybe ScriptHash) (LedgerState DijkstraEra)
forall era (f :: * -> *).
Functor f =>
(UTxOState era -> f (UTxOState era))
-> LedgerState era -> f (LedgerState era)
lsUTxOStateL ((UTxOState DijkstraEra
  -> Const (StrictMaybe ScriptHash) (UTxOState DijkstraEra))
 -> LedgerState DijkstraEra
 -> Const (StrictMaybe ScriptHash) (LedgerState DijkstraEra))
-> ((StrictMaybe ScriptHash
     -> Const (StrictMaybe ScriptHash) (StrictMaybe ScriptHash))
    -> UTxOState DijkstraEra
    -> Const (StrictMaybe ScriptHash) (UTxOState DijkstraEra))
-> Getting
     (StrictMaybe ScriptHash)
     (LedgerState DijkstraEra)
     (StrictMaybe ScriptHash)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (GovState DijkstraEra
 -> Const (StrictMaybe ScriptHash) (GovState DijkstraEra))
-> UTxOState DijkstraEra
-> Const (StrictMaybe ScriptHash) (UTxOState DijkstraEra)
(ConwayGovState DijkstraEra
 -> Const (StrictMaybe ScriptHash) (ConwayGovState DijkstraEra))
-> UTxOState DijkstraEra
-> Const (StrictMaybe ScriptHash) (UTxOState DijkstraEra)
forall era (f :: * -> *).
Functor f =>
(GovState era -> f (GovState era))
-> UTxOState era -> f (UTxOState era)
utxosGovStateL ((ConwayGovState DijkstraEra
  -> Const (StrictMaybe ScriptHash) (ConwayGovState DijkstraEra))
 -> UTxOState DijkstraEra
 -> Const (StrictMaybe ScriptHash) (UTxOState DijkstraEra))
-> ((StrictMaybe ScriptHash
     -> Const (StrictMaybe ScriptHash) (StrictMaybe ScriptHash))
    -> ConwayGovState DijkstraEra
    -> Const (StrictMaybe ScriptHash) (ConwayGovState DijkstraEra))
-> (StrictMaybe ScriptHash
    -> Const (StrictMaybe ScriptHash) (StrictMaybe ScriptHash))
-> UTxOState DijkstraEra
-> Const (StrictMaybe ScriptHash) (UTxOState DijkstraEra)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Constitution DijkstraEra
 -> Const (StrictMaybe ScriptHash) (Constitution DijkstraEra))
-> GovState DijkstraEra
-> Const (StrictMaybe ScriptHash) (GovState DijkstraEra)
(Constitution DijkstraEra
 -> Const (StrictMaybe ScriptHash) (Constitution DijkstraEra))
-> ConwayGovState DijkstraEra
-> Const (StrictMaybe ScriptHash) (ConwayGovState DijkstraEra)
forall era.
ConwayEraGov era =>
Lens' (GovState era) (Constitution era)
Lens' (GovState DijkstraEra) (Constitution DijkstraEra)
constitutionGovStateL ((Constitution DijkstraEra
  -> Const (StrictMaybe ScriptHash) (Constitution DijkstraEra))
 -> ConwayGovState DijkstraEra
 -> Const (StrictMaybe ScriptHash) (ConwayGovState DijkstraEra))
-> ((StrictMaybe ScriptHash
     -> Const (StrictMaybe ScriptHash) (StrictMaybe ScriptHash))
    -> Constitution DijkstraEra
    -> Const (StrictMaybe ScriptHash) (Constitution DijkstraEra))
-> (StrictMaybe ScriptHash
    -> Const (StrictMaybe ScriptHash) (StrictMaybe ScriptHash))
-> ConwayGovState DijkstraEra
-> Const (StrictMaybe ScriptHash) (ConwayGovState DijkstraEra)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (StrictMaybe ScriptHash
 -> Const (StrictMaybe ScriptHash) (StrictMaybe ScriptHash))
-> Constitution DijkstraEra
-> Const (StrictMaybe ScriptHash) (Constitution DijkstraEra)
forall era (f :: * -> *).
Functor f =>
(StrictMaybe ScriptHash -> f (StrictMaybe ScriptHash))
-> Constitution era -> f (Constitution era)
constitutionGuardrailsScriptHashL
      , dlecEnactState :: EnactState DijkstraEra
dlecEnactState = GovState DijkstraEra -> EnactState DijkstraEra
forall era. ConwayEraGov era => GovState era -> EnactState era
mkEnactState (GovState DijkstraEra -> EnactState DijkstraEra)
-> GovState DijkstraEra -> EnactState DijkstraEra
forall a b. (a -> b) -> a -> b
$ State (EraRule "LEDGER" DijkstraEra)
LedgerState DijkstraEra
state LedgerState DijkstraEra
-> Getting
     (GovState DijkstraEra)
     (LedgerState DijkstraEra)
     (GovState DijkstraEra)
-> GovState DijkstraEra
forall s a. s -> Getting a s a -> a
^. (UTxOState DijkstraEra
 -> Const (GovState DijkstraEra) (UTxOState DijkstraEra))
-> LedgerState DijkstraEra
-> Const (GovState DijkstraEra) (LedgerState DijkstraEra)
forall era (f :: * -> *).
Functor f =>
(UTxOState era -> f (UTxOState era))
-> LedgerState era -> f (LedgerState era)
lsUTxOStateL ((UTxOState DijkstraEra
  -> Const (GovState DijkstraEra) (UTxOState DijkstraEra))
 -> LedgerState DijkstraEra
 -> Const (GovState DijkstraEra) (LedgerState DijkstraEra))
-> ((GovState DijkstraEra
     -> Const (GovState DijkstraEra) (GovState DijkstraEra))
    -> UTxOState DijkstraEra
    -> Const (GovState DijkstraEra) (UTxOState DijkstraEra))
-> Getting
     (GovState DijkstraEra)
     (LedgerState DijkstraEra)
     (GovState DijkstraEra)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (GovState DijkstraEra
 -> Const (GovState DijkstraEra) (GovState DijkstraEra))
-> UTxOState DijkstraEra
-> Const (GovState DijkstraEra) (UTxOState DijkstraEra)
forall era (f :: * -> *).
Functor f =>
(GovState era -> f (GovState era))
-> UTxOState era -> f (UTxOState era)
utxosGovStateL
      , dlecUtxoExecContext :: UtxoExecContext DijkstraEra
dlecUtxoExecContext =
          UtxoExecContext
            { uecTx :: Tx TopTx DijkstraEra
uecTx = DijkstraStAnnTx TopTx DijkstraEra
Signal (EraRule "LEDGER" DijkstraEra)
signal 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
^. Getting
  (Tx TopTx DijkstraEra)
  (StAnnTx TopTx DijkstraEra)
  (Tx TopTx DijkstraEra)
Getting
  (Tx TopTx DijkstraEra)
  (DijkstraStAnnTx TopTx DijkstraEra)
  (Tx TopTx DijkstraEra)
forall era (l :: TxLevel).
EraTx era =>
SimpleGetter (StAnnTx l era) (Tx l era)
forall (l :: TxLevel).
SimpleGetter (StAnnTx l DijkstraEra) (Tx l DijkstraEra)
txStAnnTxG
            , uecUTxO :: UTxO DijkstraEra
uecUTxO = State (EraRule "LEDGER" DijkstraEra)
LedgerState DijkstraEra
state LedgerState DijkstraEra
-> Getting
     (UTxO DijkstraEra) (LedgerState DijkstraEra) (UTxO DijkstraEra)
-> UTxO DijkstraEra
forall s a. s -> Getting a s a -> a
^. Getting
  (UTxO DijkstraEra) (LedgerState DijkstraEra) (UTxO DijkstraEra)
forall era. Lens' (LedgerState era) (UTxO era)
forall (t :: * -> *) era. CanSetUTxO t => Lens' (t era) (UTxO era)
utxoL
            , uecUtxoEnv :: UtxoEnv DijkstraEra
uecUtxoEnv =
                Shelley.UtxoEnv
                  { ueSlot :: SlotNo
Shelley.ueSlot = LedgerEnv DijkstraEra
Environment (EraRule "LEDGER" DijkstraEra)
env LedgerEnv DijkstraEra
-> Getting SlotNo (LedgerEnv DijkstraEra) SlotNo -> SlotNo
forall s a. s -> Getting a s a -> a
^. Getting SlotNo (LedgerEnv DijkstraEra) SlotNo
forall era (f :: * -> *).
Functor f =>
(SlotNo -> f SlotNo) -> LedgerEnv era -> f (LedgerEnv era)
Shelley.ledgerSlotNoL
                  , uePParams :: PParams DijkstraEra
Shelley.uePParams = State (EraRule "LEDGER" DijkstraEra)
LedgerState DijkstraEra
state LedgerState DijkstraEra
-> Getting
     (PParams DijkstraEra)
     (LedgerState DijkstraEra)
     (PParams DijkstraEra)
-> PParams DijkstraEra
forall s a. s -> Getting a s a -> a
^. (UTxOState DijkstraEra
 -> Const (PParams DijkstraEra) (UTxOState DijkstraEra))
-> LedgerState DijkstraEra
-> Const (PParams DijkstraEra) (LedgerState DijkstraEra)
forall era (f :: * -> *).
Functor f =>
(UTxOState era -> f (UTxOState era))
-> LedgerState era -> f (LedgerState era)
lsUTxOStateL ((UTxOState DijkstraEra
  -> Const (PParams DijkstraEra) (UTxOState DijkstraEra))
 -> LedgerState DijkstraEra
 -> Const (PParams DijkstraEra) (LedgerState DijkstraEra))
-> ((PParams DijkstraEra
     -> Const (PParams DijkstraEra) (PParams DijkstraEra))
    -> UTxOState DijkstraEra
    -> Const (PParams DijkstraEra) (UTxOState DijkstraEra))
-> Getting
     (PParams DijkstraEra)
     (LedgerState DijkstraEra)
     (PParams DijkstraEra)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (GovState DijkstraEra
 -> Const (PParams DijkstraEra) (GovState DijkstraEra))
-> UTxOState DijkstraEra
-> Const (PParams DijkstraEra) (UTxOState DijkstraEra)
(ConwayGovState DijkstraEra
 -> Const (PParams DijkstraEra) (ConwayGovState DijkstraEra))
-> UTxOState DijkstraEra
-> Const (PParams DijkstraEra) (UTxOState DijkstraEra)
forall era (f :: * -> *).
Functor f =>
(GovState era -> f (GovState era))
-> UTxOState era -> f (UTxOState era)
utxosGovStateL ((ConwayGovState DijkstraEra
  -> Const (PParams DijkstraEra) (ConwayGovState DijkstraEra))
 -> UTxOState DijkstraEra
 -> Const (PParams DijkstraEra) (UTxOState DijkstraEra))
-> ((PParams DijkstraEra
     -> Const (PParams DijkstraEra) (PParams DijkstraEra))
    -> ConwayGovState DijkstraEra
    -> Const (PParams DijkstraEra) (ConwayGovState DijkstraEra))
-> (PParams DijkstraEra
    -> Const (PParams DijkstraEra) (PParams DijkstraEra))
-> UTxOState DijkstraEra
-> Const (PParams DijkstraEra) (UTxOState DijkstraEra)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PParams DijkstraEra
 -> Const (PParams DijkstraEra) (PParams DijkstraEra))
-> GovState DijkstraEra
-> Const (PParams DijkstraEra) (GovState DijkstraEra)
(PParams DijkstraEra
 -> Const (PParams DijkstraEra) (PParams DijkstraEra))
-> ConwayGovState DijkstraEra
-> Const (PParams DijkstraEra) (ConwayGovState DijkstraEra)
forall era. EraGov era => Lens' (GovState era) (PParams era)
Lens' (GovState DijkstraEra) (PParams DijkstraEra)
curPParamsGovStateL
                  , ueCertState :: CertState DijkstraEra
Shelley.ueCertState = State (EraRule "LEDGER" DijkstraEra)
LedgerState DijkstraEra
state LedgerState DijkstraEra
-> Getting
     (ConwayCertState DijkstraEra)
     (LedgerState DijkstraEra)
     (ConwayCertState DijkstraEra)
-> ConwayCertState DijkstraEra
forall s a. s -> Getting a s a -> a
^. (CertState DijkstraEra
 -> Const (ConwayCertState DijkstraEra) (CertState DijkstraEra))
-> LedgerState DijkstraEra
-> Const (ConwayCertState DijkstraEra) (LedgerState DijkstraEra)
Getting
  (ConwayCertState DijkstraEra)
  (LedgerState DijkstraEra)
  (ConwayCertState DijkstraEra)
forall era (f :: * -> *).
Functor f =>
(CertState era -> f (CertState era))
-> LedgerState era -> f (LedgerState era)
lsCertStateL
                  }
            }
      , dlecNetworkId :: Network
dlecNetworkId = Globals -> Network
networkId Globals
globals
      }