RequirementMachine: A term rewriting system for reasoning about generic signatures #37675
Conversation
slavapestov
force-pushed
the
gsb-v2
branch
2 times, most recently
from
e09f6f8
to
b693027
Compare
|
@swift-ci Please test |
|
@swift-ci Please test source compatibility |
|
Build failed |
|
Build failed |
slavapestov
changed the title
|
@swift-ci Please test source compatibility |
include/swift/AST/RewriteSystem.h
Outdated
| Term() {} | ||
|
|
||
| explicit Term(llvm::SmallVector<Atom, 3> &&atoms) | ||
| : Atoms(atoms) {} |
There was a problem hiding this comment.
N.B. There’s a copy here. Might wanna use std::move to preserve the rvalue-ness.
| : Atoms(atoms.begin(), atoms.end()) {} | ||
|
|
||
| void add(Atom atom) { | ||
| Atoms.push_back(atom); |
There was a problem hiding this comment.
Same here: emplace_back and a move are probably slight wins.
There was a problem hiding this comment.
Atom will soon become uniqued/immutable so I'll leave this alone for now.
lib/AST/ASTContext.cpp
Outdated
|
|
||
| // Store this requirement machine before adding the signature, | ||
| // to catch re-entrant construction. | ||
| machines[sig] = std::unique_ptr<RequirementMachine>(machine); |
There was a problem hiding this comment.
Nit: Could save a lookup by doing a lookup above then emplacing into it if there’s no existing match for the signature.
| @@ -4026,7 +4026,7 @@ GenericSignatureBuilder::getConformanceAccessPath(Type type, | |||
|
|
|||
| auto *Stats = Context.Stats; | |||
|
|
|||
| FrontendStatsTracer(Stats, "get-conformance-access-path"); | |||
| FrontendStatsTracer tracer(Stats, "get-conformance-access-path"); | |||
| unsigned depth = 0; | ||
|
|
||
| for (auto *inherited : info.Inherited) { | ||
| unsigned inheritedDepth = computeProtocolDepth(inherited); |
There was a problem hiding this comment.
Is there any risk of this recursion blowing out the stack? Seems unlikely, but might want to use a worklist.
There was a problem hiding this comment.
Refactoring this to use a worklist is going to be a little bit tricky. We recurse over inherited protocols in other places too. Note that we should already be able to detect cycles here, because of the 'Mark' bit.
We can have a layout requirement 'T : _UnknownLayout', and _UnknownLayout answers false to isKnownLayout().
|
@swift-ci Please smoke test |
Motivation
The GenericSignatureBuilder is used for four purposes:
The RequirementMachine is meant to provide a direct replacement for the first item above, as well as more solid underpinnings for the other three.
Implementation
A RequirementMachine consists of a term rewriting system built from a set of rewrite rules. The rewrite rules are the top-level requirements in the original generic signature, together with the union of all protocol requirement signatures of all protocols that are transitively referenced via conformance requirements.
The Knuth-Bendix algorithm together with an addition is used to compute the confluent completion. The basic completion algorithm looks for types
Twhich can be reduced into two distinct minimal typesT'andT'', and then adds a rewrite ruleT' == T'', iterating the process if needed. The addition to the completion algorithm is meant to resolve certain difficult cases where associated types with the same name from different protocols must be merged together.The
-requirement-machine-depth-limitand-requirement-machine-step-limitfrontend flags provide an upper bound on the amount of work done by the completion procedure. If the completion procedure terminates, we have a generic signature with a decidable word problem.If the generic signature does not have a decidable word problem, completion will fail. It also necessarily fails in some decidable cases.
Current status
This PR introduces an implementation of the RequirementMachine that supports conformance, layout and same-type requirements. The main entry point is a method on ASTContext for lazily creating RequirementMachines from GenericSignatures, named
getOrCreateRequirementMachine(). This new method is analogous togetOrCreateGenericSignatureBuilder().For now, if the
-enable-requirement-machinefrontend flag is passed in, a RequirementMachine is built for each generic signature, but it is not actually used for anything. The flag is off by default.Next steps
The next major milestone is adding support for concrete type and superclass requirements.
Once that's done, we can actually start using the RequirementMachine for generic signature queries. This can be staged in gradually, with parallel implementations and cross-checking between the new and old query results. At this point we will also need to optimize the rewriting engine, since it is intentionally not very good about avoiding unnecessary copying and memory allocation; furthermore, tries can be used to speed up lookups significantly.
Finally, the last step is to re-implement the GenericSignatureBuilder's algorithms for conformance access paths and requirement minimization on top of the RequirementMachine, at which point the GenericSignatureBuilder can be removed.`
References