# `Tptp.Lexer` [🔗](https://github.com/jcschuster/tptp/blob/v0.1.3/lib/tptp/lexer.ex#L1) 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 `` 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.** `` requires at least one `` and `` at least one ``, so neither `''` nor `""` is admitted (`TPTP0107`). * **Redundant leading zero.** `` 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 ``, which may not begin with `0`, so neither `1/02` nor `1/0` is a `` (`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. # `comment` ```elixir @type comment() :: {offset :: non_neg_integer(), length :: non_neg_integer(), :line | :block, :plain | :defined | :system} ``` Where a comment came from, and whether it is a pragma. # `result` ```elixir @type result() :: {:statement, [Tptp.Token.t()], non_neg_integer(), [comment()], [Tptp.Diagnostic.t()]} | {:eof, non_neg_integer(), [comment()], [Tptp.Diagnostic.t()]} ``` One call's worth of scanning. `:statement` carries the tokens up to and including a bracket-depth-zero `.`; `:eof` means the input was exhausted. Both carry the comments and diagnostics seen along the way and the offset to resume from. # `comment_text` ```elixir @spec comment_text(comment(), binary()) :: binary() ``` The bytes a comment covers, including its `%` or `/* */` delimiters. # `next_statement` ```elixir @spec next_statement(binary(), non_neg_integer(), Tptp.Span.file_id()) :: result() ``` Scan the next statement starting at `offset`. `file` is stamped into any diagnostic's span; it is the id under which the caller registered this source, and defaults to zero for a single-file scan. iex> {:statement, tokens, next, [], []} = Tptp.Lexer.next_statement("fof(a,axiom,p).", 0) iex> Enum.map(tokens, &elem(&1, 0)) [:lower_word, :lparen, :lower_word, :comma, :lower_word, :comma, :lower_word, :rparen, :dot] iex> next 15 # `statements` ```elixir @spec statements(binary(), Tptp.Span.file_id()) :: {[[Tptp.Token.t()]], [comment()], [Tptp.Diagnostic.t()]} ``` Scan an entire source into statements, eagerly. A convenience over `next_statement/3` for small inputs and for tests. Anything large should go through the streaming path instead, for the reason in the moduledoc. # `text` ```elixir @spec text(Tptp.Token.t(), binary()) :: binary() ``` The bytes a token covers. A sub-binary, not a copy. See `Tptp.Span.text/2` for when that matters. --- *Consult [api-reference.md](api-reference.md) for complete listing*