A TPTP file as read: its statements, its comments and its diagnostics.
Source retention
Every leaf's text is a sub-binary of source, so the source must outlive the
tree and is retained here. Reading a 4 MB problem therefore costs one 4 MB binary
and a tree of offsets rather than a copy of every symbol. Tptp.detach/1 returns
a copy owning its own binaries, for consumers retaining a small number of
statements from a large file.
Comments
The BNF permits a comment between any two tokens and does not treat comments as white space, so they cannot be placed in the tree without appearing among the children of arbitrary nodes. They are held as an ordered list of spans, which is the form the format-preserving printer requires in order to reattach them by position.
Computed properties
line_index/1 and digest/1 are functions rather than fields. Both are linear in
the size of the source and both are required infrequently — the first to render a
position, the second to key a cache. Callers needing either repeatedly should
retain the result.
Summary
Types
One parsed TPTP file: its source, its statements, its comments and everything said about them.
Functions
Whether anything error-severity was found.
A SHA-256 of the file's bytes, for keying a cache across runs.
Every diagnostic, rendered one per line against a single line index.
The annotated formulae, include directives excluded.
The include directives this file names, in source order.
A line-start index for turning offsets into line and column numbers.
The innermost CST node under offset, or nil.
The statement containing offset, or nil.
Types
@type t() :: %Tptp.File{ bnf_version: binary(), comments: [Tptp.Lexer.comment()], diagnostics: [Tptp.Diagnostic.t()], id: Tptp.Span.file_id(), path: Path.t() | nil, source: binary(), statements: [Tptp.Statement.t()] }
One parsed TPTP file: its source, its statements, its comments and everything said about them.
Functions
Whether anything error-severity was found.
iex> {:ok, file, _diagnostics} = Tptp.from_string("fof(a,axiom,p q).")
iex> Tptp.File.any_errors?(file)
trueA SHA-256 of the file's bytes, for keying a cache across runs.
Pair it with bnf_version — the same bytes read against a different BNF can
produce a different tree, so a cache keyed on content alone will eventually hand
back a CST the current code cannot read.
Every diagnostic, rendered one per line against a single line index.
iex> {:ok, file, _diagnostics} = Tptp.from_string("wibble(a).")
iex> Tptp.File.format_diagnostics(file)
["1:1: error: `wibble` does not start a TPTP statement [TPTP0201]"]@spec formulae(t()) :: [Tptp.Statement.Annotated.t()]
The annotated formulae, include directives excluded.
@spec includes(t()) :: [Tptp.Statement.Include.t()]
The include directives this file names, in source order.
Derived rather than stored, because a second list of the same structs would be a second thing to keep in step.
iex> {:ok, file, []} = Tptp.from_string("fof(a,axiom,p). include('b.ax').")
iex> file |> Tptp.File.includes() |> Enum.map(&Tptp.Statement.Include.path/1)
["b.ax"]@spec line_index(t()) :: Tptp.Span.line_index()
A line-start index for turning offsets into line and column numbers.
O(bytes) to build and independent of the tree, so hold it if you are resolving
more than a handful of positions. format_diagnostics/1 builds one and reuses it
for the whole list, which is the common case.
@spec node_at(t(), non_neg_integer()) :: Tptp.Node.t() | nil
The innermost CST node under offset, or nil.
iex> {:ok, file, []} = Tptp.from_string("fof(a,axiom,p(bcd)).")
iex> Tptp.File.node_at(file, 15).text
"bcd"@spec statement_at(t(), non_neg_integer()) :: Tptp.Statement.t() | nil
The statement containing offset, or nil.
The first half of the editor's incremental path: find the statement under the cursor, reparse just that one, splice it back. Linear in statements, which is what a sorted list costs; a consumer editing a 3 million statement file wants an interval tree of its own, built from these spans.