first round of link fixes
This commit is contained in:
parent
1ad9dc34e5
commit
30b6be0f7d
|
|
@ -22,34 +22,34 @@
|
|||
- [The HIR (High-level IR)](./hir.md)
|
||||
- [The `ty` module: representing types](./ty.md)
|
||||
- [Type inference](./type-inference.md)
|
||||
- [Trait solving (old-style)](./trait-resolution.md)
|
||||
- [Higher-ranked trait bounds](./trait-hrtb.md)
|
||||
- [Caching subtleties](./trait-caching.md)
|
||||
- [Specialization](./trait-specialization.md)
|
||||
- [Trait solving (old-style)](./traits/resolution.md)
|
||||
- [Higher-ranked trait bounds](./traits/hrtb.md)
|
||||
- [Caching subtleties](./traits/caching.md)
|
||||
- [Specialization](./traits/specialization.md)
|
||||
- [Trait solving (new-style)](./traits.md)
|
||||
- [Lowering to logic](./traits-lowering-to-logic.md)
|
||||
- [Goals and clauses](./traits-goals-and-clauses.md)
|
||||
- [Equality and associated types](./traits-associated-types.md)
|
||||
- [Implied bounds](./traits-implied-bounds.md)
|
||||
- [Region constraints](./traits-regions.md)
|
||||
- [Canonical queries](./traits-canonical-queries.md)
|
||||
- [Canonicalization](./traits-canonicalization.md)
|
||||
- [Lowering rules](./traits-lowering-rules.md)
|
||||
- [The lowering module in rustc](./traits-lowering-module.md)
|
||||
- [Well-formedness checking](./traits-wf.md)
|
||||
- [The SLG solver](./traits-slg.md)
|
||||
- [Lowering to logic](./traits/lowering-to-logic.md)
|
||||
- [Goals and clauses](./traits/goals-and-clauses.md)
|
||||
- [Equality and associated types](./traits/associated-types.md)
|
||||
- [Implied bounds](./traits/implied-bounds.md)
|
||||
- [Region constraints](./traits/regions.md)
|
||||
- [Canonical queries](./traits/canonical-queries.md)
|
||||
- [Canonicalization](./traits/canonicalization.md)
|
||||
- [Lowering rules](./traits/lowering-rules.md)
|
||||
- [The lowering module in rustc](./traits/lowering-module.md)
|
||||
- [Well-formedness checking](./traits/wf.md)
|
||||
- [The SLG solver](./traits/slg.md)
|
||||
- [An Overview of Chalk](./chalk-overview.md)
|
||||
- [Bibliography](./traits-bibliography.md)
|
||||
- [Bibliography](./traits/bibliography.md)
|
||||
- [Type checking](./type-checking.md)
|
||||
- [Method Lookup](./method-lookup.md)
|
||||
- [Variance](./variance.md)
|
||||
- [The MIR (Mid-level IR)](./mir.md)
|
||||
- [MIR construction](./mir-construction.md)
|
||||
- [MIR visitor and traversal](./mir-visitor.md)
|
||||
- [MIR passes: getting the MIR for a function](./mir-passes.md)
|
||||
- [MIR borrowck](./mir-borrowck.md)
|
||||
- [MIR-based region checking (NLL)](./mir-regionck.md)
|
||||
- [MIR optimizations](./mir-optimizations.md)
|
||||
- [MIR construction](./mir/construction.md)
|
||||
- [MIR visitor and traversal](./mir/visitor.md)
|
||||
- [MIR passes: getting the MIR for a function](./mir/passes.md)
|
||||
- [MIR borrowck](./mir/borrowck.md)
|
||||
- [MIR-based region checking (NLL)](./mir/regionck.md)
|
||||
- [MIR optimizations](./mir/optimizations.md)
|
||||
- [Constant evaluation](./const-eval.md)
|
||||
- [miri const evaluator](./miri.md)
|
||||
- [Parameter Environments](./param_env.md)
|
||||
|
|
@ -58,7 +58,7 @@
|
|||
|
||||
---
|
||||
|
||||
- [Appendix A: Stupid Stats](./appendix-stupid-stats.md)
|
||||
- [Appendix B: Background material](./appendix-background.md)
|
||||
- [Appendix C: Glossary](./appendix-glossary.md)
|
||||
- [Appendix D: Code Index](./appendix-code-index.md)
|
||||
- [Appendix A: Stupid Stats](./appendix/stupid-stats.md)
|
||||
- [Appendix B: Background material](./appendix/background.md)
|
||||
- [Appendix C: Glossary](./appendix/glossary.md)
|
||||
- [Appendix D: Code Index](./appendix/code-index.md)
|
||||
|
|
|
|||
|
|
@ -73,4 +73,4 @@ thread-locals, although you should rarely need to touch it.
|
|||
[`TyCtxt`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc/ty/struct.TyCtxt.html
|
||||
[`CodeMap`]: https://doc.rust-lang.org/nightly/nightly-rustc/syntax/codemap/struct.CodeMap.html
|
||||
[stupid-stats]: https://github.com/nrc/stupid-stats
|
||||
[Appendix A]: appendix-stupid-stats.html
|
||||
[Appendix A]: appendix/stupid-stats.html
|
||||
|
|
|
|||
|
|
@ -24,7 +24,7 @@ On the other hand, if there is no hit, we need to go through the [selection
|
|||
process] from scratch. Suppose, we come to the conclusion that the only
|
||||
possible impl is this one, with def-id 22:
|
||||
|
||||
[selection process]: ./trait-resolution.html#selection
|
||||
[selection process]: ./traits/resolution.html#selection
|
||||
|
||||
```rust,ignore
|
||||
impl Foo<isize> for usize { ... } // Impl #22
|
||||
|
|
@ -34,7 +34,7 @@ We would then record in the cache `usize : Foo<$0> => ImplCandidate(22)`. Next
|
|||
we would [confirm] `ImplCandidate(22)`, which would (as a side-effect) unify
|
||||
`$t` with `isize`.
|
||||
|
||||
[confirm]: ./trait-resolution.html#confirmation
|
||||
[confirm]: ./traits/resolution.html#confirmation
|
||||
|
||||
Now, at some later time, we might come along and see a `usize :
|
||||
Foo<$u>`. When skolemized, this would yield `usize : Foo<$0>`, just as
|
||||
|
|
|
|||
|
|
@ -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](./traits-associated-types.html).
|
||||
[normalize some associated type](./traits/associated-types.html).
|
||||
|
||||
This section covers queries at a fairly high level of abstraction. The
|
||||
subsections look a bit more closely at how these ideas are implemented
|
||||
|
|
@ -106,7 +106,7 @@ 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](./traits-slg.html) for details.)
|
||||
[the description of the SLG solver](./traits/slg.html) for details.)
|
||||
|
||||
The response to a trait query in rustc is typically a
|
||||
`Result<QueryResult<T>, NoSolution>` (where the `T` will vary a bit
|
||||
|
|
@ -132,7 +132,7 @@ we did find. It consists of four parts:
|
|||
- **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](./traits-regions.html) for
|
||||
[section on handling regions in traits](./traits/regions.html) for
|
||||
more details.
|
||||
- **Value:** The query result also comes with a value of type `T`. For
|
||||
some specialized queries -- like normalizing associated types --
|
||||
|
|
|
|||
|
|
@ -16,7 +16,7 @@ starting from zero and numbered in a fixed order (left to right, for
|
|||
the most part, but really it doesn't matter as long as it is
|
||||
consistent).
|
||||
|
||||
[cq]: ./traits-canonical-queries.html
|
||||
[cq]: ./traits/canonical-queries.html
|
||||
|
||||
So, for example, if we have the type `X = (?T, ?U)`, where `?T` and
|
||||
`?U` are distinct, unbound inference variables, then the canonical
|
||||
|
|
@ -98,12 +98,12 @@ Remember that substitution S though! We're going to need it later.
|
|||
|
||||
OK, now that we have a fresh inference context and an instantiated
|
||||
query, we can go ahead and try to solve it. The trait solver itself is
|
||||
explained in more detail in [another section](./traits-slg.html), but
|
||||
explained in more detail in [another section](./traits/slg.html), but
|
||||
suffice to say that it will compute a [certainty value][cqqr] (`Proven` or
|
||||
`Ambiguous`) and have side-effects on the inference variables we've
|
||||
created. For example, if there were only one impl of `Foo`, like so:
|
||||
|
||||
[cqqr]: ./traits-canonical-queries.html#query-response
|
||||
[cqqr]: ./traits/canonical-queries.html#query-response
|
||||
|
||||
```rust,ignore
|
||||
impl<'a, X> Foo<'a, X> for Vec<X>
|
||||
|
|
|
|||
|
|
@ -2,7 +2,7 @@
|
|||
|
||||
In logic programming terms, a **goal** is something that you must
|
||||
prove and a **clause** is something that you know is true. As
|
||||
described in the [lowering to logic](./traits-lowering-to-logic.html)
|
||||
described in the [lowering to logic](./traits/lowering-to-logic.html)
|
||||
chapter, Rust's trait solver is based on an extension of hereditary
|
||||
harrop (HH) clauses, which extend traditional Prolog Horn clauses with
|
||||
a few new superpowers.
|
||||
|
|
@ -37,7 +37,7 @@ paper
|
|||
["A Proof Procedure for the Logic of Hereditary Harrop Formulas"][pphhf]
|
||||
gives the details.
|
||||
|
||||
[pphhf]: ./traits-bibliography.html#pphhf
|
||||
[pphhf]: ./traits/bibliography.html#pphhf
|
||||
|
||||
<a name="domain-goals"></a>
|
||||
|
||||
|
|
@ -94,7 +94,7 @@ e.g. `ProjectionEq<T as Iterator>::Item = u8`
|
|||
|
||||
The given associated type `Projection` is equal to `Type`; this can be proved
|
||||
with either normalization or using skolemized types. See [the section
|
||||
on associated types](./traits-associated-types.html).
|
||||
on associated types](./traits/associated-types.html).
|
||||
|
||||
#### Normalize(Projection -> Type)
|
||||
e.g. `ProjectionEq<T as Iterator>::Item -> u8`
|
||||
|
|
@ -102,11 +102,12 @@ e.g. `ProjectionEq<T as Iterator>::Item -> u8`
|
|||
The given associated type `Projection` can be [normalized][n] to `Type`.
|
||||
|
||||
As discussed in [the section on associated
|
||||
types](./traits-associated-types.html), `Normalize` implies `ProjectionEq`,
|
||||
types](./traits/associated-types.html), `Normalize` implies `ProjectionEq`,
|
||||
but not vice versa. In general, proving `Normalize(<T as Trait>::Item -> U)`
|
||||
also requires proving `Implemented(T: Trait)`.
|
||||
|
||||
[n]: ./traits-associated-types.html#normalize
|
||||
[n]: ./traits/associated-types.html#normalize
|
||||
[at]: ./traits/associated-types.html
|
||||
|
||||
#### FromEnv(TraitRef), FromEnv(Projection = Type)
|
||||
e.g. `FromEnv(Self: Add<i32>)`
|
||||
|
|
@ -211,7 +212,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]: ./traits-lowering-rules.html#implied-bounds
|
||||
[implied bounds]: ./traits/lowering-rules.html#implied-bounds
|
||||
|
||||
## Incomplete chapter
|
||||
|
||||
|
|
|
|||
|
|
@ -13,20 +13,20 @@ instructions for getting involved in the
|
|||
|
||||
Trait solving is based around a few key ideas:
|
||||
|
||||
- [Lowering to logic](./traits-lowering-to-logic.html), which expresses
|
||||
- [Lowering to logic](./traits/lowering-to-logic.html), which expresses
|
||||
Rust traits in terms of standard logical terms.
|
||||
- The [goals and clauses](./traits-goals-and-clauses.html) chapter
|
||||
- The [goals and clauses](./traits/goals-and-clauses.html) chapter
|
||||
describes the precise form of rules we use, and
|
||||
[lowering rules](./traits-lowering-rules.html) gives the complete set of
|
||||
[lowering rules](./traits/lowering-rules.html) gives the complete set of
|
||||
lowering rules in a more reference-like form.
|
||||
- [Canonical queries](./traits-canonical-queries.html), which allow us
|
||||
- [Canonical queries](./traits/canonical-queries.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
|
||||
- [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.html), which are accumulated
|
||||
- [Region constraints](./traits/regions.html), 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
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
# The lowering module in rustc
|
||||
|
||||
The program clauses described in the
|
||||
[lowering rules](./traits-lowering-rules.html) section are actually
|
||||
[lowering rules](./traits/lowering-rules.html) section are actually
|
||||
created in the [`rustc_traits::lowering`][lowering] module.
|
||||
|
||||
[lowering]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_traits/lowering/
|
||||
|
|
|
|||
|
|
@ -4,8 +4,8 @@ This section gives the complete lowering rules for Rust traits into
|
|||
[program clauses][pc]. It is a kind of reference. These rules
|
||||
reference the [domain goals][dg] defined in an earlier section.
|
||||
|
||||
[pc]: ./traits-goals-and-clauses.html
|
||||
[dg]: ./traits-goals-and-clauses.html#domain-goals
|
||||
[pc]: ./traits/goals-and-clauses.html
|
||||
[dg]: ./traits/goals-and-clauses.html#domain-goals
|
||||
|
||||
## Notation
|
||||
|
||||
|
|
@ -16,7 +16,7 @@ The nonterminal `Ai` is used to mean some generic *argument*, which
|
|||
might be a lifetime like `'a` or a type like `Vec<A>`.
|
||||
|
||||
When defining the lowering rules, we will give goals and clauses in
|
||||
the [notation given in this section](./traits-goals-and-clauses.html).
|
||||
the [notation given in this section](./traits/goals-and-clauses.html).
|
||||
We sometimes insert "macros" like `LowerWhereClause!` into these
|
||||
definitions; these macros reference other sections within this chapter.
|
||||
|
||||
|
|
@ -141,7 +141,7 @@ This `WellFormed` rule states that `T: Trait` is well-formed if (a)
|
|||
`T: Trait` is implemented and (b) all the where-clauses declared on
|
||||
`Trait` are well-formed (and hence they are implemented). Remember
|
||||
that the `WellFormed` predicate is
|
||||
[coinductive](./traits-goals-and-clauses.html#coinductive); in this
|
||||
[coinductive](./traits/goals-and-clauses.html#coinductive); in this
|
||||
case, it is serving as a kind of "carrier" that allows us to enumerate
|
||||
all the where clauses that are transitively implied by `T: Trait`.
|
||||
|
||||
|
|
@ -192,7 +192,7 @@ where WC
|
|||
|
||||
We will produce a number of program clauses. The first two define
|
||||
the rules by which `ProjectionEq` can succeed; these two clauses are discussed
|
||||
in detail in the [section on associated types](./traits-associated-types.html),
|
||||
in detail in the [section on associated types](./traits/associated-types.html),
|
||||
but reproduced here for reference:
|
||||
|
||||
```text
|
||||
|
|
|
|||
|
|
@ -170,8 +170,8 @@ example Gopalan Nadathur's excellent
|
|||
["A Proof Procedure for the Logic of Hereditary Harrop Formulas"][pphhf]
|
||||
in [the bibliography].
|
||||
|
||||
[the bibliography]: ./traits-bibliography.html
|
||||
[pphhf]: ./traits-bibliography.html#pphhf
|
||||
[the bibliography]: ./traits/bibliography.html
|
||||
[pphhf]: ./traits/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
|
||||
|
|
|
|||
|
|
@ -6,7 +6,7 @@ some non-obvious things.
|
|||
**Note:** This chapter (and its subchapters) describe how the trait
|
||||
solver **currently** works. However, we are in the process of
|
||||
designing a new trait solver. If you'd prefer to read about *that*,
|
||||
see [*this* traits chapter](./traits.html).
|
||||
see [*this* traits chapter](./traits/index.html).
|
||||
|
||||
## Major concepts
|
||||
|
||||
|
|
|
|||
|
|
@ -125,7 +125,7 @@ actual return type is not `()`, but rather `InferOk<()>`. The
|
|||
to ensure that these are fulfilled (typically by enrolling them in a
|
||||
fulfillment context). See the [trait chapter] for more background on that.
|
||||
|
||||
[trait chapter]: trait-resolution.html
|
||||
[trait chapter]: traits/resolution.html
|
||||
|
||||
You can similarly enforce subtyping through `infcx.at(..).sub(..)`. The same
|
||||
basic concepts as above apply.
|
||||
|
|
|
|||
Loading…
Reference in New Issue