module Ledger.Conway.Foreign.Certs where

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

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

open import Ledger.Core.Foreign.Address
open import Ledger.Conway.Foreign.HSStructures renaming (⟦_,_,_⟧ᵈ to ⟦_,_,_⟧ᵈ'; DState to DState'
                                                              ; ⟦_,_⟧ᵛ to ⟦_,_⟧ᵛ'; GState to GState') hiding (CertEnv)
open import Ledger.Conway.Foreign.Gov.Core
open import Ledger.Conway.Foreign.PParams
open import Ledger.Conway.Conformance.Certs govStructure using (⟦_,_,_,_⟧ᵈ; ⟦_,_,_⟧ᵛ; DState; GState; CertEnv)
open import Ledger.Conway.Specification.Certs.Properties.Computational govStructure
  using (Computational-POOL)
open import Ledger.Conway.Conformance.Certs.Properties govStructure
  using ( Computational-DELEG
        ; Computational-GOVCERT
        )

open Computational

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     : RewardAddress ⇀ 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.Certs.html#2777}{\htmlId{2777}{\htmlClass{Bound}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Foreign.Certs.html#2790}{\htmlId{2790}{\htmlClass{Bound}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Conway.Foreign.Certs.html#2804}{\htmlId{2804}{\htmlClass{Bound}{\text{rewards}}}}\, \\ \,\href{Ledger.Conway.Foreign.Certs.html#2814}{\htmlId{2814}{\htmlClass{Bound}{\text{deposits}}}}\, \end{pmatrix}$ = $\begin{pmatrix} \,\href{Ledger.Conway.Foreign.Certs.html#2777}{\htmlId{2830}{\htmlClass{Bound}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Foreign.Certs.html#2790}{\htmlId{2843}{\htmlClass{Bound}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Conway.Foreign.Certs.html#2790}{\htmlId{2857}{\htmlClass{Bound}{\text{stakeDelegs}}}}\, \end{pmatrix}$
  Conv-DState-DState' .from $\begin{pmatrix} \,\href{Ledger.Conway.Foreign.Certs.html#2903}{\htmlId{2903}{\htmlClass{Bound}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Foreign.Certs.html#2916}{\htmlId{2916}{\htmlClass{Bound}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Conway.Foreign.Certs.html#2930}{\htmlId{2930}{\htmlClass{Bound}{\text{rewards}}}}\, \end{pmatrix}$         = $\begin{pmatrix} \,\href{Ledger.Conway.Foreign.Certs.html#2903}{\htmlId{2954}{\htmlClass{Bound}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Foreign.Certs.html#2916}{\htmlId{2967}{\htmlClass{Bound}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Conway.Foreign.Certs.html#2916}{\htmlId{2981}{\htmlClass{Bound}{\text{stakeDelegs}}}}\, \\ \,\href{Class.HasEmptySet.html#287}{\htmlId{2995}{\htmlClass{Field}{\text{∅}}}}\, \end{pmatrix}$

  Conv-GState-GState' : Convertible GState GState'
  Conv-GState-GState' .to $\begin{pmatrix} \,\href{Ledger.Conway.Foreign.Certs.html#3080}{\htmlId{3080}{\htmlClass{Bound}{\text{dreps}}}}\, \\ \,\href{Ledger.Conway.Foreign.Certs.html#3088}{\htmlId{3088}{\htmlClass{Bound}{\text{ccHotKeys}}}}\, \\ \,\href{Ledger.Conway.Foreign.Certs.html#3100}{\htmlId{3100}{\htmlClass{Bound}{\text{deposits}}}}\, \end{pmatrix}$ = $\begin{pmatrix} \,\href{Ledger.Conway.Foreign.Certs.html#3080}{\htmlId{3116}{\htmlClass{Bound}{\text{dreps}}}}\, \\ \,\href{Ledger.Conway.Foreign.Certs.html#3088}{\htmlId{3124}{\htmlClass{Bound}{\text{ccHotKeys}}}}\, \end{pmatrix}$
  Conv-GState-GState' .from $\begin{pmatrix} \,\href{Ledger.Conway.Foreign.Certs.html#3168}{\htmlId{3168}{\htmlClass{Bound}{\text{dreps}}}}\, \\ \,\href{Ledger.Conway.Foreign.Certs.html#3176}{\htmlId{3176}{\htmlClass{Bound}{\text{ccHotKeys}}}}\, \end{pmatrix}$         = $\begin{pmatrix} \,\href{Ledger.Conway.Foreign.Certs.html#3168}{\htmlId{3202}{\htmlClass{Bound}{\text{dreps}}}}\, \\ \,\href{Ledger.Conway.Foreign.Certs.html#3176}{\htmlId{3210}{\htmlClass{Bound}{\text{ccHotKeys}}}}\, \\ \,\href{Class.HasEmptySet.html#287}{\htmlId{3222}{\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 #-}