Initial support for traits in impure code #51
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
xldenis
reviewed
May 21, 2024
xldenis
reviewed
May 21, 2024
Comment on lines
263
to
274
| let call_trait_substs = | ||
| ty::EarlyBinder::bind(trait_ref.args).instantiate(tcx, impl_method_substs); | ||
| let impl_substs = ty::List::identity_for_item(tcx, impl_def_id); | ||
| let trait_method_substs = tcx.mk_args_from_iter( | ||
| call_trait_substs | ||
| .iter() | ||
| .chain(impl_method_substs.iter().skip(impl_substs.len())), | ||
| ); | ||
|
|
||
| // sanity check: do we now have the correct number of substs? | ||
| let identity_trait_method = ty::List::identity_for_item(tcx, trait_method_def_id); | ||
| assert_eq!(trait_method_substs.len(), identity_trait_method.len()); |
There was a problem hiding this comment.
I'm a bit fuzzy now, but I believe this is what rustc internally calls "rebasing" the substitution, no? Can we not just use that?
There was a problem hiding this comment.
Refactored to use rebase_onto. For some reason, the Nevermind, I wasn't using it correctly initially.rebase_onto operation doesn't include the initial subst for Self in the trait generics (e.g. Foo -> Self for impl Trait for Foo), so that needs to be added back in.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Start support for traits in impure code.
This PR does not yet support encoding the traits themselves as domains in Viper yet.
No support for type-conditional spec refinement yet.