-
Notifications
You must be signed in to change notification settings - Fork 10.2k
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
[Constraint solver] Introduce one-way constraints.
Introduce the notion of "one-way" binding constraints of the form $T0 one-way bind to $T1 which treats the type variables $T0 and $T1 as independent up until the point where $T1 simplifies down to a concrete type, at which point $T0 will be bound to that concrete type. $T0 won't be bound in any other way, so type information ends up being propagated right-to-left, only. This allows a constraint system to be broken up in more components that are solved independently. Specifically, the connected components algorithm now proceeds as follows: 1. Compute connected components, excluding one-way constraints from consideration. 2. Compute a directed graph amongst the components using only the one-way constraints, where an edge A -> B indicates that the type variables in component A need to be solved before those in component B. 3. Using the directed graph, compute the set of components that need to be solved before a given component. To utilize this, implement a new kind of solver step that handles the propagation of partial solutions across one-way constraints. This introduces a new kind of "split" within a connected component, where we collect each combination of partial solutions for the input components and (separately) try to solve the constraints in this component. Any correct solution from any of these attempts will then be recorded as a (partial) solution for this component. For example, consider: let _: Int8 = b ? Builtin.one_way(int8Or16(17)) : Builtin.one_way(int8Or16(42\ )) where int8Or16 is overloaded with types `(Int8) -> Int8` and `(Int16) -> Int16`. There are two one-way components (`int8Or16(17)`) and (`int8Or16(42)`), each of which can produce a value of type `Int8` or `Int16`. Those two components will be solved independently, and the partial solutions for each will be fed into the component that evaluates the ternary operator. There are four ways to attempt that evaluation: ``` [Int8, Int8] [Int8, Int16] [Int16, Int8] [Int16, Int16] To test this, introduce a new expression builtin `Builtin.one_way(x)` that introduces a one-way expression constraint binding the result of the expression 'x'. The builtin is meant to be used for testing purposes, and the one-way constraint expression itself can be synthesized by the type checker to introduce one-way constraints later on. Of these two, there are only two (partial) solutions that can work at all, because the types in the ternary operator need a common supertype: [Int8, Int8] [Int16, Int16] Therefore, these are the partial solutions that will be considered the results of the component containing the ternary expression. Note that only one of them meets the final constraint (convertibility to `Int8`), so the expression is well-formed. Part of rdar://problem/50150793.
- Loading branch information
1 parent
c88407f
commit 3c69f6a
Showing
19 changed files
with
810 additions
and
81 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.