Commit Graph

17 Commits

Author SHA1 Message Date
Slava Pestov
0e4c398048 RequirementMachine: Tweak completion loop condition 2022-03-07 23:13:05 -05:00
Slava Pestov
5e54a52c0e RequirementMachine: Remove old implementation of simplifyLeftHandSideSubstitutions()
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.
2022-02-15 04:02:46 -05:00
Slava Pestov
e2e088e082 RequirementMachine: Remove merged associated types from completion 2022-02-07 18:57:45 -05:00
Slava Pestov
037dc98845 RequirementMachine: Generalize compare() methods to return None instead of asserting on incomparable symbols 2022-02-07 08:20:59 -05:00
Slava Pestov
37be2d5dd7 RequirementMachine: Emit a diagnostic note with the offending rewrite rule if completion failed
This surfaces an implementation detail, but it might be better
than nothing.
2022-02-07 08:20:59 -05:00
Slava Pestov
634ca55764 RequirementMachine: Rework completion limits a bit
- 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()
2022-02-07 08:20:59 -05:00
Slava Pestov
d8aa79c5e5 RequirementMachine: Rename RewriteStep::AdjustConcreteType to ::PrefixSubstitutions 2022-02-07 08:20:58 -05:00
Slava Pestov
a11151a7e3 RequirementMachine: Fix up some comments 2022-02-04 22:49:28 -05:00
Slava Pestov
106896228e RequirementMachine: Split up Rule::isSimplified() into three predicates
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.
2022-01-27 18:54:03 -05:00
Slava Pestov
1c1b0e6cfc RequirementMachine: Clean up computeCriticalPair() a bit 2022-01-27 18:54:03 -05:00
Slava Pestov
746f4a5a8f RequirementMachine: Throw out rewrite loops not part of the minimization domain
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.
2022-01-05 23:59:46 -05:00
Slava Pestov
5ac43b14d2 RequirementMachine: Fully canonicalize substitutions in concrete type rules
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.
2021-12-13 18:48:23 -05:00
Slava Pestov
7f7bf2fa97 RequirementMachine: Fix subtle bug in Knuth-Bendix algorithm
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.
2021-12-10 00:49:46 -05:00
Slava Pestov
c1339240cd RequirementMachine: Add flags to enable and disable merged associated types
On by default, no change from current behavior. I'm going to try turning
this off (and hopefully ripping it out entirely) once I fix a few bugs.
2021-12-08 21:32:42 -05:00
Slava Pestov
2f2249cef1 RequirementMachine: Fix various RewriteSteps to work when re-contextualized
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.
2021-12-08 00:53:35 -05:00
Slava Pestov
d19b15b66c RequirementMachine: Introduce Symbol::Kind::ConcreteConformance 2021-12-06 23:04:46 -05:00
Slava Pestov
15bf00148d RequirementMachine: Rename RewriteSystemCompletion.cpp to KnuthBendix.cpp 2021-11-10 00:18:18 -05:00