1
2 /*
3 * File PARSER_TKV.cpp.
4 *
5 * This file is part of the source code of the software program
6 * Vampire. It is protected by applicable
7 * copyright laws.
8 *
9 * This source code is distributed under the licence found here
10 * https://vprover.github.io/license.html
11 * and in the source directory
12 *
13 * In summary, you are allowed to use Vampire for non-commercial
14 * purposes but not allowed to distribute, modify, copy, create derivatives,
15 * or use in competitions.
16 * For other uses of Vampire please contact developers for a different
17 * licence, which we will make an effort to provide.
18 */
19 /**
20 * @file Parser_TKV.cpp
21 * Implements class Parser
22 *
23 * @since 14/07/2004 Turku
24 */
25
26 #include "Debug/Assertion.hpp"
27 #include "Debug/Tracer.hpp"
28 #include "Lib/Int.hpp"
29
30 #include "Lib/IntNameTable.hpp"
31
32 #include "Lexer.hpp"
33 #include "PARSER_TKV.hpp"
34
35 using namespace Lib;
36 using namespace Shell;
37
38 /**
39 * Initialise a parser.
40 * @since 17/07/2004 Helsinki Airport
41 */
Parser(Lexer & lexer)42 Parser::Parser (Lexer& lexer)
43 :
44 _lexer(lexer),
45 _tokenCursor(0),
46 _noOfTokens(0)
47 {
48 } // Parser::Parser
49
50
51 /**
52 * Create a new parser exception.
53 * @since 17/07/2004 Turku
54 */
ParserException(vstring message,const Token & token)55 ParserException::ParserException (vstring message,const Token& token)
56 : _message (message)
57 {
58 _message += " in line ";
59 _message += Int::toString(token.line);
60 _message += " at ";
61 _message += token.text;
62 } // ParserException::ParserException
63
64
65 /**
66 * Write itself to an ostream.
67 * @since 17/07/2004 Helsinki Airport
68 */
cry(ostream & out)69 void ParserException::cry (ostream& out)
70 {
71 out << "Parser exception: " << _message << '\n';
72 } // ParserException::cry
73
74 /**
75 * Read and consume a token of type tt. If the buffer contains
76 * no tokens, one will be read.
77 * @throws ParserException if the next token has a wrong type
78 */
consumeToken(TokenType tt)79 void Parser::consumeToken (TokenType tt)
80 {
81 CALL("Parser::consumeToken/1");
82
83 if (currentToken1().tag != tt) {
84 throw ParserException(Token::toString(tt) + " expected",
85 _tokens[_tokenCursor]);
86 }
87 consumeToken();
88 } // Parser::consumeToken
89
90 /**
91 * Check that the current token has type tt.
92 * @throws ParserException if it has a wrong type
93 * @pre The buffer must contain at least one token
94 */
expectToken(TokenType tt)95 void Parser::expectToken (TokenType tt)
96 {
97 CALL("Parser::expectToken/1");
98
99 if (currentToken().tag != tt) {
100 throw ParserException(Token::toString(tt) + " expected",
101 _tokens[_tokenCursor]);
102 }
103 } // Parser::expectToken
104
105 /**
106 * Check that the current token has type tt.
107 * @throws ParserException with the given error message if it has a wrong type
108 * @pre The buffer must contain at least one token
109 */
expectToken(TokenType tt,vstring errorMessage)110 void Parser::expectToken (TokenType tt,vstring errorMessage)
111 {
112 CALL("Parser::expectToken/2");
113
114 if (currentToken().tag != tt) {
115 throw ParserException(errorMessage,
116 _tokens[_tokenCursor]);
117 }
118 } // Parser::expectToken
119
120 /**
121 * Check that the current token's text is @b keyword
122 * @throws ParserException if it the text is different and complains
123 * that this keyword is expected
124 * @pre The buffer must contain at least one token
125 */
expectKeyword(const char * keyword)126 void Parser::expectKeyword (const char* keyword)
127 {
128 CALL("Parser::expectKeyword");
129
130 if (currentToken().text != keyword) {
131 throw ParserException((vstring)"keyword '" + keyword + "' expected",
132 _tokens[_tokenCursor]);
133 }
134 } // Parser::expectKeyword
135
136
137 /**
138 * Move to the next token.
139 * @pre buffer must contain at least one token
140 * @since 15/07/2004 Turku
141 */
consumeToken()142 void Parser::consumeToken ()
143 {
144 CALL("Parser::consumeToken/0");
145
146 ASS (_noOfTokens > 0);
147 ASS (_tokenCursor < TOKEN_BUFFER_SIZE);
148
149 _tokenCursor = (_tokenCursor+1) % TOKEN_BUFFER_SIZE;
150 _noOfTokens--;
151 } // Parser::consumeToken()
152
153
154 /**
155 * Append the next token returned by the lexer to the end of the buffer
156 * @since 15/07/2004 Turku, implemented as a Lexer method
157 * @since 24/07/2004 Torrevieja
158 * @pre buffer content must be less than its capacity
159 */
readToken()160 void Parser::readToken ()
161 {
162 CALL("Parser::readToken");
163
164 ASS(_noOfTokens <= TOKEN_BUFFER_SIZE);
165
166 if (_noOfTokens == TOKEN_BUFFER_SIZE) {
167 _lexer.readToken(_tokens[0]);
168 // cout << _tokens[0].text << "\n";
169 throw ParserException("token buffer capacity exceeded",_tokens[0]);
170 }
171
172 int tokenIndex = (_tokenCursor + _noOfTokens) % TOKEN_BUFFER_SIZE;
173 _noOfTokens++;
174 _lexer.readToken(_tokens[tokenIndex]);
175 // cout << _tokens[tokenIndex].text << "\n";
176 } // Parser::readToken
177
178
179 /**
180 * Append the next token returned by the lexer to the end of the buffer
181 * and check that its type is @b tt. The same as the combination of
182 * readToken() and expectToken(tt)
183 * @pre buffer content must be less than its capacity
184 * @throws ParserException if the next token has a wrong type.
185 * @since 26/01/2009 Heathrow
186 */
readToken(TokenType tt)187 void Parser::readToken(TokenType tt)
188 {
189 CALL("Parser::readToken/1");
190 readToken();
191 expectToken(tt);
192 } // Parser::readToken
193
194 /**
195 * Append the next token returned by the lexer to the end of the buffer
196 * and check that its type is @b tt.
197 * Otherwise, throw an error with the given error message.
198 * The same as the combination of
199 * readToken() and expectToken(tt,errorMessage)
200 * @pre buffer content must be less than its capacity
201 * @throws ParserException if the next token has a wrong type.
202 * @since 26/01/2009 Heathrow
203 */
readToken(TokenType tt,vstring errorMessage)204 void Parser::readToken(TokenType tt,vstring errorMessage)
205 {
206 CALL("Parser::readToken/2");
207 readToken();
208 expectToken(tt,errorMessage);
209 } // Parser::readToken
210
211
212 /**
213 * Return the current token.
214 * @pre buffer must contain at least one token
215 * @since 03/12/2006 Haifa
216 */
currentToken()217 Token& Parser::currentToken()
218 {
219 CALL("Parser::currentToken");
220 ASS(_noOfTokens > 0);
221
222 return _tokens[_tokenCursor % TOKEN_BUFFER_SIZE];
223 } // currentToken
224
225 /**
226 * Read tokens up to the index token and return the lookahead token.
227 * If the buffer does not contain enough tokens, a sufficient number
228 * of them will be read.
229 * @pre index of the lookehead token must be less than the capacity of
230 * the buffer
231 *
232 * @since 15/07/2004 Turku
233 */
lookAhead(int index)234 Token& Parser::lookAhead (int index)
235 {
236 CALL("Parser::lookahead");
237
238 ASS (index < TOKEN_BUFFER_SIZE);
239 ASS(index > 0);
240
241 while (_noOfTokens <= index) {
242 readToken();
243 }
244 return _tokens[(_tokenCursor+index) % TOKEN_BUFFER_SIZE];
245 } // Parser::lookAhead()
246
247
248 /**
249 * Convert the token text into a variable number. No check is made
250 * whether the token type is TT_VAR.
251 *
252 * @since 26/07/2004 Torrevieja
253 */
var(const Token & t)254 int Parser::var (const Token& t)
255 {
256 CALL("Parser::var");
257 return _vars.insert(t.text);
258 } // Parser::var
259
260
261 /**
262 * Convert the token text into a double floating-point number.
263 * No check is made whether the token type is TT_REAL or TT_INTEGER.
264 *
265 * @since 02/08/2004 Torrevieja
266 */
real(const Token & token)267 double Parser::real (const Token& token)
268 {
269 CALL("Parser::real");
270 double d;
271
272 if (! Int::stringToDouble(token.text.c_str(),d)) {
273 throw ParserException("incorrect floating point number",token);
274 }
275 return d;
276 } // Parser::real
277
278
279 /**
280 * Convert the token text into an integer.
281 * No check is made whether the token type is TT_REAL or TT_INTEGER.
282 *
283 * @since 28/09/2004 Manchester
284 */
integer(const Token & token)285 int Parser::integer (const Token& token)
286 {
287 CALL("Parser::integer");
288
289 int result;
290 if (Int::stringToInt(const_cast<vstring&>(token.text),result)) {
291 return result;
292 }
293 throw ParserException("incorrect integer",token);
294 } // Parser::integer
295
296 /**
297 * Convert the token text into a 64-bit unsigned.
298 * No check is made whether the token type is TT_REAL or TT_INTEGER.
299 *
300 * @since 30/11/2006 Haifa
301 */
unsigned64(const Token & token)302 long long unsigned Parser::unsigned64 (const Token& token)
303 {
304 CALL("Parser:unsigned64");
305
306 long long unsigned result;
307
308 if (Int::stringToUnsigned64(const_cast<vstring&>(token.text),result)) {
309 return result;
310 }
311 throw ParserException("incorrect 64-bit unsigned",token);
312 } // Parser::unsigned64
313
314 /**
315 * Terminate by throwing an exception with a given error message
316 * @since 27/01/2009 Manchester
317 */
terminate(vstring errorMessage)318 void Parser::terminate(vstring errorMessage)
319 {
320 throw ParserException(errorMessage,_tokens[_tokenCursor]);
321 } // terminate
322
323