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.
Summary
Types
Which of the two spellings of a conjecture a statement used.
One symbol, as the traversal saw it.
Everything the single walk accumulated: symbols, names, parents, conjectures, dialect features and counts.
Functions
Record a conjecture, in whichever of the two spellings it was written.
Record a symbol declaration — a type-role statement's subject.
Record a dialect feature the traversal saw.
Whether a feature was seen anywhere.
Every dialect feature the traversal saw, as a list.
Put every accumulated list back into reading order.
Claim a position without recording anything, so nothing else counts it.
Record a statement's name, so a second one can be reported against the first.
Record a name used as an inference parent, to be checked against names later.
Record a symbol occurrence, at the arity it was applied with.
Types
@type conjecture() :: :conjecture | :negated_conjecture
Which of the two spellings of a conjecture a statement used.
@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.
@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.
Functions
@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.
@spec declare(t(), binary(), atom(), Tptp.Node.t() | nil, Tptp.Span.t()) :: t()
Record a symbol declaration — a type-role statement's subject.
Record a dialect feature the traversal saw.
Whether a feature was seen anywhere.
Every dialect feature the traversal saw, as a list.
Tptp.Query.from_features/1 turns this into a dialect.
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.
@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".
@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.
@spec parent(t(), binary(), Tptp.Span.t()) :: t()
Record a name used as an inference parent, to be checked against names later.
@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.