From f6e428f494b85f32d216c4248b5d4aeec90f0f79 Mon Sep 17 00:00:00 2001 From: Jacques Carette Date: Mon, 13 May 2024 22:06:11 -0400 Subject: [PATCH 1/6] put the fixity recommendations into the style guide --- doc/style-guide.md | 48 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 48 insertions(+) diff --git a/doc/style-guide.md b/doc/style-guide.md index 254a7ec071..426d86a8b8 100644 --- a/doc/style-guide.md +++ b/doc/style-guide.md @@ -525,6 +525,54 @@ 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` + +* multiplication-like: `infixl 7 _*_` + +* addition-like `infixl 6 _+_` + +* negation-like `infix 8 ¬_` + +* and-like `infixr 7 _∧_` + +* or-like `infixr 6 _∨_` + +* 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 _⊎_` + + #### Functions and relations over specific datatypes * When defining a new relation `P` over a datatype `X` in a `Data.X.Relation` module, From f92c835e7e7faf082e12335cab105db131c66beb Mon Sep 17 00:00:00 2001 From: Jacques Carette Date: Mon, 13 May 2024 22:09:57 -0400 Subject: [PATCH 2/6] mixing fixity declaration --- src/Algebra/Bundles.agda | 1 + 1 file changed, 1 insertion(+) 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 _≈_ From 6df0f398767f7298d73de76b5582a27671c7d5a7 Mon Sep 17 00:00:00 2001 From: Jacques Carette Date: Mon, 13 May 2024 22:19:45 -0400 Subject: [PATCH 3/6] was missing a case --- doc/README/Design/Fixity.agda | 1 + doc/style-guide.md | 3 +++ 2 files changed, 4 insertions(+) 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 426d86a8b8..87a9f0be32 100644 --- a/doc/style-guide.md +++ b/doc/style-guide.md @@ -569,9 +569,12 @@ Reasoning: * 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 From 3174593f95e90fb94eedba10012d3a947a21fd9f Mon Sep 17 00:00:00 2001 From: Jacques Carette Date: Mon, 13 May 2024 22:20:03 -0400 Subject: [PATCH 4/6] use the new case --- src/Algebra/Definitions.agda | 4 ++++ 1 file changed, 4 insertions(+) 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)) From c9444c4c2e4958a0b6dff0aae6e0a45273723e1d Mon Sep 17 00:00:00 2001 From: Jacques Carette Date: Mon, 13 May 2024 22:55:07 -0400 Subject: [PATCH 5/6] add fixities for everything in Algebra --- doc/style-guide.md | 5 +++++ 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 ++ src/Algebra/Properties/Monoid/Divisibility.agda | 2 ++ src/Algebra/Properties/Semiring/Divisibility.agda | 2 ++ src/Algebra/Solver/Ring/AlmostCommutativeRing.agda | 2 ++ 8 files changed, 17 insertions(+), 1 deletion(-) diff --git a/doc/style-guide.md b/doc/style-guide.md index 87a9f0be32..9627c69c06 100644 --- a/doc/style-guide.md +++ b/doc/style-guide.md @@ -532,8 +532,13 @@ 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 _+_` 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₄) From edb84a3479318f68d53e4f52921ed00a9185b511 Mon Sep 17 00:00:00 2001 From: Jacques Carette Date: Wed, 15 May 2024 21:56:30 -0400 Subject: [PATCH 6/6] incorporate some suggestions for extra cases --- doc/style-guide.md | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/doc/style-guide.md b/doc/style-guide.md index 9627c69c06..2562f76cfd 100644 --- a/doc/style-guide.md +++ b/doc/style-guide.md @@ -543,12 +543,16 @@ General operations and relations: * addition-like `infixl 6 _+_` -* negation-like `infix 8 ¬_` +* 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 _>>=_`