module Ledger.Conway.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.Conway.Foreign.HSStructures
open import Ledger.Conway.Foreign.PParams
open import Ledger.Core.Foreign.Address
open import Ledger.Conway.Specification.Gov.Base
open import Ledger.Conway.Specification.Gov.Actions govStructure using (Vote) public
open import Ledger.Core.Specification.ProtocolVersion

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  : (RewardAddress ⇀ Treasury)               →  GovAction'
  Info                :                                             GovAction'

instance
  mkGovAction' : Convertible GovAction GovAction'
  mkGovAction' = λ where
    .to $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2500}{\htmlId{1437}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\,        \\ \,\htmlId{1459}{\htmlClass{Symbol}{\text{\_}}}\,           \end{pmatrix}$ → NoConfidence
    .to $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2538}{\htmlId{1500}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\,     \\ \,\htmlId{1522}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Foreign.Gov.Actions.html#1523}{\htmlId{1523}{\htmlClass{Bound}{\text{m}}}}\, , \,\href{Ledger.Conway.Foreign.Gov.Actions.html#1527}{\htmlId{1527}{\htmlClass{Bound}{\text{p}}}}\, , \,\href{Ledger.Conway.Foreign.Gov.Actions.html#1531}{\htmlId{1531}{\htmlClass{Bound}{\text{q}}}}\,\,\htmlId{1532}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ → (UpdateCommittee m p q)
    .to $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2576}{\htmlId{1574}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\,     \\ \,\htmlId{1596}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Foreign.Gov.Actions.html#1597}{\htmlId{1597}{\htmlClass{Bound}{\text{dh}}}}\, , \,\href{Ledger.Conway.Foreign.Gov.Actions.html#1602}{\htmlId{1602}{\htmlClass{Bound}{\text{s}}}}\, \,\htmlId{1604}{\htmlClass{Symbol}{\text{)}}}\,   \end{pmatrix}$ → (NewConstitution dh s)
    .to $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2614}{\htmlId{1647}{\htmlClass{InductiveConstructor}{\text{TriggerHardFork}}}}\,     \\ \,\href{Ledger.Conway.Foreign.Gov.Actions.html#1669}{\htmlId{1669}{\htmlClass{Bound}{\text{p}}}}\,           \end{pmatrix}$ → (TriggerHardFork p)
    .to $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2652}{\htmlId{1717}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\,       \\ \,\href{Ledger.Conway.Foreign.Gov.Actions.html#1739}{\htmlId{1739}{\htmlClass{Bound}{\text{pu}}}}\,          \end{pmatrix}$ → (ChangePParams pu)
    .to $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2690}{\htmlId{1786}{\htmlClass{InductiveConstructor}{\text{TreasuryWithdrawal}}}}\,  \\ \,\href{Ledger.Conway.Foreign.Gov.Actions.html#1808}{\htmlId{1808}{\htmlClass{Bound}{\text{m}}}}\,           \end{pmatrix}$ → ((TreasuryWithdrawal m))
    .to $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2728}{\htmlId{1861}{\htmlClass{InductiveConstructor}{\text{Info}}}}\,                \\ \,\htmlId{1883}{\htmlClass{Symbol}{\text{\_}}}\,           \end{pmatrix}$ → Info
    .from NoConfidence              → $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2500}{\htmlId{1946}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\,        \\ \,\href{Agda.Builtin.Unit.html#212}{\htmlId{1968}{\htmlClass{InductiveConstructor}{\text{tt}}}}\,          \end{pmatrix}$
    .from (UpdateCommittee m p q)   → $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2538}{\htmlId{2024}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\,     \\ \,\htmlId{2046}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Foreign.Gov.Actions.html#2011}{\htmlId{2047}{\htmlClass{Bound}{\text{m}}}}\, , \,\href{Ledger.Conway.Foreign.Gov.Actions.html#2013}{\htmlId{2051}{\htmlClass{Bound}{\text{p}}}}\, , \,\href{Ledger.Conway.Foreign.Gov.Actions.html#2015}{\htmlId{2055}{\htmlClass{Bound}{\text{q}}}}\,\,\htmlId{2056}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$
    .from (NewConstitution dh s)    → $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2576}{\htmlId{2102}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\,     \\ \,\htmlId{2124}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Foreign.Gov.Actions.html#2089}{\htmlId{2125}{\htmlClass{Bound}{\text{dh}}}}\, , \,\href{Ledger.Conway.Foreign.Gov.Actions.html#2092}{\htmlId{2130}{\htmlClass{Bound}{\text{s}}}}\,\,\htmlId{2131}{\htmlClass{Symbol}{\text{)}}}\,    \end{pmatrix}$
    .from (TriggerHardFork p)       → $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2614}{\htmlId{2180}{\htmlClass{InductiveConstructor}{\text{TriggerHardFork}}}}\,     \\ \,\href{Ledger.Conway.Foreign.Gov.Actions.html#2167}{\htmlId{2202}{\htmlClass{Bound}{\text{p}}}}\,           \end{pmatrix}$
    .from (ChangePParams pu)        → $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2652}{\htmlId{2258}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\,       \\ \,\href{Ledger.Conway.Foreign.Gov.Actions.html#2243}{\htmlId{2280}{\htmlClass{Bound}{\text{pu}}}}\,          \end{pmatrix}$
    .from (TreasuryWithdrawal m)    → $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2690}{\htmlId{2336}{\htmlClass{InductiveConstructor}{\text{TreasuryWithdrawal}}}}\,  \\ \,\href{Ledger.Conway.Foreign.Gov.Actions.html#2326}{\htmlId{2358}{\htmlClass{Bound}{\text{m}}}}\,           \end{pmatrix}$
    .from Info                      → $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2728}{\htmlId{2414}{\htmlClass{InductiveConstructor}{\text{Info}}}}\,                \\ \,\href{Agda.Builtin.Unit.html#212}{\htmlId{2436}{\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'