List stmt

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(())
+}

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,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));