# Tptp v0.1.3 - Table of Contents

> A faithful, span-carrying parser, linter and printer for the TPTP language.

## Pages

- [tptp](readme.md)
- [Corpus report](corpus.md)
- [Type application census](census.md)
- [Findings: what the parse failures were hiding](findings.md)
- [Changelog](changelog.md)
- [NOTICE](notice.md)
- [LICENSE](license.md)

## Modules

- [Tptp.Checks.NoDynamicAtoms](Tptp.Checks.NoDynamicAtoms.md): ## Basics

- Reading a file
  - [Tptp](Tptp.md): A span-preserving reader for the TPTP language.
  - [Tptp.File](Tptp.File.md): A TPTP file as read: its statements, its comments and its diagnostics.
  - [Tptp.Node](Tptp.Node.md): A node of the concrete syntax tree.
  - [Tptp.Query](Tptp.Query.md): Properties of a file or unit, determined before further processing.
  - [Tptp.Statement](Tptp.Statement.md): The two forms a parsed TPTP statement takes.
  - [Tptp.Statement.Annotated](Tptp.Statement.Annotated.md): An annotated formula: `fof(name, role, formula, source, info).`
  - [Tptp.Statement.Include](Tptp.Statement.Include.md): An include directive: `include('Axioms/SET007+0.ax', [a, b], space).`
  - [Tptp.Unit](Tptp.Unit.md): A root file together with everything its `include` directives reach.

- Analysis
  - [Tptp.Analysis](Tptp.Analysis.md): The file, its diagnostics, the symbol table and the dialect, from one traversal.
  - [Tptp.Analyzer](Tptp.Analyzer.md): A named producer of diagnostics over a `Tptp.Analysis`.

- Stages
  - [Tptp.Input](Tptp.Input.md): One unparsed TPTP statement: its language, its tokens and where it came from.
  - [Tptp.Lexer](Tptp.Lexer.md): Tokenises TPTP source, one statement per call.
  - [Tptp.Parser](Tptp.Parser.md): Parses the tokens of one statement into a `Tptp.Statement`.
  - [Tptp.Splitter](Tptp.Splitter.md): Divides a token stream into `Tptp.Input` records: one statement, one language,
one token list with keywords resolved.
  - [Tptp.Token](Tptp.Token.md): The terminal vocabulary of the TPTP grammar.

- Diagnostics
  - [Tptp.Diagnostic](Tptp.Diagnostic.md): A single observation about the input.
  - [Tptp.Error](Tptp.Error.md): Raised by the `!` variants of the public API, carrying the diagnostics.
  - [Tptp.Span](Tptp.Span.md): A byte range within a file.

- Includes
  - [Tptp.Include](Tptp.Include.md): Resolves `include` directives, constructing the file graph underlying a
`Tptp.Unit`.
  - [Tptp.Resolver](Tptp.Resolver.md): The behaviour by which an `include` name is resolved to bytes.
  - [Tptp.Resolver.Cascade](Tptp.Resolver.Cascade.md): Tries each of a list of resolvers, in order, and takes the first that answers.
  - [Tptp.Resolver.Fs](Tptp.Resolver.Fs.md): Resolves an `include` against the local filesystem.
  - [Tptp.Resolver.Http](Tptp.Resolver.Http.md): Fetches from tptp.org over HTTPS, through a local cache.
  - [Tptp.Resolver.Map](Tptp.Resolver.Map.md): Resolves from an in-memory map of name to contents.
  - [Tptp.Resolver.None](Tptp.Resolver.None.md): Records an `include` and does not follow it.

- Lint
  - [Tptp.Lint](Tptp.Lint.md): The `:==` well-formedness conditions, and the conditions requiring more than one
statement.
  - [Tptp.Lint.Collect](Tptp.Lint.Collect.md): Constructs the symbol table and the dialect feature set during the traversal.
  - [Tptp.Lint.Context](Tptp.Lint.Context.md): The position of a node within the statement being traversed.
  - [Tptp.Lint.Rule](Tptp.Lint.Rule.md): The behaviour implemented by a lint rule.
  - [Tptp.Lint.Rules.AtomTyping](Tptp.Lint.Rules.AtomTyping.md): A `type`-role statement that does not declare a type, or a typing under another
role.
  - [Tptp.Lint.Rules.Conjecture](Tptp.Lint.Rules.Conjecture.md): A file stating no conjecture, or more than one.
  - [Tptp.Lint.Rules.Declaration](Tptp.Lint.Rules.Declaration.md): A symbol used without a declaration, in a dialect that has no default typing.
  - [Tptp.Lint.Rules.DefinedWord](Tptp.Lint.Rules.DefinedWord.md): A `$`-word outside the vocabularies named by the `:==` conditions.
  - [Tptp.Lint.Rules.DuplicateName](Tptp.Lint.Rules.DuplicateName.md): Two statements sharing a name.
  - [Tptp.Lint.Rules.Parent](Tptp.Lint.Rules.Parent.md): An inference record naming a parent absent from the unit.
  - [Tptp.Lint.Rules.Rank1](Tptp.Lint.Rules.Rank1.md): A type quantifier in a position admitting only rank-1 polymorphism.
  - [Tptp.Lint.Rules.Role](Tptp.Lint.Rules.Role.md): A formula role outside those named by the `:==` conditions.
  - [Tptp.Lint.Table](Tptp.Lint.Table.md): The information accumulated by the traversal, for rules requiring more than one
statement.

- Printers
  - [Tptp.Printer.Canonical](Tptp.Printer.Canonical.md): Prints a concrete syntax tree to TPTP, deterministically and without comments.
  - [Tptp.Printer.Format](Tptp.Printer.Format.md): Rewrites a file's layout without altering its token sequence.
  - [Tptp.Printer.Pretty](Tptp.Printer.Pretty.md): Prints a CST to a chosen width, breaking lines where a formula is too long to fit.
  - [Tptp.Printer.Shapes](Tptp.Printer.Shapes.md): How each node kind is spelled, derived from the grammar.
  - [Tptp.Printer.Spacing](Tptp.Printer.Spacing.md): Determines the white space between two adjacent tokens.

- SZS
  - [Tptp.Szs](Tptp.Szs.md): Reads and writes the SZS result lines that ATP systems emit around their output.
  - [Tptp.Szs.Ontology](Tptp.Szs.Ontology.md): The SZS ontologies: their 112 status values, the 3 ontologies
the values belong to, and the `isa` hierarchy among them.
  - [Tptp.Szs.Page](Tptp.Szs.Page.md): What <https://szs.tptp.org> says about the SZS values and the BNF does not:
their mnemonics and their descriptions.

- Generated from the BNFs
  - [Tptp.Bnf](Tptp.Bnf.md): Reader for the two upstream TPTP World BNF files, `SyntaxBNF` and
`SZSOntology.bnf`.
  - [Tptp.Bnf.Generator](Tptp.Bnf.Generator.md): Translates the vendored `SyntaxBNF` into `src/tptp_parser.yrl`.
  - [Tptp.Bnf.Oracle](Tptp.Bnf.Oracle.md): Renders `Tptp.Bnf.OracleTable`, the regex transcription of the BNF's token layer.
  - [Tptp.Bnf.Rule](Tptp.Bnf.Rule.md): One rule read out of the vendored `SyntaxBNF` file.
  - [Tptp.Bnf.Szs](Tptp.Bnf.Szs.md): Translates the vendored `SZSOntology.bnf` into `Tptp.Szs.Ontology`.
  - [Tptp.Bnf.Vocabulary](Tptp.Bnf.Vocabulary.md): The closed vocabularies of the TPTP `:==` semantic layer.

## Mix Tasks

- [mix tptp.census](Mix.Tasks.Tptp.Census.md): 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.
- [mix tptp.corpus](Mix.Tasks.Tptp.Corpus.md): Reads every problem and axiom file of a local TPTP library and writes a report.
- [mix tptp.format](Mix.Tasks.Tptp.Format.md): Reformat TPTP files in place.
- [mix tptp.gen](Mix.Tasks.Tptp.Gen.md): Regenerates the committed sources from the two vendored TPTP World BNFs,
`priv/bnf/SyntaxBNF-v*` and `priv/bnf/SZSOntology.bnf`.
- [mix tptp.lint](Mix.Tasks.Tptp.Lint.md): Read TPTP files and print their diagnostics.