Tptp.Diagnostic (Tptp v0.1.0)

Copy Markdown View Source

A single observation about the input.

Diagnostics do not interrupt processing. Every stage accepts and returns an accumulator of them, so a result is available even where it is partial, and success carries diagnostics alongside it.

Codes

Codes are stable and the tier is determined by the number, so an editor can filter by code and a consumer can suppress a rule without matching on message text.

RangeTier
TPTP00xxinput and resource limits — Tptp
TPTP01xxlexical — Tptp.Lexer
TPTP02xxstatement structure — Tptp.Splitter
TPTP03xxgrammar — Tptp.Parser
TPTP04xx:== well-formedness — Tptp.Lint
TPTP05xxcross-statement — Tptp.Lint
TPTP06xxinclude — Tptp.Include
TPTP08xxanalyzer infrastructure — Tptp.Analyzer

A code is never reassigned, so the numbering contains gaps: TPTP0103, TPTP0108, TPTP0403, TPTP0502, TPTP0505 and TPTP0604 are unassigned. TPTP0505 was withdrawn when the rule raising it was found to contradict the TPTP.

There is no TPTP07xx tier. It was reserved for dialect findings, of which there are none: the BNF gives each language its own nonterminals, so a construct used in a language that does not provide it fails to parse rather than reaching a rule. Tptp.Lint sets this out, and Tptp.Query.dialect/1 derives the dialect instead.

related carries the accompanying positions of a finding, such as the first declaration alongside a redeclaration.

Summary

Types

How much a diagnostic matters.

t()

One thing the library has to say about a span of input.

Functions

Whether any diagnostic is severe enough to call the result a failure.

Render one diagnostic as a single line, resolving the span against a line index.

Sort diagnostics into reading order: by file, then by offset, then by code.

Types

severity()

@type severity() :: :error | :warning | :info | :hint

How much a diagnostic matters.

Only :error means no result was produced. A :warning accompanies a CST that is perfectly usable, which is why every entry point returns diagnostics alongside success rather than instead of it.

t()

@type t() :: %Tptp.Diagnostic{
  code: binary(),
  hint: binary() | nil,
  message: binary(),
  related: [{Tptp.Span.t(), binary()}],
  severity: severity(),
  span: Tptp.Span.t()
}

One thing the library has to say about a span of input.

Functions

any_errors?(diagnostics)

@spec any_errors?([t()]) :: boolean()

Whether any diagnostic is severe enough to call the result a failure.

format(diagnostic, line_index, path \\ nil)

@spec format(t(), Tptp.Span.line_index(), Path.t() | nil) :: binary()

Render one diagnostic as a single line, resolving the span against a line index.

iex> span = Tptp.Span.new(0, 4, 1)
iex> diagnostic = Tptp.Diagnostic.new("TPTP0101", :error, span, "illegal character")
iex> index = Tptp.Span.line_index("fof(\0)")
iex> Tptp.Diagnostic.format(diagnostic, index)
"1:5: error: illegal character [TPTP0101]"

new(code, severity, span, message, options \\ [])

@spec new(binary(), severity(), Tptp.Span.t(), binary(), keyword()) :: t()

Build a diagnostic.

message is copied with :binary.copy/1 when it is a sub-binary of the source, because a diagnostic outlives the file it describes far more often than a token does.

sort(diagnostics)

@spec sort([t()]) :: [t()]

Sort diagnostics into reading order: by file, then by offset, then by code.