We want a term with more name symbols to order after a term with
fewer name symbols, even if the term with more name symbols is
shorter. That is,
[P].A > [P:X].[Q:Y].[R:Z]
This is in support of handling protocol typealiases.
I'm about to change the reduction order so that terms with more
name symbols always order after terms with fewer name symbols,
so for example
[P].A > [P:T].[Q:U].[R:V]
This will be used to implement protocol typealiases.
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.
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.
