# `Tptp.Include`
[🔗](https://github.com/jcschuster/tptp/blob/v0.1.3/lib/tptp/include.ex#L1)

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.

# `graph`

```elixir
@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.

# `expand`

```elixir
@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.

# `resolve`

```elixir
@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.

---

*Consult [api-reference.md](api-reference.md) for complete listing*