Actions

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

open import Data.Rational using (ℚ)

open import Ledger.Conway.Foreign.HSLedger.Address
open import Ledger.Conway.Foreign.HSLedger.BaseTypes
open import Ledger.Conway.Foreign.HSLedger.PParams

open import Ledger.Conway.Specification.Gov.Base
open import Ledger.Conway.Specification.Gov.Actions govStructure using (Vote) public

DocHash = GovStructure.DocHash govStructure

-- nondependent version of GovAction
data GovAction' : Type where
  NoConfidence        :                                             GovAction'
  UpdateCommittee     : (Credential ⇀ Epoch) → ℙ Credential → ℚ  →  GovAction'
  NewConstitution     : DocHash → Maybe ScriptHash               →  GovAction'
  TriggerHardFork     : ProtVer                                  →  GovAction'
  ChangePParams       : PParamsUpdate                            →  GovAction'
  TreasuryWithdrawal  : (RewardAddress ⇀ Treasury)               →  GovAction'
  Info                :                                             GovAction'

instance
  mkGovAction' : Convertible GovAction GovAction'
  mkGovAction' = λ where
    .to $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2446}{\htmlId{1252}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\,        \\ \,\htmlId{1274}{\htmlClass{Symbol}{\text{\_}}}\,           \end{pmatrix}$ → NoConfidence
    .to $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2484}{\htmlId{1315}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\,     \\ \,\htmlId{1337}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1338}{\htmlId{1338}{\htmlClass{Bound}{\text{m}}}}\, , \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1342}{\htmlId{1342}{\htmlClass{Bound}{\text{p}}}}\, , \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1346}{\htmlId{1346}{\htmlClass{Bound}{\text{q}}}}\,\,\htmlId{1347}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ → (UpdateCommittee m p q)
    .to $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2522}{\htmlId{1389}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\,     \\ \,\htmlId{1411}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1412}{\htmlId{1412}{\htmlClass{Bound}{\text{dh}}}}\, , \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1417}{\htmlId{1417}{\htmlClass{Bound}{\text{s}}}}\, \,\htmlId{1419}{\htmlClass{Symbol}{\text{)}}}\,   \end{pmatrix}$ → (NewConstitution dh s)
    .to $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2560}{\htmlId{1462}{\htmlClass{InductiveConstructor}{\text{TriggerHardFork}}}}\,     \\ \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1484}{\htmlId{1484}{\htmlClass{Bound}{\text{p}}}}\,           \end{pmatrix}$ → (TriggerHardFork p)
    .to $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2598}{\htmlId{1532}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\,       \\ \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1554}{\htmlId{1554}{\htmlClass{Bound}{\text{pu}}}}\,          \end{pmatrix}$ → (ChangePParams pu)
    .to $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2636}{\htmlId{1601}{\htmlClass{InductiveConstructor}{\text{TreasuryWithdrawal}}}}\,  \\ \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1623}{\htmlId{1623}{\htmlClass{Bound}{\text{m}}}}\,           \end{pmatrix}$ → ((TreasuryWithdrawal m))
    .to $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2674}{\htmlId{1676}{\htmlClass{InductiveConstructor}{\text{Info}}}}\,                \\ \,\htmlId{1698}{\htmlClass{Symbol}{\text{\_}}}\,           \end{pmatrix}$ → Info
    .from NoConfidence              → $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2446}{\htmlId{1761}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\,        \\ \,\href{Agda.Builtin.Unit.html#212}{\htmlId{1783}{\htmlClass{InductiveConstructor}{\text{tt}}}}\,          \end{pmatrix}$
    .from (UpdateCommittee m p q)   → $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2484}{\htmlId{1839}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\,     \\ \,\htmlId{1861}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1826}{\htmlId{1862}{\htmlClass{Bound}{\text{m}}}}\, , \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1828}{\htmlId{1866}{\htmlClass{Bound}{\text{p}}}}\, , \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1830}{\htmlId{1870}{\htmlClass{Bound}{\text{q}}}}\,\,\htmlId{1871}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$
    .from (NewConstitution dh s)    → $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2522}{\htmlId{1917}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\,     \\ \,\htmlId{1939}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1904}{\htmlId{1940}{\htmlClass{Bound}{\text{dh}}}}\, , \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1907}{\htmlId{1945}{\htmlClass{Bound}{\text{s}}}}\,\,\htmlId{1946}{\htmlClass{Symbol}{\text{)}}}\,    \end{pmatrix}$
    .from (TriggerHardFork p)       → $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2560}{\htmlId{1995}{\htmlClass{InductiveConstructor}{\text{TriggerHardFork}}}}\,     \\ \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1982}{\htmlId{2017}{\htmlClass{Bound}{\text{p}}}}\,           \end{pmatrix}$
    .from (ChangePParams pu)        → $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2598}{\htmlId{2073}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\,       \\ \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#2058}{\htmlId{2095}{\htmlClass{Bound}{\text{pu}}}}\,          \end{pmatrix}$
    .from (TreasuryWithdrawal m)    → $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2636}{\htmlId{2151}{\htmlClass{InductiveConstructor}{\text{TreasuryWithdrawal}}}}\,  \\ \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#2141}{\htmlId{2173}{\htmlClass{Bound}{\text{m}}}}\,           \end{pmatrix}$
    .from Info                      → $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2674}{\htmlId{2229}{\htmlClass{InductiveConstructor}{\text{Info}}}}\,                \\ \,\href{Agda.Builtin.Unit.html#212}{\htmlId{2251}{\htmlClass{InductiveConstructor}{\text{tt}}}}\,          \end{pmatrix}$

  HsTy-GovAction' = autoHsType GovAction' ⊣ withName "GovAction"
  Conv-GovAction' = autoConvert GovAction'

  HsTy-GovAction = MkHsType GovAction (HsType GovAction')
  Conv-GovAction = mkGovAction' ⨾ Conv-GovAction'