Commit Graph

116 Commits

Author SHA1 Message Date
Slava Pestov
92ac06a25b RequirementMachine: Rules store uniqued Terms 2021-08-05 21:42:50 -04:00
Slava Pestov
ed966e7337 RequirementMachine: Add histograms for symbol kinds and term length 2021-08-05 21:42:50 -04:00
Slava Pestov
7adfd86e37 RequirementMachine: Split off Symbol.cpp and Term.cpp from RewriteSystem.cpp 2021-08-05 21:42:49 -04:00
Slava Pestov
1d7eae7bfb RequirementMachine: lexshort => shortlex 2021-07-23 17:21:58 -04:00
Slava Pestov
cfb1595ec5 RequirementMachine: Rename Atom => Symbol 2021-07-23 15:58:50 -04:00
Slava Pestov
4184ebd0a8 RequirementMachine: Split off RewriteContext.{h,cpp} from RewriteSystem.{h,cpp} 2021-07-14 00:16:06 -04:00
Slava Pestov
c32ec95c13 RequirementMachine: Enforce that rewrite rules preserve the term's 'domain'
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).
2021-07-14 00:14:29 -04:00
Slava Pestov
e36b95d620 RequirementMachine: Split up list of associated types in ProtocolGraph
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.
2021-07-14 00:11:37 -04:00
Slava Pestov
00eca7ee97 RequirementMachine: Add reverse iterators over Term and MutableTerm
I thought I needed these for something but turns out that I don't,
but there's no harm in adding them since surely they will come up
eventually.
2021-07-14 00:06:17 -04:00
Slava Pestov
f0d59d5d4d RequirementMachine: Handle equivalence classes that both have a concrete type and protocol requirements
If a type parameter has a protocol conformance and a concrete type,
we want to map associated types of the conformance to their concrete
type witnesses.

This is implemented as a post-processing pass in the completion
procedure that runs after the equivalence class map has been built.

If we have an equivalence class T => { conforms_to: [ P ], concrete: Foo },
then for each associated type A of P, we generate a new rule:

    T.[P:A].[concrete: Foo.A] => T.[P:A]  (if Foo.A is concrete)
    T.[P:A] => T.(Foo.A)                  (if Foo.A is abstract)

If this process introduced any new rules, we check for any new
overlaps by re-running Knuth-Bendix completion; this may in turn
introduce new concrete associated type overlaps, and so on.

The overall completion procedure now alternates between Knuth-Bendix
and rebuilding the equivalence class map; the rewrite system is
complete when neither step is able to introduce any new rules.
2021-07-09 00:04:36 -04:00
Slava Pestov
35daf17dc4 RequirementMachine: Implement RewriteContext::getTypeForTerm()
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]`.
2021-07-09 00:03:39 -04:00
Slava Pestov
c97d32a654 RequirementMachine: getTermForType() produces resolved associated type atoms 2021-07-08 23:31:53 -04:00
Slava Pestov
ac9a285b8b RequirementMachine: Remove bogus pre-sorting pass 2021-06-30 01:34:07 -04:00
Slava Pestov
8107cea766 RequirementMachine: Define operator<< overloads 2021-06-29 13:09:11 -04:00
Slava Pestov
d03ff29a46 RequirementMachine: Protocol atoms order before associated type atoms
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.
2021-06-29 13:09:11 -04:00
Slava Pestov
6c164f682e RequirementMachine: Move files to a new subdirectory under lib/AST/
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.
2021-06-25 00:04:09 -04:00