# `Tptp.Bnf.Generator` [🔗](https://github.com/jcschuster/tptp/blob/v0.1.3/lib/tptp/bnf/generator.ex#L1) 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`. * **``.** An alternative consisting only of `` 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.** ` ::= !` yields `%Tptp.Node{kind: :forall}` rather than a wrapper around a token, which gives the polymorphic constants of TH1 — ` ::= !! | ?? | @@+ | @@- | @=` — 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 `` 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. ` ::= []` is such a node and denotes something different. ## Departures Three, 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 fourth cannot be introduced without appearing in the output intended to surface it. A fourth was needed until the BNF's maintainer removed `unknown` from ``, which conflicted with ` -> `; `unknown` still parses by the latter route. 1. `inference`, `introduced` and `file` are given terminals of their own and are also admitted as ``, so that `fof(file, axiom, p).` continues to parse. The `(` lookahead separates the two readings. In `` position they are relabelled `lower_word`, their keyword status being an artefact of parsing. 2. The six `$`-keywords — `$thf`, `$tff`, `$fof`, `$cnf`, `$fot` and `$let` — are reserved, and are not admitted as ``. Admitting `$let` would render `$let(a,b,c)` ambiguous between `` and ``. 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. 3. The five `$`-language markers — `$thf`, `$tff`, `$fof`, `$cnf` and `$fot` — retain their terminals as children of ``, 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 ``. This is what admits `fof(fof, axiom, p).` # `grammar` ```elixir @type grammar() :: %{required(binary()) => [[symbol()]]} ``` Nonterminal name to its alternatives, each a sequence of symbols. # `report` ```elixir @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()], injected: non_neg_integer(), departures: [binary()] } ``` Statistics and departures, for the task to report. # `symbol` ```elixir @type symbol() :: {:nonterminal, binary()} | {:terminal, Tptp.Token.category()} | {:repeat, binary()} ``` A resolved grammar symbol. # `departures` ```elixir @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() 3 # `generate` ```elixir @spec generate(Path.t()) :: {binary(), report()} ``` Build the `.yrl` source and a report from a BNF file. # `reserved_words` ```elixir @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: ` :== $domains ` 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 — ` :== $ite(,…)` 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` ```elixir @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: `` 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 — ` ::= ()` 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 ` ::= ,` 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` ```elixir @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 — ``, ``, `` 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. ` ::= ` 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` ```elixir @spec vocabularies(Path.t(), 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 `` admits any ``; 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 describes a temporal modal axiom as `$modal_axiom_`*Ax**Tm* with *Tm* in `{+, -}`, and no grammar can state it: ` ::- *` 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. Two entries are not closed `:==` rules of the `SyntaxBNF`, and each is labelled as such in the generated module. `` 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. `` is referenced by ` :== status()` and defined in neither file under that name. The `SyntaxBNF` stopped defining it when the SZS ontologies moved to a BNF of their own, and `SZSOntology.bnf` states the list as ``. The entry is taken from there and emitted under the name the `SyntaxBNF` references. Generation fails if the `SyntaxBNF` defines `` again or stops referencing it, since either ends the arrangement this documents. --- *Consult [api-reference.md](api-reference.md) for complete listing*