Instead of keeping track of the best one so far, and unifying subsequent rules
against it.
This allows us to record more identities, fixing a regression from an earlier
change where we were unable to eliminate an obviously-redundant rule.
- 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.
It doesn't actually do this yet, but the idea is to look at the
total rule count before and after, instead of just looking at the
induced rules array (which I will delete in the next commit).
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.
For homotopy reduction to properly deal with new rules introduced
while bulding the property map, rewrite loops must be recorded
relating these to existing rules.
For homotopy reduction to properly deal with rewrite rules
introduced by property map construction, we need to keep
track of the original property rules when recording properties
in property bags.
For now, this doesn't even attempt to handle unification or
conflicts; we only record the first rule for each kind of
property on a fixed key.
This isn't actually used for anything yet, except a new
verify pass that runs after property map construction.
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.
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>.
protocol Q {
associatedtype T where T == Self?
}
func foo<X, Y : Q>(_: X, _: Y) {}
This generates the rewrite system
[Q:T].[concrete: Optional<τ_0_0> with <[Q]>]
τ_0_1.[Q] => τ_0_1
With this property map:
[Q:T] => { [concrete: Optional<τ_0_0> with <[Q]>] }
τ_0_1 => { [Q] }
Suppose we're resolving the concrete type τ_0_1.[Q:T]. The property map
entry is keyed by [Q:T], so the prefix τ_0_1 must be prepended to the
concrete substitutions of [concrete: Optional<τ_0_0> with <[Q]>].
However, [Q] is just the protocol Self type, and τ_0_0.[Q] is not a
valid type-like term. We could simplify the term before building the
Swift type which would apply the second rewrite rule, but it's easier
to just drop the protocol symbol in this case.
Just as with concrete types, if we find that the same suffix has two
different superclass symbols in the property map, we need to introduce
same-type requirements between their generic parameters.
The added wrinkle is that the classes might be different; in this case,
one must be a superclass of the other, and we repeatedly substitute
the generic arguments until we get the generic arguments of the
superclass before we unify.
