Remove `deque` from files it isn't actually used in. Add it and `stack`
to files that it is - presumably they were previously transitively found
through other includes.
Although I don't plan to bring over new assertions wholesale
into the current qualification branch, it's entirely possible
that various minor changes in main will use the new assertions;
having this basic support in the release branch will simplify that.
(This is why I'm adding the includes as a separate pass from
rewriting the individual assertions)
When computing an overlap between a property-like rule (T.[p] => T for some
property symbol [p]) and another rule, try harder to ensure that the new
rule is a property-like rule.
In a conformance-valid rewrite system, all rules that are not LHS- or RHS-
simplified will eventually either be property-like or same-type rules, but
we need to maintain this invariant for that rules that become simplified
as well, to ensure that rewrite loops have a certain structure that is
important for the minimal conformances algorithm.
I don't quite understand why to be honest, but I'm close to figuring it
out.
Fixes rdar://problem/91232987.
Completion has a maximum rule limit since the Knuth-Bendix algorithm
is a semi-decision procedure that does not terminate on all inputs.
However, this means that generic signatures which import a large
number of complex protocols can hit the limit even if they are
convergent.
Since imported rules are essentially free, ignore them here, to
avoid having to increase the limit by hand.
Now the default limit is 4000 local rules per requirement machine;
it seems implausible that you would exceed this, but if anyone has
an example we can bump the limit again.
These rules would be fine since RHS simplification eliminates them,
but they cause problems for the minimal conformances algorithm.
To avoid introducing such rules, ensure that the critical pair of
two property-like rules is itself a property-like rule instead of
relying on subsequent simplifications sorting it out. See the
new comment in RewriteSystem::computeCriticalPair() for details.
I need to understand this problem better and either fix minimal
conformances or add stronger assertions, but for now this fixes
the last failure with -requirement-machine-abstract-signatures=verify.
Now that the PropertyMap to the concrete simplification version is optional,
we can just pass nullptr here to get the old behavior where type terms are
simplified to canonical anchors and no concrete simplification is performed.
- 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.
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.
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.
Filter out trivial overlaps where a rule overlaps entirely with
itself before looking at CheckedOverlaps. Otherwise, we'll miss
overlaps where a rule overlaps with itself at a non-zero
position.
When a rewrite rule is replaced with a path containing ::Adjust, ::Decompose,
::ConcreteConformance or ::SuperclassConformance rewrite steps, the steps
will get a non-zero EndOffset if the original rule appears in a step with a
non-zero EndOffset.
For this reason, these steps must work with a non-zero EndOffset, which
primarily means computing correct offsets into the term being manipulated.
