From d6c8f859fc00a55b7a6f8d25c375bd40e3f6b049 Mon Sep 17 00:00:00 2001
From: hansen <dominik_hansen@web.de>
Date: Fri, 5 Feb 2016 10:24:09 +0100
Subject: [PATCH] added support for IF-THEN-ELSE-END expression
---
build.gradle | 2 +-
.../java/de/tlc4b/analysis/Typechecker.java | 14 +++++++++++++
.../java/de/tlc4b/prettyprint/TLAPrinter.java | 11 ++++++++++
src/main/java/de/tlc4b/tla/Generator.java | 9 ++++-----
src/main/java/de/tlc4b/tla/TLAModule.java | 7 +++++--
.../prettyprint/SyntaxExtensionsTest.java | 20 +++++++++++++++++++
6 files changed, 55 insertions(+), 8 deletions(-)
create mode 100644 src/test/java/de/tlc4b/prettyprint/SyntaxExtensionsTest.java
diff --git a/build.gradle b/build.gradle
index 5d6e988..7d9929a 100644
--- a/build.gradle
+++ b/build.gradle
@@ -26,7 +26,7 @@ configurations.all {
resolutionStrategy.cacheChangingModulesFor 0, 'seconds'
}
-def parser_version = '2.5.1'
+def parser_version = '2.5.2-SNAPSHOT'
def tlatools_version = '1.0.2-SNAPSHOT'
dependencies {
diff --git a/src/main/java/de/tlc4b/analysis/Typechecker.java b/src/main/java/de/tlc4b/analysis/Typechecker.java
index 1e438a3..bf7dcf7 100644
--- a/src/main/java/de/tlc4b/analysis/Typechecker.java
+++ b/src/main/java/de/tlc4b/analysis/Typechecker.java
@@ -471,6 +471,20 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
node.getRight().apply(this);
}
+ @Override
+ public void caseAIfThenElseExpression(AIfThenElseExpression node) {
+ setType(node.getCondition(), BoolType.getInstance());
+ node.getCondition().apply(this);
+
+ UntypedType x = new UntypedType();
+ setType(node.getThen(), x);
+ setType(node.getElse(), x);
+ node.getThen().apply(this);
+ node.getElse().apply(this);
+ BType found = getType(node.getThen());
+ unify(getType(node), found, node);
+ }
+
@Override
public void caseANotEqualPredicate(ANotEqualPredicate node) {
try {
diff --git a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
index 8791cb0..55687a6 100644
--- a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
+++ b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
@@ -1196,6 +1196,17 @@ public class TLAPrinter extends DepthFirstAdapter {
node.getRight().apply(this);
outANotEqualPredicate(node);
}
+
+ @Override
+ public void caseAIfThenElseExpression(AIfThenElseExpression node) {
+ moduleStringAppend("(IF ");
+ node.getCondition().apply(this);
+ moduleStringAppend(" THEN ");
+ node.getThen().apply(this);
+ moduleStringAppend(" ELSE ");
+ node.getElse().apply(this);
+ moduleStringAppend(")");
+ }
@Override
public void caseAConjunctPredicate(AConjunctPredicate node) {
diff --git a/src/main/java/de/tlc4b/tla/Generator.java b/src/main/java/de/tlc4b/tla/Generator.java
index 97c016e..ca2b6c6 100644
--- a/src/main/java/de/tlc4b/tla/Generator.java
+++ b/src/main/java/de/tlc4b/tla/Generator.java
@@ -70,7 +70,7 @@ public class Generator extends DepthFirstAdapter {
evalMachineSets();
evalDefinitions();
evalConstants();
-
+
evalInvariant();
evalOperations();
evalGoal();
@@ -143,13 +143,12 @@ public class Generator extends DepthFirstAdapter {
Node value = idValueTable.get(param);
if (value != null) {
- tlaModule.tlaDefinitions.add(new TLADefinition(param, value));
+ tlaModule.addTLADefinition(new TLADefinition(param, value));
continue;
}
Integer intValue = constantsEvaluator.getIntValue(param);
if (intValue != null) {
- tlaModule.tlaDefinitions
- .add(new TLADefinition(param, intValue));
+ tlaModule.addTLADefinition(new TLADefinition(param, intValue));
continue;
}
@@ -205,7 +204,7 @@ public class Generator extends DepthFirstAdapter {
Node n = itr2.next();
AEnumeratedSetSet e = (AEnumeratedSetSet) n;
TLADefinition def = new TLADefinition(e, e);
- this.tlaModule.tlaDefinitions.add(def);
+ this.tlaModule.addTLADefinition(def);
List<PExpression> copy = new ArrayList<PExpression>(e.getElements());
for (PExpression element : copy) {
this.tlaModule.constants.add(element);
diff --git a/src/main/java/de/tlc4b/tla/TLAModule.java b/src/main/java/de/tlc4b/tla/TLAModule.java
index d373d37..2135d0c 100644
--- a/src/main/java/de/tlc4b/tla/TLAModule.java
+++ b/src/main/java/de/tlc4b/tla/TLAModule.java
@@ -9,14 +9,14 @@ public class TLAModule {
protected String moduleName;
- protected final ArrayList<TLADefinition> tlaDefinitions;
+ private final ArrayList<TLADefinition> tlaDefinitions;
protected final ArrayList<Node> constants;
protected final ArrayList<Node> assumes;
protected final ArrayList<Node> variables;
protected final ArrayList<Node> invariants;
private final ArrayList<Node> initPredicates;
protected final ArrayList<POperation> operations;
- private ArrayList<PDefinition> bDefinitions;
+ private ArrayList<PDefinition> bDefinitions;
private final ArrayList<Node> assertions;
protected ArrayList<PDefinition> allDefinitions;
@@ -110,4 +110,7 @@ public class TLAModule {
return this.initPredicates.size() > 0;
}
+ public void addTLADefinition(TLADefinition defintion) {
+ this.tlaDefinitions.add(defintion);
+ }
}
diff --git a/src/test/java/de/tlc4b/prettyprint/SyntaxExtensionsTest.java b/src/test/java/de/tlc4b/prettyprint/SyntaxExtensionsTest.java
new file mode 100644
index 0000000..399fb6e
--- /dev/null
+++ b/src/test/java/de/tlc4b/prettyprint/SyntaxExtensionsTest.java
@@ -0,0 +1,20 @@
+package de.tlc4b.prettyprint;
+
+import static de.tlc4b.util.TestUtil.compare;
+
+import org.junit.Test;
+
+
+public class SyntaxExtensionsTest {
+
+ @Test
+ public void testIfThenElseg() throws Exception {
+ String machine = "MACHINE test\n"
+ + "PROPERTIES 1 = (IF 1=1 THEN 1 ELSE 2 END) \n" + "END";
+
+ String expected = "---- MODULE test----\n"
+ + "ASSUME 1 = (IF 1 = 1 THEN 1 ELSE 2) \n"
+ + "======";
+ compare(expected, machine);
+ }
+}
--
GitLab