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

Parses the tokens of one statement into a `Tptp.Statement`.

The grammar is generated: `mix tptp.gen` translates the `::=` rules of the
vendored BNF into `src/tptp_parser.yrl`, which `yecc` compiles to an LALR(1)
parser. This module drives that parser and converts its output.

## Statement granularity

`yecc` provides no error recovery, so a parser generated from a whole-file
grammar halts at the first ill-formed byte and reports nothing about the
remainder. Parsing per statement makes recovery structural: a statement that
fails to parse becomes a diagnostic and the file continues. It also bounds the
effect of malformed input to a single statement, provides an incremental unit for
editor use — locate the statement containing an offset, reparse it, splice the
result — and makes statements a unit of parallelism.

## Conversion

The generated actions construct three forms — `{'$node', kind, alt, children,
open, close}`, `{'$leaf', category, alt, token}` and tokens spliced through from
chain rules — which a single bottom-up traversal converts into `Tptp.Node`:

  * **Spans are composed** rather than carried by the actions, which keeps every
    action a single template. `open` and `close` are the production's delimiters,
    which the generator omits from `children` and supplies separately, so a
    node's span covers its own delimiters.
  * **Leaf text is materialised** with `binary_part/3`, producing a sub-binary
    rather than a copy.
  * **Significant chain rules are collapsed onto their leaf.** Where one of the
    role-naming nonterminals in `Tptp.Bnf.Generator.significant/0` wraps a single
    text-carrying leaf, the node becomes that leaf and retains the outer kind, so
    `f` in `p(f)` arrives as `:constant` and `f` in `f(a)` as `:functor` without
    additional nodes. The set is enumerated rather than derived: `<tff_arguments>
    ::= <tff_term>` has the same shape, but its child is an argument rather than a
    renaming, and collapsing it would replace the argument's kind.

## Higher-order constructs

No elaboration, saturation, uncurrying or instantiation is performed. `f @ $i @ a`
retains its left-nested application spine with `$i` present as an argument
carrying its own kind and span; `!!`, `??`, `@@+`, `@@-` and `@=` arrive as
distinct leaf kinds; `!>` and `?*` schemes are recorded verbatim. The grammar does
not distinguish a THF type from a THF term, and neither does the resulting tree.

# `result`

```elixir
@type result() ::
  {:ok, Tptp.Statement.t(), [Tptp.Diagnostic.t()]}
  | {:error, [Tptp.Diagnostic.t()]}
```

A parse either produces a statement or explains why it could not.

Diagnostics ride along with success too: a statement can parse and still be worth
complaining about, and the caller decides what is fatal.

# `statement_from_input`

```elixir
@spec statement_from_input(Tptp.Input.t(), binary(), Tptp.Span.file_id()) :: result()
```

Parse one split input.

`source` is the file the input's offsets index into; `file` is the id stamped
into any diagnostic's span.

    iex> {[input], _comments, []} = Tptp.Splitter.inputs("fof(a,axiom,p).")
    iex> {:ok, statement, []} = Tptp.Parser.statement_from_input(input, "fof(a,axiom,p).")
    iex> {statement.language, statement.name.text, statement.role.text}
    {:fof, "a", "axiom"}

# `statement_from_string`

```elixir
@spec statement_from_string(binary(), Tptp.Span.file_id()) :: result()
```

Parse a source that holds exactly one statement.

A convenience for tests, doctests and single-formula input such as a prover's
answer. Anything file-shaped wants `Tptp.from_string/2`, which reports every
statement rather than refusing the second.

    iex> {:ok, statement, []} = Tptp.Parser.statement_from_string("cnf(c,axiom,p | ~q).")
    iex> statement.language
    :cnf

---

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