From c5255d0c28ca39b3233f4ade7c21a0a96b7a5b69 Mon Sep 17 00:00:00 2001
From: Jacques Carette <carette@mcmaster.ca>
Date: Thu, 16 May 2024 02:06:00 -0400
Subject: [PATCH] Algebra fixity (#2386)

* put the fixity recommendations into the style guide

* mixing fixity declaration

* was missing a case

* use the new case

* add fixities for everything in Algebra

* incorporate some suggestions for extra cases
---
 doc/README/Design/Fixity.agda                 |  1 +
 doc/style-guide.md                            | 60 +++++++++++++++++++
 src/Algebra/Bundles.agda                      |  1 +
 src/Algebra/Definitions.agda                  |  4 ++
 src/Algebra/Definitions/RawMagma.agda         |  2 +-
 src/Algebra/Module/Bundles.agda               |  1 +
 src/Algebra/Module/Definitions/Left.agda      |  2 +
 src/Algebra/Module/Definitions/Right.agda     |  2 +
 .../Properties/Monoid/Divisibility.agda       |  2 +
 .../Properties/Semiring/Divisibility.agda     |  2 +
 .../Solver/Ring/AlmostCommutativeRing.agda    |  2 +
 11 files changed, 78 insertions(+), 1 deletion(-)

diff --git a/doc/README/Design/Fixity.agda b/doc/README/Design/Fixity.agda
index 85153c1ec4..52394ff864 100644
--- a/doc/README/Design/Fixity.agda
+++ b/doc/README/Design/Fixity.agda
@@ -34,3 +34,4 @@ module README.Design.Fixity where
 -- type formers:
 -- product-like infixr 2 _×_ _-×-_ _-,-_
 -- sum-like infixr 1 _⊎_
+-- binary properties infix 4 _Absorbs_
diff --git a/doc/style-guide.md b/doc/style-guide.md
index 254a7ec071..2562f76cfd 100644
--- a/doc/style-guide.md
+++ b/doc/style-guide.md
@@ -525,6 +525,66 @@ word within a compound word is capitalized except for the first word.
 * Any exceptions to these conventions should be flagged on the GitHub
   `agda-stdlib` issue tracker in the usual way.
 
+#### Fixity
+
+All functions and operators that are not purely prefix (typically
+anything that has a `_` in its name) should have an explicit fixity
+declared for it. The guidelines for these are as follows:
+
+General operations and relations:
+
+* binary relations of all kinds are `infix 4`
+
+* unary prefix relations `infix 4 ε∣_`
+
+* unary postfix relations `infixr 8 _∣0`
+
+* multiplication-like: `infixl 7 _*_`
+
+* addition-like  `infixl 6 _+_`
+
+* arithmetic prefix minus-like  `infix  8 -_`
+
+* arithmetic infix binary minus-like `infixl 6 _-_`
+
+* and-like  `infixr 7 _∧_`
+
+* or-like  `infixr 6 _∨_`
+
+* negation-like `infix 3 ¬_`
+
+* post-fix inverse  `infix  8 _⁻¹`
+
+* bind `infixl 1 _>>=_`
+
+* list concat-like `infixr 5 _∷_`
+
+* ternary reasoning `infix 1 _⊢_≈_`
+
+* composition `infixr 9 _∘_`
+
+* application `infixr -1 _$_ _$!_`
+
+* combinatorics `infixl 6.5 _P_ _P′_ _C_ _C′_`
+
+* pair `infixr 4 _,_`
+
+Reasoning:
+
+* QED  `infix  3 _∎`
+
+* stepping  `infixr 2 _≡⟨⟩_ step-≡ step-≡˘`
+
+* begin  `infix  1 begin_`
+
+Type formers:
+
+* product-like `infixr 2 _×_ _-×-_ _-,-_`
+
+* sum-like `infixr 1 _⊎_`
+
+*  binary properties `infix 4 _Absorbs_`
+
 #### Functions and relations over specific datatypes
 
 * When defining a new relation `P` over a datatype `X` in a `Data.X.Relation` module,
diff --git a/src/Algebra/Bundles.agda b/src/Algebra/Bundles.agda
index 1969731c2c..a86529f5cd 100644
--- a/src/Algebra/Bundles.agda
+++ b/src/Algebra/Bundles.agda
@@ -917,6 +917,7 @@ record NonAssociativeRing c ℓ : Set (suc (c ⊔ ℓ)) where
     using () renaming (magma to *-magma; identity to *-identity)
 
 record Nearring c ℓ : Set (suc (c ⊔ ℓ)) where
+  infix  8 -_
   infixl 7 _*_
   infixl 6 _+_
   infix  4 _≈_
diff --git a/src/Algebra/Definitions.agda b/src/Algebra/Definitions.agda
index ae0566a4bf..62528e5b70 100644
--- a/src/Algebra/Definitions.agda
+++ b/src/Algebra/Definitions.agda
@@ -97,6 +97,8 @@ RightConical e _∙_ = ∀ x y → (x ∙ y) ≈ e → y ≈ e
 Conical : A → Op₂ A → Set _
 Conical e ∙ = (LeftConical e ∙) × (RightConical e ∙)
 
+infix 4 _DistributesOverˡ_ _DistributesOverʳ_ _DistributesOver_
+
 _DistributesOverˡ_ : Op₂ A → Op₂ A → Set _
 _*_ DistributesOverˡ _+_ =
   ∀ x y z → (x * (y + z)) ≈ ((x * y) + (x * z))
@@ -108,6 +110,8 @@ _*_ DistributesOverʳ _+_ =
 _DistributesOver_ : Op₂ A → Op₂ A → Set _
 * DistributesOver + = (* DistributesOverˡ +) × (* DistributesOverʳ +)
 
+infix 4 _MiddleFourExchange_ _IdempotentOn_ _Absorbs_
+
 _MiddleFourExchange_ : Op₂ A → Op₂ A → Set _
 _*_ MiddleFourExchange _+_ =
   ∀ w x y z → ((w + x) * (y + z)) ≈ ((w + y) * (x + z))
diff --git a/src/Algebra/Definitions/RawMagma.agda b/src/Algebra/Definitions/RawMagma.agda
index 2e1bc657c7..b8591e7ad2 100644
--- a/src/Algebra/Definitions/RawMagma.agda
+++ b/src/Algebra/Definitions/RawMagma.agda
@@ -25,7 +25,7 @@ open RawMagma M renaming (Carrier to A)
 ------------------------------------------------------------------------
 -- Divisibility
 
-infix 5 _∣ˡ_ _∤ˡ_ _∣ʳ_ _∤ʳ_ _∣_ _∤_
+infix 5 _∣ˡ_ _∤ˡ_ _∣ʳ_ _∤ʳ_ _∣_ _∤_ _∣∣_ _∤∤_
 
 -- Divisibility from the left.
 --
diff --git a/src/Algebra/Module/Bundles.agda b/src/Algebra/Module/Bundles.agda
index 33e6bfa731..5df96258d6 100644
--- a/src/Algebra/Module/Bundles.agda
+++ b/src/Algebra/Module/Bundles.agda
@@ -279,6 +279,7 @@ record Bimodule (R-ring : Ring r ℓr) (S-ring : Ring s ℓs) m ℓm
     module R = Ring R-ring
     module S = Ring S-ring
 
+  infix 8 -ᴹ_
   infixr 7 _*ₗ_
   infixl 7 _*ᵣ_
   infixl 6 _+ᴹ_
diff --git a/src/Algebra/Module/Definitions/Left.agda b/src/Algebra/Module/Definitions/Left.agda
index e8aa153507..0bb7d530c3 100644
--- a/src/Algebra/Module/Definitions/Left.agda
+++ b/src/Algebra/Module/Definitions/Left.agda
@@ -31,6 +31,8 @@ LeftIdentity a _∙ᴮ_ = ∀ m → (a ∙ᴮ m) ≈ m
 Associative : Op₂ A → Opₗ A B → Set _
 Associative _∙ᴬ_ _∙ᴮ_ = ∀ x y m → ((x ∙ᴬ y) ∙ᴮ m) ≈ (x ∙ᴮ (y ∙ᴮ m))
 
+infix 4 _DistributesOverˡ_ _DistributesOverʳ_⟶_
+
 _DistributesOverˡ_ : Opₗ A B → Op₂ B → Set _
 _*_ DistributesOverˡ _+_ =
   ∀ x m n → (x * (m + n)) ≈ ((x * m) + (x * n))
diff --git a/src/Algebra/Module/Definitions/Right.agda b/src/Algebra/Module/Definitions/Right.agda
index d1a7a878ea..a023b09e52 100644
--- a/src/Algebra/Module/Definitions/Right.agda
+++ b/src/Algebra/Module/Definitions/Right.agda
@@ -31,6 +31,8 @@ RightIdentity a _∙ᴮ_ = ∀ m → (m ∙ᴮ a) ≈ m
 Associative : Op₂ A → Opᵣ A B → Set _
 Associative _∙ᴬ_ _∙ᴮ_ = ∀ m x y → ((m ∙ᴮ x) ∙ᴮ y) ≈ (m ∙ᴮ (x ∙ᴬ y))
 
+infix 4 _DistributesOverʳ_ _DistributesOverˡ_⟶_
+
 _DistributesOverˡ_⟶_ : Opᵣ A B → Op₂ A → Op₂ B → Set _
 _*_ DistributesOverˡ _+ᴬ_ ⟶ _+ᴮ_ =
   ∀ m x y → (m * (x +ᴬ y)) ≈ ((m * x) +ᴮ (m * y))
diff --git a/src/Algebra/Properties/Monoid/Divisibility.agda b/src/Algebra/Properties/Monoid/Divisibility.agda
index 588f6ef375..c0f4c40af9 100644
--- a/src/Algebra/Properties/Monoid/Divisibility.agda
+++ b/src/Algebra/Properties/Monoid/Divisibility.agda
@@ -26,6 +26,8 @@ open import Algebra.Properties.Semigroup.Divisibility semigroup public
 ------------------------------------------------------------------------
 -- Additional properties
 
+infix 4 ε∣_
+
 ε∣_ : ∀ x → ε ∣ x
 ε∣ x = x , identityʳ x
 
diff --git a/src/Algebra/Properties/Semiring/Divisibility.agda b/src/Algebra/Properties/Semiring/Divisibility.agda
index 54a352d782..8cdcbe7e62 100644
--- a/src/Algebra/Properties/Semiring/Divisibility.agda
+++ b/src/Algebra/Properties/Semiring/Divisibility.agda
@@ -25,6 +25,8 @@ open MonoidDivisibility *-monoid public
 ------------------------------------------------------------------------
 -- Divisibility properties specific to semirings.
 
+infixr 8 _∣0
+
 _∣0 : ∀ x → x ∣ 0#
 x ∣0 = 0# , zeroˡ x
 
diff --git a/src/Algebra/Solver/Ring/AlmostCommutativeRing.agda b/src/Algebra/Solver/Ring/AlmostCommutativeRing.agda
index 4c33c7b337..9659dfc6ca 100644
--- a/src/Algebra/Solver/Ring/AlmostCommutativeRing.agda
+++ b/src/Algebra/Solver/Ring/AlmostCommutativeRing.agda
@@ -76,6 +76,8 @@ record AlmostCommutativeRing c ℓ : Set (suc (c ⊔ ℓ)) where
 ------------------------------------------------------------------------
 -- Homomorphisms
 
+infix 4 _-Raw-AlmostCommutative⟶_
+
 record _-Raw-AlmostCommutative⟶_
   {r₁ r₂ r₃ r₄}
   (From : RawRing r₁ r₄)