# `Tptp.Splitter`
[🔗](https://github.com/jcschuster/tptp/blob/v0.1.3/lib/tptp/splitter.ex#L1)

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_word` for `fof`, `inference`
    and `file`, since `fof(fof, axiom, p).` and `fof(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.

# `result`

```elixir
@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.

# `inputs`

```elixir
@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]

# `next_input`

```elixir
@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

# `stream_inputs`

```elixir
@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]

---

*Consult [api-reference.md](api-reference.md) for complete listing*