From 392242099439fd3f21abb87d55ce94050e71ccb5 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Sat, 18 Nov 2023 19:43:09 +0100 Subject: feat(language): arity validation --- .../language/validation/ProblemValidator.java | 122 ++++++++-- .../tests/validation/ArityValidationTest.java | 249 +++++++++++++++++++++ 2 files changed, 353 insertions(+), 18 deletions(-) create mode 100644 subprojects/language/src/test/java/tools/refinery/language/tests/validation/ArityValidationTest.java 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 @@ package tools.refinery.language.validation; import com.google.inject.Inject; +import org.eclipse.emf.ecore.EObject; +import org.eclipse.emf.ecore.EReference; import org.eclipse.xtext.EcoreUtil2; import org.eclipse.xtext.validation.Check; import tools.refinery.language.model.problem.*; @@ -43,6 +45,14 @@ public class ProblemValidator extends AbstractProblemValidator { public static final String INVALID_OPPOSITE_ISSUE = ISSUE_PREFIX + "INVALID_OPPOSITE"; + public static final String INVALID_SUPERTYPE_ISSUE = ISSUE_PREFIX + "INVALID_SUPERTYPE"; + + public static final String INVALID_REFERENCE_TYPE_ISSUE = ISSUE_PREFIX + "INVALID_REFERENCE_TYPE"; + + public static final String INVALID_ARITY_ISSUE = ISSUE_PREFIX + "INVALID_ARITY"; + + public static final String INVALID_TRANSITIVE_CLOSURE_ISSUE = ISSUE_PREFIX + "INVALID_TRANSITIVE_CLOSURE"; + @Inject private ReferenceCounter referenceCounter; @@ -173,24 +183,24 @@ public class ProblemValidator extends AbstractProblemValidator { } return; } - if (!referenceDeclaration.equals(oppositeOfOpposite)) { - var messageBuilder = new StringBuilder() - .append("Expected reference '") - .append(opposite.getName()) - .append("' to have opposite '") - .append(referenceDeclaration.getName()) - .append("'"); - var oppositeOfOppositeName = oppositeOfOpposite.getName(); - if (oppositeOfOppositeName != null) { - messageBuilder.append(", got '") - .append(oppositeOfOppositeName) - .append("' instead"); - } - messageBuilder.append("."); - acceptError(messageBuilder.toString(), referenceDeclaration, - ProblemPackage.Literals.REFERENCE_DECLARATION__OPPOSITE, 0, INVALID_OPPOSITE_ISSUE); - } - } + if (!referenceDeclaration.equals(oppositeOfOpposite)) { + var messageBuilder = new StringBuilder() + .append("Expected reference '") + .append(opposite.getName()) + .append("' to have opposite '") + .append(referenceDeclaration.getName()) + .append("'"); + var oppositeOfOppositeName = oppositeOfOpposite.getName(); + if (oppositeOfOppositeName != null) { + messageBuilder.append(", got '") + .append(oppositeOfOppositeName) + .append("' instead"); + } + messageBuilder.append("."); + acceptError(messageBuilder.toString(), referenceDeclaration, + ProblemPackage.Literals.REFERENCE_DECLARATION__OPPOSITE, 0, INVALID_OPPOSITE_ISSUE); + } + } @Check void checkContainerOpposite(ReferenceDeclaration referenceDeclaration) { @@ -219,4 +229,80 @@ public class ProblemValidator extends AbstractProblemValidator { } } } + + @Check + void checkSupertypes(ClassDeclaration classDeclaration) { + var supertypes = classDeclaration.getSuperTypes(); + int supertypeCount = supertypes.size(); + for (int i = 0; i < supertypeCount; i++) { + var supertype = supertypes.get(i); + if (!supertype.eIsProxy() && !(supertype instanceof ClassDeclaration)) { + var message = "Supertype '%s' of '%s' is not a class." + .formatted(supertype.getName(), classDeclaration.getName()); + acceptError(message, classDeclaration, ProblemPackage.Literals.CLASS_DECLARATION__SUPER_TYPES, i, + INVALID_SUPERTYPE_ISSUE); + } + } + } + + @Check + void checkReferenceType(ReferenceDeclaration referenceDeclaration) { + if (referenceDeclaration.getKind() == ReferenceKind.REFERENCE && + !ProblemUtil.isContainerReference(referenceDeclaration)) { + checkArity(referenceDeclaration, ProblemPackage.Literals.REFERENCE_DECLARATION__REFERENCE_TYPE, 1); + return; + } + var referenceType = referenceDeclaration.getReferenceType(); + if (referenceType == null || referenceType.eIsProxy() || referenceType instanceof ClassDeclaration) { + // Either correct, or a missing reference type where we are probably already emitting another error. + return; + } + var message = "Reference type '%s' of the containment or container reference '%s' is not a class." + .formatted(referenceType.getName(), referenceDeclaration.getName()); + acceptError(message, referenceDeclaration, ProblemPackage.Literals.REFERENCE_DECLARATION__REFERENCE_TYPE, 0, + INVALID_REFERENCE_TYPE_ISSUE); + } + + @Check + void checkParameterType(Parameter parameter) { + checkArity(parameter, ProblemPackage.Literals.PARAMETER__PARAMETER_TYPE, 1); + } + + @Check + void checkAtom(Atom atom) { + int argumentCount = atom.getArguments().size(); + checkArity(atom, ProblemPackage.Literals.ATOM__RELATION, argumentCount); + if (atom.isTransitiveClosure() && argumentCount != 2) { + var message = "Transitive closure needs exactly 2 arguments, got %d arguments instead." + .formatted(argumentCount); + acceptError(message, atom, ProblemPackage.Literals.ATOM__TRANSITIVE_CLOSURE, 0, + INVALID_TRANSITIVE_CLOSURE_ISSUE); + } + } + + @Check + void checkAssertion(Assertion assertion) { + int argumentCount = assertion.getArguments().size(); + checkArity(assertion, ProblemPackage.Literals.ASSERTION__RELATION, argumentCount); + } + + @Check + void checkTypeScope(TypeScope typeScope) { + checkArity(typeScope, ProblemPackage.Literals.TYPE_SCOPE__TARGET_TYPE, 1); + } + + void checkArity(EObject eObject, EReference reference, int expectedArity) { + var value = eObject.eGet(reference); + if (!(value instanceof Relation relation) || relation.eIsProxy()) { + // Feature does not point to a {@link Relation}, we are probably already emitting another error. + return; + } + int arity = ProblemUtil.getArity(relation); + if (arity == expectedArity) { + return; + } + var message = "Expected symbol '%s' to have arity %d, got arity %d instead." + .formatted(relation.getName(), expectedArity, arity); + acceptError(message, eObject, reference, 0, INVALID_ARITY_ISSUE); + } } 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 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.language.tests.validation; + +import com.google.inject.Inject; +import org.eclipse.emf.common.util.Diagnostic; +import org.eclipse.xtext.testing.InjectWith; +import org.eclipse.xtext.testing.extensions.InjectionExtension; +import org.junit.jupiter.api.Test; +import org.junit.jupiter.api.extension.ExtendWith; +import org.junit.jupiter.params.ParameterizedTest; +import org.junit.jupiter.params.provider.Arguments; +import org.junit.jupiter.params.provider.MethodSource; +import org.junit.jupiter.params.provider.ValueSource; +import tools.refinery.language.model.tests.utils.ProblemParseHelper; +import tools.refinery.language.tests.ProblemInjectorProvider; +import tools.refinery.language.validation.ProblemValidator; + +import java.util.stream.Stream; + +import static org.hamcrest.MatcherAssert.assertThat; +import static org.hamcrest.Matchers.*; + +@ExtendWith(InjectionExtension.class) +@InjectWith(ProblemInjectorProvider.class) +class ArityValidationTest { + @Inject + private ProblemParseHelper parseHelper; + + @ParameterizedTest + @ValueSource(strings = {""" + pred Foo(node n) <-> false. + """, """ + pred Foo(node n, node m) <-> false. + """, """ + enum Foo { FOO_A, FOO_B } + """}) + void invalidSupertypeTest(String supertypeDefinition) { + var problem = parseHelper.parse(""" + %s + + class Bar extends Foo. + """.formatted(supertypeDefinition)); + var issues = problem.validate(); + assertThat(issues, hasItem(allOf( + hasProperty("severity", is(Diagnostic.ERROR)), + hasProperty("issueCode", is(ProblemValidator.INVALID_SUPERTYPE_ISSUE)), + hasProperty("message", stringContainsInOrder("Foo", "Bar")) + ))); + } + + @ParameterizedTest + @ValueSource(strings = {""" + class Foo. + """, """ + abstract class Foo. + """}) + void validSupertypeTest(String supertypeDefinition) { + var problem = parseHelper.parse(""" + %s + + class Bar extends Foo. + """.formatted(supertypeDefinition)); + var issues = problem.validate(); + assertThat(issues, empty()); + } + + @ParameterizedTest + @ValueSource(strings = {""" + foo(). + """, """ + foo(a1, a2, a3). + """, """ + pred bar() <-> foo(). + """, """ + pred bar(node n) <-> foo(n, n, n). + """, """ + pred bar(foo n) <-> false. + """, """ + scope foo = 1..10. + """, """ + class Bar { + foo[] f + } + """, """ + class Bar { + refers foo[] f + } + """}) + void invalidArityTest(String usage) { + var problem = parseHelper.parse(""" + pred foo(node a, node b) <-> a != b. + + %s + """.formatted(usage)); + var issues = problem.validate(); + assertThat(issues, hasItem(allOf( + hasProperty("severity", is(Diagnostic.ERROR)), + hasProperty("issueCode", is(ProblemValidator.INVALID_ARITY_ISSUE)), + hasProperty("message", containsString("foo")) + ))); + } + + @ParameterizedTest + @ValueSource(strings = {""" + foo(a). + """, """ + pred bar(node m) <-> !foo(m). + """, """ + pred bar(foo f) <-> true. + """, """ + scope foo = 1..10. + """, """ + class Bar { + foo[] quux + } + """, """ + class Bar { + refers foo[] quux + } + """}) + void validUnaryArityTest(String supertypeDefinition) { + var problem = parseHelper.parse(""" + pred foo(node n) <-> false. + + %s + """.formatted(supertypeDefinition)); + var issues = problem.validate(); + assertThat(issues, empty()); + } + + @ParameterizedTest + @ValueSource(strings = {""" + foo(a, b). + """, """ + pred bar(node m) <-> !foo(m, m). + """, /* Also test for parameters without any type annotation. */ """ + pred bar(m) <-> foo(m, m). + """}) + void validBinaryArityTest(String supertypeDefinition) { + var problem = parseHelper.parse(""" + pred foo(node n, node m) <-> false. + + %s + """.formatted(supertypeDefinition)); + var issues = problem.validate(); + assertThat(issues, empty()); + } + + @Test + void notResolvedArityTest() { + var problem = parseHelper.parse(""" + notResolved(a, b). + """); + var issues = problem.validate(); + assertThat(issues, not(contains(hasProperty("issueCode", is(ProblemValidator.INVALID_ARITY_ISSUE))))); + } + + @Test + void validTransitiveClosure() { + var problem = parseHelper.parse(""" + pred foo(node a, node b) <-> false. + + pred bar(a, b) <-> foo+(a, b). + """); + var issues = problem.validate(); + assertThat(issues, not(contains(hasProperty("issueCode", + is(ProblemValidator.INVALID_TRANSITIVE_CLOSURE_ISSUE))))); + } + + @Test + void invalidTransitiveClosure() { + // 0 and 1 argument transitive closures do not get parsed as transitive closure + // due to the ambiguity with the addition operator {@code a + (b)}. + var problem = parseHelper.parse(""" + pred foo(node a, node b) <-> false. + + pred bar(node a, node b) <-> foo+(a, b, a). + """); + var issues = problem.validate(); + assertThat(issues, hasItem(allOf( + hasProperty("severity", is(Diagnostic.ERROR)), + hasProperty("issueCode", is(ProblemValidator.INVALID_TRANSITIVE_CLOSURE_ISSUE)) + ))); + } + + @ParameterizedTest + @MethodSource + void invalidReferenceTypeTest(String definition, String referenceKind) { + var problem = parseHelper.parse(""" + %s + + class Bar { + %s Foo foo + } + """.formatted(definition, referenceKind)); + var issues = problem.validate(); + assertThat(issues, allOf( + hasItem(allOf( + hasProperty("severity", is(Diagnostic.ERROR)), + hasProperty("issueCode", is(ProblemValidator.INVALID_REFERENCE_TYPE_ISSUE)), + hasProperty("message", stringContainsInOrder("Foo", "foo")) + )), + not(hasItem(hasProperty("issueCode", is(ProblemValidator.INVALID_ARITY_ISSUE)))) + )); + } + + static Stream invalidReferenceTypeTest() { + return Stream.of( + "pred Foo(node n) <-> true.", + "pred Foo(node n, node m) <-> true.", + "enum Foo { FOO_A, FOO_B }" + ).flatMap(definition -> Stream.of( + Arguments.of(definition, "contains"), + Arguments.of(definition, "container") + )); + } + + + @ParameterizedTest + @MethodSource + void validReferenceTypeTest(String definition, String referenceKind) { + var problem = parseHelper.parse(""" + %s + + class Bar { + %s Foo foo + } + """.formatted(definition, referenceKind)); + var issues = problem.validate(); + assertThat(issues, not(hasItem(hasProperty("issueCode", anyOf( + is(ProblemValidator.INVALID_REFERENCE_TYPE_ISSUE), + is(ProblemValidator.INVALID_ARITY_ISSUE) + ))))); + } + + static Stream validReferenceTypeTest() { + return Stream.of( + "class Foo.", + "abstract class Foo." + ).flatMap(definition -> Stream.of( + Arguments.of(definition, "contains"), + Arguments.of(definition, "container") + )); + } +} -- cgit v1.2.3-54-g00ecf