diff options
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner')
4 files changed, 58 insertions, 4 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 index 903ac83b..2fe82482 100644 --- 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 | |||
@@ -6,7 +6,7 @@ import org.eclipse.xtext.xtext.generator.model.project.* | |||
6 | var rootPath = ".." | 6 | var rootPath = ".." |
7 | 7 | ||
8 | Workflow { | 8 | Workflow { |
9 | 9 | //TODO | |
10 | component = XtextGenerator { | 10 | component = XtextGenerator { |
11 | configuration = { | 11 | configuration = { |
12 | project = StandardProjectConfig { | 12 | project = StandardProjectConfig { |
@@ -39,6 +39,9 @@ Workflow { | |||
39 | validator = { | 39 | validator = { |
40 | // composedCheck = "org.eclipse.xtext.validation.NamesAreUniqueValidator" | 40 | // composedCheck = "org.eclipse.xtext.validation.NamesAreUniqueValidator" |
41 | } | 41 | } |
42 | formatter={ | ||
43 | generateStub=true | ||
44 | } | ||
42 | } | 45 | } |
43 | } | 46 | } |
44 | } | 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 index daa15ca1..d5b40ed9 100644 --- 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 | |||
@@ -50,12 +50,15 @@ terminal UNSIGNED_RAT_ID: (LITERAL) ('/') ('1'..'9') (INT)? ; | |||
50 | terminal SIGNED_RAT_ID: (SIGN)* (UNSIGNED_RAT_ID); | 50 | terminal SIGNED_RAT_ID: (SIGN)* (UNSIGNED_RAT_ID); |
51 | 51 | ||
52 | //Overwriting is necessary | 52 | //Overwriting is necessary |
53 | terminal ANY_OTHER: '%' (!('\n'|'\r'))* ('\r'); | 53 | terminal ID: (!('\n'|'\r'))* ; |
54 | terminal ANY_OTHER: ID; | ||
54 | terminal SINGLE_COMMENT: ANY_OTHER; | 55 | terminal SINGLE_COMMENT: ANY_OTHER; |
55 | //terminal ID: ( !('('|')'|'\r'|'\n') )+ ; | 56 | //terminal ID: ( !('('|')'|'\r'|'\n') )+ ; |
56 | 57 | ||
57 | 58 | ||
58 | 59 | ||
60 | |||
61 | |||
59 | ////////////////////////////////// | 62 | ////////////////////////////////// |
60 | // VLS types | 63 | // VLS types |
61 | ////////////////////////////////// | 64 | ////////////////////////////////// |
@@ -71,7 +74,7 @@ VLSName: | |||
71 | 74 | ||
72 | // <comments> | 75 | // <comments> |
73 | VLSComment: | 76 | VLSComment: |
74 | comment = SINGLE_COMMENT | 77 | '%' 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 | 78 | //need to add a new line at the end of the file for the case where the last line is a comment |
76 | ; | 79 | ; |
77 | 80 | ||
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/scoping/VampireLanguageScopeProvider.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/scoping/VampireLanguageScopeProvider.xtend index d6b4a1ae..fb967eee 100644 --- 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 | |||
@@ -11,5 +11,5 @@ package ca.mcgill.ecse.dslreasoner.scoping | |||
11 | * on how and when to use it. | 11 | * on how and when to use it. |
12 | */ | 12 | */ |
13 | class VampireLanguageScopeProvider extends AbstractVampireLanguageScopeProvider { | 13 | class VampireLanguageScopeProvider extends AbstractVampireLanguageScopeProvider { |
14 | 14 | //TODO | |
15 | } | 15 | } |