module Ledger.Conway.Foreign.HSLedger.Ratify where
open import Ledger.Conway.Foreign.HSLedger.Address
open import Ledger.Conway.Foreign.HSLedger.BaseTypes
open import Ledger.Conway.Foreign.HSLedger.Certs
open import Ledger.Conway.Foreign.HSLedger.Enact
open import Ledger.Conway.Foreign.HSLedger.Gov.Core
open import Ledger.Conway.Foreign.HSLedger.Gov
open import Ledger.Conway.Specification.Enact govStructure
open import Data.String.Base renaming (_++_ to _+ˢ_) hiding (show; length)
import Data.Rational.Show as Rational
import Foreign.Haskell.Pair as F
open import Ledger.Conway.Specification.Ratify it
open import Ledger.Conway.Specification.Ratify.Properties it
instance
HsTy-StakeDistrs = autoHsType StakeDistrs
Conv-StakeDistrs = autoConvert StakeDistrs
HsTy-RatifyEnv = autoHsType RatifyEnv ⊣ withConstructor "MkRatifyEnv"
• fieldPrefix "re"
Conv-RatifyEnv = autoConvert RatifyEnv
HsTy-RatifyState = autoHsType RatifyState ⊣ withConstructor "MkRatifyState"
• fieldPrefix "rs"
• RatifyState.es ↦ "rsEnactState"
Conv-RatifyState = autoConvert RatifyState
ratify-step : HsType (RatifyEnv → RatifyState → List (GovActionID × GovActionState) → ComputationResult ⊥ RatifyState)
ratify-step = to (compute Computational-RATIFIES)
{-# COMPILE GHC ratify-step as ratifyStep #-}
instance
Show-RATIFIES : ∀ {Γ s sig s'}
→ Show (Γ ⊢ s ⇀⦇ sig ,RATIFIES⦈ s')
Show-RATIFIES {Γ} {s} {sig} .show r = ""