diff --git a/CHANGELOG.md b/CHANGELOG.md index 2d61629e75..cc18045d52 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -21,6 +21,17 @@ Bug-fixes Non-backwards compatible changes -------------------------------- +* The notation for `Decidable` relations has been (partially) standardised: thus + - `_≡?_` (at `infix 4`) for `DecidableEquality` + - `_≈?_` (ditto.) for the fieldname of the general `IsDecEquivalence` + + Despite being non-backwards compatible, because a fieldname has changed, the + old notation `_≟_` (which was used for both of the above) has been retained, + but deprecated. This leads to a large amount of (trivial) deprecations, in + addition to the substantive one under `Relation.Binary.Structures`, and in + `Data.{Nat|Fin}.Properties` for the concrete datatypes. These deprecations + are summarised below, but are not each documented for each affected module. + Minor improvements ------------------ @@ -87,6 +98,15 @@ Deprecated names ```agda ¬∀⟶∃¬-smallest ↦ ¬∀⇒∃¬-smallest ¬∀⟶∃¬- ↦ ¬∀⇒∃¬ + _≟_ ↦ _≡?_ + inj⇒≟ ↦ inj⇒≡? + ``` + +* In `Data.Nat.Properties`: + ```agda + _≟_ ↦ _≡?_ + ≟-diag ↦ ≡?-≡ + ≟-≡ ↦ ≡?-≢ ``` * In `Data.Rational.Properties`: @@ -99,16 +119,37 @@ Deprecated names truncate-irrelevant ↦ Relation.Binary.PropositionalEquality.Core.refl ``` +* In `Effect.Monad.Partiality`: + ```agda + _≟-Kind_ ↦ _≡?-Kind_ + ``` + +* In `Reflection.AST.AlphaEquality`: + ```agda + ≟⇒α ↦ ≡?⇒α + ``` + * In `Relation.Binary.Construct.Intersection`: ```agda decidable ↦ _∩?_ ``` +* In `Relation.Binary.PropositionalEquality`: + ```agda + ≡-≟-identity ↦ ≡-≡?-identity + ≢-≟-identity ↦ ≢-≡?-identity + ``` + * In `Relation.Binary.Construct.Union`: ```agda decidable ↦ _∪?_ ``` +* In `Relation.Nary`: + ```agda + ≟-mapₙ ↦ ≡?-mapₙ + ``` + * In `Relation.Nullary.Decidable.Core`: ```agda ⊤-dec ↦ ⊤? @@ -116,6 +157,7 @@ Deprecated names _×-dec_ ↦ _×?_ _⊎-dec_ ↦ _⊎?_ _→-dec_ ↦ _→?_ + ``` * In `Relation.Nullary.Negation`: ```agda @@ -249,9 +291,9 @@ Additions to existing modules * In `Data.Fin.Properties`: ```agda ≡-irrelevant : Irrelevant {A = Fin n} _≡_ - ≟-≡ : (eq : i ≡ j) → (i ≟ j) ≡ yes eq - ≟-≡-refl : (i : Fin n) → (i ≟ i) ≡ yes refl - ≟-≢ : (i≢j : i ≢ j) → (i ≟ j) ≡ no i≢j + ≡?-≡ : (eq : i ≡ j) → (i ≡? j) ≡ yes eq + ≡?-≡-refl : (i : Fin n) → (i ≡? i) ≡ yes refl + ≡?-≢ : (i≢j : i ≢ j) → (i ≡? j) ≡ no i≢j inject-< : inject j < i record Least⟨_⟩ (P : Pred (Fin n) p) : Set p where @@ -315,7 +357,7 @@ Additions to existing modules * In `Data.Nat.Properties`: ```agda - ≟-≢ : (m≢n : m ≢ n) → (m ≟ n) ≡ no m≢n + ≡?-≡-refl : ∀ n → (n ≡? n) ≡ yes refl ∸-suc : .(m ≤ n) → suc n ∸ m ≡ suc (n ∸ m) ^-distribʳ-* : ∀ m n o → (n * o) ^ m ≡ n ^ m * o ^ m 2*suc[n]≡2+n+n : ∀ n → 2 * (suc n) ≡ 2 + (n + n) diff --git a/doc/README/Data/List/Membership.agda b/doc/README/Data/List/Membership.agda index 38732fe631..d29a2cf9d8 100644 --- a/doc/README/Data/List/Membership.agda +++ b/doc/README/Data/List/Membership.agda @@ -34,7 +34,7 @@ import Data.List.Membership.DecPropositional as DecPropMembership -- propositional equality over `ℕ` and it is also decidable. Therefore -- the module `DecPropMembership` should be opened as follows: -open DecPropMembership ℕ._≟_ +open DecPropMembership ℕ._≡?_ -- As membership is just an instance of `Any` we also need to import -- the constructors `here` and `there`. (See issue #553 on Github for @@ -66,7 +66,7 @@ import Data.List.Membership.Propositional.Properties as PropProperties -- following the first `∈` refers to lists of type `List ℕ` whereas -- the second `∈` refers to lists of type `List Char`. -open DecPropMembership Char._≟_ renaming (_∈_ to _∈ᶜ_) +open DecPropMembership Char._≡?_ renaming (_∈_ to _∈ᶜ_) open SetoidProperties using (∈-map⁺) lem₂ : {v : ℕ} {xs : List ℕ} → v ∈ xs → fromℕ v ∈ᶜ map fromℕ xs diff --git a/doc/README/Data/List/Relation/Binary/Subset.agda b/doc/README/Data/List/Relation/Binary/Subset.agda index ccef725cca..646c4c6e54 100644 --- a/doc/README/Data/List/Relation/Binary/Subset.agda +++ b/doc/README/Data/List/Relation/Binary/Subset.agda @@ -22,10 +22,10 @@ module README.Data.List.Relation.Binary.Subset where -- Decidable equality over Strings open import Data.String.Base using (String) -open import Data.String.Properties using (_≟_) +open import Data.String.Properties using (_≡?_) -- Open the decidable membership module using Decidable ≡ over Strings -open import Data.List.Membership.DecPropositional _≟_ +open import Data.List.Membership.DecPropositional _≡?_ -- Simple cases are inductive proofs diff --git a/doc/README/Data/Record.agda b/doc/README/Data/Record.agda index 63fea328ae..53b3d50fb2 100644 --- a/doc/README/Data/Record.agda +++ b/doc/README/Data/Record.agda @@ -21,7 +21,7 @@ import Data.Record as Record -- Let us use strings as labels. -open Record String _≟_ +open Record String _≡?_ -- Partial equivalence relations. diff --git a/doc/README/Data/Trie/NonDependent.agda b/doc/README/Data/Trie/NonDependent.agda index 385e981880..f367b78587 100644 --- a/doc/README/Data/Trie/NonDependent.agda +++ b/doc/README/Data/Trie/NonDependent.agda @@ -83,7 +83,7 @@ record Lexer t : Set (suc t) where -- Two keywords are considered distinct if the strings are not equal Distinct : Rel Keyword 0ℓ - Distinct a b = ⌊ ¬? ((proj₁ a) String.≟ (proj₁ b)) ⌋ + Distinct a b = ⌊ ¬? ((proj₁ a) String.≡? (proj₁ b)) ⌋ field @@ -175,7 +175,7 @@ module LetIn where LPAR RPAR : TOK ID : String → TOK - keywords : List# (String × TOK) (λ a b → ⌊ ¬? ((proj₁ a) String.≟ (proj₁ b)) ⌋) + keywords : List# (String × TOK) (λ a b → ⌊ ¬? ((proj₁ a) String.≡? (proj₁ b)) ⌋) keywords = ("let" , LET) ∷# ("=" , EQ) ∷# ("in" , IN) diff --git a/doc/README/Design/Decidability.agda b/doc/README/Design/Decidability.agda index 63ab9f2021..a32fb8782f 100644 --- a/doc/README/Design/Decidability.agda +++ b/doc/README/Design/Decidability.agda @@ -24,21 +24,21 @@ open import Relation.Nary open import Relation.Nullary.Reflects -infix 4 _≟₀_ _≟₁_ _≟₂_ +infix 4 _≡?₀_ _≡?₁_ _≡?₂_ -- A proof of `Reflects P b` shows that a proposition `P` has the truth value of -- the boolean `b`. A proof of `Reflects P true` amounts to a proof of `P`, and -- a proof of `Reflects P false` amounts to a refutation of `P`. ex₀ : (n : ℕ) → Reflects (n ≡ n) true -ex₀ n = ofʸ refl +ex₀ n = of refl ex₁ : (n : ℕ) → Reflects (zero ≡ suc n) false -ex₁ n = ofⁿ λ () +ex₁ n = of λ() ex₂ : (b : Bool) → Reflects (T b) b -ex₂ false = ofⁿ id -ex₂ true = ofʸ tt +ex₂ false = of id +ex₂ true = of tt ------------------------------------------------------------------------ -- Dec @@ -64,71 +64,71 @@ ex₄ n = no λ () -- only the `yes` and `no` patterns. The following procedure decides whether two -- given natural numbers are equal. -_≟₀_ : (m n : ℕ) → Dec (m ≡ n) -zero ≟₀ zero = yes refl -zero ≟₀ suc n = no λ () -suc m ≟₀ zero = no λ () -suc m ≟₀ suc n with m ≟₀ n +_≡?₀_ : (m n : ℕ) → Dec (m ≡ n) +zero ≡?₀ zero = yes refl +zero ≡?₀ suc n = no λ() +suc m ≡?₀ zero = no λ() +suc m ≡?₀ suc n with m ≡?₀ n ... | yes p = yes (cong suc p) ... | no ¬p = no (¬p ∘ suc-injective) --- In this case, we can see that `does (suc m ≟ suc n)` should be equal to --- `does (m ≟ n)`, because a `yes` from `m ≟ n` gives rise to a `yes` from the +-- In this case, we can see that `does (suc m ≡? suc n)` should be equal to +-- `does (m ≡? n)`, because a `yes` from `m ≡? n` gives rise to a `yes` from the -- result, and similarly for `no`. However, in the above definition, this -- equality does not hold definitionally, because we always do a case split -- before returning a result. To avoid this, we can return the `does` part -- separately, before any pattern matching. -_≟₁_ : (m n : ℕ) → Dec (m ≡ n) -zero ≟₁ zero = yes refl -zero ≟₁ suc n = no λ () -suc m ≟₁ zero = no λ () -does (suc m ≟₁ suc n) = does (m ≟₁ n) -proof (suc m ≟₁ suc n) with m ≟₁ n -... | yes p = ofʸ (cong suc p) -... | no ¬p = ofⁿ (¬p ∘ suc-injective) +_≡?₁_ : (m n : ℕ) → Dec (m ≡ n) +zero ≡?₁ zero = yes refl +zero ≡?₁ suc n = no λ() +suc m ≡?₁ zero = no λ() +does (suc m ≡?₁ suc n) = does (m ≡?₁ n) +proof (suc m ≡?₁ suc n) with m ≡?₁ n +... | yes p = of (cong suc p) +... | no ¬p = of (¬p ∘ suc-injective) -- We now get definitional equalities such as the following. -_ : (m n : ℕ) → does (5 + m ≟₁ 3 + n) ≡ does (2 + m ≟₁ n) +_ : (m n : ℕ) → does (5 + m ≡?₁ 3 + n) ≡ does (2 + m ≡?₁ n) _ = λ m n → refl -- Even better, from a maintainability point of view, is to use `map` or `map′`, -- both of which capture the pattern of the `does` field remaining the same, but -- the `proof` field being updated. -_≟₂_ : (m n : ℕ) → Dec (m ≡ n) -zero ≟₂ zero = yes refl -zero ≟₂ suc n = no λ () -suc m ≟₂ zero = no λ () -suc m ≟₂ suc n = map′ (cong suc) suc-injective (m ≟₂ n) +_≡?₂_ : (m n : ℕ) → Dec (m ≡ n) +zero ≡?₂ zero = yes refl +zero ≡?₂ suc n = no λ() +suc m ≡?₂ zero = no λ() +suc m ≡?₂ suc n = map′ (cong suc) suc-injective (m ≡?₂ n) -_ : (m n : ℕ) → does (5 + m ≟₂ 3 + n) ≡ does (2 + m ≟₂ n) +_ : (m n : ℕ) → does (5 + m ≡?₂ 3 + n) ≡ does (2 + m ≡?₂ n) _ = λ m n → refl -- `map′` can be used in conjunction with combinators such as `_⊎?_` and -- `_×?_` to build complex (simply typed) decision procedures. -module ListDecEq₀ {a} {A : Set a} (_≟ᴬ_ : (x y : A) → Dec (x ≡ y)) where +module ListDecEq₀ {a} {A : Set a} (_≡?ᴬ_ : (x y : A) → Dec (x ≡ y)) where - _≟ᴸᴬ_ : (xs ys : List A) → Dec (xs ≡ ys) - [] ≟ᴸᴬ [] = yes refl - [] ≟ᴸᴬ (y ∷ ys) = no λ () - (x ∷ xs) ≟ᴸᴬ [] = no λ () - (x ∷ xs) ≟ᴸᴬ (y ∷ ys) = - map′ (uncurry (cong₂ _∷_)) ∷-injective (x ≟ᴬ y ×? xs ≟ᴸᴬ ys) + _≡?ᴸᴬ_ : (xs ys : List A) → Dec (xs ≡ ys) + [] ≡?ᴸᴬ [] = yes refl + [] ≡?ᴸᴬ (y ∷ ys) = no λ() + (x ∷ xs) ≡?ᴸᴬ [] = no λ() + (x ∷ xs) ≡?ᴸᴬ (y ∷ ys) = + map′ (uncurry (cong₂ _∷_)) ∷-injective (x ≡?ᴬ y ×? xs ≡?ᴸᴬ ys) -- The final case says that `x ∷ xs ≡ y ∷ ys` exactly when `x ≡ y` *and* -- `xs ≡ ys`. The proofs are updated by the first two arguments to `map′`. -- In the case of ≡-equality tests, the pattern --- `map′ (congₙ c) c-injective (x₀ ≟ y₀ ×? ... ×? xₙ₋₁ ≟ yₙ₋₁)` --- is captured by `≟-mapₙ n c c-injective (x₀ ≟ y₀) ... (xₙ₋₁ ≟ yₙ₋₁)`. +-- `map′ (congₙ c) c-injective (x₀ ≡? y₀ ×? ... ×? xₙ₋₁ ≡? yₙ₋₁)` +-- is captured by `≡?-mapₙ n c c-injective (x₀ ≡? y₀) ... (xₙ₋₁ ≡? yₙ₋₁)`. -module ListDecEq₁ {a} {A : Set a} (_≟ᴬ_ : (x y : A) → Dec (x ≡ y)) where +module ListDecEq₁ {a} {A : Set a} (_≡?ᴬ_ : (x y : A) → Dec (x ≡ y)) where - _≟ᴸᴬ_ : (xs ys : List A) → Dec (xs ≡ ys) - [] ≟ᴸᴬ [] = yes refl - [] ≟ᴸᴬ (y ∷ ys) = no λ () - (x ∷ xs) ≟ᴸᴬ [] = no λ () - (x ∷ xs) ≟ᴸᴬ (y ∷ ys) = ≟-mapₙ 2 _∷_ ∷-injective (x ≟ᴬ y) (xs ≟ᴸᴬ ys) + _≡?ᴸᴬ_ : (xs ys : List A) → Dec (xs ≡ ys) + [] ≡?ᴸᴬ [] = yes refl + [] ≡?ᴸᴬ (y ∷ ys) = no λ() + (x ∷ xs) ≡?ᴸᴬ [] = no λ() + (x ∷ xs) ≡?ᴸᴬ (y ∷ ys) = ≡?-mapₙ 2 _∷_ ∷-injective (x ≡?ᴬ y) (xs ≡?ᴸᴬ ys) diff --git a/doc/README/Foreign/Haskell.agda b/doc/README/Foreign/Haskell.agda index 38c6c78c4e..e608334197 100644 --- a/doc/README/Foreign/Haskell.agda +++ b/doc/README/Foreign/Haskell.agda @@ -92,12 +92,12 @@ main = run $ do content ← readFiniteFile "README/Foreign/Haskell.agda" let chars = toList content let cleanup = catMaybes ∘ List.map (λ c → if testChar c then just c else nothing) - let cleaned = dropWhile ('\n' ≟_) $ cleanup chars + let cleaned = dropWhile ('\n' ≡?_) $ cleanup chars case uncons cleaned of λ where nothing → putStrLn "I cannot believe this file is filed with dashes only!" (just (c , cs)) → putStrLn $ unlines $ ("First (non dash) character: " ++ Char.show c) - ∷ ("Rest (dash free) of the line: " ++ fromList (takeWhile (¬? ∘ ('\n' ≟_)) cs)) + ∷ ("Rest (dash free) of the line: " ++ fromList (takeWhile (¬? ∘ ('\n' ≡?_)) cs)) ∷ [] -- You can compile and run this test by writing: diff --git a/doc/README/Function/Reasoning.agda b/doc/README/Function/Reasoning.agda index 810f048aa3..7c2d3ed7d0 100644 --- a/doc/README/Function/Reasoning.agda +++ b/doc/README/Function/Reasoning.agda @@ -57,7 +57,7 @@ subpalindromes str = let Chars = List Char in |> filter (λ cs → 2 ≤? length cs) ∶ List Chars -- only keep the ones that are palindromes |> map < fromList , fromList ∘ reverse > ∶ List (String × String) - |> filter (uncurry String._≟_) ∶ List (String × String) + |> filter (uncurry String._≡?_) ∶ List (String × String) |> map proj₁ ∶ List String -- Test cases diff --git a/doc/README/Nary.agda b/doc/README/Nary.agda index b8b337832a..e06c3a8455 100644 --- a/doc/README/Nary.agda +++ b/doc/README/Nary.agda @@ -338,14 +338,14 @@ exist₁ = 19 , 793 , 3059 , 10 , refl -- ∀[_] P = ∀ {a₁} → ⋯ → ∀ {aₙ} → P a₁ ⋯ aₙ all₁ : ∀[ (λ (a₁ a₂ : ℕ) → Dec (a₁ ≡ a₂)) ] -all₁ {a₁} {a₂} = a₁ ≟ a₂ +all₁ {a₁} {a₂} = a₁ ≡? a₂ ------------------------------------------------------------------------ -- Π : (A₁ → ⋯ → Aₙ → Set r) → Set _ -- Π P = ∀ a₁ → ⋯ → ∀ aₙ → P a₁ ⋯ aₙ all₂ : Π[ (λ (a₁ a₂ : ℕ) → Dec (a₁ ≡ a₂)) ] -all₂ = _≟_ +all₂ = _≡?_ ------------------------------------------------------------------------ -- _⇒_ : (A₁ → ⋯ → Aₙ → Set r) → (A₁ → ⋯ → Aₙ → Set s) → (A₁ → ⋯ → Aₙ → Set _) diff --git a/doc/style-guide.md b/doc/style-guide.md index cfecfbd699..2714a94d4c 100644 --- a/doc/style-guide.md +++ b/doc/style-guide.md @@ -586,6 +586,12 @@ word within a compound word is capitalized except for the first word. converse relations are systematically introduced, eg `≥` as `\ge` and `≱` as `\gen`. +* Decidable predicates and relations should typically be written as `R?`, + where `R` is the underlying property being asserted to be `Decidable`, + moreover typically sharing the same fixity and precedence as `R`: thus + - `_≡?_` (at `infix 4`) for `DecidableEquality` + - `_≈?_` (ditto.) for the fieldname of the general `IsDecEquivalence` + * Any exceptions to these conventions should be flagged on the GitHub `agda-stdlib` issue tracker in the usual way. diff --git a/src/Algebra/Construct/LexProduct.agda b/src/Algebra/Construct/LexProduct.agda index 3fbcf86c80..8a4cd45e47 100644 --- a/src/Algebra/Construct/LexProduct.agda +++ b/src/Algebra/Construct/LexProduct.agda @@ -21,7 +21,7 @@ import Relation.Binary.Reasoning.Setoid as ≈-Reasoning module Algebra.Construct.LexProduct {ℓ₁ ℓ₂ ℓ₃ ℓ₄} (M : Magma ℓ₁ ℓ₂) (N : Magma ℓ₃ ℓ₄) - (_≟₁_ : Decidable (Magma._≈_ M)) + (_≈₁?_ : Decidable (Magma._≈_ M)) where open Magma M using (_∙_ ; ∙-cong) @@ -39,7 +39,7 @@ open Magma N using () ; refl to ≈₂-refl ) -import Algebra.Construct.LexProduct.Inner M N _≟₁_ as InnerLex +import Algebra.Construct.LexProduct.Inner M N _≈₁?_ as InnerLex private infix 4 _≋_ @@ -53,7 +53,7 @@ private -- Definition ------------------------------------------------------------------------ -open import Algebra.Construct.LexProduct.Base _∙_ _◦_ _≟₁_ public +open import Algebra.Construct.LexProduct.Base _∙_ _◦_ _≈₁?_ public renaming (lex to _⊕_) ------------------------------------------------------------------------ @@ -103,7 +103,7 @@ identityʳ : ∀ {e f} → RightIdentity _≈₁_ e _∙_ → RightIdentity _≈ identityʳ id₁ id₂ (x , a) = id₁ x , InnerLex.identityʳ id₁ id₂ sel : Selective _≈₁_ _∙_ → Selective _≈₂_ _◦_ → Selective _≋_ _⊕_ -sel ∙-sel ◦-sel (a , x) (b , y) with (a ∙ b) ≟₁ a | (a ∙ b) ≟₁ b +sel ∙-sel ◦-sel (a , x) (b , y) with (a ∙ b) ≈₁? a | (a ∙ b) ≈₁? b ... | no ab≉a | no ab≉b = contradiction₂ (∙-sel a b) ab≉a ab≉b ... | yes ab≈a | no _ = inj₁ (ab≈a , ≈₂-refl) ... | no _ | yes ab≈b = inj₂ (ab≈b , ≈₂-refl) diff --git a/src/Algebra/Construct/LexProduct/Base.agda b/src/Algebra/Construct/LexProduct/Base.agda index 85686fd20c..585c8d730d 100644 --- a/src/Algebra/Construct/LexProduct/Base.agda +++ b/src/Algebra/Construct/LexProduct/Base.agda @@ -16,7 +16,7 @@ open import Relation.Nullary.Decidable.Core using (does; yes; no) module Algebra.Construct.LexProduct.Base {a b ℓ} {A : Set a} {B : Set b} (_∙_ : Op₂ A) (_◦_ : Op₂ B) - {_≈₁_ : Rel A ℓ} (_≟₁_ : Decidable _≈₁_) + {_≈₁_ : Rel A ℓ} (_≈₁?_ : Decidable _≈₁_) where ------------------------------------------------------------------------ @@ -27,7 +27,7 @@ module Algebra.Construct.LexProduct.Base -- operator that only calculates the second component of product. innerLex : A → A → B → B → B -innerLex a b x y with does ((a ∙ b) ≟₁ a) | does ((a ∙ b) ≟₁ b) +innerLex a b x y with does ((a ∙ b) ≈₁? a) | does ((a ∙ b) ≈₁? b) ... | true | false = x ... | false | true = y ... | _ | _ = x ◦ y diff --git a/src/Algebra/Construct/LexProduct/Inner.agda b/src/Algebra/Construct/LexProduct/Inner.agda index beff9e9e3a..b6755e2528 100644 --- a/src/Algebra/Construct/LexProduct/Inner.agda +++ b/src/Algebra/Construct/LexProduct/Inner.agda @@ -21,7 +21,7 @@ import Algebra.Construct.LexProduct.Base as Base module Algebra.Construct.LexProduct.Inner {ℓ₁ ℓ₂ ℓ₃ ℓ₄} (M : Magma ℓ₁ ℓ₂) (N : Magma ℓ₃ ℓ₄) - (_≟₁_ : Decidable (Magma._≈_ M)) + (_≈₁?_ : Decidable (Magma._≈_ M)) where open module M = Magma M @@ -48,7 +48,7 @@ private ------------------------------------------------------------------------ -- Base definition -open Base _∙_ _◦_ _≟₁_ public +open Base _∙_ _◦_ _≈₁?_ public using (innerLex) -- Save ourselves some typing in this file @@ -122,19 +122,19 @@ open SetoidReasoning N.setoid open NaturalOrder case₁ : a ∙ b ≈₁ a → a ∙ b ≉₁ b → lex a b x y ≈₂ x -case₁ {a} {b} ab≈a ab≉b with (a ∙ b) ≟₁ a | (a ∙ b) ≟₁ b +case₁ {a} {b} ab≈a ab≉b with (a ∙ b) ≈₁? a | (a ∙ b) ≈₁? b ... | no ab≉a | _ = contradiction ab≈a ab≉a ... | yes _ | yes ab≈b = contradiction ab≈b ab≉b ... | yes _ | no _ = N.refl case₂ : a ∙ b ≉₁ a → a ∙ b ≈₁ b → lex a b x y ≈₂ y -case₂ {a} {b} ab≉a ab≈b with (a ∙ b) ≟₁ a | (a ∙ b) ≟₁ b +case₂ {a} {b} ab≉a ab≈b with (a ∙ b) ≈₁? a | (a ∙ b) ≈₁? b ... | yes ab≈a | _ = contradiction ab≈a ab≉a ... | no _ | no ab≉b = contradiction ab≈b ab≉b ... | no _ | yes _ = N.refl case₃ : a ∙ b ≈₁ a → a ∙ b ≈₁ b → lex a b x y ≈₂ (x ◦ y) -case₃ {a} {b} ab≈a ab≈b with (a ∙ b) ≟₁ a | (a ∙ b) ≟₁ b +case₃ {a} {b} ab≈a ab≈b with (a ∙ b) ≈₁? a | (a ∙ b) ≈₁? b ... | no ab≉a | _ = contradiction ab≈a ab≉a ... | yes _ | no ab≉b = contradiction ab≈b ab≉b ... | yes _ | yes _ = N.refl @@ -144,7 +144,7 @@ case₃ {a} {b} ab≈a ab≈b with (a ∙ b) ≟₁ a | (a ∙ b) ≟₁ b cong : a ≈₁ b → c ≈₁ d → w ≈₂ x → y ≈₂ z → lex a c w y ≈₂ lex b d x z cong {a} {b} {c} {d} a≈b c≈d w≈x y≈z - with (a ∙ c) ≟₁ a | (a ∙ c) ≟₁ c | (b ∙ d) ≟₁ b | (b ∙ d) ≟₁ d + with (a ∙ c) ≈₁? a | (a ∙ c) ≈₁? c | (b ∙ d) ≈₁? b | (b ∙ d) ≈₁? d ... | yes _ | yes _ | yes _ | yes _ = ◦-cong w≈x y≈z ... | yes _ | yes _ | no _ | no _ = ◦-cong w≈x y≈z ... | no _ | no _ | yes _ | yes _ = ◦-cong w≈x y≈z @@ -172,7 +172,7 @@ assoc : Associative _≈₁_ _∙_ → Commutative _≈₁_ _∙_ → Selective _≈₁_ _∙_ → Associative _≈₂_ _◦_ → ∀ a b c x y z → lex (a ∙ b) c (lex a b x y) z ≈₂ lex a (b ∙ c) x (lex b c y z) assoc ∙-assoc ∙-comm ∙-sel ◦-assoc a b c x y z - with (a ∙ b) ≟₁ a | (a ∙ b) ≟₁ b | (b ∙ c) ≟₁ b | (b ∙ c) ≟₁ c + with (a ∙ b) ≈₁? a | (a ∙ b) ≈₁? b | (b ∙ c) ≈₁? b | (b ∙ c) ≈₁? c ... | _ | _ | no bc≉b | no bc≉c = contradiction₂ (∙-sel b c) bc≉b bc≉c ... | no ab≉a | no ab≉b | _ | _ = contradiction₂ (∙-sel a b) ab≉a ab≉b ... | yes ab≈a | no ab≉b | no bc≉b | yes bc≈c = cong₁₂ ab≈a (M.sym bc≈c) @@ -229,7 +229,7 @@ assoc ∙-assoc ∙-comm ∙-sel ◦-assoc a b c x y z comm : Commutative _≈₁_ _∙_ → Commutative _≈₂_ _◦_ → ∀ a b x y → lex a b x y ≈₂ lex b a y x comm ∙-comm ◦-comm a b x y - with (a ∙ b) ≟₁ a | (a ∙ b) ≟₁ b | (b ∙ a) ≟₁ b | (b ∙ a) ≟₁ a + with (a ∙ b) ≈₁? a | (a ∙ b) ≈₁? b | (b ∙ a) ≈₁? b | (b ∙ a) ≈₁? a ... | yes ab≈a | _ | _ | no ba≉a = contradiction (M.trans (∙-comm b a) ab≈a) ba≉a ... | no ab≉a | _ | _ | yes ba≈a = contradiction (M.trans (∙-comm a b) ba≈a) ab≉a ... | _ | yes ab≈b | no ba≉b | _ = contradiction (M.trans (∙-comm b a) ab≈b) ba≉b @@ -240,7 +240,7 @@ comm ∙-comm ◦-comm a b x y ... | no _ | no _ | no _ | no _ = ◦-comm x y idem : Idempotent _≈₂_ _◦_ → ∀ a b x → lex a b x x ≈₂ x -idem ◦-idem a b x with does ((a ∙ b) ≟₁ a) | does ((a ∙ b) ≟₁ b) +idem ◦-idem a b x with does ((a ∙ b) ≈₁? a) | does ((a ∙ b) ≈₁? b) ... | false | false = ◦-idem x ... | false | true = N.refl ... | true | false = N.refl @@ -248,14 +248,14 @@ idem ◦-idem a b x with does ((a ∙ b) ≟₁ a) | does ((a ∙ b) ≟₁ b) zeroʳ : ∀ {e f} → RightZero _≈₁_ e _∙_ → RightZero _≈₂_ f _◦_ → lex a e x f ≈₂ f -zeroʳ {a} {x} {e} {f} ze₁ ze₂ with (a ∙ e) ≟₁ a | (a ∙ e) ≟₁ e +zeroʳ {a} {x} {e} {f} ze₁ ze₂ with (a ∙ e) ≈₁? a | (a ∙ e) ≈₁? e ... | _ | no a∙e≉e = contradiction (ze₁ a) a∙e≉e ... | no _ | yes _ = N.refl ... | yes _ | yes _ = ze₂ x identityʳ : ∀ {e f} → RightIdentity _≈₁_ e _∙_ → RightIdentity _≈₂_ f _◦_ → lex a e x f ≈₂ x -identityʳ {a} {x} {e} {f} id₁ id₂ with (a ∙ e) ≟₁ a | (a ∙ e) ≟₁ e +identityʳ {a} {x} {e} {f} id₁ id₂ with (a ∙ e) ≈₁? a | (a ∙ e) ≈₁? e ... | no a∙e≉a | _ = contradiction (id₁ a) a∙e≉a ... | yes _ | no _ = N.refl ... | yes _ | yes _ = id₂ x diff --git a/src/Algebra/Properties/CancellativeCommutativeSemiring.agda b/src/Algebra/Properties/CancellativeCommutativeSemiring.agda index 2062c33237..5d696058fd 100644 --- a/src/Algebra/Properties/CancellativeCommutativeSemiring.agda +++ b/src/Algebra/Properties/CancellativeCommutativeSemiring.agda @@ -26,7 +26,7 @@ open import Relation.Binary.Reasoning.Setoid setoid *-almostCancelʳ = comm∧almostCancelˡ⇒almostCancelʳ *-comm *-cancelˡ-nonZero xy≈0⇒x≈0∨y≈0 : Decidable _≈_ → ∀ {x y} → x * y ≈ 0# → x ≈ 0# ⊎ y ≈ 0# -xy≈0⇒x≈0∨y≈0 _≟_ {x} {y} xy≈0 with x ≟ 0# | y ≟ 0# +xy≈0⇒x≈0∨y≈0 _≈?_ {x} {y} xy≈0 with x ≈? 0# | y ≈? 0# ... | yes x≈0 | _ = inj₁ x≈0 ... | no _ | yes y≈0 = inj₂ y≈0 ... | no x≉0 | no y≉0 = contradiction y≈0 y≉0 @@ -35,6 +35,6 @@ xy≈0⇒x≈0∨y≈0 _≟_ {x} {y} xy≈0 with x ≟ 0# | y ≟ 0# y≈0 = *-cancelˡ-nonZero _ y 0# x≉0 xy≈x*0 x≉0∧y≉0⇒xy≉0 : Decidable _≈_ → ∀ {x y} → x ≉ 0# → y ≉ 0# → x * y ≉ 0# -x≉0∧y≉0⇒xy≉0 _≟_ x≉0 y≉0 xy≈0 with xy≈0⇒x≈0∨y≈0 _≟_ xy≈0 +x≉0∧y≉0⇒xy≉0 _≈?_ x≉0 y≉0 xy≈0 with xy≈0⇒x≈0∨y≈0 _≈?_ xy≈0 ... | inj₁ x≈0 = x≉0 x≈0 ... | inj₂ y≈0 = y≉0 y≈0 diff --git a/src/Algebra/Solver/CommutativeMonoid/Normal.agda b/src/Algebra/Solver/CommutativeMonoid/Normal.agda index 7713e497e1..ae564c1f0a 100644 --- a/src/Algebra/Solver/CommutativeMonoid/Normal.agda +++ b/src/Algebra/Solver/CommutativeMonoid/Normal.agda @@ -57,10 +57,10 @@ Normal n = Vec ℕ n -- We can decide if two normal forms are /syntactically/ equal. -infix 5 _≟_ +infix 4 _≡?_ -_≟_ : DecidableEquality (Normal n) -nf₁ ≟ nf₂ = Dec.map Pointwise-≡↔≡ (decidable ℕ._≟_ nf₁ nf₂) +_≡?_ : DecidableEquality (Normal n) +nf₁ ≡? nf₂ = Dec.map Pointwise-≡↔≡ (decidable ℕ._≡?_ nf₁ nf₂) where open Pointwise using (Pointwise-≡↔≡; decidable) ------------------------------------------------------------------------ @@ -162,3 +162,12 @@ sg-correct = singleton-correct "Warning: sg-correct was deprecated in v2.2. Please use singleton-correct instead." #-} + +-- Version 2.4 + +infix 4 _≟_ +_≟_ = _≡?_ +{-# WARNING_ON_USAGE _≟_ +"Warning: _≟_ was deprecated in v2.4. +Please use _≡?_ instead." +#-} diff --git a/src/Algebra/Solver/IdempotentCommutativeMonoid/Normal.agda b/src/Algebra/Solver/IdempotentCommutativeMonoid/Normal.agda index 0ebdf4351d..4c67728c65 100644 --- a/src/Algebra/Solver/IdempotentCommutativeMonoid/Normal.agda +++ b/src/Algebra/Solver/IdempotentCommutativeMonoid/Normal.agda @@ -56,10 +56,10 @@ Normal n = Vec Bool n -- We can decide if two normal forms are /syntactically/ equal. -infix 5 _≟_ +infix 4 _≡?_ -_≟_ : DecidableEquality (Normal n) -nf₁ ≟ nf₂ = Dec.map Pointwise-≡↔≡ (decidable Bool._≟_ nf₁ nf₂) +_≡?_ : DecidableEquality (Normal n) +nf₁ ≡? nf₂ = Dec.map Pointwise-≡↔≡ (decidable Bool._≡?_ nf₁ nf₂) where open Pointwise using (Pointwise-≡↔≡; decidable) ------------------------------------------------------------------------ @@ -167,3 +167,12 @@ sg-correct = singleton-correct "Warning: sg-correct was deprecated in v2.2. Please use singleton-correct instead." #-} + +-- Version 2.4 + +infix 4 _≟_ +_≟_ = _≡?_ +{-# WARNING_ON_USAGE _≟_ +"Warning: _≟_ was deprecated in v2.4. +Please use _≡?_ instead." +#-} diff --git a/src/Algebra/Solver/Monoid/Expression.agda b/src/Algebra/Solver/Monoid/Expression.agda index 7b71c9e9c2..3c28c07ffc 100644 --- a/src/Algebra/Solver/Monoid/Expression.agda +++ b/src/Algebra/Solver/Monoid/Expression.agda @@ -52,14 +52,14 @@ Env n = Vec Carrier n -- API for normal expressions record NormalAPI a : Set (suc a ⊔ c ⊔ ℓ) where - infix 5 _≟_ + infix 4 _≡?_ field -- The type of normal forms. Normal : ℕ → Set a -- We can decide if two normal forms are /syntactically/ equal. - _≟_ : DecidableEquality (Normal n) + _≡?_ : DecidableEquality (Normal n) -- A normaliser. normalise : Expr n → Normal n -- The semantics of a normal form. diff --git a/src/Algebra/Solver/Monoid/Normal.agda b/src/Algebra/Solver/Monoid/Normal.agda index 62a02bfca5..4554873b6e 100644 --- a/src/Algebra/Solver/Monoid/Normal.agda +++ b/src/Algebra/Solver/Monoid/Normal.agda @@ -50,11 +50,11 @@ Normal n = List (Fin n) -- We can decide if two normal forms are /syntactically/ equal. -infix 5 _≟_ +infix 4 _≡?_ -_≟_ : DecidableEquality (Normal n) -nf₁ ≟ nf₂ = Dec.map′ ≋⇒≡ ≡⇒≋ (nf₁ ≋? nf₂) - where open ≋ Fin._≟_ using (_≋?_; ≋⇒≡; ≡⇒≋) +_≡?_ : DecidableEquality (Normal n) +nf₁ ≡? nf₂ = Dec.map′ ≋⇒≡ ≡⇒≋ (nf₁ ≋? nf₂) + where open ≋ Fin._≡?_ using (_≋?_; ≋⇒≡; ≡⇒≋) -- A normaliser. @@ -87,3 +87,20 @@ correct (e₁ ⊕ e₂) ρ = begin ⟦ normalise e₁ ++ normalise e₂ ⟧⇓ ρ ≈⟨ comp-correct (normalise e₁) (normalise e₂) ρ ⟩ ⟦ normalise e₁ ⟧⇓ ρ ∙ ⟦ normalise e₂ ⟧⇓ ρ ≈⟨ ∙-cong (correct e₁ ρ) (correct e₂ ρ) ⟩ ⟦ e₁ ⟧ ρ ∙ ⟦ e₂ ⟧ ρ ∎ + + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.4 + +infix 4 _≟_ + +_≟_ = _≡?_ +{-# WARNING_ON_USAGE _≟_ +"Warning: _≟_ was deprecated in v2.4. +Please use _≡?_ instead." +#-} diff --git a/src/Algebra/Solver/Monoid/Solver.agda b/src/Algebra/Solver/Monoid/Solver.agda index a1281e9639..ab77687ed2 100644 --- a/src/Algebra/Solver/Monoid/Solver.agda +++ b/src/Algebra/Solver/Monoid/Solver.agda @@ -43,7 +43,7 @@ open R public -- for determining if two expressions have the same semantics. prove′ : ∀ e₁ e₂ → Maybe ((ρ : Env n) → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ) -prove′ e₁ e₂ = Maybe.map lemma $ dec⇒weaklyDec _≟_ (normalise e₁) (normalise e₂) +prove′ e₁ e₂ = Maybe.map lemma $ dec⇒weaklyDec _≡?_ (normalise e₁) (normalise e₂) where open import Relation.Binary.Reasoning.Setoid setoid lemma : normalise e₁ ≡ normalise e₂ → ∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ diff --git a/src/Algebra/Solver/Ring/NaturalCoefficients/Default.agda b/src/Algebra/Solver/Ring/NaturalCoefficients/Default.agda index 324f05eb04..89d4ab537b 100644 --- a/src/Algebra/Solver/Ring/NaturalCoefficients/Default.agda +++ b/src/Algebra/Solver/Ring/NaturalCoefficients/Default.agda @@ -18,7 +18,7 @@ module Algebra.Solver.Ring.NaturalCoefficients.Default import Algebra.Properties.Semiring.Mult as SemiringMultiplication using (_×_) open import Data.Maybe.Base using (Maybe; map) -open import Data.Nat using (_≟_) +open import Data.Nat using (_≡?_) open import Relation.Binary.Consequences using (dec⇒weaklyDec) import Relation.Binary.PropositionalEquality.Core as ≡ using (refl; cong) @@ -27,6 +27,6 @@ open SemiringMultiplication semiring private dec : ∀ m n → Maybe (m × 1# ≈ n × 1#) - dec m n = map (λ { ≡.refl → refl }) (dec⇒weaklyDec _≟_ m n) + dec m n = map (λ { ≡.refl → refl }) (dec⇒weaklyDec _≡?_ m n) open import Algebra.Solver.Ring.NaturalCoefficients R dec public diff --git a/src/Axiom/UniquenessOfIdentityProofs.agda b/src/Axiom/UniquenessOfIdentityProofs.agda index 752b9c444d..cb1ec76231 100644 --- a/src/Axiom/UniquenessOfIdentityProofs.agda +++ b/src/Axiom/UniquenessOfIdentityProofs.agda @@ -66,14 +66,14 @@ module Constant⇒UIP -- function over proofs of equality which is constant: it returns the -- proof produced by the decision procedure. -module Decidable⇒UIP (_≟_ : DecidableEquality A) +module Decidable⇒UIP (_≡?_ : DecidableEquality A) where ≡-normalise : _≡_ {A = A} ⇒ _≡_ - ≡-normalise {x} {y} x≡y = recompute (x ≟ y) x≡y + ≡-normalise {x} {y} x≡y = recompute (x ≡? y) x≡y ≡-normalise-constant : (p q : x ≡ y) → ≡-normalise p ≡ ≡-normalise q - ≡-normalise-constant {x = x} {y = y} = recompute-constant (x ≟ y) + ≡-normalise-constant {x = x} {y = y} = recompute-constant (x ≡? y) ≡-irrelevant : UIP A ≡-irrelevant = Constant⇒UIP.≡-irrelevant ≡-normalise ≡-normalise-constant diff --git a/src/Data/Bool.agda b/src/Data/Bool.agda index 55ed146e2c..0ead2d50b2 100644 --- a/src/Data/Bool.agda +++ b/src/Data/Bool.agda @@ -17,4 +17,4 @@ open import Data.Bool.Base public -- Publicly re-export queries open import Data.Bool.Properties public - using (T?; _≟_; _≤?_; _-weakInduction {n = n} P Pₙ Pᵢ₊₁⇒Pᵢ i = induct (>-wellFounded i) where induct : ∀ {i} → Acc _>_ i → P i - induct {i} (acc rec) with n ℕ.≟ toℕ i + induct {i} (acc rec) with n ℕ.≡? toℕ i ... | yes n≡i = subst P (toℕ-injective (trans (toℕ-fromℕ n) n≡i)) Pₙ ... | no n≢i = subst P (inject₁-lower₁ i n≢i) (Pᵢ₊₁⇒Pᵢ _ Pᵢ₊₁) where Pᵢ₊₁ = induct (rec (ℕ.≤-reflexive (cong suc (sym (toℕ-lower₁ i n≢i))))) diff --git a/src/Data/Fin/Permutation.agda b/src/Data/Fin/Permutation.agda index 078e53c3bb..ef3dd75cf2 100644 --- a/src/Data/Fin/Permutation.agda +++ b/src/Data/Fin/Permutation.agda @@ -12,7 +12,7 @@ open import Data.Bool.Base using (true; false) open import Data.Fin.Base using (Fin; suc; cast; opposite; punchIn; punchOut) open import Data.Fin.Patterns using (0F; 1F) open import Data.Fin.Properties - using (¬Fin0; _≟_; ≟-≡-refl; ≟-≢ + using (¬Fin0; _≡?_; ≡?-≡-refl; ≡?-≢ ; cast-involutive; opposite-involutive ; punchInᵢ≢i; punchOut-punchIn; punchIn-punchOut ; punchOut-cong; punchOut-cong′) @@ -218,21 +218,21 @@ insert : ∀ {m n} → Fin (suc m) → Fin (suc n) → Permutation m n → Permu insert {m} {n} i j π = permutation to from inverseˡ′ inverseʳ′ where to : Fin (suc m) → Fin (suc n) - to k with i ≟ k + to k with i ≡? k ... | yes i≡k = j ... | no i≢k = punchIn j (π ⟨$⟩ʳ punchOut i≢k) from : Fin (suc n) → Fin (suc m) - from k with j ≟ k + from k with j ≡? k ... | yes j≡k = i ... | no j≢k = punchIn i (π ⟨$⟩ˡ punchOut j≢k) inverseʳ′ : StrictlyInverseʳ _≡_ to from - inverseʳ′ k with i ≟ k - ... | yes i≡k rewrite ≟-≡-refl j = i≡k + inverseʳ′ k with i ≡? k + ... | yes i≡k rewrite ≡?-≡-refl j = i≡k ... | no i≢k with j≢punchInⱼπʳpunchOuti≢k ← punchInᵢ≢i j (π ⟨$⟩ʳ punchOut i≢k) ∘ sym - rewrite ≟-≢ j≢punchInⱼπʳpunchOuti≢k + rewrite ≡?-≢ j≢punchInⱼπʳpunchOuti≢k = begin punchIn i (π ⟨$⟩ˡ punchOut j≢punchInⱼπʳpunchOuti≢k) ≡⟨ cong (λ l → punchIn i (π ⟨$⟩ˡ l)) (punchOut-cong j refl) ⟩ punchIn i (π ⟨$⟩ˡ punchOut (punchInᵢ≢i j (π ⟨$⟩ʳ punchOut i≢k) ∘ sym)) ≡⟨ cong (λ l → punchIn i (π ⟨$⟩ˡ l)) (punchOut-punchIn j) ⟩ @@ -241,11 +241,11 @@ insert {m} {n} i j π = permutation to from inverseˡ′ inverseʳ′ k ∎ inverseˡ′ : StrictlyInverseˡ _≡_ to from - inverseˡ′ k with j ≟ k - ... | yes j≡k rewrite ≟-≡-refl i = j≡k + inverseˡ′ k with j ≡? k + ... | yes j≡k rewrite ≡?-≡-refl i = j≡k ... | no j≢k with i≢punchInᵢπˡpunchOutj≢k ← punchInᵢ≢i i (π ⟨$⟩ˡ punchOut j≢k) ∘ sym - rewrite ≟-≢ i≢punchInᵢπˡpunchOutj≢k + rewrite ≡?-≢ i≢punchInᵢπˡpunchOutj≢k = begin punchIn j (π ⟨$⟩ʳ punchOut i≢punchInᵢπˡpunchOutj≢k) ≡⟨ cong (λ l → punchIn j (π ⟨$⟩ʳ l)) (punchOut-cong i refl) ⟩ punchIn j (π ⟨$⟩ʳ punchOut (punchInᵢ≢i i (π ⟨$⟩ˡ punchOut j≢k) ∘ sym)) ≡⟨ cong (λ l → punchIn j (π ⟨$⟩ʳ l)) (punchOut-punchIn i) ⟩ @@ -317,14 +317,14 @@ lift₀-cong π ρ f (suc i) = cong suc (f i) lift₀-transpose : ∀ (i j : Fin n) → transpose (suc i) (suc j) ≈ lift₀ (transpose i j) lift₀-transpose i j 0F = refl -lift₀-transpose i j (suc k) with does (k ≟ i) +lift₀-transpose i j (suc k) with does (k ≡? i) ... | true = refl -... | false with does (k ≟ j) +... | false with does (k ≡? j) ... | false = refl ... | true = refl insert-punchIn : ∀ i j (π : Permutation m n) k → insert i j π ⟨$⟩ʳ punchIn i k ≡ punchIn j (π ⟨$⟩ʳ k) -insert-punchIn i j π k with i ≟ punchIn i k +insert-punchIn i j π k with i ≡? punchIn i k ... | yes i≡punchInᵢk = contradiction (sym i≡punchInᵢk) (punchInᵢ≢i i k) ... | no i≢punchInᵢk = begin punchIn j (π ⟨$⟩ʳ punchOut i≢punchInᵢk) ≡⟨ cong (λ l → punchIn j (π ⟨$⟩ʳ l)) (punchOut-cong i refl) ⟩ @@ -332,7 +332,7 @@ insert-punchIn i j π k with i ≟ punchIn i k punchIn j (π ⟨$⟩ʳ k) ∎ insert-remove : ∀ i (π : Permutation (suc m) (suc n)) → insert i (π ⟨$⟩ʳ i) (remove i π) ≈ π -insert-remove {m = m} {n = n} i π j with i ≟ j +insert-remove {m = m} {n = n} i π j with i ≡? j ... | yes i≡j = cong (π ⟨$⟩ʳ_) i≡j ... | no i≢j = begin punchIn (π ⟨$⟩ʳ i) (punchOut (punchInᵢ≢i i (punchOut i≢j) ∘ sym ∘ Injection.injective (↔⇒↣ π))) ≡⟨ punchIn-punchOut _ ⟩ @@ -340,7 +340,7 @@ insert-remove {m = m} {n = n} i π j with i ≟ j π ⟨$⟩ʳ j ∎ remove-insert : ∀ i j (π : Permutation m n) → remove i (insert i j π) ≈ π -remove-insert i j π k rewrite ≟-≡-refl i = begin +remove-insert i j π k rewrite ≡?-≡-refl i = begin punchOut {i = j} _ ≡⟨ punchOut-cong j (insert-punchIn i j π k) ⟩ punchOut {i = j} (punchInᵢ≢i j (π ⟨$⟩ʳ k) ∘ sym) ≡⟨ punchOut-punchIn j ⟩ π ⟨$⟩ʳ k ∎ diff --git a/src/Data/Fin/Permutation/Components.agda b/src/Data/Fin/Permutation/Components.agda index b8597674f8..f536a37519 100644 --- a/src/Data/Fin/Permutation/Components.agda +++ b/src/Data/Fin/Permutation/Components.agda @@ -11,7 +11,7 @@ module Data.Fin.Permutation.Components where open import Data.Bool.Base using (Bool; true; false) open import Data.Fin.Base using (Fin; suc; opposite; toℕ) open import Data.Fin.Properties - using (_≟_; ≟-≡; ≟-≡-refl + using (_≡?_; ≡?-≡; ≡?-≡-refl ; opposite-prop; opposite-involutive; opposite-suc) open import Relation.Nullary.Decidable.Core using (does; yes; no) open import Relation.Binary.PropositionalEquality.Core @@ -24,9 +24,9 @@ open import Relation.Binary.PropositionalEquality.Core -- 'transpose i j' swaps the places of 'i' and 'j'. transpose : ∀ {n} → Fin n → Fin n → Fin n → Fin n -transpose i j k with does (k ≟ i) +transpose i j k with does (k ≡? i) ... | true = j -... | false with does (k ≟ j) +... | false with does (k ≡? j) ... | true = i ... | false = k @@ -35,25 +35,25 @@ transpose i j k with does (k ≟ i) ------------------------------------------------------------------------ transpose[i,i,j]≡j : ∀ {n} (i j : Fin n) → transpose i i j ≡ j -transpose[i,i,j]≡j i j with j ≟ i in j≟i +transpose[i,i,j]≡j i j with j ≡? i in j≡?i ... | yes j≡i = sym j≡i -... | no _ rewrite j≟i = refl +... | no _ rewrite j≡?i = refl transpose[i,j,j]≡i : ∀ {n} (i j : Fin n) → transpose i j j ≡ i -transpose[i,j,j]≡i i j with j ≟ i +transpose[i,j,j]≡i i j with j ≡? i ... | yes j≡i = j≡i -... | no _ rewrite ≟-≡-refl j = refl +... | no _ rewrite ≡?-≡-refl j = refl transpose[i,j,i]≡j : ∀ {n} (i j : Fin n) → transpose i j i ≡ j -transpose[i,j,i]≡j i j rewrite ≟-≡-refl i = refl +transpose[i,j,i]≡j i j rewrite ≡?-≡-refl i = refl transpose-transpose : ∀ {n} {i j k l : Fin n} → transpose i j k ≡ l → transpose j i l ≡ k -transpose-transpose {n} {i} {j} {k} {l} eq with k ≟ i in k≟i -... | yes k≡i rewrite ≟-≡ (sym eq) = sym k≡i -... | no k≢i with k ≟ j in k≟j +transpose-transpose {n} {i} {j} {k} {l} eq with k ≡? i in k≡?i +... | yes k≡i rewrite ≡?-≡ (sym eq) = sym k≡i +... | no k≢i with k ≡? j in k≡?j ... | yes k≡j rewrite eq | transpose[i,j,j]≡i j l = sym k≡j -... | no k≢j rewrite eq | k≟j | k≟i = refl +... | no k≢j rewrite eq | k≡?j | k≡?i = refl transpose-inverse : ∀ {n} (i j : Fin n) {k} → transpose i j (transpose j i k) ≡ k diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index ec5767c34c..6f0d9dab42 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -46,7 +46,7 @@ open import Relation.Binary.PropositionalEquality.Core as ≡ open import Relation.Binary.PropositionalEquality.Properties as ≡ using (module ≡-Reasoning) open import Relation.Binary.PropositionalEquality as ≡ - using (≡-≟-identity; ≢-≟-identity) + using (≡-≡?-identity; ≢-≡?-identity) open import Relation.Nullary.Decidable as Dec using (Dec; _because_; yes; no; _×?_; _⊎?_; map′; decidable-stable) open import Relation.Nullary.Negation.Core @@ -97,25 +97,25 @@ nonZeroIndex {n = suc _} _ = _ suc-injective : Fin.suc i ≡ suc j → i ≡ j suc-injective refl = refl -infix 4 _≟_ +infix 4 _≡?_ -_≟_ : DecidableEquality (Fin n) -zero ≟ zero = yes refl -zero ≟ suc y = no λ() -suc x ≟ zero = no λ() -suc x ≟ suc y = map′ (cong suc) suc-injective (x ≟ y) +_≡?_ : DecidableEquality (Fin n) +zero ≡? zero = yes refl +zero ≡? suc y = no λ() +suc x ≡? zero = no λ() +suc x ≡? suc y = map′ (cong suc) suc-injective (x ≡? y) ≡-irrelevant : Irrelevant {A = Fin n} _≡_ -≡-irrelevant = Decidable⇒UIP.≡-irrelevant _≟_ +≡-irrelevant = Decidable⇒UIP.≡-irrelevant _≡?_ -≟-≡ : (eq : i ≡ j) → (i ≟ j) ≡ yes eq -≟-≡ = ≡-≟-identity _≟_ +≡?-≡ : (eq : i ≡ j) → (i ≡? j) ≡ yes eq +≡?-≡ = ≡-≡?-identity _≡?_ -≟-≡-refl : (i : Fin n) → (i ≟ i) ≡ yes refl -≟-≡-refl _ = ≟-≡ refl +≡?-≡-refl : (i : Fin n) → (i ≡? i) ≡ yes refl +≡?-≡-refl _ = ≡?-≡ refl -≟-≢ : (i≢j : i ≢ j) → (i ≟ j) ≡ no i≢j -≟-≢ = ≢-≟-identity _≟_ +≡?-≢ : (i≢j : i ≢ j) → (i ≡? j) ≡ no i≢j +≡?-≢ = ≢-≡?-identity _≡?_ ------------------------------------------------------------------------ -- Structures @@ -123,7 +123,7 @@ suc x ≟ suc y = map′ (cong suc) suc-injective (x ≟ y) ≡-isDecEquivalence : IsDecEquivalence {A = Fin n} _≡_ ≡-isDecEquivalence = record { isEquivalence = ≡.isEquivalence - ; _≟_ = _≟_ + ; _≈?_ = _≡?_ } ------------------------------------------------------------------------ @@ -356,7 +356,7 @@ m ?_ ; ≤-<-connex ; ≥->-connex ; <-≤-connex ; >-≥-connex diff --git a/src/Data/Nat/Binary/Instances.agda b/src/Data/Nat/Binary/Instances.agda index 9ef0ef6373..f8c56ebc38 100644 --- a/src/Data/Nat/Binary/Instances.agda +++ b/src/Data/Nat/Binary/Instances.agda @@ -8,9 +8,9 @@ module Data.Nat.Binary.Instances where -open import Data.Nat.Binary.Properties +open import Data.Nat.Binary.Properties using (_≡?_) open import Relation.Binary.PropositionalEquality.Properties using (isDecEquivalence) instance - ℕᵇ-≡-isDecEquivalence = isDecEquivalence _≟_ + ℕᵇ-≡-isDecEquivalence = isDecEquivalence _≡?_ diff --git a/src/Data/Nat/Binary/Properties.agda b/src/Data/Nat/Binary/Properties.agda index 6c2298d88a..79ca4687d2 100644 --- a/src/Data/Nat/Binary/Properties.agda +++ b/src/Data/Nat/Binary/Properties.agda @@ -61,7 +61,7 @@ private variable x : ℕᵇ -infix 4 _0 mod≢0) mod≤1+j , j≤k)) divₕ-offsetEq d (suc n) (suc j) (suc k) j≤d k≤d (inj₃ (eq , k (m≮n ∘ <⇒<ᵇ) m≢n (≤∧≢⇒< (≮⇒≥ (m≮n ∘ <⇒<ᵇ)) (m≢n ∘ sym)) @@ -2323,7 +2326,7 @@ _>‴?_ = flip _<‴?_ -- decidable equality. eq? : ∀ {a} {A : Set a} → A ↣ ℕ → DecidableEquality A -eq? inj = via-injection inj _≟_ +eq? inj = via-injection inj _≡?_ -- It's possible to decide existential and universal predicates up to -- a limit. @@ -2338,7 +2341,7 @@ module _ {p} {P : Pred ℕ p} (P? : U.Decidable P) where ... | no ¬Pv | no ¬Pn>= λ y′ → ♭ x >>= λ y″ → f y′ y″) ≳⟨ idem (♭ x) ⟩≅ (♭ x >>= λ y′ → f y′ y′) ∎)) + + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.4 + +_≟-Kind_ = _≡?-Kind_ +{-# WARNING_ON_USAGE _≟-Kind_ +"Warning: _≟-Kind_ was deprecated in v2.4. +Please use _≡?-Kind_ instead." +#-} diff --git a/src/Reflection.agda b/src/Reflection.agda index fd3476cebb..64aa468c25 100644 --- a/src/Reflection.agda +++ b/src/Reflection.agda @@ -48,46 +48,46 @@ Please use Reflection.AST.Argument.Information's ArgInfo instead." infix 4 _≟-Lit_ _≟-Name_ _≟-Meta_ _≟-Visibility_ _≟-Relevance_ _≟-Arg-info_ _≟-Pattern_ _≟-ArgPatterns_ -_≟-Lit_ = Literal._≟_ +_≟-Lit_ = Literal._≡?_ {-# WARNING_ON_USAGE _≟-Lit_ "Warning: _≟-Lit_ was deprecated in v1.3. -Please use Reflection.AST.Literal's _≟_ instead." +Please use Reflection.AST.Literal's _≡?_ instead." #-} -_≟-Name_ = Name._≟_ +_≟-Name_ = Name._≡?_ {-# WARNING_ON_USAGE _≟-Name_ "Warning: _≟-Name_ was deprecated in v1.3. -Please use Reflection.AST.Name's _≟_ instead." +Please use Reflection.AST.Name's _≡?_ instead." #-} -_≟-Meta_ = Meta._≟_ +_≟-Meta_ = Meta._≡?_ {-# WARNING_ON_USAGE _≟-Meta_ "Warning: _≟-Meta_ was deprecated in v1.3. -Please use Reflection.AST.Meta's _≟_ instead." +Please use Reflection.AST.Meta's _≡?_ instead." #-} -_≟-Visibility_ = Visibility._≟_ +_≟-Visibility_ = Visibility._≡?_ {-# WARNING_ON_USAGE _≟-Visibility_ "Warning: _≟-Visibility_ was deprecated in v1.3. -Please use Reflection.AST.Argument.Visibility's _≟_ instead." +Please use Reflection.AST.Argument.Visibility's _≡?_ instead." #-} -_≟-Relevance_ = Relevance._≟_ +_≟-Relevance_ = Relevance._≡?_ {-# WARNING_ON_USAGE _≟-Relevance_ "Warning: _≟-Relevance_ was deprecated in v1.3. -Please use Reflection.AST.Argument.Relevance's _≟_ instead." +Please use Reflection.AST.Argument.Relevance's _≡?_ instead." #-} -_≟-Arg-info_ = Information._≟_ +_≟-Arg-info_ = Information._≡?_ {-# WARNING_ON_USAGE _≟-Arg-info_ "Warning: _≟-Arg-info_ was deprecated in v1.3. -Please use Reflection.AST.Argument.Information's _≟_ instead." +Please use Reflection.AST.Argument.Information's _≡?_ instead." #-} -_≟-Pattern_ = Pattern._≟_ +_≟-Pattern_ = Pattern._≡?_ {-# WARNING_ON_USAGE _≟-Pattern_ "Warning: _≟-Pattern_ was deprecated in v1.3. -Please use Reflection.AST.Pattern's _≟_ instead." +Please use Reflection.AST.Pattern's _≡?_ instead." #-} _≟-ArgPatterns_ = Pattern._≟s_ @@ -130,56 +130,56 @@ infix 4 _≟-AbsTerm_ _≟-AbsType_ _≟-ArgTerm_ _≟-ArgType_ _≟-Args_ _≟-Clause_ _≟-Clauses_ _≟_ _≟-Sort_ -_≟-AbsTerm_ = Term._≟-AbsTerm_ +_≟-AbsTerm_ = Term._≡?-AbsTerm_ {-# WARNING_ON_USAGE _≟-AbsTerm_ "Warning: _≟-AbsTerm_ was deprecated in v1.3. -Please use Reflection.AST.Term's _≟-AbsTerm_ instead." +Please use Reflection.AST.Term's _≡?-AbsTerm_ instead." #-} -_≟-AbsType_ = Term._≟-AbsType_ +_≟-AbsType_ = Term._≡?-AbsType_ {-# WARNING_ON_USAGE _≟-AbsType_ "Warning: _≟-AbsType_ was deprecated in v1.3. -Please use Reflection.AST.Term's _≟-AbsType_ instead." +Please use Reflection.AST.Term's _≡?-AbsType_ instead." #-} -_≟-ArgTerm_ = Term._≟-ArgTerm_ +_≟-ArgTerm_ = Term._≡?-ArgTerm_ {-# WARNING_ON_USAGE _≟-ArgTerm_ "Warning: _≟-ArgTerm_ was deprecated in v1.3. -Please use Reflection.AST.Term's _≟-ArgTerm_ instead." +Please use Reflection.AST.Term's _≡?-ArgTerm_ instead." #-} -_≟-ArgType_ = Term._≟-ArgType_ +_≟-ArgType_ = Term._≡?-ArgType_ {-# WARNING_ON_USAGE _≟-ArgType_ "Warning: _≟-ArgType_ was deprecated in v1.3. -Please use Reflection.AST.Term's _≟-ArgType_ instead." +Please use Reflection.AST.Term's _≡?-ArgType_ instead." #-} -_≟-Args_ = Term._≟-Args_ +_≟-Args_ = Term._≡?-Args_ {-# WARNING_ON_USAGE _≟-Args_ "Warning: _≟-Args_ was deprecated in v1.3. -Please use Reflection.AST.Term's _≟-Args_ instead." +Please use Reflection.AST.Term's _≡?-Args_ instead." #-} -_≟-Clause_ = Term._≟-Clause_ +_≟-Clause_ = Term._≡?-Clause_ {-# WARNING_ON_USAGE _≟-Clause_ "Warning: _≟-Clause_ was deprecated in v1.3. -Please use Reflection.AST.Term's _≟-Clause_ instead." +Please use Reflection.AST.Term's _≡?-Clause_ instead." #-} -_≟-Clauses_ = Term._≟-Clauses_ +_≟-Clauses_ = Term._≡?-Clauses_ {-# WARNING_ON_USAGE _≟-Clauses_ "Warning: _≟-Clauses_ was deprecated in v1.3. -Please use Reflection.AST.Term's _≟-Clauses_ instead." +Please use Reflection.AST.Term's _≡?-Clauses_ instead." #-} -_≟_ = Term._≟_ +_≟_ = Term._≡?_ {-# WARNING_ON_USAGE _≟_ "Warning: _≟_ was deprecated in v1.3. -Please use Reflection.AST.Term's _≟_ instead." +Please use Reflection.AST.Term's _≡?_ instead." #-} -_≟-Sort_ = Term._≟-Sort_ +_≟-Sort_ = Term._≡?-Sort_ {-# WARNING_ON_USAGE _≟-Sort_ "Warning: _≟-Sort_ was deprecated in v1.3. -Please use Reflection.AST.Term's _≟-Sort_ instead." +Please use Reflection.AST.Term's _≡?-Sort_ instead." #-} diff --git a/src/Reflection/AST/Abstraction.agda b/src/Reflection/AST/Abstraction.agda index e91ae8d00c..3084ca87a2 100644 --- a/src/Reflection/AST/Abstraction.agda +++ b/src/Reflection/AST/Abstraction.agda @@ -9,7 +9,7 @@ module Reflection.AST.Abstraction where open import Data.String.Base as String using (String) -open import Data.String.Properties as String using (_≟_) +open import Data.String.Properties as String using (_≡?_) open import Data.Product.Base using (_×_; <_,_>; uncurry) open import Level using (Level) open import Relation.Nullary.Decidable.Core using (Dec; map′; _×?_) @@ -58,8 +58,8 @@ unAbs : Abs A → A unAbs (abs s a) = a unAbs-dec : {abs1 abs2 : Abs A} → Dec (unAbs abs1 ≡ unAbs abs2) → Dec (abs1 ≡ abs2) -unAbs-dec {abs1 = abs s a} {abs t a′} a≟a′ = - map′ (uncurry (cong₂ abs)) abs-injective (s String.≟ t ×? a≟a′) +unAbs-dec {abs1 = abs s a} {abs t a′} a≡?a′ = + map′ (uncurry (cong₂ abs)) abs-injective (s String.≡? t ×? a≡?a′) ≡-dec : DecidableEquality A → DecidableEquality (Abs A) -≡-dec _≟_ x y = unAbs-dec (unAbs x ≟ unAbs y) +≡-dec _≡?_ x y = unAbs-dec (unAbs x ≡? unAbs y) diff --git a/src/Reflection/AST/AlphaEquality.agda b/src/Reflection/AST/AlphaEquality.agda index fc2e3bfcd5..dc9a7d3e5f 100644 --- a/src/Reflection/AST/AlphaEquality.agda +++ b/src/Reflection/AST/AlphaEquality.agda @@ -44,8 +44,8 @@ open AlphaEquality {{...}} public ------------------------------------------------------------------------ -- Utilities -≟⇒α : DecidableEquality A → AlphaEquality A -≟⇒α _≟_ = mkAlphaEquality (λ x y → ⌊ x ≟ y ⌋) +≡?⇒α : DecidableEquality A → AlphaEquality A +≡?⇒α _≡?_ = mkAlphaEquality (λ x y → ⌊ x ≡? y ⌋) ------------------------------------------------------------------------ -- Propositional cases @@ -55,22 +55,22 @@ open AlphaEquality {{...}} public instance α-Visibility : AlphaEquality Visibility - α-Visibility = ≟⇒α Visibility._≟_ + α-Visibility = ≡?⇒α Visibility._≡?_ α-Modality : AlphaEquality Modality - α-Modality = ≟⇒α Modality._≟_ + α-Modality = ≡?⇒α Modality._≡?_ α-ArgInfo : AlphaEquality ArgInfo - α-ArgInfo = ≟⇒α ArgInfo._≟_ + α-ArgInfo = ≡?⇒α ArgInfo._≡?_ α-Literal : AlphaEquality Literal - α-Literal = ≟⇒α Literal._≟_ + α-Literal = ≡?⇒α Literal._≡?_ α-Meta : AlphaEquality Meta - α-Meta = ≟⇒α Meta._≟_ + α-Meta = ≡?⇒α Meta._≡?_ α-Name : AlphaEquality Name - α-Name = ≟⇒α Name._≟_ + α-Name = ≡?⇒α Name._≡?_ ------------------------------------------------------------------------ -- Interesting cases @@ -344,3 +344,18 @@ instance α-ArgsPattern : AlphaEquality (Args Pattern) α-ArgsPattern = mkAlphaEquality _=α=-ArgsPattern_ + + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.4 + +≟⇒α = ≡?⇒α +{-# WARNING_ON_USAGE ≟⇒α +"Warning: ≟⇒α was deprecated in v2.4. +Please use ≡?⇒α instead." +#-} diff --git a/src/Reflection/AST/Argument.agda b/src/Reflection/AST/Argument.agda index 9fd29e7330..5582e5b4a9 100644 --- a/src/Reflection/AST/Argument.agda +++ b/src/Reflection/AST/Argument.agda @@ -86,7 +86,7 @@ unArg (arg i a) = a unArg-dec : {arg1 arg2 : Arg A} → Dec (unArg arg1 ≡ unArg arg2) → Dec (arg1 ≡ arg2) unArg-dec {arg1 = arg i x} {arg j y} arg1≟arg2 = - map′ (uncurry (cong₂ arg)) arg-injective (i Information.≟ j ×? arg1≟arg2) + map′ (uncurry (cong₂ arg)) arg-injective (i Information.≡? j ×? arg1≟arg2) ≡-dec : DecidableEquality A → DecidableEquality (Arg A) -≡-dec _≟_ x y = unArg-dec (unArg x ≟ unArg y) +≡-dec _≡?_ x y = unArg-dec (unArg x ≡? unArg y) diff --git a/src/Reflection/AST/Argument/Information.agda b/src/Reflection/AST/Argument/Information.agda index 307a1b1976..6940c3c492 100644 --- a/src/Reflection/AST/Argument/Information.agda +++ b/src/Reflection/AST/Argument/Information.agda @@ -47,11 +47,27 @@ 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 _≟_ +infix 4 _≡?_ -_≟_ : DecidableEquality ArgInfo -arg-info v m ≟ arg-info v′ m′ = +_≡?_ : DecidableEquality ArgInfo +arg-info v m ≡? arg-info v′ m′ = map′ (uncurry (cong₂ arg-info)) arg-info-injective - (v Visibility.≟ v′ ×? m Modality.≟ m′) + (v Visibility.≡? v′ ×? m Modality.≡? m′) + + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.4 + +infix 4 _≟_ +_≟_ = _≡?_ +{-# WARNING_ON_USAGE _≟_ +"Warning: _≟_ was deprecated in v2.4. +Please use _≡?_ instead." +#-} diff --git a/src/Reflection/AST/Argument/Modality.agda b/src/Reflection/AST/Argument/Modality.agda index e71b0f2710..61886cad95 100644 --- a/src/Reflection/AST/Argument/Modality.agda +++ b/src/Reflection/AST/Argument/Modality.agda @@ -47,11 +47,28 @@ modality-injective₂ refl = refl modality-injective : modality r q ≡ modality r′ q′ → r ≡ r′ × q ≡ q′ modality-injective = < modality-injective₁ , modality-injective₂ > -infix 4 _≟_ +infix 4 _≡?_ -_≟_ : DecidableEquality Modality -modality r q ≟ modality r′ q′ = +_≡?_ : DecidableEquality Modality +modality r q ≡? modality r′ q′ = map′ (uncurry (cong₂ modality)) modality-injective - (r Relevance.≟ r′ ×? q Quantity.≟ q′) + (r Relevance.≡? r′ ×? q Quantity.≡? q′) + + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.4 + +infix 4 _≟_ + +_≟_ = _≡?_ +{-# WARNING_ON_USAGE _≟_ +"Warning: _≟_ was deprecated in v2.4. +Please use _≡?_ instead." +#-} diff --git a/src/Reflection/AST/Argument/Quantity.agda b/src/Reflection/AST/Argument/Quantity.agda index a042218660..6d1a0a7fc2 100644 --- a/src/Reflection/AST/Argument/Quantity.agda +++ b/src/Reflection/AST/Argument/Quantity.agda @@ -21,10 +21,27 @@ open Quantity public ------------------------------------------------------------------------ -- Decidable equality +infix 4 _≡?_ + +_≡?_ : DecidableEquality Quantity +quantity-ω ≡? quantity-ω = yes refl +quantity-0 ≡? quantity-0 = yes refl +quantity-ω ≡? quantity-0 = no λ() +quantity-0 ≡? quantity-ω = no λ() + + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.4 + infix 4 _≟_ -_≟_ : DecidableEquality Quantity -quantity-ω ≟ quantity-ω = yes refl -quantity-0 ≟ quantity-0 = yes refl -quantity-ω ≟ quantity-0 = no λ() -quantity-0 ≟ quantity-ω = no λ() +_≟_ = _≡?_ +{-# WARNING_ON_USAGE _≟_ +"Warning: _≟_ was deprecated in v2.4. +Please use _≡?_ instead." +#-} diff --git a/src/Reflection/AST/Argument/Relevance.agda b/src/Reflection/AST/Argument/Relevance.agda index a06095dc8b..c4020c350e 100644 --- a/src/Reflection/AST/Argument/Relevance.agda +++ b/src/Reflection/AST/Argument/Relevance.agda @@ -21,10 +21,27 @@ open Relevance public ------------------------------------------------------------------------ -- Decidable equality +infix 4 _≡?_ + +_≡?_ : DecidableEquality Relevance +relevant ≡? relevant = yes refl +irrelevant ≡? irrelevant = yes refl +relevant ≡? irrelevant = no λ() +irrelevant ≡? relevant = no λ() + + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.4 + infix 4 _≟_ -_≟_ : DecidableEquality Relevance -relevant ≟ relevant = yes refl -irrelevant ≟ irrelevant = yes refl -relevant ≟ irrelevant = no λ() -irrelevant ≟ relevant = no λ() +_≟_ = _≡?_ +{-# WARNING_ON_USAGE _≟_ +"Warning: _≟_ was deprecated in v2.4. +Please use _≡?_ instead." +#-} diff --git a/src/Reflection/AST/Argument/Visibility.agda b/src/Reflection/AST/Argument/Visibility.agda index db68cb4b27..35f7133346 100644 --- a/src/Reflection/AST/Argument/Visibility.agda +++ b/src/Reflection/AST/Argument/Visibility.agda @@ -21,15 +21,31 @@ open Visibility public ------------------------------------------------------------------------ -- Decidable equality -infix 4 _≟_ +infix 4 _≡?_ + +_≡?_ : DecidableEquality Visibility +visible ≡? visible = yes refl +hidden ≡? hidden = yes refl +instance′ ≡? instance′ = yes refl +visible ≡? hidden = no λ() +visible ≡? instance′ = no λ() +hidden ≡? visible = no λ() +hidden ≡? instance′ = no λ() +instance′ ≡? visible = no λ() +instance′ ≡? hidden = no λ() + + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. -_≟_ : DecidableEquality Visibility -visible ≟ visible = yes refl -hidden ≟ hidden = yes refl -instance′ ≟ instance′ = yes refl -visible ≟ hidden = no λ() -visible ≟ instance′ = no λ() -hidden ≟ visible = no λ() -hidden ≟ instance′ = no λ() -instance′ ≟ visible = no λ() -instance′ ≟ hidden = no λ() +-- Version 2.4 + +infix 4 _≟_ +_≟_ = _≡?_ +{-# WARNING_ON_USAGE _≟_ +"Warning: _≟_ was deprecated in v2.4. +Please use _≡?_ instead." +#-} diff --git a/src/Reflection/AST/Definition.agda b/src/Reflection/AST/Definition.agda index 400499afd3..75c9447bec 100644 --- a/src/Reflection/AST/Definition.agda +++ b/src/Reflection/AST/Definition.agda @@ -9,15 +9,15 @@ module Reflection.AST.Definition where import Data.List.Properties as List using (≡-dec) -import Data.Nat.Properties as ℕ using (_≟_) +import Data.Nat.Properties as ℕ using (_≡?_) open import Data.Product.Base using (_×_; <_,_>; uncurry) open import Relation.Nullary.Decidable.Core using (map′; _×?_; yes; no) open import Relation.Binary.Definitions using (DecidableEquality) open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong; cong₂) import Reflection.AST.Argument as Arg using (Arg; ≡-dec) -import Reflection.AST.Argument.Quantity as Quantity using (Quantity; _≟_) -import Reflection.AST.Name as Name using (Name; _≟_) -import Reflection.AST.Term as Term using (Term; _≟-Clauses_) +import Reflection.AST.Argument.Quantity as Quantity using (Quantity; _≡?_) +import Reflection.AST.Name as Name using (Name; _≡?_) +import Reflection.AST.Term as Term using (Term; _≡?-Clauses_) ------------------------------------------------------------------------ -- Re-exporting type publicly @@ -65,51 +65,51 @@ constructor′-injective₂ refl = refl constructor′-injective : ∀ {c c′ q q′} → constructor′ c q ≡ constructor′ c′ q′ → c ≡ c′ × q ≡ q′ constructor′-injective = < constructor′-injective₁ , constructor′-injective₂ > -infix 4 _≟_ +infix 4 _≡?_ -_≟_ : DecidableEquality Definition -function cs ≟ function cs′ = - map′ (cong function) function-injective (cs Term.≟-Clauses cs′) -data-type pars cs ≟ data-type pars′ cs′ = +_≡?_ : DecidableEquality Definition +function cs ≡? function cs′ = + map′ (cong function) function-injective (cs Term.≡?-Clauses cs′) +data-type pars cs ≡? data-type pars′ cs′ = map′ (uncurry (cong₂ data-type)) data-type-injective - (pars ℕ.≟ pars′ ×? List.≡-dec Name._≟_ cs cs′) -record′ c fs ≟ record′ c′ fs′ = + (pars ℕ.≡? pars′ ×? List.≡-dec Name._≡?_ cs cs′) +record′ c fs ≡? record′ c′ fs′ = map′ (uncurry (cong₂ record′)) record′-injective - (c Name.≟ c′ ×? List.≡-dec (Arg.≡-dec Name._≟_) fs fs′) -constructor′ d q ≟ constructor′ d′ q′ = + (c Name.≡? c′ ×? List.≡-dec (Arg.≡-dec Name._≡?_) fs fs′) +constructor′ d q ≡? constructor′ d′ q′ = map′ (uncurry (cong₂ constructor′)) constructor′-injective - (d Name.≟ d′ ×? q Quantity.≟ q′) -axiom ≟ axiom = yes refl -primitive′ ≟ primitive′ = yes refl + (d Name.≡? d′ ×? q Quantity.≡? q′) +axiom ≡? axiom = yes refl +primitive′ ≡? primitive′ = yes refl -- antidiagonal -function cs ≟ data-type pars cs₁ = no (λ ()) -function cs ≟ record′ c fs = no (λ ()) -function cs ≟ constructor′ d q = no (λ ()) -function cs ≟ axiom = no (λ ()) -function cs ≟ primitive′ = no (λ ()) -data-type pars cs ≟ function cs₁ = no (λ ()) -data-type pars cs ≟ record′ c fs = no (λ ()) -data-type pars cs ≟ constructor′ d q = no (λ ()) -data-type pars cs ≟ axiom = no (λ ()) -data-type pars cs ≟ primitive′ = no (λ ()) -record′ c fs ≟ function cs = no (λ ()) -record′ c fs ≟ data-type pars cs = no (λ ()) -record′ c fs ≟ constructor′ d q = no (λ ()) -record′ c fs ≟ axiom = no (λ ()) -record′ c fs ≟ primitive′ = no (λ ()) -constructor′ d q ≟ function cs = no (λ ()) -constructor′ d q ≟ data-type pars cs = no (λ ()) -constructor′ d q ≟ record′ c fs = no (λ ()) -constructor′ d q ≟ axiom = no (λ ()) -constructor′ d q ≟ primitive′ = no (λ ()) -axiom ≟ function cs = no (λ ()) -axiom ≟ data-type pars cs = no (λ ()) -axiom ≟ record′ c fs = no (λ ()) -axiom ≟ constructor′ d q = no (λ ()) -axiom ≟ primitive′ = no (λ ()) -primitive′ ≟ function cs = no (λ ()) -primitive′ ≟ data-type pars cs = no (λ ()) -primitive′ ≟ record′ c fs = no (λ ()) -primitive′ ≟ constructor′ d q = no (λ ()) -primitive′ ≟ axiom = no (λ ()) +function cs ≡? data-type pars cs₁ = no (λ ()) +function cs ≡? record′ c fs = no (λ ()) +function cs ≡? constructor′ d q = no (λ ()) +function cs ≡? axiom = no (λ ()) +function cs ≡? primitive′ = no (λ ()) +data-type pars cs ≡? function cs₁ = no (λ ()) +data-type pars cs ≡? record′ c fs = no (λ ()) +data-type pars cs ≡? constructor′ d q = no (λ ()) +data-type pars cs ≡? axiom = no (λ ()) +data-type pars cs ≡? primitive′ = no (λ ()) +record′ c fs ≡? function cs = no (λ ()) +record′ c fs ≡? data-type pars cs = no (λ ()) +record′ c fs ≡? constructor′ d q = no (λ ()) +record′ c fs ≡? axiom = no (λ ()) +record′ c fs ≡? primitive′ = no (λ ()) +constructor′ d q ≡? function cs = no (λ ()) +constructor′ d q ≡? data-type pars cs = no (λ ()) +constructor′ d q ≡? record′ c fs = no (λ ()) +constructor′ d q ≡? axiom = no (λ ()) +constructor′ d q ≡? primitive′ = no (λ ()) +axiom ≡? function cs = no (λ ()) +axiom ≡? data-type pars cs = no (λ ()) +axiom ≡? record′ c fs = no (λ ()) +axiom ≡? constructor′ d q = no (λ ()) +axiom ≡? primitive′ = no (λ ()) +primitive′ ≡? function cs = no (λ ()) +primitive′ ≡? data-type pars cs = no (λ ()) +primitive′ ≡? record′ c fs = no (λ ()) +primitive′ ≡? constructor′ d q = no (λ ()) +primitive′ ≡? axiom = no (λ ()) diff --git a/src/Reflection/AST/Instances.agda b/src/Reflection/AST/Instances.agda index 27a766076d..8d0971d71d 100644 --- a/src/Reflection/AST/Instances.agda +++ b/src/Reflection/AST/Instances.agda @@ -33,20 +33,20 @@ private A : Set a instance - Lit-≡-isDecEquivalence = isDecEquivalence Literal._≟_ - Name-≡-isDecEquivalence = isDecEquivalence Name._≟_ - Meta-≡-isDecEquivalence = isDecEquivalence Meta._≟_ - Visibility-≡-isDecEquivalence = isDecEquivalence Visibility._≟_ - Relevance-≡-isDecEquivalence = isDecEquivalence Relevance._≟_ - Quantity-≡-isDecEquivalence = isDecEquivalence Quantity._≟_ - ArgInfo-≡-isDecEquivalence = isDecEquivalence Information._≟_ - Pattern-≡-isDecEquivalence = isDecEquivalence Pattern._≟_ - Clause-≡-isDecEquivalence = isDecEquivalence Term._≟-Clause_ - Term-≡-isDecEquivalence = isDecEquivalence Term._≟_ - Sort-≡-isDecEquivalence = isDecEquivalence Term._≟-Sort_ + Lit-≡-isDecEquivalence = isDecEquivalence Literal._≡?_ + Name-≡-isDecEquivalence = isDecEquivalence Name._≡?_ + Meta-≡-isDecEquivalence = isDecEquivalence Meta._≡?_ + Visibility-≡-isDecEquivalence = isDecEquivalence Visibility._≡?_ + Relevance-≡-isDecEquivalence = isDecEquivalence Relevance._≡?_ + Quantity-≡-isDecEquivalence = isDecEquivalence Quantity._≡?_ + ArgInfo-≡-isDecEquivalence = isDecEquivalence Information._≡?_ + Pattern-≡-isDecEquivalence = isDecEquivalence Pattern._≡?_ + Clause-≡-isDecEquivalence = isDecEquivalence Term._≡?-Clause_ + Term-≡-isDecEquivalence = isDecEquivalence Term._≡?_ + Sort-≡-isDecEquivalence = isDecEquivalence Term._≡?-Sort_ Abs-≡-isDecEquivalence : {{IsDecEquivalence {A = A} _≡_}} → IsDecEquivalence {A = Abstraction.Abs A} _≡_ - Abs-≡-isDecEquivalence = isDecEquivalence (Abstraction.≡-dec _≟_) + Abs-≡-isDecEquivalence = isDecEquivalence (Abstraction.≡-dec _≈?_) Arg-≡-isDecEquivalence : {{IsDecEquivalence {A = A} _≡_}} → IsDecEquivalence {A = Argument.Arg A} _≡_ - Arg-≡-isDecEquivalence = isDecEquivalence (Argument.≡-dec _≟_) + Arg-≡-isDecEquivalence = isDecEquivalence (Argument.≡-dec _≈?_) diff --git a/src/Reflection/AST/Literal.agda b/src/Reflection/AST/Literal.agda index 9048e75ede..27e7c87816 100644 --- a/src/Reflection/AST/Literal.agda +++ b/src/Reflection/AST/Literal.agda @@ -51,59 +51,74 @@ string-injective refl = refl name-injective : ∀ {x y} → name x ≡ name y → x ≡ y name-injective refl = refl -infix 4 _≟_ -_≟_ : DecidableEquality Literal -nat x ≟ nat x₁ = map′ (cong nat) nat-injective (x ℕ.≟ x₁) -nat x ≟ word64 x₁ = no (λ ()) -nat x ≟ float x₁ = no (λ ()) -nat x ≟ char x₁ = no (λ ()) -nat x ≟ string x₁ = no (λ ()) -nat x ≟ name x₁ = no (λ ()) -nat x ≟ meta x₁ = no (λ ()) -word64 x ≟ word64 x₁ = map′ (cong word64) word64-injective (x Word64.≟ x₁) -word64 x ≟ nat x₁ = no (λ ()) -word64 x ≟ float x₁ = no (λ ()) -word64 x ≟ char x₁ = no (λ ()) -word64 x ≟ string x₁ = no (λ ()) -word64 x ≟ name x₁ = no (λ ()) -word64 x ≟ meta x₁ = no (λ ()) -float x ≟ nat x₁ = no (λ ()) -float x ≟ word64 x₁ = no (λ ()) -float x ≟ float x₁ = map′ (cong float) float-injective (x Float.≟ x₁) -float x ≟ char x₁ = no (λ ()) -float x ≟ string x₁ = no (λ ()) -float x ≟ name x₁ = no (λ ()) -float x ≟ meta x₁ = no (λ ()) -char x ≟ nat x₁ = no (λ ()) -char x ≟ word64 x₁ = no (λ ()) -char x ≟ float x₁ = no (λ ()) -char x ≟ char x₁ = map′ (cong char) char-injective (x Char.≟ x₁) -char x ≟ string x₁ = no (λ ()) -char x ≟ name x₁ = no (λ ()) -char x ≟ meta x₁ = no (λ ()) -string x ≟ nat x₁ = no (λ ()) -string x ≟ word64 x₁ = no (λ ()) -string x ≟ float x₁ = no (λ ()) -string x ≟ char x₁ = no (λ ()) -string x ≟ string x₁ = map′ (cong string) string-injective (x String.≟ x₁) -string x ≟ name x₁ = no (λ ()) -string x ≟ meta x₁ = no (λ ()) -name x ≟ nat x₁ = no (λ ()) -name x ≟ word64 x₁ = no (λ ()) -name x ≟ float x₁ = no (λ ()) -name x ≟ char x₁ = no (λ ()) -name x ≟ string x₁ = no (λ ()) -name x ≟ name x₁ = map′ (cong name) name-injective (x Name.≟ x₁) -name x ≟ meta x₁ = no (λ ()) -meta x ≟ nat x₁ = no (λ ()) -meta x ≟ word64 x₁ = no (λ ()) -meta x ≟ float x₁ = no (λ ()) -meta x ≟ char x₁ = no (λ ()) -meta x ≟ string x₁ = no (λ ()) -meta x ≟ name x₁ = no (λ ()) -meta x ≟ meta x₁ = map′ (cong meta) meta-injective (x Meta.≟ x₁) +infix 4 _≡?_ +_≡?_ : DecidableEquality Literal +nat x ≡? nat x₁ = map′ (cong nat) nat-injective (x ℕ.≡? x₁) +nat x ≡? word64 x₁ = no (λ ()) +nat x ≡? float x₁ = no (λ ()) +nat x ≡? char x₁ = no (λ ()) +nat x ≡? string x₁ = no (λ ()) +nat x ≡? name x₁ = no (λ ()) +nat x ≡? meta x₁ = no (λ ()) +word64 x ≡? word64 x₁ = map′ (cong word64) word64-injective (x Word64.≡? x₁) +word64 x ≡? nat x₁ = no (λ ()) +word64 x ≡? float x₁ = no (λ ()) +word64 x ≡? char x₁ = no (λ ()) +word64 x ≡? string x₁ = no (λ ()) +word64 x ≡? name x₁ = no (λ ()) +word64 x ≡? meta x₁ = no (λ ()) +float x ≡? nat x₁ = no (λ ()) +float x ≡? word64 x₁ = no (λ ()) +float x ≡? float x₁ = map′ (cong float) float-injective (x Float.≡? x₁) +float x ≡? char x₁ = no (λ ()) +float x ≡? string x₁ = no (λ ()) +float x ≡? name x₁ = no (λ ()) +float x ≡? meta x₁ = no (λ ()) +char x ≡? nat x₁ = no (λ ()) +char x ≡? word64 x₁ = no (λ ()) +char x ≡? float x₁ = no (λ ()) +char x ≡? char x₁ = map′ (cong char) char-injective (x Char.≡? x₁) +char x ≡? string x₁ = no (λ ()) +char x ≡? name x₁ = no (λ ()) +char x ≡? meta x₁ = no (λ ()) +string x ≡? nat x₁ = no (λ ()) +string x ≡? word64 x₁ = no (λ ()) +string x ≡? float x₁ = no (λ ()) +string x ≡? char x₁ = no (λ ()) +string x ≡? string x₁ = map′ (cong string) string-injective (x String.≡? x₁) +string x ≡? name x₁ = no (λ ()) +string x ≡? meta x₁ = no (λ ()) +name x ≡? nat x₁ = no (λ ()) +name x ≡? word64 x₁ = no (λ ()) +name x ≡? float x₁ = no (λ ()) +name x ≡? char x₁ = no (λ ()) +name x ≡? string x₁ = no (λ ()) +name x ≡? name x₁ = map′ (cong name) name-injective (x Name.≡? x₁) +name x ≡? meta x₁ = no (λ ()) +meta x ≡? nat x₁ = no (λ ()) +meta x ≡? word64 x₁ = no (λ ()) +meta x ≡? float x₁ = no (λ ()) +meta x ≡? char x₁ = no (λ ()) +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′) +l ≡ᵇ l′ = isYes (l ≡? l′) + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.4 + +infix 4 _≟_ +_≟_ = _≡?_ +{-# WARNING_ON_USAGE _≟_ +"Warning: _≟_ was deprecated in v2.4. +Please use _≡?_ instead." +#-} diff --git a/src/Reflection/AST/Meta.agda b/src/Reflection/AST/Meta.agda index bef152149f..4aaa009fa1 100644 --- a/src/Reflection/AST/Meta.agda +++ b/src/Reflection/AST/Meta.agda @@ -8,7 +8,7 @@ module Reflection.AST.Meta where -import Data.Nat.Properties as ℕ using (_≟_) +import Data.Nat.Properties as ℕ using (_≡?_) open import Function.Base using (_on_) open import Relation.Nullary.Decidable.Core using (map′) open import Relation.Binary.Core using (Rel) @@ -24,13 +24,29 @@ open import Agda.Builtin.Reflection.Properties public -- Equality of metas is decidable. -infix 4 _≈?_ _≟_ _≈_ +infix 4 _≈?_ _≡?_ _≈_ _≈_ : Rel Meta _ _≈_ = _≡_ on toℕ _≈?_ : Decidable _≈_ -_≈?_ = On.decidable toℕ _≡_ ℕ._≟_ +_≈?_ = On.decidable toℕ _≡_ ℕ._≡?_ -_≟_ : DecidableEquality Meta -m ≟ n = map′ (toℕ-injective _ _) (cong toℕ) (m ≈? n) +_≡?_ : DecidableEquality Meta +m ≡? n = map′ (toℕ-injective _ _) (cong toℕ) (m ≈? n) + + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.4 + +infix 4 _≟_ +_≟_ = _≡?_ +{-# WARNING_ON_USAGE _≟_ +"Warning: _≟_ was deprecated in v2.4. +Please use _≡?_ instead." +#-} diff --git a/src/Reflection/AST/Name.agda b/src/Reflection/AST/Name.agda index 867d14bd6e..055d5df0d1 100644 --- a/src/Reflection/AST/Name.agda +++ b/src/Reflection/AST/Name.agda @@ -10,7 +10,7 @@ module Reflection.AST.Name where open import Data.List.Base using (List) import Data.Product.Properties as Prodₚ using (≡-dec) -import Data.Word64.Properties as Wₚ using (_≟_) +import Data.Word64.Properties as Wₚ using (_≡?_) open import Function.Base using (_on_) open import Relation.Nullary.Decidable.Core using (map′) open import Relation.Binary.Core using (Rel) @@ -38,13 +38,29 @@ Names = List Name -- Decidable equality for names ------------------------------------------------------------------------ -infix 4 _≈?_ _≟_ _≈_ +infix 4 _≈?_ _≡?_ _≈_ _≈_ : Rel Name _ _≈_ = _≡_ on toWords _≈?_ : Decidable _≈_ -_≈?_ = decidable toWords _≡_ (Prodₚ.≡-dec Wₚ._≟_ Wₚ._≟_) +_≈?_ = decidable toWords _≡_ (Prodₚ.≡-dec Wₚ._≡?_ Wₚ._≡?_) -_≟_ : DecidableEquality Name -m ≟ n = map′ (toWords-injective _ _) (cong toWords) (m ≈? n) +_≡?_ : DecidableEquality Name +m ≡? n = map′ (toWords-injective _ _) (cong toWords) (m ≈? n) + + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.4 + +infix 4 _≟_ +_≟_ = _≡?_ +{-# WARNING_ON_USAGE _≟_ +"Warning: _≟_ was deprecated in v2.4. +Please use _≡?_ instead." +#-} diff --git a/src/Reflection/AST/Pattern.agda b/src/Reflection/AST/Pattern.agda index 814baf1038..ea8e41899f 100644 --- a/src/Reflection/AST/Pattern.agda +++ b/src/Reflection/AST/Pattern.agda @@ -24,6 +24,6 @@ open import Reflection.AST.Term public ; pat-con-injective to con-injective ; pat-var-injective to var-injective ; pat-lit-injective to lit-injective - ; _≟-Patterns_ to _≟s_ - ; _≟-Pattern_ to _≟_ + ; _≡?-Patterns_ to _≟s_ + ; _≡?-Pattern_ to _≡?_ ) diff --git a/src/Reflection/AST/Term.agda b/src/Reflection/AST/Term.agda index 0a1b9e3b53..9a3dc369b5 100644 --- a/src/Reflection/AST/Term.agda +++ b/src/Reflection/AST/Term.agda @@ -11,21 +11,21 @@ module Reflection.AST.Term where open import Data.List.Base as List hiding (_++_) open import Data.List.Properties using (∷-dec) open import Data.Nat.Base using (ℕ; zero; suc) -import Data.Nat.Properties as ℕ using (_≟_) +import Data.Nat.Properties as ℕ using (_≡?_) open import Data.Product.Base using (_×_; _,_; <_,_>; uncurry; map₁) open import Data.Product.Properties using (,-injective) open import Data.Maybe.Base using (Maybe; just; nothing) open import Data.String.Base using (String) -open import Data.String.Properties as String hiding (_≟_) +open import Data.String.Properties as String hiding (_≟_; _≡?_) open import Relation.Nullary.Decidable using (map′; _×?_; yes; no) open import Relation.Binary.Definitions using (Decidable; DecidableEquality) open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong; cong₂) open import Reflection.AST.Abstraction using (Abs; abs; unAbs-dec) open import Reflection.AST.Argument as Arg open import Reflection.AST.Argument.Information using (visibility) -open import Reflection.AST.Argument.Visibility as Visibility hiding (_≟_) -import Reflection.AST.Literal as Literal using (Literal; _≟_) -import Reflection.AST.Meta as Meta using (Meta; _≟_) +open import Reflection.AST.Argument.Visibility as Visibility hiding (_≟_; _≡?_) +import Reflection.AST.Literal as Literal using (Literal; _≡?_) +import Reflection.AST.Meta as Meta using (Meta; _≡?_) open import Reflection.AST.Name as Name using (Name) ------------------------------------------------------------------------ @@ -127,60 +127,60 @@ absurd-clause-injective₂ refl = refl absurd-clause-injective : ∀ {tel tel′ ps ps′} → absurd-clause tel ps ≡ absurd-clause tel′ ps′ → tel ≡ tel′ × ps ≡ ps′ absurd-clause-injective = < absurd-clause-injective₁ , absurd-clause-injective₂ > -infix 4 _≟-AbsTerm_ _≟-AbsType_ _≟-ArgTerm_ _≟-ArgType_ _≟-Args_ - _≟-Clause_ _≟-Clauses_ _≟_ - _≟-Sort_ _≟-Pattern_ _≟-Patterns_ _≟-Telescope_ - -_≟-AbsTerm_ : DecidableEquality (Abs Term) -_≟-AbsType_ : DecidableEquality (Abs Type) -_≟-ArgTerm_ : DecidableEquality (Arg Term) -_≟-ArgType_ : DecidableEquality (Arg Type) -_≟-Args_ : DecidableEquality (Args Term) -_≟-Clause_ : DecidableEquality Clause -_≟-Clauses_ : DecidableEquality Clauses -_≟_ : DecidableEquality Term -_≟-Sort_ : DecidableEquality Sort -_≟-Patterns_ : DecidableEquality (Args Pattern) -_≟-Pattern_ : DecidableEquality Pattern +infix 4 _≡?-AbsTerm_ _≡?-AbsType_ _≡?-ArgTerm_ _≡?-ArgType_ _≡?-Args_ + _≡?-Clause_ _≡?-Clauses_ _≡?_ + _≡?-Sort_ _≡?-Pattern_ _≡?-Patterns_ _≡?-Telescope_ + +_≡?-AbsTerm_ : DecidableEquality (Abs Term) +_≡?-AbsType_ : DecidableEquality (Abs Type) +_≡?-ArgTerm_ : DecidableEquality (Arg Term) +_≡?-ArgType_ : DecidableEquality (Arg Type) +_≡?-Args_ : DecidableEquality (Args Term) +_≡?-Clause_ : DecidableEquality Clause +_≡?-Clauses_ : DecidableEquality Clauses +_≡?_ : DecidableEquality Term +_≡?-Sort_ : DecidableEquality Sort +_≡?-Patterns_ : DecidableEquality (Args Pattern) +_≡?-Pattern_ : DecidableEquality Pattern -- Decidable equality 'transformers' -- We need to inline these because the terms are not sized so -- termination would not obvious if we were to use higher-order -- functions such as Data.List.Properties' ≡-dec -abs s a ≟-AbsTerm abs s′ a′ = unAbs-dec (a ≟ a′) -abs s a ≟-AbsType abs s′ a′ = unAbs-dec (a ≟ a′) -arg i a ≟-ArgTerm arg i′ a′ = unArg-dec (a ≟ a′) -arg i a ≟-ArgType arg i′ a′ = unArg-dec (a ≟ a′) - -[] ≟-Args [] = yes refl -(x ∷ xs) ≟-Args (y ∷ ys) = ∷-dec (x ≟-ArgTerm y) (xs ≟-Args ys) -[] ≟-Args (_ ∷ _) = no λ() -(_ ∷ _) ≟-Args [] = no λ() - -[] ≟-Clauses [] = yes refl -(x ∷ xs) ≟-Clauses (y ∷ ys) = ∷-dec (x ≟-Clause y) (xs ≟-Clauses ys) -[] ≟-Clauses (_ ∷ _) = no λ() -(_ ∷ _) ≟-Clauses [] = no λ() - -_≟-Telescope_ : DecidableEquality Telescope -[] ≟-Telescope [] = yes refl -((x , t) ∷ tel) ≟-Telescope ((x′ , t′) ∷ tel′) = ∷-dec - (map′ (uncurry (cong₂ _,_)) ,-injective ((x String.≟ x′) ×? (t ≟-ArgTerm t′))) - (tel ≟-Telescope tel′) -[] ≟-Telescope (_ ∷ _) = no λ () -(_ ∷ _) ≟-Telescope [] = no λ () - -clause tel ps b ≟-Clause clause tel′ ps′ b′ = +abs s a ≡?-AbsTerm abs s′ a′ = unAbs-dec (a ≡? a′) +abs s a ≡?-AbsType abs s′ a′ = unAbs-dec (a ≡? a′) +arg i a ≡?-ArgTerm arg i′ a′ = unArg-dec (a ≡? a′) +arg i a ≡?-ArgType arg i′ a′ = unArg-dec (a ≡? a′) + +[] ≡?-Args [] = yes refl +(x ∷ xs) ≡?-Args (y ∷ ys) = ∷-dec (x ≡?-ArgTerm y) (xs ≡?-Args ys) +[] ≡?-Args (_ ∷ _) = no λ() +(_ ∷ _) ≡?-Args [] = no λ() + +[] ≡?-Clauses [] = yes refl +(x ∷ xs) ≡?-Clauses (y ∷ ys) = ∷-dec (x ≡?-Clause y) (xs ≡?-Clauses ys) +[] ≡?-Clauses (_ ∷ _) = no λ() +(_ ∷ _) ≡?-Clauses [] = no λ() + +_≡?-Telescope_ : DecidableEquality Telescope +[] ≡?-Telescope [] = yes refl +((x , t) ∷ tel) ≡?-Telescope ((x′ , t′) ∷ tel′) = ∷-dec + (map′ (uncurry (cong₂ _,_)) ,-injective ((x String.≡? x′) ×? (t ≡?-ArgTerm t′))) + (tel ≡?-Telescope tel′) +[] ≡?-Telescope (_ ∷ _) = no λ () +(_ ∷ _) ≡?-Telescope [] = no λ () + +clause tel ps b ≡?-Clause clause tel′ ps′ b′ = map′ (λ (tel≡tel′ , ps≡ps′ , b≡b′) → cong₂ (uncurry clause) (cong₂ _,_ tel≡tel′ ps≡ps′) b≡b′) clause-injective - (tel ≟-Telescope tel′ ×? ps ≟-Patterns ps′ ×? b ≟ b′) -absurd-clause tel ps ≟-Clause absurd-clause tel′ ps′ = + (tel ≡?-Telescope tel′ ×? ps ≡?-Patterns ps′ ×? b ≡? b′) +absurd-clause tel ps ≡?-Clause absurd-clause tel′ ps′ = map′ (uncurry (cong₂ absurd-clause)) absurd-clause-injective - (tel ≟-Telescope tel′ ×? ps ≟-Patterns ps′) -clause _ _ _ ≟-Clause absurd-clause _ _ = no λ() -absurd-clause _ _ ≟-Clause clause _ _ _ = no λ() + (tel ≡?-Telescope tel′ ×? ps ≡?-Patterns ps′) +clause _ _ _ ≡?-Clause absurd-clause _ _ = no λ() +absurd-clause _ _ ≡?-Clause clause _ _ _ = no λ() var-injective₁ : ∀ {x x′ args args′} → Term.var x args ≡ var x′ args′ → x ≡ x′ var-injective₁ refl = refl @@ -266,151 +266,151 @@ propLit-injective refl = refl inf-injective : ∀ {x y} → inf x ≡ inf y → x ≡ y inf-injective refl = refl -var x args ≟ var x′ args′ = - map′ (uncurry (cong₂ var)) var-injective (x ℕ.≟ x′ ×? args ≟-Args args′) -con c args ≟ con c′ args′ = - map′ (uncurry (cong₂ con)) con-injective (c Name.≟ c′ ×? args ≟-Args args′) -def f args ≟ def f′ args′ = - map′ (uncurry (cong₂ def)) def-injective (f Name.≟ f′ ×? args ≟-Args args′) -meta x args ≟ meta x′ args′ = - map′ (uncurry (cong₂ meta)) meta-injective (x Meta.≟ x′ ×? args ≟-Args args′) -lam v t ≟ lam v′ t′ = - map′ (uncurry (cong₂ lam)) lam-injective (v Visibility.≟ v′ ×? t ≟-AbsTerm t′) -pat-lam cs args ≟ pat-lam cs′ args′ = - map′ (uncurry (cong₂ pat-lam)) pat-lam-injective (cs ≟-Clauses cs′ ×? args ≟-Args args′) -pi t₁ t₂ ≟ pi t₁′ t₂′ = - map′ (uncurry (cong₂ pi)) pi-injective (t₁ ≟-ArgType t₁′ ×? t₂ ≟-AbsType t₂′) -sort s ≟ sort s′ = map′ (cong sort) sort-injective (s ≟-Sort s′) -lit l ≟ lit l′ = map′ (cong lit) lit-injective (l Literal.≟ l′) -unknown ≟ unknown = yes refl - -var x args ≟ con c args′ = no λ() -var x args ≟ def f args′ = no λ() -var x args ≟ lam v t = no λ() -var x args ≟ pi t₁ t₂ = no λ() -var x args ≟ sort _ = no λ() -var x args ≟ lit _ = no λ() -var x args ≟ meta _ _ = no λ() -var x args ≟ unknown = no λ() -con c args ≟ var x args′ = no λ() -con c args ≟ def f args′ = no λ() -con c args ≟ lam v t = no λ() -con c args ≟ pi t₁ t₂ = no λ() -con c args ≟ sort _ = no λ() -con c args ≟ lit _ = no λ() -con c args ≟ meta _ _ = no λ() -con c args ≟ unknown = no λ() -def f args ≟ var x args′ = no λ() -def f args ≟ con c args′ = no λ() -def f args ≟ lam v t = no λ() -def f args ≟ pi t₁ t₂ = no λ() -def f args ≟ sort _ = no λ() -def f args ≟ lit _ = no λ() -def f args ≟ meta _ _ = no λ() -def f args ≟ unknown = no λ() -lam v t ≟ var x args = no λ() -lam v t ≟ con c args = no λ() -lam v t ≟ def f args = no λ() -lam v t ≟ pi t₁ t₂ = no λ() -lam v t ≟ sort _ = no λ() -lam v t ≟ lit _ = no λ() -lam v t ≟ meta _ _ = no λ() -lam v t ≟ unknown = no λ() -pi t₁ t₂ ≟ var x args = no λ() -pi t₁ t₂ ≟ con c args = no λ() -pi t₁ t₂ ≟ def f args = no λ() -pi t₁ t₂ ≟ lam v t = no λ() -pi t₁ t₂ ≟ sort _ = no λ() -pi t₁ t₂ ≟ lit _ = no λ() -pi t₁ t₂ ≟ meta _ _ = no λ() -pi t₁ t₂ ≟ unknown = no λ() -sort _ ≟ var x args = no λ() -sort _ ≟ con c args = no λ() -sort _ ≟ def f args = no λ() -sort _ ≟ lam v t = no λ() -sort _ ≟ pi t₁ t₂ = no λ() -sort _ ≟ lit _ = no λ() -sort _ ≟ meta _ _ = no λ() -sort _ ≟ unknown = no λ() -lit _ ≟ var x args = no λ() -lit _ ≟ con c args = no λ() -lit _ ≟ def f args = no λ() -lit _ ≟ lam v t = no λ() -lit _ ≟ pi t₁ t₂ = no λ() -lit _ ≟ sort _ = no λ() -lit _ ≟ meta _ _ = no λ() -lit _ ≟ unknown = no λ() -meta _ _ ≟ var x args = no λ() -meta _ _ ≟ con c args = no λ() -meta _ _ ≟ def f args = no λ() -meta _ _ ≟ lam v t = no λ() -meta _ _ ≟ pi t₁ t₂ = no λ() -meta _ _ ≟ sort _ = no λ() -meta _ _ ≟ lit _ = no λ() -meta _ _ ≟ unknown = no λ() -unknown ≟ var x args = no λ() -unknown ≟ con c args = no λ() -unknown ≟ def f args = no λ() -unknown ≟ lam v t = no λ() -unknown ≟ pi t₁ t₂ = no λ() -unknown ≟ sort _ = no λ() -unknown ≟ lit _ = no λ() -unknown ≟ meta _ _ = no λ() -pat-lam _ _ ≟ var x args = no λ() -pat-lam _ _ ≟ con c args = no λ() -pat-lam _ _ ≟ def f args = no λ() -pat-lam _ _ ≟ lam v t = no λ() -pat-lam _ _ ≟ pi t₁ t₂ = no λ() -pat-lam _ _ ≟ sort _ = no λ() -pat-lam _ _ ≟ lit _ = no λ() -pat-lam _ _ ≟ meta _ _ = no λ() -pat-lam _ _ ≟ unknown = no λ() -var x args ≟ pat-lam _ _ = no λ() -con c args ≟ pat-lam _ _ = no λ() -def f args ≟ pat-lam _ _ = no λ() -lam v t ≟ pat-lam _ _ = no λ() -pi t₁ t₂ ≟ pat-lam _ _ = no λ() -sort _ ≟ pat-lam _ _ = no λ() -lit _ ≟ pat-lam _ _ = no λ() -meta _ _ ≟ pat-lam _ _ = no λ() -unknown ≟ pat-lam _ _ = no λ() - -set t ≟-Sort set t′ = map′ (cong set) set-injective (t ≟ t′) -lit n ≟-Sort lit n′ = map′ (cong lit) slit-injective (n ℕ.≟ n′) -prop t ≟-Sort prop t′ = map′ (cong prop) prop-injective (t ≟ t′) -propLit n ≟-Sort propLit n′ = map′ (cong propLit) propLit-injective (n ℕ.≟ n′) -inf n ≟-Sort inf n′ = map′ (cong inf) inf-injective (n ℕ.≟ n′) -unknown ≟-Sort unknown = yes refl -set _ ≟-Sort lit _ = no λ() -set _ ≟-Sort prop _ = no λ() -set _ ≟-Sort propLit _ = no λ() -set _ ≟-Sort inf _ = no λ() -set _ ≟-Sort unknown = no λ() -lit _ ≟-Sort set _ = no λ() -lit _ ≟-Sort prop _ = no λ() -lit _ ≟-Sort propLit _ = no λ() -lit _ ≟-Sort inf _ = no λ() -lit _ ≟-Sort unknown = no λ() -prop _ ≟-Sort set _ = no λ() -prop _ ≟-Sort lit _ = no λ() -prop _ ≟-Sort propLit _ = no λ() -prop _ ≟-Sort inf _ = no λ() -prop _ ≟-Sort unknown = no λ() -propLit _ ≟-Sort set _ = no λ() -propLit _ ≟-Sort lit _ = no λ() -propLit _ ≟-Sort prop _ = no λ() -propLit _ ≟-Sort inf _ = no λ() -propLit _ ≟-Sort unknown = no λ() -inf _ ≟-Sort set _ = no λ() -inf _ ≟-Sort lit _ = no λ() -inf _ ≟-Sort prop _ = no λ() -inf _ ≟-Sort propLit _ = no λ() -inf _ ≟-Sort unknown = no λ() -unknown ≟-Sort set _ = no λ() -unknown ≟-Sort lit _ = no λ() -unknown ≟-Sort prop _ = no λ() -unknown ≟-Sort propLit _ = no λ() -unknown ≟-Sort inf _ = no λ() +var x args ≡? var x′ args′ = + map′ (uncurry (cong₂ var)) var-injective (x ℕ.≡? x′ ×? args ≡?-Args args′) +con c args ≡? con c′ args′ = + map′ (uncurry (cong₂ con)) con-injective (c Name.≡? c′ ×? args ≡?-Args args′) +def f args ≡? def f′ args′ = + map′ (uncurry (cong₂ def)) def-injective (f Name.≡? f′ ×? args ≡?-Args args′) +meta x args ≡? meta x′ args′ = + map′ (uncurry (cong₂ meta)) meta-injective (x Meta.≡? x′ ×? args ≡?-Args args′) +lam v t ≡? lam v′ t′ = + map′ (uncurry (cong₂ lam)) lam-injective (v Visibility.≡? v′ ×? t ≡?-AbsTerm t′) +pat-lam cs args ≡? pat-lam cs′ args′ = + map′ (uncurry (cong₂ pat-lam)) pat-lam-injective (cs ≡?-Clauses cs′ ×? args ≡?-Args args′) +pi t₁ t₂ ≡? pi t₁′ t₂′ = + map′ (uncurry (cong₂ pi)) pi-injective (t₁ ≡?-ArgType t₁′ ×? t₂ ≡?-AbsType t₂′) +sort s ≡? sort s′ = map′ (cong sort) sort-injective (s ≡?-Sort s′) +lit l ≡? lit l′ = map′ (cong lit) lit-injective (l Literal.≡? l′) +unknown ≡? unknown = yes refl + +var x args ≡? con c args′ = no λ() +var x args ≡? def f args′ = no λ() +var x args ≡? lam v t = no λ() +var x args ≡? pi t₁ t₂ = no λ() +var x args ≡? sort _ = no λ() +var x args ≡? lit _ = no λ() +var x args ≡? meta _ _ = no λ() +var x args ≡? unknown = no λ() +con c args ≡? var x args′ = no λ() +con c args ≡? def f args′ = no λ() +con c args ≡? lam v t = no λ() +con c args ≡? pi t₁ t₂ = no λ() +con c args ≡? sort _ = no λ() +con c args ≡? lit _ = no λ() +con c args ≡? meta _ _ = no λ() +con c args ≡? unknown = no λ() +def f args ≡? var x args′ = no λ() +def f args ≡? con c args′ = no λ() +def f args ≡? lam v t = no λ() +def f args ≡? pi t₁ t₂ = no λ() +def f args ≡? sort _ = no λ() +def f args ≡? lit _ = no λ() +def f args ≡? meta _ _ = no λ() +def f args ≡? unknown = no λ() +lam v t ≡? var x args = no λ() +lam v t ≡? con c args = no λ() +lam v t ≡? def f args = no λ() +lam v t ≡? pi t₁ t₂ = no λ() +lam v t ≡? sort _ = no λ() +lam v t ≡? lit _ = no λ() +lam v t ≡? meta _ _ = no λ() +lam v t ≡? unknown = no λ() +pi t₁ t₂ ≡? var x args = no λ() +pi t₁ t₂ ≡? con c args = no λ() +pi t₁ t₂ ≡? def f args = no λ() +pi t₁ t₂ ≡? lam v t = no λ() +pi t₁ t₂ ≡? sort _ = no λ() +pi t₁ t₂ ≡? lit _ = no λ() +pi t₁ t₂ ≡? meta _ _ = no λ() +pi t₁ t₂ ≡? unknown = no λ() +sort _ ≡? var x args = no λ() +sort _ ≡? con c args = no λ() +sort _ ≡? def f args = no λ() +sort _ ≡? lam v t = no λ() +sort _ ≡? pi t₁ t₂ = no λ() +sort _ ≡? lit _ = no λ() +sort _ ≡? meta _ _ = no λ() +sort _ ≡? unknown = no λ() +lit _ ≡? var x args = no λ() +lit _ ≡? con c args = no λ() +lit _ ≡? def f args = no λ() +lit _ ≡? lam v t = no λ() +lit _ ≡? pi t₁ t₂ = no λ() +lit _ ≡? sort _ = no λ() +lit _ ≡? meta _ _ = no λ() +lit _ ≡? unknown = no λ() +meta _ _ ≡? var x args = no λ() +meta _ _ ≡? con c args = no λ() +meta _ _ ≡? def f args = no λ() +meta _ _ ≡? lam v t = no λ() +meta _ _ ≡? pi t₁ t₂ = no λ() +meta _ _ ≡? sort _ = no λ() +meta _ _ ≡? lit _ = no λ() +meta _ _ ≡? unknown = no λ() +unknown ≡? var x args = no λ() +unknown ≡? con c args = no λ() +unknown ≡? def f args = no λ() +unknown ≡? lam v t = no λ() +unknown ≡? pi t₁ t₂ = no λ() +unknown ≡? sort _ = no λ() +unknown ≡? lit _ = no λ() +unknown ≡? meta _ _ = no λ() +pat-lam _ _ ≡? var x args = no λ() +pat-lam _ _ ≡? con c args = no λ() +pat-lam _ _ ≡? def f args = no λ() +pat-lam _ _ ≡? lam v t = no λ() +pat-lam _ _ ≡? pi t₁ t₂ = no λ() +pat-lam _ _ ≡? sort _ = no λ() +pat-lam _ _ ≡? lit _ = no λ() +pat-lam _ _ ≡? meta _ _ = no λ() +pat-lam _ _ ≡? unknown = no λ() +var x args ≡? pat-lam _ _ = no λ() +con c args ≡? pat-lam _ _ = no λ() +def f args ≡? pat-lam _ _ = no λ() +lam v t ≡? pat-lam _ _ = no λ() +pi t₁ t₂ ≡? pat-lam _ _ = no λ() +sort _ ≡? pat-lam _ _ = no λ() +lit _ ≡? pat-lam _ _ = no λ() +meta _ _ ≡? pat-lam _ _ = no λ() +unknown ≡? pat-lam _ _ = no λ() + +set t ≡?-Sort set t′ = map′ (cong set) set-injective (t ≡? t′) +lit n ≡?-Sort lit n′ = map′ (cong lit) slit-injective (n ℕ.≡? n′) +prop t ≡?-Sort prop t′ = map′ (cong prop) prop-injective (t ≡? t′) +propLit n ≡?-Sort propLit n′ = map′ (cong propLit) propLit-injective (n ℕ.≡? n′) +inf n ≡?-Sort inf n′ = map′ (cong inf) inf-injective (n ℕ.≡? n′) +unknown ≡?-Sort unknown = yes refl +set _ ≡?-Sort lit _ = no λ() +set _ ≡?-Sort prop _ = no λ() +set _ ≡?-Sort propLit _ = no λ() +set _ ≡?-Sort inf _ = no λ() +set _ ≡?-Sort unknown = no λ() +lit _ ≡?-Sort set _ = no λ() +lit _ ≡?-Sort prop _ = no λ() +lit _ ≡?-Sort propLit _ = no λ() +lit _ ≡?-Sort inf _ = no λ() +lit _ ≡?-Sort unknown = no λ() +prop _ ≡?-Sort set _ = no λ() +prop _ ≡?-Sort lit _ = no λ() +prop _ ≡?-Sort propLit _ = no λ() +prop _ ≡?-Sort inf _ = no λ() +prop _ ≡?-Sort unknown = no λ() +propLit _ ≡?-Sort set _ = no λ() +propLit _ ≡?-Sort lit _ = no λ() +propLit _ ≡?-Sort prop _ = no λ() +propLit _ ≡?-Sort inf _ = no λ() +propLit _ ≡?-Sort unknown = no λ() +inf _ ≡?-Sort set _ = no λ() +inf _ ≡?-Sort lit _ = no λ() +inf _ ≡?-Sort prop _ = no λ() +inf _ ≡?-Sort propLit _ = no λ() +inf _ ≡?-Sort unknown = no λ() +unknown ≡?-Sort set _ = no λ() +unknown ≡?-Sort lit _ = no λ() +unknown ≡?-Sort prop _ = no λ() +unknown ≡?-Sort propLit _ = no λ() +unknown ≡?-Sort inf _ = no λ() pat-con-injective₁ : ∀ {c c′ args args′} → Pattern.con c args ≡ con c′ args′ → c ≡ c′ @@ -437,46 +437,120 @@ dot-injective refl = refl absurd-injective : ∀ {x y} → absurd x ≡ absurd y → x ≡ y absurd-injective refl = refl -con c ps ≟-Pattern con c′ ps′ = map′ (uncurry (cong₂ con)) pat-con-injective (c Name.≟ c′ ×? ps ≟-Patterns ps′) -var x ≟-Pattern var x′ = map′ (cong var) pat-var-injective (x ℕ.≟ x′) -lit l ≟-Pattern lit l′ = map′ (cong lit) pat-lit-injective (l Literal.≟ l′) -proj a ≟-Pattern proj a′ = map′ (cong proj) proj-injective (a Name.≟ a′) -dot t ≟-Pattern dot t′ = map′ (cong dot) dot-injective (t ≟ t′) -absurd x ≟-Pattern absurd x′ = map′ (cong absurd) absurd-injective (x ℕ.≟ x′) - -con x x₁ ≟-Pattern dot x₂ = no (λ ()) -con x x₁ ≟-Pattern var x₂ = no (λ ()) -con x x₁ ≟-Pattern lit x₂ = no (λ ()) -con x x₁ ≟-Pattern proj x₂ = no (λ ()) -con x x₁ ≟-Pattern absurd x₂ = no (λ ()) -dot x ≟-Pattern con x₁ x₂ = no (λ ()) -dot x ≟-Pattern var x₁ = no (λ ()) -dot x ≟-Pattern lit x₁ = no (λ ()) -dot x ≟-Pattern proj x₁ = no (λ ()) -dot x ≟-Pattern absurd x₁ = no (λ ()) -var s ≟-Pattern con x x₁ = no (λ ()) -var s ≟-Pattern dot x = no (λ ()) -var s ≟-Pattern lit x = no (λ ()) -var s ≟-Pattern proj x = no (λ ()) -var s ≟-Pattern absurd x = no (λ ()) -lit x ≟-Pattern con x₁ x₂ = no (λ ()) -lit x ≟-Pattern dot x₁ = no (λ ()) -lit x ≟-Pattern var _ = no (λ ()) -lit x ≟-Pattern proj x₁ = no (λ ()) -lit x ≟-Pattern absurd x₁ = no (λ ()) -proj x ≟-Pattern con x₁ x₂ = no (λ ()) -proj x ≟-Pattern dot x₁ = no (λ ()) -proj x ≟-Pattern var _ = no (λ ()) -proj x ≟-Pattern lit x₁ = no (λ ()) -proj x ≟-Pattern absurd x₁ = no (λ ()) -absurd x ≟-Pattern con x₁ x₂ = no (λ ()) -absurd x ≟-Pattern dot x₁ = no (λ ()) -absurd x ≟-Pattern var _ = no (λ ()) -absurd x ≟-Pattern lit x₁ = no (λ ()) -absurd x ≟-Pattern proj x₁ = no (λ ()) - -[] ≟-Patterns [] = yes refl -(arg i p ∷ xs) ≟-Patterns (arg j q ∷ ys) = ∷-dec (unArg-dec (p ≟-Pattern q)) (xs ≟-Patterns ys) - -[] ≟-Patterns (_ ∷ _) = no λ() -(_ ∷ _) ≟-Patterns [] = no λ() +con c ps ≡?-Pattern con c′ ps′ = map′ (uncurry (cong₂ con)) pat-con-injective (c Name.≡? c′ ×? ps ≡?-Patterns ps′) +var x ≡?-Pattern var x′ = map′ (cong var) pat-var-injective (x ℕ.≡? x′) +lit l ≡?-Pattern lit l′ = map′ (cong lit) pat-lit-injective (l Literal.≡? l′) +proj a ≡?-Pattern proj a′ = map′ (cong proj) proj-injective (a Name.≡? a′) +dot t ≡?-Pattern dot t′ = map′ (cong dot) dot-injective (t ≡? t′) +absurd x ≡?-Pattern absurd x′ = map′ (cong absurd) absurd-injective (x ℕ.≡? x′) + +con x x₁ ≡?-Pattern dot x₂ = no (λ ()) +con x x₁ ≡?-Pattern var x₂ = no (λ ()) +con x x₁ ≡?-Pattern lit x₂ = no (λ ()) +con x x₁ ≡?-Pattern proj x₂ = no (λ ()) +con x x₁ ≡?-Pattern absurd x₂ = no (λ ()) +dot x ≡?-Pattern con x₁ x₂ = no (λ ()) +dot x ≡?-Pattern var x₁ = no (λ ()) +dot x ≡?-Pattern lit x₁ = no (λ ()) +dot x ≡?-Pattern proj x₁ = no (λ ()) +dot x ≡?-Pattern absurd x₁ = no (λ ()) +var s ≡?-Pattern con x x₁ = no (λ ()) +var s ≡?-Pattern dot x = no (λ ()) +var s ≡?-Pattern lit x = no (λ ()) +var s ≡?-Pattern proj x = no (λ ()) +var s ≡?-Pattern absurd x = no (λ ()) +lit x ≡?-Pattern con x₁ x₂ = no (λ ()) +lit x ≡?-Pattern dot x₁ = no (λ ()) +lit x ≡?-Pattern var _ = no (λ ()) +lit x ≡?-Pattern proj x₁ = no (λ ()) +lit x ≡?-Pattern absurd x₁ = no (λ ()) +proj x ≡?-Pattern con x₁ x₂ = no (λ ()) +proj x ≡?-Pattern dot x₁ = no (λ ()) +proj x ≡?-Pattern var _ = no (λ ()) +proj x ≡?-Pattern lit x₁ = no (λ ()) +proj x ≡?-Pattern absurd x₁ = no (λ ()) +absurd x ≡?-Pattern con x₁ x₂ = no (λ ()) +absurd x ≡?-Pattern dot x₁ = no (λ ()) +absurd x ≡?-Pattern var _ = no (λ ()) +absurd x ≡?-Pattern lit x₁ = no (λ ()) +absurd x ≡?-Pattern proj x₁ = no (λ ()) + +[] ≡?-Patterns [] = yes refl +(arg i p ∷ xs) ≡?-Patterns (arg j q ∷ ys) = ∷-dec (unArg-dec (p ≡?-Pattern q)) (xs ≡?-Patterns ys) + +[] ≡?-Patterns (_ ∷ _) = no λ() +(_ ∷ _) ≡?-Patterns [] = no λ() + + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.4 + +infix 4 _≟-AbsTerm_ _≟-AbsType_ _≟-ArgTerm_ _≟-ArgType_ _≟-Args_ + _≟-Clause_ _≟-Clauses_ _≟_ + _≟-Sort_ _≟-Pattern_ _≟-Patterns_ _≟-Telescope_ + +_≟_ = _≡?_ +{-# WARNING_ON_USAGE _≟_ +"Warning: _≟_ was deprecated in v2.4. +Please use _≡?_ instead." +#-} +_≟-AbsTerm_ = _≡?-AbsTerm_ +{-# WARNING_ON_USAGE _≟_ +"Warning: _≟-AbsTerm_ was deprecated in v2.4. +Please use _≡?-AbsTerm_ instead." +#-} +_≟-AbsType_ = _≡?-AbsType_ +{-# WARNING_ON_USAGE _≟-AbsType_ +"Warning: _≟-AbsType_ was deprecated in v2.4. +Please use _≡?-AbsType_ instead." +#-} +_≟-ArgTerm_ = _≡?-ArgTerm_ +{-# WARNING_ON_USAGE _≟_ +"Warning: _≟-ArgTerm_ was deprecated in v2.4. +Please use _≡?-ArgTerm_ instead." +#-} +_≟-ArgType_ = _≡?-ArgType_ +{-# WARNING_ON_USAGE _≟-ArgType_ +"Warning: _≟-ArgType_ was deprecated in v2.4. +Please use _≡?-ArgType_ instead." +#-} +_≟-Args_ = _≡?-Args_ +{-# WARNING_ON_USAGE _≟-Args_ +"Warning: _≟-Args_ was deprecated in v2.4. +Please use _≡?-Args_ instead." +#-} +_≟-Clause_ = _≡?-Clause_ +{-# WARNING_ON_USAGE _≟-Clause_ +"Warning: _≟-Clause_ was deprecated in v2.4. +Please use _≡?-Clause_ instead." +#-} +_≟-Clauses_ = _≡?-Clauses_ +{-# WARNING_ON_USAGE _≟_ +"Warning: _≟-Clauses_ was deprecated in v2.4. +Please use _≡?-Clauses_ instead." +#-} +_≟-Sort_ = _≡?-Sort_ +{-# WARNING_ON_USAGE _≟-Sort_ +"Warning: _≟-Sort_ was deprecated in v2.4. +Please use _≡?-Sort_ instead." +#-} +_≟-Pattern_ = _≡?-Pattern_ +{-# WARNING_ON_USAGE _≟-Pattern_ +"Warning: _≟-Pattern_ was deprecated in v2.4. +Please use _≡?-Pattern_ instead." +#-} +_≟-Patterns_ = _≡?-Patterns_ +{-# WARNING_ON_USAGE _≟-Patterns_ +"Warning: _≟-Patterns_ was deprecated in v2.4. +Please use _≡?-Patterns_ instead." +#-} +_≟-Telescope_ = _≡?-Telescope_ +{-# WARNING_ON_USAGE _≟-Telescope_ +"Warning: _≟-Telescope_ was deprecated in v2.4. +Please use _≡?-Telescope_ instead." +#-} diff --git a/src/Relation/Binary/Bundles.agda b/src/Relation/Binary/Bundles.agda index cd66369dec..22be21b028 100644 --- a/src/Relation/Binary/Bundles.agda +++ b/src/Relation/Binary/Bundles.agda @@ -64,7 +64,7 @@ record DecSetoid c ℓ : Set (suc (c ⊔ ℓ)) where isDecEquivalence : IsDecEquivalence _≈_ open IsDecEquivalence isDecEquivalence public - using (_≟_; isEquivalence) + using (_≈?_; _≟_; isEquivalence) setoid : Setoid c ℓ setoid = record @@ -140,7 +140,7 @@ record DecPreorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where private module DPO = IsDecPreorder isDecPreorder open DPO public - using (_≟_; _≲?_; isPreorder) + using (_≈?_; _≲?_; isPreorder) preorder : Preorder c ℓ₁ ℓ₂ preorder = record @@ -203,7 +203,7 @@ record DecPoset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where private module DPO = IsDecPartialOrder isDecPartialOrder open DPO public - using (_≟_; _≤?_; isPartialOrder; isDecPreorder) + using (_≈?_; _≤?_; isPartialOrder; isDecPreorder) poset : Poset c ℓ₁ ℓ₂ poset = record @@ -258,7 +258,7 @@ record DecStrictPartialOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂ private module DSPO = IsDecStrictPartialOrder isDecStrictPartialOrder open DSPO public - using (_ (x≉y ∘ flip antisym y≤x ∘ proj₁) x≉y (y≤x , x≉y ∘ ≈-sym) <-decidable : Decidable _≈_ → Decidable _≤_ → Decidable _<_ -<-decidable _≟_ _≤?_ x y = x ≤? y ×? ¬? (x ≟ y) +<-decidable _≈?_ _≤?_ x y = x ≤? y ×? ¬? (x ≈? y) ------------------------------------------------------------------------ -- Structures @@ -135,18 +135,18 @@ x < y = x ≤ y × x ≉ y IsDecStrictPartialOrder _≈_ _<_ <-isDecStrictPartialOrder dpo = record { isStrictPartialOrder = <-isStrictPartialOrder isPartialOrder - ; _≟_ = _≟_ - ; _ Equalₙ n l r) (Dec (uncurryₙ n con l ≡ uncurryₙ n con r)) -≟-mapₙ n con con-inj = +≡?-mapₙ : ∀ n {ls} {as : Sets n ls} (con : Arrows n as R) → Injectiveₙ n con → + ∀ {l r} → Arrows n (Dec <$> Equalₙ n l r) (Dec (uncurryₙ n con l ≡ uncurryₙ n con r)) +≡?-mapₙ n con con-inj = curryₙ n λ a?s → let as? = Product-dec n a?s in Dec.map′ (cong (uncurryₙ n con) ∘′ fromEqualₙ n) con-inj as? @@ -205,5 +204,20 @@ toWitness : ∀ {n ls r} {as : Sets n ls} (R : as ⇉ Set r) (R? : Decidable R) ∀[ R ⇒ ⌊ R? ⌋ ] toWitness {zero} R R? with R? ... | true because _ = _ -... | no ¬r = ⊥-elim ∘′ ¬r +... | no ¬r = contradiction′ ¬r toWitness {suc n} R R? = toWitness (R _) (R? _) + + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.4 + +≟-mapₙ = ≡?-mapₙ +{-# WARNING_ON_USAGE ≟-mapₙ +"Warning: ≟-mapₙ was deprecated in v2.4. +Please use ≡?-mapₙ instead." +#-} diff --git a/src/Relation/Nullary/Decidable.agda b/src/Relation/Nullary/Decidable.agda index e9e16a8c88..6caf11d5a1 100644 --- a/src/Relation/Nullary/Decidable.agda +++ b/src/Relation/Nullary/Decidable.agda @@ -47,7 +47,7 @@ module _ {S : Setoid a ℓ₁} {T : Setoid b ℓ₂} (injection : Injection S T) open Injection injection via-injection : Decidable Eq₂._≈_ → Decidable Eq₁._≈_ - via-injection _≟_ x y = map′ injective cong (to x ≟ to y) + via-injection _≈?_ x y = map′ injective cong (to x ≈? to y) ------------------------------------------------------------------------ -- A lemma relating True and Dec diff --git a/src/Tactic/Cong.agda b/src/Tactic/Cong.agda index ceffe6587d..d7e6a14571 100644 --- a/src/Tactic/Cong.agda +++ b/src/Tactic/Cong.agda @@ -108,7 +108,7 @@ private term' ← term symTerm' ← symTerm -- Don't show the same term twice. - let symErr = case term' Term.≟ symTerm' of λ where + let symErr = case term' Term.≡? symTerm' of λ where (yes _) → [] (no _) → strErr "\n" ∷ termErr symTerm' ∷ [] typeError (strErr "cong! failed, tried:\n" ∷ termErr term' ∷ symErr) diff --git a/src/Test/Golden.agda b/src/Test/Golden.agda index cc3198269c..1533f09752 100644 --- a/src/Test/Golden.agda +++ b/src/Test/Golden.agda @@ -92,7 +92,7 @@ open import Data.Nat.ListAction using (sum) import Data.Nat.Show as ℕ using (show) open import Data.Product.Base using (_×_; _,_) open import Data.String.Base as String using (String; lines; unlines; unwords; concat) -open import Data.String.Properties as String using (_≟_) +open import Data.String.Properties as String using (_≡?_) open import Data.Sum.Base using (_⊎_; inj₁; inj₂) open import Data.Unit.Base using (⊤) @@ -183,7 +183,7 @@ options(exe ∷ rest) = mkOptions exe rest where inj₂ (mfp , opts) ← pure $ go rest nothing (initOptions exe) where inj₁ arg → pure (inj₁ (InvalidArgument arg)) term ← fromMaybe "" <$> lookupEnv "TERM" - let opts = if does (term ≟ "DUMB") + let opts = if does (term ≡? "DUMB") then record opts { colour = false } else opts just fp ← pure mfp @@ -221,7 +221,7 @@ runTest opts testPath = do else putStrLn (fileNotFound "expected") pure (inj₁ testPath) - let result = does (out String.≟ exp) + let result = does (out String.≡? exp) if result then printTiming (opts .timing) time @@ -354,7 +354,7 @@ filterTests : Options → List String → List String filterTests opts = case onlyNames opts of λ where [] → id xs → let names = List.map String.toList xs in - filter (λ n → any? (λ m → infix? Char._≟_ m (String.toList n)) names) + filter (λ n → any? (λ m → infix? Char._≡?_ m (String.toList n)) names) poolRunner : Options → TestPool → IO Summary poolRunner opts pool = do diff --git a/src/Text/Regex/Properties.agda b/src/Text/Regex/Properties.agda index b384207d7f..ce76e26375 100644 --- a/src/Text/Regex/Properties.agda +++ b/src/Text/Regex/Properties.agda @@ -52,7 +52,7 @@ open import Text.Regex.Properties.Core preorder public infix 4 _∈ᴿ?_ _∉ᴿ?_ _∈?ε _∈?[_] _∈?[^_] _∈ᴿ?_ : Decidable _∈ᴿ_ -c ∈ᴿ? [ a ] = map′ [_] (λ where [ eq ] → eq) (c ≟ a) +c ∈ᴿ? [ a ] = map′ [_] (λ where [ eq ] → eq) (c ≈? a) c ∈ᴿ? (lb ─ ub) = map′ (uncurry _─_) (λ where (ge ─ le) → ge , le) $ (lb ≤? c) ×? (c ≤? ub) diff --git a/tests/data/trie/Main.agda b/tests/data/trie/Main.agda index 3ce2ad3ecb..91246b5a93 100644 --- a/tests/data/trie/Main.agda +++ b/tests/data/trie/Main.agda @@ -35,7 +35,7 @@ record Lexer t : Set (suc t) where Keyword = String × Tok Distinct : Rel Keyword 0ℓ - Distinct a b = ⌊ ¬? ((proj₁ a) String.≟ (proj₁ b)) ⌋ + Distinct a b = ⌊ ¬? ((proj₁ a) String.≡? (proj₁ b)) ⌋ field keywords : List# Keyword Distinct @@ -90,7 +90,7 @@ module LetIn where show RPAR = "RPAR" show (ID x) = "ID \"" ++ x ++ "\"" - keywords : List# (String × TOK) (λ a b → ⌊ ¬? ((proj₁ a) String.≟ (proj₁ b)) ⌋) + keywords : List# (String × TOK) (λ a b → ⌊ ¬? ((proj₁ a) String.≡? (proj₁ b)) ⌋) keywords = ("let" , LET) ∷# ("=" , EQ) ∷# ("in" , IN) diff --git a/tests/reflection/assumption/Main.agda b/tests/reflection/assumption/Main.agda index cf0d21b514..bdc397613a 100644 --- a/tests/reflection/assumption/Main.agda +++ b/tests/reflection/assumption/Main.agda @@ -13,7 +13,7 @@ open import Data.Unit.Base using (⊤) open import Function.Base using (case_of_; _$_) open import Reflection.TCM hiding (pure) open import Reflection.AST.Term -open import Reflection.AST.Literal hiding (_≟_) +open import Reflection.AST.Literal hiding (_≟_; _≡?_) open import Reflection.AST.Argument using (Arg; unArg; arg) open import Reflection.AST.DeBruijn open import Reflection.AST.Show @@ -44,7 +44,7 @@ searchEntry : ℕ → Type → List (String × Arg Type) → Maybe ℕ searchEntry n ty [] = nothing searchEntry n ty ((_ , e) ∷ es) = do ty ← strengthen ty - if does (ty ≟ unArg e) + if does (ty ≡? unArg e) then just n else searchEntry (suc n) ty es