Support IF-ELSIF-ELSE expressions

src/main/java/de/tlc4b/analysis/Typechecker.java

@@ -412,13 +412,24 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
 		
 		UntypedType x = new UntypedType();
 		setType(node.getThen(), x);
+		node.getElsifs().forEach(n -> setType(n, x));
 		setType(node.getElse(), x);
 		node.getThen().apply(this);
+		node.getElsifs().forEach(n -> n.apply(this));
 		node.getElse().apply(this);
 		BType found = getType(node.getThen());
 		unify(getType(node), found, node);
 	}
 
+	@Override
+	public void caseAIfElsifExprExpression(AIfElsifExprExpression node) {
+		setType(node.getCondition(), BoolType.getInstance());
+		node.getCondition().apply(this);
+
+		setType(node.getThen(), getType(node));
+		node.getThen().apply(this);
+	}
+
 	@Override
 	public void caseANotEqualPredicate(ANotEqualPredicate node) {
 		try {

src/main/java/de/tlc4b/analysis/UnsupportedConstructsFinder.java

@@ -33,7 +33,7 @@ public class UnsupportedConstructsFinder extends DepthFirstAdapter {
 		add(AFloatSetExpression.class);
 		add(ARealExpression.class);
 
-		add(AIfElsifExprExpression.class);
+		// should have been rewritten in parser
 		add(AIfPredicatePredicate.class);
 		add(AIfElsifPredicatePredicate.class);
 

src/main/java/de/tlc4b/prettyprint/TLAPrinter.java

@@ -1146,6 +1146,7 @@ public class TLAPrinter extends DepthFirstAdapter {
 	
 	@Override
 	public void caseAIfThenElseExpression(AIfThenElseExpression node) {
+		if (node.getElsifs().isEmpty()) {
 			moduleStringAppend("(IF ");
 			node.getCondition().apply(this);
 			moduleStringAppend(" THEN ");
@@ -1153,6 +1154,26 @@ public class TLAPrinter extends DepthFirstAdapter {
 			moduleStringAppend(" ELSE ");
 			node.getElse().apply(this);
 			moduleStringAppend(")");
+		} else {
+			moduleStringAppend("(CASE ");
+			node.getCondition().apply(this);
+			moduleStringAppend(" -> ");
+			node.getThen().apply(this);
+			node.getElsifs().forEach(n -> {
+				moduleStringAppend(" [] ");
+				n.apply(this);
+			});
+			moduleStringAppend(" [] OTHER -> ");
+			node.getElse().apply(this);
+			moduleStringAppend(")");
+		}
+	}
+
+	@Override
+	public void caseAIfElsifExprExpression(AIfElsifExprExpression node) {
+		node.getCondition().apply(this);
+		moduleStringAppend(" -> ");
+		node.getThen().apply(this);
 	}
 
 	@Override