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#368}{\htmlId{728}{\htmlClass{InductiveConstructor}{\text{CC}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Core.html#735}{\htmlId{735}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$ = CC , c mkGovVoter' .to $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#371}{\htmlId{772}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Core.html#779}{\htmlId{779}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$ = DRep , c mkGovVoter' .to $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#376}{\htmlId{816}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Core.html#823}{\htmlId{823}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$ = SPO , KeyHashObj c mkGovVoter' .from (CC , c) = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#368}{\htmlId{888}{\htmlClass{InductiveConstructor}{\text{CC}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Core.html#879}{\htmlId{895}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$ mkGovVoter' .from (DRep , c) = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#371}{\htmlId{938}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Core.html#929}{\htmlId{945}{\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#376}{\htmlId{1034}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Core.html#1026}{\htmlId{1040}{\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'