@@ -37,15 +37,33 @@ paper
3737[ "A Proof Procedure for the Logic of Hereditary Harrop Formulas"] [ pphhf ]
3838gives the details.
3939
40+ In terms of code, these types are defined in
41+ [ ` librustc/traits/mod.rs ` ] [ traits_mod ] in rustc, and in
42+ [ ` chalk-ir/src/lib.rs ` ] [ chalk_ir ] in chalk.
43+
4044[ pphhf ] : ./bibliography.html#pphhf
45+ [ traits_mod ] : https://github.com/rust-lang/rust/blob/master/src/librustc/traits/mod.rs
46+ [ chalk_ir ] : https://github.com/rust-lang-nursery/chalk/blob/master/chalk-ir/src/lib.rs
4147
4248<a name =" domain-goals " ></a >
4349
4450## Domain goals
4551
52+ * Domain goals* are the atoms of the trait logic. As can be seen in the
53+ definitions given above, general goals basically consist in a combination of
54+ domain goals.
55+
56+ Moreover, flattenning a bit the definition of clauses given previously, one can
57+ see that clauses are always of the form:
58+ ``` text
59+ forall<K1, ..., Kn> { DomainGoal :- Goal }
60+ ```
61+ hence domain goals are in fact clauses LHS. That is, at the most granular level,
62+ domain goals are what the trait solver will end up trying to prove.
63+
4664<a name =" trait-ref " ></a >
4765
48- To define the set of * domain goals* in our system, we need to first
66+ To define the set of domain goals in our system, we need to first
4967introduce a few simple formulations. A ** trait reference** consists of
5068the name of a trait along with a suitable set of inputs P0..Pn:
5169
@@ -70,18 +88,24 @@ Projection = <P0 as TraitName<P1..Pn>>::AssocItem<Pn+1..Pm>
7088Given these, we can define a ` DomainGoal ` as follows:
7189
7290``` text
73- DomainGoal = Implemented(TraitRef)
74- | ProjectionEq(Projection = Type)
75- | Normalize(Projection -> Type)
91+ DomainGoal = Holds(WhereClause)
7692 | FromEnv(TraitRef)
77- | FromEnv(Projection = Type)
78- | WellFormed(Type)
93+ | FromEnv(Type)
7994 | WellFormed(TraitRef)
80- | WellFormed(Projection = Type)
95+ | WellFormed(Type)
96+ | Normalize(Projection -> Type)
97+
98+ WhereClause = Implemented(TraitRef)
99+ | ProjectionEq(Projection = Type)
81100 | Outlives(Type: Region)
82101 | Outlives(Region: Region)
83102```
84103
104+ ` WhereClause ` refers to a ` where ` clause that a Rust user would actually be able
105+ to write in a Rust program. This abstraction exists only as a convenience as we
106+ sometimes want to only coope with domain goals that are effectively writable in
107+ Rust.
108+
85109Let's break down each one of these, one-by-one.
86110
87111#### Implemented(TraitRef)
@@ -109,12 +133,10 @@ also requires proving `Implemented(T: Trait)`.
109133[ n ] : ./associated-types.html#normalize
110134[ at ] : ./associated-types.html
111135
112- #### FromEnv(TraitRef), FromEnv(Projection = Type)
136+ #### FromEnv(TraitRef)
113137e.g. ` FromEnv(Self: Add<i32>) `
114138
115- e.g. ` FromEnv(<Self as StreamingIterator>::Item<'a> = &'a [u8]) `
116-
117- True if the inner ` TraitRef ` or projection equality is * assumed* to be true;
139+ True if the inner ` TraitRef ` is * assumed* to be true,
118140that is, if it can be derived from the in-scope where clauses.
119141
120142For example, given the following function:
@@ -131,24 +153,49 @@ where clauses nest, so a function body inside an impl body inherits the
131153impl body's where clauses, too.
132154
133155This and the next rule are used to implement [ implied bounds] . As we'll see
134- in the section on lowering, ` FromEnv(X) ` implies ` Implemented(X) ` , but not
135- vice versa. This distinction is crucial to implied bounds.
156+ in the section on lowering, ` FromEnv(TraitRef) ` implies ` Implemented(TraitRef) ` ,
157+ but not vice versa. This distinction is crucial to implied bounds.
158+
159+ #### FromEnv(Type)
160+ e.g. ` FromEnv(HashSet<K>) `
161+
162+ True if the inner ` Type ` is * assumed* to be well-formed, that is, if it is an
163+ input type of a function or an impl.
164+
165+ For example, given the following code:
166+
167+ ``` rust,ignore
168+ struct HashSet<K> where K: Hash { ... }
169+
170+ fn loud_insert<K>(set: &mut HashSet<K>, item: K) {
171+ println!("inserting!");
172+ set.insert(item);
173+ }
174+ ```
175+
176+ ` HashSet<K> ` is an input type of the ` loud_insert ` function. Hence, we assume it
177+ to be well-formed, so we would have ` FromEnv(HashSet<K>) ` inside the body or our
178+ function. Here ` FromEnv(HashSet<K>) ` implies ` Implemented(K: Hash) ` because the
179+ ` HashSet ` declaration was written with a ` K: Hash ` where clause. Hence, we don't
180+ need to repeat that bound on the ` loud_insert ` function: we rather automatically
181+ assume that it is true.
136182
137183#### WellFormed(Item)
138184These goals imply that the given item is * well-formed* .
139185
140186We can talk about different types of items being well-formed:
141187
142- ** Types* *` WellFormed(Vec<i32>) ` , which is true in Rust, or
188+ * * Types* , like ` WellFormed(Vec<i32>) ` , which is true in Rust, or
143189 ` WellFormed(Vec<str>) ` , which is not (because ` str ` is not ` Sized ` .)
144190
145- ** TraitRefs** , like ` WellFormed(Vec<i32>: Clone) ` .
146-
147- ** Projections** , like ` WellFormed(T: Iterator<Item = u32>) ` .
191+ * * TraitRefs* , like ` WellFormed(Vec<i32>: Clone) ` .
148192
149193Well-formedness is important to [ implied bounds] . In particular, the reason
150- it is okay to assume ` FromEnv(T: Clone) ` in the example above is that we
194+ it is okay to assume ` FromEnv(T: Clone) ` in the ` loud_clone ` example is that we
151195_ also_ verify ` WellFormed(T: Clone) ` for each call site of ` loud_clone ` .
196+ Similarly, it is okay to assume ` FromEnv(HashSet<K>) ` in the ` loud_insert `
197+ example because we will verify ` WellFormed(HashSet<K>) ` for each call site of
198+ ` loud_insert ` .
152199
153200#### Outlives(Type: Region), Outlives(Region: Region)
154201e.g. ` Outlives(&'a str: 'b) ` , ` Outlives('a: 'static) `
0 commit comments