Struct Database

pub struct Database { /* private fields */ }

Master type of database containers.

A variable of type Database holds a database, i.e. an ordered collection of segments and analysis results for that collection. Analysis results are generated lazily for each database, and are invalidated on any edit to the database’s segments. If you need to refer to old analysis results while making a sequence of edits, call Clone::clone on the database first; this is intended to be a relatively cheap operation.

More specifically, cloning a Database object does essentially no work until it is necessary to run an analysis pass on one clone or the other; then if the analysis pass has a result index which is normally updated in place, such as the hash table of statement labels constructed by nameck, that table must be duplicated so that it can be updated for one database without affecting the other.

Implementations

impl Database

pub fn write_stmt_use( &self, label_test: impl Fn(&[u8]) -> bool, out: &mut impl Write, ) -> Result<(), Error>

Writes a stmt_use file to the given writer.

impl Database

pub fn new(options: DbOptions) -> Database

Constructs a new database object representing an empty set of segments.

Use parse to load it with data. Currently this eagerly starts the threadpool, but that may change.

pub fn parse(&mut self, start: String, text: Vec<(String, Vec<u8>)>)

Replaces the content of a database in memory with the parsed content of one or more input files.

To load data from disk files, pass the pathname as start and leave text empty. start and any references arising from file inclusions will be processed relative to the current directory; we may add a base directory option later.

The database object will remember the name and OS modification time of all files read to construct its current state, and will skip rereading them if the modification change has not changed on the next call to parse. If your filesystem has poor modification time granulatity, beware of possible lost updates if you modify a file and the timestamp does not change.

To parse data already resident in program memory, pass an arbitrary name as start and then pass a pair in text mapping that name to the buffer to parse. Any file inclusions found in the buffer can be resolved from additional pairs in text; file inclusions which are not found in text will be resolved on disk relative to the current directory as above (this feature has an uncertain future).

All analysis passes will be invalidated; they will not immediately be rerun, but will be when next requested. If the database is not currently empty, the files loaded are assumed to be similar to the current database content and incremental processing will be used as appropriate.

pub fn name_pass(&mut self) -> &Arc<Nameset>

Calculates and returns the name to definition lookup table.

pub fn name_result(&self) -> &Arc<Nameset>

Returns the name to definition lookup table. Panics if Database::name_pass was not previously called.

pub fn scope_pass(&mut self) -> &Arc<ScopeResult>

Calculates and returns the frames for this database, i.e. the actual logical system.

All logical properties of the database (as opposed to surface syntactic properties) can be obtained from this object.

pub const fn try_scope_result(&self) -> Option<&Arc<ScopeResult>>

Returns the frames for this database, i.e. the actual logical system. Returns None 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.

pub fn scope_result(&self) -> &Arc<ScopeResult>

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.

pub fn verify_pass(&mut self) -> &Arc<VerifyResult>

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.

pub const fn try_verify_result(&self) -> Option<&Arc<VerifyResult>>

Returns verification information for the database. Returns None 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.

pub fn verify_result(&self) -> &Arc<VerifyResult>

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.

pub fn verify_usage_pass(&mut self) -> &Arc<UsageResult>

Calculates and returns axiom usage 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.

pub const fn try_usage_result(&self) -> Option<&Arc<UsageResult>>

Returns axiom usage verification information for the database. Returns None if Database::verify_usage_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.

pub fn typesetting_pass(&mut self) -> &Arc<TypesettingData>

Computes and returns the typesetting data.

pub const fn try_typesetting_result(&self) -> Option<&Arc<TypesettingData>>

Returns the typesetting data. Returns None if Database::typesetting_pass was not previously called.

pub fn typesetting_result(&self) -> &Arc<TypesettingData>

Returns the typesetting data. Panics if Database::typesetting_pass was not previously called.

pub fn outline_pass(&mut self) -> &Arc<Outline>

Computes and returns the root node of the outline.

pub const fn try_outline_result(&self) -> Option<&Arc<Outline>>

Returns the root node of the outline. Panics if Database::outline_pass was not previously called.

pub fn outline_result(&self) -> &Arc<Outline>

Returns the root node of the outline. Panics if Database::outline_pass was not previously called.

pub fn grammar_pass(&mut self) -> &Arc<Grammar>

Builds and returns the grammar.

pub const fn try_grammar_result(&self) -> Option<&Arc<Grammar>>

Returns the grammar. Returns None if Database::grammar_pass was not previously called.

pub fn grammar_result(&self) -> &Arc<Grammar>

Returns the grammar. Panics if Database::grammar_pass was not previously called.

pub fn stmt_parse_pass(&mut self) -> &Arc<StmtParse>

Parses the statements using the grammar.

pub const fn try_stmt_parse_result(&self) -> Option<&Arc<StmtParse>>

Returns the statements parsed using the grammar. Returns None if Database::stmt_parse_pass was not previously called.

pub fn stmt_parse_result(&self) -> &Arc<StmtParse>

Returns the statements parsed using the grammar. Panics if Database::stmt_parse_pass was not previously called.

pub const fn get_outline(&self) -> Option<&Arc<Outline>>

A getter method which does not build the outline.

pub fn statement(&self, name: &[u8]) -> Option<StatementRef<'_>>

Get a statement by label. Requires: Database::name_pass

pub fn statement_by_label(&self, label: Label) -> Option<StatementRef<'_>>

Get a statement by label atom. Requires: Database::name_pass

pub fn statement_by_address(&self, addr: StatementAddress) -> StatementRef<'_>

Get a statement by address. Panics if the statement does not exist.

pub fn statement_source_name(&self, addr: StatementAddress) -> &str

Get the name of the source file for a given statement.

pub fn statements( &self, ) -> impl DoubleEndedIterator<Item = StatementRef<'_>> + Clone + '_

Iterates over all the statements

pub fn statements_range( &self, range: impl RangeBounds<Label>, ) -> impl DoubleEndedIterator<Item = StatementRef<'_>> + Clone + '_

Iterates over the statements in a given range.

pub fn statements_range_address( &self, range: impl RangeBounds<StatementAddress>, ) -> impl DoubleEndedIterator<Item = StatementRef<'_>> + Clone + '_

Iterates over the statements in a given range.

pub fn cmp_label(&self, left: &Label, right: &Label) -> Option<Ordering>

Compare the database position of two label atoms. Proofs can only reference earlier theorems.

pub fn cmp(&self, left: &[u8], right: &[u8]) -> Option<Ordering>

Compare the database position of two labels. Proofs can only reference earlier theorems.

pub fn cmp_address( &self, left: &StatementAddress, right: &StatementAddress, ) -> Ordering

Compare the database position of two addresses. Proofs can only reference earlier theorems.

pub fn label_typecode(&self, label: Label) -> TypeCode

Returns the typecode for a given label.

pub fn export(&self, stmt: &str)

Export an mmp file for a given statement. Requires: Database::name_pass, Database::scope_pass

pub fn get_proof_tree(&self, sref: StatementRef<'_>) -> Option<ProofTreeArray>

Returns the proof tree for a given database theorem, in the form of a ProofTreeArray

pub fn get_syntax_proof_tree(&self, formula: &Formula) -> ProofTreeArray

Returns the syntax proof tree for a given formula, in the form of a ProofTreeArray

pub fn dump_grammar(&self)

Dump the grammar of this database. Requires: Database::name_pass, Database::grammar_pass

pub fn dump_formula(&self)

Dump the formulas of this database. Requires: Database::name_pass, Database::stmt_parse_pass

pub fn verify_parse_stmt(&self)

Verify that printing the formulas of this database gives back the original formulas. Requires: Database::name_pass, Database::stmt_parse_pass

pub fn print_outline(&self)

Dump the outline of this database. Requires: Database::outline_pass

pub fn print_typesetting(&self)

Dump the typesetting information. Requires: Database::typesetting_pass

pub const fn get_outline_node<'a>( &'a self, sref: StatementRef<'a>, ) -> OutlineNodeRef<'a>

Returns the outline node corresponding to the given statement

pub fn root_outline_node(&self) -> OutlineNodeRef<'_>

Returns the root outline node, at the level of the whole database

pub fn diag_notations(&mut self) -> Vec<(StatementAddress, Diagnostic)>

Collects and returns all errors generated by the passes run.

Currently there is no way to incrementally fetch diagnostics, so this will be a bit slow if there are thousands of errors.

pub fn render_diags<T>( &self, diags: Vec<(StatementAddress, Diagnostic)>, f: impl for<'a> FnOnce(Snippet<'a>) -> T + Copy, ) -> Vec<T>

Convert a list of diagnostics collected by diag_notations to a list of snippets.

impl Database

pub fn write_discouraged(&self, out: &mut impl Write) -> Result<(), Error>

Writes a discouraged file to the given writer.

impl Database

pub fn export_mmp<W: Write>( &self, stmt: StatementRef<'_>, out: &mut W, ) -> Result<(), ExportError>

Export an mmp file for a given statement.

impl Database

pub fn export_mmp_proof_tree<W: Write>( &self, thm_label: &[u8], arr: &ProofTreeArray, out: &mut W, ) -> Result<(), ExportError>

Export an mmp file for a given proof tree.

Panics

The ProofTreeArray must have enable_exprs = true.

impl Database

pub const fn get_outline_node_by_ref( &self, chapter_ref: usize, ) -> OutlineNodeRef<'_>

Returns the outline node with the given internal reference

impl Database

pub fn get_frame(&self, label: Label) -> Option<FrameRef<'_>>

Returns the frame for the given statement label

impl Database

pub fn verify_one<P: ProofBuilder>( &self, builder: &mut P, stmt: StatementRef<'_>, ) -> Result<P::Item, Diagnostic>

Parse a single $p statement, returning the result of the given proof builder, or an error if the proof is faulty

impl Database

pub fn verify_markup( &self, bib2: Option<&Bibliography2>, ) -> Vec<(StatementAddress, Diagnostic)>

Run the verify markup pass on the database. Requires: Database::scope_pass, Database::typesetting_pass

Trait Implementations

impl Clone for Database

fn clone(&self) -> Database

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Comparer<SegmentId> for Database

fn cmp(&self, left: &SegmentId, right: &SegmentId) -> Ordering

Compares two objects, like Ord::cmp, but with additional state data from the comparer that can be used for the ordering.

fn lt(&self, left: &T, right: &T) -> bool

Returns true if the left argument is (strictly) less than the right argument

fn le(&self, left: &T, right: &T) -> bool

Returns true if the left argument is less or equal to the right argument

impl Comparer<StatementAddress> for Database

fn cmp(&self, left: &StatementAddress, right: &StatementAddress) -> Ordering

Compares two objects, like Ord::cmp, but with additional state data from the comparer that can be used for the ordering.

fn lt(&self, left: &T, right: &T) -> bool

Returns true if the left argument is (strictly) less than the right argument

fn le(&self, left: &T, right: &T) -> bool

Returns true if the left argument is less or equal to the right argument

impl Comparer<TokenAddress> for Database

fn cmp(&self, left: &TokenAddress, right: &TokenAddress) -> Ordering

Compares two objects, like Ord::cmp, but with additional state data from the comparer that can be used for the ordering.

fn lt(&self, left: &T, right: &T) -> bool

Returns true if the left argument is (strictly) less than the right argument

fn le(&self, left: &T, right: &T) -> bool

Returns true if the left argument is less or equal to the right argument

impl Debug for Database

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for Database

fn default() -> Self

Returns the “default value” for a type.

impl Drop for Database

fn drop(&mut self)

Executes the destructor for this type.