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.
Also, introduce the layout requirement implied by a superclass requirement
when lowering requirements, instead of when building the property map.
Right now this is functionally equivalent, but if we ever start to
test properties by checking for joinability of T with T.[p] instead of
looking at the property map entry of T, this new formulation is the
right one.
Start treating the null {Can}GenericSignature as a regular signature
with no requirements and no parameters. This not only makes for a much
safer abstraction, but allows us to simplify a lot of the clients of
GenericSignature that would previously have to check for null before
using the abstraction.
This is just a straight port of the existing code in the GSB, with minimal changes.
It could be made more efficient in the future by trafficking in Terms rather than
Types, avoiding some intermediate conversion and canonicalization steps.
Store the protocol's direct associated types separately from the inherited
associated types, since in a couple of places we only need the direct
associated types.
Also, factor out a new ProtocolGraph::compute() method that does all the
steps in the right order.
We compute the canonical type by first simplifying the type term, and
then checking if it is a concrete type. If there's no concrete type,
we convert the simplified term back to an interface type and return
that; otherwise, we canonicalize any structural sub-components of
the concrete type that contain interface types, and so on.
Due to a quirk of how the existing declaration checker works, we also
need to handle "purely concrete" member types, eg if I have a
signature `<T where T == Foo>`, and we're asked to canonicalize the
type `T.[P:A]` where Foo : A.
This comes up because we can derive the signature `<T where T == Foo>`
from a generic signature like `<T where T : P>`; adding the
concrete requirement 'T == Foo' renders 'T : P' redundant. We then
want to take interface types written against the original signature
and canonicalize them with respect to the derived signature.
The problem is that `T.[P:A]` is not a valid term in the rewrite system
for `<T where T == Foo>`, since we do not have the requirement T : P.
A more principled solution would build a substitution map when
building a derived generic signature that adds new requirements;
interface types would first be substituted before being canonicalized
in the new signature.
For now, we handle this with a two-step process; we split a term up
into a longest valid prefix, which must resolve to a concrete type,
and the remaining suffix, which we use to perform a concrete
substitution using subst().
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.
