create a main function

Author: nikomatsakis

Cargo.lock

@@ -12,10 +12,11 @@ rustc_private=true
 pretty_assertions = "1.3.0"
 
 [dependencies]
+anyhow = "1"
 clap = { version = "4.0.9", features = ["derive"] }
 formality-rust = { version = "0.1.0", path = "crates/formality-rust" }
 formality-types = { version = "0.1.0", path = "crates/formality-types" }
-formality-core = { version = "0.1.0", path = "crates/formality-core" }
+formality-check = { version = "0.1.0", path = "crates/formality-check" }
 
 [workspace]
 members = [
@@ -24,6 +25,5 @@ members = [
     "crates/formality-types",
     "crates/formality-check",
     "crates/formality-rust",
-    "crates/formality-main",
     "crates/formality-prove",
 ]

Cargo.toml

@@ -1,7 +1,7 @@
 use formality_macros::term;
 use formality_types::{
     collections::Set,
-    grammar::{AliasName, AliasTy, Binder, TraitId, TraitRef, Ty, TyData, Wc, Wcs},
+    grammar::{AliasName, AliasTy, Binder, TraitId, TraitRef, Ty, Wc, Wcs},
 };
 
 #[term]
@@ -130,16 +130,6 @@ impl AliasEqDecl {
     pub fn alias_name(&self) -> AliasName {
         self.binder.peek().alias.name.clone()
     }
-
-    /// True if the target of this alias-eq declaration
-    /// is a rigid type.
-    pub fn target_is_rigid(&self) -> bool {
-        if let TyData::RigidTy(_) = self.binder.peek().ty.data() {
-            true
-        } else {
-            false
-        }
-    }
 }
 
 #[term($alias = $ty where $where_clause)]

crates/formality-main/Cargo.toml

@@ -1,30 +1,25 @@
-// use formality_types::grammar::Fallible;
+use clap::Parser;
+use formality_check::check_all_crates;
+use formality_rust::grammar::Program;
+use formality_types::parse::term;
 
-// use clap::Parser;
+#[derive(Parser, Debug)]
+#[command(author, version, about, long_about = None)]
+struct Args {
+    #[arg(long)]
+    print_rust: bool,
 
-// /// Formality test generator: convert Rust programs into redex tests
-// #[derive(Parser, Debug)]
-// #[command(author, version, about, long_about = None)]
-// struct Args {
-//     /// If set, print the racket program to stdout and quit.
-//     /// Otherwise, we will invoke racket.
-//     #[arg(long)]
-//     print: bool,
-
-//     /// If set, generate a test that expects the program not to compile.
-//     #[arg(long)]
-//     fail: bool,
+    input_path: String,
+}
 
-//     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);
 
-// fn main() -> Fallible<()> {
-//     let args = Args::parse();
-//     let input = std::fs::read_to_string(&args.input_path)?;
-//     formality_rust::test_program_ok(&input)?;
-//     Ok(())
-// }
+    if args.print_rust {
+        eprintln!("{:#?}", program);
+    }
 
-fn main() {
-    println!("FIXME");
+    check_all_crates(&program)
 }