add test crate items

Author: nikomatsakis

crates/formality-check/src/lib.rs

@@ -5,7 +5,7 @@ use std::{collections::VecDeque, fmt::Debug};
 use anyhow::bail;
 use formality_prove::{Decls, Env};
 use formality_rust::{
-    grammar::{Crate, CrateItem, Program},
+    grammar::{Crate, CrateItem, Program, Test, TestBoundData},
     prove::ToWcs,
 };
 use formality_types::grammar::{Fallible, Substitution, Wcs};
@@ -83,9 +83,16 @@ impl Check<'_> {
             CrateItem::Enum(e) => self.check_adt(&e.to_adt()),
             CrateItem::Fn(f) => self.check_free_fn(f),
             CrateItem::NegTraitImpl(i) => self.check_neg_trait_impl(i),
+            CrateItem::Test(t) => self.check_test(t),
         }
     }
 
+    fn check_test(&self, test: &Test) -> Fallible<()> {
+        let mut env = Env::default();
+        let TestBoundData { assumptions, goals } = env.instantiate_universally(&test.binder);
+        self.prove_goal(&env, assumptions, goals)
+    }
+
     fn prove_goal(
         &self,
         env: &Env,

crates/formality-rust/src/grammar.rs

@@ -64,6 +64,19 @@ pub enum CrateItem {
     NegTraitImpl(NegTraitImpl),
     #[cast]
     Fn(Fn),
+    #[cast]
+    Test(Test),
+}
+
+#[term(test $binder)]
+pub struct Test {
+    pub binder: Binder<TestBoundData>,
+}
+
+#[term($:where $,assumptions { $,goals })]
+pub struct TestBoundData {
+    pub assumptions: Vec<WhereClause>,
+    pub goals: Vec<WhereClause>,
 }
 
 #[term(struct $id $binder)]

crates/formality-rust/src/prove.rs

@@ -326,6 +326,7 @@ impl Crate {
                 CrateItem::TraitImpl(_) => None,
                 CrateItem::NegTraitImpl(_) => None,
                 CrateItem::Fn(_) => None,
+                CrateItem::Test(_) => None,
             })
             .collect()
     }