Modules
A span-preserving reader for the TPTP language.
The file, its diagnostics, the symbol table and the dialect, from one traversal.
A named producer of diagnostics over a Tptp.Analysis.
Reader for the upstream TPTP SyntaxBNF file.
Translates the vendored SyntaxBNF into src/tptp_parser.yrl.
Renders Tptp.Bnf.OracleTable, the regex transcription of the BNF's token layer.
One rule read out of the vendored SyntaxBNF file.
The closed vocabularies of the TPTP :== semantic layer.
A single observation about the input.
Raised by the ! variants of the public API, carrying the diagnostics.
A TPTP file as read: its statements, its comments and its diagnostics.
Resolves include directives, constructing the file graph underlying a
Tptp.Unit.
One unparsed TPTP statement: its language, its tokens and where it came from.
Tokenises TPTP source, one statement per call.
The :== well-formedness conditions, and the conditions requiring more than one
statement.
Constructs the symbol table and the dialect feature set during the traversal.
The position of a node within the statement being traversed.
The behaviour implemented by a lint rule.
A type-role statement that does not declare a type, or a typing under another
role.
A file stating no conjecture, or more than one.
A symbol used without a declaration, in a dialect that has no default typing.
A $-word outside the vocabularies named by the :== conditions.
Two statements sharing a name.
An inference record naming a parent absent from the unit.
A type quantifier in a position admitting only rank-1 polymorphism.
A formula role outside those named by the :== conditions.
The information accumulated by the traversal, for rules requiring more than one statement.
A node of the concrete syntax tree.
Parses the tokens of one statement into a Tptp.Statement.
Prints a concrete syntax tree to TPTP, deterministically and without comments.
Rewrites a file's layout without altering its token sequence.
Prints a CST to a chosen width, breaking lines where a formula is too long to fit.
How each node kind is spelled, derived from the grammar.
Determines the white space between two adjacent tokens.
Properties of a file or unit, determined before further processing.
The behaviour by which an include name is resolved to bytes.
Tries each of a list of resolvers, in order, and takes the first that answers.
Resolves an include against the local filesystem.
Fetches from tptp.org over HTTPS, through a local cache.
Resolves from an in-memory map of name to contents.
Records an include and does not follow it.
A byte range within a file.
Divides a token stream into Tptp.Input records: one statement, one language,
one token list with keywords resolved.
The two forms a parsed TPTP statement takes.
An annotated formula: fof(name, role, formula, source, info).
An include directive: include('Axioms/SET007+0.ax', [a, b], space).
Reads and writes the SZS result lines that ATP systems emit around their output.
The SZS status values, transcribed from https://szs.tptp.org.
The terminal vocabulary of the TPTP grammar.
A root file together with everything its include directives reach.
Mix Tasks
Read every problem and axiom file of a local TPTP library and count where it
applies a type constructor — list($i), map(A, B), tree @ $i — and in which
dialects.
Reads every problem and axiom file of a local TPTP library and writes a report.
Reformat TPTP files in place.
Regenerates the committed sources from the vendored TPTP BNF at
priv/bnf/SyntaxBNF-v*.
Read TPTP files and print their diagnostics.