RequirementMachine: Relate rules introduced by concrete type unification via rewrite loops #41159
Conversation
This file contains hidden or 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
slavapestov
force-pushed
the
concrete-unification-vs-rewrite-loop
branch
5 times, most recently
from
c9e3a5f to
9549444
Compare
Contributor
Author
|
@swift-ci Please test source compatibility |
slavapestov
force-pushed
the
concrete-unification-vs-rewrite-loop
branch
4 times, most recently
from
a3ada4e to
da94bf0
Compare
Contributor
Author
|
@swift-ci Please smoke test |
Contributor
Author
|
@swift-ci Please test source compatibility |
slavapestov
force-pushed
the
concrete-unification-vs-rewrite-loop
branch
from
da94bf0 to
abeeb79
Compare
Contributor
Author
|
@swift-ci Please smoke test |
…r use by the property map
…o use computeTypeDifference() This doesn't record rewrite loops from most concrete unifications just yet, only handling a case where two concrete types were identical except for an adjustment.
…SideSubstitutions()
- Rename StepLimit to MaxRuleCount, DepthLimit to MaxRuleLength
- Rename command line flags to -requirement-machine-max-rule-{count,length}=
- Check limits outside of PropertyMap::buildPropertyMap()
- Simplify the logic in RequirementMachine::computeCompletion()
Configured with -requirement-machine-max-concrete-nesting= frontend flag.
… rule if completion failed This surfaces an implementation detail, but it might be better than nothing.
…ad of asserting on incomparable symbols
…unifying to concrete type rules
…in processTypeDifference() We can't actually rely on concretelySimplifyLeftHandSideSubstitutions() to do this for us, because the less-simplified rule (the LHS rule) might only apply to a suffix of the base term.
…eteTypeProperty()
slavapestov
force-pushed
the
concrete-unification-vs-rewrite-loop
branch
from
abeeb79 to
729dfc7
Compare
Contributor
Author
|
@swift-ci Please smoke test |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
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.
The property map performed unification of concrete type terms, so that for example if you had
T == G<Int>andT == G<U>, we would infer thatU == Int. This worked for generic signature queries, however minimization did not understand concrete type unification because the new rules were not given a rewrite path expressing them in terms of existing rules.In our example, any two of the requirements
T == G<Int>, T == G<U> and U == Intimply the third. This means we need rewrite loops relating them. There are two loops:U == Intin empty context, andT == G<Int>andT == G<U>in non-empty context. This means if chosen, the first loop allowsU == Intto be eliminated.T == G<Int>andT == G<U>in empty context, withU == Intappearing in context. This means that if chosen, the second loop allows either of those two rules can be eliminated.The first loop is introduced when property unification records the rule
U == Int.The second loop is introduced by a new simplification pass that runs after property map construction. This pass replaces type parameters with concrete types in concrete type rules, so for example
T == G<U>is simplified down toT == G<Int>. This will record the new ruleT == G<Int>if it doesn't exist already, and record a rewrite loop relatingT == G<Int>andT == G<U>.A priori, there's no reason for homotopy reduction to pick either
T == G<Int>orT == G<U>over the other for elimination, however the simplification pass marksT == G<U>as simplified, which means we try to eliminate it earlier.The relation between two different instantiations of a concrete type symbol, like
G<U>andG<Int>is recorded in a new uniqued TypeDifference object in the RewriteSystem. The TypeDifference describes a set of transformations for converting a less-specific left hand side (G<U>) into a more-specific right hand side (G<Int>) via a series of concrete type rules (in this case,U == Int).The new
LeftConcreteProjectionandRightConcreteProjectionrewrite steps relate the left hand side and right hand side of an induced rule with the two concrete type rules that induced it. This rewrite step kind appears in the first type of rewrite loop described above.The new
DecomposeConcreterewrite step kind transforms the left hand side of a TypeDifference into the right hand side, or vice versa. This rewrite step kind appears in the second type of rewrite loop described above.This is the concrete type part of rdar://problem/88134910. Superclass unification still needs additional work to model intersections between a derived class and a base class.