Core

module Ledger.Conway.Foreign.HSLedger.Gov.Core where

open import Ledger.Conway.Foreign.HSLedger.Address
open import Ledger.Conway.Foreign.HSLedger.BaseTypes
open import Ledger.Conway.Specification.Gov.Actions govStructure using (Vote)

instance
  HsTy-GovRole = autoHsType GovRole
  Conv-GovRole = autoConvert GovRole

  HsTy-Anchor = autoHsType Anchor
  Conv-Anchor = autoConvert Anchor

  HsTy-VDeleg = autoHsType VDeleg
  Conv-VDeleg = autoConvert VDeleg

  HsTy-Vote = autoHsType Vote
  Conv-Vote = autoConvert Vote

  HsTy-GovVotes = autoHsType GovVotes
  Conv-GovVotes = autoConvert GovVotes

GovVoter' : Type
GovVoter' = GovRole × Credential

instance
  mkGovVoter' : Convertible GovVoter GovVoter'
  mkGovVoter' .to $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#970}{\htmlId{829}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   \\ \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Core.html#836}{\htmlId{836}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$ = CC   , c
  mkGovVoter' .to $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#973}{\htmlId{873}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Core.html#880}{\htmlId{880}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$ = DRep , c
  mkGovVoter' .to $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#978}{\htmlId{917}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  \\ \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Core.html#924}{\htmlId{924}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$ = SPO  , KeyHashObj c
  mkGovVoter' .from (CC   , c)   = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#970}{\htmlId{989}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   \\ \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Core.html#980}{\htmlId{996}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$
  mkGovVoter' .from (DRep , c)   = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#973}{\htmlId{1039}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Core.html#1030}{\htmlId{1046}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$
  mkGovVoter' .from (SPO  , c)   =
    case c of λ where
      (KeyHashObj kh) → $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#978}{\htmlId{1135}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Core.html#1127}{\htmlId{1141}{\htmlClass{Bound}{\text{kh}}}}\, \end{pmatrix}$
      (ScriptObj _)   → error "mkGovVoter: Converting from SPO with ScriptObj credential"

  HsTy-GovVoter = MkHsType GovVoter (HsType GovVoter')
  Conv-GovVoter : Convertible GovVoter (HsType GovVoter')
  Conv-GovVoter = mkGovVoter' ⨾ Convertible-Pair

unquoteDecl = do
  hsTypeAlias GovVoter

record GovVote' : Type where
  field
    gid         : GovActionID
    voter       : GovVoter'
    vote        : Vote
    anchor      : Maybe Anchor

instance
  mkGovVote' : Convertible GovVote GovVote'
  mkGovVote' = λ where
    .to v   → let module v = GovVote v in record { gid = v.gid ; voter = to v.voter  ; vote = v.vote ; anchor = v.anchor }
    .from v → let module v = GovVote' v in record { gid = v.gid ; voter = from v.voter ; vote = v.vote ; anchor = v.anchor }

  HsTy-GovVote' = autoHsType GovVote' ⊣ withConstructor "MkGovVote"
                                      • withName "GovVote"
  Conv-GovVote' = autoConvert GovVote'

  HsTy-GovVote = MkHsType GovVote (HsType GovVote')
  Conv-GovVote = mkGovVote' ⨾ Conv-GovVote'