Add tests for array types

Author: nathanwhit

tests/test/arrays.rs

@@ -0,0 +1,129 @@
+use super::*;
+
+#[test]
+fn arrays_are_sized_if_element_sized() {
+    test! {
+        program {
+            #[lang(sized)]
+            trait Sized { }
+        }
+
+        goal {
+            forall<const N> {
+                [u32; N]: Sized
+            }
+        } yields {
+            "Unique"
+        }
+
+    }
+}
+
+#[test]
+fn arrays_are_not_sized_if_element_not_sized() {
+    test! {
+        program {
+            #[lang(sized)]
+            trait Sized { }
+        }
+
+        goal {
+            forall<const N, T> {
+                [[T]; N]: Sized
+            }
+        } yields {
+            "No possible solution"
+        }
+    }
+}
+
+#[test]
+fn arrays_are_copy_if_element_copy() {
+    test! {
+        program {
+            #[lang(copy)]
+            trait Copy { }
+        }
+
+        goal {
+            forall<const N> {
+                [u32; N]: Copy
+            }
+        } yields {
+            "Unique"
+        }
+    }
+}
+
+#[test]
+fn arrays_are_not_copy_if_element_not_copy() {
+    test! {
+        program {
+            #[lang(copy)]
+            trait Copy { }
+
+            struct Foo { }
+        }
+
+        goal {
+            forall<const N> {
+                [Foo; N]: Copy
+            }
+        } yields {
+            "No possible solution"
+        }
+    }
+}
+
+#[test]
+fn arrays_are_clone_if_element_clone() {
+    test! {
+        program {
+            #[lang(clone)]
+            trait Clone { }
+        }
+
+        goal {
+            forall<const N> {
+                [u32; N]: Clone
+            }
+        } yields {
+            "Unique"
+        }
+    }
+}
+
+#[test]
+fn arrays_are_not_clone_if_element_not_clone() {
+    test! {
+        program {
+            #[lang(clone)]
+            trait Clone { }
+
+            struct Foo { }
+        }
+
+        goal {
+            forall<const N> {
+                [Foo; N]: Clone
+            }
+        } yields {
+            "No possible solution"
+        }
+    }
+}
+
+#[test]
+fn arrays_are_well_formed() {
+    test! {
+        program { }
+
+        goal {
+            forall<const N, T> {
+                WellFormed([T; N])
+            }
+        } yields {
+            "Unique"
+        }
+    }
+}

tests/test/mod.rs

@@ -296,6 +296,7 @@ fn solve_goal(program_text: &str, goals: Vec<(&str, SolverChoice, TestGoal)>) {
     }
 }
 
+mod arrays;
 mod auto_traits;
 mod coherence_goals;
 mod coinduction;