From 91653d0f3804b9a017467cc0ef8ef526854eeb5f Mon Sep 17 00:00:00 2001 From: Aaron Hill Date: Fri, 5 Jun 2020 17:44:24 -0400 Subject: [PATCH] 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. --- book/src/clauses/well_known_traits.md | 6 +- chalk-integration/src/lowering.rs | 13 ++-- chalk-parse/src/ast.rs | 3 +- chalk-parse/src/parser.lalrpop | 9 +-- chalk-solve/src/clauses/builtin_traits.rs | 4 ++ chalk-solve/src/clauses/builtin_traits/fn_.rs | 47 +++++++++++++++ chalk-solve/src/rust_ir.rs | 4 ++ chalk-solve/src/wf.rs | 13 ++-- tests/test/functions.rs | 60 +++++++++++++++++++ 9 files changed, 141 insertions(+), 18 deletions(-) create mode 100644 chalk-solve/src/clauses/builtin_traits/fn_.rs diff --git a/book/src/clauses/well_known_traits.md b/book/src/clauses/well_known_traits.md index 33326a9fdf5..c2751957cc6 100644 --- a/book/src/clauses/well_known_traits.md +++ b/book/src/clauses/well_known_traits.md @@ -28,7 +28,7 @@ Some common examples of auto traits are `Send` and `Sync`. [coinductive_section]: ../engine/logic/coinduction.html#coinduction-and-refinement-strands # Current state -| Type | Copy | Clone | Sized | Unsize | Drop | Fn | Unpin | Generator | auto traits | +| Type | Copy | Clone | Sized | Unsize | Drop | FnOnce | Unpin | Generator | auto traits | | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | | tuple types | ✅ | ✅ | ✅ | ✅ | ⚬ | ⚬ | ⚬ | ⚬ | ❌ | | structs | ⚬ | ⚬ | ✅ | ✅ | ⚬ | ⚬ | ⚬ | ⚬ | ✅ | @@ -37,7 +37,7 @@ Some common examples of auto traits are `Send` and `Sync`. | never type | 📚 | 📚 | ✅ | ⚬ | ⚬ | ⚬ | ⚬ | ⚬ | ❌ | | trait objects | ⚬ | ⚬ | ⚬ | ✅ | ⚬ | ⚬ | ⚬ | ⚬ | ⚬ | | functions defs | ✅ | ✅ | ✅ | ⚬ | ⚬ | ❌ | ⚬ | ⚬ | ❌ | -| functions ptrs | ✅ | ✅ | ✅ | ⚬ | ⚬ | ❌ | ⚬ | ⚬ | ❌ | +| functions ptrs | ✅ | ✅ | ✅ | ⚬ | ⚬ | ✅ | ⚬ | ⚬ | ❌ | | raw ptrs | 📚 | 📚 | ✅ | ⚬ | ⚬ | ⚬ | ⚬ | ⚬ | ❌ | | immutable refs | 📚 | 📚 | ✅ | ⚬ | ⚬ | ⚬ | ⚬ | ⚬ | ❌ | | mutable refs | ⚬ | ⚬ | ✅ | ⚬ | ⚬ | ⚬ | ⚬ | ⚬ | ❌ | @@ -55,4 +55,4 @@ legend: 📚 - implementation provided in libcore ❌ - not implemented -❌ after a type name means that type is not yet in chalk \ No newline at end of file +❌ after a type name means that type is not yet in chalk diff --git a/chalk-integration/src/lowering.rs b/chalk-integration/src/lowering.rs index b87dacb8679..0dd7af0a89a 100644 --- a/chalk-integration/src/lowering.rs +++ b/chalk-integration/src/lowering.rs @@ -1394,18 +1394,20 @@ impl LowerTy for Ty { Ty::ForAll { ref lifetime_names, - ref ty, + ref types, } => { let quantified_env = env.introduce(lifetime_names.iter().map(|id| { chalk_ir::WithKind::new(chalk_ir::VariableKind::Lifetime, id.str.clone()) }))?; + let mut lowered_tys = Vec::with_capacity(types.len()); + for ty in types { + lowered_tys.push(ty.lower(&quantified_env)?.cast(interner)); + } + let function = chalk_ir::Fn { num_binders: lifetime_names.len(), - substitution: Substitution::from( - interner, - Some(ty.lower(&quantified_env)?.cast(interner)), - ), + substitution: Substitution::from(interner, lowered_tys), }; Ok(chalk_ir::TyData::Function(function).intern(interner)) } @@ -1822,6 +1824,7 @@ impl LowerWellKnownTrait for WellKnownTrait { Self::CopyTrait => rust_ir::WellKnownTrait::CopyTrait, Self::CloneTrait => rust_ir::WellKnownTrait::CloneTrait, Self::DropTrait => rust_ir::WellKnownTrait::DropTrait, + Self::FnOnceTrait => rust_ir::WellKnownTrait::FnOnceTrait, } } } diff --git a/chalk-parse/src/ast.rs b/chalk-parse/src/ast.rs index 7925f664a58..8622e1b0a84 100644 --- a/chalk-parse/src/ast.rs +++ b/chalk-parse/src/ast.rs @@ -68,6 +68,7 @@ pub enum WellKnownTrait { CopyTrait, CloneTrait, DropTrait, + FnOnceTrait, } #[derive(Clone, PartialEq, Eq, Debug)] @@ -210,7 +211,7 @@ pub enum Ty { }, ForAll { lifetime_names: Vec, - ty: Box, + types: Vec>, }, Tuple { types: Vec>, diff --git a/chalk-parse/src/parser.lalrpop b/chalk-parse/src/parser.lalrpop index 531a8a3f778..7074969183a 100644 --- a/chalk-parse/src/parser.lalrpop +++ b/chalk-parse/src/parser.lalrpop @@ -51,6 +51,7 @@ WellKnownTrait: WellKnownTrait = { "#" "[" "lang" "(" "copy" ")" "]" => WellKnownTrait::CopyTrait, "#" "[" "lang" "(" "clone" ")" "]" => WellKnownTrait::CloneTrait, "#" "[" "lang" "(" "drop" ")" "]" => WellKnownTrait::DropTrait, + "#" "[" "lang" "(" "fn_once" ")" "]" => WellKnownTrait::FnOnceTrait, }; StructDefn: StructDefn = { @@ -220,16 +221,16 @@ pub Ty: Ty = { }; TyWithoutId: Ty = { - "for" "<" > ">" "fn" "(" ")" => Ty::ForAll { + "for" "<" > ">" "fn" "(" > ")" => Ty::ForAll { lifetime_names: l, - ty: Box::new(t) + types: types.into_iter().map(Box::new).collect() }, => Ty::Scalar { ty: <> }, "str" => Ty::Str, "!" => Ty::Never, - "fn" "(" ")" => Ty::ForAll { + "fn" "(" > ")" => Ty::ForAll { lifetime_names: vec![], - ty: Box::new(t) + types: types.into_iter().map(Box::new).collect() }, "dyn" > "+" => Ty::Dyn { bounds: b, diff --git a/chalk-solve/src/clauses/builtin_traits.rs b/chalk-solve/src/clauses/builtin_traits.rs index cb9eac50b11..a4a620125cf 100644 --- a/chalk-solve/src/clauses/builtin_traits.rs +++ b/chalk-solve/src/clauses/builtin_traits.rs @@ -4,6 +4,7 @@ use chalk_ir::{Substitution, Ty}; mod clone; mod copy; +mod fn_; mod sized; /// For well known traits we have special hard-coded impls, either as an @@ -38,6 +39,9 @@ pub fn add_builtin_program_clauses( WellKnownTrait::CloneTrait => { clone::add_clone_program_clauses(db, builder, &trait_ref, ty) } + WellKnownTrait::FnOnceTrait => { + fn_::add_fn_once_program_clauses(db, builder, &trait_ref, ty) + } // Drop impls are provided explicitly WellKnownTrait::DropTrait => (), } diff --git a/chalk-solve/src/clauses/builtin_traits/fn_.rs b/chalk-solve/src/clauses/builtin_traits/fn_.rs new file mode 100644 index 00000000000..ca404579aa7 --- /dev/null +++ b/chalk-solve/src/clauses/builtin_traits/fn_.rs @@ -0,0 +1,47 @@ +use crate::clauses::ClauseBuilder; +use crate::infer::instantiate::IntoBindersAndValue; +use crate::{Interner, RustIrDatabase, TraitRef}; +use chalk_ir::{ApplicationTy, Binders, Substitution, Ty, TyData, TypeName, VariableKinds}; + +pub fn add_fn_once_program_clauses( + db: &dyn RustIrDatabase, + builder: &mut ClauseBuilder<'_, I>, + trait_ref: &TraitRef, + ty: &TyData, +) { + match ty { + TyData::Function(fn_val) => { + let interner = db.interner(); + let (binders, sub) = fn_val.into_binders_and_value(interner); + + // We are constructing a reference to `FnOnce`, where + // `Args` is a tuple of the function's argument types + let tupled = Ty::new( + interner, + TyData::Apply(ApplicationTy { + name: TypeName::Tuple(sub.len(interner)), + substitution: sub.clone(), + }), + ); + + let self_ty = Ty::new(interner, ty); + + let tupled_sub = Substitution::from(interner, vec![self_ty, tupled]); + // Given a function type `fn(A1, A2, ..., AN)`, construct a `TraitRef` + // of the form `fn(A1, A2, ..., AN): FnOnce<(A1, A2, ..., AN)>` + let new_trait_ref = TraitRef { + trait_id: trait_ref.trait_id, + substitution: tupled_sub, + }; + + // Functions types come with a binder, which we push so + // that the `TraitRef` properly references any bound lifetimes + // (e.g. `for<'a> fn(&'a u8): FnOnce<(&'b u8)>`) + let bound_ref = Binders::new(VariableKinds::from(interner, binders), new_trait_ref); + builder.push_binders(&bound_ref, |this, inner_trait| { + this.push_fact(inner_trait); + }) + } + _ => {} + } +} diff --git a/chalk-solve/src/rust_ir.rs b/chalk-solve/src/rust_ir.rs index 4d28d1aad31..efebab921db 100644 --- a/chalk-solve/src/rust_ir.rs +++ b/chalk-solve/src/rust_ir.rs @@ -216,6 +216,10 @@ pub enum WellKnownTrait { CopyTrait, CloneTrait, DropTrait, + /// The trait `FnOnce` - the generic argument `Args` is always a tuple + /// corresponding to the arguments of a function implementing this trait. + /// E.g. `fn(u8, bool): FnOnce<(u8, bool)>` + FnOnceTrait, } impl TraitDatum { diff --git a/chalk-solve/src/wf.rs b/chalk-solve/src/wf.rs index 2bb64a3f617..9811a5f2e0f 100644 --- a/chalk-solve/src/wf.rs +++ b/chalk-solve/src/wf.rs @@ -471,9 +471,10 @@ impl WfWellKnownGoals { ) -> Option> { match db.trait_datum(trait_ref.trait_id).well_known? { WellKnownTrait::CopyTrait => Self::copy_impl_constraint(db, trait_ref), - WellKnownTrait::DropTrait | WellKnownTrait::CloneTrait | WellKnownTrait::SizedTrait => { - None - } + WellKnownTrait::DropTrait + | WellKnownTrait::CloneTrait + | WellKnownTrait::SizedTrait + | WellKnownTrait::FnOnceTrait => None, } } @@ -487,8 +488,10 @@ impl WfWellKnownGoals { let interner = db.interner(); match db.trait_datum(impl_datum.trait_id()).well_known? { - // You can't add a manual implementation of Sized - WellKnownTrait::SizedTrait => Some(GoalData::CannotProve(()).intern(interner)), + // You can't add a manual implementation of Sized or FnOnce + WellKnownTrait::SizedTrait | WellKnownTrait::FnOnceTrait => { + Some(GoalData::CannotProve(()).intern(interner)) + } WellKnownTrait::DropTrait => Self::drop_impl_constraint(db, impl_datum), WellKnownTrait::CopyTrait | WellKnownTrait::CloneTrait => None, } diff --git a/tests/test/functions.rs b/tests/test/functions.rs index 08eab42e6e7..11e7e49d502 100644 --- a/tests/test/functions.rs +++ b/tests/test/functions.rs @@ -1,5 +1,65 @@ use super::*; +#[test] +fn function_implement_fn_once() { + test! { + program { + #[lang(fn_once)] + trait FnOnce { } + } + + goal { + fn(u8): FnOnce<(u8,)> + } yields { + "Unique; substitution [], lifetime constraints []" + } + + goal { + fn(u8, u32): FnOnce<(u8,u32)> + } yields { + "Unique; substitution [], lifetime constraints []" + } + + goal { + fn(i32): FnOnce<(bool,)> + } yields { + "No possible solution" + } + + goal { + forall<'a> { + for<'b> fn(&'b u8): FnOnce<(&'a u8,)> + } + } yields { + "Unique; substitution [], lifetime constraints []" + } + + goal { + forall<'a, 'b> { + for<'c> fn(&'c u8, &'c i32): FnOnce<(&'a u8, &'b i32)> + } + } yields { + "Unique; substitution [], lifetime constraints [InEnvironment { environment: Env([]), goal: '!1_0: '!1_1 }, InEnvironment { environment: Env([]), goal: '!1_1: '!1_0 }]" + } + + goal { + forall { + fn(T, T): FnOnce<(T, U)> + } + } yields { + "No possible solution" + } + + goal { + forall { + fn(T, U): FnOnce<(T, T)> + } + } yields { + "No possible solution" + } + } +} + #[test] fn functions_are_sized() { test! {