diff options
author | Kristóf Marussy <kristof@marussy.com> | 2023-11-18 19:43:09 +0100 |
---|---|---|
committer | Kristóf Marussy <kristof@marussy.com> | 2023-11-19 14:41:17 +0100 |
commit | 392242099439fd3f21abb87d55ce94050e71ccb5 (patch) | |
tree | 2be45d93ae8ebbd3dd0cc051c3db26f0318cb7d2 /subprojects | |
parent | fix: upper and lower scopes (diff) | |
download | refinery-392242099439fd3f21abb87d55ce94050e71ccb5.tar.gz refinery-392242099439fd3f21abb87d55ce94050e71ccb5.tar.zst refinery-392242099439fd3f21abb87d55ce94050e71ccb5.zip |
feat(language): arity validation
Diffstat (limited to 'subprojects')
2 files changed, 353 insertions, 18 deletions
diff --git a/subprojects/language/src/main/java/tools/refinery/language/validation/ProblemValidator.java b/subprojects/language/src/main/java/tools/refinery/language/validation/ProblemValidator.java index 21b175ee..00ae4531 100644 --- a/subprojects/language/src/main/java/tools/refinery/language/validation/ProblemValidator.java +++ b/subprojects/language/src/main/java/tools/refinery/language/validation/ProblemValidator.java | |||
@@ -10,6 +10,8 @@ | |||
10 | package tools.refinery.language.validation; | 10 | package tools.refinery.language.validation; |
11 | 11 | ||
12 | import com.google.inject.Inject; | 12 | import com.google.inject.Inject; |
13 | import org.eclipse.emf.ecore.EObject; | ||
14 | import org.eclipse.emf.ecore.EReference; | ||
13 | import org.eclipse.xtext.EcoreUtil2; | 15 | import org.eclipse.xtext.EcoreUtil2; |
14 | import org.eclipse.xtext.validation.Check; | 16 | import org.eclipse.xtext.validation.Check; |
15 | import tools.refinery.language.model.problem.*; | 17 | import tools.refinery.language.model.problem.*; |
@@ -43,6 +45,14 @@ public class ProblemValidator extends AbstractProblemValidator { | |||
43 | 45 | ||
44 | public static final String INVALID_OPPOSITE_ISSUE = ISSUE_PREFIX + "INVALID_OPPOSITE"; | 46 | public static final String INVALID_OPPOSITE_ISSUE = ISSUE_PREFIX + "INVALID_OPPOSITE"; |
45 | 47 | ||
48 | public static final String INVALID_SUPERTYPE_ISSUE = ISSUE_PREFIX + "INVALID_SUPERTYPE"; | ||
49 | |||
50 | public static final String INVALID_REFERENCE_TYPE_ISSUE = ISSUE_PREFIX + "INVALID_REFERENCE_TYPE"; | ||
51 | |||
52 | public static final String INVALID_ARITY_ISSUE = ISSUE_PREFIX + "INVALID_ARITY"; | ||
53 | |||
54 | public static final String INVALID_TRANSITIVE_CLOSURE_ISSUE = ISSUE_PREFIX + "INVALID_TRANSITIVE_CLOSURE"; | ||
55 | |||
46 | @Inject | 56 | @Inject |
47 | private ReferenceCounter referenceCounter; | 57 | private ReferenceCounter referenceCounter; |
48 | 58 | ||
@@ -173,24 +183,24 @@ public class ProblemValidator extends AbstractProblemValidator { | |||
173 | } | 183 | } |
174 | return; | 184 | return; |
175 | } | 185 | } |
176 | if (!referenceDeclaration.equals(oppositeOfOpposite)) { | 186 | if (!referenceDeclaration.equals(oppositeOfOpposite)) { |
177 | var messageBuilder = new StringBuilder() | 187 | var messageBuilder = new StringBuilder() |
178 | .append("Expected reference '") | 188 | .append("Expected reference '") |
179 | .append(opposite.getName()) | 189 | .append(opposite.getName()) |
180 | .append("' to have opposite '") | 190 | .append("' to have opposite '") |
181 | .append(referenceDeclaration.getName()) | 191 | .append(referenceDeclaration.getName()) |
182 | .append("'"); | 192 | .append("'"); |
183 | var oppositeOfOppositeName = oppositeOfOpposite.getName(); | 193 | var oppositeOfOppositeName = oppositeOfOpposite.getName(); |
184 | if (oppositeOfOppositeName != null) { | 194 | if (oppositeOfOppositeName != null) { |
185 | messageBuilder.append(", got '") | 195 | messageBuilder.append(", got '") |
186 | .append(oppositeOfOppositeName) | 196 | .append(oppositeOfOppositeName) |
187 | .append("' instead"); | 197 | .append("' instead"); |
188 | } | 198 | } |
189 | messageBuilder.append("."); | 199 | messageBuilder.append("."); |
190 | acceptError(messageBuilder.toString(), referenceDeclaration, | 200 | acceptError(messageBuilder.toString(), referenceDeclaration, |
191 | ProblemPackage.Literals.REFERENCE_DECLARATION__OPPOSITE, 0, INVALID_OPPOSITE_ISSUE); | 201 | ProblemPackage.Literals.REFERENCE_DECLARATION__OPPOSITE, 0, INVALID_OPPOSITE_ISSUE); |
192 | } | 202 | } |
193 | } | 203 | } |
194 | 204 | ||
195 | @Check | 205 | @Check |
196 | void checkContainerOpposite(ReferenceDeclaration referenceDeclaration) { | 206 | void checkContainerOpposite(ReferenceDeclaration referenceDeclaration) { |
@@ -219,4 +229,80 @@ public class ProblemValidator extends AbstractProblemValidator { | |||
219 | } | 229 | } |
220 | } | 230 | } |
221 | } | 231 | } |
232 | |||
233 | @Check | ||
234 | void checkSupertypes(ClassDeclaration classDeclaration) { | ||
235 | var supertypes = classDeclaration.getSuperTypes(); | ||
236 | int supertypeCount = supertypes.size(); | ||
237 | for (int i = 0; i < supertypeCount; i++) { | ||
238 | var supertype = supertypes.get(i); | ||
239 | if (!supertype.eIsProxy() && !(supertype instanceof ClassDeclaration)) { | ||
240 | var message = "Supertype '%s' of '%s' is not a class." | ||
241 | .formatted(supertype.getName(), classDeclaration.getName()); | ||
242 | acceptError(message, classDeclaration, ProblemPackage.Literals.CLASS_DECLARATION__SUPER_TYPES, i, | ||
243 | INVALID_SUPERTYPE_ISSUE); | ||
244 | } | ||
245 | } | ||
246 | } | ||
247 | |||
248 | @Check | ||
249 | void checkReferenceType(ReferenceDeclaration referenceDeclaration) { | ||
250 | if (referenceDeclaration.getKind() == ReferenceKind.REFERENCE && | ||
251 | !ProblemUtil.isContainerReference(referenceDeclaration)) { | ||
252 | checkArity(referenceDeclaration, ProblemPackage.Literals.REFERENCE_DECLARATION__REFERENCE_TYPE, 1); | ||
253 | return; | ||
254 | } | ||
255 | var referenceType = referenceDeclaration.getReferenceType(); | ||
256 | if (referenceType == null || referenceType.eIsProxy() || referenceType instanceof ClassDeclaration) { | ||
257 | // Either correct, or a missing reference type where we are probably already emitting another error. | ||
258 | return; | ||
259 | } | ||
260 | var message = "Reference type '%s' of the containment or container reference '%s' is not a class." | ||
261 | .formatted(referenceType.getName(), referenceDeclaration.getName()); | ||
262 | acceptError(message, referenceDeclaration, ProblemPackage.Literals.REFERENCE_DECLARATION__REFERENCE_TYPE, 0, | ||
263 | INVALID_REFERENCE_TYPE_ISSUE); | ||
264 | } | ||
265 | |||
266 | @Check | ||
267 | void checkParameterType(Parameter parameter) { | ||
268 | checkArity(parameter, ProblemPackage.Literals.PARAMETER__PARAMETER_TYPE, 1); | ||
269 | } | ||
270 | |||
271 | @Check | ||
272 | void checkAtom(Atom atom) { | ||
273 | int argumentCount = atom.getArguments().size(); | ||
274 | checkArity(atom, ProblemPackage.Literals.ATOM__RELATION, argumentCount); | ||
275 | if (atom.isTransitiveClosure() && argumentCount != 2) { | ||
276 | var message = "Transitive closure needs exactly 2 arguments, got %d arguments instead." | ||
277 | .formatted(argumentCount); | ||
278 | acceptError(message, atom, ProblemPackage.Literals.ATOM__TRANSITIVE_CLOSURE, 0, | ||
279 | INVALID_TRANSITIVE_CLOSURE_ISSUE); | ||
280 | } | ||
281 | } | ||
282 | |||
283 | @Check | ||
284 | void checkAssertion(Assertion assertion) { | ||
285 | int argumentCount = assertion.getArguments().size(); | ||
286 | checkArity(assertion, ProblemPackage.Literals.ASSERTION__RELATION, argumentCount); | ||
287 | } | ||
288 | |||
289 | @Check | ||
290 | void checkTypeScope(TypeScope typeScope) { | ||
291 | checkArity(typeScope, ProblemPackage.Literals.TYPE_SCOPE__TARGET_TYPE, 1); | ||
292 | } | ||
293 | |||
294 | void checkArity(EObject eObject, EReference reference, int expectedArity) { | ||
295 | var value = eObject.eGet(reference); | ||
296 | if (!(value instanceof Relation relation) || relation.eIsProxy()) { | ||
297 | // Feature does not point to a {@link Relation}, we are probably already emitting another error. | ||
298 | return; | ||
299 | } | ||
300 | int arity = ProblemUtil.getArity(relation); | ||
301 | if (arity == expectedArity) { | ||
302 | return; | ||
303 | } | ||
304 | var message = "Expected symbol '%s' to have arity %d, got arity %d instead." | ||
305 | .formatted(relation.getName(), expectedArity, arity); | ||
306 | acceptError(message, eObject, reference, 0, INVALID_ARITY_ISSUE); | ||
307 | } | ||
222 | } | 308 | } |
diff --git a/subprojects/language/src/test/java/tools/refinery/language/tests/validation/ArityValidationTest.java b/subprojects/language/src/test/java/tools/refinery/language/tests/validation/ArityValidationTest.java new file mode 100644 index 00000000..68e9fa8d --- /dev/null +++ b/subprojects/language/src/test/java/tools/refinery/language/tests/validation/ArityValidationTest.java | |||
@@ -0,0 +1,249 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.language.tests.validation; | ||
7 | |||
8 | import com.google.inject.Inject; | ||
9 | import org.eclipse.emf.common.util.Diagnostic; | ||
10 | import org.eclipse.xtext.testing.InjectWith; | ||
11 | import org.eclipse.xtext.testing.extensions.InjectionExtension; | ||
12 | import org.junit.jupiter.api.Test; | ||
13 | import org.junit.jupiter.api.extension.ExtendWith; | ||
14 | import org.junit.jupiter.params.ParameterizedTest; | ||
15 | import org.junit.jupiter.params.provider.Arguments; | ||
16 | import org.junit.jupiter.params.provider.MethodSource; | ||
17 | import org.junit.jupiter.params.provider.ValueSource; | ||
18 | import tools.refinery.language.model.tests.utils.ProblemParseHelper; | ||
19 | import tools.refinery.language.tests.ProblemInjectorProvider; | ||
20 | import tools.refinery.language.validation.ProblemValidator; | ||
21 | |||
22 | import java.util.stream.Stream; | ||
23 | |||
24 | import static org.hamcrest.MatcherAssert.assertThat; | ||
25 | import static org.hamcrest.Matchers.*; | ||
26 | |||
27 | @ExtendWith(InjectionExtension.class) | ||
28 | @InjectWith(ProblemInjectorProvider.class) | ||
29 | class ArityValidationTest { | ||
30 | @Inject | ||
31 | private ProblemParseHelper parseHelper; | ||
32 | |||
33 | @ParameterizedTest | ||
34 | @ValueSource(strings = {""" | ||
35 | pred Foo(node n) <-> false. | ||
36 | """, """ | ||
37 | pred Foo(node n, node m) <-> false. | ||
38 | """, """ | ||
39 | enum Foo { FOO_A, FOO_B } | ||
40 | """}) | ||
41 | void invalidSupertypeTest(String supertypeDefinition) { | ||
42 | var problem = parseHelper.parse(""" | ||
43 | %s | ||
44 | |||
45 | class Bar extends Foo. | ||
46 | """.formatted(supertypeDefinition)); | ||
47 | var issues = problem.validate(); | ||
48 | assertThat(issues, hasItem(allOf( | ||
49 | hasProperty("severity", is(Diagnostic.ERROR)), | ||
50 | hasProperty("issueCode", is(ProblemValidator.INVALID_SUPERTYPE_ISSUE)), | ||
51 | hasProperty("message", stringContainsInOrder("Foo", "Bar")) | ||
52 | ))); | ||
53 | } | ||
54 | |||
55 | @ParameterizedTest | ||
56 | @ValueSource(strings = {""" | ||
57 | class Foo. | ||
58 | """, """ | ||
59 | abstract class Foo. | ||
60 | """}) | ||
61 | void validSupertypeTest(String supertypeDefinition) { | ||
62 | var problem = parseHelper.parse(""" | ||
63 | %s | ||
64 | |||
65 | class Bar extends Foo. | ||
66 | """.formatted(supertypeDefinition)); | ||
67 | var issues = problem.validate(); | ||
68 | assertThat(issues, empty()); | ||
69 | } | ||
70 | |||
71 | @ParameterizedTest | ||
72 | @ValueSource(strings = {""" | ||
73 | foo(). | ||
74 | """, """ | ||
75 | foo(a1, a2, a3). | ||
76 | """, """ | ||
77 | pred bar() <-> foo(). | ||
78 | """, """ | ||
79 | pred bar(node n) <-> foo(n, n, n). | ||
80 | """, """ | ||
81 | pred bar(foo n) <-> false. | ||
82 | """, """ | ||
83 | scope foo = 1..10. | ||
84 | """, """ | ||
85 | class Bar { | ||
86 | foo[] f | ||
87 | } | ||
88 | """, """ | ||
89 | class Bar { | ||
90 | refers foo[] f | ||
91 | } | ||
92 | """}) | ||
93 | void invalidArityTest(String usage) { | ||
94 | var problem = parseHelper.parse(""" | ||
95 | pred foo(node a, node b) <-> a != b. | ||
96 | |||
97 | %s | ||
98 | """.formatted(usage)); | ||
99 | var issues = problem.validate(); | ||
100 | assertThat(issues, hasItem(allOf( | ||
101 | hasProperty("severity", is(Diagnostic.ERROR)), | ||
102 | hasProperty("issueCode", is(ProblemValidator.INVALID_ARITY_ISSUE)), | ||
103 | hasProperty("message", containsString("foo")) | ||
104 | ))); | ||
105 | } | ||
106 | |||
107 | @ParameterizedTest | ||
108 | @ValueSource(strings = {""" | ||
109 | foo(a). | ||
110 | """, """ | ||
111 | pred bar(node m) <-> !foo(m). | ||
112 | """, """ | ||
113 | pred bar(foo f) <-> true. | ||
114 | """, """ | ||
115 | scope foo = 1..10. | ||
116 | """, """ | ||
117 | class Bar { | ||
118 | foo[] quux | ||
119 | } | ||
120 | """, """ | ||
121 | class Bar { | ||
122 | refers foo[] quux | ||
123 | } | ||
124 | """}) | ||
125 | void validUnaryArityTest(String supertypeDefinition) { | ||
126 | var problem = parseHelper.parse(""" | ||
127 | pred foo(node n) <-> false. | ||
128 | |||
129 | %s | ||
130 | """.formatted(supertypeDefinition)); | ||
131 | var issues = problem.validate(); | ||
132 | assertThat(issues, empty()); | ||
133 | } | ||
134 | |||
135 | @ParameterizedTest | ||
136 | @ValueSource(strings = {""" | ||
137 | foo(a, b). | ||
138 | """, """ | ||
139 | pred bar(node m) <-> !foo(m, m). | ||
140 | """, /* Also test for parameters without any type annotation. */ """ | ||
141 | pred bar(m) <-> foo(m, m). | ||
142 | """}) | ||
143 | void validBinaryArityTest(String supertypeDefinition) { | ||
144 | var problem = parseHelper.parse(""" | ||
145 | pred foo(node n, node m) <-> false. | ||
146 | |||
147 | %s | ||
148 | """.formatted(supertypeDefinition)); | ||
149 | var issues = problem.validate(); | ||
150 | assertThat(issues, empty()); | ||
151 | } | ||
152 | |||
153 | @Test | ||
154 | void notResolvedArityTest() { | ||
155 | var problem = parseHelper.parse(""" | ||
156 | notResolved(a, b). | ||
157 | """); | ||
158 | var issues = problem.validate(); | ||
159 | assertThat(issues, not(contains(hasProperty("issueCode", is(ProblemValidator.INVALID_ARITY_ISSUE))))); | ||
160 | } | ||
161 | |||
162 | @Test | ||
163 | void validTransitiveClosure() { | ||
164 | var problem = parseHelper.parse(""" | ||
165 | pred foo(node a, node b) <-> false. | ||
166 | |||
167 | pred bar(a, b) <-> foo+(a, b). | ||
168 | """); | ||
169 | var issues = problem.validate(); | ||
170 | assertThat(issues, not(contains(hasProperty("issueCode", | ||
171 | is(ProblemValidator.INVALID_TRANSITIVE_CLOSURE_ISSUE))))); | ||
172 | } | ||
173 | |||
174 | @Test | ||
175 | void invalidTransitiveClosure() { | ||
176 | // 0 and 1 argument transitive closures do not get parsed as transitive closure | ||
177 | // due to the ambiguity with the addition operator {@code a + (b)}. | ||
178 | var problem = parseHelper.parse(""" | ||
179 | pred foo(node a, node b) <-> false. | ||
180 | |||
181 | pred bar(node a, node b) <-> foo+(a, b, a). | ||
182 | """); | ||
183 | var issues = problem.validate(); | ||
184 | assertThat(issues, hasItem(allOf( | ||
185 | hasProperty("severity", is(Diagnostic.ERROR)), | ||
186 | hasProperty("issueCode", is(ProblemValidator.INVALID_TRANSITIVE_CLOSURE_ISSUE)) | ||
187 | ))); | ||
188 | } | ||
189 | |||
190 | @ParameterizedTest | ||
191 | @MethodSource | ||
192 | void invalidReferenceTypeTest(String definition, String referenceKind) { | ||
193 | var problem = parseHelper.parse(""" | ||
194 | %s | ||
195 | |||
196 | class Bar { | ||
197 | %s Foo foo | ||
198 | } | ||
199 | """.formatted(definition, referenceKind)); | ||
200 | var issues = problem.validate(); | ||
201 | assertThat(issues, allOf( | ||
202 | hasItem(allOf( | ||
203 | hasProperty("severity", is(Diagnostic.ERROR)), | ||
204 | hasProperty("issueCode", is(ProblemValidator.INVALID_REFERENCE_TYPE_ISSUE)), | ||
205 | hasProperty("message", stringContainsInOrder("Foo", "foo")) | ||
206 | )), | ||
207 | not(hasItem(hasProperty("issueCode", is(ProblemValidator.INVALID_ARITY_ISSUE)))) | ||
208 | )); | ||
209 | } | ||
210 | |||
211 | static Stream<Arguments> invalidReferenceTypeTest() { | ||
212 | return Stream.of( | ||
213 | "pred Foo(node n) <-> true.", | ||
214 | "pred Foo(node n, node m) <-> true.", | ||
215 | "enum Foo { FOO_A, FOO_B }" | ||
216 | ).flatMap(definition -> Stream.of( | ||
217 | Arguments.of(definition, "contains"), | ||
218 | Arguments.of(definition, "container") | ||
219 | )); | ||
220 | } | ||
221 | |||
222 | |||
223 | @ParameterizedTest | ||
224 | @MethodSource | ||
225 | void validReferenceTypeTest(String definition, String referenceKind) { | ||
226 | var problem = parseHelper.parse(""" | ||
227 | %s | ||
228 | |||
229 | class Bar { | ||
230 | %s Foo foo | ||
231 | } | ||
232 | """.formatted(definition, referenceKind)); | ||
233 | var issues = problem.validate(); | ||
234 | assertThat(issues, not(hasItem(hasProperty("issueCode", anyOf( | ||
235 | is(ProblemValidator.INVALID_REFERENCE_TYPE_ISSUE), | ||
236 | is(ProblemValidator.INVALID_ARITY_ISSUE) | ||
237 | ))))); | ||
238 | } | ||
239 | |||
240 | static Stream<Arguments> validReferenceTypeTest() { | ||
241 | return Stream.of( | ||
242 | "class Foo.", | ||
243 | "abstract class Foo." | ||
244 | ).flatMap(definition -> Stream.of( | ||
245 | Arguments.of(definition, "contains"), | ||
246 | Arguments.of(definition, "container") | ||
247 | )); | ||
248 | } | ||
249 | } | ||