An include directive: include('Axioms/SET007+0.ax', [a, b], space).
selection is the optional <formula_selection>: a list of names, or * as a
:star leaf. space_name is the optional third argument, which the BNF admits
without assigning it a meaning. Both are retained verbatim.
Nothing here is resolved. Resolution is performed by Tptp.Include and requires
a resolver supplied by the caller, since reading a file the caller did not name,
or retrieving one over the network, is not a decision for the parser.
Summary
Types
An include directive: the file it names, the selection it applies, and the space it names.
Functions
The included file's name, without its surrounding quotes.
The names this include selects, or nil when it takes the whole file.
Types
@type t() :: %Tptp.Statement.Include{ file_name: Tptp.Node.t(), len: non_neg_integer(), off: non_neg_integer(), selection: Tptp.Node.t() | nil, space_name: Tptp.Node.t() | nil }
An include directive: the file it names, the selection it applies, and the space it names.
Functions
The included file's name, without its surrounding quotes.
<file_name> is an <atomic_word>, and in practice always a <single_quoted>,
so the raw text carries quotes the filesystem does not want. That unquoting is
Tptp.Node.value/1 — the same canonical value every other atomic word gets —
and the copy is this function's own: a path outlives the read that produced it,
and a sub-binary of a source file is not appropriate to keep a directory alive.
iex> {:ok, statement, []} = Tptp.Parser.statement_from_string("include('Axioms/SET007+0.ax').")
iex> Tptp.Statement.Include.path(statement)
"Axioms/SET007+0.ax"The names this include selects, or nil when it takes the whole file.
* selects everything and is reported as nil, the same as no selection at all,
because the two mean the same thing and a caller should not have to know both
spellings. The names are canonical values rather than spellings, so
include('a.ax', ['b']) selects the statement named b.
iex> {:ok, statement, []} = Tptp.Parser.statement_from_string("include('a.ax',[b,c]).")
iex> Tptp.Statement.Include.selected(statement)
["b", "c"]