Goal builder #361
Goal builder #361
Conversation
|
Haven't really looked it over yet, but I'm definitely happy about this. It should make lowering Goals for rustc easier. |
The goal here is to make this code more readable and less ad-hoc.
nikomatsakis
force-pushed
the
goal-builder
branch
2 times, most recently
from
e3cbf1e
to
10013b1
Compare
For a GAT like
```
impl<T> Foo<T> { type Bar<'a> = ..}
```
Instead of constructing nested quantifiers like
```
forall<T> {
if (..) {
stuff &&
forall<'a> { more_stuff }
}
}
```
we will now build separate goals
```
forall<T> { if (...) { stuff } } &&
forall<T, 'a> { if (...) { more_stuff } }
```
This both removes the need for the 'partial' forall methods in
GoalBuilder butalso means we would be able to give better error
messages in rustc at somepoint, since we can test "is this impl header
WF" separately from "is this associated type value WF" etc.
nikomatsakis
force-pushed
the
goal-builder
branch
from
ec7d394
to
4acecc2
Compare
|
OK, the PR history took a bit of a round-about path, but I'd say this is ready for comment. Probably best to just view the "whole diff". The new APIs are in The wf.rs and coherence changes are porting code to use the goal builder. I think the result is much more readable, and it also includes no manual adjusting of debruijn indices. It's much harder to get things wrong, and the "general visual structure" of the code matches the logical goal we are building. Still, the code is more verbose than I had hoped. The new APIs do lead to a little more cloning than we used to have, but I'm not concerned. I wouldn't expect these pathways to be perf sensitive in the real compiler, and we could optimize if that were ever a problem. One possible change worth making: converting Another slight annoyance that crops up a few times is that we have to thread the id of various datums into |
chalk-solve/src/goal_builder.rs
Outdated
| { | ||
| let interner = self.interner(); | ||
| let bound_goal = binders.map_ref(|bound_value| { | ||
| let substitution: Substitution<I> = Substitution::from( |
There was a problem hiding this comment.
Can you move this out of this out of the map_ref closure? Then just either pass a &Substitution or clone? It makes it a little bit more obvious what's going on.
There was a problem hiding this comment.
I can move it out of the closure, but I'm not sure what you mean by "passing a &Substitution or clone" -- you'd rather I not give ownership of the Substitution? Or would you rather I clone the contents of the binder?
In some variant, I had the signature of the body be:
Substitution<I>B::Result(i.e., contents of binder, instantiated withSubstitution)P::Result(i.e., contents of passthru, shifted)
I changed to &B because, in fact, the substitution is always an identity substitution (in the earlier version, this wasn't always the case), so doing a substitution wasn't really necessary. But I think the above signature is kind of the most "obvious" signature, and I'd be reasonably happy to adopt it (since I think readability trumps most concerns here).
Initial work on introducing a "goal builder", with the aim of making the wf and coherence code easier to read and less error-prone. This is only part-way through. Builds on #360.