Tptp.Bnf.Generator (Tptp v0.1.0)

Translates the vendored SyntaxBNF into src/tptp_parser.yrl.

The generated grammar is committed, so installation requires only OTP, which supplies yecc. Regeneration is a maintainer action performed on a TPTP release, and the resulting diff constitutes the review of that release.

Translation

Repetition. X* becomes a right-recursive helper nonterminal with an empty production. Six ::= rules require it.
Literals. Runs of literal text are divided against Tptp.Token.spellings/0, longest match first, so tpi( becomes kw_tpi lparen and ). becomes rparen dot.
<nothing>. An alternative consisting only of <nothing> becomes yecc's '$empty', and the nonterminal is eliminated.
Punctuation and fixed spellings are omitted from the children. A node's kind and alt determine every byte of fixed text, and Tptp.Printer.Shapes is generated from the same source, so the two cannot diverge. A child is therefore a nonterminal or a value-carrying token.
Single-terminal alternatives become leaves. <fof_quantifier> ::= ! yields %Tptp.Node{kind: :forall} rather than a wrapper around a token, which gives the polymorphic constants of TH1 — <th1_defined_term> ::= !! | ?? | @@+ | @@- | @= — a distinct kind each.
Transparent rules are spliced. A rule whose every alternative yields exactly one child conveys no information; splicing it keeps the tree approximately the size of the input.

An alternative consisting only of <nothing> yields nil rather than an empty node, since there are no tokens from which to derive a span, and nil denotes absence without a consumer having to distinguish it from a node with no children. <thf_tuple> ::= [] is such a node and denotes something different.

Departures

Four, each of which would otherwise constitute an LALR(1) conflict, and none of which changes the language accepted. departures/0 returns the list, generate/1 includes it in its report, and mix tptp.gen prints it from that list rather than from a copy, so a fifth cannot be introduced without appearing in the output intended to surface it.

<source> ::= … | unknown is dropped. unknown still parses, as <dag_source> -> <name>; retaining the literal alternative would render the two indistinguishable in source position.
inference, introduced and file are given terminals of their own and are also admitted as <atomic_word>, so that fof(file, axiom, p). continues to parse. The ( lookahead separates the two readings. In <atomic_word> position they are relabelled lower_word, their keyword status being an artefact of parsing.
The six $-keywords — $thf, $tff, $fof, $cnf, $fot and $let — are reserved, and are not admitted as <atomic_defined_word>. Admitting $let would render $let(a,b,c) ambiguous between <thf_let> and <thf_fof_function>. The BNF has no notion of reservation — the word does not occur in it — so this is a decision the grammar compels rather than states.
The five $-language markers — $thf, $tff, $fof, $cnf and $fot — retain their terminals as children of <formula_data>, where the generator would otherwise omit them as fixed spellings. $fot(a) and $fof(a) are distinct nodes of the same shape, so the marker is what distinguishes them and must be present in the tree.

The seven language keywords — thf, tff, tcf, fof, cnf, tpi and include — require no such treatment. They occur only as a statement's first token, so Tptp.Splitter promotes token zero and every other occurrence remains a <lower_word>. This is what admits fof(fof, axiom, p).

Summary

Types

grammar()

Nonterminal name to its alternatives, each a sequence of symbols.

report()

Statistics and departures, for the task to report.

symbol()

A resolved grammar symbol.

Functions

departures()

Returns one line per departure from a mechanical translation of the BNF.

generate(bnf_path)

Build the .yrl source and a report from a BNF file.

reserved_words(rules)

Every $-prefixed word the BNF mentions, in any rule and any position.

shapes(bnf_path)

Builds Tptp.Printer.Shapes from the grammar the parser is generated from.

significant()

Returns the nonterminals whose node Tptp.Parser collapses onto its leaf.

vocabularies(bnf_path)

Builds Tptp.Bnf.Vocabulary from the :== rules that are closed word lists.

Types

grammar()

@type grammar() :: %{required(binary()) => [[symbol()]]}

Nonterminal name to its alternatives, each a sequence of symbols.

report()

@type report() :: %{
  rules: non_neg_integer(),
  productions: non_neg_integer(),
  nonterminals: non_neg_integer(),
  terminals: non_neg_integer(),
  inlined: [binary()],
  transparent: [binary()],
  significant: [binary()],
  pruned: [binary()],
  dropped: [binary()],
  injected: non_neg_integer(),
  departures: [binary()]
}

Statistics and departures, for the task to report.

symbol()

@type symbol() ::
  {:nonterminal, binary()}
  | {:terminal, Tptp.Token.category()}
  | {:repeat, binary()}

A resolved grammar symbol.

Functions

departures()

@spec departures() :: [binary()]

Returns one line per departure from a mechanical translation of the BNF.

Rendered from the constants producing them, so the list cannot diverge from the code. mix tptp.gen prints this list; the module documentation describes each entry.

iex> Tptp.Bnf.Generator.departures() |> length()
4

generate(bnf_path)

@spec generate(Path.t()) :: {binary(), report()}

Build the .yrl source and a report from a BNF file.

reserved_words(rules)

@spec reserved_words([Tptp.Bnf.Rule.t()]) :: [binary()]

Every $-prefixed word the BNF mentions, in any rule and any position.

The closed vocabularies capture only rules whose alternatives consist entirely of literals, and several defined words are not written that way: <ntf_domains_spec> :== $domains <identical> <ntf_domains_value> places $domains alongside two other symbols, so it is a word the language defines that no closed list contains. Checking $-words against the closed lists alone reports such words as unrecognised.

A $-word is also not always a literal run of its own. A rule applying one includes the bracket in the same run — <txf_conditional> :== $ite(<tff_logic_formula>,…) is the literal $ite( — so the word is extracted from the run rather than matched against it. Matching whole runs omits $ite and the six $-keywords, and reports $ite as undefined on the single library file using it.

shapes(bnf_path)

@spec shapes(Path.t()) :: {binary(), non_neg_integer()}

Builds Tptp.Printer.Shapes from the grammar the parser is generated from.

A canonical printer requires the spelling of each node kind: the positions of the parentheses and the literal separating the children. This is what the ::= productions state, so the table is derived from the same source in the same pass rather than written by hand.

A shape is keyed by node kind and child count. Of the groups the grammar produces, one has two spellings: <cnf_literal> admits ~p and ~(p). These are equivalent and the parentheses redundant, the operand being atomic, so the shorter is selected. The general tie-break is the fewest literals, which is sound because a tree carries its own parenthesisation nodes — <fof_unitary_formula> ::= (<fof_logic_formula>) is a node — so no parenthesis affecting a reading is ever introduced or omitted by the printer.

For the same reason a leading comma is spliced only for the comma_* list helpers, whose comma is the list separator supplied by the {:separated, ","} shape. Elsewhere — in <optional_info> ::= ,<useful_info> and its two siblings — the comma is syntax the printer must emit, and splicing it would leave a shape with two adjacent slots and no separator between them.

significant()

@spec significant() :: [atom()]

Returns the nonterminals whose node Tptp.Parser collapses onto its leaf.

These are the chain rules recording the role a symbol occupies — <constant>, <functor>, <variable> and the rest. Each is a renaming of the production beneath it, so retaining a node per level would require three nodes to record one fact. Collapsing retains the outermost name and discards the nodes.

The list is enumerated rather than derived. <tff_arguments> ::= <tff_term> is also a single-child chain, but its child is an element rather than a renaming, and collapsing it would replace the argument's kind with :tff_arguments.

vocabularies(bnf_path)

@spec vocabularies(Path.t()) :: {binary(), [{binary(), [binary()]}]}

Builds Tptp.Bnf.Vocabulary from the :== rules that are closed word lists.

These constitute the well-formedness conditions the grammar does not enforce. The syntactic rule for <formula_role> admits any <lower_word>; the :== rule names those that are defined. fof(a, axim, p). is therefore well-formed TPTP and semantically incorrect, and that difference is reported as a warning rather than a parse failure.

Emitted as multi-clause functions over binary literals, which the compiler turns into a direct dispatch — faster than a MapSet, and every atom involved stays a compile-time one.

One value set the TPTP defines cannot appear here at all. The Non-classical Logics section of https://tptp.org/UserDocs/TPTPLanguage/TPTPLanguage.shtml describes a temporal modal axiom as $modal_axiom_Ax**Tm with Tm in {+, -}, and no grammar can state it: <dollar_word> ::- <dollar><alpha_numeric>* excludes +, so $modal_axiom_K+ lexes as two tokens and the statement does not parse. Resolving it needs a change to the BNF's token rules, which its maintainer has said will follow the first temporal logic formalised in the TPTP World. No library file uses the form.

One entry is not a :== rule and is labelled as such in the generated module. <reserved_word> does not exist in the BNF — the word "reserved" does not occur in the file — and reserved_words/1 builds the list by collecting every $-prefixed literal that appears anywhere in any alternative. That is a superset of the $-words the language defines, which is the appropriate form for Tptp.Lint.Rules.DefinedWord: a $-word outside it is certainly not TPTP's, and the cost of the few extras is a warning not raised.