refactor: incomplete query lifting

* Allow specifying only the modality or only the concreteness of constraints in
  the DNF representation.
* Allow modal operators in the Refinery language that only specific modality or
  concreteness.
* Allow modal operators in shadow predicates.
* Allow non-modal literals in rule definitions.
* Lift rule definitions to partial must automatically.
* Disallow modal operators in parameter lists.
* Change the symbols for parameter binding modes.

4 files changed, 11 insertions, 131 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 cca94e66..3a897cc0 100644
--- a/subprojects/language/src/main/java/tools/refinery/language/Problem.xtext
+++ b/subprojects/language/src/main/java/tools/refinery/language/Problem.xtext
@@ -89,13 +89,10 @@ RuleDefinition:
         ".";
 
 enum ParameterBinding:
-        FOCUS="&" | MULTI="*";
+        FOCUS="+" | MULTI="?";
 
 Parameter:
-        (
-                (concreteness=Concreteness? modality=Modality)?
-                parameterType=[Relation|QualifiedName]
-        )? binding=ParameterBinding? name=Identifier;
+        parameterType=[Relation|QualifiedName]? binding=ParameterBinding? name=Identifier;
 
 Consequent:
         actions+=Action ("," actions+=Action)*;
@@ -184,14 +181,14 @@ AggregationExpr:
         "{" value=Expr "|" condition=ComparisonExpr "}";
 
 enum Concreteness:
-        CANDIDATE="candidate";
+        PARTIAL="partial" | CANDIDATE="candidate";
 
 enum Modality:
         MUST="must" | MAY="may";
 
 ModalExpr:
-        concreteness=Concreteness?
-        modality=Modality body=UnaryExpr;
+        (concreteness=Concreteness => modality=Modality? | modality=Modality)
+        body=UnaryExpr;
 
 CastExpr returns Expr:
         CastExprBody ({CastExpr.body=current} "as" targetType=[Relation|QualifiedName])?;
diff --git a/subprojects/language/src/main/java/tools/refinery/language/typesystem/TypedModule.java b/subprojects/language/src/main/java/tools/refinery/language/typesystem/TypedModule.java
index 63815506..f1e5a7ac 100644
--- a/subprojects/language/src/main/java/tools/refinery/language/typesystem/TypedModule.java
+++ b/subprojects/language/src/main/java/tools/refinery/language/typesystem/TypedModule.java
@@ -75,7 +75,7 @@ public class TypedModule {
         private void checkTypes(PredicateDefinition predicateDefinition) {
                 for (var conjunction : predicateDefinition.getBodies()) {
                         for (var literal : conjunction.getLiterals()) {
-                                coerceIntoLiteral(literal);
+                                coerceIntoLiteral(literal, predicateDefinition.isShadow());
                         }
                 }
         }
@@ -83,7 +83,7 @@ public class TypedModule {
         private void checkTypes(RuleDefinition ruleDefinition) {
                 for (var conjunction : ruleDefinition.getPreconditions()) {
                         for (var literal : conjunction.getLiterals()) {
-                                expectType(literal, ExprType.MODAL_LITERAL);
+                                coerceIntoLiteral(literal, true);
                         }
                 }
                 for (var consequent : ruleDefinition.getConsequents()) {
@@ -393,7 +393,7 @@ public class TypedModule {
 
         @NotNull
         private ExprType computeExpressionType(CountExpr countExpr) {
-                return coerceIntoLiteral(countExpr.getBody()) ? BuiltinTermInterpreter.INT_TYPE : ExprType.INVALID;
+                return coerceIntoLiteral(countExpr.getBody(), false) ? BuiltinTermInterpreter.INT_TYPE : ExprType.INVALID;
         }
 
         @NotNull
@@ -403,7 +403,7 @@ public class TypedModule {
                         return ExprType.INVALID;
                 }
                 // Avoid short-circuiting to let us type check both the value and the condition.
-                boolean ok = coerceIntoLiteral(expr.getCondition());
+                boolean ok = coerceIntoLiteral(expr.getCondition(), false);
                 var value = expr.getValue();
                 var actualType = getExpressionType(value);
                 if (actualType == ExprType.INVALID) {
@@ -617,12 +617,12 @@ public class TypedModule {
                 }
         }
 
-        private boolean coerceIntoLiteral(Expr expr) {
+        private boolean coerceIntoLiteral(Expr expr, boolean allowModal) {
                 if (expr == null) {
                         return false;
                 }
                 var actualType = getExpressionType(expr);
-                if (actualType == ExprType.LITERAL) {
+                if (actualType == ExprType.LITERAL || (allowModal && actualType == ExprType.MODAL_LITERAL)) {
                         return true;
                 }
                 return expectType(expr, actualType, BuiltinTermInterpreter.BOOLEAN_TYPE);
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
deleted file mode 100644
index 5812bdc4..00000000
--- a/subprojects/language/src/main/java/tools/refinery/language/validation/ExistsVariableCollector.java
+++ /dev/null
@@ -1,75 +0,0 @@
-/*
- * 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 58d86fa0..343340bd 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
@@ -54,7 +54,6 @@ 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";
         public static final String UNUSED_PARTIAL_RELATION = ISSUE_PREFIX + "UNUSED_PARTIAL_RELATION";
         public static final String UNUSED_PARAMETER = ISSUE_PREFIX + "UNUSED_PARAMETER";
 
@@ -62,9 +61,6 @@ public class ProblemValidator extends AbstractProblemValidator {
         private ReferenceCounter referenceCounter;
 
         @Inject
-        private ExistsVariableCollector existsVariableCollector;
-
-        @Inject
         private ActionTargetCollector actionTargetCollector;
 
         @Inject
@@ -136,14 +132,6 @@ 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();
@@ -391,10 +379,6 @@ public class ProblemValidator extends AbstractProblemValidator {
                 checkArity(parameter, ProblemPackage.Literals.PARAMETER__PARAMETER_TYPE, 1);
                 var parametricDefinition = EcoreUtil2.getContainerOfType(parameter, ParametricDefinition.class);
                 if (parametricDefinition instanceof RuleDefinition rule) {
-                        if (parameter.getParameterType() != null && parameter.getModality() == Modality.NONE) {
-                                acceptError("Parameter type modality must be specified.", parameter,
-                                                ProblemPackage.Literals.PARAMETER__PARAMETER_TYPE, 0, INVALID_MODALITY_ISSUE);
-                        }
                         var kind = rule.getKind();
                         var binding = parameter.getBinding();
                         if (kind == RuleKind.PROPAGATION && binding != ParameterBinding.SINGLE) {
@@ -405,10 +389,6 @@ public class ProblemValidator extends AbstractProblemValidator {
                                                 ProblemPackage.Literals.PARAMETER__BINDING, 0, INVALID_MODALITY_ISSUE);
                         }
                 } else {
-                        if (parameter.getConcreteness() != Concreteness.PARTIAL || parameter.getModality() != Modality.NONE) {
-                                acceptError("Modal parameter types are only supported in rule definitions.", parameter, null, 0,
-                                                INVALID_MODALITY_ISSUE);
-                        }
                         if (parameter.getBinding() != ParameterBinding.SINGLE) {
                                 acceptError("Parameter binding annotations are only supported in decision rules.", parameter,
                                                 ProblemPackage.PARAMETER__BINDING, 0, INVALID_MODALITY_ISSUE);
@@ -442,28 +422,6 @@ 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