Skip to content

Commit 70dd385

Browse files
committed
Add FnOnce trait, and provide impl for Function type
Works towards #363 I've followed the approach taken by rustc, where `FnOnce` has single generic argument: the tupled function parameters (e.g. `fn(u8, bool): FnOnce<(u8, bool)>`). I also extended the grammar to allow functions to take more than one argument. I've left `Fn` and `FnMut` for a separate PR - without a representation of closures in Chalk, they are not very useful.
1 parent 5eb7b26 commit 70dd385

File tree

9 files changed

+133
-13
lines changed

9 files changed

+133
-13
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 | 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

+8-2
Original file line numberDiff line numberDiff line change
@@ -1394,17 +1394,22 @@ 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(),
14051410
substitution: Substitution::from(
14061411
interner,
1407-
Some(ty.lower(&quantified_env)?.cast(interner)),
1412+
lowered_tys
14081413
),
14091414
};
14101415
Ok(chalk_ir::TyData::Function(function).intern(interner))
@@ -1822,6 +1827,7 @@ impl LowerWellKnownTrait for WellKnownTrait {
18221827
Self::CopyTrait => rust_ir::WellKnownTrait::CopyTrait,
18231828
Self::CloneTrait => rust_ir::WellKnownTrait::CloneTrait,
18241829
Self::DropTrait => rust_ir::WellKnownTrait::DropTrait,
1830+
Self::FnOnceTrait => rust_ir::WellKnownTrait::FnOnceTrait
18251831
}
18261832
}
18271833
}

chalk-parse/src/ast.rs

+2-1
Original file line numberDiff line numberDiff line change
@@ -68,6 +68,7 @@ pub enum WellKnownTrait {
6868
CopyTrait,
6969
CloneTrait,
7070
DropTrait,
71+
FnOnceTrait,
7172
}
7273

7374
#[derive(Clone, PartialEq, Eq, Debug)]
@@ -210,7 +211,7 @@ pub enum Ty {
210211
},
211212
ForAll {
212213
lifetime_names: Vec<Identifier>,
213-
ty: Box<Ty>,
214+
types: Vec<Box<Ty>>,
214215
},
215216
Tuple {
216217
types: Vec<Box<Ty>>,

chalk-parse/src/parser.lalrpop

+5-4
Original file line numberDiff line numberDiff line change
@@ -51,6 +51,7 @@ WellKnownTrait: WellKnownTrait = {
5151
"#" "[" "lang" "(" "copy" ")" "]" => WellKnownTrait::CopyTrait,
5252
"#" "[" "lang" "(" "clone" ")" "]" => WellKnownTrait::CloneTrait,
5353
"#" "[" "lang" "(" "drop" ")" "]" => WellKnownTrait::DropTrait,
54+
"#" "[" "lang" "(" "fn_once" ")" "]" => WellKnownTrait::FnOnceTrait,
5455
};
5556

5657
StructDefn: StructDefn = {
@@ -220,16 +221,16 @@ pub Ty: Ty = {
220221
};
221222

222223
TyWithoutId: Ty = {
223-
"for" "<" <l:Comma<LifetimeId>> ">" "fn" "(" <t:Ty> ")" => Ty::ForAll {
224+
"for" "<" <l:Comma<LifetimeId>> ">" "fn" "(" <types:Comma<Ty>> ")" => Ty::ForAll {
224225
lifetime_names: l,
225-
ty: Box::new(t)
226+
types: types.into_iter().map(Box::new).collect()
226227
},
227228
<ScalarType> => Ty::Scalar { ty: <> },
228229
"str" => Ty::Str,
229230
"!" => Ty::Never,
230-
"fn" "(" <t:Ty> ")" => Ty::ForAll {
231+
"fn" "(" <types:Comma<Ty>> ")" => Ty::ForAll {
231232
lifetime_names: vec![],
232-
ty: Box::new(t)
233+
types: types.into_iter().map(Box::new).collect()
233234
},
234235
"dyn" <b:Plus<QuantifiedInlineBound>> "+" <l:Lifetime> => Ty::Dyn {
235236
bounds: b,

chalk-solve/src/clauses/builtin_traits.rs

+4
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ use chalk_ir::{Substitution, Ty};
55
mod clone;
66
mod copy;
77
mod sized;
8+
mod fn_;
89

910
/// For well known traits we have special hard-coded impls, either as an
1011
/// optimization or to enforce special rules for correctness.
@@ -38,6 +39,9 @@ pub fn add_builtin_program_clauses<I: Interner>(
3839
WellKnownTrait::CloneTrait => {
3940
clone::add_clone_program_clauses(db, builder, &trait_ref, ty)
4041
}
42+
WellKnownTrait::FnOnceTrait => {
43+
fn_::add_fn_once_program_clauses(db, builder, &trait_ref, ty)
44+
}
4145
// Drop impls are provided explicitly
4246
WellKnownTrait::DropTrait => (),
4347
}
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,44 @@
1+
use crate::clauses::ClauseBuilder;
2+
use crate::infer::instantiate::IntoBindersAndValue;
3+
use crate::{Interner, RustIrDatabase, TraitRef};
4+
use chalk_ir::{TyData, ApplicationTy, TypeName, Substitution, Ty, Binders, VariableKinds};
5+
6+
pub fn add_fn_once_program_clauses<I: Interner>(
7+
db: &dyn RustIrDatabase<I>,
8+
builder: &mut ClauseBuilder<'_, I>,
9+
trait_ref: &TraitRef<I>,
10+
ty: &TyData<I>,
11+
) {
12+
match ty {
13+
TyData::Function(fn_val) => {
14+
let interner = db.interner();
15+
let (binders, sub) = fn_val.into_binders_and_value(interner);
16+
17+
// We are constructing a reference to `FnOnce<Args>`, where
18+
// `Args` is a tuple of the function's argument types
19+
let tupled = Ty::new(interner, TyData::Apply(ApplicationTy {
20+
name: TypeName::Tuple(sub.len(interner)),
21+
substitution: sub.clone()
22+
}));
23+
24+
let self_ty = Ty::new(interner, ty);
25+
26+
let tupled_sub = Substitution::from(interner, vec![self_ty, tupled]);
27+
// Given a function type `fn(A1, A2, ..., AN)`, construct a `TraitRef`
28+
// of the form `fn(A1, A2, ..., AN): FnOnce<(A1, A2, ..., AN)>`
29+
let new_trait_ref = TraitRef {
30+
trait_id: trait_ref.trait_id,
31+
substitution: tupled_sub
32+
};
33+
34+
// Functions types come with a binder, which we push so
35+
// that the `TraitRef` properly references any bound lifetimes
36+
// (e.g. `for<'a> fn(&'a u8): FnOnce<(&'b u8)>`)
37+
let bound_ref = Binders::new(VariableKinds::from(interner, binders), new_trait_ref);
38+
builder.push_binders(&bound_ref, |this, inner_trait| {
39+
this.push_fact(inner_trait);
40+
})
41+
}
42+
_ => {}
43+
}
44+
}

chalk-solve/src/rust_ir.rs

+4
Original file line numberDiff line numberDiff line change
@@ -216,6 +216,10 @@ pub enum WellKnownTrait {
216216
CopyTrait,
217217
CloneTrait,
218218
DropTrait,
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+
FnOnceTrait,
219223
}
220224

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

chalk-solve/src/wf.rs

+3-3
Original file line numberDiff line numberDiff line change
@@ -471,7 +471,7 @@ impl WfWellKnownGoals {
471471
) -> Option<Goal<I>> {
472472
match db.trait_datum(trait_ref.trait_id).well_known? {
473473
WellKnownTrait::CopyTrait => Self::copy_impl_constraint(db, trait_ref),
474-
WellKnownTrait::DropTrait | WellKnownTrait::CloneTrait | WellKnownTrait::SizedTrait => {
474+
WellKnownTrait::DropTrait | WellKnownTrait::CloneTrait | WellKnownTrait::SizedTrait | WellKnownTrait::FnOnceTrait => {
475475
None
476476
}
477477
}
@@ -487,8 +487,8 @@ impl WfWellKnownGoals {
487487
let interner = db.interner();
488488

489489
match db.trait_datum(impl_datum.trait_id()).well_known? {
490-
// You can't add a manual implementation of Sized
491-
WellKnownTrait::SizedTrait => Some(GoalData::CannotProve(()).intern(interner)),
490+
// You can't add a manual implementation of Sized or FnOnce
491+
WellKnownTrait::SizedTrait | WellKnownTrait::FnOnceTrait => Some(GoalData::CannotProve(()).intern(interner)),
492492
WellKnownTrait::DropTrait => Self::drop_impl_constraint(db, impl_datum),
493493
WellKnownTrait::CopyTrait | WellKnownTrait::CloneTrait => None,
494494
}

tests/test/functions.rs

+60
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,65 @@
11
use super::*;
22

3+
#[test]
4+
fn function_implement_fn_once() {
5+
test! {
6+
program {
7+
#[lang(fn_once)]
8+
trait FnOnce<Args> { }
9+
}
10+
11+
goal {
12+
fn(u8): FnOnce<(u8,)>
13+
} yields {
14+
"Unique; substitution [], lifetime constraints []"
15+
}
16+
17+
goal {
18+
fn(u8, u32): FnOnce<(u8,u32)>
19+
} yields {
20+
"Unique; substitution [], lifetime constraints []"
21+
}
22+
23+
goal {
24+
fn(i32): FnOnce<(bool,)>
25+
} yields {
26+
"No possible solution"
27+
}
28+
29+
goal {
30+
forall<'a> {
31+
for<'b> fn(&'b u8): FnOnce<(&'a u8,)>
32+
}
33+
} yields {
34+
"Unique; substitution [], lifetime constraints []"
35+
}
36+
37+
goal {
38+
forall<'a, 'b> {
39+
for<'c> fn(&'c u8, &'c i32): FnOnce<(&'a u8, &'b i32)>
40+
}
41+
} yields {
42+
"Unique; substitution [], lifetime constraints [InEnvironment { environment: Env([]), goal: '!1_0: '!1_1 }, InEnvironment { environment: Env([]), goal: '!1_1: '!1_0 }]"
43+
}
44+
45+
goal {
46+
forall<T, U> {
47+
fn(T, T): FnOnce<(T, U)>
48+
}
49+
} yields {
50+
"No possible solution"
51+
}
52+
53+
goal {
54+
forall<T, U> {
55+
fn(T, U): FnOnce<(T, T)>
56+
}
57+
} yields {
58+
"No possible solution"
59+
}
60+
}
61+
}
62+
363
#[test]
464
fn functions_are_sized() {
565
test! {

0 commit comments

Comments
 (0)