From bfdbb4af67eaa1c84569d2e38fe30f1531f7bd7f Mon Sep 17 00:00:00 2001 From: Thierry Arnoux <5831830+tirix@users.noreply.github.com> Date: Sun, 27 Aug 2023 19:15:55 +0200 Subject: [PATCH 1/7] Add a "statement use" option --- src/axiom_use.rs | 33 ++++++++++++++++++++------------- src/main.rs | 25 +++++++++++++++++++++++-- 2 files changed, 43 insertions(+), 15 deletions(-) diff --git a/src/axiom_use.rs b/src/axiom_use.rs index ee2927c..789334b 100644 --- a/src/axiom_use.rs +++ b/src/axiom_use.rs @@ -133,15 +133,26 @@ 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: 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); @@ -149,20 +160,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/main.rs b/src/main.rs index d64887d..f2eb13f 100644 --- a/src/main.rs +++ b/src/main.rs @@ -8,7 +8,7 @@ use metamath_knife::database::{Database, DbOptions}; use metamath_knife::diag::BibError; use metamath_knife::statement::StatementAddress; use metamath_knife::verify_markup::{Bibliography, Bibliography2}; -use metamath_knife::SourceInfo; +use metamath_knife::{as_str, SourceInfo}; use simple_logger::SimpleLogger; use std::fs::File; use std::io::{self, BufWriter}; @@ -20,6 +20,15 @@ fn positive_integer(val: String) -> Result<(), String> { u32::from_str(&val).map(|_| ()).map_err(|e| format!("{e}")) } +fn label_list(val: String) -> Result<(), String> { + val.chars() + .all(|c| { + c == ',' || (c.is_ascii() && c.is_alphanumeric()) || c == '-' || c == '_' || c == '.' + }) + .then_some(()) + .ok_or("Expected list of Metamaths labels".to_string()) +} + fn main() { let app = clap_app!(("smetamath-knife") => (version: crate_version!()) @@ -33,6 +42,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") +takes_value validator(label_list) "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,10 +158,21 @@ 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 stmt_list: Vec<&str> = matches.value_of("stmt_use").unwrap().split(',').collect(); + db.write_stmt_use( + |label| stmt_list.contains(&as_str(label)), + &mut BufWriter::new(io::stdout()), + ) + .unwrap_or_else(|err| diags.push((StatementAddress::default(), err.into()))); + } + let mut count = db .render_diags(diags, |snippet| { println!("{}", DisplayList::from(snippet)); From 27d35586c0e97ce39b65124f5841f0fe703869e7 Mon Sep 17 00:00:00 2001 From: Thierry Arnoux <5831830+tirix@users.noreply.github.com> Date: Mon, 28 Aug 2023 08:46:44 +0200 Subject: [PATCH 2/7] As suggested by @digama0 --- src/lib.rs | 1 + src/main.rs | 10 +++++----- src/parser.rs | 3 ++- 3 files changed, 8 insertions(+), 6 deletions(-) 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 f2eb13f..454a51e 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::{as_str, SourceInfo}; @@ -21,12 +22,11 @@ fn positive_integer(val: String) -> Result<(), String> { } fn label_list(val: String) -> Result<(), String> { - val.chars() - .all(|c| { - c == ',' || (c.is_ascii() && c.is_alphanumeric()) || c == '-' || c == '_' || c == '.' - }) + val.split(',') + .map(str::as_bytes) + .all(is_valid_label) .then_some(()) - .ok_or("Expected list of Metamaths labels".to_string()) + .ok_or("Expected list of labels".to_string()) } fn main() { 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()) From f713c6616ea60798538f30fb640c5a6588dd2463 Mon Sep 17 00:00:00 2001 From: Thierry Arnoux <5831830+tirix@users.noreply.github.com> Date: Mon, 28 Aug 2023 13:46:59 +0200 Subject: [PATCH 3/7] Use two values for the --use-stmt argument One for the file and one for the label list. --- src/main.rs | 33 +++++++++++++++++---------------- 1 file changed, 17 insertions(+), 16 deletions(-) diff --git a/src/main.rs b/src/main.rs index 454a51e..19619c5 100644 --- a/src/main.rs +++ b/src/main.rs @@ -9,7 +9,7 @@ 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::{as_str, SourceInfo}; +use metamath_knife::SourceInfo; use simple_logger::SimpleLogger; use std::fs::File; use std::io::{self, BufWriter}; @@ -21,14 +21,6 @@ fn positive_integer(val: String) -> Result<(), String> { u32::from_str(&val).map(|_| ()).map_err(|e| format!("{e}")) } -fn label_list(val: String) -> Result<(), String> { - val.split(',') - .map(str::as_bytes) - .all(is_valid_label) - .then_some(()) - .ok_or("Expected list of labels".to_string()) -} - fn main() { let app = clap_app!(("smetamath-knife") => (version: crate_version!()) @@ -42,7 +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") +takes_value validator(label_list) "Outputs statements directly or indirectly using the given list of statements") + (@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") @@ -165,12 +157,21 @@ fn main() { } if matches.is_present("stmt_use") { - let stmt_list: Vec<&str> = matches.value_of("stmt_use").unwrap().split(',').collect(); - db.write_stmt_use( - |label| stmt_list.contains(&as_str(label)), - &mut BufWriter::new(io::stdout()), - ) - .unwrap_or_else(|err| diags.push((StatementAddress::default(), err.into()))); + 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) { + eprintln!("Expected list of labels as second argument to --stmt-use"); + std::process::exit(1); + } + 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()))); } let mut count = db From 9225110be608755cb9ea4fb3e2ba51c36d3d999e Mon Sep 17 00:00:00 2001 From: Thierry Arnoux <5831830+tirix@users.noreply.github.com> Date: Mon, 28 Aug 2023 14:12:57 +0200 Subject: [PATCH 4/7] Slightly better error message --- src/main.rs | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/main.rs b/src/main.rs index 19619c5..953d221 100644 --- a/src/main.rs +++ b/src/main.rs @@ -161,8 +161,11 @@ fn main() { 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) { - eprintln!("Expected list of labels as second argument to --stmt-use"); - std::process::exit(1); + 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| { From 4d6701d18cbd917dbbbc9534ec7fc92f9b6bb8df Mon Sep 17 00:00:00 2001 From: tirix <5831830+tirix@users.noreply.github.com> Date: Tue, 29 Aug 2023 00:17:08 +0200 Subject: [PATCH 5/7] Update src/axiom_use.rs Co-authored-by: Mario Carneiro --- src/axiom_use.rs | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/src/axiom_use.rs b/src/axiom_use.rs index 789334b..fac60af 100644 --- a/src/axiom_use.rs +++ b/src/axiom_use.rs @@ -134,13 +134,11 @@ pub(crate) fn verify_usage(sset: &Arc, usage: &mut UsageResult) { impl Database { /// Writes a `stmt_use` file to the given writer. - pub fn write_stmt_use( + pub fn write_stmt_use( &self, - label_test: F, + label_test: impl Fn(&[u8]) -> bool, 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(); From bae1604c82fabc8a59fe12b739f233fb193f77d0 Mon Sep 17 00:00:00 2001 From: tirix <5831830+tirix@users.noreply.github.com> Date: Tue, 29 Aug 2023 00:17:42 +0200 Subject: [PATCH 6/7] Update src/main.rs Co-authored-by: Mario Carneiro --- src/main.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main.rs b/src/main.rs index 953d221..bb5fdd1 100644 --- a/src/main.rs +++ b/src/main.rs @@ -160,7 +160,7 @@ fn main() { 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) { + 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, From eba31bade5d4ee27af20a52c760ad65f651bc095 Mon Sep 17 00:00:00 2001 From: Thierry Arnoux <5831830+tirix@users.noreply.github.com> Date: Tue, 29 Aug 2023 06:38:36 +0200 Subject: [PATCH 7/7] Format --- src/axiom_use.rs | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/axiom_use.rs b/src/axiom_use.rs index fac60af..e1a76a9 100644 --- a/src/axiom_use.rs +++ b/src/axiom_use.rs @@ -138,8 +138,7 @@ impl Database { &self, label_test: impl Fn(&[u8]) -> bool, out: &mut impl std::io::Write, - ) -> Result<(), std::io::Error> - { + ) -> Result<(), std::io::Error> { time(&self.options.clone(), "stmt_use", || { let mut stmt_use_map = HashMap::default(); let mut stmt_list = vec![];