Divides a token stream into Tptp.Input records: one statement, one language,
one token list with keywords resolved.
Responsibility
Tptp.Lexer already terminates a statement at a . occurring at bracket depth
zero, since it tracks depth in order to identify those. What remains, and what
this module owns, is everything determined by a token's position:
- Keyword resolution. The lexer emits
lower_wordforfof,inferenceandfile, sincefof(fof, axiom, p).andfof(a, file, p).are both well formed and a spelling-based rule would reject them. Only position disambiguates, and only this module observes position. - Language identification. The first token names the language, so it is available without parsing.
- Statement-structure diagnostics. An input whose first token is not a language keyword is reported here, with a message naming both the token found and those expected, and passed on unparsed rather than submitted to the grammar for a less specific error.
Division on tokens rather than bytes is required: 'foo.bar', 1.5,
% a comment. and <.> each contain a . that does not terminate a statement.
Promotions
A lower_word at position zero becomes kw_thf, kw_tff, kw_tcf, kw_fof,
kw_cnf, kw_tpi or kw_include on spelling alone, since position zero of a
<TPTP_input> admits only those seven.
inference, introduced and file become kw_inference, kw_introduced and
kw_file only when the following token is (, since <inference_record>,
<internal_source> and <file_source> each apply the keyword immediately.
Elsewhere the word remains a lower_word, and <atomic_word> in the grammar
admits the promoted categories, so a formula named inference parses.
$thf, $tff, $fof, $cnf, $fot and $let become dw_* under the same
condition and for the same reason: <formula_data> and <thf_let> always apply
them, and elsewhere they are ordinary <dollar_word>s.
Limits of recovery
A statement terminates at a . observed at bracket depth zero. Input that leaves
a bracket open — an unterminated quoted atom consuming its own ), for instance
— keeps the depth above zero, so subsequent . characters are read as parts of a
term rather than as terminators, and following statements are absorbed into the
unterminated one. test/fixtures/regression/cascade.p covers this.
Resynchronising on a . at end of line preceding a line beginning with a
language keyword would recover in most cases and is not done, since it is an
assumption about layout and a formula may legally be laid out that way. Division
remains exact. The obligation this module accepts instead is to report the cause
rather than its consequences: the first diagnostic on such input is the
unterminated quote, at the position where it opened.
Streaming
stream_inputs/2 is the primitive and holds one statement at a time; inputs/2
is the eager form. Each Tptp.Input carries its own diagnostics, so nothing is
lost by taking the streaming path.
Summary
Functions
Every input in a source, eagerly, with its comments and diagnostics.
Split the next input starting at offset.
Every input in a source, lazily, one statement at a time.
Types
@type result() :: {:input, Tptp.Input.t(), non_neg_integer(), [Tptp.Lexer.comment()]} | {:eof, non_neg_integer(), [Tptp.Lexer.comment()], [Tptp.Diagnostic.t()]}
One call's worth of splitting.
:input carries the statement and the offset to resume from; :eof carries the
diagnostics raised after the last statement, which have no input to belong to.
Both carry the comments seen along the way, which are a side channel in both
stages and never enter the token stream.
Functions
@spec inputs(binary(), Tptp.Span.file_id()) :: {[Tptp.Input.t()], [Tptp.Lexer.comment()], [Tptp.Diagnostic.t()]}
Every input in a source, eagerly, with its comments and diagnostics.
The diagnostic list is the union of every input's own diagnostics and those
raised after the last one, flattened into reading order — convenient for a
caller holding the whole file, and redundant with Tptp.Input.diagnostics by
design so that stream_inputs/2 loses nothing.
This holds the entire token stream in memory. Use stream_inputs/2 for anything
large; see Tptp.Lexer for why that distinction is not academic.
iex> {inputs, _comments, []} = Tptp.Splitter.inputs("fof(a,axiom,p). include('b.ax').")
iex> Enum.map(inputs, & &1.language)
[:fof, :include]@spec next_input(binary(), non_neg_integer(), Tptp.Span.file_id()) :: result()
Split the next input starting at offset.
file is stamped into any diagnostic's span; it is the id under which the caller
registered this source, and defaults to zero for a single-file split.
iex> {:input, input, next, []} = Tptp.Splitter.next_input("fof(a,axiom,p). fof(b,axiom,q).", 0)
iex> {input.language, input.offset, input.length}
{:fof, 0, 15}
iex> next
15@spec stream_inputs(binary(), Tptp.Span.file_id()) :: Enumerable.t()
Every input in a source, lazily, one statement at a time.
The stream yields Tptp.Input structs, each carrying its own diagnostics.
Comments and any diagnostics raised after the last statement are not observable
through this path; a caller that needs them wants inputs/2 and has a file small
enough to afford it.
iex> "fof(a,axiom,p). cnf(b,axiom,q). thf(c,type,f: $i)."
...> |> Tptp.Splitter.stream_inputs()
...> |> Stream.map(& &1.language)
...> |> Enum.take(2)
[:fof, :cnf]