diff options
author | Kristóf Marussy <kristof@marussy.com> | 2024-05-17 17:58:15 +0200 |
---|---|---|
committer | Kristóf Marussy <kristof@marussy.com> | 2024-05-26 17:22:32 +0200 |
commit | 638566514e6c75d4677a692cb463ff87ef8caf21 (patch) | |
tree | 5fa6e1e1d2784502aeb16fa02d45a2c711f66db2 /subprojects | |
parent | feat: rule parsing (diff) | |
download | refinery-638566514e6c75d4677a692cb463ff87ef8caf21.tar.gz refinery-638566514e6c75d4677a692cb463ff87ef8caf21.tar.zst refinery-638566514e6c75d4677a692cb463ff87ef8caf21.zip |
feat: type checking for rules
Diffstat (limited to 'subprojects')
4 files changed, 102 insertions, 2 deletions
diff --git a/subprojects/language/src/main/java/tools/refinery/language/typesystem/ExprType.java b/subprojects/language/src/main/java/tools/refinery/language/typesystem/ExprType.java index 9e44063d..65721924 100644 --- a/subprojects/language/src/main/java/tools/refinery/language/typesystem/ExprType.java +++ b/subprojects/language/src/main/java/tools/refinery/language/typesystem/ExprType.java | |||
@@ -8,6 +8,7 @@ package tools.refinery.language.typesystem; | |||
8 | public sealed interface ExprType permits FixedType, MutableType { | 8 | public sealed interface ExprType permits FixedType, MutableType { |
9 | NodeType NODE = new NodeType(); | 9 | NodeType NODE = new NodeType(); |
10 | LiteralType LITERAL = new LiteralType(); | 10 | LiteralType LITERAL = new LiteralType(); |
11 | ModalLiteralType MODAL_LITERAL = new ModalLiteralType(); | ||
11 | InvalidType INVALID = new InvalidType(); | 12 | InvalidType INVALID = new InvalidType(); |
12 | 13 | ||
13 | FixedType getActualType(); | 14 | FixedType getActualType(); |
diff --git a/subprojects/language/src/main/java/tools/refinery/language/typesystem/FixedType.java b/subprojects/language/src/main/java/tools/refinery/language/typesystem/FixedType.java index 1b2ded48..f9e75f26 100644 --- a/subprojects/language/src/main/java/tools/refinery/language/typesystem/FixedType.java +++ b/subprojects/language/src/main/java/tools/refinery/language/typesystem/FixedType.java | |||
@@ -5,7 +5,8 @@ | |||
5 | */ | 5 | */ |
6 | package tools.refinery.language.typesystem; | 6 | package tools.refinery.language.typesystem; |
7 | 7 | ||
8 | public sealed interface FixedType extends ExprType permits NodeType, LiteralType, InvalidType, DataExprType { | 8 | public sealed interface FixedType extends ExprType permits NodeType, LiteralType, ModalLiteralType, InvalidType, |
9 | DataExprType { | ||
9 | @Override | 10 | @Override |
10 | default FixedType getActualType() { | 11 | default FixedType getActualType() { |
11 | return this; | 12 | return this; |
diff --git a/subprojects/language/src/main/java/tools/refinery/language/typesystem/ModalLiteralType.java b/subprojects/language/src/main/java/tools/refinery/language/typesystem/ModalLiteralType.java new file mode 100644 index 00000000..6b44977a --- /dev/null +++ b/subprojects/language/src/main/java/tools/refinery/language/typesystem/ModalLiteralType.java | |||
@@ -0,0 +1,16 @@ | |||
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.typesystem; | ||
7 | |||
8 | public final class ModalLiteralType implements FixedType { | ||
9 | ModalLiteralType() { | ||
10 | } | ||
11 | |||
12 | @Override | ||
13 | public String toString() { | ||
14 | return "modal constraint"; | ||
15 | } | ||
16 | } | ||
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 6691f0ae..0b252c09 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 | |||
@@ -8,6 +8,7 @@ package tools.refinery.language.typesystem; | |||
8 | import com.google.inject.Inject; | 8 | import com.google.inject.Inject; |
9 | import org.eclipse.emf.common.util.Diagnostic; | 9 | import org.eclipse.emf.common.util.Diagnostic; |
10 | import org.eclipse.emf.ecore.EObject; | 10 | import org.eclipse.emf.ecore.EObject; |
11 | import org.eclipse.emf.ecore.EReference; | ||
11 | import org.eclipse.emf.ecore.EStructuralFeature; | 12 | import org.eclipse.emf.ecore.EStructuralFeature; |
12 | import org.eclipse.xtext.validation.CheckType; | 13 | import org.eclipse.xtext.validation.CheckType; |
13 | import org.eclipse.xtext.validation.FeatureBasedDiagnostic; | 14 | import org.eclipse.xtext.validation.FeatureBasedDiagnostic; |
@@ -63,6 +64,7 @@ public class TypedModule { | |||
63 | for (var statement : problem.getStatements()) { | 64 | for (var statement : problem.getStatements()) { |
64 | switch (statement) { | 65 | switch (statement) { |
65 | case PredicateDefinition predicateDefinition -> checkTypes(predicateDefinition); | 66 | case PredicateDefinition predicateDefinition -> checkTypes(predicateDefinition); |
67 | case RuleDefinition ruleDefinition -> checkTypes(ruleDefinition); | ||
66 | case Assertion assertion -> checkTypes(assertion); | 68 | case Assertion assertion -> checkTypes(assertion); |
67 | default -> { | 69 | default -> { |
68 | // Nothing to type check. | 70 | // Nothing to type check. |
@@ -79,9 +81,29 @@ public class TypedModule { | |||
79 | } | 81 | } |
80 | } | 82 | } |
81 | 83 | ||
84 | private void checkTypes(RuleDefinition ruleDefinition) { | ||
85 | for (var conjunction : ruleDefinition.getPreconditions()) { | ||
86 | for (var literal : conjunction.getLiterals()) { | ||
87 | expectType(literal, ExprType.MODAL_LITERAL); | ||
88 | } | ||
89 | } | ||
90 | for (var consequent : ruleDefinition.getConsequents()) { | ||
91 | for (var action : consequent.getActions()) { | ||
92 | if (action instanceof AssertionAction assertionAction) { | ||
93 | checkTypes(assertionAction); | ||
94 | } | ||
95 | } | ||
96 | } | ||
97 | } | ||
98 | |||
82 | private void checkTypes(Assertion assertion) { | 99 | private void checkTypes(Assertion assertion) { |
83 | var relation = assertion.getRelation(); | 100 | var relation = assertion.getRelation(); |
84 | var value = assertion.getValue(); | 101 | var value = assertion.getValue(); |
102 | checkAssertion(assertion, relation, value, ProblemPackage.Literals.ASSERTION__RELATION); | ||
103 | checkNodeAssertionArgumentTypes(assertion.getArguments(), false); | ||
104 | } | ||
105 | |||
106 | private void checkAssertion(EObject assertion, Relation relation, Expr value, EReference relationReference) { | ||
85 | if (relation == null) { | 107 | if (relation == null) { |
86 | return; | 108 | return; |
87 | } | 109 | } |
@@ -95,11 +117,45 @@ public class TypedModule { | |||
95 | } | 117 | } |
96 | if (value == null) { | 118 | if (value == null) { |
97 | var message = "Assertion value of type %s is required.".formatted(type); | 119 | var message = "Assertion value of type %s is required.".formatted(type); |
98 | error(message, assertion, ProblemPackage.Literals.ASSERTION__RELATION, 0, ProblemValidator.TYPE_ERROR); | 120 | error(message, assertion, relationReference, 0, ProblemValidator.TYPE_ERROR); |
99 | } | 121 | } |
100 | expectType(value, type); | 122 | expectType(value, type); |
101 | } | 123 | } |
102 | 124 | ||
125 | private void checkNodeAssertionArgumentTypes(Collection<AssertionArgument> assertionArguments, | ||
126 | boolean allowVariables) { | ||
127 | for (var argument : assertionArguments) { | ||
128 | if (argument instanceof NodeAssertionArgument nodeAssertionArgument) { | ||
129 | checkNodeAssertionArgumentType(nodeAssertionArgument, allowVariables); | ||
130 | } | ||
131 | } | ||
132 | } | ||
133 | |||
134 | private void checkNodeAssertionArgumentType(NodeAssertionArgument nodeAssertionArgument, boolean allowVariables) { | ||
135 | var variableOrNode = nodeAssertionArgument.getNode(); | ||
136 | if (variableOrNode == null || variableOrNode.eIsProxy()) { | ||
137 | return; | ||
138 | } | ||
139 | if (allowVariables && variableOrNode instanceof Variable variable) { | ||
140 | var variableType = getVariableType(variable); | ||
141 | if (variableType == ExprType.INVALID || variableType == ExprType.NODE) { | ||
142 | return; | ||
143 | } | ||
144 | } | ||
145 | if (variableOrNode instanceof Node) { | ||
146 | return; | ||
147 | } | ||
148 | error("Assertion argument must be a node.", nodeAssertionArgument, | ||
149 | ProblemPackage.Literals.NODE_ASSERTION_ARGUMENT__NODE, 0, ProblemValidator.TYPE_ERROR); | ||
150 | } | ||
151 | |||
152 | private void checkTypes(AssertionAction assertionAction) { | ||
153 | var relation = assertionAction.getRelation(); | ||
154 | var value = assertionAction.getValue(); | ||
155 | checkAssertion(assertionAction, relation, value, ProblemPackage.Literals.ASSERTION_ACTION__RELATION); | ||
156 | checkNodeAssertionArgumentTypes(assertionAction.getArguments(), true); | ||
157 | } | ||
158 | |||
103 | public List<FeatureBasedDiagnostic> getDiagnostics() { | 159 | public List<FeatureBasedDiagnostic> getDiagnostics() { |
104 | return diagnostics; | 160 | return diagnostics; |
105 | } | 161 | } |
@@ -202,6 +258,7 @@ public class TypedModule { | |||
202 | case RangeExpr rangeExpr -> computeExpressionType(rangeExpr); | 258 | case RangeExpr rangeExpr -> computeExpressionType(rangeExpr); |
203 | case ArithmeticBinaryExpr arithmeticBinaryExpr -> computeExpressionType(arithmeticBinaryExpr); | 259 | case ArithmeticBinaryExpr arithmeticBinaryExpr -> computeExpressionType(arithmeticBinaryExpr); |
204 | case CastExpr castExpr -> computeExpressionType(castExpr); | 260 | case CastExpr castExpr -> computeExpressionType(castExpr); |
261 | case ModalExpr modalExpr -> computeExpressionType(modalExpr); | ||
205 | default -> { | 262 | default -> { |
206 | error("Unknown expression: " + expr.getClass().getSimpleName(), expr, null, 0, | 263 | error("Unknown expression: " + expr.getClass().getSimpleName(), expr, null, 0, |
207 | ProblemValidator.UNKNOWN_EXPRESSION_ISSUE); | 264 | ProblemValidator.UNKNOWN_EXPRESSION_ISSUE); |
@@ -290,6 +347,9 @@ public class TypedModule { | |||
290 | // Negation of literals yields another (non-enumerable) literal. | 347 | // Negation of literals yields another (non-enumerable) literal. |
291 | return ExprType.LITERAL; | 348 | return ExprType.LITERAL; |
292 | } | 349 | } |
350 | if (actualType == ExprType.MODAL_LITERAL) { | ||
351 | return ExprType.MODAL_LITERAL; | ||
352 | } | ||
293 | if (actualType == ExprType.INVALID) { | 353 | if (actualType == ExprType.INVALID) { |
294 | return ExprType.INVALID; | 354 | return ExprType.INVALID; |
295 | } | 355 | } |
@@ -507,6 +567,28 @@ public class TypedModule { | |||
507 | return ExprType.INVALID; | 567 | return ExprType.INVALID; |
508 | } | 568 | } |
509 | 569 | ||
570 | @NotNull | ||
571 | private ExprType computeExpressionType(ModalExpr expr) { | ||
572 | var body = expr.getBody(); | ||
573 | if (body == null) { | ||
574 | return ExprType.INVALID; | ||
575 | } | ||
576 | var actualType = getExpressionType(body); | ||
577 | if (actualType == ExprType.LITERAL || BuiltinTermInterpreter.BOOLEAN_TYPE.equals(actualType)) { | ||
578 | return ExprType.MODAL_LITERAL; | ||
579 | } | ||
580 | if (actualType == ExprType.INVALID) { | ||
581 | return ExprType.INVALID; | ||
582 | } | ||
583 | if (actualType instanceof MutableType) { | ||
584 | error(OPERAND_TYPE_ERROR_MESSAGE, body, null, 0, ProblemValidator.TYPE_ERROR); | ||
585 | return ExprType.INVALID; | ||
586 | } | ||
587 | var message = "Data type %s does not support modal operators.".formatted(actualType); | ||
588 | error(message, expr, null, 0, ProblemValidator.TYPE_ERROR); | ||
589 | return ExprType.INVALID; | ||
590 | } | ||
591 | |||
510 | private FixedType getCommonDataType(BinaryExpr expr) { | 592 | private FixedType getCommonDataType(BinaryExpr expr) { |
511 | var commonType = getCommonType(expr); | 593 | var commonType = getCommonType(expr); |
512 | if (!(commonType instanceof DataExprType) && commonType != ExprType.INVALID) { | 594 | if (!(commonType instanceof DataExprType) && commonType != ExprType.INVALID) { |