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() {
30 void flushScanBuffer() {
31 fprintf(yyout,"# %s\n",scanBuf);
32 if (omega_calc_debug) fprintf(DebugFile,"# %s\n",scanBuf);
33 initializeScanBuffer();
35 #define BUFFER strcat(scanBuf,yytext)
36 void yyerror(char *s) {
37 fprintf(stderr,"%s\n",s);
38 fprintf(stderr,"line %d, at end of \"%s\"\n",yylineno,scanBuf);
41 #define MAX_INCLUDE_DEPTH 10
42 YY_BUFFER_STATE include_stack[MAX_INCLUDE_DEPTH];
43 int include_stack_ptr = 0;
45 void includeFile(char *s) {
46 if ( include_stack_ptr >= MAX_INCLUDE_DEPTH )
48 fprintf( stderr, "Includes nested too deeply" );
52 include_stack[include_stack_ptr++] =
55 FILE *f = fopen( yytext, "r" );
59 fprintf( stderr, "Can't open %s\n",s);
64 yy_create_buffer( yyin, YY_BUF_SIZE ) );
76 "<<" {BUFFER; BEGIN(INCLUDE); }
77 <INCLUDE>[^>\n ]+">>" { BUFFER;
79 while (*s != '>') s++;
85 <INCLUDE>[ \n] { fprintf(stderr,"Error in include syntax\n");
86 fprintf(stderr,"Use <<fname>> to include the file named fname\n");
92 <LATEX>"\\ " { BUFFER; }
94 (#[^\n]*\n) {strncat(scanBuf,yytext,yyleng-1);yylineno++;flushScanBuffer();}
96 <LATEX>"\$\$" { BUFFER; BEGIN 0; }
97 "\$\$" { BUFFER; BEGIN LATEX; }
98 <LATEX>"\\t" { BUFFER; }
99 <LATEX>"\\!" { BUFFER; }
100 <LATEX>"\\\\" { BUFFER; }
102 "\n" { yylineno++; flushScanBuffer(); }
103 "{" { BUFFER; return OPEN_BRACE; }
104 <LATEX>"\\{" { BUFFER; return OPEN_BRACE; }
105 "}" { BUFFER; return CLOSE_BRACE; }
106 <LATEX>"\\}" { BUFFER; return CLOSE_BRACE; }
107 "approximate" { BUFFER; return APPROX; }
108 "union" { BUFFER; return UNION; }
109 <LATEX>"\\cup" { BUFFER; return UNION; }
110 "intersection" { BUFFER; return INTERSECTION; }
111 <LATEX>"\\cap" { BUFFER; return INTERSECTION; }
112 "symbolic" { BUFFER; return SYMBOLIC; }
113 "sym" { BUFFER; return SYMBOLIC; }
114 <LATEX>"\\mid" { BUFFER; return VERTICAL_BAR; }
115 <LATEX>"|" { BUFFER; return VERTICAL_BAR; }
116 <LATEX>"\\st" { BUFFER; return SUCH_THAT; }
117 "s.t." { BUFFER; return SUCH_THAT; }
118 "inverse" { BUFFER; return INVERSE; }
119 "complement" { BUFFER; return COMPLEMENT; }
120 <LATEX>"\\circ" { BUFFER; return COMPOSE; }
121 "compose" { BUFFER; return COMPOSE; }
122 "difference" { BUFFER; return DIFFERENCE; }
123 "diffToRel" { BUFFER; return DIFFERENCE_TO_RELATION; }
124 "project away symbols" { BUFFER; return PROJECT_AWAY_SYMBOLS; }
125 "project_away_symbols" { BUFFER; return PROJECT_AWAY_SYMBOLS; }
126 "projectAwaySymbols" { BUFFER; return PROJECT_AWAY_SYMBOLS; }
127 "project on symbols" { BUFFER; return PROJECT_ON_SYMBOLS; }
128 "project_on_symbols" { BUFFER; return PROJECT_ON_SYMBOLS; }
129 "projectOnSymbols" { BUFFER; return PROJECT_ON_SYMBOLS; }
130 <LATEX>"\\join" { BUFFER; return JOIN; }
131 "\." { BUFFER; return JOIN; }
132 "join" { BUFFER; return JOIN; }
133 "domain" { BUFFER; return DOMAIN; }
134 "time" { BUFFER; return TIME; }
135 "timeclosure" { BUFFER; return TIMECLOSURE; }
136 "range" { BUFFER; return RANGE; }
137 <LATEX>"\\forall" { BUFFER; return FORALL; }
138 "forall" { BUFFER; return FORALL; }
139 <LATEX>"\\exists" { BUFFER; return EXISTS; }
140 "exists" { BUFFER; return EXISTS; }
141 "PairwiseCheck" { BUFFER; return PAIRWISE_CHECK; }
142 "Venn" { BUFFER; return VENN; }
143 "ConvexCheck" { BUFFER; return CONVEX_CHECK; }
144 "ConvexCombination" { BUFFER; return CONVEX_COMBINATION; }
145 "PositiveCombination" { BUFFER; return POSITIVE_COMBINATION; }
146 "ConvexHull" { BUFFER; return CONVEX_HULL; }
147 "AffineHull" { BUFFER; return AFFINE_HULL; }
148 "ConicHull" { BUFFER; return CONIC_HULL; }
149 "LinearHull" { BUFFER; return LINEAR_HULL; }
150 "hull" { BUFFER; return HULL; }
151 "minimize" { BUFFER; return MINIMIZE; }
152 "maximize" { BUFFER; return MAXIMIZE; }
153 "minimize-range" { BUFFER; return MINIMIZE_RANGE; }
154 "maximize-range" { BUFFER; return MAXIMIZE_RANGE; }
155 "minimizerange" { BUFFER; return MINIMIZE_RANGE; }
156 "maximizerange" { BUFFER; return MAXIMIZE_RANGE; }
157 "minimize-domain" { BUFFER; return MINIMIZE_DOMAIN; }
158 "maximize-domain" { BUFFER; return MAXIMIZE_DOMAIN; }
159 "minimizedomain" { BUFFER; return MINIMIZE_DOMAIN; }
160 "maximizedomain" { BUFFER; return MAXIMIZE_DOMAIN; }
161 "gist" { BUFFER; return GIST; }
162 "given" { BUFFER; return GIVEN; }
163 "within" { BUFFER; return WITHIN; }
164 "subset" { BUFFER; return SUBSET; }
165 "codegen" { BUFFER; return CODEGEN; }
166 "tcodegen" { BUFFER; return TCODEGEN; }
167 "trans_is" { BUFFER; return TRANS_IS; }
168 "trans-is" { BUFFER; return TRANS_IS; }
169 "set_mmap" { BUFFER; return SET_MMAP; }
170 "set-mmap" { BUFFER; return SET_MMAP; }
171 "unroll_is" { BUFFER; return UNROLL_IS; }
172 "unroll-is" { BUFFER; return UNROLL_IS; }
173 "peel_is" { BUFFER; return PEEL_IS; }
174 "peel-is" { BUFFER; return PEEL_IS; }
175 "spmd" { BUFFER; return SPMD; }
176 "farkas" { BUFFER; return FARKAS; }
177 "decoupledfarkas" { BUFFER; return DECOUPLED_FARKAS; }
178 "decoupled-farkas" { BUFFER; return DECOUPLED_FARKAS; }
179 "decoupled_farkas" { BUFFER; return DECOUPLED_FARKAS; }
180 "upper_bound" { BUFFER; return MAKE_UPPER_BOUND; }
181 "lower_bound" { BUFFER; return MAKE_LOWER_BOUND; }
182 "supersetof" { BUFFER; return SUPERSETOF;}
183 "subsetof" { BUFFER; return SUBSETOF;}
184 "sym_example" { BUFFER; return SYM_SAMPLE;}
185 "example" { BUFFER; return SAMPLE;}
186 "carried_by" { BUFFER; return CARRIED_BY;}
187 "iterations" { BUFFER; return ITERATIONS; }
188 "reachable" { BUFFER; return REACHABLE_FROM; }
189 "reachable of" { BUFFER; return REACHABLE_OF; }
190 "restrict_domain" { BUFFER; return RESTRICT_DOMAIN; }
191 "restrictDomain" { BUFFER; return RESTRICT_DOMAIN; }
192 <LATEX>"\\" { yyerror("Can't use \\ for restrict_domain in Tex mode"); }
193 "\\" { BUFFER; return RESTRICT_DOMAIN; }
194 "restrict_range" { BUFFER; return RESTRICT_RANGE; }
195 "restrictRange" { BUFFER; return RESTRICT_RANGE; }
196 "assertUnsatisfiable" { BUFFER; return ASSERT_UNSAT; }
197 "assert_unsatisfiable" { BUFFER; return ASSERT_UNSAT; }
198 "count" { BUFFER; return COUNT; }
199 "yaml" { BUFFER; return YAML; }
200 "/" { BUFFER; return RESTRICT_RANGE; }
201 "&" { BUFFER; return AND; }
202 "|" { BUFFER; return OR; }
203 "&&" { BUFFER; return AND; }
204 "||" { BUFFER; return OR; }
205 "and" { BUFFER; return AND; }
206 "or" { BUFFER; return OR; }
207 <LATEX>"\\land" { BUFFER; return AND; }
208 <LATEX>"\\lor" { BUFFER; return OR; }
209 "!" { BUFFER; return NOT; }
210 "not" { BUFFER; return NOT; }
211 <LATEX>"\\neg" { BUFFER; return NOT; }
212 ":=" { BUFFER; return IS_ASSIGNED; }
213 "->" { BUFFER; return GOES_TO; }
214 "in" { BUFFER; return IN; }
215 <LATEX>"\\rightarrow" { BUFFER; return GOES_TO; }
216 "<=" { BUFFER; yylval.REL_OPERATOR = leq;
219 <LATEX>"\\leq" { BUFFER; yylval.REL_OPERATOR = leq;
222 <LATEX>"\\le" { BUFFER; yylval.REL_OPERATOR = leq;
225 ">=" { BUFFER; yylval.REL_OPERATOR = geq;
228 <LATEX>"\\geq" { BUFFER; yylval.REL_OPERATOR = geq;
231 <LATEX>"\\ge" { BUFFER; yylval.REL_OPERATOR = geq;
234 "!=" { BUFFER; yylval.REL_OPERATOR = neq;
237 <LATEX>"\\neq" { BUFFER; yylval.REL_OPERATOR = neq;
240 "<" { BUFFER; yylval.REL_OPERATOR = lt;
243 ">" { BUFFER; yylval.REL_OPERATOR = gt;
246 "=" { BUFFER; yylval.REL_OPERATOR = eq;
249 [A-Za-z][A-Za-z0-9_']* { BUFFER; if (yyleng > 19) yyerror("Identifier too long");
250 yylval.VAR_NAME = (char *) malloc(1+yyleng);
251 strcpy(yylval.VAR_NAME,yytext);
254 [A-Za-z][A-Za-z0-9_]*"(in)" { BUFFER; if (yyleng > 19) yyerror("Identifier too long");
255 yylval.VAR_NAME = (char *) malloc(1+yyleng);
256 strcpy(yylval.VAR_NAME,yytext);
257 yylval.VAR_NAME[yyleng-3] = 'i'; // lowercase
258 yylval.VAR_NAME[yyleng-2] = 'n';
261 [A-Za-z][A-Za-z0-9_]*"(set)" { BUFFER; if (yyleng > 19) yyerror("Identifier too long");
262 yylval.VAR_NAME = (char *) malloc(1+yyleng);
263 strcpy(yylval.VAR_NAME,yytext);
264 yylval.VAR_NAME[yyleng-4] = 'i'; // Change to "in"
265 yylval.VAR_NAME[yyleng-3] = 'n'; // Be afraid
266 yylval.VAR_NAME[yyleng-2] = ')';
267 yylval.VAR_NAME[yyleng-1] = '\0';
270 [A-Za-z][A-Za-z0-9_]*"(out)" { BUFFER; if (yyleng > 19) yyerror("Identifier too long");
271 yylval.VAR_NAME = (char *) malloc(1+yyleng);
272 strcpy(yylval.VAR_NAME,yytext);
273 yylval.VAR_NAME[yyleng-4] = 'o'; // lowercase
274 yylval.VAR_NAME[yyleng-3] = 'u';
275 yylval.VAR_NAME[yyleng-2] = 't';
279 <LATEX>"\\"[A-Za-z][A-Za-z0-9_]* { BUFFER;
280 if (yyleng > 19) yyerror("Identifier too long");
281 yylval.VAR_NAME = (char *) malloc(1+yyleng);
282 strcpy(yylval.VAR_NAME,yytext);
285 <LATEX>"\\"[A-Za-z][A-Za-z0-9_]*"(in)" { BUFFER; if (yyleng > 19) yyerror("Identifier too long");
286 yylval.VAR_NAME = (char *) malloc(1+yyleng);
287 strcpy(yylval.VAR_NAME,yytext);
288 yylval.VAR_NAME[yyleng-3] = 'i'; // lowercase
289 yylval.VAR_NAME[yyleng-2] = 'n';
292 <LATEX>"\\"[A-Za-z][A-Za-z0-9_]*"(set)" { BUFFER; if (yyleng > 19) yyerror("Identifier too long");
293 yylval.VAR_NAME = (char *) malloc(1+yyleng);
294 strcpy(yylval.VAR_NAME,yytext);
295 yylval.VAR_NAME[yyleng-4] = 'i'; // Change to "in"
296 yylval.VAR_NAME[yyleng-3] = 'n'; // Be afraid
297 yylval.VAR_NAME[yyleng-2] = ')';
298 yylval.VAR_NAME[yyleng-1] = '\0';
301 <LATEX>"\\"[A-Za-z][A-Za-z0-9_]*"(out)" { BUFFER; if (yyleng > 19) yyerror("Identifier too long");
302 yylval.VAR_NAME = (char *) malloc(1+yyleng);
303 strcpy(yylval.VAR_NAME,yytext);
304 yylval.VAR_NAME[yyleng-4] = 'o'; // lowercase
305 yylval.VAR_NAME[yyleng-3] = 'u';
306 yylval.VAR_NAME[yyleng-2] = 't';
309 [0-9]+ { BUFFER; yylval.INT_VALUE = atoi(yytext);
313 yytext[strlen(yytext)-1]='\0';
314 yylval.STRING_VALUE = new String(yytext+1);
318 if ( --include_stack_ptr < 0 )
324 yy_delete_buffer( YY_CURRENT_BUFFER );
326 include_stack[include_stack_ptr] );
330 . { BUFFER; return yytext[0]; }