RequirementMachine: Implement some generic signature queries #38147
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
The `if (other.size() > size())` check was bogus; we can still have an overlap of the second kind if the other term is longer than this term. Remove this check, and rewrite the algorithm to be clearer in general.
slavapestov
force-pushed
the
requirement-machine-queries
branch
from
37440c4 to
0bdeb98
Compare
If you have a same-type requirement like 'Self.Foo == Self' inside a protocol P, we add a rewrite rule: [P].Foo => [P] Simplification turns this into [P:Foo] => [P] Previously, the order was backwards so we would end up with [P] => [P:Foo] Which would mess up the conformance information in the equivalence class map.
slavapestov
force-pushed
the
requirement-machine-queries
branch
from
0bdeb98 to
f7a1d06
Compare
…InContext() query
slavapestov
force-pushed
the
requirement-machine-queries
branch
from
f7a1d06 to
8ffe44f
Compare
|
@swift-ci Please smoke test |
|
@swift-ci Please clean smoke test macOS |
|
@swift-ci Please smoke test macOS |
|
swiftlang/llvm-project#3065 |
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.
This PR implements the following queries on top of the rewrite system:
requiresClass()getLayoutConstraint()requiresProtocol()getRequiredProtocols()isConcreteType()areSameTypeParametersInContext()All but the last one of the above queries are implemented using the "equivalence class map", which is described below. The
areSameTypeParametersInContext()query is implemented directly by reducing the left hand side and right hand side, and then comparing the reduced terms for equality.In asserts builds, the
-enable-requirement-machineflag cross-checks the result of each query against the old implementation of the query that uses the GSB. In no-asserts builds, the requirement machine result is returned without checking when the flag is enabled.In both asserts and no-asserts builds, the flag is off by default, and the new code does not run when the flag is not passed in.
The equivalence class map
In the rewrite system, a conformance requirement
T : Pis represented as rewrite rule of the form:Similarly, layout, superclass, and concrete-type requirements are represented by a rewrite rule of the form:
Where
[p]is a "property atom":[layout: L],[superclass: Foo],[concrete: Bar].Given an arbitrary type T and a property
[p], we can check if T satisfies the property by checking if the two termsT.[p]andTreduce to the same termT'. That is, if our rewrite rules allow us to eliminate the[p]suffix, we knowthe type satisfies
[p].However, the question then becomes, given an arbitrary type T, how do we find all properties
[p]satisfied by T?The trick is that we can take advantage of confluence here.
If
T.[p] => T', andT => T'', then it must follow thatT''.[p] => T'. Furthermore, sinceT''is fully reduced,T'' == T'. SoT'' == UVfor some terms U and V, and there exist be a rewrite ruleV.[p] => V'in the system.Therefore, in order to find all
[p]satisfied by T, we start by fully reducing T, then we look for rules of the formV.[p] => V'where V is fully reduced, and a suffix of T.This is the idea behind the equivalence class map. We collect all rules of the form
V.[p] => V'into a multi-map keyed by V. Then given an arbitrary type T, we can reduce it and look up successive suffixes to find all properties[p]satisfied by T.