8000 Float DefP clauses above catch-alls by plt-amy · Pull Request #7097 · agda/agda · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Float DefP clauses above catch-alls #7097

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

Jump to bottom
Merged
merged 1 commit into from
Feb 8, 2024
Merged

Float DefP clauses above catch-alls #7097

merged 1 commit into from
Feb 8, 2024

Conversation

plt-amy
Copy link
Member
@plt-amy plt-amy commented Feb 7, 2024

Fixes #7033 by making the clause compiler rotate matching DefPs above inexact clauses, instead of duplicating the inexact clause's RHS. That is, instead of turning

f _ = X
f (hcomp u u0) = comp ...

into

f (hcomp u u0) = X
f _ = X
f (hcomp u u0) = comp ...
-- This is really the list of clauses that the clause compiler was using!

we instead rotate the generated hcomp clause above the user-written f _ clause, to get

f (hcomp u u0) = comp ...
f _ = X

instead. It was easier to do this in the clause compiler, where we have a variable index to check for overlap on, than trying to sort the list of clauses when doing addClause.

@plt-amy plt-amy added clause-compiler cubical Cubical Agda paraphernalia: Paths, Glue, partial elements, hcomp, transp labels Feb 7, 2024
@plt-amy plt-amy added this to the 2.6.4.2 milestone Feb 7, 2024
@plt-amy plt-amy merged commit bdaf429 into master Feb 8, 2024
@plt-amy plt-amy deleted the aliao/issue7033 branch February 8, 2024 15:39
andreasabel pushed a commit that referenced this pull request Feb 8, 2024
@plt-amy @andreasabel
Float DefP clauses above catch-alls (#7097)
d4865f9
@andreasabel andreasabel mentioned this pull request Feb 8, 2024
Closed
3 tasks
VitalyAnkh pushed a commit to VitalyAnkh/agda that referenced this pull request Mar 5, 2024
@plt-amy @VitalyAnkh
Float DefP clauses above catch-alls (agda#7097)
e8de33f
JobPetrovcic pushed a commit to JobPetrovcic/agda that referenced this pull request Apr 12, 2024
@plt-amy @JobPetrovcic
Float DefP clauses above catch-alls (agda#7097)
e61a597
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
clause-compiler cubical Cubical Agda paraphernalia: Paths, Glue, partial elements, hcomp, transp
Projects
None yet
Milestone
2.6.4.2
Development

Successfully merging this pull request may close these issues.

transpX clauses can be beat out by user-written _ clauses, leading to proof of ⊥
1 participant
@plt-amy
0