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'
  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.Specification.Gov.Actions.html#1476}{\htmlId{1132}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\,    \\ \,\htmlId{1150}{\htmlClass{Symbol}{\text{\_}}}\,           \end{pmatrix}$ → NoConfidence
    .to $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1511}{\htmlId{1191}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, \\ (\,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1210}{\htmlId{1210}{\htmlClass{Bound}{\text{m}}}}\, , \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1214}{\htmlId{1214}{\htmlClass{Bound}{\text{p}}}}\, , \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1218}{\htmlId{1218}{\htmlClass{Bound}{\text{q}}}}\,) \end{pmatrix}$ → (UpdateCommittee m p q)
    .to $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1546}{\htmlId{1261}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\, \\ (\,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1280}{\htmlId{1280}{\htmlClass{Bound}{\text{dh}}}}\, , \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1285}{\htmlId{1285}{\htmlClass{Bound}{\text{s}}}}\, )   \end{pmatrix}$ → (NewConstitution dh s)
    .to $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1581}{\htmlId{1330}{\htmlClass{InductiveConstructor}{\text{TriggerHF}}}}\,       \\ \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1348}{\htmlId{1348}{\htmlClass{Bound}{\text{p}}}}\,           \end{pmatrix}$ → (TriggerHF p)
    .to $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1616}{\htmlId{1390}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\,   \\ \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1408}{\htmlId{1408}{\htmlClass{Bound}{\text{pu}}}}\,          \end{pmatrix}$ → (ChangePParams pu)
    .to $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1651}{\htmlId{1455}{\htmlClass{InductiveConstructor}{\text{TreasuryWdrl}}}}\,    \\ \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1473}{\htmlId{1473}{\htmlClass{Bound}{\text{m}}}}\,           \end{pmatrix}$ → ((TreasuryWdrl m))
    .to $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1686}{\htmlId{1520}{\htmlClass{InductiveConstructor}{\text{Info}}}}\,            \\ \,\htmlId{1538}{\htmlClass{Symbol}{\text{\_}}}\,           \end{pmatrix}$ → Info
    .from NoConfidence                → $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1476}{\htmlId{1603}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\,    \\ \,\href{Agda.Builtin.Unit.html#212}{\htmlId{1621}{\htmlClass{InductiveConstructor}{\text{tt}}}}\,          \end{pmatrix}$
    .from (UpdateCommittee m p q)     → $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1511}{\htmlId{1679}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, \\ (\,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1664}{\htmlId{1698}{\htmlClass{Bound}{\text{m}}}}\, , \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1666}{\htmlId{1702}{\htmlClass{Bound}{\text{p}}}}\, , \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1668}{\htmlId{1706}{\htmlClass{Bound}{\text{q}}}}\,) \end{pmatrix}$
    .from (NewConstitution dh s)      → $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1546}{\htmlId{1755}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\, \\ (\,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1740}{\htmlId{1774}{\htmlClass{Bound}{\text{dh}}}}\, , \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1743}{\htmlId{1779}{\htmlClass{Bound}{\text{s}}}}\,)    \end{pmatrix}$
    .from (TriggerHF p)               → $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1581}{\htmlId{1831}{\htmlClass{InductiveConstructor}{\text{TriggerHF}}}}\,       \\ \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1810}{\htmlId{1849}{\htmlClass{Bound}{\text{p}}}}\,           \end{pmatrix}$
    .from (ChangePParams pu)          → $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1616}{\htmlId{1907}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\,   \\ \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1890}{\htmlId{1925}{\htmlClass{Bound}{\text{pu}}}}\,          \end{pmatrix}$
    .from (TreasuryWdrl m)            → $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1651}{\htmlId{1983}{\htmlClass{InductiveConstructor}{\text{TreasuryWdrl}}}}\,    \\ \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1965}{\htmlId{2001}{\htmlClass{Bound}{\text{m}}}}\,           \end{pmatrix}$
    .from Info                        → $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1686}{\htmlId{2059}{\htmlClass{InductiveConstructor}{\text{Info}}}}\, \\ \,\href{Agda.Builtin.Unit.html#212}{\htmlId{2066}{\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'