Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Replace record directive "eta-equality" by "no-eta-equality;pattern" #2476

Draft
wants to merge 2 commits into
base: experimental
Choose a base branch
from
Draft

Replace record directive "eta-equality" by "no-eta-equality;pattern" #2476

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
91e2c01
Tactic.RingSolver.Core.Polynomial: drop eta-equality for constructor _⊐_
andreasabel Sep 6, 2024
8caaeae
Data.Record: drop eta and pattern matching for constructor rec
andreasabel Sep 6, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion doc/README/Data/Record.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
40 changes: 21 additions & 19 deletions src/Data/Record.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down Expand Up @@ -122,30 +122,32 @@ 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 _·_

_·_ : ∀ {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
Expand All @@ -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)) ,)
5 changes: 3 additions & 2 deletions src/Tactic/RingSolver/Core/Polynomial/Base.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down