diff options
author | 2024-06-16 23:24:09 +0200 | |
---|---|---|
committer | 2024-06-16 23:24:09 +0200 | |
commit | c2907e921954749a8c22899ef4542b4b8db44c42 (patch) | |
tree | a83585db1dcdfc320f957657a8cf99f85420182b /subprojects/language/src/main/java/tools | |
parent | build: publish CLI as Docker container (diff) | |
download | refinery-c2907e921954749a8c22899ef4542b4b8db44c42.tar.gz refinery-c2907e921954749a8c22899ef4542b4b8db44c42.tar.zst refinery-c2907e921954749a8c22899ef4542b4b8db44c42.zip |
feat(language): validate quantification in rules
Diffstat (limited to 'subprojects/language/src/main/java/tools')
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 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2024 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.language.validation; | ||
7 | |||
8 | import com.google.inject.Inject; | ||
9 | import com.google.inject.Singleton; | ||
10 | import org.eclipse.xtext.EcoreUtil2; | ||
11 | import org.eclipse.xtext.util.IResourceScopeCache; | ||
12 | import org.eclipse.xtext.util.Tuples; | ||
13 | import tools.refinery.language.model.problem.*; | ||
14 | import tools.refinery.language.scoping.imports.ImportAdapterProvider; | ||
15 | import tools.refinery.language.utils.ProblemUtil; | ||
16 | |||
17 | import java.util.HashSet; | ||
18 | import java.util.Set; | ||
19 | |||
20 | @Singleton | ||
21 | public class ExistsVariableCollector { | ||
22 | private static final String EXISTS_VARIABLES = | ||
23 | "tools.refinery.language.validation.ExistsVariableCollector.EXISTS_VARIABLES"; | ||
24 | |||
25 | @Inject | ||
26 | private IResourceScopeCache cache = IResourceScopeCache.NullImpl.INSTANCE; | ||
27 | |||
28 | @Inject | ||
29 | private ImportAdapterProvider importAdapterProvider; | ||
30 | |||
31 | public boolean missingExistsConstraint(Variable variable) { | ||
32 | if (variable instanceof Parameter) { | ||
33 | return false; | ||
34 | } | ||
35 | if (ProblemUtil.isImplicitVariable(variable)) { | ||
36 | var negation = EcoreUtil2.getContainerOfType(variable, NegationExpr.class); | ||
37 | if (negation != null) { | ||
38 | // Negations are implicitly quantified. | ||
39 | return false; | ||
40 | } | ||
41 | } | ||
42 | var conjunction = EcoreUtil2.getContainerOfType(variable, Conjunction.class); | ||
43 | if (conjunction == null) { | ||
44 | return true; | ||
45 | } | ||
46 | var variables = getExistsVariables(conjunction); | ||
47 | return !variables.contains(variable); | ||
48 | } | ||
49 | |||
50 | protected Set<Variable> getExistsVariables(Conjunction conjunction) { | ||
51 | var resource = conjunction.eResource(); | ||
52 | if (resource == null) { | ||
53 | return doGetExistsVariables(conjunction); | ||
54 | } | ||
55 | return cache.get(Tuples.create(conjunction, EXISTS_VARIABLES), resource, | ||
56 | () -> doGetExistsVariables(conjunction)); | ||
57 | } | ||
58 | |||
59 | protected Set<Variable> doGetExistsVariables(Conjunction conjunction) { | ||
60 | var builtinSymbols = importAdapterProvider.getBuiltinSymbols(conjunction); | ||
61 | var existsRelation = builtinSymbols.exists(); | ||
62 | var set = new HashSet<Variable>(); | ||
63 | for (var atom : EcoreUtil2.getAllContentsOfType(conjunction, Atom.class)) { | ||
64 | if (existsRelation.equals(atom.getRelation())) { | ||
65 | for (var argument : atom.getArguments()) { | ||
66 | if (argument instanceof VariableOrNodeExpr variableOrNodeExpr && | ||
67 | variableOrNodeExpr.getVariableOrNode() instanceof Variable variable) { | ||
68 | set.add(variable); | ||
69 | } | ||
70 | } | ||
71 | } | ||
72 | } | ||
73 | return set; | ||
74 | } | ||
75 | } | ||
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; | |||
24 | import tools.refinery.language.typesystem.SignatureProvider; | 24 | import tools.refinery.language.typesystem.SignatureProvider; |
25 | import tools.refinery.language.utils.ProblemUtil; | 25 | import tools.refinery.language.utils.ProblemUtil; |
26 | 26 | ||
27 | import java.util.ArrayList; | 27 | import java.util.*; |
28 | import java.util.LinkedHashMap; | ||
29 | import java.util.LinkedHashSet; | ||
30 | import java.util.Set; | ||
31 | 28 | ||
32 | /** | 29 | /** |
33 | * This class contains custom validation rules. | 30 | * This class contains custom validation rules. |
@@ -56,11 +53,15 @@ public class ProblemValidator extends AbstractProblemValidator { | |||
56 | public static final String UNKNOWN_EXPRESSION_ISSUE = ISSUE_PREFIX + "UNKNOWN_EXPRESSION"; | 53 | public static final String UNKNOWN_EXPRESSION_ISSUE = ISSUE_PREFIX + "UNKNOWN_EXPRESSION"; |
57 | public static final String INVALID_ASSIGNMENT_ISSUE = ISSUE_PREFIX + "INVALID_ASSIGNMENT"; | 54 | public static final String INVALID_ASSIGNMENT_ISSUE = ISSUE_PREFIX + "INVALID_ASSIGNMENT"; |
58 | public static final String TYPE_ERROR = ISSUE_PREFIX + "TYPE_ERROR"; | 55 | public static final String TYPE_ERROR = ISSUE_PREFIX + "TYPE_ERROR"; |
56 | public static final String VARIABLE_WITHOUT_EXISTS = ISSUE_PREFIX + "VARIABLE_WITHOUT_EXISTS"; | ||
59 | 57 | ||
60 | @Inject | 58 | @Inject |
61 | private ReferenceCounter referenceCounter; | 59 | private ReferenceCounter referenceCounter; |
62 | 60 | ||
63 | @Inject | 61 | @Inject |
62 | private ExistsVariableCollector existsVariableCollector; | ||
63 | |||
64 | @Inject | ||
64 | private IQualifiedNameConverter qualifiedNameConverter; | 65 | private IQualifiedNameConverter qualifiedNameConverter; |
65 | 66 | ||
66 | @Inject | 67 | @Inject |
@@ -129,6 +130,14 @@ public class ProblemValidator extends AbstractProblemValidator { | |||
129 | var variableOrNode = expr.getVariableOrNode(); | 130 | var variableOrNode = expr.getVariableOrNode(); |
130 | if (variableOrNode instanceof Variable variable && ProblemUtil.isImplicitVariable(variable) | 131 | if (variableOrNode instanceof Variable variable && ProblemUtil.isImplicitVariable(variable) |
131 | && !ProblemUtil.isSingletonVariable(variable)) { | 132 | && !ProblemUtil.isSingletonVariable(variable)) { |
133 | if (EcoreUtil2.getContainerOfType(variable, ParametricDefinition.class) instanceof RuleDefinition && | ||
134 | EcoreUtil2.getContainerOfType(variable, NegationExpr.class) == null && | ||
135 | // If there is an exists constraint, it is the only constraint. | ||
136 | existsVariableCollector.missingExistsConstraint(variable)) { | ||
137 | // Existentially quantified variables in rules should not be singletons, | ||
138 | // because we have to add an {@code exists} constraint as well. | ||
139 | return; | ||
140 | } | ||
132 | var problem = EcoreUtil2.getContainerOfType(variable, Problem.class); | 141 | var problem = EcoreUtil2.getContainerOfType(variable, Problem.class); |
133 | if (problem != null && referenceCounter.countReferences(problem, variable) <= 1) { | 142 | if (problem != null && referenceCounter.countReferences(problem, variable) <= 1) { |
134 | var name = variable.getName(); | 143 | var name = variable.getName(); |
@@ -412,6 +421,28 @@ public class ProblemValidator extends AbstractProblemValidator { | |||
412 | acceptError("Rules must have exactly one consequent.", ruleDefinition, | 421 | acceptError("Rules must have exactly one consequent.", ruleDefinition, |
413 | ProblemPackage.Literals.NAMED_ELEMENT__NAME, 0, INVALID_RULE_ISSUE); | 422 | ProblemPackage.Literals.NAMED_ELEMENT__NAME, 0, INVALID_RULE_ISSUE); |
414 | } | 423 | } |
424 | var unquantifiedVariables = new HashSet<Variable>(); | ||
425 | for (var variable : EcoreUtil2.getAllContentsOfType(ruleDefinition, Variable.class)) { | ||
426 | if (existsVariableCollector.missingExistsConstraint(variable)) { | ||
427 | unquantifiedVariables.add(variable); | ||
428 | } | ||
429 | } | ||
430 | for (var expr : EcoreUtil2.getAllContentsOfType(ruleDefinition, VariableOrNodeExpr.class)) { | ||
431 | if (expr.getVariableOrNode() instanceof Variable variable && unquantifiedVariables.contains(variable)) { | ||
432 | unquantifiedVariables.remove(variable); | ||
433 | var name = variable.getName(); | ||
434 | String message; | ||
435 | if (ProblemUtil.isSingletonVariable(variable)) { | ||
436 | message = ("Remove the singleton variable marker '_' and clarify the quantification of variable " + | ||
437 | "'%s'.").formatted(name); | ||
438 | } else { | ||
439 | message = ("Add a 'must exists(%s)', 'may exists(%s)', or 'may !exists(%s)' constraint to " + | ||
440 | "clarify the quantification of variable '%s'.").formatted(name, name, name, name); | ||
441 | } | ||
442 | acceptWarning(message, expr, ProblemPackage.Literals.VARIABLE_OR_NODE_EXPR__VARIABLE_OR_NODE, 0, | ||
443 | VARIABLE_WITHOUT_EXISTS); | ||
444 | } | ||
445 | } | ||
415 | } | 446 | } |
416 | 447 | ||
417 | @Check | 448 | @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 @@ | |||
5 | */ | 5 | */ |
6 | package tools.refinery.language.validation; | 6 | package tools.refinery.language.validation; |
7 | 7 | ||
8 | import java.util.HashMap; | 8 | import com.google.inject.Inject; |
9 | import java.util.Map; | 9 | import com.google.inject.Singleton; |
10 | |||
11 | import org.eclipse.emf.ecore.EObject; | 10 | import org.eclipse.emf.ecore.EObject; |
12 | import org.eclipse.xtext.util.IResourceScopeCache; | 11 | import org.eclipse.xtext.util.IResourceScopeCache; |
13 | import org.eclipse.xtext.util.Tuples; | 12 | import org.eclipse.xtext.util.Tuples; |
14 | |||
15 | import com.google.inject.Inject; | ||
16 | import com.google.inject.Singleton; | ||
17 | |||
18 | import tools.refinery.language.model.problem.Problem; | 13 | import tools.refinery.language.model.problem.Problem; |
19 | 14 | ||
15 | import java.util.HashMap; | ||
16 | import java.util.Map; | ||
17 | |||
20 | @Singleton | 18 | @Singleton |
21 | public class ReferenceCounter { | 19 | public class ReferenceCounter { |
20 | private static final String REFERENCE_COUNTS = | ||
21 | "tools.refinery.language.validation.ReferenceCounter.REFERENCE_COUNTS"; | ||
22 | |||
22 | @Inject | 23 | @Inject |
23 | private IResourceScopeCache cache = IResourceScopeCache.NullImpl.INSTANCE; | 24 | private IResourceScopeCache cache = IResourceScopeCache.NullImpl.INSTANCE; |
24 | 25 | ||
@@ -35,7 +36,7 @@ public class ReferenceCounter { | |||
35 | if (resource == null) { | 36 | if (resource == null) { |
36 | return doGetReferenceCounts(problem); | 37 | return doGetReferenceCounts(problem); |
37 | } | 38 | } |
38 | return cache.get(Tuples.create(problem, "referenceCounts"), resource, () -> doGetReferenceCounts(problem)); | 39 | return cache.get(Tuples.create(problem, REFERENCE_COUNTS), resource, () -> doGetReferenceCounts(problem)); |
39 | } | 40 | } |
40 | 41 | ||
41 | protected Map<EObject, Integer> doGetReferenceCounts(Problem problem) { | 42 | protected Map<EObject, Integer> doGetReferenceCounts(Problem problem) { |