make export_mmp[_proof_tree] public

src/database.rs

@@ -565,7 +565,8 @@ impl Database {
         self.verify_result()
     }
 
-    /// Calculates and returns verification information for the database.
+    /// Returns verification information for the database.
+    /// Panics if [`Database::verify_pass`] was not previously called.
     ///
     /// This is an optimized verifier which returns no useful information other
     /// than error diagnostics.  It does not save any parsed proof data.

src/export.rs

@@ -1,16 +1,13 @@
 //! Export support for mmj2 proof files.
 
 use crate::diag::Diagnostic;
-use crate::nameck::Nameset;
 use crate::parser::as_str;
 use crate::parser::StatementRef;
 use crate::parser::StatementType;
 use crate::parser::TokenRef;
 use crate::proof::ProofStyle;
 use crate::proof::ProofTreeArray;
 use crate::proof::ProofTreePrinter;
-use crate::scopeck::ScopeResult;
-use crate::segment_set::SegmentSet;
 use crate::Database;
 use regex::Regex;
 use std::error;
@@ -73,139 +70,126 @@ impl Database {
         stmt: StatementRef<'_>,
         out: &mut W,
     ) -> Result<(), ExportError> {
-        let sset = self.parse_result();
-        let nset = self.name_result();
-        let scope = self.scope_result();
-        export_mmp(sset, nset, scope, stmt, out)
-    }
-}
+        let thm_label = stmt.label();
+        writeln!(
+            out,
+            "$( <MM> <PROOF_ASST> THEOREM={}  LOC_AFTER=?\n",
+            as_str(thm_label)
+        )?;
+        if let Some(comment) = stmt.associated_comment() {
+            let mut span = comment.span();
+            span.start += 2;
+            span.end -= 3;
+            let cstr = Regex::new(r"\n +").unwrap().replace_all(
+                as_str(span.as_ref(&comment.segment().segment.buffer)),
+                "\n  ",
+            );
+            writeln!(out, "*{}\n", cstr)?;
+        }
 
-/// Export an mmp file for a given statement.
-pub(crate) fn export_mmp<W: Write>(
-    sset: &SegmentSet,
-    nset: &Nameset,
-    scope: &ScopeResult,
-    stmt: StatementRef<'_>,
-    out: &mut W,
-) -> Result<(), ExportError> {
-    let thm_label = stmt.label();
-    writeln!(
-        out,
-        "$( <MM> <PROOF_ASST> THEOREM={}  LOC_AFTER=?\n",
-        as_str(thm_label)
-    )?;
-    if let Some(comment) = stmt.associated_comment() {
-        let mut span = comment.span();
-        span.start += 2;
-        span.end -= 3;
-        let cstr = Regex::new(r"\n +").unwrap().replace_all(
-            as_str(span.as_ref(&comment.segment().segment.buffer)),
-            "\n  ",
-        );
-        writeln!(out, "*{}\n", cstr)?;
+        let arr = ProofTreeArray::new(self, stmt)?;
+        self.export_mmp_proof_tree(thm_label, &arr, out)
     }
 
-    let arr = ProofTreeArray::new(sset, nset, scope, stmt)?;
-    export_mmp_proof_tree(sset, nset, scope, thm_label, &arr, out)
-}
+    /// Export an mmp file for a given proof tree.
+    pub fn export_mmp_proof_tree<W: Write>(
+        &self,
+        thm_label: &[u8],
+        arr: &ProofTreeArray,
+        out: &mut W,
+    ) -> Result<(), ExportError> {
+        let sset = self.parse_result();
+        let nset = self.name_result();
 
-/// Export an mmp file for a given proof tree.
-fn export_mmp_proof_tree<W: Write>(
-    sset: &SegmentSet,
-    nset: &Nameset,
-    scope: &ScopeResult,
-    thm_label: &[u8],
-    arr: &ProofTreeArray,
-    out: &mut W,
-) -> Result<(), ExportError> {
-    // TODO(Mario): remove hardcoded logical step symbol
-    let provable_tc = b"|-";
-    let provable_tc = nset.lookup_symbol(provable_tc).map(|_| provable_tc);
+        // TODO(Mario): remove hardcoded logical step symbol
+        let provable_tc = b"|-";
+        let provable_tc = nset.lookup_symbol(provable_tc).map(|_| provable_tc);
 
-    // This array maps the proof tree index to 0 for syntax proofs and a 1-based
-    // index for logical steps
-    let mut logical_steps: Vec<usize> = vec![];
-    let mut ix = 0usize;
-    // This is indexed based on the numbering in logical_steps, so
-    // if logical_steps[i] = j+1 then arr.trees[i] corresponds to (i, typecode[i], lines[j])
-    let mut lines: Vec<(usize, TokenRef<'_>, String)> = vec![];
-    for tree in &arr.trees {
-        let stmt = sset.statement(tree.address);
-        let label = stmt.label();
-        let tc = stmt.math_at(0);
-        let logical = provable_tc.map_or(true, |tref| *tref == *tc);
+        // This array maps the proof tree index to 0 for syntax proofs and a 1-based
+        // index for logical steps
+        let mut logical_steps: Vec<usize> = vec![];
+        let mut ix = 0usize;
+        // This is indexed based on the numbering in logical_steps, so
+        // if logical_steps[i] = j+1 then arr.trees[i] corresponds to (i, typecode[i], lines[j])
+        let mut lines: Vec<(usize, TokenRef<'_>, String)> = vec![];
+        for tree in &arr.trees {
+            let stmt = sset.statement(tree.address);
+            let label = stmt.label();
+            let tc = stmt.math_at(0);
+            let logical = provable_tc.map_or(true, |tref| *tref == *tc);
 
-        let cur = logical_steps.len();
-        logical_steps.push(if logical {
-            ix += 1;
-            ix
-        } else {
-            0
-        });
+            let cur = logical_steps.len();
+            logical_steps.push(if logical {
+                ix += 1;
+                ix
+            } else {
+                0
+            });
 
-        // Because a step only references previous steps in the array,
-        // we are clear to start output before finishing the loop
-        if logical {
-            let mut line = match stmt.statement_type() {
-                // Floating will not happen unless we don't recognize the grammar
-                StatementType::Essential | StatementType::Floating => format!("h{}", ix),
-                _ => {
-                    if cur == arr.qed {
-                        "qed".to_string()
-                    } else {
-                        ix.to_string()
+            // Because a step only references previous steps in the array,
+            // we are clear to start output before finishing the loop
+            if logical {
+                let mut line = match stmt.statement_type() {
+                    // Floating will not happen unless we don't recognize the grammar
+                    StatementType::Essential | StatementType::Floating => format!("h{}", ix),
+                    _ => {
+                        if cur == arr.qed {
+                            "qed".to_string()
+                        } else {
+                            ix.to_string()
+                        }
+                    }
+                };
+                let mut delim = ':';
+                for &hyp in &tree.children {
+                    let hix = logical_steps[hyp];
+                    if hix != 0 {
+                        line.push(delim);
+                        delim = ',';
+                        line.push_str(&hix.to_string());
                     }
                 }
-            };
-            let mut delim = ':';
-            for &hyp in &tree.children {
-                let hix = logical_steps[hyp];
-                if hix != 0 {
+                if delim == ':' {
                     line.push(delim);
-                    delim = ',';
-                    line.push_str(&hix.to_string());
                 }
+                line.push(':');
+                line.push_str(str::from_utf8(label).unwrap());
+                line.push(' ');
+                lines.push((cur, tc, line));
             }
-            if delim == ':' {
-                line.push(delim);
-            }
-            line.push(':');
-            line.push_str(str::from_utf8(label).unwrap());
-            line.push(' ');
-            lines.push((cur, tc, line));
         }
-    }
 
-    let indent = arr.indent();
-    let spaces = lines
-        .iter()
-        .map(|&(cur, _, ref line)| line.len() as i16 - indent[cur] as i16)
-        .max()
-        .unwrap() as u16;
-    for &mut (cur, tc, ref mut line) in &mut lines {
-        for _ in 0..(spaces + indent[cur] - line.len() as u16) {
-            line.push(' ')
-        }
-        line.push_str(str::from_utf8(&tc).unwrap());
-        line.push_str(&String::from_utf8_lossy(&arr.exprs[cur]));
-        writeln!(out, "{}", line)?;
-    }
-    writeln!(
-        out,
-        "\n$={}",
-        ProofTreePrinter {
-            sset,
-            nset,
-            scope,
-            thm_label,
-            style: ProofStyle::Compressed,
-            arr,
-            initial_chr: 2,
-            indent: 6,
-            line_width: 79,
+        let indent = arr.indent();
+        let spaces = lines
+            .iter()
+            .map(|&(cur, _, ref line)| line.len() as i16 - indent[cur] as i16)
+            .max()
+            .unwrap() as u16;
+        for &mut (cur, tc, ref mut line) in &mut lines {
+            for _ in 0..(spaces + indent[cur] - line.len() as u16) {
+                line.push(' ')
+            }
+            line.push_str(str::from_utf8(&tc).unwrap());
+            line.push_str(&String::from_utf8_lossy(&arr.exprs[cur]));
+            writeln!(out, "{}", line)?;
         }
-    )?;
+        writeln!(
+            out,
+            "\n$={}",
+            ProofTreePrinter {
+                sset,
+                nset,
+                scope: self.scope_result(),
+                thm_label,
+                style: ProofStyle::Compressed,
+                arr,
+                initial_chr: 2,
+                indent: 6,
+                line_width: 79,
+            }
+        )?;
 
-    writeln!(out, "\n$)")?;
-    Ok(())
+        writeln!(out, "\n$)")?;
+        Ok(())
+    }
 }

src/proof.rs

@@ -11,6 +11,7 @@ use crate::util::new_map;
 use crate::util::HashMap;
 use crate::verify::verify_one;
 use crate::verify::ProofBuilder;
+use crate::Database;
 use std::cmp::max;
 use std::cmp::Ord;
 use std::cmp::Ordering;
@@ -126,14 +127,9 @@ impl ProofTreeArray {
     /// Create a proof tree array from the proof a single $p statement,
     /// returning the result of the given proof builder, or an error if the
     /// proof is faulty
-    pub(crate) fn new(
-        sset: &SegmentSet,
-        nset: &Nameset,
-        scopes: &ScopeResult,
-        stmt: StatementRef<'_>,
-    ) -> Result<ProofTreeArray, Diagnostic> {
+    pub(crate) fn new(db: &Database, stmt: StatementRef<'_>) -> Result<ProofTreeArray, Diagnostic> {
         let mut arr = ProofTreeArray::default();
-        arr.qed = verify_one(sset, nset, scopes, &mut arr, stmt)?;
+        arr.qed = verify_one(db, &mut arr, stmt)?;
         arr.calc_indent();
         Ok(arr)
     }

src/verify.rs

@@ -55,6 +55,7 @@ use crate::util::fast_extend;
 use crate::util::new_map;
 use crate::util::ptr_eq;
 use crate::util::HashMap;
+use crate::Database;
 use std::cmp::Ordering;
 use std::mem;
 use std::ops::Range;
@@ -910,19 +911,17 @@ pub(crate) fn verify(
 /// Parse a single $p statement, returning the result of the given
 /// proof builder, or an error if the proof is faulty
 pub(crate) fn verify_one<P: ProofBuilder>(
-    sset: &SegmentSet,
-    nset: &Nameset,
-    scopes: &ScopeResult,
+    db: &Database,
     builder: &mut P,
     stmt: StatementRef<'_>,
 ) -> result::Result<P::Item, Diagnostic> {
     let dummy_frame = Frame::default();
     let mut state = VerifyState {
         this_seg: stmt.segment(),
-        scoper: ScopeReader::new(scopes),
-        nameset: nset,
+        scoper: ScopeReader::new(db.scope_result()),
+        nameset: db.name_result(),
         builder,
-        order: &sset.order,
+        order: &db.parse_result().order,
         cur_frame: &dummy_frame,
         stack: Vec::new(),
         stack_buffer: Vec::new(),