Add function to export theorem dependencies in GraphML format

Cargo.toml

@@ -27,10 +27,12 @@ simple_logger = "1.13"
 
 # Optional dependencies
 dot-writer = { version = "0.1.2", optional = true }
+xml-rs = { version = "0.8.14", optional = true }
 
 [features]
 default = ["annotate-snippets/color"]
 dot = ["dot-writer"]
+xml = ["xml-rs"]
 
 [profile]
 

src/export_deps.rs

@@ -0,0 +1,62 @@
+//! Generation of a `GraphML` file containing all theorem dependencies.
+
+use crate::StatementType;
+use crate::{as_str, database::time, Database};
+use xml::writer::{EmitterConfig, XmlEvent};
+
+use crate::diag::Diagnostic;
+
+impl From<xml::writer::Error> for Diagnostic {
+    fn from(err: xml::writer::Error) -> Diagnostic {
+        Diagnostic::IoError(format!("{err}"))
+    }
+}
+
+impl Database {
+    /// Writes down all dependencies in a `GraphML` file format to the given writer.
+    pub fn export_graphml_deps(&mut self, out: &mut impl std::io::Write) -> Result<(), Diagnostic> {
+        self.name_pass();
+        time(&self.options.clone(), "export_graphml_deps", || {
+            let mut writer = EmitterConfig::new().perform_indent(true).create_writer(out);
+            writer.write(
+                XmlEvent::start_element("graphml")
+                    .attr("xmlns", "http://graphml.graphdrawing.org/xmlns")
+                    .attr("xmlns:xsi", "http://www.w3.org/2001/XMLSchema-instance")
+                    .attr(
+                        "xsi:schemaLocation",
+                        "http://graphml.graphdrawing.org/xmlns/1.0/graphml.xsd",
+                    ),
+            )?;
+            writer.write(XmlEvent::start_element("graph").attr("id", "dependencies"))?;
+            for sref in self.statements().filter(|stmt| stmt.is_assertion()) {
+                let label = sref.label();
+                writer.write(XmlEvent::start_element("node").attr("id", as_str(label)))?;
+                writer.write(XmlEvent::end_element())?; // node
+                if sref.statement_type() == StatementType::Provable {
+                    let mut i = 1;
+                    loop {
+                        let tk = sref.proof_slice_at(i);
+                        i += 1;
+                        if tk == b")" {
+                            break;
+                        }
+                        let sref = self
+                            .statement(tk)
+                            .ok_or_else(|| Diagnostic::UnknownLabel(sref.proof_span(i)))?;
+                        if sref.statement_type() == StatementType::Provable {
+                            writer.write(
+                                XmlEvent::start_element("edge")
+                                    .attr("source", as_str(label))
+                                    .attr("target", as_str(tk)),
+                            )?;
+                            writer.write(XmlEvent::end_element())?;
+                        }
+                    }
+                }
+            }
+            writer.write(XmlEvent::end_element())?; // graph
+            writer.write(XmlEvent::end_element())?; // graphml
+            Ok(())
+        })
+    }
+}

src/lib.rs

@@ -76,6 +76,9 @@ pub mod typesetting;
 pub mod verify;
 pub mod verify_markup;
 
+#[cfg(feature = "xml")]
+pub mod export_deps;
+
 #[cfg(test)]
 mod comment_parser_tests;
 #[cfg(test)]

src/main.rs

@@ -61,6 +61,12 @@ fn main() {
             "Export the database's grammar in Graphviz DOT format for visualization")
     );
 
+    #[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")
+    );
+
     let matches = app.get_matches();
 
     let options = DbOptions {
@@ -127,6 +133,14 @@ fn main() {
                 .unwrap_or_else(|err| diags.push((StatementAddress::default(), err.into())));
         }
 
+        #[cfg(feature = "xml")]
+        if matches.is_present("export_graphml_deps") {
+            File::create(matches.value_of("export_graphml_deps").unwrap())
+                .map_err(|err| err.into())
+                .and_then(|file| db.export_graphml_deps(&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| db.write_axiom_use(&mut BufWriter::new(file)))