From ae11e6c2b690d76e97f53a245d1319642b2c20b8 Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Thu, 4 Jul 2024 00:28:52 +0200
Subject: [PATCH] check global dv ordering

fixes #163
---
 metamath-rs/src/lib.rs          |  2 ++
 metamath-rs/src/nameck.rs       | 21 +++++++++++++++++++++
 metamath-rs/src/scopeck.rs      |  8 ++++++--
 metamath-rs/src/verify_tests.rs | 25 +++++++++++++++++++++++++
 4 files changed, 54 insertions(+), 2 deletions(-)
 create mode 100644 metamath-rs/src/verify_tests.rs

diff --git a/metamath-rs/src/lib.rs b/metamath-rs/src/lib.rs
index 1118f7c..64bd68d 100644
--- a/metamath-rs/src/lib.rs
+++ b/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;
diff --git a/metamath-rs/src/nameck.rs b/metamath-rs/src/nameck.rs
index d27c666..4a66899 100644
--- a/metamath-rs/src/nameck.rs
+++ b/metamath-rs/src/nameck.rs
@@ -105,6 +105,10 @@ where
     }
 }
 
+/// A position in the `dv_info` array.
+#[derive(Debug, Copy, Clone)]
+pub struct DvId(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.
diff --git a/metamath-rs/src/scopeck.rs b/metamath-rs/src/scopeck.rs
index 24d77b1..eb24ac5 100644
--- a/metamath-rs/src/scopeck.rs
+++ b/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)
     }
 
@@ -897,6 +900,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(),
diff --git a/metamath-rs/src/verify_tests.rs b/metamath-rs/src/verify_tests.rs
new file mode 100644
index 0000000..cb593f6
--- /dev/null
+++ b/metamath-rs/src/verify_tests.rs
@@ -0,0 +1,25 @@
+use crate::grammar_tests::mkdb;
+
+#[test]
+fn issue_163() {
+    const DB: &[u8] = 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 $.
+    ";
+    let mut db = mkdb(DB);
+
+    assert!(db.parse_result().parse_diagnostics().is_empty());
+    assert!(db.verify_pass().diagnostics().is_empty());
+}