diff --git a/src/main/java/de/tlc4b/analysis/MachineContext.java b/src/main/java/de/tlc4b/analysis/MachineContext.java
index ff194588996457bf2a9878714cba8103dd67b1bc..ae6f85e10e87716b1af3cfedb36b7207b2fb0f25 100644
--- a/src/main/java/de/tlc4b/analysis/MachineContext.java
+++ b/src/main/java/de/tlc4b/analysis/MachineContext.java
@@ -635,6 +635,31 @@ public class MachineContext extends DepthFirstAdapter {
}
node.getPredicate().apply(this);
node.getSubstitution().apply(this);
+ contextTable.remove(contextTable.size() - 1);
+ }
+
+ @Override
+ public void caseALetExpressionExpression(ALetExpressionExpression node) {
+ contextTable.add(new LinkedHashMap<>());
+ List<PExpression> copy = new ArrayList<>(node.getIdentifiers());
+ for (PExpression e : copy) {
+ putLocalVariableIntoCurrentScope((AIdentifierExpression) e);
+ }
+ node.getAssignment().apply(this);
+ node.getExpr().apply(this);
+ contextTable.remove(contextTable.size() - 1);
+ }
+
+ @Override
+ public void caseALetPredicatePredicate(ALetPredicatePredicate node) {
+ contextTable.add(new LinkedHashMap<>());
+ List<PExpression> copy = new ArrayList<>(node.getIdentifiers());
+ for (PExpression e : copy) {
+ putLocalVariableIntoCurrentScope((AIdentifierExpression) e);
+ }
+ node.getAssignment().apply(this);
+ node.getPred().apply(this);
+ contextTable.remove(contextTable.size() - 1);
}
@Override
@@ -646,6 +671,7 @@ public class MachineContext extends DepthFirstAdapter {
}
node.getWhere().apply(this);
node.getThen().apply(this);
+ contextTable.remove(contextTable.size() - 1);
}
@Override
diff --git a/src/main/java/de/tlc4b/analysis/Renamer.java b/src/main/java/de/tlc4b/analysis/Renamer.java
index d98a9ffe40983a34cb856a37234bb8579d71315a..dd9b2d4ed3e17596b7087a3f428b9bd834d4d5ed 100644
--- a/src/main/java/de/tlc4b/analysis/Renamer.java
+++ b/src/main/java/de/tlc4b/analysis/Renamer.java
@@ -19,6 +19,8 @@ import de.be4.classicalb.core.parser.node.AGeneralProductExpression;
import de.be4.classicalb.core.parser.node.AGeneralSumExpression;
import de.be4.classicalb.core.parser.node.AIdentifierExpression;
import de.be4.classicalb.core.parser.node.ALambdaExpression;
+import de.be4.classicalb.core.parser.node.ALetExpressionExpression;
+import de.be4.classicalb.core.parser.node.ALetPredicatePredicate;
import de.be4.classicalb.core.parser.node.ALetSubstitution;
import de.be4.classicalb.core.parser.node.AOperation;
import de.be4.classicalb.core.parser.node.APredicateDefinitionDefinition;
@@ -350,6 +352,34 @@ public class Renamer extends DepthFirstAdapter {
removeLastContext();
}
+ @Override
+ public void caseALetExpressionExpression(ALetExpressionExpression node) {
+ List<PExpression> list = new ArrayList<>(node.getIdentifiers());
+ evalBoundedVariables(node, list);
+
+ List<PExpression> copy = new ArrayList<>(node.getIdentifiers());
+ for (PExpression e : copy) {
+ e.apply(this);
+ }
+ node.getAssignment().apply(this);
+ node.getExpr().apply(this);
+ removeLastContext();
+ }
+
+ @Override
+ public void caseALetPredicatePredicate(ALetPredicatePredicate node) {
+ List<PExpression> list = new ArrayList<>(node.getIdentifiers());
+ evalBoundedVariables(node, list);
+
+ List<PExpression> copy = new ArrayList<>(node.getIdentifiers());
+ for (PExpression e : copy) {
+ e.apply(this);
+ }
+ node.getAssignment().apply(this);
+ node.getPred().apply(this);
+ removeLastContext();
+ }
+
@Override
public void caseAVarSubstitution(AVarSubstitution node) {
List<PExpression> list = new ArrayList<>(node.getIdentifiers());
diff --git a/src/main/java/de/tlc4b/analysis/Typechecker.java b/src/main/java/de/tlc4b/analysis/Typechecker.java
index 55e34f707b6f8ae63d3d45fb9fd816a389ec50a6..4503bc3bc169f2cd16573d4318d8afd0549a9329 100644
--- a/src/main/java/de/tlc4b/analysis/Typechecker.java
+++ b/src/main/java/de/tlc4b/analysis/Typechecker.java
@@ -605,6 +605,38 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
node.getSubstitution().apply(this);
}
+ @Override
+ public void caseALetExpressionExpression(ALetExpressionExpression node) {
+ List<PExpression> copy = new ArrayList<>(node.getIdentifiers());
+ for (PExpression e : copy) {
+ AIdentifierExpression v = (AIdentifierExpression) e;
+ setType(v, new UntypedType());
+ }
+
+ setType(node.getAssignment(), BoolType.getInstance());
+ node.getAssignment().apply(this);
+
+ setType(node.getExpr(), new UntypedType());
+ node.getExpr().apply(this);
+ unify(getType(node), getType(node.getExpr()), node);
+ }
+
+ @Override
+ public void caseALetPredicatePredicate(ALetPredicatePredicate node) {
+ List<PExpression> copy = new ArrayList<>(node.getIdentifiers());
+ for (PExpression e : copy) {
+ AIdentifierExpression v = (AIdentifierExpression) e;
+ setType(v, new UntypedType());
+ }
+
+ setType(node.getAssignment(), BoolType.getInstance());
+ node.getAssignment().apply(this);
+
+ setType(node.getPred(), BoolType.getInstance());
+ node.getPred().apply(this);
+ unify(getType(node), getType(node.getPred()), node);
+ }
+
/****************************************************************************
* Arithmetic operators *
****************************************************************************/
diff --git a/src/main/java/de/tlc4b/analysis/UnsupportedConstructsFinder.java b/src/main/java/de/tlc4b/analysis/UnsupportedConstructsFinder.java
index 15cca6529a0b4d8d6a6edb9a4993c29a5248a998..55459d4b0447badd56a280ebf3a5a53a00d112e8 100644
--- a/src/main/java/de/tlc4b/analysis/UnsupportedConstructsFinder.java
+++ b/src/main/java/de/tlc4b/analysis/UnsupportedConstructsFinder.java
@@ -37,9 +37,6 @@ public class UnsupportedConstructsFinder extends DepthFirstAdapter {
// should have been rewritten in parser
add(AIfPredicatePredicate.class);
add(AIfElsifPredicatePredicate.class);
-
- add(ALetExpressionExpression.class);
- add(ALetPredicatePredicate.class);
}
private static void add(Class<? extends Node> clazz) {
diff --git a/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java b/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java
index 2d2a7d6d3852312a1a6691e4034d366513b9b58b..9cc265d4e2c88c24a04cf22d336ffb137b3c5b6d 100644
--- a/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java
+++ b/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java
@@ -25,6 +25,8 @@ import de.be4.classicalb.core.parser.node.AImplicationPredicate;
import de.be4.classicalb.core.parser.node.AInitialisationMachineClause;
import de.be4.classicalb.core.parser.node.AIntersectionExpression;
import de.be4.classicalb.core.parser.node.ALambdaExpression;
+import de.be4.classicalb.core.parser.node.ALetExpressionExpression;
+import de.be4.classicalb.core.parser.node.ALetPredicatePredicate;
import de.be4.classicalb.core.parser.node.ALetSubstitution;
import de.be4.classicalb.core.parser.node.AMemberPredicate;
import de.be4.classicalb.core.parser.node.ANotMemberPredicate;
@@ -456,6 +458,22 @@ public class TypeRestrictor extends DepthFirstAdapter {
createRestrictedTypeofLocalVariables(new HashSet<>(node.getIdentifiers()), false);
}
+ @Override
+ public void inALetExpressionExpression(ALetExpressionExpression node) {
+ super.inALetExpressionExpression(node);
+ // no type restriction, will use "LET var == value IN expr" construct
+ }
+
+ @Override
+ public void inALetPredicatePredicate(ALetPredicatePredicate node) {
+ HashSet<Node> list = new HashSet<>();
+ List<PExpression> copy = new ArrayList<>(node.getIdentifiers());
+ list.addAll(copy);
+ list.addAll(getExpectedIdentifier(node));
+ analysePredicate(node.getAssignment(), list, new HashSet<>());
+ createRestrictedTypeofLocalVariables(new HashSet<>(node.getIdentifiers()), false);
+ }
+
private Hashtable<Node, Node> variablesHashTable;
public void inABecomesSuchSubstitution(ABecomesSuchSubstitution node) {
diff --git a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
index aa0c57c918bff4b949a8bc77eafcd0babf7679ab..9474ba326984a31d5db08e5b5c7860ebe205ee3f 100644
--- a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
+++ b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
@@ -2,10 +2,12 @@ package de.tlc4b.prettyprint;
import java.util.ArrayList;
import java.util.Collection;
+import java.util.HashMap;
import java.util.HashSet;
import java.util.Iterator;
import java.util.LinkedList;
import java.util.List;
+import java.util.Map;
import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
import de.be4.classicalb.core.parser.node.*;
@@ -28,6 +30,7 @@ import de.tlc4b.btypes.PairType;
import de.tlc4b.btypes.SetType;
import de.tlc4b.btypes.StructType;
import de.tlc4b.btypes.UntypedType;
+import de.tlc4b.exceptions.TranslationException;
import de.tlc4b.ltl.LTLFormulaVisitor;
import de.tlc4b.tla.ConfigFile;
import de.tlc4b.tla.TLADefinition;
@@ -997,20 +1000,18 @@ public class TLAPrinter extends DepthFirstAdapter {
@Override
public void caseALetSubstitution(ALetSubstitution node) {
inALetSubstitution(node);
+ moduleStringAppend("\\E ");
List<PExpression> copy = new ArrayList<>(node.getIdentifiers());
- if (!copy.isEmpty()) {
- moduleStringAppend("\\E ");
- for (int i = 0; i < copy.size(); i++) {
- PExpression e = copy.get(i);
- e.apply(this);
- moduleStringAppend(" \\in ");
- typeRestrictor.getRestrictedNode(e).apply(this);
- if (i < copy.size() - 1) {
- moduleStringAppend(", ");
- }
+ for (int i = 0; i < copy.size(); i++) {
+ PExpression e = copy.get(i);
+ e.apply(this);
+ moduleStringAppend(" \\in ");
+ typeRestrictor.getRestrictedNode(e).apply(this);
+ if (i < copy.size() - 1) {
+ moduleStringAppend(", ");
}
- moduleStringAppend(" : ");
}
+ moduleStringAppend(" : ");
if (typeRestrictor.isARemovedNode(node.getPredicate())) {
moduleStringAppend("TRUE");
@@ -1025,6 +1026,87 @@ public class TLAPrinter extends DepthFirstAdapter {
outALetSubstitution(node);
}
+ @Override
+ public void caseALetPredicatePredicate(ALetPredicatePredicate node) {
+ inALetPredicatePredicate(node);
+ moduleStringAppend("\\E ");
+ List<PExpression> copy = new ArrayList<>(node.getIdentifiers());
+ for (int i = 0; i < copy.size(); i++) {
+ PExpression e = copy.get(i);
+ e.apply(this);
+ moduleStringAppend(" \\in ");
+ typeRestrictor.getRestrictedNode(e).apply(this);
+ if (i < copy.size() - 1) {
+ moduleStringAppend(", ");
+ }
+ }
+ moduleStringAppend(" : ");
+
+ if (typeRestrictor.isARemovedNode(node.getAssignment())) {
+ moduleStringAppend("TRUE");
+ } else {
+ node.getAssignment().apply(this);
+ }
+
+ moduleStringAppend(" /\\ ");
+ node.getPred().apply(this);
+
+ outALetPredicatePredicate(node);
+ }
+
+ private static Map<String, PExpression> getValuesFromEqualPredicates(PPredicate p, Map<String, PExpression> values) {
+ if (p instanceof AEqualPredicate) {
+ AEqualPredicate eq = (AEqualPredicate) p;
+ PExpression left = eq.getLeft();
+ if (left instanceof AIdentifierExpression) {
+ String s = Utils.getAIdentifierAsString((AIdentifierExpression) left);
+ if (values.containsKey(s)) {
+ throw new TranslationException("invalid predicate in LET expr: " + p);
+ }
+ values.put(s, eq.getRight());
+ } else {
+ throw new TranslationException("invalid predicate in LET expr: " + p);
+ }
+ } else if (p instanceof AConjunctPredicate) {
+ AConjunctPredicate conj = (AConjunctPredicate) p;
+ getValuesFromEqualPredicates(conj.getLeft(), values);
+ getValuesFromEqualPredicates(conj.getRight(), values);
+ } else {
+ throw new TranslationException("invalid predicate in LET expr: " + p);
+ }
+
+ return values;
+ }
+
+ @Override
+ public void caseALetExpressionExpression(ALetExpressionExpression node) {
+ inALetExpressionExpression(node);
+ moduleStringAppend("LET ");
+ Map<String, PExpression> values = getValuesFromEqualPredicates(node.getAssignment(), new HashMap<>());
+ List<PExpression> copy = new ArrayList<>(node.getIdentifiers());
+ for (int i = 0; i < copy.size(); i++) {
+ PExpression e = copy.get(i);
+ e.apply(this);
+ moduleStringAppend(" == ");
+
+ String identifier = Utils.getAIdentifierAsString((AIdentifierExpression) e);
+ PExpression value = values.get(identifier);
+ if (value == null) {
+ throw new TranslationException("no equals predicate for identifier " + identifier + " in LET expr");
+ }
+ value.apply(this);
+
+ if (i < copy.size() - 1) {
+ moduleStringAppend(", ");
+ }
+ }
+
+ moduleStringAppend(" IN ");
+ node.getExpr().apply(this);
+
+ outALetExpressionExpression(node);
+ }
+
@Override
public void caseAOperation(AOperation node) {
String name = renamer.getNameOfRef(node);
diff --git a/src/test/java/de/tlc4b/analysis/UnsupportedConstructsTest.java b/src/test/java/de/tlc4b/analysis/UnsupportedConstructsTest.java
index dd99257b7a4ffc1ff7c8aa8635ddb3b668aceff6..d1720cac8a80f5f7be01bb5eeeecaabd32f058f4 100644
--- a/src/test/java/de/tlc4b/analysis/UnsupportedConstructsTest.java
+++ b/src/test/java/de/tlc4b/analysis/UnsupportedConstructsTest.java
@@ -25,16 +25,4 @@ public class UnsupportedConstructsTest {
final String machine = "MACHINE M FREETYPES F = F1, F2(INTEGER) END";
translate(machine);
}
-
- @Test(expected = NotSupportedException.class)
- public void testLetExpr() throws Exception {
- final String machine = "MACHINE M VARIABLES x INVARIANT x : INTEGER INITIALISATION x := (LET foo BE foo=42 IN foo END) END";
- translate(machine);
- }
-
- @Test(expected = NotSupportedException.class)
- public void testLetPred() throws Exception {
- final String machine = "MACHINE M VARIABLES x INVARIANT x : INTEGER INITIALISATION x : (LET foo BE foo=42 IN x=foo END) END";
- translate(machine);
- }
}
diff --git a/src/test/java/de/tlc4b/prettyprint/OperationsTest.java b/src/test/java/de/tlc4b/prettyprint/OperationsTest.java
index 1741ed12ab89d41915f1e5f45f3c31da107b9f36..bad0b01ad8bb5ece9b2bc415909504f91a6db3f4 100644
--- a/src/test/java/de/tlc4b/prettyprint/OperationsTest.java
+++ b/src/test/java/de/tlc4b/prettyprint/OperationsTest.java
@@ -426,5 +426,46 @@ public class OperationsTest {
+ "====";
compare(expected, machine);
}
-
+
+ @Test
+ public void testOperationWithLetExpr() throws Exception {
+ String machine = "MACHINE test\n"
+ + "VARIABLES x\n"
+ + "INVARIANT x : 1..10\n"
+ + "INITIALISATION x := 1\n"
+ + "OPERATIONS\n"
+ + "inc = x := LET y BE y = x+1 IN y+1 END\n"
+ + "END";
+
+ String expected = "---- MODULE test ----\n"
+ + "EXTENDS Naturals\n"
+ + "VARIABLES x\n"
+ + "Invariant1 == x \\in 1..10\n"
+ + "Init == x = 1\n"
+ + "inc == x' = LET y == x+1 IN y+1\n"
+ + "Next == \\/ inc\n"
+ + "====";
+ compare(expected, machine);
+ }
+
+ @Test
+ public void testOperationWithLetPred() throws Exception {
+ String machine = "MACHINE test\n"
+ + "VARIABLES x\n"
+ + "INVARIANT x : 1..10\n"
+ + "INITIALISATION x := 1\n"
+ + "OPERATIONS\n"
+ + "inc = SELECT (LET y BE y = 1 IN x=y END) THEN x := x+1 END\n"
+ + "END";
+
+ String expected = "---- MODULE test ----\n"
+ + "EXTENDS Naturals\n"
+ + "VARIABLES x\n"
+ + "Invariant1 == x \\in 1..10\n"
+ + "Init == x = 1 \n"
+ + "inc == (\\E y \\in {1} : TRUE /\\ x = y /\\ x' = x + 1)\n"
+ + "Next == \\/ inc\n"
+ + "====";
+ compare(expected, machine);
+ }
}