{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Test.Cardano.Ledger.Conformance.SpecTranslate.Dijkstra.Base (
  committeeCredentialToStrictMaybe,
  SpecTranslate (..),
) where

import Cardano.Ledger.Address (
  DirectDeposits (..),
  accountAddressCredentialL,
 )
import Cardano.Ledger.Allegra.Scripts (
  pattern RequireTimeExpire,
  pattern RequireTimeStart,
 )
import Cardano.Ledger.Alonzo (AlonzoTxAuxData, MaryValue)
import Cardano.Ledger.Alonzo.PParams (OrdExUnits (OrdExUnits))
import Cardano.Ledger.Alonzo.Scripts (plutusScriptLanguage)
import Cardano.Ledger.Alonzo.TxWits (AlonzoTxWits (..), Redeemers (..), TxDats (..), unTxDats)
import Cardano.Ledger.Babbage.TxOut (BabbageTxOut (..))
import Cardano.Ledger.BaseTypes
import Cardano.Ledger.Coin (Coin (..))
import Cardano.Ledger.Conway.Core
import Cardano.Ledger.Conway.Governance
import Cardano.Ledger.Conway.PParams (ConwayEraPParams (..), THKD (..))
import qualified Cardano.Ledger.Conway.Rules as Conway
import Cardano.Ledger.Conway.Scripts (AlonzoScript (..))
import Cardano.Ledger.Conway.State
import Cardano.Ledger.Credential (Credential (..))
import Cardano.Ledger.Dijkstra (DijkstraEra)
import Cardano.Ledger.Dijkstra.PParams (DijkstraPParams (..))
import Cardano.Ledger.Dijkstra.Scripts (
  AccountBalanceInterval (..),
  AccountBalanceIntervals (..),
  DijkstraNativeScript,
  DijkstraPlutusPurpose (..),
  pattern RequireGuard,
 )
import Cardano.Ledger.HKD (HKD)
import Cardano.Ledger.Plutus.CostModels (CostModels, costModelsValid)
import Cardano.Ledger.Plutus.Data (BinaryData, Data, Datum (..), hashBinaryData)
import Cardano.Ledger.Plutus.ExUnits (ExUnits (..))
import Cardano.Ledger.Plutus.Language (Language (..))
import Cardano.Ledger.Shelley.Scripts (
  pattern RequireAllOf,
  pattern RequireAnyOf,
  pattern RequireMOf,
  pattern RequireSignature,
 )
import Cardano.Ledger.TxIn (TxId (..), TxIn (..))
import Cardano.Ledger.Val (Val (..))
import Control.Monad.Except (MonadError (..))
import Data.Default (Default (..))
import Data.Foldable (Foldable (..))
import Data.Functor.Identity (Identity)
import Data.List (sortOn)
import qualified Data.Map.Strict as Map
import Data.OMap.Strict (OMap)
import qualified Data.Set as Set
import qualified Data.Text as T
import Data.Traversable (forM)
import qualified GHC.Exts as Exts
import Lens.Micro
import Lens.Micro.Extras (view)
import qualified MAlonzo.Code.Ledger.Dijkstra.Foreign.API as Agda
import Test.Cardano.Ledger.Conformance.Orphans.Core ()
import Test.Cardano.Ledger.Conformance.Orphans.Dijkstra ()
import Test.Cardano.Ledger.Conformance.SpecTranslate.Base
import Test.Cardano.Ledger.Conformance.SpecTranslate.Core (committeeCredentialToStrictMaybe)
import Test.Cardano.Ledger.Conway.TreeDiff (showExpr)
import Test.Cardano.Ledger.Dijkstra.TreeDiff ()

instance SpecTranslate DijkstraEra TxId where
  type SpecRep DijkstraEra TxId = Agda.TxId

  toSpecRep :: TxId
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra TxId)
     (SpecRep DijkstraEra TxId)
toSpecRep (TxId SafeHash EraIndependentTxBody
x) = SafeHash EraIndependentTxBody
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (SafeHash EraIndependentTxBody))
     (SpecRep DijkstraEra (SafeHash EraIndependentTxBody))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep SafeHash EraIndependentTxBody
x

instance SpecTranslate DijkstraEra TxIn where
  type SpecRep DijkstraEra TxIn = Agda.TxIn

  toSpecRep :: TxIn
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra TxIn)
     (SpecRep DijkstraEra TxIn)
toSpecRep (TxIn TxId
txId TxIx
txIx) = (TxId, TxIx)
-> SpecTransM
     DijkstraEra () (SpecRep DijkstraEra TxId, SpecRep DijkstraEra TxIx)
forall era a b ctx.
(SpecTranslate era a, SpecTranslate era b, SpecContext era a ~ ctx,
 SpecContext era b ~ ctx) =>
(a, b) -> SpecTransM era ctx (SpecRep era a, SpecRep era b)
toSpecRepTuple (TxId
txId, TxIx
txIx)

instance SpecTranslate DijkstraEra (SafeHash a) where
  type SpecRep DijkstraEra (SafeHash a) = Agda.DataHash

  toSpecRep :: SafeHash a
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (SafeHash a))
     (SpecRep DijkstraEra (SafeHash a))
toSpecRep = Hash HASH a -> SpecTransM DijkstraEra () Integer
Hash HASH a
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (Hash HASH a))
     (SpecRep DijkstraEra (Hash HASH a))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep (Hash HASH a -> SpecTransM DijkstraEra () Integer)
-> (SafeHash a -> Hash HASH a)
-> SafeHash a
-> SpecTransM DijkstraEra () Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SafeHash a -> Hash HASH a
forall i. SafeHash i -> Hash HASH i
extractHash

instance SpecTranslate DijkstraEra Language where
  type SpecRep DijkstraEra Language = Agda.HSLanguage

  toSpecRep :: Language
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra Language)
     (SpecRep DijkstraEra Language)
toSpecRep Language
l = case Language
l of
    Language
PlutusV1 -> HSLanguage -> SpecTransM DijkstraEra () HSLanguage
forall a. a -> SpecTransM DijkstraEra () a
forall (m :: * -> *) a. Monad m => a -> m a
return HSLanguage
Agda.PV1
    Language
PlutusV2 -> HSLanguage -> SpecTransM DijkstraEra () HSLanguage
forall a. a -> SpecTransM DijkstraEra () a
forall (m :: * -> *) a. Monad m => a -> m a
return HSLanguage
Agda.PV2
    Language
PlutusV3 -> HSLanguage -> SpecTransM DijkstraEra () HSLanguage
forall a. a -> SpecTransM DijkstraEra () a
forall (m :: * -> *) a. Monad m => a -> m a
return HSLanguage
Agda.PV3
    Language
PlutusV4 -> [Char] -> SpecTransM DijkstraEra () HSLanguage
forall a. HasCallStack => [Char] -> a
error [Char]
"PlutusV4 not supported"

instance SpecTranslate DijkstraEra CostModels where
  type SpecRep DijkstraEra CostModels = Agda.LanguageCostModels

  toSpecRep :: CostModels
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra CostModels)
     (SpecRep DijkstraEra CostModels)
toSpecRep CostModels
cm =
    [(HSLanguage, ())] -> LanguageCostModels
Agda.MkLanguageCostModels
      ([(HSLanguage, ())] -> LanguageCostModels)
-> SpecTransM DijkstraEra () [(HSLanguage, ())]
-> SpecTransM DijkstraEra () LanguageCostModels
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Language, CostModel)
 -> SpecTransM DijkstraEra () (HSLanguage, ()))
-> [(Language, CostModel)]
-> SpecTransM DijkstraEra () [(HSLanguage, ())]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\(Language
l, CostModel
_) -> (,()) (HSLanguage -> (HSLanguage, ()))
-> SpecTransM DijkstraEra () HSLanguage
-> SpecTransM DijkstraEra () (HSLanguage, ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Language
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra Language)
     (SpecRep DijkstraEra Language)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep Language
l) (Map Language CostModel -> [(Language, CostModel)]
forall k a. Map k a -> [(k, a)]
Map.toList (CostModels -> Map Language CostModel
costModelsValid CostModels
cm))

instance SpecTranslate DijkstraEra ExUnits where
  type SpecRep DijkstraEra ExUnits = Agda.ExUnits

  toSpecRep :: ExUnits
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra ExUnits)
     (SpecRep DijkstraEra ExUnits)
toSpecRep (ExUnits Natural
a Natural
b) = (Integer, Integer) -> SpecTransM DijkstraEra () (Integer, Integer)
forall a. a -> SpecTransM DijkstraEra () a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
a, Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
b)

instance SpecTranslate DijkstraEra (BinaryData DijkstraEra) where
  type SpecRep DijkstraEra (BinaryData DijkstraEra) = Agda.DataHash

  toSpecRep :: BinaryData DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (BinaryData DijkstraEra))
     (SpecRep DijkstraEra (BinaryData DijkstraEra))
toSpecRep = DataHash -> SpecTransM DijkstraEra () Integer
DataHash
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra DataHash)
     (SpecRep DijkstraEra DataHash)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep (DataHash -> SpecTransM DijkstraEra () Integer)
-> (BinaryData DijkstraEra -> DataHash)
-> BinaryData DijkstraEra
-> SpecTransM DijkstraEra () Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BinaryData DijkstraEra -> DataHash
forall era. BinaryData era -> DataHash
hashBinaryData

instance SpecTranslate DijkstraEra (Datum DijkstraEra) where
  type SpecRep DijkstraEra (Datum DijkstraEra) = Maybe (Either Agda.Datum Agda.DataHash)

  toSpecRep :: Datum DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (Datum DijkstraEra))
     (SpecRep DijkstraEra (Datum DijkstraEra))
toSpecRep Datum DijkstraEra
NoDatum = Maybe (Either Integer Integer)
-> SpecTransM DijkstraEra () (Maybe (Either Integer Integer))
forall a. a -> SpecTransM DijkstraEra () a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Either Integer Integer)
forall a. Maybe a
Nothing
  toSpecRep (Datum BinaryData DijkstraEra
d) = Either Integer Integer -> Maybe (Either Integer Integer)
forall a. a -> Maybe a
Just (Either Integer Integer -> Maybe (Either Integer Integer))
-> (Integer -> Either Integer Integer)
-> Integer
-> Maybe (Either Integer Integer)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Either Integer Integer
forall a b. a -> Either a b
Left (Integer -> Maybe (Either Integer Integer))
-> SpecTransM DijkstraEra () Integer
-> SpecTransM DijkstraEra () (Maybe (Either Integer Integer))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BinaryData DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (BinaryData DijkstraEra))
     (SpecRep DijkstraEra (BinaryData DijkstraEra))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep BinaryData DijkstraEra
d
  toSpecRep (DatumHash DataHash
h) = Either Integer Integer -> Maybe (Either Integer Integer)
forall a. a -> Maybe a
Just (Either Integer Integer -> Maybe (Either Integer Integer))
-> (Integer -> Either Integer Integer)
-> Integer
-> Maybe (Either Integer Integer)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Either Integer Integer
forall a b. b -> Either a b
Right (Integer -> Maybe (Either Integer Integer))
-> SpecTransM DijkstraEra () Integer
-> SpecTransM DijkstraEra () (Maybe (Either Integer Integer))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DataHash
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra DataHash)
     (SpecRep DijkstraEra DataHash)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep DataHash
h

instance SpecTranslate DijkstraEra (Data DijkstraEra) where
  type SpecRep DijkstraEra (Data DijkstraEra) = Agda.DataHash

  toSpecRep :: Data DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (Data DijkstraEra))
     (SpecRep DijkstraEra (Data DijkstraEra))
toSpecRep = DataHash -> SpecTransM DijkstraEra () Integer
DataHash
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra DataHash)
     (SpecRep DijkstraEra DataHash)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep (DataHash -> SpecTransM DijkstraEra () Integer)
-> (Data DijkstraEra -> DataHash)
-> Data DijkstraEra
-> SpecTransM DijkstraEra () Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Data DijkstraEra -> DataHash
forall x i. HashAnnotated x i => x -> SafeHash i
hashAnnotated

instance SpecTranslate DijkstraEra TxAuxDataHash where
  type SpecRep DijkstraEra TxAuxDataHash = Agda.DataHash

  toSpecRep :: TxAuxDataHash
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra TxAuxDataHash)
     (SpecRep DijkstraEra TxAuxDataHash)
toSpecRep (TxAuxDataHash SafeHash EraIndependentTxAuxData
x) = SafeHash EraIndependentTxAuxData
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (SafeHash EraIndependentTxAuxData))
     (SpecRep DijkstraEra (SafeHash EraIndependentTxAuxData))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep SafeHash EraIndependentTxAuxData
x

instance SpecTranslate DijkstraEra (DijkstraNativeScript DijkstraEra) where
  type SpecRep DijkstraEra (DijkstraNativeScript DijkstraEra) = Agda.HSNativeScript

  toSpecRep :: DijkstraNativeScript DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (DijkstraNativeScript DijkstraEra))
     (SpecRep DijkstraEra (DijkstraNativeScript DijkstraEra))
toSpecRep DijkstraNativeScript DijkstraEra
ns =
    NativeScript -> Integer -> Integer -> HSNativeScript
Agda.HSNativeScript
      (NativeScript -> Integer -> Integer -> HSNativeScript)
-> SpecTransM DijkstraEra () NativeScript
-> SpecTransM DijkstraEra () (Integer -> Integer -> HSNativeScript)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NativeScript DijkstraEra -> SpecTransM DijkstraEra () NativeScript
forall {era} {era}.
(Assert
   (OrdCond
      (CmpNat (ProtVerLow era) (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat 0 (ProtVerLow era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat 0 (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 DijkstraEraScript era) =>
NativeScript era -> SpecTransM era () NativeScript
nativeScriptToSpecRep NativeScript DijkstraEra
DijkstraNativeScript DijkstraEra
ns
      SpecTransM DijkstraEra () (Integer -> Integer -> HSNativeScript)
-> SpecTransM DijkstraEra () Integer
-> SpecTransM DijkstraEra () (Integer -> HSNativeScript)
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
<*> ScriptHash
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra ScriptHash)
     (SpecRep DijkstraEra ScriptHash)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep (Script DijkstraEra -> ScriptHash
forall era. EraScript era => Script era -> ScriptHash
hashScript (Script DijkstraEra -> ScriptHash)
-> Script DijkstraEra -> ScriptHash
forall a b. (a -> b) -> a -> b
$ NativeScript DijkstraEra -> AlonzoScript DijkstraEra
forall era. NativeScript era -> AlonzoScript era
NativeScript NativeScript DijkstraEra
DijkstraNativeScript DijkstraEra
ns)
      SpecTransM DijkstraEra () (Integer -> HSNativeScript)
-> SpecTransM DijkstraEra () Integer
-> SpecTransM DijkstraEra () HSNativeScript
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
<*> Integer -> SpecTransM DijkstraEra () Integer
forall a. a -> SpecTransM DijkstraEra () a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Integer) -> Int -> Integer
forall a b. (a -> b) -> a -> b
$ DijkstraNativeScript DijkstraEra -> Int
forall t. SafeToHash t => t -> Int
originalBytesSize DijkstraNativeScript DijkstraEra
ns)
    where
      nativeScriptToSpecRep :: NativeScript era -> SpecTransM era () NativeScript
nativeScriptToSpecRep NativeScript era
x =
        case NativeScript era
x of
          RequireSignature KeyHash Witness
kh ->
            Integer -> NativeScript
Agda.RequireSig (Integer -> NativeScript)
-> SpecTransM era () Integer -> SpecTransM era () NativeScript
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KeyHash Witness
-> SpecTransM
     era
     (SpecContext era (KeyHash Witness))
     (SpecRep era (KeyHash Witness))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep KeyHash Witness
kh
          RequireAllOf StrictSeq (NativeScript era)
ss -> do
            tls <- (NativeScript era -> SpecTransM era () NativeScript)
-> StrictSeq (NativeScript era)
-> SpecTransM era () (StrictSeq NativeScript)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> StrictSeq a -> f (StrictSeq b)
traverse NativeScript era -> SpecTransM era () NativeScript
nativeScriptToSpecRep StrictSeq (NativeScript era)
ss
            pure . Agda.RequireAllOf $ toList tls
          RequireAnyOf StrictSeq (NativeScript era)
ss -> do
            tls <- (NativeScript era -> SpecTransM era () NativeScript)
-> StrictSeq (NativeScript era)
-> SpecTransM era () (StrictSeq NativeScript)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> StrictSeq a -> f (StrictSeq b)
traverse NativeScript era -> SpecTransM era () NativeScript
nativeScriptToSpecRep StrictSeq (NativeScript era)
ss
            pure . Agda.RequireAnyOf $ toList tls
          RequireMOf Int
m StrictSeq (NativeScript era)
ss -> do
            tls <- (NativeScript era -> SpecTransM era () NativeScript)
-> StrictSeq (NativeScript era)
-> SpecTransM era () (StrictSeq NativeScript)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> StrictSeq a -> f (StrictSeq b)
traverse NativeScript era -> SpecTransM era () NativeScript
nativeScriptToSpecRep StrictSeq (NativeScript era)
ss
            pure . Agda.RequireMOf (toInteger m) $ toList tls
          RequireTimeExpire SlotNo
slot -> Integer -> NativeScript
Agda.RequireTimeExpire (Integer -> NativeScript)
-> SpecTransM era () Integer -> SpecTransM era () NativeScript
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SlotNo
-> SpecTransM era (SpecContext era SlotNo) (SpecRep era SlotNo)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep SlotNo
slot
          RequireTimeStart SlotNo
slot -> Integer -> NativeScript
Agda.RequireTimeStart (Integer -> NativeScript)
-> SpecTransM era () Integer -> SpecTransM era () NativeScript
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SlotNo
-> SpecTransM era (SpecContext era SlotNo) (SpecRep era SlotNo)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep SlotNo
slot
          RequireGuard Credential Guard
cred -> Credential -> NativeScript
Agda.RequireGuard (Credential -> NativeScript)
-> SpecTransM era () Credential -> SpecTransM era () NativeScript
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Credential Guard
-> SpecTransM
     era
     (SpecContext era (Credential Guard))
     (SpecRep era (Credential Guard))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep Credential Guard
cred
          NativeScript era
_ -> [Char] -> SpecTransM era () NativeScript
forall a. HasCallStack => [Char] -> a
error [Char]
"Impossible: All NativeScripts should have been accounted for"

instance SpecTranslate DijkstraEra (PlutusScript DijkstraEra) where
  type SpecRep DijkstraEra (PlutusScript DijkstraEra) = Agda.HSPlutusScript

  toSpecRep :: PlutusScript DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (PlutusScript DijkstraEra))
     (SpecRep DijkstraEra (PlutusScript DijkstraEra))
toSpecRep PlutusScript DijkstraEra
ps =
    Integer -> Integer -> HSLanguage -> HSPlutusScript
Agda.MkHSPlutusScript
      (Integer -> Integer -> HSLanguage -> HSPlutusScript)
-> SpecTransM DijkstraEra () Integer
-> SpecTransM
     DijkstraEra () (Integer -> HSLanguage -> HSPlutusScript)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ScriptHash
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra ScriptHash)
     (SpecRep DijkstraEra ScriptHash)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep (Script DijkstraEra -> ScriptHash
forall era. EraScript era => Script era -> ScriptHash
hashScript (Script DijkstraEra -> ScriptHash)
-> Script DijkstraEra -> ScriptHash
forall a b. (a -> b) -> a -> b
$ PlutusScript DijkstraEra -> AlonzoScript DijkstraEra
forall era. PlutusScript era -> AlonzoScript era
PlutusScript PlutusScript DijkstraEra
ps)
      SpecTransM DijkstraEra () (Integer -> HSLanguage -> HSPlutusScript)
-> SpecTransM DijkstraEra () Integer
-> SpecTransM DijkstraEra () (HSLanguage -> HSPlutusScript)
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
<*> Integer -> SpecTransM DijkstraEra () Integer
forall a. a -> SpecTransM DijkstraEra () a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Integer) -> Int -> Integer
forall a b. (a -> b) -> a -> b
$ PlutusScript DijkstraEra -> Int
forall t. SafeToHash t => t -> Int
originalBytesSize PlutusScript DijkstraEra
ps)
      SpecTransM DijkstraEra () (HSLanguage -> HSPlutusScript)
-> SpecTransM DijkstraEra () HSLanguage
-> SpecTransM DijkstraEra () HSPlutusScript
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
<*> Language
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra Language)
     (SpecRep DijkstraEra Language)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep (PlutusScript DijkstraEra -> Language
forall era. AlonzoEraScript era => PlutusScript era -> Language
plutusScriptLanguage PlutusScript DijkstraEra
ps)

instance SpecTranslate DijkstraEra DirectDeposits where
  type SpecRep DijkstraEra DirectDeposits = Agda.HSMap Agda.RewardAddress Integer

  toSpecRep :: DirectDeposits
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra DirectDeposits)
     (SpecRep DijkstraEra DirectDeposits)
toSpecRep (DirectDeposits Map AccountAddress Coin
m) = Map AccountAddress Coin
-> SpecTransM
     DijkstraEra
     ()
     (HSMap
        (SpecRep DijkstraEra AccountAddress) (SpecRep DijkstraEra Coin))
forall era k v ctx.
(SpecTranslate era k, SpecTranslate era v, SpecContext era k ~ ctx,
 SpecContext era v ~ ctx) =>
Map k v
-> SpecTransM era ctx (HSMap (SpecRep era k) (SpecRep era v))
toSpecRepMap Map AccountAddress Coin
m

instance SpecTranslate DijkstraEra (AccountBalanceInterval DijkstraEra) where
  type SpecRep DijkstraEra (AccountBalanceInterval DijkstraEra) = Agda.BalanceInterval

  toSpecRep :: AccountBalanceInterval DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (AccountBalanceInterval DijkstraEra))
     (SpecRep DijkstraEra (AccountBalanceInterval DijkstraEra))
toSpecRep = \case
    AccountBalanceLowerBound (Inclusive (Coin Integer
l)) ->
      BalanceInterval
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (AccountBalanceInterval DijkstraEra))
     BalanceInterval
forall a.
a
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (AccountBalanceInterval DijkstraEra))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BalanceInterval
 -> SpecTransM
      DijkstraEra
      (SpecContext DijkstraEra (AccountBalanceInterval DijkstraEra))
      BalanceInterval)
-> BalanceInterval
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (AccountBalanceInterval DijkstraEra))
     BalanceInterval
forall a b. (a -> b) -> a -> b
$ Integer -> BalanceInterval
Agda.Lower Integer
l
    AccountBalanceUpperBound (Exclusive (Coin Integer
u)) ->
      BalanceInterval
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (AccountBalanceInterval DijkstraEra))
     BalanceInterval
forall a.
a
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (AccountBalanceInterval DijkstraEra))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BalanceInterval
 -> SpecTransM
      DijkstraEra
      (SpecContext DijkstraEra (AccountBalanceInterval DijkstraEra))
      BalanceInterval)
-> BalanceInterval
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (AccountBalanceInterval DijkstraEra))
     BalanceInterval
forall a b. (a -> b) -> a -> b
$ Integer -> BalanceInterval
Agda.Upper Integer
u
    AccountBalanceBothBounds (Inclusive (Coin Integer
l)) (Exclusive (Coin Integer
u)) ->
      BalanceInterval
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (AccountBalanceInterval DijkstraEra))
     BalanceInterval
forall a.
a
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (AccountBalanceInterval DijkstraEra))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BalanceInterval
 -> SpecTransM
      DijkstraEra
      (SpecContext DijkstraEra (AccountBalanceInterval DijkstraEra))
      BalanceInterval)
-> BalanceInterval
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (AccountBalanceInterval DijkstraEra))
     BalanceInterval
forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> BalanceInterval
Agda.Both Integer
l Integer
u

instance SpecTranslate DijkstraEra (AccountBalanceIntervals DijkstraEra) where
  type
    SpecRep DijkstraEra (AccountBalanceIntervals DijkstraEra) =
      Agda.HSMap Agda.Credential Agda.BalanceInterval

  toSpecRep :: AccountBalanceIntervals DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (AccountBalanceIntervals DijkstraEra))
     (SpecRep DijkstraEra (AccountBalanceIntervals DijkstraEra))
toSpecRep (AccountBalanceIntervals Map AccountId (AccountBalanceInterval DijkstraEra)
m) =
    Map (Credential Staking) (AccountBalanceInterval DijkstraEra)
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (AccountBalanceIntervals DijkstraEra))
     (HSMap
        (SpecRep DijkstraEra (Credential Staking))
        (SpecRep DijkstraEra (AccountBalanceInterval DijkstraEra)))
forall era k v ctx.
(SpecTranslate era k, SpecTranslate era v, SpecContext era k ~ ctx,
 SpecContext era v ~ ctx) =>
Map k v
-> SpecTransM era ctx (HSMap (SpecRep era k) (SpecRep era v))
toSpecRepMap (Map (Credential Staking) (AccountBalanceInterval DijkstraEra)
 -> SpecTransM
      DijkstraEra
      (SpecContext DijkstraEra (AccountBalanceIntervals DijkstraEra))
      (HSMap
         (SpecRep DijkstraEra (Credential Staking))
         (SpecRep DijkstraEra (AccountBalanceInterval DijkstraEra))))
-> Map (Credential Staking) (AccountBalanceInterval DijkstraEra)
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (AccountBalanceIntervals DijkstraEra))
     (HSMap
        (SpecRep DijkstraEra (Credential Staking))
        (SpecRep DijkstraEra (AccountBalanceInterval DijkstraEra)))
forall a b. (a -> b) -> a -> b
$ (AccountId -> Credential Staking)
-> Map AccountId (AccountBalanceInterval DijkstraEra)
-> Map (Credential Staking) (AccountBalanceInterval DijkstraEra)
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys (\(AccountId Credential Staking
c) -> Credential Staking
c) Map AccountId (AccountBalanceInterval DijkstraEra)
m

instance SpecTranslate DijkstraEra (AlonzoScript DijkstraEra) where
  type SpecRep DijkstraEra (AlonzoScript DijkstraEra) = Agda.Script

  toSpecRep :: AlonzoScript DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (AlonzoScript DijkstraEra))
     (SpecRep DijkstraEra (AlonzoScript DijkstraEra))
toSpecRep (NativeScript NativeScript DijkstraEra
s) = HSNativeScript -> Either HSNativeScript HSPlutusScript
forall a b. a -> Either a b
Left (HSNativeScript -> Either HSNativeScript HSPlutusScript)
-> SpecTransM DijkstraEra () HSNativeScript
-> SpecTransM DijkstraEra () (Either HSNativeScript HSPlutusScript)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DijkstraNativeScript DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (DijkstraNativeScript DijkstraEra))
     (SpecRep DijkstraEra (DijkstraNativeScript DijkstraEra))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep NativeScript DijkstraEra
DijkstraNativeScript DijkstraEra
s
  toSpecRep (PlutusScript PlutusScript DijkstraEra
s) = HSPlutusScript -> Either HSNativeScript HSPlutusScript
forall a b. b -> Either a b
Right (HSPlutusScript -> Either HSNativeScript HSPlutusScript)
-> SpecTransM DijkstraEra () HSPlutusScript
-> SpecTransM DijkstraEra () (Either HSNativeScript HSPlutusScript)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PlutusScript DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (PlutusScript DijkstraEra))
     (SpecRep DijkstraEra (PlutusScript DijkstraEra))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep PlutusScript DijkstraEra
s

instance SpecTranslate DijkstraEra (BabbageTxOut DijkstraEra) where
  type SpecRep DijkstraEra (BabbageTxOut DijkstraEra) = Agda.TxOut

  toSpecRep :: BabbageTxOut DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (BabbageTxOut DijkstraEra))
     (SpecRep DijkstraEra (BabbageTxOut DijkstraEra))
toSpecRep (BabbageTxOut Addr
addr Value DijkstraEra
val Datum DijkstraEra
datum StrictMaybe (Script DijkstraEra)
script) = do
    addr' <- Addr
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra Addr)
     (SpecRep DijkstraEra Addr)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep Addr
addr
    val' <- toSpecRep val
    datum' <- toSpecRep datum
    script' <- toSpecRep script
    pure (addr', (val', (datum', script')))

instance SpecTranslate DijkstraEra (UTxO DijkstraEra) where
  type
    SpecRep DijkstraEra (UTxO DijkstraEra) =
      Agda.HSMap (SpecRep DijkstraEra TxIn) (SpecRep DijkstraEra (TxOut DijkstraEra))

  toSpecRep :: UTxO DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (UTxO DijkstraEra))
     (SpecRep DijkstraEra (UTxO DijkstraEra))
toSpecRep (UTxO Map TxIn (TxOut DijkstraEra)
m) = Map TxIn (BabbageTxOut DijkstraEra)
-> SpecTransM
     DijkstraEra
     ()
     (HSMap
        (SpecRep DijkstraEra TxIn)
        (SpecRep DijkstraEra (BabbageTxOut DijkstraEra)))
forall era k v ctx.
(SpecTranslate era k, SpecTranslate era v, SpecContext era k ~ ctx,
 SpecContext era v ~ ctx) =>
Map k v
-> SpecTransM era ctx (HSMap (SpecRep era k) (SpecRep era v))
toSpecRepMap Map TxIn (TxOut DijkstraEra)
Map TxIn (BabbageTxOut DijkstraEra)
m

deriving instance SpecTranslate DijkstraEra OrdExUnits

deriving instance SpecTranslate DijkstraEra CoinPerByte

instance
  SpecTranslate DijkstraEra (HKD f a) =>
  SpecTranslate DijkstraEra (THKD r f a)
  where
  type SpecRep DijkstraEra (THKD r f a) = SpecRep DijkstraEra (HKD f a)
  type SpecContext DijkstraEra (THKD r f a) = SpecContext DijkstraEra (HKD f a)

  toSpecRep :: THKD r f a
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (THKD r f a))
     (SpecRep DijkstraEra (THKD r f a))
toSpecRep = HKD f a
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (HKD f a))
     (SpecRep DijkstraEra (HKD f a))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep (HKD f a
 -> SpecTransM
      DijkstraEra
      (SpecContext DijkstraEra (HKD f a))
      (SpecRep DijkstraEra (HKD f a)))
-> (THKD r f a -> HKD f a)
-> THKD r f a
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (HKD f a))
     (SpecRep DijkstraEra (HKD f a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. THKD r f a -> HKD f a
forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD

instance SpecTranslate DijkstraEra DRepVotingThresholds where
  type SpecRep DijkstraEra DRepVotingThresholds = Agda.DrepThresholds

  toSpecRep :: DRepVotingThresholds
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra DRepVotingThresholds)
     (SpecRep DijkstraEra DRepVotingThresholds)
toSpecRep DRepVotingThresholds {UnitInterval
dvtMotionNoConfidence :: UnitInterval
dvtCommitteeNormal :: UnitInterval
dvtCommitteeNoConfidence :: UnitInterval
dvtUpdateToConstitution :: UnitInterval
dvtHardForkInitiation :: UnitInterval
dvtPPNetworkGroup :: UnitInterval
dvtPPEconomicGroup :: UnitInterval
dvtPPTechnicalGroup :: UnitInterval
dvtPPGovGroup :: UnitInterval
dvtTreasuryWithdrawal :: UnitInterval
dvtTreasuryWithdrawal :: DRepVotingThresholds -> UnitInterval
dvtPPGovGroup :: DRepVotingThresholds -> UnitInterval
dvtPPTechnicalGroup :: DRepVotingThresholds -> UnitInterval
dvtPPEconomicGroup :: DRepVotingThresholds -> UnitInterval
dvtPPNetworkGroup :: DRepVotingThresholds -> UnitInterval
dvtHardForkInitiation :: DRepVotingThresholds -> UnitInterval
dvtUpdateToConstitution :: DRepVotingThresholds -> UnitInterval
dvtCommitteeNoConfidence :: DRepVotingThresholds -> UnitInterval
dvtCommitteeNormal :: DRepVotingThresholds -> UnitInterval
dvtMotionNoConfidence :: DRepVotingThresholds -> UnitInterval
..} =
    Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> DrepThresholds
Agda.MkDrepThresholds
      (Rational
 -> Rational
 -> Rational
 -> Rational
 -> Rational
 -> Rational
 -> Rational
 -> Rational
 -> Rational
 -> Rational
 -> DrepThresholds)
-> SpecTransM DijkstraEra () Rational
-> SpecTransM
     DijkstraEra
     ()
     (Rational
      -> Rational
      -> Rational
      -> Rational
      -> Rational
      -> Rational
      -> Rational
      -> Rational
      -> Rational
      -> DrepThresholds)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UnitInterval
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra UnitInterval)
     (SpecRep DijkstraEra UnitInterval)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep UnitInterval
dvtMotionNoConfidence
      SpecTransM
  DijkstraEra
  ()
  (Rational
   -> Rational
   -> Rational
   -> Rational
   -> Rational
   -> Rational
   -> Rational
   -> Rational
   -> Rational
   -> DrepThresholds)
-> SpecTransM DijkstraEra () Rational
-> SpecTransM
     DijkstraEra
     ()
     (Rational
      -> Rational
      -> Rational
      -> Rational
      -> Rational
      -> Rational
      -> Rational
      -> Rational
      -> DrepThresholds)
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
<*> UnitInterval
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra UnitInterval)
     (SpecRep DijkstraEra UnitInterval)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep UnitInterval
dvtCommitteeNormal
      SpecTransM
  DijkstraEra
  ()
  (Rational
   -> Rational
   -> Rational
   -> Rational
   -> Rational
   -> Rational
   -> Rational
   -> Rational
   -> DrepThresholds)
-> SpecTransM DijkstraEra () Rational
-> SpecTransM
     DijkstraEra
     ()
     (Rational
      -> Rational
      -> Rational
      -> Rational
      -> Rational
      -> Rational
      -> Rational
      -> DrepThresholds)
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
<*> UnitInterval
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra UnitInterval)
     (SpecRep DijkstraEra UnitInterval)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep UnitInterval
dvtCommitteeNoConfidence
      SpecTransM
  DijkstraEra
  ()
  (Rational
   -> Rational
   -> Rational
   -> Rational
   -> Rational
   -> Rational
   -> Rational
   -> DrepThresholds)
-> SpecTransM DijkstraEra () Rational
-> SpecTransM
     DijkstraEra
     ()
     (Rational
      -> Rational
      -> Rational
      -> Rational
      -> Rational
      -> Rational
      -> DrepThresholds)
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
<*> UnitInterval
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra UnitInterval)
     (SpecRep DijkstraEra UnitInterval)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep UnitInterval
dvtUpdateToConstitution
      SpecTransM
  DijkstraEra
  ()
  (Rational
   -> Rational
   -> Rational
   -> Rational
   -> Rational
   -> Rational
   -> DrepThresholds)
-> SpecTransM DijkstraEra () Rational
-> SpecTransM
     DijkstraEra
     ()
     (Rational
      -> Rational -> Rational -> Rational -> Rational -> DrepThresholds)
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
<*> UnitInterval
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra UnitInterval)
     (SpecRep DijkstraEra UnitInterval)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep UnitInterval
dvtHardForkInitiation
      SpecTransM
  DijkstraEra
  ()
  (Rational
   -> Rational -> Rational -> Rational -> Rational -> DrepThresholds)
-> SpecTransM DijkstraEra () Rational
-> SpecTransM
     DijkstraEra
     ()
     (Rational -> Rational -> Rational -> Rational -> DrepThresholds)
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
<*> UnitInterval
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra UnitInterval)
     (SpecRep DijkstraEra UnitInterval)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep UnitInterval
dvtPPNetworkGroup
      SpecTransM
  DijkstraEra
  ()
  (Rational -> Rational -> Rational -> Rational -> DrepThresholds)
-> SpecTransM DijkstraEra () Rational
-> SpecTransM
     DijkstraEra () (Rational -> Rational -> Rational -> DrepThresholds)
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
<*> UnitInterval
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra UnitInterval)
     (SpecRep DijkstraEra UnitInterval)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep UnitInterval
dvtPPEconomicGroup
      SpecTransM
  DijkstraEra () (Rational -> Rational -> Rational -> DrepThresholds)
-> SpecTransM DijkstraEra () Rational
-> SpecTransM
     DijkstraEra () (Rational -> Rational -> DrepThresholds)
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
<*> UnitInterval
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra UnitInterval)
     (SpecRep DijkstraEra UnitInterval)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep UnitInterval
dvtPPTechnicalGroup
      SpecTransM DijkstraEra () (Rational -> Rational -> DrepThresholds)
-> SpecTransM DijkstraEra () Rational
-> SpecTransM DijkstraEra () (Rational -> DrepThresholds)
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
<*> UnitInterval
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra UnitInterval)
     (SpecRep DijkstraEra UnitInterval)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep UnitInterval
dvtPPGovGroup
      SpecTransM DijkstraEra () (Rational -> DrepThresholds)
-> SpecTransM DijkstraEra () Rational
-> SpecTransM DijkstraEra () DrepThresholds
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
<*> UnitInterval
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra UnitInterval)
     (SpecRep DijkstraEra UnitInterval)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep UnitInterval
dvtTreasuryWithdrawal

instance SpecTranslate DijkstraEra PoolVotingThresholds where
  type SpecRep DijkstraEra PoolVotingThresholds = Agda.PoolThresholds

  toSpecRep :: PoolVotingThresholds
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra PoolVotingThresholds)
     (SpecRep DijkstraEra PoolVotingThresholds)
toSpecRep PoolVotingThresholds {UnitInterval
pvtMotionNoConfidence :: UnitInterval
pvtCommitteeNormal :: UnitInterval
pvtCommitteeNoConfidence :: UnitInterval
pvtHardForkInitiation :: UnitInterval
pvtPPSecurityGroup :: UnitInterval
pvtPPSecurityGroup :: PoolVotingThresholds -> UnitInterval
pvtHardForkInitiation :: PoolVotingThresholds -> UnitInterval
pvtCommitteeNoConfidence :: PoolVotingThresholds -> UnitInterval
pvtCommitteeNormal :: PoolVotingThresholds -> UnitInterval
pvtMotionNoConfidence :: PoolVotingThresholds -> UnitInterval
..} =
    Rational
-> Rational -> Rational -> Rational -> Rational -> PoolThresholds
Agda.MkPoolThresholds
      (Rational
 -> Rational -> Rational -> Rational -> Rational -> PoolThresholds)
-> SpecTransM DijkstraEra () Rational
-> SpecTransM
     DijkstraEra
     ()
     (Rational -> Rational -> Rational -> Rational -> PoolThresholds)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UnitInterval
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra UnitInterval)
     (SpecRep DijkstraEra UnitInterval)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep UnitInterval
pvtMotionNoConfidence
      SpecTransM
  DijkstraEra
  ()
  (Rational -> Rational -> Rational -> Rational -> PoolThresholds)
-> SpecTransM DijkstraEra () Rational
-> SpecTransM
     DijkstraEra () (Rational -> Rational -> Rational -> PoolThresholds)
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
<*> UnitInterval
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra UnitInterval)
     (SpecRep DijkstraEra UnitInterval)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep UnitInterval
pvtCommitteeNormal
      SpecTransM
  DijkstraEra () (Rational -> Rational -> Rational -> PoolThresholds)
-> SpecTransM DijkstraEra () Rational
-> SpecTransM
     DijkstraEra () (Rational -> Rational -> PoolThresholds)
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
<*> UnitInterval
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra UnitInterval)
     (SpecRep DijkstraEra UnitInterval)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep UnitInterval
pvtCommitteeNoConfidence
      SpecTransM DijkstraEra () (Rational -> Rational -> PoolThresholds)
-> SpecTransM DijkstraEra () Rational
-> SpecTransM DijkstraEra () (Rational -> PoolThresholds)
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
<*> UnitInterval
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra UnitInterval)
     (SpecRep DijkstraEra UnitInterval)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep UnitInterval
pvtHardForkInitiation
      SpecTransM DijkstraEra () (Rational -> PoolThresholds)
-> SpecTransM DijkstraEra () Rational
-> SpecTransM DijkstraEra () PoolThresholds
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
<*> UnitInterval
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra UnitInterval)
     (SpecRep DijkstraEra UnitInterval)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep UnitInterval
pvtPPSecurityGroup

instance SpecTranslate DijkstraEra (DijkstraPParams Identity DijkstraEra) where
  type SpecRep DijkstraEra (DijkstraPParams Identity DijkstraEra) = Agda.PParams

  toSpecRep :: DijkstraPParams Identity DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (DijkstraPParams Identity DijkstraEra))
     (SpecRep DijkstraEra (DijkstraPParams Identity DijkstraEra))
toSpecRep dpp :: DijkstraPParams Identity DijkstraEra
dpp@DijkstraPParams {THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word16
THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity OrdExUnits
THKD
  ('PPGroups 'NetworkGroup 'SecurityGroup) Identity (NonZero Word32)
THKD
  ('PPGroups 'NetworkGroup 'SecurityGroup) Identity PositiveInterval
THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) Identity Word16
THKD
  ('PPGroups 'NetworkGroup 'NoStakePoolGroup) Identity OrdExUnits
THKD ('PPGroups 'EconomicGroup 'SecurityGroup) Identity CoinPerByte
THKD
  ('PPGroups 'EconomicGroup 'SecurityGroup)
  Identity
  (CompactForm Coin)
THKD
  ('PPGroups 'EconomicGroup 'SecurityGroup)
  Identity
  NonNegativeInterval
THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity Prices
THKD
  ('PPGroups 'EconomicGroup 'NoStakePoolGroup)
  Identity
  (CompactForm Coin)
THKD
  ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity UnitInterval
THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) Identity Word16
THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) Identity CostModels
THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
  Identity
  EpochInterval
THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
  Identity
  NonNegativeInterval
THKD
  ('PPGroups 'GovGroup 'SecurityGroup) Identity (CompactForm Coin)
THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity Word16
THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup)
  Identity
  DRepVotingThresholds
THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup)
  Identity
  PoolVotingThresholds
THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity (CompactForm Coin)
HKDNoUpdate Identity ProtVer
dppTxFeePerByte :: THKD ('PPGroups 'EconomicGroup 'SecurityGroup) Identity CoinPerByte
dppTxFeeFixed :: THKD
  ('PPGroups 'EconomicGroup 'SecurityGroup)
  Identity
  (CompactForm Coin)
dppMaxBBSize :: THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
dppMaxTxSize :: THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
dppMaxBHSize :: THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word16
dppKeyDeposit :: THKD
  ('PPGroups 'EconomicGroup 'NoStakePoolGroup)
  Identity
  (CompactForm Coin)
dppPoolDeposit :: THKD
  ('PPGroups 'EconomicGroup 'NoStakePoolGroup)
  Identity
  (CompactForm Coin)
dppEMax :: THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
  Identity
  EpochInterval
dppNOpt :: THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) Identity Word16
dppA0 :: THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
  Identity
  NonNegativeInterval
dppRho :: THKD
  ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity UnitInterval
dppTau :: THKD
  ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity UnitInterval
dppProtocolVersion :: HKDNoUpdate Identity ProtVer
dppMinPoolCost :: THKD
  ('PPGroups 'EconomicGroup 'NoStakePoolGroup)
  Identity
  (CompactForm Coin)
dppCoinsPerUTxOByte :: THKD ('PPGroups 'EconomicGroup 'SecurityGroup) Identity CoinPerByte
dppCostModels :: THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) Identity CostModels
dppPrices :: THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity Prices
dppMaxTxExUnits :: THKD
  ('PPGroups 'NetworkGroup 'NoStakePoolGroup) Identity OrdExUnits
dppMaxBlockExUnits :: THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity OrdExUnits
dppMaxValSize :: THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
dppCollateralPercentage :: THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) Identity Word16
dppMaxCollateralInputs :: THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) Identity Word16
dppPoolVotingThresholds :: THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup)
  Identity
  PoolVotingThresholds
dppDRepVotingThresholds :: THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup)
  Identity
  DRepVotingThresholds
dppCommitteeMinSize :: THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity Word16
dppCommitteeMaxTermLength :: THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
dppGovActionLifetime :: THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
dppGovActionDeposit :: THKD
  ('PPGroups 'GovGroup 'SecurityGroup) Identity (CompactForm Coin)
dppDRepDeposit :: THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity (CompactForm Coin)
dppDRepActivity :: THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
dppMinFeeRefScriptCostPerByte :: THKD
  ('PPGroups 'EconomicGroup 'SecurityGroup)
  Identity
  NonNegativeInterval
dppMaxRefScriptSizePerBlock :: THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
dppMaxRefScriptSizePerTx :: THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
dppRefScriptCostStride :: THKD
  ('PPGroups 'NetworkGroup 'SecurityGroup) Identity (NonZero Word32)
dppRefScriptCostMultiplier :: THKD
  ('PPGroups 'NetworkGroup 'SecurityGroup) Identity PositiveInterval
dppRefScriptCostMultiplier :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f PositiveInterval
dppRefScriptCostStride :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f (NonZero Word32)
dppMaxRefScriptSizePerTx :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f Word32
dppMaxRefScriptSizePerBlock :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f Word32
dppMinFeeRefScriptCostPerByte :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD
     ('PPGroups 'EconomicGroup 'SecurityGroup) f NonNegativeInterval
dppDRepActivity :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) f EpochInterval
dppDRepDeposit :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD
     ('PPGroups 'GovGroup 'NoStakePoolGroup) f (CompactForm Coin)
dppGovActionDeposit :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD ('PPGroups 'GovGroup 'SecurityGroup) f (CompactForm Coin)
dppGovActionLifetime :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) f EpochInterval
dppCommitteeMaxTermLength :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) f EpochInterval
dppCommitteeMinSize :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) f Word16
dppDRepVotingThresholds :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD
     ('PPGroups 'GovGroup 'NoStakePoolGroup) f DRepVotingThresholds
dppPoolVotingThresholds :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD
     ('PPGroups 'GovGroup 'NoStakePoolGroup) f PoolVotingThresholds
dppMaxCollateralInputs :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) f Word16
dppCollateralPercentage :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) f Word16
dppMaxValSize :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f Word32
dppMaxBlockExUnits :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f OrdExUnits
dppMaxTxExUnits :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) f OrdExUnits
dppPrices :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f Prices
dppCostModels :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) f CostModels
dppCoinsPerUTxOByte :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD ('PPGroups 'EconomicGroup 'SecurityGroup) f CoinPerByte
dppMinPoolCost :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD
     ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f (CompactForm Coin)
dppProtocolVersion :: forall (f :: * -> *) era.
DijkstraPParams f era -> HKDNoUpdate f ProtVer
dppTau :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f UnitInterval
dppRho :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f UnitInterval
dppA0 :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD
     ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) f NonNegativeInterval
dppNOpt :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) f Word16
dppEMax :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD
     ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) f EpochInterval
dppPoolDeposit :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD
     ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f (CompactForm Coin)
dppKeyDeposit :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD
     ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f (CompactForm Coin)
dppMaxBHSize :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f Word16
dppMaxTxSize :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f Word32
dppMaxBBSize :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f Word32
dppTxFeeFixed :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD
     ('PPGroups 'EconomicGroup 'SecurityGroup) f (CompactForm Coin)
dppTxFeePerByte :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD ('PPGroups 'EconomicGroup 'SecurityGroup) f CoinPerByte
..} = do
    ppA <- THKD ('PPGroups 'EconomicGroup 'SecurityGroup) Identity CoinPerByte
-> SpecTransM
     DijkstraEra
     (SpecContext
        DijkstraEra
        (THKD
           ('PPGroups 'EconomicGroup 'SecurityGroup) Identity CoinPerByte))
     (SpecRep
        DijkstraEra
        (THKD
           ('PPGroups 'EconomicGroup 'SecurityGroup) Identity CoinPerByte))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep THKD ('PPGroups 'EconomicGroup 'SecurityGroup) Identity CoinPerByte
dppTxFeePerByte
    ppB <- toSpecRep dppTxFeeFixed
    ppA0 <- toSpecRep dppA0
    ppMinFeeRefScriptCoinsPerByte <- toSpecRep dppMinFeeRefScriptCostPerByte
    ppCollateralPercentage <- toSpecRep dppCollateralPercentage
    let
      ppMaxBlockSize = Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger (Word32 -> Integer) -> Word32 -> Integer
forall a b. (a -> b) -> a -> b
$ THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
-> HKD Identity Word32
forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
dppMaxBBSize
      ppMaxTxSize = Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger (Word32 -> Integer) -> Word32 -> Integer
forall a b. (a -> b) -> a -> b
$ THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
-> HKD Identity Word32
forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
dppMaxTxSize
      ppMaxHeaderSize = Word16 -> Integer
forall a. Integral a => a -> Integer
toInteger (Word16 -> Integer) -> Word16 -> Integer
forall a b. (a -> b) -> a -> b
$ THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word16
-> HKD Identity Word16
forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word16
dppMaxBHSize
    ppKeyDeposit <- toSpecRep dppKeyDeposit
    ppPoolDeposit <- toSpecRep dppPoolDeposit
    ppEmax <- toSpecRep dppEMax
    ppNopt <- toSpecRep (toInteger $ unTHKD dppNOpt)
    let
      ppPv = (Integer
0, Integer
0)
      ppMinUTxOValue = Integer
0
    ppCoinsPerUTxOByte <- toSpecRep dppCoinsPerUTxOByte
    ppCostmdlsAssoc <- toSpecRep dppCostModels
    ppPrices <- toSpecRep dppPrices
    let
      pp = PParamsHKD Identity DijkstraEra -> PParams DijkstraEra
forall era. PParamsHKD Identity era -> PParams era
PParams PParamsHKD Identity DijkstraEra
DijkstraPParams Identity DijkstraEra
dpp
      ppMaxRefScriptSizePerTx = Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger (Word32 -> Integer) -> Word32 -> Integer
forall a b. (a -> b) -> a -> b
$ PParams DijkstraEra
pp PParams DijkstraEra
-> Getting Word32 (PParams DijkstraEra) Word32 -> Word32
forall s a. s -> Getting a s a -> a
^. Getting Word32 (PParams DijkstraEra) Word32
forall era.
ConwayEraPParams era =>
SimpleGetter (PParams era) Word32
SimpleGetter (PParams DijkstraEra) Word32
ppMaxRefScriptSizePerTxG
      ppMaxRefScriptSizePerBlock = Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger (Word32 -> Integer) -> Word32 -> Integer
forall a b. (a -> b) -> a -> b
$ PParams DijkstraEra
pp PParams DijkstraEra
-> Getting Word32 (PParams DijkstraEra) Word32 -> Word32
forall s a. s -> Getting a s a -> a
^. Getting Word32 (PParams DijkstraEra) Word32
forall era.
ConwayEraPParams era =>
SimpleGetter (PParams era) Word32
SimpleGetter (PParams DijkstraEra) Word32
ppMaxRefScriptSizePerBlockG
      ppRefScriptCostStride = Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger (Word32 -> Integer)
-> (NonZero Word32 -> Word32) -> NonZero Word32 -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonZero Word32 -> Word32
forall a. NonZero a -> a
unNonZero (NonZero Word32 -> Integer) -> NonZero Word32 -> Integer
forall a b. (a -> b) -> a -> b
$ PParams DijkstraEra
pp PParams DijkstraEra
-> Getting (NonZero Word32) (PParams DijkstraEra) (NonZero Word32)
-> NonZero Word32
forall s a. s -> Getting a s a -> a
^. Getting (NonZero Word32) (PParams DijkstraEra) (NonZero Word32)
forall era.
ConwayEraPParams era =>
SimpleGetter (PParams era) (NonZero Word32)
SimpleGetter (PParams DijkstraEra) (NonZero Word32)
ppRefScriptCostStrideG
      ppRefScriptCostMultiplier = PositiveInterval -> Rational
forall r. BoundedRational r => r -> Rational
unboundRational (PositiveInterval -> Rational) -> PositiveInterval -> Rational
forall a b. (a -> b) -> a -> b
$ PParams DijkstraEra
pp PParams DijkstraEra
-> Getting PositiveInterval (PParams DijkstraEra) PositiveInterval
-> PositiveInterval
forall s a. s -> Getting a s a -> a
^. Getting PositiveInterval (PParams DijkstraEra) PositiveInterval
forall era.
ConwayEraPParams era =>
SimpleGetter (PParams era) PositiveInterval
SimpleGetter (PParams DijkstraEra) PositiveInterval
ppRefScriptCostMultiplierG
    ppMaxTxExUnits <- toSpecRep dppMaxTxExUnits
    ppMaxBlockExUnits <- toSpecRep dppMaxBlockExUnits
    let
      ppMaxValSize = Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger (Word32 -> Integer)
-> (THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
    -> Word32)
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
-> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
-> Word32
THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
-> HKD Identity Word32
forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD (THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
 -> Integer)
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
-> Integer
forall a b. (a -> b) -> a -> b
$ THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
dppMaxValSize
      ppMaxCollateralInputs = Word16 -> Integer
forall a. Integral a => a -> Integer
toInteger (Word16 -> Integer)
-> (THKD
      ('PPGroups 'NetworkGroup 'NoStakePoolGroup) Identity Word16
    -> Word16)
-> THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) Identity Word16
-> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) Identity Word16
-> Word16
THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) Identity Word16
-> HKD Identity Word16
forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD (THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) Identity Word16
 -> Integer)
-> THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) Identity Word16
-> Integer
forall a b. (a -> b) -> a -> b
$ THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) Identity Word16
dppMaxCollateralInputs
    ppPoolThresholds <- toSpecRep dppPoolVotingThresholds
    ppDrepThresholds <- toSpecRep dppDRepVotingThresholds
    let
      ppCcMinSize = Word16 -> Integer
forall a. Integral a => a -> Integer
toInteger (Word16 -> Integer)
-> (THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity Word16
    -> Word16)
-> THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity Word16
-> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity Word16
-> Word16
THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity Word16
-> HKD Identity Word16
forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD (THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity Word16
 -> Integer)
-> THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity Word16
-> Integer
forall a b. (a -> b) -> a -> b
$ THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity Word16
dppCommitteeMinSize
      ppCcMaxTermLength = Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger (Word32 -> Integer)
-> (THKD
      ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
    -> Word32)
-> THKD
     ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
-> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EpochInterval -> Word32
unEpochInterval (EpochInterval -> Word32)
-> (THKD
      ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
    -> EpochInterval)
-> THKD
     ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
-> Word32
forall b c a. (b -> c) -> (a -> b) -> a -> c
. THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
-> EpochInterval
THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
-> HKD Identity EpochInterval
forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD (THKD
   ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
 -> Integer)
-> THKD
     ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
-> Integer
forall a b. (a -> b) -> a -> b
$ THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
dppCommitteeMaxTermLength
    ppGovActionLifetime <- toSpecRep dppGovActionLifetime
    ppGovActionDeposit <- toSpecRep dppGovActionDeposit
    ppDrepDeposit <- toSpecRep dppDRepDeposit
    ppDrepActivity <- toSpecRep dppDRepActivity
    ppMonetaryExpansion <- toSpecRep dppRho
    ppTreasuryCut <- toSpecRep dppTau

    pure Agda.MkPParams {..}

instance SpecTranslate DijkstraEra ValidityInterval where
  type SpecRep DijkstraEra ValidityInterval = (Maybe Integer, Maybe Integer)

  toSpecRep :: ValidityInterval
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra ValidityInterval)
     (SpecRep DijkstraEra ValidityInterval)
toSpecRep (ValidityInterval StrictMaybe SlotNo
lo StrictMaybe SlotNo
hi) = (StrictMaybe SlotNo, StrictMaybe SlotNo)
-> SpecTransM
     DijkstraEra
     ()
     (SpecRep DijkstraEra (StrictMaybe SlotNo),
      SpecRep DijkstraEra (StrictMaybe SlotNo))
forall era a b ctx.
(SpecTranslate era a, SpecTranslate era b, SpecContext era a ~ ctx,
 SpecContext era b ~ ctx) =>
(a, b) -> SpecTransM era ctx (SpecRep era a, SpecRep era b)
toSpecRepTuple (StrictMaybe SlotNo
lo, StrictMaybe SlotNo
hi)

instance SpecTranslate DijkstraEra (TxDats DijkstraEra) where
  type SpecRep DijkstraEra (TxDats DijkstraEra) = Agda.HSSet Agda.Datum

  toSpecRep :: TxDats DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (TxDats DijkstraEra))
     (SpecRep DijkstraEra (TxDats DijkstraEra))
toSpecRep = ([Integer] -> HSSet Integer)
-> SpecTransM DijkstraEra () [Integer]
-> SpecTransM DijkstraEra () (HSSet Integer)
forall a b.
(a -> b)
-> SpecTransM DijkstraEra () a -> SpecTransM DijkstraEra () b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Integer] -> HSSet Integer
forall a. [a] -> HSSet a
Agda.MkHSSet (SpecTransM DijkstraEra () [Integer]
 -> SpecTransM DijkstraEra () (HSSet Integer))
-> (TxDats DijkstraEra -> SpecTransM DijkstraEra () [Integer])
-> TxDats DijkstraEra
-> SpecTransM DijkstraEra () (HSSet Integer)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((DataHash, Data DijkstraEra) -> SpecTransM DijkstraEra () Integer)
-> [(DataHash, Data DijkstraEra)]
-> SpecTransM DijkstraEra () [Integer]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (Data DijkstraEra -> SpecTransM DijkstraEra () Integer
Data DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (Data DijkstraEra))
     (SpecRep DijkstraEra (Data DijkstraEra))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep (Data DijkstraEra -> SpecTransM DijkstraEra () Integer)
-> ((DataHash, Data DijkstraEra) -> Data DijkstraEra)
-> (DataHash, Data DijkstraEra)
-> SpecTransM DijkstraEra () Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DataHash, Data DijkstraEra) -> Data DijkstraEra
forall a b. (a, b) -> b
snd) ([(DataHash, Data DijkstraEra)]
 -> SpecTransM DijkstraEra () [Integer])
-> (TxDats DijkstraEra -> [(DataHash, Data DijkstraEra)])
-> TxDats DijkstraEra
-> SpecTransM DijkstraEra () [Integer]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map DataHash (Data DijkstraEra) -> [(DataHash, Data DijkstraEra)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map DataHash (Data DijkstraEra) -> [(DataHash, Data DijkstraEra)])
-> (TxDats DijkstraEra -> Map DataHash (Data DijkstraEra))
-> TxDats DijkstraEra
-> [(DataHash, Data DijkstraEra)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TxDats DijkstraEra -> Map DataHash (Data DijkstraEra)
forall era. TxDats era -> Map DataHash (Data era)
unTxDats

instance SpecTranslate DijkstraEra (DijkstraPlutusPurpose AsIx DijkstraEra) where
  type SpecRep DijkstraEra (DijkstraPlutusPurpose AsIx DijkstraEra) = Agda.RedeemerPtr

  toSpecRep :: DijkstraPlutusPurpose AsIx DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (DijkstraPlutusPurpose AsIx DijkstraEra))
     (SpecRep DijkstraEra (DijkstraPlutusPurpose AsIx DijkstraEra))
toSpecRep = \case
    DijkstraSpending (AsIx Word32
i) -> (Tag, Integer) -> SpecTransM DijkstraEra () (Tag, Integer)
forall a. a -> SpecTransM DijkstraEra () a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tag
Agda.Spend, Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger Word32
i)
    DijkstraMinting (AsIx Word32
i) -> (Tag, Integer) -> SpecTransM DijkstraEra () (Tag, Integer)
forall a. a -> SpecTransM DijkstraEra () a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tag
Agda.Mint, Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger Word32
i)
    DijkstraCertifying (AsIx Word32
i) -> (Tag, Integer) -> SpecTransM DijkstraEra () (Tag, Integer)
forall a. a -> SpecTransM DijkstraEra () a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tag
Agda.Cert, Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger Word32
i)
    DijkstraRewarding (AsIx Word32
i) -> (Tag, Integer) -> SpecTransM DijkstraEra () (Tag, Integer)
forall a. a -> SpecTransM DijkstraEra () a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tag
Agda.Reward, Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger Word32
i)
    DijkstraVoting (AsIx Word32
i) -> (Tag, Integer) -> SpecTransM DijkstraEra () (Tag, Integer)
forall a. a -> SpecTransM DijkstraEra () a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tag
Agda.Vote, Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger Word32
i)
    DijkstraProposing (AsIx Word32
i) -> (Tag, Integer) -> SpecTransM DijkstraEra () (Tag, Integer)
forall a. a -> SpecTransM DijkstraEra () a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tag
Agda.Propose, Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger Word32
i)
    DijkstraGuarding (AsIx Word32
i) -> (Tag, Integer) -> SpecTransM DijkstraEra () (Tag, Integer)
forall a. a -> SpecTransM DijkstraEra () a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tag
Agda.Guard, Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger Word32
i)

instance SpecTranslate DijkstraEra (Redeemers DijkstraEra) where
  type
    SpecRep DijkstraEra (Redeemers DijkstraEra) =
      Agda.HSMap (SpecRep DijkstraEra (PlutusPurpose AsIx DijkstraEra)) (Agda.Redeemer, Agda.ExUnits)

  toSpecRep :: Redeemers DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (Redeemers DijkstraEra))
     (SpecRep DijkstraEra (Redeemers DijkstraEra))
toSpecRep (Redeemers Map (PlutusPurpose AsIx DijkstraEra) (Data DijkstraEra, ExUnits)
x) =
    ([((Tag, Integer), (Integer, (Integer, Integer)))]
 -> HSMap (Tag, Integer) (Integer, (Integer, Integer)))
-> SpecTransM
     DijkstraEra () [((Tag, Integer), (Integer, (Integer, Integer)))]
-> SpecTransM
     DijkstraEra () (HSMap (Tag, Integer) (Integer, (Integer, Integer)))
forall a b.
(a -> b)
-> SpecTransM DijkstraEra () a -> SpecTransM DijkstraEra () b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [((Tag, Integer), (Integer, (Integer, Integer)))]
-> HSMap (Tag, Integer) (Integer, (Integer, Integer))
forall k v. [(k, v)] -> HSMap k v
Agda.MkHSMap
      (SpecTransM
   DijkstraEra () [((Tag, Integer), (Integer, (Integer, Integer)))]
 -> SpecTransM
      DijkstraEra
      (SpecContext DijkstraEra (Redeemers DijkstraEra))
      (SpecRep DijkstraEra (Redeemers DijkstraEra)))
-> (Map
      (PlutusPurpose AsIx DijkstraEra) (Data DijkstraEra, ExUnits)
    -> SpecTransM
         DijkstraEra () [((Tag, Integer), (Integer, (Integer, Integer)))])
-> Map (PlutusPurpose AsIx DijkstraEra) (Data DijkstraEra, ExUnits)
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (Redeemers DijkstraEra))
     (SpecRep DijkstraEra (Redeemers DijkstraEra))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((DijkstraPlutusPurpose AsIx DijkstraEra,
  (Data DijkstraEra, ExUnits))
 -> SpecTransM
      DijkstraEra () ((Tag, Integer), (Integer, (Integer, Integer))))
-> [(DijkstraPlutusPurpose AsIx DijkstraEra,
     (Data DijkstraEra, ExUnits))]
-> SpecTransM
     DijkstraEra () [((Tag, Integer), (Integer, (Integer, Integer)))]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse ((DijkstraPlutusPurpose AsIx DijkstraEra
 -> SpecTransM DijkstraEra () (Tag, Integer))
-> ((Data DijkstraEra, ExUnits)
    -> SpecTransM DijkstraEra () (Integer, (Integer, Integer)))
-> (DijkstraPlutusPurpose AsIx DijkstraEra,
    (Data DijkstraEra, ExUnits))
-> SpecTransM
     DijkstraEra () ((Tag, Integer), (Integer, (Integer, Integer)))
forall era a b c d ctx.
(a -> SpecTransM era ctx c)
-> (b -> SpecTransM era ctx d)
-> (a, b)
-> SpecTransM era ctx (c, d)
toSpecRepTupleGen DijkstraPlutusPurpose AsIx DijkstraEra
-> SpecTransM DijkstraEra () (Tag, Integer)
DijkstraPlutusPurpose AsIx DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (DijkstraPlutusPurpose AsIx DijkstraEra))
     (SpecRep DijkstraEra (DijkstraPlutusPurpose AsIx DijkstraEra))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep (Data DijkstraEra, ExUnits)
-> SpecTransM DijkstraEra () (Integer, (Integer, Integer))
(Data DijkstraEra, ExUnits)
-> SpecTransM
     DijkstraEra
     ()
     (SpecRep DijkstraEra (Data DijkstraEra),
      SpecRep DijkstraEra ExUnits)
forall era a b ctx.
(SpecTranslate era a, SpecTranslate era b, SpecContext era a ~ ctx,
 SpecContext era b ~ ctx) =>
(a, b) -> SpecTransM era ctx (SpecRep era a, SpecRep era b)
toSpecRepTuple)
      ([(DijkstraPlutusPurpose AsIx DijkstraEra,
   (Data DijkstraEra, ExUnits))]
 -> SpecTransM
      DijkstraEra () [((Tag, Integer), (Integer, (Integer, Integer)))])
-> (Map
      (DijkstraPlutusPurpose AsIx DijkstraEra)
      (Data DijkstraEra, ExUnits)
    -> [(DijkstraPlutusPurpose AsIx DijkstraEra,
         (Data DijkstraEra, ExUnits))])
-> Map
     (DijkstraPlutusPurpose AsIx DijkstraEra)
     (Data DijkstraEra, ExUnits)
-> SpecTransM
     DijkstraEra () [((Tag, Integer), (Integer, (Integer, Integer)))]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map
  (DijkstraPlutusPurpose AsIx DijkstraEra)
  (Data DijkstraEra, ExUnits)
-> [(DijkstraPlutusPurpose AsIx DijkstraEra,
     (Data DijkstraEra, ExUnits))]
forall k a. Map k a -> [(k, a)]
Map.toList
      (Map (PlutusPurpose AsIx DijkstraEra) (Data DijkstraEra, ExUnits)
 -> SpecTransM
      DijkstraEra
      (SpecContext DijkstraEra (Redeemers DijkstraEra))
      (SpecRep DijkstraEra (Redeemers DijkstraEra)))
-> Map (PlutusPurpose AsIx DijkstraEra) (Data DijkstraEra, ExUnits)
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (Redeemers DijkstraEra))
     (SpecRep DijkstraEra (Redeemers DijkstraEra))
forall a b. (a -> b) -> a -> b
$ Map (PlutusPurpose AsIx DijkstraEra) (Data DijkstraEra, ExUnits)
x

instance SpecTranslate DijkstraEra (AlonzoTxWits DijkstraEra) where
  type SpecRep DijkstraEra (AlonzoTxWits DijkstraEra) = Agda.TxWitnesses

  toSpecRep :: AlonzoTxWits DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (AlonzoTxWits DijkstraEra))
     (SpecRep DijkstraEra (AlonzoTxWits DijkstraEra))
toSpecRep AlonzoTxWits DijkstraEra
x =
    HSMap HSVKey Integer
-> HSSet (Either HSNativeScript HSPlutusScript)
-> HSSet Integer
-> HSMap (Tag, Integer) (Integer, (Integer, Integer))
-> TxWitnesses
Agda.MkTxWitnesses
      (HSMap HSVKey Integer
 -> HSSet (Either HSNativeScript HSPlutusScript)
 -> HSSet Integer
 -> HSMap (Tag, Integer) (Integer, (Integer, Integer))
 -> TxWitnesses)
-> SpecTransM DijkstraEra () (HSMap HSVKey Integer)
-> SpecTransM
     DijkstraEra
     ()
     (HSSet (Either HSNativeScript HSPlutusScript)
      -> HSSet Integer
      -> HSMap (Tag, Integer) (Integer, (Integer, Integer))
      -> TxWitnesses)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([(HSVKey, Integer)] -> HSMap HSVKey Integer)
-> SpecTransM DijkstraEra () [(HSVKey, Integer)]
-> SpecTransM DijkstraEra () (HSMap HSVKey Integer)
forall a b.
(a -> b)
-> SpecTransM DijkstraEra () a -> SpecTransM DijkstraEra () b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [(HSVKey, Integer)] -> HSMap HSVKey Integer
forall k v. [(k, v)] -> HSMap k v
Agda.MkHSMap ([WitVKey Witness]
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra [WitVKey Witness])
     (SpecRep DijkstraEra [WitVKey Witness])
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep [WitVKey Witness]
txWitsMap)
      SpecTransM
  DijkstraEra
  ()
  (HSSet (Either HSNativeScript HSPlutusScript)
   -> HSSet Integer
   -> HSMap (Tag, Integer) (Integer, (Integer, Integer))
   -> TxWitnesses)
-> SpecTransM
     DijkstraEra () (HSSet (Either HSNativeScript HSPlutusScript))
-> SpecTransM
     DijkstraEra
     ()
     (HSSet Integer
      -> HSMap (Tag, Integer) (Integer, (Integer, Integer))
      -> TxWitnesses)
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
<*> ([Either HSNativeScript HSPlutusScript]
 -> HSSet (Either HSNativeScript HSPlutusScript))
-> SpecTransM DijkstraEra () [Either HSNativeScript HSPlutusScript]
-> SpecTransM
     DijkstraEra () (HSSet (Either HSNativeScript HSPlutusScript))
forall a b.
(a -> b)
-> SpecTransM DijkstraEra () a -> SpecTransM DijkstraEra () b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Either HSNativeScript HSPlutusScript]
-> HSSet (Either HSNativeScript HSPlutusScript)
forall a. [a] -> HSSet a
Agda.MkHSSet ([AlonzoScript DijkstraEra]
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra [AlonzoScript DijkstraEra])
     (SpecRep DijkstraEra [AlonzoScript DijkstraEra])
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep (Map ScriptHash (AlonzoScript DijkstraEra)
-> [AlonzoScript DijkstraEra]
forall k a. Map k a -> [a]
Map.elems (Map ScriptHash (AlonzoScript DijkstraEra)
 -> [AlonzoScript DijkstraEra])
-> Map ScriptHash (AlonzoScript DijkstraEra)
-> [AlonzoScript DijkstraEra]
forall a b. (a -> b) -> a -> b
$ AlonzoTxWits DijkstraEra -> Map ScriptHash (Script DijkstraEra)
forall era.
AlonzoEraScript era =>
AlonzoTxWits era -> Map ScriptHash (Script era)
txscripts AlonzoTxWits DijkstraEra
x))
      SpecTransM
  DijkstraEra
  ()
  (HSSet Integer
   -> HSMap (Tag, Integer) (Integer, (Integer, Integer))
   -> TxWitnesses)
-> SpecTransM DijkstraEra () (HSSet Integer)
-> SpecTransM
     DijkstraEra
     ()
     (HSMap (Tag, Integer) (Integer, (Integer, Integer)) -> TxWitnesses)
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
<*> TxDats DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (TxDats DijkstraEra))
     (SpecRep DijkstraEra (TxDats DijkstraEra))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep (AlonzoTxWits DijkstraEra -> TxDats DijkstraEra
forall era. AlonzoEraScript era => AlonzoTxWits era -> TxDats era
txdats AlonzoTxWits DijkstraEra
x)
      SpecTransM
  DijkstraEra
  ()
  (HSMap (Tag, Integer) (Integer, (Integer, Integer)) -> TxWitnesses)
-> SpecTransM
     DijkstraEra () (HSMap (Tag, Integer) (Integer, (Integer, Integer)))
-> SpecTransM DijkstraEra () TxWitnesses
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
<*> Redeemers DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (Redeemers DijkstraEra))
     (SpecRep DijkstraEra (Redeemers DijkstraEra))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep (AlonzoTxWits DijkstraEra -> Redeemers DijkstraEra
forall era.
AlonzoEraScript era =>
AlonzoTxWits era -> Redeemers era
txrdmrs AlonzoTxWits DijkstraEra
x)
    where
      txWitsMap :: [WitVKey Witness]
txWitsMap = Set (WitVKey Witness) -> [WitVKey Witness]
forall a. Set a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (AlonzoTxWits DijkstraEra -> Set (WitVKey Witness)
forall era.
AlonzoEraScript era =>
AlonzoTxWits era -> Set (WitVKey Witness)
txwitsVKey AlonzoTxWits DijkstraEra
x)

instance SpecTranslate DijkstraEra (AlonzoTxAuxData DijkstraEra) where
  type SpecRep DijkstraEra (AlonzoTxAuxData DijkstraEra) = Agda.AuxiliaryData

  toSpecRep :: AlonzoTxAuxData DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (AlonzoTxAuxData DijkstraEra))
     (SpecRep DijkstraEra (AlonzoTxAuxData DijkstraEra))
toSpecRep = SafeHash EraIndependentTxAuxData
-> SpecTransM DijkstraEra () Integer
SafeHash EraIndependentTxAuxData
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (SafeHash EraIndependentTxAuxData))
     (SpecRep DijkstraEra (SafeHash EraIndependentTxAuxData))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep (SafeHash EraIndependentTxAuxData
 -> SpecTransM DijkstraEra () Integer)
-> (AlonzoTxAuxData DijkstraEra
    -> SafeHash EraIndependentTxAuxData)
-> AlonzoTxAuxData DijkstraEra
-> SpecTransM DijkstraEra () Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AlonzoTxAuxData DijkstraEra -> SafeHash EraIndependentTxAuxData
forall x i. HashAnnotated x i => x -> SafeHash i
hashAnnotated

instance SpecTranslate DijkstraEra StakePoolParams where
  type SpecRep DijkstraEra StakePoolParams = Agda.StakePoolParams

  toSpecRep :: StakePoolParams
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra StakePoolParams)
     (SpecRep DijkstraEra StakePoolParams)
toSpecRep StakePoolParams {Set (KeyHash Staking)
StrictMaybe PoolMetadata
AccountAddress
KeyHash StakePool
VRFVerKeyHash StakePoolVRF
Coin
UnitInterval
StrictSeq StakePoolRelay
sppId :: KeyHash StakePool
sppVrf :: VRFVerKeyHash StakePoolVRF
sppPledge :: Coin
sppCost :: Coin
sppMargin :: UnitInterval
sppAccountAddress :: AccountAddress
sppOwners :: Set (KeyHash Staking)
sppRelays :: StrictSeq StakePoolRelay
sppMetadata :: StrictMaybe PoolMetadata
sppAccountAddress :: StakePoolParams -> AccountAddress
sppCost :: StakePoolParams -> Coin
sppId :: StakePoolParams -> KeyHash StakePool
sppMargin :: StakePoolParams -> UnitInterval
sppMetadata :: StakePoolParams -> StrictMaybe PoolMetadata
sppOwners :: StakePoolParams -> Set (KeyHash Staking)
sppPledge :: StakePoolParams -> Coin
sppRelays :: StakePoolParams -> StrictSeq StakePoolRelay
sppVrf :: StakePoolParams -> VRFVerKeyHash StakePoolVRF
..} =
    HSSet Integer
-> Integer -> Rational -> Integer -> Credential -> StakePoolParams
Agda.StakePoolParams
      (HSSet Integer
 -> Integer -> Rational -> Integer -> Credential -> StakePoolParams)
-> SpecTransM DijkstraEra () (HSSet Integer)
-> SpecTransM
     DijkstraEra
     ()
     (Integer -> Rational -> Integer -> Credential -> StakePoolParams)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set (KeyHash Staking)
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (Set (KeyHash Staking)))
     (SpecRep DijkstraEra (Set (KeyHash Staking)))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep Set (KeyHash Staking)
sppOwners
      SpecTransM
  DijkstraEra
  ()
  (Integer -> Rational -> Integer -> Credential -> StakePoolParams)
-> SpecTransM DijkstraEra () Integer
-> SpecTransM
     DijkstraEra
     ()
     (Rational -> Integer -> Credential -> StakePoolParams)
forall a b.
SpecTransM DijkstraEra () (a -> b)
-> SpecTransM DijkstraEra () a -> SpecTransM DijkstraEra () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Coin
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra Coin)
     (SpecRep DijkstraEra Coin)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep Coin
sppCost
      SpecTransM
  DijkstraEra
  ()
  (Rational -> Integer -> Credential -> StakePoolParams)
-> SpecTransM DijkstraEra () Rational
-> SpecTransM
     DijkstraEra () (Integer -> Credential -> StakePoolParams)
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
<*> UnitInterval
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra UnitInterval)
     (SpecRep DijkstraEra UnitInterval)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep UnitInterval
sppMargin
      SpecTransM
  DijkstraEra () (Integer -> Credential -> StakePoolParams)
-> SpecTransM DijkstraEra () Integer
-> SpecTransM DijkstraEra () (Credential -> StakePoolParams)
forall a b.
SpecTransM DijkstraEra () (a -> b)
-> SpecTransM DijkstraEra () a -> SpecTransM DijkstraEra () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Coin
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra Coin)
     (SpecRep DijkstraEra Coin)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep Coin
sppPledge
      SpecTransM DijkstraEra () (Credential -> StakePoolParams)
-> SpecTransM DijkstraEra () Credential
-> SpecTransM DijkstraEra () StakePoolParams
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
<*> Credential Staking
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (Credential Staking))
     (SpecRep DijkstraEra (Credential Staking))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep (AccountAddress
sppAccountAddress AccountAddress
-> Getting (Credential Staking) AccountAddress (Credential Staking)
-> Credential Staking
forall s a. s -> Getting a s a -> a
^. Getting (Credential Staking) AccountAddress (Credential Staking)
Lens' AccountAddress (Credential Staking)
accountAddressCredentialL)

instance SpecTranslate DijkstraEra DRep where
  type SpecRep DijkstraEra DRep = Agda.VDeleg

  toSpecRep :: DRep
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra DRep)
     (SpecRep DijkstraEra DRep)
toSpecRep (DRepCredential Credential DRepRole
c) = Credential -> VDeleg
Agda.VDelegCredential (Credential -> VDeleg)
-> SpecTransM DijkstraEra () Credential
-> SpecTransM DijkstraEra () VDeleg
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Credential DRepRole
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (Credential DRepRole))
     (SpecRep DijkstraEra (Credential DRepRole))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep Credential DRepRole
c
  toSpecRep DRep
DRepAlwaysAbstain = VDeleg -> SpecTransM DijkstraEra () VDeleg
forall a. a -> SpecTransM DijkstraEra () a
forall (f :: * -> *) a. Applicative f => a -> f a
pure VDeleg
Agda.VDelegAbstain
  toSpecRep DRep
DRepAlwaysNoConfidence = VDeleg -> SpecTransM DijkstraEra () VDeleg
forall a. a -> SpecTransM DijkstraEra () a
forall (f :: * -> *) a. Applicative f => a -> f a
pure VDeleg
Agda.VDelegNoConfidence

instance SpecTranslate DijkstraEra Url where
  type SpecRep DijkstraEra Url = T.Text
  toSpecRep :: Url
-> SpecTransM
     DijkstraEra (SpecContext DijkstraEra Url) (SpecRep DijkstraEra Url)
toSpecRep = Text -> SpecTransM DijkstraEra () Text
forall a. a -> SpecTransM DijkstraEra () a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Text -> SpecTransM DijkstraEra () Text)
-> (Url -> Text) -> Url -> SpecTransM DijkstraEra () Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Url -> Text
urlToText

instance SpecTranslate DijkstraEra Anchor where
  type SpecRep DijkstraEra Anchor = Agda.Anchor
  toSpecRep :: Anchor
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra Anchor)
     (SpecRep DijkstraEra Anchor)
toSpecRep (Anchor Url
url SafeHash AnchorData
h) = Text -> Integer -> Anchor
Agda.Anchor (Text -> Integer -> Anchor)
-> SpecTransM DijkstraEra () Text
-> SpecTransM DijkstraEra () (Integer -> Anchor)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Url
-> SpecTransM
     DijkstraEra (SpecContext DijkstraEra Url) (SpecRep DijkstraEra Url)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep Url
url SpecTransM DijkstraEra () (Integer -> Anchor)
-> SpecTransM DijkstraEra () Integer
-> SpecTransM DijkstraEra () Anchor
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
<*> SafeHash AnchorData
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (SafeHash AnchorData))
     (SpecRep DijkstraEra (SafeHash AnchorData))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep SafeHash AnchorData
h

instance SpecTranslate DijkstraEra Withdrawals where
  type SpecRep DijkstraEra Withdrawals = Agda.Withdrawals

  toSpecRep :: Withdrawals
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra Withdrawals)
     (SpecRep DijkstraEra Withdrawals)
toSpecRep (Withdrawals Map AccountAddress Coin
w) = Map AccountAddress Coin
-> SpecTransM
     DijkstraEra
     ()
     (HSMap
        (SpecRep DijkstraEra AccountAddress) (SpecRep DijkstraEra Coin))
forall era k v ctx.
(SpecTranslate era k, SpecTranslate era v, SpecContext era k ~ ctx,
 SpecContext era v ~ ctx) =>
Map k v
-> SpecTransM era ctx (HSMap (SpecRep era k) (SpecRep era v))
toSpecRepMap Map AccountAddress Coin
w

instance SpecTranslate DijkstraEra IsValid where
  type SpecRep DijkstraEra IsValid = Bool

  toSpecRep :: IsValid
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra IsValid)
     (SpecRep DijkstraEra IsValid)
toSpecRep (IsValid Bool
b) = Bool -> SpecTransM DijkstraEra () Bool
forall a. a -> SpecTransM DijkstraEra () a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
b

instance SpecTranslate DijkstraEra (GovPurposeId r) where
  type SpecRep DijkstraEra (GovPurposeId r) = (Agda.TxId, Integer)

  toSpecRep :: GovPurposeId r
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (GovPurposeId r))
     (SpecRep DijkstraEra (GovPurposeId r))
toSpecRep (GovPurposeId GovActionId
gaId) = GovActionId
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra GovActionId)
     (SpecRep DijkstraEra GovActionId)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep GovActionId
gaId

instance SpecTranslate DijkstraEra (Committee DijkstraEra) where
  type
    SpecRep DijkstraEra (Committee DijkstraEra) =
      (Agda.HSMap Agda.Credential Agda.Epoch, Agda.Rational)

  toSpecRep :: Committee DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (Committee DijkstraEra))
     (SpecRep DijkstraEra (Committee DijkstraEra))
toSpecRep (Committee Map (Credential ColdCommitteeRole) EpochNo
members UnitInterval
threshold) = (,) (HSMap Credential Integer
 -> Rational -> (HSMap Credential Integer, Rational))
-> SpecTransM DijkstraEra () (HSMap Credential Integer)
-> SpecTransM
     DijkstraEra () (Rational -> (HSMap Credential Integer, Rational))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map (Credential ColdCommitteeRole) EpochNo
-> SpecTransM
     DijkstraEra
     ()
     (HSMap
        (SpecRep DijkstraEra (Credential ColdCommitteeRole))
        (SpecRep DijkstraEra EpochNo))
forall era k v ctx.
(SpecTranslate era k, SpecTranslate era v, SpecContext era k ~ ctx,
 SpecContext era v ~ ctx) =>
Map k v
-> SpecTransM era ctx (HSMap (SpecRep era k) (SpecRep era v))
toSpecRepMap Map (Credential ColdCommitteeRole) EpochNo
members SpecTransM
  DijkstraEra () (Rational -> (HSMap Credential Integer, Rational))
-> SpecTransM DijkstraEra () Rational
-> SpecTransM DijkstraEra () (HSMap Credential Integer, Rational)
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
<*> UnitInterval
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra UnitInterval)
     (SpecRep DijkstraEra UnitInterval)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep UnitInterval
threshold

instance SpecTranslate DijkstraEra (Constitution DijkstraEra) where
  type SpecRep DijkstraEra (Constitution DijkstraEra) = (Agda.DataHash, Maybe Agda.ScriptHash)

  toSpecRep :: Constitution DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (Constitution DijkstraEra))
     (SpecRep DijkstraEra (Constitution DijkstraEra))
toSpecRep (Constitution (Anchor Url
_ SafeHash AnchorData
h) StrictMaybe ScriptHash
policy) = (SafeHash AnchorData, StrictMaybe ScriptHash)
-> SpecTransM
     DijkstraEra
     ()
     (SpecRep DijkstraEra (SafeHash AnchorData),
      SpecRep DijkstraEra (StrictMaybe ScriptHash))
forall era a b ctx.
(SpecTranslate era a, SpecTranslate era b, SpecContext era a ~ ctx,
 SpecContext era b ~ ctx) =>
(a, b) -> SpecTransM era ctx (SpecRep era a, SpecRep era b)
toSpecRepTuple (SafeHash AnchorData
h, StrictMaybe ScriptHash
policy)

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

  toSpecRep :: EnactState DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (EnactState DijkstraEra))
     (SpecRep DijkstraEra (EnactState DijkstraEra))
toSpecRep EnactState {Map (Credential Staking) Coin
StrictMaybe (Committee DijkstraEra)
PParams DijkstraEra
Constitution DijkstraEra
GovRelation StrictMaybe
Coin
ensCommittee :: StrictMaybe (Committee DijkstraEra)
ensConstitution :: Constitution DijkstraEra
ensCurPParams :: PParams DijkstraEra
ensPrevPParams :: PParams DijkstraEra
ensTreasury :: Coin
ensWithdrawals :: Map (Credential Staking) Coin
ensPrevGovActionIds :: GovRelation StrictMaybe
ensPrevGovActionIds :: forall era. EnactState era -> GovRelation StrictMaybe
ensWithdrawals :: forall era. EnactState era -> Map (Credential Staking) Coin
ensTreasury :: forall era. EnactState era -> Coin
ensPrevPParams :: forall era. EnactState era -> PParams era
ensCurPParams :: forall era. EnactState era -> PParams era
ensConstitution :: forall era. EnactState era -> Constitution era
ensCommittee :: forall era. EnactState era -> StrictMaybe (Committee era)
..} =
    (Maybe (HSMap Credential Integer, Rational), (Integer, Integer))
-> ((Integer, Maybe Integer), (Integer, Integer))
-> ((Integer, Integer), (Integer, Integer))
-> (PParams, (Integer, Integer))
-> HSMap RewardAddress Integer
-> EnactState
Agda.MkEnactState
      ((Maybe (HSMap Credential Integer, Rational), (Integer, Integer))
 -> ((Integer, Maybe Integer), (Integer, Integer))
 -> ((Integer, Integer), (Integer, Integer))
 -> (PParams, (Integer, Integer))
 -> HSMap RewardAddress Integer
 -> EnactState)
-> SpecTransM
     DijkstraEra
     ()
     (Maybe (HSMap Credential Integer, Rational), (Integer, Integer))
-> SpecTransM
     DijkstraEra
     ()
     (((Integer, Maybe Integer), (Integer, Integer))
      -> ((Integer, Integer), (Integer, Integer))
      -> (PParams, (Integer, Integer))
      -> HSMap RewardAddress Integer
      -> EnactState)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StrictMaybe (Committee DijkstraEra)
-> StrictMaybe (GovPurposeId 'CommitteePurpose)
-> SpecTransM
     DijkstraEra
     ()
     (SpecRep DijkstraEra (StrictMaybe (Committee DijkstraEra)),
      (Integer, Integer))
forall a (p :: GovActionPurpose).
(SpecTranslate DijkstraEra a, SpecContext DijkstraEra a ~ ()) =>
a
-> StrictMaybe (GovPurposeId p)
-> SpecTransM
     DijkstraEra () (SpecRep DijkstraEra a, (Integer, Integer))
transHashProtected StrictMaybe (Committee DijkstraEra)
ensCommittee StrictMaybe (GovPurposeId 'CommitteePurpose)
grCommittee
      SpecTransM
  DijkstraEra
  ()
  (((Integer, Maybe Integer), (Integer, Integer))
   -> ((Integer, Integer), (Integer, Integer))
   -> (PParams, (Integer, Integer))
   -> HSMap RewardAddress Integer
   -> EnactState)
-> SpecTransM
     DijkstraEra () ((Integer, Maybe Integer), (Integer, Integer))
-> SpecTransM
     DijkstraEra
     ()
     (((Integer, Integer), (Integer, Integer))
      -> (PParams, (Integer, Integer))
      -> HSMap RewardAddress Integer
      -> EnactState)
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
<*> Constitution DijkstraEra
-> StrictMaybe (GovPurposeId 'ConstitutionPurpose)
-> SpecTransM
     DijkstraEra
     ()
     (SpecRep DijkstraEra (Constitution DijkstraEra),
      (Integer, Integer))
forall a (p :: GovActionPurpose).
(SpecTranslate DijkstraEra a, SpecContext DijkstraEra a ~ ()) =>
a
-> StrictMaybe (GovPurposeId p)
-> SpecTransM
     DijkstraEra () (SpecRep DijkstraEra a, (Integer, Integer))
transHashProtected Constitution DijkstraEra
ensConstitution StrictMaybe (GovPurposeId 'ConstitutionPurpose)
grConstitution
      SpecTransM
  DijkstraEra
  ()
  (((Integer, Integer), (Integer, Integer))
   -> (PParams, (Integer, Integer))
   -> HSMap RewardAddress Integer
   -> EnactState)
-> SpecTransM
     DijkstraEra () ((Integer, Integer), (Integer, Integer))
-> SpecTransM
     DijkstraEra
     ()
     ((PParams, (Integer, Integer))
      -> HSMap RewardAddress Integer -> EnactState)
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
<*> ProtVer
-> StrictMaybe (GovPurposeId 'HardForkPurpose)
-> SpecTransM
     DijkstraEra () (SpecRep DijkstraEra ProtVer, (Integer, Integer))
forall a (p :: GovActionPurpose).
(SpecTranslate DijkstraEra a, SpecContext DijkstraEra a ~ ()) =>
a
-> StrictMaybe (GovPurposeId p)
-> SpecTransM
     DijkstraEra () (SpecRep DijkstraEra a, (Integer, Integer))
transHashProtected (PParams DijkstraEra
ensCurPParams PParams DijkstraEra
-> Getting ProtVer (PParams DijkstraEra) ProtVer -> ProtVer
forall s a. s -> Getting a s a -> a
^. Getting ProtVer (PParams DijkstraEra) ProtVer
forall era. EraPParams era => Lens' (PParams era) ProtVer
Lens' (PParams DijkstraEra) ProtVer
ppProtocolVersionL) StrictMaybe (GovPurposeId 'HardForkPurpose)
grHardFork
      SpecTransM
  DijkstraEra
  ()
  ((PParams, (Integer, Integer))
   -> HSMap RewardAddress Integer -> EnactState)
-> SpecTransM DijkstraEra () (PParams, (Integer, Integer))
-> SpecTransM
     DijkstraEra () (HSMap RewardAddress Integer -> EnactState)
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
<*> PParams DijkstraEra
-> StrictMaybe (GovPurposeId 'PParamUpdatePurpose)
-> SpecTransM
     DijkstraEra
     ()
     (SpecRep DijkstraEra (PParams DijkstraEra), (Integer, Integer))
forall a (p :: GovActionPurpose).
(SpecTranslate DijkstraEra a, SpecContext DijkstraEra a ~ ()) =>
a
-> StrictMaybe (GovPurposeId p)
-> SpecTransM
     DijkstraEra () (SpecRep DijkstraEra a, (Integer, Integer))
transHashProtected PParams DijkstraEra
ensCurPParams StrictMaybe (GovPurposeId 'PParamUpdatePurpose)
grPParamUpdate
      SpecTransM
  DijkstraEra () (HSMap RewardAddress Integer -> EnactState)
-> SpecTransM DijkstraEra () (HSMap RewardAddress Integer)
-> SpecTransM DijkstraEra () EnactState
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
<*> Map (Credential Staking) Coin
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (Credential Staking))
     (HSMap RewardAddress Integer)
forall {era} {a}.
(SpecRep era a ~ Credential, SpecContext era a ~ (),
 SpecTranslate era a) =>
Map a Coin
-> SpecTransM era (SpecContext era a) (HSMap RewardAddress Integer)
transWithdrawals Map (Credential Staking) Coin
ensWithdrawals
    where
      GovRelation {StrictMaybe (GovPurposeId 'PParamUpdatePurpose)
StrictMaybe (GovPurposeId 'HardForkPurpose)
StrictMaybe (GovPurposeId 'CommitteePurpose)
StrictMaybe (GovPurposeId 'ConstitutionPurpose)
grCommittee :: StrictMaybe (GovPurposeId 'CommitteePurpose)
grConstitution :: StrictMaybe (GovPurposeId 'ConstitutionPurpose)
grHardFork :: StrictMaybe (GovPurposeId 'HardForkPurpose)
grPParamUpdate :: StrictMaybe (GovPurposeId 'PParamUpdatePurpose)
grConstitution :: forall (f :: * -> *).
GovRelation f -> f (GovPurposeId 'ConstitutionPurpose)
grCommittee :: forall (f :: * -> *).
GovRelation f -> f (GovPurposeId 'CommitteePurpose)
grHardFork :: forall (f :: * -> *).
GovRelation f -> f (GovPurposeId 'HardForkPurpose)
grPParamUpdate :: forall (f :: * -> *).
GovRelation f -> f (GovPurposeId 'PParamUpdatePurpose)
..} = GovRelation StrictMaybe
ensPrevGovActionIds
      transWithdrawals :: Map a Coin
-> SpecTransM era (SpecContext era a) (HSMap RewardAddress Integer)
transWithdrawals Map a Coin
ws = ([(RewardAddress, Integer)] -> HSMap RewardAddress Integer)
-> SpecTransM era (SpecContext era a) [(RewardAddress, Integer)]
-> SpecTransM era (SpecContext era a) (HSMap RewardAddress Integer)
forall a b.
(a -> b)
-> SpecTransM era (SpecContext era a) a
-> SpecTransM era (SpecContext era a) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [(RewardAddress, Integer)] -> HSMap RewardAddress Integer
forall k v. [(k, v)] -> HSMap k v
Agda.MkHSMap (SpecTransM era (SpecContext era a) [(RewardAddress, Integer)]
 -> SpecTransM
      era (SpecContext era a) (HSMap RewardAddress Integer))
-> (((a, Coin)
     -> SpecTransM era (SpecContext era a) (RewardAddress, Integer))
    -> SpecTransM era (SpecContext era a) [(RewardAddress, Integer)])
-> ((a, Coin)
    -> SpecTransM era (SpecContext era a) (RewardAddress, Integer))
-> SpecTransM era (SpecContext era a) (HSMap RewardAddress Integer)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(a, Coin)]
-> ((a, Coin)
    -> SpecTransM era (SpecContext era a) (RewardAddress, Integer))
-> SpecTransM era (SpecContext era a) [(RewardAddress, Integer)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (Map a Coin -> [(a, Coin)]
forall k a. Map k a -> [(k, a)]
Map.toList Map a Coin
ws) (((a, Coin)
  -> SpecTransM era (SpecContext era a) (RewardAddress, Integer))
 -> SpecTransM
      era (SpecContext era a) (HSMap RewardAddress Integer))
-> ((a, Coin)
    -> SpecTransM era (SpecContext era a) (RewardAddress, Integer))
-> SpecTransM era (SpecContext era a) (HSMap RewardAddress Integer)
forall a b. (a -> b) -> a -> b
$
        \(a
cred, Coin Integer
amount) -> do
          agdaCred <- a -> SpecTransM era (SpecContext era a) (SpecRep era a)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep a
cred
          network <- toSpecRep Testnet
          pure (Agda.RewardAddress network agdaCred, amount)
      transHashProtected ::
        (SpecTranslate DijkstraEra a, SpecContext DijkstraEra a ~ ()) =>
        a ->
        StrictMaybe (GovPurposeId p) ->
        SpecTransM DijkstraEra () (SpecRep DijkstraEra a, (Integer, Integer))
      transHashProtected :: forall a (p :: GovActionPurpose).
(SpecTranslate DijkstraEra a, SpecContext DijkstraEra a ~ ()) =>
a
-> StrictMaybe (GovPurposeId p)
-> SpecTransM
     DijkstraEra () (SpecRep DijkstraEra a, (Integer, Integer))
transHashProtected a
x StrictMaybe (GovPurposeId p)
h = do
        committee <- a
-> SpecTransM
     DijkstraEra (SpecContext DijkstraEra a) (SpecRep DijkstraEra a)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep a
x
        agdaLastId <- case h of
          SJust GovPurposeId p
lastId -> GovPurposeId p
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (GovPurposeId p))
     (SpecRep DijkstraEra (GovPurposeId p))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep GovPurposeId p
lastId
          StrictMaybe (GovPurposeId p)
SNothing -> (Integer, Integer) -> SpecTransM DijkstraEra () (Integer, Integer)
forall a. a -> SpecTransM DijkstraEra () a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer
0, Integer
0)
        pure (committee, agdaLastId)

instance SpecTranslate DijkstraEra Voter where
  type SpecRep DijkstraEra Voter = Agda.GovVoter

  toSpecRep :: Voter
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra Voter)
     (SpecRep DijkstraEra Voter)
toSpecRep (CommitteeVoter Credential HotCommitteeRole
c) = (GovRole
Agda.CC,) (Credential -> (GovRole, Credential))
-> SpecTransM DijkstraEra () Credential
-> SpecTransM DijkstraEra () (GovRole, Credential)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Credential HotCommitteeRole
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (Credential HotCommitteeRole))
     (SpecRep DijkstraEra (Credential HotCommitteeRole))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep Credential HotCommitteeRole
c
  toSpecRep (DRepVoter Credential DRepRole
c) = (GovRole
Agda.DRep,) (Credential -> (GovRole, Credential))
-> SpecTransM DijkstraEra () Credential
-> SpecTransM DijkstraEra () (GovRole, Credential)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Credential DRepRole
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (Credential DRepRole))
     (SpecRep DijkstraEra (Credential DRepRole))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep Credential DRepRole
c
  toSpecRep (StakePoolVoter KeyHash StakePool
kh) = (GovRole
Agda.SPO,) (Credential -> (GovRole, Credential))
-> SpecTransM DijkstraEra () Credential
-> SpecTransM DijkstraEra () (GovRole, Credential)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Credential StakePool
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (Credential StakePool))
     (SpecRep DijkstraEra (Credential StakePool))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep (KeyHash StakePool -> Credential StakePool
forall (kr :: KeyRole). KeyHash kr -> Credential kr
KeyHashObj KeyHash StakePool
kh)

instance SpecTranslate DijkstraEra Vote where
  type SpecRep DijkstraEra Vote = Agda.Vote

  toSpecRep :: Vote
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra Vote)
     (SpecRep DijkstraEra Vote)
toSpecRep Vote
VoteYes = Vote -> SpecTransM DijkstraEra () Vote
forall a. a -> SpecTransM DijkstraEra () a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Vote
Agda.Yes
  toSpecRep Vote
VoteNo = Vote -> SpecTransM DijkstraEra () Vote
forall a. a -> SpecTransM DijkstraEra () a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Vote
Agda.No
  toSpecRep Vote
Abstain = Vote -> SpecTransM DijkstraEra () Vote
forall a. a -> SpecTransM DijkstraEra () a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Vote
Agda.Abstain

instance SpecTranslate DijkstraEra (VotingProcedures DijkstraEra) where
  type SpecRep DijkstraEra (VotingProcedures DijkstraEra) = [Agda.GovVote]

  toSpecRep :: VotingProcedures DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (VotingProcedures DijkstraEra))
     (SpecRep DijkstraEra (VotingProcedures DijkstraEra))
toSpecRep = (Voter
 -> GovActionId
 -> VotingProcedure DijkstraEra
 -> SpecTransM DijkstraEra () [GovVote]
 -> SpecTransM DijkstraEra () [GovVote])
-> SpecTransM DijkstraEra () [GovVote]
-> VotingProcedures DijkstraEra
-> SpecTransM DijkstraEra () [GovVote]
forall era c.
(Voter -> GovActionId -> VotingProcedure era -> c -> c)
-> c -> VotingProcedures era -> c
foldrVotingProcedures Voter
-> GovActionId
-> VotingProcedure DijkstraEra
-> SpecTransM DijkstraEra () [GovVote]
-> SpecTransM DijkstraEra () [GovVote]
go ([GovVote] -> SpecTransM DijkstraEra () [GovVote]
forall a. a -> SpecTransM DijkstraEra () a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [])
    where
      go ::
        Voter ->
        GovActionId ->
        VotingProcedure DijkstraEra ->
        SpecTransM DijkstraEra () [Agda.GovVote] ->
        SpecTransM DijkstraEra () [Agda.GovVote]
      go :: Voter
-> GovActionId
-> VotingProcedure DijkstraEra
-> SpecTransM DijkstraEra () [GovVote]
-> SpecTransM DijkstraEra () [GovVote]
go Voter
voter GovActionId
gaId VotingProcedure DijkstraEra
votingProcedure SpecTransM DijkstraEra () [GovVote]
m =
        (:)
          (GovVote -> [GovVote] -> [GovVote])
-> SpecTransM DijkstraEra () GovVote
-> SpecTransM DijkstraEra () ([GovVote] -> [GovVote])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ( (Integer, Integer)
-> (GovRole, Credential) -> Vote -> Maybe Anchor -> GovVote
Agda.MkGovVote
                  ((Integer, Integer)
 -> (GovRole, Credential) -> Vote -> Maybe Anchor -> GovVote)
-> SpecTransM DijkstraEra () (Integer, Integer)
-> SpecTransM
     DijkstraEra
     ()
     ((GovRole, Credential) -> Vote -> Maybe Anchor -> GovVote)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GovActionId
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra GovActionId)
     (SpecRep DijkstraEra GovActionId)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep GovActionId
gaId
                  SpecTransM
  DijkstraEra
  ()
  ((GovRole, Credential) -> Vote -> Maybe Anchor -> GovVote)
-> SpecTransM DijkstraEra () (GovRole, Credential)
-> SpecTransM DijkstraEra () (Vote -> Maybe Anchor -> GovVote)
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
<*> Voter
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra Voter)
     (SpecRep DijkstraEra Voter)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep Voter
voter
                  SpecTransM DijkstraEra () (Vote -> Maybe Anchor -> GovVote)
-> SpecTransM DijkstraEra () Vote
-> SpecTransM DijkstraEra () (Maybe Anchor -> GovVote)
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
<*> Vote
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra Vote)
     (SpecRep DijkstraEra Vote)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep (VotingProcedure DijkstraEra -> Vote
forall era. VotingProcedure era -> Vote
vProcVote VotingProcedure DijkstraEra
votingProcedure)
                  SpecTransM DijkstraEra () (Maybe Anchor -> GovVote)
-> SpecTransM DijkstraEra () (Maybe Anchor)
-> SpecTransM DijkstraEra () GovVote
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 Anchor
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (StrictMaybe Anchor))
     (SpecRep DijkstraEra (StrictMaybe Anchor))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep (VotingProcedure DijkstraEra -> StrictMaybe Anchor
forall era. VotingProcedure era -> StrictMaybe Anchor
vProcAnchor VotingProcedure DijkstraEra
votingProcedure)
              )
          SpecTransM DijkstraEra () ([GovVote] -> [GovVote])
-> SpecTransM DijkstraEra () [GovVote]
-> SpecTransM DijkstraEra () [GovVote]
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 () [GovVote]
m

instance SpecTranslate DijkstraEra (DijkstraPParams StrictMaybe DijkstraEra) where
  type SpecRep DijkstraEra (DijkstraPParams StrictMaybe DijkstraEra) = Agda.PParamsUpdate

  toSpecRep :: DijkstraPParams StrictMaybe DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (DijkstraPParams StrictMaybe DijkstraEra))
     (SpecRep DijkstraEra (DijkstraPParams StrictMaybe DijkstraEra))
toSpecRep (DijkstraPParams {THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word16
THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
THKD
  ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe OrdExUnits
THKD
  ('PPGroups 'NetworkGroup 'SecurityGroup)
  StrictMaybe
  (NonZero Word32)
THKD
  ('PPGroups 'NetworkGroup 'SecurityGroup)
  StrictMaybe
  PositiveInterval
THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) StrictMaybe Word16
THKD
  ('PPGroups 'NetworkGroup 'NoStakePoolGroup) StrictMaybe OrdExUnits
THKD
  ('PPGroups 'EconomicGroup 'SecurityGroup) StrictMaybe CoinPerByte
THKD
  ('PPGroups 'EconomicGroup 'SecurityGroup)
  StrictMaybe
  (CompactForm Coin)
THKD
  ('PPGroups 'EconomicGroup 'SecurityGroup)
  StrictMaybe
  NonNegativeInterval
THKD
  ('PPGroups 'EconomicGroup 'NoStakePoolGroup) StrictMaybe Prices
THKD
  ('PPGroups 'EconomicGroup 'NoStakePoolGroup)
  StrictMaybe
  (CompactForm Coin)
THKD
  ('PPGroups 'EconomicGroup 'NoStakePoolGroup)
  StrictMaybe
  UnitInterval
THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) StrictMaybe Word16
THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
  StrictMaybe
  CostModels
THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
  StrictMaybe
  EpochInterval
THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
  StrictMaybe
  NonNegativeInterval
THKD
  ('PPGroups 'GovGroup 'SecurityGroup) StrictMaybe (CompactForm Coin)
THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) StrictMaybe Word16
THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup)
  StrictMaybe
  DRepVotingThresholds
THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup)
  StrictMaybe
  PoolVotingThresholds
THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup) StrictMaybe EpochInterval
THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup)
  StrictMaybe
  (CompactForm Coin)
HKDNoUpdate StrictMaybe ProtVer
dppRefScriptCostMultiplier :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f PositiveInterval
dppRefScriptCostStride :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f (NonZero Word32)
dppMaxRefScriptSizePerTx :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f Word32
dppMaxRefScriptSizePerBlock :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f Word32
dppMinFeeRefScriptCostPerByte :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD
     ('PPGroups 'EconomicGroup 'SecurityGroup) f NonNegativeInterval
dppDRepActivity :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) f EpochInterval
dppDRepDeposit :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD
     ('PPGroups 'GovGroup 'NoStakePoolGroup) f (CompactForm Coin)
dppGovActionDeposit :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD ('PPGroups 'GovGroup 'SecurityGroup) f (CompactForm Coin)
dppGovActionLifetime :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) f EpochInterval
dppCommitteeMaxTermLength :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) f EpochInterval
dppCommitteeMinSize :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) f Word16
dppDRepVotingThresholds :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD
     ('PPGroups 'GovGroup 'NoStakePoolGroup) f DRepVotingThresholds
dppPoolVotingThresholds :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD
     ('PPGroups 'GovGroup 'NoStakePoolGroup) f PoolVotingThresholds
dppMaxCollateralInputs :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) f Word16
dppCollateralPercentage :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) f Word16
dppMaxValSize :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f Word32
dppMaxBlockExUnits :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f OrdExUnits
dppMaxTxExUnits :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) f OrdExUnits
dppPrices :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f Prices
dppCostModels :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) f CostModels
dppCoinsPerUTxOByte :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD ('PPGroups 'EconomicGroup 'SecurityGroup) f CoinPerByte
dppMinPoolCost :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD
     ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f (CompactForm Coin)
dppProtocolVersion :: forall (f :: * -> *) era.
DijkstraPParams f era -> HKDNoUpdate f ProtVer
dppTau :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f UnitInterval
dppRho :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f UnitInterval
dppA0 :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD
     ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) f NonNegativeInterval
dppNOpt :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) f Word16
dppEMax :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD
     ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) f EpochInterval
dppPoolDeposit :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD
     ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f (CompactForm Coin)
dppKeyDeposit :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD
     ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f (CompactForm Coin)
dppMaxBHSize :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f Word16
dppMaxTxSize :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f Word32
dppMaxBBSize :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f Word32
dppTxFeeFixed :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD
     ('PPGroups 'EconomicGroup 'SecurityGroup) f (CompactForm Coin)
dppTxFeePerByte :: forall (f :: * -> *) era.
DijkstraPParams f era
-> THKD ('PPGroups 'EconomicGroup 'SecurityGroup) f CoinPerByte
dppTxFeePerByte :: THKD
  ('PPGroups 'EconomicGroup 'SecurityGroup) StrictMaybe CoinPerByte
dppTxFeeFixed :: THKD
  ('PPGroups 'EconomicGroup 'SecurityGroup)
  StrictMaybe
  (CompactForm Coin)
dppMaxBBSize :: THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
dppMaxTxSize :: THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
dppMaxBHSize :: THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word16
dppKeyDeposit :: THKD
  ('PPGroups 'EconomicGroup 'NoStakePoolGroup)
  StrictMaybe
  (CompactForm Coin)
dppPoolDeposit :: THKD
  ('PPGroups 'EconomicGroup 'NoStakePoolGroup)
  StrictMaybe
  (CompactForm Coin)
dppEMax :: THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
  StrictMaybe
  EpochInterval
dppNOpt :: THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) StrictMaybe Word16
dppA0 :: THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
  StrictMaybe
  NonNegativeInterval
dppRho :: THKD
  ('PPGroups 'EconomicGroup 'NoStakePoolGroup)
  StrictMaybe
  UnitInterval
dppTau :: THKD
  ('PPGroups 'EconomicGroup 'NoStakePoolGroup)
  StrictMaybe
  UnitInterval
dppProtocolVersion :: HKDNoUpdate StrictMaybe ProtVer
dppMinPoolCost :: THKD
  ('PPGroups 'EconomicGroup 'NoStakePoolGroup)
  StrictMaybe
  (CompactForm Coin)
dppCoinsPerUTxOByte :: THKD
  ('PPGroups 'EconomicGroup 'SecurityGroup) StrictMaybe CoinPerByte
dppCostModels :: THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
  StrictMaybe
  CostModels
dppPrices :: THKD
  ('PPGroups 'EconomicGroup 'NoStakePoolGroup) StrictMaybe Prices
dppMaxTxExUnits :: THKD
  ('PPGroups 'NetworkGroup 'NoStakePoolGroup) StrictMaybe OrdExUnits
dppMaxBlockExUnits :: THKD
  ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe OrdExUnits
dppMaxValSize :: THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
dppCollateralPercentage :: THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) StrictMaybe Word16
dppMaxCollateralInputs :: THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) StrictMaybe Word16
dppPoolVotingThresholds :: THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup)
  StrictMaybe
  PoolVotingThresholds
dppDRepVotingThresholds :: THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup)
  StrictMaybe
  DRepVotingThresholds
dppCommitteeMinSize :: THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) StrictMaybe Word16
dppCommitteeMaxTermLength :: THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup) StrictMaybe EpochInterval
dppGovActionLifetime :: THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup) StrictMaybe EpochInterval
dppGovActionDeposit :: THKD
  ('PPGroups 'GovGroup 'SecurityGroup) StrictMaybe (CompactForm Coin)
dppDRepDeposit :: THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup)
  StrictMaybe
  (CompactForm Coin)
dppDRepActivity :: THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup) StrictMaybe EpochInterval
dppMinFeeRefScriptCostPerByte :: THKD
  ('PPGroups 'EconomicGroup 'SecurityGroup)
  StrictMaybe
  NonNegativeInterval
dppMaxRefScriptSizePerBlock :: THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
dppMaxRefScriptSizePerTx :: THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
dppRefScriptCostStride :: THKD
  ('PPGroups 'NetworkGroup 'SecurityGroup)
  StrictMaybe
  (NonZero Word32)
dppRefScriptCostMultiplier :: THKD
  ('PPGroups 'NetworkGroup 'SecurityGroup)
  StrictMaybe
  PositiveInterval
..}) = do
    ppuA <- THKD
  ('PPGroups 'EconomicGroup 'SecurityGroup) StrictMaybe CoinPerByte
-> SpecTransM
     DijkstraEra
     (SpecContext
        DijkstraEra
        (THKD
           ('PPGroups 'EconomicGroup 'SecurityGroup) StrictMaybe CoinPerByte))
     (SpecRep
        DijkstraEra
        (THKD
           ('PPGroups 'EconomicGroup 'SecurityGroup) StrictMaybe CoinPerByte))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep THKD
  ('PPGroups 'EconomicGroup 'SecurityGroup) StrictMaybe CoinPerByte
dppTxFeePerByte
    ppuB <- toSpecRep dppTxFeeFixed
    ppuA0 <- toSpecRep dppA0
    ppuMinFeeRefScriptCoinsPerByte <- toSpecRep dppMinFeeRefScriptCostPerByte
    ppuCollateralPercentage <- toSpecRep dppCollateralPercentage
    let
      ppuMaxBlockSize = (Word32 -> Integer) -> Maybe Word32 -> Maybe Integer
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger (Maybe Word32 -> Maybe Integer)
-> (THKD
      ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
    -> Maybe Word32)
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
-> Maybe Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StrictMaybe Word32 -> Maybe Word32
forall a. StrictMaybe a -> Maybe a
strictMaybeToMaybe (StrictMaybe Word32 -> Maybe Word32)
-> (THKD
      ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
    -> StrictMaybe Word32)
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
-> Maybe Word32
forall b c a. (b -> c) -> (a -> b) -> a -> c
. THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
-> StrictMaybe Word32
THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
-> HKD StrictMaybe Word32
forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD (THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
 -> Maybe Integer)
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
-> Maybe Integer
forall a b. (a -> b) -> a -> b
$ THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
dppMaxBBSize
      ppuMaxTxSize = (Word32 -> Integer) -> Maybe Word32 -> Maybe Integer
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger (Maybe Word32 -> Maybe Integer)
-> (THKD
      ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
    -> Maybe Word32)
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
-> Maybe Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StrictMaybe Word32 -> Maybe Word32
forall a. StrictMaybe a -> Maybe a
strictMaybeToMaybe (StrictMaybe Word32 -> Maybe Word32)
-> (THKD
      ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
    -> StrictMaybe Word32)
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
-> Maybe Word32
forall b c a. (b -> c) -> (a -> b) -> a -> c
. THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
-> StrictMaybe Word32
THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
-> HKD StrictMaybe Word32
forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD (THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
 -> Maybe Integer)
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
-> Maybe Integer
forall a b. (a -> b) -> a -> b
$ THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
dppMaxTxSize
      ppuMaxHeaderSize = (Word16 -> Integer) -> Maybe Word16 -> Maybe Integer
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Word16 -> Integer
forall a. Integral a => a -> Integer
toInteger (Maybe Word16 -> Maybe Integer)
-> (THKD
      ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word16
    -> Maybe Word16)
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word16
-> Maybe Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StrictMaybe Word16 -> Maybe Word16
forall a. StrictMaybe a -> Maybe a
strictMaybeToMaybe (StrictMaybe Word16 -> Maybe Word16)
-> (THKD
      ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word16
    -> StrictMaybe Word16)
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word16
-> Maybe Word16
forall b c a. (b -> c) -> (a -> b) -> a -> c
. THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word16
-> StrictMaybe Word16
THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word16
-> HKD StrictMaybe Word16
forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD (THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word16
 -> Maybe Integer)
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word16
-> Maybe Integer
forall a b. (a -> b) -> a -> b
$ THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word16
dppMaxBHSize
    ppuKeyDeposit <- toSpecRep dppKeyDeposit
    ppuPoolDeposit <- toSpecRep dppPoolDeposit
    ppuEmax <- toSpecRep dppEMax
    ppuNopt <- toSpecRep (fmap toInteger . strictMaybeToMaybe $ unTHKD dppNOpt)
    let
      ppuPv = Maybe a
forall a. Maybe a
Nothing
      ppuMinUTxOValue = Maybe a
forall a. Maybe a
Nothing
    ppuCoinsPerUTxOByte <- toSpecRep dppCoinsPerUTxOByte
    ppuCostmdls <- toSpecRep dppCostModels
    ppuPrices <- toSpecRep dppPrices
    let
      ppuMaxRefScriptSizePerTx = Maybe a
forall a. Maybe a
Nothing
      ppuMaxRefScriptSizePerBlock = Maybe a
forall a. Maybe a
Nothing
      ppuRefScriptCostStride = Maybe a
forall a. Maybe a
Nothing
      ppuRefScriptCostMultiplier = Maybe a
forall a. Maybe a
Nothing
    ppuMaxTxExUnits <- toSpecRep dppMaxTxExUnits
    ppuMaxBlockExUnits <- toSpecRep dppMaxBlockExUnits
    let
      ppuMaxValSize = (Word32 -> Integer) -> Maybe Word32 -> Maybe Integer
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger (Maybe Word32 -> Maybe Integer)
-> (THKD
      ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
    -> Maybe Word32)
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
-> Maybe Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StrictMaybe Word32 -> Maybe Word32
forall a. StrictMaybe a -> Maybe a
strictMaybeToMaybe (StrictMaybe Word32 -> Maybe Word32)
-> (THKD
      ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
    -> StrictMaybe Word32)
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
-> Maybe Word32
forall b c a. (b -> c) -> (a -> b) -> a -> c
. THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
-> StrictMaybe Word32
THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
-> HKD StrictMaybe Word32
forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD (THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
 -> Maybe Integer)
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
-> Maybe Integer
forall a b. (a -> b) -> a -> b
$ THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
dppMaxValSize
      ppuMaxCollateralInputs = (Word16 -> Integer) -> Maybe Word16 -> Maybe Integer
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Word16 -> Integer
forall a. Integral a => a -> Integer
toInteger (Maybe Word16 -> Maybe Integer)
-> (THKD
      ('PPGroups 'NetworkGroup 'NoStakePoolGroup) StrictMaybe Word16
    -> Maybe Word16)
-> THKD
     ('PPGroups 'NetworkGroup 'NoStakePoolGroup) StrictMaybe Word16
-> Maybe Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StrictMaybe Word16 -> Maybe Word16
forall a. StrictMaybe a -> Maybe a
strictMaybeToMaybe (StrictMaybe Word16 -> Maybe Word16)
-> (THKD
      ('PPGroups 'NetworkGroup 'NoStakePoolGroup) StrictMaybe Word16
    -> StrictMaybe Word16)
-> THKD
     ('PPGroups 'NetworkGroup 'NoStakePoolGroup) StrictMaybe Word16
-> Maybe Word16
forall b c a. (b -> c) -> (a -> b) -> a -> c
. THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) StrictMaybe Word16
-> StrictMaybe Word16
THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) StrictMaybe Word16
-> HKD StrictMaybe Word16
forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD (THKD
   ('PPGroups 'NetworkGroup 'NoStakePoolGroup) StrictMaybe Word16
 -> Maybe Integer)
-> THKD
     ('PPGroups 'NetworkGroup 'NoStakePoolGroup) StrictMaybe Word16
-> Maybe Integer
forall a b. (a -> b) -> a -> b
$ THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) StrictMaybe Word16
dppMaxCollateralInputs
    ppuPoolThresholds <- toSpecRep dppPoolVotingThresholds
    ppuDrepThresholds <- toSpecRep dppDRepVotingThresholds
    let
      ppuCcMinSize = (Word16 -> Integer) -> Maybe Word16 -> Maybe Integer
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Word16 -> Integer
forall a. Integral a => a -> Integer
toInteger (Maybe Word16 -> Maybe Integer)
-> (StrictMaybe Word16 -> Maybe Word16)
-> StrictMaybe Word16
-> Maybe Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StrictMaybe Word16 -> Maybe Word16
forall a. StrictMaybe a -> Maybe a
strictMaybeToMaybe (StrictMaybe Word16 -> Maybe Integer)
-> StrictMaybe Word16 -> Maybe Integer
forall a b. (a -> b) -> a -> b
$ THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) StrictMaybe Word16
-> HKD StrictMaybe Word16
forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) StrictMaybe Word16
dppCommitteeMinSize
      ppuCcMaxTermLength =
        (EpochInterval -> Integer) -> Maybe EpochInterval -> Maybe Integer
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger (Word32 -> Integer)
-> (EpochInterval -> Word32) -> EpochInterval -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EpochInterval -> Word32
unEpochInterval) (Maybe EpochInterval -> Maybe Integer)
-> (StrictMaybe EpochInterval -> Maybe EpochInterval)
-> StrictMaybe EpochInterval
-> Maybe Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StrictMaybe EpochInterval -> Maybe EpochInterval
forall a. StrictMaybe a -> Maybe a
strictMaybeToMaybe (StrictMaybe EpochInterval -> Maybe Integer)
-> StrictMaybe EpochInterval -> Maybe Integer
forall a b. (a -> b) -> a -> b
$ THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup) StrictMaybe EpochInterval
-> HKD StrictMaybe EpochInterval
forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup) StrictMaybe EpochInterval
dppCommitteeMaxTermLength
    ppuGovActionLifetime <- toSpecRep dppGovActionLifetime
    ppuGovActionDeposit <- toSpecRep dppGovActionDeposit
    ppuDrepDeposit <- toSpecRep dppDRepDeposit
    ppuDrepActivity <- toSpecRep dppDRepActivity
    ppuMonetaryExpansion <- toSpecRep dppRho
    ppuTreasuryCut <- toSpecRep dppTau

    pure Agda.MkPParamsUpdate {..}

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

  toSpecRep :: GovAction DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (GovAction DijkstraEra))
     (SpecRep DijkstraEra (GovAction DijkstraEra))
toSpecRep (ParameterChange StrictMaybe (GovPurposeId 'PParamUpdatePurpose)
_ PParamsUpdate DijkstraEra
ppu StrictMaybe ScriptHash
_) = PParamsUpdate -> GovAction
Agda.ChangePParams (PParamsUpdate -> GovAction)
-> SpecTransM DijkstraEra () PParamsUpdate
-> SpecTransM DijkstraEra () GovAction
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PParamsUpdate DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (PParamsUpdate DijkstraEra))
     (SpecRep DijkstraEra (PParamsUpdate DijkstraEra))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep PParamsUpdate DijkstraEra
ppu
  toSpecRep (HardForkInitiation StrictMaybe (GovPurposeId 'HardForkPurpose)
_ ProtVer
pv) = (Integer, Integer) -> GovAction
Agda.TriggerHardFork ((Integer, Integer) -> GovAction)
-> SpecTransM DijkstraEra () (Integer, Integer)
-> SpecTransM DijkstraEra () GovAction
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ProtVer
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra ProtVer)
     (SpecRep DijkstraEra ProtVer)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep ProtVer
pv
  toSpecRep (TreasuryWithdrawals Map AccountAddress Coin
withdrawals StrictMaybe ScriptHash
_) =
    HSMap RewardAddress Integer -> GovAction
Agda.TreasuryWithdrawal
      (HSMap RewardAddress Integer -> GovAction)
-> SpecTransM DijkstraEra () (HSMap RewardAddress Integer)
-> SpecTransM DijkstraEra () GovAction
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map AccountAddress Coin
-> SpecTransM
     DijkstraEra
     ()
     (HSMap
        (SpecRep DijkstraEra AccountAddress) (SpecRep DijkstraEra Coin))
forall era k v ctx.
(SpecTranslate era k, SpecTranslate era v, SpecContext era k ~ ctx,
 SpecContext era v ~ ctx) =>
Map k v
-> SpecTransM era ctx (HSMap (SpecRep era k) (SpecRep era v))
toSpecRepMap Map AccountAddress Coin
withdrawals
  toSpecRep (NoConfidence StrictMaybe (GovPurposeId 'CommitteePurpose)
_) = GovAction -> SpecTransM DijkstraEra () GovAction
forall a. a -> SpecTransM DijkstraEra () a
forall (f :: * -> *) a. Applicative f => a -> f a
pure GovAction
Agda.NoConfidence
  toSpecRep (UpdateCommittee StrictMaybe (GovPurposeId 'CommitteePurpose)
_ Set (Credential ColdCommitteeRole)
remove Map (Credential ColdCommitteeRole) EpochNo
add UnitInterval
threshold) =
    HSMap Credential Integer
-> HSSet Credential -> Rational -> GovAction
Agda.UpdateCommittee
      (HSMap Credential Integer
 -> HSSet Credential -> Rational -> GovAction)
-> SpecTransM DijkstraEra () (HSMap Credential Integer)
-> SpecTransM
     DijkstraEra () (HSSet Credential -> Rational -> GovAction)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map (Credential ColdCommitteeRole) EpochNo
-> SpecTransM
     DijkstraEra
     ()
     (HSMap
        (SpecRep DijkstraEra (Credential ColdCommitteeRole))
        (SpecRep DijkstraEra EpochNo))
forall era k v ctx.
(SpecTranslate era k, SpecTranslate era v, SpecContext era k ~ ctx,
 SpecContext era v ~ ctx) =>
Map k v
-> SpecTransM era ctx (HSMap (SpecRep era k) (SpecRep era v))
toSpecRepMap Map (Credential ColdCommitteeRole) EpochNo
add
      SpecTransM
  DijkstraEra () (HSSet Credential -> Rational -> GovAction)
-> SpecTransM DijkstraEra () (HSSet Credential)
-> SpecTransM DijkstraEra () (Rational -> GovAction)
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
<*> Set (Credential ColdCommitteeRole)
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (Set (Credential ColdCommitteeRole)))
     (SpecRep DijkstraEra (Set (Credential ColdCommitteeRole)))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep Set (Credential ColdCommitteeRole)
remove
      SpecTransM DijkstraEra () (Rational -> GovAction)
-> SpecTransM DijkstraEra () Rational
-> SpecTransM DijkstraEra () GovAction
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
<*> UnitInterval
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra UnitInterval)
     (SpecRep DijkstraEra UnitInterval)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep UnitInterval
threshold
  toSpecRep (NewConstitution StrictMaybe (GovPurposeId 'ConstitutionPurpose)
_ (Constitution (Anchor Url
_ SafeHash AnchorData
h) StrictMaybe ScriptHash
policy)) =
    Integer -> Maybe Integer -> GovAction
Agda.NewConstitution
      (Integer -> Maybe Integer -> GovAction)
-> SpecTransM DijkstraEra () Integer
-> SpecTransM DijkstraEra () (Maybe Integer -> GovAction)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SafeHash AnchorData
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (SafeHash AnchorData))
     (SpecRep DijkstraEra (SafeHash AnchorData))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep SafeHash AnchorData
h
      SpecTransM DijkstraEra () (Maybe Integer -> GovAction)
-> SpecTransM DijkstraEra () (Maybe Integer)
-> SpecTransM DijkstraEra () GovAction
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 ScriptHash
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (StrictMaybe ScriptHash))
     (SpecRep DijkstraEra (StrictMaybe ScriptHash))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep StrictMaybe ScriptHash
policy
  toSpecRep GovAction DijkstraEra
InfoAction = GovAction -> SpecTransM DijkstraEra () GovAction
forall a. a -> SpecTransM DijkstraEra () a
forall (f :: * -> *) a. Applicative f => a -> f a
pure GovAction
Agda.Info

instance SpecTranslate DijkstraEra (ProposalProcedure DijkstraEra) where
  type SpecRep DijkstraEra (ProposalProcedure DijkstraEra) = Agda.GovProposal

  toSpecRep :: ProposalProcedure DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (ProposalProcedure DijkstraEra))
     (SpecRep DijkstraEra (ProposalProcedure DijkstraEra))
toSpecRep ProposalProcedure {AccountAddress
Anchor
GovAction DijkstraEra
Coin
pProcDeposit :: Coin
pProcReturnAddr :: AccountAddress
pProcGovAction :: GovAction DijkstraEra
pProcAnchor :: Anchor
pProcAnchor :: forall era. ProposalProcedure era -> Anchor
pProcGovAction :: forall era. ProposalProcedure era -> GovAction era
pProcReturnAddr :: forall era. ProposalProcedure era -> AccountAddress
pProcDeposit :: forall era. ProposalProcedure era -> Coin
..} =
    GovAction
-> (Integer, Integer)
-> Maybe Integer
-> Integer
-> RewardAddress
-> Anchor
-> GovProposal
Agda.MkGovProposal
      (GovAction
 -> (Integer, Integer)
 -> Maybe Integer
 -> Integer
 -> RewardAddress
 -> Anchor
 -> GovProposal)
-> SpecTransM DijkstraEra () GovAction
-> SpecTransM
     DijkstraEra
     ()
     ((Integer, Integer)
      -> Maybe Integer
      -> Integer
      -> RewardAddress
      -> Anchor
      -> GovProposal)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GovAction DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (GovAction DijkstraEra))
     (SpecRep DijkstraEra (GovAction DijkstraEra))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep GovAction DijkstraEra
pProcGovAction
      SpecTransM
  DijkstraEra
  ()
  ((Integer, Integer)
   -> Maybe Integer
   -> Integer
   -> RewardAddress
   -> Anchor
   -> GovProposal)
-> SpecTransM DijkstraEra () (Integer, Integer)
-> SpecTransM
     DijkstraEra
     ()
     (Maybe Integer
      -> Integer -> RewardAddress -> Anchor -> GovProposal)
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
<*> GovActionId
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra GovActionId)
     (SpecRep DijkstraEra GovActionId)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep (StrictMaybe GovActionId -> GovAction DijkstraEra -> GovActionId
forall era. StrictMaybe GovActionId -> GovAction era -> GovActionId
nullifyIfNotNeeded StrictMaybe GovActionId
prevActionId GovAction DijkstraEra
pProcGovAction)
      SpecTransM
  DijkstraEra
  ()
  (Maybe Integer
   -> Integer -> RewardAddress -> Anchor -> GovProposal)
-> SpecTransM DijkstraEra () (Maybe Integer)
-> SpecTransM
     DijkstraEra () (Integer -> RewardAddress -> Anchor -> GovProposal)
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 ScriptHash
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (StrictMaybe ScriptHash))
     (SpecRep DijkstraEra (StrictMaybe ScriptHash))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep StrictMaybe ScriptHash
policy
      SpecTransM
  DijkstraEra () (Integer -> RewardAddress -> Anchor -> GovProposal)
-> SpecTransM DijkstraEra () Integer
-> SpecTransM
     DijkstraEra () (RewardAddress -> Anchor -> GovProposal)
forall a b.
SpecTransM DijkstraEra () (a -> b)
-> SpecTransM DijkstraEra () a -> SpecTransM DijkstraEra () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Coin
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra Coin)
     (SpecRep DijkstraEra Coin)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep Coin
pProcDeposit
      SpecTransM DijkstraEra () (RewardAddress -> Anchor -> GovProposal)
-> SpecTransM DijkstraEra () RewardAddress
-> SpecTransM DijkstraEra () (Anchor -> GovProposal)
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
<*> AccountAddress
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra AccountAddress)
     (SpecRep DijkstraEra AccountAddress)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep AccountAddress
pProcReturnAddr
      SpecTransM DijkstraEra () (Anchor -> GovProposal)
-> SpecTransM DijkstraEra () Anchor
-> SpecTransM DijkstraEra () GovProposal
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
<*> Anchor
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra Anchor)
     (SpecRep DijkstraEra Anchor)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep Anchor
pProcAnchor
    where
      prevActionId :: StrictMaybe GovActionId
prevActionId = GovAction DijkstraEra -> StrictMaybe GovActionId
forall era. GovAction era -> StrictMaybe GovActionId
prevGovActionId GovAction DijkstraEra
pProcGovAction
      policy :: StrictMaybe ScriptHash
policy =
        case GovAction DijkstraEra
pProcGovAction of
          TreasuryWithdrawals Map AccountAddress Coin
_ StrictMaybe ScriptHash
sh -> StrictMaybe ScriptHash
sh
          ParameterChange StrictMaybe (GovPurposeId 'PParamUpdatePurpose)
_ PParamsUpdate DijkstraEra
_ StrictMaybe ScriptHash
sh -> StrictMaybe ScriptHash
sh
          GovAction DijkstraEra
_ -> StrictMaybe ScriptHash
forall a. StrictMaybe a
SNothing

prevGovActionId :: GovAction era -> StrictMaybe GovActionId
prevGovActionId :: forall era. GovAction era -> StrictMaybe GovActionId
prevGovActionId GovAction era
action =
  case GovAction era
action of
    ParameterChange StrictMaybe (GovPurposeId 'PParamUpdatePurpose)
x PParamsUpdate era
_ StrictMaybe ScriptHash
_ -> GovPurposeId 'PParamUpdatePurpose -> GovActionId
forall (p :: GovActionPurpose). GovPurposeId p -> GovActionId
unGovPurposeId (GovPurposeId 'PParamUpdatePurpose -> GovActionId)
-> StrictMaybe (GovPurposeId 'PParamUpdatePurpose)
-> StrictMaybe GovActionId
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StrictMaybe (GovPurposeId 'PParamUpdatePurpose)
x
    HardForkInitiation StrictMaybe (GovPurposeId 'HardForkPurpose)
x ProtVer
_ -> GovPurposeId 'HardForkPurpose -> GovActionId
forall (p :: GovActionPurpose). GovPurposeId p -> GovActionId
unGovPurposeId (GovPurposeId 'HardForkPurpose -> GovActionId)
-> StrictMaybe (GovPurposeId 'HardForkPurpose)
-> StrictMaybe GovActionId
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StrictMaybe (GovPurposeId 'HardForkPurpose)
x
    UpdateCommittee StrictMaybe (GovPurposeId 'CommitteePurpose)
x Set (Credential ColdCommitteeRole)
_ Map (Credential ColdCommitteeRole) EpochNo
_ UnitInterval
_ -> GovPurposeId 'CommitteePurpose -> GovActionId
forall (p :: GovActionPurpose). GovPurposeId p -> GovActionId
unGovPurposeId (GovPurposeId 'CommitteePurpose -> GovActionId)
-> StrictMaybe (GovPurposeId 'CommitteePurpose)
-> StrictMaybe GovActionId
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StrictMaybe (GovPurposeId 'CommitteePurpose)
x
    NoConfidence StrictMaybe (GovPurposeId 'CommitteePurpose)
x -> GovPurposeId 'CommitteePurpose -> GovActionId
forall (p :: GovActionPurpose). GovPurposeId p -> GovActionId
unGovPurposeId (GovPurposeId 'CommitteePurpose -> GovActionId)
-> StrictMaybe (GovPurposeId 'CommitteePurpose)
-> StrictMaybe GovActionId
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StrictMaybe (GovPurposeId 'CommitteePurpose)
x
    NewConstitution StrictMaybe (GovPurposeId 'ConstitutionPurpose)
x Constitution era
_ -> GovPurposeId 'ConstitutionPurpose -> GovActionId
forall (p :: GovActionPurpose). GovPurposeId p -> GovActionId
unGovPurposeId (GovPurposeId 'ConstitutionPurpose -> GovActionId)
-> StrictMaybe (GovPurposeId 'ConstitutionPurpose)
-> StrictMaybe GovActionId
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StrictMaybe (GovPurposeId 'ConstitutionPurpose)
x
    GovAction era
_ -> StrictMaybe GovActionId
forall a. StrictMaybe a
SNothing

nullGovActionId :: GovActionId
nullGovActionId :: GovActionId
nullGovActionId = TxId -> GovActionIx -> GovActionId
GovActionId (SafeHash EraIndependentTxBody -> TxId
TxId SafeHash EraIndependentTxBody
forall a. Default a => a
def) (Word16 -> GovActionIx
GovActionIx Word16
0)

nullifyIfNotNeeded :: StrictMaybe GovActionId -> GovAction era -> GovActionId
nullifyIfNotNeeded :: forall era. StrictMaybe GovActionId -> GovAction era -> GovActionId
nullifyIfNotNeeded StrictMaybe GovActionId
SNothing = GovActionId -> GovAction era -> GovActionId
forall a b. a -> b -> a
const GovActionId
nullGovActionId
nullifyIfNotNeeded (SJust GovActionId
gaId) = \case
  TreasuryWithdrawals {} -> GovActionId
nullGovActionId
  GovAction era
InfoAction -> GovActionId
nullGovActionId
  GovAction era
_ -> GovActionId
gaId

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

  toSpecRep :: GovActionState DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (GovActionState DijkstraEra))
     (SpecRep DijkstraEra (GovActionState DijkstraEra))
toSpecRep gas :: GovActionState DijkstraEra
gas@GovActionState {Map (KeyHash StakePool) Vote
Map (Credential DRepRole) Vote
Map (Credential HotCommitteeRole) Vote
ProposalProcedure DijkstraEra
GovActionId
EpochNo
gasId :: GovActionId
gasCommitteeVotes :: Map (Credential HotCommitteeRole) Vote
gasDRepVotes :: Map (Credential DRepRole) Vote
gasStakePoolVotes :: Map (KeyHash StakePool) Vote
gasProposalProcedure :: ProposalProcedure DijkstraEra
gasProposedIn :: EpochNo
gasExpiresAfter :: EpochNo
gasExpiresAfter :: forall era. GovActionState era -> EpochNo
gasProposedIn :: forall era. GovActionState era -> EpochNo
gasProposalProcedure :: forall era. GovActionState era -> ProposalProcedure era
gasStakePoolVotes :: forall era. GovActionState era -> Map (KeyHash StakePool) Vote
gasDRepVotes :: forall era. GovActionState era -> Map (Credential DRepRole) Vote
gasCommitteeVotes :: forall era.
GovActionState era -> Map (Credential HotCommitteeRole) Vote
gasId :: forall era. GovActionState era -> GovActionId
..} = do
    GovVotes
-> RewardAddress
-> Integer
-> GovAction
-> (Integer, Integer)
-> Integer
-> GovActionState
Agda.MkGovActionState
      (GovVotes
 -> RewardAddress
 -> Integer
 -> GovAction
 -> (Integer, Integer)
 -> Integer
 -> GovActionState)
-> SpecTransM DijkstraEra () GovVotes
-> SpecTransM
     DijkstraEra
     ()
     (RewardAddress
      -> Integer
      -> GovAction
      -> (Integer, Integer)
      -> Integer
      -> GovActionState)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ( HSMap Credential Vote
-> HSMap Credential Vote -> HSMap Integer Vote -> GovVotes
Agda.GovVotes
              (HSMap Credential Vote
 -> HSMap Credential Vote -> HSMap Integer Vote -> GovVotes)
-> SpecTransM DijkstraEra () (HSMap Credential Vote)
-> SpecTransM
     DijkstraEra
     ()
     (HSMap Credential Vote -> HSMap Integer Vote -> GovVotes)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map (Credential HotCommitteeRole) Vote
-> SpecTransM
     DijkstraEra
     ()
     (HSMap
        (SpecRep DijkstraEra (Credential HotCommitteeRole))
        (SpecRep DijkstraEra Vote))
forall era k v ctx.
(SpecTranslate era k, SpecTranslate era v, SpecContext era k ~ ctx,
 SpecContext era v ~ ctx) =>
Map k v
-> SpecTransM era ctx (HSMap (SpecRep era k) (SpecRep era v))
toSpecRepMap Map (Credential HotCommitteeRole) Vote
gasCommitteeVotes
              SpecTransM
  DijkstraEra
  ()
  (HSMap Credential Vote -> HSMap Integer Vote -> GovVotes)
-> SpecTransM DijkstraEra () (HSMap Credential Vote)
-> SpecTransM DijkstraEra () (HSMap Integer Vote -> GovVotes)
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
<*> Map (Credential DRepRole) Vote
-> SpecTransM
     DijkstraEra
     ()
     (HSMap
        (SpecRep DijkstraEra (Credential DRepRole))
        (SpecRep DijkstraEra Vote))
forall era k v ctx.
(SpecTranslate era k, SpecTranslate era v, SpecContext era k ~ ctx,
 SpecContext era v ~ ctx) =>
Map k v
-> SpecTransM era ctx (HSMap (SpecRep era k) (SpecRep era v))
toSpecRepMap Map (Credential DRepRole) Vote
gasDRepVotes
              SpecTransM DijkstraEra () (HSMap Integer Vote -> GovVotes)
-> SpecTransM DijkstraEra () (HSMap Integer Vote)
-> SpecTransM DijkstraEra () GovVotes
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
<*> Map (KeyHash StakePool) Vote
-> SpecTransM
     DijkstraEra
     ()
     (HSMap
        (SpecRep DijkstraEra (KeyHash StakePool))
        (SpecRep DijkstraEra Vote))
forall era k v ctx.
(SpecTranslate era k, SpecTranslate era v, SpecContext era k ~ ctx,
 SpecContext era v ~ ctx) =>
Map k v
-> SpecTransM era ctx (HSMap (SpecRep era k) (SpecRep era v))
toSpecRepMap Map (KeyHash StakePool) Vote
gasStakePoolVotes
          )
      SpecTransM
  DijkstraEra
  ()
  (RewardAddress
   -> Integer
   -> GovAction
   -> (Integer, Integer)
   -> Integer
   -> GovActionState)
-> SpecTransM DijkstraEra () RewardAddress
-> SpecTransM
     DijkstraEra
     ()
     (Integer
      -> GovAction -> (Integer, Integer) -> Integer -> GovActionState)
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
<*> AccountAddress
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra AccountAddress)
     (SpecRep DijkstraEra AccountAddress)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep (GovActionState DijkstraEra -> AccountAddress
forall era. GovActionState era -> AccountAddress
gasReturnAddr GovActionState DijkstraEra
gas)
      SpecTransM
  DijkstraEra
  ()
  (Integer
   -> GovAction -> (Integer, Integer) -> Integer -> GovActionState)
-> SpecTransM DijkstraEra () Integer
-> SpecTransM
     DijkstraEra
     ()
     (GovAction -> (Integer, Integer) -> Integer -> GovActionState)
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
<*> EpochNo
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra EpochNo)
     (SpecRep DijkstraEra EpochNo)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep EpochNo
gasExpiresAfter
      SpecTransM
  DijkstraEra
  ()
  (GovAction -> (Integer, Integer) -> Integer -> GovActionState)
-> SpecTransM DijkstraEra () GovAction
-> SpecTransM
     DijkstraEra () ((Integer, Integer) -> Integer -> GovActionState)
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
<*> GovAction DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (GovAction DijkstraEra))
     (SpecRep DijkstraEra (GovAction DijkstraEra))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep GovAction DijkstraEra
action
      SpecTransM
  DijkstraEra () ((Integer, Integer) -> Integer -> GovActionState)
-> SpecTransM DijkstraEra () (Integer, Integer)
-> SpecTransM DijkstraEra () (Integer -> GovActionState)
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
<*> GovActionId
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra GovActionId)
     (SpecRep DijkstraEra GovActionId)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep (StrictMaybe GovActionId -> GovAction DijkstraEra -> GovActionId
forall era. StrictMaybe GovActionId -> GovAction era -> GovActionId
nullifyIfNotNeeded (GovAction DijkstraEra -> StrictMaybe GovActionId
forall era. GovAction era -> StrictMaybe GovActionId
prevGovActionId GovAction DijkstraEra
action) GovAction DijkstraEra
action)
      SpecTransM DijkstraEra () (Integer -> GovActionState)
-> SpecTransM DijkstraEra () Integer
-> SpecTransM DijkstraEra () GovActionState
forall a b.
SpecTransM DijkstraEra () (a -> b)
-> SpecTransM DijkstraEra () a -> SpecTransM DijkstraEra () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Coin
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra Coin)
     (SpecRep DijkstraEra Coin)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep (GovActionState DijkstraEra -> Coin
forall era. GovActionState era -> Coin
gasDeposit GovActionState DijkstraEra
gas)
    where
      action :: GovAction DijkstraEra
action = GovActionState DijkstraEra -> GovAction DijkstraEra
forall era. GovActionState era -> GovAction era
gasAction GovActionState DijkstraEra
gas

instance SpecTranslate DijkstraEra GovActionIx where
  type SpecRep DijkstraEra GovActionIx = Integer

  toSpecRep :: GovActionIx
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra GovActionIx)
     (SpecRep DijkstraEra GovActionIx)
toSpecRep = Integer -> SpecTransM DijkstraEra () Integer
forall a. a -> SpecTransM DijkstraEra () a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> SpecTransM DijkstraEra () Integer)
-> (GovActionIx -> Integer)
-> GovActionIx
-> SpecTransM DijkstraEra () Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word16 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word16 -> Integer)
-> (GovActionIx -> Word16) -> GovActionIx -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GovActionIx -> Word16
unGovActionIx

instance SpecTranslate DijkstraEra GovActionId where
  type SpecRep DijkstraEra GovActionId = Agda.GovActionID

  toSpecRep :: GovActionId
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra GovActionId)
     (SpecRep DijkstraEra GovActionId)
toSpecRep (GovActionId TxId
txId GovActionIx
gaIx) = (TxId, GovActionIx)
-> SpecTransM
     DijkstraEra
     ()
     (SpecRep DijkstraEra TxId, SpecRep DijkstraEra GovActionIx)
forall era a b ctx.
(SpecTranslate era a, SpecTranslate era b, SpecContext era a ~ ctx,
 SpecContext era b ~ ctx) =>
(a, b) -> SpecTransM era ctx (SpecRep era a, SpecRep era b)
toSpecRepTuple (TxId
txId, GovActionIx
gaIx)

instance SpecTranslate DijkstraEra (Proposals DijkstraEra) where
  type SpecRep DijkstraEra (Proposals DijkstraEra) = Agda.GovState

  toSpecRep :: Proposals DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (Proposals DijkstraEra))
     (SpecRep DijkstraEra (Proposals DijkstraEra))
toSpecRep = OMap GovActionId (GovActionState DijkstraEra)
-> SpecTransM DijkstraEra () [((Integer, Integer), GovActionState)]
OMap GovActionId (GovActionState DijkstraEra)
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra GovActionId)
     [(SpecRep DijkstraEra GovActionId,
       SpecRep DijkstraEra (GovActionState DijkstraEra))]
forall era k v ctx.
(Ord k, SpecTranslate era k, SpecTranslate era v,
 SpecContext era k ~ ctx, SpecContext era v ~ ctx) =>
OMap k v -> SpecTransM era ctx [(SpecRep era k, SpecRep era v)]
toSpecRepOMap (OMap GovActionId (GovActionState DijkstraEra)
 -> SpecTransM
      DijkstraEra () [((Integer, Integer), GovActionState)])
-> (Proposals DijkstraEra
    -> OMap GovActionId (GovActionState DijkstraEra))
-> Proposals DijkstraEra
-> SpecTransM DijkstraEra () [((Integer, Integer), GovActionState)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OMap GovActionId (GovActionState DijkstraEra)
-> OMap GovActionId (GovActionState DijkstraEra)
prioritySort (OMap GovActionId (GovActionState DijkstraEra)
 -> OMap GovActionId (GovActionState DijkstraEra))
-> (Proposals DijkstraEra
    -> OMap GovActionId (GovActionState DijkstraEra))
-> Proposals DijkstraEra
-> OMap GovActionId (GovActionState DijkstraEra)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting
  (OMap GovActionId (GovActionState DijkstraEra))
  (Proposals DijkstraEra)
  (OMap GovActionId (GovActionState DijkstraEra))
-> Proposals DijkstraEra
-> OMap GovActionId (GovActionState DijkstraEra)
forall a s. Getting a s a -> s -> a
view Getting
  (OMap GovActionId (GovActionState DijkstraEra))
  (Proposals DijkstraEra)
  (OMap GovActionId (GovActionState DijkstraEra))
forall era (f :: * -> *).
Functor f =>
(OMap GovActionId (GovActionState era)
 -> f (OMap GovActionId (GovActionState era)))
-> Proposals era -> f (Proposals era)
pPropsL
    where
      prioritySort ::
        OMap GovActionId (GovActionState DijkstraEra) ->
        OMap GovActionId (GovActionState DijkstraEra)
      prioritySort :: OMap GovActionId (GovActionState DijkstraEra)
-> OMap GovActionId (GovActionState DijkstraEra)
prioritySort = [Item (OMap GovActionId (GovActionState DijkstraEra))]
-> OMap GovActionId (GovActionState DijkstraEra)
[GovActionState DijkstraEra]
-> OMap GovActionId (GovActionState DijkstraEra)
forall l. IsList l => [Item l] -> l
Exts.fromList ([GovActionState DijkstraEra]
 -> OMap GovActionId (GovActionState DijkstraEra))
-> (OMap GovActionId (GovActionState DijkstraEra)
    -> [GovActionState DijkstraEra])
-> OMap GovActionId (GovActionState DijkstraEra)
-> OMap GovActionId (GovActionState DijkstraEra)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (GovActionState DijkstraEra -> Int)
-> [GovActionState DijkstraEra] -> [GovActionState DijkstraEra]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn (GovAction DijkstraEra -> Int
forall era. GovAction era -> Int
actionPriority (GovAction DijkstraEra -> Int)
-> (GovActionState DijkstraEra -> GovAction DijkstraEra)
-> GovActionState DijkstraEra
-> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GovActionState DijkstraEra -> GovAction DijkstraEra
forall era. GovActionState era -> GovAction era
gasAction) ([GovActionState DijkstraEra] -> [GovActionState DijkstraEra])
-> (OMap GovActionId (GovActionState DijkstraEra)
    -> [GovActionState DijkstraEra])
-> OMap GovActionId (GovActionState DijkstraEra)
-> [GovActionState DijkstraEra]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OMap GovActionId (GovActionState DijkstraEra)
-> [Item (OMap GovActionId (GovActionState DijkstraEra))]
OMap GovActionId (GovActionState DijkstraEra)
-> [GovActionState DijkstraEra]
forall l. IsList l => l -> [Item l]
Exts.toList

instance SpecTranslate DijkstraEra MaryValue where
  type SpecRep DijkstraEra MaryValue = Agda.Coin

  toSpecRep :: MaryValue
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra MaryValue)
     (SpecRep DijkstraEra MaryValue)
toSpecRep = Coin -> SpecTransM DijkstraEra () Integer
Coin
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra Coin)
     (SpecRep DijkstraEra Coin)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep (Coin -> SpecTransM DijkstraEra () Integer)
-> (MaryValue -> Coin)
-> MaryValue
-> SpecTransM DijkstraEra () Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MaryValue -> Coin
forall t. Val t => t -> Coin
coin

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

  type SpecContext DijkstraEra (RatifyState DijkstraEra) = [GovActionState DijkstraEra]
  toSpecRep :: RatifyState DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (RatifyState DijkstraEra))
     (SpecRep DijkstraEra (RatifyState DijkstraEra))
toSpecRep RatifyState {Bool
Set GovActionId
EnactState DijkstraEra
Seq (GovActionState DijkstraEra)
rsEnactState :: EnactState DijkstraEra
rsEnacted :: Seq (GovActionState DijkstraEra)
rsExpired :: Set GovActionId
rsDelayed :: Bool
rsDelayed :: forall era. RatifyState era -> Bool
rsExpired :: forall era. RatifyState era -> Set GovActionId
rsEnacted :: forall era. RatifyState era -> Seq (GovActionState era)
rsEnactState :: forall era. RatifyState era -> EnactState era
..} = do
    govActionMap <-
      (Map GovActionId (GovActionState DijkstraEra)
 -> GovActionState DijkstraEra
 -> Map GovActionId (GovActionState DijkstraEra))
-> Map GovActionId (GovActionState DijkstraEra)
-> [GovActionState DijkstraEra]
-> Map GovActionId (GovActionState DijkstraEra)
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\Map GovActionId (GovActionState DijkstraEra)
acc GovActionState DijkstraEra
gas -> GovActionId
-> GovActionState DijkstraEra
-> Map GovActionId (GovActionState DijkstraEra)
-> Map GovActionId (GovActionState DijkstraEra)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (GovActionState DijkstraEra -> GovActionId
forall era. GovActionState era -> GovActionId
gasId GovActionState DijkstraEra
gas) GovActionState DijkstraEra
gas Map GovActionId (GovActionState DijkstraEra)
acc) Map GovActionId (GovActionState DijkstraEra)
forall a. Monoid a => a
mempty
        ([GovActionState DijkstraEra]
 -> Map GovActionId (GovActionState DijkstraEra))
-> SpecTransM
     DijkstraEra
     [GovActionState DijkstraEra]
     [GovActionState DijkstraEra]
-> SpecTransM
     DijkstraEra
     [GovActionState DijkstraEra]
     (Map GovActionId (GovActionState DijkstraEra))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SpecTransM
  DijkstraEra
  [GovActionState DijkstraEra]
  [GovActionState DijkstraEra]
forall era ctx. SpecTransM era ctx ctx
askSpecTransM
    let
      lookupGAS GovActionId
gaId SpecTransM
  DijkstraEra
  [GovActionState DijkstraEra]
  (Set (GovActionId, GovActionState DijkstraEra))
m = do
        case GovActionId
-> Map GovActionId (GovActionState DijkstraEra)
-> Maybe (GovActionState DijkstraEra)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup GovActionId
gaId Map GovActionId (GovActionState DijkstraEra)
govActionMap of
          Just GovActionState DijkstraEra
x -> (GovActionId, GovActionState DijkstraEra)
-> Set (GovActionId, GovActionState DijkstraEra)
-> Set (GovActionId, GovActionState DijkstraEra)
forall a. Ord a => a -> Set a -> Set a
Set.insert (GovActionId
gaId, GovActionState DijkstraEra
x) (Set (GovActionId, GovActionState DijkstraEra)
 -> Set (GovActionId, GovActionState DijkstraEra))
-> SpecTransM
     DijkstraEra
     [GovActionState DijkstraEra]
     (Set (GovActionId, GovActionState DijkstraEra))
-> SpecTransM
     DijkstraEra
     [GovActionState DijkstraEra]
     (Set (GovActionId, GovActionState DijkstraEra))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SpecTransM
  DijkstraEra
  [GovActionState DijkstraEra]
  (Set (GovActionId, GovActionState DijkstraEra))
m
          Maybe (GovActionState DijkstraEra)
Nothing ->
            Text
-> SpecTransM
     DijkstraEra
     [GovActionState DijkstraEra]
     (Set (GovActionId, GovActionState DijkstraEra))
forall a.
Text -> SpecTransM DijkstraEra [GovActionState DijkstraEra] a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Text
 -> SpecTransM
      DijkstraEra
      [GovActionState DijkstraEra]
      (Set (GovActionId, GovActionState DijkstraEra)))
-> Text
-> SpecTransM
     DijkstraEra
     [GovActionState DijkstraEra]
     (Set (GovActionId, GovActionState DijkstraEra))
forall a b. (a -> b) -> a -> b
$
              Text
"gaId: "
                Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> [Char] -> Text
T.pack (GovActionId -> [Char]
forall a. ToExpr a => a -> [Char]
showExpr GovActionId
gaId)
                Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"\n\ngovActionMap: "
                Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> [Char] -> Text
T.pack (Map GovActionId (GovActionState DijkstraEra) -> [Char]
forall a. ToExpr a => a -> [Char]
showExpr Map GovActionId (GovActionState DijkstraEra)
govActionMap)
                Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"\n\nGovActionId is not contained in the govActionMap"
    removed <-
      Set.foldr'
        lookupGAS
        (pure Set.empty)
        (rsExpired `Set.union` Set.fromList (gasId <$> toList rsEnacted))
    withCtxSpecTransM () $ do
      Agda.MkRatifyState
        <$> toSpecRep rsEnactState
        <*> (Agda.MkHSSet <$> traverse toSpecRepTuple (toList removed))
        <*> toSpecRep rsDelayed

instance SpecTranslate DijkstraEra (RatifySignal DijkstraEra) where
  type
    SpecRep DijkstraEra (RatifySignal DijkstraEra) =
      [(SpecRep DijkstraEra GovActionId, SpecRep DijkstraEra (GovActionState DijkstraEra))]
  toSpecRep :: RatifySignal DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (RatifySignal DijkstraEra))
     (SpecRep DijkstraEra (RatifySignal DijkstraEra))
toSpecRep (RatifySignal StrictSeq (GovActionState DijkstraEra)
x) =
    (GovActionState DijkstraEra
 -> SpecTransM DijkstraEra () ((Integer, Integer), GovActionState))
-> [GovActionState DijkstraEra]
-> SpecTransM DijkstraEra () [((Integer, Integer), GovActionState)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (\gas :: GovActionState DijkstraEra
gas@GovActionState {GovActionId
gasId :: forall era. GovActionState era -> GovActionId
gasId :: GovActionId
gasId} -> (GovActionId, GovActionState DijkstraEra)
-> SpecTransM
     DijkstraEra
     ()
     (SpecRep DijkstraEra GovActionId,
      SpecRep DijkstraEra (GovActionState DijkstraEra))
forall era a b ctx.
(SpecTranslate era a, SpecTranslate era b, SpecContext era a ~ ctx,
 SpecContext era b ~ ctx) =>
(a, b) -> SpecTransM era ctx (SpecRep era a, SpecRep era b)
toSpecRepTuple (GovActionId
gasId, GovActionState DijkstraEra
gas)) (StrictSeq (GovActionState DijkstraEra)
-> [GovActionState DijkstraEra]
forall a. StrictSeq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList StrictSeq (GovActionState DijkstraEra)
x)

instance SpecTranslate DijkstraEra (Conway.EnactSignal DijkstraEra) where
  type
    SpecRep DijkstraEra (Conway.EnactSignal DijkstraEra) =
      SpecRep DijkstraEra (GovAction DijkstraEra)

  toSpecRep :: EnactSignal DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (EnactSignal DijkstraEra))
     (SpecRep DijkstraEra (EnactSignal DijkstraEra))
toSpecRep (Conway.EnactSignal GovActionId
_ GovAction DijkstraEra
ga) = GovAction DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (GovAction DijkstraEra))
     (SpecRep DijkstraEra (GovAction DijkstraEra))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep GovAction DijkstraEra
ga

instance SpecNormalize Agda.NativeScript

instance SpecNormalize Agda.HSNativeScript

instance SpecNormalize Agda.LanguageCostModels where
  specNormalize :: LanguageCostModels -> LanguageCostModels
specNormalize = [(HSLanguage, ())] -> LanguageCostModels
Agda.MkLanguageCostModels ([(HSLanguage, ())] -> LanguageCostModels)
-> (LanguageCostModels -> [(HSLanguage, ())])
-> LanguageCostModels
-> LanguageCostModels
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((HSLanguage, ()) -> HSLanguage)
-> [(HSLanguage, ())] -> [(HSLanguage, ())]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn (HSLanguage, ()) -> HSLanguage
forall a b. (a, b) -> a
fst ([(HSLanguage, ())] -> [(HSLanguage, ())])
-> (LanguageCostModels -> [(HSLanguage, ())])
-> LanguageCostModels
-> [(HSLanguage, ())]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LanguageCostModels -> [(HSLanguage, ())]
Agda.lcmLanguageCostModels

instance SpecNormalize Agda.HSLanguage

instance SpecNormalize Agda.HSPlutusScript

instance SpecNormalize Agda.UTxOState

instance SpecNormalize Agda.GovRole

instance SpecNormalize Agda.GovVotes

instance SpecNormalize Agda.VDeleg

instance SpecNormalize Agda.DState

instance SpecNormalize Agda.StakePoolParams

instance SpecNormalize Agda.PState

instance SpecNormalize Agda.GState

instance SpecNormalize Agda.CertState

instance SpecNormalize Agda.Vote

instance SpecNormalize Agda.PParamsUpdate

instance SpecNormalize Agda.GovAction

instance SpecNormalize Agda.GovActionState

instance SpecNormalize Agda.StakeDistrs

instance SpecNormalize Agda.PoolThresholds

instance SpecNormalize Agda.DrepThresholds

instance SpecNormalize Agda.PParams

instance SpecNormalize Agda.EnactState

instance SpecNormalize Agda.RatifyEnv

instance SpecNormalize Agda.RatifyState

instance SpecNormalize Agda.EpochState

instance SpecNormalize Agda.Snapshots

instance SpecNormalize Agda.Snapshot where
  specNormalize :: Snapshot -> Snapshot
specNormalize (Agda.MkSnapshot HSMap Credential Integer
s HSMap Credential Integer
d HSMap Integer StakePoolParams
p) =
    HSMap Credential Integer
-> HSMap Credential Integer
-> HSMap Integer StakePoolParams
-> Snapshot
Agda.MkSnapshot (HSMap Credential Integer -> HSMap Credential Integer
forall a. SpecNormalize a => a -> a
specNormalize HSMap Credential Integer
s') (HSMap Credential Integer -> HSMap Credential Integer
forall a. SpecNormalize a => a -> a
specNormalize HSMap Credential Integer
d') HSMap Integer StakePoolParams
p
    where
      s' :: HSMap Credential Integer
s' = HSMap Credential Integer -> HSMap Credential Integer
forall {b} {k}. (Eq b, Num b) => HSMap k b -> HSMap k b
removeZero HSMap Credential Integer
s
      -- Only keep delegations for credentials that have non-zero stake,
      -- since ActiveStake drops zero-stake credentials
      d' :: HSMap Credential Integer
d' = HSMap Credential Integer
-> HSMap Credential Integer -> HSMap Credential Integer
forall {b} {b} {v}. Ord b => HSMap b b -> HSMap b v -> HSMap b v
keepOnlyStaked HSMap Credential Integer
s' (HSMap Credential Integer -> HSMap Credential Integer
forall {b} {k}. (Eq b, Num b) => HSMap k b -> HSMap k b
removeZero HSMap Credential Integer
d)
      removeZero :: HSMap k b -> HSMap k b
removeZero (Agda.MkHSMap [(k, b)]
l) = [(k, b)] -> HSMap k b
forall k v. [(k, v)] -> HSMap k v
Agda.MkHSMap ([(k, b)] -> HSMap k b) -> [(k, b)] -> HSMap k b
forall a b. (a -> b) -> a -> b
$ ((k, b) -> Bool) -> [(k, b)] -> [(k, b)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((b -> b -> Bool
forall a. Eq a => a -> a -> Bool
/= b
0) (b -> Bool) -> ((k, b) -> b) -> (k, b) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (k, b) -> b
forall a b. (a, b) -> b
snd) [(k, b)]
l
      keepOnlyStaked :: HSMap b b -> HSMap b v -> HSMap b v
keepOnlyStaked (Agda.MkHSMap [(b, b)]
sl) (Agda.MkHSMap [(b, v)]
dl) =
        let stakeKeys :: Set b
stakeKeys = [b] -> Set b
forall a. Ord a => [a] -> Set a
Set.fromList (((b, b) -> b) -> [(b, b)] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map (b, b) -> b
forall a b. (a, b) -> a
fst [(b, b)]
sl)
         in [(b, v)] -> HSMap b v
forall k v. [(k, v)] -> HSMap k v
Agda.MkHSMap ([(b, v)] -> HSMap b v) -> [(b, v)] -> HSMap b v
forall a b. (a -> b) -> a -> b
$ ((b, v) -> Bool) -> [(b, v)] -> [(b, v)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((b -> Set b -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set b
stakeKeys) (b -> Bool) -> ((b, v) -> b) -> (b, v) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (b, v) -> b
forall a b. (a, b) -> a
fst) [(b, v)]
dl

instance SpecNormalize Agda.Acnt

instance SpecNormalize Agda.LedgerState

instance SpecNormalize Agda.LedgerEnv

instance SpecNormalize Agda.RewardUpdate

instance SpecNormalize Agda.NewEpochState

instance SpecNormalize Agda.BalanceInterval

instance SpecNormalize Agda.Anchor