Remove constructor from Acnt

IntersectMBO · Jan 31, 2025 · 675be19 · 675be19
1 parent 219777a
commit 675be19
Show file tree

Hide file tree

Showing 3 changed files with 13 additions and 5 deletions.
diff --git a/src/Ledger/Conway/Conformance/Epoch.agda b/src/Ledger/Conway/Conformance/Epoch.agda
@@ -95,7 +95,7 @@ open GovActionState using (returnAddr)
 
 applyRUpd : RewardUpdate → EpochState → EpochState
 applyRUpd ⟦ Δt , Δr , Δf , rs ⟧ʳᵘ
-  ⟦ ⟦ treasury , reserves ⟧ᵃ
+  ⟦ acnt
   , ss
   , ⟦ utxoSt
     , govSt
@@ -104,14 +104,15 @@ applyRUpd ⟦ Δt , Δr , Δf , rs ⟧ʳᵘ
   , fut
   ⟧ᵉ' =
   ⟦ ⟦ posPart (ℤ.+ treasury ℤ.+ Δt ℤ.+ ℤ.+ unregRU')
-    , posPart (ℤ.+ reserves ℤ.+ Δr) ⟧ᵃ
+    , posPart (ℤ.+ reserves ℤ.+ Δr) ⟧
   , ss
   , ⟦ ⟦ utxo , posPart (ℤ.+ fees ℤ.+ Δf) , deposits , donations ⟧
     , govSt
     , ⟦ ⟦ voteDelegs , stakeDelegs , rewards ∪⁺ regRU , dDeposits ⟧ᵈ , pState , gState ⟧ᶜˢ ⟧ˡ
   , es
   , fut ⟧ᵉ'
   where
+    open Acnt acnt
     open UTxOState utxoSt
     regRU     = rs ∣ dom rewards
     unregRU   = rs ∣ dom rewards ᶜ

diff --git a/src/Ledger/Epoch.lagda b/src/Ledger/Epoch.lagda
@@ -124,7 +124,7 @@ open GovActionState using (returnAddr)
 \begin{code}
 applyRUpd : RewardUpdate → EpochState → EpochState
 applyRUpd ⟦ Δt , Δr , Δf , rs ⟧ʳᵘ
-  ⟦ ⟦ treasury , reserves ⟧ᵃ
+  ⟦ acnt
   , ss
   , ⟦ utxoSt 
     , govSt
@@ -133,14 +133,15 @@ applyRUpd ⟦ Δt , Δr , Δf , rs ⟧ʳᵘ
   , fut
   ⟧ᵉ' =
   ⟦ ⟦ posPart (ℤ.+ treasury ℤ.+ Δt ℤ.+ ℤ.+ unregRU')
-    , posPart (ℤ.+ reserves ℤ.+ Δr) ⟧ᵃ
+    , posPart (ℤ.+ reserves ℤ.+ Δr) ⟧
   , ss
   , ⟦ ⟦ utxo , posPart (ℤ.+ fees ℤ.+ Δf) , deposits , donations ⟧
     , govSt
     , ⟦ ⟦ voteDelegs , stakeDelegs , rewards ∪⁺ regRU ⟧ , pState , gState ⟧ᶜˢ ⟧ˡ
   , es
   , fut ⟧ᵉ'
   where
+    open Acnt acnt
     open UTxOState utxoSt
     open DState stᵈ
     regRU     = rs ∣ dom rewards

diff --git a/src/Ledger/PParams.lagda b/src/Ledger/PParams.lagda
@@ -12,6 +12,8 @@ open import Data.Rational using (ℚ)
 open import Relation.Nullary.Decidable
 open import Data.List.Relation.Unary.Any using (Any; here; there)
 
+open import Data.Product.Nary.NonDependent using (uncurryₙ)
+
 open import Tactic.Derive.DecEq
 open import Tactic.Derive.Show
 
@@ -41,7 +43,6 @@ remain in treasury and reserves.
 record Acnt : Type where
 \end{code}
 \begin{code}[hide]
-  constructor ⟦_,_⟧ᵃ
   field
 \end{code}
 \begin{code}
@@ -63,6 +64,11 @@ data pvCanFollow : ProtVer → ProtVer → Type where
 \label{fig:protocol-parameter-defs}
 \end{figure*}
 \end{NoConway}
+\begin{code}[hide]
+instance
+  ToRecord-Acnt : ToRecord (Coin × Coin) Acnt
+  ToRecord-Acnt = record { ⟦_⟧ = uncurryₙ 2 (λ z z₁ → record { treasury = z ; reserves = z₁ }) }
+\end{code}
 
 \begin{figure*}[ht]
 \begin{AgdaMultiCode}