diff --git a/src/main/java/de/tla2b/analysis/TypeChecker.java b/src/main/java/de/tla2b/analysis/TypeChecker.java index 582bd30151e28908743a9184d04de6c6105c7966..f51225d3ac5e01a5a41332d8d620bb8988a6b695 100644 --- a/src/main/java/de/tla2b/analysis/TypeChecker.java +++ b/src/main/java/de/tla2b/analysis/TypeChecker.java @@ -1285,14 +1285,39 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns, case B_OPCODE_uminus: // -x { - try { + // TODO: simplify + TLAType type; + if (expected instanceof RealType) { + 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) { + throw new TypeErrorException( + String.format("Expected %s, found INTEGER at '-',%n%s", expected, n.getLocation())); + } + } else if (expected instanceof UntypedType) { IntType.getInstance().unify(expected); - } catch (UnificationException e) { + 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())); + String.format("Expected %s, found INTEGER at '-',%n%s", expected, n.getLocation())); } - visitExprOrOpArgNode(n.getArgs()[0], IntType.getInstance()); - return IntType.getInstance(); + visitExprOrOpArgNode(n.getArgs()[0], type); + return type; } /* diff --git a/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleReals.java b/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleReals.java index 928def9cb3c902a05d9dc6e192b8bdb5866cd241..f154d7ee5c0450e77bfa36ceb63370afe60337fd 100644 --- a/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleReals.java +++ b/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleReals.java @@ -35,8 +35,6 @@ public class TestModuleReals { TestUtil.typeCheckString(module); } - // FIXME: support: - @Ignore /* * unary minus: -x */ @@ -44,12 +42,20 @@ public class TestModuleReals { public void unifyUnaryMinusReal() throws TLA2BException { final String module = "-------------- MODULE Testing ----------------\n" + "EXTENDS Reals \n" - + "CONSTANTS k, k2 \n" - + "ASSUME k = -k2 \n" + "================================="; + + "CONSTANTS k \n" + + "ASSUME k = -1.0 \n" + "================================="; TestTypeChecker t = TestUtil.typeCheckString(module); assertEquals("REAL", t.getConstantType("k")); - assertEquals("REAL", t.getConstantType("k2")); + } + + @Test(expected = TypeErrorException.class) + public void unifyUnaryMinusRealError() throws TLA2BException { + final String module = "-------------- MODULE Testing ----------------\n" + + "EXTENDS Reals \n" + + "ASSUME -1 = -1.0 \n" + "================================="; + + TestTypeChecker t = TestUtil.typeCheckString(module); } @Test(expected = TypeErrorException.class)