diff options
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill')
2 files changed, 96 insertions, 70 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 index d5b40ed9..a76107c4 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 | |||
@@ -10,15 +10,15 @@ generate vampireLanguage "http://www.mcgill.ca/ecse/dslreasoner/VampireLanguage" | |||
10 | //@@@@@@@@@@@ | 10 | //@@@@@@@@@@@ |
11 | 11 | ||
12 | VampireModel: | 12 | VampireModel: |
13 | // TODO ensures there is always exactly 1 conjecture | ||
14 | ( | 13 | ( |
15 | includes += VLSInclude | | 14 | includes += VLSInclude | |
16 | comments += VLSComment | | 15 | comments += VLSComment | |
17 | formulas += VLSFofFormula | 16 | confirmations += VLSConfirmations| |
17 | formulas += VLSFofFormula | | ||
18 | tfformulas += VLSTffFormula | ||
19 | |||
18 | )* | 20 | )* |
19 | ; | 21 | ; |
20 | |||
21 | |||
22 | 22 | ||
23 | ////////////////////////////////// | 23 | ////////////////////////////////// |
24 | // VLS terminals | 24 | // VLS terminals |
@@ -56,9 +56,6 @@ terminal SINGLE_COMMENT: ANY_OTHER; | |||
56 | //terminal ID: ( !('('|')'|'\r'|'\n') )+ ; | 56 | //terminal ID: ( !('('|')'|'\r'|'\n') )+ ; |
57 | 57 | ||
58 | 58 | ||
59 | |||
60 | |||
61 | |||
62 | ////////////////////////////////// | 59 | ////////////////////////////////// |
63 | // VLS types | 60 | // VLS types |
64 | ////////////////////////////////// | 61 | ////////////////////////////////// |
@@ -80,83 +77,112 @@ VLSComment: | |||
80 | 77 | ||
81 | //VLSConstantDeclaration: name = (LOWER_WORD_ID | SINGLE_QUOTE | DOLLAR_ID | DOUBLE_DOLLAR_ID ); | 78 | //VLSConstantDeclaration: name = (LOWER_WORD_ID | SINGLE_QUOTE | DOLLAR_ID | DOUBLE_DOLLAR_ID ); |
82 | 79 | ||
83 | // <FOF formulas> | 80 | VLSConfirmations: |
84 | VLSFofFormula: | 81 | VLSSatisfiable //| VLSFiniteModel// | VLSTrying |
85 | 'fof' '(' name = (LOWER_WORD_ID | SIGNED_LITERAL | SINGLE_QUOTE) ',' fofRole = VLSRole ',' fofFormula = VLSTerm (',' annotations = VLSAnnotation)? ')' '.' | ||
86 | ; | ||
87 | /* | ||
88 | //NAME | ||
89 | VLSName: | ||
90 | //(atomic_Word = Atomic_Word | integer = Integer | single_quote_word = Single_Quote_Word) | ||
91 | name = (LOWER_WORD_ID | SIGNED_INT_ID | SINGLE_QUOTE) | ||
92 | ; | ||
93 | */ | ||
94 | //<ROLE> | ||
95 | VLSRole: | ||
96 | VLSAxiom | VLSConjecture | VLSHypothesis | VLSDefinition | | ||
97 | VLSAssumption | VLSLemma | VLSTheorem | VLSCorollary | VLSNegated_Conjecture | | ||
98 | VLSPlain | VLSType |VLSFi_Domain | VLSFi_Functors | VLSFi_Predicates | VLSUnknown | ||
99 | ; | 82 | ; |
100 | 83 | ||
101 | VLSAxiom: | 84 | VLSSatisfiable: |
102 | "axiom" | 85 | {VLSSatisfiable} 'Satisfiable!' |
103 | ; | 86 | ; |
104 | 87 | ||
105 | VLSConjecture: | 88 | VLSTrying: |
106 | "conjecture" | 89 | 'TRYING' '[' name = LITERAL ']' |
107 | ; | 90 | ; |
108 | 91 | ||
109 | VLSHypothesis: | 92 | VLSFiniteModel: |
110 | "hypothesis" | 93 | {VLSFiniteModel} 'Finite' 'Model' 'Found!' |
111 | ; | ||
112 | |||
113 | VLSDefinition: | ||
114 | "definition" | ||
115 | ; | 94 | ; |
116 | 95 | ||
117 | VLSAssumption: | 96 | // <FOF formulas> |
118 | "assumption" | 97 | VLSFofFormula: |
119 | ; | 98 | 'fof' '(' name = (LOWER_WORD_ID | SIGNED_LITERAL | SINGLE_QUOTE) ',' fofRole = VLSRole ',' fofFormula = VLSTerm (',' annotations = VLSAnnotation)? ')' '.' |
120 | |||
121 | VLSLemma: | ||
122 | "lemma" | ||
123 | ; | ||
124 | |||
125 | VLSTheorem: | ||
126 | "theorem" | ||
127 | ; | ||
128 | |||
129 | VLSCorollary: | ||
130 | "corollary" | ||
131 | ; | ||
132 | |||
133 | VLSNegated_Conjecture: | ||
134 | "negated_conjecture" | ||
135 | ; | 99 | ; |
136 | 100 | ||
137 | VLSPlain: | ||
138 | "plain" | ||
139 | ; | ||
140 | 101 | ||
141 | VLSType: | 102 | VLSTffFormula: |
142 | "type" | 103 | 'tff' '(' name = (LOWER_WORD_ID | SIGNED_LITERAL | SINGLE_QUOTE) ',' fofRole = VLSRole ',' fofFormula = VLSTerm (',' annotations = VLSAnnotation)? ')' '.' |
143 | ; | 104 | ; |
144 | 105 | ||
145 | VLSFi_Domain: | ||
146 | "fi_domain" | ||
147 | ; | ||
148 | 106 | ||
149 | VLSFi_Functors: | 107 | /* |
150 | "fi_functors" | 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) | ||
151 | ; | 112 | ; |
152 | 113 | */ | |
153 | VLSFi_Predicates: | 114 | //<ROLE> |
154 | "fi_predicates" | 115 | VLSRole: |
116 | "axiom" | "conjecture" | "hypothesis" | "definition" | "assumption" | "lemma" | ||
117 | | "theorem" | "corollary" | "negated_conjecture" | "plain" | "type" | | ||
118 | "fi_domain" | "fi_functors" | "fi_predicates" | "unknown" | ||
155 | ; | 119 | ; |
156 | 120 | ||
157 | VLSUnknown: | 121 | //VLSRole: |
158 | "unknown" | 122 | // VLSAxiom | VLSConjecture | VLSHypothesis | VLSDefinition | |
159 | ; | 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 | //; | ||
160 | 186 | ||
161 | // <ANNOTATION> | 187 | // <ANNOTATION> |
162 | // Not at all based on the website. based on what we think the output will be like | 188 | // Not at all based on the website. based on what we think the output will be like |
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 index f943daad..4398d659 100644 --- 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 | |||
@@ -38,11 +38,11 @@ class VampireLanguageFormatter extends AbstractFormatter2 { | |||
38 | } | 38 | } |
39 | 39 | ||
40 | def dispatch void format(VLSFofFormula formula, extension IFormattableDocument document){ | 40 | def dispatch void format(VLSFofFormula formula, extension IFormattableDocument document){ |
41 | formula.append[newLine] | 41 | // formula.append[newLine] |
42 | } | 42 | } |
43 | 43 | ||
44 | def dispatch void format(VLSComment comment, extension IFormattableDocument document){ | 44 | def dispatch void format(VLSComment comment, extension IFormattableDocument document){ |
45 | comment.append[newLine] | 45 | // comment.append[newLine] |
46 | } | 46 | } |
47 | // TODO: implement for VLSFofFormula, VLSAnnotation, VLSAnd, VLSOr, VLSUniversalQuantifier, VLSExistentialQuantifier, VLSUnaryNegation, VLSFunction, VLSLess, VLSFunctionFof, VLSEquivalent, VLSImplies, VLSRevImplies, VLSXnor, VLSNor, VLSNand, VLSInequality, VLSEquality, VLSAssignment | 47 | // TODO: implement for VLSFofFormula, VLSAnnotation, VLSAnd, VLSOr, VLSUniversalQuantifier, VLSExistentialQuantifier, VLSUnaryNegation, VLSFunction, VLSLess, VLSFunctionFof, VLSEquivalent, VLSImplies, VLSRevImplies, VLSXnor, VLSNor, VLSNand, VLSInequality, VLSEquality, VLSAssignment |
48 | } | 48 | } |