Skip to content

Commit ce31db8

Browse files
committed
Make the Generator trait well-known
Signed-off-by: Nick Cameron <nrc@ncameron.org>
1 parent 9a8674f commit ce31db8

File tree

9 files changed

+134
-2
lines changed

9 files changed

+134
-2
lines changed

chalk-integration/src/lowering.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1133,6 +1133,7 @@ impl Lower for WellKnownTrait {
11331133
WellKnownTrait::Unpin => rust_ir::WellKnownTrait::Unpin,
11341134
WellKnownTrait::CoerceUnsized => rust_ir::WellKnownTrait::CoerceUnsized,
11351135
WellKnownTrait::DiscriminantKind => rust_ir::WellKnownTrait::DiscriminantKind,
1136+
WellKnownTrait::Generator => rust_ir::WellKnownTrait::Generator,
11361137
}
11371138
}
11381139
}

chalk-parse/src/ast.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -158,6 +158,7 @@ pub enum WellKnownTrait {
158158
Unpin,
159159
CoerceUnsized,
160160
DiscriminantKind,
161+
Generator,
161162
}
162163

163164
#[derive(Clone, PartialEq, Eq, Debug)]

chalk-parse/src/parser.lalrpop

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -66,6 +66,7 @@ WellKnownTrait: WellKnownTrait = {
6666
"#" "[" "lang" "(" "unpin" ")" "]" => WellKnownTrait::Unpin,
6767
"#" "[" "lang" "(" "coerce_unsized" ")" "]" => WellKnownTrait::CoerceUnsized,
6868
"#" "[" "lang" "(" "discriminant_kind" ")" "]" => WellKnownTrait::DiscriminantKind,
69+
"#" "[" "lang" "(" "generator" ")" "]" => WellKnownTrait::Generator,
6970
};
7071

7172
AdtReprAttr: AdtReprAttr = {

chalk-solve/src/clauses/builtin_traits.rs

Lines changed: 12 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ mod clone;
66
mod copy;
77
mod discriminant_kind;
88
mod fn_family;
9+
mod generator;
910
mod sized;
1011
mod unsize;
1112

@@ -37,13 +38,16 @@ pub fn add_builtin_program_clauses<I: Interner>(
3738
clone::add_clone_program_clauses(db, builder, trait_ref, ty, binders)?;
3839
}
3940
WellKnownTrait::FnOnce | WellKnownTrait::FnMut | WellKnownTrait::Fn => {
40-
fn_family::add_fn_trait_program_clauses(db, builder, well_known, self_ty)?
41+
fn_family::add_fn_trait_program_clauses(db, builder, well_known, self_ty)?;
4142
}
4243
WellKnownTrait::Unsize => {
4344
unsize::add_unsize_program_clauses(db, builder, trait_ref, ty)
4445
}
4546
// DiscriminantKind is automatically implemented for all types
4647
WellKnownTrait::DiscriminantKind => builder.push_fact(trait_ref),
48+
WellKnownTrait::Generator => {
49+
generator::add_generator_program_clauses(db, builder, self_ty)?;
50+
}
4751
// There are no builtin impls provided for the following traits:
4852
WellKnownTrait::Unpin | WellKnownTrait::Drop | WellKnownTrait::CoerceUnsized => (),
4953
}
@@ -73,6 +77,13 @@ pub fn add_builtin_assoc_program_clauses<I: Interner>(
7377
WellKnownTrait::DiscriminantKind => {
7478
discriminant_kind::add_discriminant_clauses(db, builder, self_ty)
7579
}
80+
WellKnownTrait::Generator => {
81+
let generalized = generalize::Generalize::apply(db.interner(), self_ty);
82+
83+
builder.push_binders(generalized, |builder, self_ty| {
84+
generator::add_generator_program_clauses(db, builder, self_ty)
85+
})
86+
}
7687
_ => Ok(()),
7788
}
7889
}
Lines changed: 76 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,76 @@
1+
use crate::clauses::ClauseBuilder;
2+
use crate::rust_ir::WellKnownTrait;
3+
use crate::{Interner, RustIrDatabase, TraitRef};
4+
use chalk_ir::cast::Cast;
5+
use chalk_ir::{AliasTy, Floundered, Normalize, ProjectionTy, Substitution, Ty, TyKind};
6+
7+
/// Add implicit impls of the generator trait, i.e., add a clause that all generators implement
8+
/// `Generator` and clauses for `Generator`'s associated types.
9+
pub fn add_generator_program_clauses<I: Interner>(
10+
db: &dyn RustIrDatabase<I>,
11+
builder: &mut ClauseBuilder<'_, I>,
12+
self_ty: Ty<I>,
13+
) -> Result<(), Floundered> {
14+
let interner = db.interner();
15+
16+
match self_ty.kind(interner) {
17+
TyKind::Generator(id, substitution) => {
18+
let generator_datum = db.generator_datum(*id);
19+
let generator_io_datum = generator_datum
20+
.input_output
21+
.clone()
22+
.substitute(interner, &substitution);
23+
24+
let trait_id = db.well_known_trait_id(WellKnownTrait::Generator).unwrap();
25+
let trait_datum = db.trait_datum(trait_id);
26+
assert_eq!(
27+
trait_datum.associated_ty_ids.len(),
28+
2,
29+
"Generator trait should have exactly two associated types, found {:?}",
30+
trait_datum.associated_ty_ids
31+
);
32+
33+
let substitution = Substitution::from_iter(
34+
interner,
35+
&[
36+
self_ty.cast(interner),
37+
generator_io_datum.resume_type.cast(interner),
38+
],
39+
);
40+
41+
// generator: Generator<resume_type>
42+
builder.push_fact(TraitRef {
43+
trait_id,
44+
substitution: substitution.clone(),
45+
});
46+
47+
// `Generator::Yield`
48+
let yield_id = trait_datum.associated_ty_ids[0];
49+
let yield_alias = AliasTy::Projection(ProjectionTy {
50+
associated_ty_id: yield_id,
51+
substitution: substitution.clone(),
52+
});
53+
builder.push_fact(Normalize {
54+
alias: yield_alias,
55+
ty: generator_io_datum.yield_type,
56+
});
57+
58+
// `Generator::Return`
59+
let return_id = trait_datum.associated_ty_ids[1];
60+
let return_alias = AliasTy::Projection(ProjectionTy {
61+
associated_ty_id: return_id,
62+
substitution,
63+
});
64+
builder.push_fact(Normalize {
65+
alias: return_alias,
66+
ty: generator_io_datum.return_type,
67+
});
68+
69+
Ok(())
70+
}
71+
72+
// Generator trait is non-enumerable
73+
TyKind::InferenceVar(..) | TyKind::BoundVar(_) | TyKind::Alias(..) => Err(Floundered),
74+
_ => Ok(()),
75+
}
76+
}

chalk-solve/src/display/items.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -203,6 +203,7 @@ impl<I: Interner> RenderAsRust<I> for TraitDatum<I> {
203203
WellKnownTrait::Unpin => "unpin",
204204
WellKnownTrait::CoerceUnsized => "coerce_unsized",
205205
WellKnownTrait::DiscriminantKind => "discriminant_kind",
206+
WellKnownTrait::Generator => "generator",
206207
};
207208
writeln!(f, "#[lang({})]", name)?;
208209
}

chalk-solve/src/rust_ir.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -262,6 +262,7 @@ pub enum WellKnownTrait {
262262
Unpin,
263263
CoerceUnsized,
264264
DiscriminantKind,
265+
Generator,
265266
}
266267

267268
chalk_ir::const_visit!(WellKnownTrait);

chalk-solve/src/wf.rs

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -426,7 +426,8 @@ where
426426
| WellKnownTrait::FnMut
427427
| WellKnownTrait::Unsize
428428
| WellKnownTrait::Sized
429-
| WellKnownTrait::DiscriminantKind => false,
429+
| WellKnownTrait::DiscriminantKind
430+
| WellKnownTrait::Generator => false,
430431
};
431432

432433
if is_legal {

tests/test/generators.rs

Lines changed: 39 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,11 @@ fn generator_test() {
66
program {
77
#[auto] trait Send { }
88

9+
#[lang(generator)]
10+
trait Generator<R> {
11+
type Yield;
12+
type Return;
13+
}
914

1015
struct StructOne {}
1116
struct NotSend {}
@@ -37,6 +42,10 @@ fn generator_test() {
3742
witnesses []
3843
}
3944

45+
generator gen_with_types<U>[resume = U, yield = StructOne] -> NotSend {
46+
upvars []
47+
witnesses []
48+
}
4049
}
4150

4251
goal {
@@ -51,6 +60,36 @@ fn generator_test() {
5160
"Unique"
5261
}
5362

63+
goal {
64+
empty_gen: Generator<()>
65+
} yields {
66+
"Unique"
67+
}
68+
69+
goal {
70+
forall<T> {
71+
gen_with_types<T>: Generator<T>
72+
}
73+
} yields {
74+
"Unique"
75+
}
76+
77+
goal {
78+
forall<T> {
79+
Normalize(<gen_with_types<T> as Generator<T>>::Yield -> StructOne)
80+
}
81+
} yields {
82+
"Unique"
83+
}
84+
85+
goal {
86+
forall<T> {
87+
Normalize(<gen_with_types<T> as Generator<T>>::Return -> NotSend)
88+
}
89+
} yields {
90+
"Unique"
91+
}
92+
5493
goal {
5594
forall<T> {
5695
upvar_lifetime_restrict<T>: Send

0 commit comments

Comments
 (0)