basis_reduction_cdd: check for possibly incorrect output from cddlib 0.94d
[barvinok.git] / omega / parser.l
blob47deab3927981fd431c66a208f89301b7367e526
1 %{
2 #include <stdio.h>
3 #include <string.h>
4 #include <ginac/ginac.h>
5 #include <omega/AST.h>
6 #include <basic/Dynamic_Array.h>
7 #include <code_gen/mmap-codegen.h>
8 #include "polyfunc.h"
9 #include "y.tab.hh"
10 #include <omega/calc_debug.h>
11 #ifdef WIN32
12 #include <io.h>
13 #define isatty _isatty
14 #include <malloc.h>
15 #define alloca _alloca
16 #endif
18 extern "C" int yywrap() {return 1;};
21 #if defined BRAIN_DAMAGED_FREE
22 void free(void *p);
23 void *realloc(void *p, size_t s);
24 #else
25 #define free(x)         free((char *)(x))
26 #endif
28 char scanBuf[1024];
29 void initializeScanBuffer() {
30         scanBuf[0] = '\0';
31         };
32 void flushScanBuffer() {
33         fprintf(yyout,"# %s\n",scanBuf);
34         if (omega_calc_debug) fprintf(DebugFile,"# %s\n",scanBuf);
35         initializeScanBuffer();
36         }
37 #define BUFFER strcat(scanBuf,yytext)
38 void yyerror(const char *s) {
39     fprintf(stderr,"%s\n",s);
40     fprintf(stderr,"line %d, at end of \"%s\"\n",yylineno,scanBuf);
41     }
43 #define MAX_INCLUDE_DEPTH 10
44 YY_BUFFER_STATE include_stack[MAX_INCLUDE_DEPTH];
45 int include_stack_ptr = 0;
47 void includeFile(char *s) {
48                  if ( include_stack_ptr >= MAX_INCLUDE_DEPTH )
49                      {
50                      fprintf( stderr, "Includes nested too deeply" );
51                      exit( 1 );
52                      }
54                  include_stack[include_stack_ptr++] =
55                      YY_CURRENT_BUFFER;
57                  FILE *f = fopen( yytext, "r" );
59                  if ( ! f ) {
60                         include_stack_ptr--;    
61                      fprintf( stderr, "Can't open %s\n",s);
62                         }
63                 else {
64                         yyin = f;
65                          yy_switch_to_buffer(
66                              yy_create_buffer( yyin, YY_BUF_SIZE ) );
67                         }
69                 }
73 %option yylineno
74 %s LATEX INCLUDE
76 %% 
79 "<<"            {BUFFER; BEGIN(INCLUDE); }
80 <INCLUDE>[^>\n ]+">>"   { BUFFER; 
81                           char *s = yytext;
82                           while (*s != '>') s++;
83                           *s = '\0';
84                           includeFile(s);
85                           BEGIN(INITIAL);
87                         }
88 <INCLUDE>[ \n]  {       fprintf(stderr,"Error in include syntax\n");
89                         fprintf(stderr,"Use <<fname>> to include the file named fname\n");
90                         Exit(1);
92                 }
93                         
95 <LATEX>"\\ "            { BUFFER; }
96 [ \t]+        { BUFFER; }
97 (#[^\n]*\n)     {strncat(scanBuf,yytext,yyleng-1);yylineno++;flushScanBuffer();}
99 <LATEX>"\$\$"           { BUFFER; BEGIN 0; }
100 "\$\$"                  { BUFFER; BEGIN LATEX; }
101 <LATEX>"\\t"            { BUFFER; }
102 <LATEX>"\\!"            { BUFFER; }
103 <LATEX>"\\\\"           { BUFFER; }
105 "\n"            { yylineno++; flushScanBuffer(); }
106 "{"             { BUFFER;  return OPEN_BRACE; }
107 <LATEX>"\\{"            { BUFFER;  return OPEN_BRACE; }
108 "}"             { BUFFER;  return CLOSE_BRACE; }
109 <LATEX>"\\}"            { BUFFER;  return CLOSE_BRACE; }
110 "approximate"           { BUFFER;  return APPROX; }
111 "union"         { BUFFER;  return UNION; }
112 <LATEX>"\\cup"          { BUFFER;  return UNION; }
113 "intersection"  { BUFFER;  return INTERSECTION; }
114 <LATEX>"\\cap"          { BUFFER;  return INTERSECTION; }
115 "symbolic"      { BUFFER;  return SYMBOLIC; }
116 "sym"           { BUFFER;  return SYMBOLIC; }
117 <LATEX>"\\mid"          { BUFFER;  return VERTICAL_BAR; }
118 <LATEX>"|"              { BUFFER;  return VERTICAL_BAR; }
119 <LATEX>"\\st"           { BUFFER;  return SUCH_THAT; }
120 "s.t."          { BUFFER;  return SUCH_THAT; }
121 "inverse"       { BUFFER;  return INVERSE; }
122 "complement"    { BUFFER;  return COMPLEMENT; }
123 <LATEX>"\\circ" { BUFFER;  return COMPOSE; }
124 "compose"       { BUFFER;  return COMPOSE; }
125 "difference"    { BUFFER;  return DIFFERENCE; }
126 "diffToRel"     { BUFFER;  return DIFFERENCE_TO_RELATION; }
127 "project away symbols"  { BUFFER;  return PROJECT_AWAY_SYMBOLS; }
128 "project_away_symbols"  { BUFFER;  return PROJECT_AWAY_SYMBOLS; }
129 "projectAwaySymbols"    { BUFFER;  return PROJECT_AWAY_SYMBOLS; }
130 "project on symbols"    { BUFFER;  return PROJECT_ON_SYMBOLS; }
131 "project_on_symbols"    { BUFFER;  return PROJECT_ON_SYMBOLS; }
132 "projectOnSymbols"      { BUFFER;  return PROJECT_ON_SYMBOLS; }
133 <LATEX>"\\join" { BUFFER;  return JOIN; }
134 "\."            { BUFFER;  return JOIN; }
135 "join"          { BUFFER;  return JOIN; }
136 "domain"        { BUFFER;  return OMEGA_DOMAIN; }
137 "time"          { BUFFER; return TIME; }
138 "timeclosure"   { BUFFER; return TIMECLOSURE; }
139 "range"         { BUFFER;  return RANGE; }
140 <LATEX>"\\forall"       { BUFFER;  return FORALL; }
141 "forall"        { BUFFER;  return FORALL; }
142 <LATEX>"\\exists"       { BUFFER;  return EXISTS; }
143 "exists"        { BUFFER;  return EXISTS; }
144 "PairwiseCheck"         { BUFFER;  return PAIRWISE_CHECK; }
145 "Venn"          { BUFFER;  return VENN; }
146 "ConvexCheck"           { BUFFER;  return CONVEX_CHECK; }
147 "ConvexCombination"             { BUFFER;  return CONVEX_COMBINATION; }
148 "PositiveCombination"           { BUFFER;  return POSITIVE_COMBINATION; }
149 "ConvexHull"            { BUFFER;  return CONVEX_HULL; }
150 "AffineHull"            { BUFFER;  return AFFINE_HULL; }
151 "ConicHull"             { BUFFER;  return CONIC_HULL; }
152 "LinearHull"            { BUFFER;  return LINEAR_HULL; }
153 "hull"          { BUFFER;  return HULL; }
154 "bmax"          { BUFFER;  return BMAX; }
155 "minimize"              { BUFFER;  return MINIMIZE; }
156 "maximize"              { BUFFER;  return MAXIMIZE; }
157 "minimize-range"                { BUFFER;  return MINIMIZE_RANGE; }
158 "maximize-range"                { BUFFER;  return MAXIMIZE_RANGE; }
159 "minimizerange"         { BUFFER;  return MINIMIZE_RANGE; }
160 "maximizerange"         { BUFFER;  return MAXIMIZE_RANGE; }
161 "minimize-domain"               { BUFFER;  return MINIMIZE_DOMAIN; }
162 "maximize-domain"               { BUFFER;  return MAXIMIZE_DOMAIN; }
163 "minimizedomain"                { BUFFER;  return MINIMIZE_DOMAIN; }
164 "maximizedomain"                { BUFFER;  return MAXIMIZE_DOMAIN; }
165 "gist"          { BUFFER;  return GIST; }
166 "given"         { BUFFER;  return GIVEN; }
167 "within"        { BUFFER;  return WITHIN; }
168 "subset"        { BUFFER;  return SUBSET; }
169 "codegen"       { BUFFER;  return CODEGEN; }
170 "tcodegen"      { BUFFER;  return TCODEGEN; }
171 "trans_is"      { BUFFER;  return TRANS_IS; }
172 "trans-is"      { BUFFER;  return TRANS_IS; }
173 "set_mmap"      { BUFFER;  return SET_MMAP; }
174 "set-mmap"      { BUFFER;  return SET_MMAP; }
175 "unroll_is"     { BUFFER;  return UNROLL_IS; }
176 "unroll-is"     { BUFFER;  return UNROLL_IS; }
177 "peel_is"       { BUFFER;  return PEEL_IS; }
178 "peel-is"       { BUFFER;  return PEEL_IS; }
179 "spmd"          { BUFFER;  return SPMD; }
180 "farkas"         { BUFFER;  return FARKAS; }
181 "decoupledfarkas"         { BUFFER;  return DECOUPLED_FARKAS; }
182 "decoupled-farkas"         { BUFFER;  return DECOUPLED_FARKAS; }
183 "decoupled_farkas"         { BUFFER;  return DECOUPLED_FARKAS; }
184 "upper_bound"         { BUFFER;  return MAKE_UPPER_BOUND; }
185 "lower_bound"         { BUFFER;  return MAKE_LOWER_BOUND; }
186 "supersetof"    { BUFFER;  return SUPERSETOF;}
187 "subsetof"      { BUFFER;  return SUBSETOF;}
188 "sym_example"   { BUFFER;  return SYM_SAMPLE;}
189 "example"       { BUFFER;  return SAMPLE;}
190 "carried_by"    { BUFFER;  return CARRIED_BY;}
191 "iterations"    { BUFFER;  return ITERATIONS; }
192 "reachable"     { BUFFER;  return REACHABLE_FROM; }
193 "reachable of"     { BUFFER;  return REACHABLE_OF; }
194 "restrict_domain"       { BUFFER;  return RESTRICT_DOMAIN; }
195 "restrictDomain"        { BUFFER;  return RESTRICT_DOMAIN; }
196 <LATEX>"\\"     { yyerror("Can't use \\ for restrict_domain in Tex mode"); }
197 "\\"            { BUFFER;  return RESTRICT_DOMAIN; }
198 "restrict_range"        { BUFFER;  return RESTRICT_RANGE; }
199 "restrictRange"         { BUFFER;  return RESTRICT_RANGE; }
200 "assertUnsatisfiable"   { BUFFER;  return ASSERT_UNSAT; }
201 "assert_unsatisfiable"  { BUFFER;  return ASSERT_UNSAT; }
202 "card"          { BUFFER;  return CARD; }
203 "ranking"       { BUFFER;  return RANKING; }
204 "count_lexsmaller"      { BUFFER;  return COUNT_LEXSMALLER; }
205 "vertices"      { BUFFER;  return VERTICES; }
206 "&"             { BUFFER;  return AND; }
207 "|"             { BUFFER;  return OR; }
208 "&&"            { BUFFER;  return AND; }
209 "||"            { BUFFER;  return OR; }
210 "and"           { BUFFER;  return AND; }
211 "or"            { BUFFER;  return OR; }
212 <LATEX>"\\land" { BUFFER;  return AND; }
213 <LATEX>"\\lor"  { BUFFER;  return OR; }
214 "!"             { BUFFER;  return NOT; }
215 "not"           { BUFFER;  return NOT; }
216 <LATEX>"\\neg"  { BUFFER;  return NOT; }
217 ":="            { BUFFER;  return IS_ASSIGNED; }
218 "->"            { BUFFER;  return GOES_TO; }
219 "in"            { BUFFER;  return IN; }
220 <LATEX>"\\rightarrow"   { BUFFER;  return GOES_TO; }
221 "<="            { BUFFER;  yylval.REL_OPERATOR = leq;
222                   return REL_OP;
223                   }
224 <LATEX>"\\leq"          { BUFFER;  yylval.REL_OPERATOR = leq;
225                   return REL_OP;
226                   }
227 <LATEX>"\\le"           { BUFFER;  yylval.REL_OPERATOR = leq;
228                   return REL_OP;
229                   }
230 ">="            { BUFFER;  yylval.REL_OPERATOR = geq;
231                   return REL_OP;
232                   }
233 <LATEX>"\\geq"          { BUFFER;  yylval.REL_OPERATOR = geq;
234                   return REL_OP;
235                   }
236 <LATEX>"\\ge"           { BUFFER;  yylval.REL_OPERATOR = geq;
237                   return REL_OP;
238                   }
239 "!="            { BUFFER;  yylval.REL_OPERATOR = neq;
240                   return REL_OP;
241                   }
242 <LATEX>"\\neq"          { BUFFER;  yylval.REL_OPERATOR = neq;
243                   return REL_OP;
244                   }
245 "<"             { BUFFER;  yylval.REL_OPERATOR = lt;
246                   return REL_OP;
247                   }
248 ">"             { BUFFER;  yylval.REL_OPERATOR = gt;
249                   return REL_OP;
250                   }
251 "="             { BUFFER;  yylval.REL_OPERATOR = eq;
252                   return REL_OP;
253                   }
254 [A-Za-z][A-Za-z0-9_']*  { BUFFER;  if (yyleng > 19) yyerror("Identifier too long");
255                           yylval.VAR_NAME = (char *) malloc(1+yyleng);
256                           strcpy(yylval.VAR_NAME,yytext);
257                           return VAR;
258                           }
259 [A-Za-z][A-Za-z0-9_]*"(in)" { BUFFER; if (yyleng > 19) yyerror("Identifier too long");
260                           yylval.VAR_NAME = (char *) malloc(1+yyleng);
261                           strcpy(yylval.VAR_NAME,yytext);
262                           yylval.VAR_NAME[yyleng-3] = 'i';  // lowercase
263                           yylval.VAR_NAME[yyleng-2] = 'n';
264                           return VAR;
265                           }
266 [A-Za-z][A-Za-z0-9_]*"(set)" { BUFFER; if (yyleng > 19) yyerror("Identifier too long");
267                           yylval.VAR_NAME = (char *) malloc(1+yyleng);
268                           strcpy(yylval.VAR_NAME,yytext);
269                           yylval.VAR_NAME[yyleng-4] = 'i';  // Change to "in"
270                           yylval.VAR_NAME[yyleng-3] = 'n';  // Be afraid
271                           yylval.VAR_NAME[yyleng-2] = ')';
272                           yylval.VAR_NAME[yyleng-1] = '\0';
273                           return VAR;
274                           }
275 [A-Za-z][A-Za-z0-9_]*"(out)" { BUFFER; if (yyleng > 19) yyerror("Identifier too long");
276                           yylval.VAR_NAME = (char *) malloc(1+yyleng);
277                           strcpy(yylval.VAR_NAME,yytext);
278                           yylval.VAR_NAME[yyleng-4] = 'o';  // lowercase
279                           yylval.VAR_NAME[yyleng-3] = 'u';
280                           yylval.VAR_NAME[yyleng-2] = 't';
281                           return VAR;
282                           }
284 <LATEX>"\\"[A-Za-z][A-Za-z0-9_]*        { BUFFER;  
285                           if (yyleng > 19) yyerror("Identifier too long");
286                           yylval.VAR_NAME = (char *) malloc(1+yyleng);
287                           strcpy(yylval.VAR_NAME,yytext);
288                           return VAR;
289                           }
290 <LATEX>"\\"[A-Za-z][A-Za-z0-9_]*"(in)" { BUFFER; if (yyleng > 19) yyerror("Identifier too long");
291                           yylval.VAR_NAME = (char *) malloc(1+yyleng);
292                           strcpy(yylval.VAR_NAME,yytext);
293                           yylval.VAR_NAME[yyleng-3] = 'i';  // lowercase
294                           yylval.VAR_NAME[yyleng-2] = 'n';
295                           return VAR;
296                           }
297 <LATEX>"\\"[A-Za-z][A-Za-z0-9_]*"(set)" { BUFFER; if (yyleng > 19) yyerror("Identifier too long");
298                           yylval.VAR_NAME = (char *) malloc(1+yyleng);
299                           strcpy(yylval.VAR_NAME,yytext);
300                           yylval.VAR_NAME[yyleng-4] = 'i';  // Change to "in"
301                           yylval.VAR_NAME[yyleng-3] = 'n';  // Be afraid
302                           yylval.VAR_NAME[yyleng-2] = ')';
303                           yylval.VAR_NAME[yyleng-1] = '\0';
304                           return VAR;
305                           }
306 <LATEX>"\\"[A-Za-z][A-Za-z0-9_]*"(out)" { BUFFER; if (yyleng > 19) yyerror("Identifier too long");
307                           yylval.VAR_NAME = (char *) malloc(1+yyleng);
308                           strcpy(yylval.VAR_NAME,yytext);
309                           yylval.VAR_NAME[yyleng-4] = 'o';  // lowercase
310                           yylval.VAR_NAME[yyleng-3] = 'u';
311                           yylval.VAR_NAME[yyleng-2] = 't';
312                           return VAR;
313                           }
314 [0-9]+          { BUFFER;  yylval.INT_VALUE = atoi(yytext);
315                   return INT;
316                         }
317 \"[^"]*\"       { BUFFER;
318                   yytext[strlen(yytext)-1]='\0';
319                   yylval.STRING_VALUE = new String(yytext+1);
320                   return STRING;
321                 }
322 <<EOF>> {
323                  if ( --include_stack_ptr < 0 )
324                      {
325                      yyterminate();
326                      }
327                 else
328                      {
329                      yy_delete_buffer( YY_CURRENT_BUFFER );
330                      yy_switch_to_buffer(
331                           include_stack[include_stack_ptr] );
332                      }
333                  }
335 .               { BUFFER;  return yytext[0]; }