diff options
author | 2024-07-01 21:53:06 +0200 | |
---|---|---|
committer | 2024-07-01 21:53:06 +0200 | |
commit | f9936245c2a0b23f50da85b5f660f1b576d87eed (patch) | |
tree | c7bac2c796e7570499bbc7693bc4805c6c36a2cb /subprojects/language/src/main/java/tools | |
parent | refactor(language): shadow predicates instead of computed value operator (diff) | |
download | refinery-f9936245c2a0b23f50da85b5f660f1b576d87eed.tar.gz refinery-f9936245c2a0b23f50da85b5f660f1b576d87eed.tar.zst refinery-f9936245c2a0b23f50da85b5f660f1b576d87eed.zip |
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.
Diffstat (limited to 'subprojects/language/src/main/java/tools')
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: | |||
89 | "."; | 89 | "."; |
90 | 90 | ||
91 | enum ParameterBinding: | 91 | enum ParameterBinding: |
92 | FOCUS="&" | MULTI="*"; | 92 | FOCUS="+" | MULTI="?"; |
93 | 93 | ||
94 | Parameter: | 94 | Parameter: |
95 | ( | 95 | parameterType=[Relation|QualifiedName]? binding=ParameterBinding? name=Identifier; |
96 | (concreteness=Concreteness? modality=Modality)? | ||
97 | parameterType=[Relation|QualifiedName] | ||
98 | )? binding=ParameterBinding? name=Identifier; | ||
99 | 96 | ||
100 | Consequent: | 97 | Consequent: |
101 | actions+=Action ("," actions+=Action)*; | 98 | actions+=Action ("," actions+=Action)*; |
@@ -184,14 +181,14 @@ AggregationExpr: | |||
184 | "{" value=Expr "|" condition=ComparisonExpr "}"; | 181 | "{" value=Expr "|" condition=ComparisonExpr "}"; |
185 | 182 | ||
186 | enum Concreteness: | 183 | enum Concreteness: |
187 | CANDIDATE="candidate"; | 184 | PARTIAL="partial" | CANDIDATE="candidate"; |
188 | 185 | ||
189 | enum Modality: | 186 | enum Modality: |
190 | MUST="must" | MAY="may"; | 187 | MUST="must" | MAY="may"; |
191 | 188 | ||
192 | ModalExpr: | 189 | ModalExpr: |
193 | concreteness=Concreteness? | 190 | (concreteness=Concreteness => modality=Modality? | modality=Modality) |
194 | modality=Modality body=UnaryExpr; | 191 | body=UnaryExpr; |
195 | 192 | ||
196 | CastExpr returns Expr: | 193 | CastExpr returns Expr: |
197 | CastExprBody ({CastExpr.body=current} "as" targetType=[Relation|QualifiedName])?; | 194 | 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 { | |||
75 | private void checkTypes(PredicateDefinition predicateDefinition) { | 75 | private void checkTypes(PredicateDefinition predicateDefinition) { |
76 | for (var conjunction : predicateDefinition.getBodies()) { | 76 | for (var conjunction : predicateDefinition.getBodies()) { |
77 | for (var literal : conjunction.getLiterals()) { | 77 | for (var literal : conjunction.getLiterals()) { |
78 | coerceIntoLiteral(literal); | 78 | coerceIntoLiteral(literal, predicateDefinition.isShadow()); |
79 | } | 79 | } |
80 | } | 80 | } |
81 | } | 81 | } |
@@ -83,7 +83,7 @@ public class TypedModule { | |||
83 | private void checkTypes(RuleDefinition ruleDefinition) { | 83 | private void checkTypes(RuleDefinition ruleDefinition) { |
84 | for (var conjunction : ruleDefinition.getPreconditions()) { | 84 | for (var conjunction : ruleDefinition.getPreconditions()) { |
85 | for (var literal : conjunction.getLiterals()) { | 85 | for (var literal : conjunction.getLiterals()) { |
86 | expectType(literal, ExprType.MODAL_LITERAL); | 86 | coerceIntoLiteral(literal, true); |
87 | } | 87 | } |
88 | } | 88 | } |
89 | for (var consequent : ruleDefinition.getConsequents()) { | 89 | for (var consequent : ruleDefinition.getConsequents()) { |
@@ -393,7 +393,7 @@ public class TypedModule { | |||
393 | 393 | ||
394 | @NotNull | 394 | @NotNull |
395 | private ExprType computeExpressionType(CountExpr countExpr) { | 395 | private ExprType computeExpressionType(CountExpr countExpr) { |
396 | return coerceIntoLiteral(countExpr.getBody()) ? BuiltinTermInterpreter.INT_TYPE : ExprType.INVALID; | 396 | return coerceIntoLiteral(countExpr.getBody(), false) ? BuiltinTermInterpreter.INT_TYPE : ExprType.INVALID; |
397 | } | 397 | } |
398 | 398 | ||
399 | @NotNull | 399 | @NotNull |
@@ -403,7 +403,7 @@ public class TypedModule { | |||
403 | return ExprType.INVALID; | 403 | return ExprType.INVALID; |
404 | } | 404 | } |
405 | // Avoid short-circuiting to let us type check both the value and the condition. | 405 | // Avoid short-circuiting to let us type check both the value and the condition. |
406 | boolean ok = coerceIntoLiteral(expr.getCondition()); | 406 | boolean ok = coerceIntoLiteral(expr.getCondition(), false); |
407 | var value = expr.getValue(); | 407 | var value = expr.getValue(); |
408 | var actualType = getExpressionType(value); | 408 | var actualType = getExpressionType(value); |
409 | if (actualType == ExprType.INVALID) { | 409 | if (actualType == ExprType.INVALID) { |
@@ -617,12 +617,12 @@ public class TypedModule { | |||
617 | } | 617 | } |
618 | } | 618 | } |
619 | 619 | ||
620 | private boolean coerceIntoLiteral(Expr expr) { | 620 | private boolean coerceIntoLiteral(Expr expr, boolean allowModal) { |
621 | if (expr == null) { | 621 | if (expr == null) { |
622 | return false; | 622 | return false; |
623 | } | 623 | } |
624 | var actualType = getExpressionType(expr); | 624 | var actualType = getExpressionType(expr); |
625 | if (actualType == ExprType.LITERAL) { | 625 | if (actualType == ExprType.LITERAL || (allowModal && actualType == ExprType.MODAL_LITERAL)) { |
626 | return true; | 626 | return true; |
627 | } | 627 | } |
628 | return expectType(expr, actualType, BuiltinTermInterpreter.BOOLEAN_TYPE); | 628 | 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 @@ | |||
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 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 { | |||
54 | public static final String UNKNOWN_EXPRESSION_ISSUE = ISSUE_PREFIX + "UNKNOWN_EXPRESSION"; | 54 | public static final String UNKNOWN_EXPRESSION_ISSUE = ISSUE_PREFIX + "UNKNOWN_EXPRESSION"; |
55 | public static final String INVALID_ASSIGNMENT_ISSUE = ISSUE_PREFIX + "INVALID_ASSIGNMENT"; | 55 | public static final String INVALID_ASSIGNMENT_ISSUE = ISSUE_PREFIX + "INVALID_ASSIGNMENT"; |
56 | public static final String TYPE_ERROR = ISSUE_PREFIX + "TYPE_ERROR"; | 56 | public static final String TYPE_ERROR = ISSUE_PREFIX + "TYPE_ERROR"; |
57 | public static final String VARIABLE_WITHOUT_EXISTS = ISSUE_PREFIX + "VARIABLE_WITHOUT_EXISTS"; | ||
58 | public static final String UNUSED_PARTIAL_RELATION = ISSUE_PREFIX + "UNUSED_PARTIAL_RELATION"; | 57 | public static final String UNUSED_PARTIAL_RELATION = ISSUE_PREFIX + "UNUSED_PARTIAL_RELATION"; |
59 | public static final String UNUSED_PARAMETER = ISSUE_PREFIX + "UNUSED_PARAMETER"; | 58 | public static final String UNUSED_PARAMETER = ISSUE_PREFIX + "UNUSED_PARAMETER"; |
60 | 59 | ||
@@ -62,9 +61,6 @@ public class ProblemValidator extends AbstractProblemValidator { | |||
62 | private ReferenceCounter referenceCounter; | 61 | private ReferenceCounter referenceCounter; |
63 | 62 | ||
64 | @Inject | 63 | @Inject |
65 | private ExistsVariableCollector existsVariableCollector; | ||
66 | |||
67 | @Inject | ||
68 | private ActionTargetCollector actionTargetCollector; | 64 | private ActionTargetCollector actionTargetCollector; |
69 | 65 | ||
70 | @Inject | 66 | @Inject |
@@ -136,14 +132,6 @@ public class ProblemValidator extends AbstractProblemValidator { | |||
136 | var variableOrNode = expr.getVariableOrNode(); | 132 | var variableOrNode = expr.getVariableOrNode(); |
137 | if (variableOrNode instanceof Variable variable && ProblemUtil.isImplicitVariable(variable) | 133 | if (variableOrNode instanceof Variable variable && ProblemUtil.isImplicitVariable(variable) |
138 | && !ProblemUtil.isSingletonVariable(variable)) { | 134 | && !ProblemUtil.isSingletonVariable(variable)) { |
139 | if (EcoreUtil2.getContainerOfType(variable, ParametricDefinition.class) instanceof RuleDefinition && | ||
140 | EcoreUtil2.getContainerOfType(variable, NegationExpr.class) == null && | ||
141 | // If there is an exists constraint, it is the only constraint. | ||
142 | existsVariableCollector.missingExistsConstraint(variable)) { | ||
143 | // Existentially quantified variables in rules should not be singletons, | ||
144 | // because we have to add an {@code exists} constraint as well. | ||
145 | return; | ||
146 | } | ||
147 | var problem = EcoreUtil2.getContainerOfType(variable, Problem.class); | 135 | var problem = EcoreUtil2.getContainerOfType(variable, Problem.class); |
148 | if (problem != null && referenceCounter.countReferences(problem, variable) <= 1) { | 136 | if (problem != null && referenceCounter.countReferences(problem, variable) <= 1) { |
149 | var name = variable.getName(); | 137 | var name = variable.getName(); |
@@ -391,10 +379,6 @@ public class ProblemValidator extends AbstractProblemValidator { | |||
391 | checkArity(parameter, ProblemPackage.Literals.PARAMETER__PARAMETER_TYPE, 1); | 379 | checkArity(parameter, ProblemPackage.Literals.PARAMETER__PARAMETER_TYPE, 1); |
392 | var parametricDefinition = EcoreUtil2.getContainerOfType(parameter, ParametricDefinition.class); | 380 | var parametricDefinition = EcoreUtil2.getContainerOfType(parameter, ParametricDefinition.class); |
393 | if (parametricDefinition instanceof RuleDefinition rule) { | 381 | if (parametricDefinition instanceof RuleDefinition rule) { |
394 | if (parameter.getParameterType() != null && parameter.getModality() == Modality.NONE) { | ||
395 | acceptError("Parameter type modality must be specified.", parameter, | ||
396 | ProblemPackage.Literals.PARAMETER__PARAMETER_TYPE, 0, INVALID_MODALITY_ISSUE); | ||
397 | } | ||
398 | var kind = rule.getKind(); | 382 | var kind = rule.getKind(); |
399 | var binding = parameter.getBinding(); | 383 | var binding = parameter.getBinding(); |
400 | if (kind == RuleKind.PROPAGATION && binding != ParameterBinding.SINGLE) { | 384 | if (kind == RuleKind.PROPAGATION && binding != ParameterBinding.SINGLE) { |
@@ -405,10 +389,6 @@ public class ProblemValidator extends AbstractProblemValidator { | |||
405 | ProblemPackage.Literals.PARAMETER__BINDING, 0, INVALID_MODALITY_ISSUE); | 389 | ProblemPackage.Literals.PARAMETER__BINDING, 0, INVALID_MODALITY_ISSUE); |
406 | } | 390 | } |
407 | } else { | 391 | } else { |
408 | if (parameter.getConcreteness() != Concreteness.PARTIAL || parameter.getModality() != Modality.NONE) { | ||
409 | acceptError("Modal parameter types are only supported in rule definitions.", parameter, null, 0, | ||
410 | INVALID_MODALITY_ISSUE); | ||
411 | } | ||
412 | if (parameter.getBinding() != ParameterBinding.SINGLE) { | 392 | if (parameter.getBinding() != ParameterBinding.SINGLE) { |
413 | acceptError("Parameter binding annotations are only supported in decision rules.", parameter, | 393 | acceptError("Parameter binding annotations are only supported in decision rules.", parameter, |
414 | ProblemPackage.PARAMETER__BINDING, 0, INVALID_MODALITY_ISSUE); | 394 | ProblemPackage.PARAMETER__BINDING, 0, INVALID_MODALITY_ISSUE); |
@@ -442,28 +422,6 @@ public class ProblemValidator extends AbstractProblemValidator { | |||
442 | acceptError("Rules must have exactly one consequent.", ruleDefinition, | 422 | acceptError("Rules must have exactly one consequent.", ruleDefinition, |
443 | ProblemPackage.Literals.NAMED_ELEMENT__NAME, 0, INVALID_RULE_ISSUE); | 423 | ProblemPackage.Literals.NAMED_ELEMENT__NAME, 0, INVALID_RULE_ISSUE); |
444 | } | 424 | } |
445 | var unquantifiedVariables = new HashSet<Variable>(); | ||
446 | for (var variable : EcoreUtil2.getAllContentsOfType(ruleDefinition, Variable.class)) { | ||
447 | if (existsVariableCollector.missingExistsConstraint(variable)) { | ||
448 | unquantifiedVariables.add(variable); | ||
449 | } | ||
450 | } | ||
451 | for (var expr : EcoreUtil2.getAllContentsOfType(ruleDefinition, VariableOrNodeExpr.class)) { | ||
452 | if (expr.getVariableOrNode() instanceof Variable variable && unquantifiedVariables.contains(variable)) { | ||
453 | unquantifiedVariables.remove(variable); | ||
454 | var name = variable.getName(); | ||
455 | String message; | ||
456 | if (ProblemUtil.isSingletonVariable(variable)) { | ||
457 | message = ("Remove the singleton variable marker '_' and clarify the quantification of variable " + | ||
458 | "'%s'.").formatted(name); | ||
459 | } else { | ||
460 | message = ("Add a 'must exists(%s)', 'may exists(%s)', or 'may !exists(%s)' constraint to " + | ||
461 | "clarify the quantification of variable '%s'.").formatted(name, name, name, name); | ||
462 | } | ||
463 | acceptWarning(message, expr, ProblemPackage.Literals.VARIABLE_OR_NODE_EXPR__VARIABLE_OR_NODE, 0, | ||
464 | VARIABLE_WITHOUT_EXISTS); | ||
465 | } | ||
466 | } | ||
467 | } | 425 | } |
468 | 426 | ||
469 | @Check | 427 | @Check |