From bd12dea9436c96161f57494851875d629870a7d9 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Thu, 14 Oct 2021 02:58:08 -0400 Subject: [PATCH 1/9] Misc API changes * DB passes are now separated into `get` and `get_or_insert` style methods. Fixes #24 (not the follow on stuff though) * `SegmentSet` and any function referencing it is now `pub(crate)`. * Implement `FormulaRef` and the display impl. The debug impl is TODO. * Most uses of `&Arc` in parameters are replaced with `&T`, unless cloning is actually required in the body. --- src/database.rs | 219 ++++++++++++++++++++++++------------------- src/diag.rs | 2 +- src/export.rs | 4 +- src/formula.rs | 143 ++++++++++++++++------------ src/formula_tests.rs | 10 +- src/grammar.rs | 79 +++++++--------- src/grammar_tests.rs | 35 ++++--- src/nameck.rs | 2 +- src/outline.rs | 18 ++-- src/parser_tests.rs | 6 +- src/proof.rs | 20 ++-- src/scopeck.rs | 2 +- src/segment_set.rs | 26 ++--- src/tree.rs | 10 +- src/verify.rs | 4 +- 15 files changed, 312 insertions(+), 268 deletions(-) diff --git a/src/database.rs b/src/database.rs index 654a603..223f1f4 100644 --- a/src/database.rs +++ b/src/database.rs @@ -105,7 +105,6 @@ use crate::grammar; use crate::grammar::Grammar; use crate::grammar::StmtParse; use crate::nameck::Nameset; -use crate::outline; use crate::outline::OutlineNode; use crate::parser::StatementRef; use crate::scopeck; @@ -471,26 +470,29 @@ impl Database { /// /// Unlike the other accessors, this is not lazy (subject to change when the /// modification API goes in.) - pub fn parse_result(&mut self) -> &Arc { + pub(crate) fn parse_result(&self) -> &Arc { self.segments.as_ref().unwrap() } /// Calculates and returns the name to definition lookup table. - pub fn name_result(&mut self) -> &Arc { + pub fn name_pass(&mut self) -> &Arc { if self.nameset.is_none() { time(&self.options.clone(), "nameck", || { - if self.prev_nameset.is_none() { - self.prev_nameset = Some(Arc::new(Nameset::new())); - } - let pr = self.parse_result().clone(); - { - let ns = Arc::make_mut(self.prev_nameset.as_mut().unwrap()); - ns.update(&pr); - } - self.nameset = self.prev_nameset.clone(); + let mut ns = self.prev_nameset.take().unwrap_or_default(); + let pr = self.parse_result(); + Arc::make_mut(&mut ns).update(pr); + self.prev_nameset = Some(ns.clone()); + self.nameset = Some(ns); }); } + self.name_result() + } + + /// Returns the name to definition lookup table. + /// Panics if [`Database::name_pass`] was not previously called. + #[must_use] + pub fn name_result(&self) -> &Arc { self.nameset.as_ref().unwrap() } @@ -499,24 +501,28 @@ impl Database { /// /// All logical properties of the database (as opposed to surface syntactic /// properties) can be obtained from this object. - pub fn scope_result(&mut self) -> &Arc { + pub fn scope_pass(&mut self) -> &Arc { if self.scopes.is_none() { - self.name_result(); + self.name_pass(); time(&self.options.clone(), "scopeck", || { - if self.prev_scopes.is_none() { - self.prev_scopes = Some(Arc::new(ScopeResult::default())); - } - - let parse = self.parse_result().clone(); - let name = self.name_result().clone(); - { - let ns = Arc::make_mut(self.prev_scopes.as_mut().unwrap()); - scopeck::scope_check(ns, &parse, &name); - } - self.scopes = self.prev_scopes.clone(); + let mut sc = self.prev_scopes.take().unwrap_or_default(); + let parse = self.parse_result(); + let name = self.name_result(); + scopeck::scope_check(Arc::make_mut(&mut sc), parse, name); + self.prev_scopes = Some(sc.clone()); + self.scopes = Some(sc); }); } + self.scope_result() + } + /// Returns the frames for this database, i.e. the actual logical system. + /// Panics if [`Database::scope_pass`] was not previously called. + /// + /// All logical properties of the database (as opposed to surface syntactic + /// properties) can be obtained from this object. + #[must_use] + pub fn scope_result(&self) -> &Arc { self.scopes.as_ref().unwrap() } @@ -524,71 +530,97 @@ impl Database { /// /// This is an optimized verifier which returns no useful information other /// than error diagnostics. It does not save any parsed proof data. - pub fn verify_result(&mut self) -> &Arc { + pub fn verify_pass(&mut self) -> &Arc { if self.verify.is_none() { - self.name_result(); - self.scope_result(); + self.name_pass(); + self.scope_pass(); time(&self.options.clone(), "verify", || { - if self.prev_verify.is_none() { - self.prev_verify = Some(Arc::new(VerifyResult::default())); - } - - let parse = self.parse_result().clone(); - let scope = self.scope_result().clone(); - let name = self.name_result().clone(); - { - let ver = Arc::make_mut(self.prev_verify.as_mut().unwrap()); - verify::verify(ver, &parse, &name, &scope); - } - self.verify = self.prev_verify.clone(); + let mut ver = self.prev_verify.take().unwrap_or_default(); + let parse = self.parse_result(); + let scope = self.scope_result(); + let name = self.name_result(); + verify::verify(Arc::make_mut(&mut ver), parse, name, scope); + self.prev_verify = Some(ver.clone()); + self.verify = Some(ver); }); } + self.verify_result() + } + + /// Calculates and returns verification information for the database. + /// + /// This is an optimized verifier which returns no useful information other + /// than error diagnostics. It does not save any parsed proof data. + #[must_use] + pub fn verify_result(&self) -> &Arc { self.verify.as_ref().unwrap() } - /// Returns the root node of the outline - pub fn outline_result(&mut self) -> &Arc { + /// Computes and returns the root node of the outline. + pub fn outline_pass(&mut self) -> &Arc { if self.outline.is_none() { time(&self.options.clone(), "outline", || { let parse = self.parse_result().clone(); let mut outline = OutlineNode::default(); - outline::build_outline(&mut outline, &parse); + parse.build_outline(&mut outline); self.outline = Some(Arc::new(outline)); }) } + self.outline_result() + } + + /// Returns the root node of the outline. + /// Panics if [`Database::outline_pass`] was not previously called. + #[must_use] + pub fn outline_result(&self) -> &Arc { self.outline.as_ref().unwrap() } - /// Builds and returns the grammar - pub fn grammar_result(&mut self) -> &Arc { + /// Builds and returns the grammar. + pub fn grammar_pass(&mut self) -> &Arc { if self.grammar.is_none() { - self.name_result(); - self.scope_result(); + self.name_pass(); + self.scope_pass(); time(&self.options.clone(), "grammar", || { - let parse = self.parse_result().clone(); - let name = self.name_result().clone(); + let parse = self.parse_result(); + let name = self.name_result(); let mut grammar = Grammar::default(); - grammar::build_grammar(&mut grammar, &parse, &name); + grammar::build_grammar(&mut grammar, parse, name); self.grammar = Some(Arc::new(grammar)); }) } + self.grammar_result() + } + + /// Returns the grammar. + /// Panics if [`Database::grammar_pass`] was not previously called. + #[must_use] + pub fn grammar_result(&self) -> &Arc { self.grammar.as_ref().unwrap() } - /// Parses the statements using the grammar - pub fn stmt_parse_result(&mut self) -> &Arc { + /// Parses the statements using the grammar. + pub fn stmt_parse(&mut self) -> &Arc { if self.stmt_parse.is_none() { - self.name_result(); - self.scope_result(); + self.name_pass(); + self.scope_pass(); + self.grammar_pass(); time(&self.options.clone(), "stmt_parse", || { - let parse = self.parse_result().clone(); - let name = self.name_result().clone(); - let grammar = self.grammar_result().clone(); + let parse = self.parse_result(); + let name = self.name_result(); + let grammar = self.grammar_result(); let mut stmt_parse = StmtParse::default(); - grammar::parse_statements(&mut stmt_parse, &parse, &name, &grammar); + grammar::parse_statements(&mut stmt_parse, parse, name, grammar); self.stmt_parse = Some(Arc::new(stmt_parse)); }) } + self.stmt_parse_result() + } + + /// Returns the statements parsed using the grammar. + /// Panics if [`Database::stmt_parse`] was not previously called. + #[must_use] + pub fn stmt_parse_result(&self) -> &Arc { self.stmt_parse.as_ref().unwrap() } @@ -599,83 +631,78 @@ impl Database { } /// Get a statement by label. - pub fn statement(&mut self, name: &str) -> Option> { + #[must_use] + pub fn statement(&self, name: &str) -> Option> { let lookup = self.name_result().lookup_label(name.as_bytes())?; Some(self.parse_result().statement(lookup.address)) } /// Export an mmp file for a given statement. - pub fn export(&mut self, stmt: &str) { - time(&self.options.clone(), "export", || { - let parse = self.parse_result().clone(); - let scope = self.scope_result().clone(); - let name = self.name_result().clone(); + pub fn export(&self, stmt: &str) { + time(&self.options, "export", || { + let parse = self.parse_result(); + let scope = self.scope_result(); + let name = self.name_result(); let sref = self.statement(stmt).unwrap_or_else(|| { panic!("Label {} did not correspond to an existing statement", stmt) }); File::create(format!("{}.mmp", stmt)) .map_err(export::ExportError::Io) - .and_then(|mut file| export::export_mmp(&parse, &name, &scope, sref, &mut file)) + .and_then(|mut file| export::export_mmp(parse, name, scope, sref, &mut file)) .unwrap() }) } /// Export the grammar of this database in DOT format. #[cfg(feature = "dot")] - pub fn export_grammar_dot(&mut self) { - time(&self.options.clone(), "export_grammar_dot", || { - let name = self.name_result().clone(); - let grammar = self.grammar_result().clone(); + pub fn export_grammar_dot(&self) { + time(&self.options, "export_grammar_dot", || { + let name = self.name_result(); + let grammar = self.grammar_result(); File::create("grammar.dot") .map_err(export::ExportError::Io) - .and_then(|mut file| grammar.export_dot(&name, &mut file)) + .and_then(|mut file| grammar.export_dot(name, &mut file)) .unwrap() }) } /// Dump the grammar of this database. - pub fn print_grammar(&mut self) { - time(&self.options.clone(), "print_grammar", || { - let name = self.name_result().clone(); - let grammar = self.grammar_result().clone(); - grammar.dump(&name); + pub fn print_grammar(&self) { + time(&self.options, "print_grammar", || { + let name = self.name_result(); + let grammar = self.grammar_result(); + grammar.dump(name); }) } /// Dump the formulas of this database. - pub fn print_formula(&mut self) { - time(&self.options.clone(), "print_formulas", || { - let parse = self.parse_result().clone(); - let name = self.name_result().clone(); - let stmt_parse = self.stmt_parse_result().clone(); - stmt_parse.dump(&parse, &name); + pub fn print_formula(&self) { + time(&self.options, "print_formulas", || { + self.stmt_parse_result().dump(self); }) } /// Verify that printing the formulas of this database gives back the original formulas - pub fn verify_parse_stmt(&mut self) { - time(&self.options.clone(), "verify_parse_stmt", || { - let parse = self.parse_result().clone(); - let name = self.name_result().clone(); - let stmt_parse = self.stmt_parse_result().clone(); - if let Err(diag) = stmt_parse.verify(&parse, &name) { + pub fn verify_parse_stmt(&self) { + time(&self.options, "verify_parse_stmt", || { + if let Err(diag) = self.stmt_parse_result().verify(self) { drop(diag::to_annotations(self.parse_result(), vec![diag])); } }) } /// Dump the outline of this database. - pub fn print_outline(&mut self) { - time(&self.options.clone(), "print_outline", || { - let root_node = self.outline_result().clone(); - self.print_outline_node(&root_node, 0); + pub fn print_outline(&self) { + time(&self.options, "print_outline", || { + let root_node = self.outline_result(); + self.print_outline_node(root_node, 0); }) } /// Dump the outline of this database. - fn print_outline_node(&mut self, node: &OutlineNode, indent: usize) { + fn print_outline_node(&self, node: &OutlineNode, indent: usize) { // let indent = (node.level as usize) * 3 println!( "{:indent$} {:?} {:?}", @@ -703,16 +730,16 @@ impl Database { diags.extend(self.parse_result().parse_diagnostics()); } if types.contains(&DiagnosticClass::Scope) { - diags.extend(self.scope_result().diagnostics()); + diags.extend(self.scope_pass().diagnostics()); } if types.contains(&DiagnosticClass::Verify) { - diags.extend(self.verify_result().diagnostics()); + diags.extend(self.verify_pass().diagnostics()); } if types.contains(&DiagnosticClass::Grammar) { - diags.extend(self.grammar_result().diagnostics()); + diags.extend(self.grammar_pass().diagnostics()); } if types.contains(&DiagnosticClass::StmtParse) { - diags.extend(self.stmt_parse_result().diagnostics()); + diags.extend(self.stmt_parse().diagnostics()); } time(&self.options.clone(), "diag", || { diag::to_annotations(self.parse_result(), diags) diff --git a/src/diag.rs b/src/diag.rs index b23c035..4f2c02d 100644 --- a/src/diag.rs +++ b/src/diag.rs @@ -166,7 +166,7 @@ pub struct Notation { /// Converts a collection of raw diagnostics to a notation list before output. #[must_use] -pub fn to_annotations( +pub(crate) fn to_annotations( sset: &SegmentSet, mut diags: Vec<(StatementAddress, Diagnostic)>, ) -> Vec { diff --git a/src/export.rs b/src/export.rs index f26812e..e46dfe5 100644 --- a/src/export.rs +++ b/src/export.rs @@ -66,7 +66,7 @@ impl error::Error for ExportError { } /// Export an mmp file for a given statement. -pub fn export_mmp( +pub(crate) fn export_mmp( sset: &SegmentSet, nset: &Nameset, scope: &ScopeResult, @@ -95,7 +95,7 @@ pub fn export_mmp( } /// Export an mmp file for a given proof tree. -pub fn export_mmp_proof_tree( +fn export_mmp_proof_tree( sset: &SegmentSet, nset: &Nameset, scope: &ScopeResult, diff --git a/src/formula.rs b/src/formula.rs index aec2574..46f9ee3 100644 --- a/src/formula.rs +++ b/src/formula.rs @@ -33,7 +33,10 @@ use crate::util::fast_extend; use crate::util::new_map; use crate::util::HashMap; use crate::verify::ProofBuilder; +use crate::Database; use core::ops::Index; +use std::fmt::Debug; +use std::fmt::Display; use std::iter::FromIterator; use std::ops::Range; use std::sync::Arc; @@ -84,30 +87,11 @@ pub struct Formula { } impl Formula { - /// Convert the formula back to a flat list of symbols - /// This is slow and shall not normally be called except for showing a result to the user. + /// Augment a formula with a database reference, to produce a [`FormulaRef`]. + /// The resulting object implements [`Display`], [`Debug`], and [`IntoIterator`]. #[must_use] - pub fn iter<'a>(&'a self, sset: &'a Arc, nset: &'a Arc) -> Flatten<'a> { - let mut f = Flatten { - formula: self, - stack: vec![], - sset, - nset, - }; - f.step_into(self.root); - f - } - - /// Displays the formula as a string - #[must_use] - pub fn display(&self, sset: &Arc, nset: &Arc) -> String { - let mut str = String::new(); - str.push_str(as_str(nset.atom_name(self.typecode))); - for symbol in self.iter(sset, nset) { - str.push(' '); - str.push_str(as_str(nset.atom_name(symbol))); - } - str + pub const fn as_ref<'a>(&'a self, db: &'a Database) -> FormulaRef<'a> { + FormulaRef { db, formula: self } } /// Appends this formula to the provided stack buffer. @@ -118,14 +102,10 @@ impl Formula { /// and returns the range the newly added string occupies on the buffer. /// /// See [`crate::verify`] for more about this format. - pub fn append_to_stack_buffer( - &self, - stack_buffer: &mut Vec, - sset: &Arc, - nset: &Arc, - ) -> Range { + fn append_to_stack_buffer(&self, stack_buffer: &mut Vec, db: &Database) -> Range { let tos = stack_buffer.len(); - for symbol in self.iter(sset, nset) { + let nset = &**db.name_result(); + for symbol in self.as_ref(db) { fast_extend(stack_buffer, nset.atom_name(symbol)); *stack_buffer.last_mut().unwrap() |= 0x80; } @@ -143,11 +123,11 @@ impl Formula { &self, stack_buffer: &mut Vec, arr: &mut dyn ProofBuilder, - sset: &Arc, - nset: &Arc, - scope: &Arc, + db: &Database, ) -> I { - self.sub_build_syntax_proof(self.root, stack_buffer, arr, sset, nset, scope) + let nset = db.name_result(); + let scope = db.scope_result(); + self.sub_build_syntax_proof(self.root, stack_buffer, arr, db, nset, scope) } /// Stores and returns the index of a [`ProofTree`] in a [`ProofBuilder`], @@ -162,9 +142,9 @@ impl Formula { node_id: NodeId, stack_buffer: &mut Vec, arr: &mut dyn ProofBuilder, - sset: &Arc, - nset: &Arc, - scope: &Arc, + db: &Database, + nset: &Nameset, + scope: &ScopeResult, ) -> I { let token = nset.atom_name(self.tree[node_id]); let address = nset.lookup_label(token).unwrap().address; @@ -172,9 +152,8 @@ impl Formula { let children_hyps = self .tree .children_iter(node_id) - .map(|s_id| self.sub_build_syntax_proof(s_id, stack_buffer, arr, sset, nset, scope)) - .collect::>() - .into_boxed_slice(); + .map(|s_id| self.sub_build_syntax_proof(s_id, stack_buffer, arr, db, nset, scope)) + .collect::>(); let hyps = frame .hypotheses .iter() @@ -186,12 +165,12 @@ impl Formula { } }) .collect(); - let range = self.append_to_stack_buffer(stack_buffer, sset, nset); + let range = self.append_to_stack_buffer(stack_buffer, db); arr.build(address, hyps, stack_buffer, range) } /// Debug only, dumps the internal structure of the formula. - pub fn dump(&self, nset: &Arc) { + pub fn dump(&self, nset: &Nameset) { println!(" Root: {}", self.root); self.tree.dump(|atom| as_str(nset.atom_name(*atom))); } @@ -303,28 +282,25 @@ impl Formula { substitutions: &Substitutions, formula_builder: &mut FormulaBuilder, ) { - let mut done = false; // TODO(tirix): use https://rust-lang.github.io/rfcs/2497-if-let-chains.html once it's out! if self.is_variable(node_id) { if let Some(formula) = substitutions.0.get(&self.tree[node_id]) { // We encounter a variable, perform substitution. formula.copy_sub_formula(formula.root, formula_builder); - done = true; + return; } } - if !done { - let mut children_count = 0; - for child_node_id in self.tree.children_iter(node_id) { - self.sub_substitute(child_node_id, substitutions, formula_builder); - children_count += 1; - } - formula_builder.reduce( - self.tree[node_id], - children_count, - 0, - self.is_variable(node_id), - ); + let mut children_count = 0; + for child_node_id in self.tree.children_iter(node_id) { + self.sub_substitute(child_node_id, substitutions, formula_builder); + children_count += 1; } + formula_builder.reduce( + self.tree[node_id], + children_count, + 0, + self.is_variable(node_id), + ); } // Copy a sub-formula of this formula to a formula builder @@ -349,13 +325,53 @@ impl PartialEq for Formula { } } +/// A [`Formula`] reference in the context of a [`Database`]. +/// This allows the values in the [`Formula`] to be resolved, +#[derive(Copy, Clone, Debug)] // TODO(Mario): manual Debug impl +pub struct FormulaRef<'a> { + db: &'a Database, + formula: &'a Formula, +} + +impl<'a> std::ops::Deref for FormulaRef<'a> { + type Target = Formula; + + fn deref(&self) -> &Self::Target { + self.formula + } +} + +impl<'a> FormulaRef<'a> { + /// Convert the formula back to a flat list of symbols + /// This is slow and shall not normally be called except for showing a result to the user. + #[must_use] + pub(crate) fn iter(&self) -> Flatten<'a> { + let mut f = Flatten { + formula: self.formula, + stack: vec![], + sset: self.db.parse_result(), + nset: self.db.name_result(), + }; + f.step_into(self.root); + f + } +} + +impl<'a> IntoIterator for FormulaRef<'a> { + type Item = Symbol; + type IntoIter = Flatten<'a>; + fn into_iter(self) -> Flatten<'a> { + self.iter() + } +} + /// An iterator going through each symbol in a formula #[derive(Debug)] pub struct Flatten<'a> { formula: &'a Formula, stack: Vec<(TokenIter<'a>, Option>)>, - sset: &'a Arc, - nset: &'a Arc, + sset: &'a SegmentSet, + nset: &'a Nameset, } impl<'a> Flatten<'a> { @@ -412,6 +428,17 @@ impl<'a> Iterator for Flatten<'a> { // TODO(tirix): provide an implementation for size_hint? } +impl<'a> Display for FormulaRef<'a> { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + let nset = &**self.db.name_result(); + write!(f, "{}", as_str(nset.atom_name(self.typecode)))?; + for symbol in *self { + write!(f, " {}", as_str(nset.atom_name(symbol)))?; + } + Ok(()) + } +} + #[derive(Default)] pub(crate) struct FormulaBuilder { stack: Vec, diff --git a/src/formula_tests.rs b/src/formula_tests.rs index 7725586..4eda37b 100644 --- a/src/formula_tests.rs +++ b/src/formula_tests.rs @@ -25,8 +25,8 @@ const FORMULA_DB: &[u8] = b" /// Shall result in ` A := 1 ` and ` B := 2 ` fn test_unify() { let mut db = mkdb(FORMULA_DB); - let stmt_parse = db.stmt_parse_result().clone(); - let names = db.name_result().clone(); + let stmt_parse = db.stmt_parse().clone(); + let names = db.name_pass().clone(); let goal = stmt_parse .get_formula(&db.statement("1p2com").unwrap()) .unwrap(); @@ -44,7 +44,7 @@ fn test_unify() { /// Unification of ` ( 1 + 2 ) = ( 2 + 1 ) ` with ` ( A + 1 ) = ( B + 1 ) ` shall fail. fn test_unify_fail() { let mut db = mkdb(FORMULA_DB); - let stmt_parse = db.stmt_parse_result().clone(); + let stmt_parse = db.stmt_parse().clone(); let goal = stmt_parse .get_formula(&db.statement("1p2com").unwrap()) .unwrap(); @@ -59,8 +59,8 @@ fn test_unify_fail() { /// Shall result in ` ( ( 1 + 2 ) + 1 ) = ( ( 2 + 1 ) + 1 ) ` fn test_substitute() { let mut db = mkdb(FORMULA_DB); - let stmt_parse = db.stmt_parse_result().clone(); - let names = db.name_result().clone(); + let stmt_parse = db.stmt_parse().clone(); + let names = db.name_pass().clone(); let goal = stmt_parse .get_formula(&db.statement("1p2com").unwrap()) .unwrap(); diff --git a/src/grammar.rs b/src/grammar.rs index a03a98f..9f388c1 100644 --- a/src/grammar.rs +++ b/src/grammar.rs @@ -12,6 +12,7 @@ use crate::parser::{ }; use crate::segment_set::SegmentSet; use crate::util::{new_map, HashMap}; +use crate::Database; use log::{debug, warn}; use std::collections::hash_map::Entry; use std::fmt; @@ -149,7 +150,7 @@ impl GrammarTree { /// // Create an empty database and load any file provided /// let mut db = Database::new(options); /// db.parse("set.mm".to_string(), vec![]); -/// let grammar = db.grammar_result(); +/// let grammar = db.grammar_pass(); /// ``` #[derive(Debug)] pub struct Grammar { @@ -290,7 +291,7 @@ impl GrammarNode { } } -struct GrammarNodeDebug<'a>(&'a GrammarNode, &'a Arc); +struct GrammarNodeDebug<'a>(&'a GrammarNode, &'a Nameset); impl fmt::Debug for GrammarNodeDebug<'_> { /// Lists the contents of the grammar node fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result { @@ -351,7 +352,7 @@ impl fmt::Debug for GrammarNodeDebug<'_> { } } -struct GrammarNodeIdDebug<'a>(&'a Grammar, NodeId, &'a Arc); +struct GrammarNodeIdDebug<'a>(&'a Grammar, NodeId, &'a Nameset); impl fmt::Debug for GrammarNodeIdDebug<'_> { /// Lists the contents of the grammar node, given the grammar and a node id fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result { @@ -383,7 +384,7 @@ impl Default for Grammar { impl Grammar { /// Initializes the grammar using the parser commands - fn initialize(&mut self, sset: &Arc, nset: &Arc) { + fn initialize(&mut self, sset: &SegmentSet, nset: &Nameset) { for (_, command) in sset.parser_commands() { assert!(!command.is_empty(), "Empty parser command!"); if &command[0].as_ref() == b"syntax" { @@ -415,7 +416,7 @@ impl Grammar { /// Creates an "Ambiguous" diagnostic for the grammar /// The node given is the other node found with the same syntax. /// We're looking for any label in that branch. - fn ambiguous(&self, start_node: NodeId, nset: &Arc) -> Diagnostic { + fn ambiguous(&self, start_node: NodeId, nset: &Nameset) -> Diagnostic { let mut node = start_node; loop { match self.nodes.get(node) { @@ -434,7 +435,7 @@ impl Grammar { } } - fn too_short(map: &HashMap<(SymbolType, Atom), NextNode>, nset: &Arc) -> Diagnostic { + fn too_short(map: &HashMap<(SymbolType, Atom), NextNode>, nset: &Nameset) -> Diagnostic { let expected_symbol = map.keys().find(|k| k.0 == SymbolType::Constant).unwrap().1; let expected_token = copy_token(nset.atom_name(expected_symbol)); Diagnostic::ParsedStatementTooShort(expected_token) @@ -511,7 +512,7 @@ impl Grammar { fn add_axiom( &mut self, sref: &StatementRef<'_>, - nset: &Arc, + nset: &Nameset, names: &mut NameReader<'_>, type_conversions: &mut Vec<(TypeCode, TypeCode, Label)>, ) -> Result<(), Diagnostic> { @@ -581,7 +582,7 @@ impl Grammar { fn add_floating( &mut self, sref: &StatementRef<'_>, - nset: &Arc, + nset: &Nameset, names: &mut NameReader<'_>, ) -> Result<(), Diagnostic> { let mut tokens = sref.math_iter(); @@ -639,7 +640,7 @@ impl Grammar { from_typecode: TypeCode, to_typecode: TypeCode, label: Label, - nset: &Arc, + nset: &Nameset, ) -> Result<(), Diagnostic> { let len = self.nodes.len(); for node_id in 0..len { @@ -716,7 +717,7 @@ impl Grammar { &mut self, add_from_node_id: NodeId, add_to_node_id: NodeId, - nset: &Arc, + nset: &Nameset, mut stored_reduces: ReduceVec, make_final: F, ) where @@ -837,7 +838,7 @@ impl Grammar { to_node: NodeId, symbol: Symbol, stype: SymbolType, - nset: &Arc, + nset: &Nameset, ) -> NodeId { let next_node_id_from_root = self .nodes @@ -880,7 +881,7 @@ impl Grammar { &mut self, prefix: &[Token], shadows: &[Token], - nset: &Arc, + nset: &Nameset, names: &mut NameReader<'_>, ) -> Result<(), Diagnostic> { let mut node_id = self.root; @@ -999,8 +1000,8 @@ impl Grammar { /// ` fn handle_commands( &mut self, - sset: &Arc, - nset: &Arc, + sset: &SegmentSet, + nset: &Nameset, names: &mut NameReader<'_>, type_conversions: &[(TypeCode, TypeCode, Label)], ) -> Result<(), (StatementAddress, Diagnostic)> { @@ -1045,11 +1046,7 @@ impl Grammar { Ok(()) } - fn do_shift( - &self, - symbol_iter: &mut dyn Iterator, - nset: &Arc, - ) { + fn do_shift(&self, symbol_iter: &mut dyn Iterator, nset: &Nameset) { if let Some((_ix, symbol)) = symbol_iter.next() { if self.debug { debug!(" SHIFT {:?}", as_str(nset.atom_name(symbol))); @@ -1057,7 +1054,7 @@ impl Grammar { } } - fn do_reduce(formula_builder: &mut FormulaBuilder, reduce: Reduce, nset: &Arc) { + fn do_reduce(formula_builder: &mut FormulaBuilder, reduce: Reduce, nset: &Nameset) { debug!(" REDUCE {:?}", as_str(nset.atom_name(reduce.label))); formula_builder.reduce( reduce.label, @@ -1079,7 +1076,7 @@ impl Grammar { &self, symbol_iter: &mut impl Iterator, expected_typecodes: &[TypeCode], - nset: &Arc, + nset: &Nameset, ) -> Result { struct StackElement { node_id: NodeId, @@ -1206,7 +1203,7 @@ impl Grammar { fn parse_statement( &self, sref: &StatementRef<'_>, - nset: &Arc, + nset: &Nameset, names: &mut NameReader<'_>, ) -> Result, Diagnostic> { if sref.math_len() == 0 { @@ -1249,7 +1246,7 @@ impl Grammar { } /// Lists the contents of the grammar's parse table. This can be used for debugging. - pub fn dump(&self, nset: &Arc) { + pub fn dump(&self, nset: &Nameset) { println!("Grammar tree has {:?} nodes.", self.nodes.len()); for i in 0..self.nodes.len() { println!("{:?}", GrammarNodeIdDebug(self, i, nset)); @@ -1260,7 +1257,7 @@ impl Grammar { /// Exports the grammar tree in the "dot" format. /// See /// This dot file can then be converted to an SVG image using ` dot -Tsvg -o grammar.svg grammar.dot ` - pub fn export_dot(&self, nset: &Arc, write: &mut File) -> Result<(), ExportError> { + pub fn export_dot(&self, nset: &Nameset, write: &mut File) -> Result<(), ExportError> { let mut dot_writer = DotWriter::from(write); let mut digraph = dot_writer.digraph(); for node_id in 0..self.nodes.len() { @@ -1339,11 +1336,7 @@ impl Grammar { /// The grammar can then be used to parse the statements of the database (see [`parse_statements`]), /// or to parse a single statement. /// Use [`Grammar::default`] to get an initial state. -pub(crate) fn build_grammar<'a>( - grammar: &mut Grammar, - sset: &'a Arc, - nset: &Arc, -) { +pub(crate) fn build_grammar<'a>(grammar: &mut Grammar, sset: &'a Arc, nset: &Nameset) { // Read information about the grammar from the parser commands grammar.initialize(sset, nset); grammar.root = grammar.nodes.create_branch(); @@ -1390,7 +1383,7 @@ pub(crate) fn build_grammar<'a>( /// // Create an empty database and load any file provided /// let mut db = Database::new(options); /// db.parse("set.mm".to_string(), vec![]); -/// let stmt_parse = db.stmt_parse_result(); +/// let stmt_parse = db.stmt_parse(); /// ``` /// /// The parse tree for a given statement can then be obtained through [`StmtParse::get_formula`]. @@ -1422,18 +1415,16 @@ impl StmtParse { /// Check that printing parsed statements gives back the original formulas // TODO(tirix): this could be parallelized - pub fn verify( - &self, - sset: &Arc, - nset: &Arc, - ) -> Result<(), (StatementAddress, Diagnostic)> { + pub(crate) fn verify(&self, db: &Database) -> Result<(), (StatementAddress, Diagnostic)> { + let sset = db.parse_result(); + let nset = db.name_result(); for sps in self.segments.values() { for (&sa, formula) in &sps.formulas { let sref = sset.statement(sa); let math_iter = sref .math_iter() .map(|token| nset.lookup_symbol(token.slice).unwrap().atom); - let fmla_iter = formula.iter(sset, nset); + let fmla_iter = formula.as_ref(db).iter(); if math_iter.ne(fmla_iter) { return Err((sa, Diagnostic::FormulaVerificationFailed)); } @@ -1443,15 +1434,17 @@ impl StmtParse { } /// Writes down all formulas - pub fn dump(&self, sset: &Arc, nset: &Arc) { + pub(crate) fn dump(&self, db: &Database) { println!("Formula Dump:"); + let sset = db.parse_result(); + let nset = db.name_result(); for sps in self.segments.values() { for (&sa, formula) in &sps.formulas { let sref = sset.statement(sa); println!( "{}: {}", as_str(nset.statement_name(&sref)), - formula.display(sset, nset) + formula.as_ref(db) ); } } @@ -1475,10 +1468,10 @@ struct StmtParseSegment { /// Runs statement parsing for a single segment. fn parse_statements_single<'a>( - sset: &'a Arc, - nset: &Arc, + sset: &'a SegmentSet, + nset: &Nameset, names: &mut NameReader<'_>, - grammar: &Arc, + grammar: &Grammar, sid: SegmentId, ) -> StmtParseSegment { let segment = sset.segment(sid); @@ -1518,9 +1511,9 @@ fn parse_statements_single<'a>( /// The parse tree for a given statement can then be obtained through [`StmtParse::get_formula`]. /// Use [`StmtParse::default`] to get an initial state. /// Like for several other phases, this occurs in parallel. -pub(crate) fn parse_statements<'a>( +pub(crate) fn parse_statements( stmt_parse: &mut StmtParse, - segments: &'a Arc, + segments: &Arc, nset: &Arc, grammar: &Arc, ) { diff --git a/src/grammar_tests.rs b/src/grammar_tests.rs index d11cf37..f555329 100644 --- a/src/grammar_tests.rs +++ b/src/grammar_tests.rs @@ -32,7 +32,7 @@ pub(super) fn mkdb(text: &[u8]) -> Database { #[test] fn test_lookup() { let mut db = mkdb(GRAMMAR_DB); - let names = db.name_result(); + let names = db.name_pass(); assert!(as_str(names.atom_name(names.lookup_symbol(b"A").unwrap().atom)) == "A"); assert!(as_str(names.atom_name(names.lookup_symbol(b"B").unwrap().atom)) == "B"); assert!(as_str(names.atom_name(names.lookup_label(b"weq").unwrap().atom)) == "weq"); @@ -43,8 +43,8 @@ fn test_lookup() { fn test_db_stmt_parse() { let mut db = mkdb(GRAMMAR_DB); let sset = db.parse_result().clone(); - let grammar = db.grammar_result().clone(); - let stmt_parse = db.stmt_parse_result().clone(); + let grammar = db.grammar_pass().clone(); + let stmt_parse = db.stmt_parse().clone(); assert!(sset.parse_diagnostics().is_empty()); assert!(grammar.diagnostics().is_empty()); assert!(stmt_parse.diagnostics().is_empty()); @@ -53,8 +53,8 @@ fn test_db_stmt_parse() { #[test] fn test_db_formula() { let mut db = mkdb(GRAMMAR_DB); - let stmt_parse = db.stmt_parse_result().clone(); - let names = db.name_result().clone(); + let stmt_parse = db.stmt_parse().clone(); + let names = db.name_pass().clone(); { let sref = db.statement("ax-com").unwrap(); let formula = stmt_parse.get_formula(&sref).unwrap(); @@ -71,9 +71,8 @@ fn test_db_formula() { #[test] fn test_parse_formula() { let mut db = mkdb(GRAMMAR_DB); - let sset = db.parse_result().clone(); - let names = db.name_result().clone(); - let grammar = db.grammar_result().clone(); + let names = db.name_pass().clone(); + let grammar = db.grammar_pass().clone(); let wff = names.lookup_symbol(b"wff").unwrap().atom; let class = names.lookup_symbol(b"class").unwrap().atom; let a = names.lookup_symbol(b"A").unwrap().atom; @@ -91,7 +90,7 @@ fn test_parse_formula() { assert!(as_str(names.atom_name(formula.get_by_path(&[2]).unwrap())) == "cadd"); assert!(as_str(names.atom_name(formula.get_by_path(&[2, 1]).unwrap())) == "cB"); assert!(as_str(names.atom_name(formula.get_by_path(&[2, 2]).unwrap())) == "cA"); - assert!(formula.iter(&sset, &names).eq(fmla_vec.into_iter())); + assert!(formula.as_ref(&db).iter().eq(fmla_vec.into_iter())); } // This grammar exposes issue #32 in the statement parser @@ -113,8 +112,8 @@ const GRAMMAR_DB_32: &[u8] = b" #[test] fn test_db_32_formula() { let mut db = mkdb(GRAMMAR_DB_32); - let stmt_parse = db.stmt_parse_result().clone(); - let names = db.name_result().clone(); + let stmt_parse = db.stmt_parse().clone(); + let names = db.name_pass().clone(); { let sref = db.statement("check").unwrap(); let formula = stmt_parse.get_formula(&sref).unwrap(); @@ -156,8 +155,8 @@ const GARDEN_PATH_DB: &[u8] = b" fn test_garden_path_1() { let mut db = mkdb(GARDEN_PATH_DB); let sset = db.parse_result().clone(); - let stmt_parse = db.stmt_parse_result().clone(); - let names = db.name_result().clone(); + let stmt_parse = db.stmt_parse().clone(); + let names = db.name_pass().clone(); assert!(sset.parse_diagnostics().is_empty()); let sref = db.statement("formula1").unwrap(); let formula = stmt_parse.get_formula(&sref).unwrap(); @@ -172,8 +171,8 @@ fn test_garden_path_1() { #[test] fn test_garden_path_2() { let mut db = mkdb(GARDEN_PATH_DB); - let stmt_parse = db.stmt_parse_result().clone(); - let names = db.name_result().clone(); + let stmt_parse = db.stmt_parse().clone(); + let names = db.name_pass().clone(); let sref = db.statement("formula2").unwrap(); let formula = stmt_parse.get_formula(&sref).unwrap(); assert!(as_str(names.atom_name(formula.get_by_path(&[]).unwrap())) == "weq"); @@ -189,8 +188,8 @@ fn test_garden_path_2() { #[test] fn test_garden_path_3() { let mut db = mkdb(GARDEN_PATH_DB); - let stmt_parse = db.stmt_parse_result().clone(); - let names = db.name_result().clone(); + let stmt_parse = db.stmt_parse().clone(); + let names = db.name_pass().clone(); let sref = db.statement("formula3").unwrap(); let formula = stmt_parse.get_formula(&sref).unwrap(); assert!(as_str(names.atom_name(formula.get_by_path(&[]).unwrap())) == "weq"); @@ -219,7 +218,7 @@ macro_rules! grammar_test { fn $name() { let mut db = mkdb($text); let sset = db.parse_result().clone(); - let grammar = db.grammar_result(); + let grammar = db.grammar_pass(); assert!(sset.parse_diagnostics().is_empty()); assert_eq!(grammar.diagnostics(), &[(sa!($id, $index), $diag)]); } diff --git a/src/nameck.rs b/src/nameck.rs index 4390cc9..ebb6f0d 100644 --- a/src/nameck.rs +++ b/src/nameck.rs @@ -175,7 +175,7 @@ impl Nameset { } /// Called by Database to bring the index up to date with segment changes. - pub fn update(&mut self, segs: &SegmentSet) { + pub(crate) fn update(&mut self, segs: &SegmentSet) { self.order = segs.order.clone(); self.generation = self.generation.checked_add(1).unwrap(); self.options = segs.options.clone(); diff --git a/src/outline.rs b/src/outline.rs index 344dadf..e8319a6 100644 --- a/src/outline.rs +++ b/src/outline.rs @@ -83,15 +83,17 @@ impl OutlineNode { } /// Builds the overall outline from the different segments -pub fn build_outline(node: &mut OutlineNode, sset: &Arc) { - let segments = sset.segments(); - assert!(!segments.is_empty(), "Parse returned no segment!"); - *node = OutlineNode::root_node(&segments); +impl SegmentSet { + pub(crate) fn build_outline(&self, node: &mut OutlineNode) { + let segments = self.segments(); + assert!(!segments.is_empty(), "Parse returned no segment!"); + *node = OutlineNode::root_node(&segments); - for vsr in &segments { - for heading in &vsr.segment.outline { - let new_node = OutlineNode::from_heading_def(heading, vsr.id); - node.add_child(new_node); + for vsr in &segments { + for heading in &vsr.segment.outline { + let new_node = OutlineNode::from_heading_def(heading, vsr.id); + node.add_child(new_node); + } } } } diff --git a/src/parser_tests.rs b/src/parser_tests.rs index 7c93f0e..5b9e452 100644 --- a/src/parser_tests.rs +++ b/src/parser_tests.rs @@ -47,7 +47,7 @@ fn mkdb(text: &[u8]) -> Database { #[test] fn test_segref() { - let mut db = mkdb(b"${ $}"); + let db = mkdb(b"${ $}"); let seg = db.parse_result().segments()[0]; assert_eq!(seg.bytes(), 5); let mut stmt_iter = seg.into_iter(); @@ -68,7 +68,7 @@ fn test_segref() { #[test] fn test_stref_v() { - let mut db = mkdb(b"$v X $. ${ $v Y Z $. $}"); + let db = mkdb(b"$v X $. ${ $v Y Z $. $}"); let seg = db.parse_result().segments()[0]; let vx = seg.statement(0); let vyz = seg.statement(2); @@ -95,7 +95,7 @@ macro_rules! parse_test { ($name:ident, $text:expr, $diags:expr) => { #[test] fn $name() { - let mut db = mkdb($text); + let db = mkdb($text); let seg = db.parse_result().segments()[0]; assert_eq!(seg.diagnostics, &$diags); } diff --git a/src/proof.rs b/src/proof.rs index 66a0c76..fae07d9 100644 --- a/src/proof.rs +++ b/src/proof.rs @@ -126,7 +126,7 @@ 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 fn new( + pub(crate) fn new( sset: &SegmentSet, nset: &Nameset, scopes: &ScopeResult, @@ -409,23 +409,23 @@ impl ProofStyle { #[derive(Debug)] pub struct ProofTreePrinter<'a> { /// The segment set, for looking up statements - pub sset: &'a SegmentSet, + pub(crate) sset: &'a SegmentSet, /// The nameset, for looking up statements - pub nset: &'a Nameset, + pub(crate) nset: &'a Nameset, /// The scoping pass, for looking up statements - pub scope: &'a ScopeResult, + pub(crate) scope: &'a ScopeResult, /// The current statement label (only used in explicit style) - pub thm_label: TokenPtr<'a>, + pub(crate) thm_label: TokenPtr<'a>, /// The type of output (normal, compressed, packed, ...) - pub style: ProofStyle, + pub(crate) style: ProofStyle, /// The source data - pub arr: &'a ProofTreeArray, + pub(crate) arr: &'a ProofTreeArray, /// The initial cursor character number on the current line - pub initial_chr: u16, + pub(crate) initial_chr: u16, /// The amount of leading whitespace to print - pub indent: u16, + pub(crate) indent: u16, /// The number of characters to fit before going to a new line - pub line_width: u16, + pub(crate) line_width: u16, } /// The local variables of `ProofTreePrinter::fmt()`, extracted into a struct diff --git a/src/scopeck.rs b/src/scopeck.rs index e5f2dea..8f4225f 100644 --- a/src/scopeck.rs +++ b/src/scopeck.rs @@ -968,7 +968,7 @@ impl ScopeResult { /// Extracts scope data for a database. /// /// Use `ScopeResult::default()` to get an initial state. -pub fn scope_check(result: &mut ScopeResult, segments: &Arc, names: &Arc) { +pub(crate) fn scope_check(result: &mut ScopeResult, segments: &SegmentSet, names: &Nameset) { result.incremental |= result.frame_index.is_empty(); result.incremental &= segments.options.incremental; result.generation += 1; diff --git a/src/segment_set.rs b/src/segment_set.rs index 07abd86..6c4c9e0 100644 --- a/src/segment_set.rs +++ b/src/segment_set.rs @@ -145,14 +145,14 @@ struct FileSR(Option<(String, FileTime)>, Vec); /// option block and the work queue executor, although those responsibilities /// may be moved. #[derive(Debug, Clone)] -pub struct SegmentSet { +pub(crate) struct SegmentSet { /// The option block controlling this database. - pub options: Arc, + pub(crate) options: Arc, /// The work queue for use with this database. - pub exec: Executor, + pub(crate) exec: Executor, /// Order structure which records the relative order of segment IDs created /// by the SegmentSet. - pub order: Arc, + pub(crate) order: Arc, /// Track segment and source info in parallel so they can be updated /// independently in the slicing case and if a file is renamed. segments: HashMap, Arc)>, @@ -165,7 +165,7 @@ pub struct SegmentSet { impl SegmentSet { /// Start a new empty segment set in the context of an option block and /// executor which were previously created by the `Database`. - pub fn new(opts: Arc, exec: &Executor) -> Self { + pub(crate) fn new(opts: Arc, exec: &Executor) -> Self { SegmentSet { options: opts, exec: exec.clone(), @@ -177,7 +177,7 @@ impl SegmentSet { } /// Iterates over all loaded segments in logical order. - pub fn segments(&self) -> Vec> { + pub(crate) fn segments(&self) -> Vec> { // this might be an actual iterator in the future if needs be let mut out: Vec> = self .segments @@ -192,7 +192,7 @@ impl SegmentSet { } /// Fetch a handle to a loaded segment given its ID. - pub fn segment(&self, seg_id: SegmentId) -> SegmentRef<'_> { + pub(crate) fn segment(&self, seg_id: SegmentId) -> SegmentRef<'_> { SegmentRef { id: seg_id, segment: &self.segments[&seg_id].0, @@ -200,7 +200,7 @@ impl SegmentSet { } /// Fetch a handle to a loaded segment given a possibly stale ID. - pub fn segment_opt(&self, seg_id: SegmentId) -> Option> { + pub(crate) fn segment_opt(&self, seg_id: SegmentId) -> Option> { self.segments .get(&seg_id) .map(|&(ref seg, ref _srcinfo)| SegmentRef { @@ -210,17 +210,17 @@ impl SegmentSet { } /// Fetch source information for a loaded segment given its ID. - pub fn source_info(&self, seg_id: SegmentId) -> &Arc { + pub(crate) fn source_info(&self, seg_id: SegmentId) -> &Arc { &self.segments[&seg_id].1 } /// Fetches a handle to a statement given a global address. - pub fn statement(&self, addr: StatementAddress) -> StatementRef<'_> { + pub(crate) fn statement(&self, addr: StatementAddress) -> StatementRef<'_> { self.segment(addr.segment_id).statement(addr.index) } /// Reports any parse errors associated with loaded segments. - pub fn parse_diagnostics(&self) -> Vec<(StatementAddress, Diagnostic)> { + pub(crate) fn parse_diagnostics(&self) -> Vec<(StatementAddress, Diagnostic)> { let mut out = Vec::new(); for sref in self.segments() { for &(ix, ref d) in &sref.diagnostics { @@ -231,7 +231,7 @@ impl SegmentSet { } /// Returns the commands parsed from the $j comments - pub fn parser_commands(&self) -> Vec<(StatementAddress, Command)> { + pub(crate) fn parser_commands(&self) -> Vec<(StatementAddress, Command)> { let mut out = Vec::new(); for sref in self.segments() { for &(ix, ref command) in &sref.commands { @@ -247,7 +247,7 @@ impl SegmentSet { /// Each element of `data` intercedes a file with the same name for the /// purposes of file inclusion statements. If a match is not made in /// `data`, it will be accessed as a file relative to the current directory. - pub fn read(&mut self, path: String, data: Vec<(String, Vec)>) { + pub(crate) fn read(&mut self, path: String, data: Vec<(String, Vec)>) { // data which is kept during the recursive load process, which does // _not_ have access to the SegmentSet struct RecState { diff --git a/src/tree.rs b/src/tree.rs index 8804de3..c907eff 100644 --- a/src/tree.rs +++ b/src/tree.rs @@ -125,12 +125,8 @@ impl Iterator for SiblingIter<'_, TreeItem> { type Item = NodeId; fn next(&mut self) -> Option { - if self.current_id == 0 { - None - } else { - let current_id = self.current_id; - self.current_id = self.tree.nodes[current_id - 1].next_sibling; - Some(current_id) - } + let current_id = self.current_id; + self.current_id = self.tree.nodes[current_id.checked_sub(1)?].next_sibling; + Some(current_id) } } diff --git a/src/verify.rs b/src/verify.rs index fc5ff42..68ac339 100644 --- a/src/verify.rs +++ b/src/verify.rs @@ -870,7 +870,7 @@ fn verify_segment( } /// Calculates or updates the verification result for a database. -pub fn verify( +pub(crate) fn verify( result: &mut VerifyResult, segments: &Arc, nset: &Arc, @@ -909,7 +909,7 @@ pub fn verify( /// Parse a single $p statement, returning the result of the given /// proof builder, or an error if the proof is faulty -pub fn verify_one( +pub(crate) fn verify_one( sset: &SegmentSet, nset: &Nameset, scopes: &ScopeResult, From d43fcd6587b9309a463ed8a730d929bc2b2b43ca Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Thu, 14 Oct 2021 03:06:48 -0400 Subject: [PATCH 2/9] add `Database::export_mmp` --- src/database.rs | 5 +---- src/export.rs | 15 +++++++++++++++ 2 files changed, 16 insertions(+), 4 deletions(-) diff --git a/src/database.rs b/src/database.rs index 223f1f4..9beb273 100644 --- a/src/database.rs +++ b/src/database.rs @@ -640,16 +640,13 @@ impl Database { /// Export an mmp file for a given statement. pub fn export(&self, stmt: &str) { time(&self.options, "export", || { - let parse = self.parse_result(); - let scope = self.scope_result(); - let name = self.name_result(); let sref = self.statement(stmt).unwrap_or_else(|| { panic!("Label {} did not correspond to an existing statement", stmt) }); File::create(format!("{}.mmp", stmt)) .map_err(export::ExportError::Io) - .and_then(|mut file| export::export_mmp(parse, name, scope, sref, &mut file)) + .and_then(|mut file| self.export_mmp(sref, &mut file)) .unwrap() }) } diff --git a/src/export.rs b/src/export.rs index e46dfe5..70961f6 100644 --- a/src/export.rs +++ b/src/export.rs @@ -11,6 +11,7 @@ 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; use std::fmt; @@ -65,6 +66,20 @@ impl error::Error for ExportError { } } +impl Database { + /// Export an mmp file for a given statement. + pub fn export_mmp( + &self, + 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) + } +} + /// Export an mmp file for a given statement. pub(crate) fn export_mmp( sset: &SegmentSet, From a12359fa62de42444fd9281ce45663ebd65e707c Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Thu, 14 Oct 2021 03:39:45 -0400 Subject: [PATCH 3/9] fix --- src/main.rs | 1 + 1 file changed, 1 insertion(+) diff --git a/src/main.rs b/src/main.rs index 02d765d..32bd7e7 100644 --- a/src/main.rs +++ b/src/main.rs @@ -103,6 +103,7 @@ fn main() { } if matches.is_present("verify_parse_stmt") { + db.stmt_parse(); db.verify_parse_stmt(); } From fc45dbcc7cb33d64c469f817803eb2382316dea9 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Thu, 14 Oct 2021 04:02:39 -0400 Subject: [PATCH 4/9] fix Default impl for Database --- src/database.rs | 20 +++++++++++++++++++- 1 file changed, 19 insertions(+), 1 deletion(-) diff --git a/src/database.rs b/src/database.rs index 9beb273..2961898 100644 --- a/src/database.rs +++ b/src/database.rs @@ -128,7 +128,7 @@ use std::time::Instant; /// for the lifetime of the database container. /// /// Some of these could theoretically support modification. -#[derive(Copy, Clone, Default, Debug)] +#[derive(Copy, Clone, Debug)] pub struct DbOptions { /// If true, the automatic splitting of large files described above is /// enabled, with the caveat about chapter comments inside grouping @@ -152,6 +152,18 @@ pub struct DbOptions { pub jobs: usize, } +impl Default for DbOptions { + fn default() -> Self { + Self { + autosplit: false, + timing: false, + trace_recalc: false, + incremental: false, + jobs: 1, + } + } +} + /// Wraps a heap-allocated closure with a difficulty score which can be used for /// sorting; this might belong in the standard library as `CompareFirst` or such. struct Job(usize, Box); @@ -377,6 +389,12 @@ pub struct Database { stmt_parse: Option>, } +impl Default for Database { + fn default() -> Self { + Self::new(DbOptions::default()) + } +} + fn time R>(opts: &DbOptions, name: &str, f: F) -> R { let now = Instant::now(); let ret = f(); From 2ddd2221dee556a237928a083e91131cc40bce42 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Thu, 14 Oct 2021 04:13:31 -0400 Subject: [PATCH 5/9] make `Database::segments` not an option --- src/database.rs | 16 ++++++++-------- src/segment_set.rs | 8 ++++++++ 2 files changed, 16 insertions(+), 8 deletions(-) diff --git a/src/database.rs b/src/database.rs index 2961898..ada590a 100644 --- a/src/database.rs +++ b/src/database.rs @@ -373,7 +373,7 @@ impl Promise { #[derive(Debug)] pub struct Database { options: Arc, - segments: Option>, + segments: Arc, /// We track the "current" and "previous" for all known passes, so that each /// pass can use its most recent results for optimized incremental /// processing. Any change to the segment vector zeroizes the current @@ -414,7 +414,7 @@ impl Drop for Database { self.scopes = None; self.prev_nameset = None; self.nameset = None; - self.segments = None; + Arc::make_mut(&mut self.segments).clear(); self.outline = None; }); } @@ -430,7 +430,7 @@ impl Database { let options = Arc::new(options); let exec = Executor::new(options.jobs); Database { - segments: Some(Arc::new(SegmentSet::new(options.clone(), &exec))), + segments: Arc::new(SegmentSet::new(options.clone(), &exec)), options, nameset: None, scopes: None, @@ -475,7 +475,7 @@ impl Database { /// appropriate. pub fn parse(&mut self, start: String, text: Vec<(String, Vec)>) { time(&self.options.clone(), "parse", || { - Arc::make_mut(self.segments.as_mut().unwrap()).read(start, text); + Arc::make_mut(&mut self.segments).read(start, text); self.nameset = None; self.scopes = None; self.verify = None; @@ -488,8 +488,8 @@ impl Database { /// /// Unlike the other accessors, this is not lazy (subject to change when the /// modification API goes in.) - pub(crate) fn parse_result(&self) -> &Arc { - self.segments.as_ref().unwrap() + pub(crate) const fn parse_result(&self) -> &Arc { + &self.segments } /// Calculates and returns the name to definition lookup table. @@ -644,8 +644,8 @@ impl Database { /// A getter method which does not build the outline #[must_use] - pub const fn get_outline(&self) -> &Option> { - &self.outline + pub const fn get_outline(&self) -> Option<&Arc> { + self.outline.as_ref() } /// Get a statement by label. diff --git a/src/segment_set.rs b/src/segment_set.rs index 6c4c9e0..6aeb774 100644 --- a/src/segment_set.rs +++ b/src/segment_set.rs @@ -176,6 +176,14 @@ impl SegmentSet { } } + /// Reset the segment set to the empty state. + pub(crate) fn clear(&mut self) { + *Arc::make_mut(&mut self.order) = SegmentOrder::new(); + self.segments = new_map(); + self.parse_cache = new_map(); + self.file_cache = new_map(); + } + /// Iterates over all loaded segments in logical order. pub(crate) fn segments(&self) -> Vec> { // this might be an actual iterator in the future if needs be From cd79a6da2ad0665e2639d6d4d69cc86ef2a72634 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Thu, 14 Oct 2021 22:58:05 -0400 Subject: [PATCH 6/9] make `export_mmp[_proof_tree]` public --- src/database.rs | 3 +- src/export.rs | 228 ++++++++++++++++++++++-------------------------- src/proof.rs | 10 +-- src/verify.rs | 11 ++- 4 files changed, 116 insertions(+), 136 deletions(-) diff --git a/src/database.rs b/src/database.rs index ada590a..0faaa6c 100644 --- a/src/database.rs +++ b/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. diff --git a/src/export.rs b/src/export.rs index 70961f6..f7bdf68 100644 --- a/src/export.rs +++ b/src/export.rs @@ -1,7 +1,6 @@ //! 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; @@ -9,8 +8,6 @@ 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, + "$( 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( - sset: &SegmentSet, - nset: &Nameset, - scope: &ScopeResult, - stmt: StatementRef<'_>, - out: &mut W, -) -> Result<(), ExportError> { - let thm_label = stmt.label(); - writeln!( - out, - "$( 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( + &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( - 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 = 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 = 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(()) + } } diff --git a/src/proof.rs b/src/proof.rs index fae07d9..be159fb 100644 --- a/src/proof.rs +++ b/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 { + pub(crate) fn new(db: &Database, stmt: StatementRef<'_>) -> Result { 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) } diff --git a/src/verify.rs b/src/verify.rs index 68ac339..1c5d169 100644 --- a/src/verify.rs +++ b/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( - sset: &SegmentSet, - nset: &Nameset, - scopes: &ScopeResult, + db: &Database, builder: &mut P, stmt: StatementRef<'_>, ) -> result::Result { 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(), From 57dacafda5e864d877a5cb6bf06d2c41640bcc3a Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Thu, 14 Oct 2021 23:05:15 -0400 Subject: [PATCH 7/9] move `append_to_stack_buffer` to `FormulaRef` --- src/formula.rs | 149 ++++++++++++++++++++++++------------------------- 1 file changed, 72 insertions(+), 77 deletions(-) diff --git a/src/formula.rs b/src/formula.rs index 46f9ee3..6acd0b1 100644 --- a/src/formula.rs +++ b/src/formula.rs @@ -24,7 +24,6 @@ use crate::parser::as_str; use crate::parser::SymbolType; use crate::parser::TokenIter; use crate::scopeck::Hyp; -use crate::scopeck::ScopeResult; use crate::segment_set::SegmentSet; use crate::tree::NodeId; use crate::tree::SiblingIter; @@ -94,81 +93,6 @@ impl Formula { FormulaRef { db, formula: self } } - /// Appends this formula to the provided stack buffer. - /// - /// The [`ProofBuilder`] structure uses a dense representation of formulas as byte strings, - /// using the high bit to mark the end of each token. - /// This function creates such a byte string, stores it in the provided buffer, - /// and returns the range the newly added string occupies on the buffer. - /// - /// See [`crate::verify`] for more about this format. - fn append_to_stack_buffer(&self, stack_buffer: &mut Vec, db: &Database) -> Range { - let tos = stack_buffer.len(); - let nset = &**db.name_result(); - for symbol in self.as_ref(db) { - fast_extend(stack_buffer, nset.atom_name(symbol)); - *stack_buffer.last_mut().unwrap() |= 0x80; - } - let n_tos = stack_buffer.len(); - tos..n_tos - } - - /// Builds the syntax proof for this formula. - /// - /// In Metamath, it is possible to write proofs that a given formula is a well-formed formula. - /// This methos builds such a syntax proof for the formula into a [`crate::proof::ProofTree`], - /// stores that proof tree in the provided [`ProofBuilder`] `arr`, - /// and returns the index of that `ProofTree` within `arr`. - pub fn build_syntax_proof>( - &self, - stack_buffer: &mut Vec, - arr: &mut dyn ProofBuilder, - db: &Database, - ) -> I { - let nset = db.name_result(); - let scope = db.scope_result(); - self.sub_build_syntax_proof(self.root, stack_buffer, arr, db, nset, scope) - } - - /// Stores and returns the index of a [`ProofTree`] in a [`ProofBuilder`], - /// corresponding to the syntax proof for the sub-formula with root at the given `node_id`. - // Formulas children nodes are stored in the order of appearance of the variables - // in the formula, which is efficient when parsing or rendering the formula from - // or into a string of tokens. However, proofs require children nodes - // sorted in the order of mandatory floating hypotheses. - // This method performs this mapping. - fn sub_build_syntax_proof>( - &self, - node_id: NodeId, - stack_buffer: &mut Vec, - arr: &mut dyn ProofBuilder, - db: &Database, - nset: &Nameset, - scope: &ScopeResult, - ) -> I { - let token = nset.atom_name(self.tree[node_id]); - let address = nset.lookup_label(token).unwrap().address; - let frame = scope.get(token).unwrap(); - let children_hyps = self - .tree - .children_iter(node_id) - .map(|s_id| self.sub_build_syntax_proof(s_id, stack_buffer, arr, db, nset, scope)) - .collect::>(); - let hyps = frame - .hypotheses - .iter() - .filter_map(|hyp| { - if let Hyp::Floating(_sa, index, _) = hyp { - Some(children_hyps[*index]) - } else { - None - } - }) - .collect(); - let range = self.append_to_stack_buffer(stack_buffer, db); - arr.build(address, hyps, stack_buffer, range) - } - /// Debug only, dumps the internal structure of the formula. pub fn dump(&self, nset: &Nameset) { println!(" Root: {}", self.root); @@ -345,7 +269,7 @@ impl<'a> FormulaRef<'a> { /// Convert the formula back to a flat list of symbols /// This is slow and shall not normally be called except for showing a result to the user. #[must_use] - pub(crate) fn iter(&self) -> Flatten<'a> { + pub(crate) fn iter(self) -> Flatten<'a> { let mut f = Flatten { formula: self.formula, stack: vec![], @@ -355,6 +279,77 @@ impl<'a> FormulaRef<'a> { f.step_into(self.root); f } + + /// Appends this formula to the provided stack buffer. + /// + /// The [`ProofBuilder`] structure uses a dense representation of formulas as byte strings, + /// using the high bit to mark the end of each token. + /// This function creates such a byte string, stores it in the provided buffer, + /// and returns the range the newly added string occupies on the buffer. + /// + /// See [`crate::verify`] for more about this format. + fn append_to_stack_buffer(self, stack_buffer: &mut Vec) -> Range { + let tos = stack_buffer.len(); + let nset = &**self.db.name_result(); + for symbol in self { + fast_extend(stack_buffer, nset.atom_name(symbol)); + *stack_buffer.last_mut().unwrap() |= 0x80; + } + let n_tos = stack_buffer.len(); + tos..n_tos + } + + /// Builds the syntax proof for this formula. + /// + /// In Metamath, it is possible to write proofs that a given formula is a well-formed formula. + /// This methos builds such a syntax proof for the formula into a [`crate::proof::ProofTree`], + /// stores that proof tree in the provided [`ProofBuilder`] `arr`, + /// and returns the index of that `ProofTree` within `arr`. + pub fn build_syntax_proof>( + self, + stack_buffer: &mut Vec, + arr: &mut dyn ProofBuilder, + ) -> I { + self.sub_build_syntax_proof(self.root, stack_buffer, arr) + } + + /// Stores and returns the index of a [`ProofTree`] in a [`ProofBuilder`], + /// corresponding to the syntax proof for the sub-formula with root at the given `node_id`. + // Formulas children nodes are stored in the order of appearance of the variables + // in the formula, which is efficient when parsing or rendering the formula from + // or into a string of tokens. However, proofs require children nodes + // sorted in the order of mandatory floating hypotheses. + // This method performs this mapping. + fn sub_build_syntax_proof>( + self, + node_id: NodeId, + stack_buffer: &mut Vec, + arr: &mut dyn ProofBuilder, + ) -> I { + let nset = self.db.name_result(); + + let token = nset.atom_name(self.tree[node_id]); + let address = nset.lookup_label(token).unwrap().address; + let frame = self.db.scope_result().get(token).unwrap(); + let children_hyps = self + .tree + .children_iter(node_id) + .map(|s_id| self.sub_build_syntax_proof(s_id, stack_buffer, arr)) + .collect::>(); + let hyps = frame + .hypotheses + .iter() + .filter_map(|hyp| { + if let Hyp::Floating(_sa, index, _) = hyp { + Some(children_hyps[*index]) + } else { + None + } + }) + .collect(); + let range = self.append_to_stack_buffer(stack_buffer); + arr.build(address, hyps, stack_buffer, range) + } } impl<'a> IntoIterator for FormulaRef<'a> { From 28cb1bb69daffdb65e827c1607f8fe2cf464b5f8 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Thu, 14 Oct 2021 23:06:31 -0400 Subject: [PATCH 8/9] rename `stmt_parse` to `stmt_parse_pass` --- src/database.rs | 4 ++-- src/formula_tests.rs | 6 +++--- src/grammar.rs | 2 +- src/grammar_tests.rs | 12 ++++++------ src/main.rs | 2 +- 5 files changed, 13 insertions(+), 13 deletions(-) diff --git a/src/database.rs b/src/database.rs index 0faaa6c..ec79f49 100644 --- a/src/database.rs +++ b/src/database.rs @@ -619,7 +619,7 @@ impl Database { } /// Parses the statements using the grammar. - pub fn stmt_parse(&mut self) -> &Arc { + pub fn stmt_parse_pass(&mut self) -> &Arc { if self.stmt_parse.is_none() { self.name_pass(); self.scope_pass(); @@ -755,7 +755,7 @@ impl Database { diags.extend(self.grammar_pass().diagnostics()); } if types.contains(&DiagnosticClass::StmtParse) { - diags.extend(self.stmt_parse().diagnostics()); + diags.extend(self.stmt_parse_pass().diagnostics()); } time(&self.options.clone(), "diag", || { diag::to_annotations(self.parse_result(), diags) diff --git a/src/formula_tests.rs b/src/formula_tests.rs index 4eda37b..5de3f0e 100644 --- a/src/formula_tests.rs +++ b/src/formula_tests.rs @@ -25,7 +25,7 @@ const FORMULA_DB: &[u8] = b" /// Shall result in ` A := 1 ` and ` B := 2 ` fn test_unify() { let mut db = mkdb(FORMULA_DB); - let stmt_parse = db.stmt_parse().clone(); + let stmt_parse = db.stmt_parse_pass().clone(); let names = db.name_pass().clone(); let goal = stmt_parse .get_formula(&db.statement("1p2com").unwrap()) @@ -44,7 +44,7 @@ fn test_unify() { /// Unification of ` ( 1 + 2 ) = ( 2 + 1 ) ` with ` ( A + 1 ) = ( B + 1 ) ` shall fail. fn test_unify_fail() { let mut db = mkdb(FORMULA_DB); - let stmt_parse = db.stmt_parse().clone(); + let stmt_parse = db.stmt_parse_pass().clone(); let goal = stmt_parse .get_formula(&db.statement("1p2com").unwrap()) .unwrap(); @@ -59,7 +59,7 @@ fn test_unify_fail() { /// Shall result in ` ( ( 1 + 2 ) + 1 ) = ( ( 2 + 1 ) + 1 ) ` fn test_substitute() { let mut db = mkdb(FORMULA_DB); - let stmt_parse = db.stmt_parse().clone(); + let stmt_parse = db.stmt_parse_pass().clone(); let names = db.name_pass().clone(); let goal = stmt_parse .get_formula(&db.statement("1p2com").unwrap()) diff --git a/src/grammar.rs b/src/grammar.rs index 9f388c1..3344476 100644 --- a/src/grammar.rs +++ b/src/grammar.rs @@ -1383,7 +1383,7 @@ pub(crate) fn build_grammar<'a>(grammar: &mut Grammar, sset: &'a Arc /// // Create an empty database and load any file provided /// let mut db = Database::new(options); /// db.parse("set.mm".to_string(), vec![]); -/// let stmt_parse = db.stmt_parse(); +/// let stmt_parse = db.stmt_parse_pass(); /// ``` /// /// The parse tree for a given statement can then be obtained through [`StmtParse::get_formula`]. diff --git a/src/grammar_tests.rs b/src/grammar_tests.rs index f555329..abea51f 100644 --- a/src/grammar_tests.rs +++ b/src/grammar_tests.rs @@ -44,7 +44,7 @@ fn test_db_stmt_parse() { let mut db = mkdb(GRAMMAR_DB); let sset = db.parse_result().clone(); let grammar = db.grammar_pass().clone(); - let stmt_parse = db.stmt_parse().clone(); + let stmt_parse = db.stmt_parse_pass().clone(); assert!(sset.parse_diagnostics().is_empty()); assert!(grammar.diagnostics().is_empty()); assert!(stmt_parse.diagnostics().is_empty()); @@ -53,7 +53,7 @@ fn test_db_stmt_parse() { #[test] fn test_db_formula() { let mut db = mkdb(GRAMMAR_DB); - let stmt_parse = db.stmt_parse().clone(); + let stmt_parse = db.stmt_parse_pass().clone(); let names = db.name_pass().clone(); { let sref = db.statement("ax-com").unwrap(); @@ -112,7 +112,7 @@ const GRAMMAR_DB_32: &[u8] = b" #[test] fn test_db_32_formula() { let mut db = mkdb(GRAMMAR_DB_32); - let stmt_parse = db.stmt_parse().clone(); + let stmt_parse = db.stmt_parse_pass().clone(); let names = db.name_pass().clone(); { let sref = db.statement("check").unwrap(); @@ -155,7 +155,7 @@ const GARDEN_PATH_DB: &[u8] = b" fn test_garden_path_1() { let mut db = mkdb(GARDEN_PATH_DB); let sset = db.parse_result().clone(); - let stmt_parse = db.stmt_parse().clone(); + let stmt_parse = db.stmt_parse_pass().clone(); let names = db.name_pass().clone(); assert!(sset.parse_diagnostics().is_empty()); let sref = db.statement("formula1").unwrap(); @@ -171,7 +171,7 @@ fn test_garden_path_1() { #[test] fn test_garden_path_2() { let mut db = mkdb(GARDEN_PATH_DB); - let stmt_parse = db.stmt_parse().clone(); + let stmt_parse = db.stmt_parse_pass().clone(); let names = db.name_pass().clone(); let sref = db.statement("formula2").unwrap(); let formula = stmt_parse.get_formula(&sref).unwrap(); @@ -188,7 +188,7 @@ fn test_garden_path_2() { #[test] fn test_garden_path_3() { let mut db = mkdb(GARDEN_PATH_DB); - let stmt_parse = db.stmt_parse().clone(); + let stmt_parse = db.stmt_parse_pass().clone(); let names = db.name_pass().clone(); let sref = db.statement("formula3").unwrap(); let formula = stmt_parse.get_formula(&sref).unwrap(); diff --git a/src/main.rs b/src/main.rs index 32bd7e7..970d424 100644 --- a/src/main.rs +++ b/src/main.rs @@ -103,7 +103,7 @@ fn main() { } if matches.is_present("verify_parse_stmt") { - db.stmt_parse(); + db.stmt_parse_pass(); db.verify_parse_stmt(); } From 25cf85a7979cf32cdd184c85ad2d53433d8273ca Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Thu, 14 Oct 2021 23:27:52 -0400 Subject: [PATCH 9/9] pass db around instead of nset/sset --- src/database.rs | 17 +++--- src/grammar.rs | 152 ++++++++++++++++++++++++++---------------------- 2 files changed, 90 insertions(+), 79 deletions(-) diff --git a/src/database.rs b/src/database.rs index ec79f49..06e0d6d 100644 --- a/src/database.rs +++ b/src/database.rs @@ -509,6 +509,7 @@ impl Database { /// Returns the name to definition lookup table. /// Panics if [`Database::name_pass`] was not previously called. + #[inline] #[must_use] pub fn name_result(&self) -> &Arc { self.nameset.as_ref().unwrap() @@ -539,6 +540,7 @@ impl Database { /// /// All logical properties of the database (as opposed to surface syntactic /// properties) can be obtained from this object. + #[inline] #[must_use] pub fn scope_result(&self) -> &Arc { self.scopes.as_ref().unwrap() @@ -570,6 +572,7 @@ impl Database { /// /// This is an optimized verifier which returns no useful information other /// than error diagnostics. It does not save any parsed proof data. + #[inline] #[must_use] pub fn verify_result(&self) -> &Arc { self.verify.as_ref().unwrap() @@ -590,6 +593,7 @@ impl Database { /// Returns the root node of the outline. /// Panics if [`Database::outline_pass`] was not previously called. + #[inline] #[must_use] pub fn outline_result(&self) -> &Arc { self.outline.as_ref().unwrap() @@ -601,11 +605,7 @@ impl Database { self.name_pass(); self.scope_pass(); time(&self.options.clone(), "grammar", || { - let parse = self.parse_result(); - let name = self.name_result(); - let mut grammar = Grammar::default(); - grammar::build_grammar(&mut grammar, parse, name); - self.grammar = Some(Arc::new(grammar)); + self.grammar = Some(Arc::new(Grammar::new(self))); }) } self.grammar_result() @@ -613,6 +613,7 @@ impl Database { /// Returns the grammar. /// Panics if [`Database::grammar_pass`] was not previously called. + #[inline] #[must_use] pub fn grammar_result(&self) -> &Arc { self.grammar.as_ref().unwrap() @@ -638,12 +639,14 @@ impl Database { /// Returns the statements parsed using the grammar. /// Panics if [`Database::stmt_parse`] was not previously called. + #[inline] #[must_use] pub fn stmt_parse_result(&self) -> &Arc { self.stmt_parse.as_ref().unwrap() } /// A getter method which does not build the outline + #[inline] #[must_use] pub const fn get_outline(&self) -> Option<&Arc> { self.outline.as_ref() @@ -687,9 +690,7 @@ impl Database { /// Dump the grammar of this database. pub fn print_grammar(&self) { time(&self.options, "print_grammar", || { - let name = self.name_result(); - let grammar = self.grammar_result(); - grammar.dump(name); + self.grammar_result().dump(self); }) } diff --git a/src/grammar.rs b/src/grammar.rs index 3344476..38fc580 100644 --- a/src/grammar.rs +++ b/src/grammar.rs @@ -291,8 +291,8 @@ impl GrammarNode { } } -struct GrammarNodeDebug<'a>(&'a GrammarNode, &'a Nameset); -impl fmt::Debug for GrammarNodeDebug<'_> { +struct GrammarNodeRef<'a>(&'a GrammarNode, &'a Nameset); +impl fmt::Debug for GrammarNodeRef<'_> { /// Lists the contents of the grammar node fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result { let nset = self.1; @@ -352,18 +352,20 @@ impl fmt::Debug for GrammarNodeDebug<'_> { } } -struct GrammarNodeIdDebug<'a>(&'a Grammar, NodeId, &'a Nameset); -impl fmt::Debug for GrammarNodeIdDebug<'_> { +struct GrammarNodeIdRef<'a> { + grammar: &'a Grammar, + node_id: NodeId, + nset: &'a Nameset, +} + +impl fmt::Debug for GrammarNodeIdRef<'_> { /// Lists the contents of the grammar node, given the grammar and a node id fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result { - let grammar = self.0; - let node_id = self.1; - let nset = self.2; write!( f, "{}: {:?}", - node_id, - GrammarNodeDebug(&grammar.nodes.0[node_id], nset) + self.node_id, + GrammarNodeRef(&self.grammar.nodes.0[self.node_id], self.nset) ) } } @@ -640,7 +642,7 @@ impl Grammar { from_typecode: TypeCode, to_typecode: TypeCode, label: Label, - nset: &Nameset, + db: &Database, ) -> Result<(), Diagnostic> { let len = self.nodes.len(); for node_id in 0..len { @@ -651,7 +653,7 @@ impl Grammar { None => { // No branch exist for the converted type: create one, with a leaf label. debug!("Type Conv adding to {} node id {}", node_id, next_node_id); - debug!("{:?}", GrammarNodeIdDebug(self, node_id, nset)); + debug!("{:?}", self.node_id(db, node_id)); let mut leaf_label = ref_next_node.leaf_label; leaf_label.insert(0, Reduce::new(label, 1)); self.add_branch( @@ -671,11 +673,8 @@ impl Grammar { "Type Conv copying to {} node id {}", next_node_id, existing_next_node.next_node_id ); - debug!("{:?}", GrammarNodeIdDebug(self, next_node_id, nset)); - debug!( - "{:?}", - GrammarNodeIdDebug(self, existing_next_node.next_node_id, nset) - ); + debug!("{:?}", self.node_id(db, next_node_id)); + debug!("{:?}", self.node_id(db, existing_next_node.next_node_id)); let existing_next_node_id = existing_next_node.next_node_id; self.nodes .copy_branches( @@ -717,15 +716,15 @@ impl Grammar { &mut self, add_from_node_id: NodeId, add_to_node_id: NodeId, - nset: &Nameset, + db: &Database, mut stored_reduces: ReduceVec, make_final: F, ) where F: FnOnce(&ReduceVec, TypeCode) -> NextNode + Copy, { debug!("Clone {} to {}", add_from_node_id, add_to_node_id); - debug!("{:?}", GrammarNodeIdDebug(self, add_from_node_id, nset)); - debug!("{:?}", GrammarNodeIdDebug(self, add_to_node_id, nset)); + debug!("{:?}", self.node_id(db, add_from_node_id)); + debug!("{:?}", self.node_id(db, add_to_node_id)); let map = &self.get_branch(add_from_node_id).clone(); // can we prevent cloning here? for &stype in &[SymbolType::Constant, SymbolType::Variable] { if stype == SymbolType::Variable { @@ -795,7 +794,7 @@ impl Grammar { self.clone_branches( next_node.next_node_id, new_next_node_id, - nset, + db, new_stored_reduces, make_final, ); @@ -838,7 +837,7 @@ impl Grammar { to_node: NodeId, symbol: Symbol, stype: SymbolType, - nset: &Nameset, + db: &Database, ) -> NodeId { let next_node_id_from_root = self .nodes @@ -853,7 +852,7 @@ impl Grammar { self.clone_branches( next_node_id_from_root, new_node_id, - nset, + db, ReduceVec::new(), |rv, t| { node_from_root @@ -881,7 +880,7 @@ impl Grammar { &mut self, prefix: &[Token], shadows: &[Token], - nset: &Nameset, + db: &Database, names: &mut NameReader<'_>, ) -> Result<(), Diagnostic> { let mut node_id = self.root; @@ -894,7 +893,11 @@ impl Grammar { } // TODO(tirix): use https://rust-lang.github.io/rfcs/2497-if-let-chains.html once it's out! if let GrammarNode::Branch { map } = self.nodes.get(node_id) { - let prefix_symbol = nset.lookup_symbol(prefix[index].as_ref()).unwrap().atom; + let prefix_symbol = db + .name_result() + .lookup_symbol(prefix[index].as_ref()) + .unwrap() + .atom; let next_node = map .get(&(SymbolType::Constant, prefix_symbol)) .expect("Prefix cannot be parsed!"); @@ -940,7 +943,7 @@ impl Grammar { .next_node(shadowing_atom, shadowing_stype) { Some(next_node) => next_node.next_node_id, - None => self.expand_tree(add_from_node_id, shadowing_atom, shadowing_stype, nset), + None => self.expand_tree(add_from_node_id, shadowing_atom, shadowing_stype, db), } } @@ -963,13 +966,7 @@ impl Grammar { }; match self.nodes.get(add_from_node_id) { GrammarNode::Branch { .. } => { - self.clone_branches( - add_from_node_id, - node_id, - nset, - ReduceVec::new(), - make_final, - ); + self.clone_branches(add_from_node_id, node_id, db, ReduceVec::new(), make_final); } GrammarNode::Leaf { reduce, .. } => { let rv = single_reduce(*reduce); @@ -1000,12 +997,12 @@ impl Grammar { /// ` fn handle_commands( &mut self, - sset: &SegmentSet, - nset: &Nameset, + db: &Database, names: &mut NameReader<'_>, type_conversions: &[(TypeCode, TypeCode, Label)], ) -> Result<(), (StatementAddress, Diagnostic)> { - for (address, command) in sset.parser_commands() { + let nset = db.name_result(); + for (address, command) in db.parse_result().parser_commands() { assert!(!command.is_empty(), "Empty parser command!"); if &command[0].as_ref() == b"syntax" { if command.len() == 4 && &command[2].as_ref() == b"as" { @@ -1027,7 +1024,7 @@ impl Grammar { .expect("'=>' not present in 'garden_path' command!"); let (prefix, shadows) = command.split_at(split_index); if let Err(diag) = - self.handle_common_prefixes(&prefix[1..], &shadows[1..], nset, names) + self.handle_common_prefixes(&prefix[1..], &shadows[1..], db, names) { return Err((address, diag)); } @@ -1036,7 +1033,7 @@ impl Grammar { if &command[0].as_ref() == b"type_conversions" { for (from_typecode, to_typecode, label) in type_conversions { if let Err(diag) = - self.perform_type_conversion(*from_typecode, *to_typecode, *label, nset) + self.perform_type_conversion(*from_typecode, *to_typecode, *label, db) { return Err((address, diag)); } @@ -1246,10 +1243,18 @@ impl Grammar { } /// Lists the contents of the grammar's parse table. This can be used for debugging. - pub fn dump(&self, nset: &Nameset) { + pub fn dump(&self, db: &Database) { println!("Grammar tree has {:?} nodes.", self.nodes.len()); for i in 0..self.nodes.len() { - println!("{:?}", GrammarNodeIdDebug(self, i, nset)); + println!("{:?}", self.node_id(db, i)); + } + } + + fn node_id<'a>(&'a self, db: &'a Database, node_id: NodeId) -> GrammarNodeIdRef<'a> { + GrammarNodeIdRef { + grammar: self, + node_id, + nset: db.name_result(), } } @@ -1329,42 +1334,47 @@ impl Grammar { } } -/// Called by [`crate::Database`] to build the grammar from the syntax axioms in the database. -/// -/// The provided `sset`, and `nset` shall be the result of previous phases over the database. -/// The provided `grammar` will be updated with the results of the grammar build. -/// The grammar can then be used to parse the statements of the database (see [`parse_statements`]), -/// or to parse a single statement. -/// Use [`Grammar::default`] to get an initial state. -pub(crate) fn build_grammar<'a>(grammar: &mut Grammar, sset: &'a Arc, nset: &Nameset) { - // Read information about the grammar from the parser commands - grammar.initialize(sset, nset); - grammar.root = grammar.nodes.create_branch(); - - let mut names = NameReader::new(nset); - let mut type_conversions = Vec::new(); - - // Build the initial grammar tree, just form syntax axioms and floats. - let segments = sset.segments(); - assert!(!segments.is_empty(), "Parse returned no segment!"); - for segment in &segments { - for sref in *segment { - if let Err(diag) = match sref.statement_type() { - StatementType::Axiom => { - grammar.add_axiom(&sref, nset, &mut names, &mut type_conversions) +impl Grammar { + /// Called by [`crate::Database`] to build the grammar from the syntax axioms in the database. + /// + /// The provided `sset`, and `nset` shall be the result of previous phases over the database. + /// The provided `grammar` will be updated with the results of the grammar build. + /// The grammar can then be used to parse the statements of the database (see [`parse_statements`]), + /// or to parse a single statement. + /// Use [`Grammar::default`] to get an initial state. + pub(crate) fn new(db: &Database) -> Grammar { + let mut grammar = Grammar::default(); + let sset = db.parse_result(); + let nset = db.name_result(); + // Read information about the grammar from the parser commands + grammar.initialize(sset, nset); + grammar.root = grammar.nodes.create_branch(); + + let mut names = NameReader::new(nset); + let mut type_conversions = Vec::new(); + + // Build the initial grammar tree, just form syntax axioms and floats. + let segments = sset.segments(); + assert!(!segments.is_empty(), "Parse returned no segment!"); + for segment in &segments { + for sref in *segment { + if let Err(diag) = match sref.statement_type() { + StatementType::Axiom => { + grammar.add_axiom(&sref, nset, &mut names, &mut type_conversions) + } + StatementType::Floating => grammar.add_floating(&sref, nset, &mut names), + _ => Ok(()), + } { + grammar.diagnostics.insert(sref.address(), diag); } - StatementType::Floating => grammar.add_floating(&sref, nset, &mut names), - _ => Ok(()), - } { - grammar.diagnostics.insert(sref.address(), diag); } } - } - // Post-treatement (type conversion and garden paths) as instructed by $j parser commands - if let Err((address, diag)) = grammar.handle_commands(sset, nset, &mut names, &type_conversions) - { - grammar.diagnostics.insert(address, diag); + // Post-treatement (type conversion and garden paths) as instructed by $j parser commands + if let Err((address, diag)) = grammar.handle_commands(db, &mut names, &type_conversions) { + grammar.diagnostics.insert(address, diag); + } + grammar } }