With this change the RequirementMachine's minimization behavior with
protocol refinement rules matches the GenericSignatureBuilder.
See https://github.com/apple/swift/pull/37466 for a full explanation
of what's going on here.
A superclass requirement implies a layout requirement. We don't
want the layout requirement to be present in the minimal
signature, so instead of adding a pair of requirements:
T.[superclass: C<X, Y>] => T
T.[layout: _NativeClass] => T
Add this pair of requirements:
T.[superclass: C<X, Y>] => T
[superclass: C<X, Y>].[layout: _NativeClass] => [superclass: C<X, Y>] [permanent]
Completion then derives the rule as a consequence:
T.[layout: _NativeClass] => T
Since this rule is a consequence of the other two rules, homotopy
reduction will mark it redundant.
This is a refactoring needed to implement 'verify' mode. The
RequirementMachine computes the requirement signature for an
entire connected component of protocols at once, whereas the
GenericSignatureBuilder only does one protocol at a time.
Using the same request for both in 'verify' mode meant that
we would only call the GSB for the first protocol in a
connected component, and then the RequirementMachine would
fill in the rest.
To fix this, split it up into two requests. The original
RequirementSignatureRequest calls into the GSB, and then
kicks off a RequirementSignatureRequestRQM to get the
requirement signature computed by the RequirementMachine
(possibly cached, if this protocol is part of a connected
component with more than one protocol in it).
When re-contextualizing a path containing RewriteStep::Decompose,
don't update StartOffset/EndOffset for steps that execute with
more than one term on the stack.
Using StartOffset to encode the prefix length is wrong, because
then we get an invalid rewrite step after replaceRuleWithPath().
Instead, encode the prefix length in the RuleID field.
Now that the property map stores a reference to the RewriteSystem,
defining the buildPropertyMap() method on PropertyMap feels cleaner,
and allows more of the property map's internals to be private.
Just like in homotopy reduction, when finding a minimal set of generating
conformances, we should try to eliminate less canonical conformance rules
first.
This fixes a test case where we would delete a more canonical conformance
requirement, triggering an assertion that simplifed rules must be
redundant, because the less canonical conformance was simplified, whereas
the more canonical one was redundant and not simplified.
Consider this example:
protocol P {
associatedtype X : P where X == Self
}
Clearly the conformance requirement 'X : P' is redundant, but previously
nothing in our formulation would make it so.
Here is the rewrite system:
(1) [P:X].[P] => [P:X]
(2) [P:X] => [P]
These two terms overlap on [P:X].[P]; resolving the critical pair introduces
the 'identity conformance' [P].[P] => [P]. Homotopy reduction would delete
this conformance, but at this point, [P:X].[P] => [P:X] would no longer be
redundant, since nothing else proves that [P].[P] => [P].
Now that [P].[P] => [P] is a permanent rule, we can handle this properly;
any conformance that appears in a rewrite loop together with an identity
conformance without context is completely redundant; it is equivalent to the
empty generating conformance path.
Now that the 'identity conformance' [P].[P] => [P] is permanent,
we won't see it here, so we can just assume that any non-permanent,
non-redundant rule maps to a requirement.
Instead of finding the best redundancy candidate from the first
homotopy generator that has one, find the best redundancy
candidate from *all* homotopy generators that have one.
This correctly minimizes the "Joe Groff monoid" without hitting
the assertion guarding against simplified rules being non-redundant.
It also brings us closer to being able to correctly minimize
the protocol from https://bugs.swift.org/browse/SR-7353.
Completion adds this rule when a same-type requirement equates the Self of P
with some other type parameter conforming to P; one example is something like this:
protocol P {
associatedtype T : P where T.T == Self
}
The initial rewrite system looks like this:
(1) [P].T => [P:T]
(2) [P:T].[P] => [P:T]
(3) [P:T].[P:T] => [P]
Rules (2) and (3) overlap on the term
[P:T].[P:T].[P]
Simplifying the overlapped term with rule (2) produces
[P:T].[P:T]
Which further reduces to
[P]
Simplifying the overlapped term with rule (3) produces
[P].[P]
So we get a new rule
[P].[P] => [P]
This is not a "real" conformance rule, and homotopy reduction wastes work
unraveling it in rewrite loops where this rule occurs. Instead, it's better
to introduce it as a permanent rule that is not subject to homotopy reduction
for every protocol.
Suppose we have these rules:
(1) [P].[P] => [P]
(2) [P].[P:X] => [P:X]
(3) [P].[P:Y] => [P:Y]
(4) [P:X].[concrete: G<τ_0_0> with <[P:Y]>]
Rule (2) and (4) overlap on the following term, which has had the concrete
type adjustment applied:
[P].[P:X].[concrete: G<τ_0_0> with <[P].[P:Y]>]
The critical pair is obtained by applying rule (2) to both sides of the
branching is
[P:X].[concrete: G<τ_0_0> with <[P].[P:Y]>] => [P:X]
Note that this is a distinct rule from (4), and again this new rule overlaps
with (2), producing another rule
[P:X].[concrete: G<τ_0_0> with <[P].[P].[P:Y]>] => [P:X]
This process doesn't terminate. The root cause of this problem is the
existence of rule (1), which appears when there are multiple non-trivial
conformance paths witnessing the conformance Self : P. This occurs when a
same-type requirement is defined between Self and some other type conforming
to P.
To make this work, we need to simplify concrete substitutions when adding a
new rule in completion. Now that rewrite paths can represent this form of
simplification, this is easy to add.
I need to simplify concrete substitutions when adding a rewrite rule, so
for example if X.Y => Z, we want to simplify
A.[concrete: G<τ_0_0, τ_0_1> with <X.Y, X>] => A
to
A.[concrete: G<τ_0_0, τ_0_1> with <Z, X>] => A
The requirement machine used to do this, but I took it out, because it
didn't fit with the rewrite path representation. However, I found a case
where this is needed so I need to bring it back.
Until now, a rewrite path was a composition of rewrite steps where each
step would transform a source term into a destination term.
The question then becomes, how do we represent concrete substitution
simplification with such a scheme.
One approach is to rework rewrite paths to a 'nested' representation,
where a new kind of rewrite step applies a sequence of rewrite paths to
the concrete substitution terms. Unfortunately this would complicate
memory management and require recursion when visiting the steps of a
rewrite path.
Another, simpler approach that I'm going with here is to generalize a
rewrite path to a stack machine program instead.
I'm adding two new kinds of rewrite steps which manipulate a pair of
stacks, called 'A' and 'B':
- Decompose, which takes a term ending in a superclass or concrete type
symbol, and pushes each concrete substitution on the 'A' stack.
- A>B, which pops the top of the 'A' stack and pushes it onto the 'B'
stack.
Since all rewrite steps are invertible, the inverse of the two new
step kinds are as follows:
- Compose, which pops a series of terms from the 'A' stack, and replaces
the concrete substitutions in the term ending in a superclass or
concrete type symbol underneath.
- B>A, which pops the top of the 'B' stack and pushes it onto the
'B' stack.
Both Decompose and Compose take an operand, which is the number of
concrete substitutions to expect. This is encoded in the RuleID field
of RewriteStep.
The two existing rewrite steps ApplyRewriteRule and AdjustConcreteType
simply pop and push the term at the top of the 'A' stack.
Now, if addRule() wishes to transform
A.[concrete: G<τ_0_0, τ_0_1> with <X.Y, X>] => A
into
A.[concrete: G<τ_0_0, τ_0_1> with <Z, X>] => A
it can construct the rewrite path
Decompose(2) ⊗ A>B ⊗ <<rewrite path from X.Y to Z>> ⊗ B>A ⊗ Compose(2)
This commit lays down the plumbing for these new rewrite steps, and
replaces the existing 'evaluation' walks over rewrite paths that
mutate a single MutableTerm with a new RewritePathEvaluator type, that
stores the two stacks.
The changes to addRule() are coming in a subsequent commit.
We didn't look at the length of terms appearing in concrete substitutions,
so runaway recursion there was only caught by the completion step limit
which takes much longer.
Previously we said that if P1 inherits from P2, then [P1:T] < [P2:T].
However, this didn't generalize to merged associated type symbols;
we always had [P1&P2:T] < [P3:T] even if P3 inherited from both P1
and P2.
This meant that the 'merge' operation did not preserve order, which
fired an assertion in the completion logic.
Fix this by generalizing the linear order to compare the 'support'
of protocols rather than the 'depth', where the 'support' is
defined as the size of the transitive closure of the set under
protocol inheritance.
Then, if you have something like
protocol P1 {}
protocol P2 {}
protocol P3 : P1, P2 {}
The support of 'P1 & P2' is 2, and the support of 'P3' is 3,
therefore [P3:T] < [P1&P2:T] in this example.
Fixes <rdar://problem/83768458>.
When a type parameter is subject to a conformance requirement and a
concrete type requirement, the concrete type unification pass
recursively walks each nested type introduced by the conformance
requirement, and fixes it to the concrete type witness in the
concrete type conformance.
In general, this can produce an infinite sequence of concrete type
requirements. There are a couple of heuristics to "tie off" the
recursion.
One heuristic is that if a nested type of a concrete parent type is
exactly equal to the parent type, a same-type requirement is
introduced between the child and the parent, preventing concrete
type unification from recursing further.
This used to check for exact equality of types, but it is possible
for the type witness to be equal under canonical type equivalence,
but use a different spelling via same-type requirements for some
type parameter appearing in structural position.
Instead, canonicalize terms here, allowing recursion where the
type witness names a different spelling of the same type.
Fixes <rdar://problem/83894546>.
Also while plumbing this through, don't record homotopy generators
unless we're minimizing a protocol signature, since they're not
used for anything else yet.
