diff options
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/parser/antlr/internal/InternalVampireLanguage.g')
-rw-r--r-- | Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/parser/antlr/internal/InternalVampireLanguage.g | 1153 |
1 files changed, 720 insertions, 433 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/parser/antlr/internal/InternalVampireLanguage.g b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/parser/antlr/internal/InternalVampireLanguage.g index 62840209..96bf62b2 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/parser/antlr/internal/InternalVampireLanguage.g +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/parser/antlr/internal/InternalVampireLanguage.g | |||
@@ -79,29 +79,9 @@ ruleVampireModel returns [EObject current=null] | |||
79 | ( | 79 | ( |
80 | ( | 80 | ( |
81 | { | 81 | { |
82 | newCompositeNode(grammarAccess.getVampireModelAccess().getIncludesVLSIncludeParserRuleCall_0_0()); | 82 | newCompositeNode(grammarAccess.getVampireModelAccess().getCommentsVLSCommentParserRuleCall_0_0()); |
83 | } | 83 | } |
84 | lv_includes_0_0=ruleVLSInclude | 84 | lv_comments_0_0=ruleVLSComment |
85 | { | ||
86 | if ($current==null) { | ||
87 | $current = createModelElementForParent(grammarAccess.getVampireModelRule()); | ||
88 | } | ||
89 | add( | ||
90 | $current, | ||
91 | "includes", | ||
92 | lv_includes_0_0, | ||
93 | "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSInclude"); | ||
94 | afterParserOrEnumRuleCall(); | ||
95 | } | ||
96 | ) | ||
97 | ) | ||
98 | | | ||
99 | ( | ||
100 | ( | ||
101 | { | ||
102 | newCompositeNode(grammarAccess.getVampireModelAccess().getCommentsVLSCommentParserRuleCall_1_0()); | ||
103 | } | ||
104 | lv_comments_1_0=ruleVLSComment | ||
105 | { | 85 | { |
106 | if ($current==null) { | 86 | if ($current==null) { |
107 | $current = createModelElementForParent(grammarAccess.getVampireModelRule()); | 87 | $current = createModelElementForParent(grammarAccess.getVampireModelRule()); |
@@ -109,7 +89,7 @@ ruleVampireModel returns [EObject current=null] | |||
109 | add( | 89 | add( |
110 | $current, | 90 | $current, |
111 | "comments", | 91 | "comments", |
112 | lv_comments_1_0, | 92 | lv_comments_0_0, |
113 | "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSComment"); | 93 | "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSComment"); |
114 | afterParserOrEnumRuleCall(); | 94 | afterParserOrEnumRuleCall(); |
115 | } | 95 | } |
@@ -119,9 +99,9 @@ ruleVampireModel returns [EObject current=null] | |||
119 | ( | 99 | ( |
120 | ( | 100 | ( |
121 | { | 101 | { |
122 | newCompositeNode(grammarAccess.getVampireModelAccess().getConfirmationsVLSConfirmationsParserRuleCall_2_0()); | 102 | newCompositeNode(grammarAccess.getVampireModelAccess().getConfirmationsVLSConfirmationsParserRuleCall_1_0()); |
123 | } | 103 | } |
124 | lv_confirmations_2_0=ruleVLSConfirmations | 104 | lv_confirmations_1_0=ruleVLSConfirmations |
125 | { | 105 | { |
126 | if ($current==null) { | 106 | if ($current==null) { |
127 | $current = createModelElementForParent(grammarAccess.getVampireModelRule()); | 107 | $current = createModelElementForParent(grammarAccess.getVampireModelRule()); |
@@ -129,7 +109,7 @@ ruleVampireModel returns [EObject current=null] | |||
129 | add( | 109 | add( |
130 | $current, | 110 | $current, |
131 | "confirmations", | 111 | "confirmations", |
132 | lv_confirmations_2_0, | 112 | lv_confirmations_1_0, |
133 | "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSConfirmations"); | 113 | "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSConfirmations"); |
134 | afterParserOrEnumRuleCall(); | 114 | afterParserOrEnumRuleCall(); |
135 | } | 115 | } |
@@ -139,9 +119,9 @@ ruleVampireModel returns [EObject current=null] | |||
139 | ( | 119 | ( |
140 | ( | 120 | ( |
141 | { | 121 | { |
142 | newCompositeNode(grammarAccess.getVampireModelAccess().getFormulasVLSFofFormulaParserRuleCall_3_0()); | 122 | newCompositeNode(grammarAccess.getVampireModelAccess().getFormulasVLSFofFormulaParserRuleCall_2_0()); |
143 | } | 123 | } |
144 | lv_formulas_3_0=ruleVLSFofFormula | 124 | lv_formulas_2_0=ruleVLSFofFormula |
145 | { | 125 | { |
146 | if ($current==null) { | 126 | if ($current==null) { |
147 | $current = createModelElementForParent(grammarAccess.getVampireModelRule()); | 127 | $current = createModelElementForParent(grammarAccess.getVampireModelRule()); |
@@ -149,7 +129,7 @@ ruleVampireModel returns [EObject current=null] | |||
149 | add( | 129 | add( |
150 | $current, | 130 | $current, |
151 | "formulas", | 131 | "formulas", |
152 | lv_formulas_3_0, | 132 | lv_formulas_2_0, |
153 | "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSFofFormula"); | 133 | "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSFofFormula"); |
154 | afterParserOrEnumRuleCall(); | 134 | afterParserOrEnumRuleCall(); |
155 | } | 135 | } |
@@ -159,9 +139,9 @@ ruleVampireModel returns [EObject current=null] | |||
159 | ( | 139 | ( |
160 | ( | 140 | ( |
161 | { | 141 | { |
162 | newCompositeNode(grammarAccess.getVampireModelAccess().getTfformulasVLSTffFormulaParserRuleCall_4_0()); | 142 | newCompositeNode(grammarAccess.getVampireModelAccess().getTfformulasVLSTffFormulaParserRuleCall_3_0()); |
163 | } | 143 | } |
164 | lv_tfformulas_4_0=ruleVLSTffFormula | 144 | lv_tfformulas_3_0=ruleVLSTffFormula |
165 | { | 145 | { |
166 | if ($current==null) { | 146 | if ($current==null) { |
167 | $current = createModelElementForParent(grammarAccess.getVampireModelRule()); | 147 | $current = createModelElementForParent(grammarAccess.getVampireModelRule()); |
@@ -169,7 +149,7 @@ ruleVampireModel returns [EObject current=null] | |||
169 | add( | 149 | add( |
170 | $current, | 150 | $current, |
171 | "tfformulas", | 151 | "tfformulas", |
172 | lv_tfformulas_4_0, | 152 | lv_tfformulas_3_0, |
173 | "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSTffFormula"); | 153 | "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSTffFormula"); |
174 | afterParserOrEnumRuleCall(); | 154 | afterParserOrEnumRuleCall(); |
175 | } | 155 | } |
@@ -178,15 +158,15 @@ ruleVampireModel returns [EObject current=null] | |||
178 | )* | 158 | )* |
179 | ; | 159 | ; |
180 | 160 | ||
181 | // Entry rule entryRuleVLSInclude | 161 | // Entry rule entryRuleVLSComment |
182 | entryRuleVLSInclude returns [EObject current=null]: | 162 | entryRuleVLSComment returns [EObject current=null]: |
183 | { newCompositeNode(grammarAccess.getVLSIncludeRule()); } | 163 | { newCompositeNode(grammarAccess.getVLSCommentRule()); } |
184 | iv_ruleVLSInclude=ruleVLSInclude | 164 | iv_ruleVLSComment=ruleVLSComment |
185 | { $current=$iv_ruleVLSInclude.current; } | 165 | { $current=$iv_ruleVLSComment.current; } |
186 | EOF; | 166 | EOF; |
187 | 167 | ||
188 | // Rule VLSInclude | 168 | // Rule VLSComment |
189 | ruleVLSInclude returns [EObject current=null] | 169 | ruleVLSComment returns [EObject current=null] |
190 | @init { | 170 | @init { |
191 | enterRule(); | 171 | enterRule(); |
192 | } | 172 | } |
@@ -194,94 +174,34 @@ ruleVLSInclude returns [EObject current=null] | |||
194 | leaveRule(); | 174 | leaveRule(); |
195 | }: | 175 | }: |
196 | ( | 176 | ( |
197 | otherlv_0='include(' | ||
198 | { | ||
199 | newLeafNode(otherlv_0, grammarAccess.getVLSIncludeAccess().getIncludeKeyword_0()); | ||
200 | } | ||
201 | ( | 177 | ( |
202 | ( | 178 | lv_comment_0_0=RULE_SINGLE_COMMENT |
203 | lv_fileName_1_0=RULE_SINGLE_QUOTE | ||
204 | { | ||
205 | newLeafNode(lv_fileName_1_0, grammarAccess.getVLSIncludeAccess().getFileNameSINGLE_QUOTETerminalRuleCall_1_0()); | ||
206 | } | ||
207 | { | ||
208 | if ($current==null) { | ||
209 | $current = createModelElement(grammarAccess.getVLSIncludeRule()); | ||
210 | } | ||
211 | setWithLastConsumed( | ||
212 | $current, | ||
213 | "fileName", | ||
214 | lv_fileName_1_0, | ||
215 | "ca.mcgill.ecse.dslreasoner.VampireLanguage.SINGLE_QUOTE"); | ||
216 | } | ||
217 | ) | ||
218 | ) | ||
219 | ( | ||
220 | otherlv_2=',[' | ||
221 | { | 179 | { |
222 | newLeafNode(otherlv_2, grammarAccess.getVLSIncludeAccess().getCommaLeftSquareBracketKeyword_2_0()); | 180 | newLeafNode(lv_comment_0_0, grammarAccess.getVLSCommentAccess().getCommentSINGLE_COMMENTTerminalRuleCall_0()); |
223 | } | 181 | } |
224 | ( | ||
225 | ( | ||
226 | { | ||
227 | newCompositeNode(grammarAccess.getVLSIncludeAccess().getNamesVLSNameParserRuleCall_2_1_0()); | ||
228 | } | ||
229 | lv_names_3_0=ruleVLSName | ||
230 | { | ||
231 | if ($current==null) { | ||
232 | $current = createModelElementForParent(grammarAccess.getVLSIncludeRule()); | ||
233 | } | ||
234 | add( | ||
235 | $current, | ||
236 | "names", | ||
237 | lv_names_3_0, | ||
238 | "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSName"); | ||
239 | afterParserOrEnumRuleCall(); | ||
240 | } | ||
241 | ) | ||
242 | ) | ||
243 | ( | ||
244 | otherlv_4=',' | ||
245 | { | ||
246 | newLeafNode(otherlv_4, grammarAccess.getVLSIncludeAccess().getCommaKeyword_2_2_0()); | ||
247 | } | ||
248 | ( | ||
249 | ( | ||
250 | { | ||
251 | newCompositeNode(grammarAccess.getVLSIncludeAccess().getNamesVLSNameParserRuleCall_2_2_1_0()); | ||
252 | } | ||
253 | lv_names_5_0=ruleVLSName | ||
254 | { | ||
255 | if ($current==null) { | ||
256 | $current = createModelElementForParent(grammarAccess.getVLSIncludeRule()); | ||
257 | } | ||
258 | add( | ||
259 | $current, | ||
260 | "names", | ||
261 | lv_names_5_0, | ||
262 | "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSName"); | ||
263 | afterParserOrEnumRuleCall(); | ||
264 | } | ||
265 | ) | ||
266 | ) | ||
267 | )* | ||
268 | otherlv_6=']' | ||
269 | { | 182 | { |
270 | newLeafNode(otherlv_6, grammarAccess.getVLSIncludeAccess().getRightSquareBracketKeyword_2_3()); | 183 | if ($current==null) { |
184 | $current = createModelElement(grammarAccess.getVLSCommentRule()); | ||
185 | } | ||
186 | setWithLastConsumed( | ||
187 | $current, | ||
188 | "comment", | ||
189 | lv_comment_0_0, | ||
190 | "ca.mcgill.ecse.dslreasoner.VampireLanguage.SINGLE_COMMENT"); | ||
271 | } | 191 | } |
272 | )? | 192 | ) |
273 | ) | 193 | ) |
274 | ; | 194 | ; |
275 | 195 | ||
276 | // Entry rule entryRuleVLSName | 196 | // Entry rule entryRuleVLSConfirmations |
277 | entryRuleVLSName returns [EObject current=null]: | 197 | entryRuleVLSConfirmations returns [EObject current=null]: |
278 | { newCompositeNode(grammarAccess.getVLSNameRule()); } | 198 | { newCompositeNode(grammarAccess.getVLSConfirmationsRule()); } |
279 | iv_ruleVLSName=ruleVLSName | 199 | iv_ruleVLSConfirmations=ruleVLSConfirmations |
280 | { $current=$iv_ruleVLSName.current; } | 200 | { $current=$iv_ruleVLSConfirmations.current; } |
281 | EOF; | 201 | EOF; |
282 | 202 | ||
283 | // Rule VLSName | 203 | // Rule VLSConfirmations |
284 | ruleVLSName returns [EObject current=null] | 204 | ruleVLSConfirmations returns [EObject current=null] |
285 | @init { | 205 | @init { |
286 | enterRule(); | 206 | enterRule(); |
287 | } | 207 | } |
@@ -291,163 +211,121 @@ ruleVLSName returns [EObject current=null] | |||
291 | ( | 211 | ( |
292 | ( | 212 | ( |
293 | ( | 213 | ( |
294 | lv_name_0_1=RULE_LOWER_WORD_ID | ||
295 | { | ||
296 | newLeafNode(lv_name_0_1, grammarAccess.getVLSNameAccess().getNameLOWER_WORD_IDTerminalRuleCall_0_0()); | ||
297 | } | ||
298 | { | 214 | { |
299 | if ($current==null) { | 215 | $current = forceCreateModelElement( |
300 | $current = createModelElement(grammarAccess.getVLSNameRule()); | 216 | grammarAccess.getVLSConfirmationsAccess().getVLSSatisfiableAction_0_0(), |
301 | } | 217 | $current); |
302 | setWithLastConsumed( | ||
303 | $current, | ||
304 | "name", | ||
305 | lv_name_0_1, | ||
306 | "ca.mcgill.ecse.dslreasoner.VampireLanguage.LOWER_WORD_ID"); | ||
307 | } | ||
308 | | | ||
309 | lv_name_0_2=RULE_SINGLE_QUOTE | ||
310 | { | ||
311 | newLeafNode(lv_name_0_2, grammarAccess.getVLSNameAccess().getNameSINGLE_QUOTETerminalRuleCall_0_1()); | ||
312 | } | 218 | } |
219 | ) | ||
220 | otherlv_1='Satisfiable!' | ||
221 | { | ||
222 | newLeafNode(otherlv_1, grammarAccess.getVLSConfirmationsAccess().getSatisfiableKeyword_0_1()); | ||
223 | } | ||
224 | ) | ||
225 | | | ||
226 | ( | ||
227 | ( | ||
313 | { | 228 | { |
314 | if ($current==null) { | 229 | $current = forceCreateModelElement( |
315 | $current = createModelElement(grammarAccess.getVLSNameRule()); | 230 | grammarAccess.getVLSConfirmationsAccess().getVLSWarningAction_1_0(), |
316 | } | 231 | $current); |
317 | setWithLastConsumed( | ||
318 | $current, | ||
319 | "name", | ||
320 | lv_name_0_2, | ||
321 | "ca.mcgill.ecse.dslreasoner.VampireLanguage.SINGLE_QUOTE"); | ||
322 | } | 232 | } |
323 | | | 233 | ) |
324 | lv_name_0_3=RULE_LITERAL | 234 | otherlv_3='WARNING!' |
235 | { | ||
236 | newLeafNode(otherlv_3, grammarAccess.getVLSConfirmationsAccess().getWARNINGKeyword_1_1()); | ||
237 | } | ||
238 | otherlv_4='Could' | ||
239 | { | ||
240 | newLeafNode(otherlv_4, grammarAccess.getVLSConfirmationsAccess().getCouldKeyword_1_2()); | ||
241 | } | ||
242 | otherlv_5='not' | ||
243 | { | ||
244 | newLeafNode(otherlv_5, grammarAccess.getVLSConfirmationsAccess().getNotKeyword_1_3()); | ||
245 | } | ||
246 | otherlv_6='set' | ||
247 | { | ||
248 | newLeafNode(otherlv_6, grammarAccess.getVLSConfirmationsAccess().getSetKeyword_1_4()); | ||
249 | } | ||
250 | otherlv_7='resource' | ||
251 | { | ||
252 | newLeafNode(otherlv_7, grammarAccess.getVLSConfirmationsAccess().getResourceKeyword_1_5()); | ||
253 | } | ||
254 | otherlv_8='limit:' | ||
255 | { | ||
256 | newLeafNode(otherlv_8, grammarAccess.getVLSConfirmationsAccess().getLimitKeyword_1_6()); | ||
257 | } | ||
258 | otherlv_9='Virtual' | ||
259 | { | ||
260 | newLeafNode(otherlv_9, grammarAccess.getVLSConfirmationsAccess().getVirtualKeyword_1_7()); | ||
261 | } | ||
262 | otherlv_10='memory.' | ||
263 | { | ||
264 | newLeafNode(otherlv_10, grammarAccess.getVLSConfirmationsAccess().getMemoryKeyword_1_8()); | ||
265 | } | ||
266 | ) | ||
267 | | | ||
268 | ( | ||
269 | ( | ||
325 | { | 270 | { |
326 | newLeafNode(lv_name_0_3, grammarAccess.getVLSNameAccess().getNameLITERALTerminalRuleCall_0_2()); | 271 | $current = forceCreateModelElement( |
272 | grammarAccess.getVLSConfirmationsAccess().getVLSTryingAction_2_0(), | ||
273 | $current); | ||
327 | } | 274 | } |
328 | { | 275 | ) |
329 | if ($current==null) { | 276 | otherlv_12='TRYING' |
330 | $current = createModelElement(grammarAccess.getVLSNameRule()); | 277 | { |
278 | newLeafNode(otherlv_12, grammarAccess.getVLSConfirmationsAccess().getTRYINGKeyword_2_1()); | ||
279 | } | ||
280 | otherlv_13='[' | ||
281 | { | ||
282 | newLeafNode(otherlv_13, grammarAccess.getVLSConfirmationsAccess().getLeftSquareBracketKeyword_2_2()); | ||
283 | } | ||
284 | ( | ||
285 | ( | ||
286 | lv_name_14_0=RULE_LITERAL | ||
287 | { | ||
288 | newLeafNode(lv_name_14_0, grammarAccess.getVLSConfirmationsAccess().getNameLITERALTerminalRuleCall_2_3_0()); | ||
331 | } | 289 | } |
332 | setWithLastConsumed( | 290 | { |
333 | $current, | 291 | if ($current==null) { |
334 | "name", | 292 | $current = createModelElement(grammarAccess.getVLSConfirmationsRule()); |
335 | lv_name_0_3, | 293 | } |
336 | "ca.mcgill.ecse.dslreasoner.VampireLanguage.LITERAL"); | 294 | setWithLastConsumed( |
337 | } | 295 | $current, |
338 | | | 296 | "name", |
339 | lv_name_0_4=RULE_SIGNED_LITERAL | 297 | lv_name_14_0, |
340 | { | 298 | "ca.mcgill.ecse.dslreasoner.VampireLanguage.LITERAL"); |
341 | newLeafNode(lv_name_0_4, grammarAccess.getVLSNameAccess().getNameSIGNED_LITERALTerminalRuleCall_0_3()); | ||
342 | } | ||
343 | { | ||
344 | if ($current==null) { | ||
345 | $current = createModelElement(grammarAccess.getVLSNameRule()); | ||
346 | } | 299 | } |
347 | setWithLastConsumed( | 300 | ) |
348 | $current, | ||
349 | "name", | ||
350 | lv_name_0_4, | ||
351 | "ca.mcgill.ecse.dslreasoner.VampireLanguage.SIGNED_LITERAL"); | ||
352 | } | ||
353 | ) | 301 | ) |
302 | otherlv_15=']' | ||
303 | { | ||
304 | newLeafNode(otherlv_15, grammarAccess.getVLSConfirmationsAccess().getRightSquareBracketKeyword_2_4()); | ||
305 | } | ||
354 | ) | 306 | ) |
355 | ) | 307 | | |
356 | ; | ||
357 | |||
358 | // Entry rule entryRuleVLSComment | ||
359 | entryRuleVLSComment returns [EObject current=null]: | ||
360 | { newCompositeNode(grammarAccess.getVLSCommentRule()); } | ||
361 | iv_ruleVLSComment=ruleVLSComment | ||
362 | { $current=$iv_ruleVLSComment.current; } | ||
363 | EOF; | ||
364 | |||
365 | // Rule VLSComment | ||
366 | ruleVLSComment returns [EObject current=null] | ||
367 | @init { | ||
368 | enterRule(); | ||
369 | } | ||
370 | @after { | ||
371 | leaveRule(); | ||
372 | }: | ||
373 | ( | ||
374 | otherlv_0='%' | ||
375 | { | ||
376 | newLeafNode(otherlv_0, grammarAccess.getVLSCommentAccess().getPercentSignKeyword_0()); | ||
377 | } | ||
378 | ( | 308 | ( |
379 | ( | 309 | ( |
380 | lv_comment_1_0=RULE_SINGLE_COMMENT | ||
381 | { | 310 | { |
382 | newLeafNode(lv_comment_1_0, grammarAccess.getVLSCommentAccess().getCommentSINGLE_COMMENTTerminalRuleCall_1_0()); | 311 | $current = forceCreateModelElement( |
383 | } | 312 | grammarAccess.getVLSConfirmationsAccess().getVLSFiniteModelAction_3_0(), |
384 | { | 313 | $current); |
385 | if ($current==null) { | ||
386 | $current = createModelElement(grammarAccess.getVLSCommentRule()); | ||
387 | } | ||
388 | setWithLastConsumed( | ||
389 | $current, | ||
390 | "comment", | ||
391 | lv_comment_1_0, | ||
392 | "ca.mcgill.ecse.dslreasoner.VampireLanguage.SINGLE_COMMENT"); | ||
393 | } | 314 | } |
394 | ) | 315 | ) |
395 | ) | 316 | otherlv_17='Finite' |
396 | ) | ||
397 | ; | ||
398 | |||
399 | // Entry rule entryRuleVLSConfirmations | ||
400 | entryRuleVLSConfirmations returns [EObject current=null]: | ||
401 | { newCompositeNode(grammarAccess.getVLSConfirmationsRule()); } | ||
402 | iv_ruleVLSConfirmations=ruleVLSConfirmations | ||
403 | { $current=$iv_ruleVLSConfirmations.current; } | ||
404 | EOF; | ||
405 | |||
406 | // Rule VLSConfirmations | ||
407 | ruleVLSConfirmations returns [EObject current=null] | ||
408 | @init { | ||
409 | enterRule(); | ||
410 | } | ||
411 | @after { | ||
412 | leaveRule(); | ||
413 | }: | ||
414 | { | ||
415 | newCompositeNode(grammarAccess.getVLSConfirmationsAccess().getVLSSatisfiableParserRuleCall()); | ||
416 | } | ||
417 | this_VLSSatisfiable_0=ruleVLSSatisfiable | ||
418 | { | ||
419 | $current = $this_VLSSatisfiable_0.current; | ||
420 | afterParserOrEnumRuleCall(); | ||
421 | } | ||
422 | ; | ||
423 | |||
424 | // Entry rule entryRuleVLSSatisfiable | ||
425 | entryRuleVLSSatisfiable returns [EObject current=null]: | ||
426 | { newCompositeNode(grammarAccess.getVLSSatisfiableRule()); } | ||
427 | iv_ruleVLSSatisfiable=ruleVLSSatisfiable | ||
428 | { $current=$iv_ruleVLSSatisfiable.current; } | ||
429 | EOF; | ||
430 | |||
431 | // Rule VLSSatisfiable | ||
432 | ruleVLSSatisfiable returns [EObject current=null] | ||
433 | @init { | ||
434 | enterRule(); | ||
435 | } | ||
436 | @after { | ||
437 | leaveRule(); | ||
438 | }: | ||
439 | ( | ||
440 | ( | ||
441 | { | 317 | { |
442 | $current = forceCreateModelElement( | 318 | newLeafNode(otherlv_17, grammarAccess.getVLSConfirmationsAccess().getFiniteKeyword_3_1()); |
443 | grammarAccess.getVLSSatisfiableAccess().getVLSSatisfiableAction_0(), | 319 | } |
444 | $current); | 320 | otherlv_18='Model' |
321 | { | ||
322 | newLeafNode(otherlv_18, grammarAccess.getVLSConfirmationsAccess().getModelKeyword_3_2()); | ||
323 | } | ||
324 | otherlv_19='Found!' | ||
325 | { | ||
326 | newLeafNode(otherlv_19, grammarAccess.getVLSConfirmationsAccess().getFoundKeyword_3_3()); | ||
445 | } | 327 | } |
446 | ) | 328 | ) |
447 | otherlv_1='Satisfiable!' | ||
448 | { | ||
449 | newLeafNode(otherlv_1, grammarAccess.getVLSSatisfiableAccess().getSatisfiableKeyword_1()); | ||
450 | } | ||
451 | ) | 329 | ) |
452 | ; | 330 | ; |
453 | 331 | ||
@@ -633,52 +511,21 @@ ruleVLSTffFormula returns [EObject current=null] | |||
633 | } | 511 | } |
634 | ( | 512 | ( |
635 | ( | 513 | ( |
636 | ( | 514 | { |
637 | lv_name_2_1=RULE_LOWER_WORD_ID | 515 | newCompositeNode(grammarAccess.getVLSTffFormulaAccess().getNameVLSTffNameParserRuleCall_2_0()); |
638 | { | 516 | } |
639 | newLeafNode(lv_name_2_1, grammarAccess.getVLSTffFormulaAccess().getNameLOWER_WORD_IDTerminalRuleCall_2_0_0()); | 517 | lv_name_2_0=ruleVLSTffName |
640 | } | 518 | { |
641 | { | 519 | if ($current==null) { |
642 | if ($current==null) { | 520 | $current = createModelElementForParent(grammarAccess.getVLSTffFormulaRule()); |
643 | $current = createModelElement(grammarAccess.getVLSTffFormulaRule()); | ||
644 | } | ||
645 | setWithLastConsumed( | ||
646 | $current, | ||
647 | "name", | ||
648 | lv_name_2_1, | ||
649 | "ca.mcgill.ecse.dslreasoner.VampireLanguage.LOWER_WORD_ID"); | ||
650 | } | ||
651 | | | ||
652 | lv_name_2_2=RULE_SIGNED_LITERAL | ||
653 | { | ||
654 | newLeafNode(lv_name_2_2, grammarAccess.getVLSTffFormulaAccess().getNameSIGNED_LITERALTerminalRuleCall_2_0_1()); | ||
655 | } | ||
656 | { | ||
657 | if ($current==null) { | ||
658 | $current = createModelElement(grammarAccess.getVLSTffFormulaRule()); | ||
659 | } | ||
660 | setWithLastConsumed( | ||
661 | $current, | ||
662 | "name", | ||
663 | lv_name_2_2, | ||
664 | "ca.mcgill.ecse.dslreasoner.VampireLanguage.SIGNED_LITERAL"); | ||
665 | } | ||
666 | | | ||
667 | lv_name_2_3=RULE_SINGLE_QUOTE | ||
668 | { | ||
669 | newLeafNode(lv_name_2_3, grammarAccess.getVLSTffFormulaAccess().getNameSINGLE_QUOTETerminalRuleCall_2_0_2()); | ||
670 | } | ||
671 | { | ||
672 | if ($current==null) { | ||
673 | $current = createModelElement(grammarAccess.getVLSTffFormulaRule()); | ||
674 | } | ||
675 | setWithLastConsumed( | ||
676 | $current, | ||
677 | "name", | ||
678 | lv_name_2_3, | ||
679 | "ca.mcgill.ecse.dslreasoner.VampireLanguage.SINGLE_QUOTE"); | ||
680 | } | 521 | } |
681 | ) | 522 | set( |
523 | $current, | ||
524 | "name", | ||
525 | lv_name_2_0, | ||
526 | "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSTffName"); | ||
527 | afterParserOrEnumRuleCall(); | ||
528 | } | ||
682 | ) | 529 | ) |
683 | ) | 530 | ) |
684 | otherlv_3=',' | 531 | otherlv_3=',' |
@@ -688,17 +535,17 @@ ruleVLSTffFormula returns [EObject current=null] | |||
688 | ( | 535 | ( |
689 | ( | 536 | ( |
690 | { | 537 | { |
691 | newCompositeNode(grammarAccess.getVLSTffFormulaAccess().getFofRoleVLSRoleParserRuleCall_4_0()); | 538 | newCompositeNode(grammarAccess.getVLSTffFormulaAccess().getTffRoleVLSRoleParserRuleCall_4_0()); |
692 | } | 539 | } |
693 | lv_fofRole_4_0=ruleVLSRole | 540 | lv_tffRole_4_0=ruleVLSRole |
694 | { | 541 | { |
695 | if ($current==null) { | 542 | if ($current==null) { |
696 | $current = createModelElementForParent(grammarAccess.getVLSTffFormulaRule()); | 543 | $current = createModelElementForParent(grammarAccess.getVLSTffFormulaRule()); |
697 | } | 544 | } |
698 | set( | 545 | set( |
699 | $current, | 546 | $current, |
700 | "fofRole", | 547 | "tffRole", |
701 | lv_fofRole_4_0, | 548 | lv_tffRole_4_0, |
702 | "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSRole"); | 549 | "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSRole"); |
703 | afterParserOrEnumRuleCall(); | 550 | afterParserOrEnumRuleCall(); |
704 | } | 551 | } |
@@ -711,9 +558,9 @@ ruleVLSTffFormula returns [EObject current=null] | |||
711 | ( | 558 | ( |
712 | ( | 559 | ( |
713 | { | 560 | { |
714 | newCompositeNode(grammarAccess.getVLSTffFormulaAccess().getFofFormulaVLSTermParserRuleCall_6_0()); | 561 | newCompositeNode(grammarAccess.getVLSTffFormulaAccess().getFofFormulaVLSTffTermParserRuleCall_6_0()); |
715 | } | 562 | } |
716 | lv_fofFormula_6_0=ruleVLSTerm | 563 | lv_fofFormula_6_0=ruleVLSTffTerm |
717 | { | 564 | { |
718 | if ($current==null) { | 565 | if ($current==null) { |
719 | $current = createModelElementForParent(grammarAccess.getVLSTffFormulaRule()); | 566 | $current = createModelElementForParent(grammarAccess.getVLSTffFormulaRule()); |
@@ -722,7 +569,7 @@ ruleVLSTffFormula returns [EObject current=null] | |||
722 | $current, | 569 | $current, |
723 | "fofFormula", | 570 | "fofFormula", |
724 | lv_fofFormula_6_0, | 571 | lv_fofFormula_6_0, |
725 | "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSTerm"); | 572 | "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSTffTerm"); |
726 | afterParserOrEnumRuleCall(); | 573 | afterParserOrEnumRuleCall(); |
727 | } | 574 | } |
728 | ) | 575 | ) |
@@ -763,6 +610,142 @@ ruleVLSTffFormula returns [EObject current=null] | |||
763 | ) | 610 | ) |
764 | ; | 611 | ; |
765 | 612 | ||
613 | // Entry rule entryRuleVLSTffName | ||
614 | entryRuleVLSTffName returns [String current=null]: | ||
615 | { newCompositeNode(grammarAccess.getVLSTffNameRule()); } | ||
616 | iv_ruleVLSTffName=ruleVLSTffName | ||
617 | { $current=$iv_ruleVLSTffName.current.getText(); } | ||
618 | EOF; | ||
619 | |||
620 | // Rule VLSTffName | ||
621 | ruleVLSTffName returns [AntlrDatatypeRuleToken current=new AntlrDatatypeRuleToken()] | ||
622 | @init { | ||
623 | enterRule(); | ||
624 | } | ||
625 | @after { | ||
626 | leaveRule(); | ||
627 | }: | ||
628 | ( | ||
629 | { | ||
630 | newCompositeNode(grammarAccess.getVLSTffNameAccess().getVLSTffDeclPredParserRuleCall_0()); | ||
631 | } | ||
632 | this_VLSTffDeclPred_0=ruleVLSTffDeclPred | ||
633 | { | ||
634 | $current.merge(this_VLSTffDeclPred_0); | ||
635 | } | ||
636 | { | ||
637 | afterParserOrEnumRuleCall(); | ||
638 | } | ||
639 | | | ||
640 | { | ||
641 | newCompositeNode(grammarAccess.getVLSTffNameAccess().getVLSTffFiniteParserRuleCall_1()); | ||
642 | } | ||
643 | this_VLSTffFinite_1=ruleVLSTffFinite | ||
644 | { | ||
645 | $current.merge(this_VLSTffFinite_1); | ||
646 | } | ||
647 | { | ||
648 | afterParserOrEnumRuleCall(); | ||
649 | } | ||
650 | | | ||
651 | { | ||
652 | newCompositeNode(grammarAccess.getVLSTffNameAccess().getVLSTffDistinctParserRuleCall_2()); | ||
653 | } | ||
654 | this_VLSTffDistinct_2=ruleVLSTffDistinct | ||
655 | { | ||
656 | $current.merge(this_VLSTffDistinct_2); | ||
657 | } | ||
658 | { | ||
659 | afterParserOrEnumRuleCall(); | ||
660 | } | ||
661 | ) | ||
662 | ; | ||
663 | |||
664 | // Entry rule entryRuleVLSTffDistinct | ||
665 | entryRuleVLSTffDistinct returns [String current=null]: | ||
666 | { newCompositeNode(grammarAccess.getVLSTffDistinctRule()); } | ||
667 | iv_ruleVLSTffDistinct=ruleVLSTffDistinct | ||
668 | { $current=$iv_ruleVLSTffDistinct.current.getText(); } | ||
669 | EOF; | ||
670 | |||
671 | // Rule VLSTffDistinct | ||
672 | ruleVLSTffDistinct returns [AntlrDatatypeRuleToken current=new AntlrDatatypeRuleToken()] | ||
673 | @init { | ||
674 | enterRule(); | ||
675 | } | ||
676 | @after { | ||
677 | leaveRule(); | ||
678 | }: | ||
679 | kw='distinct_domain' | ||
680 | { | ||
681 | $current.merge(kw); | ||
682 | newLeafNode(kw, grammarAccess.getVLSTffDistinctAccess().getDistinct_domainKeyword()); | ||
683 | } | ||
684 | ; | ||
685 | |||
686 | // Entry rule entryRuleVLSTffFinite | ||
687 | entryRuleVLSTffFinite returns [String current=null]: | ||
688 | { newCompositeNode(grammarAccess.getVLSTffFiniteRule()); } | ||
689 | iv_ruleVLSTffFinite=ruleVLSTffFinite | ||
690 | { $current=$iv_ruleVLSTffFinite.current.getText(); } | ||
691 | EOF; | ||
692 | |||
693 | // Rule VLSTffFinite | ||
694 | ruleVLSTffFinite returns [AntlrDatatypeRuleToken current=new AntlrDatatypeRuleToken()] | ||
695 | @init { | ||
696 | enterRule(); | ||
697 | } | ||
698 | @after { | ||
699 | leaveRule(); | ||
700 | }: | ||
701 | kw='finite_domain' | ||
702 | { | ||
703 | $current.merge(kw); | ||
704 | newLeafNode(kw, grammarAccess.getVLSTffFiniteAccess().getFinite_domainKeyword()); | ||
705 | } | ||
706 | ; | ||
707 | |||
708 | // Entry rule entryRuleVLSTffDeclPred | ||
709 | entryRuleVLSTffDeclPred returns [String current=null]: | ||
710 | { newCompositeNode(grammarAccess.getVLSTffDeclPredRule()); } | ||
711 | iv_ruleVLSTffDeclPred=ruleVLSTffDeclPred | ||
712 | { $current=$iv_ruleVLSTffDeclPred.current.getText(); } | ||
713 | EOF; | ||
714 | |||
715 | // Rule VLSTffDeclPred | ||
716 | ruleVLSTffDeclPred returns [AntlrDatatypeRuleToken current=new AntlrDatatypeRuleToken()] | ||
717 | @init { | ||
718 | enterRule(); | ||
719 | } | ||
720 | @after { | ||
721 | leaveRule(); | ||
722 | }: | ||
723 | ( | ||
724 | ( | ||
725 | kw='declare_' | ||
726 | { | ||
727 | $current.merge(kw); | ||
728 | newLeafNode(kw, grammarAccess.getVLSTffDeclPredAccess().getDeclare_Keyword_0_0()); | ||
729 | } | ||
730 | this_DOLLAR_ID_1=RULE_DOLLAR_ID | ||
731 | { | ||
732 | $current.merge(this_DOLLAR_ID_1); | ||
733 | } | ||
734 | { | ||
735 | newLeafNode(this_DOLLAR_ID_1, grammarAccess.getVLSTffDeclPredAccess().getDOLLAR_IDTerminalRuleCall_0_1()); | ||
736 | } | ||
737 | ) | ||
738 | | | ||
739 | this_LOWER_WORD_ID_2=RULE_LOWER_WORD_ID | ||
740 | { | ||
741 | $current.merge(this_LOWER_WORD_ID_2); | ||
742 | } | ||
743 | { | ||
744 | newLeafNode(this_LOWER_WORD_ID_2, grammarAccess.getVLSTffDeclPredAccess().getLOWER_WORD_IDTerminalRuleCall_1()); | ||
745 | } | ||
746 | ) | ||
747 | ; | ||
748 | |||
766 | // Entry rule entryRuleVLSRole | 749 | // Entry rule entryRuleVLSRole |
767 | entryRuleVLSRole returns [String current=null]: | 750 | entryRuleVLSRole returns [String current=null]: |
768 | { newCompositeNode(grammarAccess.getVLSRoleRule()); } | 751 | { newCompositeNode(grammarAccess.getVLSRoleRule()); } |
@@ -1045,6 +1028,304 @@ ruleVLSAnnotationTerms returns [EObject current=null] | |||
1045 | ) | 1028 | ) |
1046 | ; | 1029 | ; |
1047 | 1030 | ||
1031 | // Entry rule entryRuleVLSTffTerm | ||
1032 | entryRuleVLSTffTerm returns [EObject current=null]: | ||
1033 | { newCompositeNode(grammarAccess.getVLSTffTermRule()); } | ||
1034 | iv_ruleVLSTffTerm=ruleVLSTffTerm | ||
1035 | { $current=$iv_ruleVLSTffTerm.current; } | ||
1036 | EOF; | ||
1037 | |||
1038 | // Rule VLSTffTerm | ||
1039 | ruleVLSTffTerm returns [EObject current=null] | ||
1040 | @init { | ||
1041 | enterRule(); | ||
1042 | } | ||
1043 | @after { | ||
1044 | leaveRule(); | ||
1045 | }: | ||
1046 | ( | ||
1047 | { | ||
1048 | newCompositeNode(grammarAccess.getVLSTffTermAccess().getVLSTermParserRuleCall_0()); | ||
1049 | } | ||
1050 | this_VLSTerm_0=ruleVLSTerm | ||
1051 | { | ||
1052 | $current = $this_VLSTerm_0.current; | ||
1053 | afterParserOrEnumRuleCall(); | ||
1054 | } | ||
1055 | | | ||
1056 | { | ||
1057 | newCompositeNode(grammarAccess.getVLSTffTermAccess().getVLSDeclarationParserRuleCall_1()); | ||
1058 | } | ||
1059 | this_VLSDeclaration_1=ruleVLSDeclaration | ||
1060 | { | ||
1061 | $current = $this_VLSDeclaration_1.current; | ||
1062 | afterParserOrEnumRuleCall(); | ||
1063 | } | ||
1064 | ) | ||
1065 | ; | ||
1066 | |||
1067 | // Entry rule entryRuleVLSDeclaration | ||
1068 | entryRuleVLSDeclaration returns [EObject current=null]: | ||
1069 | { newCompositeNode(grammarAccess.getVLSDeclarationRule()); } | ||
1070 | iv_ruleVLSDeclaration=ruleVLSDeclaration | ||
1071 | { $current=$iv_ruleVLSDeclaration.current; } | ||
1072 | EOF; | ||
1073 | |||
1074 | // Rule VLSDeclaration | ||
1075 | ruleVLSDeclaration returns [EObject current=null] | ||
1076 | @init { | ||
1077 | enterRule(); | ||
1078 | } | ||
1079 | @after { | ||
1080 | leaveRule(); | ||
1081 | }: | ||
1082 | ( | ||
1083 | { | ||
1084 | newCompositeNode(grammarAccess.getVLSDeclarationAccess().getVLSVariableDeclarationParserRuleCall_0()); | ||
1085 | } | ||
1086 | this_VLSVariableDeclaration_0=ruleVLSVariableDeclaration | ||
1087 | { | ||
1088 | $current = $this_VLSVariableDeclaration_0.current; | ||
1089 | afterParserOrEnumRuleCall(); | ||
1090 | } | ||
1091 | | | ||
1092 | { | ||
1093 | newCompositeNode(grammarAccess.getVLSDeclarationAccess().getVLSOtherDeclarationParserRuleCall_1()); | ||
1094 | } | ||
1095 | this_VLSOtherDeclaration_1=ruleVLSOtherDeclaration | ||
1096 | { | ||
1097 | $current = $this_VLSOtherDeclaration_1.current; | ||
1098 | afterParserOrEnumRuleCall(); | ||
1099 | } | ||
1100 | ) | ||
1101 | ; | ||
1102 | |||
1103 | // Entry rule entryRuleVLSOtherDeclaration | ||
1104 | entryRuleVLSOtherDeclaration returns [EObject current=null]: | ||
1105 | { newCompositeNode(grammarAccess.getVLSOtherDeclarationRule()); } | ||
1106 | iv_ruleVLSOtherDeclaration=ruleVLSOtherDeclaration | ||
1107 | { $current=$iv_ruleVLSOtherDeclaration.current; } | ||
1108 | EOF; | ||
1109 | |||
1110 | // Rule VLSOtherDeclaration | ||
1111 | ruleVLSOtherDeclaration returns [EObject current=null] | ||
1112 | @init { | ||
1113 | enterRule(); | ||
1114 | } | ||
1115 | @after { | ||
1116 | leaveRule(); | ||
1117 | }: | ||
1118 | ( | ||
1119 | { | ||
1120 | newCompositeNode(grammarAccess.getVLSOtherDeclarationAccess().getVLSAtomicConstantParserRuleCall_0()); | ||
1121 | } | ||
1122 | this_VLSAtomicConstant_0=ruleVLSAtomicConstant | ||
1123 | { | ||
1124 | $current = $this_VLSAtomicConstant_0.current; | ||
1125 | afterParserOrEnumRuleCall(); | ||
1126 | } | ||
1127 | otherlv_1=':' | ||
1128 | { | ||
1129 | newLeafNode(otherlv_1, grammarAccess.getVLSOtherDeclarationAccess().getColonKeyword_1()); | ||
1130 | } | ||
1131 | ( | ||
1132 | ( | ||
1133 | { | ||
1134 | newCompositeNode(grammarAccess.getVLSOtherDeclarationAccess().getTypeVLSTypeDefParserRuleCall_2_0()); | ||
1135 | } | ||
1136 | lv_type_2_0=ruleVLSTypeDef | ||
1137 | { | ||
1138 | if ($current==null) { | ||
1139 | $current = createModelElementForParent(grammarAccess.getVLSOtherDeclarationRule()); | ||
1140 | } | ||
1141 | set( | ||
1142 | $current, | ||
1143 | "type", | ||
1144 | lv_type_2_0, | ||
1145 | "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSTypeDef"); | ||
1146 | afterParserOrEnumRuleCall(); | ||
1147 | } | ||
1148 | ) | ||
1149 | ) | ||
1150 | ) | ||
1151 | ; | ||
1152 | |||
1153 | // Entry rule entryRuleVLSVariableDeclaration | ||
1154 | entryRuleVLSVariableDeclaration returns [EObject current=null]: | ||
1155 | { newCompositeNode(grammarAccess.getVLSVariableDeclarationRule()); } | ||
1156 | iv_ruleVLSVariableDeclaration=ruleVLSVariableDeclaration | ||
1157 | { $current=$iv_ruleVLSVariableDeclaration.current; } | ||
1158 | EOF; | ||
1159 | |||
1160 | // Rule VLSVariableDeclaration | ||
1161 | ruleVLSVariableDeclaration returns [EObject current=null] | ||
1162 | @init { | ||
1163 | enterRule(); | ||
1164 | } | ||
1165 | @after { | ||
1166 | leaveRule(); | ||
1167 | }: | ||
1168 | ( | ||
1169 | { | ||
1170 | newCompositeNode(grammarAccess.getVLSVariableDeclarationAccess().getVLSVariableParserRuleCall_0()); | ||
1171 | } | ||
1172 | this_VLSVariable_0=ruleVLSVariable | ||
1173 | { | ||
1174 | $current = $this_VLSVariable_0.current; | ||
1175 | afterParserOrEnumRuleCall(); | ||
1176 | } | ||
1177 | otherlv_1=':' | ||
1178 | { | ||
1179 | newLeafNode(otherlv_1, grammarAccess.getVLSVariableDeclarationAccess().getColonKeyword_1()); | ||
1180 | } | ||
1181 | ( | ||
1182 | ( | ||
1183 | { | ||
1184 | newCompositeNode(grammarAccess.getVLSVariableDeclarationAccess().getTypeVLSTypeDefParserRuleCall_2_0()); | ||
1185 | } | ||
1186 | lv_type_2_0=ruleVLSTypeDef | ||
1187 | { | ||
1188 | if ($current==null) { | ||
1189 | $current = createModelElementForParent(grammarAccess.getVLSVariableDeclarationRule()); | ||
1190 | } | ||
1191 | set( | ||
1192 | $current, | ||
1193 | "type", | ||
1194 | lv_type_2_0, | ||
1195 | "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSTypeDef"); | ||
1196 | afterParserOrEnumRuleCall(); | ||
1197 | } | ||
1198 | ) | ||
1199 | ) | ||
1200 | ) | ||
1201 | ; | ||
1202 | |||
1203 | // Entry rule entryRuleVLSTypeDef | ||
1204 | entryRuleVLSTypeDef returns [EObject current=null]: | ||
1205 | { newCompositeNode(grammarAccess.getVLSTypeDefRule()); } | ||
1206 | iv_ruleVLSTypeDef=ruleVLSTypeDef | ||
1207 | { $current=$iv_ruleVLSTypeDef.current; } | ||
1208 | EOF; | ||
1209 | |||
1210 | // Rule VLSTypeDef | ||
1211 | ruleVLSTypeDef returns [EObject current=null] | ||
1212 | @init { | ||
1213 | enterRule(); | ||
1214 | } | ||
1215 | @after { | ||
1216 | leaveRule(); | ||
1217 | }: | ||
1218 | ( | ||
1219 | ( | ||
1220 | ( | ||
1221 | { | ||
1222 | newCompositeNode(grammarAccess.getVLSTypeDefAccess().getTypeSigVLSUnitaryTermParserRuleCall_0_0()); | ||
1223 | } | ||
1224 | lv_typeSig_0_0=ruleVLSUnitaryTerm | ||
1225 | { | ||
1226 | if ($current==null) { | ||
1227 | $current = createModelElementForParent(grammarAccess.getVLSTypeDefRule()); | ||
1228 | } | ||
1229 | set( | ||
1230 | $current, | ||
1231 | "typeSig", | ||
1232 | lv_typeSig_0_0, | ||
1233 | "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSUnitaryTerm"); | ||
1234 | afterParserOrEnumRuleCall(); | ||
1235 | } | ||
1236 | ) | ||
1237 | ) | ||
1238 | ( | ||
1239 | otherlv_1='>' | ||
1240 | { | ||
1241 | newLeafNode(otherlv_1, grammarAccess.getVLSTypeDefAccess().getGreaterThanSignKeyword_1_0()); | ||
1242 | } | ||
1243 | ( | ||
1244 | ( | ||
1245 | { | ||
1246 | newCompositeNode(grammarAccess.getVLSTypeDefAccess().getMapsToVLSAtomicConstantParserRuleCall_1_1_0()); | ||
1247 | } | ||
1248 | lv_mapsTo_2_0=ruleVLSAtomicConstant | ||
1249 | { | ||
1250 | if ($current==null) { | ||
1251 | $current = createModelElementForParent(grammarAccess.getVLSTypeDefRule()); | ||
1252 | } | ||
1253 | set( | ||
1254 | $current, | ||
1255 | "mapsTo", | ||
1256 | lv_mapsTo_2_0, | ||
1257 | "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSAtomicConstant"); | ||
1258 | afterParserOrEnumRuleCall(); | ||
1259 | } | ||
1260 | ) | ||
1261 | ) | ||
1262 | )? | ||
1263 | ) | ||
1264 | ; | ||
1265 | |||
1266 | // Entry rule entryRuleVLSUnitaryTerm | ||
1267 | entryRuleVLSUnitaryTerm returns [EObject current=null]: | ||
1268 | { newCompositeNode(grammarAccess.getVLSUnitaryTermRule()); } | ||
1269 | iv_ruleVLSUnitaryTerm=ruleVLSUnitaryTerm | ||
1270 | { $current=$iv_ruleVLSUnitaryTerm.current; } | ||
1271 | EOF; | ||
1272 | |||
1273 | // Rule VLSUnitaryTerm | ||
1274 | ruleVLSUnitaryTerm returns [EObject current=null] | ||
1275 | @init { | ||
1276 | enterRule(); | ||
1277 | } | ||
1278 | @after { | ||
1279 | leaveRule(); | ||
1280 | }: | ||
1281 | ( | ||
1282 | ( | ||
1283 | ( | ||
1284 | { | ||
1285 | newCompositeNode(grammarAccess.getVLSUnitaryTermAccess().getInitTypeVLSAtomicParserRuleCall_0_0()); | ||
1286 | } | ||
1287 | lv_initType_0_0=ruleVLSAtomic | ||
1288 | { | ||
1289 | if ($current==null) { | ||
1290 | $current = createModelElementForParent(grammarAccess.getVLSUnitaryTermRule()); | ||
1291 | } | ||
1292 | set( | ||
1293 | $current, | ||
1294 | "initType", | ||
1295 | lv_initType_0_0, | ||
1296 | "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSAtomic"); | ||
1297 | afterParserOrEnumRuleCall(); | ||
1298 | } | ||
1299 | ) | ||
1300 | ) | ||
1301 | ( | ||
1302 | otherlv_1='*' | ||
1303 | { | ||
1304 | newLeafNode(otherlv_1, grammarAccess.getVLSUnitaryTermAccess().getAsteriskKeyword_1_0()); | ||
1305 | } | ||
1306 | ( | ||
1307 | ( | ||
1308 | { | ||
1309 | newCompositeNode(grammarAccess.getVLSUnitaryTermAccess().getNextTypeVLSAtomicConstantParserRuleCall_1_1_0()); | ||
1310 | } | ||
1311 | lv_nextType_2_0=ruleVLSAtomicConstant | ||
1312 | { | ||
1313 | if ($current==null) { | ||
1314 | $current = createModelElementForParent(grammarAccess.getVLSUnitaryTermRule()); | ||
1315 | } | ||
1316 | set( | ||
1317 | $current, | ||
1318 | "nextType", | ||
1319 | lv_nextType_2_0, | ||
1320 | "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSAtomicConstant"); | ||
1321 | afterParserOrEnumRuleCall(); | ||
1322 | } | ||
1323 | ) | ||
1324 | ) | ||
1325 | )* | ||
1326 | ) | ||
1327 | ; | ||
1328 | |||
1048 | // Entry rule entryRuleVLSTerm | 1329 | // Entry rule entryRuleVLSTerm |
1049 | entryRuleVLSTerm returns [EObject current=null]: | 1330 | entryRuleVLSTerm returns [EObject current=null]: |
1050 | { newCompositeNode(grammarAccess.getVLSTermRule()); } | 1331 | { newCompositeNode(grammarAccess.getVLSTermRule()); } |
@@ -1378,34 +1659,11 @@ ruleVLSUniversalQuantifier returns [EObject current=null] | |||
1378 | } | 1659 | } |
1379 | ( | 1660 | ( |
1380 | ( | 1661 | ( |
1381 | { | ||
1382 | newCompositeNode(grammarAccess.getVLSUniversalQuantifierAccess().getVariablesVLSVariableParserRuleCall_1_2_0()); | ||
1383 | } | ||
1384 | lv_variables_3_0=ruleVLSVariable | ||
1385 | { | ||
1386 | if ($current==null) { | ||
1387 | $current = createModelElementForParent(grammarAccess.getVLSUniversalQuantifierRule()); | ||
1388 | } | ||
1389 | add( | ||
1390 | $current, | ||
1391 | "variables", | ||
1392 | lv_variables_3_0, | ||
1393 | "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSVariable"); | ||
1394 | afterParserOrEnumRuleCall(); | ||
1395 | } | ||
1396 | ) | ||
1397 | ) | ||
1398 | ( | ||
1399 | otherlv_4=',' | ||
1400 | { | ||
1401 | newLeafNode(otherlv_4, grammarAccess.getVLSUniversalQuantifierAccess().getCommaKeyword_1_3_0()); | ||
1402 | } | ||
1403 | ( | ||
1404 | ( | 1662 | ( |
1405 | { | 1663 | { |
1406 | newCompositeNode(grammarAccess.getVLSUniversalQuantifierAccess().getVariablesVLSVariableParserRuleCall_1_3_1_0()); | 1664 | newCompositeNode(grammarAccess.getVLSUniversalQuantifierAccess().getVariablesVLSVariableParserRuleCall_1_2_0_0()); |
1407 | } | 1665 | } |
1408 | lv_variables_5_0=ruleVLSVariable | 1666 | lv_variables_3_1=ruleVLSVariable |
1409 | { | 1667 | { |
1410 | if ($current==null) { | 1668 | if ($current==null) { |
1411 | $current = createModelElementForParent(grammarAccess.getVLSUniversalQuantifierRule()); | 1669 | $current = createModelElementForParent(grammarAccess.getVLSUniversalQuantifierRule()); |
@@ -1413,10 +1671,69 @@ ruleVLSUniversalQuantifier returns [EObject current=null] | |||
1413 | add( | 1671 | add( |
1414 | $current, | 1672 | $current, |
1415 | "variables", | 1673 | "variables", |
1416 | lv_variables_5_0, | 1674 | lv_variables_3_1, |
1417 | "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSVariable"); | 1675 | "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSVariable"); |
1418 | afterParserOrEnumRuleCall(); | 1676 | afterParserOrEnumRuleCall(); |
1419 | } | 1677 | } |
1678 | | | ||
1679 | { | ||
1680 | newCompositeNode(grammarAccess.getVLSUniversalQuantifierAccess().getVariablesVLSVariableDeclarationParserRuleCall_1_2_0_1()); | ||
1681 | } | ||
1682 | lv_variables_3_2=ruleVLSVariableDeclaration | ||
1683 | { | ||
1684 | if ($current==null) { | ||
1685 | $current = createModelElementForParent(grammarAccess.getVLSUniversalQuantifierRule()); | ||
1686 | } | ||
1687 | add( | ||
1688 | $current, | ||
1689 | "variables", | ||
1690 | lv_variables_3_2, | ||
1691 | "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSVariableDeclaration"); | ||
1692 | afterParserOrEnumRuleCall(); | ||
1693 | } | ||
1694 | ) | ||
1695 | ) | ||
1696 | ) | ||
1697 | ( | ||
1698 | otherlv_4=',' | ||
1699 | { | ||
1700 | newLeafNode(otherlv_4, grammarAccess.getVLSUniversalQuantifierAccess().getCommaKeyword_1_3_0()); | ||
1701 | } | ||
1702 | ( | ||
1703 | ( | ||
1704 | ( | ||
1705 | { | ||
1706 | newCompositeNode(grammarAccess.getVLSUniversalQuantifierAccess().getVariablesVLSVariableParserRuleCall_1_3_1_0_0()); | ||
1707 | } | ||
1708 | lv_variables_5_1=ruleVLSVariable | ||
1709 | { | ||
1710 | if ($current==null) { | ||
1711 | $current = createModelElementForParent(grammarAccess.getVLSUniversalQuantifierRule()); | ||
1712 | } | ||
1713 | add( | ||
1714 | $current, | ||
1715 | "variables", | ||
1716 | lv_variables_5_1, | ||
1717 | "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSVariable"); | ||
1718 | afterParserOrEnumRuleCall(); | ||
1719 | } | ||
1720 | | | ||
1721 | { | ||
1722 | newCompositeNode(grammarAccess.getVLSUniversalQuantifierAccess().getVariablesVLSVariableDeclarationParserRuleCall_1_3_1_0_1()); | ||
1723 | } | ||
1724 | lv_variables_5_2=ruleVLSVariableDeclaration | ||
1725 | { | ||
1726 | if ($current==null) { | ||
1727 | $current = createModelElementForParent(grammarAccess.getVLSUniversalQuantifierRule()); | ||
1728 | } | ||
1729 | add( | ||
1730 | $current, | ||
1731 | "variables", | ||
1732 | lv_variables_5_2, | ||
1733 | "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSVariableDeclaration"); | ||
1734 | afterParserOrEnumRuleCall(); | ||
1735 | } | ||
1736 | ) | ||
1420 | ) | 1737 | ) |
1421 | ) | 1738 | ) |
1422 | )* | 1739 | )* |
@@ -1485,34 +1802,11 @@ ruleVLSExistentialQuantifier returns [EObject current=null] | |||
1485 | } | 1802 | } |
1486 | ( | 1803 | ( |
1487 | ( | 1804 | ( |
1488 | { | ||
1489 | newCompositeNode(grammarAccess.getVLSExistentialQuantifierAccess().getVariablesVLSVariableParserRuleCall_1_2_0()); | ||
1490 | } | ||
1491 | lv_variables_3_0=ruleVLSVariable | ||
1492 | { | ||
1493 | if ($current==null) { | ||
1494 | $current = createModelElementForParent(grammarAccess.getVLSExistentialQuantifierRule()); | ||
1495 | } | ||
1496 | add( | ||
1497 | $current, | ||
1498 | "variables", | ||
1499 | lv_variables_3_0, | ||
1500 | "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSVariable"); | ||
1501 | afterParserOrEnumRuleCall(); | ||
1502 | } | ||
1503 | ) | ||
1504 | ) | ||
1505 | ( | ||
1506 | otherlv_4=',' | ||
1507 | { | ||
1508 | newLeafNode(otherlv_4, grammarAccess.getVLSExistentialQuantifierAccess().getCommaKeyword_1_3_0()); | ||
1509 | } | ||
1510 | ( | ||
1511 | ( | 1805 | ( |
1512 | { | 1806 | { |
1513 | newCompositeNode(grammarAccess.getVLSExistentialQuantifierAccess().getVariablesVLSVariableParserRuleCall_1_3_1_0()); | 1807 | newCompositeNode(grammarAccess.getVLSExistentialQuantifierAccess().getVariablesVLSVariableParserRuleCall_1_2_0_0()); |
1514 | } | 1808 | } |
1515 | lv_variables_5_0=ruleVLSVariable | 1809 | lv_variables_3_1=ruleVLSVariable |
1516 | { | 1810 | { |
1517 | if ($current==null) { | 1811 | if ($current==null) { |
1518 | $current = createModelElementForParent(grammarAccess.getVLSExistentialQuantifierRule()); | 1812 | $current = createModelElementForParent(grammarAccess.getVLSExistentialQuantifierRule()); |
@@ -1520,10 +1814,69 @@ ruleVLSExistentialQuantifier returns [EObject current=null] | |||
1520 | add( | 1814 | add( |
1521 | $current, | 1815 | $current, |
1522 | "variables", | 1816 | "variables", |
1523 | lv_variables_5_0, | 1817 | lv_variables_3_1, |
1524 | "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSVariable"); | 1818 | "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSVariable"); |
1525 | afterParserOrEnumRuleCall(); | 1819 | afterParserOrEnumRuleCall(); |
1526 | } | 1820 | } |
1821 | | | ||
1822 | { | ||
1823 | newCompositeNode(grammarAccess.getVLSExistentialQuantifierAccess().getVariablesVLSVariableDeclarationParserRuleCall_1_2_0_1()); | ||
1824 | } | ||
1825 | lv_variables_3_2=ruleVLSVariableDeclaration | ||
1826 | { | ||
1827 | if ($current==null) { | ||
1828 | $current = createModelElementForParent(grammarAccess.getVLSExistentialQuantifierRule()); | ||
1829 | } | ||
1830 | add( | ||
1831 | $current, | ||
1832 | "variables", | ||
1833 | lv_variables_3_2, | ||
1834 | "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSVariableDeclaration"); | ||
1835 | afterParserOrEnumRuleCall(); | ||
1836 | } | ||
1837 | ) | ||
1838 | ) | ||
1839 | ) | ||
1840 | ( | ||
1841 | otherlv_4=',' | ||
1842 | { | ||
1843 | newLeafNode(otherlv_4, grammarAccess.getVLSExistentialQuantifierAccess().getCommaKeyword_1_3_0()); | ||
1844 | } | ||
1845 | ( | ||
1846 | ( | ||
1847 | ( | ||
1848 | { | ||
1849 | newCompositeNode(grammarAccess.getVLSExistentialQuantifierAccess().getVariablesVLSVariableParserRuleCall_1_3_1_0_0()); | ||
1850 | } | ||
1851 | lv_variables_5_1=ruleVLSVariable | ||
1852 | { | ||
1853 | if ($current==null) { | ||
1854 | $current = createModelElementForParent(grammarAccess.getVLSExistentialQuantifierRule()); | ||
1855 | } | ||
1856 | add( | ||
1857 | $current, | ||
1858 | "variables", | ||
1859 | lv_variables_5_1, | ||
1860 | "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSVariable"); | ||
1861 | afterParserOrEnumRuleCall(); | ||
1862 | } | ||
1863 | | | ||
1864 | { | ||
1865 | newCompositeNode(grammarAccess.getVLSExistentialQuantifierAccess().getVariablesVLSVariableDeclarationParserRuleCall_1_3_1_0_1()); | ||
1866 | } | ||
1867 | lv_variables_5_2=ruleVLSVariableDeclaration | ||
1868 | { | ||
1869 | if ($current==null) { | ||
1870 | $current = createModelElementForParent(grammarAccess.getVLSExistentialQuantifierRule()); | ||
1871 | } | ||
1872 | add( | ||
1873 | $current, | ||
1874 | "variables", | ||
1875 | lv_variables_5_2, | ||
1876 | "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSVariableDeclaration"); | ||
1877 | afterParserOrEnumRuleCall(); | ||
1878 | } | ||
1879 | ) | ||
1527 | ) | 1880 | ) |
1528 | ) | 1881 | ) |
1529 | )* | 1882 | )* |
@@ -2392,15 +2745,15 @@ ruleVLSDefinedTerm returns [EObject current=null] | |||
2392 | ( | 2745 | ( |
2393 | { | 2746 | { |
2394 | $current = forceCreateModelElement( | 2747 | $current = forceCreateModelElement( |
2395 | grammarAccess.getVLSDefinedTermAccess().getVLSRealAction_1_0(), | 2748 | grammarAccess.getVLSDefinedTermAccess().getVLSDoubleQuoteAction_1_0(), |
2396 | $current); | 2749 | $current); |
2397 | } | 2750 | } |
2398 | ) | 2751 | ) |
2399 | ( | 2752 | ( |
2400 | ( | 2753 | ( |
2401 | lv_value_3_0=RULE_SIGNED_REAL_ID | 2754 | lv_value_3_0=RULE_DOUBLE_QUOTE |
2402 | { | 2755 | { |
2403 | newLeafNode(lv_value_3_0, grammarAccess.getVLSDefinedTermAccess().getValueSIGNED_REAL_IDTerminalRuleCall_1_1_0()); | 2756 | newLeafNode(lv_value_3_0, grammarAccess.getVLSDefinedTermAccess().getValueDOUBLE_QUOTETerminalRuleCall_1_1_0()); |
2404 | } | 2757 | } |
2405 | { | 2758 | { |
2406 | if ($current==null) { | 2759 | if ($current==null) { |
@@ -2410,62 +2763,6 @@ ruleVLSDefinedTerm returns [EObject current=null] | |||
2410 | $current, | 2763 | $current, |
2411 | "value", | 2764 | "value", |
2412 | lv_value_3_0, | 2765 | lv_value_3_0, |
2413 | "ca.mcgill.ecse.dslreasoner.VampireLanguage.SIGNED_REAL_ID"); | ||
2414 | } | ||
2415 | ) | ||
2416 | ) | ||
2417 | ) | ||
2418 | | | ||
2419 | ( | ||
2420 | ( | ||
2421 | { | ||
2422 | $current = forceCreateModelElement( | ||
2423 | grammarAccess.getVLSDefinedTermAccess().getVLSRationalAction_2_0(), | ||
2424 | $current); | ||
2425 | } | ||
2426 | ) | ||
2427 | ( | ||
2428 | ( | ||
2429 | lv_value_5_0=RULE_SIGNED_RAT_ID | ||
2430 | { | ||
2431 | newLeafNode(lv_value_5_0, grammarAccess.getVLSDefinedTermAccess().getValueSIGNED_RAT_IDTerminalRuleCall_2_1_0()); | ||
2432 | } | ||
2433 | { | ||
2434 | if ($current==null) { | ||
2435 | $current = createModelElement(grammarAccess.getVLSDefinedTermRule()); | ||
2436 | } | ||
2437 | setWithLastConsumed( | ||
2438 | $current, | ||
2439 | "value", | ||
2440 | lv_value_5_0, | ||
2441 | "ca.mcgill.ecse.dslreasoner.VampireLanguage.SIGNED_RAT_ID"); | ||
2442 | } | ||
2443 | ) | ||
2444 | ) | ||
2445 | ) | ||
2446 | | | ||
2447 | ( | ||
2448 | ( | ||
2449 | { | ||
2450 | $current = forceCreateModelElement( | ||
2451 | grammarAccess.getVLSDefinedTermAccess().getVLSDoubleQuoteAction_3_0(), | ||
2452 | $current); | ||
2453 | } | ||
2454 | ) | ||
2455 | ( | ||
2456 | ( | ||
2457 | lv_value_7_0=RULE_DOUBLE_QUOTE | ||
2458 | { | ||
2459 | newLeafNode(lv_value_7_0, grammarAccess.getVLSDefinedTermAccess().getValueDOUBLE_QUOTETerminalRuleCall_3_1_0()); | ||
2460 | } | ||
2461 | { | ||
2462 | if ($current==null) { | ||
2463 | $current = createModelElement(grammarAccess.getVLSDefinedTermRule()); | ||
2464 | } | ||
2465 | setWithLastConsumed( | ||
2466 | $current, | ||
2467 | "value", | ||
2468 | lv_value_7_0, | ||
2469 | "ca.mcgill.ecse.dslreasoner.VampireLanguage.DOUBLE_QUOTE"); | 2766 | "ca.mcgill.ecse.dslreasoner.VampireLanguage.DOUBLE_QUOTE"); |
2470 | } | 2767 | } |
2471 | ) | 2768 | ) |
@@ -2494,21 +2791,9 @@ RULE_LITERAL : ('0'|'1'..'9' RULE_INT?); | |||
2494 | 2791 | ||
2495 | RULE_SIGNED_LITERAL : RULE_SIGN* RULE_LITERAL; | 2792 | RULE_SIGNED_LITERAL : RULE_SIGN* RULE_LITERAL; |
2496 | 2793 | ||
2497 | fragment RULE_UNSIGNED_REAL_FRAC_ID : RULE_LITERAL '.' RULE_INT; | 2794 | RULE_SINGLE_COMMENT : '%' ~(('\n'|'\r'))* ('\r'? '\n')?; |
2498 | |||
2499 | fragment RULE_UNSIGNED_REAL_EXP_ID : (RULE_LITERAL|RULE_UNSIGNED_REAL_FRAC_ID) 'Ee' RULE_SIGN* RULE_INT; | ||
2500 | |||
2501 | RULE_SIGNED_REAL_ID : RULE_SIGN* (RULE_UNSIGNED_REAL_FRAC_ID|RULE_UNSIGNED_REAL_EXP_ID); | ||
2502 | 2795 | ||
2503 | fragment RULE_UNSIGNED_RAT_ID : RULE_LITERAL '/' '1'..'9' RULE_INT?; | 2796 | RULE_ID : '^'? ('a'..'z'|'A'..'Z'|'_') ('a'..'z'|'A'..'Z'|'_'|'0'..'9')*; |
2504 | |||
2505 | RULE_SIGNED_RAT_ID : RULE_SIGN* RULE_UNSIGNED_RAT_ID; | ||
2506 | |||
2507 | fragment RULE_ID : ~(('\n'|'\r'))*; | ||
2508 | |||
2509 | fragment RULE_ANY_OTHER : RULE_ID; | ||
2510 | |||
2511 | RULE_SINGLE_COMMENT : RULE_ANY_OTHER; | ||
2512 | 2797 | ||
2513 | fragment RULE_INT : ('0'..'9')+; | 2798 | fragment RULE_INT : ('0'..'9')+; |
2514 | 2799 | ||
@@ -2519,3 +2804,5 @@ RULE_ML_COMMENT : '/*' ( options {greedy=false;} : . )*'*/'; | |||
2519 | RULE_SL_COMMENT : '//' ~(('\n'|'\r'))* ('\r'? '\n')?; | 2804 | RULE_SL_COMMENT : '//' ~(('\n'|'\r'))* ('\r'? '\n')?; |
2520 | 2805 | ||
2521 | RULE_WS : (' '|'\t'|'\r'|'\n')+; | 2806 | RULE_WS : (' '|'\t'|'\r'|'\n')+; |
2807 | |||
2808 | RULE_ANY_OTHER : .; | ||