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  : (RwdAddr  Treasury)                       GovAction'
  Info                :                                             GovAction'

instance
  mkGovAction' : Convertible GovAction GovAction'
  mkGovAction' = λ where
    .to $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#809}{\htmlId{1145}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\,        \\ \,\htmlId{1167}{\htmlClass{Symbol}{\text{\_}}}\,           \end{pmatrix}$  NoConfidence
    .to $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#847}{\htmlId{1208}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\,     \\ \,\htmlId{1230}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1231}{\htmlId{1231}{\htmlClass{Bound}{\text{m}}}}\, , \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1235}{\htmlId{1235}{\htmlClass{Bound}{\text{p}}}}\, , \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1239}{\htmlId{1239}{\htmlClass{Bound}{\text{q}}}}\,\,\htmlId{1240}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$  (UpdateCommittee m p q)
    .to $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#885}{\htmlId{1282}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\,     \\ \,\htmlId{1304}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1305}{\htmlId{1305}{\htmlClass{Bound}{\text{dh}}}}\, , \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1310}{\htmlId{1310}{\htmlClass{Bound}{\text{s}}}}\, \,\htmlId{1312}{\htmlClass{Symbol}{\text{)}}}\,   \end{pmatrix}$  (NewConstitution dh s)
    .to $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#923}{\htmlId{1355}{\htmlClass{InductiveConstructor}{\text{TriggerHardFork}}}}\,     \\ \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1377}{\htmlId{1377}{\htmlClass{Bound}{\text{p}}}}\,           \end{pmatrix}$  (TriggerHardFork p)
    .to $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#961}{\htmlId{1425}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\,       \\ \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1447}{\htmlId{1447}{\htmlClass{Bound}{\text{pu}}}}\,          \end{pmatrix}$  (ChangePParams pu)
    .to $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#999}{\htmlId{1494}{\htmlClass{InductiveConstructor}{\text{TreasuryWithdrawal}}}}\,  \\ \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1516}{\htmlId{1516}{\htmlClass{Bound}{\text{m}}}}\,           \end{pmatrix}$  ((TreasuryWithdrawal m))
    .to $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1037}{\htmlId{1569}{\htmlClass{InductiveConstructor}{\text{Info}}}}\,                \\ \,\htmlId{1591}{\htmlClass{Symbol}{\text{\_}}}\,           \end{pmatrix}$  Info
    .from NoConfidence               $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#809}{\htmlId{1654}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\,        \\ \,\href{Agda.Builtin.Unit.html#212}{\htmlId{1676}{\htmlClass{InductiveConstructor}{\text{tt}}}}\,          \end{pmatrix}$
    .from (UpdateCommittee m p q)    $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#847}{\htmlId{1732}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\,     \\ \,\htmlId{1754}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1719}{\htmlId{1755}{\htmlClass{Bound}{\text{m}}}}\, , \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1721}{\htmlId{1759}{\htmlClass{Bound}{\text{p}}}}\, , \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1723}{\htmlId{1763}{\htmlClass{Bound}{\text{q}}}}\,\,\htmlId{1764}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$
    .from (NewConstitution dh s)     $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#885}{\htmlId{1810}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\,     \\ \,\htmlId{1832}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1797}{\htmlId{1833}{\htmlClass{Bound}{\text{dh}}}}\, , \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1800}{\htmlId{1838}{\htmlClass{Bound}{\text{s}}}}\,\,\htmlId{1839}{\htmlClass{Symbol}{\text{)}}}\,    \end{pmatrix}$
    .from (TriggerHardFork p)        $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#923}{\htmlId{1888}{\htmlClass{InductiveConstructor}{\text{TriggerHardFork}}}}\,     \\ \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1875}{\htmlId{1910}{\htmlClass{Bound}{\text{p}}}}\,           \end{pmatrix}$
    .from (ChangePParams pu)         $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#961}{\htmlId{1966}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\,       \\ \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1951}{\htmlId{1988}{\htmlClass{Bound}{\text{pu}}}}\,          \end{pmatrix}$
    .from (TreasuryWithdrawal m)     $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#999}{\htmlId{2044}{\htmlClass{InductiveConstructor}{\text{TreasuryWithdrawal}}}}\,  \\ \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#2034}{\htmlId{2066}{\htmlClass{Bound}{\text{m}}}}\,           \end{pmatrix}$
    .from Info                       $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1037}{\htmlId{2122}{\htmlClass{InductiveConstructor}{\text{Info}}}}\,                \\ \,\href{Agda.Builtin.Unit.html#212}{\htmlId{2144}{\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'