module Ledger.Conway.Foreign.Cert where

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

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

open import Ledger.Conway.Foreign.HSStructures hiding (CertEnv; DCert) renaming (⟦_,_,_⟧ᶜˢ to ⟦_,_,_⟧ᶜˢ'; CertState to CertState')
open import Ledger.Conway.Foreign.Certs public
open import Ledger.Conway.Conformance.Certs.Properties govStructure
  using ( Computational-CERT
        ; Computational-CERTS
        )
open import Ledger.Conway.Conformance.Certs govStructure

open Computational

instance
  Conv-CertState-CertState' : Convertible CertState CertState'
  Conv-CertState-CertState' .to $\begin{pmatrix} \,\href{Ledger.Conway.Foreign.Cert.html#742}{\htmlId{742}{\htmlClass{Bound}{\text{dState}}}}\, \\ \,\href{Ledger.Conway.Foreign.Cert.html#751}{\htmlId{751}{\htmlClass{Bound}{\text{pState}}}}\, \\ \,\href{Ledger.Conway.Foreign.Cert.html#760}{\htmlId{760}{\htmlClass{Bound}{\text{gState}}}}\, \end{pmatrix}$    = $\begin{pmatrix} \,\href{Class.Convertible.Core.html#228}{\htmlId{778}{\htmlClass{Field}{\text{to}}}}\, \,\href{Ledger.Conway.Foreign.Cert.html#742}{\htmlId{781}{\htmlClass{Bound}{\text{dState}}}}\, \\ \,\href{Ledger.Conway.Foreign.Cert.html#751}{\htmlId{790}{\htmlClass{Bound}{\text{pState}}}}\, \\ \,\href{Class.Convertible.Core.html#228}{\htmlId{799}{\htmlClass{Field}{\text{to}}}}\, \,\href{Ledger.Conway.Foreign.Cert.html#760}{\htmlId{802}{\htmlClass{Bound}{\text{gState}}}}\, \end{pmatrix}$
  Conv-CertState-CertState' .from $\begin{pmatrix} \,\href{Ledger.Conway.Foreign.Cert.html#850}{\htmlId{850}{\htmlClass{Bound}{\text{dState}}}}\, \\ \,\href{Ledger.Conway.Foreign.Cert.html#859}{\htmlId{859}{\htmlClass{Bound}{\text{pState}}}}\, \\ \,\href{Ledger.Conway.Foreign.Cert.html#868}{\htmlId{868}{\htmlClass{Bound}{\text{gState}}}}\, \end{pmatrix}$ = $\begin{pmatrix} \,\href{Class.Convertible.Core.html#249}{\htmlId{884}{\htmlClass{Field}{\text{from}}}}\, \,\href{Ledger.Conway.Foreign.Cert.html#850}{\htmlId{889}{\htmlClass{Bound}{\text{dState}}}}\, \\ \,\href{Ledger.Conway.Foreign.Cert.html#859}{\htmlId{898}{\htmlClass{Bound}{\text{pState}}}}\, \\ \,\href{Class.Convertible.Core.html#249}{\htmlId{907}{\htmlClass{Field}{\text{from}}}}\, \,\href{Ledger.Conway.Foreign.Cert.html#868}{\htmlId{912}{\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 #-}