add negative test

metamath-rs/src/nameck.rs

@@ -107,7 +107,7 @@ where
 
 /// A position in the `dv_info` array.
 #[derive(Debug, Copy, Clone)]
-pub struct DvId(u32);
+pub struct DvId(pub u32);
 
 // that which we keep in the hash slot for math symbols
 #[derive(Default, PartialEq, Eq, Debug, Clone)]

metamath-rs/src/scopeck.rs

@@ -702,20 +702,22 @@ fn scope_check_dv<'a>(state: &mut ScopeState<'a>, sref: StatementRef<'a>) {
         }
     }
 
-    if bad {
-        return;
-    }
-
     // we need to do validity checking on global $d _somewhere_, and that
     // happens to be here, but the knowledge of the $d is handled by nameck
     // in that case and we need to not duplicate it
     if sref.in_group() {
-        // record the $d in our local storage, will be deleted in
-        // construct_full_frame when it's no longer in scope
-        state.local_dv.push(LocalDvInfo {
-            valid: sref.scope_range(),
-            vars,
-        });
+        if !bad {
+            // record the $d in our local storage, will be deleted in
+            // construct_full_frame when it's no longer in scope
+            state.local_dv.push(LocalDvInfo {
+                valid: sref.scope_range(),
+                vars,
+            });
+        }
+    } else {
+        // Note, unlike the local case this will use the DV anyway if it has diagnostics...
+        // we have to keep moving the pointer forward or the count will get messed up
+        state.global_dv_pos.0 += 1;
     }
 }
 

metamath-rs/src/verify_tests.rs

@@ -1,9 +1,10 @@
-use crate::grammar_tests::mkdb;
+use crate::{diag::Diagnostic, grammar_tests::mkdb};
+use assert_matches::assert_matches;
 
 #[test]
 fn issue_163() {
-    const DB: &[u8] = b"
-        $c term |- R $.
+    let mut db = mkdb(
+        b"$c term |- R $.
         $v x y $.
         x-term $f term x $.
         y-term $f term y $.
@@ -16,10 +17,27 @@ fn issue_163() {
         z-term $f term z $.
         padding-lemma $a |- x R x $.
         
-        $d x y $.
-    ";
-    let mut db = mkdb(DB);
+        $d x y $.",
+    );
 
     assert!(db.parse_result().parse_diagnostics().is_empty());
     assert!(db.verify_pass().diagnostics().is_empty());
+
+    db = mkdb(
+        b"$c term |- R $.
+        $v x y $.
+        x-term $f term x $.
+        y-term $f term y $.
+        
+        $d x y $.
+
+        R-any $a |- x R y $.
+        R-id $p |- x R x $= x-term x-term R-any $.",
+    );
+
+    assert!(db.parse_result().parse_diagnostics().is_empty());
+    assert_matches!(
+        *db.verify_pass().diagnostics(),
+        [(_, Diagnostic::ProofDvViolation)]
+    );
 }