The position of a node within the statement being traversed.
A Tptp.Node carries no parent pointer and no reference to its statement, since
storing either on every node would be prohibitive at the scale the traversal
operates on. The traversal carries this structure alongside instead, rebuilt per
statement rather than per node.
whole records the subject of the traversal: a complete Tptp.Unit with
includes resolved, or a single Tptp.File that may be one part of a problem. A
rule whose question concerns the problem rather than the statement — whether any
proof obligation is stated — must decline when this is false, since the answer
may lie in an unread file.
slot records which part of the statement the traversal is within: :formula,
:name, :role, :source or :info. It allows a rule concerned with symbols
to disregard the annotations, where the same words denote something else — file
in a <source> is a keyword, and an atom in a <general_term> is a label rather
than a functor.
Summary
Types
Which part of the statement the walk is currently inside.
Where the fused walk currently is: which file, which statement, and which slot of it.
Functions
The language the statement is written in, or :include.
The role of the statement, or nil for an include.
A span in the file the walk is reading, for a node the rule wants to report.
Types
@type slot() :: :name | :role | :formula | :source | :info | :file_name | :selection
Which part of the statement the walk is currently inside.
@type t() :: %Tptp.Lint.Context{ depth: non_neg_integer(), file: Tptp.Span.file_id(), path: Path.t() | nil, slot: slot(), statement: Tptp.Statement.t(), whole: boolean() }
Where the fused walk currently is: which file, which statement, and which slot of it.
Functions
@spec language(t()) :: Tptp.Input.language()
The language the statement is written in, or :include.
iex> {:ok, statement, []} = Tptp.Parser.statement_from_string("cnf(a,axiom,p).")
iex> context = %Tptp.Lint.Context{file: 0, statement: statement, slot: :formula}
iex> Tptp.Lint.Context.language(context)
:cnfThe role of the statement, or nil for an include.
@spec span(t(), Tptp.Node.t()) :: Tptp.Span.t()
A span in the file the walk is reading, for a node the rule wants to report.