- Skip permanent rules (there's no point, we'll add them back next time)
- Skip conformance rules (these will be handled separately)
- Delete 3-cells that are entirely "in-context" (but don't quote me on
this one, I'm not quite yet convinced it's correct, but it feels right)
The left and right hand side of a merged associated type candidate rule
have a common prefix except for the associated type symbol at the end.
Instead of passing two MutableTerms, we can pass a single uniqued
Term and a Symbol.
Also, we can compute the merged symbol before pushing the candidate
onto the vector. This avoids unnecessary work if the merged symbol
is equal to the right hand side's symbol.
In a confluent rewrite system, if the left hand side of a rule
X => Y can be reduced by some other rule X' => Y', then it is
permissible to delete the original rule X => Y altogether.
Confluence means that rewrite rules can be applied in any
order, so it is always valid to apply X' => Y' first, thus
X => Y is obsolete.
This was previously done in the completion procedure via a
quadratic algorithm that attempted to reduce each existing
rule via the newly-added rule obtained by resolving a critical
pair. Instead, we can do this in the post-processing pass
where we reduce right hand sides using a trie to speed up
the lookup.
This increases the amount of work performed by the
completion procedure, but eliminates the quadratic algorithm,
saving time overall.
The PropertyMap wants to use a try to map to PropertyBags, and it
needs longest-suffix rather than shortest-prefix matching.
Implement both by making Trie into a template class with two
parameters; the ValueType, and the MatchKind.
Note that while the MatchKind encodes the longest vs shortest
match part, matching on the prefix vs suffix of a term is up
to the caller, since the find() and insert() methods of Trie
take a pair of iterators, so simply passing in begin()/end() vs
rbegin()/rend() selects the direction.
Previously RewriteSystem::simplify() would attempt to apply every
rewrite rule at every position in the original term, which was
obviously a source of overhead.
The trie itself is somewhat unoptimized; for example, with a bit of
effort it could merge a node with its only child, if nodes stored
a range of elements to compare rather than a single element.
Intuitively, the first token of a rewrite rule determines if the rule
applies to a protocol requirement signature 'Self', or a generic
parameter in the top-level generic signature. A rewrite rule can never
take a type starting with the protocol 'Self' to a type starting with a
generic parameter, or vice versa.
Enforce this by defining the notion of a 'domain', which is the set of
protocols to which the first atom in a term applies to. This set can be
empty (if we have a generic parameter atom), or it may contain more than
one element (if we have an associated type atom for a merged associated
type).
Protocol atoms map to the 'Self' parameter; GenericParam and Name
atoms map in the obvious way.
An associated type atom `[P1&P1&...&Pn:A]` has one or more protocols
P0...Pn and an identifier 'A'.
We map it back to a AssociatedTypeDecl as follows:
- For each protocol Pn, look for associated types A in Pn itself,
and all protocols that Pn refines.
- For each candidate associated type An in protocol Qn where
Pn refines Qn, get the associated type anchor An' defined in
protocol Qn', where Qn refines Qn'.
- Out of all the candidiate pairs (Qn', An'), pick the one where
the protocol Qn' is the lowest element according to the linear
order defined by TypeDecl::compare().
The associated type An' is then the canonical associated type
representative of the associated type atom `[P0&...&Pn:A]`.
If you have a same-type requirement like 'Self.Foo == Self' inside a
protocol P, we add a rewrite rule:
[P].Foo => [P]
Simplification turns this into
[P:Foo] => [P]
Previously, the order was backwards so we would end up with
[P] => [P:Foo]
Which would mess up the conformance information in the equivalence class map.
Also move a all headers other than RequirementMachine.h there, since
I don't expect they will be used outside of the rewrite system
implementation itself.
