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

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.

# `language`

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

# `t`

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

# `include?`

```elixir
@spec include?(t()) :: boolean()
```

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

# `language_for`

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

# `languages`

```elixir
@spec languages() :: [{Tptp.Token.category(), language()}]
```

The keyword categories that open an input, paired with the language they name.

# `span`

```elixir
@spec span(t(), Tptp.Span.file_id()) :: Tptp.Span.t()
```

The input's extent, as a span in the file it was read from.

# `text`

```elixir
@spec text(t(), binary()) :: binary()
```

The bytes the input covers, terminating `.` included.

A sub-binary, not a copy.

---

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