feat(language): validate quantification in rules

3 files changed, 119 insertions, 12 deletions

diff --git a/subprojects/language/src/main/java/tools/refinery/language/validation/ExistsVariableCollector.java b/subprojects/language/src/main/java/tools/refinery/language/validation/ExistsVariableCollector.java
new file mode 100644
index 00000000..5812bdc4
--- /dev/null
+++ b/subprojects/language/src/main/java/tools/refinery/language/validation/ExistsVariableCollector.java
@@ -0,0 +1,75 @@
+/*
+ * SPDX-FileCopyrightText: 2024 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.language.validation;
+
+import com.google.inject.Inject;
+import com.google.inject.Singleton;
+import org.eclipse.xtext.EcoreUtil2;
+import org.eclipse.xtext.util.IResourceScopeCache;
+import org.eclipse.xtext.util.Tuples;
+import tools.refinery.language.model.problem.*;
+import tools.refinery.language.scoping.imports.ImportAdapterProvider;
+import tools.refinery.language.utils.ProblemUtil;
+
+import java.util.HashSet;
+import java.util.Set;
+
+@Singleton
+public class ExistsVariableCollector {
+        private static final String EXISTS_VARIABLES =
+                        "tools.refinery.language.validation.ExistsVariableCollector.EXISTS_VARIABLES";
+
+        @Inject
+        private IResourceScopeCache cache = IResourceScopeCache.NullImpl.INSTANCE;
+
+        @Inject
+        private ImportAdapterProvider importAdapterProvider;
+
+        public boolean missingExistsConstraint(Variable variable) {
+                if (variable instanceof Parameter) {
+                        return false;
+                }
+                if (ProblemUtil.isImplicitVariable(variable)) {
+                        var negation = EcoreUtil2.getContainerOfType(variable, NegationExpr.class);
+                        if (negation != null) {
+                                // Negations are implicitly quantified.
+                                return false;
+                        }
+                }
+                var conjunction = EcoreUtil2.getContainerOfType(variable, Conjunction.class);
+                if (conjunction == null) {
+                        return true;
+                }
+                var variables = getExistsVariables(conjunction);
+                return !variables.contains(variable);
+        }
+
+        protected Set<Variable> getExistsVariables(Conjunction conjunction) {
+                var resource = conjunction.eResource();
+                if (resource == null) {
+                        return doGetExistsVariables(conjunction);
+                }
+                return cache.get(Tuples.create(conjunction, EXISTS_VARIABLES), resource,
+                                () -> doGetExistsVariables(conjunction));
+        }
+
+        protected Set<Variable> doGetExistsVariables(Conjunction conjunction) {
+                var builtinSymbols = importAdapterProvider.getBuiltinSymbols(conjunction);
+                var existsRelation = builtinSymbols.exists();
+                var set = new HashSet<Variable>();
+                for (var atom : EcoreUtil2.getAllContentsOfType(conjunction, Atom.class)) {
+                        if (existsRelation.equals(atom.getRelation())) {
+                                for (var argument : atom.getArguments()) {
+                                        if (argument instanceof VariableOrNodeExpr variableOrNodeExpr &&
+                                                        variableOrNodeExpr.getVariableOrNode() instanceof Variable variable) {
+                                                set.add(variable);
+                                        }
+                                }
+                        }
+                }
+                return set;
+        }
+}
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 754572d1..21dd7218 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
@@ -24,10 +24,7 @@ import tools.refinery.language.typesystem.ProblemTypeAnalyzer;
 import tools.refinery.language.typesystem.SignatureProvider;
 import tools.refinery.language.utils.ProblemUtil;
 
-import java.util.ArrayList;
-import java.util.LinkedHashMap;
-import java.util.LinkedHashSet;
-import java.util.Set;
+import java.util.*;
 
 /**
  * This class contains custom validation rules.
@@ -56,11 +53,15 @@ public class ProblemValidator extends AbstractProblemValidator {
         public static final String UNKNOWN_EXPRESSION_ISSUE = ISSUE_PREFIX + "UNKNOWN_EXPRESSION";
         public static final String INVALID_ASSIGNMENT_ISSUE = ISSUE_PREFIX + "INVALID_ASSIGNMENT";
         public static final String TYPE_ERROR = ISSUE_PREFIX + "TYPE_ERROR";
+        public static final String VARIABLE_WITHOUT_EXISTS = ISSUE_PREFIX + "VARIABLE_WITHOUT_EXISTS";
 
         @Inject
         private ReferenceCounter referenceCounter;
 
         @Inject
+        private ExistsVariableCollector existsVariableCollector;
+
+        @Inject
         private IQualifiedNameConverter qualifiedNameConverter;
 
         @Inject
@@ -129,6 +130,14 @@ public class ProblemValidator extends AbstractProblemValidator {
                 var variableOrNode = expr.getVariableOrNode();
                 if (variableOrNode instanceof Variable variable && ProblemUtil.isImplicitVariable(variable)
                                 && !ProblemUtil.isSingletonVariable(variable)) {
+                        if (EcoreUtil2.getContainerOfType(variable, ParametricDefinition.class) instanceof RuleDefinition &&
+                                        EcoreUtil2.getContainerOfType(variable, NegationExpr.class) == null &&
+                                        // If there is an exists constraint, it is the only constraint.
+                                        existsVariableCollector.missingExistsConstraint(variable)) {
+                                // Existentially quantified variables in rules should not be singletons,
+                                // because we have to add an {@code exists} constraint as well.
+                                return;
+                        }
                         var problem = EcoreUtil2.getContainerOfType(variable, Problem.class);
                         if (problem != null && referenceCounter.countReferences(problem, variable) <= 1) {
                                 var name = variable.getName();
@@ -412,6 +421,28 @@ public class ProblemValidator extends AbstractProblemValidator {
                         acceptError("Rules must have exactly one consequent.", ruleDefinition,
                                         ProblemPackage.Literals.NAMED_ELEMENT__NAME, 0, INVALID_RULE_ISSUE);
                 }
+                var unquantifiedVariables = new HashSet<Variable>();
+                for (var variable : EcoreUtil2.getAllContentsOfType(ruleDefinition, Variable.class)) {
+                        if (existsVariableCollector.missingExistsConstraint(variable)) {
+                                unquantifiedVariables.add(variable);
+                        }
+                }
+                for (var expr : EcoreUtil2.getAllContentsOfType(ruleDefinition, VariableOrNodeExpr.class)) {
+                        if (expr.getVariableOrNode() instanceof Variable variable && unquantifiedVariables.contains(variable)) {
+                                unquantifiedVariables.remove(variable);
+                                var name = variable.getName();
+                                String message;
+                                if (ProblemUtil.isSingletonVariable(variable)) {
+                                        message = ("Remove the singleton variable marker '_' and clarify the quantification of variable " +
+                            "'%s'.").formatted(name);
+                                } else {
+                                        message = ("Add a 'must exists(%s)', 'may exists(%s)', or 'may !exists(%s)' constraint to " +
+                                                        "clarify the quantification of variable '%s'.").formatted(name, name, name, name);
+                                }
+                                acceptWarning(message, expr, ProblemPackage.Literals.VARIABLE_OR_NODE_EXPR__VARIABLE_OR_NODE, 0,
+                                                VARIABLE_WITHOUT_EXISTS);
+                        }
+                }
         }
 
         @Check
diff --git a/subprojects/language/src/main/java/tools/refinery/language/validation/ReferenceCounter.java b/subprojects/language/src/main/java/tools/refinery/language/validation/ReferenceCounter.java
index 55cbd71d..40781168 100644
--- a/subprojects/language/src/main/java/tools/refinery/language/validation/ReferenceCounter.java
+++ b/subprojects/language/src/main/java/tools/refinery/language/validation/ReferenceCounter.java
@@ -5,20 +5,21 @@
  */
 package tools.refinery.language.validation;
 
-import java.util.HashMap;
-import java.util.Map;
-
+import com.google.inject.Inject;
+import com.google.inject.Singleton;
 import org.eclipse.emf.ecore.EObject;
 import org.eclipse.xtext.util.IResourceScopeCache;
 import org.eclipse.xtext.util.Tuples;
-
-import com.google.inject.Inject;
-import com.google.inject.Singleton;
-
 import tools.refinery.language.model.problem.Problem;
 
+import java.util.HashMap;
+import java.util.Map;
+
 @Singleton
 public class ReferenceCounter {
+        private static final String REFERENCE_COUNTS =
+                        "tools.refinery.language.validation.ReferenceCounter.REFERENCE_COUNTS";
+
         @Inject
         private IResourceScopeCache cache = IResourceScopeCache.NullImpl.INSTANCE;
 
@@ -35,7 +36,7 @@ public class ReferenceCounter {
                 if (resource == null) {
                         return doGetReferenceCounts(problem);
                 }
-                return cache.get(Tuples.create(problem, "referenceCounts"), resource, () -> doGetReferenceCounts(problem));
+                return cache.get(Tuples.create(problem, REFERENCE_COUNTS), resource, () -> doGetReferenceCounts(problem));
         }
 
         protected Map<EObject, Integer> doGetReferenceCounts(Problem problem) {