From 638566514e6c75d4677a692cb463ff87ef8caf21 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Fri, 17 May 2024 17:58:15 +0200 Subject: feat: type checking for rules --- .../refinery/language/typesystem/ExprType.java | 1 + .../refinery/language/typesystem/FixedType.java | 3 +- .../language/typesystem/ModalLiteralType.java | 16 +++++ .../refinery/language/typesystem/TypedModule.java | 84 +++++++++++++++++++++- 4 files changed, 102 insertions(+), 2 deletions(-) create mode 100644 subprojects/language/src/main/java/tools/refinery/language/typesystem/ModalLiteralType.java (limited to 'subprojects') 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; public sealed interface ExprType permits FixedType, MutableType { NodeType NODE = new NodeType(); LiteralType LITERAL = new LiteralType(); + ModalLiteralType MODAL_LITERAL = new ModalLiteralType(); InvalidType INVALID = new InvalidType(); 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 @@ */ package tools.refinery.language.typesystem; -public sealed interface FixedType extends ExprType permits NodeType, LiteralType, InvalidType, DataExprType { +public sealed interface FixedType extends ExprType permits NodeType, LiteralType, ModalLiteralType, InvalidType, + DataExprType { @Override default FixedType getActualType() { 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 @@ +/* + * SPDX-FileCopyrightText: 2024 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.language.typesystem; + +public final class ModalLiteralType implements FixedType { + ModalLiteralType() { + } + + @Override + public String toString() { + return "modal constraint"; + } +} 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; import com.google.inject.Inject; import org.eclipse.emf.common.util.Diagnostic; import org.eclipse.emf.ecore.EObject; +import org.eclipse.emf.ecore.EReference; import org.eclipse.emf.ecore.EStructuralFeature; import org.eclipse.xtext.validation.CheckType; import org.eclipse.xtext.validation.FeatureBasedDiagnostic; @@ -63,6 +64,7 @@ public class TypedModule { for (var statement : problem.getStatements()) { switch (statement) { case PredicateDefinition predicateDefinition -> checkTypes(predicateDefinition); + case RuleDefinition ruleDefinition -> checkTypes(ruleDefinition); case Assertion assertion -> checkTypes(assertion); default -> { // Nothing to type check. @@ -79,9 +81,29 @@ public class TypedModule { } } + private void checkTypes(RuleDefinition ruleDefinition) { + for (var conjunction : ruleDefinition.getPreconditions()) { + for (var literal : conjunction.getLiterals()) { + expectType(literal, ExprType.MODAL_LITERAL); + } + } + for (var consequent : ruleDefinition.getConsequents()) { + for (var action : consequent.getActions()) { + if (action instanceof AssertionAction assertionAction) { + checkTypes(assertionAction); + } + } + } + } + private void checkTypes(Assertion assertion) { var relation = assertion.getRelation(); var value = assertion.getValue(); + checkAssertion(assertion, relation, value, ProblemPackage.Literals.ASSERTION__RELATION); + checkNodeAssertionArgumentTypes(assertion.getArguments(), false); + } + + private void checkAssertion(EObject assertion, Relation relation, Expr value, EReference relationReference) { if (relation == null) { return; } @@ -95,11 +117,45 @@ public class TypedModule { } if (value == null) { var message = "Assertion value of type %s is required.".formatted(type); - error(message, assertion, ProblemPackage.Literals.ASSERTION__RELATION, 0, ProblemValidator.TYPE_ERROR); + error(message, assertion, relationReference, 0, ProblemValidator.TYPE_ERROR); } expectType(value, type); } + private void checkNodeAssertionArgumentTypes(Collection assertionArguments, + boolean allowVariables) { + for (var argument : assertionArguments) { + if (argument instanceof NodeAssertionArgument nodeAssertionArgument) { + checkNodeAssertionArgumentType(nodeAssertionArgument, allowVariables); + } + } + } + + private void checkNodeAssertionArgumentType(NodeAssertionArgument nodeAssertionArgument, boolean allowVariables) { + var variableOrNode = nodeAssertionArgument.getNode(); + if (variableOrNode == null || variableOrNode.eIsProxy()) { + return; + } + if (allowVariables && variableOrNode instanceof Variable variable) { + var variableType = getVariableType(variable); + if (variableType == ExprType.INVALID || variableType == ExprType.NODE) { + return; + } + } + if (variableOrNode instanceof Node) { + return; + } + error("Assertion argument must be a node.", nodeAssertionArgument, + ProblemPackage.Literals.NODE_ASSERTION_ARGUMENT__NODE, 0, ProblemValidator.TYPE_ERROR); + } + + private void checkTypes(AssertionAction assertionAction) { + var relation = assertionAction.getRelation(); + var value = assertionAction.getValue(); + checkAssertion(assertionAction, relation, value, ProblemPackage.Literals.ASSERTION_ACTION__RELATION); + checkNodeAssertionArgumentTypes(assertionAction.getArguments(), true); + } + public List getDiagnostics() { return diagnostics; } @@ -202,6 +258,7 @@ public class TypedModule { case RangeExpr rangeExpr -> computeExpressionType(rangeExpr); case ArithmeticBinaryExpr arithmeticBinaryExpr -> computeExpressionType(arithmeticBinaryExpr); case CastExpr castExpr -> computeExpressionType(castExpr); + case ModalExpr modalExpr -> computeExpressionType(modalExpr); default -> { error("Unknown expression: " + expr.getClass().getSimpleName(), expr, null, 0, ProblemValidator.UNKNOWN_EXPRESSION_ISSUE); @@ -290,6 +347,9 @@ public class TypedModule { // Negation of literals yields another (non-enumerable) literal. return ExprType.LITERAL; } + if (actualType == ExprType.MODAL_LITERAL) { + return ExprType.MODAL_LITERAL; + } if (actualType == ExprType.INVALID) { return ExprType.INVALID; } @@ -507,6 +567,28 @@ public class TypedModule { return ExprType.INVALID; } + @NotNull + private ExprType computeExpressionType(ModalExpr expr) { + var body = expr.getBody(); + if (body == null) { + return ExprType.INVALID; + } + var actualType = getExpressionType(body); + if (actualType == ExprType.LITERAL || BuiltinTermInterpreter.BOOLEAN_TYPE.equals(actualType)) { + return ExprType.MODAL_LITERAL; + } + if (actualType == ExprType.INVALID) { + return ExprType.INVALID; + } + if (actualType instanceof MutableType) { + error(OPERAND_TYPE_ERROR_MESSAGE, body, null, 0, ProblemValidator.TYPE_ERROR); + return ExprType.INVALID; + } + var message = "Data type %s does not support modal operators.".formatted(actualType); + error(message, expr, null, 0, ProblemValidator.TYPE_ERROR); + return ExprType.INVALID; + } + private FixedType getCommonDataType(BinaryExpr expr) { var commonType = getCommonType(expr); if (!(commonType instanceof DataExprType) && commonType != ExprType.INVALID) { -- cgit v1.2.3-54-g00ecf