From d7f630a0c7e2a708b35e33cba0172db44514adad Mon Sep 17 00:00:00 2001 From: hansen <dominik_hansen@web.de> Date: Wed, 25 Jun 2014 14:02:41 +0200 Subject: [PATCH] Fixed a bug translating LET IN statements --- .../java/de/tlc4b/analysis/Typechecker.java | 7 +++++- .../java/de/tlc4b/prettyprint/TLAPrinter.java | 22 ++++++++++++++----- src/test/java/de/tlc4b/util/TLC4BTester.java | 2 +- .../resources/basics/SubstitutionsTest.mch | 4 +++- 4 files changed, 26 insertions(+), 9 deletions(-) diff --git a/src/main/java/de/tlc4b/analysis/Typechecker.java b/src/main/java/de/tlc4b/analysis/Typechecker.java index c8595a3..589cf83 100644 --- a/src/main/java/de/tlc4b/analysis/Typechecker.java +++ b/src/main/java/de/tlc4b/analysis/Typechecker.java @@ -1367,8 +1367,13 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker { throw new TypeErrorException("Excepted '" + expected + "' , found " + found + "'"); } - setType(node.getExpression(), new SetType(new UntypedType())); + + setType(node.getExpression(), new UntypedType()); node.getExpression().apply(this); + BType type = getType(node.getExpression()); + if (! (type instanceof FunctionType)){ + new SetType(new UntypedType()).unify(type, this); + } } @Override diff --git a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java index f07ed67..8f9eff5 100644 --- a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java +++ b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java @@ -920,7 +920,12 @@ public class TLAPrinter extends DepthFirstAdapter { tlaModuleString.append(" : "); } - node.getPredicate().apply(this); + if (typeRestrictor.isARemovedNode(node.getPredicate())) { + tlaModuleString.append("TRUE"); + } else { + node.getPredicate().apply(this); + } + tlaModuleString.append(" /\\ "); node.getSubstitution().apply(this); printUnchangedVariables(node, true); @@ -2050,11 +2055,16 @@ public class TLAPrinter extends DepthFirstAdapter { @Override public void caseACardExpression(ACardExpression node) { - inACardExpression(node); - tlaModuleString.append("Cardinality("); - node.getExpression().apply(this); - tlaModuleString.append(")"); - outACardExpression(node); + BType type = typechecker.getType(node.getExpression()); + if(type instanceof FunctionType){ + tlaModuleString.append("Cardinality(DOMAIN("); + node.getExpression().apply(this); + tlaModuleString.append("))"); + }else{ + tlaModuleString.append("Cardinality("); + node.getExpression().apply(this); + tlaModuleString.append(")"); + } } @Override diff --git a/src/test/java/de/tlc4b/util/TLC4BTester.java b/src/test/java/de/tlc4b/util/TLC4BTester.java index 651c0e5..438b8c0 100644 --- a/src/test/java/de/tlc4b/util/TLC4BTester.java +++ b/src/test/java/de/tlc4b/util/TLC4BTester.java @@ -7,7 +7,7 @@ public class TLC4BTester { public static void main(String[] args) throws Exception { System.setProperty("apple.awt.UIElement", "true"); // avoiding pop up windows - TLC4B.test(args,false); + TLC4B.test(args,true); } } diff --git a/src/test/resources/basics/SubstitutionsTest.mch b/src/test/resources/basics/SubstitutionsTest.mch index 17c44c4..6703ea1 100644 --- a/src/test/resources/basics/SubstitutionsTest.mch +++ b/src/test/resources/basics/SubstitutionsTest.mch @@ -6,5 +6,7 @@ OPERATIONS op1 = PRE 1 = 1 THEN x := 2 END; op2 = LET a, b, c BE a = 1 & b : {1} & c = 2 IN x := 2 END; op3 = SELECT 1=1 THEN x := 1 WHEN 1=1 THEN x:=2 ELSE x:= 3 END; -op4 = SELECT 1=1 THEN x := 1 WHEN 1=1 THEN x:=2 WHEN 1=1 THEN x:=3 ELSE x:= 4 END +op4 = SELECT 1=1 THEN x := 1 WHEN 1=1 THEN x:=2 WHEN 1=1 THEN x:=3 ELSE x:= 4 END; + +op5 = BEGIN LET p BE p = 2 IN x:= p END END END \ No newline at end of file -- GitLab