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.Gov.Base
open import Ledger.Conway.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'
  TriggerHF        : ProtVer                                  →  GovAction'
  ChangePParams    : PParamsUpdate                            →  GovAction'
  TreasuryWdrl     : (RwdAddr ⇀ Coin)                         →  GovAction'
  Info             :                                             GovAction'

instance
  mkGovAction' : Convertible GovAction GovAction'
  mkGovAction' = λ where
    .to $\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#1420}{\htmlId{1105}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\,    \\ \,\htmlId{1123}{\htmlClass{Symbol}{\text{\_}}}\,           \end{pmatrix}$ → NoConfidence
    .to $\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#1455}{\htmlId{1164}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, \\ (\,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1183}{\htmlId{1183}{\htmlClass{Bound}{\text{m}}}}\, , \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1187}{\htmlId{1187}{\htmlClass{Bound}{\text{p}}}}\, , \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1191}{\htmlId{1191}{\htmlClass{Bound}{\text{q}}}}\,) \end{pmatrix}$ → (UpdateCommittee m p q)
    .to $\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#1490}{\htmlId{1234}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\, \\ (\,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1253}{\htmlId{1253}{\htmlClass{Bound}{\text{dh}}}}\, , \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1258}{\htmlId{1258}{\htmlClass{Bound}{\text{s}}}}\, )   \end{pmatrix}$ → (NewConstitution dh s)
    .to $\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#1525}{\htmlId{1303}{\htmlClass{InductiveConstructor}{\text{TriggerHF}}}}\,       \\ \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1321}{\htmlId{1321}{\htmlClass{Bound}{\text{p}}}}\,           \end{pmatrix}$ → (TriggerHF p)
    .to $\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#1560}{\htmlId{1363}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\,   \\ \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1381}{\htmlId{1381}{\htmlClass{Bound}{\text{pu}}}}\,          \end{pmatrix}$ → (ChangePParams pu)
    .to $\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#1595}{\htmlId{1428}{\htmlClass{InductiveConstructor}{\text{TreasuryWdrl}}}}\,    \\ \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1446}{\htmlId{1446}{\htmlClass{Bound}{\text{m}}}}\,           \end{pmatrix}$ → ((TreasuryWdrl m))
    .to $\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#1630}{\htmlId{1493}{\htmlClass{InductiveConstructor}{\text{Info}}}}\,            \\ \,\htmlId{1511}{\htmlClass{Symbol}{\text{\_}}}\,           \end{pmatrix}$ → Info
    .from NoConfidence                → $\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#1420}{\htmlId{1576}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\,    \\ \,\href{Agda.Builtin.Unit.html#212}{\htmlId{1594}{\htmlClass{InductiveConstructor}{\text{tt}}}}\,          \end{pmatrix}$
    .from (UpdateCommittee m p q)     → $\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#1455}{\htmlId{1652}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, \\ (\,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1637}{\htmlId{1671}{\htmlClass{Bound}{\text{m}}}}\, , \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1639}{\htmlId{1675}{\htmlClass{Bound}{\text{p}}}}\, , \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1641}{\htmlId{1679}{\htmlClass{Bound}{\text{q}}}}\,) \end{pmatrix}$
    .from (NewConstitution dh s)      → $\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#1490}{\htmlId{1728}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\, \\ (\,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1713}{\htmlId{1747}{\htmlClass{Bound}{\text{dh}}}}\, , \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1716}{\htmlId{1752}{\htmlClass{Bound}{\text{s}}}}\,)    \end{pmatrix}$
    .from (TriggerHF p)               → $\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#1525}{\htmlId{1804}{\htmlClass{InductiveConstructor}{\text{TriggerHF}}}}\,       \\ \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1783}{\htmlId{1822}{\htmlClass{Bound}{\text{p}}}}\,           \end{pmatrix}$
    .from (ChangePParams pu)          → $\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#1560}{\htmlId{1880}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\,   \\ \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1863}{\htmlId{1898}{\htmlClass{Bound}{\text{pu}}}}\,          \end{pmatrix}$
    .from (TreasuryWdrl m)            → $\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#1595}{\htmlId{1956}{\htmlClass{InductiveConstructor}{\text{TreasuryWdrl}}}}\,    \\ \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1938}{\htmlId{1974}{\htmlClass{Bound}{\text{m}}}}\,           \end{pmatrix}$
    .from Info                        → $\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#1630}{\htmlId{2032}{\htmlClass{InductiveConstructor}{\text{Info}}}}\, \\ \,\href{Agda.Builtin.Unit.html#212}{\htmlId{2039}{\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'