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.

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

Closure Specification Inference #1200

Merged
merged 7 commits into from
Oct 26, 2024
Merged

Closure Specification Inference #1200

merged 7 commits into from
Oct 26, 2024

Conversation

xldenis
Copy link
Collaborator

@xldenis xldenis commented Oct 24, 2024

This PR is the reason we adopted Coma in the first place, it allows us to infer the specifications of closures!

The implementation has one weakness: postcondition_mut expects a &mut F which means we need to be able to create a borrow in Pearlite. For this reason I added TermKind::Borrow, which is not super desirable. A motivated soul would refactor closure_capture_subst so that we can change the signature of postcondition_mut but I unfortunately don't currently have enough time to tackle this.

I think that this is still a worthwhile addition in the meantime which makes closures actually usable.

@xldenis xldenis changed the title closure infer new new Closure Specification Inference Oct 24, 2024
@xldenis xldenis force-pushed the closure-infer-new-new branch 6 times, most recently from 6529ab7 to 8e1863e Compare October 26, 2024 08:45
@arnaudgolfouse
Copy link
Collaborator

I see you updated some tests to use this, it looks good! Do you think should_succeed/option.rs could also benefit from this? 😁

@xldenis xldenis merged commit 87d476a into master Oct 26, 2024
4 checks passed
@xldenis xldenis deleted the closure-infer-new-new branch October 26, 2024 16:15
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants