Skip to content

Commit f360594

Browse files
committed
Add some extra work
1 parent e27bc3f commit f360594

File tree

2 files changed

+95
-13
lines changed

2 files changed

+95
-13
lines changed

chalk-solve/src/clauses.rs

Lines changed: 62 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -183,10 +183,14 @@ pub fn push_auto_trait_impls_generator<I: Interner>(
183183

184184
builder.push_binders(&generator_datum.input_output, |builder, input_output| {
185185
let self_ty: Ty<_> = ApplicationTy {
186-
name: generator_id.cast(interner),
186+
name: TypeName::Generator(generator_id),
187187
substitution: builder.substitution_in_scope(),
188-
}
189-
.intern(interner);
188+
}.intern(interner);
189+
190+
let witness_ty = ApplicationTy {
191+
name: TypeName::GeneratorWitness(generator_id),
192+
substitution: builder.substitution_in_scope(),
193+
}.intern(interner);
190194

191195
// trait_ref = `Generator<...>: MyAutoTrait`
192196
let auto_trait_ref = TraitRef {
@@ -207,11 +211,62 @@ pub fn push_auto_trait_impls_generator<I: Interner>(
207211
input_output.upvars.iter().map(|upvar_ty| TraitRef {
208212
trait_id: auto_trait_id,
209213
substitution: Substitution::from1(interner, upvar_ty.clone()),
210-
}),
214+
}).chain(std::iter::once(TraitRef {
215+
trait_id: auto_trait_id,
216+
substitution: Substitution::from1(interner, witness_ty)
217+
})),
211218
);
212219
});
213220
}
214221

222+
#[instrument(level = "debug", skip(builder))]
223+
pub fn push_auto_trait_impls_generator_witness<I: Interner>(
224+
builder: &mut ClauseBuilder<'_, I>,
225+
auto_trait_id: TraitId<I>,
226+
generator_id: GeneratorId<I>,
227+
) {
228+
let witness_datum = builder.db.generator_witness_datum(generator_id);
229+
let interner = builder.interner();
230+
231+
// Must be an auto trait.
232+
assert!(builder.db.trait_datum(auto_trait_id).is_auto_trait());
233+
234+
// Auto traits never have generic parameters of their own (apart from `Self`).
235+
assert_eq!(
236+
builder.db.trait_datum(auto_trait_id).binders.len(interner),
237+
1
238+
);
239+
240+
builder.push_binders(&witness_datum.inner_types, |builder, inner_types| {
241+
let witness_ty = ApplicationTy {
242+
name: TypeName::GeneratorWitness(generator_id),
243+
substitution: builder.substitution_in_scope(),
244+
}.intern(interner);
245+
246+
// trait_ref = `GeneratorWitness<...>: MyAutoTrait`
247+
let auto_trait_ref = TraitRef {
248+
trait_id: auto_trait_id,
249+
substitution: Substitution::from1(interner, witness_ty),
250+
};
251+
252+
builder.push_binders(&inner_types.types, |builder, types| {
253+
// forall<P0..Pn> { // generic parameters from struct
254+
// MyStruct<...>: MyAutoTrait :-
255+
// Field0: MyAutoTrait,
256+
// ...
257+
// FieldN: MyAutoTrait
258+
// }
259+
builder.push_clause(
260+
auto_trait_ref,
261+
types.iter().map(|witness_ty| TraitRef {
262+
trait_id: auto_trait_id,
263+
substitution: Substitution::from1(interner, witness_ty.clone())
264+
})
265+
);
266+
});
267+
})
268+
}
269+
215270
/// Given some goal `goal` that must be proven, along with
216271
/// its `environment`, figures out the program clauses that apply
217272
/// to this goal from the Rust program. So for example if the goal
@@ -301,6 +356,9 @@ fn program_clauses_that_could_match<I: Interner>(
301356
TypeName::Generator(generator_id) => {
302357
push_auto_trait_impls_generator(builder, trait_id, *generator_id);
303358
}
359+
TypeName::GeneratorWitness(generator_id) => {
360+
push_auto_trait_impls_generator_witness(builder, trait_id, *generator_id);
361+
}
304362
_ => {}
305363
},
306364
TyData::InferenceVar(_, _) | TyData::BoundVar(_) => {

tests/test/generators.rs

Lines changed: 33 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,28 +1,52 @@
11
use super::*;
22

33
#[test]
4+
fn simple_impl() {
5+
test! {
6+
program {
7+
#[auto] trait Send { }
8+
9+
struct Generic<'a, 'b, T> { val: &'a T, other: &'b T }
10+
impl<'a, 'b, T> Send for Generic<'b, 'b, T> {}
11+
}
12+
13+
goal {
14+
forall<'a, 'b, T> {
15+
Generic<'a, 'b, T>: Send
16+
}
17+
} yields {
18+
"Unique; substitution [], lifetime constraints []"
19+
}
20+
}
21+
22+
}
23+
24+
//#[test]
425
fn generator_is_well_formed() {
526
test! {
627
program {
728
#[auto] trait Send { }
829

30+
931
struct StructOne {}
1032
struct NotSend {}
11-
impl !Send for NotSend {}
12-
struct StructThree<'a> { val: &'a () }
33+
struct Generic<'a, 'b, T> { val: &'a T, other: &'b T }
34+
impl<'a, 'b, T> Send for Generic<'b, 'b, T> {}
35+
//impl !Send for NotSend {}
36+
//struct StructThree<'a> { val: &'a () }
1337

14-
generator foo<>[resume = (), yield = ()] {
38+
/*generator foo<>[resume = (), yield = ()] {
1539
upvars []
1640
witnesses []
17-
}
41+
}*/
1842

1943
generator bar<T>[resume = (), yield = ()] {
20-
upvars [T; StructOne]
21-
witnesses for<'a> [NotSend]
44+
upvars [/*T; StructOne*/]
45+
witnesses for<'a, 'b> [Generic<'a, 'b, T>]
2246
}
2347
}
2448

25-
goal {
49+
/*goal {
2650
WellFormed(foo)
2751
} yields {
2852
"Unique"
@@ -40,7 +64,7 @@ fn generator_is_well_formed() {
4064
}
4165
} yields {
4266
"No possible solution"
43-
}
67+
}*/
4468

4569
goal {
4670
forall<T> {
@@ -49,7 +73,7 @@ fn generator_is_well_formed() {
4973
}
5074
}
5175
} yields {
52-
"Unique"
76+
"Unique; substitution [], lifetime constraints []"
5377
}
5478
}
5579
}

0 commit comments

Comments
 (0)