aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/VampireLanguage.xtext
diff options
context:
space:
mode:
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/VampireLanguage.xtext')
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/VampireLanguage.xtext278
1 files changed, 278 insertions, 0 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/VampireLanguage.xtext b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/VampireLanguage.xtext
new file mode 100644
index 00000000..daa15ca1
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/VampireLanguage.xtext
@@ -0,0 +1,278 @@
1grammar ca.mcgill.ecse.dslreasoner.VampireLanguage with org.eclipse.xtext.common.Terminals hidden (WS)
2
3generate vampireLanguage "http://www.mcgill.ca/ecse/dslreasoner/VampireLanguage"
4
5//@@@@@@@@@@@
6//2 things TODO:
7//1. fix anotations (ln77)
8//2. can only use declared variables in formula (ln 158)
9
10//@@@@@@@@@@@
11
12VampireModel:
13 // TODO ensures there is always exactly 1 conjecture
14 (
15 includes += VLSInclude |
16 comments += VLSComment |
17 formulas += VLSFofFormula
18 )*
19;
20
21
22
23//////////////////////////////////
24// VLS terminals
25//////////////////////////////////
26
27terminal ALPHA_NUMERIC: ( 'a'..'z' | 'A'..'Z' | '0'..'9' | '_');
28terminal UPPER_WORD_ID: ('A'..'Z') (ALPHA_NUMERIC)*;
29terminal LOWER_WORD_ID: ('a'..'z') (ALPHA_NUMERIC)*;
30
31
32//TODO MIGHT NEED TO IMPLEMENT SOME WAY TO ONLY CONSIDER WHAT IS INSIDE QUOTES AS NAME
33//incorporate quotes in the line of calling. ex. "'" name=SINGLEQUOTE "'"
34terminal DOUBLE_QUOTE: '"' ( '\\' ('"'|'\\') | !('\\'|'"') )* '"';//from terminal STRING rule, positive about this
35terminal SINGLE_QUOTE: "'" ( '\\' ("'"|'\\') | !('\\'|"'") )+ "'";//from terminal STRING rule, positive about this
36
37terminal SIGN: ('+' | '-');
38
39terminal DOLLAR_ID: ('$') (LOWER_WORD_ID);
40terminal DOUBLE_DOLLAR_ID: ('$$') (LOWER_WORD_ID);
41
42terminal LITERAL: '0' | ('1'..'9') (INT)?;
43terminal SIGNED_LITERAL: (SIGN)* (LITERAL);
44
45terminal UNSIGNED_REAL_FRAC_ID: (LITERAL) ('.') (INT);
46terminal UNSIGNED_REAL_EXP_ID: (LITERAL | UNSIGNED_REAL_FRAC_ID) ('Ee') (SIGN)* (INT) ;
47terminal SIGNED_REAL_ID: (SIGN)* (UNSIGNED_REAL_FRAC_ID | UNSIGNED_REAL_EXP_ID);
48
49terminal UNSIGNED_RAT_ID: (LITERAL) ('/') ('1'..'9') (INT)? ;
50terminal SIGNED_RAT_ID: (SIGN)* (UNSIGNED_RAT_ID);
51
52//Overwriting is necessary
53terminal ANY_OTHER: '%' (!('\n'|'\r'))* ('\r');
54terminal SINGLE_COMMENT: ANY_OTHER;
55//terminal ID: ( !('('|')'|'\r'|'\n') )+ ;
56
57
58
59//////////////////////////////////
60// VLS types
61//////////////////////////////////
62
63// <includes>
64VLSInclude:
65 'include(' fileName = SINGLE_QUOTE ( ',[' names += VLSName (',' names += VLSName)* ']' )?
66;
67
68VLSName:
69 name = (LOWER_WORD_ID | SINGLE_QUOTE | LITERAL | SIGNED_LITERAL)
70;
71
72// <comments>
73VLSComment:
74 comment = SINGLE_COMMENT
75 //need to add a new line at the end of the file for the case where the last line is a comment
76;
77
78//VLSConstantDeclaration: name = (LOWER_WORD_ID | SINGLE_QUOTE | DOLLAR_ID | DOUBLE_DOLLAR_ID );
79
80// <FOF formulas>
81VLSFofFormula:
82 'fof' '(' name = (LOWER_WORD_ID | SIGNED_LITERAL | SINGLE_QUOTE) ',' fofRole = VLSRole ',' fofFormula = VLSTerm (',' annotations = VLSAnnotation)? ')' '.'
83;
84/*
85//NAME
86VLSName:
87 //(atomic_Word = Atomic_Word | integer = Integer | single_quote_word = Single_Quote_Word)
88 name = (LOWER_WORD_ID | SIGNED_INT_ID | SINGLE_QUOTE)
89;
90*/
91//<ROLE>
92VLSRole:
93 VLSAxiom | VLSConjecture | VLSHypothesis | VLSDefinition |
94 VLSAssumption | VLSLemma | VLSTheorem | VLSCorollary | VLSNegated_Conjecture |
95 VLSPlain | VLSType |VLSFi_Domain | VLSFi_Functors | VLSFi_Predicates | VLSUnknown
96;
97
98VLSAxiom:
99 "axiom"
100;
101
102VLSConjecture:
103 "conjecture"
104;
105
106VLSHypothesis:
107 "hypothesis"
108;
109
110VLSDefinition:
111 "definition"
112;
113
114VLSAssumption:
115 "assumption"
116;
117
118VLSLemma:
119 "lemma"
120;
121
122VLSTheorem:
123 "theorem"
124;
125
126VLSCorollary:
127 "corollary"
128;
129
130VLSNegated_Conjecture:
131 "negated_conjecture"
132;
133
134VLSPlain:
135 "plain"
136;
137
138VLSType:
139 "type"
140;
141
142VLSFi_Domain:
143 "fi_domain"
144;
145
146VLSFi_Functors:
147 "fi_functors"
148;
149
150VLSFi_Predicates:
151 "fi_predicates"
152;
153
154VLSUnknown:
155 "unknown"
156;
157
158// <ANNOTATION>
159// Not at all based on the website. based on what we think the output will be like
160VLSAnnotation:
161 ('[')? (name = (LOWER_WORD_ID | SINGLE_QUOTE | VLSRole))? ( '(' followup = VLSAnnotationTerms ')' )? (']')?
162;
163
164VLSAnnotationTerms returns VLSAnnotation:
165 terms += VLSAnnotation (',' terms += VLSAnnotation )*
166;
167
168//////////////////////////////////
169// VLS Terms
170//////////////////////////////////
171
172VLSTerm:
173 //( VLSLogic | VLSSequent)
174 VLSBinary
175;
176//*
177//VLSBinaryFormula
178VLSBinary returns VLSTerm:
179 VLSUnitaryFormula
180 (
181 (({VLSEquivalent.left = current} "<=>" |
182 {VLSImplies.left = current} "=>" |
183 {VLSRevImplies.left = current} "<=" |
184 {VLSXnor.left = current} "<~>" |
185 {VLSNor.left = current} "~|" |
186 {VLSNand.left = current} "~&") right = VLSUnitaryFormula)
187 |
188 ({VLSAnd.left = current} '&' right = VLSUnitaryFormula)+
189 |
190 ({VLSOr.left = current} '|' right = VLSUnitaryFormula)+
191 )?
192;
193
194//VLSUnitaryFormula
195VLSUnitaryFormula returns VLSTerm:
196 VLSUniversalQuantifier | VLSExistentialQuantifier | VLSUnaryNegation | VLSUnaryInfix
197 //| VLSEquality
198 | '(' VLSTerm ')'
199;
200
201VLSUniversalQuantifier returns VLSTerm:
202 {VLSUniversalQuantifier} (("!") '[' variables += VLSVariable (',' variables += VLSVariable)* ']' ':') operand = VLSUnitaryFormula
203;
204
205VLSExistentialQuantifier returns VLSTerm:
206 {VLSExistentialQuantifier} (("?") '[' variables += VLSVariable (',' variables += VLSVariable)* ']' ':') operand = VLSUnitaryFormula
207;
208
209VLSUnaryNegation returns VLSTerm:
210 {VLSUnaryNegation} ('~') operand = VLSUnitaryFormula
211;
212
213VLSUnaryInfix returns VLSTerm:
214 VLSAtomic (({VLSInequality.left = current} "!=" |
215 {VLSEquality.left = current} "=" |
216 {VLSAssignment.left = current} ":=")
217 right = VLSAtomic)?
218;
219
220//NOT SUREEEE
221//VLSEquality returns VLSTerm:
222// VLSFofTerm ({VLSEquality.left = current} "=" right = VLSFofTerm)?
223//
224//;
225
226/*
227enum VLSDefinedFunctor:
228 UMINUS='$uminus' | SUM='$sum' | DIFFERENCE='$difference' | PRODUCT='$product' | QUOTIENT='$quotient' |
229 QUOTIENT_E='$quotient_e' | QUOTIENT_T='$quotient_t' | QUOTIENT_F='$quotient_f' | REMAINDER_E='$remainder_e' |
230 REMAINDER_T='$remainder_t' | REMAINDER_F='$remainder_f' | FLOOR='$floor' | CEILING='$ceiling' |
231 TRUNCATE='$truncate' | ROUND='$round' | TO_INT='$to_int' | TO_RAT='$to_rat' | TO_REAL='$to_real'
232 ;
233*/
234
235VLSAtomic returns VLSTerm:
236 VLSAtomicConstant | VLSAtomicFunction | VLSVariable
237 | VLSDefinedTerm //temporary solution. this is only valid for equality, not for != or :=
238 //| VLSEquality
239;
240
241VLSAtomicConstant returns VLSTerm:
242 //{VLSConstant} name = VLSConstantDeclaration |
243 {VLSConstant} name = (LOWER_WORD_ID | SINGLE_QUOTE | DOLLAR_ID | DOUBLE_DOLLAR_ID | VLSRole) |
244 {VLSTrue} '$true' |
245 {VLSFalse} '$false'
246;
247
248VLSAtomicFunction returns VLSTerm:
249 //? on next line causes warning
250 //TODO might need replace DOLLAR_ID with enum rule
251 //{VLSFunction} name = VLSConstantDeclaration ( '(' terms += VLSFofTerm (',' terms += VLSFofTerm)* ')' ) |
252 {VLSFunction} constant = (LOWER_WORD_ID | SINGLE_QUOTE | DOLLAR_ID | DOUBLE_DOLLAR_ID | VLSRole ) ( '(' terms += VLSFofTerm (',' terms += VLSFofTerm)* ')') |
253 {VLSLess} name = '$less' '(' terms += VLSFofTerm ',' terms += VLSFofTerm ')'
254;
255
256VLSVariable :
257
258 name = UPPER_WORD_ID
259;
260
261VLSFofTerm returns VLSTerm:
262 //(VLSVariable | VLSFunction | VLSTffConditional | VLSTffLet | VLSTffTuple)
263 (VLSVariable | VLSFunctionFof | VLSDefinedTerm )
264;
265
266VLSFunctionFof:
267 //? on next line causes warning
268 //TODO might need replace DOLLAR_ID with enum rule
269 functor = (LOWER_WORD_ID | SINGLE_QUOTE | DOLLAR_ID | DOUBLE_DOLLAR_ID ) ( '(' terms += VLSFofTerm (',' terms += VLSFofTerm)* ')')?
270;
271
272VLSDefinedTerm:
273 {VLSInt} value = SIGNED_LITERAL |
274 {VLSReal} value = SIGNED_REAL_ID |
275 {VLSRational} value = SIGNED_RAT_ID |
276 {VLSDoubleQuote} value = DOUBLE_QUOTE
277;
278
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-06-17 17:31:26 +0000