feat(language): arity validation

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 @@
 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 <https://refinery.tools/>
+ *
+ * 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<Arguments> 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<Arguments> validReferenceTypeTest() {
+                return Stream.of(
+                                "class Foo.",
+                                "abstract class Foo."
+                ).flatMap(definition -> Stream.of(
+                                Arguments.of(definition, "contains"),
+                                Arguments.of(definition, "container")
+                ));
+        }
+}