{-# 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 TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

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

import Cardano.Ledger.Address (accountAddressCredentialL)
import Cardano.Ledger.Allegra.Scripts (
  Timelock,
  pattern RequireTimeExpire,
  pattern RequireTimeStart,
 )
import Cardano.Ledger.Alonzo (AlonzoTxAuxData, MaryValue)
import Cardano.Ledger.Alonzo.PParams (OrdExUnits (OrdExUnits))
import Cardano.Ledger.Alonzo.Scripts (AlonzoPlutusPurpose (..), 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 (ConwayEra)
import Cardano.Ledger.Conway.Core
import Cardano.Ledger.Conway.Governance
import Cardano.Ledger.Conway.PParams (ConwayEraPParams (..), ConwayPParams (..), THKD (..))
import qualified Cardano.Ledger.Conway.Rules as Conway
import Cardano.Ledger.Conway.Scripts (AlonzoScript (..), ConwayPlutusPurpose (..))
import Cardano.Ledger.Conway.State
import Cardano.Ledger.Credential (Credential (..))
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 qualified Cardano.Ledger.Shelley.Rules as Shelley
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.Conway.Foreign.API as Agda
import Test.Cardano.Ledger.Conformance.Orphans.Conway ()
import Test.Cardano.Ledger.Conformance.SpecTranslate.Base
import Test.Cardano.Ledger.Conformance.SpecTranslate.Core (committeeCredentialToStrictMaybe)
import Test.Cardano.Ledger.Conway.TreeDiff (showExpr)

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

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

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

  toSpecRep :: TxIn
-> SpecTransM
     ConwayEra (SpecContext ConwayEra TxIn) (SpecRep ConwayEra TxIn)
toSpecRep (TxIn TxId
txId TxIx
txIx) = (TxId, TxIx)
-> SpecTransM
     ConwayEra () (SpecRep ConwayEra TxId, SpecRep ConwayEra 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 ConwayEra (SafeHash a) where
  type SpecRep ConwayEra (SafeHash a) = Agda.DataHash

  toSpecRep :: SafeHash a
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (SafeHash a))
     (SpecRep ConwayEra (SafeHash a))
toSpecRep = Hash HASH a -> SpecTransM ConwayEra () Integer
Hash HASH a
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (Hash HASH a))
     (SpecRep ConwayEra (Hash HASH a))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep (Hash HASH a -> SpecTransM ConwayEra () Integer)
-> (SafeHash a -> Hash HASH a)
-> SafeHash a
-> SpecTransM ConwayEra () 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 ConwayEra Language where
  type SpecRep ConwayEra Language = Agda.HSLanguage

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

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

  toSpecRep :: CostModels
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra CostModels)
     (SpecRep ConwayEra CostModels)
toSpecRep CostModels
cm =
    -- filter out PlutusV4 language
    let validCostModels :: [(Language, CostModel)]
validCostModels = ((Language, CostModel) -> Bool)
-> [(Language, CostModel)] -> [(Language, CostModel)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Language -> Language -> Bool
forall a. Eq a => a -> a -> Bool
/= Language
PlutusV4) (Language -> Bool)
-> ((Language, CostModel) -> Language)
-> (Language, CostModel)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Language, CostModel) -> Language
forall a b. (a, b) -> a
fst) ([(Language, CostModel)] -> [(Language, CostModel)])
-> [(Language, CostModel)] -> [(Language, CostModel)]
forall a b. (a -> b) -> a -> b
$ Map Language CostModel -> [(Language, CostModel)]
forall k a. Map k a -> [(k, a)]
Map.toList (CostModels -> Map Language CostModel
costModelsValid CostModels
cm)
     in [(HSLanguage, ())] -> LanguageCostModels
Agda.MkLanguageCostModels ([(HSLanguage, ())] -> LanguageCostModels)
-> SpecTransM ConwayEra () [(HSLanguage, ())]
-> SpecTransM ConwayEra () LanguageCostModels
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Language, CostModel) -> SpecTransM ConwayEra () (HSLanguage, ()))
-> [(Language, CostModel)]
-> SpecTransM ConwayEra () [(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 ConwayEra () HSLanguage
-> SpecTransM ConwayEra () (HSLanguage, ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Language
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra Language)
     (SpecRep ConwayEra Language)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep Language
l) [(Language, CostModel)]
validCostModels

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

  toSpecRep :: ExUnits
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra ExUnits)
     (SpecRep ConwayEra ExUnits)
toSpecRep (ExUnits Natural
a Natural
b) = (Integer, Integer) -> SpecTransM ConwayEra () (Integer, Integer)
forall a. a -> SpecTransM ConwayEra () 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 ConwayEra (BinaryData ConwayEra) where
  type SpecRep ConwayEra (BinaryData ConwayEra) = Agda.DataHash

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

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

  toSpecRep :: Datum ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (Datum ConwayEra))
     (SpecRep ConwayEra (Datum ConwayEra))
toSpecRep Datum ConwayEra
NoDatum = Maybe (Either Integer Integer)
-> SpecTransM ConwayEra () (Maybe (Either Integer Integer))
forall a. a -> SpecTransM ConwayEra () a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Either Integer Integer)
forall a. Maybe a
Nothing
  toSpecRep (Datum BinaryData ConwayEra
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 ConwayEra () Integer
-> SpecTransM ConwayEra () (Maybe (Either Integer Integer))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BinaryData ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (BinaryData ConwayEra))
     (SpecRep ConwayEra (BinaryData ConwayEra))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep BinaryData ConwayEra
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 ConwayEra () Integer
-> SpecTransM ConwayEra () (Maybe (Either Integer Integer))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DataHash
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra DataHash)
     (SpecRep ConwayEra DataHash)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep DataHash
h

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

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

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

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

instance SpecTranslate ConwayEra (Timelock ConwayEra) where
  type SpecRep ConwayEra (Timelock ConwayEra) = Agda.HSTimelock

  toSpecRep :: Timelock ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (Timelock ConwayEra))
     (SpecRep ConwayEra (Timelock ConwayEra))
toSpecRep Timelock ConwayEra
tl =
    Timelock -> Integer -> Integer -> HSTimelock
Agda.HSTimelock
      (Timelock -> Integer -> Integer -> HSTimelock)
-> SpecTransM ConwayEra () Timelock
-> SpecTransM ConwayEra () (Integer -> Integer -> HSTimelock)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NativeScript ConwayEra -> SpecTransM ConwayEra () Timelock
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 ...),
 AllegraEraScript era) =>
NativeScript era -> SpecTransM era () Timelock
timelockToSpecRep Timelock ConwayEra
NativeScript ConwayEra
tl
      SpecTransM ConwayEra () (Integer -> Integer -> HSTimelock)
-> SpecTransM ConwayEra () Integer
-> SpecTransM ConwayEra () (Integer -> HSTimelock)
forall a b.
SpecTransM ConwayEra () (a -> b)
-> SpecTransM ConwayEra () a -> SpecTransM ConwayEra () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ScriptHash
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra ScriptHash)
     (SpecRep ConwayEra ScriptHash)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep (Script ConwayEra -> ScriptHash
forall era. EraScript era => Script era -> ScriptHash
hashScript (Script ConwayEra -> ScriptHash) -> Script ConwayEra -> ScriptHash
forall a b. (a -> b) -> a -> b
$ NativeScript ConwayEra -> AlonzoScript ConwayEra
forall era. NativeScript era -> AlonzoScript era
NativeScript Timelock ConwayEra
NativeScript ConwayEra
tl)
      SpecTransM ConwayEra () (Integer -> HSTimelock)
-> SpecTransM ConwayEra () Integer
-> SpecTransM ConwayEra () HSTimelock
forall a b.
SpecTransM ConwayEra () (a -> b)
-> SpecTransM ConwayEra () a -> SpecTransM ConwayEra () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Integer -> SpecTransM ConwayEra () Integer
forall a. a -> SpecTransM ConwayEra () 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
$ Timelock ConwayEra -> Int
forall t. SafeToHash t => t -> Int
originalBytesSize Timelock ConwayEra
tl)
    where
      timelockToSpecRep :: NativeScript era -> SpecTransM era () Timelock
timelockToSpecRep NativeScript era
x =
        case NativeScript era
x of
          RequireSignature KeyHash Witness
kh ->
            Integer -> Timelock
Agda.RequireSig (Integer -> Timelock)
-> SpecTransM era () Integer -> SpecTransM era () Timelock
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 () Timelock)
-> StrictSeq (NativeScript era)
-> SpecTransM era () (StrictSeq Timelock)
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 () Timelock
timelockToSpecRep StrictSeq (NativeScript era)
ss
            pure . Agda.RequireAllOf $ toList tls
          RequireAnyOf StrictSeq (NativeScript era)
ss -> do
            tls <- (NativeScript era -> SpecTransM era () Timelock)
-> StrictSeq (NativeScript era)
-> SpecTransM era () (StrictSeq Timelock)
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 () Timelock
timelockToSpecRep StrictSeq (NativeScript era)
ss
            pure . Agda.RequireAnyOf $ toList tls
          RequireMOf Int
m StrictSeq (NativeScript era)
ss -> do
            tls <- (NativeScript era -> SpecTransM era () Timelock)
-> StrictSeq (NativeScript era)
-> SpecTransM era () (StrictSeq Timelock)
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 () Timelock
timelockToSpecRep StrictSeq (NativeScript era)
ss
            pure . Agda.RequireMOf (toInteger m) $ toList tls
          RequireTimeExpire SlotNo
slot -> Integer -> Timelock
Agda.RequireTimeExpire (Integer -> Timelock)
-> SpecTransM era () Integer -> SpecTransM era () Timelock
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 -> Timelock
Agda.RequireTimeStart (Integer -> Timelock)
-> SpecTransM era () Integer -> SpecTransM era () Timelock
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
          NativeScript era
_ -> [Char] -> SpecTransM era () Timelock
forall a. HasCallStack => [Char] -> a
error [Char]
"Impossible: All NativeScripts should have been accounted for"

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

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

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

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

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

  toSpecRep :: BabbageTxOut ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (BabbageTxOut ConwayEra))
     (SpecRep ConwayEra (BabbageTxOut ConwayEra))
toSpecRep (BabbageTxOut Addr
addr Value ConwayEra
val Datum ConwayEra
datum StrictMaybe (Script ConwayEra)
script) = do
    addr' <- Addr
-> SpecTransM
     ConwayEra (SpecContext ConwayEra Addr) (SpecRep ConwayEra 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 ConwayEra (UTxO ConwayEra) where
  type
    SpecRep ConwayEra (UTxO ConwayEra) =
      Agda.HSMap (SpecRep ConwayEra TxIn) (SpecRep ConwayEra (TxOut ConwayEra))

  toSpecRep :: UTxO ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (UTxO ConwayEra))
     (SpecRep ConwayEra (UTxO ConwayEra))
toSpecRep (UTxO Map TxIn (TxOut ConwayEra)
m) = Map TxIn (BabbageTxOut ConwayEra)
-> SpecTransM
     ConwayEra
     ()
     (HSMap
        (SpecRep ConwayEra TxIn)
        (SpecRep ConwayEra (BabbageTxOut ConwayEra)))
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 ConwayEra)
Map TxIn (BabbageTxOut ConwayEra)
m

deriving instance SpecTranslate ConwayEra OrdExUnits

deriving instance SpecTranslate ConwayEra CoinPerByte

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

  toSpecRep :: THKD r f a
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (THKD r f a))
     (SpecRep ConwayEra (THKD r f a))
toSpecRep = HKD f a
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (HKD f a))
     (SpecRep ConwayEra (HKD f a))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep (HKD f a
 -> SpecTransM
      ConwayEra
      (SpecContext ConwayEra (HKD f a))
      (SpecRep ConwayEra (HKD f a)))
-> (THKD r f a -> HKD f a)
-> THKD r f a
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (HKD f a))
     (SpecRep ConwayEra (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 ConwayEra DRepVotingThresholds where
  type SpecRep ConwayEra DRepVotingThresholds = Agda.DrepThresholds

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

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

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

instance SpecTranslate ConwayEra (ConwayPParams Identity ConwayEra) where
  type SpecRep ConwayEra (ConwayPParams Shelley.Identity ConwayEra) = Agda.PParams

  toSpecRep :: ConwayPParams Identity ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (ConwayPParams Identity ConwayEra))
     (SpecRep ConwayEra (ConwayPParams Identity ConwayEra))
toSpecRep cpp :: ConwayPParams Identity ConwayEra
cpp@ConwayPParams {THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word16
THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity OrdExUnits
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
cppTxFeePerByte :: THKD ('PPGroups 'EconomicGroup 'SecurityGroup) Identity CoinPerByte
cppTxFeeFixed :: THKD
  ('PPGroups 'EconomicGroup 'SecurityGroup)
  Identity
  (CompactForm Coin)
cppMaxBBSize :: THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
cppMaxTxSize :: THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
cppMaxBHSize :: THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word16
cppKeyDeposit :: THKD
  ('PPGroups 'EconomicGroup 'NoStakePoolGroup)
  Identity
  (CompactForm Coin)
cppPoolDeposit :: THKD
  ('PPGroups 'EconomicGroup 'NoStakePoolGroup)
  Identity
  (CompactForm Coin)
cppEMax :: THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
  Identity
  EpochInterval
cppNOpt :: THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) Identity Word16
cppA0 :: THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
  Identity
  NonNegativeInterval
cppRho :: THKD
  ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity UnitInterval
cppTau :: THKD
  ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity UnitInterval
cppProtocolVersion :: HKDNoUpdate Identity ProtVer
cppMinPoolCost :: THKD
  ('PPGroups 'EconomicGroup 'NoStakePoolGroup)
  Identity
  (CompactForm Coin)
cppCoinsPerUTxOByte :: THKD ('PPGroups 'EconomicGroup 'SecurityGroup) Identity CoinPerByte
cppCostModels :: THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) Identity CostModels
cppPrices :: THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity Prices
cppMaxTxExUnits :: THKD
  ('PPGroups 'NetworkGroup 'NoStakePoolGroup) Identity OrdExUnits
cppMaxBlockExUnits :: THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity OrdExUnits
cppMaxValSize :: THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
cppCollateralPercentage :: THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) Identity Word16
cppMaxCollateralInputs :: THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) Identity Word16
cppPoolVotingThresholds :: THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup)
  Identity
  PoolVotingThresholds
cppDRepVotingThresholds :: THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup)
  Identity
  DRepVotingThresholds
cppCommitteeMinSize :: THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity Word16
cppCommitteeMaxTermLength :: THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
cppGovActionLifetime :: THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
cppGovActionDeposit :: THKD
  ('PPGroups 'GovGroup 'SecurityGroup) Identity (CompactForm Coin)
cppDRepDeposit :: THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity (CompactForm Coin)
cppDRepActivity :: THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
cppMinFeeRefScriptCostPerByte :: THKD
  ('PPGroups 'EconomicGroup 'SecurityGroup)
  Identity
  NonNegativeInterval
cppMinFeeRefScriptCostPerByte :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
     ('PPGroups 'EconomicGroup 'SecurityGroup) f NonNegativeInterval
cppDRepActivity :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) f EpochInterval
cppDRepDeposit :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
     ('PPGroups 'GovGroup 'NoStakePoolGroup) f (CompactForm Coin)
cppGovActionDeposit :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'GovGroup 'SecurityGroup) f (CompactForm Coin)
cppGovActionLifetime :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) f EpochInterval
cppCommitteeMaxTermLength :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) f EpochInterval
cppCommitteeMinSize :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) f Word16
cppDRepVotingThresholds :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
     ('PPGroups 'GovGroup 'NoStakePoolGroup) f DRepVotingThresholds
cppPoolVotingThresholds :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
     ('PPGroups 'GovGroup 'NoStakePoolGroup) f PoolVotingThresholds
cppMaxCollateralInputs :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) f Word16
cppCollateralPercentage :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) f Word16
cppMaxValSize :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f Word32
cppMaxBlockExUnits :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f OrdExUnits
cppMaxTxExUnits :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) f OrdExUnits
cppPrices :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f Prices
cppCostModels :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) f CostModels
cppCoinsPerUTxOByte :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'SecurityGroup) f CoinPerByte
cppMinPoolCost :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
     ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f (CompactForm Coin)
cppProtocolVersion :: forall (f :: * -> *) era.
ConwayPParams f era -> HKDNoUpdate f ProtVer
cppTau :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f UnitInterval
cppRho :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f UnitInterval
cppA0 :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
     ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) f NonNegativeInterval
cppNOpt :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) f Word16
cppEMax :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
     ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) f EpochInterval
cppPoolDeposit :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
     ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f (CompactForm Coin)
cppKeyDeposit :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
     ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f (CompactForm Coin)
cppMaxBHSize :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f Word16
cppMaxTxSize :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f Word32
cppMaxBBSize :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f Word32
cppTxFeeFixed :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
     ('PPGroups 'EconomicGroup 'SecurityGroup) f (CompactForm Coin)
cppTxFeePerByte :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'SecurityGroup) f CoinPerByte
..} = do
    ppA <- THKD ('PPGroups 'EconomicGroup 'SecurityGroup) Identity CoinPerByte
-> SpecTransM
     ConwayEra
     (SpecContext
        ConwayEra
        (THKD
           ('PPGroups 'EconomicGroup 'SecurityGroup) Identity CoinPerByte))
     (SpecRep
        ConwayEra
        (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
cppTxFeePerByte
    ppB <- toSpecRep cppTxFeeFixed
    ppA0 <- toSpecRep cppA0
    ppMinFeeRefScriptCoinsPerByte <- toSpecRep cppMinFeeRefScriptCostPerByte
    ppCollateralPercentage <- toSpecRep cppCollateralPercentage
    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
cppMaxBBSize
      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
cppMaxTxSize
      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
cppMaxBHSize
    ppKeyDeposit <- toSpecRep cppKeyDeposit
    ppPoolDeposit <- toSpecRep cppPoolDeposit
    ppEmax <- toSpecRep cppEMax
    ppNopt <- toSpecRep (toInteger $ unTHKD cppNOpt)
    let
      -- We don't really care about `ppPv` in conformance testing, because
      -- the actual protocol version is stored elsewhere starting from Conway
      -- and this is just here for backwards compatibility
      ppPv = (Integer
0, Integer
0)
      ppMinUTxOValue = Integer
0 -- minUTxOValue has been deprecated and is not supported in Conway
    ppCoinsPerUTxOByte <- toSpecRep cppCoinsPerUTxOByte
    ppCostmdlsAssoc <- toSpecRep cppCostModels
    ppPrices <- toSpecRep cppPrices
    let
      pp = PParamsHKD Identity ConwayEra -> PParams ConwayEra
forall era. PParamsHKD Identity era -> PParams era
PParams PParamsHKD Identity ConwayEra
ConwayPParams Identity ConwayEra
cpp
      ppMaxRefScriptSizePerTx = Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger (Word32 -> Integer) -> Word32 -> Integer
forall a b. (a -> b) -> a -> b
$ PParams ConwayEra
pp PParams ConwayEra
-> Getting Word32 (PParams ConwayEra) Word32 -> Word32
forall s a. s -> Getting a s a -> a
^. Getting Word32 (PParams ConwayEra) Word32
forall era.
ConwayEraPParams era =>
SimpleGetter (PParams era) Word32
SimpleGetter (PParams ConwayEra) Word32
ppMaxRefScriptSizePerTxG
      ppMaxRefScriptSizePerBlock = Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger (Word32 -> Integer) -> Word32 -> Integer
forall a b. (a -> b) -> a -> b
$ PParams ConwayEra
pp PParams ConwayEra
-> Getting Word32 (PParams ConwayEra) Word32 -> Word32
forall s a. s -> Getting a s a -> a
^. Getting Word32 (PParams ConwayEra) Word32
forall era.
ConwayEraPParams era =>
SimpleGetter (PParams era) Word32
SimpleGetter (PParams ConwayEra) 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 ConwayEra
pp PParams ConwayEra
-> Getting (NonZero Word32) (PParams ConwayEra) (NonZero Word32)
-> NonZero Word32
forall s a. s -> Getting a s a -> a
^. Getting (NonZero Word32) (PParams ConwayEra) (NonZero Word32)
forall era.
ConwayEraPParams era =>
SimpleGetter (PParams era) (NonZero Word32)
SimpleGetter (PParams ConwayEra) (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 ConwayEra
pp PParams ConwayEra
-> Getting PositiveInterval (PParams ConwayEra) PositiveInterval
-> PositiveInterval
forall s a. s -> Getting a s a -> a
^. Getting PositiveInterval (PParams ConwayEra) PositiveInterval
forall era.
ConwayEraPParams era =>
SimpleGetter (PParams era) PositiveInterval
SimpleGetter (PParams ConwayEra) PositiveInterval
ppRefScriptCostMultiplierG
    ppMaxTxExUnits <- toSpecRep cppMaxTxExUnits
    ppMaxBlockExUnits <- toSpecRep cppMaxBlockExUnits
    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
cppMaxValSize
      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
cppMaxCollateralInputs
    ppPoolThresholds <- toSpecRep cppPoolVotingThresholds
    ppDrepThresholds <- toSpecRep cppDRepVotingThresholds
    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
cppCommitteeMinSize
      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
cppCommitteeMaxTermLength
    ppGovActionLifetime <- toSpecRep cppGovActionLifetime
    ppGovActionDeposit <- toSpecRep cppGovActionDeposit
    ppDrepDeposit <- toSpecRep cppDRepDeposit
    ppDrepActivity <- toSpecRep cppDRepActivity
    ppMonetaryExpansion <- toSpecRep cppRho
    ppTreasuryCut <- toSpecRep cppTau

    pure Agda.MkPParams {..}

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

  toSpecRep :: ValidityInterval
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra ValidityInterval)
     (SpecRep ConwayEra ValidityInterval)
toSpecRep (ValidityInterval StrictMaybe SlotNo
lo StrictMaybe SlotNo
hi) = (StrictMaybe SlotNo, StrictMaybe SlotNo)
-> SpecTransM
     ConwayEra
     ()
     (SpecRep ConwayEra (StrictMaybe SlotNo),
      SpecRep ConwayEra (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 ConwayEra (TxDats ConwayEra) where
  type SpecRep ConwayEra (TxDats ConwayEra) = Agda.HSSet Agda.Datum

  toSpecRep :: TxDats ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (TxDats ConwayEra))
     (SpecRep ConwayEra (TxDats ConwayEra))
toSpecRep = ([Integer] -> HSSet Integer)
-> SpecTransM ConwayEra () [Integer]
-> SpecTransM ConwayEra () (HSSet Integer)
forall a b.
(a -> b) -> SpecTransM ConwayEra () a -> SpecTransM ConwayEra () 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 ConwayEra () [Integer]
 -> SpecTransM ConwayEra () (HSSet Integer))
-> (TxDats ConwayEra -> SpecTransM ConwayEra () [Integer])
-> TxDats ConwayEra
-> SpecTransM ConwayEra () (HSSet Integer)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((DataHash, Data ConwayEra) -> SpecTransM ConwayEra () Integer)
-> [(DataHash, Data ConwayEra)]
-> SpecTransM ConwayEra () [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 ConwayEra -> SpecTransM ConwayEra () Integer
Data ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (Data ConwayEra))
     (SpecRep ConwayEra (Data ConwayEra))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep (Data ConwayEra -> SpecTransM ConwayEra () Integer)
-> ((DataHash, Data ConwayEra) -> Data ConwayEra)
-> (DataHash, Data ConwayEra)
-> SpecTransM ConwayEra () Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DataHash, Data ConwayEra) -> Data ConwayEra
forall a b. (a, b) -> b
snd) ([(DataHash, Data ConwayEra)] -> SpecTransM ConwayEra () [Integer])
-> (TxDats ConwayEra -> [(DataHash, Data ConwayEra)])
-> TxDats ConwayEra
-> SpecTransM ConwayEra () [Integer]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map DataHash (Data ConwayEra) -> [(DataHash, Data ConwayEra)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map DataHash (Data ConwayEra) -> [(DataHash, Data ConwayEra)])
-> (TxDats ConwayEra -> Map DataHash (Data ConwayEra))
-> TxDats ConwayEra
-> [(DataHash, Data ConwayEra)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TxDats ConwayEra -> Map DataHash (Data ConwayEra)
forall era. TxDats era -> Map DataHash (Data era)
unTxDats

instance SpecTranslate ConwayEra (AlonzoPlutusPurpose AsIx ConwayEra) where
  type SpecRep ConwayEra (AlonzoPlutusPurpose AsIx ConwayEra) = Agda.RdmrPtr

  toSpecRep :: AlonzoPlutusPurpose AsIx ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (AlonzoPlutusPurpose AsIx ConwayEra))
     (SpecRep ConwayEra (AlonzoPlutusPurpose AsIx ConwayEra))
toSpecRep = \case
    AlonzoSpending (AsIx Word32
i) -> (Tag, Integer) -> SpecTransM ConwayEra () (Tag, Integer)
forall a. a -> SpecTransM ConwayEra () a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tag
Agda.Spend, Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger Word32
i)
    AlonzoMinting (AsIx Word32
i) -> (Tag, Integer) -> SpecTransM ConwayEra () (Tag, Integer)
forall a. a -> SpecTransM ConwayEra () a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tag
Agda.Mint, Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger Word32
i)
    AlonzoCertifying (AsIx Word32
i) -> (Tag, Integer) -> SpecTransM ConwayEra () (Tag, Integer)
forall a. a -> SpecTransM ConwayEra () a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tag
Agda.Cert, Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger Word32
i)
    AlonzoRewarding (AsIx Word32
i) -> (Tag, Integer) -> SpecTransM ConwayEra () (Tag, Integer)
forall a. a -> SpecTransM ConwayEra () a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tag
Agda.Rewrd, Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger Word32
i)

instance SpecTranslate ConwayEra (ConwayPlutusPurpose AsIx ConwayEra) where
  type SpecRep ConwayEra (ConwayPlutusPurpose AsIx ConwayEra) = Agda.RdmrPtr

  toSpecRep :: ConwayPlutusPurpose AsIx ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (ConwayPlutusPurpose AsIx ConwayEra))
     (SpecRep ConwayEra (ConwayPlutusPurpose AsIx ConwayEra))
toSpecRep = \case
    ConwaySpending (AsIx Word32
i) -> (Tag, Integer) -> SpecTransM ConwayEra () (Tag, Integer)
forall a. a -> SpecTransM ConwayEra () a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tag
Agda.Spend, Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger Word32
i)
    ConwayMinting (AsIx Word32
i) -> (Tag, Integer) -> SpecTransM ConwayEra () (Tag, Integer)
forall a. a -> SpecTransM ConwayEra () a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tag
Agda.Mint, Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger Word32
i)
    ConwayCertifying (AsIx Word32
i) -> (Tag, Integer) -> SpecTransM ConwayEra () (Tag, Integer)
forall a. a -> SpecTransM ConwayEra () a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tag
Agda.Cert, Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger Word32
i)
    ConwayRewarding (AsIx Word32
i) -> (Tag, Integer) -> SpecTransM ConwayEra () (Tag, Integer)
forall a. a -> SpecTransM ConwayEra () a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tag
Agda.Rewrd, Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger Word32
i)
    ConwayVoting (AsIx Word32
i) -> (Tag, Integer) -> SpecTransM ConwayEra () (Tag, Integer)
forall a. a -> SpecTransM ConwayEra () a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tag
Agda.Vote, Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger Word32
i)
    ConwayProposing (AsIx Word32
i) -> (Tag, Integer) -> SpecTransM ConwayEra () (Tag, Integer)
forall a. a -> SpecTransM ConwayEra () a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tag
Agda.Propose, Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger Word32
i)

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

  toSpecRep :: Redeemers ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (Redeemers ConwayEra))
     (SpecRep ConwayEra (Redeemers ConwayEra))
toSpecRep (Redeemers Map (PlutusPurpose AsIx ConwayEra) (Data ConwayEra, ExUnits)
x) =
    ([((Tag, Integer), (Integer, (Integer, Integer)))]
 -> HSMap (Tag, Integer) (Integer, (Integer, Integer)))
-> SpecTransM
     ConwayEra () [((Tag, Integer), (Integer, (Integer, Integer)))]
-> SpecTransM
     ConwayEra () (HSMap (Tag, Integer) (Integer, (Integer, Integer)))
forall a b.
(a -> b) -> SpecTransM ConwayEra () a -> SpecTransM ConwayEra () 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
   ConwayEra () [((Tag, Integer), (Integer, (Integer, Integer)))]
 -> SpecTransM
      ConwayEra
      (SpecContext ConwayEra (Redeemers ConwayEra))
      (SpecRep ConwayEra (Redeemers ConwayEra)))
-> (Map (PlutusPurpose AsIx ConwayEra) (Data ConwayEra, ExUnits)
    -> SpecTransM
         ConwayEra () [((Tag, Integer), (Integer, (Integer, Integer)))])
-> Map (PlutusPurpose AsIx ConwayEra) (Data ConwayEra, ExUnits)
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (Redeemers ConwayEra))
     (SpecRep ConwayEra (Redeemers ConwayEra))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((ConwayPlutusPurpose AsIx ConwayEra, (Data ConwayEra, ExUnits))
 -> SpecTransM
      ConwayEra () ((Tag, Integer), (Integer, (Integer, Integer))))
-> [(ConwayPlutusPurpose AsIx ConwayEra,
     (Data ConwayEra, ExUnits))]
-> SpecTransM
     ConwayEra () [((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 ((ConwayPlutusPurpose AsIx ConwayEra
 -> SpecTransM ConwayEra () (Tag, Integer))
-> ((Data ConwayEra, ExUnits)
    -> SpecTransM ConwayEra () (Integer, (Integer, Integer)))
-> (ConwayPlutusPurpose AsIx ConwayEra, (Data ConwayEra, ExUnits))
-> SpecTransM
     ConwayEra () ((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 ConwayPlutusPurpose AsIx ConwayEra
-> SpecTransM ConwayEra () (Tag, Integer)
ConwayPlutusPurpose AsIx ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (ConwayPlutusPurpose AsIx ConwayEra))
     (SpecRep ConwayEra (ConwayPlutusPurpose AsIx ConwayEra))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep (Data ConwayEra, ExUnits)
-> SpecTransM ConwayEra () (Integer, (Integer, Integer))
(Data ConwayEra, ExUnits)
-> SpecTransM
     ConwayEra
     ()
     (SpecRep ConwayEra (Data ConwayEra), SpecRep ConwayEra 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)
      ([(ConwayPlutusPurpose AsIx ConwayEra, (Data ConwayEra, ExUnits))]
 -> SpecTransM
      ConwayEra () [((Tag, Integer), (Integer, (Integer, Integer)))])
-> (Map
      (ConwayPlutusPurpose AsIx ConwayEra) (Data ConwayEra, ExUnits)
    -> [(ConwayPlutusPurpose AsIx ConwayEra,
         (Data ConwayEra, ExUnits))])
-> Map
     (ConwayPlutusPurpose AsIx ConwayEra) (Data ConwayEra, ExUnits)
-> SpecTransM
     ConwayEra () [((Tag, Integer), (Integer, (Integer, Integer)))]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map (ConwayPlutusPurpose AsIx ConwayEra) (Data ConwayEra, ExUnits)
-> [(ConwayPlutusPurpose AsIx ConwayEra,
     (Data ConwayEra, ExUnits))]
forall k a. Map k a -> [(k, a)]
Map.toList
      (Map (PlutusPurpose AsIx ConwayEra) (Data ConwayEra, ExUnits)
 -> SpecTransM
      ConwayEra
      (SpecContext ConwayEra (Redeemers ConwayEra))
      (SpecRep ConwayEra (Redeemers ConwayEra)))
-> Map (PlutusPurpose AsIx ConwayEra) (Data ConwayEra, ExUnits)
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (Redeemers ConwayEra))
     (SpecRep ConwayEra (Redeemers ConwayEra))
forall a b. (a -> b) -> a -> b
$ Map (PlutusPurpose AsIx ConwayEra) (Data ConwayEra, ExUnits)
x

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

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

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

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

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

  toSpecRep :: StakePoolParams
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra StakePoolParams)
     (SpecRep ConwayEra 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 ConwayEra () (HSSet Integer)
-> SpecTransM
     ConwayEra
     ()
     (Integer -> Rational -> Integer -> Credential -> StakePoolParams)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set (KeyHash Staking)
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (Set (KeyHash Staking)))
     (SpecRep ConwayEra (Set (KeyHash Staking)))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep Set (KeyHash Staking)
sppOwners
      SpecTransM
  ConwayEra
  ()
  (Integer -> Rational -> Integer -> Credential -> StakePoolParams)
-> SpecTransM ConwayEra () Integer
-> SpecTransM
     ConwayEra () (Rational -> Integer -> Credential -> StakePoolParams)
forall a b.
SpecTransM ConwayEra () (a -> b)
-> SpecTransM ConwayEra () a -> SpecTransM ConwayEra () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Coin
-> SpecTransM
     ConwayEra (SpecContext ConwayEra Coin) (SpecRep ConwayEra Coin)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep Coin
sppCost
      SpecTransM
  ConwayEra () (Rational -> Integer -> Credential -> StakePoolParams)
-> SpecTransM ConwayEra () Rational
-> SpecTransM
     ConwayEra () (Integer -> Credential -> StakePoolParams)
forall a b.
SpecTransM ConwayEra () (a -> b)
-> SpecTransM ConwayEra () a -> SpecTransM ConwayEra () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> UnitInterval
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra UnitInterval)
     (SpecRep ConwayEra UnitInterval)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep UnitInterval
sppMargin
      SpecTransM ConwayEra () (Integer -> Credential -> StakePoolParams)
-> SpecTransM ConwayEra () Integer
-> SpecTransM ConwayEra () (Credential -> StakePoolParams)
forall a b.
SpecTransM ConwayEra () (a -> b)
-> SpecTransM ConwayEra () a -> SpecTransM ConwayEra () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Coin
-> SpecTransM
     ConwayEra (SpecContext ConwayEra Coin) (SpecRep ConwayEra Coin)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep Coin
sppPledge
      SpecTransM ConwayEra () (Credential -> StakePoolParams)
-> SpecTransM ConwayEra () Credential
-> SpecTransM ConwayEra () StakePoolParams
forall a b.
SpecTransM ConwayEra () (a -> b)
-> SpecTransM ConwayEra () a -> SpecTransM ConwayEra () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Credential Staking
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (Credential Staking))
     (SpecRep ConwayEra (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 ConwayEra DRep where
  type SpecRep ConwayEra DRep = Agda.VDeleg

  toSpecRep :: DRep
-> SpecTransM
     ConwayEra (SpecContext ConwayEra DRep) (SpecRep ConwayEra DRep)
toSpecRep (DRepCredential Credential DRepRole
c) = Credential -> VDeleg
Agda.VDelegCredential (Credential -> VDeleg)
-> SpecTransM ConwayEra () Credential
-> SpecTransM ConwayEra () VDeleg
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Credential DRepRole
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (Credential DRepRole))
     (SpecRep ConwayEra (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 ConwayEra () VDeleg
forall a. a -> SpecTransM ConwayEra () a
forall (f :: * -> *) a. Applicative f => a -> f a
pure VDeleg
Agda.VDelegAbstain
  toSpecRep DRep
DRepAlwaysNoConfidence = VDeleg -> SpecTransM ConwayEra () VDeleg
forall a. a -> SpecTransM ConwayEra () a
forall (f :: * -> *) a. Applicative f => a -> f a
pure VDeleg
Agda.VDelegNoConfidence

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

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

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

  toSpecRep :: Withdrawals
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra Withdrawals)
     (SpecRep ConwayEra Withdrawals)
toSpecRep (Withdrawals Map AccountAddress Coin
w) = Map AccountAddress Coin
-> SpecTransM
     ConwayEra
     ()
     (HSMap (SpecRep ConwayEra AccountAddress) (SpecRep ConwayEra 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 ConwayEra IsValid where
  type SpecRep ConwayEra IsValid = Bool

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

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

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

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

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

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

  toSpecRep :: Constitution ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (Constitution ConwayEra))
     (SpecRep ConwayEra (Constitution ConwayEra))
toSpecRep (Constitution (Anchor Url
_ SafeHash AnchorData
h) StrictMaybe ScriptHash
policy) = (SafeHash AnchorData, StrictMaybe ScriptHash)
-> SpecTransM
     ConwayEra
     ()
     (SpecRep ConwayEra (SafeHash AnchorData),
      SpecRep ConwayEra (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 ConwayEra (EnactState ConwayEra) where
  type SpecRep ConwayEra (EnactState ConwayEra) = Agda.EnactState

  toSpecRep :: EnactState ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (EnactState ConwayEra))
     (SpecRep ConwayEra (EnactState ConwayEra))
toSpecRep EnactState {Map (Credential Staking) Coin
StrictMaybe (Committee ConwayEra)
PParams ConwayEra
Constitution ConwayEra
GovRelation StrictMaybe
Coin
ensCommittee :: StrictMaybe (Committee ConwayEra)
ensConstitution :: Constitution ConwayEra
ensCurPParams :: PParams ConwayEra
ensPrevPParams :: PParams ConwayEra
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
     ConwayEra
     ()
     (Maybe (HSMap Credential Integer, Rational), (Integer, Integer))
-> SpecTransM
     ConwayEra
     ()
     (((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 ConwayEra)
-> StrictMaybe (GovPurposeId 'CommitteePurpose)
-> SpecTransM
     ConwayEra
     ()
     (SpecRep ConwayEra (StrictMaybe (Committee ConwayEra)),
      (Integer, Integer))
forall a (p :: GovActionPurpose).
(SpecTranslate ConwayEra a, SpecContext ConwayEra a ~ ()) =>
a
-> StrictMaybe (GovPurposeId p)
-> SpecTransM
     ConwayEra () (SpecRep ConwayEra a, (Integer, Integer))
transHashProtected StrictMaybe (Committee ConwayEra)
ensCommittee StrictMaybe (GovPurposeId 'CommitteePurpose)
grCommittee
      SpecTransM
  ConwayEra
  ()
  (((Integer, Maybe Integer), (Integer, Integer))
   -> ((Integer, Integer), (Integer, Integer))
   -> (PParams, (Integer, Integer))
   -> HSMap RewardAddress Integer
   -> EnactState)
-> SpecTransM
     ConwayEra () ((Integer, Maybe Integer), (Integer, Integer))
-> SpecTransM
     ConwayEra
     ()
     (((Integer, Integer), (Integer, Integer))
      -> (PParams, (Integer, Integer))
      -> HSMap RewardAddress Integer
      -> EnactState)
forall a b.
SpecTransM ConwayEra () (a -> b)
-> SpecTransM ConwayEra () a -> SpecTransM ConwayEra () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Constitution ConwayEra
-> StrictMaybe (GovPurposeId 'ConstitutionPurpose)
-> SpecTransM
     ConwayEra
     ()
     (SpecRep ConwayEra (Constitution ConwayEra), (Integer, Integer))
forall a (p :: GovActionPurpose).
(SpecTranslate ConwayEra a, SpecContext ConwayEra a ~ ()) =>
a
-> StrictMaybe (GovPurposeId p)
-> SpecTransM
     ConwayEra () (SpecRep ConwayEra a, (Integer, Integer))
transHashProtected Constitution ConwayEra
ensConstitution StrictMaybe (GovPurposeId 'ConstitutionPurpose)
grConstitution
      SpecTransM
  ConwayEra
  ()
  (((Integer, Integer), (Integer, Integer))
   -> (PParams, (Integer, Integer))
   -> HSMap RewardAddress Integer
   -> EnactState)
-> SpecTransM ConwayEra () ((Integer, Integer), (Integer, Integer))
-> SpecTransM
     ConwayEra
     ()
     ((PParams, (Integer, Integer))
      -> HSMap RewardAddress Integer -> EnactState)
forall a b.
SpecTransM ConwayEra () (a -> b)
-> SpecTransM ConwayEra () a -> SpecTransM ConwayEra () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ProtVer
-> StrictMaybe (GovPurposeId 'HardForkPurpose)
-> SpecTransM
     ConwayEra () (SpecRep ConwayEra ProtVer, (Integer, Integer))
forall a (p :: GovActionPurpose).
(SpecTranslate ConwayEra a, SpecContext ConwayEra a ~ ()) =>
a
-> StrictMaybe (GovPurposeId p)
-> SpecTransM
     ConwayEra () (SpecRep ConwayEra a, (Integer, Integer))
transHashProtected (PParams ConwayEra
ensCurPParams PParams ConwayEra
-> Getting ProtVer (PParams ConwayEra) ProtVer -> ProtVer
forall s a. s -> Getting a s a -> a
^. Getting ProtVer (PParams ConwayEra) ProtVer
forall era. EraPParams era => Lens' (PParams era) ProtVer
Lens' (PParams ConwayEra) ProtVer
ppProtocolVersionL) StrictMaybe (GovPurposeId 'HardForkPurpose)
grHardFork
      SpecTransM
  ConwayEra
  ()
  ((PParams, (Integer, Integer))
   -> HSMap RewardAddress Integer -> EnactState)
-> SpecTransM ConwayEra () (PParams, (Integer, Integer))
-> SpecTransM
     ConwayEra () (HSMap RewardAddress Integer -> EnactState)
forall a b.
SpecTransM ConwayEra () (a -> b)
-> SpecTransM ConwayEra () a -> SpecTransM ConwayEra () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> PParams ConwayEra
-> StrictMaybe (GovPurposeId 'PParamUpdatePurpose)
-> SpecTransM
     ConwayEra
     ()
     (SpecRep ConwayEra (PParams ConwayEra), (Integer, Integer))
forall a (p :: GovActionPurpose).
(SpecTranslate ConwayEra a, SpecContext ConwayEra a ~ ()) =>
a
-> StrictMaybe (GovPurposeId p)
-> SpecTransM
     ConwayEra () (SpecRep ConwayEra a, (Integer, Integer))
transHashProtected PParams ConwayEra
ensCurPParams StrictMaybe (GovPurposeId 'PParamUpdatePurpose)
grPParamUpdate
      SpecTransM ConwayEra () (HSMap RewardAddress Integer -> EnactState)
-> SpecTransM ConwayEra () (HSMap RewardAddress Integer)
-> SpecTransM ConwayEra () EnactState
forall a b.
SpecTransM ConwayEra () (a -> b)
-> SpecTransM ConwayEra () a -> SpecTransM ConwayEra () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Map (Credential Staking) Coin
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (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 -- TODO where should this really come from?
          pure (Agda.RewardAddress network agdaCred, amount)
      transHashProtected ::
        (SpecTranslate ConwayEra a, SpecContext ConwayEra a ~ ()) =>
        a ->
        StrictMaybe (GovPurposeId p) ->
        SpecTransM ConwayEra () (SpecRep ConwayEra a, (Integer, Integer))
      transHashProtected :: forall a (p :: GovActionPurpose).
(SpecTranslate ConwayEra a, SpecContext ConwayEra a ~ ()) =>
a
-> StrictMaybe (GovPurposeId p)
-> SpecTransM
     ConwayEra () (SpecRep ConwayEra a, (Integer, Integer))
transHashProtected a
x StrictMaybe (GovPurposeId p)
h = do
        committee <- a
-> SpecTransM
     ConwayEra (SpecContext ConwayEra a) (SpecRep ConwayEra 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
     ConwayEra
     (SpecContext ConwayEra (GovPurposeId p))
     (SpecRep ConwayEra (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 ConwayEra () (Integer, Integer)
forall a. a -> SpecTransM ConwayEra () a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer
0, Integer
0)
        pure (committee, agdaLastId)

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

  toSpecRep :: Voter
-> SpecTransM
     ConwayEra (SpecContext ConwayEra Voter) (SpecRep ConwayEra Voter)
toSpecRep (CommitteeVoter Credential HotCommitteeRole
c) = (GovRole
Agda.CC,) (Credential -> (GovRole, Credential))
-> SpecTransM ConwayEra () Credential
-> SpecTransM ConwayEra () (GovRole, Credential)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Credential HotCommitteeRole
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (Credential HotCommitteeRole))
     (SpecRep ConwayEra (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 ConwayEra () Credential
-> SpecTransM ConwayEra () (GovRole, Credential)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Credential DRepRole
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (Credential DRepRole))
     (SpecRep ConwayEra (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 ConwayEra () Credential
-> SpecTransM ConwayEra () (GovRole, Credential)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Credential StakePool
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (Credential StakePool))
     (SpecRep ConwayEra (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 ConwayEra Vote where
  type SpecRep ConwayEra Vote = Agda.Vote

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

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

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

instance SpecTranslate ConwayEra (ConwayPParams StrictMaybe ConwayEra) where
  type SpecRep ConwayEra (ConwayPParams StrictMaybe ConwayEra) = Agda.PParamsUpdate

  toSpecRep :: ConwayPParams StrictMaybe ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (ConwayPParams StrictMaybe ConwayEra))
     (SpecRep ConwayEra (ConwayPParams StrictMaybe ConwayEra))
toSpecRep (ConwayPParams {THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word16
THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
THKD
  ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe OrdExUnits
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
cppMinFeeRefScriptCostPerByte :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
     ('PPGroups 'EconomicGroup 'SecurityGroup) f NonNegativeInterval
cppDRepActivity :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) f EpochInterval
cppDRepDeposit :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
     ('PPGroups 'GovGroup 'NoStakePoolGroup) f (CompactForm Coin)
cppGovActionDeposit :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'GovGroup 'SecurityGroup) f (CompactForm Coin)
cppGovActionLifetime :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) f EpochInterval
cppCommitteeMaxTermLength :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) f EpochInterval
cppCommitteeMinSize :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) f Word16
cppDRepVotingThresholds :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
     ('PPGroups 'GovGroup 'NoStakePoolGroup) f DRepVotingThresholds
cppPoolVotingThresholds :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
     ('PPGroups 'GovGroup 'NoStakePoolGroup) f PoolVotingThresholds
cppMaxCollateralInputs :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) f Word16
cppCollateralPercentage :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) f Word16
cppMaxValSize :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f Word32
cppMaxBlockExUnits :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f OrdExUnits
cppMaxTxExUnits :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) f OrdExUnits
cppPrices :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f Prices
cppCostModels :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) f CostModels
cppCoinsPerUTxOByte :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'SecurityGroup) f CoinPerByte
cppMinPoolCost :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
     ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f (CompactForm Coin)
cppProtocolVersion :: forall (f :: * -> *) era.
ConwayPParams f era -> HKDNoUpdate f ProtVer
cppTau :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f UnitInterval
cppRho :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f UnitInterval
cppA0 :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
     ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) f NonNegativeInterval
cppNOpt :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) f Word16
cppEMax :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
     ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) f EpochInterval
cppPoolDeposit :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
     ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f (CompactForm Coin)
cppKeyDeposit :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
     ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f (CompactForm Coin)
cppMaxBHSize :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f Word16
cppMaxTxSize :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f Word32
cppMaxBBSize :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f Word32
cppTxFeeFixed :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
     ('PPGroups 'EconomicGroup 'SecurityGroup) f (CompactForm Coin)
cppTxFeePerByte :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'SecurityGroup) f CoinPerByte
cppTxFeePerByte :: THKD
  ('PPGroups 'EconomicGroup 'SecurityGroup) StrictMaybe CoinPerByte
cppTxFeeFixed :: THKD
  ('PPGroups 'EconomicGroup 'SecurityGroup)
  StrictMaybe
  (CompactForm Coin)
cppMaxBBSize :: THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
cppMaxTxSize :: THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
cppMaxBHSize :: THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word16
cppKeyDeposit :: THKD
  ('PPGroups 'EconomicGroup 'NoStakePoolGroup)
  StrictMaybe
  (CompactForm Coin)
cppPoolDeposit :: THKD
  ('PPGroups 'EconomicGroup 'NoStakePoolGroup)
  StrictMaybe
  (CompactForm Coin)
cppEMax :: THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
  StrictMaybe
  EpochInterval
cppNOpt :: THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) StrictMaybe Word16
cppA0 :: THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
  StrictMaybe
  NonNegativeInterval
cppRho :: THKD
  ('PPGroups 'EconomicGroup 'NoStakePoolGroup)
  StrictMaybe
  UnitInterval
cppTau :: THKD
  ('PPGroups 'EconomicGroup 'NoStakePoolGroup)
  StrictMaybe
  UnitInterval
cppProtocolVersion :: HKDNoUpdate StrictMaybe ProtVer
cppMinPoolCost :: THKD
  ('PPGroups 'EconomicGroup 'NoStakePoolGroup)
  StrictMaybe
  (CompactForm Coin)
cppCoinsPerUTxOByte :: THKD
  ('PPGroups 'EconomicGroup 'SecurityGroup) StrictMaybe CoinPerByte
cppCostModels :: THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
  StrictMaybe
  CostModels
cppPrices :: THKD
  ('PPGroups 'EconomicGroup 'NoStakePoolGroup) StrictMaybe Prices
cppMaxTxExUnits :: THKD
  ('PPGroups 'NetworkGroup 'NoStakePoolGroup) StrictMaybe OrdExUnits
cppMaxBlockExUnits :: THKD
  ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe OrdExUnits
cppMaxValSize :: THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
cppCollateralPercentage :: THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) StrictMaybe Word16
cppMaxCollateralInputs :: THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) StrictMaybe Word16
cppPoolVotingThresholds :: THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup)
  StrictMaybe
  PoolVotingThresholds
cppDRepVotingThresholds :: THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup)
  StrictMaybe
  DRepVotingThresholds
cppCommitteeMinSize :: THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) StrictMaybe Word16
cppCommitteeMaxTermLength :: THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup) StrictMaybe EpochInterval
cppGovActionLifetime :: THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup) StrictMaybe EpochInterval
cppGovActionDeposit :: THKD
  ('PPGroups 'GovGroup 'SecurityGroup) StrictMaybe (CompactForm Coin)
cppDRepDeposit :: THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup)
  StrictMaybe
  (CompactForm Coin)
cppDRepActivity :: THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup) StrictMaybe EpochInterval
cppMinFeeRefScriptCostPerByte :: THKD
  ('PPGroups 'EconomicGroup 'SecurityGroup)
  StrictMaybe
  NonNegativeInterval
..}) = do
    ppuA <- THKD
  ('PPGroups 'EconomicGroup 'SecurityGroup) StrictMaybe CoinPerByte
-> SpecTransM
     ConwayEra
     (SpecContext
        ConwayEra
        (THKD
           ('PPGroups 'EconomicGroup 'SecurityGroup) StrictMaybe CoinPerByte))
     (SpecRep
        ConwayEra
        (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
cppTxFeePerByte
    ppuB <- toSpecRep cppTxFeeFixed
    ppuA0 <- toSpecRep cppA0
    ppuMinFeeRefScriptCoinsPerByte <- toSpecRep cppMinFeeRefScriptCostPerByte
    ppuCollateralPercentage <- toSpecRep cppCollateralPercentage
    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
cppMaxBBSize
      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
cppMaxTxSize
      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
cppMaxBHSize
    ppuKeyDeposit <- toSpecRep cppKeyDeposit
    ppuPoolDeposit <- toSpecRep cppPoolDeposit
    ppuEmax <- toSpecRep cppEMax
    ppuNopt <- toSpecRep (fmap toInteger . strictMaybeToMaybe $ unTHKD cppNOpt)
    let
      ppuPv = Maybe a
forall a. Maybe a
Nothing
      ppuMinUTxOValue = Maybe a
forall a. Maybe a
Nothing -- minUTxOValue has been deprecated and is not supported in Conway
    ppuCoinsPerUTxOByte <- toSpecRep cppCoinsPerUTxOByte
    ppuCostmdls <- toSpecRep cppCostModels
    ppuPrices <- toSpecRep cppPrices
    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 cppMaxTxExUnits
    ppuMaxBlockExUnits <- toSpecRep cppMaxBlockExUnits
    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
cppMaxValSize
      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
cppMaxCollateralInputs
    ppuPoolThresholds <- toSpecRep cppPoolVotingThresholds
    ppuDrepThresholds <- toSpecRep cppDRepVotingThresholds
    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
cppCommitteeMinSize
      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
cppCommitteeMaxTermLength
    ppuGovActionLifetime <- toSpecRep cppGovActionLifetime
    ppuGovActionDeposit <- toSpecRep cppGovActionDeposit
    ppuDrepDeposit <- toSpecRep cppDRepDeposit
    ppuDrepActivity <- toSpecRep cppDRepActivity
    ppuMonetaryExpansion <- toSpecRep cppRho
    ppuTreasuryCut <- toSpecRep cppTau

    pure Agda.MkPParamsUpdate {..}

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

  toSpecRep :: GovAction ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (GovAction ConwayEra))
     (SpecRep ConwayEra (GovAction ConwayEra))
toSpecRep (ParameterChange StrictMaybe (GovPurposeId 'PParamUpdatePurpose)
_ PParamsUpdate ConwayEra
ppu StrictMaybe ScriptHash
_) = PParamsUpdate -> GovAction
Agda.ChangePParams (PParamsUpdate -> GovAction)
-> SpecTransM ConwayEra () PParamsUpdate
-> SpecTransM ConwayEra () GovAction
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PParamsUpdate ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (PParamsUpdate ConwayEra))
     (SpecRep ConwayEra (PParamsUpdate ConwayEra))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep PParamsUpdate ConwayEra
ppu
  toSpecRep (HardForkInitiation StrictMaybe (GovPurposeId 'HardForkPurpose)
_ ProtVer
pv) = (Integer, Integer) -> GovAction
Agda.TriggerHardFork ((Integer, Integer) -> GovAction)
-> SpecTransM ConwayEra () (Integer, Integer)
-> SpecTransM ConwayEra () GovAction
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ProtVer
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra ProtVer)
     (SpecRep ConwayEra 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 ConwayEra () (HSMap RewardAddress Integer)
-> SpecTransM ConwayEra () GovAction
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map AccountAddress Coin
-> SpecTransM
     ConwayEra
     ()
     (HSMap (SpecRep ConwayEra AccountAddress) (SpecRep ConwayEra 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 ConwayEra () GovAction
forall a. a -> SpecTransM ConwayEra () 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 ConwayEra () (HSMap Credential Integer)
-> SpecTransM
     ConwayEra () (HSSet Credential -> Rational -> GovAction)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map (Credential ColdCommitteeRole) EpochNo
-> SpecTransM
     ConwayEra
     ()
     (HSMap
        (SpecRep ConwayEra (Credential ColdCommitteeRole))
        (SpecRep ConwayEra 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 ConwayEra () (HSSet Credential -> Rational -> GovAction)
-> SpecTransM ConwayEra () (HSSet Credential)
-> SpecTransM ConwayEra () (Rational -> GovAction)
forall a b.
SpecTransM ConwayEra () (a -> b)
-> SpecTransM ConwayEra () a -> SpecTransM ConwayEra () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Set (Credential ColdCommitteeRole)
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (Set (Credential ColdCommitteeRole)))
     (SpecRep ConwayEra (Set (Credential ColdCommitteeRole)))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep Set (Credential ColdCommitteeRole)
remove
      SpecTransM ConwayEra () (Rational -> GovAction)
-> SpecTransM ConwayEra () Rational
-> SpecTransM ConwayEra () GovAction
forall a b.
SpecTransM ConwayEra () (a -> b)
-> SpecTransM ConwayEra () a -> SpecTransM ConwayEra () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> UnitInterval
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra UnitInterval)
     (SpecRep ConwayEra 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 ConwayEra () Integer
-> SpecTransM ConwayEra () (Maybe Integer -> GovAction)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SafeHash AnchorData
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (SafeHash AnchorData))
     (SpecRep ConwayEra (SafeHash AnchorData))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep SafeHash AnchorData
h
      SpecTransM ConwayEra () (Maybe Integer -> GovAction)
-> SpecTransM ConwayEra () (Maybe Integer)
-> SpecTransM ConwayEra () GovAction
forall a b.
SpecTransM ConwayEra () (a -> b)
-> SpecTransM ConwayEra () a -> SpecTransM ConwayEra () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StrictMaybe ScriptHash
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (StrictMaybe ScriptHash))
     (SpecRep ConwayEra (StrictMaybe ScriptHash))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep StrictMaybe ScriptHash
policy
  toSpecRep GovAction ConwayEra
InfoAction = GovAction -> SpecTransM ConwayEra () GovAction
forall a. a -> SpecTransM ConwayEra () a
forall (f :: * -> *) a. Applicative f => a -> f a
pure GovAction
Agda.Info

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

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

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

instance SpecTranslate ConwayEra GovActionIx where
  type SpecRep ConwayEra GovActionIx = Integer

  toSpecRep :: GovActionIx
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra GovActionIx)
     (SpecRep ConwayEra GovActionIx)
toSpecRep = Integer -> SpecTransM ConwayEra () Integer
forall a. a -> SpecTransM ConwayEra () a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> SpecTransM ConwayEra () Integer)
-> (GovActionIx -> Integer)
-> GovActionIx
-> SpecTransM ConwayEra () 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 ConwayEra GovActionId where
  type SpecRep ConwayEra GovActionId = Agda.GovActionID

  toSpecRep :: GovActionId
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra GovActionId)
     (SpecRep ConwayEra GovActionId)
toSpecRep (GovActionId TxId
txId GovActionIx
gaIx) = (TxId, GovActionIx)
-> SpecTransM
     ConwayEra
     ()
     (SpecRep ConwayEra TxId, SpecRep ConwayEra 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 ConwayEra (Proposals ConwayEra) where
  type SpecRep ConwayEra (Proposals ConwayEra) = Agda.GovState

  -- TODO get rid of `prioritySort` once we've changed the implementation so
  -- that the proposals are always sorted
  toSpecRep :: Proposals ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (Proposals ConwayEra))
     (SpecRep ConwayEra (Proposals ConwayEra))
toSpecRep = OMap GovActionId (GovActionState ConwayEra)
-> SpecTransM ConwayEra () [((Integer, Integer), GovActionState)]
OMap GovActionId (GovActionState ConwayEra)
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra GovActionId)
     [(SpecRep ConwayEra GovActionId,
       SpecRep ConwayEra (GovActionState ConwayEra))]
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 ConwayEra)
 -> SpecTransM ConwayEra () [((Integer, Integer), GovActionState)])
-> (Proposals ConwayEra
    -> OMap GovActionId (GovActionState ConwayEra))
-> Proposals ConwayEra
-> SpecTransM ConwayEra () [((Integer, Integer), GovActionState)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OMap GovActionId (GovActionState ConwayEra)
-> OMap GovActionId (GovActionState ConwayEra)
prioritySort (OMap GovActionId (GovActionState ConwayEra)
 -> OMap GovActionId (GovActionState ConwayEra))
-> (Proposals ConwayEra
    -> OMap GovActionId (GovActionState ConwayEra))
-> Proposals ConwayEra
-> OMap GovActionId (GovActionState ConwayEra)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting
  (OMap GovActionId (GovActionState ConwayEra))
  (Proposals ConwayEra)
  (OMap GovActionId (GovActionState ConwayEra))
-> Proposals ConwayEra
-> OMap GovActionId (GovActionState ConwayEra)
forall a s. Getting a s a -> s -> a
view Getting
  (OMap GovActionId (GovActionState ConwayEra))
  (Proposals ConwayEra)
  (OMap GovActionId (GovActionState ConwayEra))
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 ConwayEra) ->
        OMap GovActionId (GovActionState ConwayEra)
      prioritySort :: OMap GovActionId (GovActionState ConwayEra)
-> OMap GovActionId (GovActionState ConwayEra)
prioritySort = [Item (OMap GovActionId (GovActionState ConwayEra))]
-> OMap GovActionId (GovActionState ConwayEra)
[GovActionState ConwayEra]
-> OMap GovActionId (GovActionState ConwayEra)
forall l. IsList l => [Item l] -> l
Exts.fromList ([GovActionState ConwayEra]
 -> OMap GovActionId (GovActionState ConwayEra))
-> (OMap GovActionId (GovActionState ConwayEra)
    -> [GovActionState ConwayEra])
-> OMap GovActionId (GovActionState ConwayEra)
-> OMap GovActionId (GovActionState ConwayEra)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (GovActionState ConwayEra -> Int)
-> [GovActionState ConwayEra] -> [GovActionState ConwayEra]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn (GovAction ConwayEra -> Int
forall era. GovAction era -> Int
actionPriority (GovAction ConwayEra -> Int)
-> (GovActionState ConwayEra -> GovAction ConwayEra)
-> GovActionState ConwayEra
-> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GovActionState ConwayEra -> GovAction ConwayEra
forall era. GovActionState era -> GovAction era
gasAction) ([GovActionState ConwayEra] -> [GovActionState ConwayEra])
-> (OMap GovActionId (GovActionState ConwayEra)
    -> [GovActionState ConwayEra])
-> OMap GovActionId (GovActionState ConwayEra)
-> [GovActionState ConwayEra]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OMap GovActionId (GovActionState ConwayEra)
-> [Item (OMap GovActionId (GovActionState ConwayEra))]
OMap GovActionId (GovActionState ConwayEra)
-> [GovActionState ConwayEra]
forall l. IsList l => l -> [Item l]
Exts.toList

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

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

instance SpecTranslate ConwayEra (RatifyEnv ConwayEra) where
  type SpecRep ConwayEra (RatifyEnv ConwayEra) = Agda.RatifyEnv
  type SpecContext ConwayEra (RatifyEnv ConwayEra) = Coin

  toSpecRep :: RatifyEnv ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (RatifyEnv ConwayEra))
     (SpecRep ConwayEra (RatifyEnv ConwayEra))
toSpecRep RatifyEnv {Map (KeyHash StakePool) StakePoolState
Map DRep (CompactForm Coin)
Map (Credential DRepRole) DRepState
Accounts ConwayEra
CommitteeState ConwayEra
PoolDistr
InstantStake ConwayEra
EpochNo
reInstantStake :: InstantStake ConwayEra
reStakePoolDistr :: PoolDistr
reDRepDistr :: Map DRep (CompactForm Coin)
reDRepState :: Map (Credential DRepRole) DRepState
reCurrentEpoch :: EpochNo
reCommitteeState :: CommitteeState ConwayEra
reAccounts :: Accounts ConwayEra
reStakePools :: Map (KeyHash StakePool) StakePoolState
reStakePools :: forall era. RatifyEnv era -> Map (KeyHash StakePool) StakePoolState
reAccounts :: forall era. RatifyEnv era -> Accounts era
reCommitteeState :: forall era. RatifyEnv era -> CommitteeState era
reCurrentEpoch :: forall era. RatifyEnv era -> EpochNo
reDRepState :: forall era. RatifyEnv era -> Map (Credential DRepRole) DRepState
reDRepDistr :: forall era. RatifyEnv era -> Map DRep (CompactForm Coin)
reStakePoolDistr :: forall era. RatifyEnv era -> PoolDistr
reInstantStake :: forall era. RatifyEnv era -> InstantStake era
..} = do
    let
      stakeDistrs :: SpecTransM ConwayEra () StakeDistrs
stakeDistrs =
        HSMap VDeleg Integer -> HSMap Integer Integer -> StakeDistrs
Agda.StakeDistrs
          (HSMap VDeleg Integer -> HSMap Integer Integer -> StakeDistrs)
-> SpecTransM ConwayEra () (HSMap VDeleg Integer)
-> SpecTransM ConwayEra () (HSMap Integer Integer -> StakeDistrs)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map DRep (CompactForm Coin)
-> SpecTransM
     ConwayEra
     ()
     (HSMap
        (SpecRep ConwayEra DRep) (SpecRep ConwayEra (CompactForm 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 DRep (CompactForm Coin)
reDRepDistr
          SpecTransM ConwayEra () (HSMap Integer Integer -> StakeDistrs)
-> SpecTransM ConwayEra () (HSMap Integer Integer)
-> SpecTransM ConwayEra () StakeDistrs
forall a b.
SpecTransM ConwayEra () (a -> b)
-> SpecTransM ConwayEra () a -> SpecTransM ConwayEra () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> PoolDistr
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra PoolDistr)
     (SpecRep ConwayEra PoolDistr)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep PoolDistr
reStakePoolDistr
      dreps :: SpecTransM
  ConwayEra
  ()
  (HSMap
     (SpecRep ConwayEra (Credential DRepRole))
     (SpecRep ConwayEra EpochNo))
dreps = Map (Credential DRepRole) EpochNo
-> SpecTransM
     ConwayEra
     ()
     (HSMap
        (SpecRep ConwayEra (Credential DRepRole))
        (SpecRep ConwayEra 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 DRepRole) EpochNo
 -> SpecTransM
      ConwayEra
      ()
      (HSMap
         (SpecRep ConwayEra (Credential DRepRole))
         (SpecRep ConwayEra EpochNo)))
-> Map (Credential DRepRole) EpochNo
-> SpecTransM
     ConwayEra
     ()
     (HSMap
        (SpecRep ConwayEra (Credential DRepRole))
        (SpecRep ConwayEra EpochNo))
forall a b. (a -> b) -> a -> b
$ (DRepState -> EpochNo)
-> Map (Credential DRepRole) DRepState
-> Map (Credential DRepRole) EpochNo
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map DRepState -> EpochNo
drepExpiry Map (Credential DRepRole) DRepState
reDRepState
    treasury <- SpecTransM ConwayEra Coin Coin
forall era ctx. SpecTransM era ctx ctx
askSpecTransM
    withCtxSpecTransM () $ do
      Agda.MkRatifyEnv
        <$> stakeDistrs
        <*> toSpecRep reCurrentEpoch
        <*> dreps
        <*> toSpecRep reCommitteeState
        <*> toSpecRep treasury
        <*> toSpecRepMap (Map.mapWithKey (stakePoolStateToStakePoolParams Testnet) reStakePools)
        <*> toSpecRepMap (Map.mapMaybe (view dRepDelegationAccountStateL) (reAccounts ^. accountsMapL))

instance SpecTranslate ConwayEra (RatifyState ConwayEra) where
  type SpecRep ConwayEra (RatifyState ConwayEra) = Agda.RatifyState
  type SpecContext ConwayEra (RatifyState ConwayEra) = [GovActionState ConwayEra]

  toSpecRep :: RatifyState ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (RatifyState ConwayEra))
     (SpecRep ConwayEra (RatifyState ConwayEra))
toSpecRep RatifyState {Bool
Set GovActionId
EnactState ConwayEra
Seq (GovActionState ConwayEra)
rsEnactState :: EnactState ConwayEra
rsEnacted :: Seq (GovActionState ConwayEra)
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 ConwayEra)
 -> GovActionState ConwayEra
 -> Map GovActionId (GovActionState ConwayEra))
-> Map GovActionId (GovActionState ConwayEra)
-> [GovActionState ConwayEra]
-> Map GovActionId (GovActionState ConwayEra)
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 ConwayEra)
acc GovActionState ConwayEra
gas -> GovActionId
-> GovActionState ConwayEra
-> Map GovActionId (GovActionState ConwayEra)
-> Map GovActionId (GovActionState ConwayEra)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (GovActionState ConwayEra -> GovActionId
forall era. GovActionState era -> GovActionId
gasId GovActionState ConwayEra
gas) GovActionState ConwayEra
gas Map GovActionId (GovActionState ConwayEra)
acc) Map GovActionId (GovActionState ConwayEra)
forall a. Monoid a => a
mempty
        ([GovActionState ConwayEra]
 -> Map GovActionId (GovActionState ConwayEra))
-> SpecTransM
     ConwayEra [GovActionState ConwayEra] [GovActionState ConwayEra]
-> SpecTransM
     ConwayEra
     [GovActionState ConwayEra]
     (Map GovActionId (GovActionState ConwayEra))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SpecTransM
  ConwayEra [GovActionState ConwayEra] [GovActionState ConwayEra]
forall era ctx. SpecTransM era ctx ctx
askSpecTransM
    let
      lookupGAS GovActionId
gaId SpecTransM
  ConwayEra
  [GovActionState ConwayEra]
  (Set (GovActionId, GovActionState ConwayEra))
m = do
        case GovActionId
-> Map GovActionId (GovActionState ConwayEra)
-> Maybe (GovActionState ConwayEra)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup GovActionId
gaId Map GovActionId (GovActionState ConwayEra)
govActionMap of
          Just GovActionState ConwayEra
x -> (GovActionId, GovActionState ConwayEra)
-> Set (GovActionId, GovActionState ConwayEra)
-> Set (GovActionId, GovActionState ConwayEra)
forall a. Ord a => a -> Set a -> Set a
Set.insert (GovActionId
gaId, GovActionState ConwayEra
x) (Set (GovActionId, GovActionState ConwayEra)
 -> Set (GovActionId, GovActionState ConwayEra))
-> SpecTransM
     ConwayEra
     [GovActionState ConwayEra]
     (Set (GovActionId, GovActionState ConwayEra))
-> SpecTransM
     ConwayEra
     [GovActionState ConwayEra]
     (Set (GovActionId, GovActionState ConwayEra))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SpecTransM
  ConwayEra
  [GovActionState ConwayEra]
  (Set (GovActionId, GovActionState ConwayEra))
m
          Maybe (GovActionState ConwayEra)
Nothing ->
            Text
-> SpecTransM
     ConwayEra
     [GovActionState ConwayEra]
     (Set (GovActionId, GovActionState ConwayEra))
forall a. Text -> SpecTransM ConwayEra [GovActionState ConwayEra] a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Text
 -> SpecTransM
      ConwayEra
      [GovActionState ConwayEra]
      (Set (GovActionId, GovActionState ConwayEra)))
-> Text
-> SpecTransM
     ConwayEra
     [GovActionState ConwayEra]
     (Set (GovActionId, GovActionState ConwayEra))
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 ConwayEra) -> [Char]
forall a. ToExpr a => a -> [Char]
showExpr Map GovActionId (GovActionState ConwayEra)
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 ConwayEra (RatifySignal ConwayEra) where
  type
    SpecRep ConwayEra (RatifySignal ConwayEra) =
      [(SpecRep ConwayEra GovActionId, SpecRep ConwayEra (GovActionState ConwayEra))]

  toSpecRep :: RatifySignal ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (RatifySignal ConwayEra))
     (SpecRep ConwayEra (RatifySignal ConwayEra))
toSpecRep (RatifySignal StrictSeq (GovActionState ConwayEra)
x) =
    (GovActionState ConwayEra
 -> SpecTransM ConwayEra () ((Integer, Integer), GovActionState))
-> [GovActionState ConwayEra]
-> SpecTransM ConwayEra () [((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 ConwayEra
gas@GovActionState {GovActionId
gasId :: forall era. GovActionState era -> GovActionId
gasId :: GovActionId
gasId} -> (GovActionId, GovActionState ConwayEra)
-> SpecTransM
     ConwayEra
     ()
     (SpecRep ConwayEra GovActionId,
      SpecRep ConwayEra (GovActionState ConwayEra))
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 ConwayEra
gas)) (StrictSeq (GovActionState ConwayEra) -> [GovActionState ConwayEra]
forall a. StrictSeq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList StrictSeq (GovActionState ConwayEra)
x)

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

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

instance SpecNormalize TxId where
  specNormalize :: TxId -> TxId
specNormalize = TxId -> TxId
forall a. a -> a
id

instance SpecNormalize Agda.Timelock

instance SpecNormalize Agda.HSTimelock

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.DepositPurpose

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.LState

instance SpecNormalize Agda.HsRewardUpdate

instance SpecNormalize Agda.NewEpochState