feat(language): validate module isolation

4 files changed, 50 insertions, 12 deletions

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);
+                                }
+                        }
+                }
+        }
 }