AtpClient.Lint.Local (AtpClient v0.1.6)

Copy Markdown View Source

Pure-Elixir structural checker for TPTP input.

Runs in microseconds on typical problem sizes, so it can drive the editor feedback loop on every keystroke without going through the network. Catches the common classes of errors that TPTP4X would otherwise flag after a round-trip:

  • unmatched / mismatched brackets ((, [, {);
  • unterminated block comments and quoted atoms;
  • unknown TPTP language prefix (e.g. fff instead of fof);
  • unknown formula role (e.g. axim instead of axiom);
  • a statement body that never sees its closing ) and ..
  • juxtaposed identifiers (e.g. F X in THF where F @ X is required).

The checker is intentionally forgiving inside formula bodies: it does not try to parse the logical content, only the TPTP framing around it. That keeps the code small and lets us delegate the authoritative syntactic and type analysis to TPTP4X.

analyze/1 additionally walks type-role statements and returns a list of AtpClient.Lint.Symbols — used by the Smart Cell to power Monaco hover and completion.

Summary

Functions

analyze(source)

Tokenises source, checks it for structural issues, and extracts any symbol declarations. Always returns a Report — a lexer-level failure (e.g. unterminated block comment) surfaces as a single diagnostic and an empty symbol list.

check(source, opts \\ [])

Convenience wrapper matching the AtpClient.Lint backend contract.

Functions

analyze(source)

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

Tokenises source, checks it for structural issues, and extracts any symbol declarations. Always returns a Report — a lexer-level failure (e.g. unterminated block comment) surfaces as a single diagnostic and an empty symbol list.

check(source, opts \\ [])

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

Convenience wrapper matching the AtpClient.Lint backend contract.