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

The two forms a parsed TPTP statement takes.

`<TPTP_input> ::= <annotated_formula> | <include>`, so there are exactly two.
They are separate structs rather than one struct with a discriminator, since they
share no fields and a consumer requires one or the other.

`Tptp.Statement.Annotated` is the `thf`, `tff`, `tcf`, `fof`, `cnf` and `tpi`
form. `Tptp.Statement.Include` is the `include` directive, which makes a set of
files a graph rather than a list.

# `t`

```elixir
@type t() :: Tptp.Statement.Annotated.t() | Tptp.Statement.Include.t()
```

Either kind of top-level input the grammar admits.

# `detach`

```elixir
@spec detach(t()) :: t()
```

A copy whose every leaf owns its bytes, so the file it came from can be collected.

See `Tptp.Node.detach/1` for why this is not the default.

# `roots`

```elixir
@spec roots(t()) :: [Tptp.Node.t()]
```

Every CST subtree the statement holds, in source order.

A statement is a handful of named slots rather than one tree, because its shape
is fixed by the grammar and naming the slots is more useful than making a caller
index into children. This is the escape hatch for the operations that genuinely
want all of them — walking for symbols, checking span invariants, detaching.

    iex> {:ok, statement, []} = Tptp.Parser.statement_from_string("fof(a,axiom,p).")
    iex> statement |> Tptp.Statement.roots() |> Enum.map(& &1.kind)
    [:name, :formula_role, :constant]

# `span`

```elixir
@spec span(t(), Tptp.Span.file_id()) :: Tptp.Span.t()
```

The statement's extent, as a span in the file it was read from.

# `text`

```elixir
@spec text(t(), binary()) :: binary()
```

The bytes the statement covers, terminating `.` included.

---

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