From d718d047731e3a9bf3347c9a4aaf130634f33646 Mon Sep 17 00:00:00 2001
From: Thierry Arnoux <5831830+tirix@users.noreply.github.com>
Date: Mon, 6 Jan 2025 10:18:20 +0100
Subject: [PATCH] Check for unknown labels in usage commands

---
 metamath-rs/src/axiom_use.rs   | 18 ++++++++++++++++--
 metamath-rs/src/usage_tests.rs |  7 ++++---
 2 files changed, 20 insertions(+), 5 deletions(-)

diff --git a/metamath-rs/src/axiom_use.rs b/metamath-rs/src/axiom_use.rs
index a8bf1e7..f39363e 100644
--- a/metamath-rs/src/axiom_use.rs
+++ b/metamath-rs/src/axiom_use.rs
@@ -52,6 +52,9 @@ impl<'a> UsagePass<'a> {
                 let mut diags = vec![];
                 for cmd in axioms {
                     let axiom = &*cmd.value(buf);
+                    if !axiom.starts_with(b"ax-") {
+                        continue;
+                    }
                     if let Some(index) = self.axioms.iter().position(|&x| x == axiom) {
                         if usage.has_bit(index) {
                             // TODO possibly research the usage "path" leading to this error.
@@ -61,6 +64,8 @@ impl<'a> UsagePass<'a> {
                                 axiom.into(),
                             ));
                         }
+                    } else {
+                        diags.push(Diagnostic::UnknownLabel(cmd.full_span()));
                     }
                 }
                 Err(diags)
@@ -71,9 +76,18 @@ impl<'a> UsagePass<'a> {
 
     /// Verify that all usage declarations are correct.
     fn verify_usage(&'a mut self, sset: &'a SegmentSet) {
+        for sref in sset.segments(..) {
+            for stmt in sref.range(..) {
+                if stmt.statement_type() == StatementType::Axiom && stmt.label().starts_with(b"ax-")
+                {
+                    self.axioms.push(stmt.label());
+                }
+            }
+        }
         for sref in sset.segments(..) {
             let mut j_commands: std::slice::Iter<'_, (i32, (crate::Span, Vec<CommandToken>))> =
                 sref.j_commands.iter();
+            let mut axiom_index = 0;
             for stmt in sref.range(..) {
                 match stmt.statement_type() {
                     StatementType::AdditionalInfoComment => {
@@ -110,8 +124,8 @@ impl<'a> UsagePass<'a> {
                         let label = stmt.label();
                         if label.starts_with(b"ax-") {
                             let mut usage = Bitset::new();
-                            usage.set_bit(self.axioms.len());
-                            self.axioms.push(label);
+                            usage.set_bit(axiom_index);
+                            axiom_index += 1;
                             self.axiom_use_map.insert(label, usage);
                         }
                     }
diff --git a/metamath-rs/src/usage_tests.rs b/metamath-rs/src/usage_tests.rs
index cb53d0e..4b3ad9f 100644
--- a/metamath-rs/src/usage_tests.rs
+++ b/metamath-rs/src/usage_tests.rs
@@ -1,4 +1,4 @@
-use crate::diag::Diagnostic::UsageViolation;
+use crate::diag::Diagnostic::{UnknownLabel, UsageViolation};
 use crate::grammar_tests::mkdb;
 use assert_matches::assert_matches;
 
@@ -9,7 +9,7 @@ ax-1 $a |- > a $.
 thm1 $p |- > a $= wa ax-1 $.
 $( $j usage 'thm1' avoids 'ax-1'; $)
 thm2 $p |- > a $= ( ax-1 ) AB $.
-$( $j usage 'thm2' avoids 'ax-1'; $)
+$( $j usage 'thm2' avoids 'ax-1' 'ax-unknown'; $)
 ";
 
 #[test]
@@ -19,7 +19,8 @@ fn test_usage() {
     let usage = db.verify_usage_pass();
     let diags = usage.diagnostics();
 
-    assert_eq!(diags.len(), 2);
+    assert_eq!(diags.len(), 3);
     assert_matches!(diags[0], (_, UsageViolation(..)));
     assert_matches!(diags[1], (_, UsageViolation(..)));
+    assert_matches!(diags[2], (_, UnknownLabel(..)));
 }