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#710}{\htmlId{1097}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\,    \\ \,\htmlId{1115}{\htmlClass{Symbol}{\text{\_}}}\,           \end{pmatrix}$ → NoConfidence
    .to $\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#745}{\htmlId{1156}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, \\ (\,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1175}{\htmlId{1175}{\htmlClass{Bound}{\text{m}}}}\, , \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1179}{\htmlId{1179}{\htmlClass{Bound}{\text{p}}}}\, , \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1183}{\htmlId{1183}{\htmlClass{Bound}{\text{q}}}}\,) \end{pmatrix}$ → (UpdateCommittee m p q)
    .to $\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#780}{\htmlId{1226}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\, \\ (\,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1245}{\htmlId{1245}{\htmlClass{Bound}{\text{dh}}}}\, , \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1250}{\htmlId{1250}{\htmlClass{Bound}{\text{s}}}}\, )   \end{pmatrix}$ → (NewConstitution dh s)
    .to $\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#815}{\htmlId{1295}{\htmlClass{InductiveConstructor}{\text{TriggerHF}}}}\,       \\ \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1313}{\htmlId{1313}{\htmlClass{Bound}{\text{p}}}}\,           \end{pmatrix}$ → (TriggerHF p)
    .to $\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#850}{\htmlId{1355}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\,   \\ \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1373}{\htmlId{1373}{\htmlClass{Bound}{\text{pu}}}}\,          \end{pmatrix}$ → (ChangePParams pu)
    .to $\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#885}{\htmlId{1420}{\htmlClass{InductiveConstructor}{\text{TreasuryWdrl}}}}\,    \\ \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1438}{\htmlId{1438}{\htmlClass{Bound}{\text{m}}}}\,           \end{pmatrix}$ → ((TreasuryWdrl m))
    .to $\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#920}{\htmlId{1485}{\htmlClass{InductiveConstructor}{\text{Info}}}}\,            \\ \,\htmlId{1503}{\htmlClass{Symbol}{\text{\_}}}\,           \end{pmatrix}$ → Info
    .from NoConfidence                → $\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#710}{\htmlId{1568}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\,    \\ \,\href{Agda.Builtin.Unit.html#212}{\htmlId{1586}{\htmlClass{InductiveConstructor}{\text{tt}}}}\,          \end{pmatrix}$
    .from (UpdateCommittee m p q)     → $\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#745}{\htmlId{1644}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, \\ (\,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1629}{\htmlId{1663}{\htmlClass{Bound}{\text{m}}}}\, , \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1631}{\htmlId{1667}{\htmlClass{Bound}{\text{p}}}}\, , \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1633}{\htmlId{1671}{\htmlClass{Bound}{\text{q}}}}\,) \end{pmatrix}$
    .from (NewConstitution dh s)      → $\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#780}{\htmlId{1720}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\, \\ (\,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1705}{\htmlId{1739}{\htmlClass{Bound}{\text{dh}}}}\, , \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1708}{\htmlId{1744}{\htmlClass{Bound}{\text{s}}}}\,)    \end{pmatrix}$
    .from (TriggerHF p)               → $\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#815}{\htmlId{1796}{\htmlClass{InductiveConstructor}{\text{TriggerHF}}}}\,       \\ \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1775}{\htmlId{1814}{\htmlClass{Bound}{\text{p}}}}\,           \end{pmatrix}$
    .from (ChangePParams pu)          → $\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#850}{\htmlId{1872}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\,   \\ \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1855}{\htmlId{1890}{\htmlClass{Bound}{\text{pu}}}}\,          \end{pmatrix}$
    .from (TreasuryWdrl m)            → $\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#885}{\htmlId{1948}{\htmlClass{InductiveConstructor}{\text{TreasuryWdrl}}}}\,    \\ \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1930}{\htmlId{1966}{\htmlClass{Bound}{\text{m}}}}\,           \end{pmatrix}$
    .from Info                        → $\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#920}{\htmlId{2024}{\htmlClass{InductiveConstructor}{\text{Info}}}}\, \\ \,\href{Agda.Builtin.Unit.html#212}{\htmlId{2031}{\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'