diff --git a/src/main/java/de/tla2b/analysis/AbstractASTVisitor.java b/src/main/java/de/tla2b/analysis/AbstractASTVisitor.java
index d94b61163dcda9b7ecd3d88fead074dc14494593..d8d94aff6ebde8098560ffcbf079e2360697edfd 100644
--- a/src/main/java/de/tla2b/analysis/AbstractASTVisitor.java
+++ b/src/main/java/de/tla2b/analysis/AbstractASTVisitor.java
@@ -1,18 +1,7 @@
package de.tla2b.analysis;
import de.tla2b.global.BBuiltInOPs;
-import tla2sany.semantic.ASTConstants;
-import tla2sany.semantic.AssumeNode;
-import tla2sany.semantic.AtNode;
-import tla2sany.semantic.ExprNode;
-import tla2sany.semantic.ExprOrOpArgNode;
-import tla2sany.semantic.LetInNode;
-import tla2sany.semantic.ModuleNode;
-import tla2sany.semantic.NumeralNode;
-import tla2sany.semantic.OpApplNode;
-import tla2sany.semantic.OpDefNode;
-import tla2sany.semantic.StringNode;
-import tla2sany.semantic.SubstInNode;
+import tla2sany.semantic.*;
import tlc2.tool.BuiltInOPs;
public class AbstractASTVisitor extends BuiltInOPs implements ASTConstants {
@@ -63,6 +52,10 @@ public class AbstractASTVisitor extends BuiltInOPs implements ASTConstants {
visitNumeralNode((NumeralNode) node);
return;
}
+ case DecimalKind: {
+ visitDecimalNode((DecimalNode) node);
+ return;
+ }
case StringKind: {
visitStringNode((StringNode) node);
return;
@@ -186,4 +179,7 @@ public class AbstractASTVisitor extends BuiltInOPs implements ASTConstants {
public void visitNumeralNode(NumeralNode n) {
}
+ public void visitDecimalNode(DecimalNode n) {
+ }
+
}
diff --git a/src/main/java/de/tla2b/analysis/InstanceTransformation.java b/src/main/java/de/tla2b/analysis/InstanceTransformation.java
index 5a21093d6988631ff6e33b9387bb9ca1e5c1b019..6b59d16f92e052463ae11ae46043782fa0dfe62d 100644
--- a/src/main/java/de/tla2b/analysis/InstanceTransformation.java
+++ b/src/main/java/de/tla2b/analysis/InstanceTransformation.java
@@ -3,23 +3,7 @@ package de.tla2b.analysis;
import java.util.Hashtable;
import de.tla2b.global.BBuiltInOPs;
-import tla2sany.semantic.ASTConstants;
-import tla2sany.semantic.AbortException;
-import tla2sany.semantic.AtNode;
-import tla2sany.semantic.Context;
-import tla2sany.semantic.ExprNode;
-import tla2sany.semantic.ExprOrOpArgNode;
-import tla2sany.semantic.FormalParamNode;
-import tla2sany.semantic.LetInNode;
-import tla2sany.semantic.ModuleNode;
-import tla2sany.semantic.NumeralNode;
-import tla2sany.semantic.OpApplNode;
-import tla2sany.semantic.OpArgNode;
-import tla2sany.semantic.OpDeclNode;
-import tla2sany.semantic.OpDefNode;
-import tla2sany.semantic.StringNode;
-import tla2sany.semantic.Subst;
-import tla2sany.semantic.SubstInNode;
+import tla2sany.semantic.*;
import tlc2.tool.BuiltInOPs;
import util.UniqueString;
@@ -84,6 +68,14 @@ public class InstanceTransformation extends BuiltInOPs implements ASTConstants {
return new NumeralNode(num.toString(), n.getTreeNode());
}
+ case DecimalKind: {
+ String[] image = n.toString().split("\\.");
+ if (image.length != 2) {
+ throw new IllegalStateException("expected '.' in decimal number");
+ }
+ return new DecimalNode(image[0], image[1], n.getTreeNode());
+ }
+
case StringKind: {
StringNode str = (StringNode) n;
return new StringNode(str.getTreeNode(), false);
diff --git a/src/main/java/de/tla2b/analysis/TypeChecker.java b/src/main/java/de/tla2b/analysis/TypeChecker.java
index 75775ddd4f2dd6a5b4f6f44a9985b8692a7b992b..d32b67acd2ea0beec0a6d65c9f46fac0a7b95578 100644
--- a/src/main/java/de/tla2b/analysis/TypeChecker.java
+++ b/src/main/java/de/tla2b/analysis/TypeChecker.java
@@ -1,13 +1,8 @@
package de.tla2b.analysis;
-import java.util.ArrayList;
-import java.util.HashSet;
-import java.util.Hashtable;
-import java.util.Iterator;
-import java.util.LinkedList;
-import java.util.List;
-import java.util.Set;
+import java.util.*;
import java.util.Map.Entry;
+import java.util.stream.Collectors;
import de.tla2b.config.ConfigfileEvaluator;
import de.tla2b.config.TLCValueNode;
@@ -21,21 +16,7 @@ import de.tla2b.global.BBuildIns;
import de.tla2b.global.BBuiltInOPs;
import de.tla2b.global.TranslationGlobals;
import de.tla2b.types.*;
-import tla2sany.semantic.ASTConstants;
-import tla2sany.semantic.AssumeNode;
-import tla2sany.semantic.AtNode;
-import tla2sany.semantic.ExprNode;
-import tla2sany.semantic.ExprOrOpArgNode;
-import tla2sany.semantic.FormalParamNode;
-import tla2sany.semantic.LetInNode;
-import tla2sany.semantic.ModuleNode;
-import tla2sany.semantic.NumeralNode;
-import tla2sany.semantic.OpApplNode;
-import tla2sany.semantic.OpDeclNode;
-import tla2sany.semantic.OpDefNode;
-import tla2sany.semantic.SemanticNode;
-import tla2sany.semantic.StringNode;
-import tla2sany.semantic.SymbolNode;
+import tla2sany.semantic.*;
import tlc2.tool.BuiltInOPs;
public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns, TranslationGlobals {
@@ -275,6 +256,14 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
throw new TypeErrorException(String.format("Expected %s, found INTEGER at '%s',%n%s ", expected,
((NumeralNode) exprNode).val(), exprNode.getLocation()));
}
+ case DecimalKind: {
+ try {
+ return RealType.getInstance().unify(expected);
+ } catch (UnificationException e) {
+ throw new TypeErrorException(String.format("Expected %s, found REAL at '%s',%n%s ", expected,
+ exprNode, exprNode.getLocation()));
+ }
+ }
case StringKind: {
try {
return StringType.getInstance().unify(expected);
@@ -311,10 +300,6 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
throw new RuntimeException("SubstInKind should never occur after InstanceTransformation");
}
- case DecimalKind: {
- // currently not supported
- }
-
}
throw new NotImplementedException(exprNode.toString(2));
@@ -1209,15 +1194,24 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
case B_OPCODE_mod: // % modulo
case B_OPCODE_exp: { // x hoch y, x^y
try {
- IntType.getInstance().unify(expected);
+ RealType.getInstance().unify(expected);
+ for (int i = 0; i < n.getArgs().length; i++) {
+ visitExprOrOpArgNode(n.getArgs()[i], RealType.getInstance());
+ }
+ return RealType.getInstance();
} catch (UnificationException e) {
- throw new TypeErrorException(String.format("Expected %s, found INTEGER at '%s',%n%s", expected,
+ try {
+ IntType.getInstance().unify(expected);
+ for (int i = 0; i < n.getArgs().length; i++) {
+ visitExprOrOpArgNode(n.getArgs()[i], IntType.getInstance());
+ }
+ return IntType.getInstance();
+ } catch (UnificationException e2) {
+ throw new TypeErrorException(String.format("Expected %s, found INTEGER at '%s',%n%s", expected,
n.getOperator().getName(), n.getLocation()));
+ }
}
- for (int i = 0; i < n.getArgs().length; i++) {
- visitExprOrOpArgNode(n.getArgs()[i], IntType.getInstance());
- }
- return IntType.getInstance();
+
}
case B_OPCODE_dotdot: // ..
@@ -1262,6 +1256,18 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
}
}
+ case B_OPCODE_real: // Real
+ {
+ try {
+ SetType found = new SetType(RealType.getInstance());
+ found = found.unify(expected);
+ return found;
+ } catch (UnificationException e) {
+ throw new TypeErrorException(
+ String.format("Expected %s, found POW(REAL) at 'Real',%n%s", expected, n.getLocation()));
+ }
+ }
+
case B_OPCODE_uminus: // -x
{
try {
diff --git a/src/main/java/de/tla2b/config/ModuleOverrider.java b/src/main/java/de/tla2b/config/ModuleOverrider.java
index 5e60dbbb9024cb13932536c06734f15001ad77b6..aff07f2fc3dbced2458aa15790da202f44fb5042 100644
--- a/src/main/java/de/tla2b/config/ModuleOverrider.java
+++ b/src/main/java/de/tla2b/config/ModuleOverrider.java
@@ -105,7 +105,8 @@ public class ModuleOverrider extends BuiltInOPs implements ASTConstants {
case StringKind:
case AtNodeKind: // @
- case NumeralKind: {
+ case NumeralKind:
+ case DecimalKind: {
return null;
}
diff --git a/src/main/java/de/tla2b/global/BBuildIns.java b/src/main/java/de/tla2b/global/BBuildIns.java
index a77165cb44e5c3c2df0e9d507d20afe9e9ab5bf6..40a6b50eb1c708872cbcccd22d9dcfda20a33242 100644
--- a/src/main/java/de/tla2b/global/BBuildIns.java
+++ b/src/main/java/de/tla2b/global/BBuildIns.java
@@ -29,6 +29,8 @@ public interface BBuildIns {
.uniqueStringOf("Nat");
public static final UniqueString OP_int = UniqueString
.uniqueStringOf("Int");
+ UniqueString OP_real = UniqueString
+ .uniqueStringOf("Real");
public static final UniqueString OP_bool = UniqueString
.uniqueStringOf("BOOLEAN");
public static final UniqueString OP_true = UniqueString
@@ -129,4 +131,6 @@ public interface BBuildIns {
public static final int B_OPCODE_rel_inverse = B_OPCODE_pow1 + 1;
public static final int B_OPCODE_assert = B_OPCODE_rel_inverse + 1;
+
+ int B_OPCODE_real = B_OPCODE_assert + 1;
}
diff --git a/src/main/java/de/tla2b/global/BBuiltInOPs.java b/src/main/java/de/tla2b/global/BBuiltInOPs.java
index 73a553381b845cb3e08555693437a2dde089d341..d1c1d33dae232408575fdcf042ac8fd01918edca 100644
--- a/src/main/java/de/tla2b/global/BBuiltInOPs.java
+++ b/src/main/java/de/tla2b/global/BBuiltInOPs.java
@@ -1,12 +1,11 @@
package de.tla2b.global;
-
import java.util.Hashtable;
import util.UniqueString;
public class BBuiltInOPs implements BBuildIns{
- private static Hashtable<UniqueString, Integer> B_Opcode_Table;
+ private static final Hashtable<UniqueString, Integer> B_Opcode_Table;
static {
B_Opcode_Table = new Hashtable<UniqueString, Integer>();
B_Opcode_Table.put(OP_dotdot, B_OPCODE_dotdot);
@@ -27,6 +26,7 @@ public class BBuiltInOPs implements BBuildIns{
B_Opcode_Table.put(OP_false, B_OPCODE_false);
B_Opcode_Table.put(OP_nat, B_OPCODE_nat);
B_Opcode_Table.put(OP_int, B_OPCODE_int);
+ B_Opcode_Table.put(OP_real, B_OPCODE_real);
B_Opcode_Table.put(OP_string, B_OPCODE_string);
B_Opcode_Table.put(OP_finite, B_OPCODE_finite);
diff --git a/src/main/java/de/tla2b/global/TranslationGlobals.java b/src/main/java/de/tla2b/global/TranslationGlobals.java
index 9c5c6d88426d1145faacc77a4d81860f3809448e..981b611acfda0d2fe369cd03684d5159d7a18811 100644
--- a/src/main/java/de/tla2b/global/TranslationGlobals.java
+++ b/src/main/java/de/tla2b/global/TranslationGlobals.java
@@ -26,7 +26,7 @@ public interface TranslationGlobals {
final String CHOOSE = " CHOOSE(X) == \"a member of X\"; EXTERNAL_FUNCTION_CHOOSE(T) == (POW(T)-->T)";
final String IF_THEN_ELSE = " IF_THEN_ELSE(P, a, b) == (%t_.(t_ = TRUE & P = TRUE | a )\\/%t_.(t_= TRUE & not(P= TRUE) | b ))(TRUE)";
- final ArrayList<String> STANDARD_MODULES = new ArrayList<String>(
- Arrays.asList(new String[] { "Naturals", "FiniteSets", "Integers",
- "Sequences", "TLC", "Relations", "TLA2B", "BBuildIns" }));
+ ArrayList<String> STANDARD_MODULES = new ArrayList<>(
+ Arrays.asList("Naturals", "FiniteSets", "Integers", "Reals",
+ "Sequences", "TLC", "Relations", "TLA2B", "BBuildIns"));
}
diff --git a/src/main/java/de/tla2b/output/TlaTypePrinter.java b/src/main/java/de/tla2b/output/TlaTypePrinter.java
index 210c4ac379ea3d985cd4ee244de2e6666931b40f..5d5fc8c51e5ec5233fcb1b8d90c68895f0df74be 100644
--- a/src/main/java/de/tla2b/output/TlaTypePrinter.java
+++ b/src/main/java/de/tla2b/output/TlaTypePrinter.java
@@ -10,19 +10,7 @@ import de.be4.classicalb.core.parser.node.Node;
import de.hhu.stups.sablecc.patch.PositionedNode;
import de.prob.prolog.output.IPrologTermOutput;
import de.tla2b.exceptions.NotImplementedException;
-import de.tla2b.types.BoolType;
-import de.tla2b.types.EnumType;
-import de.tla2b.types.FunctionType;
-import de.tla2b.types.IntType;
-import de.tla2b.types.ModelValueType;
-import de.tla2b.types.PairType;
-import de.tla2b.types.SetType;
-import de.tla2b.types.StringType;
-import de.tla2b.types.StructOrFunctionType;
-import de.tla2b.types.StructType;
-import de.tla2b.types.TLAType;
-import de.tla2b.types.TupleType;
-import de.tla2b.types.UntypedType;
+import de.tla2b.types.*;
public class TlaTypePrinter implements PositionPrinter, TypeVisitorInterface {
private IPrologTermOutput pout;
@@ -114,6 +102,10 @@ public class TlaTypePrinter implements PositionPrinter, TypeVisitorInterface {
pout.closeTerm();
}
+ public void caseRealType(RealType type) {
+ pout.printAtom("real");
+ }
+
public void caseSetType(SetType type) {
pout.openTerm("set");
type.getSubType().apply(this);
diff --git a/src/main/java/de/tla2b/output/TypeVisitorInterface.java b/src/main/java/de/tla2b/output/TypeVisitorInterface.java
index 5fbfc9174dacdb44eb23c58c37a3fcff34739944..2edd3469afe00119c8b69307e42b9e5c5ff66826 100644
--- a/src/main/java/de/tla2b/output/TypeVisitorInterface.java
+++ b/src/main/java/de/tla2b/output/TypeVisitorInterface.java
@@ -1,17 +1,6 @@
package de.tla2b.output;
-import de.tla2b.types.BoolType;
-import de.tla2b.types.EnumType;
-import de.tla2b.types.FunctionType;
-import de.tla2b.types.IntType;
-import de.tla2b.types.ModelValueType;
-import de.tla2b.types.PairType;
-import de.tla2b.types.SetType;
-import de.tla2b.types.StringType;
-import de.tla2b.types.StructOrFunctionType;
-import de.tla2b.types.StructType;
-import de.tla2b.types.TupleType;
-import de.tla2b.types.UntypedType;
+import de.tla2b.types.*;
public interface TypeVisitorInterface {
@@ -22,6 +11,7 @@ public interface TypeVisitorInterface {
void caseFunctionType(FunctionType type);
void caseModelValueType(ModelValueType type);
void casePairType(PairType type);
+ void caseRealType(RealType type);
void caseSetType(SetType type);
void caseStringType(StringType type);
void caseStructOrFunction(StructOrFunctionType type);
diff --git a/src/main/java/de/tla2b/translation/OperationsFinder.java b/src/main/java/de/tla2b/translation/OperationsFinder.java
index 6ee42491b342516b2f977760dcd5b59729db930e..dbe48dcef54b934433d1eb5a7a156e2439e4997e 100644
--- a/src/main/java/de/tla2b/translation/OperationsFinder.java
+++ b/src/main/java/de/tla2b/translation/OperationsFinder.java
@@ -47,7 +47,8 @@ public class OperationsFinder extends AbstractASTVisitor implements
visitOpApplNode((OpApplNode) n);
return;
}
- case NumeralKind: {
+ case NumeralKind:
+ case DecimalKind: {
throw new RuntimeException(String.format(
"Expected an action (instead of a number).%n%s", n.getLocation().toString()));
}
diff --git a/src/main/java/de/tla2b/types/IType.java b/src/main/java/de/tla2b/types/IType.java
index fcb3bbd32f3d76b8a7756324dfb8b2fe89123cb7..2f1f877aa3369a4672c15a674fdddf351aea1ce8 100644
--- a/src/main/java/de/tla2b/types/IType.java
+++ b/src/main/java/de/tla2b/types/IType.java
@@ -3,19 +3,21 @@ package de.tla2b.types;
import de.tla2b.output.TypeVisitorInterface;
public interface IType {
- public final int UNTYPED = 0;
- public final int INTEGER = 1;
- public final int BOOL = 2;
- public final int STRING = 3;
- public final int MODELVALUE = 4;
- public final int POW = 5;
- public final int PAIR = 6;
- public final int STRUCT = 7;
- public final int TUPLEORSEQ =8;
- public final int STRUCT_OR_FUNCTION = 9;
- public final int FUNCTION = 10;
- public final int TUPLE = 11;
- public final int TUPLE_OR_FUNCTION =12;
+ int UNTYPED = 0;
+ int INTEGER = 1;
+ int BOOL = 2;
+ int STRING = 3;
+ int MODELVALUE = 4;
+ int POW = 5;
+ int PAIR = 6;
+ int STRUCT = 7;
+ int TUPLEORSEQ = 8;
+ int STRUCT_OR_FUNCTION = 9;
+ int FUNCTION = 10;
+ int TUPLE = 11;
+ int TUPLE_OR_FUNCTION = 12;
+ int REAL = 13;
+
void apply(TypeVisitorInterface visitor);
}
diff --git a/src/main/java/de/tla2b/types/RealType.java b/src/main/java/de/tla2b/types/RealType.java
new file mode 100644
index 0000000000000000000000000000000000000000..f0becfe519d4038fae55fecdf7fc314fd105948b
--- /dev/null
+++ b/src/main/java/de/tla2b/types/RealType.java
@@ -0,0 +1,65 @@
+package de.tla2b.types;
+
+import de.be4.classicalb.core.parser.node.ARealSetExpression;
+import de.be4.classicalb.core.parser.node.PExpression;
+import de.tla2b.exceptions.UnificationException;
+import de.tla2b.output.TypeVisitorInterface;
+
+public class RealType extends TLAType {
+
+ private static final RealType instance = new RealType();
+
+ private RealType() {
+ super(REAL);
+ }
+
+ public static RealType getInstance() {
+ return instance;
+ }
+
+ @Override
+ public String toString() {
+ return "REAL";
+ }
+
+ @Override
+ public boolean isUntyped() {
+ return false;
+ }
+
+ @Override
+ public boolean compare(TLAType o) {
+ return o.getKind() == UNTYPED || o.getKind() == REAL;
+ }
+
+ @Override
+ public RealType unify(TLAType o) throws UnificationException {
+ if (o.getKind() == REAL) {
+ return this;
+ } else if (o instanceof UntypedType) {
+ ((UntypedType) o).setFollowersTo(this);
+ return this;
+ } else
+ throw new UnificationException();
+ }
+
+ @Override
+ public RealType cloneTLAType() {
+ return this;
+ }
+
+ @Override
+ public boolean contains(TLAType o) {
+ return false;
+ }
+
+ @Override
+ public PExpression getBNode() {
+ return new ARealSetExpression();
+ }
+
+ public void apply(TypeVisitorInterface visitor) {
+ visitor.caseRealType(this);
+ }
+
+}
diff --git a/src/main/java/de/tla2bAst/BAstCreator.java b/src/main/java/de/tla2bAst/BAstCreator.java
index bfbc8ecce8303dc0371cf125488bcf3fd9edeff2..ff61c9d6cfeca5fc4f26268a1855ce50269aa0a5 100644
--- a/src/main/java/de/tla2bAst/BAstCreator.java
+++ b/src/main/java/de/tla2bAst/BAstCreator.java
@@ -10,22 +10,7 @@ import java.util.List;
import java.util.Map.Entry;
import java.util.Set;
-import tla2sany.semantic.ASTConstants;
-import tla2sany.semantic.AssumeNode;
-import tla2sany.semantic.AtNode;
-import tla2sany.semantic.ExprNode;
-import tla2sany.semantic.ExprOrOpArgNode;
-import tla2sany.semantic.FormalParamNode;
-import tla2sany.semantic.LetInNode;
-import tla2sany.semantic.ModuleNode;
-import tla2sany.semantic.NumeralNode;
-import tla2sany.semantic.OpApplNode;
-import tla2sany.semantic.OpDeclNode;
-import tla2sany.semantic.OpDefNode;
-import tla2sany.semantic.SemanticNode;
-import tla2sany.semantic.StringNode;
-import tla2sany.semantic.SymbolNode;
-import tla2sany.semantic.ThmOrAssumpDefNode;
+import tla2sany.semantic.*;
import tla2sany.st.Location;
import tlc2.tool.BuiltInOPs;
import tlc2.value.ModelValue;
@@ -663,6 +648,9 @@ public class BAstCreator extends BuiltInOPs
String number = String.valueOf(((NumeralNode) exprNode).val());
return createPositionedNode(new AIntegerExpression(new TIntegerLiteral(number)), exprNode);
}
+ case DecimalKind: {
+ return createPositionedNode(new ARealExpression(new TRealLiteral(exprNode.toString())), exprNode);
+ }
case StringKind: {
StringNode s = (StringNode) exprNode;
return createPositionedNode(new AStringExpression(new TStringLiteral(s.getRep().toString())), exprNode);
@@ -1079,6 +1067,10 @@ public class BAstCreator extends BuiltInOPs
returnNode = new AIntegerSetExpression();
break;
+ case B_OPCODE_real: // Real
+ returnNode = new ARealSetExpression();
+ break;
+
case B_OPCODE_uminus: // -x
returnNode = new AUnaryMinusExpression(visitExprOrOpArgNodeExpression(opApplNode.getArgs()[0]));
break;