aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse
diff options
context:
space:
mode:
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse')
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/GenerateVampireLanguage.mwe247
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/VampireLanguage.xtext307
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/VampireLanguageRuntimeModule.xtend11
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/VampireLanguageStandaloneSetup.xtend15
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/formatting2/VampireLanguageFormatter.xtend48
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/generator/VampireLanguageGenerator.xtend25
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/scoping/VampireLanguageScopeProvider.xtend15
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/validation/VampireLanguageValidator.xtend25
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 @@
1module ca.mcgill.ecse.dslreasoner.GenerateVampireLanguage
2
3import org.eclipse.xtext.xtext.generator.*
4import org.eclipse.xtext.xtext.generator.model.project.*
5
6var rootPath = ".."
7
8Workflow {
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 @@
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 (
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
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 ID: (!('\n'|'\r'))* ;
54terminal ANY_OTHER: ID;
55terminal SINGLE_COMMENT: ANY_OTHER;
56//terminal ID: ( !('('|')'|'\r'|'\n') )+ ;
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
80VLSConfirmations:
81 VLSSatisfiable //| VLSFiniteModel// | VLSTrying
82;
83
84VLSSatisfiable:
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>
97VLSFofFormula:
98 'fof' '(' name = (LOWER_WORD_ID | SIGNED_LITERAL | SINGLE_QUOTE) ',' fofRole = VLSRole ',' fofFormula = VLSTerm (',' annotations = VLSAnnotation)? ')' '.'
99;
100
101
102VLSTffFormula:
103 'tff' '(' name = (LOWER_WORD_ID | SIGNED_LITERAL | SINGLE_QUOTE) ',' fofRole = VLSRole ',' fofFormula = VLSTerm (',' annotations = VLSAnnotation)? ')' '.'
104;
105
106
107/*
108//NAME
109VLSName:
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>
115VLSRole:
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
189VLSAnnotation:
190 ('[')? (name = (LOWER_WORD_ID | SINGLE_QUOTE | VLSRole))? ( '(' followup = VLSAnnotationTerms ')' )? (']')?
191;
192
193VLSAnnotationTerms returns VLSAnnotation:
194 terms += VLSAnnotation (',' terms += VLSAnnotation )*
195;
196
197//////////////////////////////////
198// VLS Terms
199//////////////////////////////////
200
201VLSTerm:
202 //( VLSLogic | VLSSequent)
203 VLSBinary
204;
205//*
206//VLSBinaryFormula
207VLSBinary 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
224VLSUnitaryFormula returns VLSTerm:
225 VLSUniversalQuantifier | VLSExistentialQuantifier | VLSUnaryNegation | VLSUnaryInfix
226 //| VLSEquality
227 | '(' VLSTerm ')'
228;
229
230VLSUniversalQuantifier returns VLSTerm:
231 {VLSUniversalQuantifier} (("!") '[' variables += VLSVariable (',' variables += VLSVariable)* ']' ':') operand = VLSUnitaryFormula
232;
233
234VLSExistentialQuantifier returns VLSTerm:
235 {VLSExistentialQuantifier} (("?") '[' variables += VLSVariable (',' variables += VLSVariable)* ']' ':') operand = VLSUnitaryFormula
236;
237
238VLSUnaryNegation returns VLSTerm:
239 {VLSUnaryNegation} ('~') operand = VLSUnitaryFormula
240;
241
242VLSUnaryInfix 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/*
256enum 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
264VLSAtomic returns VLSTerm:
265 VLSAtomicConstant | VLSAtomicFunction | VLSVariable
266 | VLSDefinedTerm //temporary solution. this is only valid for equality, not for != or :=
267 //| VLSEquality
268;
269
270VLSAtomicConstant 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
277VLSAtomicFunction 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
285VLSVariable :
286
287 name = UPPER_WORD_ID
288;
289
290VLSFofTerm returns VLSTerm:
291 //(VLSVariable | VLSFunction | VLSTffConditional | VLSTffLet | VLSTffTuple)
292 (VLSVariable | VLSFunctionAsTerm | VLSDefinedTerm )
293;
294
295VLSFunctionAsTerm:
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
301VLSDefinedTerm:
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 */
4package 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 */
10class 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 */
4package ca.mcgill.ecse.dslreasoner
5
6
7/**
8 * Initialization support for running Xtext languages without Equinox extension registry.
9 */
10class 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 */
4package ca.mcgill.ecse.dslreasoner.formatting2
5
6import ca.mcgill.ecse.dslreasoner.services.VampireLanguageGrammarAccess
7import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSComment
8import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula
9import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSInclude
10import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSName
11import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel
12import com.google.inject.Inject
13import org.eclipse.xtext.formatting2.AbstractFormatter2
14import org.eclipse.xtext.formatting2.IFormattableDocument
15
16class 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 */
4package ca.mcgill.ecse.dslreasoner.generator
5
6import org.eclipse.emf.ecore.resource.Resource
7import org.eclipse.xtext.generator.AbstractGenerator
8import org.eclipse.xtext.generator.IFileSystemAccess2
9import 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 */
16class 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 */
4package 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 */
13class 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 */
4package 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 */
12class 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}
generated by cgit v1.2.3-70-g09d2 (git 2.46.0) at 2024-08-19 17:31:48 +0000