diff --git a/src/Ledger/Foreign/HSLedger.agda b/src/Ledger/Foreign/HSLedger.agda index 3f3b6b9e7..502c99164 100644 --- a/src/Ledger/Foreign/HSLedger.agda +++ b/src/Ledger/Foreign/HSLedger.agda @@ -238,10 +238,10 @@ instance Convertible-VDeleg : Convertible VDeleg F.VDeleg Convertible-VDeleg = λ where - .to (credVoter x x₁) → F.CredVoter (to x) (to x₁) + .to (credVoter (x , x₁)) → F.CredVoter (to x) (to x₁) .to abstainRep → F.AbstainRep .to noConfidenceRep → F.NoConfidenceRep - .from (F.CredVoter x x₁) → VDeleg.credVoter (from x) (from x₁) + .from (F.CredVoter x x₁) → VDeleg.credVoter (from x , from x₁) .from F.AbstainRep → VDeleg.abstainRep .from F.NoConfidenceRep → VDeleg.noConfidenceRep diff --git a/src/Ledger/GovernanceActions.lagda b/src/Ledger/GovernanceActions.lagda index 0e50ac2f3..4f2aeb9d7 100644 --- a/src/Ledger/GovernanceActions.lagda +++ b/src/Ledger/GovernanceActions.lagda @@ -35,7 +35,7 @@ Voter = GovRole × Credential GovActionID = TxId × ℕ data VDeleg : Set where - credVoter : GovRole → Credential → VDeleg + credVoter : (GovRole × Credential) → VDeleg abstainRep : VDeleg noConfidenceRep : VDeleg diff --git a/src/Ledger/Ratify.lagda b/src/Ledger/Ratify.lagda index 830b1286d..10098c98e 100644 --- a/src/Ledger/Ratify.lagda +++ b/src/Ledger/Ratify.lagda @@ -191,7 +191,7 @@ CCData : Set CCData = Maybe ((Credential ⇀ Epoch) × ℚ) govRole : VDeleg → GovRole -govRole (credVoter gv _) = gv +govRole (credVoter (gv , _)) = gv govRole abstainRep = DRep govRole noConfidenceRep = DRep @@ -291,14 +291,14 @@ restrictedDists coins rank dists = dists actualVotes : RatifyEnv → PParams → CCData → GovAction → (GovRole × Credential ⇀ Vote) → (VDeleg ⇀ Vote) actualVotes Γ pparams cc ga votes - = mapKeys (credVoter CC) (actualCCVotes cc) ∪ˡ actualPDRepVotes ga + = mapKeys (λ x → (credVoter (CC , x))) (actualCCVotes cc) ∪ˡ actualPDRepVotes ga ∪ˡ actualDRepVotes ∪ˡ actualSPOVotes ga where open RatifyEnv Γ open PParams pparams roleVotes : GovRole → VDeleg ⇀ Vote - roleVotes r = mapKeys (uncurry credVoter) (filterᵐ (λ (x , _) → r ≡ proj₁ x) votes) + roleVotes r = mapKeys credVoter (filterᵐ (λ (x , _) → r ≡ proj₁ x) votes) activeDReps = dom (filterᵐ (λ (_ , e) → currentEpoch ≤ e) dreps) spos = filterˢ IsSPO (dom (stakeDistr stakeDistrs)) @@ -325,7 +325,7 @@ actualVotes Γ pparams cc ga votes actualDRepVotes : VDeleg ⇀ Vote actualDRepVotes = roleVotes DRep - ∪ˡ constMap (mapˢ (credVoter DRep) activeDReps) Vote.no + ∪ˡ constMap (mapˢ (λ x → (credVoter (DRep , x))) activeDReps) Vote.no actualSPOVotes : GovAction → VDeleg ⇀ Vote actualSPOVotes (TriggerHF _) = roleVotes SPO ∪ˡ constMap spos Vote.no