module Ledger.Conway.Foreign.HSLedger.Certs where

open import Ledger.Conway.Foreign.HSLedger.Address
open import Ledger.Conway.Foreign.HSLedger.BaseTypes renaming (⟦_,_,_⟧ᵈ to ⟦_,_,_⟧ᵈ'; DState to DState'
                                                              ; ⟦_,_⟧ᵛ to ⟦_,_⟧ᵛ'; GState to GState') hiding (CertEnv)
open import Ledger.Conway.Foreign.HSLedger.Gov.Core
open import Ledger.Conway.Foreign.HSLedger.PParams

open import Ledger.Conway.Conformance.Certs govStructure using (⟦_,_,_,_⟧ᵈ; ⟦_,_,_⟧ᵛ; DState; GState; CertEnv)

open import Ledger.Conway.Conformance.Certs.Properties govStructure
  using ( Computational-DELEG
        ; Computational-GOVCERT
        ; Computational-POOL
        )

instance
  HsTy-StakePoolParams = autoHsType StakePoolParams
  Conv-StakePoolParams = autoConvert StakePoolParams

  HsTy-DepositPurpose = autoHsType DepositPurpose
  Conv-DepositPurpose = autoConvert DepositPurpose

  HsTy-DelegEnv = autoHsType DelegEnv
     withConstructor "MkDelegEnv"
     fieldPrefix "de"
     withName "DelegEnv"
  Conv-DelegEnv = autoConvert DelegEnv

  HsTy-PState = autoHsType PState
     withConstructor "MkPState"
     fieldPrefix "ps"
  Conv-PState = autoConvert PState

record CertEnv' : Type where
  field
    epoch     : Epoch
    pp        : PParams
    votes     : List GovVote'
    wdrls     : RwdAddr  Coin
    coldCreds :  Credential

instance
  HsTy-CertEnv' = autoHsType CertEnv'
     withConstructor "MkCertEnv"
     withName "CertEnv"
     fieldPrefix "ce"
  Conv-CertEnv' = autoConvert CertEnv'

  mkCertEnv' : Convertible CertEnv CertEnv'
  mkCertEnv' = λ where
    .to   ce  let module ce = CertEnv ce in record { epoch = ce.epoch ; pp = ce.pp ; votes = to ce.votes ; wdrls = ce.wdrls ; coldCreds = ce.coldCreds }
    .from ce  let module ce = CertEnv' ce in record { epoch = ce.epoch ; pp = ce.pp ; votes = from ce.votes ; wdrls = ce.wdrls ; coldCreds = ce.coldCreds }

  HsTy-CertEnv = MkHsType CertEnv (HsType CertEnv')
  Conv-CertEnv = mkCertEnv'  Conv-CertEnv'

instance
  HsTy-DState = autoHsType DState
     withConstructor "MkDState"
     withName "DState"
     fieldPrefix "ds"
  Conv-DState = autoConvert DState

  HsTy-DCert = autoHsType DCert
  Conv-DCert = autoConvert DCert

  HsTy-GState = autoHsType GState
     withConstructor "MkGState"
     fieldPrefix "gs"
  Conv-GState = autoConvert GState

  Conv-DState-DState' : Convertible DState DState'
  Conv-DState-DState' .to $\begin{pmatrix} \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2466}{\htmlId{2466}{\htmlClass{Bound}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2479}{\htmlId{2479}{\htmlClass{Bound}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2493}{\htmlId{2493}{\htmlClass{Bound}{\text{rewards}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2503}{\htmlId{2503}{\htmlClass{Bound}{\text{deposits}}}}\, \end{pmatrix}$ = $\begin{pmatrix} \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2466}{\htmlId{2519}{\htmlClass{Bound}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2479}{\htmlId{2532}{\htmlClass{Bound}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2479}{\htmlId{2546}{\htmlClass{Bound}{\text{stakeDelegs}}}}\, \end{pmatrix}$
  Conv-DState-DState' .from $\begin{pmatrix} \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2592}{\htmlId{2592}{\htmlClass{Bound}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2605}{\htmlId{2605}{\htmlClass{Bound}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2619}{\htmlId{2619}{\htmlClass{Bound}{\text{rewards}}}}\, \end{pmatrix}$         = $\begin{pmatrix} \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2592}{\htmlId{2643}{\htmlClass{Bound}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2605}{\htmlId{2656}{\htmlClass{Bound}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2605}{\htmlId{2670}{\htmlClass{Bound}{\text{stakeDelegs}}}}\, \\ \,\href{Class.HasEmptySet.html#287}{\htmlId{2684}{\htmlClass{Field}{\text{∅}}}}\, \end{pmatrix}$

  Conv-GState-GState' : Convertible GState GState'
  Conv-GState-GState' .to $\begin{pmatrix} \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2769}{\htmlId{2769}{\htmlClass{Bound}{\text{dreps}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2777}{\htmlId{2777}{\htmlClass{Bound}{\text{ccHotKeys}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2789}{\htmlId{2789}{\htmlClass{Bound}{\text{deposits}}}}\, \end{pmatrix}$ = $\begin{pmatrix} \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2769}{\htmlId{2805}{\htmlClass{Bound}{\text{dreps}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2777}{\htmlId{2813}{\htmlClass{Bound}{\text{ccHotKeys}}}}\, \end{pmatrix}$
  Conv-GState-GState' .from $\begin{pmatrix} \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2857}{\htmlId{2857}{\htmlClass{Bound}{\text{dreps}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2865}{\htmlId{2865}{\htmlClass{Bound}{\text{ccHotKeys}}}}\, \end{pmatrix}$         = $\begin{pmatrix} \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2857}{\htmlId{2891}{\htmlClass{Bound}{\text{dreps}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2865}{\htmlId{2899}{\htmlClass{Bound}{\text{ccHotKeys}}}}\, \\ \,\href{Class.HasEmptySet.html#287}{\htmlId{2911}{\htmlClass{Field}{\text{∅}}}}\, \end{pmatrix}$

deleg-step : HsType (DelegEnv  DState  DCert  ComputationResult String DState)
deleg-step = to (compute Computational-DELEG)

{-# COMPILE GHC deleg-step as delegStep #-}

pool-step : HsType (PParams  PState  DCert  ComputationResult String PState)
pool-step = to (compute Computational-POOL)

{-# COMPILE GHC pool-step as poolStep #-}

govcert-step : HsType (CertEnv  GState  DCert  ComputationResult String GState)
govcert-step = to (compute Computational-GOVCERT)

{-# COMPILE GHC govcert-step as govCertStep #-}