From 91faa98b3b2ba1d834795fa2b2989d0ea7b3ea31 Mon Sep 17 00:00:00 2001 From: Saransh Chopra Date: Wed, 14 Jun 2023 18:13:38 -0400 Subject: [PATCH 1/2] Add fixities in `Function` --- src/Algebra/Definitions.agda | 2 +- src/Function/Endomorphism/Propositional.agda | 2 ++ src/Function/Endomorphism/Setoid.agda | 2 ++ src/Function/HalfAdjointEquivalence.agda | 2 ++ src/Function/Metric/Bundles.agda | 7 +++++++ src/Function/Metric/Nat/Bundles.agda | 6 ++++++ src/Function/Related.agda | 2 ++ 7 files changed, 22 insertions(+), 1 deletion(-) diff --git a/src/Algebra/Definitions.agda b/src/Algebra/Definitions.agda index c0820fafb7..e64fc4f30b 100644 --- a/src/Algebra/Definitions.agda +++ b/src/Algebra/Definitions.agda @@ -109,7 +109,7 @@ _DistributesOver_ : Op₂ A → Op₂ A → Set _ * DistributesOver + = (* DistributesOverˡ +) × (* DistributesOverʳ +) _MiddleFourExchange_ : Op₂ A → Op₂ A → Set _ -_*_ MiddleFourExchange _+_ = +_*_ MiddleFourExchange _+_ = ∀ w x y z → ((w + x) * (y + z)) ≈ ((w + y) * (x + z)) _IdempotentOn_ : Op₂ A → A → Set _ diff --git a/src/Function/Endomorphism/Propositional.agda b/src/Function/Endomorphism/Propositional.agda index 32a5522318..8a78f69496 100644 --- a/src/Function/Endomorphism/Propositional.agda +++ b/src/Function/Endomorphism/Propositional.agda @@ -43,6 +43,8 @@ toSetoidEndo f = record ------------------------------------------------------------------------ -- N-th composition +infixr 8 _^_ + _^_ : Endo → ℕ → Endo f ^ zero = id f ^ suc n = f ∘′ (f ^ n) diff --git a/src/Function/Endomorphism/Setoid.agda b/src/Function/Endomorphism/Setoid.agda index 9c3d18e7f4..b02976db88 100644 --- a/src/Function/Endomorphism/Setoid.agda +++ b/src/Function/Endomorphism/Setoid.agda @@ -35,6 +35,8 @@ private Endo : Set _ Endo = S ⟶ S +infixr 8 _^_ + _^_ : Endo → ℕ → Endo f ^ zero = id f ^ suc n = f ∘ (f ^ n) diff --git a/src/Function/HalfAdjointEquivalence.agda b/src/Function/HalfAdjointEquivalence.agda index f600dfe759..59b11d5f69 100644 --- a/src/Function/HalfAdjointEquivalence.agda +++ b/src/Function/HalfAdjointEquivalence.agda @@ -16,6 +16,8 @@ open import Relation.Binary.PropositionalEquality -- Half adjoint equivalences (see the HoTT book). +infix 4 _≃_ + record _≃_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where field to : A → B diff --git a/src/Function/Metric/Bundles.agda b/src/Function/Metric/Bundles.agda index 7acf81de13..ad3a29c333 100644 --- a/src/Function/Metric/Bundles.agda +++ b/src/Function/Metric/Bundles.agda @@ -22,6 +22,7 @@ open import Function.Metric.Core record ProtoMetric (a i ℓ₁ ℓ₂ ℓ₃ : Level) : Set (suc (a ⊔ i ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃)) where + infix 4 _≈_ _≈ᵢ_ _≤_ field Carrier : Set a Image : Set i @@ -39,6 +40,7 @@ record ProtoMetric (a i ℓ₁ ℓ₂ ℓ₃ : Level) record PreMetric (a i ℓ₁ ℓ₂ ℓ₃ : Level) : Set (suc (a ⊔ i ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃)) where + infix 4 _≈_ _≈ᵢ_ _≤_ field Carrier : Set a Image : Set i @@ -61,6 +63,8 @@ record PreMetric (a i ℓ₁ ℓ₂ ℓ₃ : Level) record QuasiSemiMetric (a i ℓ₁ ℓ₂ ℓ₃ : Level) : Set (suc (a ⊔ i ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃)) where + + infix 4 _≈_ _≈ᵢ_ _≤_ field Carrier : Set a Image : Set i @@ -86,6 +90,7 @@ record QuasiSemiMetric (a i ℓ₁ ℓ₂ ℓ₃ : Level) record SemiMetric (a i ℓ₁ ℓ₂ ℓ₃ : Level) : Set (suc (a ⊔ i ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃)) where + infix 4 _≈_ _≈ᵢ_ _≤_ field Carrier : Set a Image : Set i @@ -120,6 +125,8 @@ record SemiMetric (a i ℓ₁ ℓ₂ ℓ₃ : Level) record GeneralMetric (a i ℓ₁ ℓ₂ ℓ₃ : Level) : Set (suc (a ⊔ i ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃)) where + infix 4 _≈_ _≈ᵢ_ _≤_ + infixl 6 _∙_ field Carrier : Set a Image : Set i diff --git a/src/Function/Metric/Nat/Bundles.agda b/src/Function/Metric/Nat/Bundles.agda index 3e406d7611..e0983246eb 100644 --- a/src/Function/Metric/Nat/Bundles.agda +++ b/src/Function/Metric/Nat/Bundles.agda @@ -28,6 +28,7 @@ open import Function.Metric.Bundles as Base -- Proto-metric record ProtoMetric a ℓ : Set (suc (a ⊔ ℓ)) where + infix 4 _≈_ field Carrier : Set a _≈_ : Rel Carrier ℓ @@ -40,6 +41,7 @@ record ProtoMetric a ℓ : Set (suc (a ⊔ ℓ)) where -- PreMetric record PreMetric a ℓ : Set (suc (a ⊔ ℓ)) where + infix 4 _≈_ field Carrier : Set a _≈_ : Rel Carrier ℓ @@ -57,6 +59,7 @@ record PreMetric a ℓ : Set (suc (a ⊔ ℓ)) where -- QuasiSemiMetric record QuasiSemiMetric a ℓ : Set (suc (a ⊔ ℓ)) where + infix 4 _≈_ field Carrier : Set a _≈_ : Rel Carrier ℓ @@ -77,6 +80,7 @@ record QuasiSemiMetric a ℓ : Set (suc (a ⊔ ℓ)) where -- SemiMetric record SemiMetric a ℓ : Set (suc (a ⊔ ℓ)) where + infix 4 _≈_ field Carrier : Set a _≈_ : Rel Carrier ℓ @@ -97,6 +101,7 @@ record SemiMetric a ℓ : Set (suc (a ⊔ ℓ)) where -- Metrics record Metric a ℓ : Set (suc (a ⊔ ℓ)) where + infix 4 _≈_ field Carrier : Set a _≈_ : Rel Carrier ℓ @@ -117,6 +122,7 @@ record Metric a ℓ : Set (suc (a ⊔ ℓ)) where -- UltraMetrics record UltraMetric a ℓ : Set (suc (a ⊔ ℓ)) where + infix 4 _≈_ field Carrier : Set a _≈_ : Rel Carrier ℓ diff --git a/src/Function/Related.agda b/src/Function/Related.agda index 0746b3c14a..fa114d077c 100644 --- a/src/Function/Related.agda +++ b/src/Function/Related.agda @@ -53,6 +53,8 @@ open R public using -- (which implies that Agda can deduce the universe code from an -- expression matching any of the right-hand sides). +infix 3 _←_ _↢_ + record _←_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where constructor lam field app-← : B → A From 193277b47853b511b5e1b7ced0f810c5e15ca2f8 Mon Sep 17 00:00:00 2001 From: Saransh Chopra Date: Wed, 14 Jun 2023 21:31:13 -0400 Subject: [PATCH 2/2] Fixities for `Reflection` and `Data` --- CHANGELOG.md | 24 +++++++++++++++++++ .../Relation/Binary/Equality/Setoid.agda | 2 ++ src/Data/Vec/N-ary.agda | 2 ++ src/Reflection/AST/Argument/Information.agda | 2 ++ src/Reflection/AST/Argument/Modality.agda | 2 ++ src/Reflection/AST/Argument/Quantity.agda | 2 ++ src/Reflection/AST/Argument/Relevance.agda | 2 ++ src/Reflection/AST/Argument/Visibility.agda | 2 ++ src/Reflection/AST/Definition.agda | 2 ++ src/Reflection/AST/Literal.agda | 2 ++ src/Reflection/AST/Meta.agda | 3 ++- src/Reflection/AST/Name.agda | 4 ++-- src/Reflection/AST/Term.agda | 2 +- 13 files changed, 47 insertions(+), 4 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index d5ba31beaf..df113ca7a4 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -29,6 +29,30 @@ Highlights Bug-fixes --------- +* The following operators were missing a fixity declaration, which has now + been fixed - + ``` + infix -1 _$ⁿ_ (Data.Vec.N-ary) + infix 4 _≋_ (Data.Vec.Functional.Relation.Binary.Equality.Setoid) + infix 4 _≟_ (Reflection.AST.Definition) + infix 4 _≡ᵇ_ (Reflection.AST.Literal) + infix 4 _≈?_ _≟_ _≈_ (Reflection.AST.Meta) + infix 4 _≈?_ _≟_ _≈_ (Reflection.AST.Name) + infix 4 _≟-Telescope_ (Reflection.AST.Term) + infix 4 _≟_ (Reflection.AST.Argument.Information) + infix 4 _≟_ (Reflection.AST.Argument.Modality) + infix 4 _≟_ (Reflection.AST.Argument.Quantity) + infix 4 _≟_ (Reflection.AST.Argument.Relevance) + infix 4 _≟_ (Reflection.AST.Argument.Visibility) + infixr 8 _^_ (Function.Endomorphism.Propositional) + infixr 8 _^_ (Function.Endomorphism.Setoid) + infix 4 _≃_ (Function.HalfAdjointEquivalence) + infix 4 _≈_ _≈ᵢ_ _≤_ (Function.Metric.Bundles) + infixl 6 _∙_ (Function.Metric.Bundles) + infix 4 _≈_ (Function.Metric.Nat.Bundles) + infix 3 _←_ _↢_ (Function.Related) + ``` + * In `System.Exit`, the `ExitFailure` constructor is now carrying an integer rather than a natural. The previous binding was incorrectly assuming that all exit codes where non-negative. diff --git a/src/Data/Vec/Functional/Relation/Binary/Equality/Setoid.agda b/src/Data/Vec/Functional/Relation/Binary/Equality/Setoid.agda index 932ac19c95..8b29e710f8 100644 --- a/src/Data/Vec/Functional/Relation/Binary/Equality/Setoid.agda +++ b/src/Data/Vec/Functional/Relation/Binary/Equality/Setoid.agda @@ -24,6 +24,8 @@ open Setoid S renaming (Carrier to A) -- Definition ------------------------------------------------------------------------ +infix 4 _≋_ + _≋_ : ∀ {n} → Vector A n → Vector A n → Set ℓ _≋_ = Pointwise _≈_ diff --git a/src/Data/Vec/N-ary.agda b/src/Data/Vec/N-ary.agda index 02b6e704ba..7e10c5567c 100644 --- a/src/Data/Vec/N-ary.agda +++ b/src/Data/Vec/N-ary.agda @@ -45,6 +45,8 @@ curryⁿ : ∀ {n} → (Vec A n → B) → N-ary n A B curryⁿ {n = zero} f = f [] curryⁿ {n = suc n} f = λ x → curryⁿ (f ∘ _∷_ x) +infix -1 _$ⁿ_ + _$ⁿ_ : ∀ {n} → N-ary n A B → (Vec A n → B) f $ⁿ [] = f f $ⁿ (x ∷ xs) = f x $ⁿ xs diff --git a/src/Reflection/AST/Argument/Information.agda b/src/Reflection/AST/Argument/Information.agda index 3e97598d46..fe09976fb9 100644 --- a/src/Reflection/AST/Argument/Information.agda +++ b/src/Reflection/AST/Argument/Information.agda @@ -48,6 +48,8 @@ arg-info-injective₂ refl = refl arg-info-injective : arg-info v m ≡ arg-info v′ m′ → v ≡ v′ × m ≡ m′ arg-info-injective = < arg-info-injective₁ , arg-info-injective₂ > +infix 4 _≟_ + _≟_ : DecidableEquality ArgInfo arg-info v m ≟ arg-info v′ m′ = map′ diff --git a/src/Reflection/AST/Argument/Modality.agda b/src/Reflection/AST/Argument/Modality.agda index 1e39783349..95f15b2264 100644 --- a/src/Reflection/AST/Argument/Modality.agda +++ b/src/Reflection/AST/Argument/Modality.agda @@ -48,6 +48,8 @@ modality-injective₂ refl = refl modality-injective : modality r q ≡ modality r′ q′ → r ≡ r′ × q ≡ q′ modality-injective = < modality-injective₁ , modality-injective₂ > +infix 4 _≟_ + _≟_ : DecidableEquality Modality modality r q ≟ modality r′ q′ = map′ diff --git a/src/Reflection/AST/Argument/Quantity.agda b/src/Reflection/AST/Argument/Quantity.agda index 3942a667a1..0c53a521c1 100644 --- a/src/Reflection/AST/Argument/Quantity.agda +++ b/src/Reflection/AST/Argument/Quantity.agda @@ -21,6 +21,8 @@ open Quantity public ------------------------------------------------------------------------ -- Decidable equality +infix 4 _≟_ + _≟_ : DecidableEquality Quantity quantity-ω ≟ quantity-ω = yes refl quantity-0 ≟ quantity-0 = yes refl diff --git a/src/Reflection/AST/Argument/Relevance.agda b/src/Reflection/AST/Argument/Relevance.agda index 1ec1606453..6cdce1d96f 100644 --- a/src/Reflection/AST/Argument/Relevance.agda +++ b/src/Reflection/AST/Argument/Relevance.agda @@ -21,6 +21,8 @@ open Relevance public ------------------------------------------------------------------------ -- Decidable equality +infix 4 _≟_ + _≟_ : DecidableEquality Relevance relevant ≟ relevant = yes refl irrelevant ≟ irrelevant = yes refl diff --git a/src/Reflection/AST/Argument/Visibility.agda b/src/Reflection/AST/Argument/Visibility.agda index 93654a018c..4f94b24fe3 100644 --- a/src/Reflection/AST/Argument/Visibility.agda +++ b/src/Reflection/AST/Argument/Visibility.agda @@ -21,6 +21,8 @@ open Visibility public ------------------------------------------------------------------------ -- Decidable equality +infix 4 _≟_ + _≟_ : DecidableEquality Visibility visible ≟ visible = yes refl hidden ≟ hidden = yes refl diff --git a/src/Reflection/AST/Definition.agda b/src/Reflection/AST/Definition.agda index 7cb403fb49..5b6dace7cd 100644 --- a/src/Reflection/AST/Definition.agda +++ b/src/Reflection/AST/Definition.agda @@ -59,6 +59,8 @@ record′-injective = < record′-injective₁ , record′-injective₂ > constructor′-injective : ∀ {c c′} → constructor′ c ≡ constructor′ c′ → c ≡ c′ constructor′-injective refl = refl +infix 4 _≟_ + _≟_ : DecidableEquality Definition function cs ≟ function cs′ = map′ (cong function) function-injective (cs Term.≟-Clauses cs′) diff --git a/src/Reflection/AST/Literal.agda b/src/Reflection/AST/Literal.agda index 280ba13010..33ceed9ca5 100644 --- a/src/Reflection/AST/Literal.agda +++ b/src/Reflection/AST/Literal.agda @@ -104,5 +104,7 @@ meta x ≟ string x₁ = no (λ ()) meta x ≟ name x₁ = no (λ ()) meta x ≟ meta x₁ = map′ (cong meta) meta-injective (x Meta.≟ x₁) +infix 4 _≡ᵇ_ + _≡ᵇ_ : Literal → Literal → Bool l ≡ᵇ l′ = isYes (l ≟ l′) diff --git a/src/Reflection/AST/Meta.agda b/src/Reflection/AST/Meta.agda index b5db1fad1a..59ca4ae4db 100644 --- a/src/Reflection/AST/Meta.agda +++ b/src/Reflection/AST/Meta.agda @@ -23,12 +23,13 @@ open import Agda.Builtin.Reflection.Properties public -- Equality of metas is decidable. +infix 4 _≈?_ _≟_ _≈_ + _≈_ : Rel Meta _ _≈_ = _≡_ on toℕ _≈?_ : Decidable _≈_ _≈?_ = On.decidable toℕ _≡_ ℕₚ._≟_ -infix 4 _≟_ _≟_ : DecidableEquality Meta m ≟ n = map′ (toℕ-injective _ _) (cong toℕ) (m ≈? n) diff --git a/src/Reflection/AST/Name.agda b/src/Reflection/AST/Name.agda index 50c6ee7878..203521330c 100644 --- a/src/Reflection/AST/Name.agda +++ b/src/Reflection/AST/Name.agda @@ -37,11 +37,11 @@ Names = List Name -- Decidable equality for names ---------------------------------------------------------------------- +infix 4 _≈?_ _≟_ _≈_ + _≈_ : Rel Name _ _≈_ = _≡_ on toWords -infix 4 _≈?_ _≟_ - _≈?_ : Decidable _≈_ _≈?_ = decidable toWords _≡_ (Prodₚ.≡-dec Wₚ._≟_ Wₚ._≟_) diff --git a/src/Reflection/AST/Term.agda b/src/Reflection/AST/Term.agda index fb0f5bde61..183f839015 100644 --- a/src/Reflection/AST/Term.agda +++ b/src/Reflection/AST/Term.agda @@ -128,7 +128,7 @@ absurd-clause-injective = < absurd-clause-injective₁ , absurd-clause-injective infix 4 _≟-AbsTerm_ _≟-AbsType_ _≟-ArgTerm_ _≟-ArgType_ _≟-Args_ _≟-Clause_ _≟-Clauses_ _≟_ - _≟-Sort_ _≟-Pattern_ _≟-Patterns_ + _≟-Sort_ _≟-Pattern_ _≟-Patterns_ _≟-Telescope_ _≟-AbsTerm_ : DecidableEquality (Abs Term) _≟-AbsType_ : DecidableEquality (Abs Type)