Verify definitions

metamath-knife/src/main.rs

@@ -30,6 +30,7 @@ fn main() {
         (@arg split: --split "Processes files > 1 MiB in multiple segments")
         (@arg timing: --time "Prints milliseconds after each stage")
         (@arg verify: -v --verify "Checks proof validity")
+        (@arg verify_defs: --("verify-defs") "Checks definitions")
         (@arg discouraged: -D --discouraged [FILE] "Regenerates `discouraged` file")
         (@arg axiom_use: -X --("axiom-use") [FILE] "Generate `axiom-use` file")
         (@arg stmt_use: --("stmt-use") value_names(&["FILE", "LABELS"]) "Outputs statements directly or indirectly using the given list of statements")
@@ -66,7 +67,9 @@ fn main() {
     #[cfg(feature = "xml")]
     let app = clap_app!(@app (app)
         (@arg export_graphml_deps: --("export-graphml-deps") [FILE]
-        "Exports all theorem dependencies in the GraphML file format")
+            "Exports all theorem dependencies in the GraphML file format")
+        (@arg export_graphml_defs: --("export-graphml-defs") [FILE]
+            "Exports all definition dependencies in the GraphML file format")
     );
 
     #[cfg(feature = "verify_markup")]
@@ -84,9 +87,11 @@ fn main() {
             || matches.is_present("grammar")
             || matches.is_present("parse_stmt")
             || matches.is_present("verify_parse_stmt")
+            || matches.is_present("verify_defs")
             || matches.is_present("export_grammar_dot")
             || matches.is_present("dump_grammar")
-            || matches.is_present("dump_formula"),
+            || matches.is_present("dump_formula")
+            || matches.is_present("export_graphml_defs"),
         jobs: usize::from_str(matches.value_of("jobs").unwrap_or("1"))
             .expect("validator should check this"),
     };
@@ -132,6 +137,10 @@ fn main() {
             db.verify_parse_stmt();
         }
 
+        if matches.is_present("verify_defs") {
+            db.definitions_pass();
+        }
+
         if matches.is_present("verify_usage") {
             db.verify_usage_pass();
         }
@@ -152,6 +161,14 @@ fn main() {
                 .unwrap_or_else(|diag| diags.push((StatementAddress::default(), diag)));
         }
 
+        #[cfg(feature = "xml")]
+        if matches.is_present("export_graphml_defs") {
+            File::create(matches.value_of("export_graphml_defs").unwrap())
+                .map_err(|err| err.into())
+                .and_then(|file| db.export_graphml_defs(&mut BufWriter::new(file)))
+                .unwrap_or_else(|diag| diags.push((StatementAddress::default(), diag)));
+        }
+
         if matches.is_present("axiom_use") {
             File::create(matches.value_of("axiom_use").unwrap())
                 .and_then(|file| {

metamath-rs/src/bit_set.rs

@@ -67,10 +67,7 @@ impl Bitset {
     }
 
     fn tail_mut(&mut self) -> &mut Vec<usize> {
-        if self.tail.is_none() {
-            self.tail = Some(Box::default());
-        }
-        self.tail.as_mut().unwrap()
+        self.tail.get_or_insert_with(Box::default)
     }
 
     /// Adds a single bit to a set.
@@ -87,6 +84,28 @@ impl Bitset {
         }
     }
 
+    /// Removes a single bit from a set.
+    pub fn unset_bit(&mut self, bit: usize) {
+        if bit < bits_per_word() {
+            self.head &= !(1 << bit);
+        } else if let Some(tail) = &mut self.tail {
+            let mut word = bit / bits_per_word() - 1;
+            if word < tail.len() {
+                tail[word] &= !(1 << (bit & (bits_per_word() - 1)));
+                if word + 1 == tail.len() && tail[word] == 0 {
+                    while tail[word] == 0 {
+                        if word == 0 {
+                            self.tail = None;
+                            return;
+                        }
+                        word -= 1;
+                    }
+                    tail.truncate(word + 1);
+                }
+            }
+        }
+    }
+
     /// Tests a set for a specific bit.
     pub fn has_bit(&self, bit: usize) -> bool {
         if bit < bits_per_word() {
@@ -120,6 +139,21 @@ impl Bitset {
         }
     }
 
+    pub fn is_subset_of(&self, rhs: &Self) -> bool {
+        !rhs.head & self.head == 0
+            && match &self.tail {
+                Some(ltail) => (0..ltail.len()).all(|i| {
+                    let rtail_i = rhs
+                        .tail
+                        .as_ref()
+                        .and_then(|rtail| rtail.get(i).copied())
+                        .unwrap_or(0);
+                    !rtail_i & ltail[i] == 0
+                }),
+                _ => true,
+            }
+    }
+
     /// Returns true if this bitset has no bits set.
     pub fn is_empty(&self) -> bool {
         self.head == 0

metamath-rs/src/database.rs

@@ -99,6 +99,7 @@
 
 use crate::as_str;
 use crate::axiom_use::UsageResult;
+use crate::defck::DefResult;
 use crate::diag;
 use crate::diag::Diagnostic;
 use crate::export;
@@ -404,6 +405,7 @@
     outline: Option<Arc<Outline>>,
     grammar: Option<Arc<Grammar>>,
     stmt_parse: Option<Arc<StmtParse>>,
+    definitions: Option<Arc<DefResult>>,
 }
 
 impl Default for Database {
@@ -434,6 +436,7 @@
             Arc::make_mut(&mut self.segments).clear();
             self.typesetting = None;
             self.outline = None;
+            self.definitions = None;
         });
     }
 }
@@ -458,6 +461,7 @@
             outline: None,
             grammar: None,
             stmt_parse: None,
+            definitions: None,
             prev_nameset: None,
             prev_scopes: None,
             prev_verify: None,
@@ -503,6 +507,7 @@
             self.typesetting = None;
             self.outline = None;
             self.grammar = None;
+            self.definitions = None;
         });
     }
 
@@ -776,6 +781,38 @@
         )
     }
 
+    /// Checks all definitions soundness.
+    pub fn definitions_pass(&mut self) -> &Arc<DefResult> {
+        if self.definitions.is_none() {
+            self.stmt_parse_pass();
+            time(&self.options.clone(), "defck_pass", || {
+                let parse = self.parse_result();
+                let mut definitions = DefResult::default();
+                self.verify_definitions(parse, &mut definitions);
+                self.definitions = Some(Arc::new(definitions));
+            })
+        }
+        self.definitions_result()
+    }
+
+    /// Returns the results of the definition check pass.
+    /// Returns `None` if [`Database::definitions_pass`] was not previously called.
+    #[inline]
+    #[must_use]
+    pub const fn try_definitions_result(&self) -> Option<&Arc<DefResult>> {
+        self.definitions.as_ref()
+    }
+
+    /// Returns the results of the definition check pass.
+    /// Panics if [`Database::definition_pass`] was not previously called.
+    #[inline]
+    #[must_use]
+    pub fn definitions_result(&self) -> &Arc<DefResult> {
+        self.try_definitions_result().expect(
+            "The database has not run `stmt_parse_pass()`. Please ensure it is run before calling depending methods."
+        )
+    }
+
     /// A getter method which does not build the outline.
     #[inline]
     #[must_use]
@@ -1016,6 +1053,9 @@
         if let Some(pass) = self.try_typesetting_result() {
             diags.extend_from_slice(&pass.diagnostics)
         }
+        if let Some(pass) = self.try_definitions_result() {
+            diags.extend(pass.diagnostics())
+        }
         diags
     }