lib/smt/src/smtlib/parse/token.zig

daab053ee43316e1809a84551d573ddd1e5bf3d2

 1 //! Splits SMT-LIB text into parentheses and atoms. Every step of the reader has to skip whitespace
 2 //! and comments and then read one parenthesis or one atom. An atom is every character up to the
 3 //! next whitespace or parenthesis, so the reader has no quoted symbols and no string literals.
 4 const errors = @import("error.zig");
 5 const state = @import("state.zig");
 6 
 7 const Error = errors.Error;
 8 const ParseError = errors.ParseError;
 9 const Parser = state.Parser;
10 
11 /// Moves the position past spaces, tabs, carriage returns, newlines and `;` comments, which run to
12 /// the end of their line. The call returns true when a character remains, so the command reader
13 /// learns whether another command follows.
14 pub 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 }
26 
27 /// Skips whitespace and comments and returns true when the next character is `(`, so the term and
28 /// sort readers decide between an atom and a list. The call leaves the parenthesis unconsumed.
29 pub fn peekLeft(parser: *Parser) bool {
30     _ = skipSpace(parser);
31     return parser.pos < parser.source.len and parser.source[parser.pos] == '(';
32 }
33 
34 /// Skips whitespace and comments and returns true when the next character is `)`, so the list
35 /// readers find the end of an operand list. The call leaves the parenthesis unconsumed.
36 pub fn peekRight(parser: *Parser) bool {
37     _ = skipSpace(parser);
38     return parser.pos < parser.source.len and parser.source[parser.pos] == ')';
39 }
40 
41 /// Skips whitespace and comments and consumes a `(` for the readers where a list has to open. The
42 /// call returns `ExpectedList` for any other character or the end of the text.
43 pub fn expectLeft(parser: *Parser) Error!void {
44     if (!peekLeft(parser)) return ParseError.ExpectedList;
45     parser.pos += 1;
46 }
47 
48 /// Skips whitespace and comments and consumes a `)` for the readers where a list has to close. The
49 /// call returns `ExpectedRightParen` for any other character or the end of the text.
50 pub fn expectRight(parser: *Parser) Error!void {
51     if (!peekRight(parser)) return ParseError.ExpectedRightParen;
52     parser.pos += 1;
53 }
54 
55 /// Skips whitespace and comments and returns the next atom: the characters up to the next
56 /// whitespace or parenthesis. The readers call it for every command name, operator, name and
57 /// number. The atom is a slice of the parser's text. The call returns `ExpectedAtom` at the end of
58 /// the text or at a parenthesis.
59 pub 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 }