module Ledger.Conway.Foreign.HSLedger.Cert where

open import Ledger.Conway.Foreign.HSLedger.BaseTypes hiding (CertEnv; DCert) renaming (⟦_,_,_⟧ᶜˢ to ⟦_,_,_⟧ᶜˢ'; CertState to CertState')
open import Ledger.Conway.Foreign.HSLedger.Certs

open import Ledger.Conway.Conformance.Certs.Properties govStructure
  using ( Computational-CERT
        ; Computational-CERTS
        )

open import Ledger.Conway.Conformance.Certs govStructure

instance
  -- HsTy-CertState = autoHsType' CertState (⟦_,_,_⟧ᶜˢ ↦ "MkCertState" ∷ [])
  -- Conv-CertState = autoConvert CertState

  HsTy-CertState = autoHsType CertState ⊣ withConstructor "MkCertState"
  Conv-CertState = autoConvert CertState

  Conv-CertState-CertState' : Convertible CertState CertState'
  Conv-CertState-CertState' .to $\begin{pmatrix} \,\href{Ledger.Conway.Foreign.HSLedger.Cert.html#776}{\htmlId{776}{\htmlClass{Bound}{\text{dState}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Cert.html#785}{\htmlId{785}{\htmlClass{Bound}{\text{pState}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Cert.html#794}{\htmlId{794}{\htmlClass{Bound}{\text{gState}}}}\, \end{pmatrix}$    = $\begin{pmatrix} \,\href{Foreign.Convertible.html#149}{\htmlId{812}{\htmlClass{Field}{\text{to}}}}\, \,\href{Ledger.Conway.Foreign.HSLedger.Cert.html#776}{\htmlId{815}{\htmlClass{Bound}{\text{dState}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Cert.html#785}{\htmlId{824}{\htmlClass{Bound}{\text{pState}}}}\, \\ \,\href{Foreign.Convertible.html#149}{\htmlId{833}{\htmlClass{Field}{\text{to}}}}\, \,\href{Ledger.Conway.Foreign.HSLedger.Cert.html#794}{\htmlId{836}{\htmlClass{Bound}{\text{gState}}}}\, \end{pmatrix}$
  Conv-CertState-CertState' .from $\begin{pmatrix} \,\href{Ledger.Conway.Foreign.HSLedger.Cert.html#884}{\htmlId{884}{\htmlClass{Bound}{\text{dState}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Cert.html#893}{\htmlId{893}{\htmlClass{Bound}{\text{pState}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Cert.html#902}{\htmlId{902}{\htmlClass{Bound}{\text{gState}}}}\, \end{pmatrix}$ = $\begin{pmatrix} \,\href{Foreign.Convertible.html#170}{\htmlId{918}{\htmlClass{Field}{\text{from}}}}\, \,\href{Ledger.Conway.Foreign.HSLedger.Cert.html#884}{\htmlId{923}{\htmlClass{Bound}{\text{dState}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Cert.html#893}{\htmlId{932}{\htmlClass{Bound}{\text{pState}}}}\, \\ \,\href{Foreign.Convertible.html#170}{\htmlId{941}{\htmlClass{Field}{\text{from}}}}\, \,\href{Ledger.Conway.Foreign.HSLedger.Cert.html#902}{\htmlId{946}{\htmlClass{Bound}{\text{gState}}}}\, \end{pmatrix}$

certs-step : HsType (CertEnv → CertState → List DCert → ComputationResult String CertState)
certs-step = to (compute Computational-CERTS)

{-# COMPILE GHC certs-step as certsStep #-}

cert-step : HsType (CertEnv → CertState → DCert → ComputationResult String CertState)
cert-step = to (compute Computational-CERT)

{-# COMPILE GHC cert-step as certStep #-}