Skip to content
Snippets Groups Projects
Commit d7f630a0 authored by hansen's avatar hansen
Browse files

Fixed a bug translating LET IN statements

parent 8c8485b7
No related branches found
No related tags found
No related merge requests found
...@@ -1367,8 +1367,13 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker { ...@@ -1367,8 +1367,13 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
throw new TypeErrorException("Excepted '" + expected + "' , found " throw new TypeErrorException("Excepted '" + expected + "' , found "
+ found + "'"); + found + "'");
} }
setType(node.getExpression(), new SetType(new UntypedType()));
setType(node.getExpression(), new UntypedType());
node.getExpression().apply(this); node.getExpression().apply(this);
BType type = getType(node.getExpression());
if (! (type instanceof FunctionType)){
new SetType(new UntypedType()).unify(type, this);
}
} }
@Override @Override
......
...@@ -920,7 +920,12 @@ public class TLAPrinter extends DepthFirstAdapter { ...@@ -920,7 +920,12 @@ public class TLAPrinter extends DepthFirstAdapter {
tlaModuleString.append(" : "); tlaModuleString.append(" : ");
} }
if (typeRestrictor.isARemovedNode(node.getPredicate())) {
tlaModuleString.append("TRUE");
} else {
node.getPredicate().apply(this); node.getPredicate().apply(this);
}
tlaModuleString.append(" /\\ "); tlaModuleString.append(" /\\ ");
node.getSubstitution().apply(this); node.getSubstitution().apply(this);
printUnchangedVariables(node, true); printUnchangedVariables(node, true);
...@@ -2050,11 +2055,16 @@ public class TLAPrinter extends DepthFirstAdapter { ...@@ -2050,11 +2055,16 @@ public class TLAPrinter extends DepthFirstAdapter {
@Override @Override
public void caseACardExpression(ACardExpression node) { public void caseACardExpression(ACardExpression node) {
inACardExpression(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("); tlaModuleString.append("Cardinality(");
node.getExpression().apply(this); node.getExpression().apply(this);
tlaModuleString.append(")"); tlaModuleString.append(")");
outACardExpression(node); }
} }
@Override @Override
......
...@@ -7,7 +7,7 @@ public class TLC4BTester { ...@@ -7,7 +7,7 @@ public class TLC4BTester {
public static void main(String[] args) throws Exception { public static void main(String[] args) throws Exception {
System.setProperty("apple.awt.UIElement", "true"); // avoiding pop up windows System.setProperty("apple.awt.UIElement", "true"); // avoiding pop up windows
TLC4B.test(args,false); TLC4B.test(args,true);
} }
} }
...@@ -6,5 +6,7 @@ OPERATIONS ...@@ -6,5 +6,7 @@ OPERATIONS
op1 = PRE 1 = 1 THEN x := 2 END; op1 = PRE 1 = 1 THEN x := 2 END;
op2 = LET a, b, c BE a = 1 & b : {1} & c = 2 IN 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; 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 END
\ No newline at end of file
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment