The terminal vocabulary of the TPTP grammar.
This module is the single source of truth shared by three consumers:
Tptp.Bnf.Generator, which resolves the literal text appearing in::=rules to terminal atoms when it emitssrc/tptp_parser.yrl;Tptp.Lexer, which emits these atoms as token categories;Tptp.Printer.Canonical, which turns them back into bytes.
A token is a plain three-tuple {category, offset, length} — never a struct and
never carrying a binary. yecc reads elem(token, 0) as the category and
elem(token, 1) as the position, so a parse error reports a byte offset
directly. Token text is recovered with binary_part/3 during the CST post-pass,
which keeps the scan loop free of binary allocation.
Every atom named here is created at compile time. Nothing in this library ever
calls String.to_atom/1 on input; see Tptp.Checks.NoDynamicAtoms, the custom
Credo check that enforces it mechanically.
Summary
Types
A terminal category. Always a compile-time atom.
A lexed token: category, byte offset, byte length.
Functions
Every terminal category, operators and keywords and value categories alike.
The category for a literal spelling as it appears in the BNF, or nil.
The six $-word keywords, which are also legal <dollar_word>s.
Operators and punctuation only, longest spelling first.
Whether a category is pure punctuation, and so dropped from the CST.
The four <source> keywords, which are also legal <atomic_word>s.
The fixed text of a category, or nil for a value-carrying category.
{category, spelling} pairs for every fixed-text terminal, longest spelling first.
The seven language keywords that open a statement.
Categories whose text must be carried because the category does not determine it.
Types
@type category() :: atom()
A terminal category. Always a compile-time atom.
@type t() :: {category(), non_neg_integer(), non_neg_integer()}
A lexed token: category, byte offset, byte length.
Functions
@spec categories() :: [category()]
Every terminal category, operators and keywords and value categories alike.
The category for a literal spelling as it appears in the BNF, or nil.
iex> Tptp.Token.category_for("~|")
:nor
iex> Tptp.Token.category_for("wibble")
nilThe six $-word keywords, which are also legal <dollar_word>s.
Operators and punctuation only, longest spelling first.
This is what Tptp.Lexer generates its scan clauses from. Keywords are excluded
deliberately: a keyword must be recognised by scanning the whole word and then
looking it up, never by matching a prefix, or filename lexes as file followed
by name.
Whether a category is pure punctuation, and so dropped from the CST.
iex> Tptp.Token.punctuation?(:comma)
true
iex> Tptp.Token.punctuation?(:ampersand)
falseThe four <source> keywords, which are also legal <atomic_word>s.
The fixed text of a category, or nil for a value-carrying category.
iex> Tptp.Token.spelling(:iff)
"<=>"
iex> Tptp.Token.spelling(:lower_word)
nil{category, spelling} pairs for every fixed-text terminal, longest spelling first.
Sorted so that a caller matching prefixes in list order gets maximal munch for free.
The seven language keywords that open a statement.
@spec value_categories() :: [category()]
Categories whose text must be carried because the category does not determine it.