Reader for the upstream TPTP SyntaxBNF file.
The BNF uses four separators, and which one a rule carries decides where the rule ends up:
| Separator | Meaning | Destination |
|---|---|---|
::= | syntactic rule | the generated src/tptp_parser.yrl |
:== | semantic rule | Tptp.Bnf.Vocabulary and the lint rules |
::- | token rule | Tptp.Lexer and the regex oracle |
::: | character class | Tptp.Lexer and the regex oracle |
Folding the :== layer into the grammar is how a TPTP parser ends up rejecting
files that tptp4X accepts: <formula_role> ::= <lower_word> accepts any
lower word, and only the :== rule lists the thirteen that mean something. So
this reader keeps the layers separate and hands the :== rules to the linter.
Only ::= and :== rules get their right-hand sides parsed into symbols; ::-
and ::: rules keep their raw regex-ish text, because that is what
Tptp.Bnf.Generator needs to emit the conformance oracle.
Summary
Functions
Map from nonterminal name to the separator that defines it.
Merge rules sharing a left-hand side and separator into one rule.
Read a SyntaxBNF file into rules, in source order.
The single vendored BNF under priv/bnf.
The BNF version, taken from the filename (SyntaxBNF-v9.3.1.3 -> "9.3.1.3").
Rules carrying the given separator, in source order.
Functions
@spec definitions([Tptp.Bnf.Rule.t()]) :: %{required(binary()) => binary()}
Map from nonterminal name to the separator that defines it.
When a name carries both a ::= and a :== rule — fourteen do, including
<formula_role> and <thf_unitary_type> — the ::= rule wins, because that is
the layer the parser is built from.
@spec merge_alternatives([Tptp.Bnf.Rule.t()]) :: [Tptp.Bnf.Rule.t()]
Merge rules sharing a left-hand side and separator into one rule.
<defined_predicate> and <defined_proposition> each carry two :== rules
whose alternatives belong to a single set; without merging, the second silently
shadows the first.
@spec read!(Path.t()) :: [Tptp.Bnf.Rule.t()]
Read a SyntaxBNF file into rules, in source order.
Raises File.Error if the path does not exist. Malformed rules raise
ArgumentError with the line number — this reader only ever runs on a vendored
file at generation time, so failing loudly is the right behaviour. (The rule that
the library never raises on input applies to TPTP input, not to our own BNF.)
@spec vendored_path!() :: Path.t()
The single vendored BNF under priv/bnf.
Raises if there is not exactly one, which keeps a half-finished version bump from silently shipping the wrong grammar.
The BNF version, taken from the filename (SyntaxBNF-v9.3.1.3 -> "9.3.1.3").
@spec with_separator([Tptp.Bnf.Rule.t()], binary()) :: [Tptp.Bnf.Rule.t()]
Rules carrying the given separator, in source order.