tiny.smt.smtlib.parse.token

1pub const token = @import("token.zig");

1//! Splits SMT-LIB text into parentheses and atoms. Every step of the reader has to skip whitespace2//! and comments and then read one parenthesis or one atom. An atom is every character up to the3//! next whitespace or parenthesis, so the reader has no quoted symbols and no string literals.4const errors = @import("error.zig");5const state = @import("state.zig");67const Error = errors.Error;8const ParseError = errors.ParseError;9const Parser = state.Parser;1011/// Moves the position past spaces, tabs, carriage returns, newlines and `;` comments, which run to12/// the end of their line. The call returns true when a character remains, so the command reader13/// learns whether another command follows.14pub fn skipSpace(parser: *Parser) bool {15    while (parser.pos < parser.source.len) {16        switch (parser.source[parser.pos]) {17            ' ', '\t', '\r', '\n' => parser.pos += 1,18            ';' => {19                while (parser.pos < parser.source.len and parser.source[parser.pos] != '\n') parser.pos += 1;20            },21            else => return true,22        }23    }24    return false;25}2627/// Skips whitespace and comments and returns true when the next character is `(`, so the term and28/// sort readers decide between an atom and a list. The call leaves the parenthesis unconsumed.29pub fn peekLeft(parser: *Parser) bool {30    _ = skipSpace(parser);31    return parser.pos < parser.source.len and parser.source[parser.pos] == '(';32}3334/// Skips whitespace and comments and returns true when the next character is `)`, so the list35/// readers find the end of an operand list. The call leaves the parenthesis unconsumed.36pub fn peekRight(parser: *Parser) bool {37    _ = skipSpace(parser);38    return parser.pos < parser.source.len and parser.source[parser.pos] == ')';39}4041/// Skips whitespace and comments and consumes a `(` for the readers where a list has to open. The42/// call returns `ExpectedList` for any other character or the end of the text.43pub fn expectLeft(parser: *Parser) Error!void {44    if (!peekLeft(parser)) return ParseError.ExpectedList;45    parser.pos += 1;46}4748/// Skips whitespace and comments and consumes a `)` for the readers where a list has to close. The49/// call returns `ExpectedRightParen` for any other character or the end of the text.50pub fn expectRight(parser: *Parser) Error!void {51    if (!peekRight(parser)) return ParseError.ExpectedRightParen;52    parser.pos += 1;53}5455/// Skips whitespace and comments and returns the next atom: the characters up to the next56/// whitespace or parenthesis. The readers call it for every command name, operator, name and57/// number. The atom is a slice of the parser's text. The call returns `ExpectedAtom` at the end of58/// the text or at a parenthesis.59pub fn atom(parser: *Parser) Error![]const u8 {60    _ = skipSpace(parser);61    if (parser.pos >= parser.source.len) return ParseError.ExpectedAtom;62    if (parser.source[parser.pos] == '(' or parser.source[parser.pos] == ')') return ParseError.ExpectedAtom;63    const start = parser.pos;64    while (parser.pos < parser.source.len) {65        switch (parser.source[parser.pos]) {66            ' ', '\t', '\r', '\n', '(', ')' => break,67            else => parser.pos += 1,68        }69    }70    return parser.source[start..parser.pos];71}