diff options
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner')
8 files changed, 493 insertions, 0 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/GenerateVampireLanguage.mwe2 b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/GenerateVampireLanguage.mwe2 new file mode 100644 index 00000000..2fe82482 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/GenerateVampireLanguage.mwe2 | |||
@@ -0,0 +1,47 @@ | |||
1 | module ca.mcgill.ecse.dslreasoner.GenerateVampireLanguage | ||
2 | |||
3 | import org.eclipse.xtext.xtext.generator.* | ||
4 | import org.eclipse.xtext.xtext.generator.model.project.* | ||
5 | |||
6 | var rootPath = ".." | ||
7 | |||
8 | Workflow { | ||
9 | //TODO | ||
10 | component = XtextGenerator { | ||
11 | configuration = { | ||
12 | project = StandardProjectConfig { | ||
13 | baseName = "ca.mcgill.ecse.dslreasoner.vampire.language" | ||
14 | rootPath = rootPath | ||
15 | runtimeTest = { | ||
16 | enabled = true | ||
17 | } | ||
18 | eclipsePlugin = { | ||
19 | enabled = true | ||
20 | } | ||
21 | eclipsePluginTest = { | ||
22 | enabled = true | ||
23 | } | ||
24 | createEclipseMetaData = true | ||
25 | } | ||
26 | code = { | ||
27 | encoding = "UTF-8" | ||
28 | lineDelimiter = "\r\n" | ||
29 | fileHeader = "/*\n * generated by Xtext \${version}\n */" | ||
30 | } | ||
31 | } | ||
32 | language = StandardLanguage { | ||
33 | name = "ca.mcgill.ecse.dslreasoner.VampireLanguage" | ||
34 | fileExtensions = "tptp" | ||
35 | |||
36 | serializer = { | ||
37 | generateStub = false | ||
38 | } | ||
39 | validator = { | ||
40 | // composedCheck = "org.eclipse.xtext.validation.NamesAreUniqueValidator" | ||
41 | } | ||
42 | formatter={ | ||
43 | generateStub=true | ||
44 | } | ||
45 | } | ||
46 | } | ||
47 | } | ||
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..7d20da72 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/VampireLanguage.xtext | |||
@@ -0,0 +1,307 @@ | |||
1 | grammar ca.mcgill.ecse.dslreasoner.VampireLanguage with org.eclipse.xtext.common.Terminals hidden (WS) | ||
2 | |||
3 | generate 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 | |||
12 | VampireModel: | ||
13 | ( | ||
14 | includes += VLSInclude | | ||
15 | comments += VLSComment | | ||
16 | confirmations += VLSConfirmations| | ||
17 | formulas += VLSFofFormula | | ||
18 | tfformulas += VLSTffFormula | ||
19 | |||
20 | )* | ||
21 | ; | ||
22 | |||
23 | ////////////////////////////////// | ||
24 | // VLS terminals | ||
25 | ////////////////////////////////// | ||
26 | |||
27 | terminal ALPHA_NUMERIC: ( 'a'..'z' | 'A'..'Z' | '0'..'9' | '_'); | ||
28 | terminal UPPER_WORD_ID: ('A'..'Z') (ALPHA_NUMERIC)*; | ||
29 | terminal 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 "'" | ||
34 | terminal DOUBLE_QUOTE: '"' ( '\\' ('"'|'\\') | !('\\'|'"') )* '"';//from terminal STRING rule, positive about this | ||
35 | terminal SINGLE_QUOTE: "'" ( '\\' ("'"|'\\') | !('\\'|"'") )+ "'";//from terminal STRING rule, positive about this | ||
36 | |||
37 | terminal SIGN: ('+' | '-'); | ||
38 | |||
39 | terminal DOLLAR_ID: ('$') (LOWER_WORD_ID); | ||
40 | terminal DOUBLE_DOLLAR_ID: ('$$') (LOWER_WORD_ID); | ||
41 | |||
42 | terminal LITERAL: '0' | ('1'..'9') (INT)?; | ||
43 | terminal SIGNED_LITERAL: (SIGN)* (LITERAL); | ||
44 | |||
45 | terminal UNSIGNED_REAL_FRAC_ID: (LITERAL) ('.') (INT); | ||
46 | terminal UNSIGNED_REAL_EXP_ID: (LITERAL | UNSIGNED_REAL_FRAC_ID) ('Ee') (SIGN)* (INT) ; | ||
47 | terminal SIGNED_REAL_ID: (SIGN)* (UNSIGNED_REAL_FRAC_ID | UNSIGNED_REAL_EXP_ID); | ||
48 | |||
49 | terminal UNSIGNED_RAT_ID: (LITERAL) ('/') ('1'..'9') (INT)? ; | ||
50 | terminal SIGNED_RAT_ID: (SIGN)* (UNSIGNED_RAT_ID); | ||
51 | |||
52 | //Overwriting is necessary | ||
53 | terminal ID: (!('\n'|'\r'))* ; | ||
54 | terminal ANY_OTHER: ID; | ||
55 | terminal SINGLE_COMMENT: ANY_OTHER; | ||
56 | //terminal ID: ( !('('|')'|'\r'|'\n') )+ ; | ||
57 | |||
58 | |||
59 | ////////////////////////////////// | ||
60 | // VLS types | ||
61 | ////////////////////////////////// | ||
62 | |||
63 | // <includes> | ||
64 | VLSInclude: | ||
65 | 'include(' fileName = SINGLE_QUOTE ( ',[' names += VLSName (',' names += VLSName)* ']' )? | ||
66 | ; | ||
67 | |||
68 | VLSName: | ||
69 | name = (LOWER_WORD_ID | SINGLE_QUOTE | LITERAL | SIGNED_LITERAL) | ||
70 | ; | ||
71 | |||
72 | // <comments> | ||
73 | VLSComment: | ||
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 | VLSConfirmations: | ||
81 | VLSSatisfiable //| VLSFiniteModel// | VLSTrying | ||
82 | ; | ||
83 | |||
84 | VLSSatisfiable: | ||
85 | {VLSSatisfiable} 'Satisfiable!' | ||
86 | ; | ||
87 | |||
88 | //VLSTrying: | ||
89 | // 'TRYING' '[' name = LITERAL ']' | ||
90 | //; | ||
91 | // | ||
92 | //VLSFiniteModel: | ||
93 | // {VLSFiniteModel} 'Finite' 'Model' 'Found!' | ||
94 | //; | ||
95 | |||
96 | // <FOF formulas> | ||
97 | VLSFofFormula: | ||
98 | 'fof' '(' name = (LOWER_WORD_ID | SIGNED_LITERAL | SINGLE_QUOTE) ',' fofRole = VLSRole ',' fofFormula = VLSTerm (',' annotations = VLSAnnotation)? ')' '.' | ||
99 | ; | ||
100 | |||
101 | |||
102 | VLSTffFormula: | ||
103 | 'tff' '(' name = (LOWER_WORD_ID | SIGNED_LITERAL | SINGLE_QUOTE) ',' fofRole = VLSRole ',' fofFormula = VLSTerm (',' annotations = VLSAnnotation)? ')' '.' | ||
104 | ; | ||
105 | |||
106 | |||
107 | /* | ||
108 | //NAME | ||
109 | VLSName: | ||
110 | //(atomic_Word = Atomic_Word | integer = Integer | single_quote_word = Single_Quote_Word) | ||
111 | name = (LOWER_WORD_ID | SIGNED_INT_ID | SINGLE_QUOTE) | ||
112 | ; | ||
113 | */ | ||
114 | //<ROLE> | ||
115 | VLSRole: | ||
116 | "axiom" | "conjecture" | "hypothesis" | "definition" | "assumption" | "lemma" | ||
117 | | "theorem" | "corollary" | "negated_conjecture" | "plain" | "type" | | ||
118 | "fi_domain" | "fi_functors" | "fi_predicates" | "unknown" | ||
119 | ; | ||
120 | |||
121 | //VLSRole: | ||
122 | // VLSAxiom | VLSConjecture | VLSHypothesis | VLSDefinition | | ||
123 | // VLSAssumption | VLSLemma | VLSTheorem | VLSCorollary | VLSNegated_Conjecture | | ||
124 | // VLSPlain | VLSType |VLSFi_Domain | VLSFi_Functors | VLSFi_Predicates | VLSUnknown | ||
125 | //; | ||
126 | // | ||
127 | //VLSAxiom: | ||
128 | // "axiom" | ||
129 | //; | ||
130 | // | ||
131 | //VLSConjecture: | ||
132 | // "conjecture" | ||
133 | //; | ||
134 | // | ||
135 | //VLSHypothesis: | ||
136 | // "hypothesis" | ||
137 | //; | ||
138 | // | ||
139 | //VLSDefinition: | ||
140 | // "definition" | ||
141 | //; | ||
142 | // | ||
143 | //VLSAssumption: | ||
144 | // "assumption" | ||
145 | //; | ||
146 | // | ||
147 | //VLSLemma: | ||
148 | // "lemma" | ||
149 | //; | ||
150 | // | ||
151 | //VLSTheorem: | ||
152 | // "theorem" | ||
153 | //; | ||
154 | // | ||
155 | //VLSCorollary: | ||
156 | // "corollary" | ||
157 | //; | ||
158 | // | ||
159 | //VLSNegated_Conjecture: | ||
160 | // "negated_conjecture" | ||
161 | //; | ||
162 | // | ||
163 | //VLSPlain: | ||
164 | // "plain" | ||
165 | //; | ||
166 | // | ||
167 | //VLSType: | ||
168 | // "type" | ||
169 | //; | ||
170 | // | ||
171 | //VLSFi_Domain: | ||
172 | // "fi_domain" | ||
173 | //; | ||
174 | // | ||
175 | //VLSFi_Functors: | ||
176 | // "fi_functors" | ||
177 | //; | ||
178 | // | ||
179 | //VLSFi_Predicates: | ||
180 | // "fi_predicates" | ||
181 | //; | ||
182 | // | ||
183 | //VLSUnknown: | ||
184 | // "unknown" | ||
185 | //; | ||
186 | |||
187 | // <ANNOTATION> | ||
188 | // Not at all based on the website. based on what we think the output will be like | ||
189 | VLSAnnotation: | ||
190 | ('[')? (name = (LOWER_WORD_ID | SINGLE_QUOTE | VLSRole))? ( '(' followup = VLSAnnotationTerms ')' )? (']')? | ||
191 | ; | ||
192 | |||
193 | VLSAnnotationTerms returns VLSAnnotation: | ||
194 | terms += VLSAnnotation (',' terms += VLSAnnotation )* | ||
195 | ; | ||
196 | |||
197 | ////////////////////////////////// | ||
198 | // VLS Terms | ||
199 | ////////////////////////////////// | ||
200 | |||
201 | VLSTerm: | ||
202 | //( VLSLogic | VLSSequent) | ||
203 | VLSBinary | ||
204 | ; | ||
205 | //* | ||
206 | //VLSBinaryFormula | ||
207 | VLSBinary returns VLSTerm: | ||
208 | VLSUnitaryFormula | ||
209 | ( | ||
210 | (({VLSEquivalent.left = current} "<=>" | | ||
211 | {VLSImplies.left = current} "=>" | | ||
212 | {VLSRevImplies.left = current} "<=" | | ||
213 | {VLSXnor.left = current} "<~>" | | ||
214 | {VLSNor.left = current} "~|" | | ||
215 | {VLSNand.left = current} "~&") right = VLSUnitaryFormula) | ||
216 | | | ||
217 | ({VLSAnd.left = current} '&' right = VLSUnitaryFormula)+ | ||
218 | | | ||
219 | ({VLSOr.left = current} '|' right = VLSUnitaryFormula)+ | ||
220 | )? | ||
221 | ; | ||
222 | |||
223 | //VLSUnitaryFormula | ||
224 | VLSUnitaryFormula returns VLSTerm: | ||
225 | VLSUniversalQuantifier | VLSExistentialQuantifier | VLSUnaryNegation | VLSUnaryInfix | ||
226 | //| VLSEquality | ||
227 | | '(' VLSTerm ')' | ||
228 | ; | ||
229 | |||
230 | VLSUniversalQuantifier returns VLSTerm: | ||
231 | {VLSUniversalQuantifier} (("!") '[' variables += VLSVariable (',' variables += VLSVariable)* ']' ':') operand = VLSUnitaryFormula | ||
232 | ; | ||
233 | |||
234 | VLSExistentialQuantifier returns VLSTerm: | ||
235 | {VLSExistentialQuantifier} (("?") '[' variables += VLSVariable (',' variables += VLSVariable)* ']' ':') operand = VLSUnitaryFormula | ||
236 | ; | ||
237 | |||
238 | VLSUnaryNegation returns VLSTerm: | ||
239 | {VLSUnaryNegation} ('~') operand = VLSUnitaryFormula | ||
240 | ; | ||
241 | |||
242 | VLSUnaryInfix returns VLSTerm: | ||
243 | VLSAtomic (({VLSInequality.left = current} "!=" | | ||
244 | {VLSEquality.left = current} "=" | | ||
245 | {VLSAssignment.left = current} ":=") | ||
246 | right = VLSAtomic)? | ||
247 | ; | ||
248 | |||
249 | //NOT SUREEEE | ||
250 | //VLSEquality returns VLSTerm: | ||
251 | // VLSFofTerm ({VLSEquality.left = current} "=" right = VLSFofTerm)? | ||
252 | // | ||
253 | //; | ||
254 | |||
255 | /* | ||
256 | enum VLSDefinedFunctor: | ||
257 | UMINUS='$uminus' | SUM='$sum' | DIFFERENCE='$difference' | PRODUCT='$product' | QUOTIENT='$quotient' | | ||
258 | QUOTIENT_E='$quotient_e' | QUOTIENT_T='$quotient_t' | QUOTIENT_F='$quotient_f' | REMAINDER_E='$remainder_e' | | ||
259 | REMAINDER_T='$remainder_t' | REMAINDER_F='$remainder_f' | FLOOR='$floor' | CEILING='$ceiling' | | ||
260 | TRUNCATE='$truncate' | ROUND='$round' | TO_INT='$to_int' | TO_RAT='$to_rat' | TO_REAL='$to_real' | ||
261 | ; | ||
262 | */ | ||
263 | |||
264 | VLSAtomic returns VLSTerm: | ||
265 | VLSAtomicConstant | VLSAtomicFunction | VLSVariable | ||
266 | | VLSDefinedTerm //temporary solution. this is only valid for equality, not for != or := | ||
267 | //| VLSEquality | ||
268 | ; | ||
269 | |||
270 | VLSAtomicConstant returns VLSTerm: | ||
271 | //{VLSConstant} name = VLSConstantDeclaration | | ||
272 | {VLSConstant} name = (LOWER_WORD_ID | SINGLE_QUOTE | DOLLAR_ID | DOUBLE_DOLLAR_ID | VLSRole) | | ||
273 | {VLSTrue} '$true' | | ||
274 | {VLSFalse} '$false' | ||
275 | ; | ||
276 | |||
277 | VLSAtomicFunction returns VLSTerm: | ||
278 | //? on next line causes warning | ||
279 | //TODO might need replace DOLLAR_ID with enum rule | ||
280 | //{VLSFunction} name = VLSConstantDeclaration ( '(' terms += VLSFofTerm (',' terms += VLSFofTerm)* ')' ) | | ||
281 | {VLSFunction} constant = (LOWER_WORD_ID | SINGLE_QUOTE | DOLLAR_ID | DOUBLE_DOLLAR_ID | VLSRole ) ( '(' terms += VLSFofTerm (',' terms += VLSFofTerm)* ')') | | ||
282 | {VLSLess} name = '$less' '(' terms += VLSFofTerm ',' terms += VLSFofTerm ')' | ||
283 | ; | ||
284 | |||
285 | VLSVariable : | ||
286 | |||
287 | name = UPPER_WORD_ID | ||
288 | ; | ||
289 | |||
290 | VLSFofTerm returns VLSTerm: | ||
291 | //(VLSVariable | VLSFunction | VLSTffConditional | VLSTffLet | VLSTffTuple) | ||
292 | (VLSVariable | VLSFunctionAsTerm | VLSDefinedTerm ) | ||
293 | ; | ||
294 | |||
295 | VLSFunctionAsTerm: | ||
296 | //? on next line causes warning | ||
297 | //TODO might need replace DOLLAR_ID with enum rule | ||
298 | functor = (LOWER_WORD_ID | SINGLE_QUOTE | DOLLAR_ID | DOUBLE_DOLLAR_ID ) ( '(' terms += VLSFofTerm (',' terms += VLSFofTerm)* ')')? | ||
299 | ; | ||
300 | |||
301 | VLSDefinedTerm: | ||
302 | {VLSInt} value = SIGNED_LITERAL | | ||
303 | {VLSReal} value = SIGNED_REAL_ID | | ||
304 | {VLSRational} value = SIGNED_RAT_ID | | ||
305 | {VLSDoubleQuote} value = DOUBLE_QUOTE | ||
306 | ; | ||
307 | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/VampireLanguageRuntimeModule.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/VampireLanguageRuntimeModule.xtend new file mode 100644 index 00000000..162df1e2 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/VampireLanguageRuntimeModule.xtend | |||
@@ -0,0 +1,11 @@ | |||
1 | /* | ||
2 | * generated by Xtext 2.12.0 | ||
3 | */ | ||
4 | package ca.mcgill.ecse.dslreasoner | ||
5 | |||
6 | |||
7 | /** | ||
8 | * Use this class to register components to be used at runtime / without the Equinox extension registry. | ||
9 | */ | ||
10 | class VampireLanguageRuntimeModule extends AbstractVampireLanguageRuntimeModule { | ||
11 | } | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/VampireLanguageStandaloneSetup.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/VampireLanguageStandaloneSetup.xtend new file mode 100644 index 00000000..38a05c51 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/VampireLanguageStandaloneSetup.xtend | |||
@@ -0,0 +1,15 @@ | |||
1 | /* | ||
2 | * generated by Xtext 2.12.0 | ||
3 | */ | ||
4 | package ca.mcgill.ecse.dslreasoner | ||
5 | |||
6 | |||
7 | /** | ||
8 | * Initialization support for running Xtext languages without Equinox extension registry. | ||
9 | */ | ||
10 | class VampireLanguageStandaloneSetup extends VampireLanguageStandaloneSetupGenerated { | ||
11 | |||
12 | def static void doSetup() { | ||
13 | new VampireLanguageStandaloneSetup().createInjectorAndDoEMFRegistration() | ||
14 | } | ||
15 | } | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/formatting2/VampireLanguageFormatter.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/formatting2/VampireLanguageFormatter.xtend new file mode 100644 index 00000000..f943daad --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/formatting2/VampireLanguageFormatter.xtend | |||
@@ -0,0 +1,48 @@ | |||
1 | /* | ||
2 | * generated by Xtext 2.12.0 | ||
3 | */ | ||
4 | package ca.mcgill.ecse.dslreasoner.formatting2 | ||
5 | |||
6 | import ca.mcgill.ecse.dslreasoner.services.VampireLanguageGrammarAccess | ||
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSComment | ||
8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula | ||
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSInclude | ||
10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSName | ||
11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel | ||
12 | import com.google.inject.Inject | ||
13 | import org.eclipse.xtext.formatting2.AbstractFormatter2 | ||
14 | import org.eclipse.xtext.formatting2.IFormattableDocument | ||
15 | |||
16 | class VampireLanguageFormatter extends AbstractFormatter2 { | ||
17 | |||
18 | @Inject extension VampireLanguageGrammarAccess | ||
19 | |||
20 | def dispatch void format(VampireModel vampireModel, extension IFormattableDocument document) { | ||
21 | // TODO: format HiddenRegions around keywords, attributes, cross references, etc. | ||
22 | for (VLSInclude vLSInclude : vampireModel.getIncludes()) { | ||
23 | vLSInclude.format; | ||
24 | } | ||
25 | for (VLSComment vLSComment : vampireModel.getComments()) { | ||
26 | vLSComment.format; | ||
27 | } | ||
28 | for (VLSFofFormula vLSFofFormula : vampireModel.getFormulas()) { | ||
29 | vLSFofFormula.format; | ||
30 | } | ||
31 | } | ||
32 | |||
33 | def dispatch void format(VLSInclude vLSInclude, extension IFormattableDocument document) { | ||
34 | // TODO: format HiddenRegions around keywords, attributes, cross references, etc. | ||
35 | for (VLSName vLSName : vLSInclude.getNames()) { | ||
36 | vLSName.format; | ||
37 | } | ||
38 | } | ||
39 | |||
40 | def dispatch void format(VLSFofFormula formula, extension IFormattableDocument document){ | ||
41 | formula.append[newLine] | ||
42 | } | ||
43 | |||
44 | def dispatch void format(VLSComment comment, extension IFormattableDocument document){ | ||
45 | comment.append[newLine] | ||
46 | } | ||
47 | // TODO: implement for VLSFofFormula, VLSAnnotation, VLSAnd, VLSOr, VLSUniversalQuantifier, VLSExistentialQuantifier, VLSUnaryNegation, VLSFunction, VLSLess, VLSFunctionFof, VLSEquivalent, VLSImplies, VLSRevImplies, VLSXnor, VLSNor, VLSNand, VLSInequality, VLSEquality, VLSAssignment | ||
48 | } | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/generator/VampireLanguageGenerator.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/generator/VampireLanguageGenerator.xtend new file mode 100644 index 00000000..f099486a --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/generator/VampireLanguageGenerator.xtend | |||
@@ -0,0 +1,25 @@ | |||
1 | /* | ||
2 | * generated by Xtext 2.12.0 | ||
3 | */ | ||
4 | package ca.mcgill.ecse.dslreasoner.generator | ||
5 | |||
6 | import org.eclipse.emf.ecore.resource.Resource | ||
7 | import org.eclipse.xtext.generator.AbstractGenerator | ||
8 | import org.eclipse.xtext.generator.IFileSystemAccess2 | ||
9 | import org.eclipse.xtext.generator.IGeneratorContext | ||
10 | |||
11 | /** | ||
12 | * Generates code from your model files on save. | ||
13 | * | ||
14 | * See https://www.eclipse.org/Xtext/documentation/303_runtime_concepts.html#code-generation | ||
15 | */ | ||
16 | class VampireLanguageGenerator extends AbstractGenerator { | ||
17 | |||
18 | override void doGenerate(Resource resource, IFileSystemAccess2 fsa, IGeneratorContext context) { | ||
19 | // fsa.generateFile('greetings.txt', 'People to greet: ' + | ||
20 | // resource.allContents | ||
21 | // .filter(Greeting) | ||
22 | // .map[name] | ||
23 | // .join(', ')) | ||
24 | } | ||
25 | } | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/scoping/VampireLanguageScopeProvider.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/scoping/VampireLanguageScopeProvider.xtend new file mode 100644 index 00000000..fb967eee --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/scoping/VampireLanguageScopeProvider.xtend | |||
@@ -0,0 +1,15 @@ | |||
1 | /* | ||
2 | * generated by Xtext 2.12.0 | ||
3 | */ | ||
4 | package ca.mcgill.ecse.dslreasoner.scoping | ||
5 | |||
6 | |||
7 | /** | ||
8 | * This class contains custom scoping description. | ||
9 | * | ||
10 | * See https://www.eclipse.org/Xtext/documentation/303_runtime_concepts.html#scoping | ||
11 | * on how and when to use it. | ||
12 | */ | ||
13 | class VampireLanguageScopeProvider extends AbstractVampireLanguageScopeProvider { | ||
14 | //TODO | ||
15 | } | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/validation/VampireLanguageValidator.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/validation/VampireLanguageValidator.xtend new file mode 100644 index 00000000..8d7a9f76 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/validation/VampireLanguageValidator.xtend | |||
@@ -0,0 +1,25 @@ | |||
1 | /* | ||
2 | * generated by Xtext 2.12.0 | ||
3 | */ | ||
4 | package ca.mcgill.ecse.dslreasoner.validation | ||
5 | |||
6 | |||
7 | /** | ||
8 | * This class contains custom validation rules. | ||
9 | * | ||
10 | * See https://www.eclipse.org/Xtext/documentation/303_runtime_concepts.html#validation | ||
11 | */ | ||
12 | class VampireLanguageValidator extends AbstractVampireLanguageValidator { | ||
13 | |||
14 | // public static val INVALID_NAME = 'invalidName' | ||
15 | // | ||
16 | // @Check | ||
17 | // def checkGreetingStartsWithCapital(Greeting greeting) { | ||
18 | // if (!Character.isUpperCase(greeting.name.charAt(0))) { | ||
19 | // warning('Name should start with a capital', | ||
20 | // VampireLanguagePackage.Literals.GREETING__NAME, | ||
21 | // INVALID_NAME) | ||
22 | // } | ||
23 | // } | ||
24 | |||
25 | } | ||