From c2907e921954749a8c22899ef4542b4b8db44c42 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Sun, 16 Jun 2024 23:24:09 +0200 Subject: feat(language): validate quantification in rules --- .../validation/ExistsVariableCollector.java | 75 ++++++++++++++++++++++ .../language/validation/ProblemValidator.java | 39 +++++++++-- .../language/validation/ReferenceCounter.java | 17 ++--- 3 files changed, 119 insertions(+), 12 deletions(-) create mode 100644 subprojects/language/src/main/java/tools/refinery/language/validation/ExistsVariableCollector.java 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 + * + * 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 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 doGetExistsVariables(Conjunction conjunction) { + var builtinSymbols = importAdapterProvider.getBuiltinSymbols(conjunction); + var existsRelation = builtinSymbols.exists(); + var set = new HashSet(); + 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,10 +53,14 @@ 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; @@ -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(); + 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 doGetReferenceCounts(Problem problem) { -- cgit v1.2.3-54-g00ecf