{-# OPTIONS --safe #-}

open import Data.Nat.Properties using (+-0-monoid)
open import Data.Rational using (ℚ; 0ℚ; 1ℚ)

open import Tactic.Derive.DecEq
open import Tactic.Derive.Show

open import Ledger.Prelude hiding (yes; no)
open import Ledger.Types.GovStructure

module Ledger.GovernanceActions (gs : _) (open GovStructure gs) where


data GovRole : Type where
  CC DRep SPO : GovRole

Voter        = GovRole × Credential
GovActionID  = TxId × ℕ

data VDeleg : Type where
  credVoter        : GovRole → Credential →  VDeleg
  abstainRep       :                         VDeleg
  noConfidenceRep  :                         VDeleg

record Anchor : Type where
  field
    url   : String
    hash  : DocHash

data GovActionType : Type where
  NoConfidence     : GovActionType
  UpdateCommittee  : GovActionType
  NewConstitution  : GovActionType
  TriggerHF        : GovActionType
  ChangePParams    : GovActionType
  TreasuryWdrl     : GovActionType
  Info             : GovActionType

GovActionData : GovActionType → Type
GovActionData NoConfidence     = ⊤
GovActionData UpdateCommittee  = (Credential ⇀ Epoch) × ℙ Credential × ℚ
GovActionData NewConstitution  = DocHash × Maybe ScriptHash
GovActionData TriggerHF        = ProtVer
GovActionData ChangePParams    = PParamsUpdate
GovActionData TreasuryWdrl     = RwdAddr ⇀ Coin
GovActionData Info             = ⊤

record GovAction : Type where
  constructor ⟦_,_⟧ᵍᵃ
  field
    gaType : GovActionType
    gaData : GovActionData gaType

open GovAction public


NeedsHash : GovActionType → Type
NeedsHash NoConfidence     = GovActionID
NeedsHash UpdateCommittee  = GovActionID
NeedsHash NewConstitution  = GovActionID
NeedsHash TriggerHF        = GovActionID
NeedsHash ChangePParams    = GovActionID
NeedsHash TreasuryWdrl     = ⊤
NeedsHash Info             = ⊤

HashProtected : Type → Type
HashProtected A = A × GovActionID


data Vote : Type where
  yes no abstain  : Vote

record GovVote : Type where
  field
    gid         : GovActionID
    voter       : Voter
    vote        : Vote
    anchor      : Maybe Anchor

record GovProposal : Type where
  field
    action      : GovAction
    prevAction  : NeedsHash (gaType action)
    policy      : Maybe ScriptHash
    deposit     : Coin
    returnAddr  : RwdAddr
    anchor      : Anchor

record GovActionState : Type where
  field
    votes       : Voter ⇀ Vote
    returnAddr  : RwdAddr
    expiresIn   : Epoch
    action      : GovAction
    prevAction  : NeedsHash (gaType action)


instance
  unquoteDecl DecEq-GovActionType = derive-DecEq ((quote GovActionType , DecEq-GovActionType) ∷ [])
  unquoteDecl DecEq-GovRole       = derive-DecEq ((quote GovRole , DecEq-GovRole) ∷ [])
  unquoteDecl DecEq-Vote          = derive-DecEq ((quote Vote    , DecEq-Vote)    ∷ [])
  unquoteDecl DecEq-VDeleg        = derive-DecEq ((quote VDeleg  , DecEq-VDeleg)  ∷ [])

  unquoteDecl To-GovVote = derive-To [ (quote GovVote     , To-GovVote) ]


getDRepVote : GovVote → Maybe Credential
getDRepVote record { voter = (DRep , credential) }  = just credential
getDRepVote _                                       = nothing

proposedCC : GovAction → ℙ Credential
proposedCC ⟦ UpdateCommittee , (x , _ , _) ⟧ᵍᵃ  = dom x
proposedCC _                                    = ∅