Validate that rewrite constraints match the requirements #5506
Conversation
|
The changes to eval are kind of terrible, but this is a starting point that works and shows what is needed, from which we can discuss what to actually do. |
danakj
force-pushed
the
validate-rewrites
branch
3 times, most recently
from
569afc9 to
7fdd7fe
Compare
|
I have gone ahead and cleaned up the impl lookup code now since it is not immediately obvious that this is not how we need to/should solve this problem. I resolved a TODO to share more code between impl lookup and eval by doing the canonicalization of the |
| } | ||
|
|
||
| // Returns each RewriteRule found in the FacetType, then returns nullopt. | ||
| auto Next() -> std::optional<RewriteRule> { |
There was a problem hiding this comment.
I should explain what is going on here.
I wrote the tool to get rewrite rules from a facet type (here) and from a witness table (below) each as a generator object. Or you could think of it as an iterator in the shape of Rust. The reason I wrote it this way is to avoid allocating 2 more vectors on the heap just to collect things to iterate over and immediately discard/free. It's not significantly more difficult IMO to follow what is going on, the difference is just largely that it stores the current iterator as a field in each generator/iterator class.
If you're interested, in the future, we could introduce an adaptor that takes a class with an auto Next() -> optional<T> method and turns it into a C++ range with begin/end that return types with appropriate operators. That would allow us to write below
for (auto rule: MakeIter(RewriteRulesFromFacetType(...))) { ... }instead of the current
for (auto rules = RewriteRulesFromFacetType(...);
auto rule = rules.Next();) { ... }
|
I have added This will benefit from #5517 but it's not dependent on it. This removes the eval.cpp specialization for |
|
I have rebased this onto trunk to make it easier to review, and get tests to run again, so it now already includes #5517. |
When doing impl lookup from a concrete value, or converting between facet values (which is implemented as impl lookup), ensure that the rewrite constraints known about the source value cover all of the requirements from the target facet type, and do not contradict any requirements.
To do this, we need additional information returned from the second stage of
LookupImplWitness()(the stage on the other side of eval), to know the FacetType from which a symbolicLookupImplWitnessfinds its answer. The instruction itself erases that information, since it will continuing looking for a concrete answer on further (more specific) evaluations, but LookupImplWitness() needs the facet type to combine the rewrite constraints across all found witnesses and verify that they satisfy the query's constraints.