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

The `:==` well-formedness conditions, and the conditions requiring more than one
statement.

The grammar admits considerably more than the language defines.
`<formula_role> ::= <lower_word>` admits `wibble`; `<defined_functor> ::=
<atomic_defined_word>` admits `$wibble`; `<thf_top_level_type>` admits a rank-2
type that no TPTP implementation accepts. The `:==` rules of the BNF state which
of these are well formed, and the parser does not enforce them: input violating
one still yields a usable tree, and refusing to produce it would preclude the
malformed input this library exists to describe.

    {:ok, file, []} = Tptp.from_string("fof(a, wibble, p).")
    Tptp.Lint.run(file)
    #=> [%Tptp.Diagnostic{code: "TPTP0401", severity: :warning, ...}]

## Single traversal

`run/2` traverses once, offering each node to every enabled rule, and accumulates
the symbol table and the dialect features in the same pass. Rules requiring the
complete picture run afterwards against the table rather than the tree. Eight
rules over a large axiom set would otherwise require eight traversals of a tree
that does not fit in cache.

## No type inference

The symbol table records a declared type as the unelaborated `Tptp.Node` it was
written as. No unification or substitution is performed, and `$i` is not
interpreted as a type. Every rule is either syntactic or declines. See
`Tptp.Lint.Rules.Rank1`, which determines only whether a `!>` occurs within a
typing.

## Absence of a dialect rule

Use of a construct in a language that does not provide it is not reportable,
because it cannot occur. The BNF gives each language its own nonterminals, so `^`
is unreachable from `<tff_formula>`, `!!` from `<fof_formula>`, and a THF tuple
from anything but THF. Each was tested against every statement keyword; the
grammar rejects all of them at parse time, so such a rule could never apply.

What remains is classification rather than defect — a `tff` file using `!>` is
TF1 rather than TF0, and well formed — which `Tptp.Query.dialect/1` derives from
the same traversal.

## Severities

A rule's severity is a default. `:severity` overrides it per code, and
`:only`/`:except` select the rules that run. No shipped rule reports an error on
a conforming TPTP library file, and a corpus test enforces this. One rule is
`:info` rather than `:warning`: `Tptp.Lint.Rules.Conjecture` reports a property of
the problem rather than a defect in it. The remainder are warnings.

## Analyzer interface

`Tptp.Lint` implements `Tptp.Analyzer` as `:tptp_lint`, applicable to any
dialect. The callback performs the traversal under the options it is given.
Consumers requiring only the default rule set should read `analysis.diagnostics`
from `Tptp.analyze/2` rather than dispatching through
`Tptp.Analyzer.run_all/3`.

# `option`

```elixir
@type option() ::
  {:only, [module()]}
  | {:except, [module()]}
  | {:severity, %{required(binary()) =&gt; Tptp.Diagnostic.severity()}}
  | {:suppress, [binary()]}
```

Options accepted by `run/2`.

  * `:only` — run only these rule modules.
  * `:except` — run every rule but these.
  * `:severity` — a map from code to severity, overriding the rule's default.
    `severity: %{"TPTP0401" => :error}` raises an unrecognised role to an error.
    Keyed by binary rather than atom: a diagnostic code originates in
    configuration, and converting it to an atom for lookup would admit unbounded
    growth of the atom table.
  * `:suppress` — diagnostic codes to discard.

# `scan`

```elixir
@type scan() :: {[Tptp.Diagnostic.t()], Tptp.Lint.Table.t()}
```

The diagnostics a lint pass produced and the table it built, from one traversal.

# `rules`

```elixir
@spec rules() :: [module()]
```

Returns the shipped rules, in the order each node is offered to them.

# `run`

```elixir
@spec run(Tptp.File.t(), [option()]) :: [Tptp.Diagnostic.t()]
```

Lint one file.

    iex> {:ok, file, []} = Tptp.from_string("fof(a, axiom, p). fof(a, axiom, q).")
    iex> file |> Tptp.Lint.run() |> Enum.map(& &1.code)
    ["TPTP0503"]

# `run_unit`

```elixir
@spec run_unit(Tptp.Unit.t(), [option()]) :: [Tptp.Diagnostic.t()]
```

Lint a whole unit, includes expanded.

A declaration in an axiom file and a use in the problem file are one symbol here,
which is the point: an undeclared-symbol rule that could not see across an
`include` would report every typed problem in the library.

# `scan`

```elixir
@spec scan(Tptp.File.t() | Tptp.Unit.t(), [option()]) :: scan()
```

One traversal, both halves kept.

Every enabled rule is offered every node, and the symbol table and dialect
features accumulate in the same pass; the diagnostics and the finished table
are returned together rather than one being recomputed later.

`run/2`, `run_unit/2` and `table/1` are projections of this. Pass `only: []` to
build the table without applying a rule, as `table/1` does.

# `statements`

```elixir
@spec statements(Tptp.File.t() | Tptp.Unit.t()) :: [
  {Tptp.Span.file_id(), Tptp.Statement.t()}
]
```

Every statement of a file or unit, paired with the file it came from.

# `table`

```elixir
@spec table(Tptp.File.t() | Tptp.Unit.t()) :: Tptp.Lint.Table.t()
```

The symbol table and feature set, without running a single rule.

The same traversal `run/2` makes, stopping before the opinions. `Tptp.Query` is
built on this, which is what maintains "one walk" true across both modules rather
than only within one of them.

---

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