1 /*-----------------------------------------------------------------------
2
3 File : cio_basicparser.c
4
5 Author: Stephan Schulz
6
7 Contents
8
9 Parsing routines for useful C build-in Datatypes not covered by the
10 scanner.
11
12 Copyright 1998, 1999 by the author.
13 This code is released under the GNU General Public Licence and
14 the GNU Lesser General Public License.
15 See the file COPYING in the main E directory for details..
16 Run "eprover -h" for contact information.
17
18 Changes
19
20 <1> Sat Jul 5 02:28:25 MET DST 1997
21 New
22
23 -----------------------------------------------------------------------*/
24
25
26 #include <stdlib.h>
27 #include "cio_basicparser.h"
28
29
30 /*---------------------------------------------------------------------*/
31 /* Global Variables */
32 /*---------------------------------------------------------------------*/
33
34
35 /*---------------------------------------------------------------------*/
36 /* Forward Declarations */
37 /*---------------------------------------------------------------------*/
38
39
40 /*---------------------------------------------------------------------*/
41 /* Internal Functions */
42 /*---------------------------------------------------------------------*/
43
44
45
46 /*---------------------------------------------------------------------*/
47 /* Exported Functions */
48 /*---------------------------------------------------------------------*/
49
50 /*-----------------------------------------------------------------------
51 //
52 // Function: ParseInt()
53 //
54 // Parses a (possibly negative) Integer, defined as an optional "-",
55 // followed by a sequence of digits. Returns the value or gives an
56 // error on overflow.
57 //
58 // Global Variables: -
59 //
60 // Side Effects : Input is read (and checked)
61 //
62 /----------------------------------------------------------------------*/
63
ParseInt(Scanner_p in)64 long ParseInt(Scanner_p in)
65 {
66 long value;
67
68 if(TestInpTok(in, Hyphen))
69 {
70 NextToken(in);
71 CheckInpTokNoSkip(in, PosInt);
72 if((AktToken(in)->numval-1) > LONG_MAX)
73 {
74 AktTokenError(in, "Long integer underflow", false);
75 }
76 value = -AktToken(in)->numval;
77 NextToken(in);
78 }
79 else
80 {
81 CheckInpTok(in, PosInt);
82 if(AktToken(in)->numval > LONG_MAX)
83 {
84 AktTokenError(in, "Long integer overflow", false);
85 }
86 value = AktToken(in)->numval;
87 NextToken(in);
88 }
89 return value;
90 }
91
92
93 /*-----------------------------------------------------------------------
94 //
95 // Function: ParseFloat()
96 //
97 // Parse a float in x.yEz format (optional negative and so on...)
98 //
99 // Global Variables: -
100 //
101 // Side Effects : Input, may cause error
102 //
103 /----------------------------------------------------------------------*/
104
105 #ifndef ALLOW_COMMA_AS_DECIMAL_DOT
106 #define DECIMAL_DOT Fullstop
107 #else
108 #define DECIMAL_DOT Fullstop|Comma
109 #endif
110
ParseFloat(Scanner_p in)111 double ParseFloat(Scanner_p in)
112 {
113 double value;
114
115 DStrReset(in->accu);
116
117 if(TestInpTok(in, Hyphen|Plus))
118 {
119 DStrAppendDStr(in->accu, AktToken(in)->literal);
120 NextToken(in);
121 CheckInpTokNoSkip(in, PosInt);
122 }
123 else
124 {
125 CheckInpTok(in, PosInt);
126 }
127 DStrAppendDStr(in->accu, AktToken(in)->literal);
128 NextToken(in);
129
130 /* Parsed [-]123 so far */
131
132 if(TestInpNoSkip(in)&&TestInpTok(in, DECIMAL_DOT))
133 {
134 DStrAppendChar(in->accu, '.');
135 AcceptInpTokNoSkip(in, DECIMAL_DOT);
136 DStrAppendDStr(in->accu, AktToken(in)->literal);
137 AcceptInpTokNoSkip(in, PosInt);
138 }
139
140 /* Parsed -123.1123 so far */
141
142 if(TestInpNoSkip(in)&&TestInpId(in, "e|E"))
143 {
144 DStrAppendDStr(in->accu, AktToken(in)->literal);
145 NextToken(in); /* Skip E */
146 DStrAppendDStr(in->accu, AktToken(in)->literal);
147 AcceptInpTokNoSkip(in, Hyphen|Plus); /* Eat - */
148 DStrAppendDStr(in->accu, AktToken(in)->literal);
149 AcceptInpTokNoSkip(in, PosInt);
150 }
151 errno = 0;
152 value = strtod(DStrView(in->accu), NULL);
153
154 if(errno)
155 {
156 TmpErrno = errno;
157 AktTokenError(in, "Cannot translate double", true);
158 }
159 return value;
160 }
161
162
163 /*-----------------------------------------------------------------------
164 //
165 // Function: ParseNumString()
166 //
167 // Parse a (possibly signed) number (Integer, Rational, or Float)
168 // and return the most specific type compatible with it. The number
169 // is not evaluated, but its ASCII representation is stored in
170 // in->accu.
171 //
172 // Global Variables: -
173 //
174 // Side Effects : Reads input, DStr handling may cause memory
175 // operations.
176 //
177 /----------------------------------------------------------------------*/
178
ParseNumString(Scanner_p in)179 StrNumType ParseNumString(Scanner_p in)
180 {
181 StrNumType res = SNInteger;
182 DStr_p accumulator = in->accu;
183
184 DStrReset(accumulator);
185
186 if(TestInpTok(in, Hyphen|Plus))
187 {
188 DStrAppendDStr(accumulator, AktToken(in)->literal);
189 NextToken(in);
190 CheckInpTokNoSkip(in, PosInt);
191 }
192 else
193 {
194 CheckInpTok(in, PosInt);
195 }
196 DStrAppendDStr(accumulator, AktToken(in)->literal);
197 NextToken(in);
198
199 if(TestInpTokNoSkip(in, Slash))
200 {
201 DStrAppendChar(accumulator, '/');
202 NextToken(in);
203
204 if(TestInpTok(in, Hyphen|Plus))
205 {
206 DStrAppendDStr(accumulator, AktToken(in)->literal);
207 NextToken(in);
208 }
209 DStrAppendDStr(accumulator, AktToken(in)->literal);
210 AcceptInpTokNoSkip(in, PosInt);
211
212 res = SNRational;
213 }
214 else
215 {
216 if(TestInpTokNoSkip(in, DECIMAL_DOT) &&
217 TestTok(LookToken(in,1), PosInt) &&
218 !(LookToken(in,1)->skipped))
219 {
220 DStrAppendChar(accumulator, '.');
221 AcceptInpTokNoSkip(in, DECIMAL_DOT);
222 DStrAppendDStr(accumulator, AktToken(in)->literal);
223 AcceptInpTokNoSkip(in, PosInt);
224 res = SNFloat;
225 }
226 if(TestInpNoSkip(in))
227 {
228 if(TestInpId(in, "e|E"))
229 {
230 DStrAppendStr(accumulator, "e");
231 NextToken(in); /* Skip E */
232 DStrAppendDStr(accumulator, AktToken(in)->literal);
233 AcceptInpTokNoSkip(in, Hyphen|Plus); /* Eat - */
234 DStrAppendDStr(accumulator, AktToken(in)->literal);
235 AcceptInpTokNoSkip(in, PosInt);
236 res = SNFloat;
237 }
238 else if(TestInpIdnum(in, "e|E"))
239 {
240 DStrAppendDStr(accumulator, AktToken(in)->literal);
241 AcceptInpTokNoSkip(in, Idnum);
242 res = SNFloat;
243 }
244 }
245 }
246 return res;
247 }
248
249
250 /*-----------------------------------------------------------------------
251 //
252 // Function: DDArrayParse()
253 //
254 // Parse a coma-delimited list of double values into array. If
255 // brackets is true, expect the list to be enclosed into (). Return
256 // the number of values parsed.
257 //
258 // Global Variables: -
259 //
260 // Side Effects : Reads input
261 //
262 /----------------------------------------------------------------------*/
263
DDArrayParse(Scanner_p in,DDArray_p array,bool brackets)264 long DDArrayParse(Scanner_p in, DDArray_p array, bool brackets)
265 {
266 long i=0;
267
268 if(brackets)
269 {
270 AcceptInpTok(in, OpenBracket);
271 }
272
273 if(TestInpTok(in, Hyphen|Plus|PosInt))
274 {
275 DDArrayAssign(array, i, ParseFloat(in));
276 i++;
277
278 while(TestInpTok(in, Comma))
279 {
280 NextToken(in); /* We know it's a comma */
281 DDArrayAssign(array, i, ParseFloat(in));
282 i++;
283 }
284 }
285 if(brackets)
286 {
287 AcceptInpTok(in, CloseBracket);
288 }
289 return i;
290 }
291
292
293 /*-----------------------------------------------------------------------
294 //
295 // Function: ParseFilename()
296 //
297 // Parse a filename and return
298 // it. Note that we only allow reasonably "normal" filenames or
299 // strings, i.e. not spaces, non-printables, most meta-charachters,
300 // or quotes.
301 //
302 // Global Variables: -
303 //
304 // Side Effects : Read input, allocates space (which must be freed
305 // by the caller)
306 //
307 /----------------------------------------------------------------------*/
308
309 #define PLAIN_FILE_TOKENS String|Name|PosInt|Fullstop|Plus|Hyphen
310
ParseFilename(Scanner_p in)311 char* ParseFilename(Scanner_p in)
312 {
313 bool first_tok = true;
314
315 DStrReset(in->accu);
316
317 while((first_tok || TestInpNoSkip(in)) &&
318 TestInpTok(in, PLAIN_FILE_TOKENS|Slash))
319 {
320 DStrAppendDStr(in->accu, AktToken(in)->literal);
321 NextToken(in);
322 first_tok = false;
323 }
324 return SecureStrdup(DStrView(in->accu));
325 }
326
327
328 /*-----------------------------------------------------------------------
329 //
330 // Function: ParsePlainFileName()
331 //
332 // Parse a local file name (without /) and return it. The caller has
333 // to free the allocated memory!
334 //
335 // Global Variables: -
336 //
337 // Side Effects :
338 //
339 /----------------------------------------------------------------------*/
340
ParsePlainFilename(Scanner_p in)341 char* ParsePlainFilename(Scanner_p in)
342 {
343 bool first_tok = true;
344 DStrReset(in->accu);
345
346 while((first_tok || TestInpNoSkip(in)) &&
347 TestInpTok(in, PLAIN_FILE_TOKENS|Slash))
348 {
349 DStrAppendDStr(in->accu, AktToken(in)->literal);
350 NextToken(in);
351 first_tok = false;
352 }
353 return SecureStrdup(DStrView(in->accu));
354 }
355
356 /*-----------------------------------------------------------------------
357 //
358 // Function: ParseBasicInclude()
359 //
360 // Parse a basic TPTP-3 include (without optional selector),
361 // return the file name (which the caller has to free).
362 //
363 // Global Variables: -
364 //
365 // Side Effects : Input, memory allocation.
366 //
367 /----------------------------------------------------------------------*/
368
ParseBasicInclude(Scanner_p in)369 char* ParseBasicInclude(Scanner_p in)
370 {
371 char* res;
372
373 AcceptInpId(in, "include");
374 AcceptInpTok(in, OpenBracket);
375 CheckInpTok(in, SQString);
376 res = DStrCopyCore(AktToken(in)->literal);
377 NextToken(in);
378 AcceptInpTok(in, CloseBracket);
379 AcceptInpTok(in, Fullstop);
380
381 return res;
382 }
383
384
385 /*-----------------------------------------------------------------------
386 //
387 // Function: ParseDottedId()
388 //
389 // Parse a sequence id1.id2.id2 ... and return it as a string.
390 //
391 // Global Variables: -
392 //
393 // Side Effects : Input, memory ops.
394 //
395 /----------------------------------------------------------------------*/
396
ParseDottedId(Scanner_p in)397 char* ParseDottedId(Scanner_p in)
398 {
399 DStrReset(in->accu);
400
401 DStrAppendDStr(in->accu, AktToken(in)->literal);
402 AcceptInpTok(in, Identifier|PosInt);
403
404 while(TestInpNoSkip(in) && TestInpTok(in, Fullstop))
405 {
406 DStrAppendDStr(in->accu, AktToken(in)->literal);
407 AcceptInpTok(in, Fullstop);
408 DStrAppendDStr(in->accu, AktToken(in)->literal);
409 AcceptInpTok(in, Identifier|PosInt);
410 }
411 return SecureStrdup(DStrView(in->accu));
412 }
413
414
415 /*-----------------------------------------------------------------------
416 //
417 // Function: AcceptDottedId()
418 //
419 // Parse a sequence id1.id2.id2..., check it against an expected
420 // value, and skip it. Print error and terminate on mismatch.
421 //
422 // Global Variables: -
423 //
424 // Side Effects : Input, memory ops.
425 //
426 /----------------------------------------------------------------------*/
427
AcceptDottedId(Scanner_p in,char * expected)428 void AcceptDottedId(Scanner_p in, char* expected)
429 {
430 char* candidate;
431 char* posrep = TokenPosRep(AktToken(in));
432
433 candidate = ParseDottedId(in);
434 if(strcmp(candidate, expected)!=0)
435 {
436 Error("%s %s expected, but %s read", SYNTAX_ERROR,
437 posrep, expected, candidate);
438 }
439 FREE(candidate);
440 }
441
442
443 /*-----------------------------------------------------------------------
444 //
445 // Function: ParseContinous()
446 //
447 // Parse a sequence of tokens with no whitespace and return the
448 // result as a string.
449 //
450 // Global Variables: -
451 //
452 // Side Effects : Input, memory ops.
453 //
454 /----------------------------------------------------------------------*/
455
ParseContinous(Scanner_p in)456 char* ParseContinous(Scanner_p in)
457 {
458 DStrReset(in->accu);
459
460 DStrAppendDStr(in->accu, AktToken(in)->literal);
461 NextToken(in);
462
463 while(TestInpNoSkip(in))
464 {
465 DStrAppendDStr(in->accu, AktToken(in)->literal);
466 NextToken(in);
467 }
468 return SecureStrdup(DStrView(in->accu));
469 }
470
471
472
473
474
475 /*-----------------------------------------------------------------------
476 //
477 // Function: ParseSkipParenthesizedExpr()
478 //
479 // Skip any expression containing balanced (), [], {}. Print error
480 // on missmatch. Note that no full syntax check is performed, we are
481 // only interested in the different braces.
482 //
483 // Global Variables: -
484 //
485 // Side Effects : Input
486 //
487 /----------------------------------------------------------------------*/
488
ParseSkipParenthesizedExpr(Scanner_p in)489 void ParseSkipParenthesizedExpr(Scanner_p in)
490 {
491 PStack_p paren_stack = PStackAlloc();
492 TokenType tok;
493
494 CheckInpTok(in, OpenBracket|OpenCurly|OpenSquare);
495 PStackPushInt(paren_stack, AktTokenType(in));
496 NextToken(in);
497 while(!PStackEmpty(paren_stack))
498 {
499 if(TestInpTok(in, OpenBracket|OpenCurly|OpenSquare))
500 {
501 PStackPushInt(paren_stack, AktTokenType(in));
502 NextToken(in);
503 }
504 else if(TestInpTok(in, CloseBracket|CloseCurly|CloseSquare))
505 {
506 tok = PStackPopInt(paren_stack);
507 switch(tok)
508 {
509 case OpenBracket:
510 AcceptInpTok(in,CloseBracket);
511 break;
512 case OpenCurly:
513 AcceptInpTok(in, CloseCurly);
514 break;
515 case OpenSquare:
516 AcceptInpTok(in,CloseSquare);
517 break;
518 default:
519 assert(false && "Impossible value on parentheses stack");
520 break;
521 }
522 }
523 else
524 {
525 NextToken(in);
526 }
527 }
528 PStackFree(paren_stack);
529 }
530
531
532 /*---------------------------------------------------------------------*/
533 /* End of File */
534 /*---------------------------------------------------------------------*/
535
536
537