module Ledger.Dijkstra.Foreign.PParams where

open import Class.Convertible
open import Class.HasHsType.Foreign
open import Class.Convertible.Foreign
open import Tactic.Derive.Convertible
open import Tactic.Derive.HsType

open import Ledger.Prelude
open import Ledger.Prelude.Foreign.HSTypes

open import Ledger.Dijkstra.Foreign.HSStructures

instance
  HsTy-LanguageCostModels = autoHsType LanguageCostModels ⊣ withConstructor "MkLanguageCostModels"
                                                          • fieldPrefix "lcm"
  Conv-LanguageCostModels = autoConvert LanguageCostModels

  HsTy-DrepThresholds = autoHsType DrepThresholds
    ⊣ withConstructor "MkDrepThresholds"
  Conv-DrepThresholds = autoConvert DrepThresholds

  HsTy-PoolThresholds = autoHsType PoolThresholds
    ⊣ withConstructor "MkPoolThresholds"
  Conv-PoolThresholds = autoConvert PoolThresholds

  HsTy-Acnt = autoHsType Acnt ⊣ withConstructor "MkAcnt"
  Conv-Acnt = autoConvert Acnt

  HsTy-PParams = autoHsType PParams ⊣ withConstructor "MkPParams"
                                    • fieldPrefix "pp"
  Conv-PParams = autoConvert PParams

  HsTy-PParamsUpdate = autoHsType PParamsUpdate.PParamsUpdate ⊣ withConstructor "MkPParamsUpdate"
                                                              • fieldPrefix "ppu"
  Conv-PParamsUpdate = autoConvert PParamsUpdate.PParamsUpdate