support unary minus for reals

also needs to be simplified

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
 		{
+			// 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()));
 				}
-			visitExprOrOpArgNode(n.getArgs()[0], IntType.getInstance());
-			return IntType.getInstance();
+			} 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;
 		}
 
 		/*

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)