Add a "statement use" option

src/axiom_use.rs

@@ -133,36 +133,43 @@ pub(crate) fn verify_usage(sset: &Arc<SegmentSet>, usage: &mut UsageResult) {
 }
 
 impl Database {
-    /// Writes a `axiom_use` file to the given writer.
-    pub fn write_axiom_use(&self, out: &mut impl std::io::Write) -> Result<(), std::io::Error> {
-        time(&self.options.clone(), "axiom_use", || {
-            let mut axiom_use_map = HashMap::default();
-            let mut axioms = vec![];
+    /// Writes a `stmt_use` file to the given writer.
+    pub fn write_stmt_use<F>(
+        &self,
+        label_test: F,
+        out: &mut impl std::io::Write,
+    ) -> Result<(), std::io::Error>
+    where
+        F: Fn(&[u8]) -> bool,
+    {
+        time(&self.options.clone(), "stmt_use", || {
+            let mut stmt_use_map = HashMap::default();
+            let mut stmt_list = vec![];
             for sref in self.statements().filter(|stmt| stmt.is_assertion()) {
                 let label = sref.label();
                 let mut usage = Bitset::new();
-                if sref.statement_type() == StatementType::Provable {
+                if label_test(label) {
+                    usage.set_bit(stmt_list.len());
+                    stmt_list.push(as_str(label));
+                    stmt_use_map.insert(label, usage);
+                } else if sref.statement_type() == StatementType::Provable {
                     let mut i = 1;
                     loop {
                         let tk = sref.proof_slice_at(i);
                         i += 1;
                         if tk == b")" {
                             break;
                         }
-                        if let Some(usage2) = axiom_use_map.get(tk) {
+                        if let Some(usage2) = stmt_use_map.get(tk) {
                             usage |= usage2
                         }
                     }
                     write!(out, "{}:", as_str(label))?;
                     for i in &usage {
-                        write!(out, " {}", axioms[i])?;
+                        write!(out, " {}", stmt_list[i])?;
                     }
                     writeln!(out)?;
-                    axiom_use_map.insert(label, usage);
-                } else if label.starts_with(b"ax-") {
-                    usage.set_bit(axioms.len());
-                    axioms.push(as_str(label));
-                    axiom_use_map.insert(label, usage);
+                    stmt_use_map.insert(label, usage);
                 }
             }
             Ok(())

src/lib.rs

@@ -97,6 +97,7 @@ pub use formula::Formula;
 pub use formula::FormulaRef;
 pub use formula::Label;
 pub use formula::Symbol;
+pub use parser::is_valid_label;
 pub use segment::Comparer;
 pub use segment_set::SourceInfo;
 pub use statement::as_str;

src/main.rs

@@ -6,6 +6,7 @@ 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;
@@ -33,6 +34,7 @@ fn main() {
         (@arg verify_markup: -m --("verify-markup") "Checks comment markup")
         (@arg discouraged: -D --discouraged [FILE] "Regenerates `discouraged` file")
         (@arg axiom_use: -X --("axiom-use") [FILE] "Generate `axiom-use` file")
+        (@arg stmt_use: --("stmt-use") value_names(&["FILE", "LABELS"]) "Outputs statements directly or indirectly using the given list of statements")
         (@arg verify_usage: -u --("verify-usage") "Checks axiom usage")
         (@arg outline: -O --outline "Shows database outline")
         (@arg dump_typesetting: -T --("dump-typesetting") "Dumps typesetting information")
@@ -148,7 +150,30 @@ fn main() {
 
         if matches.is_present("axiom_use") {
             File::create(matches.value_of("axiom_use").unwrap())
-                .and_then(|file| db.write_axiom_use(&mut BufWriter::new(file)))
+                .and_then(|file| {
+                    db.write_stmt_use(|label| label.starts_with(b"ax-"), &mut BufWriter::new(file))
+                })
+                .unwrap_or_else(|err| diags.push((StatementAddress::default(), err.into())));
+        }
+
+        if matches.is_present("stmt_use") {
+            let vals: Vec<_> = matches.values_of("stmt_use").unwrap().collect();
+            let output_file_path = vals[0];
+            let stmt_list: Vec<_> = vals[1].split(',').map(str::as_bytes).collect();
+            if !stmt_list.clone().into_iter().all(is_valid_label) {
+                clap::Error::with_description(
+                    "Expected list of labels as second argument to --stmt-use",
+                    clap::ErrorKind::InvalidValue,
+                )
+                .exit();
+            }
+            File::create(output_file_path)
+                .and_then(|file| {
+                    db.write_stmt_use(
+                        |label| stmt_list.contains(&label),
+                        &mut BufWriter::new(file),
+                    )
+                })
                 .unwrap_or_else(|err| diags.push((StatementAddress::default(), err.into())));
         }
 

src/parser.rs

@@ -759,7 +759,8 @@ fn collect_definitions(seg: &mut Segment) {
 }
 
 /// Metamath spec valid label characters are `[-._a-zA-Z0-9]`
-fn is_valid_label(label: &[u8]) -> bool {
+#[must_use]
+pub fn is_valid_label(label: &[u8]) -> bool {
     label
         .iter()
         .all(|&c| c == b'.' || c == b'-' || c == b'_' || c.is_ascii_alphanumeric())