-
Notifications
You must be signed in to change notification settings - Fork 14
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
Add precise filtering of which items to translate #316
Conversation
b0bc39a
to
62c0e8e
Compare
62c0e8e
to
33539f6
Compare
name: String, | ||
generics: Vec<PatTy>, | ||
/// For pretty-printing only: whether this is the name of a trait. | ||
is_trait: bool, |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It would make sense to also use it for matching I think.
For the Charon-ML side: we should have the same, but should also use it for matching (if true
, we can only match a trait impl; if false
then no restriction because we can use the syntax without impl ... for ...
both for regular impls and trait impls).
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'm not sure how useful that is: there cannot be a trait with the same name as a type
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Well, I guess with wildcards there can be 🤔
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Actually you're probably right: it may be useless. But I was mostly thinking about consistency/sanity...
It's super nice to finally have this, thanks :) |
This PR adds a rust implementation of something like the
NameMatcher
. This makes it possible to precisely filter items precisely, e.g. translate exactly one impl from the standard library. This fixes the issue of--extract-opaque-bodies
triggering a slurry of errors. This is still a bit rough but already useful.Fixes #214