--verify-parse-stmt does nothing (#171)

metamath · Oct 28, 2024 · 5268bcf · 5268bcf
1 parent 5908b0b
commit 5268bcf
Show file tree

Hide file tree

Showing 3 changed files with 16 additions and 11 deletions.
diff --git a/metamath-knife/src/main.rs b/metamath-knife/src/main.rs
@@ -161,11 +161,6 @@ fn main() {
             db.typesetting_pass();
         }
 
-        if cli.verify_parse_stmt {
-            db.stmt_parse_pass();
-            db.verify_parse_stmt();
-        }
-
         if cli.verify_usage {
             db.verify_usage_pass();
         }
@@ -225,6 +220,14 @@ fn main() {
             .render_diags(diags, |msg| println!("{}", r.render(msg)))
             .len();
 
+        if cli.verify_parse_stmt {
+            db.stmt_parse_pass();
+            let diags = db.verify_parse_stmt();
+            count += db
+                .render_diags(diags, |msg| println!("{}", r.render(msg)))
+                .len();
+        }
+
         #[cfg(feature = "verify_markup")]
         if cli.verify_markup {
             use metamath_rs::diag::BibError;

diff --git a/metamath-rs/src/database.rs b/metamath-rs/src/database.rs
@@ -958,9 +958,10 @@ impl Database {
 
     /// Verify that printing the formulas of this database gives back the original formulas.
     /// Requires: [`Database::name_pass`], [`Database::stmt_parse_pass`]
-    pub fn verify_parse_stmt(&self) {
+    #[must_use]
+    pub fn verify_parse_stmt(&self) -> Vec<(StatementAddress, Diagnostic)> {
         time(&self.options, "verify_parse_stmt", || {
-            drop(self.stmt_parse_result().verify(self));
+            self.stmt_parse_result().verify(self)
         })
     }
 

diff --git a/metamath-rs/src/grammar.rs b/metamath-rs/src/grammar.rs
@@ -1705,13 +1705,14 @@ impl StmtParse {
 
     /// Check that printing parsed statements gives back the original formulas
     // TODO(tirix): this could be parallelized
-    pub(crate) fn verify(&self, db: &Database) -> Result<(), (StatementAddress, Diagnostic)> {
+    pub(crate) fn verify(&self, db: &Database) -> Vec<(StatementAddress, Diagnostic)> {
         let sset = db.parse_result();
         let nset = db.name_result();
+        let mut diags = vec![];
         for sps in self.segments.values() {
             for (&sa, formula) in &sps.formulas {
                 let sref = sset.statement(sa);
-                let math_iter = sref.math_iter().flat_map(|token| {
+                let math_iter = sref.math_iter().skip(1).flat_map(|token| {
                     nset.lookup_symbol(token.slice)
                         .ok_or_else(|| {
                             (
@@ -1723,11 +1724,11 @@ impl StmtParse {
                 });
                 let fmla_iter = formula.as_ref(db).iter();
                 if math_iter.ne(fmla_iter) {
-                    return Err((sa, Diagnostic::FormulaVerificationFailed));
+                    diags.push((sa, Diagnostic::FormulaVerificationFailed));
                 }
             }
         }
-        Ok(())
+        diags
     }
 
     /// Writes down all formulas