Core

module Ledger.Conway.Foreign.Gov.Core where

open import Foreign.Convertible
open import Foreign.Convertible.Deriving
open import Foreign.HaskellTypes.Deriving

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

open import Ledger.Core.Foreign.Address
open import Ledger.Conway.Foreign.HSStructures hiding (Vote)
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#1024}{\htmlId{1038}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   \\ \,\href{Ledger.Conway.Foreign.Gov.Core.html#1045}{\htmlId{1045}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$ = CC   , c
  mkGovVoter' .to $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1027}{\htmlId{1082}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, \\ \,\href{Ledger.Conway.Foreign.Gov.Core.html#1089}{\htmlId{1089}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$ = DRep , c
  mkGovVoter' .to $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1032}{\htmlId{1126}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  \\ \,\href{Ledger.Conway.Foreign.Gov.Core.html#1133}{\htmlId{1133}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$ = SPO  , KeyHashObj c
  mkGovVoter' .from (CC   , c)   = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1024}{\htmlId{1198}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   \\ \,\href{Ledger.Conway.Foreign.Gov.Core.html#1189}{\htmlId{1205}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$
  mkGovVoter' .from (DRep , c)   = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1027}{\htmlId{1248}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, \\ \,\href{Ledger.Conway.Foreign.Gov.Core.html#1239}{\htmlId{1255}{\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#1032}{\htmlId{1344}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\, \\ \,\href{Ledger.Conway.Foreign.Gov.Core.html#1336}{\htmlId{1350}{\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'