module Ledger.Core.Foreign.Address where

open import Ledger.Prelude
open import Ledger.Prelude.Foreign.HSTypes
open import Ledger.Core.Specification.Address ℕ ℕ ℕ ⦃ it ⦄ ⦃ it ⦄ ⦃ it ⦄

open import Class.Convertible
open import Class.HasHsType.Foreign
open import Tactic.Derive.Convertible
open import Tactic.Derive.HsType
open import stdlib.Foreign.Haskell.Empty

instance
  HsTy-Credential = autoHsType Credential
  Conv-Credential = autoConvert Credential

  HsTy-BaseAddr = autoHsType BaseAddr ⊣ fieldPrefix "base"
  Conv-BaseAddr = autoConvert BaseAddr

  HsTy-BootstrapAddr = autoHsType BootstrapAddr ⊣ fieldPrefix "boot"
  Conv-BootstrapAddr = autoConvert BootstrapAddr

  HsTy-RewardAddress = autoHsType RewardAddress ⊣ fieldPrefix "rwd"
  Conv-RewardAddress = autoConvert RewardAddress

unquoteDecl = do
  hsTypeAlias Addr