diff --git a/src/traits/canonical-queries.md b/src/traits/canonical-queries.md index e15bdaae..5ba450d4 100644 --- a/src/traits/canonical-queries.md +++ b/src/traits/canonical-queries.md @@ -7,7 +7,7 @@ would like to know the answer to – and in the checker or other parts of the system, may in the course of doing their thing want to know whether some trait is implemented for some type (e.g., is `u32: Debug` true?). Or they may want to -[normalize some associated type](./associated-types.html). +normalize some associated type. This section covers queries at a fairly high level of abstraction. The subsections look a bit more closely at how these ideas are implemented @@ -104,9 +104,7 @@ trying to enumerate **all possible** answers for you, they are looking for an **unambiguous** answer. In particular, when they tell you the value for a type variable, that means that this is the **only possible instantiation** that you could use, given the current set of impls and -where-clauses, that would be provable. (Internally within the solver, -though, they can potentially enumerate all possible answers. See -[the description of the SLG solver](./slg.html) for details.) +where-clauses, that would be provable. The response to a trait query in rustc is typically a `Result, NoSolution>` (where the `T` will vary a bit @@ -130,10 +128,7 @@ we did find. It consists of four parts: - As we'll see in the example below, we can get back var values even for `Ambiguous` cases. - **Region constraints:** these are relations that must hold between - the lifetimes that you supplied as inputs. We'll ignore these here, - but see the - [section on handling regions in traits](./regions.html) for - more details. + the lifetimes that you supplied as inputs. We'll ignore these here. - **Value:** The query result also comes with a value of type `T`. For some specialized queries – like normalizing associated types – this is used to carry back an extra result, but it's often just diff --git a/src/traits/goals-and-clauses.md b/src/traits/goals-and-clauses.md index ecd2ce14..f4ceb99a 100644 --- a/src/traits/goals-and-clauses.md +++ b/src/traits/goals-and-clauses.md @@ -41,7 +41,7 @@ In terms of code, these types are defined in [`librustc_middle/traits/mod.rs`][traits_mod] in rustc, and in [`chalk-ir/src/lib.rs`][chalk_ir] in chalk. -[pphhf]: ./bibliography.html#pphhf +[pphhf]: https://rust-lang.github.io/chalk/book/bibliography.html#pphhf [traits_mod]: https://github.com/rust-lang/rust/blob/master/src/librustc_middle/traits/mod.rs [chalk_ir]: https://github.com/rust-lang/chalk/blob/master/chalk-ir/src/lib.rs @@ -118,7 +118,7 @@ e.g. `ProjectionEq::Item = u8` The given associated type `Projection` is equal to `Type`; this can be proved with either normalization or using placeholder associated types. See -[the section on associated types](./associated-types.html). +[the section on associated types in Chalk Book][at]. #### Normalize(Projection -> Type) e.g. `ProjectionEq::Item -> u8` @@ -126,12 +126,12 @@ e.g. `ProjectionEq::Item -> u8` The given associated type `Projection` can be [normalized][n] to `Type`. As discussed in [the section on associated -types](./associated-types.html), `Normalize` implies `ProjectionEq`, +types in Chalk Book][at], `Normalize` implies `ProjectionEq`, but not vice versa. In general, proving `Normalize(::Item -> U)` also requires proving `Implemented(T: Trait)`. -[n]: ./associated-types.html#normalize -[at]: ./associated-types.html +[n]: https://rust-lang.github.io/chalk/book/clauses/type_equality.html#normalize +[at]: https://rust-lang.github.io/chalk/book/clauses/type_equality.html #### FromEnv(TraitRef) e.g. `FromEnv(Self: Add)` @@ -260,7 +260,7 @@ In addition to auto traits, `WellFormed` predicates are co-inductive. These are used to achieve a similar "enumerate all the cases" pattern, as described in the section on [implied bounds]. -[implied bounds]: ./lowering-rules.html#implied-bounds +[implied bounds]: https://rust-lang.github.io/chalk/book/clauses/implied_bounds.html#implied-bounds ## Incomplete chapter diff --git a/src/traits/lowering-to-logic.md b/src/traits/lowering-to-logic.md index e1a6c136..cc8b3bf8 100644 --- a/src/traits/lowering-to-logic.md +++ b/src/traits/lowering-to-logic.md @@ -168,10 +168,10 @@ the body". But it's nice to know the proper name, because there is a lot of work describing how to efficiently handle FOHH clauses; see for example Gopalan Nadathur's excellent ["A Proof Procedure for the Logic of Hereditary Harrop Formulas"][pphhf] -in [the bibliography]. +in [the bibliography of Chalk Book][bibliography]. -[the bibliography]: ./bibliography.html -[pphhf]: ./bibliography.html#pphhf +[bibliography]: https://rust-lang.github.io/chalk/book/bibliography.html +[pphhf]: https://rust-lang.github.io/chalk/book/bibliography.html#pphhf It turns out that supporting FOHH is not really all that hard. And once we are able to do that, we can easily describe the type-checking