Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

PDF cleanup 282: remove uncurry from code appearing in pdf #358

Draft
wants to merge 1 commit into
base: master
Choose a base branch
from
Draft

PDF cleanup 282: remove uncurry from code appearing in pdf #358

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
4 changes: 2 additions & 2 deletions src/Ledger/Foreign/HSLedger.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
2 changes: 1 addition & 1 deletion src/Ledger/GovernanceActions.lagda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
8 changes: 4 additions & 4 deletions src/Ledger/Ratify.lagda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down Expand Up @@ -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))
Expand All @@ -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
Expand Down