feat: type checking for rules

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;
 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 <https://refinery.tools/>
+ *
+ * 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<AssertionArgument> 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<FeatureBasedDiagnostic> 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) {