feat(language): validate module isolation

8 files changed, 198 insertions, 16 deletions

diff --git a/subprojects/frontend/src/language/problem.grammar b/subprojects/frontend/src/language/problem.grammar
index b08a9c36..ac451e7a 100644
--- a/subprojects/frontend/src/language/problem.grammar
+++ b/subprojects/frontend/src/language/problem.grammar
@@ -57,10 +57,10 @@ statement {
   //  RuleBody { ":" sep<OrOp, Conjunction> "==>" sep<OrOp, Consequent> "." }
   //} |
   AtomDeclaration {
-    ckw<"atom"> sep<",", AtomNodeName> "."
+    kw<"declare">? ckw<"atom"> sep<",", AtomNodeName> "."
   } |
   NodeDeclaration {
-    (ckw<"node"> | ckw<"multi">) sep<",", NodeName> "."
+    (kw<"declare"> | kw<"declare">? ckw<"multi">) sep<",", NodeName> "."
   } |
   ScopeDeclaration {
     kw<"scope"> sep<",", ScopeElement> "."
diff --git a/subprojects/frontend/src/language/problemLanguageSupport.ts b/subprojects/frontend/src/language/problemLanguageSupport.ts
index 3847fdd8..2483c2e3 100644
--- a/subprojects/frontend/src/language/problemLanguageSupport.ts
+++ b/subprojects/frontend/src/language/problemLanguageSupport.ts
@@ -28,7 +28,7 @@ const parserWithMetadata = parser.configure({
       LineComment: t.lineComment,
       BlockComment: t.blockComment,
       'module problem class enum pred fn scope': t.definitionKeyword,
-      'node atom multi': t.definitionKeyword,
+      'declare atom multi': t.definitionKeyword,
       'abstract extends refers contains container opposite': t.modifier,
       'default error contained containment': t.modifier,
       'true false unknown error': t.keyword,
diff --git a/subprojects/language/src/main/java/tools/refinery/language/Problem.xtext b/subprojects/language/src/main/java/tools/refinery/language/Problem.xtext
index c5c42ebe..4ce3fae1 100644
--- a/subprojects/language/src/main/java/tools/refinery/language/Problem.xtext
+++ b/subprojects/language/src/main/java/tools/refinery/language/Problem.xtext
@@ -256,10 +256,11 @@ ExactMultiplicity:
         exactValue=INT;
 
 NodeDeclaration:
-        kind=NodeKind nodes+=EnumLiteral ("," nodes+=EnumLiteral)* ".";
+        ("declare" | "declare"? kind=NodeKind)
+        nodes+=EnumLiteral ("," nodes+=EnumLiteral)* ".";
 
 enum NodeKind:
-        NODE="node" | ATOM="atom" | MULTI="multi";
+        ATOM="atom" | MULTI="multi";
 
 UpperBound returns ecore::EInt:
         INT | "*";
@@ -274,7 +275,7 @@ Identifier:
         NonContainmentIdentifier | "contains" | "container";
 
 NonContainmentIdentifier:
-        ID | "node" | "atom" | "multi" | "contained" |
+        ID | "atom" | "multi" | "contained" |
         "sum" | "prod" | "min" | "max" | "problem" | "module";
 
 Real returns ecore::EDouble:
diff --git a/subprojects/language/src/main/java/tools/refinery/language/formatting2/ProblemFormatter.java b/subprojects/language/src/main/java/tools/refinery/language/formatting2/ProblemFormatter.java
index 0b87e8bb..d6ece1ea 100644
--- a/subprojects/language/src/main/java/tools/refinery/language/formatting2/ProblemFormatter.java
+++ b/subprojects/language/src/main/java/tools/refinery/language/formatting2/ProblemFormatter.java
@@ -23,7 +23,7 @@ public class ProblemFormatter extends AbstractJavaFormatter {
         protected void format(Problem problem, IFormattableDocument doc) {
                 doc.prepend(problem, this::noSpace);
                 var region = regionFor(problem);
-                doc.append(region.feature(ProblemPackage.Literals.PROBLEM__KIND), this::oneSpace);
+                doc.prepend(region.feature(ProblemPackage.Literals.NAMED_ELEMENT__NAME), this::oneSpace);
                 doc.prepend(region.keyword("."), this::noSpace);
                 appendNewLines(doc, region.keyword("."), this::twoNewLines);
                 for (var statement : problem.getStatements()) {
@@ -135,6 +135,7 @@ public class ProblemFormatter extends AbstractJavaFormatter {
         protected void format(NodeDeclaration nodeDeclaration, IFormattableDocument doc) {
                 surroundNewLines(doc, nodeDeclaration, this::singleNewLine);
                 var region = regionFor(nodeDeclaration);
+                doc.append(region.keyword("declare"), this::oneSpace);
                 doc.append(region.feature(ProblemPackage.Literals.NODE_DECLARATION__KIND), this::oneSpace);
                 formatList(region, ",", doc);
                 doc.prepend(region.keyword("."), this::noSpace);
diff --git a/subprojects/language/src/main/java/tools/refinery/language/utils/ProblemUtil.java b/subprojects/language/src/main/java/tools/refinery/language/utils/ProblemUtil.java
index ee0e141d..0f87c04b 100644
--- a/subprojects/language/src/main/java/tools/refinery/language/utils/ProblemUtil.java
+++ b/subprojects/language/src/main/java/tools/refinery/language/utils/ProblemUtil.java
@@ -8,6 +8,7 @@ package tools.refinery.language.utils;
 import org.eclipse.emf.common.util.URI;
 import org.eclipse.emf.ecore.EObject;
 import org.eclipse.emf.ecore.util.EcoreUtil;
+import org.eclipse.xtext.EcoreUtil2;
 import tools.refinery.language.model.problem.*;
 
 public final class ProblemUtil {
@@ -126,6 +127,11 @@ public final class ProblemUtil {
                 };
         }
 
+        public static boolean isInModule(EObject eObject) {
+                var problem = EcoreUtil2.getContainerOfType(eObject, Problem.class);
+                return problem != null && problem.getKind() == ModuleKind.MODULE;
+        }
+
         private static URI getLibraryUri() {
                 var libraryResource = ProblemUtil.class.getClassLoader()
                                 .getResource("tools/refinery/language/%s.problem".formatted(BUILTIN_LIBRARY_NAME));
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 a95e8b3c..4cbb02c2 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
@@ -86,8 +86,8 @@ public class ProblemValidator extends AbstractProblemValidator {
                 var variableOrNode = expr.getVariableOrNode();
                 if (variableOrNode instanceof Node node && !ProblemUtil.isAtomNode(node)) {
                         var name = node.getName();
-                        var message = ("Only individuals can be referenced in predicates. " +
-                                        "Mark '%s' as individual with the declaration 'indiv %s.'").formatted(name, name);
+                        var message = ("Only atoms can be referenced in predicates. " +
+                                        "Mark '%s' as an atom with the declaration 'atom %s.'").formatted(name, name);
                         error(message, expr, ProblemPackage.Literals.VARIABLE_OR_NODE_EXPR__VARIABLE_OR_NODE,
                                         INSIGNIFICANT_INDEX, NODE_CONSTANT_ISSUE);
                 }
@@ -302,6 +302,10 @@ public class ProblemValidator extends AbstractProblemValidator {
         @Check
         public void checkTypeScope(TypeScope typeScope) {
                 checkArity(typeScope, ProblemPackage.Literals.TYPE_SCOPE__TARGET_TYPE, 1);
+                if (typeScope.isIncrement() && ProblemUtil.isInModule(typeScope)) {
+                        acceptError("Incremental type scopes are not supported in modules", typeScope, null, 0,
+                                        INVALID_MULTIPLICITY_ISSUE);
+                }
         }
 
         private void checkArity(EObject eObject, EReference reference, int expectedArity) {
@@ -351,9 +355,9 @@ public class ProblemValidator extends AbstractProblemValidator {
         }
 
         private void checkExistsAssertion(Assertion assertion, LogicValue value) {
-                if (value == LogicValue.TRUE || value == LogicValue.UNKNOWN) {
-                        // {@code true} is always a valid value for {@code exists}, while {@code unknown} values may always be
-                        // refined to {@code true} if necessary (e.g., for individual nodes).
+                if (value == LogicValue.UNKNOWN) {
+                        // {@code unknown} values may always be refined to {@code true} of {@code false} if necessary (e.g., for
+                        // atom nodes or removed multi-objects).
                         return;
                 }
                 var arguments = assertion.getArguments();
@@ -361,9 +365,16 @@ public class ProblemValidator extends AbstractProblemValidator {
                         // We already report an error on invalid arity.
                         return;
                 }
-                var node = getNodeArgumentForMultiObjectAssertion(arguments.get(0));
-                if (node != null && !node.eIsProxy() && ProblemUtil.isAtomNode(node)) {
-                        acceptError("Individual nodes must exist.", assertion, null, 0, UNSUPPORTED_ASSERTION_ISSUE);
+                var node = getNodeArgumentForMultiObjectAssertion(arguments.getFirst());
+                if (node == null || node.eIsProxy()) {
+                        return;
+                }
+                if (ProblemUtil.isAtomNode(node) && value != LogicValue.TRUE) {
+                        acceptError("Atom nodes must exist.", assertion, null, 0, UNSUPPORTED_ASSERTION_ISSUE);
+                }
+                if (ProblemUtil.isMultiNode(node) && value != LogicValue.FALSE && ProblemUtil.isInModule(node)) {
+                        acceptError("Multi-objects in modules cannot be required to exist.", assertion, null, 0,
+                                        UNSUPPORTED_ASSERTION_ISSUE);
                 }
         }
 
@@ -403,4 +414,23 @@ public class ProblemValidator extends AbstractProblemValidator {
                 }
                 throw new IllegalArgumentException("Unknown assertion argument: " + argument);
         }
+
+        @Check
+        private void checkImplicitNodeInModule(Assertion assertion) {
+                if (!ProblemUtil.isInModule(assertion)) {
+                        return;
+                }
+                for (var argument : assertion.getArguments()) {
+                        if (argument instanceof NodeAssertionArgument nodeAssertionArgument) {
+                                var node = nodeAssertionArgument.getNode();
+                                if (node != null && !node.eIsProxy() && ProblemUtil.isImplicitNode(node)) {
+                                        var name = node.getName();
+                                        var message = ("Implicit nodes are not allowed in modules. Explicitly declare '%s' as a node " +
+                                                        "with the declaration 'declare %s.'").formatted(name, name);
+                                        acceptError(message, nodeAssertionArgument, ProblemPackage.Literals.NODE_ASSERTION_ARGUMENT__NODE,
+                                                        0, UNSUPPORTED_ASSERTION_ISSUE);
+                                }
+                        }
+                }
+        }
 }
diff --git a/subprojects/language/src/test/java/tools/refinery/language/tests/validation/AssertionValidationTest.java b/subprojects/language/src/test/java/tools/refinery/language/tests/validation/AssertionValidationTest.java
index 82dea31b..1fb08845 100644
--- a/subprojects/language/src/test/java/tools/refinery/language/tests/validation/AssertionValidationTest.java
+++ b/subprojects/language/src/test/java/tools/refinery/language/tests/validation/AssertionValidationTest.java
@@ -82,7 +82,6 @@ class AssertionValidationTest {
                         "exists(n).",
                         "?exists(n).",
                         "!exists(n).",
-                        "exists(*).",
                         "?exists(*).",
                         "exists(Foo::new).",
                         "?exists(Foo::new).",
diff --git a/subprojects/language/src/test/java/tools/refinery/language/tests/validation/ModuleValidationTest.java b/subprojects/language/src/test/java/tools/refinery/language/tests/validation/ModuleValidationTest.java
new file mode 100644
index 00000000..00ad051b
--- /dev/null
+++ b/subprojects/language/src/test/java/tools/refinery/language/tests/validation/ModuleValidationTest.java
@@ -0,0 +1,145 @@
+/*
+ * SPDX-FileCopyrightText: 2024 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.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 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 ModuleValidationTest {
+        @Inject
+        private ProblemParseHelper parseHelper;
+
+        @ParameterizedTest
+        @MethodSource
+        void invalidMultiObjectExistsTest(String invalidDeclaration) {
+                var problem = parseHelper.parse("""
+                                module.
+
+                                %s
+                                """.formatted(invalidDeclaration));
+                var issues = problem.validate();
+                assertThat(issues, hasItem(hasProperty("issueCode",
+                                is(ProblemValidator.UNSUPPORTED_ASSERTION_ISSUE))));
+        }
+
+        static Stream<Arguments> invalidMultiObjectExistsTest() {
+                return Stream.of(
+                                Arguments.of("""
+                                                class Foo.
+                                                exists(Foo::new).
+                                                """),
+                                Arguments.of("""
+                                                multi m.
+                                                exists(m).
+                                                """));
+        }
+
+        @Test
+        void invalidScopeTest() {
+                var problem = parseHelper.parse("""
+                                module.
+
+                                class Foo.
+                                scope Foo += 1.
+                                """);
+                var issues = problem.validate();
+                assertThat(issues, hasItem(hasProperty("issueCode",
+                                is(ProblemValidator.INVALID_MULTIPLICITY_ISSUE))));
+        }
+
+        @Test
+        void invalidAssertionArgumentTest() {
+                var problem = parseHelper.parse("""
+                                module.
+
+                                class Foo.
+                                Foo(foo1).
+                                """);
+                var issues = problem.validate();
+                assertThat(issues, hasItem(allOf(
+                                hasProperty("issueCode", is(ProblemValidator.UNSUPPORTED_ASSERTION_ISSUE)),
+                                hasProperty("message", containsString("foo1")))));
+        }
+
+        @ParameterizedTest
+        @MethodSource
+        void validDeclarationTest(String validDeclaration) {
+                var problem = parseHelper.parse(validDeclaration);
+                var issues = problem.validate();
+                assertThat(issues, hasSize(0));
+        }
+
+        static Stream<Arguments> validDeclarationTest() {
+                return Stream.concat(
+                                invalidMultiObjectExistsTest(),
+                                Stream.of(
+                                                Arguments.of("""
+                                                                class Foo.
+                                                                scope Foo += 1.
+                                                                """),
+                                                Arguments.of("""
+                                                                module.
+
+                                                                class Foo.
+                                                                scope Foo = 1.
+                                                                """),
+                                                Arguments.of("""
+                                                                class Foo.
+                                                                Foo(foo1).
+                                                                """),
+                                                Arguments.of("""
+                                                                module.
+
+                                                                class Foo.
+                                                                multi foo1.
+                                                                Foo(foo1).
+                                                                """),
+                                                Arguments.of("""
+                                                                module.
+
+                                                                class Foo.
+                                                                atom foo1.
+                                                                Foo(foo1).
+                                                                """),
+                                                Arguments.of("""
+                                                                module.
+
+                                                                class Foo.
+                                                                declare foo1.
+                                                                Foo(foo1).
+                                                                """),
+                                                Arguments.of("""
+                                                                module.
+
+                                                                enum Foo { foo1 }
+                                                                Foo(foo1).
+                                                                """),
+                                                Arguments.of("""
+                                                                module.
+
+                                                                class Foo.
+                                                                Foo(Foo::new).
+                                                                """)
+                                )
+                );
+        }
+}