- 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()
We have three simplification passes, give each one its own predicate:
- Left hand side simplification
- Right hand side simplification
- Substitution simplification
This is for debugging output and will also allow me to tighten up
some invariants.
Conditional requirement inference needs to be able to add rewrite rules
from the requirement signatures of hitherto-unseen protocols, so to
help with that, extract out the RuleBuilder's ProtocolMap and move it
into the RewriteSystem.
When minimizing a generic signature, we only care about loops
where the basepoint is a generic parameter symbol.
When minimizing protocol requirement signatures in a connected
component, we only care about loops where the basepoint is a
protocol symbol or associated type symbol whose protocol is
part of the connected component.
All other loops can be discarded since they do not encode
redundancies that are relevant to us.
A superclass requirement 'T : C' implies a layout requirement
'T : AnyObject' (if the class is @objc) or 'T : _NativeObject'
(if the class is not @objc).
In the latter case, there might already be a 'T : AnyObject'
requirement, in which case the type parameter 'T' is subject
to two layout requirements:
T : AnyObject
T : _NativeObject
The second requirement implies the first however. To encode this
in the world of rewrite loops, we the notion of a 'relation'
between property symbols, and a 'Relation' rewrite step.
Here, the relation is that _NativeObject < AnyObject. Once this
relation is recorded, the Relation rewrite step will transform
T.[layout: _NativeObject].[layout: AnyObject]
into
T.[layout: _NativeObject]
and vice versa.
This rewrite step allows us to construct a rewrite loop which
makes the first rewrite rule redundant via the second.
First pass:
- Eliminate rules with unresolved name symbols in LHS
- Eliminate simplified non-conformance rules
Second pass:
- Eliminate non-minimal conformance rules
Third pass:
- Eliminate all other non-conformance rules
If you have a concrete requirement with a non-canonical substitution, like
A : P, A == G<B.T>
We add an induced rule for the abstract type witness,
A.T == B.T
This rule has a rewrite path in terms of the previous two rules, but we
want to try to eliminate the other two rules first.
This new ordering ensures we eliminate the simplified rule A == G<B.T> and
compute minimal conformances before we get around to considering A.T == B.T,
which can no longer be eliminated by that point.
If we eliminate A.T == B.T first, we end up with simplified concrete
type and concrete conformance rules which cannot be eliminated:
A.[concrete: G<B.T>] => A
A.[concrete: G<B.T> : P] => A
This changes the minimized signature in an incompatible way in two test cases.
In Generics/rdar83308672.swift, the signature becomes equivalent to what the
GSB used to output.
In Generics/sr10532.swift, the GSB would output an invalid signature anyway,
so it doesn't matter.
Previously we did this when adding new concrete type rules,
but we don't have a complete rewrite system at that point yet,
so there was no guarantee concrete substitution terms would
be canonical.
Now, perform simplification in a post-pass after completion,
at the same time as simplifying rule right hand sides.
Rewrite loops are recorded relating the original rule with the
simplified substitutions.
This is a source-level error, not an invariant violation. Instead, plumb
a new hadError() flag, which in the future will assert if no diagnostic
was produced.
If a rewrite loop contains two rules in empty context and one of them
is explicit, propagate the explicit bit to the other rule if the original
rule was found to be redundant.
This means that if we begin with an unresolved rule like
[P].X.[Q] => [P].X [explicit]
And then completion added the resolved rule
[P:X].[Q] => [P:X]
Then the new rule will become explicit once the original rule becomes
redundant.
This was a hack from before the change to minimize away the
least canonical rules first. Now, there's no reason to perform
a separate pass over rules containing unresolved name symbols.
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.
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.
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.
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.
