Tokenises TPTP source, one statement per call.

Resumability

The scanner is resumable over (source, offset) and returns the tokens of a single statement per call. The source is retained whole as one reference-counted binary; the token stream is not materialised. Peak memory is therefore bounded by the largest statement rather than by the size of the input, which matters at the scale of the larger TPTP axiom sets: 75 million tokens held as three-tuples require approximately 2.4 GB.

Byte-oriented matching

Every character class in the BNF lies within 40–176, so byte matching is correct and the UTF-8 aware, grapheme-based functions of String are both unnecessary and slower. This module uses byte patterns and :binary throughout.

Non-ASCII bytes can occur only inside a quoted atom or a comment in non-conforming input. They are carried through without validation, since validating them would introduce a branch per byte of every string for a condition a lint rule can evaluate from the token text.

Token representation

A token is {category, offset, length}. Text is recovered later with binary_part/3, so scanning allocates nothing per token beyond the tuple.

Longest match

The operator clauses are generated from Tptp.Token.operators/0, which is ordered by descending spelling length, so <=> is attempted before <= before < as a property of the table rather than of the clause order.

Three cases are not resolved by the table alone:

• Statement terminator against decimal point. Numbers are scanned from their leading digit and consume their own .; the terminator clause applies only to a . not followed by a digit. p(3). is therefore terminated correctly, since <decimal_fraction> requires digits after the point.
• Words are scanned to their end rather than truncated at a prefix that forms a keyword. $letter is a single dollar_word and filename a single lower_word. Tptp.Splitter relies on this when resolving keywords by whole-word comparison.
• [.], <.>, {.} and (.) are single tokens. Without this, <.> would introduce a . at bracket depth zero and divide a statement.

Accepted departures from the BNF

Two forms lex without ambiguity but are not admitted by the BNF. Each yields a token together with a warning, rather than being silently accepted or rejected:

• Empty quoted token. <single_quoted> requires at least one <sq_char> and <distinct_object> at least one <do_char>, so neither '' nor "" is admitted (TPTP0107).
• Redundant leading zero. <unsigned_integer> is 0 or a digit sequence beginning 1–9, so 00, -007 and 01.5 are not admitted (TPTP0110). A rational's denominator is a <positive_integer>, which may not begin with 0, so neither 1/02 nor 1/0 is a <rational> (TPTP0111).

Emitting the token allows the statement to parse, which is why these are warnings. That the list is exactly these two is checked rather than asserted: Tptp.Bnf.OracleTable transcribes the ::- and ::: rules mechanically, and Tptp.LexerOracleTest verifies that every token emitted without a diagnostic satisfies its BNF pattern.

Deferred decisions

This module emits lower_word for fof, inference and file, and dollar_word for $let and $thf. These are ordinary words except in positions that admit a keyword reading, and position is resolved by Tptp.Splitter: the first token of a statement, and a word immediately preceding (. Resolving them here would reject fof(fof, axiom, p)., which is well formed, and would divide keyword resolution across two modules.

Comments

The BNF permits comments between any two tokens but does not treat them as white space. They are collected into a separate ordered list rather than the token stream, so the parser does not observe them and the format-preserving printer can reattach them by position. %$ and /*$ introduce a defined comment and %$$ and /*$$ a system comment; both are reserved by the BNF and used by some tools, so the classification is retained.