create main, top-level tests

Author: nikomatsakis

Cargo.lock

@@ -10,6 +10,7 @@ rustc_private=true
 
 [dev-dependencies]
 pretty_assertions = "1.3.0"
+expect-test = "1.4.0"
 
 [dependencies]
 anyhow = "1"

Cargo.toml

@@ -29,8 +29,13 @@ pub fn check_all_crates(program: &Program) -> Fallible<()> {
 }
 
 /// Checks the current crate in the program, assuming all other crates are valid.
-fn check_current_crate(_program: &Program) -> Fallible<()> {
-    todo!()
+fn check_current_crate(program: &Program) -> Fallible<()> {
+    let decls = program.to_prove_decls();
+    Check {
+        program,
+        decls: &decls,
+    }
+    .check()
 }
 
 mod adts;
@@ -100,6 +105,6 @@ impl Check<'_> {
             return Ok(());
         }
 
-        bail!("failed to prove {goal:?} from {assumptions:?}, got {cs:?}")
+        bail!("failed to prove {goal:?} given {assumptions:?}, got {cs:?}")
     }
 }

crates/formality-check/src/lib.rs

@@ -0,0 +1,30 @@
+use clap::Parser;
+use formality_check::check_all_crates;
+use formality_rust::grammar::Program;
+use formality_types::parse::term;
+
+#[derive(Parser, Debug)]
+#[command(author, version, about, long_about = None)]
+struct Args {
+    #[arg(long)]
+    print_rust: bool,
+
+    input_path: String,
+}
+
+pub fn main() -> anyhow::Result<()> {
+    let args = Args::parse();
+    let input: String = std::fs::read_to_string(&args.input_path)?;
+    let program: Program = term(&input);
+
+    if args.print_rust {
+        eprintln!("{:#?}", program);
+    }
+
+    check_all_crates(&program)
+}
+
+pub fn test_program_ok(input: &str) -> anyhow::Result<()> {
+    let program: Program = term(&input);
+    check_all_crates(&program)
+}

src/lib.rs

@@ -1,25 +1,3 @@
-use clap::Parser;
-use formality_check::check_all_crates;
-use formality_rust::grammar::Program;
-use formality_types::parse::term;
-
-#[derive(Parser, Debug)]
-#[command(author, version, about, long_about = None)]
-struct Args {
-    #[arg(long)]
-    print_rust: bool,
-
-    input_path: String,
-}
-
 fn main() -> anyhow::Result<()> {
-    let args = Args::parse();
-    let input: String = std::fs::read_to_string(&args.input_path)?;
-    let program: Program = term(&input);
-
-    if args.print_rust {
-        eprintln!("{:#?}", program);
-    }
-
-    check_all_crates(&program)
+    formality::main()
 }

src/main.rs

@@ -1,7 +1,6 @@
 #![allow(non_snake_case)]
-#![cfg(FIXME)]
 
-use formality_rust::test_program_ok;
+use formality::test_program_ok;
 
 const PROGRAM_BROKEN: &str = "[
     crate Foo {
@@ -24,7 +23,6 @@ const PROGRAM_OK: &str = "[
 ]";
 
 #[test]
-#[ignore]
 fn test_broken() {
     expect_test::expect![[r#"
         Err(
@@ -40,7 +38,6 @@ fn test_broken() {
 }
 
 #[test]
-#[ignore]
 fn test_ok() {
     expect_test::expect![[r#"
         Ok(