A superclass requirement implies a layout requirement. We don't
want the layout requirement to be present in the minimal
signature, so instead of adding a pair of requirements:
T.[superclass: C<X, Y>] => T
T.[layout: _NativeClass] => T
Add this pair of requirements:
T.[superclass: C<X, Y>] => T
[superclass: C<X, Y>].[layout: _NativeClass] => [superclass: C<X, Y>] [permanent]
Completion then derives the rule as a consequence:
T.[layout: _NativeClass] => T
Since this rule is a consequence of the other two rules, homotopy
reduction will mark it redundant.
Now that the property map stores a reference to the RewriteSystem,
defining the buildPropertyMap() method on PropertyMap feels cleaner,
and allows more of the property map's internals to be private.
Completion adds this rule when a same-type requirement equates the Self of P
with some other type parameter conforming to P; one example is something like this:
protocol P {
associatedtype T : P where T.T == Self
}
The initial rewrite system looks like this:
(1) [P].T => [P:T]
(2) [P:T].[P] => [P:T]
(3) [P:T].[P:T] => [P]
Rules (2) and (3) overlap on the term
[P:T].[P:T].[P]
Simplifying the overlapped term with rule (2) produces
[P:T].[P:T]
Which further reduces to
[P]
Simplifying the overlapped term with rule (3) produces
[P].[P]
So we get a new rule
[P].[P] => [P]
This is not a "real" conformance rule, and homotopy reduction wastes work
unraveling it in rewrite loops where this rule occurs. Instead, it's better
to introduce it as a permanent rule that is not subject to homotopy reduction
for every protocol.
Also while plumbing this through, don't record homotopy generators
unless we're minimizing a protocol signature, since they're not
used for anything else yet.
When using the requirement machine to build protocol signatures,
we can't get the protocol's dependencies by looking at the
conformance requirements in it's requirement signature, because
we haven't computed the requirement signature yet.
Instead, get the dependencies via the recently-added
getStructuralRequirements() request.
- 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)
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.
