From 22cde57ef5f09b5095c1a79239d9d2116cb70f87 Mon Sep 17 00:00:00 2001
From: Jan Gruteser <jan.gruteser@hhu.de>
Date: Mon, 29 Apr 2024 14:33:07 +0200
Subject: [PATCH] simplify type checker for arithmetic operators
---
.../java/de/tla2b/analysis/TypeChecker.java | 75 ++++++-------------
1 file changed, 24 insertions(+), 51 deletions(-)
diff --git a/src/main/java/de/tla2b/analysis/TypeChecker.java b/src/main/java/de/tla2b/analysis/TypeChecker.java
index aaf85a4..9336e6d 100644
--- a/src/main/java/de/tla2b/analysis/TypeChecker.java
+++ b/src/main/java/de/tla2b/analysis/TypeChecker.java
@@ -1172,6 +1172,8 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
return BoolType.getInstance();
}
+ // arithmetic operators: support both integers and reals
+ // for UntypedTypes the default is integer; if this leads to a TypeErrorException real is tried instead
case B_OPCODE_plus: // +
case B_OPCODE_minus: // -
case B_OPCODE_times: // *
@@ -1179,40 +1181,25 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
case B_OPCODE_mod: // % modulo
case B_OPCODE_exp: { // x hoch y, x^y
TLAType type;
- // TODO: Simplify
- if (expected instanceof RealType) {
+ try {
+ IntType.getInstance().unify(expected); // throws UnificationException
+ type = IntType.getInstance();
+ for (int i = 0; i < n.getArgs().length; i++) {
+ // throws TypeErrorException; check whether IntType is OK, else try the same with RealType
+ visitExprOrOpArgNode(n.getArgs()[i], type);
+ }
+ } catch (UnificationException | TypeErrorException e) {
try {
RealType.getInstance().unify(expected);
type = RealType.getInstance();
- } catch (UnificationException e) {
- throw new TypeErrorException(String.format("Expected %s, found REAL at '%s',%n%s", expected,
- n.getOperator().getName(), n.getLocation()));
- }
- } else if (expected instanceof IntType) {
- try {
- IntType.getInstance().unify(expected);
- type = IntType.getInstance();
- } catch (UnificationException ue) {
- throw new TypeErrorException(String.format("Expected %s, found INTEGER at '%s',%n%s", expected,
- n.getOperator().getName(), n.getLocation()));
- }
- } else if (expected instanceof UntypedType) {
- IntType.getInstance().unify(expected);
- type = IntType.getInstance();
- try {
for (int i = 0; i < n.getArgs().length; i++) {
+ // if TypeErrorException is thrown here, the type is incompatible and it is a real type error!
visitExprOrOpArgNode(n.getArgs()[i], type);
}
- } catch (TypeErrorException e) {
- RealType.getInstance().unify(expected);
- type = RealType.getInstance();
+ } catch (UnificationException ue) {
+ throw new TypeErrorException(String.format("Expected %s, found INTEGER at '%s',%n%s", expected,
+ n.getOperator().getName(), n.getLocation()));
}
- } else {
- throw new TypeErrorException(String.format("Expected %s, found INTEGER at '%s',%n%s", expected,
- n.getOperator().getName(), n.getLocation()));
- }
- for (int i = 0; i < n.getArgs().length; i++) {
- visitExprOrOpArgNode(n.getArgs()[i], type);
}
return type;
@@ -1287,38 +1274,24 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
case B_OPCODE_uminus: // -x
{
- // TODO: simplify
TLAType type;
- if (expected instanceof RealType) {
+ try {
+ IntType.getInstance().unify(expected); // throws UnificationException
+ type = IntType.getInstance();
+ // throws TypeErrorException; check whether IntType is OK, else try the same with RealType
+ visitExprOrOpArgNode(n.getArgs()[0], type);
+ } catch (UnificationException | TypeErrorException e) {
try {
RealType.getInstance().unify(expected);
type = RealType.getInstance();
- } catch (UnificationException e) {
- throw new TypeErrorException(
- String.format("Expected %s, found REAL at '-',%n%s", expected, n.getLocation()));
- }
- } else if (expected instanceof IntType) {
- try {
- IntType.getInstance().unify(expected);
- type = IntType.getInstance();
- } catch (UnificationException e) {
+ // if TypeErrorException is thrown here, the type is incompatible and it is a real type error!
+ visitExprOrOpArgNode(n.getArgs()[0], type);
+ } catch (UnificationException ue) {
throw new TypeErrorException(
String.format("Expected %s, found INTEGER at '-',%n%s", expected, n.getLocation()));
}
- } else if (expected instanceof UntypedType) {
- IntType.getInstance().unify(expected);
- type = IntType.getInstance();
- try {
- visitExprOrOpArgNode(n.getArgs()[0], type);
- } catch (TypeErrorException e) {
- RealType.getInstance().unify(expected);
- type = RealType.getInstance();
- }
- } else {
- throw new TypeErrorException(
- String.format("Expected %s, found INTEGER at '-',%n%s", expected, n.getLocation()));
}
- visitExprOrOpArgNode(n.getArgs()[0], type);
+
return type;
}
--
GitLab