module Ledger.Conway.Foreign.HSLedger.NewEpoch where open import Ledger.Conway.Foreign.HSLedger.BaseTypes open import Ledger.Conway.Foreign.HSLedger.Epoch open import Ledger.Conway.Foreign.HSLedger.Rewards open import Ledger.Conway.Conformance.Epoch it it open import Ledger.Conway.Conformance.Epoch.Properties it it import Data.String as S instance Show-NEWEPOCH : ∀ {eps e eps'} → Show (_ ⊢ eps ⇀⦇ e ,NEWEPOCH⦈ eps') Show-NEWEPOCH .show (NEWEPOCH-New (_ , e)) = "NEWEPOCH-New " S.++ show e Show-NEWEPOCH .show (NEWEPOCH-Not-New x) = "NEWEPOCH-Not-New" Show-NEWEPOCH .show (NEWEPOCH-No-Reward-Update x) = "NEWEPOCH-No-Reward-Update" instance HsTy-NewEpochState = autoHsType NewEpochState ⊣ withConstructor "MkNewEpochState" Conv-NewEpochState = autoConvert NewEpochState newepoch-step : HsType (⊤ → NewEpochState → Epoch → ComputationResult ⊥ (NewEpochState × String)) newepoch-step _ newEpochSt e = let r = Computational-NEWEPOCH .computeProof _ (from newEpochSt) e in case r of λ where (success (s , p)) → to (success (s , show p)) {-# COMPILE GHC newepoch-step as newEpochStep #-}