improve axiom detection heuristic in axiom_use.rs

metamath · Jun 15, 2024 · 08a19fd · 08a19fd
1 parent 251c70c
commit 08a19fd
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 6 deletions.
diff --git a/metamath-knife/src/main.rs b/metamath-knife/src/main.rs
@@ -10,6 +10,7 @@ use list_stmt::list_statements;
 use metamath_rs::database::{Database, DbOptions};
 use metamath_rs::parser::is_valid_label;
 use metamath_rs::statement::StatementAddress;
+use metamath_rs::StatementType;
 use simple_logger::SimpleLogger;
 use std::fs::File;
 use std::io::{self, stdout, BufWriter};
@@ -155,7 +156,14 @@ fn main() {
         if matches.is_present("axiom_use") {
             File::create(matches.value_of("axiom_use").unwrap())
                 .and_then(|file| {
-                    db.write_stmt_use(|label| label.starts_with(b"ax-"), &mut BufWriter::new(file))
+                    db.write_stmt_use(
+                        |sref| {
+                            sref.statement_type() == StatementType::Axiom
+                                && sref.proof_slice_at(0) == b"|-"
+                                && !sref.label().starts_with(b"df-")
+                        },
+                        &mut BufWriter::new(file),
+                    )
                 })
                 .unwrap_or_else(|err| diags.push((StatementAddress::default(), err.into())));
         }
@@ -174,7 +182,7 @@ fn main() {
             File::create(output_file_path)
                 .and_then(|file| {
                     db.write_stmt_use(
-                        |label| stmt_list.contains(&label),
+                        |sref| stmt_list.contains(&sref.label()),
                         &mut BufWriter::new(file),
                     )
                 })

diff --git a/metamath-rs/src/axiom_use.rs b/metamath-rs/src/axiom_use.rs
@@ -9,8 +9,8 @@ use crate::segment::SegmentRef;
 use crate::segment_set::SegmentSet;
 use crate::statement::{CommandToken, StatementAddress, TokenPtr};
 use crate::util::HashMap;
-use crate::StatementType;
 use crate::{as_str, database::time, Database};
+use crate::{StatementRef, StatementType};
 
 /// Diagnostics issued when checking axiom usage in the Database.
 ///
@@ -108,7 +108,7 @@ impl<'a> UsagePass<'a> {
                     }
                     StatementType::Axiom => {
                         let label = stmt.label();
-                        if label.starts_with(b"ax-") {
+                        if !label.starts_with(b"df-") {
                             let mut usage = Bitset::new();
                             usage.set_bit(self.axioms.len());
                             self.axioms.push(label);
@@ -136,7 +136,7 @@ impl Database {
     /// Writes a `stmt_use` file to the given writer.
     pub fn write_stmt_use(
         &self,
-        label_test: impl Fn(&[u8]) -> bool,
+        test: impl Fn(&StatementRef<'_>) -> bool,
         out: &mut impl std::io::Write,
     ) -> Result<(), std::io::Error> {
         time(&self.options.clone(), "stmt_use", || {
@@ -145,7 +145,7 @@ impl Database {
             for sref in self.statements().filter(|stmt| stmt.is_assertion()) {
                 let label = sref.label();
                 let mut usage = Bitset::new();
-                if label_test(label) {
+                if test(&sref) {
                     usage.set_bit(stmt_list.len());
                     stmt_list.push(as_str(label));
                     stmt_use_map.insert(label, usage);