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

A root file together with everything its `include` directives reach.

`Tptp.from_file/2` reads a single file. This reads a problem: the root and the
axiom sets it includes, with every span identifying the file it originates in, so
that a diagnostic concerning a symbol declared in an axiom file and used in the
problem can refer to both.

    {:ok, unit, diagnostics} =
      Tptp.Unit.from_file("Problems/PUZ/PUZ001+1.p", resolver: Tptp.Resolver.Fs)

    Tptp.Unit.statements(unit)   # [{file_id, statement}], includes expanded in place
    unit.files[unit.root]        # the root %Tptp.File{}

## Resolution is explicit

The default resolver is `Tptp.Resolver.None`, which records each directive and
reads nothing. Resolution reads files the caller did not name and, under
`Tptp.Resolver.Http`, performs network access, so the resolver is supplied by the
caller rather than defaulted.

## Two representations

`files` is the set of files, each read once even where a diamond in the graph
reaches it twice. `statements/1` is the sequence, with each `include` expanded in
position, which is what textual inclusion denotes and what a prover observes. A
file read once may therefore occur twice in the sequence.

## Formula selection

`include('big.ax', [key_lemma])` retains only the named formulae, and the filter
applies to the whole subtree beneath that directive rather than to `big.ax`
alone. The TPTP standard does not define the meaning of a selection when the
selected file has includes of its own; this reading makes `include(f, [x])`
denote the formula `x` wherever it occurs beneath the directive. A name occurring
nowhere beneath it produces a `TPTP0603` warning.

# `option`

```elixir
@type option() ::
  Tptp.option()
  | {:resolver, Tptp.Resolver.t()}
  | {:max_depth, pos_integer()}
  | {:max_concurrency, pos_integer()}
```

Options accepted by the entry points.

Everything `t:Tptp.option/0` accepts, plus:

  * `:resolver` — how an `include` name becomes bytes. Defaults to
    `Tptp.Resolver.None`, which follows nothing.
  * `:max_concurrency` — how many sibling includes are parsed at once. Defaults to
    `System.schedulers_online()`; set it to `1` for a strictly sequential walk, which
    is what a caller running under its own `max_heap_size` needs, since that ceiling
    is not inherited by the processes `Tptp.Include` spawns.
  * `:max_depth` — how deep the include graph may nest before the walk stops and
    says so. Defaults to 64.

# `t`

```elixir
@type t() :: %Tptp.Unit{
  diagnostics: [Tptp.Diagnostic.t()],
  files: %{required(Tptp.Span.file_id()) => Tptp.File.t()},
  resolutions: %{
    required({Tptp.Span.file_id(), non_neg_integer()}) => Tptp.Span.file_id()
  },
  root: Tptp.Span.file_id()
}
```

A root file and everything reachable from it through `include`, with the resolutions that got there.

# `any_errors?`

```elixir
@spec any_errors?(t()) :: boolean()
```

Whether anything error-severity was found, in any file.

# `file`

```elixir
@spec file(t(), Tptp.Span.file_id() | Tptp.Span.t()) :: Tptp.File.t() | nil
```

The file a span or id belongs to.

# `format_diagnostics`

```elixir
@spec format_diagnostics(t()) :: [binary()]
```

Every diagnostic, rendered one per line against the file it belongs to.

# `formulae`

```elixir
@spec formulae(t()) :: [{Tptp.Span.file_id(), Tptp.Statement.Annotated.t()}]
```

Every annotated formula, `include` directives expanded and filtered by selection.

# `from_file`

```elixir
@spec from_file(Path.t(), [option()]) ::
  {:ok, t(), [Tptp.Diagnostic.t()]} | {:error, [Tptp.Diagnostic.t()]}
```

Read a file from disk and everything it includes.

Fails only when the root file cannot be read; an include that cannot be resolved
is a diagnostic on an otherwise usable unit.

# `from_file!`

```elixir
@spec from_file!(Path.t(), [option()]) :: t()
```

Read a file and everything it includes, raising `Tptp.Error` on any error.

# `from_name`

```elixir
@spec from_name(binary(), [option()]) ::
  {:ok, t(), [Tptp.Diagnostic.t()]} | {:error, [Tptp.Diagnostic.t()]}
```

Read a file the resolver knows by name, and everything it includes.

The entry point for a caller who has a TPTP name rather than a path — from a
problem list, a benchmark set, or a user typing `PUZ001+1.p`. The root goes
through the same resolver as its includes, so pointing `$TPTP_ROOT` at a local
library or passing `Tptp.Resolver.Http` changes where everything comes from at
once.

    Tptp.Unit.from_name("Problems/PUZ/PUZ001+1.p", resolver: Tptp.Resolver.Fs)

# `from_string`

```elixir
@spec from_string(binary(), [option()]) :: {:ok, t(), [Tptp.Diagnostic.t()]}
```

Read a file and everything it includes.

    iex> resolver = {Tptp.Resolver.Map, files: %{"a.ax" => "fof(a, axiom, p)."}}
    iex> {:ok, unit, []} = Tptp.Unit.from_string("include('a.ax'). fof(b, conjecture, p).", resolver: resolver)
    iex> unit |> Tptp.Unit.statements() |> Enum.map(fn {_id, statement} -> statement.name.text end)
    ["a", "b"]

# `statements`

```elixir
@spec statements(t()) :: [{Tptp.Span.file_id(), Tptp.Statement.t()}]
```

Every statement, with `include` directives expanded where they stand.

Each element is `{file_id, statement}`, because the statement itself carries only
offsets — the file it belongs to is what turns those into a position. The
directives themselves are not in the result; they have been replaced by what they
name. An unresolved directive contributes nothing, and said so at read time.

# `text`

```elixir
@spec text(t(), Tptp.Span.t()) :: binary() | nil
```

The bytes a span names, wherever in the unit it points.

---

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