1
2 /*
3 * File LispParser.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 LispParser.cpp
21 * Implements class LispParser
22 *
23 * @since 26/08/2009 Redmond
24 */
25
26 #include <fstream>
27
28 #include "Lib/Stack.hpp"
29 #include "Lib/Int.hpp"
30
31 #include "LispLexer.hpp"
32 #include "LispParser.hpp"
33
34 namespace Shell {
35
36 using namespace Lib;
37 using namespace Kernel;
38
LispParser(LispLexer & lexer)39 LispParser::LispParser(LispLexer& lexer)
40 : _lexer(lexer),
41 _balance(0)
42 {}
43
44 /**
45 * @since 26/08/2009 Redmond
46 */
parse()47 LispParser::Expression* LispParser::parse()
48 {
49 CALL("LispParser::parse/0");
50
51 Expression* result = new Expression(LIST);
52 parse(&result->list);
53 return result;
54 } // parse()
55
56 ///**
57 // * @since 26/08/2009 Redmond
58 // */
59 //void LispParser::parse(List** expr)
60 //{
61 // CALL("LispParser::parse/1");
62 //
63 // Token t;
64 // for (;;) {
65 // _lexer.readToken(t);
66 // switch (t.tag) {
67 // case TT_RPAR:
68 // if (_balance == 0) {
69 // throw ParserException("unmatched right parenthesis",t);
70 // }
71 // _balance--;
72 // return;
73 // case TT_LPAR:
74 // _balance++;
75 // {
76 // Expression* subexpr = new Expression(LIST);
77 // parse(&subexpr->list);
78 // List* sub = new List(subexpr);
79 // *expr = sub;
80 // expr = sub->tailPtr();
81 // }
82 // break;
83 // case TT_NAME:
84 // case TT_INTEGER:
85 // case TT_REAL:
86 // {
87 // Expression* subexpr = new Expression(ATOM,t.text);
88 // List* sub = new List(subexpr);
89 // *expr = sub;
90 // expr = sub->tailPtr();
91 // break;
92 // }
93 // case TT_EOF:
94 // if (_balance == 0) {
95 // return;
96 // }
97 // throw ParserException("unmatched left parenthesis",t);
98 //#if VDEBUG
99 // default:
100 // ASS(false);
101 //#endif
102 // }
103 // }
104 //} // parse()
105
106 /**
107 * @since 26/08/2009 Redmond
108 */
parse(List ** expr0)109 void LispParser::parse(List** expr0)
110 {
111 CALL("LispParser::parse/1");
112
113 static Stack<List**> stack;
114 stack.reset();
115
116 stack.push(expr0);
117
118 Token t;
119
120 List** expr = expr0;
121 for(;;) {
122 new_parsing_level:
123 for (;;) {
124 _lexer.readToken(t);
125 switch (t.tag) {
126 case TT_RPAR:
127 if (_balance == 0) {
128 throw Exception("unmatched right parenthesis",t);
129 }
130 _balance--;
131 goto parsing_level_done;
132 case TT_LPAR:
133 _balance++;
134 {
135 Expression* subexpr = new Expression(LIST);
136 List* sub = new List(subexpr);
137 *expr = sub;
138 expr = sub->tailPtr();
139 stack.push(expr);
140 expr = &subexpr->list;
141 goto new_parsing_level;
142 }
143 break;
144 case TT_NAME:
145 case TT_INTEGER:
146 case TT_REAL:
147 {
148 Expression* subexpr = new Expression(ATOM,t.text);
149 List* sub = new List(subexpr);
150 *expr = sub;
151 expr = sub->tailPtr();
152 break;
153 }
154 case TT_EOF:
155 if (_balance == 0) {
156 return;
157 }
158 throw Exception("unmatched left parenthesis",t);
159 #if VDEBUG
160 default:
161 ASSERTION_VIOLATION;
162 #endif
163 }
164 }
165
166 parsing_level_done:
167 ASS(stack.isNonEmpty());
168 expr = stack.pop();
169 }
170
171 } // parse()
172
173 /**
174 * Return a LISP string corresponding to this expression
175 * @since 26/08/2009 Redmond
176 */
toString(bool outerParentheses) const177 vstring LispParser::Expression::toString(bool outerParentheses) const
178 {
179 CALL("LispParser::Expression::toString");
180
181 switch (tag) {
182 case ATOM:
183 return str;
184 case LIST:
185 {
186 vstring result;
187 if(outerParentheses) {
188 result = "(";
189 }
190 for (List* l = list;l;l = l->tail()) {
191 result += l->head()->toString();
192 if (l->tail()) {
193 result += outerParentheses ? ' ' : '\n';
194 }
195 }
196 if(outerParentheses) {
197 result += ')';
198 }
199 return result;
200 }
201 }
202 ASSERTION_VIOLATION;
203 } // LispParser::Expression::toString
204
205 /**
206 * If expression corresponds to a unary function named @c funcionName,
207 * return true and assign its argument to @c arg. Otherwise return false.
208 */
get1Arg(vstring functionName,Expression * & arg)209 bool LispParser::Expression::get1Arg(vstring functionName, Expression*& arg)
210 {
211 CALL("LispParser::Expression::get1Arg");
212
213 if(!isList()) {
214 return false;
215 }
216
217 List::Iterator args(list);
218 if(!args.hasNext()) { return false; }
219 vstring name = args.next()->str;
220 if(name!=functionName) { return false; }
221
222 if(!args.hasNext()) { return false; }
223 Expression* tmpArg = args.next();
224
225 if(args.hasNext()) { return false; }
226
227 arg = tmpArg;
228 return true;
229 }
230
231 /**
232 * If expression corresponds to a binary function named @c funcionName,
233 * return true and assign its arguments to @c arg1 and @c arg2. Otherwise
234 * return false.
235 */
get2Args(vstring functionName,Expression * & arg1,Expression * & arg2)236 bool LispParser::Expression::get2Args(vstring functionName, Expression*& arg1, Expression*& arg2)
237 {
238 CALL("LispParser::Expression::get2Args");
239
240 if(!isList()) {
241 return false;
242 }
243
244 List::Iterator args(list);
245 if(!args.hasNext()) { return false; }
246 vstring name = args.next()->str;
247 if(name!=functionName) { return false; }
248
249 if(!args.hasNext()) { return false; }
250 Expression* tmpArg1 = args.next();
251
252 if(!args.hasNext()) { return false; }
253 Expression* tmpArg2 = args.next();
254
255 if(args.hasNext()) { return false; }
256
257 arg1 = tmpArg1;
258 arg2 = tmpArg2;
259 return true;
260 }
261
262 /**
263 * If expression is a list of two elements, return true and assign them
264 * into @c el1 and @c el2.
265 */
getPair(Expression * & el1,Expression * & el2)266 bool LispParser::Expression::getPair(Expression*& el1, Expression*& el2)
267 {
268 CALL("LispParser::Expression::getPair");
269
270 if(!isList()) {
271 return false;
272 }
273
274 List::Iterator args(list);
275 if(!args.hasNext()) { return false; }
276 Expression* tmpEl1 = args.next();
277
278 if(!args.hasNext()) { return false; }
279 Expression* tmpEl2 = args.next();
280
281 if(args.hasNext()) { return false; }
282
283 el1 = tmpEl1;
284 el2 = tmpEl2;
285 return true;
286 }
287
getSingleton(Expression * & el)288 bool LispParser::Expression::getSingleton(Expression*& el)
289 {
290 CALL("LispParser::Expression::getSingleton");
291
292 if(!isList()) {
293 return false;
294 }
295
296 List::Iterator args(list);
297 if(!args.hasNext()) { return false; }
298 Expression* tmpEl = args.next();
299
300 if(args.hasNext()) { return false; }
301
302 el = tmpEl;
303 return true;
304 }
305
306 /**
307 * Create a new parser exception.
308 * @since 17/07/2004 Turku
309 */
Exception(vstring message,const Token & token)310 LispParser::Exception::Exception(vstring message,const Token& token)
311 : _message (message)
312 {
313 _message += " in line ";
314 _message += Int::toString(token.line);
315 _message += " at ";
316 _message += token.text;
317 } // LispParser::Exception::Exception
318
319 /**
320 * Write itself to an ostream.
321 * @since 17/07/2004 Helsinki Airport
322 */
cry(ostream & out)323 void LispParser::Exception::cry(ostream& out)
324 {
325 out << "Parser exception: " << _message << '\n';
326 } // Exception::cry
327
328 ///////////////////////
329 // LispListReader
330 //
331
lispError(LExpr * expr,vstring reason)332 void LispListReader::lispError(LExpr* expr, vstring reason)
333 {
334 CALL("LispListReader::lispError");
335
336 if(expr) {
337 USER_ERROR(reason+": "+expr->toString());
338 }
339 else {
340 USER_ERROR(reason+": <eol>");
341 }
342 }
343
344 /**
345 * Report error with the current lisp element
346 */
lispCurrError(vstring reason)347 void LispListReader::lispCurrError(vstring reason)
348 {
349 CALL("LispListReader::lispCurrError");
350
351 if(hasNext()) {
352 lispError(peekAtNext(), reason);
353 }
354 else {
355 lispError(0, reason);
356 }
357 }
358
peekAtNext()359 LExpr* LispListReader::peekAtNext()
360 {
361 CALL("LispListReader::peekAtNext");
362 ASS(hasNext());
363
364 return it.peekAtNext();
365 }
366
readNext()367 LExpr* LispListReader::readNext()
368 {
369 CALL("LispListReader::readNext");
370 ASS(hasNext());
371
372 return it.next();
373 }
374
tryReadAtom(vstring & atom)375 bool LispListReader::tryReadAtom(vstring& atom)
376 {
377 CALL("LispListReader::tryReadAtom");
378
379 if(!hasNext()) { return false; }
380
381 LExpr* next = peekAtNext();
382 if(next->isAtom()) {
383 atom = next->str;
384 ALWAYS(readNext()==next);
385 return true;
386 }
387 return false;
388 }
389
readAtom()390 vstring LispListReader::readAtom()
391 {
392 CALL("LispListReader::readAtom");
393
394 vstring atm;
395 if(!tryReadAtom(atm)) {
396 lispCurrError("atom expected");
397 }
398 return atm;
399 }
400
tryAcceptAtom(vstring atom)401 bool LispListReader::tryAcceptAtom(vstring atom)
402 {
403 CALL("SMTLIBConcat::tryAcceptAtom");
404
405 if(!hasNext()) { return false; }
406
407 LExpr* next = peekAtNext();
408 if(next->isAtom() && next->str==atom) {
409 ALWAYS(readNext()==next);
410 return true;
411 }
412 return false;
413 }
414
acceptAtom(vstring atom)415 void LispListReader::acceptAtom(vstring atom)
416 {
417 CALL("SMTLIBConcat::acceptAtom");
418
419 if(!tryAcceptAtom(atom)) {
420 lispCurrError("atom \""+atom+"\" expected");
421 }
422 }
423
tryReadListExpr(LExpr * & e)424 bool LispListReader::tryReadListExpr(LExpr*& e)
425 {
426 CALL("LispListReader::tryReadListExpr");
427
428 if(!hasNext()) { return false; }
429
430 LExpr* next = peekAtNext();
431 if(next->isList()) {
432 e = next;
433 ALWAYS(readNext()==next);
434 return true;
435 }
436 return false;
437 }
438
readListExpr()439 LExpr* LispListReader::readListExpr()
440 {
441 CALL("LispListReader::readListExpr");
442
443 LExpr* list;
444 if(!tryReadListExpr(list)) {
445 lispCurrError("list expected");
446 }
447 return list;
448 }
449
tryReadList(LExprList * & list)450 bool LispListReader::tryReadList(LExprList*& list)
451 {
452 CALL("LispListReader::tryReadList");
453
454 LExpr* lstExpr;
455 if(tryReadListExpr(lstExpr)) {
456 list = lstExpr->list;
457 return true;
458 }
459 return false;
460 }
461
readList()462 LExprList* LispListReader::readList()
463 {
464 CALL("LispListReader::readList");
465
466 return readListExpr()->list;
467 }
468
tryAcceptList()469 bool LispListReader::tryAcceptList()
470 {
471 CALL("LispListReader::tryAcceptList");
472 LExprList* lst;
473 return tryReadList(lst);
474 }
acceptList()475 void LispListReader::acceptList()
476 {
477 CALL("LispListReader::acceptList");
478 readList();
479 }
480
acceptEOL()481 void LispListReader::acceptEOL()
482 {
483 CALL("LispListReader::acceptEOL");
484
485 if(hasNext()) {
486 lispCurrError("<eol> expected");
487 }
488 }
489
lookAheadAtom(vstring atom)490 bool LispListReader::lookAheadAtom(vstring atom)
491 {
492 CALL("LispListReader::lookAheadAtom");
493
494 if(!hasNext()) { return false; }
495 LExpr* next = peekAtNext();
496 return next->isAtom() && next->str==atom;
497 }
498
tryAcceptCurlyBrackets()499 bool LispListReader::tryAcceptCurlyBrackets()
500 {
501 CALL("LispListReader::tryAcceptCurlyBrackets");
502
503 LExpr* next = peekAtNext();
504 if(!next->isAtom() || next->str!="{") {
505 return false;
506 }
507 unsigned depth = 1;
508 readNext();
509 while(depth!=0 && hasNext()) {
510 next = readNext();
511
512 if(!next->isAtom()) {
513 continue;
514 }
515 if(next->str=="{") {
516 depth++;
517 }
518 else if(next->str=="}") {
519 depth--;
520 }
521 }
522 if(depth!=0) {
523 lispCurrError("unpaired opening curly bracket");
524 }
525 return true;
526 }
527
528 }
529