5 #include <basic/Dynamic_Array.h>
6 #include <code_gen/mmap-codegen.h>
8 #include <omega/calc_debug.h>
11 #define isatty _isatty
13 #define alloca _alloca
16 extern "C" int yywrap() {return 1;};
19 #if defined BRAIN_DAMAGED_FREE
21 void *realloc(void *p, size_t s);
23 #define free(x) free((char *)(x))
27 void initializeScanBuffer() {
31 void flushScanBuffer() {
32 fprintf(yyout,"# %s\n",scanBuf);
33 if (omega_calc_debug) fprintf(DebugFile,"# %s\n",scanBuf);
34 initializeScanBuffer();
36 #define BUFFER strcat(scanBuf,yytext)
37 void yyerror(char *s) {
38 fprintf(stderr,"%s\n",s);
39 fprintf(stderr,"line %d, at end of \"%s\"\n",yylineno,scanBuf);
42 #define MAX_INCLUDE_DEPTH 10
43 YY_BUFFER_STATE include_stack[MAX_INCLUDE_DEPTH];
44 int include_stack_ptr = 0;
46 void includeFile(char *s) {
47 if ( include_stack_ptr >= MAX_INCLUDE_DEPTH )
49 fprintf( stderr, "Includes nested too deeply" );
53 include_stack[include_stack_ptr++] =
56 FILE *f = fopen( yytext, "r" );
60 fprintf( stderr, "Can't open %s\n",s);
65 yy_create_buffer( yyin, YY_BUF_SIZE ) );
77 "<<" {BUFFER; BEGIN(INCLUDE); }
78 <INCLUDE>[^>\n ]+">>" { BUFFER;
80 while (*s != '>') s++;
86 <INCLUDE>[ \n] { fprintf(stderr,"Error in include syntax\n");
87 fprintf(stderr,"Use <<fname>> to include the file named fname\n");
93 <LATEX>"\\ " { BUFFER; }
95 (#[^\n]*\n) {strncat(scanBuf,yytext,yyleng-1);yylineno++;flushScanBuffer();}
97 <LATEX>"\$\$" { BUFFER; BEGIN 0; }
98 "\$\$" { BUFFER; BEGIN LATEX; }
99 <LATEX>"\\t" { BUFFER; }
100 <LATEX>"\\!" { BUFFER; }
101 <LATEX>"\\\\" { BUFFER; }
103 "\n" { yylineno++; flushScanBuffer(); }
104 "{" { BUFFER; return OPEN_BRACE; }
105 <LATEX>"\\{" { BUFFER; return OPEN_BRACE; }
106 "}" { BUFFER; return CLOSE_BRACE; }
107 <LATEX>"\\}" { BUFFER; return CLOSE_BRACE; }
108 "approximate" { BUFFER; return APPROX; }
109 "union" { BUFFER; return UNION; }
110 <LATEX>"\\cup" { BUFFER; return UNION; }
111 "intersection" { BUFFER; return INTERSECTION; }
112 <LATEX>"\\cap" { BUFFER; return INTERSECTION; }
113 "symbolic" { BUFFER; return SYMBOLIC; }
114 "sym" { BUFFER; return SYMBOLIC; }
115 <LATEX>"\\mid" { BUFFER; return VERTICAL_BAR; }
116 <LATEX>"|" { BUFFER; return VERTICAL_BAR; }
117 <LATEX>"\\st" { BUFFER; return SUCH_THAT; }
118 "s.t." { BUFFER; return SUCH_THAT; }
119 "inverse" { BUFFER; return INVERSE; }
120 "complement" { BUFFER; return COMPLEMENT; }
121 <LATEX>"\\circ" { BUFFER; return COMPOSE; }
122 "compose" { BUFFER; return COMPOSE; }
123 "difference" { BUFFER; return DIFFERENCE; }
124 "diffToRel" { BUFFER; return DIFFERENCE_TO_RELATION; }
125 "project away symbols" { BUFFER; return PROJECT_AWAY_SYMBOLS; }
126 "project_away_symbols" { BUFFER; return PROJECT_AWAY_SYMBOLS; }
127 "projectAwaySymbols" { BUFFER; return PROJECT_AWAY_SYMBOLS; }
128 "project on symbols" { BUFFER; return PROJECT_ON_SYMBOLS; }
129 "project_on_symbols" { BUFFER; return PROJECT_ON_SYMBOLS; }
130 "projectOnSymbols" { BUFFER; return PROJECT_ON_SYMBOLS; }
131 <LATEX>"\\join" { BUFFER; return JOIN; }
132 "\." { BUFFER; return JOIN; }
133 "join" { BUFFER; return JOIN; }
134 "domain" { BUFFER; return OMEGA_DOMAIN; }
135 "time" { BUFFER; return TIME; }
136 "timeclosure" { BUFFER; return TIMECLOSURE; }
137 "range" { BUFFER; return RANGE; }
138 <LATEX>"\\forall" { BUFFER; return FORALL; }
139 "forall" { BUFFER; return FORALL; }
140 <LATEX>"\\exists" { BUFFER; return EXISTS; }
141 "exists" { BUFFER; return EXISTS; }
142 "PairwiseCheck" { BUFFER; return PAIRWISE_CHECK; }
143 "Venn" { BUFFER; return VENN; }
144 "ConvexCheck" { BUFFER; return CONVEX_CHECK; }
145 "ConvexCombination" { BUFFER; return CONVEX_COMBINATION; }
146 "PositiveCombination" { BUFFER; return POSITIVE_COMBINATION; }
147 "ConvexHull" { BUFFER; return CONVEX_HULL; }
148 "AffineHull" { BUFFER; return AFFINE_HULL; }
149 "ConicHull" { BUFFER; return CONIC_HULL; }
150 "LinearHull" { BUFFER; return LINEAR_HULL; }
151 "hull" { BUFFER; return HULL; }
152 "minimize" { BUFFER; return MINIMIZE; }
153 "maximize" { BUFFER; return MAXIMIZE; }
154 "minimize-range" { BUFFER; return MINIMIZE_RANGE; }
155 "maximize-range" { BUFFER; return MAXIMIZE_RANGE; }
156 "minimizerange" { BUFFER; return MINIMIZE_RANGE; }
157 "maximizerange" { BUFFER; return MAXIMIZE_RANGE; }
158 "minimize-domain" { BUFFER; return MINIMIZE_DOMAIN; }
159 "maximize-domain" { BUFFER; return MAXIMIZE_DOMAIN; }
160 "minimizedomain" { BUFFER; return MINIMIZE_DOMAIN; }
161 "maximizedomain" { BUFFER; return MAXIMIZE_DOMAIN; }
162 "gist" { BUFFER; return GIST; }
163 "given" { BUFFER; return GIVEN; }
164 "within" { BUFFER; return WITHIN; }
165 "subset" { BUFFER; return SUBSET; }
166 "codegen" { BUFFER; return CODEGEN; }
167 "tcodegen" { BUFFER; return TCODEGEN; }
168 "trans_is" { BUFFER; return TRANS_IS; }
169 "trans-is" { BUFFER; return TRANS_IS; }
170 "set_mmap" { BUFFER; return SET_MMAP; }
171 "set-mmap" { BUFFER; return SET_MMAP; }
172 "unroll_is" { BUFFER; return UNROLL_IS; }
173 "unroll-is" { BUFFER; return UNROLL_IS; }
174 "peel_is" { BUFFER; return PEEL_IS; }
175 "peel-is" { BUFFER; return PEEL_IS; }
176 "spmd" { BUFFER; return SPMD; }
177 "farkas" { BUFFER; return FARKAS; }
178 "decoupledfarkas" { BUFFER; return DECOUPLED_FARKAS; }
179 "decoupled-farkas" { BUFFER; return DECOUPLED_FARKAS; }
180 "decoupled_farkas" { BUFFER; return DECOUPLED_FARKAS; }
181 "upper_bound" { BUFFER; return MAKE_UPPER_BOUND; }
182 "lower_bound" { BUFFER; return MAKE_LOWER_BOUND; }
183 "supersetof" { BUFFER; return SUPERSETOF;}
184 "subsetof" { BUFFER; return SUBSETOF;}
185 "sym_example" { BUFFER; return SYM_SAMPLE;}
186 "example" { BUFFER; return SAMPLE;}
187 "carried_by" { BUFFER; return CARRIED_BY;}
188 "iterations" { BUFFER; return ITERATIONS; }
189 "reachable" { BUFFER; return REACHABLE_FROM; }
190 "reachable of" { BUFFER; return REACHABLE_OF; }
191 "restrict_domain" { BUFFER; return RESTRICT_DOMAIN; }
192 "restrictDomain" { BUFFER; return RESTRICT_DOMAIN; }
193 <LATEX>"\\" { yyerror("Can't use \\ for restrict_domain in Tex mode"); }
194 "\\" { BUFFER; return RESTRICT_DOMAIN; }
195 "restrict_range" { BUFFER; return RESTRICT_RANGE; }
196 "restrictRange" { BUFFER; return RESTRICT_RANGE; }
197 "assertUnsatisfiable" { BUFFER; return ASSERT_UNSAT; }
198 "assert_unsatisfiable" { BUFFER; return ASSERT_UNSAT; }
199 "card" { BUFFER; return CARD; }
200 "ranking" { BUFFER; return RANKING; }
201 "count_lexsmaller" { BUFFER; return COUNT_LEXSMALLER; }
202 "/" { BUFFER; return RESTRICT_RANGE; }
203 "&" { BUFFER; return AND; }
204 "|" { BUFFER; return OR; }
205 "&&" { BUFFER; return AND; }
206 "||" { BUFFER; return OR; }
207 "and" { BUFFER; return AND; }
208 "or" { BUFFER; return OR; }
209 <LATEX>"\\land" { BUFFER; return AND; }
210 <LATEX>"\\lor" { BUFFER; return OR; }
211 "!" { BUFFER; return NOT; }
212 "not" { BUFFER; return NOT; }
213 <LATEX>"\\neg" { BUFFER; return NOT; }
214 ":=" { BUFFER; return IS_ASSIGNED; }
215 "->" { BUFFER; return GOES_TO; }
216 "in" { BUFFER; return IN; }
217 <LATEX>"\\rightarrow" { BUFFER; return GOES_TO; }
218 "<=" { BUFFER; yylval.REL_OPERATOR = leq;
221 <LATEX>"\\leq" { BUFFER; yylval.REL_OPERATOR = leq;
224 <LATEX>"\\le" { BUFFER; yylval.REL_OPERATOR = leq;
227 ">=" { BUFFER; yylval.REL_OPERATOR = geq;
230 <LATEX>"\\geq" { BUFFER; yylval.REL_OPERATOR = geq;
233 <LATEX>"\\ge" { BUFFER; yylval.REL_OPERATOR = geq;
236 "!=" { BUFFER; yylval.REL_OPERATOR = neq;
239 <LATEX>"\\neq" { BUFFER; yylval.REL_OPERATOR = neq;
242 "<" { BUFFER; yylval.REL_OPERATOR = lt;
245 ">" { BUFFER; yylval.REL_OPERATOR = gt;
248 "=" { BUFFER; yylval.REL_OPERATOR = eq;
251 [A-Za-z][A-Za-z0-9_']* { BUFFER; if (yyleng > 19) yyerror("Identifier too long");
252 yylval.VAR_NAME = (char *) malloc(1+yyleng);
253 strcpy(yylval.VAR_NAME,yytext);
256 [A-Za-z][A-Za-z0-9_]*"(in)" { BUFFER; if (yyleng > 19) yyerror("Identifier too long");
257 yylval.VAR_NAME = (char *) malloc(1+yyleng);
258 strcpy(yylval.VAR_NAME,yytext);
259 yylval.VAR_NAME[yyleng-3] = 'i'; // lowercase
260 yylval.VAR_NAME[yyleng-2] = 'n';
263 [A-Za-z][A-Za-z0-9_]*"(set)" { BUFFER; if (yyleng > 19) yyerror("Identifier too long");
264 yylval.VAR_NAME = (char *) malloc(1+yyleng);
265 strcpy(yylval.VAR_NAME,yytext);
266 yylval.VAR_NAME[yyleng-4] = 'i'; // Change to "in"
267 yylval.VAR_NAME[yyleng-3] = 'n'; // Be afraid
268 yylval.VAR_NAME[yyleng-2] = ')';
269 yylval.VAR_NAME[yyleng-1] = '\0';
272 [A-Za-z][A-Za-z0-9_]*"(out)" { BUFFER; if (yyleng > 19) yyerror("Identifier too long");
273 yylval.VAR_NAME = (char *) malloc(1+yyleng);
274 strcpy(yylval.VAR_NAME,yytext);
275 yylval.VAR_NAME[yyleng-4] = 'o'; // lowercase
276 yylval.VAR_NAME[yyleng-3] = 'u';
277 yylval.VAR_NAME[yyleng-2] = 't';
281 <LATEX>"\\"[A-Za-z][A-Za-z0-9_]* { BUFFER;
282 if (yyleng > 19) yyerror("Identifier too long");
283 yylval.VAR_NAME = (char *) malloc(1+yyleng);
284 strcpy(yylval.VAR_NAME,yytext);
287 <LATEX>"\\"[A-Za-z][A-Za-z0-9_]*"(in)" { BUFFER; if (yyleng > 19) yyerror("Identifier too long");
288 yylval.VAR_NAME = (char *) malloc(1+yyleng);
289 strcpy(yylval.VAR_NAME,yytext);
290 yylval.VAR_NAME[yyleng-3] = 'i'; // lowercase
291 yylval.VAR_NAME[yyleng-2] = 'n';
294 <LATEX>"\\"[A-Za-z][A-Za-z0-9_]*"(set)" { BUFFER; if (yyleng > 19) yyerror("Identifier too long");
295 yylval.VAR_NAME = (char *) malloc(1+yyleng);
296 strcpy(yylval.VAR_NAME,yytext);
297 yylval.VAR_NAME[yyleng-4] = 'i'; // Change to "in"
298 yylval.VAR_NAME[yyleng-3] = 'n'; // Be afraid
299 yylval.VAR_NAME[yyleng-2] = ')';
300 yylval.VAR_NAME[yyleng-1] = '\0';
303 <LATEX>"\\"[A-Za-z][A-Za-z0-9_]*"(out)" { BUFFER; if (yyleng > 19) yyerror("Identifier too long");
304 yylval.VAR_NAME = (char *) malloc(1+yyleng);
305 strcpy(yylval.VAR_NAME,yytext);
306 yylval.VAR_NAME[yyleng-4] = 'o'; // lowercase
307 yylval.VAR_NAME[yyleng-3] = 'u';
308 yylval.VAR_NAME[yyleng-2] = 't';
311 [0-9]+ { BUFFER; yylval.INT_VALUE = atoi(yytext);
315 yytext[strlen(yytext)-1]='\0';
316 yylval.STRING_VALUE = new String(yytext+1);
320 if ( --include_stack_ptr < 0 )
326 yy_delete_buffer( YY_CURRENT_BUFFER );
328 include_stack[include_stack_ptr] );
332 . { BUFFER; return yytext[0]; }