AtpClient.Lint (AtpClient v0.2.0)

Copy Markdown View Source

Syntax and type diagnostics for TPTP input, aggregated across one or more backends.

Two backends ship with this module:

  • AtpClient.Lint.Local — a pure-Elixir structural checker that runs in-process, catches common typos (unknown role, missing dot, mismatched brackets) and extracts type declarations for hover and completion data.
  • AtpClient.Lint.Tptp4x — delegates to TPTP4X on the configured SystemOnTPTP deployment for authoritative syntax and type analysis.

The default configuration runs both: the local pass is essentially free, and when it finds an error the remote pass is skipped to save a round-trip. Editor integrations (see KinoAtpClient.SystemOnTptp) call analyze/2 on every debounced keystroke.

Example

iex> %AtpClient.Lint.Report{diagnostics: diags, symbols: syms} =
...>   AtpClient.Lint.analyze("fof(a, axim, p).")
iex> Enum.map(diags, & &1.message)
["unknown TPTP role `axim`; expected one of: axiom, hypothesis, ..."]
iex> syms
[]

Summary

Types

backend()

Functions

analyze(problem, opts \\ [])

Runs the enabled backends against problem and returns a merged Report.

check(problem, opts \\ [])

Convenience wrapper that returns just the diagnostics list — useful for callers that don't care about symbol extraction.

Types

backend()

@type backend() :: :local | :tptp4x

Functions

analyze(problem, opts \\ [])

@spec analyze(
  String.t(),
  keyword()
) :: AtpClient.Lint.Report.t()

Runs the enabled backends against problem and returns a merged Report.

Options

  • :backends — a list of backend/0 atoms. Defaults to [:local, :tptp4x];
  • any option accepted by the chosen backends (e.g. :url, :tptp4x_system) — forwarded verbatim.

When both backends run and the local pass reports any :error diagnostic, the remote pass is skipped: the user will fix the obvious issue first, and a failing TPTP4X result on top of a local error adds noise without new information. Warnings do not suppress the remote pass.

check(problem, opts \\ [])

@spec check(
  String.t(),
  keyword()
) :: {:ok, [AtpClient.Lint.Diagnostic.t()]}

Convenience wrapper that returns just the diagnostics list — useful for callers that don't care about symbol extraction.