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#738}{\htmlId{1124}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\,    \\ \,\htmlId{1142}{\htmlClass{Symbol}{\text{\_}}}\,           \end{pmatrix}$ → NoConfidence
    .to $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#773}{\htmlId{1183}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, \\ (\,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1202}{\htmlId{1202}{\htmlClass{Bound}{\text{m}}}}\, , \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1206}{\htmlId{1206}{\htmlClass{Bound}{\text{p}}}}\, , \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1210}{\htmlId{1210}{\htmlClass{Bound}{\text{q}}}}\,) \end{pmatrix}$ → (UpdateCommittee m p q)
    .to $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#808}{\htmlId{1253}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\, \\ (\,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1272}{\htmlId{1272}{\htmlClass{Bound}{\text{dh}}}}\, , \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1277}{\htmlId{1277}{\htmlClass{Bound}{\text{s}}}}\, )   \end{pmatrix}$ → (NewConstitution dh s)
    .to $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#843}{\htmlId{1322}{\htmlClass{InductiveConstructor}{\text{TriggerHF}}}}\,       \\ \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1340}{\htmlId{1340}{\htmlClass{Bound}{\text{p}}}}\,           \end{pmatrix}$ → (TriggerHF p)
    .to $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#878}{\htmlId{1382}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\,   \\ \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1400}{\htmlId{1400}{\htmlClass{Bound}{\text{pu}}}}\,          \end{pmatrix}$ → (ChangePParams pu)
    .to $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#913}{\htmlId{1447}{\htmlClass{InductiveConstructor}{\text{TreasuryWdrl}}}}\,    \\ \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1465}{\htmlId{1465}{\htmlClass{Bound}{\text{m}}}}\,           \end{pmatrix}$ → ((TreasuryWdrl m))
    .to $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#948}{\htmlId{1512}{\htmlClass{InductiveConstructor}{\text{Info}}}}\,            \\ \,\htmlId{1530}{\htmlClass{Symbol}{\text{\_}}}\,           \end{pmatrix}$ → Info
    .from NoConfidence                → $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#738}{\htmlId{1595}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\,    \\ \,\href{Agda.Builtin.Unit.html#212}{\htmlId{1613}{\htmlClass{InductiveConstructor}{\text{tt}}}}\,          \end{pmatrix}$
    .from (UpdateCommittee m p q)     → $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#773}{\htmlId{1671}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, \\ (\,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1656}{\htmlId{1690}{\htmlClass{Bound}{\text{m}}}}\, , \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1658}{\htmlId{1694}{\htmlClass{Bound}{\text{p}}}}\, , \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1660}{\htmlId{1698}{\htmlClass{Bound}{\text{q}}}}\,) \end{pmatrix}$
    .from (NewConstitution dh s)      → $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#808}{\htmlId{1747}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\, \\ (\,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1732}{\htmlId{1766}{\htmlClass{Bound}{\text{dh}}}}\, , \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1735}{\htmlId{1771}{\htmlClass{Bound}{\text{s}}}}\,)    \end{pmatrix}$
    .from (TriggerHF p)               → $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#843}{\htmlId{1823}{\htmlClass{InductiveConstructor}{\text{TriggerHF}}}}\,       \\ \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1802}{\htmlId{1841}{\htmlClass{Bound}{\text{p}}}}\,           \end{pmatrix}$
    .from (ChangePParams pu)          → $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#878}{\htmlId{1899}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\,   \\ \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1882}{\htmlId{1917}{\htmlClass{Bound}{\text{pu}}}}\,          \end{pmatrix}$
    .from (TreasuryWdrl m)            → $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#913}{\htmlId{1975}{\htmlClass{InductiveConstructor}{\text{TreasuryWdrl}}}}\,    \\ \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1957}{\htmlId{1993}{\htmlClass{Bound}{\text{m}}}}\,           \end{pmatrix}$
    .from Info                        → $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#948}{\htmlId{2051}{\htmlClass{InductiveConstructor}{\text{Info}}}}\, \\ \,\href{Agda.Builtin.Unit.html#212}{\htmlId{2058}{\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'