From c3a5d9f521cc279417519e14ab59d8674aa02c1b Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Thu, 14 Oct 2021 02:58:08 -0400 Subject: [PATCH] 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 | 217 ++++++++++++++++++++++++------------------- 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, 311 insertions(+), 267 deletions(-) diff --git a/src/database.rs b/src/database.rs index 654a603..796827a 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); + 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,