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.
rust-lang · Jun 5, 2020 · 91653d0 · 91653d0
1 parent 5eb7b26
commit 91653d0
Show file tree

Hide file tree

Showing 9 changed files with 141 additions and 18 deletions.
diff --git 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
+❌ 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
@@ -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
@@ -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<Identifier>,
-        ty: Box<Ty>,
+        types: Vec<Box<Ty>>,
     },
     Tuple {
         types: Vec<Box<Ty>>,

diff --git 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" "<" <l:Comma<LifetimeId>> ">" "fn" "(" <t:Ty> ")" => Ty::ForAll {
+    "for" "<" <l:Comma<LifetimeId>> ">" "fn" "(" <types:Comma<Ty>> ")" => Ty::ForAll {
         lifetime_names: l,
-        ty: Box::new(t)
+        types: types.into_iter().map(Box::new).collect()
     },
     <ScalarType> => Ty::Scalar { ty: <> },
     "str" => Ty::Str,
     "!" => Ty::Never,
-    "fn" "(" <t:Ty> ")" => Ty::ForAll {
+    "fn" "(" <types:Comma<Ty>> ")" => Ty::ForAll {
         lifetime_names: vec![],
-        ty: Box::new(t)
+        types: types.into_iter().map(Box::new).collect()
     },
     "dyn" <b:Plus<QuantifiedInlineBound>> "+" <l:Lifetime> => Ty::Dyn {
         bounds: b,

diff --git 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<I: Interner>(
             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
@@ -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<I: Interner>(
+    db: &dyn RustIrDatabase<I>,
+    builder: &mut ClauseBuilder<'_, I>,
+    trait_ref: &TraitRef<I>,
+    ty: &TyData<I>,
+) {
+    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<Args>`, 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
@@ -216,6 +216,10 @@ pub enum WellKnownTrait {
     CopyTrait,
     CloneTrait,
     DropTrait,
+    /// The trait `FnOnce<Args>` - 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<I: Interner> TraitDatum<I> {

diff --git a/chalk-solve/src/wf.rs b/chalk-solve/src/wf.rs
@@ -471,9 +471,10 @@ impl WfWellKnownGoals {
     ) -> Option<Goal<I>> {
         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
@@ -1,5 +1,65 @@
 use super::*;
 
+#[test]
+fn function_implement_fn_once() {
+    test! {
+        program {
+            #[lang(fn_once)]
+            trait FnOnce<Args> { }
+        }
+
+        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<T, U> {
+                fn(T, T): FnOnce<(T, U)>
+            }
+        } yields {
+            "No possible solution"
+        }
+
+        goal {
+            forall<T, U> {
+                fn(T, U): FnOnce<(T, T)>
+            }
+        } yields {
+            "No possible solution"
+        }
+    }
+}
+
 #[test]
 fn functions_are_sized() {
     test! {