Commit Graph

44 Commits

Author SHA1 Message Date
Slava Pestov
fbe3d71b19 RequirementMachine: Small cleanup 2024-09-14 23:33:11 -04:00
Holly Borla
2ea4586580 [Requirement Machine] Implement same-element requirements. 2024-07-15 10:19:32 -07:00
Slava Pestov
273c4b2b1a RequirementMachine: Convert to new assertions 2024-06-22 08:53:22 -04:00
Tim Kientzle
1d961ba22d Add #include "swift/Basic/Assertions.h" to a lot of source files
Although I don't plan to bring over new assertions wholesale
into the current qualification branch, it's entirely possible
that various minor changes in main will use the new assertions;
having this basic support in the release branch will simplify that.
(This is why I'm adding the includes as a separate pass from
rewriting the individual assertions)
2024-06-05 19:37:30 -07:00
Holly Borla
0f13eda26c [RequirementMachine] Add a new symbol kind for the shape of a parameter
pack.
2022-10-06 20:38:30 -07:00
Slava Pestov
5a49a337d9 RequirementMachine: Fix some comments 2022-08-11 14:10:01 -04:00
Slava Pestov
919101d4b3 RequirementMachine: Remove old minimal conformances algorithm 2022-07-06 11:57:21 -04:00
Slava Pestov
506cc356c1 RequirementMachine: New minimal conformances algorithm 2022-07-05 21:40:27 -04:00
Slava Pestov
93b94f9211 RequirementMachine: Relax an invariant in decomposeTermIntoConformanceRuleLeftHandSides() 2022-07-05 21:40:06 -04:00
Slava Pestov
e3488cecb2 RequirementMachine: Move decomposeTermIntoConformanceRuleLeftHandSides() to RewriteSystem 2022-07-05 21:40:06 -04:00
Slava Pestov
ea980d6fbd RequirementMachine: Dump rewrite system when minimal conformances detects an invariant violation 2022-06-08 00:34:55 -04:00
Josh Soref
81d3ad76ac Spelling ast (#42463)
* spelling: accessor

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: accommodates

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: argument

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: associated

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: availability

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: available

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: belongs

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: bookkeeping

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: building

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: clazz

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: clonable

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: closure

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: concatenated

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: conformance

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: context

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: conversion

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: correspondence

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: declarations

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: declared

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: defining

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: delayed

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: dependency

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: deployed

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: descendants

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: diagnose

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: diagnostic

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: equitable

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: evaluation

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: exclusivity

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: existence

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: existential

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: explicit

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: expressed

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: for

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: foreign

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: function

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: identifier

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: implicit

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: indices

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: information

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: instance

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: interchangeable

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: interface

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: introduced

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: invalid

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: kind-in

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: least

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: library

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: location

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: namespace

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: necessary

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: nonexistent

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: not

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: number

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: obtains

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: occurs

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: opaque

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: overridden

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: parameter

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: precede

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: preceding

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: property

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: protocol

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: qualified

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: recognized

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: recursively

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: references

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: relaxing

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: represented

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: request

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: requirement

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: requirements

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: retrieve

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: returned

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: satisfied

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: satisfy

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: scanner

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: siblings

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: simplified

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: something

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: source

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: specializations

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: specially

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: statement

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: stripped

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: structure

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: substitution

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: the

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: transform

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: transformed

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: transitively

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: transparent

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: typecheck

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: unknown

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: unlabeled

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: unqualified

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: whether

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: with

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

* spelling: scanner

Signed-off-by: Josh Soref <jsoref@users.noreply.github.com>

Co-authored-by: Josh Soref <jsoref@users.noreply.github.com>
2022-04-21 12:57:16 -07:00
Slava Pestov
30da30e0ee RequirementMachine: Rule::isProtocolRefinementRule() allows transitive refinement
Without this, we only considered a protocol refinement rule redundant if
it was derived by directly-stated protocol refinements. But this broke
when completion introduced a 'transitive' refinement [P].[R] => [P]
from two directly-stated refinements [P].[Q] => [P] and [Q].[R] => [Q].

Fixes rdar://problem/90402503.
2022-03-17 15:06:05 -04:00
Slava Pestov
c5cef953bc RequirementMachine: Minimal conformances collects protocol refinement rules from all minimization domains 2022-03-17 15:06:05 -04:00
Slava Pestov
54c83ead9e RequirementMachine: Make some low-cost assertions unconditional 2022-03-11 17:28:01 -05:00
Slava Pestov
517fb4568e RequirementMachine: Fix minimal conformances algorithm to cope with unordered concrete conformances 2022-03-03 14:05:02 -05:00
Slava Pestov
b497c790fa RequirementMachine: Check invariants in noassert builds 2022-03-03 14:05:02 -05:00
Slava Pestov
5281426569 RequirementMachine: Fix minimization when protocol is constrained to a class that conforms to the protocol
Consider this example:

    protocol P : C {}
    class C : P {}

    <T where T : P>

The GenericSignatureBuilder thinks the minimized signature is
<T where T : P>. The RequirementMachine would minimize it down to
<T where T : C>. The latter is more correct, since the conformance
here is concrete and no witness table needs to be passed in at
runtime, however for strict binary compatibility we need to produce
the same signature as the GenericSignatureBuilder.

Accomplish this by changing the minimal conformances algorithm to
detect "circular concrete conformance rules", which take the form

    [P].[concrete: C : Q]

Where Q : P. These rules are given special handling. Ordinarily a
protocol conformance rule is eliminated before a concrete conformance
rule; however concrete conformances derived from circular
conformances are considered to be redundant from the get-go,
preventing protocol conformances that can be written in terms of
such concrete conformances from themselves becoming redundant.

Fixes rdar://problem/89633532.
2022-03-02 03:13:41 -05:00
Slava Pestov
048a64d4c0 RequirementMachine: Tweak debug output and fix typo 2022-02-28 18:41:42 -05:00
Slava Pestov
fa65fd0e05 RequirementMachine: Plumb protocol typealiases through minimization
Now that we can detect protocol typealias rules, collect and keep
track of them so that they can be recorded in protocol requirement
signatures.

For now, this is all NFC since nothing introduces such rules into
the rewrite system, except for invalid requirements which are
diagnosed anyway.
2022-02-13 00:24:23 -05:00
Slava Pestov
0f3ec0f2f0 RequirementMachine: Simpler handling of concrete conformances in minimal conformances algorithm
This logic was tricky and unsound.

Correct handling of concrete conformances requires rebuilding the
signature after dropping protocol conformance requiremnts made
redundant by concrete type requirements.

The old support for "derived-via-concrete" requirements in the
minimal conformances algorithm was causing other problems, and it
is the wrong approach anyway, so just remove it.
2022-02-09 01:05:12 -05:00
Slava Pestov
0d0bcb2ff1 RequirementMachine: Simplify the Symbol API for removal of merged associated types 2022-02-07 18:57:45 -05:00
Slava Pestov
2c355de71b RequirementMachine: Introduce RewriteStep::{Left,Right}ConcreteProjection 2022-02-07 08:20:59 -05:00
Slava Pestov
037dc98845 RequirementMachine: Generalize compare() methods to return None instead of asserting on incomparable symbols 2022-02-07 08:20:59 -05:00
Slava Pestov
7e4a5876d1 RequirementMachine: Introduce RewriteStep::DecomposeConcrete 2022-02-07 08:20:58 -05:00
Slava Pestov
d8aa79c5e5 RequirementMachine: Rename RewriteStep::AdjustConcreteType to ::PrefixSubstitutions 2022-02-07 08:20:58 -05:00
Slava Pestov
8df7ca01fd RequirementMachine: Remove useless assertion from MinimalConformances::collectConformanceRules()
We rule out RHS-simplified rules immediately above.
2022-02-04 22:47:19 -05:00
Slava Pestov
8e94fff3d4 RequirementMachine: Fix up concrete conformance handling in minimal conformances algorithm 2022-01-27 18:54:03 -05:00
Slava Pestov
04f9bce79a RequirementMachine: Treat LHS-simplified and RHS-simplified/substitution-simplified rules separately in minimization 2022-01-27 18:54:03 -05:00
Slava Pestov
106896228e RequirementMachine: Split up Rule::isSimplified() into three predicates
We have three simplification passes, give each one its own predicate:
- Left hand side simplification
- Right hand side simplification
- Substitution simplification

This is for debugging output and will also allow me to tighten up
some invariants.
2022-01-27 18:54:03 -05:00
Slava Pestov
ad9c701152 RequirementMachine: Don't record useless minimal conformance equations 2022-01-27 18:54:03 -05:00
Slava Pestov
75dfc8b3a8 RequirementMachine: Minimal conformances algorithm ignores conformance rules not in our minimization domain 2022-01-27 18:54:03 -05:00
Slava Pestov
bdbf50e1e3 RequirementMachine: Replace RewriteStep::SameTypeWitness with a relation 2022-01-13 19:14:52 -05:00
Slava Pestov
6064671abd RequirementMachine: Replace RewriteStep::ConcreteTypeWitness with relations 2022-01-13 18:01:15 -05:00
Slava Pestov
84e2a627ec RequirementMachine: Replace RewriteStep::AbstractTypeWitness with relations 2022-01-13 00:02:31 -05:00
Slava Pestov
abb85fb3ca RequirementMachine: Replace RewriteStep::{Superclass,Concrete}Conformance with relations 2022-01-13 00:02:31 -05:00
Slava Pestov
3d2492fe56 RequirementMachine: Rename RewriteStep::ApplyRewriteRule to RewriteStep::Rule 2022-01-13 00:02:31 -05:00
Slava Pestov
66cf913d68 RequirementMachine: Minimization understands 'relations' among layout requirements
A superclass requirement 'T : C' implies a layout requirement
'T : AnyObject' (if the class is @objc) or 'T : _NativeObject'
(if the class is not @objc).

In the latter case, there might already be a 'T : AnyObject'
requirement, in which case the type parameter 'T' is subject
to two layout requirements:

    T : AnyObject
    T : _NativeObject

The second requirement implies the first however. To encode this
in the world of rewrite loops, we the notion of a 'relation'
between property symbols, and a 'Relation' rewrite step.

Here, the relation is that _NativeObject < AnyObject. Once this
relation is recorded, the Relation rewrite step will transform

    T.[layout: _NativeObject].[layout: AnyObject]

into

    T.[layout: _NativeObject]

and vice versa.

This rewrite step allows us to construct a rewrite loop which
makes the first rewrite rule redundant via the second.
2022-01-04 22:35:58 -05:00
Slava Pestov
7148aea7ed RequirementMachine: Rename RewriteStep::RuleID to RewriteStep::Arg
It's used to store more than just the rule ID. However, add a
getRuleID() method that also asserts that Kind is ApplyRewriteRule
for readability.
2022-01-04 22:35:58 -05:00
Slava Pestov
f4ff260ee7 RequirementMachine: Subtle fix for minimal conformances algorithm
We don't need to be able to recover the parent type of a conformance
rule if the rule itself is redundant.
2021-12-20 17:59:31 -05:00
Slava Pestov
8a222b50fd RequirementMachine: Better debug output from minimal conformances algorithm 2021-12-20 17:59:31 -05:00
Slava Pestov
3c9344cc80 RequirementMachine: Improved verifyMinimizedRules() 2021-12-17 10:04:52 -05:00
Slava Pestov
2bca132380 RequirementMachine: Introduce RewriteStep::AbstractTypeWitness 2021-12-17 10:04:52 -05:00
Slava Pestov
317743a487 RequirementMachine: Rename GeneratingConformances => MinimalConformances 2021-12-17 10:04:52 -05:00