Merge pull request #443 from nathanwhit/typename-slice

Add slice type to `TypeName`

Author: jackh726

book/src/clauses/well_known_traits.md

@@ -36,8 +36,9 @@ Some common examples of auto traits are `Send` and `Sync`.
 | trait objects   | ⚬    | ⚬    | ⚬     |  ✅    | ⚬    | ⚬   | ⚬      |  ⚬       |    ⚬        |
 | functions ptrs  | ✅    | ✅    | ✅     | ⚬     | ⚬    | ❌   | ⚬      |  ⚬       |    ❌         |
 | raw ptrs        | ✅   |  ✅  |   ✅   |  ⚬    |   ⚬   |  ⚬  |   ⚬    |   ⚬      |      ❌      |
+| references      | ✅   |  ✅  |   ✅   |  ⚬    |   ⚬   |  ⚬  |   ⚬    |   ⚬      |      ❌      |
+| slices          | ⚬     | ⚬    | ⚬     |   ✅    | ⚬   | ⚬   | ⚬      |  ⚬       |    ❌       |
 | arrays❌         | ❌     | ❌    | ❌     | ❌      | ⚬   | ⚬   | ⚬      |  ⚬       |    ❌        |
-| slices❌         | ❌     | ❌    | ⚬     | ❌      | ⚬   | ⚬   | ⚬      |  ⚬       |    ❌       |
 | closures❌       | ❌     | ❌    | ❌     | ⚬      | ⚬   | ❌   | ⚬      |  ⚬       |    ❌        |
 | generators❌     |  ⚬    |  ⚬  | ❌     |  ⚬     | ⚬    | ⚬  | ❌      |   ❌       |    ❌       |
 | gen. witness❌   |  ⚬    |   ⚬  |  ⚬   |   ⚬    |  ⚬   |  ⚬ |  ⚬    |   ⚬       |    ❌       |

chalk-integration/src/lowering.rs

@@ -1211,6 +1211,15 @@ impl LowerTy for Ty {
             })
             .intern(interner)),
 
+            Ty::Slice { ty } => Ok(chalk_ir::TyData::Apply(chalk_ir::ApplicationTy {
+                name: chalk_ir::TypeName::Slice,
+                substitution: chalk_ir::Substitution::from_fallible(
+                    interner,
+                    std::iter::once(ty.lower(env)),
+                )?,
+            })
+            .intern(interner)),
+
             Ty::Raw { mutability, ty } => Ok(chalk_ir::TyData::Apply(chalk_ir::ApplicationTy {
                 name: chalk_ir::TypeName::Raw(ast_mutability_to_chalk_mutability(
                     mutability.clone(),

chalk-ir/src/debug.rs

@@ -144,6 +144,7 @@ impl<I: Interner> Debug for TypeName<I> {
             TypeName::Scalar(scalar) => write!(fmt, "{:?}", scalar),
             TypeName::Tuple(arity) => write!(fmt, "{:?}", arity),
             TypeName::OpaqueType(opaque_ty) => write!(fmt, "!{:?}", opaque_ty),
+            TypeName::Slice => write!(fmt, "{{slice}}"),
             TypeName::Raw(mutability) => write!(fmt, "{:?}", mutability),
             TypeName::Ref(mutability) => write!(fmt, "{:?}", mutability),
             TypeName::Error => write!(fmt, "{{error}}"),

chalk-ir/src/lib.rs

@@ -156,6 +156,9 @@ pub enum TypeName<I: Interner> {
     /// a tuple of the given arity
     Tuple(usize),
 
+    /// a slice type like `[T]`
+    Slice,
+
     /// a raw pointer type like `*const T` or `*mut T`
     Raw(Mutability),
 

chalk-parse/src/ast.rs

@@ -193,6 +193,9 @@ pub enum Ty {
     Scalar {
         ty: ScalarType,
     },
+    Slice {
+        ty: Box<Ty>,
+    },
     Raw {
         mutability: Mutability,
         ty: Box<Ty>,

chalk-parse/src/parser.lalrpop

@@ -208,6 +208,7 @@ TyWithoutFor: Ty = {
     "*" <m: RawMutability> <t:Ty> => Ty::Raw{ mutability: m, ty: Box::new(t) },
     "&" <l: Lifetime> "mut" <t:Ty> => Ty::Ref{ mutability: Mutability::Mut, lifetime: l, ty: Box::new(t) },
     "&" <l: Lifetime> <t:Ty> => Ty::Ref{ mutability: Mutability::Not, lifetime: l, ty: Box::new(t) },
+    "[" <t:Ty> "]" => Ty::Slice { ty: Box::new(t) }, 
 };
 
 ScalarType: ScalarType = {

chalk-solve/src/clauses.rs

@@ -410,6 +410,7 @@ fn match_type_name<I: Interner>(
         TypeName::Tuple(_) => {
             builder.push_fact(WellFormed::Ty(application.clone().intern(interner)))
         }
+        TypeName::Slice => builder.push_fact(WellFormed::Ty(application.clone().intern(interner))),
         TypeName::Raw(_) => builder.push_fact(WellFormed::Ty(application.clone().intern(interner))),
         TypeName::Ref(_) => builder.push_fact(WellFormed::Ty(application.clone().intern(interner))),
     }

tests/lowering/mod.rs

@@ -533,3 +533,29 @@ fn refs() {
         }
     }
 }
+
+#[test]
+fn slices() {
+    lowering_success! {
+        program {
+            trait Foo { }
+
+            impl Foo for [i32] { }
+            impl<T> Foo for [T] { }
+
+            impl Foo for [[i32]] { }
+            impl Foo for [()] { }
+        }
+    }
+
+    lowering_error! {
+        program {
+            trait Foo { }
+            impl Foo for [] {}
+        }
+
+        error_msg {
+            "parse error: UnrecognizedToken { token: (29, Token(30, \"]\"), 30), expected: [\"\\\"&\\\"\", \"\\\"(\\\"\", \"\\\"*\\\"\", \"\\\"<\\\"\", \"\\\"[\\\"\", \"\\\"bool\\\"\", \"\\\"char\\\"\", \"\\\"dyn\\\"\", \"\\\"f32\\\"\", \"\\\"f64\\\"\", \"\\\"fn\\\"\", \"\\\"for\\\"\", \"\\\"i128\\\"\", \"\\\"i16\\\"\", \"\\\"i32\\\"\", \"\\\"i64\\\"\", \"\\\"i8\\\"\", \"\\\"isize\\\"\", \"\\\"u128\\\"\", \"\\\"u16\\\"\", \"\\\"u32\\\"\", \"\\\"u64\\\"\", \"\\\"u8\\\"\", \"\\\"usize\\\"\", \"r#\\\"([A-Za-z]|_)([A-Za-z0-9]|_)*\\\"#\"] }"
+        }
+    }
+}

tests/test/mod.rs

@@ -316,6 +316,7 @@ mod negation;
 mod projection;
 mod refs;
 mod scalars;
+mod slices;
 mod tuples;
 mod unify;
 mod wf_goals;

tests/test/slices.rs

@@ -0,0 +1,63 @@
+use super::*;
+
+#[test]
+fn slices_are_not_sized() {
+    test! {
+        program {
+            #[lang(sized)]
+            trait Sized { }
+        }
+
+        goal {
+            forall<T> { not { [T]: Sized } }
+        } yields {
+            "Unique; substitution [], lifetime constraints []"
+        }
+    }
+}
+
+#[test]
+fn slices_are_well_formed() {
+    test! {
+        program {
+        }
+
+        goal {
+            forall<T> { WellFormed([T]) }
+        } yields {
+            "Unique; substitution [], lifetime constraints []"
+        }
+    }
+}
+
+#[test]
+fn slices_are_not_copy() {
+    test! {
+        program {
+            #[lang(copy)]
+            trait Copy { }
+        }
+
+        goal {
+            forall<T> { not { [T]: Copy } }
+        } yields {
+            "Unique; substitution [], lifetime constraints []"
+        }
+    }
+}
+
+#[test]
+fn slices_are_not_clone() {
+    test! {
+        program {
+            #[lang(clone)]
+            trait Clone { }
+        }
+
+        goal {
+            forall<T> { not { [T]: Clone } }
+        } yields {
+            "Unique; substitution [], lifetime constraints []"
+        }
+    }
+}