One unparsed TPTP statement: its language, its tokens and where it came from.
The name is the BNF's own. <TPTP_input> ::= <annotated_formula> | <include> is
the unit a <TPTP_file> is a sequence of, and it is what Tptp.Splitter hands
to Tptp.Parser — hence Tptp.Input rather than a second Statement, which is
the parsed thing.
Why the language is decided before parsing
Every input begins with one of seven keywords, so the dialect is knowable from
token zero without looking at anything else. Deciding it here buys three things:
an input whose prefix is not a keyword can be reported precisely and skipped
rather than dragged through the grammar for a worse error; a consumer can filter
a 455 MB axiom file down to its include statements without parsing a single
formula; and Tptp.Query.dialect/1 gets its cheapest input for free.
:unknown means exactly that the first token was not one of the seven, and it
always comes with a TPTP0201 or TPTP0202 diagnostic on the input.
Offsets, not spans
Like Tptp.Node, an input stores a bare offset and length. The file id belongs
to the file, not to each of its thousands of statements, so span/2 builds a
Tptp.Span on demand when a diagnostic needs one.
Summary
Types
The TPTP language this input is written in, or :unknown when token zero was
not a language keyword.
One statement's worth of tokens, with the span they cover and the language they open with.
Functions
Whether this input is an include directive.
The language an opening keyword category names.
The keyword categories that open an input, paired with the language they name.
The input's extent, as a span in the file it was read from.
The bytes the input covers, terminating . included.
Types
@type language() :: :thf | :tff | :tcf | :fof | :cnf | :tpi | :include | :unknown
The TPTP language this input is written in, or :unknown when token zero was
not a language keyword.
@type t() :: %Tptp.Input{ diagnostics: [Tptp.Diagnostic.t()], language: language(), length: non_neg_integer(), offset: non_neg_integer(), tokens: [Tptp.Token.t()] }
One statement's worth of tokens, with the span they cover and the language they open with.
Functions
Whether this input is an include directive.
Cheaper and clearer at a call site than matching on the language atom, and it is
the question Tptp.Include asks of every input in a file.
iex> {[input], _comments, _diagnostics} = Tptp.Splitter.inputs("include('a.ax').")
iex> Tptp.Input.include?(input)
true@spec language_for(Tptp.Token.category()) :: language()
The language an opening keyword category names.
iex> Tptp.Input.language_for(:kw_cnf)
:cnf
iex> Tptp.Input.language_for(:lower_word)
:unknown@spec languages() :: [{Tptp.Token.category(), language()}]
The keyword categories that open an input, paired with the language they name.
@spec span(t(), Tptp.Span.file_id()) :: Tptp.Span.t()
The input's extent, as a span in the file it was read from.
The bytes the input covers, terminating . included.
A sub-binary, not a copy.