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#1200}{\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#1203}{\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#1208}{\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#1200}{\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#1203}{\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#1208}{\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'