Fix links.
This commit is contained in:
parent
d79227e453
commit
9d9eb150de
|
|
@ -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
|
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
|
thing want to know whether some trait is implemented for some type
|
||||||
(e.g., is `u32: Debug` true?). Or they may want to
|
(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
|
This section covers queries at a fairly high level of abstraction. The
|
||||||
subsections look a bit more closely at how these ideas are implemented
|
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
|
for an **unambiguous** answer. In particular, when they tell you the
|
||||||
value for a type variable, that means that this is the **only possible
|
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
|
instantiation** that you could use, given the current set of impls and
|
||||||
where-clauses, that would be provable. (Internally within the solver,
|
where-clauses, that would be provable.
|
||||||
though, they can potentially enumerate all possible answers. See
|
|
||||||
[the description of the SLG solver](./slg.html) for details.)
|
|
||||||
|
|
||||||
The response to a trait query in rustc is typically a
|
The response to a trait query in rustc is typically a
|
||||||
`Result<QueryResult<T>, NoSolution>` (where the `T` will vary a bit
|
`Result<QueryResult<T>, 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
|
- As we'll see in the example below, we can get back var values even
|
||||||
for `Ambiguous` cases.
|
for `Ambiguous` cases.
|
||||||
- **Region constraints:** these are relations that must hold between
|
- **Region constraints:** these are relations that must hold between
|
||||||
the lifetimes that you supplied as inputs. We'll ignore these here,
|
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.
|
|
||||||
- **Value:** The query result also comes with a value of type `T`. For
|
- **Value:** The query result also comes with a value of type `T`. For
|
||||||
some specialized queries – like normalizing associated types –
|
some specialized queries – like normalizing associated types –
|
||||||
this is used to carry back an extra result, but it's often just
|
this is used to carry back an extra result, but it's often just
|
||||||
|
|
|
||||||
|
|
@ -41,7 +41,7 @@ In terms of code, these types are defined in
|
||||||
[`librustc_middle/traits/mod.rs`][traits_mod] in rustc, and in
|
[`librustc_middle/traits/mod.rs`][traits_mod] in rustc, and in
|
||||||
[`chalk-ir/src/lib.rs`][chalk_ir] in chalk.
|
[`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
|
[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
|
[chalk_ir]: https://github.com/rust-lang/chalk/blob/master/chalk-ir/src/lib.rs
|
||||||
|
|
||||||
|
|
@ -118,7 +118,7 @@ e.g. `ProjectionEq<T as Iterator>::Item = u8`
|
||||||
|
|
||||||
The given associated type `Projection` is equal to `Type`; this can be proved
|
The given associated type `Projection` is equal to `Type`; this can be proved
|
||||||
with either normalization or using placeholder associated types. See
|
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)
|
#### Normalize(Projection -> Type)
|
||||||
e.g. `ProjectionEq<T as Iterator>::Item -> u8`
|
e.g. `ProjectionEq<T as Iterator>::Item -> u8`
|
||||||
|
|
@ -126,12 +126,12 @@ e.g. `ProjectionEq<T as Iterator>::Item -> u8`
|
||||||
The given associated type `Projection` can be [normalized][n] to `Type`.
|
The given associated type `Projection` can be [normalized][n] to `Type`.
|
||||||
|
|
||||||
As discussed in [the section on associated
|
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(<T as Trait>::Item -> U)`
|
but not vice versa. In general, proving `Normalize(<T as Trait>::Item -> U)`
|
||||||
also requires proving `Implemented(T: Trait)`.
|
also requires proving `Implemented(T: Trait)`.
|
||||||
|
|
||||||
[n]: ./associated-types.html#normalize
|
[n]: https://rust-lang.github.io/chalk/book/clauses/type_equality.html#normalize
|
||||||
[at]: ./associated-types.html
|
[at]: https://rust-lang.github.io/chalk/book/clauses/type_equality.html
|
||||||
|
|
||||||
#### FromEnv(TraitRef)
|
#### FromEnv(TraitRef)
|
||||||
e.g. `FromEnv(Self: Add<i32>)`
|
e.g. `FromEnv(Self: Add<i32>)`
|
||||||
|
|
@ -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,
|
These are used to achieve a similar "enumerate all the cases" pattern,
|
||||||
as described in the section on [implied bounds].
|
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
|
## Incomplete chapter
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -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
|
lot of work describing how to efficiently handle FOHH clauses; see for
|
||||||
example Gopalan Nadathur's excellent
|
example Gopalan Nadathur's excellent
|
||||||
["A Proof Procedure for the Logic of Hereditary Harrop Formulas"][pphhf]
|
["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
|
[bibliography]: https://rust-lang.github.io/chalk/book/bibliography.html
|
||||||
[pphhf]: ./bibliography.html#pphhf
|
[pphhf]: https://rust-lang.github.io/chalk/book/bibliography.html#pphhf
|
||||||
|
|
||||||
It turns out that supporting FOHH is not really all that hard. And
|
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
|
once we are able to do that, we can easily describe the type-checking
|
||||||
|
|
|
||||||
Loading…
Reference in New Issue