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

The information accumulated by the traversal, for rules requiring more than one
statement.

## Syntactic content only

A symbol's entry records the unelaborated `Tptp.Node` its type was declared as.
No unification or substitution is performed and `$i` is not interpreted as a
type. The questions asked of `declared_as` are syntactic: whether it contains a
`!>`, how many arrows its spine has. Anything further requires a signature and
belongs to the consumer.

## Keys

Every key — symbol, statement name, inference parent — is a `Tptp.Node.value/1`
rather than a `text`. `'p'` and `p` are one atomic word by the BNF's definition
and therefore one entry, and `name` in a symbol holds the unquoted word. A caller
reporting the spelling has the spans from which to read it.

## Arities

`arities` records every application arity observed for a symbol. No rule reads it
to derive a finding, because arity overloading is well formed. The TPTP language
page states:

> Symbols may be overloaded with different arity signatures, and are treated as
> different symbols.

So `color/1` alongside `color/2` denotes two symbols in every dialect. A rule
reporting such pairs was shipped for a period and was incorrect on every file it
applied to; see the CHANGELOG.

Two consequences follow. Arity forms part of a symbol's identity in TPTP, and
this table is keyed on the name alone, so `sqrt/1` and `sqrt/2` occupy one entry.
That suffices for the rules reading this table, each of which asks only whether a
name was declared, and is recorded here because a consumer deriving a signature
from `Tptp.Query.symbols/1` must account for it. Further, the arity condition
TPTP does state — "If a symbol's type is declared more than once, and the types
are not the same, that's an error" — concerns a single symbol and therefore
compares two declarations at the same arity, which this table cannot presently
distinguish.

# `conjecture`

```elixir
@type conjecture() :: :conjecture | :negated_conjecture
```

Which of the two spellings of a conjecture a statement used.

# `symbol`

```elixir
@type symbol() :: %{
  name: binary(),
  kind: atom(),
  declared_as: Tptp.Node.t() | nil,
  declared_at: Tptp.Span.t() | nil,
  used_at: [Tptp.Span.t()],
  arities: MapSet.t(non_neg_integer())
}
```

One symbol, as the traversal saw it.

`name` is the canonical atomic word, so a symbol written `'p'` in one statement
and `p` in the next is this one entry. `declared_as` is `nil` for a symbol that
was used but never declared, which is legal in FOF and CNF and a finding in the
typed dialects.

# `t`

```elixir
@type t() :: %Tptp.Lint.Table{
  conjectures: [{conjecture(), Tptp.Span.t()}],
  counted: MapSet.t({Tptp.Span.file_id(), non_neg_integer()}),
  features: MapSet.t(atom()),
  names: %{required(binary()) => [Tptp.Span.t()]},
  parents: [{binary(), Tptp.Span.t()}],
  symbols: %{required(binary()) => symbol()}
}
```

Everything the single walk accumulated: symbols, names, parents, conjectures, dialect features and counts.

# `conjecture`

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

Record a conjecture, in whichever of the two spellings it was written.

`conjecture` and `negated_conjecture` are kept apart because they do not count
the same way: one conjecture negated into clause normal form becomes many
`negated_conjecture` clauses, so counting those would call every CNF problem in
the library over-specified.

One position counts once, for the reason `use/5` gives.

# `declare`

```elixir
@spec declare(t(), binary(), atom(), Tptp.Node.t() | nil, Tptp.Span.t()) :: t()
```

Record a symbol declaration — a `type`-role statement's subject.

# `feature`

```elixir
@spec feature(t(), atom()) :: t()
```

Record a dialect feature the traversal saw.

# `feature?`

```elixir
@spec feature?(t(), atom()) :: boolean()
```

Whether a feature was seen anywhere.

# `features`

```elixir
@spec features(t()) :: [atom()]
```

Every dialect feature the traversal saw, as a list.

`Tptp.Query.from_features/1` turns this into a dialect.

# `finish`

```elixir
@spec finish(t()) :: t()
```

Put every accumulated list back into reading order.

The traversal prepends, because prepending is what a list is for; this is the one
place that matters, called once when the walk is done.

# `ignore`

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

Claim a position without recording anything, so nothing else counts it.

For a subtree whose atoms are labels rather than uses — the term of an
`<ntf_index>`, where `#agent` names a modality rather than applying a symbol.
`use/5` drops a position it has already seen, so claiming the position first is
how a top-down walk with no way to look up says "not this one".

# `name`

```elixir
@spec name(t(), binary(), Tptp.Span.t()) :: t()
```

Record a statement's name, so a second one can be reported against the first.

One position counts once, for the same reason `use/5` says so and a sharper one:
`Tptp.Unit.statements/1` expands an `include` wherever it stands, so a file
reached down two paths of a diamond is walked twice. Counting both would report
every name in every shared axiom set as a duplicate — 46,724 of them across a
quarter of the library, none of them a real finding. Two *different* statements
sharing a name still are, and still are reported.

# `parent`

```elixir
@spec parent(t(), binary(), Tptp.Span.t()) :: t()
```

Record a name used as an inference parent, to be checked against `names` later.

# `use`

```elixir
@spec use(t(), binary(), atom(), non_neg_integer(), Tptp.Span.t()) :: t()
```

Record a symbol occurrence, at the arity it was applied with.

One position counts once. `p(b)` reaches this twice — the traversal offers the
`fof_plain_term` before its `functor` child, so the application arrives with
arity 1 and the head leaf arrives again with arity 0 — and counting both would
report every applied symbol in the library as having two arities. The application
comes first because the walk is top-down, so first writer wins and the leaf's
second look is dropped.

---

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