Rename ∅ᵐ → ∅ (#305)

* Rename ∅ᵐ → ∅ Addresses one item of #282 * rename empty set using typeclasses --------- Co-authored-by: Andre Knispel <andre.knispel@gmx.de>
IntersectMBO · Nov 17, 2023 · eafd83a · eafd83a
1 parent cf73110
commit eafd83a
Show file tree

Hide file tree

Showing 12 changed files with 39 additions and 19 deletions.
diff --git a/src/Interface/HasEmptySet.agda b/src/Interface/HasEmptySet.agda
@@ -0,0 +1,21 @@
+{-# OPTIONS --safe #-}
+
+open import Axiom.Set using (Theory)
+
+module Interface.HasEmptySet (th : Theory) where
+
+open Theory th renaming (Set to ℙ_; ∅ to ∅ˢ)
+open import Axiom.Set.Map th
+
+record HasEmptySet (A : Set) : Set where
+  field
+    ∅ : A
+
+instance
+  HasEmptySet-Set : {A : Set} → HasEmptySet (ℙ A)
+  HasEmptySet-Set = record { ∅ = ∅ˢ }
+
+  HasEmptySet-Map : {A B : Set} → HasEmptySet (Map A B)
+  HasEmptySet-Map = record { ∅ = ∅ᵐ }
+
+open HasEmptySet ⦃...⦄ public
diff --git a/src/Ledger/Chain.lagda b/src/Ledger/Chain.lagda
@@ -84,7 +84,7 @@ data _⊢_⇀⦇_,NEWEPOCH⦈_ : NewEpochEnv → NewEpochState → Epoch → New
              ((deposits ∣ ❴ GovActionDeposit gaid ❵) ˢ)
       govActionReturns = aggregate₊ $ mapˢ (λ (a , _ , d) → a , d) removedGovActions ᶠˢ
 
-      es        = record esW { withdrawals = ∅ᵐ }
+      es        = record esW { withdrawals = ∅ }
       retired   = retiring ⁻¹ e
       refunds   = govActionReturns ∪⁺ trWithdrawals ∣ dom rewards
       unclaimed = govActionReturns ∪⁺ trWithdrawals ∣ dom rewards ᶜ
@@ -150,7 +150,7 @@ govActionDeposits : LState → VDeleg ⇀ Coin
 govActionDeposits ls =
   let open LState ls; open CertState certState; open PState pState
       open UTxOState utxoSt; open DState dState
-   in foldl _∪⁺_ ∅ᵐ $ setToList $
+   in foldl _∪⁺_ ∅ $ setToList $
     mapPartial
       (λ where (gaid , record { returnAddr = record {stake = c} }) → do
         vd ← lookupᵐ? voteDelegs c ⦃ _ ∈? _ ⦄
@@ -162,8 +162,8 @@ calculateStakeDistrs : LState → StakeDistrs
 calculateStakeDistrs ls =
   let open LState ls; open CertState certState; open PState pState
       open UTxOState utxoSt; open DState dState
-      spoDelegs = ∅ᵐ -- TODO
-      drepDelegs = ∅ᵐ -- TODO
+      spoDelegs = ∅ -- TODO
+      drepDelegs = ∅ -- TODO
   in
   record
     { stakeDistr = govActionDeposits ls

diff --git a/src/Ledger/Chain/Properties.agda b/src/Ledger/Chain/Properties.agda
@@ -25,7 +25,7 @@ module _ {Γ : NewEpochEnv} {nes : NewEpochState} {e : Epoch} where
   open NewEpochState nes hiding (es)
   open RatifyState fut using (removed) renaming (es to esW)
   open LState ls; open CertState certState; open Acnt acnt
-  es         = record esW { withdrawals = ∅ᵐ }
+  es         = record esW { withdrawals = ∅ }
   govSt'     = filter (λ x → ¿ ¬ proj₁ x ∈ mapˢ proj₁ removed ¿) govSt
 
   NEWEPOCH-total : ∃[ nes' ] Γ ⊢ nes ⇀⦇ e ,NEWEPOCH⦈ nes'

diff --git a/src/Ledger/Deleg.lagda b/src/Ledger/Deleg.lagda
@@ -10,7 +10,7 @@ module Ledger.Deleg (gs : _) (open GovStructure gs) where
 
 open import Ledger.GovernanceActions gs
 \end{code}
-\begin{figure*}[h]
+\begin{figure*}[h!]
 \begin{code}
 record PoolParams : Set where
   field rewardAddr : Credential

diff --git a/src/Ledger/Foreign/HSLedger.agda b/src/Ledger/Foreign/HSLedger.agda
@@ -247,7 +247,7 @@ instance
       ; mint       = ε -- tokenAlgebra only contains ada atm, so mint is surely empty
       ; txfee      = txfee
       ; txvldt     = from txvldt
-      ; txwdrls    = ∅ᵐ
+      ; txwdrls    = ∅
       ; txup       = nothing
       ; txADhash   = nothing
       ; netwrk     = nothing

diff --git a/src/Ledger/Gov.lagda b/src/Ledger/Gov.lagda
@@ -71,8 +71,7 @@ addAction : GovState
           → Epoch → GovActionID → RwdAddr → (a : GovAction) → NeedsHash a
           → GovState
 addAction s e aid addr a prev = s ∷ʳ (aid , record
-  { votes = ∅ᵐ ; returnAddr = addr ; expiresIn = e ; action = a ; prevAction = prev })
-
+  { votes = ∅ ; returnAddr = addr ; expiresIn = e ; action = a ; prevAction = prev })
 \end{code}
 \caption{Types and functions used in the GOV transition system\protect\footnotemark}
 \label{defs:gov-defs}

diff --git a/src/Ledger/GovernanceActions.lagda b/src/Ledger/GovernanceActions.lagda
@@ -305,7 +305,7 @@ data _⊢_⇀⦇_,ENACT⦈_ : EnactEnv → EnactState → GovAction → EnactSta
     ⟦ gid , t , e ⟧ᵉ ⊢   s ⇀⦇ NoConfidence ,ENACT⦈
                  record  s { cc = nothing , gid }
 
-  Enact-NewComm : let old      = maybe proj₁ ∅ᵐ (s .EnactState.cc .proj₁)
+  Enact-NewComm : let old      = maybe proj₁ ∅ (s .EnactState.cc .proj₁)
                       maxTerm  = s .pparams .proj₁ .PParams.ccMaxTermLength +ᵉ e
                   in
     ∀[ term ∈ range new ] term ≤ maxTerm

diff --git a/src/Ledger/NewPP.lagda b/src/Ledger/NewPP.lagda
@@ -25,8 +25,8 @@ record NewPParamState : Set where
 updatePPUp : PParams → PPUpdateState → PPUpdateState
 updatePPUp pparams record { fpup = fpup }
   with allᵇ (isViableUpdate? pparams) (range fpup)
-... | false  = record { pup = ∅ᵐ    ; fpup = ∅ᵐ }
-... | true   = record { pup = fpup  ; fpup = ∅ᵐ }
+... | false  = record { pup = ∅     ; fpup = ∅ }
+... | true   = record { pup = fpup  ; fpup = ∅ }
 
 votedValue : ProposedPPUpdates → PParams → ℕ → Maybe PParamsUpdate
 votedValue pup pparams quorum =

diff --git a/src/Ledger/Prelude.agda b/src/Ledger/Prelude.agda
@@ -34,4 +34,5 @@ open import Tactic.DeriveComp public
 open import Tactic.Premises public
 
 open import Ledger.Interface.HasCoin public
-open import Ledger.Set public
+open import Ledger.Set renaming (∅ to ∅ˢ) public
+open import Interface.HasEmptySet th public
diff --git a/src/Ledger/Ratify.lagda b/src/Ledger/Ratify.lagda
@@ -265,7 +265,7 @@ actualVotes Γ pparams cc ga votes  =   mapKeys (credVoter CC) (actualCCVotes cc
              _                        → Vote.abstain -- expired, no hot key or resigned
 
   actualCCVotes : CCData → Credential ⇀ Vote
-  actualCCVotes nothing          =  ∅ᵐ
+  actualCCVotes nothing          =  ∅
   actualCCVotes (just (cc , q))  =  ifᵈ (ccMinSize ≤ lengthˢ (activeCC $ just (cc , q)))
                                     then mapWithKey actualCCVote cc
                                     else constMap (dom cc) Vote.no

diff --git a/src/Ledger/Transaction.lagda b/src/Ledger/Transaction.lagda
@@ -151,17 +151,14 @@ the transaction body are:
           wits     : TxWitnesses
           -- isValid  : Bool
           txAD     : Maybe AuxiliaryData
-
-\end{code}
-\emph{Abstract functions}
-\begin{code}
 \end{code}
 \end{AgdaSuppressSpace}
 \caption{Definitions used in the UTxO transition system}
 \label{fig:defs:utxo-shelley}
 \end{figure*}
 
 \begin{figure*}[h]
+\emph{Abstract functions}
 \begin{code}
   getValue : TxOut → Value
   getValue (_ , v , _) = v
@@ -187,6 +184,8 @@ the transaction body are:
   isP2Script : Script → Bool
   isP2Script = is-just ∘ isInj₂
 \end{code}
+\caption{Definitions used in the UTxO transition system, continued}
+\label{fig:defs:utxo-shelley-cont}
 \end{figure*}
 \begin{code}[hide]
   instance

diff --git a/src/Ledger/Utxo.lagda b/src/Ledger/Utxo.lagda
@@ -109,7 +109,7 @@ module _ (let open Tx; open TxBody) where
   certDepositᵐ : PParams → DCert → DepositPurpose ⇀ Coin
   certDepositᵐ pp cert = case certDeposit pp cert of λ where
     (just (p , v))  → ❴ p , v ❵ᵐ
-    nothing         → ∅ᵐ
+    nothing         → ∅
 
   propDepositᵐ : PParams → GovActionID → GovProposal → DepositPurpose ⇀ Coin
   propDepositᵐ pp gaid record { returnAddr = record { stake = c } }