module Ledger.Dijkstra.Foreign.Gov.Actions where

open import Data.Rational using (ℚ)
open import Class.Convertible
open import Class.Convertible.Foreign
open import Tactic.Derive.Convertible
open import Class.HasHsType
open import Class.HasHsType.Foreign
open import Tactic.Derive.HsType

open import Ledger.Prelude
open import Ledger.Prelude.Foreign.HSTypes

open import Ledger.Dijkstra.Foreign.HSStructures
open import Ledger.Dijkstra.Foreign.PParams
open import Ledger.Core.Foreign.Address
open import Ledger.Core.Specification.ProtocolVersion

-- nondependent version of GovAction
data GovAction' : Type where
  NoConfidence        :                                             GovAction'
  UpdateCommittee     : (Credential ⇀ Epoch) → ℙ Credential → ℚ  →  GovAction'
  NewConstitution     : ADHash → Maybe ScriptHash               →  GovAction'
  TriggerHardFork     : ProtVer                                  →  GovAction'
  ChangePParams       : PParamsUpdate                            →  GovAction'
  TreasuryWithdrawal  : (RewardAddress ⇀ Treasury)               →  GovAction'
  Info                :                                             GovAction'

instance
  mkGovAction' : Convertible GovAction GovAction'
  mkGovAction' = λ where
    .to $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1049}{\htmlId{1263}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\,        \\ \,\htmlId{1285}{\htmlClass{Symbol}{\text{\_}}}\,           \end{pmatrix}$ → NoConfidence
    .to $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1087}{\htmlId{1326}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\,     \\ \,\htmlId{1348}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Foreign.Gov.Actions.html#1349}{\htmlId{1349}{\htmlClass{Bound}{\text{m}}}}\, , \,\href{Ledger.Dijkstra.Foreign.Gov.Actions.html#1353}{\htmlId{1353}{\htmlClass{Bound}{\text{s}}}}\, , \,\href{Ledger.Dijkstra.Foreign.Gov.Actions.html#1357}{\htmlId{1357}{\htmlClass{Bound}{\text{q}}}}\,\,\htmlId{1358}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ → UpdateCommittee m s q
    .to $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1125}{\htmlId{1398}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\,     \\ \,\htmlId{1420}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Foreign.Gov.Actions.html#1421}{\htmlId{1421}{\htmlClass{Bound}{\text{h}}}}\, , \,\href{Ledger.Dijkstra.Foreign.Gov.Actions.html#1425}{\htmlId{1425}{\htmlClass{Bound}{\text{s}}}}\,\,\htmlId{1426}{\htmlClass{Symbol}{\text{)}}}\,     \end{pmatrix}$ → NewConstitution h s
    .to $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1163}{\htmlId{1468}{\htmlClass{InductiveConstructor}{\text{TriggerHardFork}}}}\,     \\ \,\href{Ledger.Dijkstra.Foreign.Gov.Actions.html#1490}{\htmlId{1490}{\htmlClass{Bound}{\text{v}}}}\,           \end{pmatrix}$ → TriggerHardFork v
    .to $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1201}{\htmlId{1536}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\,       \\ \,\href{Ledger.Dijkstra.Foreign.Gov.Actions.html#1558}{\htmlId{1558}{\htmlClass{Bound}{\text{u}}}}\,           \end{pmatrix}$ → ChangePParams u
    .to $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1239}{\htmlId{1602}{\htmlClass{InductiveConstructor}{\text{TreasuryWithdrawal}}}}\,  \\ \,\href{Ledger.Dijkstra.Foreign.Gov.Actions.html#1624}{\htmlId{1624}{\htmlClass{Bound}{\text{w}}}}\,           \end{pmatrix}$ → TreasuryWithdrawal w
    .to $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1277}{\htmlId{1673}{\htmlClass{InductiveConstructor}{\text{Info}}}}\,                \\ \,\htmlId{1695}{\htmlClass{Symbol}{\text{\_}}}\,           \end{pmatrix}$ → Info
    .from NoConfidence              → $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1049}{\htmlId{1758}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\,        \\ \,\href{Agda.Builtin.Unit.html#212}{\htmlId{1780}{\htmlClass{InductiveConstructor}{\text{tt}}}}\,          \end{pmatrix}$
    .from (UpdateCommittee m s q)   → $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1087}{\htmlId{1836}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\,     \\ \,\htmlId{1858}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Foreign.Gov.Actions.html#1823}{\htmlId{1859}{\htmlClass{Bound}{\text{m}}}}\, , \,\href{Ledger.Dijkstra.Foreign.Gov.Actions.html#1825}{\htmlId{1863}{\htmlClass{Bound}{\text{s}}}}\, , \,\href{Ledger.Dijkstra.Foreign.Gov.Actions.html#1827}{\htmlId{1867}{\htmlClass{Bound}{\text{q}}}}\,\,\htmlId{1868}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$
    .from (NewConstitution h s)     → $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1125}{\htmlId{1914}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\,     \\ \,\htmlId{1936}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Foreign.Gov.Actions.html#1901}{\htmlId{1937}{\htmlClass{Bound}{\text{h}}}}\, , \,\href{Ledger.Dijkstra.Foreign.Gov.Actions.html#1903}{\htmlId{1941}{\htmlClass{Bound}{\text{s}}}}\,\,\htmlId{1942}{\htmlClass{Symbol}{\text{)}}}\,     \end{pmatrix}$
    .from (TriggerHardFork v)       → $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1163}{\htmlId{1992}{\htmlClass{InductiveConstructor}{\text{TriggerHardFork}}}}\,     \\ \,\href{Ledger.Dijkstra.Foreign.Gov.Actions.html#1979}{\htmlId{2014}{\htmlClass{Bound}{\text{v}}}}\,           \end{pmatrix}$
    .from (ChangePParams u)         → $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1201}{\htmlId{2070}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\,       \\ \,\href{Ledger.Dijkstra.Foreign.Gov.Actions.html#2055}{\htmlId{2092}{\htmlClass{Bound}{\text{u}}}}\,           \end{pmatrix}$
    .from (TreasuryWithdrawal w)    → $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1239}{\htmlId{2148}{\htmlClass{InductiveConstructor}{\text{TreasuryWithdrawal}}}}\,  \\ \,\href{Ledger.Dijkstra.Foreign.Gov.Actions.html#2138}{\htmlId{2170}{\htmlClass{Bound}{\text{w}}}}\,           \end{pmatrix}$
    .from Info                      → $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1277}{\htmlId{2226}{\htmlClass{InductiveConstructor}{\text{Info}}}}\,                \\ \,\href{Agda.Builtin.Unit.html#212}{\htmlId{2248}{\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'