Skip to content

Commit 52787a6

Browse files
nikomatsakismark-i-m
authored andcommitted
add names to the trait lowering rules
This allows cross-references from the code.
1 parent 81071c6 commit 52787a6

File tree

1 file changed

+21
-0
lines changed

1 file changed

+21
-0
lines changed

Diff for: src/traits-lowering-rules.md

+21
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,16 @@ the [notation given in this section](./traits-goals-and-clauses.html).
2020
We sometimes insert "macros" like `LowerWhereClause!` into these
2121
definitions; these macros reference other sections within this chapter.
2222

23+
## Rule names and cross-references
24+
25+
Each of these lowering rules is given a name, documented with a
26+
comment like so:
27+
28+
// Rule Foo-Bar-Baz
29+
30+
you can also search through the `librustc_traits` crate in rustc
31+
to find the corresponding rules from the implementation.
32+
2333
## Lowering where clauses
2434

2535
When used in a goal position, where clauses can be mapped directly to
@@ -76,6 +86,7 @@ relationships between different kinds of domain goals. The first such
7686
rule from the trait header creates the mapping between the `FromEnv`
7787
and `Implemented` predicates:
7888

89+
// Rule Implemented-From-Env
7990
forall<Self, P1..Pn> {
8091
Implemented(Self: Trait<P1..Pn>) :- FromEnv(Self: Trait<P1..Pn>)
8192
}
@@ -89,6 +100,8 @@ The next few clauses have to do with implied bounds (see also
89100

90101
[RFC 2089]: https://rust-lang.github.io/rfcs/2089-implied-bounds.html
91102

103+
// Rule Implied-Bound-From-Trait
104+
//
92105
// For each where clause WC:
93106
forall<Self, P1..Pn> {
94107
FromEnv(WC) :- FromEnv(Self: Trait<P1..Pn)
@@ -112,6 +125,8 @@ clauses** but also things that follow from them.
112125
The next rule is related; it defines what it means for a trait reference
113126
to be **well-formed**:
114127

128+
// Rule WellFormed-TraitRef
129+
//
115130
// For each where clause WC:
116131
forall<Self, P1..Pn> {
117132
WellFormed(Self: Trait<P1..Pn>) :- Implemented(Self: Trait<P1..Pn>) && WellFormed(WC)
@@ -175,12 +190,16 @@ the rules by which `ProjectionEq` can succeed; these two clauses are discussed
175190
in detail in the [section on associated types](./traits-associated-types.html),,
176191
but reproduced here for reference:
177192

193+
// Rule ProjectionEq-Normalize
194+
//
178195
// ProjectionEq can succeed by normalizing:
179196
forall<Self, P1..Pn, Pn+1..Pm, U> {
180197
ProjectionEq(<Self as Trait<P1..Pn>>::AssocType<Pn+1..Pm> = U) :-
181198
Normalize(<Self as Trait<P1..Pn>>::AssocType<Pn+1..Pm> -> U)
182199
}
183200

201+
// Rule ProjectionEq-Skolemize
202+
//
184203
// ProjectionEq can succeed by skolemizing, see "associated type"
185204
// chapter for more:
186205
forall<Self, P1..Pn, Pn+1..Pm> {
@@ -223,6 +242,7 @@ where WC
223242
Let `TraitRef` be the trait reference `A0: Trait<A1..An>`. Then we
224243
will create the following rules:
225244

245+
// Rule Implemented-From-Impl
226246
forall<P0..Pn> {
227247
Implemented(TraitRef) :- WC
228248
}
@@ -245,6 +265,7 @@ where WC
245265

246266
We produce the following rule:
247267

268+
// Rule Normalize-From-Impl
248269
forall<P0..Pm> {
249270
forall<Pn+1..Pm> {
250271
Normalize(<A0 as Trait<A1..An>>::AssocType<Pn+1..Pm> -> T) :-

0 commit comments

Comments
 (0)