Skip to content

Commit 2943c77

Browse files
committed
Fix links.
1 parent 1717735 commit 2943c77

File tree

11 files changed

+40
-38
lines changed

11 files changed

+40
-38
lines changed

book/src/canonical_queries/canonicalization.md

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -6,8 +6,8 @@ from its context. It is a key part of implementing
66
to get more context.
77

88
Canonicalization is really based on a very simple concept: every
9-
[inference variable](../type-inference.html#vars) is always in one of
10-
two states: either it is **unbound**, in which case we don't know yet
9+
[inference variable](https://rustc-dev-guide.rust-lang.org/type-inference.html#vars)
10+
is always in one of two states: either it is **unbound**, in which case we don't know yet
1111
what type it is, or it is **bound**, in which case we do. So to
1212
isolate some data-structure T that contains types/regions from its
1313
environment, we just walk down and find the unbound variables that
@@ -16,7 +16,7 @@ starting from zero and numbered in a fixed order (left to right, for
1616
the most part, but really it doesn't matter as long as it is
1717
consistent).
1818

19-
[cq]: ./canonical-queries.html
19+
[cq]: ../canonical_queries.html
2020

2121
So, for example, if we have the type `X = (?T, ?U)`, where `?T` and
2222
`?U` are distinct, unbound inference variables, then the canonical
@@ -41,7 +41,7 @@ trait query: `?A: Foo<'static, ?B>`, where `?A` and `?B` are unbound.
4141
This query contains two unbound variables, but it also contains the
4242
lifetime `'static`. The trait system generally ignores all lifetimes
4343
and treats them equally, so when canonicalizing, we will *also*
44-
replace any [free lifetime](../appendix/background.html#free-vs-bound) with a
44+
replace any [free lifetime](https://rustc-dev-guide.rust-lang.org/appendix/background.html#free-vs-bound) with a
4545
canonical variable (Note that `'static` is actually a _free_ lifetime
4646
variable here. We are not considering it in the typing context of the whole
4747
program but only in the context of this trait reference. Mathematically, we
@@ -102,12 +102,12 @@ Remember that substitution S though! We're going to need it later.
102102

103103
OK, now that we have a fresh inference context and an instantiated
104104
query, we can go ahead and try to solve it. The trait solver itself is
105-
explained in more detail in [another section](./slg.html), but
105+
explained in more detail in [another section](../engine/slg.html), but
106106
suffice to say that it will compute a [certainty value][cqqr] (`Proven` or
107107
`Ambiguous`) and have side-effects on the inference variables we've
108108
created. For example, if there were only one impl of `Foo`, like so:
109109

110-
[cqqr]: ./canonical-queries.html#query-response
110+
[cqqr]: ../canonical_queries.html#query-response
111111

112112
```rust,ignore
113113
impl<'a, X> Foo<'a, X> for Vec<X>

book/src/clauses/goals_and_clauses.md

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22

33
In logic programming terms, a **goal** is something that you must
44
prove and a **clause** is something that you know is true. As
5-
described in the [lowering to logic](./lowering-to-logic.html)
5+
described in the [lowering to logic](../clauses.html)
66
chapter, Rust's trait solver is based on an extension of hereditary
77
harrop (HH) clauses, which extend traditional Prolog Horn clauses with
88
a few new superpowers.
@@ -41,7 +41,7 @@ In terms of code, these types are defined in
4141
[`librustc_middle/traits/mod.rs`][traits_mod] in rustc, and in
4242
[`chalk-ir/src/lib.rs`][chalk_ir] in chalk.
4343

44-
[pphhf]: ./bibliography.html#pphhf
44+
[pphhf]: ../bibliography.html#pphhf
4545
[traits_mod]: https://github.com/rust-lang/rust/blob/master/src/librustc_middle/traits/mod.rs
4646
[chalk_ir]: https://github.com/rust-lang/chalk/blob/master/chalk-ir/src/lib.rs
4747

@@ -118,20 +118,20 @@ e.g. `ProjectionEq<T as Iterator>::Item = u8`
118118

119119
The given associated type `Projection` is equal to `Type`; this can be proved
120120
with either normalization or using placeholder associated types. See
121-
[the section on associated types](./associated-types.html).
121+
[the section on associated types](./type_equality.html).
122122

123123
#### Normalize(Projection -> Type)
124124
e.g. `ProjectionEq<T as Iterator>::Item -> u8`
125125

126126
The given associated type `Projection` can be [normalized][n] to `Type`.
127127

128128
As discussed in [the section on associated
129-
types](./associated-types.html), `Normalize` implies `ProjectionEq`,
129+
types](./type_equality.html), `Normalize` implies `ProjectionEq`,
130130
but not vice versa. In general, proving `Normalize(<T as Trait>::Item -> U)`
131131
also requires proving `Implemented(T: Trait)`.
132132

133-
[n]: ./associated-types.html#normalize
134-
[at]: ./associated-types.html
133+
[n]: ./type_equality.html#normalize
134+
[at]: ./type_equality.html
135135

136136
#### FromEnv(TraitRef)
137137
e.g. `FromEnv(Self: Add<i32>)`
@@ -260,4 +260,4 @@ In addition to auto traits, `WellFormed` predicates are co-inductive.
260260
These are used to achieve a similar "enumerate all the cases" pattern,
261261
as described in the section on [implied bounds].
262262

263-
[implied bounds]: ./lowering-rules.html#implied-bounds
263+
[implied bounds]: ./lowering_rules.html#implied-bounds

book/src/clauses/implied_bounds.md

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -89,7 +89,7 @@ works for outlive requirements, super trait bounds, and bounds on associated
8989
types. The full RFC can be found [here][RFC]. We'll give here a brief view
9090
of how implied bounds work and why we chose to implement it that way. The
9191
complete set of lowering rules can be found in the corresponding
92-
[chapter](./lowering-rules.md).
92+
[chapter](./lowering_rules.md).
9393

9494
[RFC]: https://github.com/rust-lang/rfcs/blob/master/text/2089-implied-bounds.md
9595

@@ -449,7 +449,7 @@ this clearly is a cycle and cycles are usually rejected by the trait solver,
449449
unless... if the `WellFormed` predicate was made to be co-inductive.
450450

451451
A co-inductive predicate, as discussed in the chapter on
452-
[goals and clauses](./goals-and-clauses.md#coinductive-goals), are predicates
452+
[goals and clauses](./goals_and_clauses.html#coinductive-goals), are predicates
453453
for which the
454454
trait solver accepts cycles. In our setting, this would be a valid thing to do:
455455
indeed, the `WellFormed` predicate just serves as a way of enumerating all

book/src/clauses/lowering_rules.md

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -4,8 +4,8 @@ This section gives the complete lowering rules for Rust traits into
44
[program clauses][pc]. It is a kind of reference. These rules
55
reference the [domain goals][dg] defined in an earlier section.
66

7-
[pc]: ./goals-and-clauses.html
8-
[dg]: ./goals-and-clauses.html#domain-goals
7+
[pc]: ./goals_and_clauses.html
8+
[dg]: ./goals_and_clauses.html#domain-goals
99

1010
## Notation
1111

@@ -16,7 +16,7 @@ The nonterminal `Ai` is used to mean some generic *argument*, which
1616
might be a lifetime like `'a` or a type like `Vec<A>`.
1717

1818
When defining the lowering rules, we will give goals and clauses in
19-
the [notation given in this section](./goals-and-clauses.html).
19+
the [notation given in this section](./goals_and_clauses.html).
2020
We sometimes insert "macros" like `LowerWhereClause!` into these
2121
definitions; these macros reference other sections within this chapter.
2222

@@ -107,7 +107,7 @@ The next few clauses have to do with implied bounds (see also
107107
cover). For each trait, we produce two clauses:
108108

109109
[RFC 2089]: https://rust-lang.github.io/rfcs/2089-implied-bounds.html
110-
[implied_bounds]: ./implied-bounds.md
110+
[implied_bounds]: ./implied_bounds.md
111111

112112
```text
113113
// Rule Implied-Bound-From-Trait
@@ -147,7 +147,7 @@ This `WellFormed` rule states that `T: Trait` is well-formed if (a)
147147
`T: Trait` is implemented and (b) all the where-clauses declared on
148148
`Trait` are well-formed (and hence they are implemented). Remember
149149
that the `WellFormed` predicate is
150-
[coinductive](./goals-and-clauses.html#coinductive); in this
150+
[coinductive](./goals_and_clauses.html#coinductive); in this
151151
case, it is serving as a kind of "carrier" that allows us to enumerate
152152
all the where clauses that are transitively implied by `T: Trait`.
153153

@@ -272,7 +272,7 @@ where WC
272272

273273
We will produce a number of program clauses. The first two define
274274
the rules by which `ProjectionEq` can succeed; these two clauses are discussed
275-
in detail in the [section on associated types](./associated-types.html),
275+
in detail in the [section on associated types](./type_equality.html),
276276
but reproduced here for reference:
277277

278278
```text

book/src/clauses/type_equality.md

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@ type can be referenced by the user using an **associated type
1717
projection** like `<Option<u32> as IntoIterator>::Item`.
1818

1919
> Often, people will use the shorthand syntax `T::Item`. Presently, that
20-
> syntax is expanded during ["type collection"](../type-checking.html) into the
20+
> syntax is expanded during ["type collection"](https://rustc-dev-guide.rust-lang.org/type-checking.html) into the
2121
> explicit form, though that is something we may want to change in the future.
2222
2323
[intoiter-item]: https://doc.rust-lang.org/nightly/core/iter/trait.IntoIterator.html#associatedtype.Item
@@ -141,8 +141,8 @@ any given associated item.
141141

142142
Now we are ready to discuss how associated type equality integrates
143143
with unification. As described in the
144-
[type inference](../type-inference.html) section, unification is
145-
basically a procedure with a signature like this:
144+
[type inference](https://rustc-dev-guide.rust-lang.org/type-inference.html)
145+
section, unification is basically a procedure with a signature like this:
146146

147147
```text
148148
Unify(A, B) = Result<(Subgoals, RegionConstraints), NoSolution>

book/src/clauses/wf.md

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ the trait.
88

99
For each declaration in a Rust program, we will generate a logical goal and try
1010
to prove it using the lowered rules we described in the
11-
[lowering rules](./lowering-rules.md) chapter. If we are able to prove it, we
11+
[lowering rules](./lowering_rules.md) chapter. If we are able to prove it, we
1212
say that the construct is well-formed. If not, we report an error to the user.
1313

1414
Well-formedness checking happens in the [`chalk/chalk-solve/src/wf.rs`][wf]
@@ -285,7 +285,7 @@ the input types of `SomeType<A2...>` are well-formed, we prove that
285285
`WellFormed(SomeType<A2...>: Trait<A1...>)` hold. That is, we want to prove
286286
that `SomeType<A2...>` verify all the where clauses that might transitively
287287
be required by the `Trait` definition (see
288-
[this subsection](./implied-bounds.md#co-inductiveness-of-wellformed)).
288+
[this subsection](./implied_bounds.md#co-inductiveness-of-wellformed)).
289289

290290
Lastly, assuming in addition that the where clauses on the associated type
291291
`WC_assoc` hold,

book/src/engine/logic/coinduction.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -291,4 +291,4 @@ What happens here is that we get an initial answer from `C1` that looks like:
291291
C1(44) :- C1(22) |
292292
```
293293

294-
Ensure root answer will thus try to refine by trying to solve `C1(22)`. Interestingly, this is going to go to a distinct table, because the canonical form is not the same, but that table will just fail.
294+
Ensure root answer will thus try to refine by trying to solve `C1(22)`. Interestingly, this is going to go to a distinct table, because the canonical form is not the same, but that table will just fail.

book/src/engine/slg.md

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ For example, `exists<T> { Vec<T>: FromIterator<u32> }` has one solution, so
88
its result is `Unique; substitution [?T := u32]`. A solution also comes with
99
a set of region constraints, which we'll ignore in this introduction.
1010

11-
[lowering]: ./lowering-rules.html
11+
[lowering]: ../clauses.html
1212

1313
## Goals of the Solver
1414

@@ -23,7 +23,7 @@ done. This is similar to how Prolog works.
2323

2424
*See also: [The traditional, interactive Prolog query][pq]*
2525

26-
[pq]: ./canonical-queries.html#the-traditional-interactive-prolog-query
26+
[pq]: ../canonical_queries.html#the-traditional-interactive-prolog-query
2727

2828
### Breadth-first
2929

@@ -246,7 +246,7 @@ applied to the table goal; actually, in the code, the goals for each
246246
X-clause are also represented as substitutions, but in this exposition
247247
I've chosen to write them as full goals, following [NFTD].
248248

249-
[NFTD]: ./bibliography.html#slg
249+
[NFTD]: ../bibliography.html#slg
250250

251251
Since we now have an answer, `ensure_answer(T1, A0)` will return `Ok`
252252
to the table T0, indicating that answer A0 is available. T0 now has

book/src/types/operations/fold.md

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -45,6 +45,8 @@ The overall flow of folding is like this.
4545
as [`Folder::fold_free_var_ty`], which makes it easier to write
4646
folders that just intercept *certain* types.
4747

48+
[`Folder::fold_free_var_ty`]: https://rust-lang.github.io/chalk/chalk_ir/fold/trait.Folder.html#method.fold_free_var_ty
49+
4850
Thus, as a user, you can customize folding by:
4951

5052
* Defining your own `Folder` type

book/src/types/rust_types.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -204,7 +204,7 @@ types. The intention is that, at least when transitioning, rustc would
204204
implement the `Interner` trait and would map from the [`TyKind`]
205205
enum to chalk's `TyData` on the fly, when `data()` is invoked.
206206

207-
[`TyKind`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc/ty/enum.TyKind.html
207+
[`TyKind`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/ty/enum.TyKind.html
208208

209209
This section describes how each of rustc's variants can be mapped to
210210
Chalk variants.

0 commit comments

Comments
 (0)