Tptp.Analysis (Tptp v0.1.0)

Copy Markdown View Source

The file, its diagnostics, the symbol table and the dialect, from one traversal.

An editor integration requires all four on each edit. Tptp.analyze/2 produces them in a single traversal and returns them here; obtaining them through Tptp.Lint.run/2 and Tptp.Lint.table/1 would require two.

Input that does not parse still yields an Analysis, with a shortened statement list and the diagnostics recording the failure, since an editor must render markers for a buffer it cannot parse.

Line index

line_index is nil until with_line_index/1 populates it. Converting byte offsets to line and column requires one scan of the source, which an analysis that is never rendered should not incur and one rendering many positions should incur once. line_column/2 operates in either state, so with_line_index/1 is required only to hoist the scan out of a loop, as Tptp.File.format_diagnostics/1 does.

analysis = source |> Tptp.analyze() |> Tptp.Analysis.with_line_index()

for d <- analysis.diagnostics do
  {line, column} = Tptp.Analysis.line_column(analysis, d.span.offset)
  %{line: line, column: column, code: d.code, message: d.message}
end

Summary

Types

t()

A parsed subject, every diagnostic about it, the symbol table one traversal built, and — once with_line_index/1 has run — a line index over its source.

Functions

The narrowest dialect that accepts the file.

The one-based line and column of a byte offset.

A copy of the analysis with the line index computed and stored.

Types

t()

@type t() :: %Tptp.Analysis{
  diagnostics: [Tptp.Diagnostic.t()],
  file: Tptp.File.t() | Tptp.Unit.t(),
  line_index: Tptp.Span.line_index() | nil,
  table: Tptp.Lint.Table.t()
}

A parsed subject, every diagnostic about it, the symbol table one traversal built, and — once with_line_index/1 has run — a line index over its source.

Functions

dialect(analysis)

@spec dialect(t()) :: Tptp.Query.dialect()

The narrowest dialect that accepts the file.

Read from the feature set the traversal already recorded, so this costs nothing beyond the walk Tptp.analyze/2 did. Equal to Tptp.Query.dialect/1.

iex> Tptp.Analysis.dialect(Tptp.analyze("cnf(a, axiom, p | ~q)."))
:cnf

line_column(analysis, offset)

@spec line_column(t(), non_neg_integer()) :: {pos_integer(), pos_integer()}

The one-based line and column of a byte offset.

Uses the memoised index when with_line_index/1 has run and a fresh scan otherwise, so the answer is the same either way. Offsets resolve against the root file of a unit.

iex> analysis = Tptp.analyze("fof(a, axiom, p).\nfof(b, axiom, q).")
iex> Tptp.Analysis.line_column(analysis, 18)
{2, 1}

with_line_index(analysis)

@spec with_line_index(t()) :: t()

A copy of the analysis with the line index computed and stored.

Idempotent — an analysis that already has one is returned unchanged.