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

A node of the concrete syntax tree.

## Content

A node records what the grammar matched and nothing further. It carries no type,
no arity and no scope information, and does not classify `$i` as a type or `a` as
a term. The grammar itself does not distinguish a THF type from a THF term, so
the tree does not either; consumers requiring types elaborate them against a
signature of their own.

## Positions

`off` and `len` are byte offsets into the source. The file identifier is a
property of the file rather than of each of its nodes, so `span/2` constructs a
`Tptp.Span` on demand. Storing a span per node would approximately double the
size of a tree in order to repeat a single value.

A node's span covers the source it was built from including its own delimiters:
`[a, b]` spans the brackets and `f(a)` spans the closing parenthesis. The
generated grammar supplies the parser with the delimiters it omits from
`children` for this purpose, which makes containment queries — whether a given
comment falls inside a node — well defined.

## `text`

A leaf carrying text — a word, a number, a quoted atom — has `text` set to a
sub-binary of the source rather than a copy. Leaves whose spelling is determined
by their kind, such as `:vline`, `:iff` and `:big_forall`, have `text: nil`. The
invariant is that a non-`nil` `text` equals `binary_part(source, off, len)`.

Sub-binaries keep the source reachable. `Tptp.File` retains it for that reason;
`Tptp.detach/1` produces a copy owning its own binaries.

## `text` and `value/1`

`text` is the spelling as written. It is not the identity of the symbol. The BNF
defines a `<single_quoted>` as the enclosed `<atomic_word>` without the quotes,
so `cat` and `'cat'` denote the same atomic word, and `'it's'` is one word whose
fifth byte is an apostrophe. `text` retains quotes and escapes because the
printer must reproduce the input.

Symbol identity must therefore be taken from `value/1`. A table keyed on `text`
separates one symbol into two entries, and a signature derived from it inherits
that separation: `p` and `'p'` become distinct constants that never unify, which
is unsound in whatever is built above.

## Production indices

The generated grammar numbers the alternatives of each nonterminal. The parser
discards that number: a node records the kind that produced it and its children,
not which alternative was taken. Kind and children determine the alternative
except in one case. Of the 28 nonterminals with more than one node-building
alternative, only `<cnf_literal>` has two alternatives that agree on both, `~p`
and `~(p)` each yielding a `:cnf_literal` over a single `:constant`.

This does not affect `shape/1` or the printer round trip, which is why the index
is not retained.

## Kinds

`kind` is the grammar nonterminal that produced the node, or the token category
for a leaf. The generator splices out chain rules such as `<functor> ::=
<atomic_word>`, except for the significant ones listed in
`Tptp.Bnf.Generator.significant/0`, which are collapsed onto their leaf so that
the leaf retains the role the chain assigned it:

    f in f(a)           ->  %Node{kind: :functor,  text: "f"}
    f in p(f)           ->  %Node{kind: :constant, text: "f"}
    $i in tff(_,type,_) ->  %Node{kind: :defined_type, text: "$i"}

This records the role of a symbol without additional nodes, and allows a lint
rule to distinguish a constant from a functor without inspecting ancestors.

The third example is TFF. In a THF statement the same `$i` arrives as
`:defined_constant`, since TFF has separate productions for types and terms and
THF does not. This reflects a distinction the language does not draw.

## Construction

Nodes are ordinarily produced by the parser. Consumers that emit TPTP — a prover
backend, a translation to another format, a derivation in TSTP — construct them
instead. `new/3` defaults `off` and `len` to `0`, since a synthesised node
corresponds to no source position and supplying a plausible one would produce
diagnostics pointing at unrelated text. The sub-binary invariant above therefore
describes parsed trees only.

`Tptp.Printer.Canonical` operates on `kind`, `text` and `children` alone, so a
constructed tree prints. Its well-formedness is established by the round trip:
printing the tree and parsing the result must yield a tree with the same
`shape/1`. Failure indicates a malformed tree, typically a kind given the wrong
number of children or a leaf whose text does not lex as its kind.

# `t`

```elixir
@type t() :: %Tptp.Node{
  children: [t()],
  kind: atom(),
  len: non_neg_integer(),
  off: non_neg_integer(),
  text: binary() | nil
}
```

One CST node.

`text` is set on leaves only, as a sub-binary of the file's source, so a tree
costs no copies. `off` and `len` are byte offsets; a `Tptp.Span` — which needs
the file id too — is built on demand.

# `at`

```elixir
@spec at(t(), non_neg_integer()) :: t() | nil
```

Returns the innermost node whose span contains `offset`, or `nil`.

Descends the tree rather than searching it, so the cost is proportional to depth
rather than to size.

# `detach`

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

Returns a deep copy of the subtree with each `text` detached from the source.

Every leaf's `text` is ordinarily a sub-binary of the source, so retaining one
leaf retains the whole file. Copying each leaf's bytes allows the source to be
collected. Use it when keeping a small number of statements from a large file.

# `leaf?`

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

Returns whether the node has no children.

    iex> {:ok, statement, []} = Tptp.Parser.statement_from_string("fof(a,axiom,p).")
    iex> Tptp.Node.leaf?(statement.formula)
    true

# `new`

```elixir
@spec new(atom(), binary() | nil, [t()]) :: t()
```

Constructs a node with no corresponding source position.

For consumers emitting TPTP rather than reading it. `off` and `len` are `0`,
since a synthesised node indexes no source and a fabricated offset would be
reported by any diagnostic referring to it.

Well-formedness is established by the round trip: print the tree, parse the
result, and compare `shape/1`.

    iex> alias Tptp.Node
    iex> tree = Node.new(:fof_and_formula, nil, [Node.new(:constant, "p"), Node.new(:constant, "q")])
    iex> text = Tptp.Printer.Canonical.to_string(tree)
    "p & q"
    iex> {:ok, statement, []} = Tptp.Parser.statement_from_string("fof(a, axiom, " <> text <> ").")
    iex> Node.shape(statement.formula) == Node.shape(tree)
    true

# `reduce`

```elixir
@spec reduce(t(), acc, (t(), acc -&gt; acc)) :: acc when acc: var
```

Folds over the subtree in pre-order.

The eager counterpart to `walk/1`. Prefer it where the fold visits every node,
as it avoids the per-element overhead of the stream.

# `select`

```elixir
@spec select(t(), atom()) :: [t()]
```

Returns the nodes of the given kind, in source order.

    iex> {:ok, statement, []} = Tptp.Parser.statement_from_string("fof(a,axiom,![X]: p(X)).")
    iex> statement.formula |> Tptp.Node.select(:variable) |> Enum.map(& &1.text)
    ["X", "X"]

# `shape`

```elixir
@spec shape(t()) :: tuple()
```

Returns the subtree with positions removed, for comparison by structure.

Used by the printer round-trip property: `from_string(print(tree))` must have the
same shape as `tree`, though every offset in it differs.

    iex> {:ok, one, []} = Tptp.Parser.statement_from_string("fof(a,axiom,p).")
    iex> {:ok, two, []} = Tptp.Parser.statement_from_string("fof( a , axiom , p ).")
    iex> Tptp.Node.shape(one.formula) == Tptp.Node.shape(two.formula)
    true

# `span`

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

Returns the node's extent as a span in the given file.

# `text`

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

Returns the bytes the node covers, delimiters included.

A sub-binary rather than a copy. For a leaf this is `text`; for an interior node
it is the source of the entire subtree.

# `value`

```elixir
@spec value(t()) :: binary() | nil
```

Returns the leaf's canonical value: the atomic word rather than its spelling.

A `<single_quoted>` has its quotes and escapes removed, since the BNF defines
`cat` and `'cat'` as the same atomic word and `'it\'s'` as one word containing
an apostrophe. Any other leaf returns `text` unchanged, and `nil` returns `nil`.

Use this value to identify a symbol, and `text` to print it.

    iex> {:ok, statement, []} = Tptp.Parser.statement_from_string("fof(a, axiom, 'p'('q')).")
    iex> statement.formula |> Tptp.Node.walk() |> Enum.map(&Tptp.Node.value/1)
    [nil, "p", "q"]

Distinctions the BNF draws are preserved. A `<distinct_object>` is not an atomic
word, so `"cat"` denotes neither `'cat'` nor `cat`; and the body of a
`<back_quoted>` is an `<upper_word>`, which no unquoted atomic word may be.
Removing either delimiter would assert an identity the BNF does not state, so
both retain their quotes:

    iex> {:ok, statement, []} = Tptp.Parser.statement_from_string(~S|fof(a, axiom, p("cat")).|)
    iex> statement.formula |> Tptp.Node.select(:distinct_object) |> Enum.map(&Tptp.Node.value/1)
    [~S|"cat"|]

# `walk`

```elixir
@spec walk(t()) :: Enumerable.t()
```

Returns the nodes of the subtree in pre-order, left to right.

Lazy: `Enum.find/2` over a large formula halts at the first match rather than
materialising the full list.

    iex> {:ok, statement, []} = Tptp.Parser.statement_from_string("fof(a,axiom,p(X) & q).")
    iex> statement.formula |> Tptp.Node.walk() |> Enum.map(& &1.kind)
    [:fof_and_formula, :fof_plain_term, :functor, :variable, :constant]

---

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