Tptp.Span (Tptp v0.1.0)

Copy Markdown View Source

A byte range within a file.

Spans record byte offsets rather than line and column pairs. Tracking a line and column in the scanner costs a branch and two increments per byte for information most tokens never require; a line index is constructed once per file instead, and only where a diagnostic is rendered.

The file field is required by include resolution. A declaration may originate in an axiom file and be used in the problem file, and a diagnostic concerning it must refer to both, so a span is not interpretable without the file it indexes.

Nodes do not store spans. %Tptp.Node{} carries an offset and a length, and a span is constructed on demand, the file identifier being a property of the file rather than of each of its nodes.

Summary

Types

Which file a span is in.

Line-start byte offsets, one per line, as a tuple for constant-time indexing.

t()

A byte range in one file.

Functions

The byte just past the end of the span.

Resolve a byte offset to a one-based line and column, by binary search.

The number of lines the index covers.

Build the line index for a file.

A span over length bytes starting at offset in file file.

The bytes the span covers.

The smallest span covering both, which must be in the same file.

Types

file_id()

@type file_id() :: non_neg_integer()

Which file a span is in.

An integer rather than a path, because include makes spans cross files and every statement, diagnostic and symbol has to carry one.

line_index()

@opaque line_index()

Line-start byte offsets, one per line, as a tuple for constant-time indexing.

t()

@type t() :: %Tptp.Span{
  file: file_id(),
  length: non_neg_integer(),
  offset: non_neg_integer()
}

A byte range in one file.

Functions

ending(span)

@spec ending(t()) :: non_neg_integer()

The byte just past the end of the span.

line_column(index, offset)

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

Resolve a byte offset to a one-based line and column, by binary search.

iex> index = Tptp.Span.line_index("fof(a,axiom,p).\nfof(b,axiom,q).\n")
iex> Tptp.Span.line_column(index, 0)
{1, 1}
iex> Tptp.Span.line_column(index, 16)
{2, 1}
iex> Tptp.Span.line_column(index, 20)
{2, 5}

line_count(index)

@spec line_count(line_index()) :: pos_integer()

The number of lines the index covers.

line_index(source)

@spec line_index(binary()) :: line_index()

Build the line index for a file.

One pass, using :binary.matches/2, which is a NIF. Build it lazily: a corpus run that reports no diagnostics should never pay for it.

new(file, offset, length)

@spec new(file_id(), non_neg_integer(), non_neg_integer()) :: t()

A span over length bytes starting at offset in file file.

text(span, source)

@spec text(t(), binary()) :: binary()

The bytes the span covers.

The result is a sub-binary: four words and no copy, holding a reference into source. That is what you want while the file is alive anyway, and a leak when it is not — a thirty-byte functor name can retain a ten-megabyte file. Use :binary.copy/1 at the boundary where a name outlives its file.

union(left, right)

@spec union(t(), t()) :: t()

The smallest span covering both, which must be in the same file.