SMM stores the state of a Metamath database as an instance of the MMOM.Database class.
A database represents a sequence of zero or more individually well-formed statements of the Metamath language.
A database can legally represent states which are jointly invalid, such as a database containing a proof but not some of the steps the proof depends on.
Individual statements are represented by instances of MMOM.Statement.
A statement is born into a database, and thereafter is not (observably) modified except to remove it.
Databases are modified by calling methods on the database to insert statements, remove statements, and replace statements with modified versions.
Statements in SMM are the statements defined in the Metamath specification, plus SMM-specific statement types COMMENT, INCLUDE, BOGUS, METACOMMENT, and EOF;
these statement types have no effect on the mathematical content of the database, but serve to hold text during parsing that does not naturally correspond to any statement.
SMM always knows the character data corresponding to a statement.
It is impossible to create a statement without making some decision about the whitespace that would be used to write that statement to a file.
Statements own their leading whitespace.
Whitespace at the end of the file is owned by the special EOF statement.
Comments are treated as whitespace if found inside statements, but are promoted to statements in their own right if they appear between statements.
import { parseSync } from 'smm';
database = parseSync('filename', '$( file content $)');Call parseSync with two strings to parse a database which is already loaded as a string.
Returns a MMOM.Database instance.
The filename will be used for error messages (also, $[ will ignore that filename but give errors for all others).
Never throws, returns errors in the database object.
database = parseSync('file1',
new Map().set('file1','$[ file2 $]').set('file2',''));The second argument to parseSync may be a Map if multiple files are used.
database = parseSync('file1', filename => 'foo');The second argument to parseSync may be a function, which will be passed a file name and must return a string or throw an exception.
Exceptions will be wrapped into failed-to-read errors.
import { parseAsync } from 'smm'
promise = parseAsync('file1', filename =>
fetch(filename).then(rpy => rpy.text())).then(db => ... );parseAsync functions like parseSync except that only the function form is supported, the function is expected to return a promise, and a promise is returned at the end.
As parseSync never throws, the promise returned from parseAsync never rejects.
The parsing process will attempt to recover from arbitrary errors in the source, and the resulting database will contain only valid statements.
Some statements will be repaired, those which cannot will be turned into BOGUS type statements.
However, a database with parsing errors cannot be modified, due to the difficulty in updating the parsing error data after changes.
text = database.textConvert a database back into text, to save in a file.
Does not support $[ $].
count = database.statementCount;
statement = database.statement(42);A database has a statementCount property and a statement reader method.
Currently all database access is mediated by statement indices.
This is problematic as when an insert or delete is done, statement indices are invalidated.
It is likely that a future version of SMM will use another technique to record statement positions;
statement(N) will still be supported, but will suffer an O(n) penalty to build an index.
Statements are immutable. To change a database, splice in new statements; do not attempt to modify existing ones.
import { MMOMStatement } from 'smm';
statement.type === MMOMStatement.OPEN;
statement.type === MMOMStatement.CLOSE;
statement.type === MMOMStatement.CONSTANT;
statement.type === MMOMStatement.VARIABLE;
statement.type === MMOMStatement.DISJOINT;
statement.type === MMOMStatement.ESSENTIAL;
statement.type === MMOMStatement.FLOATING;
statement.type === MMOMStatement.AXIOM;
statement.type === MMOMStatement.PROVABLE;Statements have a type property, which is equal to the constants above for real statements. Fake statements also have types, but their number and roles are not currently considered stable.
string = statement.label;
arrayString = statement.math;
arrayString = statement.proof;Accessors for the fundamental parts of a statement.
math and proof may be null on statement types for which they are not applicable;
when they are applicable, they will always be present even if empty.
text = statement.raw; // the while statement
text = statement.mathText; // inside $acefpv $=.
text = statement.proofText; // inside $= $.
text = statement.commentText; // inside $( $), COMMENT onlyAccessors for portions of a statement, identified but with whitespace and embedded comments preserved.
index = statement.index;
database = statement.database;
statement === database.statement(index);A statement which is in a database knows its database and index.
database.replaceStatements(3,4,'');
database.replaceStatements(2,2,' $( A NEW COMMENT $)');
database.replaceMathString(database.statement(2), ' 2 + 2 ');
database.replaceProofString(database.statement(2), ' ? ');Databases can be modified by replacing a run of statements with a new run of statements. Several rules apply to ensure that the new database can still be parsed.
This module calculates scopes and symbol tables.
let sym = database.scoper.lookup('ruc');
database.verifier.errors(sym.labelled);Symbol table entries are returned as objects with slots for different types of usage of symbols. Currently only labelled (find the statement with this label) has API status.
This is the standard-mode verifier; it does not exploit statement parsing (that works only for set.mm). It implements the common error checking protocol but has no other API.
Metadata from the $t comment can be accessed using the metadata analyzer.
title = database.metadata.param('htmltitle');
andsign = database.metadata.tokenDef('htmldef', '/\\');Both methods return null if not defined.
array_of_errors = database.scoper.errors(statement);
map_of_errors = database.scoper.allErrors;
array_of_errors = database.verifier.errors(statement);
map_of_errors = database.verifier.allErrors;Several analyzers have the capability to generate warnings or errors while analyzing the database.
These analyzers implement a common API: errors fetches a list of errors for a specific statement, allErrors fetches a map with error data for each statement with at least one error.
array_of_errors = database.scanner.errors;Scanner errors are reported differently because they cannot generally be linked to a statement.
process.stdout.write( error.toConsoleString(), 'utf8' );Renders an error as a string containing newlines for human consumption.