From b0176d4c66b3a0fa24302d69de388b1765e7aa8c Mon Sep 17 00:00:00 2001
From: Miles Vella <673-vella@users.noreply.gitlab.cs.uni-duesseldorf.de>
Date: Wed, 12 Mar 2025 15:26:37 +0100
Subject: [PATCH] Support IF-ELSIF-ELSE expressions
---
.../java/de/tlc4b/analysis/Typechecker.java | 11 +++++++
.../analysis/UnsupportedConstructsFinder.java | 2 +-
.../java/de/tlc4b/prettyprint/TLAPrinter.java | 31 ++++++++++++++++---
3 files changed, 38 insertions(+), 6 deletions(-)
diff --git a/src/main/java/de/tlc4b/analysis/Typechecker.java b/src/main/java/de/tlc4b/analysis/Typechecker.java
index 01baa17..55e34f7 100644
--- a/src/main/java/de/tlc4b/analysis/Typechecker.java
+++ b/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 {
diff --git a/src/main/java/de/tlc4b/analysis/UnsupportedConstructsFinder.java b/src/main/java/de/tlc4b/analysis/UnsupportedConstructsFinder.java
index 31727e9..207a6ad 100644
--- a/src/main/java/de/tlc4b/analysis/UnsupportedConstructsFinder.java
+++ b/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);
diff --git a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
index b43f7a1..aa0c57c 100644
--- a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
+++ b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
@@ -1146,13 +1146,34 @@ public class TLAPrinter extends DepthFirstAdapter {
@Override
public void caseAIfThenElseExpression(AIfThenElseExpression node) {
- moduleStringAppend("(IF ");
+ if (node.getElsifs().isEmpty()) {
+ moduleStringAppend("(IF ");
+ node.getCondition().apply(this);
+ moduleStringAppend(" THEN ");
+ node.getThen().apply(this);
+ 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(" THEN ");
+ moduleStringAppend(" -> ");
node.getThen().apply(this);
- moduleStringAppend(" ELSE ");
- node.getElse().apply(this);
- moduleStringAppend(")");
}
@Override
--
GitLab