List stmt

Cargo.toml

@@ -1,42 +1,21 @@
-[package]
+[workspace]
+members = [
+    "metamath-rs",
+    "metamath-knife",
+]
+resolver = "2"
+
+[workspace.package]
 authors = ["David A. Wheeler <dwheeler@dwheeler.com>", "Stefan O'Rear <sorear2@gmail.com>"]
 license = "MIT OR Apache-2.0"
-name = "metamath-knife"
 readme = "README.md"
 version = "0.3.6"
 description = "A parallel and incremental verifier for Metamath databases"
-repository = "/~https://github.com/david-a-wheeler/metamath-knife"
+repository = "/~https://github.com/metamath/metamath-knife"
 keywords = ["theorem", "proving", "verifier", "proof", "assistant"]
 categories = ["command-line-utilities", "development-tools", "mathematics"]
 edition = "2021"
 
-[dependencies]
-lazy_static = "1.4"
-itertools = "0.10"
-filetime = "0.2"
-fnv = "1.0"
-regex = { version = "1.5", default-features = false, features = ["std", "perf"] }
-tinyvec = "1.5"
-log = "0.4"
-annotate-snippets = "0.9"
-typed-arena = "2.0"
-
-# Dependencies for standalone executable, not needed for a library
-clap = "2.33"
-simple_logger = "1.13"
-
-# Optional dependencies
-dot-writer = { version = "0.1.2", optional = true }
-xml-rs = { version = "0.8.14", optional = true }
-
-[dev-dependencies]
-assert_matches = "1.5"
-
-[features]
-default = ["annotate-snippets/color"]
-dot = ["dot-writer"]
-xml = ["xml-rs"]
-
 [profile]
 
 [profile.release]
@@ -49,8 +28,3 @@ codegen-units = 4
 
 [profile.test]
 codegen-units = 4
-
-[[bin]]
-name = "metamath-knife"
-path = "src/main.rs"
-doc = false

metamath-knife/Cargo.toml

@@ -0,0 +1,22 @@
+[package]
+name = "metamath-knife"
+readme = "metamath-knife/README.md"
+description = "A command-line tool for Metamath, including parallel and incremental verifier for Metamath databases"
+version.workspace = true
+authors.workspace = true
+license.workspace = true
+repository.workspace = true
+keywords.workspace = true
+categories.workspace = true
+edition = "2021"
+
+[dependencies]
+clap = "2.33"
+simple_logger = "1.13"
+annotate-snippets = "0.9"
+metamath-rs = { path = "../metamath-rs" }
+
+[[bin]]
+name = "metamath-knife"
+path = "src/main.rs"
+doc = false

metamath-knife/src/list_stmt.rs

@@ -0,0 +1,56 @@
+use metamath_rs::{as_str, Database, StatementRef, StatementType};
+
+pub fn list_statements(
+    db: &Database,
+    label_test: impl Fn(&[u8]) -> bool,
+    out: &mut impl std::io::Write,
+) -> Result<(), std::io::Error> {
+    let separator = "-".repeat(79);
+    let scope = db.scope_result();
+    let name = db.name_result();
+    for stmt in db.statements() {
+        if let StatementType::Axiom | StatementType::Provable = stmt.statement_type() {
+            let label = stmt.label();
+            if label_test(label) {
+                if let Some(frame) = scope.get(label) {
+                    for (ix1, ix2) in &*frame.mandatory_dv {
+                        writeln!(
+                            out,
+                            "$d {} {} $.",
+                            as_str(name.atom_name(frame.var_list[*ix1])),
+                            as_str(name.atom_name(frame.var_list[*ix2]))
+                        )?;
+                    }
+                    for hyp in frame.hypotheses.iter().skip(frame.mandatory_count) {
+                        write_statement(db.statement_by_address(hyp.address()), out)?;
+                    }
+                    write_statement(stmt, out)?;
+                    writeln!(out, "{}", separator)?;
+                }
+            }
+        }
+    }
+    Ok(())
+}
+
+pub fn write_statement(
+    stmt: StatementRef,
+    out: &mut impl std::io::Write,
+) -> Result<(), std::io::Error> {
+    write!(
+        out,
+        "{} ${}",
+        as_str(stmt.label()),
+        match stmt.statement_type() {
+            StatementType::Axiom => "a",
+            StatementType::Essential => "e",
+            StatementType::Provable => "p",
+            _ => "x",
+        }
+    )?;
+    for token in stmt.math_iter() {
+        write!(out, " {}", as_str(&token))?;
+    }
+    writeln!(out)?;
+    Ok(())
+}

src/main.rs → metamath-knife/src/main.rs

@@ -2,17 +2,20 @@
 //! databases.  The entry point for all API operations is in the `database`
 //! module, as is a discussion of the data representation.
 
+mod list_stmt;
+
 use annotate_snippets::display_list::DisplayList;
 use clap::{clap_app, crate_version};
-use metamath_knife::database::{Database, DbOptions};
-use metamath_knife::diag::BibError;
-use metamath_knife::parser::is_valid_label;
-use metamath_knife::statement::StatementAddress;
-use metamath_knife::verify_markup::{Bibliography, Bibliography2};
-use metamath_knife::SourceInfo;
+use list_stmt::list_statements;
+use metamath_rs::database::{Database, DbOptions};
+use metamath_rs::diag::BibError;
+use metamath_rs::parser::is_valid_label;
+use metamath_rs::statement::StatementAddress;
+use metamath_rs::verify_markup::{Bibliography, Bibliography2};
+use metamath_rs::SourceInfo;
 use simple_logger::SimpleLogger;
 use std::fs::File;
-use std::io::{self, BufWriter};
+use std::io::{self, stdout, BufWriter};
 use std::mem;
 use std::str::FromStr;
 use std::sync::Arc;
@@ -46,6 +49,7 @@ fn main() {
             "Checks that printing parsed statements gives back the original formulas")
         (@arg dump_grammar: -G --("dump-grammar") "Dumps the database's grammar")
         (@arg dump_formula: -F --("dump-formula") "Dumps the formulas of this database")
+        (@arg list_statements: -S --("list-statements") "List all statements of this database")
         (@arg debug: --debug
             "Activates debug logs, including for the grammar building and statement parsing")
         (@arg trace_recalc: --("trace-recalc") "Prints segments as they are recalculated")
@@ -177,6 +181,11 @@ fn main() {
                 .unwrap_or_else(|err| diags.push((StatementAddress::default(), err.into())));
         }
 
+        if matches.is_present("list_statements") {
+            db.scope_pass();
+            _ = list_statements(&db, |_label| true, &mut stdout());
+        }
+
         let mut count = db
             .render_diags(diags, |snippet| {
                 println!("{}", DisplayList::from(snippet));

metamath-rs/Cargo.toml

@@ -0,0 +1,34 @@
+[package]
+name = "metamath-rs"
+readme = "metamath-rs/README.md"
+description = "A library manipulating Metamath databases, including a parallel and incremental verifier for Metamath databases"
+version.workspace = true
+authors.workspace = true
+license.workspace = true
+repository.workspace = true
+keywords.workspace = true
+categories.workspace = true
+edition = "2021"
+
+[dependencies]
+lazy_static = "1.4"
+itertools = "0.10"
+filetime = "0.2"
+fnv = "1.0"
+regex = { version = "1.5", default-features = false, features = ["std", "perf"] }
+tinyvec = "1.5"
+log = "0.4"
+annotate-snippets = "0.9"
+typed-arena = "2.0"
+
+# Optional dependencies
+dot-writer = { version = "0.1.2", optional = true }
+xml-rs = { version = "0.8.14", optional = true }
+
+[dev-dependencies]
+assert_matches = "1.5"
+
+[features]
+default = ["annotate-snippets/color"]
+dot = ["dot-writer"]
+xml = ["xml-rs"]

src/grammar.rs → metamath-rs/src/grammar.rs

@@ -139,7 +139,7 @@ impl GrammarTree {
 ///
 /// Example:
 /// ```
-/// use metamath_knife::database::{Database, DbOptions};
+/// use metamath_rs::database::{Database, DbOptions};
 ///
 /// // Setup the required options
 /// let mut options = DbOptions::default();
@@ -1675,7 +1675,7 @@ impl Grammar {
 ///
 /// Example:
 /// ```
-/// use metamath_knife::database::{Database, DbOptions};
+/// use metamath_rs::database::{Database, DbOptions};
 ///
 /// // Setup the required options
 /// let mut options = DbOptions::default();

src/typesetting.rs → metamath-rs/src/typesetting.rs

@@ -1,7 +1,7 @@
 //! The typesetting data.
 //!
 //! This is the result of parsing a `$t` metamath comment, which contains information
-//! used by the metamath website generator. Although `metamath-knife` tries to be
+//! used by the metamath website generator. Although `metamath-rs` tries to be
 //! generic and so it does not itself contain a website generator, this pass can be
 //! used to collect information for generating HTML in the style of
 //! [`metamath.exe`](/~https://github.com/metamath/metamath-exe).