check global dv ordering

metamath-rs/src/lib.rs

@@ -93,6 +93,8 @@ mod parser_tests;
 mod usage_tests;
 #[cfg(test)]
 mod util_tests;
+#[cfg(test)]
+mod verify_tests;
 
 pub use database::Database;
 pub use formula::Formula;

metamath-rs/src/nameck.rs

@@ -105,6 +105,10 @@ where
     }
 }
 
+/// A position in the `dv_info` array.
+#[derive(Debug, Copy, Clone)]
+pub struct DvId(pub u32);
+
 // that which we keep in the hash slot for math symbols
 #[derive(Default, PartialEq, Eq, Debug, Clone)]
 struct SymbolInfo {
@@ -315,6 +319,23 @@ impl Nameset {
         }
     }
 
+    /// Looks up the list of global $d statements before index `idx`.
+    #[inline]
+    #[must_use]
+    pub fn global_dv_before(&self, idx: DvId) -> &[(StatementAddress, Vec<Atom>)] {
+        &self.dv_info[..idx.0 as usize]
+    }
+
+    /// Returns the initial position of the global $d index at the start of segment `id`.
+    #[inline]
+    #[must_use]
+    pub fn global_dv_initial(&self, id: SegmentId) -> DvId {
+        let i = self
+            .dv_info
+            .partition_point(|(addr, _)| self.order.lt(&addr.segment_id, &id));
+        DvId(i as u32)
+    }
+
     /// Given a name which is known to represent a defined atom, get the atom.
     ///
     /// If you don't know about the name, use [`lookup_symbol`](Self::lookup_symbol) instead.

metamath-rs/src/scopeck.rs

@@ -30,7 +30,7 @@
 
 use crate::bit_set::Bitset;
 use crate::diag::Diagnostic;
-use crate::nameck::{Atom, NameReader, NameUsage, Nameset};
+use crate::nameck::{Atom, DvId, NameReader, NameUsage, Nameset};
 use crate::segment::{Comparer, Segment, SegmentOrder, SegmentRef};
 use crate::segment_set::SegmentSet;
 use crate::statement::{
@@ -267,6 +267,9 @@ struct ScopeState<'a> {
     nameset: &'a Nameset,
     /// Name reader, tracks labels and math symbols used in this segment.
     gnames: NameReader<'a>,
+    /// Current position in `nameset.dv_info`; global `$d` statements before this index are
+    /// in effect at this point.
+    global_dv_pos: DvId,
     /// Local `$v` statements in effect at this point.
     local_vars: HashMap<Token, Vec<LocalVarInfo>>,
     /// Local `$f` statements in effect at this point.
@@ -609,7 +612,7 @@ fn construct_full_frame<'a>(
     // any variables added for DV are not mandatory
     iframe.mandatory_count = iframe.var_list.len();
 
-    for (_, vars) in state.gnames.lookup_global_dv() {
+    for (_, vars) in state.nameset.global_dv_before(state.global_dv_pos) {
         scan_dv(&mut iframe, vars)
     }
 
@@ -699,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;
     }
 }
 
@@ -897,6 +902,7 @@ fn scope_check_single(
         order: &sset.order,
         nameset: names,
         gnames: NameReader::new(names),
+        global_dv_pos: names.global_dv_initial(seg.id),
         local_vars: HashMap::default(),
         local_floats: HashMap::default(),
         local_dv: Vec::new(),

metamath-rs/src/verify_tests.rs

@@ -0,0 +1,43 @@
+use crate::{diag::Diagnostic, grammar_tests::mkdb};
+use assert_matches::assert_matches;
+
+#[test]
+fn issue_163() {
+    let mut db = mkdb(
+        b"$c term |- R $.
+        $v x y $.
+        x-term $f term x $.
+        y-term $f term y $.
+
+        R-any $a |- x R y $.
+        R-id $p |- x R x $= x-term x-term R-any $.
+
+        $( The offending $d may come after multiple declarations $)
+        $v z $.
+        z-term $f term z $.
+        padding-lemma $a |- x R x $.
+
+        $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)]
+    );
+}