Skip to content

Move All Resolution to the Resolution Stage #297

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 33 commits into from
Apr 26, 2025
Merged

Move All Resolution to the Resolution Stage #297

merged 33 commits into from
Apr 26, 2025

Conversation

FlandiaYingman
Copy link

This PR is based on #295 so that there are some duplicated commits. I will fix them once #295 is merged.

It moves the whole implicit arguments resolution to the resolution stage, supporting forward type classes usage.

The features in this PR are complete but there may have some styling or designing issues that require refactorization.

@FlandiaYingman FlandiaYingman changed the title [WIP] Move Implicit Resolution [½ WIP] Move Implicit Resolution Apr 10, 2025
@FlandiaYingman FlandiaYingman requested a review from Copilot April 10, 2025 05:05
Copilot

This comment was marked as off-topic.

Sign in to view

@FlandiaYingman

This comment was marked as off-topic.

Sign in to view
@LPTK LPTK force-pushed the move-implicit-resolution branch from 291be61 to 48d1f31 Compare April 10, 2025 07:03
@FlandiaYingman FlandiaYingman force-pushed the move-implicit-resolution branch from 44d860a to ebe2b51 Compare April 11, 2025 15:07
@LPTK LPTK mentioned this pull request Apr 15, 2025
Merged
@LPTK LPTK marked this pull request as draft April 15, 2025 13:03
@FlandiaYingman FlandiaYingman force-pushed the move-implicit-resolution branch from 7bf2ceb to 424b104 Compare April 16, 2025 06:55
@FlandiaYingman FlandiaYingman marked this pull request as ready for review April 16, 2025 06:56
@FlandiaYingman FlandiaYingman changed the title [½ WIP] Move Implicit Resolution Move All Resolution to the Resolution Stage Apr 16, 2025
@LPTK LPTK marked this pull request as draft April 16, 2025 09:08
FlandiaYingman
FlandiaYingman commented Apr 23, 2025
View reviewed changes
Copy link
Author

@FlandiaYingman FlandiaYingman left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM

@FlandiaYingman FlandiaYingman force-pushed the move-implicit-resolution branch from 0062994 to 3c41858 Compare April 23, 2025 05:32
@FlandiaYingman FlandiaYingman requested a review from LPTK April 23, 2025 05:43
@FlandiaYingman FlandiaYingman marked this pull request as ready for review April 23, 2025 05:44
LPTK
LPTK reviewed Apr 23, 2025
View reviewed changes
Copy link
Contributor

@LPTK LPTK left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nice work! I did not yet have time to review the whole diff, but here are preliminary comments.

hkmc2/shared/src/main/scala/hkmc2/semantics/Term.scala
case _ => N

def withIArgs(iargsLs: Ls[Term.Tup]): Term =
this.iargsLs = S(iargsLs)
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
this.iargsLs = S(iargsLs)
require(this.iargsLs.isEmpty)
this.iargsLs = S(iargsLs)

Copy link
Author

@FlandiaYingman FlandiaYingman Apr 25, 2025 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I just realized that there is probably a hole in the implementation... In the codebase, there are some places (mostly UCS normalization) that use the same term in different places as if they were immutable. So we couldn't simply apply this change. We may need a proper duplication mechanism to resolve this problem.

A more problematic thing is that the implicit arguments of a term might be resolved differently if the same term was used in different places... I changed the condition to this.iargsLs.isEmpty || this.iargsLs.get == iargsLs and fortunately it doesn't report any problem.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Good catch. But I think this will be fine once the UCS normalization is moved to/after the resolution phase: we will probably not even need to duplicate the terms, which will be already resolved.

Cc @chengluyu

mostly UCS normalization

Are there any other places where this happens?

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, a few places in the elaborator. I remember it is somewhere in elaborating SynthSel.

FlandiaYingman and others added 10 commits April 25, 2025 22:42
@FlandiaYingman
Merge branch 'hkmc2' into move-implicit-resolution
a83d71c
@FlandiaYingman @LPTK
Update hkmc2/shared/src/main/scala/hkmc2/semantics/Resolver.scala
13d0dc7 
Co-authored-by: Lionel Parreaux <lionel.parreaux@gmail.com>
@FlandiaYingman @LPTK
Update hkmc2/shared/src/main/scala/hkmc2/semantics/Resolver.scala
51e907c 
Co-authored-by: Lionel Parreaux <lionel.parreaux@gmail.com>
@FlandiaYingman @LPTK
Update hkmc2/shared/src/main/scala/hkmc2/semantics/Elaborator.scala
74fadce 
Co-authored-by: Lionel Parreaux <lionel.parreaux@gmail.com>
@FlandiaYingman @LPTK
Update hkmc2/shared/src/main/scala/hkmc2/semantics/Resolver.scala
99726ff 
Co-authored-by: Lionel Parreaux <lionel.parreaux@gmail.com>
@FlandiaYingman @LPTK
Update hkmc2/shared/src/main/scala/hkmc2/semantics/Resolver.scala
96d9a17 
Co-authored-by: Lionel Parreaux <lionel.parreaux@gmail.com>
@FlandiaYingman @LPTK
Update hkmc2/shared/src/main/scala/hkmc2/semantics/Resolver.scala
2c2f7c0 
Co-authored-by: Lionel Parreaux <lionel.parreaux@gmail.com>
@FlandiaYingman @LPTK
Update hkmc2/shared/src/main/scala/hkmc2/semantics/Resolver.scala
778228f 
Co-authored-by: Lionel Parreaux <lionel.parreaux@gmail.com>
@FlandiaYingman @LPTK
Update hkmc2/shared/src/main/scala/hkmc2/semantics/Resolver.scala
b2cb124 
Co-authored-by: Lionel Parreaux <lionel.parreaux@gmail.com>
@FlandiaYingman
Fix comments
ce4e1f3
LPTK
LPTK requested changes Apr 26, 2025
View reviewed changes
hkmc2/shared/src/main/scala/hkmc2/semantics/Term.scala
case _ => N

def withIArgs(iargsLs: Ls[Term.Tup]): Term =
this.iargsLs = S(iargsLs)
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Good catch. But I think this will be fine once the UCS normalization is moved to/after the resolution phase: we will probably not even need to duplicate the terms, which will be already resolved.

Cc @chengluyu

mostly UCS normalization

Are there any other places where this happens?

LPTK
LPTK approved these changes Apr 26, 2025
View reviewed changes
Copy link
Contributor

@LPTK LPTK left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for another great contribution!

@LPTK LPTK merged commit 53d2587 into hkust-taco:hkmc2 Apr 26, 2025
1 check passed
@FlandiaYingman FlandiaYingman deleted the move-implicit-resolution branch April 26, 2025 13:29
@FlandiaYingman FlandiaYingman mentioned this pull request Apr 26, 2025
Open
12 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

Copilot code review Copilot Copilot left review comments

@LPTK LPTK LPTK approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@FlandiaYingman @LPTK