Commit Graph

55 Commits

Author SHA1 Message Date
Slava Pestov
399a600e32 RequirementMachine: Add -debug-requirement-machine= flag to control debug output 2021-08-20 01:29:22 -04:00
Slava Pestov
9738d4eef6 RequirementMachine: PropertyMap can use Terms instead of MutableTerms as keys
Also, we don't have to sort rules in term order before adding them to
the map; a bucket sort by term length is sufficient.
2021-08-06 14:17:20 -04:00
Slava Pestov
47fc3d87ad RequirementMachine: Speed up PropertyMap lookups with a suffix trie
Whereas term simplification uses a prefix trie with shortest matching,
the PropertyMap uses a suffix trie with longest matching.
2021-08-06 14:17:20 -04:00
Slava Pestov
9a8ee6017a RequirementMachine: Fix silly oversight when resolving concrete types and superclass bounds
The property map stores the concrete type or superclass bound for all
terms whose suffix is equal to some key, so eg if you have

  protocol P {
    associatedtype T where T == U?
    associatedtype U
  }

Then you have this rewrite system

  [P].T => [P:T]
  [P].U => [P:U]
  [P:T].[concrete: Optional<τ_0_0> with <[P:U]>] => [P:T]

Which creates this property map

  [P:T] => { [concrete: Optional<τ_0_0> with <[P:U]>] }

Now if I start with a generic signature like

  <T, U where U : P>

This produces the following rewrite system:

  τ_0_1.[U] => τ_0_1
  τ_0_1.T => τ_0_1.[P:T]
  τ_0_1.U => τ_0_1.[P:U]

Consider the computation of the canonical type of τ_0_1.T. This term
reduces to τ_0_1.[P:T]. The suffix [P:T] has a concrete type symbol in
the property map, [concrete: Optional<τ_0_0> with <[P:U]>].

However it would not be correct to canonicalize τ_0_1.[P:T] to
Optional<τ_0_0>.subst { τ_0_0 => getTypeForTerm([P:T]) }; this
produces the type Optional<τ_0_0.T>, and not Optional<τ_0_1.T> as
expected.

The reason is that the substitution τ_0_0 => getTypeForTerm([P:T])
is "relative" to the protocol Self type of P, since domain([P:T]) = {P}.

Indeed, the right solution here is to note that τ_0_1.[P:T] has a suffix
equal to the key of the property map entry, [P:T]. If we strip off the
suffix, we get τ_0_1. If we then prepend τ_0_1 to the substitution term,
we get the term τ_0_1.[P:U], whose canonical type is τ_0_1.U.

Now, applying the substitution τ_0_0 => τ_0_1.U to Optional<τ_0_0>
produces the desired result, Optional<τ_0_1.U>.

Note that this is the same "prepend a prefix to each substitution of
a concrete type symbol" operation that is performed in checkForOverlap()
and PropertyBag::copyPropertiesFrom(), however we can simplify things
slightly by open-coding it instead of calling the utility method
prependPrefixToConcreteSubstitutions(), since the latter creates a
new symbol, which we don't actually need.
2021-08-04 01:21:21 -04:00
Slava Pestov
d3db1b6753 RequirementMachine: EquivalenceClassMap => PropertyMap
EquivalenceClass is now PropertyBag.
2021-07-23 17:21:57 -04:00