Skip to content

Commit 13aa9d3

Browse files
authored
Merge pull request #494 from Aaron1011/feature/fn-once
Add FnOnce trait, and provide impl for Function type
2 parents 4dba5a5 + 1f6ea3a commit 13aa9d3

File tree

11 files changed

+361
-25
lines changed

11 files changed

+361
-25
lines changed

book/src/clauses/well_known_traits.md

+3-3
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,7 @@ Some common examples of auto traits are `Send` and `Sync`.
2828
[coinductive_section]: ../engine/logic/coinduction.html#coinduction-and-refinement-strands
2929

3030
# Current state
31-
| Type | Copy | Clone | Sized | Unsize | Drop | Fn | Unpin | Generator | auto traits |
31+
| Type | Copy | Clone | Sized | Unsize | Drop | FnOnce/FnMut/Fn | Unpin | Generator | auto traits |
3232
| --- | --- | --- | --- | --- | --- | --- | --- | --- | --- |
3333
| tuple types ||||||||||
3434
| structs ||||||||||
@@ -37,7 +37,7 @@ Some common examples of auto traits are `Send` and `Sync`.
3737
| never type | 📚 | 📚 ||||||||
3838
| trait objects ||||||||||
3939
| functions defs ||||||||||
40-
| functions ptrs |||||| ||||
40+
| functions ptrs |||||| ||||
4141
| raw ptrs | 📚 | 📚 ||||||||
4242
| immutable refs | 📚 | 📚 ||||||||
4343
| mutable refs ||||||||||
@@ -55,4 +55,4 @@ legend:
5555
📚 - implementation provided in libcore
5656
❌ - not implemented
5757

58-
❌ after a type name means that type is not yet in chalk
58+
❌ after a type name means that type is not yet in chalk

chalk-integration/src/lowering.rs

+10-5
Original file line numberDiff line numberDiff line change
@@ -1394,18 +1394,20 @@ impl LowerTy for Ty {
13941394

13951395
Ty::ForAll {
13961396
ref lifetime_names,
1397-
ref ty,
1397+
ref types,
13981398
} => {
13991399
let quantified_env = env.introduce(lifetime_names.iter().map(|id| {
14001400
chalk_ir::WithKind::new(chalk_ir::VariableKind::Lifetime, id.str.clone())
14011401
}))?;
14021402

1403+
let mut lowered_tys = Vec::with_capacity(types.len());
1404+
for ty in types {
1405+
lowered_tys.push(ty.lower(&quantified_env)?.cast(interner));
1406+
}
1407+
14031408
let function = chalk_ir::Fn {
14041409
num_binders: lifetime_names.len(),
1405-
substitution: Substitution::from(
1406-
interner,
1407-
Some(ty.lower(&quantified_env)?.cast(interner)),
1408-
),
1410+
substitution: Substitution::from(interner, lowered_tys),
14091411
};
14101412
Ok(chalk_ir::TyData::Function(function).intern(interner))
14111413
}
@@ -1822,6 +1824,9 @@ impl LowerWellKnownTrait for WellKnownTrait {
18221824
Self::Copy => rust_ir::WellKnownTrait::Copy,
18231825
Self::Clone => rust_ir::WellKnownTrait::Clone,
18241826
Self::Drop => rust_ir::WellKnownTrait::Drop,
1827+
Self::FnOnce => rust_ir::WellKnownTrait::FnOnce,
1828+
Self::FnMut => rust_ir::WellKnownTrait::FnMut,
1829+
Self::Fn => rust_ir::WellKnownTrait::Fn,
18251830
}
18261831
}
18271832
}

chalk-parse/src/ast.rs

+4-1
Original file line numberDiff line numberDiff line change
@@ -68,6 +68,9 @@ pub enum WellKnownTrait {
6868
Copy,
6969
Clone,
7070
Drop,
71+
FnOnce,
72+
FnMut,
73+
Fn,
7174
}
7275

7376
#[derive(Clone, PartialEq, Eq, Debug)]
@@ -210,7 +213,7 @@ pub enum Ty {
210213
},
211214
ForAll {
212215
lifetime_names: Vec<Identifier>,
213-
ty: Box<Ty>,
216+
types: Vec<Box<Ty>>,
214217
},
215218
Tuple {
216219
types: Vec<Box<Ty>>,

chalk-parse/src/parser.lalrpop

+13-4
Original file line numberDiff line numberDiff line change
@@ -51,6 +51,9 @@ WellKnownTrait: WellKnownTrait = {
5151
"#" "[" "lang" "(" "copy" ")" "]" => WellKnownTrait::Copy,
5252
"#" "[" "lang" "(" "clone" ")" "]" => WellKnownTrait::Clone,
5353
"#" "[" "lang" "(" "drop" ")" "]" => WellKnownTrait::Drop,
54+
"#" "[" "lang" "(" "fn_once" ")" "]" => WellKnownTrait::FnOnce,
55+
"#" "[" "lang" "(" "fn_mut" ")" "]" => WellKnownTrait::FnMut,
56+
"#" "[" "lang" "(" "fn" ")" "]" => WellKnownTrait::Fn,
5457
};
5558

5659
StructDefn: StructDefn = {
@@ -220,16 +223,22 @@ pub Ty: Ty = {
220223
};
221224

222225
TyWithoutId: Ty = {
223-
"for" "<" <l:Comma<LifetimeId>> ">" "fn" "(" <t:Ty> ")" => Ty::ForAll {
226+
"for" "<" <l:Comma<LifetimeId>> ">" "fn" "(" <types:Comma<Ty>> ")" <ret_ty:FnReturn?> => Ty::ForAll {
224227
lifetime_names: l,
225-
ty: Box::new(t)
228+
types: types
229+
.into_iter()
230+
.chain(std::iter::once(ret_ty.unwrap_or_else(|| Ty::Tuple { types: Vec::new() })))
231+
.map(Box::new).collect()
226232
},
227233
<ScalarType> => Ty::Scalar { ty: <> },
228234
"str" => Ty::Str,
229235
"!" => Ty::Never,
230-
"fn" "(" <t:Ty> ")" => Ty::ForAll {
236+
"fn" "(" <types:Comma<Ty>> ")" <ret_ty:FnReturn?> => Ty::ForAll {
231237
lifetime_names: vec![],
232-
ty: Box::new(t)
238+
types: types
239+
.into_iter()
240+
.chain(std::iter::once(ret_ty.unwrap_or_else(|| Ty::Tuple { types: Vec::new() })))
241+
.map(Box::new).collect()
233242
},
234243
"dyn" <b:Plus<QuantifiedInlineBound>> "+" <l:Lifetime> => Ty::Dyn {
235244
bounds: b,

chalk-solve/src/clauses.rs

+10-4
Original file line numberDiff line numberDiff line change
@@ -295,7 +295,7 @@ fn program_clauses_that_could_match<I: Interner>(
295295
}
296296

297297
if let Some(well_known) = trait_datum.well_known {
298-
builtin_traits::add_builtin_program_clauses(db, builder, well_known, trait_ref);
298+
builtin_traits::add_builtin_program_clauses(db, builder, well_known, trait_ref)?;
299299
}
300300
}
301301
DomainGoal::Holds(WhereClause::AliasEq(alias_eq)) => match &alias_eq.alias {
@@ -358,15 +358,21 @@ fn program_clauses_that_could_match<I: Interner>(
358358

359359
let trait_datum = db.trait_datum(trait_id);
360360

361+
let self_ty = alias.self_type_parameter(interner);
362+
361363
// Flounder if the self-type is unknown and the trait is non-enumerable.
362364
//
363365
// e.g., Normalize(<?X as Iterator>::Item = u32)
364-
if (alias.self_type_parameter(interner).is_var(interner))
365-
&& trait_datum.is_non_enumerable_trait()
366-
{
366+
if (self_ty.is_var(interner)) && trait_datum.is_non_enumerable_trait() {
367367
return Err(Floundered);
368368
}
369369

370+
if let Some(well_known) = trait_datum.well_known {
371+
builtin_traits::add_builtin_assoc_program_clauses(
372+
db, builder, well_known, self_ty,
373+
)?;
374+
}
375+
370376
push_program_clauses_for_associated_type_values_in_impls_of(
371377
builder,
372378
trait_id,

chalk-solve/src/clauses/builder.rs

+7-2
Original file line numberDiff line numberDiff line change
@@ -114,7 +114,11 @@ impl<'me, I: Interner> ClauseBuilder<'me, I> {
114114
/// The new binders are always pushed onto the end of the internal
115115
/// list of binders; this means that any extant values where were
116116
/// created referencing the *old* list of binders are still valid.
117-
pub fn push_binders<V>(&mut self, binders: &Binders<V>, op: impl FnOnce(&mut Self, V::Result))
117+
pub fn push_binders<R, V>(
118+
&mut self,
119+
binders: &Binders<V>,
120+
op: impl FnOnce(&mut Self, V::Result) -> R,
121+
) -> R
118122
where
119123
V: Fold<I> + HasInterner<Interner = I>,
120124
V::Result: std::fmt::Debug,
@@ -134,10 +138,11 @@ impl<'me, I: Interner> ClauseBuilder<'me, I> {
134138

135139
let value = binders.substitute(self.interner(), &self.parameters[old_len..]);
136140
debug!("push_binders: value={:?}", value);
137-
op(self, value);
141+
let res = op(self, value);
138142

139143
self.binders.truncate(old_len);
140144
self.parameters.truncate(old_len);
145+
res
141146
}
142147

143148
/// Push a single binder, for a type, at the end of the binder

chalk-solve/src/clauses/builtin_traits.rs

+27-4
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,10 @@
11
use super::{builder::ClauseBuilder, generalize};
22
use crate::{Interner, RustIrDatabase, TraitRef, WellKnownTrait};
3-
use chalk_ir::{Substitution, Ty};
3+
use chalk_ir::{Floundered, Substitution, Ty};
44

55
mod clone;
66
mod copy;
7+
mod fn_family;
78
mod sized;
89

910
/// For well known traits we have special hard-coded impls, either as an
@@ -13,7 +14,7 @@ pub fn add_builtin_program_clauses<I: Interner>(
1314
builder: &mut ClauseBuilder<'_, I>,
1415
well_known: WellKnownTrait,
1516
trait_ref: &TraitRef<I>,
16-
) {
17+
) -> Result<(), Floundered> {
1718
// If `trait_ref` contains bound vars, we want to universally quantify them.
1819
// `Generalize` collects them for us.
1920
let generalized = generalize::Generalize::apply(db.interner(), trait_ref);
@@ -25,17 +26,39 @@ pub fn add_builtin_program_clauses<I: Interner>(
2526
if force_impl {
2627
builder.push_fact(trait_ref.clone());
2728
}
28-
return;
29+
return Ok(());
2930
}
3031

3132
match well_known {
3233
WellKnownTrait::Sized => sized::add_sized_program_clauses(db, builder, &trait_ref, ty),
3334
WellKnownTrait::Copy => copy::add_copy_program_clauses(db, builder, &trait_ref, ty),
3435
WellKnownTrait::Clone => clone::add_clone_program_clauses(db, builder, &trait_ref, ty),
36+
WellKnownTrait::FnOnce | WellKnownTrait::FnMut | WellKnownTrait::Fn => {
37+
fn_family::add_fn_trait_program_clauses(db, builder, trait_ref.trait_id, self_ty)?
38+
}
3539
// Drop impls are provided explicitly
3640
WellKnownTrait::Drop => (),
3741
}
38-
});
42+
Ok(())
43+
})
44+
}
45+
46+
/// Like `add_builtin_program_clauses`, but for `DomainGoal::Normalize` involving
47+
/// a projection (e.g. `<fn(u8) as FnOnce<(u8,)>>::Output`)
48+
pub fn add_builtin_assoc_program_clauses<I: Interner>(
49+
db: &dyn RustIrDatabase<I>,
50+
builder: &mut ClauseBuilder<'_, I>,
51+
well_known: WellKnownTrait,
52+
self_ty: Ty<I>,
53+
) -> Result<(), Floundered> {
54+
match well_known {
55+
WellKnownTrait::FnOnce => {
56+
let trait_id = db.well_known_trait_id(well_known).unwrap();
57+
fn_family::add_fn_trait_program_clauses(db, builder, trait_id, self_ty)?;
58+
}
59+
_ => {}
60+
}
61+
Ok(())
3962
}
4063

4164
/// Given a trait ref `T0: Trait` and a list of types `U0..Un`, pushes a clause of the form
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,90 @@
1+
use crate::clauses::ClauseBuilder;
2+
use crate::infer::instantiate::IntoBindersAndValue;
3+
use crate::rust_ir::WellKnownTrait;
4+
use crate::{Interner, RustIrDatabase, TraitRef};
5+
use chalk_ir::{
6+
AliasTy, ApplicationTy, Binders, Floundered, Normalize, ProjectionTy, Substitution, TraitId,
7+
Ty, TyData, TypeName, VariableKinds,
8+
};
9+
10+
/// Handles clauses for FnOnce/FnMut/Fn.
11+
/// If `self_ty` is a function, we push a clause of the form
12+
/// `fn(A1, A2, ..., AN) -> O: FnTrait<(A1, A2, ..., AN)>`, where `FnTrait`
13+
/// is the trait corresponding to `trait_id` (FnOnce/FnMut/Fn)
14+
///
15+
/// If `trait_id` is `FnOnce`, we also push a clause for the output type of the form:
16+
/// `Normalize(<fn(A) -> B as FnOnce<(A,)>>::Output -> B)`
17+
/// We do not add the usual `Implemented(fn(A) -> b as FnOnce<(A,)>` clause
18+
/// as a condition, since we already called `push_fact` with it
19+
pub fn add_fn_trait_program_clauses<I: Interner>(
20+
db: &dyn RustIrDatabase<I>,
21+
builder: &mut ClauseBuilder<'_, I>,
22+
trait_id: TraitId<I>,
23+
self_ty: Ty<I>,
24+
) -> Result<(), Floundered> {
25+
let interner = db.interner();
26+
match self_ty.data(interner) {
27+
TyData::Function(fn_val) => {
28+
let (binders, orig_sub) = fn_val.into_binders_and_value(interner);
29+
let bound_ref = Binders::new(VariableKinds::from(interner, binders), orig_sub);
30+
builder.push_binders(&bound_ref, |builder, orig_sub| {
31+
// The last parameter represents the function return type
32+
let (arg_sub, fn_output_ty) = orig_sub
33+
.parameters(interner)
34+
.split_at(orig_sub.len(interner) - 1);
35+
let arg_sub = Substitution::from(interner, arg_sub);
36+
let fn_output_ty = fn_output_ty[0].assert_ty_ref(interner);
37+
38+
// We are constructing a reference to `FnOnce<Args>`, where
39+
// `Args` is a tuple of the function's argument types
40+
let tupled = Ty::new(
41+
interner,
42+
TyData::Apply(ApplicationTy {
43+
name: TypeName::Tuple(arg_sub.len(interner)),
44+
substitution: arg_sub.clone(),
45+
}),
46+
);
47+
48+
let tupled_sub = Substitution::from(interner, vec![self_ty.clone(), tupled]);
49+
// Given a function type `fn(A1, A2, ..., AN)`, construct a `TraitRef`
50+
// of the form `fn(A1, A2, ..., AN): FnOnce<(A1, A2, ..., AN)>`
51+
let new_trait_ref = TraitRef {
52+
trait_id,
53+
substitution: tupled_sub.clone(),
54+
};
55+
56+
builder.push_fact(new_trait_ref.clone());
57+
58+
if let Some(WellKnownTrait::FnOnce) = db.trait_datum(trait_id).well_known {
59+
//The `Output` type is defined on the `FnOnce`
60+
let fn_once = db.trait_datum(trait_id);
61+
assert_eq!(fn_once.well_known, Some(WellKnownTrait::FnOnce));
62+
let assoc_types = &fn_once.associated_ty_ids;
63+
assert_eq!(
64+
assoc_types.len(),
65+
1,
66+
"FnOnce trait should have exactly one associated type, found {:?}",
67+
assoc_types
68+
);
69+
70+
// Construct `Normalize(<fn(A) -> B as FnOnce<(A,)>>::Output -> B)`
71+
let assoc_output_ty = assoc_types[0];
72+
let proj_ty = ProjectionTy {
73+
associated_ty_id: assoc_output_ty,
74+
substitution: tupled_sub,
75+
};
76+
let normalize = Normalize {
77+
alias: AliasTy::Projection(proj_ty),
78+
ty: fn_output_ty.clone(),
79+
};
80+
81+
builder.push_fact(normalize);
82+
}
83+
});
84+
Ok(())
85+
}
86+
// Function traits are non-enumerable
87+
TyData::InferenceVar(..) | TyData::Alias(..) => Err(Floundered),
88+
_ => Ok(()),
89+
}
90+
}

chalk-solve/src/rust_ir.rs

+6
Original file line numberDiff line numberDiff line change
@@ -216,6 +216,12 @@ pub enum WellKnownTrait {
216216
Copy,
217217
Clone,
218218
Drop,
219+
/// The trait `FnOnce<Args>` - the generic argument `Args` is always a tuple
220+
/// corresponding to the arguments of a function implementing this trait.
221+
/// E.g. `fn(u8, bool): FnOnce<(u8, bool)>`
222+
FnOnce,
223+
FnMut,
224+
Fn,
219225
}
220226

221227
impl<I: Interner> TraitDatum<I> {

chalk-solve/src/wf.rs

+10-2
Original file line numberDiff line numberDiff line change
@@ -471,7 +471,12 @@ impl WfWellKnownGoals {
471471
) -> Option<Goal<I>> {
472472
match db.trait_datum(trait_ref.trait_id).well_known? {
473473
WellKnownTrait::Copy => Self::copy_impl_constraint(db, trait_ref),
474-
WellKnownTrait::Drop | WellKnownTrait::Clone | WellKnownTrait::Sized => None,
474+
WellKnownTrait::Drop
475+
| WellKnownTrait::Clone
476+
| WellKnownTrait::Sized
477+
| WellKnownTrait::FnOnce
478+
| WellKnownTrait::FnMut
479+
| WellKnownTrait::Fn => None,
475480
}
476481
}
477482

@@ -486,7 +491,10 @@ impl WfWellKnownGoals {
486491

487492
match db.trait_datum(impl_datum.trait_id()).well_known? {
488493
// You can't add a manual implementation of Sized
489-
WellKnownTrait::Sized => Some(GoalData::CannotProve(()).intern(interner)),
494+
WellKnownTrait::Sized
495+
| WellKnownTrait::FnOnce
496+
| WellKnownTrait::FnMut
497+
| WellKnownTrait::Fn => Some(GoalData::CannotProve(()).intern(interner)),
490498
WellKnownTrait::Drop => Self::drop_impl_constraint(db, impl_datum),
491499
WellKnownTrait::Copy | WellKnownTrait::Clone => None,
492500
}

0 commit comments

Comments
 (0)