From a7b1b24fe19eb42506c1bcccb1a95e06da09601a Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Fri, 9 Mar 2018 04:30:48 -0500 Subject: [PATCH] expand reorder topic list slightly --- src/SUMMARY.md | 2 +- src/traits-canonicalization.md | 5 +++-- src/traits.md | 22 ++++++++++++++++------ 3 files changed, 20 insertions(+), 9 deletions(-) diff --git a/src/SUMMARY.md b/src/SUMMARY.md index 1c5bc284..9c1920d3 100644 --- a/src/SUMMARY.md +++ b/src/SUMMARY.md @@ -22,8 +22,8 @@ - [Caching subtleties](./trait-caching.md) - [Specialization](./trait-specialization.md) - [Trait solving (new-style)](./traits.md) - - [Canonicalization](./traits-canonicalization.md) - [Lowering to logic](./traits-lowering-to-logic.md) + - [Canonical queries](./traits-canonicalization.md) - [Goals and clauses](./traits-goals-and-clauses.md) - [Lowering rules](./traits-lowering-rules.md) - [Equality and associated types](./traits-associated-types.md) diff --git a/src/traits-canonicalization.md b/src/traits-canonicalization.md index 8ab73a7f..9b71c847 100644 --- a/src/traits-canonicalization.md +++ b/src/traits-canonicalization.md @@ -24,8 +24,9 @@ they are repeated. We use this to improve caching as well as to detect cycles and other things during trait resolution. Roughly speaking, the idea is that if two trait queries have the same canonicalize form, then they will get -the same answer -- modulo the precise identities of the variables -involved. +the same answer. That answer will be expressed in terms of the +canonical variables (`?0`, `?1`), which we can then map back to the +original variables (`?T`, `?U`). To see how it works, imagine that we are asking to solve the following trait query: `?A: Foo<'static, ?B>`, where `?A` and `?B` are unbound. diff --git a/src/traits.md b/src/traits.md index f0e67ffd..18cb0c64 100644 --- a/src/traits.md +++ b/src/traits.md @@ -13,11 +13,21 @@ instructions for getting involved in the Trait solving is based around a few key ideas: -- [Canonicalization](./traits-canonicalization.html), which allows us to - extract types that contain inference variables in them from their - inference context, work with them, and then bring the results back - into the original context. - [Lowering to logic](./traits-lowering-to-logic.html), which expresses Rust traits in terms of standard logical terms. - -*more to come* + - The [goals and clauses](./traits-goals-and-clauses.html) chapter + describes the precise lowering rules we use. +- [Canonical queries](./traits-canonicalization.html), which allow us + to solve trait problems (like "is `Foo` implemented for the type + `Bar`?") once, and then apply that same result independently in many + different inference contexts. +- [Lazy normalization](./traits-associated-types.html), which is the + technique we use to accommodate associated types when figuring out + whether types are equal. +- [Region constraints](./traits-regions.md), which are accumulated + during trait solving but mostly ignored. This means that trait + solving effectively ignores the precise regions involved, always -- + but we still remember the constraints on them so that those + constraints can be checked by thet type checker. + +Note: this is not a complete list of topics. See the sidebar for more.