diff --git a/src/traits-canonical-queries.md b/src/traits-canonical-queries.md index 3fea5fbd..b291a289 100644 --- a/src/traits-canonical-queries.md +++ b/src/traits-canonical-queries.md @@ -99,7 +99,8 @@ that the query was false and had no answers (e.g., `Box: Copy`). Otherwise, the `QueryResult` gives back information about the possible answer(s) we did find. It consists of four parts: -- **Certainty:** tells you how sure we are of this answer. It can have two values: +- **Certainty:** tells you how sure we are of this answer. It can have two + values: - `Proven` means that the result is known to be true. - This might be the result for trying to prove `Vec: Clone`, say, or `Rc: Clone`. @@ -171,7 +172,8 @@ Therefore, the result we get back would be as follows (I'm going to ignore region constraints and the "value"): - Certainty: `Ambiguous` -- we're not sure yet if this holds -- Var values: `[?T = ?T, ?U = ?U]` -- we learned nothing about the values of the variables +- Var values: `[?T = ?T, ?U = ?U]` -- we learned nothing about the values of + the variables In short, the query result says that it is too soon to say much about whether this trait is proven. During type-checking, this is not an diff --git a/src/traits-canonicalization.md b/src/traits-canonicalization.md index bef858af..9f3af36c 100644 --- a/src/traits-canonicalization.md +++ b/src/traits-canonicalization.md @@ -129,8 +129,8 @@ for which we made a substutition S: S = [?A, '?B, ?C] -We then did some work which unified some of those variables with other things. If we -"refresh" S with the latest results, we get: +We then did some work which unified some of those variables with other things. +If we "refresh" S with the latest results, we get: S = [Vec, '?D, ?E] diff --git a/src/traits-goals-and-clauses.md b/src/traits-goals-and-clauses.md index 92e1b67d..8e5e82d0 100644 --- a/src/traits-goals-and-clauses.md +++ b/src/traits-goals-and-clauses.md @@ -81,13 +81,15 @@ Given that, we can define a `DomainGoal` as follows: - as we'll see in the section on lowering, `FromEnv(X)` implies `Implemented(X)` but not vice versa. This distinction is crucial to [implied bounds]. -- `ProjectionEq(Projection = Type)` -- the given associated type `Projection` is equal - to `Type`; see [the section on associated types](./traits-associated-types.html) +- `ProjectionEq(Projection = Type)` -- the given associated type `Projection` + is equal to `Type`; see [the section on associated + types](./traits-associated-types.html) - in general, proving `ProjectionEq(TraitRef::Item = Type)` also requires proving `Implemented(TraitRef)` -- `Normalize(Projection -> Type)` -- the given associated type `Projection` can be [normalized][n] - to `Type` - - as discussed in [the section on associated types](./traits-associated-types.html), +- `Normalize(Projection -> Type)` -- 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` but not vice versa - `WellFormed(..)` -- these goals imply that the given item is *well-formed* diff --git a/src/traits-lowering-rules.md b/src/traits-lowering-rules.md index 8de20f1d..544ae41b 100644 --- a/src/traits-lowering-rules.md +++ b/src/traits-lowering-rules.md @@ -26,7 +26,7 @@ Each of these lowering rules is given a name, documented with a comment like so: // Rule Foo-Bar-Baz - + you can also search through the `librustc_traits` crate in rustc to find the corresponding rules from the implementation. @@ -36,7 +36,8 @@ When used in a goal position, where clauses can be mapped directly to [domain goals][dg], as follows: - `A0: Foo` maps to `Implemented(A0: Foo)`. -- `A0: Foo` maps to `ProjectionEq(>::Item = T)` +- `A0: Foo` maps to + `ProjectionEq(>::Item = T)` - `T: 'r` maps to `Outlives(T, 'r)` - `'a: 'b` maps to `Outlives('a, 'b)` @@ -58,7 +59,7 @@ on the lowered where clauses, as defined here: - `WellFormed(WC)` -- this indicates that: - `Implemented(TraitRef)` becomes `WellFormed(TraitRef)` - `ProjectionEq(Projection = Ty)` becomes `WellFormed(Projection = Ty)` - + *TODO*: I suspect that we want to alter the outlives relations too, but Chalk isn't modeling those right now. @@ -106,7 +107,7 @@ The next few clauses have to do with implied bounds (see also forall { FromEnv(WC) :- FromEnv(Self: Trait { - WellFormed(Self: Trait) :- Implemented(Self: Trait) && WellFormed(WC) - } +```txt +// Rule WellFormed-TraitRef +// +// For each where clause WC: +forall { + WellFormed(Self: Trait) :- Implemented(Self: Trait) && WellFormed(WC) +} +``` This `WellFormed` rule states that `T: Trait` is well-formed if (a) `T: Trait` is implemented and (b) all the where-clauses declared on @@ -149,9 +152,9 @@ trait A { } trait B { } ``` -Here, the transitive set of implications for `T: Foo` are `T: A`, `T: Bar`, and `T: B`. -And indeed if we were to try to prove `WellFormed(T: Foo)`, we would have to prove each -one of those: +Here, the transitive set of implications for `T: Foo` are `T: A`, `T: Bar`, and +`T: B`. And indeed if we were to try to prove `WellFormed(T: Foo)`, we would +have to prove each one of those: - `WellFormed(T: Foo)` - `Implemented(T: Foo)` @@ -212,7 +215,7 @@ but reproduced here for reference: Implemented(Self: Trait) && WC1 } - + The next rule covers implied bounds for the projection. In particular, the `Bounds` declared on the associated type must be proven to hold to show that the impl is well-formed, and hence we can rely on them @@ -223,8 +226,8 @@ elsewhere. ### Lowering function and constant declarations -Chalk didn't model functions and constants, but I would eventually -like to treat them exactly like normalization. See [the section on function/constant +Chalk didn't model functions and constants, but I would eventually like to +treat them exactly like normalization. See [the section on function/constant values below](#constant-vals) for more details. ## Lowering impls @@ -272,7 +275,7 @@ We produce the following rule: WC && WC1 } } - + Note that `WC` and `WC1` both encode where-clauses that the impl can rely on.