Resolves include directives, constructing the file graph underlying a
Tptp.Unit.
Memoisation
Memoisation is keyed on the resolved path rather than the name, since two files
may reach one axiom set under different names — Axioms/SET007+0.ax from the
library root and SET007+0.ax from beside it. A graph reading it twice would
duplicate the work and report every formula in it as a duplicate. The resolver
returns a canonical path for this purpose, so a diamond is read once.
Being read once is distinct from occurring once. An include denotes textual
inclusion, so Tptp.Unit.statements/1 expands each directive in position and the
statements of one file may occur twice under two directives. Consumers requiring
the set rather than the sequence can derive it.
Cycles
A file including itself, directly or transitively, is cut at the edge closing the
cycle: that edge resolves to nothing, TPTP0602 names every file on the cycle,
and the traversal continues. The resolved graph is therefore acyclic and
expansion terminates.
Depth
Bounded by :max_depth, 64 by default. The bound exists because a resolver
returning unexpected paths can otherwise convert a misspelling into an unbounded
traversal.
Concurrency
Sibling includes are parsed in parallel. The median problem in the TPTP library
includes two files and resolves in approximately 1.5 ms; the largest,
ITP022^4.p, includes 144 siblings totalling 59 MB and requires 6.7 s
sequentially, of which 56 ms is I/O. Parsing dominates and is therefore what is
parallelised.
The memoisation table is not shared during the parallel phase. Each level proceeds in three passes: resolve every sibling, which is I/O and runs sequentially; determine which are new and assign their file identifiers in source order; then parse those in parallel. Since identifiers are assigned beforehand, the resulting graph does not depend on task completion order, and the same input produces the same graph.
:max_concurrency bounds the parallel phase; set it to 1 for a sequential
traversal.
Summary
Functions
Every statement of a file and of everything it includes, in reading order.
Read a root file's includes, transitively.
Types
@type graph() :: %{ files: %{required(Tptp.Span.file_id()) => Tptp.File.t()}, paths: %{required(Path.t()) => Tptp.Span.file_id()}, resolutions: %{ required({Tptp.Span.file_id(), non_neg_integer()}) => Tptp.Span.file_id() }, diagnostics: [Tptp.Diagnostic.t()], next: Tptp.Span.file_id() }
The graph as it is being built.
files is keyed by the id stamped into that file's spans; paths maps a
resolved path back to its id, which is the memo table; resolutions records
where each include directive led, keyed by the directive's own position, which
is unique within its file.
Functions
@spec expand(graph() | Tptp.Unit.t(), Tptp.Span.file_id(), [binary()] | nil) :: [ {Tptp.Span.file_id(), Tptp.Statement.t()} ]
Every statement of a file and of everything it includes, in reading order.
Each include is replaced by what it names, right where it stands, which is what
the language means by inclusion. selection filters the whole subtree by formula
name; nil keeps all of it.
Takes the graph resolve/3 builds or the Tptp.Unit made from it — they carry
the same two fields, and the walk needs nothing else.
@spec resolve(Tptp.File.t(), Tptp.Resolver.t(), keyword()) :: graph()
Read a root file's includes, transitively.
The root file is already parsed; this adds everything it reaches. Returns the graph and every diagnostic raised along the way, the included files' own included.