List statements

metamath-knife/src/list_stmt.rs

@@ -0,0 +1,23 @@
+use metamath_rs::{as_str, Database, StatementType};
+
+pub fn list_statements(
+    db: &Database,
+    label_test: impl Fn(&[u8]) -> bool,
+    out: &mut impl std::io::Write,
+) -> Result<(), std::io::Error> {
+    for stmt in db.statements() {
+        if let StatementType::Axiom | StatementType::Essential | StatementType::Provable =
+            stmt.statement_type()
+        {
+            let label = stmt.label();
+            if label_test(label) {
+                write!(out, "{}:", as_str(label))?;
+                for token in stmt.math_iter() {
+                    write!(out, " {}", as_str(&token))?;
+                }
+                writeln!(out)?;
+            }
+        }
+    }
+    Ok(())
+}

metamath-knife/src/main.rs

@@ -2,8 +2,11 @@
 //! 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 list_stmt::list_statements;
 use metamath_rs::database::{Database, DbOptions};
 use metamath_rs::diag::BibError;
 use metamath_rs::parser::is_valid_label;
@@ -12,7 +15,7 @@ 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,10 @@ fn main() {
                 .unwrap_or_else(|err| diags.push((StatementAddress::default(), err.into())));
         }
 
+        if matches.is_present("list_statements") {
+            _ = list_statements(&db, |_label| true, &mut stdout());
+        }
+
         let mut count = db
             .render_diags(diags, |snippet| {
                 println!("{}", DisplayList::from(snippet));