diff --git a/src/axiom_use.rs b/src/axiom_use.rs index ee2927c..e1a76a9 100644 --- a/src/axiom_use.rs +++ b/src/axiom_use.rs @@ -133,15 +133,23 @@ pub(crate) fn verify_usage(sset: &Arc, 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( + &self, + label_test: impl Fn(&[u8]) -> bool, + out: &mut impl std::io::Write, + ) -> Result<(), std::io::Error> { + 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); @@ -149,20 +157,16 @@ impl Database { 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(()) diff --git a/src/lib.rs b/src/lib.rs index b207453..8dddc38 100644 --- a/src/lib.rs +++ b/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; diff --git a/src/main.rs b/src/main.rs index d64887d..bb5fdd1 100644 --- a/src/main.rs +++ b/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.iter().copied().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()))); } diff --git a/src/parser.rs b/src/parser.rs index 84b1613..74b49aa 100644 --- a/src/parser.rs +++ b/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())