1 |
|
2 |
|
3 |
|
4 |
|
5 |
|
6 |
|
7 |
|
8 |
|
9 |
|
10 |
|
11 |
|
12 |
|
13 |
|
14 |
|
15 |
|
16 |
|
17 |
|
18 |
|
19 |
|
20 |
|
21 |
|
22 |
|
23 |
|
24 |
|
25 |
|
26 |
|
27 |
|
28 |
|
29 |
|
30 |
|
31 |
|
32 |
|
33 |
|
34 |
|
35 |
|
36 |
|
37 |
|
38 |
|
39 |
|
40 |
|
41 |
|
42 |
|
43 |
|
44 |
|
45 |
|
46 |
|
47 |
|
48 |
|
49 |
|
50 |
|
51 |
|
52 |
|
53 |
|
54 |
|
55 |
|
56 |
|
57 |
|
58 |
|
59 |
|
60 |
|
61 |
|
62 |
|
63 |
|
64 |
|
65 |
|
66 |
|
67 |
|
68 |
|
69 |
|
70 |
|
71 |
|
72 |
|
73 |
|
74 | var parser = (function(){
|
75 | var parser = {trace: function trace() { },
|
76 | yy: {},
|
77 | symbols_: {"error":2,"proof":3,"clause_list":4,"proof_option0":5,"ENDOFFILE":6,"box":7,"EOL":8,"BOX":9,"with":10,"box_option0":11,"DEBOX":12,"box_option1":13,"sentence":14,"box_option2":15,"WITH":16,"ID":17,"e_iff":18,"IFF":19,"e_imp":20,"e_exists":21,"IMPLIES":22,"EXISTS":23,"e_forall":24,"FORALL":25,"e_or":26,"OR":27,"e_and":28,"AND":29,"e_eq":30,"EQUALS":31,"e_not":32,"NOT":33,"atom":34,"term":35,"LPAREN":36,"RPAREN":37,"term_list":38,"COMMA":39,"JUSTIFICATION":40,"$accept":0,"$end":1},
|
78 | terminals_: {2:"error",6:"ENDOFFILE",8:"EOL",9:"BOX",12:"DEBOX",16:"WITH",17:"ID",19:"IFF",22:"IMPLIES",23:"EXISTS",25:"FORALL",27:"OR",29:"AND",31:"EQUALS",33:"NOT",36:"LPAREN",37:"RPAREN",39:"COMMA",40:"JUSTIFICATION"},
|
79 | productions_: [0,[3,3],[4,1],[4,3],[4,0],[7,6],[7,4],[7,2],[10,2],[14,1],[14,1],[18,3],[18,1],[20,3],[20,1],[21,3],[21,1],[24,3],[24,1],[26,3],[26,1],[28,3],[28,1],[30,3],[30,1],[32,2],[32,1],[34,1],[34,3],[38,1],[38,3],[35,4],[35,3],[35,1],[5,0],[5,1],[11,0],[11,1],[13,0],[13,1],[15,0],[15,1]],
|
80 | performAction: function anonymous(yytext, yyleng, yylineno, yy, yystate /* action[1] */, $$ /* vstack */, _$ /* lstack */) {
|
81 |
|
82 |
|
83 | var $0 = $$.length - 1;
|
84 | switch (yystate) {
|
85 | case 1: this.$ = $$[$0-2]; return this.$;
|
86 | break;
|
87 | case 2: this.$ = [$$[$0]];
|
88 | break;
|
89 | case 3: this.$ = $$[$0-2]; this.$.push($$[$0]);
|
90 | break;
|
91 | case 4: this.$ = [];
|
92 | break;
|
93 | case 5: this.$ = ['folbox', $$[$0-2], $$[$0-4], this._$];
|
94 | if ($$[$0-2] && $$[$0-2][0] && $$[$0-2][0][0] == 'rule' && $$[$0-2][0][2].auto)
|
95 | $$[$0-2][0][2] = ['assumption', null];
|
96 |
|
97 | break;
|
98 | case 6: this.$ = ['box', $$[$0-2], this._$];
|
99 | if ($$[$0-2] && $$[$0-2][0] && $$[$0-2][0][0] == 'rule' && $$[$0-2][0][2].auto)
|
100 | $$[$0-2][0][2] = ['assumption', null];
|
101 |
|
102 | break;
|
103 | case 7: this.$ = $$[$0-1][0] != 'error'
|
104 | ? ['rule', $$[$0-1], $$[$0], this._$]
|
105 | : $$[$0-1];
|
106 | if (this.$[0] === 'rule' && !this.$[2]) {
|
107 | this.$[2] = ['premise', null];
|
108 | this.$[2].auto = true;
|
109 | }
|
110 |
|
111 | break;
|
112 | case 8: this.$ = ['with', $$[$0]];
|
113 | break;
|
114 | case 10: this.$ = ['error', yytext];
|
115 | break;
|
116 | case 11: this.$ = ['iff', $$[$0-2], $$[$0]];
|
117 | break;
|
118 | case 12: this.$ = $$[$0];
|
119 | break;
|
120 | case 13: this.$ = ['->', $$[$0-2], $$[$0]];
|
121 | break;
|
122 | case 14: this.$ = $$[$0];
|
123 | break;
|
124 | case 15: this.$ = ['exists', $$[$0-1], $$[$0]];
|
125 | break;
|
126 | case 16: this.$ = $$[$0];
|
127 | break;
|
128 | case 17: this.$ = ['forall', $$[$0-1], $$[$0]];
|
129 | break;
|
130 | case 18: this.$ = $$[$0];
|
131 | break;
|
132 | case 19: this.$ = ['or', $$[$0-2], $$[$0]];
|
133 | break;
|
134 | case 20: this.$ = $$[$0];
|
135 | break;
|
136 | case 21: this.$ = ['and', $$[$0-2], $$[$0]];
|
137 | break;
|
138 | case 22: this.$ = $$[$0];
|
139 | break;
|
140 | case 23: this.$ = ['=', $$[$0-2], $$[$0]];
|
141 | break;
|
142 | case 24: this.$ = $$[$0];
|
143 | break;
|
144 | case 25: this.$ = ['not', $$[$0]];
|
145 | break;
|
146 | case 26: this.$ = $$[$0];
|
147 | break;
|
148 | case 27: this.$ = $$[$0];
|
149 | break;
|
150 | case 28: this.$ = $$[$0-1]; this.$.userParens = true;
|
151 | break;
|
152 | case 29: this.$ = [$$[$0]];
|
153 | break;
|
154 | case 30: this.$ = $$[$0]; this.$.unshift($$[$0-2]);
|
155 | break;
|
156 | case 31: this.$ = ['id', $$[$0-3], $$[$0-1]];
|
157 | break;
|
158 | case 32: this.$ = ['id', $$[$0-2], []];
|
159 | break;
|
160 | case 33: this.$ = ['id', $$[$0]];
|
161 | break;
|
162 | }
|
163 | },
|
164 | table: [{2:[1,7],3:1,4:2,6:[2,4],7:3,8:[2,4],9:[1,4],14:5,17:[1,21],18:6,20:8,21:9,23:[1,10],24:11,25:[1,12],26:13,28:14,30:15,32:16,33:[1,17],34:18,35:19,36:[1,20]},{1:[3]},{5:22,6:[2,34],8:[1,23]},{6:[2,2],8:[2,2],12:[2,2]},{2:[1,7],4:25,7:3,8:[2,4],9:[1,4],10:24,12:[2,4],14:5,16:[1,26],17:[1,21],18:6,20:8,21:9,23:[1,10],24:11,25:[1,12],26:13,28:14,30:15,32:16,33:[1,17],34:18,35:19,36:[1,20]},{6:[2,40],8:[2,40],12:[2,40],15:27,40:[1,28]},{6:[2,9],8:[2,9],12:[2,9],19:[1,29],37:[2,9],40:[2,9]},{6:[2,10],8:[2,10],12:[2,10],37:[2,10],40:[2,10]},{6:[2,12],8:[2,12],12:[2,12],19:[2,12],37:[2,12],40:[2,12]},{6:[2,14],8:[2,14],12:[2,14],19:[2,14],22:[1,30],37:[2,14],40:[2,14]},{17:[1,31]},{6:[2,16],8:[2,16],12:[2,16],19:[2,16],22:[2,16],37:[2,16],40:[2,16]},{17:[1,32]},{6:[2,18],8:[2,18],12:[2,18],19:[2,18],22:[2,18],27:[1,33],37:[2,18],40:[2,18]},{6:[2,20],8:[2,20],12:[2,20],19:[2,20],22:[2,20],27:[2,20],29:[1,34],37:[2,20],40:[2,20]},{6:[2,22],8:[2,22],12:[2,22],19:[2,22],22:[2,22],27:[2,22],29:[2,22],31:[1,35],37:[2,22],40:[2,22]},{6:[2,24],8:[2,24],12:[2,24],19:[2,24],22:[2,24],27:[2,24],29:[2,24],31:[2,24],37:[2,24],40:[2,24]},{17:[1,21],32:36,33:[1,17],34:18,35:19,36:[1,20]},{6:[2,26],8:[2,26],12:[2,26],19:[2,26],22:[2,26],27:[2,26],29:[2,26],31:[2,26],37:[2,26],40:[2,26]},{6:[2,27],8:[2,27],12:[2,27],19:[2,27],22:[2,27],27:[2,27],29:[2,27],31:[2,27],37:[2,27],40:[2,27]},{2:[1,7],14:37,17:[1,21],18:6,20:8,21:9,23:[1,10],24:11,25:[1,12],26:13,28:14,30:15,32:16,33:[1,17],34:18,35:19,36:[1,20]},{6:[2,33],8:[2,33],12:[2,33],19:[2,33],22:[2,33],27:[2,33],29:[2,33],31:[2,33],36:[1,38],37:[2,33],39:[2,33],40:[2,33]},{6:[1,39]},{2:[1,7],6:[2,35],7:40,9:[1,4],14:5,17:[1,21],18:6,20:8,21:9,23:[1,10],24:11,25:[1,12],26:13,28:14,30:15,32:16,33:[1,17],34:18,35:19,36:[1,20]},{8:[1,41]},{8:[1,43],12:[2,38],13:42},{17:[1,44]},{6:[2,7],8:[2,7],12:[2,7]},{6:[2,41],8:[2,41],12:[2,41]},{17:[1,21],20:45,21:9,23:[1,10],24:11,25:[1,12],26:13,28:14,30:15,32:16,33:[1,17],34:18,35:19,36:[1,20]},{17:[1,21],20:46,21:9,23:[1,10],24:11,25:[1,12],26:13,28:14,30:15,32:16,33:[1,17],34:18,35:19,36:[1,20]},{17:[1,21],21:47,23:[1,10],24:11,25:[1,12],26:13,28:14,30:15,32:16,33:[1,17],34:18,35:19,36:[1,20]},{17:[1,21],24:48,25:[1,12],26:13,28:14,30:15,32:16,33:[1,17],34:18,35:19,36:[1,20]},{17:[1,21],28:49,30:15,32:16,33:[1,17],34:18,35:19,36:[1,20]},{17:[1,21],30:50,32:16,33:[1,17],34:18,35:19,36:[1,20]},{17:[1,21],32:51,33:[1,17],34:18,35:19,36:[1,20]},{6:[2,25],8:[2,25],12:[2,25],19:[2,25],22:[2,25],27:[2,25],29:[2,25],31:[2,25],37:[2,25],40:[2,25]},{37:[1,52]},{17:[1,21],35:55,37:[1,54],38:53},{1:[2,1]},{6:[2,3],8:[2,3],12:[2,3]},{2:[1,7],4:56,7:3,8:[2,4],9:[1,4],12:[2,4],14:5,17:[1,21],18:6,20:8,21:9,23:[1,10],24:11,25:[1,12],26:13,28:14,30:15,32:16,33:[1,17],34:18,35:19,36:[1,20]},{12:[1,57]},{2:[1,7],7:40,9:[1,4],12:[2,39],14:5,17:[1,21],18:6,20:8,21:9,23:[1,10],24:11,25:[1,12],26:13,28:14,30:15,32:16,33:[1,17],34:18,35:19,36:[1,20]},{8:[2,8]},{6:[2,11],8:[2,11],12:[2,11],19:[2,11],37:[2,11],40:[2,11]},{6:[2,13],8:[2,13],12:[2,13],19:[2,13],37:[2,13],40:[2,13]},{6:[2,15],8:[2,15],12:[2,15],19:[2,15],22:[2,15],37:[2,15],40:[2,15]},{6:[2,17],8:[2,17],12:[2,17],19:[2,17],22:[2,17],37:[2,17],40:[2,17]},{6:[2,19],8:[2,19],12:[2,19],19:[2,19],22:[2,19],27:[2,19],29:[1,34],37:[2,19],40:[2,19]},{6:[2,21],8:[2,21],12:[2,21],19:[2,21],22:[2,21],27:[2,21],29:[2,21],31:[1,35],37:[2,21],40:[2,21]},{6:[2,23],8:[2,23],12:[2,23],19:[2,23],22:[2,23],27:[2,23],29:[2,23],31:[2,23],37:[2,23],40:[2,23]},{6:[2,28],8:[2,28],12:[2,28],19:[2,28],22:[2,28],27:[2,28],29:[2,28],31:[2,28],37:[2,28],40:[2,28]},{37:[1,58]},{6:[2,32],8:[2,32],12:[2,32],19:[2,32],22:[2,32],27:[2,32],29:[2,32],31:[2,32],37:[2,32],39:[2,32],40:[2,32]},{37:[2,29],39:[1,59]},{8:[1,61],11:60,12:[2,36]},{6:[2,6],8:[2,6],12:[2,6]},{6:[2,31],8:[2,31],12:[2,31],19:[2,31],22:[2,31],27:[2,31],29:[2,31],31:[2,31],37:[2,31],39:[2,31],40:[2,31]},{17:[1,21],35:55,38:62},{12:[1,63]},{2:[1,7],7:40,9:[1,4],12:[2,37],14:5,17:[1,21],18:6,20:8,21:9,23:[1,10],24:11,25:[1,12],26:13,28:14,30:15,32:16,33:[1,17],34:18,35:19,36:[1,20]},{37:[2,30]},{6:[2,5],8:[2,5],12:[2,5]}],
|
165 | defaultActions: {39:[2,1],44:[2,8],62:[2,30]},
|
166 | parseError: function parseError(str, hash) {
|
167 | if (hash.recoverable) {
|
168 | this.trace(str);
|
169 | } else {
|
170 | throw new Error(str);
|
171 | }
|
172 | },
|
173 | parse: function parse(input) {
|
174 | var self = this, stack = [0], tstack = [], vstack = [null], lstack = [], table = this.table, yytext = '', yylineno = 0, yyleng = 0, recovering = 0, TERROR = 2, EOF = 1;
|
175 | var args = lstack.slice.call(arguments, 1);
|
176 | var lexer = Object.create(this.lexer);
|
177 | var sharedState = { yy: {} };
|
178 | for (var k in this.yy) {
|
179 | if (Object.prototype.hasOwnProperty.call(this.yy, k)) {
|
180 | sharedState.yy[k] = this.yy[k];
|
181 | }
|
182 | }
|
183 | lexer.setInput(input, sharedState.yy);
|
184 | sharedState.yy.lexer = lexer;
|
185 | sharedState.yy.parser = this;
|
186 | if (typeof lexer.yylloc == 'undefined') {
|
187 | lexer.yylloc = {};
|
188 | }
|
189 | var yyloc = lexer.yylloc;
|
190 | lstack.push(yyloc);
|
191 | var ranges = lexer.options && lexer.options.ranges;
|
192 | if (typeof sharedState.yy.parseError === 'function') {
|
193 | this.parseError = sharedState.yy.parseError;
|
194 | } else {
|
195 | this.parseError = Object.getPrototypeOf(this).parseError;
|
196 | }
|
197 | function popStack(n) {
|
198 | stack.length = stack.length - 2 * n;
|
199 | vstack.length = vstack.length - n;
|
200 | lstack.length = lstack.length - n;
|
201 | }
|
202 | function lex() {
|
203 | var token;
|
204 | token = tstack.pop() || lexer.lex() || EOF;
|
205 | if (typeof token !== 'number') {
|
206 | if (token instanceof Array) {
|
207 | tstack = token;
|
208 | token = tstack.pop();
|
209 | }
|
210 | token = self.symbols_[token] || token;
|
211 | }
|
212 | return token;
|
213 | }
|
214 | var symbol, preErrorSymbol, state, action, a, r, yyval = {}, p, len, newState, expected;
|
215 | while (true) {
|
216 | state = stack[stack.length - 1];
|
217 | if (this.defaultActions[state]) {
|
218 | action = this.defaultActions[state];
|
219 | } else {
|
220 | if (symbol === null || typeof symbol == 'undefined') {
|
221 | symbol = lex();
|
222 | }
|
223 | action = table[state] && table[state][symbol];
|
224 | }
|
225 | _handle_error:
|
226 | if (typeof action === 'undefined' || !action.length || !action[0]) {
|
227 | var error_rule_depth;
|
228 | var errStr = '';
|
229 | function locateNearestErrorRecoveryRule(state) {
|
230 | var stack_probe = stack.length - 1;
|
231 | var depth = 0;
|
232 | for (;;) {
|
233 | if (TERROR.toString() in table[state]) {
|
234 | return depth;
|
235 | }
|
236 | if (state === 0 || stack_probe < 2) {
|
237 | return false;
|
238 | }
|
239 | stack_probe -= 2;
|
240 | state = stack[stack_probe];
|
241 | ++depth;
|
242 | }
|
243 | }
|
244 | if (!recovering) {
|
245 | error_rule_depth = locateNearestErrorRecoveryRule(state);
|
246 | expected = [];
|
247 | for (p in table[state]) {
|
248 | if (this.terminals_[p] && p > TERROR) {
|
249 | expected.push('\'' + this.terminals_[p] + '\'');
|
250 | }
|
251 | }
|
252 | if (lexer.showPosition) {
|
253 | errStr = 'Parse error on line ' + (yylineno + 1) + ':\n' + lexer.showPosition() + '\nExpecting ' + expected.join(', ') + ', got \'' + (this.terminals_[symbol] || symbol) + '\'';
|
254 | } else {
|
255 | errStr = 'Parse error on line ' + (yylineno + 1) + ': Unexpected ' + (symbol == EOF ? 'end of input' : '\'' + (this.terminals_[symbol] || symbol) + '\'');
|
256 | }
|
257 | this.parseError(errStr, {
|
258 | text: lexer.match,
|
259 | token: this.terminals_[symbol] || symbol,
|
260 | line: lexer.yylineno,
|
261 | loc: yyloc,
|
262 | expected: expected,
|
263 | recoverable: error_rule_depth !== false
|
264 | });
|
265 | } else if (preErrorSymbol !== EOF) {
|
266 | error_rule_depth = locateNearestErrorRecoveryRule(state);
|
267 | }
|
268 | if (recovering == 3) {
|
269 | if (symbol === EOF || preErrorSymbol === EOF) {
|
270 | throw new Error(errStr || 'Parsing halted while starting to recover from another error.');
|
271 | }
|
272 | yyleng = lexer.yyleng;
|
273 | yytext = lexer.yytext;
|
274 | yylineno = lexer.yylineno;
|
275 | yyloc = lexer.yylloc;
|
276 | symbol = lex();
|
277 | }
|
278 | if (error_rule_depth === false) {
|
279 | throw new Error(errStr || 'Parsing halted. No suitable error recovery rule available.');
|
280 | }
|
281 | popStack(error_rule_depth);
|
282 | preErrorSymbol = symbol == TERROR ? null : symbol;
|
283 | symbol = TERROR;
|
284 | state = stack[stack.length - 1];
|
285 | action = table[state] && table[state][TERROR];
|
286 | recovering = 3;
|
287 | }
|
288 | if (action[0] instanceof Array && action.length > 1) {
|
289 | throw new Error('Parse Error: multiple actions possible at state: ' + state + ', token: ' + symbol);
|
290 | }
|
291 | switch (action[0]) {
|
292 | case 1:
|
293 | stack.push(symbol);
|
294 | vstack.push(lexer.yytext);
|
295 | lstack.push(lexer.yylloc);
|
296 | stack.push(action[1]);
|
297 | symbol = null;
|
298 | if (!preErrorSymbol) {
|
299 | yyleng = lexer.yyleng;
|
300 | yytext = lexer.yytext;
|
301 | yylineno = lexer.yylineno;
|
302 | yyloc = lexer.yylloc;
|
303 | if (recovering > 0) {
|
304 | recovering--;
|
305 | }
|
306 | } else {
|
307 | symbol = preErrorSymbol;
|
308 | preErrorSymbol = null;
|
309 | }
|
310 | break;
|
311 | case 2:
|
312 | len = this.productions_[action[1]][1];
|
313 | yyval.$ = vstack[vstack.length - len];
|
314 | yyval._$ = {
|
315 | first_line: lstack[lstack.length - (len || 1)].first_line,
|
316 | last_line: lstack[lstack.length - 1].last_line,
|
317 | first_column: lstack[lstack.length - (len || 1)].first_column,
|
318 | last_column: lstack[lstack.length - 1].last_column
|
319 | };
|
320 | if (ranges) {
|
321 | yyval._$.range = [
|
322 | lstack[lstack.length - (len || 1)].range[0],
|
323 | lstack[lstack.length - 1].range[1]
|
324 | ];
|
325 | }
|
326 | r = this.performAction.apply(yyval, [
|
327 | yytext,
|
328 | yyleng,
|
329 | yylineno,
|
330 | sharedState.yy,
|
331 | action[1],
|
332 | vstack,
|
333 | lstack
|
334 | ].concat(args));
|
335 | if (typeof r !== 'undefined') {
|
336 | return r;
|
337 | }
|
338 | if (len) {
|
339 | stack = stack.slice(0, -1 * len * 2);
|
340 | vstack = vstack.slice(0, -1 * len);
|
341 | lstack = lstack.slice(0, -1 * len);
|
342 | }
|
343 | stack.push(this.productions_[action[1]][0]);
|
344 | vstack.push(yyval.$);
|
345 | lstack.push(yyval._$);
|
346 | newState = table[stack[stack.length - 2]][stack[stack.length - 1]];
|
347 | stack.push(newState);
|
348 | break;
|
349 | case 3:
|
350 | return true;
|
351 | }
|
352 | }
|
353 | return true;
|
354 | }};
|
355 |
|
356 | var lexer = (function(){
|
357 | var lexer = ({
|
358 |
|
359 | EOF:1,
|
360 |
|
361 | parseError:function parseError(str, hash) {
|
362 | if (this.yy.parser) {
|
363 | this.yy.parser.parseError(str, hash);
|
364 | } else {
|
365 | throw new Error(str);
|
366 | }
|
367 | },
|
368 |
|
369 |
|
370 | setInput:function (input, yy) {
|
371 | this.yy = yy || this.yy || {};
|
372 | this._input = input;
|
373 | this._more = this._backtrack = this.done = false;
|
374 | this.yylineno = this.yyleng = 0;
|
375 | this.yytext = this.matched = this.match = '';
|
376 | this.conditionStack = ['INITIAL'];
|
377 | this.yylloc = {
|
378 | first_line: 1,
|
379 | first_column: 0,
|
380 | last_line: 1,
|
381 | last_column: 0
|
382 | };
|
383 | if (this.options.ranges) {
|
384 | this.yylloc.range = [0,0];
|
385 | }
|
386 | this.offset = 0;
|
387 | return this;
|
388 | },
|
389 |
|
390 |
|
391 | input:function () {
|
392 | var ch = this._input[0];
|
393 | this.yytext += ch;
|
394 | this.yyleng++;
|
395 | this.offset++;
|
396 | this.match += ch;
|
397 | this.matched += ch;
|
398 | var lines = ch.match(/(?:\r\n?|\n).*/g);
|
399 | if (lines) {
|
400 | this.yylineno++;
|
401 | this.yylloc.last_line++;
|
402 | } else {
|
403 | this.yylloc.last_column++;
|
404 | }
|
405 | if (this.options.ranges) {
|
406 | this.yylloc.range[1]++;
|
407 | }
|
408 |
|
409 | this._input = this._input.slice(1);
|
410 | return ch;
|
411 | },
|
412 |
|
413 |
|
414 | unput:function (ch) {
|
415 | var len = ch.length;
|
416 | var lines = ch.split(/(?:\r\n?|\n)/g);
|
417 |
|
418 | this._input = ch + this._input;
|
419 | this.yytext = this.yytext.substr(0, this.yytext.length - len);
|
420 |
|
421 | this.offset -= len;
|
422 | var oldLines = this.match.split(/(?:\r\n?|\n)/g);
|
423 | this.match = this.match.substr(0, this.match.length - 1);
|
424 | this.matched = this.matched.substr(0, this.matched.length - 1);
|
425 |
|
426 | if (lines.length - 1) {
|
427 | this.yylineno -= lines.length - 1;
|
428 | }
|
429 | var r = this.yylloc.range;
|
430 |
|
431 | this.yylloc = {
|
432 | first_line: this.yylloc.first_line,
|
433 | last_line: this.yylineno + 1,
|
434 | first_column: this.yylloc.first_column,
|
435 | last_column: lines ?
|
436 | (lines.length === oldLines.length ? this.yylloc.first_column : 0)
|
437 | + oldLines[oldLines.length - lines.length].length - lines[0].length :
|
438 | this.yylloc.first_column - len
|
439 | };
|
440 |
|
441 | if (this.options.ranges) {
|
442 | this.yylloc.range = [r[0], r[0] + this.yyleng - len];
|
443 | }
|
444 | this.yyleng = this.yytext.length;
|
445 | return this;
|
446 | },
|
447 |
|
448 |
|
449 | more:function () {
|
450 | this._more = true;
|
451 | return this;
|
452 | },
|
453 |
|
454 |
|
455 | reject:function () {
|
456 | if (this.options.backtrack_lexer) {
|
457 | this._backtrack = true;
|
458 | } else {
|
459 | return this.parseError('Lexical error on line ' + (this.yylineno + 1) + '. You can only invoke reject() in the lexer when the lexer is of the backtracking persuasion (options.backtrack_lexer = true).\n' + this.showPosition(), {
|
460 | text: "",
|
461 | token: null,
|
462 | line: this.yylineno
|
463 | });
|
464 |
|
465 | }
|
466 | return this;
|
467 | },
|
468 |
|
469 |
|
470 | less:function (n) {
|
471 | this.unput(this.match.slice(n));
|
472 | },
|
473 |
|
474 |
|
475 | pastInput:function () {
|
476 | var past = this.matched.substr(0, this.matched.length - this.match.length);
|
477 | return (past.length > 20 ? '...':'') + past.substr(-20).replace(/\n/g, "");
|
478 | },
|
479 |
|
480 |
|
481 | upcomingInput:function () {
|
482 | var next = this.match;
|
483 | if (next.length < 20) {
|
484 | next += this._input.substr(0, 20-next.length);
|
485 | }
|
486 | return (next.substr(0,20) + (next.length > 20 ? '...' : '')).replace(/\n/g, "");
|
487 | },
|
488 |
|
489 |
|
490 | showPosition:function () {
|
491 | var pre = this.pastInput();
|
492 | var c = new Array(pre.length + 1).join("-");
|
493 | return pre + this.upcomingInput() + "\n" + c + "^";
|
494 | },
|
495 |
|
496 |
|
497 | test_match:function (match, indexed_rule) {
|
498 | var token,
|
499 | lines,
|
500 | backup;
|
501 |
|
502 | if (this.options.backtrack_lexer) {
|
503 |
|
504 | backup = {
|
505 | yylineno: this.yylineno,
|
506 | yylloc: {
|
507 | first_line: this.yylloc.first_line,
|
508 | last_line: this.last_line,
|
509 | first_column: this.yylloc.first_column,
|
510 | last_column: this.yylloc.last_column
|
511 | },
|
512 | yytext: this.yytext,
|
513 | match: this.match,
|
514 | matches: this.matches,
|
515 | matched: this.matched,
|
516 | yyleng: this.yyleng,
|
517 | offset: this.offset,
|
518 | _more: this._more,
|
519 | _input: this._input,
|
520 | yy: this.yy,
|
521 | conditionStack: this.conditionStack.slice(0),
|
522 | done: this.done
|
523 | };
|
524 | if (this.options.ranges) {
|
525 | backup.yylloc.range = this.yylloc.range.slice(0);
|
526 | }
|
527 | }
|
528 |
|
529 | lines = match[0].match(/(?:\r\n?|\n).*/g);
|
530 | if (lines) {
|
531 | this.yylineno += lines.length;
|
532 | }
|
533 | this.yylloc = {
|
534 | first_line: this.yylloc.last_line,
|
535 | last_line: this.yylineno + 1,
|
536 | first_column: this.yylloc.last_column,
|
537 | last_column: lines ?
|
538 | lines[lines.length - 1].length - lines[lines.length - 1].match(/\r?\n?/)[0].length :
|
539 | this.yylloc.last_column + match[0].length
|
540 | };
|
541 | this.yytext += match[0];
|
542 | this.match += match[0];
|
543 | this.matches = match;
|
544 | this.yyleng = this.yytext.length;
|
545 | if (this.options.ranges) {
|
546 | this.yylloc.range = [this.offset, this.offset += this.yyleng];
|
547 | }
|
548 | this._more = false;
|
549 | this._backtrack = false;
|
550 | this._input = this._input.slice(match[0].length);
|
551 | this.matched += match[0];
|
552 | token = this.performAction.call(this, this.yy, this, indexed_rule, this.conditionStack[this.conditionStack.length - 1]);
|
553 | if (this.done && this._input) {
|
554 | this.done = false;
|
555 | }
|
556 | if (token) {
|
557 | return token;
|
558 | } else if (this._backtrack) {
|
559 |
|
560 | for (var k in backup) {
|
561 | this[k] = backup[k];
|
562 | }
|
563 | return false;
|
564 | }
|
565 | return false;
|
566 | },
|
567 |
|
568 |
|
569 | next:function () {
|
570 | if (this.done) {
|
571 | return this.EOF;
|
572 | }
|
573 | if (!this._input) {
|
574 | this.done = true;
|
575 | }
|
576 |
|
577 | var token,
|
578 | match,
|
579 | tempMatch,
|
580 | index;
|
581 | if (!this._more) {
|
582 | this.yytext = '';
|
583 | this.match = '';
|
584 | }
|
585 | var rules = this._currentRules();
|
586 | for (var i = 0; i < rules.length; i++) {
|
587 | tempMatch = this._input.match(this.rules[rules[i]]);
|
588 | if (tempMatch && (!match || tempMatch[0].length > match[0].length)) {
|
589 | match = tempMatch;
|
590 | index = i;
|
591 | if (this.options.backtrack_lexer) {
|
592 | token = this.test_match(tempMatch, rules[i]);
|
593 | if (token !== false) {
|
594 | return token;
|
595 | } else if (this._backtrack) {
|
596 | match = false;
|
597 | continue;
|
598 | } else {
|
599 |
|
600 | return false;
|
601 | }
|
602 | } else if (!this.options.flex) {
|
603 | break;
|
604 | }
|
605 | }
|
606 | }
|
607 | if (match) {
|
608 | token = this.test_match(match, rules[index]);
|
609 | if (token !== false) {
|
610 | return token;
|
611 | }
|
612 |
|
613 | return false;
|
614 | }
|
615 | if (this._input === "") {
|
616 | return this.EOF;
|
617 | } else {
|
618 | return this.parseError('Lexical error on line ' + (this.yylineno + 1) + '. Unrecognized text.\n' + this.showPosition(), {
|
619 | text: "",
|
620 | token: null,
|
621 | line: this.yylineno
|
622 | });
|
623 | }
|
624 | },
|
625 |
|
626 |
|
627 | lex:function lex() {
|
628 | var r = this.next();
|
629 | if (r) {
|
630 | return r;
|
631 | } else {
|
632 | return this.lex();
|
633 | }
|
634 | },
|
635 |
|
636 |
|
637 | begin:function begin(condition) {
|
638 | this.conditionStack.push(condition);
|
639 | },
|
640 |
|
641 |
|
642 | popState:function popState() {
|
643 | var n = this.conditionStack.length - 1;
|
644 | if (n > 0) {
|
645 | return this.conditionStack.pop();
|
646 | } else {
|
647 | return this.conditionStack[0];
|
648 | }
|
649 | },
|
650 |
|
651 |
|
652 | _currentRules:function _currentRules() {
|
653 | if (this.conditionStack.length && this.conditionStack[this.conditionStack.length - 1]) {
|
654 | return this.conditions[this.conditionStack[this.conditionStack.length - 1]].rules;
|
655 | } else {
|
656 | return this.conditions["INITIAL"].rules;
|
657 | }
|
658 | },
|
659 |
|
660 |
|
661 | topState:function topState(n) {
|
662 | n = this.conditionStack.length - 1 - Math.abs(n || 0);
|
663 | if (n >= 0) {
|
664 | return this.conditionStack[n];
|
665 | } else {
|
666 | return "INITIAL";
|
667 | }
|
668 | },
|
669 |
|
670 |
|
671 | pushState:function pushState(condition) {
|
672 | this.begin(condition);
|
673 | },
|
674 |
|
675 |
|
676 | stateStackSize:function stateStackSize() {
|
677 | return this.conditionStack.length;
|
678 | },
|
679 | options: {},
|
680 | performAction: function anonymous(yy,yy_,$avoiding_name_collisions,YY_START) {
|
681 | var YYSTATE=YY_START;
|
682 | switch($avoiding_name_collisions) {
|
683 | case 0:
|
684 | break;
|
685 | case 1:return 29;
|
686 | break;
|
687 | case 2:return 27;
|
688 | break;
|
689 | case 3:return 22;
|
690 | break;
|
691 | case 4:return 19;
|
692 | break;
|
693 | case 5:return 33;
|
694 | break;
|
695 | case 6:return 'UNION';
|
696 | break;
|
697 | case 7:return 'INTERSECTION';
|
698 | break;
|
699 | case 8:return 31;
|
700 | break;
|
701 | case 9:return 'EVERY';
|
702 | break;
|
703 | case 10:return 16;
|
704 | break;
|
705 | case 11:return "OF";
|
706 | break;
|
707 | case 12:
|
708 | break;
|
709 | case 13:
|
710 |
|
711 |
|
712 |
|
713 | yy_.yytext = yy_.yytext.substr(yy_.yytext.substr(1).search(/\S/));
|
714 |
|
715 |
|
716 | yy_.yytext = yy_.yytext.trim();
|
717 | var pos = yy_.yytext.search(/\s+\d+/);
|
718 | var lineranges = null, name = yy_.yytext;
|
719 | if (pos != -1) {
|
720 | name = yy_.yytext.substr(0, pos);
|
721 | lineranges = yy_.yytext.substr(pos+1).split(/\s*,\s*/);
|
722 | }
|
723 | var parts = name.split(' ');
|
724 | var rtype = null, side = null;
|
725 | if (parts[0]) {
|
726 | name = parts[0];
|
727 | rtype = parts[1];
|
728 | if (rtype && (parts = rtype.match(/([a-zA-Z]+)(\d+)/))) {
|
729 | rtype = parts[1];
|
730 | side = parts[2];
|
731 | }
|
732 | }
|
733 | var sub = name.split('/');
|
734 | if (sub.length == 2) {
|
735 | name = sub[0];
|
736 | sub = sub[1];
|
737 | } else {
|
738 | sub = null;
|
739 | }
|
740 | yy_.yytext = [name, rtype, side, lineranges, sub];
|
741 | return 40;
|
742 |
|
743 | break;
|
744 | case 14:return 23;
|
745 | break;
|
746 | case 15:return 'IN';
|
747 | break;
|
748 | case 16:return 'EMPTYSET';
|
749 | break;
|
750 | case 17:return 25;
|
751 | break;
|
752 | case 18:return 36;
|
753 | break;
|
754 | case 19:return 37;
|
755 | break;
|
756 | case 20:return 17;
|
757 | break;
|
758 | case 21:return 39;
|
759 | break;
|
760 | case 22:
|
761 |
|
762 | var tokens = [];
|
763 |
|
764 | while (this._iemitstack[0]) {
|
765 | tokens.unshift("DEBOX");
|
766 | this._iemitstack.shift();
|
767 | }
|
768 | tokens.unshift("ENDOFFILE");
|
769 | if (tokens.length) return tokens;
|
770 |
|
771 | break;
|
772 | case 23:
|
773 | this._log("MANUAL DEBOX");
|
774 | this._iemitstack.shift();
|
775 | return ['DEBOX', 'EOL'];
|
776 |
|
777 | break;
|
778 | case 24:
|
779 | break;
|
780 | case 25:
|
781 | |
782 |
|
783 |
|
784 | var indentation = (yy_.yytext.match(/\|/g)||[]).length;
|
785 | if (indentation > this._iemitstack[0]) {
|
786 | this._iemitstack.unshift(indentation);
|
787 | this._log(this.topState(), "BOX", this.stateStackSize());
|
788 | this.myBegin(this.topState(), 'deepening, due to indent');
|
789 | return ['BOX', 'EOL'];
|
790 | }
|
791 |
|
792 | var tokens = ["EOL"];
|
793 | while (indentation < this._iemitstack[0]) {
|
794 | this.myPopState();
|
795 | this._log(this.topState(), "DEBOX", this.stateStackSize());
|
796 | tokens.push("DEBOX");
|
797 | this._iemitstack.shift();
|
798 | }
|
799 | if (tokens[tokens.length-1] === "DEBOX")
|
800 | tokens.push("EOL");
|
801 | return tokens;
|
802 |
|
803 | break;
|
804 | case 26:return 8;
|
805 | break;
|
806 | case 27:
|
807 | break;
|
808 | case 28:return 2;
|
809 | break;
|
810 | }
|
811 | },
|
812 | rules: [/^(?:[\n\r]?#.*)/,/^(?:and\b)/,/^(?:or\b)/,/^(?:implies|->|=>)/,/^(?:iff|<->|=>)/,/^(?:not|~|!)/,/^(?:union\b)/,/^(?:intersection\b)/,/^(?:=)/,/^(?:every\b)/,/^(?:with\b)/,/^(?:of\b)/,/^(?:\d+)/,/^(?:(:.*))/,/^(?:E\.)/,/^(?:in\b)/,/^(?:empty\b)/,/^(?:A\.)/,/^(?:\()/,/^(?:\))/,/^(?:([a-zA-Z_][a-zA-Z_'"0-9\|]*))/,/^(?:,)/,/^(?:[\n\r]*$)/,/^(?:\n([\t \u00a0\u2000\u2001\u2002\u2003\u2004\u2005\u2006\u2007\u2008\u2009\u200a\u200b\u2028\u2029\u3000])*\|*-+)/,/^(?:[\n\r]+([\t \u00a0\u2000\u2001\u2002\u2003\u2004\u2005\u2006\u2007\u2008\u2009\u200a\u200b\u2028\u2029\u3000])*(?![^\n\r]))/,/^(?:[\n|^]([\t \u00a0\u2000\u2001\u2002\u2003\u2004\u2005\u2006\u2007\u2008\u2009\u200a\u200b\u2028\u2029\u3000])*\d*([\t \u00a0\u2000\u2001\u2002\u2003\u2004\u2005\u2006\u2007\u2008\u2009\u200a\u200b\u2028\u2029\u3000])*\|*)/,/^(?:\n)/,/^(?:([\t \u00a0\u2000\u2001\u2002\u2003\u2004\u2005\u2006\u2007\u2008\u2009\u200a\u200b\u2028\u2029\u3000])+)/,/^(?:.*)/],
|
813 | conditions: {"INITIAL":{"rules":[0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28],"inclusive":true}}
|
814 | });
|
815 | jisonLexerFn = lexer.setInput;
|
816 | lexer.setInput = function(input) {
|
817 | var debug = false;
|
818 | this._iemitstack = [0];
|
819 | this._log = function() { if (debug) console.log.apply(this, arguments); };
|
820 | this.myBegin = function(state, why) { this._log("Begin " + state + " because " + why); this.begin(state); };
|
821 | this.myPopState = function() { this._log("Popping " + this.popState() + " to " + this.topState()); };
|
822 | return jisonLexerFn.call(this, input);
|
823 | };;
|
824 | return lexer;
|
825 | })();
|
826 | parser.lexer = lexer;
|
827 | function Parser () {
|
828 | this.yy = {};
|
829 | }
|
830 | Parser.prototype = parser;parser.Parser = Parser;
|
831 | return new Parser;
|
832 | })();
|
833 |
|
834 |
|
835 | if (typeof require !== 'undefined' && typeof exports !== 'undefined') {
|
836 | exports.parser = parser;
|
837 | exports.Parser = parser.Parser;
|
838 | exports.parse = function () { return parser.parse.apply(parser, arguments); };
|
839 | exports.main = function commonjsMain(args) {
|
840 | if (!args[1]) {
|
841 | console.log('Usage: '+args[0]+' FILE');
|
842 | process.exit(1);
|
843 | }
|
844 | var source = require('fs').readFileSync(require('path').normalize(args[1]), "utf8");
|
845 | return exports.parser.parse(source);
|
846 | };
|
847 | if (typeof module !== 'undefined' && require.main === module) {
|
848 | exports.main(process.argv.slice(1));
|
849 | }
|
850 | } |
\ | No newline at end of file |