Tptp.Parser (Tptp v0.1.0)

Copy Markdown View Source

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.

Summary

Types

result()

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

Functions

statement_from_input(input, source, file \\ 0)

Parse one split input.

statement_from_string(source, file \\ 0)

Parse a source that holds exactly one statement.

Types

result()

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

Functions

statement_from_input(input, source, file \\ 0)

@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(source, file \\ 0)

@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