From 91e2c0130edc60a24b09ed1a69aa8fdebe7a106a Mon Sep 17 00:00:00 2001 From: Andreas Abel Date: Fri, 6 Sep 2024 22:23:25 +0200 Subject: [PATCH 1/2] =?UTF-8?q?Tactic.RingSolver.Core.Polynomial:=20drop?= =?UTF-8?q?=20eta-equality=20for=20constructor=20=5F=E2=8A=90=5F?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Future Agda versions might no longer support eta for unguarded records in `--safe` mode. Dropping eta-equality for constructor _⊐_ only requires changing the order of clauses in ⊞-inj. Re: https://github.com/agda/agda/pull/7470 --- src/Tactic/RingSolver/Core/Polynomial/Base.agda | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/Tactic/RingSolver/Core/Polynomial/Base.agda b/src/Tactic/RingSolver/Core/Polynomial/Base.agda index 6de64bf839..56c26b8054 100644 --- a/src/Tactic/RingSolver/Core/Polynomial/Base.agda +++ b/src/Tactic/RingSolver/Core/Polynomial/Base.agda @@ -130,8 +130,9 @@ Normalised : ∀ {i} → Coeff i + → Set infixl 6 _⊐_ record Poly n where inductive + no-eta-equality + pattern -- To allow matching on constructor constructor _⊐_ - eta-equality -- To allow matching on constructor field {i} : ℕ flat : FlatPoly i @@ -285,8 +286,8 @@ mutual → FlatPoly i → Coeff k + → Coeff k * - ⊞-inj i≤k xs (y ⊐ j≤k ≠0 Δ zero & ys) = ⊞-match (inj-compare j≤k i≤k) y xs Δ zero ∷↓ ys ⊞-inj i≤k xs (y Δ suc j & ys) = xs ⊐ i≤k Δ zero ∷↓ ∹ y Δ j & ys + ⊞-inj i≤k xs (y ⊐ j≤k ≠0 Δ zero & ys) = ⊞-match (inj-compare j≤k i≤k) y xs Δ zero ∷↓ ys ⊞-coeffs : ∀ {n} → Coeff n * → Coeff n * → Coeff n * ⊞-coeffs (∹ x Δ i & xs) ys = ⊞-zip-r x i xs ys From 8caaeaec60404d0ce8c95bc71384b32aa962daf1 Mon Sep 17 00:00:00 2001 From: Andreas Abel Date: Fri, 6 Sep 2024 22:29:54 +0200 Subject: [PATCH 2/2] Data.Record: drop eta and pattern matching for constructor rec Future Agda might not allow unguarded record types with eta-equality in `--safe` mode anymore. Re: https://github.com/agda/agda/pull/7470 Switching of eta for `rec` is slightly inconvenient, as was observed already in this issue: https://github.com/agda/agda/issues/840 Allowing it would need improvements to the Agda positivity checker, so that it can recognize `Record` as guarded record that can safely support eta. --- doc/README/Data/Record.agda | 2 +- src/Data/Record.agda | 40 +++++++++++++++++++------------------ 2 files changed, 22 insertions(+), 20 deletions(-) diff --git a/doc/README/Data/Record.agda b/doc/README/Data/Record.agda index 63fea328ae..92a785b57c 100644 --- a/doc/README/Data/Record.agda +++ b/doc/README/Data/Record.agda @@ -37,6 +37,6 @@ converse : (P : Record PER) → Record (PER With "S" ≔ (λ _ → P · "S") With "R" ≔ (λ _ → flip (P · "R"))) converse P = - rec (rec (_ , + rec (rec (rec (rec (rec _ ,) ,) , lift λ {_} → lower (P · "sym")) , lift λ {_} yRx zRy → lower (P · "trans") zRy yRx) diff --git a/src/Data/Record.agda b/src/Data/Record.agda index 709ce69a67..ad60c0f87d 100644 --- a/src/Data/Record.agda +++ b/src/Data/Record.agda @@ -63,8 +63,8 @@ mutual -- inferred from a value of type Record Sig. record Record {s} (Sig : Signature s) : Set s where - eta-equality inductive + no-eta-equality constructor rec field fun : Record-fun Sig @@ -122,17 +122,19 @@ Proj (_,_≔_ Sig ℓ′ {A = A} a) ℓ {ℓ∈} with does (ℓ ≟ ℓ′) -- Record restriction and projection. +open Record renaming (fun to fields) + infixl 5 _∣_ _∣_ : ∀ {s} {Sig : Signature s} → Record Sig → (ℓ : Label) {ℓ∈ : ℓ ∈ Sig} → Restricted Sig ℓ ℓ∈ _∣_ {Sig = ∅} r ℓ {} -_∣_ {Sig = Sig , ℓ′ ∶ A} (rec r) ℓ {ℓ∈} with does (ℓ ≟ ℓ′) -... | true = Σ.proj₁ r -... | false = _∣_ (Σ.proj₁ r) ℓ {ℓ∈} -_∣_ {Sig = Sig , ℓ′ ≔ a} (rec r) ℓ {ℓ∈} with does (ℓ ≟ ℓ′) -... | true = Manifest-Σ.proj₁ r -... | false = _∣_ (Manifest-Σ.proj₁ r) ℓ {ℓ∈} +_∣_ {Sig = Sig , ℓ′ ∶ A} r ℓ {ℓ∈} with does (ℓ ≟ ℓ′) +... | true = Σ.proj₁ (fields r) +... | false = _∣_ (Σ.proj₁ (fields r)) ℓ {ℓ∈} +_∣_ {Sig = Sig , ℓ′ ≔ a} r ℓ {ℓ∈} with does (ℓ ≟ ℓ′) +... | true = Manifest-Σ.proj₁ (fields r) +... | false = _∣_ (Manifest-Σ.proj₁ (fields r)) ℓ {ℓ∈} infixl 5 _·_ @@ -140,12 +142,12 @@ _·_ : ∀ {s} {Sig : Signature s} (r : Record Sig) (ℓ : Label) {ℓ∈ : ℓ ∈ Sig} → Proj Sig ℓ {ℓ∈} (r ∣ ℓ) _·_ {Sig = ∅} r ℓ {} -_·_ {Sig = Sig , ℓ′ ∶ A} (rec r) ℓ {ℓ∈} with does (ℓ ≟ ℓ′) -... | true = Σ.proj₂ r -... | false = _·_ (Σ.proj₁ r) ℓ {ℓ∈} -_·_ {Sig = Sig , ℓ′ ≔ a} (rec r) ℓ {ℓ∈} with does (ℓ ≟ ℓ′) -... | true = Manifest-Σ.proj₂ r -... | false = _·_ (Manifest-Σ.proj₁ r) ℓ {ℓ∈} +_·_ {Sig = Sig , ℓ′ ∶ A} r ℓ {ℓ∈} with does (ℓ ≟ ℓ′) +... | true = Σ.proj₂ (fields r) +... | false = _·_ (Σ.proj₁ (fields r)) ℓ {ℓ∈} +_·_ {Sig = Sig , ℓ′ ≔ a} r ℓ {ℓ∈} with does (ℓ ≟ ℓ′) +... | true = Manifest-Σ.proj₂ (fields r) +... | false = _·_ (Manifest-Σ.proj₁ (fields r)) ℓ {ℓ∈} ------------------------------------------------------------------------ -- With @@ -170,9 +172,9 @@ mutual {a : (r : Restricted Sig ℓ ℓ∈) → Proj Sig ℓ r} → Record (_With_≔_ Sig ℓ {ℓ∈} a) → Record Sig drop-With {Sig = ∅} {ℓ∈ = ()} r - drop-With {Sig = Sig , ℓ′ ∶ A} {ℓ} (rec r) with does (ℓ ≟ ℓ′) - ... | true = rec (Manifest-Σ.proj₁ r , Manifest-Σ.proj₂ r) - ... | false = rec (drop-With (Σ.proj₁ r) , Σ.proj₂ r) - drop-With {Sig = Sig , ℓ′ ≔ a} {ℓ} (rec r) with does (ℓ ≟ ℓ′) - ... | true = rec (Manifest-Σ.proj₁ r ,) - ... | false = rec (drop-With (Manifest-Σ.proj₁ r) ,) + drop-With {Sig = Sig , ℓ′ ∶ A} {ℓ} r with does (ℓ ≟ ℓ′) + ... | true = rec (Manifest-Σ.proj₁ (fields r) , Manifest-Σ.proj₂ (fields r)) + ... | false = rec (drop-With (Σ.proj₁ (fields r)) , Σ.proj₂ (fields r)) + drop-With {Sig = Sig , ℓ′ ≔ a} {ℓ} r with does (ℓ ≟ ℓ′) + ... | true = rec (Manifest-Σ.proj₁ (fields r) ,) + ... | false = rec (drop-With (Manifest-Σ.proj₁ (fields r)) ,)