# `Tptp.Lint.Collect`
[🔗](https://github.com/jcschuster/tptp/blob/v0.1.3/lib/tptp/lint/collect.ex#L1)

Constructs the symbol table and the dialect feature set during the traversal.

Not a rule. It is applied before the rules at every node and produces the data
read afterwards by the `c:Tptp.Lint.Rule.review/2` callbacks, which is what
allows `Tptp.Lint` to require a single pass.

## Declarations

A `type`-role statement whose formula is an atom typing, such as
`tff(f_decl, type, f: $i > $o).` The subject is recorded as declared and the
right-hand side of the colon is stored verbatim as the declared type. It is not
interpreted.

## Uses

A `constant`, `functor`, `defined_functor` or `system_functor`, or their nullary
counterparts, occurring within a formula — not within a name, role, source or
info field. Never a `variable`: in `X @ a` the head is bound by its quantifier
rather than declared by a `type` statement.

The annotations contain atoms indistinguishable in form from symbols that are not
symbols: `file` in a `<source>` is a keyword and `status(thm)` is a label.
Counting them would report the TSTP vocabulary as undeclared.

An `<ntf_index>` is the second such position. In `{$necessary(#agent)}` the word
`agent` labels a modality rather than denoting a constant of the problem's
signature, and `SYN000^7.p`, the reference example for the syntax, declares no
type for it. The subtree beneath an `ntf_index` is therefore claimed before the
traversal reaches it, and none of it is counted.

## Symbol identity

`'p'` and `p` denote one symbol, since the BNF defines a `<single_quoted>` as the
enclosed atomic word without its quotes. Every key passed to `Tptp.Lint.Table` is
therefore taken from `Tptp.Node.value/1` rather than from `text`. Keying on the
spelling separates `tff(t, type, 'p': $i > $o). tff(a, axiom, p(x)).` into two
entries, producing a spurious undeclared-symbol finding and a missed duplicate
name, and propagates the separation to anything built on
`Tptp.Query.symbols/1`. The same applies to statement names and to the names an
inference record supplies as parents, since `<name> ::= <atomic_word> |
<integer>`.

## Arity

Arity is the length of the application spine, recorded at the application node.
`f(a, b)` is a `fof_plain_term` with a functor and an argument list, so the arity
is the length of that list; `f @ a @ b` is a left-nested application spine, so the
arity is its depth. Both are recorded and neither is evaluated here.

Argument lists differ in shape between dialects, and the difference originates in
the BNF rather than the generator: `<fof_arguments> ::= <fof_term> |
<fof_term>,<fof_arguments>` nests to the right, while `<tff_arguments> ::=
<tff_term><comma_tff_term>*` is flat. `p(x, y, z)` is therefore a two-child node
in FOF and a three-child node in TFF, and counting children directly would give
the FOF form an arity of two. The count recurses through children of the same
kind instead, which is correct for both.

# `known_dollar_word?`

```elixir
@spec known_dollar_word?(binary()) :: boolean()
```

Whether a `$`-word is one the BNF mentions anywhere.

Every `$`-literal in every rule, not only the closed vocabularies: several
reserved words appear beside other symbols rather than alone —
`<ntf_domains_spec> :== $domains <identical> <ntf_domains_value>` — and checking
only the closed lists reports those as unknown.

    iex> Tptp.Lint.Collect.known_dollar_word?("$sum")
    true
    iex> Tptp.Lint.Collect.known_dollar_word?("$wibble")
    false

# `observe`

```elixir
@spec observe(Tptp.Node.t(), Tptp.Lint.Context.t(), Tptp.Lint.Table.t()) ::
  Tptp.Lint.Table.t()
```

Fold one node into the table.

# `typing?`

```elixir
@spec typing?(Tptp.Statement.Annotated.t()) :: boolean()
```

Whether a statement declares a symbol rather than asserting something.

    iex> {:ok, statement, []} = Tptp.Parser.statement_from_string("tff(d, type, f: $i).")
    iex> Tptp.Lint.Collect.typing?(statement)
    true

---

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