From 4ca233ba03ebf5559d0594fe67b24a9cc7b6e52f Mon Sep 17 00:00:00 2001
From: Jan Gruteser <jan.gruteser@hhu.de>
Date: Sun, 28 Apr 2024 08:35:13 +0200
Subject: [PATCH] apply IntelliJ reformat code to fix many indents
---
src/main/java/de/tla2b/TLA2B.java | 10 +-
.../de/tla2b/analysis/AbstractASTVisitor.java | 100 +-
.../java/de/tla2b/analysis/BOperation.java | 212 +-
.../analysis/InstanceTransformation.java | 332 +--
.../tla2b/analysis/PredicateVsExpression.java | 100 +-
.../tla2b/analysis/RecursiveDefinition.java | 14 +-
.../de/tla2b/analysis/RecursiveFunktion.java | 2 +-
.../java/de/tla2b/analysis/SpecAnalyser.java | 118 +-
.../java/de/tla2b/analysis/SymbolRenamer.java | 190 +-
.../java/de/tla2b/analysis/SymbolSorter.java | 20 +-
.../java/de/tla2b/analysis/TypeChecker.java | 1884 ++++++++---------
.../tla2b/analysis/UsedExternalFunctions.java | 34 +-
.../de/tla2b/config/ConfigfileEvaluator.java | 83 +-
.../java/de/tla2b/config/ModuleOverrider.java | 186 +-
.../java/de/tla2b/config/TLCValueNode.java | 4 +-
src/main/java/de/tla2b/config/ValueObj.java | 6 +-
.../exceptions/ConfigFileErrorException.java | 2 +-
.../tla2b/exceptions/FrontEndException.java | 5 +-
.../exceptions/ModuleErrorException.java | 4 +-
.../exceptions/NotImplementedException.java | 2 +-
.../exceptions/SemanticErrorException.java | 4 +-
.../de/tla2b/exceptions/TLA2BException.java | 4 +-
.../de/tla2b/exceptions/TLA2BIOException.java | 4 +-
.../exceptions/UnificationException.java | 3 +-
src/main/java/de/tla2b/global/BBuildIns.java | 80 +-
.../java/de/tla2b/global/BBuiltInOPs.java | 29 +-
.../java/de/tla2b/global/OperatorTypes.java | 4 +-
src/main/java/de/tla2b/global/Priorities.java | 56 +-
.../de/tla2b/global/TranslationGlobals.java | 10 +-
.../java/de/tla2b/global/VersionHelper.java | 3 +-
.../java/de/tla2b/output/Indentation.java | 19 +-
.../java/de/tla2b/output/PrologPrinter.java | 24 +-
.../java/de/tla2b/output/TlaTypePrinter.java | 10 +-
.../de/tla2b/output/TypeVisitorInterface.java | 14 +-
.../tla2b/translation/BDefinitionsFinder.java | 17 +-
.../de/tla2b/translation/BMacroHandler.java | 73 +-
.../tla2b/translation/OperationsFinder.java | 167 +-
.../translation/RecursiveFunctionHandler.java | 66 +-
.../translation/UsedDefinitionsFinder.java | 10 +-
.../de/tla2b/types/AbstractHasFollowers.java | 5 +-
.../java/de/tla2b/types/AbstractSymbol.java | 6 +-
src/main/java/de/tla2b/types/BoolType.java | 4 +-
src/main/java/de/tla2b/types/EnumType.java | 10 +-
.../java/de/tla2b/types/FunctionType.java | 8 +-
src/main/java/de/tla2b/types/IType.java | 4 +-
.../java/de/tla2b/types/ModelValueType.java | 6 +-
src/main/java/de/tla2b/types/PairType.java | 4 +-
src/main/java/de/tla2b/types/SetType.java | 14 +-
.../de/tla2b/types/StructOrFunctionType.java | 14 +-
src/main/java/de/tla2b/types/StructType.java | 18 +-
src/main/java/de/tla2b/types/TLAType.java | 12 +-
.../java/de/tla2b/types/TupleOrFunction.java | 28 +-
src/main/java/de/tla2b/types/TupleType.java | 6 +-
src/main/java/de/tla2b/types/UntypedType.java | 10 +-
src/main/java/de/tla2b/util/FileUtils.java | 9 +-
.../de/tla2bAst/ExpressionTranslator.java | 172 +-
src/main/java/de/tla2bAst/SimpleResolver.java | 8 +-
src/main/java/de/tla2bAst/Translator.java | 43 +-
58 files changed, 2085 insertions(+), 2201 deletions(-)
diff --git a/src/main/java/de/tla2b/TLA2B.java b/src/main/java/de/tla2b/TLA2B.java
index cc760f0..b41976d 100644
--- a/src/main/java/de/tla2b/TLA2B.java
+++ b/src/main/java/de/tla2b/TLA2B.java
@@ -5,13 +5,7 @@ import de.tla2b.exceptions.NotImplementedException;
import de.tla2b.exceptions.TLA2BException;
import de.tla2b.global.TranslationGlobals;
import de.tla2bAst.Translator;
-
-import org.apache.commons.cli.CommandLine;
-import org.apache.commons.cli.DefaultParser;
-import org.apache.commons.cli.HelpFormatter;
-import org.apache.commons.cli.Option;
-import org.apache.commons.cli.Options;
-import org.apache.commons.cli.ParseException;
+import org.apache.commons.cli.*;
public class TLA2B implements TranslationGlobals {
public final static String VERSION = "version";
@@ -84,7 +78,7 @@ public class TLA2B implements TranslationGlobals {
Options options = new Options();
options.addOption(VERSION, false, "prints the current version of TLA2B");
options.addOption(VERBOSE, false, "makes output more verbose (not used yet)");
-
+
Option config = Option.builder("config")
.argName("file")
.hasArg()
diff --git a/src/main/java/de/tla2b/analysis/AbstractASTVisitor.java b/src/main/java/de/tla2b/analysis/AbstractASTVisitor.java
index 075a150..592c9da 100644
--- a/src/main/java/de/tla2b/analysis/AbstractASTVisitor.java
+++ b/src/main/java/de/tla2b/analysis/AbstractASTVisitor.java
@@ -44,65 +44,65 @@ public class AbstractASTVisitor extends BuiltInOPs implements ASTConstants {
public void visitExprNode(ExprNode node) {
switch (node.getKind()) {
- case OpApplKind: {
- visitOpApplNode((OpApplNode) node);
- return;
- }
- case NumeralKind: {
- visitNumeralNode((NumeralNode) node);
- return;
- }
- case DecimalKind: {
- visitDecimalNode((DecimalNode) node);
- return;
- }
- case StringKind: {
- visitStringNode((StringNode) node);
- return;
- }
- case SubstInKind: {
- visitStubstInNode((SubstInNode) node);
- return;
- }
- case AtNodeKind: { // @
- visitAtNode((AtNode) node);
- return;
- }
- case LetInKind: {
- visitLetInNode((LetInNode) node);
- }
+ case OpApplKind: {
+ visitOpApplNode((OpApplNode) node);
+ return;
+ }
+ case NumeralKind: {
+ visitNumeralNode((NumeralNode) node);
+ return;
+ }
+ case DecimalKind: {
+ visitDecimalNode((DecimalNode) node);
+ return;
+ }
+ case StringKind: {
+ visitStringNode((StringNode) node);
+ return;
+ }
+ case SubstInKind: {
+ visitStubstInNode((SubstInNode) node);
+ return;
+ }
+ case AtNodeKind: { // @
+ visitAtNode((AtNode) node);
+ return;
+ }
+ case LetInKind: {
+ visitLetInNode((LetInNode) node);
+ }
}
}
public void visitOpApplNode(OpApplNode node) {
switch (node.getOperator().getKind()) {
- case VariableDeclKind: {
- visitVariableNode(node);
- return;
- }
- case ConstantDeclKind: {
- visitConstantNode(node);
- return;
- }
-
- case FormalParamKind: {
- visitFormalParamNode(node);
- return;
- }
+ case VariableDeclKind: {
+ visitVariableNode(node);
+ return;
+ }
+ case ConstantDeclKind: {
+ visitConstantNode(node);
+ return;
+ }
- case BuiltInKind: {
- visitBuiltInNode(node);
- return;
- }
+ case FormalParamKind: {
+ visitFormalParamNode(node);
+ return;
+ }
- case UserDefinedOpKind: {
- if (BBuiltInOPs.contains(node.getOperator().getName())) {
- visitBBuiltinsNode(node);
- } else {
- visitUserDefinedNode(node);
+ case BuiltInKind: {
+ visitBuiltInNode(node);
+ return;
}
- }
+ case UserDefinedOpKind: {
+ if (BBuiltInOPs.contains(node.getOperator().getName())) {
+ visitBBuiltinsNode(node);
+ } else {
+ visitUserDefinedNode(node);
+ }
+
+ }
}
}
diff --git a/src/main/java/de/tla2b/analysis/BOperation.java b/src/main/java/de/tla2b/analysis/BOperation.java
index 84fd88d..f9a9d72 100644
--- a/src/main/java/de/tla2b/analysis/BOperation.java
+++ b/src/main/java/de/tla2b/analysis/BOperation.java
@@ -1,37 +1,19 @@
package de.tla2b.analysis;
-import java.util.*;
-import java.util.Map.Entry;
-
-import de.be4.classicalb.core.parser.node.AAnySubstitution;
-import de.be4.classicalb.core.parser.node.AAssignSubstitution;
-import de.be4.classicalb.core.parser.node.ABlockSubstitution;
-import de.be4.classicalb.core.parser.node.AMemberPredicate;
-import de.be4.classicalb.core.parser.node.AOperation;
-import de.be4.classicalb.core.parser.node.ASelectSubstitution;
-import de.be4.classicalb.core.parser.node.ASkipSubstitution;
-import de.be4.classicalb.core.parser.node.PExpression;
-import de.be4.classicalb.core.parser.node.PPredicate;
+import de.be4.classicalb.core.parser.node.*;
import de.tla2b.global.BBuiltInOPs;
import de.tla2b.global.TranslationGlobals;
import de.tla2b.types.TLAType;
import de.tla2bAst.BAstCreator;
-import tla2sany.semantic.ASTConstants;
-import tla2sany.semantic.ExprNode;
-import tla2sany.semantic.ExprOrOpArgNode;
-import tla2sany.semantic.FormalParamNode;
-import tla2sany.semantic.LetInNode;
-import tla2sany.semantic.OpApplNode;
-import tla2sany.semantic.OpDeclNode;
-import tla2sany.semantic.OpDefNode;
-import tla2sany.semantic.SemanticNode;
-import tla2sany.semantic.SubstInNode;
-import tla2sany.semantic.SymbolNode;
+import tla2sany.semantic.*;
import tlc2.tool.BuiltInOPs;
import tlc2.tool.ToolGlobals;
+import java.util.*;
+import java.util.Map.Entry;
+
public class BOperation extends BuiltInOPs implements ASTConstants,
- ToolGlobals, TranslationGlobals {
+ ToolGlobals, TranslationGlobals {
private final String name;
private final ExprNode node;
private final ArrayList<OpApplNode> existQuans;
@@ -46,7 +28,7 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
private final SpecAnalyser specAnalyser;
public BOperation(String name, ExprNode n,
- ArrayList<OpApplNode> existQuans, SpecAnalyser specAnalyser) {
+ ArrayList<OpApplNode> existQuans, SpecAnalyser specAnalyser) {
this.name = name;
this.node = n;
this.existQuans = existQuans;
@@ -72,7 +54,7 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
ArrayList<PPredicate> whereList = new ArrayList<>();
for (int j = 0; j < this.getFormalParams().size(); j++) {
paramList.add(bASTCreator.createIdentifierNode(this
- .getFormalParams().get(j)));
+ .getFormalParams().get(j)));
}
for (int j = 0; j < this.getExistQuans().size(); j++) {
OpApplNode o = this.getExistQuans().get(j);
@@ -91,9 +73,9 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
ArrayList<PExpression> rightSideOfAssigment = new ArrayList<>();
for (Entry<SymbolNode, ExprOrOpArgNode> entry : assignments.entrySet()) {
leftSideOfAssigment.add(bASTCreator.createIdentifierNode(entry
- .getKey()));
+ .getKey()));
rightSideOfAssigment.add(bASTCreator
- .visitExprOrOpArgNodeExpression(entry.getValue()));
+ .visitExprOrOpArgNodeExpression(entry.getValue()));
}
AAssignSubstitution assign = new AAssignSubstitution();
if (!anyVariables.isEmpty()) { // ANY x_n WHERE P THEN A END
@@ -112,7 +94,7 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
whereList.add(member);
leftSideOfAssigment.add(bASTCreator.createIdentifierNode(var));
rightSideOfAssigment.add(BAstCreator
- .createIdentifierNode(nextName));
+ .createIdentifierNode(nextName));
}
any.setIdentifiers(anyParams);
@@ -145,21 +127,21 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
}
private ArrayList<PPredicate> createBeforeAfterPredicates(
- BAstCreator bAstCreator) {
+ BAstCreator bAstCreator) {
ArrayList<PPredicate> predicates = new ArrayList<>();
for (ExprOrOpArgNode e : beforeAfterPredicates) {
PPredicate body = null;
if (e instanceof OpApplNode) {
OpApplNode opApplNode = (OpApplNode) e;
if (opApplNode.getOperator().getKind() == UserDefinedOpKind
- && !BBuiltInOPs.contains(opApplNode.getOperator()
- .getName())) {
+ && !BBuiltInOPs.contains(opApplNode.getOperator()
+ .getName())) {
OpDefNode def = (OpDefNode) opApplNode.getOperator();
FormalParamNode[] params = def.getParams();
for (int j = 0; j < params.length; j++) {
FormalParamNode param = params[j];
param.setToolObject(SUBSTITUTE_PARAM,
- opApplNode.getArgs()[j]);
+ opApplNode.getArgs()[j]);
}
body = bAstCreator.visitExprNodePredicate(def.getBody());
}
@@ -174,7 +156,7 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
private void findAssignments() {
PrimedVariablesFinder primedVariablesFinder = new PrimedVariablesFinder(
- beforeAfterPredicates);
+ beforeAfterPredicates);
for (ExprOrOpArgNode node : new ArrayList<>(
beforeAfterPredicates)) {
if (node instanceof OpApplNode) {
@@ -182,7 +164,7 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
if (opApplNode.getOperator().getKind() == BuiltInKind) {
if (OPCODE_eq == getOpCode(opApplNode.getOperator()
- .getName())) {
+ .getName())) {
ExprOrOpArgNode arg1 = opApplNode.getArgs()[0]; // we have equality arg1 = RHS
try {
OpApplNode arg11 = (OpApplNode) arg1;
@@ -191,14 +173,14 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
SymbolNode var = v.getOperator();
// we have equality var' = RHS
if (!primedVariablesFinder
- .getTwiceUsedVariables().contains(var)) {
+ .getTwiceUsedVariables().contains(var)) {
// var' is only used once in all before after predicates
// meaning we do not need it as parameter of the ANY
// and can add an assignment var := RHS
assignments.put(v.getOperator(),
- opApplNode.getArgs()[1]); // RHS of assignment
+ opApplNode.getArgs()[1]); // RHS of assignment
beforeAfterPredicates.remove(node);
- // System.out.println("Detected assignment " + var.getName().toString() + "' = <RHS>");
+ // System.out.println("Detected assignment " + var.getName().toString() + "' = <RHS>");
}
}
@@ -224,28 +206,28 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
OpApplNode opApplNode = (OpApplNode) node;
if (opApplNode.getOperator().getKind() == BuiltInKind) {
switch (getOpCode(opApplNode.getOperator().getName())) {
- case OPCODE_land: // \land
- {
- separateGuardsAndBeforeAfterPredicates(opApplNode.getArgs()[0]);
- separateGuardsAndBeforeAfterPredicates(opApplNode.getArgs()[1]);
- return;
- }
- case OPCODE_cl: // $ConjList
- {
- for (int i = 0; i < opApplNode.getArgs().length; i++) {
- separateGuardsAndBeforeAfterPredicates(opApplNode
+ case OPCODE_land: // \land
+ {
+ separateGuardsAndBeforeAfterPredicates(opApplNode.getArgs()[0]);
+ separateGuardsAndBeforeAfterPredicates(opApplNode.getArgs()[1]);
+ return;
+ }
+ case OPCODE_cl: // $ConjList
+ {
+ for (int i = 0; i < opApplNode.getArgs().length; i++) {
+ separateGuardsAndBeforeAfterPredicates(opApplNode
.getArgs()[i]);
+ }
+ return;
}
- return;
- }
- default: {
- if (opApplNode.level < 2) {
- guards.add(node); // should we be checking nonLeibnizParams is empty ?
- } else {
- beforeAfterPredicates.add(node);
+ default: {
+ if (opApplNode.level < 2) {
+ guards.add(node); // should we be checking nonLeibnizParams is empty ?
+ } else {
+ beforeAfterPredicates.add(node);
+ }
+ return;
}
- return;
- }
}
}
@@ -264,9 +246,9 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
for (OpApplNode n : existQuans) {
FormalParamNode[][] params = n.getBdedQuantSymbolLists();
for (FormalParamNode[] param : params) {
- for (int j = 0; j < param.length; j++) {
- formalParams.add(param[j]);
- opParams.add(param[j].getName().toString());
+ for (FormalParamNode formalParamNode : param) {
+ formalParams.add(formalParamNode);
+ opParams.add(formalParamNode.getName().toString());
}
}
}
@@ -313,20 +295,20 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
private void findUnchangedVaribalesInSemanticNode(SemanticNode node) {
switch (node.getKind()) {
- case OpApplKind: {
- findUnchangedVariablesInOpApplNode((OpApplNode) node);
- return;
- }
- case LetInKind: {
- LetInNode letNode = (LetInNode) node;
- findUnchangedVaribalesInSemanticNode(letNode.getBody());
- return;
- }
+ case OpApplKind: {
+ findUnchangedVariablesInOpApplNode((OpApplNode) node);
+ return;
+ }
+ case LetInKind: {
+ LetInNode letNode = (LetInNode) node;
+ findUnchangedVaribalesInSemanticNode(letNode.getBody());
+ return;
+ }
- case SubstInKind: {
- SubstInNode substInNode = (SubstInNode) node;
- findUnchangedVaribalesInSemanticNode(substInNode.getBody());
- }
+ case SubstInKind: {
+ SubstInNode substInNode = (SubstInNode) node;
+ findUnchangedVaribalesInSemanticNode(substInNode.getBody());
+ }
}
}
@@ -334,62 +316,62 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
int kind = n.getOperator().getKind();
if (kind == UserDefinedOpKind
- && !BBuiltInOPs.contains(n.getOperator().getName())) {
+ && !BBuiltInOPs.contains(n.getOperator().getName())) {
OpDefNode def = (OpDefNode) n.getOperator();
findUnchangedVaribalesInSemanticNode(def.getBody());
} else if (kind == BuiltInKind) {
int opcode = BuiltInOPs.getOpCode(n.getOperator().getName());
switch (opcode) {
- case OPCODE_land: // \land
- case OPCODE_cl: { // $ConjList
- for (int i = 0; i < n.getArgs().length; i++) {
- findUnchangedVaribalesInSemanticNode(n.getArgs()[i]);
+ case OPCODE_land: // \land
+ case OPCODE_cl: { // $ConjList
+ for (int i = 0; i < n.getArgs().length; i++) {
+ findUnchangedVaribalesInSemanticNode(n.getArgs()[i]);
+ }
+ return;
}
- return;
- }
- case OPCODE_unchanged: {
- n.setToolObject(USED, false);
- OpApplNode k = (OpApplNode) n.getArgs()[0];
- if (k.getOperator().getKind() == VariableDeclKind) {
- unchangedVariablesList.add((OpDeclNode) k.getOperator());
- String name = k.getOperator().getName().toString();
- unchangedVariables.add(name);
- } else {
- // Tuple
- for (int i = 0; i < k.getArgs().length; i++) {
- OpApplNode var = (OpApplNode) k.getArgs()[i];
- //findUnchangedVariablesInOpApplNode(var);
- // System.out.println("var.getOperator() = " + var.getOperator().getName() + " at " + var.getOperator() + " of class " + var.getOperator().getClass().getSimpleName());
- if(var.getOperator() instanceof OpDefNode) {
- // we have a definition
- OpDefNode def = (OpDefNode) var.getOperator();
- if(def.getParams().length > 0) {
- // we do not support definitions with arguments yet
- throw new RuntimeException("Declaration with parameters not supported for UNCHANGED: " + var.getOperator().getName() + " " + var.getLocation());
- }
- ExprNode body = def.getBody();
- // System.out.println("Body = " + body + " of class " + body.getClass().getSimpleName());
- if(body instanceof OpApplNode) {
- OpApplNode obody = (OpApplNode) body;
- // System.out.println("Operator = " + obody.getOperator()); // In module --TLA+ BUILTINS--
- findUnchangedVariablesInOpApplNode(obody);
- }
- } else if(!(var.getOperator() instanceof OpDeclNode)) {
- throw new RuntimeException("Cannot convert to list of UNCHANGED variables: " + var.getOperator().getName() + " " + var.getLocation());
- } else {
- unchangedVariablesList.add((OpDeclNode) var
+ case OPCODE_unchanged: {
+ n.setToolObject(USED, false);
+ OpApplNode k = (OpApplNode) n.getArgs()[0];
+ if (k.getOperator().getKind() == VariableDeclKind) {
+ unchangedVariablesList.add((OpDeclNode) k.getOperator());
+ String name = k.getOperator().getName().toString();
+ unchangedVariables.add(name);
+ } else {
+ // Tuple
+ for (int i = 0; i < k.getArgs().length; i++) {
+ OpApplNode var = (OpApplNode) k.getArgs()[i];
+ //findUnchangedVariablesInOpApplNode(var);
+ // System.out.println("var.getOperator() = " + var.getOperator().getName() + " at " + var.getOperator() + " of class " + var.getOperator().getClass().getSimpleName());
+ if (var.getOperator() instanceof OpDefNode) {
+ // we have a definition
+ OpDefNode def = (OpDefNode) var.getOperator();
+ if (def.getParams().length > 0) {
+ // we do not support definitions with arguments yet
+ throw new RuntimeException("Declaration with parameters not supported for UNCHANGED: " + var.getOperator().getName() + " " + var.getLocation());
+ }
+ ExprNode body = def.getBody();
+ // System.out.println("Body = " + body + " of class " + body.getClass().getSimpleName());
+ if (body instanceof OpApplNode) {
+ OpApplNode obody = (OpApplNode) body;
+ // System.out.println("Operator = " + obody.getOperator()); // In module --TLA+ BUILTINS--
+ findUnchangedVariablesInOpApplNode(obody);
+ }
+ } else if (!(var.getOperator() instanceof OpDeclNode)) {
+ throw new RuntimeException("Cannot convert to list of UNCHANGED variables: " + var.getOperator().getName() + " " + var.getLocation());
+ } else {
+ unchangedVariablesList.add((OpDeclNode) var
.getOperator());
- String name = var.getOperator().getName().toString();
- unchangedVariables.add(name);
+ String name = var.getOperator().getName().toString();
+ unchangedVariables.add(name);
+ }
}
}
}
- }
}
}
}
-
+
}
diff --git a/src/main/java/de/tla2b/analysis/InstanceTransformation.java b/src/main/java/de/tla2b/analysis/InstanceTransformation.java
index c5732a4..a11ae97 100644
--- a/src/main/java/de/tla2b/analysis/InstanceTransformation.java
+++ b/src/main/java/de/tla2b/analysis/InstanceTransformation.java
@@ -1,12 +1,12 @@
package de.tla2b.analysis;
-import java.util.Hashtable;
-
import de.tla2b.global.BBuiltInOPs;
import tla2sany.semantic.*;
import tlc2.tool.BuiltInOPs;
import util.UniqueString;
+import java.util.Hashtable;
+
public class InstanceTransformation extends BuiltInOPs implements ASTConstants {
final OpDefNode[] defs;
@@ -46,7 +46,7 @@ public class InstanceTransformation extends BuiltInOPs implements ASTConstants {
}
private ExprOrOpArgNode generateNewExprOrOpArgNode(ExprOrOpArgNode n,
- String prefix) throws AbortException {
+ String prefix) throws AbortException {
if (n instanceof ExprNode) {
return generateNewExprNode((ExprNode) n, prefix);
} else {
@@ -55,236 +55,236 @@ public class InstanceTransformation extends BuiltInOPs implements ASTConstants {
}
private ExprNode generateNewExprNode(ExprNode n, String prefix)
- throws AbortException {
+ throws AbortException {
switch (n.getKind()) {
- case OpApplKind: {
- return generateNewOpApplNode((OpApplNode) n, prefix);
- }
+ case OpApplKind: {
+ return generateNewOpApplNode((OpApplNode) n, prefix);
+ }
- case NumeralKind: {
- NumeralNode num = (NumeralNode) n;
- return new NumeralNode(num.toString(), n.getTreeNode());
- }
+ case NumeralKind: {
+ NumeralNode num = (NumeralNode) n;
+ 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");
+ 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());
}
- return new DecimalNode(image[0], image[1], n.getTreeNode());
- }
- case StringKind: {
- StringNode str = (StringNode) n;
- return new StringNode(str.getTreeNode(), false);
- }
+ case StringKind: {
+ StringNode str = (StringNode) n;
+ return new StringNode(str.getTreeNode(), false);
+ }
- case SubstInKind: {
- SubstInNode substInNode = (SubstInNode) n;
+ case SubstInKind: {
+ SubstInNode substInNode = (SubstInNode) n;
- Subst[] subs = substInNode.getSubsts();
- for (Subst sub : subs) {
- OpDeclNode op = sub.getOp();
- ExprOrOpArgNode expr = sub.getExpr();
- op.setToolObject(substitutionId, expr);
+ Subst[] subs = substInNode.getSubsts();
+ for (Subst sub : subs) {
+ OpDeclNode op = sub.getOp();
+ ExprOrOpArgNode expr = sub.getExpr();
+ op.setToolObject(substitutionId, expr);
+ }
+ return generateNewExprNode(substInNode.getBody(), prefix);
}
- return generateNewExprNode(substInNode.getBody(), prefix);
- }
- case AtNodeKind: { // @
- AtNode old = (AtNode) n;
- OpApplNode oldExcept = old.getExceptRef();
- OpApplNode newExcept = (OpApplNode) oldExcept
+ case AtNodeKind: { // @
+ AtNode old = (AtNode) n;
+ OpApplNode oldExcept = old.getExceptRef();
+ OpApplNode newExcept = (OpApplNode) oldExcept
.getToolObject(substitutionId);
- OpApplNode oldComponent = old.getExceptComponentRef();
- OpApplNode newComponent = (OpApplNode) oldComponent
+ OpApplNode oldComponent = old.getExceptComponentRef();
+ OpApplNode newComponent = (OpApplNode) oldComponent
.getToolObject(substitutionId);
- return new AtNode(newExcept, newComponent);
- }
+ return new AtNode(newExcept, newComponent);
+ }
- case LetInKind: {
- LetInNode oldLetNode = (LetInNode) n;
- OpDefNode[] newLets = new OpDefNode[oldLetNode.getLets().length];
- Context cc = oldLetNode.context;
- for (int i = 0; i < oldLetNode.getLets().length; i++) {
- OpDefNode let = oldLetNode.getLets()[i];
- UniqueString newName = UniqueString.uniqueStringOf(prefix
+ case LetInKind: {
+ LetInNode oldLetNode = (LetInNode) n;
+ OpDefNode[] newLets = new OpDefNode[oldLetNode.getLets().length];
+ Context cc = oldLetNode.context;
+ for (int i = 0; i < oldLetNode.getLets().length; i++) {
+ OpDefNode let = oldLetNode.getLets()[i];
+ UniqueString newName = UniqueString.uniqueStringOf(prefix
+ let.getName().toString());
- OpDefNode newLet = new OpDefNode(newName, let.getKind(),
+ OpDefNode newLet = new OpDefNode(newName, let.getKind(),
generateNewParams(let.getParams()), let.isLocal(),
generateNewExprNode(let.getBody(), prefix),
let.getOriginallyDefinedInModuleNode(), null,
let.getTreeNode(), true, let.getSource());
- let.setToolObject(substitutionId, newLet);
- newLets[i] = newLet;
- cc.addSymbolToContext(newName, newLet);
- }
+ let.setToolObject(substitutionId, newLet);
+ newLets[i] = newLet;
+ cc.addSymbolToContext(newName, newLet);
+ }
- LetInNode newLetNode = new LetInNode(oldLetNode.getTreeNode(),
+ LetInNode newLetNode = new LetInNode(oldLetNode.getTreeNode(),
newLets, null, generateNewExprNode(oldLetNode.getBody(),
- prefix), cc);
- return newLetNode;
- }
+ prefix), cc);
+ return newLetNode;
+ }
}
throw new RuntimeException();
}
private ExprNode generateNewOpApplNode(OpApplNode n, String prefix)
- throws AbortException {
+ throws AbortException {
switch (n.getOperator().getKind()) {
- case VariableDeclKind:
- case ConstantDeclKind: {
- ExprOrOpArgNode e = (ExprOrOpArgNode) n.getOperator()
+ case VariableDeclKind:
+ case ConstantDeclKind: {
+ ExprOrOpArgNode e = (ExprOrOpArgNode) n.getOperator()
.getToolObject(substitutionId);
- if (e != null) {
- if (e instanceof ExprNode) {
- // TODO newprefix, witout last prefix
- return generateNewExprNode((ExprNode) e, "");
- } else {
- OpArgNode opArg = (OpArgNode) e;
- while (opArg.getOp().getToolObject(substitutionId) != null) {
- opArg = (OpArgNode) opArg.getOp().getToolObject(
+ if (e != null) {
+ if (e instanceof ExprNode) {
+ // TODO newprefix, witout last prefix
+ return generateNewExprNode((ExprNode) e, "");
+ } else {
+ OpArgNode opArg = (OpArgNode) e;
+ while (opArg.getOp().getToolObject(substitutionId) != null) {
+ opArg = (OpArgNode) opArg.getOp().getToolObject(
substitutionId);
- }
- return new OpApplNode(opArg.getOp(), generateNewArgs(
+ }
+ return new OpApplNode(opArg.getOp(), generateNewArgs(
n.getArgs(), prefix), n.getTreeNode(), null);
- }
- } else {
- return new OpApplNode(n.getOperator(), generateNewArgs(
+ }
+ } else {
+ return new OpApplNode(n.getOperator(), generateNewArgs(
n.getArgs(), prefix), n.getTreeNode(), null);
+ }
}
- }
- case FormalParamKind: {
- FormalParamNode f = (FormalParamNode) n.getOperator()
+ case FormalParamKind: {
+ FormalParamNode f = (FormalParamNode) n.getOperator()
.getToolObject(substitutionId);
- if (f == null) {
- throw new RuntimeException();
- }
- return new OpApplNode(f, generateNewArgs(n.getArgs(), prefix),
+ if (f == null) {
+ throw new RuntimeException();
+ }
+ return new OpApplNode(f, generateNewArgs(n.getArgs(), prefix),
n.getTreeNode(), null);
- }
+ }
- case BuiltInKind: {
- return generateNewBuiltInNode(n, prefix);
- }
+ case BuiltInKind: {
+ return generateNewBuiltInNode(n, prefix);
+ }
- case UserDefinedOpKind: {
- // in case of a call of a LetInNode
- OpDefNode letOp = (OpDefNode) n.getOperator().getToolObject(
+ case UserDefinedOpKind: {
+ // in case of a call of a LetInNode
+ OpDefNode letOp = (OpDefNode) n.getOperator().getToolObject(
substitutionId);
- if (letOp != null) {
- return new OpApplNode(letOp, generateNewArgs(n.getArgs(),
+ if (letOp != null) {
+ return new OpApplNode(letOp, generateNewArgs(n.getArgs(),
prefix), n.getTreeNode(), null);
- }
+ }
- // in case of a call of BBuiltInOp e.g. +, -
- if (BBuiltInOPs.contains(n.getOperator().getName())) {
- return new OpApplNode(n.getOperator(), generateNewArgs(
+ // in case of a call of BBuiltInOp e.g. +, -
+ if (BBuiltInOPs.contains(n.getOperator().getName())) {
+ return new OpApplNode(n.getOperator(), generateNewArgs(
n.getArgs(), prefix), n.stn, null);
- }
+ }
- // normal userdefined Operator
- String opName = prefix + n.getOperator().getName().toString();
- OpDefNode op = defsHash.get(opName);
- if (op == null) {
- throw new RuntimeException();
- }
- return new OpApplNode(op, generateNewArgs(n.getArgs(),
+ // normal userdefined Operator
+ String opName = prefix + n.getOperator().getName().toString();
+ OpDefNode op = defsHash.get(opName);
+ if (op == null) {
+ throw new RuntimeException();
+ }
+ return new OpApplNode(op, generateNewArgs(n.getArgs(),
prefix), n.getTreeNode(), null);
- }
+ }
}
throw new RuntimeException("OpApplkind not implemented jet");
}
private ExprNode generateNewBuiltInNode(OpApplNode n, String prefix)
- throws AbortException {
+ throws AbortException {
switch (getOpCode(n.getOperator().getName())) {
- case OPCODE_exc: { // Except
- OpApplNode newNode = new OpApplNode(n.getOperator().getName(),
+ case OPCODE_exc: { // Except
+ OpApplNode newNode = new OpApplNode(n.getOperator().getName(),
null, n.getTreeNode(), null);
- n.setToolObject(substitutionId, newNode); // needed for @ node
- ExprOrOpArgNode[] newArgs = new ExprOrOpArgNode[n.getArgs().length];
- newArgs[0] = generateNewExprOrOpArgNode(n.getArgs()[0], prefix);
+ n.setToolObject(substitutionId, newNode); // needed for @ node
+ ExprOrOpArgNode[] newArgs = new ExprOrOpArgNode[n.getArgs().length];
+ newArgs[0] = generateNewExprOrOpArgNode(n.getArgs()[0], prefix);
- for (int i = 1; i < n.getArgs().length; i++) {
- OpApplNode pair = (OpApplNode) n.getArgs()[i];
- OpApplNode newPair = new OpApplNode(pair.getOperator()
+ for (int i = 1; i < n.getArgs().length; i++) {
+ OpApplNode pair = (OpApplNode) n.getArgs()[i];
+ OpApplNode newPair = new OpApplNode(pair.getOperator()
.getName(), null, pair.getTreeNode(), null);
- // needed for @ node: we have to set a reference from the old
- // pair to the new pair
- // before evaluation the arguments which may be contains a @
- // node
- pair.setToolObject(substitutionId, newPair);
- newPair.setArgs(generateNewArgs(pair.getArgs(), prefix));
- newArgs[i] = newPair;
- }
- newNode.setArgs(newArgs);
- return newNode;
+ // needed for @ node: we have to set a reference from the old
+ // pair to the new pair
+ // before evaluation the arguments which may be contains a @
+ // node
+ pair.setToolObject(substitutionId, newPair);
+ newPair.setArgs(generateNewArgs(pair.getArgs(), prefix));
+ newArgs[i] = newPair;
+ }
+ newNode.setArgs(newArgs);
+ return newNode;
- }
- case OPCODE_uc: { // CHOOSE x : P
- FormalParamNode[] oldSymbols = n.getUnbdedQuantSymbols();
- FormalParamNode[] newSymbols = new FormalParamNode[oldSymbols.length];
- for (int i = 0; i < n.getUnbdedQuantSymbols().length; i++) {
- FormalParamNode f = oldSymbols[i];
- newSymbols[i] = new FormalParamNode(f.getName(), f.getArity(),
- f.getTreeNode(), null, null);
- f.setToolObject(substitutionId, newSymbols[i]);
}
- OpApplNode newNode = new OpApplNode(n.getOperator().getName(),
+ case OPCODE_uc: { // CHOOSE x : P
+ FormalParamNode[] oldSymbols = n.getUnbdedQuantSymbols();
+ FormalParamNode[] newSymbols = new FormalParamNode[oldSymbols.length];
+ for (int i = 0; i < n.getUnbdedQuantSymbols().length; i++) {
+ FormalParamNode f = oldSymbols[i];
+ newSymbols[i] = new FormalParamNode(f.getName(), f.getArity(),
+ f.getTreeNode(), null, null);
+ f.setToolObject(substitutionId, newSymbols[i]);
+ }
+ OpApplNode newNode = new OpApplNode(n.getOperator().getName(),
newSymbols, generateNewArgs(n.getArgs(), prefix), null,
null, null, n.getTreeNode(), null);
- return newNode;
- }
+ return newNode;
+ }
- case OPCODE_rfs:
- case OPCODE_nrfs:
- case OPCODE_fc: // Represents [x \in S |-> e]
- case OPCODE_be: // \E x \in S : P
- case OPCODE_bf: // \A x \in S : P
- case OPCODE_bc: // CHOOSE x \in S: P
- case OPCODE_sso: // $SubsetOf Represents {x \in S : P}
- case OPCODE_soa: // $SetOfAll Represents {e : p1 \in S, p2,p3 \in S2}
- {
- // new formalparamnodes
- FormalParamNode[][] oldParams = n.getBdedQuantSymbolLists();
- FormalParamNode[][] newParams = new FormalParamNode[oldParams.length][0];
- for (int i = 0; i < oldParams.length; i++) {
- FormalParamNode[] temp = new FormalParamNode[oldParams[i].length];
- for (int j = 0; j < oldParams[i].length; j++) {
- FormalParamNode f = oldParams[i][j];
- temp[j] = new FormalParamNode(f.getName(), f.getArity(),
+ case OPCODE_rfs:
+ case OPCODE_nrfs:
+ case OPCODE_fc: // Represents [x \in S |-> e]
+ case OPCODE_be: // \E x \in S : P
+ case OPCODE_bf: // \A x \in S : P
+ case OPCODE_bc: // CHOOSE x \in S: P
+ case OPCODE_sso: // $SubsetOf Represents {x \in S : P}
+ case OPCODE_soa: // $SetOfAll Represents {e : p1 \in S, p2,p3 \in S2}
+ {
+ // new formalparamnodes
+ FormalParamNode[][] oldParams = n.getBdedQuantSymbolLists();
+ FormalParamNode[][] newParams = new FormalParamNode[oldParams.length][0];
+ for (int i = 0; i < oldParams.length; i++) {
+ FormalParamNode[] temp = new FormalParamNode[oldParams[i].length];
+ for (int j = 0; j < oldParams[i].length; j++) {
+ FormalParamNode f = oldParams[i][j];
+ temp[j] = new FormalParamNode(f.getName(), f.getArity(),
f.getTreeNode(), null, null);
- // set reference the old param to the new
- f.setToolObject(substitutionId, temp[j]);
+ // set reference the old param to the new
+ f.setToolObject(substitutionId, temp[j]);
+ }
+ newParams[i] = temp;
}
- newParams[i] = temp;
- }
- // new ranges
- ExprNode[] ranges = new ExprNode[n.getBdedQuantBounds().length];
- for (int i = 0; i < n.getBdedQuantBounds().length; i++) {
- ranges[i] = generateNewExprNode(n.getBdedQuantBounds()[i],
+ // new ranges
+ ExprNode[] ranges = new ExprNode[n.getBdedQuantBounds().length];
+ for (int i = 0; i < n.getBdedQuantBounds().length; i++) {
+ ranges[i] = generateNewExprNode(n.getBdedQuantBounds()[i],
prefix);
- }
- OpApplNode newNode = new OpApplNode(n.getOperator().getName(),
+ }
+ OpApplNode newNode = new OpApplNode(n.getOperator().getName(),
null, generateNewArgs(n.getArgs(), prefix), newParams,
n.isBdedQuantATuple(), ranges, n.getTreeNode(), null);
- return newNode;
- }
+ return newNode;
+ }
- default: { // =
- OpApplNode newNode = new OpApplNode(n.getOperator(),
+ default: { // =
+ OpApplNode newNode = new OpApplNode(n.getOperator(),
generateNewArgs(n.getArgs(), prefix), n.getTreeNode(), null);
- return newNode;
- }
+ return newNode;
+ }
}
}
private ExprOrOpArgNode[] generateNewArgs(ExprOrOpArgNode[] args,
- String prefix) throws AbortException {
+ String prefix) throws AbortException {
ExprOrOpArgNode[] res = new ExprOrOpArgNode[args.length];
for (int i = 0; i < args.length; i++) {
res[i] = generateNewExprOrOpArgNode(args[i], prefix);
@@ -297,7 +297,7 @@ public class InstanceTransformation extends BuiltInOPs implements ASTConstants {
for (int i = 0; i < oldParams.length; i++) {
FormalParamNode oldParam = oldParams[i];
FormalParamNode newParam = new FormalParamNode(oldParam.getName(),
- oldParam.getArity(), oldParam.getTreeNode(), null, null);
+ oldParam.getArity(), oldParam.getTreeNode(), null, null);
// set reference to the old param to the new
oldParam.setToolObject(substitutionId, newParam);
newParams[i] = newParam;
diff --git a/src/main/java/de/tla2b/analysis/PredicateVsExpression.java b/src/main/java/de/tla2b/analysis/PredicateVsExpression.java
index 6445fde..1a9cfd7 100644
--- a/src/main/java/de/tla2b/analysis/PredicateVsExpression.java
+++ b/src/main/java/de/tla2b/analysis/PredicateVsExpression.java
@@ -9,7 +9,7 @@ import tlc2.tool.BuiltInOPs;
import java.util.HashMap;
public class PredicateVsExpression extends BuiltInOPs implements ASTConstants,
- BBuildIns, TranslationGlobals {
+ BBuildIns, TranslationGlobals {
private final HashMap<OpDefNode, DefinitionType> definitionsTypeMap;
@@ -34,14 +34,14 @@ public class PredicateVsExpression extends BuiltInOPs implements ASTConstants,
private DefinitionType visitSemanticNode(SemanticNode s) {
switch (s.getKind()) {
- case OpApplKind: {
- return visitOppApplNode((OpApplNode) s);
- }
+ case OpApplKind: {
+ return visitOppApplNode((OpApplNode) s);
+ }
- case LetInKind: {
- LetInNode letInNode = (LetInNode) s;
- return visitSemanticNode(letInNode.getBody());
- }
+ case LetInKind: {
+ LetInNode letInNode = (LetInNode) s;
+ return visitSemanticNode(letInNode.getBody());
+ }
}
@@ -53,37 +53,37 @@ public class PredicateVsExpression extends BuiltInOPs implements ASTConstants,
if (kind == BuiltInKind) {
switch (getOpCode(opApplNode.getOperator().getName())) {
- case OPCODE_eq: // =
- case OPCODE_noteq: // /=
- case OPCODE_cl: // $ConjList
- case OPCODE_land: // \land
- case OPCODE_dl: // $DisjList
- case OPCODE_lor: // \/
- case OPCODE_equiv: // \equiv
- case OPCODE_implies: // =>
- case OPCODE_lnot: // \lnot
- case OPCODE_be: // \E x \in S : P
- case OPCODE_bf: // \A x \in S : P
- case OPCODE_in: // \in
- case OPCODE_subseteq: // \subseteq {1,2} <: {1,2,3}
- case OPCODE_unchanged: {
- return DefinitionType.PREDICATE;
- }
-
- case OPCODE_ite: // IF THEN ELSE
- {
- return visitSemanticNode(opApplNode.getArgs()[1]);
- }
-
- case OPCODE_case: // CASE p1 -> e1 [] p2 -> e2
- {
- OpApplNode pair = (OpApplNode) opApplNode.getArgs()[0];
- return visitSemanticNode(pair.getArgs()[1]);
- }
-
- default: {
- return DefinitionType.EXPRESSION;
- }
+ case OPCODE_eq: // =
+ case OPCODE_noteq: // /=
+ case OPCODE_cl: // $ConjList
+ case OPCODE_land: // \land
+ case OPCODE_dl: // $DisjList
+ case OPCODE_lor: // \/
+ case OPCODE_equiv: // \equiv
+ case OPCODE_implies: // =>
+ case OPCODE_lnot: // \lnot
+ case OPCODE_be: // \E x \in S : P
+ case OPCODE_bf: // \A x \in S : P
+ case OPCODE_in: // \in
+ case OPCODE_subseteq: // \subseteq {1,2} <: {1,2,3}
+ case OPCODE_unchanged: {
+ return DefinitionType.PREDICATE;
+ }
+
+ case OPCODE_ite: // IF THEN ELSE
+ {
+ return visitSemanticNode(opApplNode.getArgs()[1]);
+ }
+
+ case OPCODE_case: // CASE p1 -> e1 [] p2 -> e2
+ {
+ OpApplNode pair = (OpApplNode) opApplNode.getArgs()[0];
+ return visitSemanticNode(pair.getArgs()[1]);
+ }
+
+ default: {
+ return DefinitionType.EXPRESSION;
+ }
}
} else if (kind == UserDefinedOpKind) {
return visitUserdefinedOp(opApplNode);
@@ -94,19 +94,19 @@ public class PredicateVsExpression extends BuiltInOPs implements ASTConstants,
private DefinitionType visitUserdefinedOp(OpApplNode s) {
OpDefNode def = (OpDefNode) s.getOperator();
if (BBuiltInOPs.contains(def.getName())
- && STANDARD_MODULES.contains(def.getSource()
- .getOriginallyDefinedInModuleNode().getName()
- .toString())) {
+ && STANDARD_MODULES.contains(def.getSource()
+ .getOriginallyDefinedInModuleNode().getName()
+ .toString())) {
switch (BBuiltInOPs.getOpcode(def.getName())) {
- case B_OPCODE_lt: // <
- case B_OPCODE_gt: // >
- case B_OPCODE_leq: // <=
- case B_OPCODE_geq: // >=
- case B_OPCODE_finite:
- return DefinitionType.PREDICATE;
- default:
- return DefinitionType.EXPRESSION;
+ case B_OPCODE_lt: // <
+ case B_OPCODE_gt: // >
+ case B_OPCODE_leq: // <=
+ case B_OPCODE_geq: // >=
+ case B_OPCODE_finite:
+ return DefinitionType.PREDICATE;
+ default:
+ return DefinitionType.EXPRESSION;
}
}
diff --git a/src/main/java/de/tla2b/analysis/RecursiveDefinition.java b/src/main/java/de/tla2b/analysis/RecursiveDefinition.java
index 58e07e7..7dfb305 100644
--- a/src/main/java/de/tla2b/analysis/RecursiveDefinition.java
+++ b/src/main/java/de/tla2b/analysis/RecursiveDefinition.java
@@ -1,20 +1,20 @@
package de.tla2b.analysis;
+import de.tla2b.exceptions.NotImplementedException;
import tla2sany.semantic.OpApplNode;
import tla2sany.semantic.OpDefNode;
import tlc2.tool.BuiltInOPs;
-import de.tla2b.exceptions.NotImplementedException;
-public class RecursiveDefinition extends BuiltInOPs{
+public class RecursiveDefinition extends BuiltInOPs {
private final OpDefNode def;
private OpApplNode ifThenElse;
-
- public RecursiveDefinition(OpDefNode def) throws NotImplementedException{
+
+ public RecursiveDefinition(OpDefNode def) throws NotImplementedException {
this.def = def;
evalRecursiveDefinition();
}
-
+
private void evalRecursiveDefinition() throws NotImplementedException {
if (def.getBody() instanceof OpApplNode) {
OpApplNode o = (OpApplNode) def.getBody();
@@ -24,9 +24,9 @@ public class RecursiveDefinition extends BuiltInOPs{
}
}
throw new NotImplementedException(
- "Only IF/THEN/ELSE or CASE constructs are supported at the body of a recursive function.");
+ "Only IF/THEN/ELSE or CASE constructs are supported at the body of a recursive function.");
}
-
+
public OpDefNode getOpDefNode() {
return def;
}
diff --git a/src/main/java/de/tla2b/analysis/RecursiveFunktion.java b/src/main/java/de/tla2b/analysis/RecursiveFunktion.java
index f516fa5..d07d58d 100644
--- a/src/main/java/de/tla2b/analysis/RecursiveFunktion.java
+++ b/src/main/java/de/tla2b/analysis/RecursiveFunktion.java
@@ -12,7 +12,7 @@ public class RecursiveFunktion extends BuiltInOPs {
private OpApplNode ifThenElse;
public RecursiveFunktion(OpDefNode n, OpApplNode rfs)
- throws NotImplementedException {
+ throws NotImplementedException {
def = n;
this.rfs = rfs;
//evalDef();
diff --git a/src/main/java/de/tla2b/analysis/SpecAnalyser.java b/src/main/java/de/tla2b/analysis/SpecAnalyser.java
index 40b765f..c31a20a 100644
--- a/src/main/java/de/tla2b/analysis/SpecAnalyser.java
+++ b/src/main/java/de/tla2b/analysis/SpecAnalyser.java
@@ -1,11 +1,5 @@
package de.tla2b.analysis;
-import java.util.ArrayList;
-import java.util.Arrays;
-import java.util.HashSet;
-import java.util.Hashtable;
-import java.util.Set;
-
import de.tla2b.config.ConfigfileEvaluator;
import de.tla2b.exceptions.ConfigFileErrorException;
import de.tla2b.exceptions.FrontEndException;
@@ -16,19 +10,12 @@ import de.tla2b.global.TranslationGlobals;
import de.tla2b.translation.BDefinitionsFinder;
import de.tla2b.translation.OperationsFinder;
import de.tla2b.translation.UsedDefinitionsFinder;
-import tla2sany.semantic.ASTConstants;
-import tla2sany.semantic.ExprNode;
-import tla2sany.semantic.ExprOrOpArgNode;
-import tla2sany.semantic.FormalParamNode;
-import tla2sany.semantic.ModuleNode;
-import tla2sany.semantic.OpApplNode;
-import tla2sany.semantic.OpDeclNode;
-import tla2sany.semantic.OpDefNode;
-import tla2sany.semantic.SemanticNode;
-import tla2sany.semantic.SymbolNode;
+import tla2sany.semantic.*;
import tlc2.tool.BuiltInOPs;
import tlc2.tool.ToolGlobals;
+import java.util.*;
+
public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobals, TranslationGlobals {
private OpDefNode spec;
private OpDefNode init;
@@ -95,49 +82,67 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal
for (int i = 0; i < m.getOpDefs().length; i++) {
definitions.put(m.getOpDefs()[i].getName().toString(), m.getOpDefs()[i]);
}
-
+
if (definitions.containsKey("Spec")) {
- specAnalyser.spec = definitions.get("Spec"); ClausefDetected("Spec","INITIALISATION+OPERATIONS");
+ specAnalyser.spec = definitions.get("Spec");
+ ClausefDetected("Spec", "INITIALISATION+OPERATIONS");
} else if (definitions.containsKey("SPECIFICATION")) {
- specAnalyser.spec = definitions.get("SPECIFICATION"); ClausefDetected("SPECIFICATION","INITIALISATION+OPERATIONS");
+ specAnalyser.spec = definitions.get("SPECIFICATION");
+ ClausefDetected("SPECIFICATION", "INITIALISATION+OPERATIONS");
} else if (definitions.containsKey("SPEC")) {
- specAnalyser.spec = definitions.get("SPEC"); ClausefDetected("SPEC","INITIALISATION+OPERATIONS");
+ specAnalyser.spec = definitions.get("SPEC");
+ ClausefDetected("SPEC", "INITIALISATION+OPERATIONS");
}
-
+
if (definitions.containsKey("Init")) {
- specAnalyser.init = definitions.get("Init"); ClausefDetected("Init","INITIALISATION");
+ specAnalyser.init = definitions.get("Init");
+ ClausefDetected("Init", "INITIALISATION");
} else if (definitions.containsKey("INIT")) {
- specAnalyser.init = definitions.get("INIT"); ClausefDetected("INIT","INITIALISATION");
+ specAnalyser.init = definitions.get("INIT");
+ ClausefDetected("INIT", "INITIALISATION");
} else if (definitions.containsKey("Initialisation")) {
- specAnalyser.init = definitions.get("Initialisation"); ClausefDetected("Initialisation","INITIALISATION");
+ specAnalyser.init = definitions.get("Initialisation");
+ ClausefDetected("Initialisation", "INITIALISATION");
} else if (definitions.containsKey("INITIALISATION")) {
- specAnalyser.init = definitions.get("INITIALISATION"); ClausefDetected("INITIALISATION","INITIALISATION");
+ specAnalyser.init = definitions.get("INITIALISATION");
+ ClausefDetected("INITIALISATION", "INITIALISATION");
}
-
+
if (definitions.containsKey("Next")) {
- specAnalyser.next = definitions.get("Next"); ClausefDetected("Next","OPERATIONS");
+ specAnalyser.next = definitions.get("Next");
+ ClausefDetected("Next", "OPERATIONS");
} else if (definitions.containsKey("NEXT")) {
- specAnalyser.next = definitions.get("NEXT"); ClausefDetected("NEXT","OPERATIONS");
+ specAnalyser.next = definitions.get("NEXT");
+ ClausefDetected("NEXT", "OPERATIONS");
}
-
+
if (definitions.containsKey("Inv")) {
- specAnalyser.invariants.add(definitions.get("Inv")); ClausefDetected("Inv","INVARIANTS");
+ specAnalyser.invariants.add(definitions.get("Inv"));
+ ClausefDetected("Inv", "INVARIANTS");
} else if (definitions.containsKey("INVARIANTS")) {
- specAnalyser.invariants.add(definitions.get("INVARIANTS")); ClausefDetected("INVARIANTS","INVARIANTS");
+ specAnalyser.invariants.add(definitions.get("INVARIANTS"));
+ ClausefDetected("INVARIANTS", "INVARIANTS");
} else if (definitions.containsKey("INVARIANT")) {
- specAnalyser.invariants.add(definitions.get("INVARIANT")); ClausefDetected("INVARIANT","INVARIANTS");
+ specAnalyser.invariants.add(definitions.get("INVARIANT"));
+ ClausefDetected("INVARIANT", "INVARIANTS");
} else if (definitions.containsKey("INV")) {
- specAnalyser.invariants.add(definitions.get("INV")); ClausefDetected("INV","INVARIANTS");
+ specAnalyser.invariants.add(definitions.get("INV"));
+ ClausefDetected("INV", "INVARIANTS");
} else if (definitions.containsKey("Invariant")) {
- specAnalyser.invariants.add(definitions.get("Invariant")); ClausefDetected("Invariant","INVARIANTS");
+ specAnalyser.invariants.add(definitions.get("Invariant"));
+ ClausefDetected("Invariant", "INVARIANTS");
} else if (definitions.containsKey("Invariants")) {
- specAnalyser.invariants.add(definitions.get("Invariants")); ClausefDetected("Invariants","INVARIANTS");
+ specAnalyser.invariants.add(definitions.get("Invariants"));
+ ClausefDetected("Invariants", "INVARIANTS");
} else if (definitions.containsKey("TypeInv")) {
- specAnalyser.invariants.add(definitions.get("TypeInv")); ClausefDetected("TypeInv","INVARIANTS");
+ specAnalyser.invariants.add(definitions.get("TypeInv"));
+ ClausefDetected("TypeInv", "INVARIANTS");
} else if (definitions.containsKey("TypeOK")) {
- specAnalyser.invariants.add(definitions.get("TypeOK")); ClausefDetected("TypeOK","INVARIANTS");
- }else if (definitions.containsKey("IndInv")) {
- specAnalyser.invariants.add(definitions.get("IndInv")); ClausefDetected("IndInv","INVARIANTS");
+ specAnalyser.invariants.add(definitions.get("TypeOK"));
+ ClausefDetected("TypeOK", "INVARIANTS");
+ } else if (definitions.containsKey("IndInv")) {
+ specAnalyser.invariants.add(definitions.get("IndInv"));
+ ClausefDetected("IndInv", "INVARIANTS");
}
// TODO are constant in the right order
@@ -145,18 +150,19 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal
return specAnalyser;
}
-
+
public static void ClausefDetected(String Name, String Clause) {
- // TODO: use -verbose OPTION from command line
- System.out.println("Detected TLA+ Default Definition "+Name+" for Clause: "+Clause);
+ // TODO: use -verbose OPTION from command line
+ System.out.println("Detected TLA+ Default Definition " + Name + " for Clause: " + Clause);
}
+
public static void DebugMsg(String Msg) {
- // TODO: use -verbose OPTION from command line
- System.out.println(Msg);
+ // TODO: use -verbose OPTION from command line
+ System.out.println(Msg);
}
public void start()
- throws SemanticErrorException, FrontEndException, ConfigFileErrorException, NotImplementedException {
+ throws SemanticErrorException, FrontEndException, ConfigFileErrorException, NotImplementedException {
if (spec != null) {
evalSpec();
@@ -174,17 +180,17 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal
if (opDefNode.getKind() == UserDefinedOpKind && !BBuiltInOPs.contains(opDefNode.getName())) {
int i = invariants.indexOf(inv);
invariants.set(i, opDefNode);
- DebugMsg("Adding invariant "+i);
+ DebugMsg("Adding invariant " + i);
}
} catch (ClassCastException e) {
}
}
- DebugMsg("Detecting OPERATIONS from disjunctions");
+ DebugMsg("Detecting OPERATIONS from disjunctions");
OperationsFinder operationsFinder = new OperationsFinder(this);
bOperations = operationsFinder.getBOperations();
- DebugMsg("Finding used definitions");
+ DebugMsg("Finding used definitions");
UsedDefinitionsFinder definitionFinder = new UsedDefinitionsFinder(this);
this.usedDefinitions = definitionFinder.getUsedDefinitions();
@@ -192,7 +198,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal
this.bDefinitionsSet = bDefinitionFinder.getBDefinitionsSet();
// usedDefinitions.addAll(bDefinitionsSet);
- DebugMsg("Computing variable declarations");
+ DebugMsg("Computing variable declarations");
// test whether there is a init predicate if there is a variable
if (moduleNode.getVariableDecls().length > 0 && inits == null) {
throw new SemanticErrorException("No initial predicate is defined.");
@@ -210,11 +216,11 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal
for (OpDeclNode var : moduleNode.getVariableDecls()) {
namingHashTable.put(var.getName().toString(), var);
}
- DebugMsg("Number of variables detected: " + moduleNode.getVariableDecls().length);
+ DebugMsg("Number of variables detected: " + moduleNode.getVariableDecls().length);
for (OpDeclNode con : moduleNode.getConstantDecls()) {
namingHashTable.put(con.getName().toString(), con);
}
- DebugMsg("Number of constants detected: " + moduleNode.getConstantDecls().length);
+ DebugMsg("Number of constants detected: " + moduleNode.getConstantDecls().length);
for (OpDefNode def : usedDefinitions) {
namingHashTable.put(def.getName().toString(), def);
}
@@ -223,21 +229,21 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal
private void evalInit() {
if (init != null) {
- System.out.println("Using TLA+ Init definition to determine B INITIALISATION");
+ System.out.println("Using TLA+ Init definition to determine B INITIALISATION");
inits.add(init.getBody());
}
}
private void evalNext() {
if (next != null) {
- System.out.println("Using TLA+ Next definition to determine B OPERATIONS");
+ System.out.println("Using TLA+ Next definition to determine B OPERATIONS");
this.nextExpr = next.getBody();
}
}
public void evalSpec() throws SemanticErrorException {
if (spec != null) {
- System.out.println("Using TLA+ Spec to determine B INITIALISATION and OPERATIONS");
+ System.out.println("Using TLA+ Spec to determine B INITIALISATION and OPERATIONS");
processConfigSpec(spec.getBody());
}
@@ -274,7 +280,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal
if (opcode == OPCODE_box) {
SemanticNode boxArg = args[0];
if ((boxArg instanceof OpApplNode)
- && BuiltInOPs.getOpCode(((OpApplNode) boxArg).getOperator().getName()) == OPCODE_sa) {
+ && BuiltInOPs.getOpCode(((OpApplNode) boxArg).getOperator().getName()) == OPCODE_sa) {
this.nextExpr = (ExprNode) ((OpApplNode) boxArg).getArgs()[0];
return;
}
@@ -297,7 +303,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal
for (OpDefNode def : set) {
if (def.getInRecursive()) {
throw new NotImplementedException("Recursive definitions are currently not supported: " + def.getName()
- + "\n" + def.getLocation());
+ + "\n" + def.getLocation());
// bDefinitionsSet.remove(def);
// RecursiveDefinition rd = new RecursiveDefinition(def);
// recursiveDefinitions.add(rd);
diff --git a/src/main/java/de/tla2b/analysis/SymbolRenamer.java b/src/main/java/de/tla2b/analysis/SymbolRenamer.java
index a9cd4c0..22c13bc 100644
--- a/src/main/java/de/tla2b/analysis/SymbolRenamer.java
+++ b/src/main/java/de/tla2b/analysis/SymbolRenamer.java
@@ -1,27 +1,20 @@
package de.tla2b.analysis;
-import java.util.HashSet;
-import java.util.Hashtable;
-import java.util.Set;
-
import de.tla2b.global.BBuiltInOPs;
import de.tla2b.global.TranslationGlobals;
-import tla2sany.semantic.ASTConstants;
-import tla2sany.semantic.AssumeNode;
-import tla2sany.semantic.FormalParamNode;
-import tla2sany.semantic.LetInNode;
-import tla2sany.semantic.ModuleNode;
-import tla2sany.semantic.OpApplNode;
-import tla2sany.semantic.OpDeclNode;
-import tla2sany.semantic.OpDefNode;
-import tla2sany.semantic.SemanticNode;
+import tla2sany.semantic.*;
import tlc2.tool.BuiltInOPs;
+import java.util.HashSet;
+import java.util.Hashtable;
+import java.util.Set;
+
public class SymbolRenamer extends BuiltInOPs implements TranslationGlobals,
- ASTConstants {
+ ASTConstants {
private final static Set<String> KEYWORDS = new HashSet<>();
+
static {
KEYWORDS.add("seq");
KEYWORDS.add("left");
@@ -76,6 +69,7 @@ public class SymbolRenamer extends BuiltInOPs implements TranslationGlobals,
}
private final static Hashtable<String, String> INFIX_OPERATOR = new Hashtable<>();
+
static {
INFIX_OPERATOR.put("!!", "exclamationmark2");
INFIX_OPERATOR.put("??", "questionmark2");
@@ -98,6 +92,7 @@ public class SymbolRenamer extends BuiltInOPs implements TranslationGlobals,
}
private final static Hashtable<String, String> BBUILTIN_OPERATOR = new Hashtable<>();
+
static {
BBUILTIN_OPERATOR.put("+", "plus");
BBUILTIN_OPERATOR.put("-", "minus");
@@ -182,70 +177,70 @@ public class SymbolRenamer extends BuiltInOPs implements TranslationGlobals,
switch (n.getKind()) {
- case LetInKind: {
- LetInNode letInNode = (LetInNode) n;
- OpDefNode[] defs = letInNode.getLets();
-
- // Initialize all local definitions (get a new name, get an empty
- // list)
- for (OpDefNode def : defs) {
- String newName = getOperatorName(def);
- globalNames.add(newName);
- def.setToolObject(NEW_NAME, newName);
- usedNamesTable.put(def, new HashSet<>(usedNames));
- }
-
- // first visit the IN expression
- visitNode(letInNode.getBody(), usedNames);
-
- // visit the definition itself
- for (int i = defs.length - 1; i >= 0; i--) {
- OpDefNode def = defs[i];
- Set<String> usedNamesOfDef = usedNamesTable.get(def);
- for (int j = 0; j < def.getParams().length; j++) {
- FormalParamNode p = def.getParams()[j];
- String paramName = p.getName().toString();
- String newParamName = incName(paramName);
- p.setToolObject(NEW_NAME, newParamName);
- //usedNamesOfDef.add(newParamName);
+ case LetInKind: {
+ LetInNode letInNode = (LetInNode) n;
+ OpDefNode[] defs = letInNode.getLets();
+
+ // Initialize all local definitions (get a new name, get an empty
+ // list)
+ for (OpDefNode def : defs) {
+ String newName = getOperatorName(def);
+ globalNames.add(newName);
+ def.setToolObject(NEW_NAME, newName);
+ usedNamesTable.put(def, new HashSet<>(usedNames));
}
- visitNode(def.getBody(), usedNamesOfDef);
- }
- return;
- }
-
- case OpApplKind: {
- OpApplNode opApplNode = (OpApplNode) n;
- switch (opApplNode.getOperator().getKind()) {
- case BuiltInKind: {
- visitBuiltinNode(opApplNode, usedNames);
+ // first visit the IN expression
+ visitNode(letInNode.getBody(), usedNames);
+
+ // visit the definition itself
+ for (int i = defs.length - 1; i >= 0; i--) {
+ OpDefNode def = defs[i];
+ Set<String> usedNamesOfDef = usedNamesTable.get(def);
+ for (int j = 0; j < def.getParams().length; j++) {
+ FormalParamNode p = def.getParams()[j];
+ String paramName = p.getName().toString();
+ String newParamName = incName(paramName);
+ p.setToolObject(NEW_NAME, newParamName);
+ //usedNamesOfDef.add(newParamName);
+ }
+ visitNode(def.getBody(), usedNamesOfDef);
+ }
return;
}
- case UserDefinedOpKind: {
- OpDefNode def = (OpDefNode) opApplNode.getOperator();
- if (BBuiltInOPs.contains(def.getName())) {
- break;
- }
- Set<String> set = usedNamesTable.get(def);
- if (set!=null){
- usedNamesTable.get(def).addAll(usedNames);
+ case OpApplKind: {
+ OpApplNode opApplNode = (OpApplNode) n;
+ switch (opApplNode.getOperator().getKind()) {
+
+ case BuiltInKind: {
+ visitBuiltinNode(opApplNode, usedNames);
+ return;
+ }
+
+ case UserDefinedOpKind: {
+ OpDefNode def = (OpDefNode) opApplNode.getOperator();
+ if (BBuiltInOPs.contains(def.getName())) {
+ break;
+ }
+ Set<String> set = usedNamesTable.get(def);
+ if (set != null) {
+ usedNamesTable.get(def).addAll(usedNames);
+ }
+
+
+ for (int i = 0; i < n.getChildren().length; i++) {
+ visitNode(opApplNode.getArgs()[i], usedNames);
+ }
+ return;
+ }
}
-
-
- for (int i = 0; i < n.getChildren().length; i++) {
+
+ for (int i = 0; i < opApplNode.getArgs().length; i++) {
visitNode(opApplNode.getArgs()[i], usedNames);
}
return;
}
- }
-
- for (int i = 0; i < opApplNode.getArgs().length; i++) {
- visitNode(opApplNode.getArgs()[i], usedNames);
- }
- return;
- }
}
if (n.getChildren() != null) {
@@ -259,40 +254,39 @@ public class SymbolRenamer extends BuiltInOPs implements TranslationGlobals,
switch (getOpCode(opApplNode.getOperator().getName())) {
- case OPCODE_nrfs:
- case OPCODE_fc: // Represents [x \in S |-> e]
- case OPCODE_bc: // CHOOSE x \in S: P
- case OPCODE_soa: // $SetOfAll Represents {e : p1 \in S, p2,p3 \in S2}
- case OPCODE_sso: // $SubsetOf Represents {x \in S : P}
- case OPCODE_bf: // \A x \in S : P
- case OPCODE_be: // \E x \in S : P
- {
- FormalParamNode[][] params = opApplNode.getBdedQuantSymbolLists();
- Set<String> newUsedNames = new HashSet<>(usedNames);
- for (FormalParamNode[] formalParamNodes : params) {
- for (int j = 0; j < formalParamNodes.length; j++) {
- FormalParamNode param = formalParamNodes[j];
- String paramName = param.getName().toString();
- String newName = incName(paramName, usedNames);
- param.setToolObject(NEW_NAME, newName);
- newUsedNames.add(newName);
+ case OPCODE_nrfs:
+ case OPCODE_fc: // Represents [x \in S |-> e]
+ case OPCODE_bc: // CHOOSE x \in S: P
+ case OPCODE_soa: // $SetOfAll Represents {e : p1 \in S, p2,p3 \in S2}
+ case OPCODE_sso: // $SubsetOf Represents {x \in S : P}
+ case OPCODE_bf: // \A x \in S : P
+ case OPCODE_be: // \E x \in S : P
+ {
+ FormalParamNode[][] params = opApplNode.getBdedQuantSymbolLists();
+ Set<String> newUsedNames = new HashSet<>(usedNames);
+ for (FormalParamNode[] formalParamNodes : params) {
+ for (FormalParamNode param : formalParamNodes) {
+ String paramName = param.getName().toString();
+ String newName = incName(paramName, usedNames);
+ param.setToolObject(NEW_NAME, newName);
+ newUsedNames.add(newName);
+ }
+ }
+ for (int i = 0; i < opApplNode.getBdedQuantBounds().length; i++) {
+ visitNode(opApplNode.getBdedQuantBounds()[i], usedNames);
}
- }
- for (int i = 0; i < opApplNode.getBdedQuantBounds().length; i++) {
- visitNode(opApplNode.getBdedQuantBounds()[i], usedNames);
- }
- visitNode(opApplNode.getArgs()[0], newUsedNames);
+ visitNode(opApplNode.getArgs()[0], newUsedNames);
- return;
- }
+ return;
+ }
- default:
- for (int i = 0; i < opApplNode.getArgs().length; i++) {
- if (opApplNode.getArgs()[i] != null) {
- visitNode(opApplNode.getArgs()[i], usedNames);
+ default:
+ for (int i = 0; i < opApplNode.getArgs().length; i++) {
+ if (opApplNode.getArgs()[i] != null) {
+ visitNode(opApplNode.getArgs()[i], usedNames);
+ }
}
- }
}
}
@@ -303,7 +297,7 @@ public class SymbolRenamer extends BuiltInOPs implements TranslationGlobals,
if (BBUILTIN_OPERATOR.containsKey(newName)) {
// a B built-in operator is defined outside of a standard module
if (!STANDARD_MODULES.contains(def.getSource()
- .getOriginallyDefinedInModuleNode().getName().toString())) {
+ .getOriginallyDefinedInModuleNode().getName().toString())) {
return incName(BBUILTIN_OPERATOR.get(newName));
}
}
diff --git a/src/main/java/de/tla2b/analysis/SymbolSorter.java b/src/main/java/de/tla2b/analysis/SymbolSorter.java
index 2edb094..34b4616 100644
--- a/src/main/java/de/tla2b/analysis/SymbolSorter.java
+++ b/src/main/java/de/tla2b/analysis/SymbolSorter.java
@@ -1,13 +1,13 @@
package de.tla2b.analysis;
-import java.util.Arrays;
-import java.util.Comparator;
-import java.util.Hashtable;
-
import tla2sany.semantic.ModuleNode;
import tla2sany.semantic.OpDeclNode;
import tla2sany.semantic.OpDefNode;
+import java.util.Arrays;
+import java.util.Comparator;
+import java.util.Hashtable;
+
public class SymbolSorter {
private final ModuleNode moduleNode;
@@ -23,16 +23,16 @@ public class SymbolSorter {
// sort definitions
Arrays.sort(moduleNode.getOpDefs(), new OpDefNodeComparator());
}
-
- public static void sortDeclNodes(OpDeclNode[] opDeclNodes){
+
+ public static void sortDeclNodes(OpDeclNode[] opDeclNodes) {
Arrays.sort(opDeclNodes, new OpDeclNodeComparator());
}
-
- public static void sortOpDefNodes(OpDefNode[] opDefNodes){
+
+ public static void sortOpDefNodes(OpDefNode[] opDefNodes) {
Arrays.sort(opDefNodes, new OpDefNodeComparator());
}
- public static Hashtable<String, OpDefNode> getDefsHashTable(OpDefNode[] opDefNodes){
+ public static Hashtable<String, OpDefNode> getDefsHashTable(OpDefNode[] opDefNodes) {
Hashtable<String, OpDefNode> definitions = new Hashtable<>();
for (OpDefNode def : opDefNodes) {
// Definition in this module
@@ -47,7 +47,7 @@ public class SymbolSorter {
}
return definitions;
}
-
+
}
class OpDeclNodeComparator implements Comparator<OpDeclNode> {
diff --git a/src/main/java/de/tla2b/analysis/TypeChecker.java b/src/main/java/de/tla2b/analysis/TypeChecker.java
index 4f7e1be..aaf85a4 100644
--- a/src/main/java/de/tla2b/analysis/TypeChecker.java
+++ b/src/main/java/de/tla2b/analysis/TypeChecker.java
@@ -1,16 +1,9 @@
package de.tla2b.analysis;
-import java.util.*;
-import java.util.Map.Entry;
-
import de.tla2b.config.ConfigfileEvaluator;
import de.tla2b.config.TLCValueNode;
import de.tla2b.config.ValueObj;
-import de.tla2b.exceptions.FrontEndException;
-import de.tla2b.exceptions.NotImplementedException;
-import de.tla2b.exceptions.TLA2BException;
-import de.tla2b.exceptions.TypeErrorException;
-import de.tla2b.exceptions.UnificationException;
+import de.tla2b.exceptions.*;
import de.tla2b.global.BBuildIns;
import de.tla2b.global.BBuiltInOPs;
import de.tla2b.global.TranslationGlobals;
@@ -18,6 +11,9 @@ import de.tla2b.types.*;
import tla2sany.semantic.*;
import tlc2.tool.BuiltInOPs;
+import java.util.*;
+import java.util.Map.Entry;
+
public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns, TranslationGlobals {
private static final int TEMP_TYPE_ID = 6;
@@ -225,71 +221,71 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
private TLAType visitExprNode(ExprNode exprNode, TLAType expected) throws TLA2BException {
switch (exprNode.getKind()) {
- case TLCValueKind: {
- TLCValueNode valueNode = (TLCValueNode) exprNode;
- try {
- return valueNode.getType().unify(expected);
- } catch (UnificationException e) {
- throw new TypeErrorException(
+ case TLCValueKind: {
+ TLCValueNode valueNode = (TLCValueNode) exprNode;
+ try {
+ return valueNode.getType().unify(expected);
+ } catch (UnificationException e) {
+ throw new TypeErrorException(
String.format("Expected %s, found %s at '%s'(assigned in the configuration file),%n%s ",
- expected, valueNode.getType(), valueNode.getValue(), exprNode.getLocation()));
- }
+ expected, valueNode.getType(), valueNode.getValue(), exprNode.getLocation()));
+ }
- }
+ }
- case OpApplKind:
- return visitOpApplNode((OpApplNode) exprNode, expected);
+ case OpApplKind:
+ return visitOpApplNode((OpApplNode) exprNode, expected);
- case NumeralKind:
- try {
- return IntType.getInstance().unify(expected);
- } catch (UnificationException e) {
- throw new TypeErrorException(String.format("Expected %s, found INTEGER at '%s',%n%s ", expected,
+ case NumeralKind:
+ try {
+ return IntType.getInstance().unify(expected);
+ } catch (UnificationException e) {
+ 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 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);
- } catch (UnificationException e) {
- throw new TypeErrorException(String.format("Expected %s, found STRING at '%s',%n%s ", expected,
+ case StringKind: {
+ try {
+ return StringType.getInstance().unify(expected);
+ } catch (UnificationException e) {
+ throw new TypeErrorException(String.format("Expected %s, found STRING at '%s',%n%s ", expected,
((StringNode) exprNode).getRep(), exprNode.getLocation()));
+ }
}
- }
- case AtNodeKind: { // @
- AtNode a = (AtNode) exprNode;
- OpApplNode pair2 = a.getExceptComponentRef();
- ExprOrOpArgNode rightside = pair2.getArgs()[1];
- TLAType type = (TLAType) rightside.getToolObject(TYPE_ID);
- try {
- TLAType res = type.unify(expected);
- setType(exprNode, res);
- return res;
- } catch (UnificationException e) {
- throw new TypeErrorException(
+ case AtNodeKind: { // @
+ AtNode a = (AtNode) exprNode;
+ OpApplNode pair2 = a.getExceptComponentRef();
+ ExprOrOpArgNode rightside = pair2.getArgs()[1];
+ TLAType type = (TLAType) rightside.getToolObject(TYPE_ID);
+ try {
+ TLAType res = type.unify(expected);
+ setType(exprNode, res);
+ return res;
+ } catch (UnificationException e) {
+ throw new TypeErrorException(
String.format("Expected %s, found %s at '@',%n%s ", expected, type, exprNode.getLocation()));
- }
+ }
- }
+ }
- case LetInKind: {
- LetInNode l = (LetInNode) exprNode;
- for (int i = 0; i < l.getLets().length; i++) {
- visitOpDefNode(l.getLets()[i]);
+ case LetInKind: {
+ LetInNode l = (LetInNode) exprNode;
+ for (int i = 0; i < l.getLets().length; i++) {
+ visitOpDefNode(l.getLets()[i]);
+ }
+ return visitExprNode(l.getBody(), expected);
}
- return visitExprNode(l.getBody(), expected);
- }
- case SubstInKind: {
- throw new RuntimeException("SubstInKind should never occur after InstanceTransformation");
- }
+ case SubstInKind: {
+ throw new RuntimeException("SubstInKind should never occur after InstanceTransformation");
+ }
}
@@ -311,139 +307,139 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
private TLAType visitOpApplNode(OpApplNode n, TLAType expected) throws TLA2BException {
switch (n.getOperator().getKind()) {
- case ConstantDeclKind: {
- OpDeclNode con = (OpDeclNode) n.getOperator();
-
- TLAType c = (TLAType) con.getToolObject(TYPE_ID);
- if (c == null) {
- throw new RuntimeException(con.getName() + " has no type yet!");
- }
- try {
- TLAType result = expected.unify(c);
- con.setToolObject(TYPE_ID, result);
- return result;
- } catch (UnificationException e) {
- throw new TypeErrorException(String.format("Expected %s, found %s at constant '%s',%n%s", expected, c,
+ case ConstantDeclKind: {
+ OpDeclNode con = (OpDeclNode) n.getOperator();
+
+ TLAType c = (TLAType) con.getToolObject(TYPE_ID);
+ if (c == null) {
+ throw new RuntimeException(con.getName() + " has no type yet!");
+ }
+ try {
+ TLAType result = expected.unify(c);
+ con.setToolObject(TYPE_ID, result);
+ return result;
+ } catch (UnificationException e) {
+ throw new TypeErrorException(String.format("Expected %s, found %s at constant '%s',%n%s", expected, c,
con.getName(), n.getLocation())
- );
+ );
+ }
}
- }
- case VariableDeclKind: {
- SymbolNode symbolNode = n.getOperator();
- String vName = symbolNode.getName().toString();
- TLAType v = (TLAType) symbolNode.getToolObject(TYPE_ID);
- if (v == null) {
- SymbolNode var = this.specAnalyser.getSymbolNodeByName(vName);
- if (var != null) {
- // symbolNode is variable of an expression, e.g. v + 1
- v = (TLAType) var.getToolObject(TYPE_ID);
- } else {
- throw new RuntimeException(vName + " has no type yet!");
+ case VariableDeclKind: {
+ SymbolNode symbolNode = n.getOperator();
+ String vName = symbolNode.getName().toString();
+ TLAType v = (TLAType) symbolNode.getToolObject(TYPE_ID);
+ if (v == null) {
+ SymbolNode var = this.specAnalyser.getSymbolNodeByName(vName);
+ if (var != null) {
+ // symbolNode is variable of an expression, e.g. v + 1
+ v = (TLAType) var.getToolObject(TYPE_ID);
+ } else {
+ throw new RuntimeException(vName + " has no type yet!");
+ }
}
- }
- try {
- TLAType result = expected.unify(v);
- symbolNode.setToolObject(TYPE_ID, result);
- return result;
- } catch (UnificationException e) {
- throw new TypeErrorException(String.format("Expected %s, found %s at variable '%s',%n%s", expected, v,
+ try {
+ TLAType result = expected.unify(v);
+ symbolNode.setToolObject(TYPE_ID, result);
+ return result;
+ } catch (UnificationException e) {
+ throw new TypeErrorException(String.format("Expected %s, found %s at variable '%s',%n%s", expected, v,
vName, n.getLocation()));
+ }
}
- }
-
- case BuiltInKind: {
- return evalBuiltInKind(n, expected);
- }
- case FormalParamKind: {
- SymbolNode symbolNode = n.getOperator();
- String pName = symbolNode.getName().toString();
- TLAType t = (TLAType) symbolNode.getToolObject(paramId);
- if (t == null) {
- t = (TLAType) symbolNode.getToolObject(TYPE_ID);
+ case BuiltInKind: {
+ return evalBuiltInKind(n, expected);
}
- if (t == null) {
- t = new UntypedType(); // TODO is this correct?
- // throw new RuntimeException();
- }
- try {
- TLAType result = expected.unify(t);
- symbolNode.setToolObject(paramId, result);
- return result;
- } catch (UnificationException e) {
- throw new TypeErrorException(String.format("Expected %s, found %s at parameter '%s',%n%s", expected, t,
+ case FormalParamKind: {
+ SymbolNode symbolNode = n.getOperator();
+ String pName = symbolNode.getName().toString();
+ TLAType t = (TLAType) symbolNode.getToolObject(paramId);
+ if (t == null) {
+ t = (TLAType) symbolNode.getToolObject(TYPE_ID);
+ }
+
+ if (t == null) {
+ t = new UntypedType(); // TODO is this correct?
+ // throw new RuntimeException();
+ }
+ try {
+ TLAType result = expected.unify(t);
+ symbolNode.setToolObject(paramId, result);
+ return result;
+ } catch (UnificationException e) {
+ throw new TypeErrorException(String.format("Expected %s, found %s at parameter '%s',%n%s", expected, t,
pName, n.getLocation()));
+ }
}
- }
- case UserDefinedOpKind: {
- OpDefNode def = (OpDefNode) n.getOperator();
+ case UserDefinedOpKind: {
+ OpDefNode def = (OpDefNode) n.getOperator();
- // Definition is a BBuilt-in definition
- String sourceModule = def.getSource().getOriginallyDefinedInModuleNode().getName().toString();
- if (BBuiltInOPs.contains(def.getName()) && STANDARD_MODULES.contains(sourceModule)) {
- return evalBBuiltIns(n, expected);
- }
+ // Definition is a BBuilt-in definition
+ String sourceModule = def.getSource().getOriginallyDefinedInModuleNode().getName().toString();
+ if (BBuiltInOPs.contains(def.getName()) && STANDARD_MODULES.contains(sourceModule)) {
+ return evalBBuiltIns(n, expected);
+ }
- TLAType found = ((TLAType) def.getToolObject(TYPE_ID));
- if (found == null) {
- found = new UntypedType();
- // throw new RuntimeException(def.getName() +
- // " has no type yet!");
- }
- if (n.getArgs().length != 0) {
- found = found.cloneTLAType();
- }
+ TLAType found = ((TLAType) def.getToolObject(TYPE_ID));
+ if (found == null) {
+ found = new UntypedType();
+ // throw new RuntimeException(def.getName() +
+ // " has no type yet!");
+ }
+ if (n.getArgs().length != 0) {
+ found = found.cloneTLAType();
+ }
- try {
- found = found.unify(expected);
- } catch (UnificationException e) {
- throw new TypeErrorException(String.format("Expected %s, found %s at definition '%s',%n%s", expected,
+ try {
+ found = found.unify(expected);
+ } catch (UnificationException e) {
+ throw new TypeErrorException(String.format("Expected %s, found %s at definition '%s',%n%s", expected,
found, def.getName(), n.getLocation()));
- }
- boolean untyped = false;
- FormalParamNode[] params = def.getParams();
- for (int i = 0; i < n.getArgs().length; i++) {
- // clone the parameter type, because the parameter type is not
- // set/changed at a definition call
- FormalParamNode p = params[i];
- TLAType pType = ((TLAType) p.getToolObject(TYPE_ID));
- if (pType == null) {
- pType = new UntypedType();
- // throw new RuntimeException("Parameter " + p.getName()
- // + " has no type yet!%n" + p.getLocation());
}
- pType = pType.cloneTLAType();
- if (pType.isUntyped())
- untyped = true;
-
- pType = visitExprOrOpArgNode(n.getArgs()[i], pType); // unify
- // both
- // types
- // set types of the arguments of the definition call to the
- // parameters for reevaluation the def body
- p.setToolObject(TEMP_TYPE_ID, pType);
- }
+ boolean untyped = false;
+ FormalParamNode[] params = def.getParams();
+ for (int i = 0; i < n.getArgs().length; i++) {
+ // clone the parameter type, because the parameter type is not
+ // set/changed at a definition call
+ FormalParamNode p = params[i];
+ TLAType pType = ((TLAType) p.getToolObject(TYPE_ID));
+ if (pType == null) {
+ pType = new UntypedType();
+ // throw new RuntimeException("Parameter " + p.getName()
+ // + " has no type yet!%n" + p.getLocation());
+ }
+ pType = pType.cloneTLAType();
+ if (pType.isUntyped())
+ untyped = true;
+
+ pType = visitExprOrOpArgNode(n.getArgs()[i], pType); // unify
+ // both
+ // types
+ // set types of the arguments of the definition call to the
+ // parameters for reevaluation the def body
+ p.setToolObject(TEMP_TYPE_ID, pType);
+ }
- if (found.isUntyped() || untyped || !def.getInRecursive()) {
- // evaluate the body of the definition again
- paramId = TEMP_TYPE_ID;
- found = visitExprNode(def.getBody(), found);
- paramId = TYPE_ID;
- }
+ if (found.isUntyped() || untyped || !def.getInRecursive()) {
+ // evaluate the body of the definition again
+ paramId = TEMP_TYPE_ID;
+ found = visitExprNode(def.getBody(), found);
+ paramId = TYPE_ID;
+ }
- n.setToolObject(TYPE_ID, found);
+ n.setToolObject(TYPE_ID, found);
- return found;
+ return found;
- }
+ }
- default: {
- throw new NotImplementedException(n.getOperator().getName().toString());
- }
+ default: {
+ throw new NotImplementedException(n.getOperator().getName().toString());
+ }
}
}
@@ -452,555 +448,555 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
switch (getOpCode(n.getOperator().getName())) {
- /*
- * equality and disequality: =, #, /=
- */
- case OPCODE_eq: // =
- case OPCODE_noteq: // /=, #
- {
- try {
- BoolType.getInstance().unify(expected);
- } catch (UnificationException e) {
- throw new TypeErrorException(String.format("Expected %s, found BOOL at '%s',%n%s", expected,
+ /*
+ * equality and disequality: =, #, /=
+ */
+ case OPCODE_eq: // =
+ case OPCODE_noteq: // /=, #
+ {
+ try {
+ BoolType.getInstance().unify(expected);
+ } catch (UnificationException e) {
+ throw new TypeErrorException(String.format("Expected %s, found BOOL at '%s',%n%s", expected,
n.getOperator().getName(), n.getLocation()));
+ }
+ TLAType left = visitExprOrOpArgNode(n.getArgs()[0], new de.tla2b.types.UntypedType());
+ visitExprOrOpArgNode(n.getArgs()[1], left);
+ return BoolType.getInstance();
}
- TLAType left = visitExprOrOpArgNode(n.getArgs()[0], new de.tla2b.types.UntypedType());
- visitExprOrOpArgNode(n.getArgs()[1], left);
- return BoolType.getInstance();
- }
- /*
- * Logic Operators: \neg, \lnot, \land, \cl, \lor, \dl, \equiv, =>
- */
- case OPCODE_neg: // Negation
- case OPCODE_lnot: // Negation
- case OPCODE_cl: // $ConjList
- case OPCODE_dl: // $DisjList
- case OPCODE_land: // \land
- case OPCODE_lor: // \lor
- case OPCODE_equiv: // \equiv
- case OPCODE_implies: // =>
- {
- try {
- BoolType.getInstance().unify(expected);
- } catch (UnificationException e) {
- throw new TypeErrorException(String.format("Expected %s, found BOOL at '%s',%n%s", expected,
+ /*
+ * Logic Operators: \neg, \lnot, \land, \cl, \lor, \dl, \equiv, =>
+ */
+ case OPCODE_neg: // Negation
+ case OPCODE_lnot: // Negation
+ case OPCODE_cl: // $ConjList
+ case OPCODE_dl: // $DisjList
+ case OPCODE_land: // \land
+ case OPCODE_lor: // \lor
+ case OPCODE_equiv: // \equiv
+ case OPCODE_implies: // =>
+ {
+ try {
+ BoolType.getInstance().unify(expected);
+ } catch (UnificationException e) {
+ throw new TypeErrorException(String.format("Expected %s, found BOOL at '%s',%n%s", expected,
n.getOperator().getName(), n.getLocation()));
+ }
+ for (int i = 0; i < n.getArgs().length; i++) {
+ visitExprOrOpArgNode(n.getArgs()[i], BoolType.getInstance());
+ }
+ return BoolType.getInstance();
}
- for (int i = 0; i < n.getArgs().length; i++) {
- visitExprOrOpArgNode(n.getArgs()[i], BoolType.getInstance());
- }
- return BoolType.getInstance();
- }
- /*
- * Quantification: \A x \in S : P or \E x \in S : P
- */
- case OPCODE_be: // \E x \in S : P
- case OPCODE_bf: // \A x \in S : P
- {
- try {
- BoolType.getInstance().unify(expected);
- } catch (UnificationException e) {
- throw new TypeErrorException(String.format("Expected %s, found BOOL at '%s',%n%s", expected,
+ /*
+ * Quantification: \A x \in S : P or \E x \in S : P
+ */
+ case OPCODE_be: // \E x \in S : P
+ case OPCODE_bf: // \A x \in S : P
+ {
+ try {
+ BoolType.getInstance().unify(expected);
+ } catch (UnificationException e) {
+ throw new TypeErrorException(String.format("Expected %s, found BOOL at '%s',%n%s", expected,
n.getOperator().getName(), n.getLocation()));
+ }
+ evalBoundedVariables(n);
+ visitExprOrOpArgNode(n.getArgs()[0], BoolType.getInstance());
+ return BoolType.getInstance();
}
- evalBoundedVariables(n);
- visitExprOrOpArgNode(n.getArgs()[0], BoolType.getInstance());
- return BoolType.getInstance();
- }
- /*
- * Set Operators
- */
- case OPCODE_se: // SetEnumeration {..}
- {
- SetType found = new SetType(new UntypedType());
- try {
- found = found.unify(expected);
- } catch (UnificationException e) {
- throw new TypeErrorException(
+ /*
+ * Set Operators
+ */
+ case OPCODE_se: // SetEnumeration {..}
+ {
+ SetType found = new SetType(new UntypedType());
+ try {
+ found = found.unify(expected);
+ } catch (UnificationException e) {
+ throw new TypeErrorException(
String.format("Expected %s, found POW(_A) at set enumeration,%n%s", expected, n.getLocation()));
+ }
+ TLAType current = found.getSubType();
+ for (int i = 0; i < n.getArgs().length; i++) {
+ current = visitExprOrOpArgNode(n.getArgs()[i], current);
+ }
+ return found;
}
- TLAType current = found.getSubType();
- for (int i = 0; i < n.getArgs().length; i++) {
- current = visitExprOrOpArgNode(n.getArgs()[i], current);
- }
- return found;
- }
- case OPCODE_in: // \in
- case OPCODE_notin: // \notin
- {
- if (!BoolType.getInstance().compare(expected)) {
- throw new TypeErrorException(String.format("Expected %s, found BOOL at '%s',%n%s", expected,
+ case OPCODE_in: // \in
+ case OPCODE_notin: // \notin
+ {
+ if (!BoolType.getInstance().compare(expected)) {
+ throw new TypeErrorException(String.format("Expected %s, found BOOL at '%s',%n%s", expected,
n.getOperator().getName(), n.getLocation()));
- }
- TLAType element = visitExprOrOpArgNode(n.getArgs()[0], new UntypedType());
- visitExprOrOpArgNode(n.getArgs()[1], new SetType(element));
+ }
+ TLAType element = visitExprOrOpArgNode(n.getArgs()[0], new UntypedType());
+ visitExprOrOpArgNode(n.getArgs()[1], new SetType(element));
- return BoolType.getInstance();
- }
+ return BoolType.getInstance();
+ }
- case OPCODE_setdiff: // set difference
- case OPCODE_cup: // set union
- case OPCODE_cap: // set intersection
- {
- SetType found = new SetType(new UntypedType());
- try {
- found = found.unify(expected);
- } catch (UnificationException e) {
- throw new TypeErrorException(String.format("Expected %s, found POW(_A) at '%s',%n%s", expected,
+ case OPCODE_setdiff: // set difference
+ case OPCODE_cup: // set union
+ case OPCODE_cap: // set intersection
+ {
+ SetType found = new SetType(new UntypedType());
+ try {
+ found = found.unify(expected);
+ } catch (UnificationException e) {
+ throw new TypeErrorException(String.format("Expected %s, found POW(_A) at '%s',%n%s", expected,
n.getOperator().getName(), n.getLocation()));
+ }
+ TLAType left = visitExprOrOpArgNode(n.getArgs()[0], found);
+ TLAType right = visitExprOrOpArgNode(n.getArgs()[1], left);
+ return right;
}
- TLAType left = visitExprOrOpArgNode(n.getArgs()[0], found);
- TLAType right = visitExprOrOpArgNode(n.getArgs()[1], left);
- return right;
- }
- case OPCODE_subseteq: // \subseteq - subset or equal
- {
- try {
- BoolType.getInstance().unify(expected);
- } catch (UnificationException e) {
- throw new TypeErrorException(String.format("Expected %s, found BOOL at '%s',%n%s", expected,
+ case OPCODE_subseteq: // \subseteq - subset or equal
+ {
+ try {
+ BoolType.getInstance().unify(expected);
+ } catch (UnificationException e) {
+ throw new TypeErrorException(String.format("Expected %s, found BOOL at '%s',%n%s", expected,
n.getOperator().getName(), n.getLocation()));
+ }
+ TLAType left = visitExprOrOpArgNode(n.getArgs()[0], new SetType(new UntypedType()));
+ visitExprOrOpArgNode(n.getArgs()[1], left);
+ return BoolType.getInstance();
}
- TLAType left = visitExprOrOpArgNode(n.getArgs()[0], new SetType(new UntypedType()));
- visitExprOrOpArgNode(n.getArgs()[1], left);
- return BoolType.getInstance();
- }
- /*
- * Set Constructor
- */
- case OPCODE_sso: // $SubsetOf Represents {x \in S : P}
- {
-
- TLAType domainType = evalBoundedVariables(n);
- SetType found = new SetType(domainType);
- try {
- found = found.unify(expected);
- } catch (UnificationException e) {
- throw new TypeErrorException(String.format("Expected %s, found %s at '%s',%n%s", expected, found,
+ /*
+ * Set Constructor
+ */
+ case OPCODE_sso: // $SubsetOf Represents {x \in S : P}
+ {
+
+ TLAType domainType = evalBoundedVariables(n);
+ SetType found = new SetType(domainType);
+ try {
+ found = found.unify(expected);
+ } catch (UnificationException e) {
+ throw new TypeErrorException(String.format("Expected %s, found %s at '%s',%n%s", expected, found,
n.getOperator().getName(), n.getLocation()));
+ }
+ visitExprOrOpArgNode(n.getArgs()[0], BoolType.getInstance());
+ return found;
}
- visitExprOrOpArgNode(n.getArgs()[0], BoolType.getInstance());
- return found;
- }
- case OPCODE_soa: // $SetOfAll Represents {e : p1 \in S, p2,p3 \in S2}
- {
- SetType found = new SetType(new UntypedType());
- try {
- found = found.unify(expected);
- } catch (UnificationException e) {
- throw new TypeErrorException(String.format("Expected %s, found POW(_A) at '%s',%n%s", expected,
+ case OPCODE_soa: // $SetOfAll Represents {e : p1 \in S, p2,p3 \in S2}
+ {
+ SetType found = new SetType(new UntypedType());
+ try {
+ found = found.unify(expected);
+ } catch (UnificationException e) {
+ throw new TypeErrorException(String.format("Expected %s, found POW(_A) at '%s',%n%s", expected,
n.getOperator().getName(), n.getLocation()));
+ }
+ evalBoundedVariables(n);
+ visitExprOrOpArgNode(n.getArgs()[0], found.getSubType());
+ return found;
}
- evalBoundedVariables(n);
- visitExprOrOpArgNode(n.getArgs()[0], found.getSubType());
- return found;
- }
- case OPCODE_subset: // SUBSET (conforms POW in B)
- {
- SetType found = new SetType(new UntypedType());
- try {
- found = found.unify(expected);
- } catch (UnificationException e) {
- throw new TypeErrorException(
+ case OPCODE_subset: // SUBSET (conforms POW in B)
+ {
+ SetType found = new SetType(new UntypedType());
+ try {
+ found = found.unify(expected);
+ } catch (UnificationException e) {
+ throw new TypeErrorException(
String.format("Expected %s, found POW(_A) at 'SUBSET',%n%s", expected, n.getLocation()));
+ }
+ visitExprOrOpArgNode(n.getArgs()[0], found.getSubType());
+ return found;
}
- visitExprOrOpArgNode(n.getArgs()[0], found.getSubType());
- return found;
- }
- case OPCODE_union: // Union - Union{{1},{2}}
- {
- SetType found = new SetType(new UntypedType());
- try {
- found = found.unify(expected);
- } catch (UnificationException e) {
- throw new TypeErrorException(
+ case OPCODE_union: // Union - Union{{1},{2}}
+ {
+ SetType found = new SetType(new UntypedType());
+ try {
+ found = found.unify(expected);
+ } catch (UnificationException e) {
+ throw new TypeErrorException(
String.format("Expected %s, found POW(_A) at 'SUBSET',%n%s", expected, n.getLocation()));
+ }
+ SetType setOfSet = (SetType) visitExprOrOpArgNode(n.getArgs()[0], new SetType(found));
+ return setOfSet.getSubType();
}
- SetType setOfSet = (SetType) visitExprOrOpArgNode(n.getArgs()[0], new SetType(found));
- return setOfSet.getSubType();
- }
- /*
- * Prime
- */
- case OPCODE_prime: // prime
- {
- try {
- OpApplNode node = (OpApplNode) n.getArgs()[0];
- if (node.getOperator().getKind() != VariableDeclKind) {
- throw new TypeErrorException(
+ /*
+ * Prime
+ */
+ case OPCODE_prime: // prime
+ {
+ try {
+ OpApplNode node = (OpApplNode) n.getArgs()[0];
+ if (node.getOperator().getKind() != VariableDeclKind) {
+ throw new TypeErrorException(
"Expected variable at \"" + node.getOperator().getName() + "\":\n" + node.getLocation());
- }
- return visitExprOrOpArgNode(n.getArgs()[0], expected);
- } catch (ClassCastException e) {
- throw new TypeErrorException(
+ }
+ return visitExprOrOpArgNode(n.getArgs()[0], expected);
+ } catch (ClassCastException e) {
+ throw new TypeErrorException(
"Expected variable as argument of prime operator:\n" + n.getArgs()[0].getLocation());
+ }
}
- }
- /*
- * Tuple: Tuple as Function 1..n to Set (Sequence)
- */
- case OPCODE_tup: { // $Tuple
- ArrayList<TLAType> list = new ArrayList<>();
- for (int i = 0; i < n.getArgs().length; i++) {
- list.add(visitExprOrOpArgNode(n.getArgs()[i], new UntypedType()));
- }
- TLAType found;
- if (list.isEmpty()) {
- found = new FunctionType(IntType.getInstance(), new UntypedType());
- } else if (list.size() == 1) {
- found = new FunctionType(IntType.getInstance(), list.get(0));
- } else {
- found = TupleOrFunction.createTupleOrFunctionType(list);
- // found = new TupleType(list);
- }
- try {
- found = found.unify(expected);
- } catch (UnificationException e) {
- throw new TypeErrorException(
+ /*
+ * Tuple: Tuple as Function 1..n to Set (Sequence)
+ */
+ case OPCODE_tup: { // $Tuple
+ ArrayList<TLAType> list = new ArrayList<>();
+ for (int i = 0; i < n.getArgs().length; i++) {
+ list.add(visitExprOrOpArgNode(n.getArgs()[i], new UntypedType()));
+ }
+ TLAType found;
+ if (list.isEmpty()) {
+ found = new FunctionType(IntType.getInstance(), new UntypedType());
+ } else if (list.size() == 1) {
+ found = new FunctionType(IntType.getInstance(), list.get(0));
+ } else {
+ found = TupleOrFunction.createTupleOrFunctionType(list);
+ // found = new TupleType(list);
+ }
+ try {
+ found = found.unify(expected);
+ } catch (UnificationException e) {
+ throw new TypeErrorException(
String.format("Expected %s, found %s at Tuple,%n%s", expected, found, n.getLocation()));
+ }
+ n.setToolObject(TYPE_ID, found);
+ tupleNodeList.add(n);
+ if (found instanceof AbstractHasFollowers) {
+ ((AbstractHasFollowers) found).addFollower(n);
+ }
+ return found;
}
- n.setToolObject(TYPE_ID, found);
- tupleNodeList.add(n);
- if (found instanceof AbstractHasFollowers) {
- ((AbstractHasFollowers) found).addFollower(n);
- }
- return found;
- }
- /*
- * Function constructors
- */
- case OPCODE_rfs: // recursive function ( f[x\in Nat] == IF x = 0 THEN 1
- // ELSE f[n-1]
- {
+ /*
+ * Function constructors
+ */
+ case OPCODE_rfs: // recursive function ( f[x\in Nat] == IF x = 0 THEN 1
+ // ELSE f[n-1]
+ {
- FormalParamNode recFunc = n.getUnbdedQuantSymbols()[0];
- symbolNodeList.add(recFunc);
- FunctionType recType = new FunctionType();
- recFunc.setToolObject(TYPE_ID, recType);
- recType.addFollower(recFunc);
+ FormalParamNode recFunc = n.getUnbdedQuantSymbols()[0];
+ symbolNodeList.add(recFunc);
+ FunctionType recType = new FunctionType();
+ recFunc.setToolObject(TYPE_ID, recType);
+ recType.addFollower(recFunc);
- TLAType domainType = evalBoundedVariables(n);
- FunctionType found = new FunctionType(domainType, new UntypedType());
- visitExprOrOpArgNode(n.getArgs()[0], found.getRange());
+ TLAType domainType = evalBoundedVariables(n);
+ FunctionType found = new FunctionType(domainType, new UntypedType());
+ visitExprOrOpArgNode(n.getArgs()[0], found.getRange());
- try {
- found = (FunctionType) found.unify(expected);
- } catch (UnificationException e) {
- throw new TypeErrorException("Expected '" + expected + "', found '" + found + "'.\n" + n.getLocation());
- }
+ try {
+ found = (FunctionType) found.unify(expected);
+ } catch (UnificationException e) {
+ throw new TypeErrorException("Expected '" + expected + "', found '" + found + "'.\n" + n.getLocation());
+ }
- TLAType t = null;
- try {
- t = (TLAType) recFunc.getToolObject(TYPE_ID);
- found = (FunctionType) found.unify(t);
- } catch (UnificationException e) {
- throw new TypeErrorException("Expected '" + expected + "', found '" + t + "'.\n" + n.getLocation());
- }
+ TLAType t = null;
+ try {
+ t = (TLAType) recFunc.getToolObject(TYPE_ID);
+ found = (FunctionType) found.unify(t);
+ } catch (UnificationException e) {
+ throw new TypeErrorException("Expected '" + expected + "', found '" + t + "'.\n" + n.getLocation());
+ }
- return found;
- }
+ return found;
+ }
- case OPCODE_nrfs: // succ[n \in Nat] == n + 1
- case OPCODE_fc: // [n \in Nat |-> n+1]
- {
- TLAType domainType = evalBoundedVariables(n);
- FunctionType found = new FunctionType(domainType, new UntypedType());
- visitExprOrOpArgNode(n.getArgs()[0], found.getRange());
+ case OPCODE_nrfs: // succ[n \in Nat] == n + 1
+ case OPCODE_fc: // [n \in Nat |-> n+1]
+ {
+ TLAType domainType = evalBoundedVariables(n);
+ FunctionType found = new FunctionType(domainType, new UntypedType());
+ visitExprOrOpArgNode(n.getArgs()[0], found.getRange());
- try {
- found = (FunctionType) found.unify(expected);
- } catch (UnificationException e) {
- throw new TypeErrorException("Expected '" + expected + "', found '" + found + "'.\n" + n.getLocation());
+ try {
+ found = (FunctionType) found.unify(expected);
+ } catch (UnificationException e) {
+ throw new TypeErrorException("Expected '" + expected + "', found '" + found + "'.\n" + n.getLocation());
+ }
+ return found;
}
- return found;
- }
- /*
- * Function call
- */
- case OPCODE_fa: // $FcnApply f[1]
- {
- TLAType domType;
- ExprOrOpArgNode dom = n.getArgs()[1];
- if (dom instanceof OpApplNode && ((OpApplNode) dom).getOperator().getName().toString().equals("$Tuple")) {
- ArrayList<TLAType> domList = new ArrayList<>();
- OpApplNode domOpAppl = (OpApplNode) dom;
- for (int i = 0; i < domOpAppl.getArgs().length; i++) {
- TLAType d = visitExprOrOpArgNode(domOpAppl.getArgs()[i], new UntypedType());
- domList.add(d);
- }
-
- if (domList.size() == 1) { // one-tuple
- domType = new FunctionType(IntType.getInstance(), domList.get(0));
- FunctionType func = new FunctionType(domType, expected);
- TLAType res = visitExprOrOpArgNode(n.getArgs()[0], func);
- return ((FunctionType) res).getRange();
- } else {
- domType = new TupleType(domList);
- FunctionType func = new FunctionType(domType, expected);
- TLAType res = visitExprOrOpArgNode(n.getArgs()[0], func);
- return ((FunctionType) res).getRange();
- }
- } else {
- ExprOrOpArgNode arg = n.getArgs()[1];
- if (arg instanceof NumeralNode) {
- NumeralNode num = (NumeralNode) arg;
- UntypedType u = new UntypedType();
- n.setToolObject(TYPE_ID, u);
- u.addFollower(n);
- TupleOrFunction tupleOrFunc = new TupleOrFunction(num.val(), u);
-
- TLAType res = visitExprOrOpArgNode(n.getArgs()[0], tupleOrFunc);
- n.getArgs()[0].setToolObject(TYPE_ID, res);
- tupleNodeList.add(n.getArgs()[0]);
- if (res instanceof AbstractHasFollowers) {
- ((AbstractHasFollowers) res).addFollower(n.getArgs()[0]);
+ /*
+ * Function call
+ */
+ case OPCODE_fa: // $FcnApply f[1]
+ {
+ TLAType domType;
+ ExprOrOpArgNode dom = n.getArgs()[1];
+ if (dom instanceof OpApplNode && ((OpApplNode) dom).getOperator().getName().toString().equals("$Tuple")) {
+ ArrayList<TLAType> domList = new ArrayList<>();
+ OpApplNode domOpAppl = (OpApplNode) dom;
+ for (int i = 0; i < domOpAppl.getArgs().length; i++) {
+ TLAType d = visitExprOrOpArgNode(domOpAppl.getArgs()[i], new UntypedType());
+ domList.add(d);
}
- TLAType found = (TLAType) n.getToolObject(TYPE_ID);
- try {
- found = found.unify(expected);
- } catch (UnificationException e) {
- throw new TypeErrorException("Expected '" + expected + "', found '" + found + "'.\n"
+
+ if (domList.size() == 1) { // one-tuple
+ domType = new FunctionType(IntType.getInstance(), domList.get(0));
+ FunctionType func = new FunctionType(domType, expected);
+ TLAType res = visitExprOrOpArgNode(n.getArgs()[0], func);
+ return ((FunctionType) res).getRange();
+ } else {
+ domType = new TupleType(domList);
+ FunctionType func = new FunctionType(domType, expected);
+ TLAType res = visitExprOrOpArgNode(n.getArgs()[0], func);
+ return ((FunctionType) res).getRange();
+ }
+ } else {
+ ExprOrOpArgNode arg = n.getArgs()[1];
+ if (arg instanceof NumeralNode) {
+ NumeralNode num = (NumeralNode) arg;
+ UntypedType u = new UntypedType();
+ n.setToolObject(TYPE_ID, u);
+ u.addFollower(n);
+ TupleOrFunction tupleOrFunc = new TupleOrFunction(num.val(), u);
+
+ TLAType res = visitExprOrOpArgNode(n.getArgs()[0], tupleOrFunc);
+ n.getArgs()[0].setToolObject(TYPE_ID, res);
+ tupleNodeList.add(n.getArgs()[0]);
+ if (res instanceof AbstractHasFollowers) {
+ ((AbstractHasFollowers) res).addFollower(n.getArgs()[0]);
+ }
+ TLAType found = (TLAType) n.getToolObject(TYPE_ID);
+ try {
+ found = found.unify(expected);
+ } catch (UnificationException e) {
+ throw new TypeErrorException("Expected '" + expected + "', found '" + found + "'.\n"
+ n.getArgs()[0].toString(2) + "\n" + n.getLocation());
+ }
+ return found;
}
- return found;
+ domType = visitExprOrOpArgNode(n.getArgs()[1], new UntypedType());
}
- domType = visitExprOrOpArgNode(n.getArgs()[1], new UntypedType());
+ FunctionType func = new FunctionType(domType, expected);
+ TLAType res = visitExprOrOpArgNode(n.getArgs()[0], func);
+ return ((FunctionType) res).getRange();
+
}
- FunctionType func = new FunctionType(domType, expected);
- TLAType res = visitExprOrOpArgNode(n.getArgs()[0], func);
- return ((FunctionType) res).getRange();
- }
+ /*
+ * Domain of Function
+ */
+ case OPCODE_domain: {
- /*
- * Domain of Function
- */
- case OPCODE_domain: {
-
- FunctionType func = new FunctionType(new UntypedType(), new UntypedType());
- func = (FunctionType) visitExprOrOpArgNode(n.getArgs()[0], func);
- TLAType res = null;
- try {
- res = new SetType(func.getDomain()).unify(expected);
- } catch (UnificationException e) {
- throw new TypeErrorException(String.format("Expected '%s', found '%s' at 'DOMAIN(..)',%n%s", expected,
+ FunctionType func = new FunctionType(new UntypedType(), new UntypedType());
+ func = (FunctionType) visitExprOrOpArgNode(n.getArgs()[0], func);
+ TLAType res = null;
+ try {
+ res = new SetType(func.getDomain()).unify(expected);
+ } catch (UnificationException e) {
+ throw new TypeErrorException(String.format("Expected '%s', found '%s' at 'DOMAIN(..)',%n%s", expected,
func, n.getLocation()));
+ }
+ return res;
}
- return res;
- }
- /*
- * Set of Function
- */
- case OPCODE_sof: // [ A -> B]
- {
- SetType A = (SetType) visitExprOrOpArgNode(n.getArgs()[0], new SetType(new UntypedType()));
- SetType B = (SetType) visitExprOrOpArgNode(n.getArgs()[1], new SetType(new UntypedType()));
-
- SetType found = new SetType(new FunctionType(A.getSubType(), B.getSubType()));
- try {
- found = found.unify(expected);
- } catch (UnificationException e) {
- throw new TypeErrorException(String.format("Expected '%s', found '%s' at Set of Function,%n%s",
+ /*
+ * Set of Function
+ */
+ case OPCODE_sof: // [ A -> B]
+ {
+ SetType A = (SetType) visitExprOrOpArgNode(n.getArgs()[0], new SetType(new UntypedType()));
+ SetType B = (SetType) visitExprOrOpArgNode(n.getArgs()[1], new SetType(new UntypedType()));
+
+ SetType found = new SetType(new FunctionType(A.getSubType(), B.getSubType()));
+ try {
+ found = found.unify(expected);
+ } catch (UnificationException e) {
+ throw new TypeErrorException(String.format("Expected '%s', found '%s' at Set of Function,%n%s",
expected, found, n.getLocation()));
+ }
+ return found;
}
- return found;
- }
- /*
- * Except
- */
- case OPCODE_exc: // $Except
- {
- return evalExcept(n, expected);
- }
+ /*
+ * Except
+ */
+ case OPCODE_exc: // $Except
+ {
+ return evalExcept(n, expected);
+ }
- /*
- * Cartesian Product: A \X B
- */
- case OPCODE_cp: // $CartesianProd A \X B \X C as $CartesianProd(A, B, C)
- {
- ArrayList<TLAType> list = new ArrayList<>();
- for (int i = 0; i < n.getArgs().length; i++) {
- SetType t = (SetType) visitExprOrOpArgNode(n.getArgs()[i], new SetType(new UntypedType()));
- list.add(t.getSubType());
- }
- SetType found = new SetType(new TupleType(list));
- try {
- found = found.unify(expected);
- } catch (UnificationException e) {
- throw new TypeErrorException(String.format("Expected %s, found %s at Cartesian Product,%n%s", expected,
+ /*
+ * Cartesian Product: A \X B
+ */
+ case OPCODE_cp: // $CartesianProd A \X B \X C as $CartesianProd(A, B, C)
+ {
+ ArrayList<TLAType> list = new ArrayList<>();
+ for (int i = 0; i < n.getArgs().length; i++) {
+ SetType t = (SetType) visitExprOrOpArgNode(n.getArgs()[i], new SetType(new UntypedType()));
+ list.add(t.getSubType());
+ }
+ SetType found = new SetType(new TupleType(list));
+ try {
+ found = found.unify(expected);
+ } catch (UnificationException e) {
+ throw new TypeErrorException(String.format("Expected %s, found %s at Cartesian Product,%n%s", expected,
found, n.getLocation()));
- }
+ }
- return found;
- }
+ return found;
+ }
- /*
- * Records
- */
- case OPCODE_sor: // $SetOfRcds [L1 : e1, L2 : e2]
- {
- StructType struct = new StructType();
- for (int i = 0; i < n.getArgs().length; i++) {
- OpApplNode pair = (OpApplNode) n.getArgs()[i];
- StringNode field = (StringNode) pair.getArgs()[0];
- SetType fieldType = (SetType) visitExprOrOpArgNode(pair.getArgs()[1], new SetType(new UntypedType()));
- struct.add(field.getRep().toString(), fieldType.getSubType());
- }
-
- SetType found = new SetType(struct);
- try {
- found = found.unify(expected);
- } catch (UnificationException e) {
- throw new TypeErrorException(String.format("Expected %s, found %s at Set of Records,%n%s", expected,
+ /*
+ * Records
+ */
+ case OPCODE_sor: // $SetOfRcds [L1 : e1, L2 : e2]
+ {
+ StructType struct = new StructType();
+ for (int i = 0; i < n.getArgs().length; i++) {
+ OpApplNode pair = (OpApplNode) n.getArgs()[i];
+ StringNode field = (StringNode) pair.getArgs()[0];
+ SetType fieldType = (SetType) visitExprOrOpArgNode(pair.getArgs()[1], new SetType(new UntypedType()));
+ struct.add(field.getRep().toString(), fieldType.getSubType());
+ }
+
+ SetType found = new SetType(struct);
+ try {
+ found = found.unify(expected);
+ } catch (UnificationException e) {
+ throw new TypeErrorException(String.format("Expected %s, found %s at Set of Records,%n%s", expected,
found, n.getLocation()));
+ }
+ n.setToolObject(TYPE_ID, found);
+ found.addFollower(n);
+ return found;
}
- n.setToolObject(TYPE_ID, found);
- found.addFollower(n);
- return found;
- }
- case OPCODE_rc: // [h_1 |-> 1, h_2 |-> 2]
- {
- StructType found = new StructType();
- for (int i = 0; i < n.getArgs().length; i++) {
- OpApplNode pair = (OpApplNode) n.getArgs()[i];
- StringNode field = (StringNode) pair.getArgs()[0];
- TLAType fieldType = visitExprOrOpArgNode(pair.getArgs()[1], new UntypedType());
- found.add(field.getRep().toString(), fieldType);
- }
- try {
- found = found.unify(expected);
- } catch (UnificationException e) {
- throw new TypeErrorException(
+ case OPCODE_rc: // [h_1 |-> 1, h_2 |-> 2]
+ {
+ StructType found = new StructType();
+ for (int i = 0; i < n.getArgs().length; i++) {
+ OpApplNode pair = (OpApplNode) n.getArgs()[i];
+ StringNode field = (StringNode) pair.getArgs()[0];
+ TLAType fieldType = visitExprOrOpArgNode(pair.getArgs()[1], new UntypedType());
+ found.add(field.getRep().toString(), fieldType);
+ }
+ try {
+ found = found.unify(expected);
+ } catch (UnificationException e) {
+ throw new TypeErrorException(
String.format("Expected %s, found %s at Record,%n%s", expected, found, n.getLocation()));
- }
- n.setToolObject(TYPE_ID, found);
- found.addFollower(n);
+ }
+ n.setToolObject(TYPE_ID, found);
+ found.addFollower(n);
- return found;
+ return found;
- }
+ }
- case OPCODE_rs: // $RcdSelect r.c
- {
- String fieldName = ((StringNode) n.getArgs()[1]).getRep().toString();
- StructType r = (StructType) visitExprOrOpArgNode(n.getArgs()[0], StructType.getIncompleteStruct());
+ case OPCODE_rs: // $RcdSelect r.c
+ {
+ String fieldName = ((StringNode) n.getArgs()[1]).getRep().toString();
+ StructType r = (StructType) visitExprOrOpArgNode(n.getArgs()[0], StructType.getIncompleteStruct());
- StructType expectedStruct = StructType.getIncompleteStruct();
- expectedStruct.add(fieldName, expected);
+ StructType expectedStruct = StructType.getIncompleteStruct();
+ expectedStruct.add(fieldName, expected);
- try {
- r = r.unify(expectedStruct);
- } catch (UnificationException e) {
- throw new TypeErrorException(String.format("Struct has no field %s with type %s: %s%n%s", fieldName,
+ try {
+ r = r.unify(expectedStruct);
+ } catch (UnificationException e) {
+ throw new TypeErrorException(String.format("Struct has no field %s with type %s: %s%n%s", fieldName,
r.getType(fieldName), r, n.getLocation()));
+ }
+ n.getArgs()[0].setToolObject(TYPE_ID, r);
+ r.addFollower(n.getArgs()[0]);
+ return r.getType(fieldName);
}
- n.getArgs()[0].setToolObject(TYPE_ID, r);
- r.addFollower(n.getArgs()[0]);
- return r.getType(fieldName);
- }
- /*
- * miscellaneous constructs
- */
- case OPCODE_ite: // IF THEN ELSE
- {
- visitExprOrOpArgNode(n.getArgs()[0], BoolType.getInstance());
- TLAType then = visitExprOrOpArgNode(n.getArgs()[1], expected);
- TLAType eelse = visitExprOrOpArgNode(n.getArgs()[2], then);
- n.setToolObject(TYPE_ID, eelse);
- if (eelse instanceof AbstractHasFollowers) {
- ((AbstractHasFollowers) eelse).addFollower(n);
- }
- return eelse;
- }
-
- case OPCODE_case: {
/*
- * CASE p1 -> e1 [] p2 -> e2 represented as $Case( $Pair(p1,
- * e1),$Pair(p2, e2) ) and CASE p1 -> e1 [] p2 -> e2 [] OTHER -> e3
- * represented as $Case( $Pair(p1, e1), $Pair(p2, e2), $Pair(null,
- * e3))
+ * miscellaneous constructs
*/
- TLAType found = expected;
- for (int i = 0; i < n.getArgs().length; i++) {
- OpApplNode pair = (OpApplNode) n.getArgs()[i];
- if (pair.getArgs()[0] != null) {
- visitExprOrOpArgNode(pair.getArgs()[0], BoolType.getInstance());
+ case OPCODE_ite: // IF THEN ELSE
+ {
+ visitExprOrOpArgNode(n.getArgs()[0], BoolType.getInstance());
+ TLAType then = visitExprOrOpArgNode(n.getArgs()[1], expected);
+ TLAType eelse = visitExprOrOpArgNode(n.getArgs()[2], then);
+ n.setToolObject(TYPE_ID, eelse);
+ if (eelse instanceof AbstractHasFollowers) {
+ ((AbstractHasFollowers) eelse).addFollower(n);
}
- found = visitExprOrOpArgNode(pair.getArgs()[1], found);
+ return eelse;
}
- return found;
- }
+ case OPCODE_case: {
+ /*
+ * CASE p1 -> e1 [] p2 -> e2 represented as $Case( $Pair(p1,
+ * e1),$Pair(p2, e2) ) and CASE p1 -> e1 [] p2 -> e2 [] OTHER -> e3
+ * represented as $Case( $Pair(p1, e1), $Pair(p2, e2), $Pair(null,
+ * e3))
+ */
+ TLAType found = expected;
+ for (int i = 0; i < n.getArgs().length; i++) {
+ OpApplNode pair = (OpApplNode) n.getArgs()[i];
+ if (pair.getArgs()[0] != null) {
+ visitExprOrOpArgNode(pair.getArgs()[0], BoolType.getInstance());
+ }
+ found = visitExprOrOpArgNode(pair.getArgs()[1], found);
+ }
+ return found;
- case OPCODE_uc: {
- List<TLAType> list = new ArrayList<>();
- for (FormalParamNode param : n.getUnbdedQuantSymbols()) {
- TLAType paramType = new UntypedType();
- symbolNodeList.add(param);
- setType(param, paramType);
- list.add(paramType);
- }
- TLAType found = null;
- if (list.size() == 1) {
- found = list.get(0);
- } else {
- found = new TupleType(list);
}
- try {
- found = found.unify(expected);
- } catch (UnificationException e) {
- throw new TypeErrorException(
+
+ case OPCODE_uc: {
+ List<TLAType> list = new ArrayList<>();
+ for (FormalParamNode param : n.getUnbdedQuantSymbols()) {
+ TLAType paramType = new UntypedType();
+ symbolNodeList.add(param);
+ setType(param, paramType);
+ list.add(paramType);
+ }
+ TLAType found = null;
+ if (list.size() == 1) {
+ found = list.get(0);
+ } else {
+ found = new TupleType(list);
+ }
+ try {
+ found = found.unify(expected);
+ } catch (UnificationException e) {
+ throw new TypeErrorException(
String.format("Expected %s, found %s at 'CHOOSE',%n%s", expected, found, n.getLocation()));
- }
- setType(n, found);
- visitExprOrOpArgNode(n.getArgs()[0], BoolType.getInstance());
+ }
+ setType(n, found);
+ visitExprOrOpArgNode(n.getArgs()[0], BoolType.getInstance());
- return getType(n);
+ return getType(n);
- }
+ }
- case OPCODE_bc: { // CHOOSE x \in S: P
- TLAType found = evalBoundedVariables(n);
- try {
- found = found.unify(expected);
- } catch (UnificationException e) {
- throw new TypeErrorException(
+ case OPCODE_bc: { // CHOOSE x \in S: P
+ TLAType found = evalBoundedVariables(n);
+ try {
+ found = found.unify(expected);
+ } catch (UnificationException e) {
+ throw new TypeErrorException(
String.format("Expected %s, found %s at 'CHOOSE',%n%s", expected, found, n.getLocation()));
+ }
+ visitExprOrOpArgNode(n.getArgs()[0], BoolType.getInstance());
+ return found;
}
- visitExprOrOpArgNode(n.getArgs()[0], BoolType.getInstance());
- return found;
- }
- case OPCODE_unchanged: {
- return BoolType.getInstance().unify(expected);
- }
+ case OPCODE_unchanged: {
+ return BoolType.getInstance().unify(expected);
+ }
- /*
- * no TLA+ Built-ins
- */
- case 0: {
- return evalBBuiltIns(n, expected);
- }
+ /*
+ * no TLA+ Built-ins
+ */
+ case 0: {
+ return evalBBuiltIns(n, expected);
+ }
}
throw new NotImplementedException(
- "Not supported Operator: " + n.getOperator().getName() + "\n" + n.getLocation());
+ "Not supported Operator: " + n.getOperator().getName() + "\n" + n.getLocation());
}
private TLAType evalBoundedVariables(OpApplNode n) throws TLA2BException {
@@ -1019,7 +1015,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
expected = (FunctionType) expected.unify(subType);
} catch (UnificationException e) {
throw new TypeErrorException(String.format("Expected %s, found %s at parameter %s,%n%s",
- expected, subType, p.getName().toString(), bounds[i].getLocation()));
+ expected, subType, p.getName().toString(), bounds[i].getLocation()));
}
domList.add(expected);
symbolNodeList.add(p);
@@ -1033,7 +1029,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
tuple = (TupleType) tuple.unify(subType);
} catch (UnificationException e) {
throw new TypeErrorException(String.format("Expected %s, found %s at tuple,%n%s", tuple,
- subType, bounds[i].getLocation()));
+ subType, bounds[i].getLocation()));
}
domList.add(tuple);
for (int j = 0; j < params[i].length; j++) {
@@ -1101,7 +1097,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
t = t.unify(s);
} catch (UnificationException e) {
throw new TypeErrorException(
- String.format("Expected %s, found %s at 'EXCEPT',%n%s", t, s, pair.getLocation()));
+ String.format("Expected %s, found %s at 'EXCEPT',%n%s", t, s, pair.getLocation()));
}
} else {
@@ -1110,7 +1106,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
TLAType domType;
TLAType rangeType;
if (domExpr instanceof OpApplNode
- && ((OpApplNode) domExpr).getOperator().getName().toString().equals("$Tuple")) {
+ && ((OpApplNode) domExpr).getOperator().getName().toString().equals("$Tuple")) {
ArrayList<TLAType> domList = new ArrayList<>();
OpApplNode domOpAppl = (OpApplNode) domExpr;
for (int j = 0; j < domOpAppl.getArgs().length; j++) {
@@ -1128,7 +1124,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
t = t.unify(func);
} catch (UnificationException e) {
throw new TypeErrorException(
- String.format("Expected %s, found %s at 'EXCEPT',%n%s", t, func, pair.getLocation()));
+ String.format("Expected %s, found %s at 'EXCEPT',%n%s", t, func, pair.getLocation()));
}
}
}
@@ -1154,73 +1150,73 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
private TLAType evalBBuiltIns(OpApplNode n, TLAType expected) throws TLA2BException {
switch (BBuiltInOPs.getOpcode(n.getOperator().getName())) {
- // B Builtins
-
- /*
- * Standard Module Naturals
- */
- case B_OPCODE_gt: // >
- case B_OPCODE_lt: // <
- case B_OPCODE_leq: // <=
- case B_OPCODE_geq: // >=
- {
- try {
- BoolType.getInstance().unify(expected);
- } catch (UnificationException e) {
- throw new TypeErrorException(String.format("Expected %s, found BOOL 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 BoolType.getInstance();
- }
+ // B Builtins
- case B_OPCODE_plus: // +
- case B_OPCODE_minus: // -
- case B_OPCODE_times: // *
- case B_OPCODE_div: // /
- case B_OPCODE_mod: // % modulo
- case B_OPCODE_exp: { // x hoch y, x^y
- TLAType type;
- // TODO: Simplify
- if (expected instanceof RealType) {
+ /*
+ * Standard Module Naturals
+ */
+ case B_OPCODE_gt: // >
+ case B_OPCODE_lt: // <
+ case B_OPCODE_leq: // <=
+ case B_OPCODE_geq: // >=
+ {
try {
- RealType.getInstance().unify(expected);
- type = RealType.getInstance();
+ BoolType.getInstance().unify(expected);
} catch (UnificationException e) {
- throw new TypeErrorException(String.format("Expected %s, found REAL at '%s',%n%s", expected,
- n.getOperator().getName(), n.getLocation()));
+ throw new TypeErrorException(String.format("Expected %s, found BOOL at '%s',%n%s", expected,
+ n.getOperator().getName(), n.getLocation()));
}
- } else if (expected instanceof IntType) {
- try {
+ for (int i = 0; i < n.getArgs().length; i++) {
+ visitExprOrOpArgNode(n.getArgs()[i], IntType.getInstance());
+ }
+ return BoolType.getInstance();
+ }
+
+ case B_OPCODE_plus: // +
+ case B_OPCODE_minus: // -
+ case B_OPCODE_times: // *
+ case B_OPCODE_div: // /
+ case B_OPCODE_mod: // % modulo
+ case B_OPCODE_exp: { // x hoch y, x^y
+ TLAType type;
+ // TODO: Simplify
+ if (expected instanceof RealType) {
+ try {
+ RealType.getInstance().unify(expected);
+ type = RealType.getInstance();
+ } catch (UnificationException e) {
+ throw new TypeErrorException(String.format("Expected %s, found REAL at '%s',%n%s", expected,
+ n.getOperator().getName(), n.getLocation()));
+ }
+ } else if (expected instanceof IntType) {
+ try {
+ IntType.getInstance().unify(expected);
+ type = IntType.getInstance();
+ } catch (UnificationException ue) {
+ throw new TypeErrorException(String.format("Expected %s, found INTEGER at '%s',%n%s", expected,
+ n.getOperator().getName(), n.getLocation()));
+ }
+ } else if (expected instanceof UntypedType) {
IntType.getInstance().unify(expected);
type = IntType.getInstance();
- } catch (UnificationException ue) {
+ try {
+ for (int i = 0; i < n.getArgs().length; i++) {
+ visitExprOrOpArgNode(n.getArgs()[i], type);
+ }
+ } catch (TypeErrorException e) {
+ RealType.getInstance().unify(expected);
+ type = RealType.getInstance();
+ }
+ } else {
throw new TypeErrorException(String.format("Expected %s, found INTEGER at '%s',%n%s", expected,
n.getOperator().getName(), n.getLocation()));
}
- } else if (expected instanceof UntypedType) {
- IntType.getInstance().unify(expected);
- type = IntType.getInstance();
- try {
- for (int i = 0; i < n.getArgs().length; i++) {
- visitExprOrOpArgNode(n.getArgs()[i], type);
- }
- } catch (TypeErrorException e) {
- RealType.getInstance().unify(expected);
- type = RealType.getInstance();
+ for (int i = 0; i < n.getArgs().length; i++) {
+ visitExprOrOpArgNode(n.getArgs()[i], type);
}
- } else {
- 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], type);
- }
- return type;
- }
+ return type;
+ }
case B_OPCODE_realdiv: { // /
try {
@@ -1235,337 +1231,337 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
return RealType.getInstance();
}
- case B_OPCODE_dotdot: // ..
- {
- try {
- expected.unify(new SetType(IntType.getInstance()));
- } catch (UnificationException e) {
- throw new TypeErrorException(
+ case B_OPCODE_dotdot: // ..
+ {
+ try {
+ expected.unify(new SetType(IntType.getInstance()));
+ } catch (UnificationException e) {
+ throw new TypeErrorException(
String.format("Expected %s, found POW(INTEGER) at '..',%n%s", expected, n.getLocation()));
- }
+ }
- for (int i = 0; i < n.getArgs().length; i++) {
- visitExprOrOpArgNode(n.getArgs()[i], IntType.getInstance());
+ for (int i = 0; i < n.getArgs().length; i++) {
+ visitExprOrOpArgNode(n.getArgs()[i], IntType.getInstance());
+ }
+ return new SetType(IntType.getInstance());
}
- return new SetType(IntType.getInstance());
- }
- case B_OPCODE_nat: // Nat
- {
- try {
- SetType found = new SetType(IntType.getInstance());
- found = found.unify(expected);
- return found;
- } catch (UnificationException e) {
- throw new TypeErrorException(
+ case B_OPCODE_nat: // Nat
+ {
+ try {
+ SetType found = new SetType(IntType.getInstance());
+ found = found.unify(expected);
+ return found;
+ } catch (UnificationException e) {
+ throw new TypeErrorException(
String.format("Expected %s, found POW(INTEGER) at 'Nat',%n%s", expected, n.getLocation()));
+ }
}
- }
- /*
- * Standard Module Integers
- */
- case B_OPCODE_int: // Int
- {
- try {
- SetType found = new SetType(IntType.getInstance());
- found = found.unify(expected);
- return found;
- } catch (UnificationException e) {
- throw new TypeErrorException(
+ /*
+ * Standard Module Integers
+ */
+ case B_OPCODE_int: // Int
+ {
+ try {
+ SetType found = new SetType(IntType.getInstance());
+ found = found.unify(expected);
+ return found;
+ } catch (UnificationException e) {
+ throw new TypeErrorException(
String.format("Expected %s, found POW(INTEGER) at 'Int',%n%s", expected, n.getLocation()));
+ }
}
- }
-
- 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
- {
- // TODO: simplify
- TLAType type;
- if (expected instanceof RealType) {
+ case B_OPCODE_real: // Real
+ {
try {
- RealType.getInstance().unify(expected);
- type = RealType.getInstance();
+ SetType found = new SetType(RealType.getInstance());
+ found = found.unify(expected);
+ return found;
} catch (UnificationException e) {
throw new TypeErrorException(
- String.format("Expected %s, found REAL at '-',%n%s", expected, n.getLocation()));
+ String.format("Expected %s, found POW(REAL) at 'Real',%n%s", expected, n.getLocation()));
}
- } else if (expected instanceof IntType) {
- try {
+ }
+
+ case B_OPCODE_uminus: // -x
+ {
+ // TODO: simplify
+ TLAType type;
+ if (expected instanceof RealType) {
+ try {
+ RealType.getInstance().unify(expected);
+ type = RealType.getInstance();
+ } catch (UnificationException e) {
+ throw new TypeErrorException(
+ String.format("Expected %s, found REAL at '-',%n%s", expected, n.getLocation()));
+ }
+ } else if (expected instanceof IntType) {
+ try {
+ IntType.getInstance().unify(expected);
+ type = IntType.getInstance();
+ } catch (UnificationException e) {
+ throw new TypeErrorException(
+ String.format("Expected %s, found INTEGER at '-',%n%s", expected, n.getLocation()));
+ }
+ } else if (expected instanceof UntypedType) {
IntType.getInstance().unify(expected);
type = IntType.getInstance();
- } catch (UnificationException e) {
+ try {
+ visitExprOrOpArgNode(n.getArgs()[0], type);
+ } catch (TypeErrorException e) {
+ RealType.getInstance().unify(expected);
+ type = RealType.getInstance();
+ }
+ } else {
throw new TypeErrorException(
String.format("Expected %s, found INTEGER at '-',%n%s", expected, n.getLocation()));
}
- } else if (expected instanceof UntypedType) {
- IntType.getInstance().unify(expected);
- type = IntType.getInstance();
- try {
- visitExprOrOpArgNode(n.getArgs()[0], type);
- } catch (TypeErrorException e) {
- RealType.getInstance().unify(expected);
- type = RealType.getInstance();
- }
- } else {
- throw new TypeErrorException(
- String.format("Expected %s, found INTEGER at '-',%n%s", expected, n.getLocation()));
+ visitExprOrOpArgNode(n.getArgs()[0], type);
+ return type;
}
- visitExprOrOpArgNode(n.getArgs()[0], type);
- return type;
- }
- /*
- * Standard Module FiniteSets
- */
- case B_OPCODE_finite: // IsFiniteSet
- {
- try {
- BoolType.getInstance().unify(expected);
- } catch (UnificationException e) {
- throw new TypeErrorException(
+ /*
+ * Standard Module FiniteSets
+ */
+ case B_OPCODE_finite: // IsFiniteSet
+ {
+ try {
+ BoolType.getInstance().unify(expected);
+ } catch (UnificationException e) {
+ throw new TypeErrorException(
String.format("Expected %s, found BOOL at 'IsFiniteSet',%n%s", expected, n.getLocation()));
+ }
+ visitExprOrOpArgNode(n.getArgs()[0], new SetType(new UntypedType()));
+ return BoolType.getInstance();
}
- visitExprOrOpArgNode(n.getArgs()[0], new SetType(new UntypedType()));
- return BoolType.getInstance();
- }
- case B_OPCODE_card: // Cardinality
- {
- try {
- IntType.getInstance().unify(expected);
- } catch (UnificationException e) {
- throw new TypeErrorException(
+ case B_OPCODE_card: // Cardinality
+ {
+ try {
+ IntType.getInstance().unify(expected);
+ } catch (UnificationException e) {
+ throw new TypeErrorException(
String.format("Expected %s, found INTEGER at 'Cardinality',%n%s", expected, n.getLocation()));
+ }
+ visitExprOrOpArgNode(n.getArgs()[0], new SetType(new UntypedType()));
+ return IntType.getInstance();
}
- visitExprOrOpArgNode(n.getArgs()[0], new SetType(new UntypedType()));
- return IntType.getInstance();
- }
- /*
- * Standard Module Sequences
- */
- case B_OPCODE_seq: { // Seq(S) - set of sequences, S must be a set
+ /*
+ * Standard Module Sequences
+ */
+ case B_OPCODE_seq: { // Seq(S) - set of sequences, S must be a set
- SetType S = (SetType) visitExprOrOpArgNode(n.getArgs()[0], new SetType(new UntypedType()));
+ SetType S = (SetType) visitExprOrOpArgNode(n.getArgs()[0], new SetType(new UntypedType()));
- SetType set_of_seq = new SetType(new FunctionType(IntType.getInstance(), S.getSubType()));
- try {
- set_of_seq = set_of_seq.unify(expected);
- } catch (UnificationException e) {
- throw new TypeErrorException(
+ SetType set_of_seq = new SetType(new FunctionType(IntType.getInstance(), S.getSubType()));
+ try {
+ set_of_seq = set_of_seq.unify(expected);
+ } catch (UnificationException e) {
+ throw new TypeErrorException(
String.format("Expected %s, found %s at 'Seq',%n%s", expected, set_of_seq, n.getLocation()));
+ }
+ return set_of_seq;
}
- return set_of_seq;
- }
- case B_OPCODE_len: { // length of the sequence
- try {
- IntType.getInstance().unify(expected);
- } catch (UnificationException e) {
- throw new TypeErrorException(
+ case B_OPCODE_len: { // length of the sequence
+ try {
+ IntType.getInstance().unify(expected);
+ } catch (UnificationException e) {
+ throw new TypeErrorException(
String.format("Expected %s, found INTEGER at 'Len',%n%s", expected, n.getLocation()));
+ }
+ visitExprOrOpArgNode(n.getArgs()[0], new FunctionType(IntType.getInstance(), new UntypedType()));
+ return IntType.getInstance();
}
- visitExprOrOpArgNode(n.getArgs()[0], new FunctionType(IntType.getInstance(), new UntypedType()));
- return IntType.getInstance();
- }
- case B_OPCODE_conc: { // s \o s2 - concatenation of s and s2
- TLAType found = new FunctionType(IntType.getInstance(), new UntypedType());
- found = visitExprOrOpArgNode(n.getArgs()[0], found);
- found = visitExprOrOpArgNode(n.getArgs()[1], found);
- try {
- found = found.unify(expected);
- } catch (UnificationException e) {
- throw new TypeErrorException(
+ case B_OPCODE_conc: { // s \o s2 - concatenation of s and s2
+ TLAType found = new FunctionType(IntType.getInstance(), new UntypedType());
+ found = visitExprOrOpArgNode(n.getArgs()[0], found);
+ found = visitExprOrOpArgNode(n.getArgs()[1], found);
+ try {
+ found = found.unify(expected);
+ } catch (UnificationException e) {
+ throw new TypeErrorException(
String.format("Expected %s, found POW(INTEGER*_A) at '\\o',%n%s", expected, n.getLocation()));
+ }
+ return found;
}
- return found;
- }
- case B_OPCODE_append: // Append(s, e)
- {
- FunctionType found = new FunctionType(IntType.getInstance(), new UntypedType());
- found = (FunctionType) visitExprOrOpArgNode(n.getArgs()[0], found);
- visitExprOrOpArgNode(n.getArgs()[1], found.getRange());
- try {
- found = (FunctionType) found.unify(expected);
- } catch (UnificationException e) {
- throw new TypeErrorException(
+ case B_OPCODE_append: // Append(s, e)
+ {
+ FunctionType found = new FunctionType(IntType.getInstance(), new UntypedType());
+ found = (FunctionType) visitExprOrOpArgNode(n.getArgs()[0], found);
+ visitExprOrOpArgNode(n.getArgs()[1], found.getRange());
+ try {
+ found = (FunctionType) found.unify(expected);
+ } catch (UnificationException e) {
+ throw new TypeErrorException(
String.format("Expected %s, found %s at 'Append',%n%s", expected, found, n.getLocation()));
+ }
+ return found;
}
- return found;
- }
- case B_OPCODE_head: { // HEAD(s) - the first element of the sequence
- FunctionType func = new FunctionType(IntType.getInstance(), new UntypedType());
- func = (FunctionType) visitExprOrOpArgNode(n.getArgs()[0], func);
+ case B_OPCODE_head: { // HEAD(s) - the first element of the sequence
+ FunctionType func = new FunctionType(IntType.getInstance(), new UntypedType());
+ func = (FunctionType) visitExprOrOpArgNode(n.getArgs()[0], func);
- TLAType found = func.getRange();
- try {
- found = found.unify(expected);
- } catch (UnificationException e) {
- throw new TypeErrorException(
+ TLAType found = func.getRange();
+ try {
+ found = found.unify(expected);
+ } catch (UnificationException e) {
+ throw new TypeErrorException(
String.format("Expected %s, found %s at 'Head',%n%s", expected, found, n.getLocation()));
+ }
+ return found;
}
- return found;
- }
- case B_OPCODE_tail: { // Tail(s)
- FunctionType found = new FunctionType(IntType.getInstance(), new UntypedType());
- found = (FunctionType) visitExprOrOpArgNode(n.getArgs()[0], found);
- try {
- found = (FunctionType) found.unify(expected);
- } catch (UnificationException e) {
- throw new TypeErrorException(
+ case B_OPCODE_tail: { // Tail(s)
+ FunctionType found = new FunctionType(IntType.getInstance(), new UntypedType());
+ found = (FunctionType) visitExprOrOpArgNode(n.getArgs()[0], found);
+ try {
+ found = (FunctionType) found.unify(expected);
+ } catch (UnificationException e) {
+ throw new TypeErrorException(
String.format("Expected %s, found %s at 'Tail',%n%s", expected, found, n.getLocation()));
+ }
+ return found;
}
- return found;
- }
- case B_OPCODE_subseq: { // SubSeq(s,m,n)
- TLAType found = new FunctionType(IntType.getInstance(), new UntypedType());
- found = visitExprOrOpArgNode(n.getArgs()[0], found);
- visitExprOrOpArgNode(n.getArgs()[1], IntType.getInstance());
- visitExprOrOpArgNode(n.getArgs()[2], IntType.getInstance());
- try {
- found = found.unify(expected);
- } catch (UnificationException e) {
- throw new TypeErrorException(
+ case B_OPCODE_subseq: { // SubSeq(s,m,n)
+ TLAType found = new FunctionType(IntType.getInstance(), new UntypedType());
+ found = visitExprOrOpArgNode(n.getArgs()[0], found);
+ visitExprOrOpArgNode(n.getArgs()[1], IntType.getInstance());
+ visitExprOrOpArgNode(n.getArgs()[2], IntType.getInstance());
+ try {
+ found = found.unify(expected);
+ } catch (UnificationException e) {
+ throw new TypeErrorException(
String.format("Expected %s, found %s at 'SubSeq',%n%s", expected, found, n.getLocation()));
+ }
+ return found;
}
- return found;
- }
- // TODO add BSeq to tla standard modules
-
- /*
- * Standard Module TLA2B
- */
-
- case B_OPCODE_min: // MinOfSet(S)
- case B_OPCODE_max: // MaxOfSet(S)
- case B_OPCODE_setprod: // SetProduct(S)
- case B_OPCODE_setsum: // SetSummation(S)
- {
- try {
- IntType.getInstance().unify(expected);
- } catch (UnificationException e) {
- throw new TypeErrorException(String.format("Expected %s, found INTEGER at '%s',%n%s", expected,
+ // TODO add BSeq to tla standard modules
+
+ /*
+ * Standard Module TLA2B
+ */
+
+ case B_OPCODE_min: // MinOfSet(S)
+ case B_OPCODE_max: // MaxOfSet(S)
+ case B_OPCODE_setprod: // SetProduct(S)
+ case B_OPCODE_setsum: // SetSummation(S)
+ {
+ try {
+ IntType.getInstance().unify(expected);
+ } catch (UnificationException e) {
+ throw new TypeErrorException(String.format("Expected %s, found INTEGER at '%s',%n%s", expected,
n.getOperator().getName(), n.getLocation()));
+ }
+ visitExprOrOpArgNode(n.getArgs()[0], new SetType(IntType.getInstance()));
+ return IntType.getInstance();
}
- visitExprOrOpArgNode(n.getArgs()[0], new SetType(IntType.getInstance()));
- return IntType.getInstance();
- }
- case B_OPCODE_permseq: { // PermutedSequences(S)
- SetType argType = (SetType) visitExprOrOpArgNode(n.getArgs()[0], new SetType(new UntypedType()));
- SetType found = new SetType(new FunctionType(IntType.getInstance(), argType.getSubType()));
- try {
- found = found.unify(expected);
- } catch (UnificationException e) {
- throw new TypeErrorException(String.format("Expected %s, found %s at 'PermutedSequences',%n%s",
+ case B_OPCODE_permseq: { // PermutedSequences(S)
+ SetType argType = (SetType) visitExprOrOpArgNode(n.getArgs()[0], new SetType(new UntypedType()));
+ SetType found = new SetType(new FunctionType(IntType.getInstance(), argType.getSubType()));
+ try {
+ found = found.unify(expected);
+ } catch (UnificationException e) {
+ throw new TypeErrorException(String.format("Expected %s, found %s at 'PermutedSequences',%n%s",
expected, found, n.getLocation()));
+ }
+ return found;
}
- return found;
- }
- /*
- * Standard Module TLA2B
- */
- case B_OPCODE_pow1: // POW1
- {
-
- SetType set = new SetType(new UntypedType());
- set = (SetType) visitExprOrOpArgNode(n.getArgs()[0], set);
- SetType found = new SetType(set);
- try {
- found = found.unify(expected);
- } catch (UnificationException e) {
- throw new TypeErrorException(String.format("Expected %s, found %s at '%s',%n%s", expected, found,
+ /*
+ * Standard Module TLA2B
+ */
+ case B_OPCODE_pow1: // POW1
+ {
+
+ SetType set = new SetType(new UntypedType());
+ set = (SetType) visitExprOrOpArgNode(n.getArgs()[0], set);
+ SetType found = new SetType(set);
+ try {
+ found = found.unify(expected);
+ } catch (UnificationException e) {
+ throw new TypeErrorException(String.format("Expected %s, found %s at '%s',%n%s", expected, found,
n.getOperator().getName(), n.getLocation()));
+ }
+ return found;
}
- return found;
- }
- /*
- * Standard Module Relations
- */
- case B_OPCODE_rel_inverse: // POW1
- {
- SetType set = new SetType(new TupleType(2));
- set = (SetType) visitExprOrOpArgNode(n.getArgs()[0], set);
- TupleType t = (TupleType) set.getSubType();
- ArrayList<TLAType> list = new ArrayList<>();
- list.add(t.getTypes().get(1));
- list.add(t.getTypes().get(0));
- SetType found = new SetType(new TupleType(list));
- try {
- found = found.unify(expected);
- } catch (UnificationException e) {
- throw new TypeErrorException(String.format("Expected %s, found %s at '%s',%n%s", expected, found,
+ /*
+ * Standard Module Relations
+ */
+ case B_OPCODE_rel_inverse: // POW1
+ {
+ SetType set = new SetType(new TupleType(2));
+ set = (SetType) visitExprOrOpArgNode(n.getArgs()[0], set);
+ TupleType t = (TupleType) set.getSubType();
+ ArrayList<TLAType> list = new ArrayList<>();
+ list.add(t.getTypes().get(1));
+ list.add(t.getTypes().get(0));
+ SetType found = new SetType(new TupleType(list));
+ try {
+ found = found.unify(expected);
+ } catch (UnificationException e) {
+ throw new TypeErrorException(String.format("Expected %s, found %s at '%s',%n%s", expected, found,
n.getOperator().getName(), n.getLocation()));
+ }
+ return found;
}
- return found;
- }
- /*
- * TLA+ Built-Ins, but not in tlc.tool.BuiltInOPs
- */
- case B_OPCODE_bool: // BOOLEAN
- try {
- SetType found = new SetType(BoolType.getInstance());
- found = found.unify(expected);
- return found;
- } catch (UnificationException e) {
- throw new TypeErrorException(
+ /*
+ * TLA+ Built-Ins, but not in tlc.tool.BuiltInOPs
+ */
+ case B_OPCODE_bool: // BOOLEAN
+ try {
+ SetType found = new SetType(BoolType.getInstance());
+ found = found.unify(expected);
+ return found;
+ } catch (UnificationException e) {
+ throw new TypeErrorException(
String.format("Expected %s, found POW(BOOL) at 'BOOLEAN',%n%s", expected, n.getLocation()));
- }
+ }
- case B_OPCODE_string: // STRING
- try {
- SetType found = new SetType(StringType.getInstance());
- found = found.unify(expected);
- return found;
- } catch (UnificationException e) {
- throw new TypeErrorException(
+ case B_OPCODE_string: // STRING
+ try {
+ SetType found = new SetType(StringType.getInstance());
+ found = found.unify(expected);
+ return found;
+ } catch (UnificationException e) {
+ throw new TypeErrorException(
String.format("Expected %s, found POW(STRING) at 'STRING',%n%s", expected, n.getLocation()));
- }
+ }
- case B_OPCODE_true:
- case B_OPCODE_false:
- try {
- BoolType.getInstance().unify(expected);
- return BoolType.getInstance();
- } catch (Exception e) {
- throw new TypeErrorException(String.format("Expected %s, found BOOL at '%s',%n%s", expected,
+ case B_OPCODE_true:
+ case B_OPCODE_false:
+ try {
+ BoolType.getInstance().unify(expected);
+ return BoolType.getInstance();
+ } catch (Exception e) {
+ throw new TypeErrorException(String.format("Expected %s, found BOOL at '%s',%n%s", expected,
n.getOperator().getName(), n.getLocation()));
- }
+ }
- case B_OPCODE_assert: {
- try {
- BoolType.getInstance().unify(expected);
- return BoolType.getInstance();
- } catch (Exception e) {
- throw new TypeErrorException(String.format("Expected %s, found BOOL at '%s',%n%s", expected,
+ case B_OPCODE_assert: {
+ try {
+ BoolType.getInstance().unify(expected);
+ return BoolType.getInstance();
+ } catch (Exception e) {
+ throw new TypeErrorException(String.format("Expected %s, found BOOL at '%s',%n%s", expected,
n.getOperator().getName(), n.getLocation()));
+ }
}
- }
- default: {
- throw new NotImplementedException(n.getOperator().getName().toString());
- }
+ default: {
+ throw new NotImplementedException(n.getOperator().getName().toString());
+ }
}
}
}
diff --git a/src/main/java/de/tla2b/analysis/UsedExternalFunctions.java b/src/main/java/de/tla2b/analysis/UsedExternalFunctions.java
index 8d31a3b..af6bb2e 100644
--- a/src/main/java/de/tla2b/analysis/UsedExternalFunctions.java
+++ b/src/main/java/de/tla2b/analysis/UsedExternalFunctions.java
@@ -1,17 +1,13 @@
package de.tla2b.analysis;
-import java.util.HashSet;
-import java.util.Set;
-
import de.tla2b.global.BBuildIns;
import de.tla2b.global.BBuiltInOPs;
-import tla2sany.semantic.ExprNode;
-import tla2sany.semantic.ExprOrOpArgNode;
-import tla2sany.semantic.ModuleNode;
-import tla2sany.semantic.OpApplNode;
-import tla2sany.semantic.OpDefNode;
+import tla2sany.semantic.*;
+
+import java.util.HashSet;
+import java.util.Set;
-public class UsedExternalFunctions extends AbstractASTVisitor implements BBuildIns{
+public class UsedExternalFunctions extends AbstractASTVisitor implements BBuildIns {
public enum EXTERNAL_FUNCTIONS {
CHOOSE, ASSERT
@@ -24,7 +20,7 @@ public class UsedExternalFunctions extends AbstractASTVisitor implements BBuildI
}
public UsedExternalFunctions(ModuleNode moduleNode,
- SpecAnalyser specAnalyser) {
+ SpecAnalyser specAnalyser) {
usedExternalFunctions = new HashSet<>();
visitAssumptions(moduleNode.getAssumptions());
@@ -38,12 +34,12 @@ public class UsedExternalFunctions extends AbstractASTVisitor implements BBuildI
@Override
public void visitBuiltInNode(OpApplNode n) {
switch (getOpCode(n.getOperator().getName())) {
- case OPCODE_case:
- case OPCODE_uc:
- case OPCODE_bc: {
- usedExternalFunctions.add(EXTERNAL_FUNCTIONS.CHOOSE);
- }
- default:
+ case OPCODE_case:
+ case OPCODE_uc:
+ case OPCODE_bc: {
+ usedExternalFunctions.add(EXTERNAL_FUNCTIONS.CHOOSE);
+ }
+ default:
}
ExprNode[] in = n.getBdedQuantBounds();
@@ -59,14 +55,14 @@ public class UsedExternalFunctions extends AbstractASTVisitor implements BBuildI
}
}
}
-
+
@Override
public void visitBBuiltinsNode(OpApplNode n) {
if (BBuiltInOPs.getOpcode(n.getOperator().getName()) == B_OPCODE_assert) {
usedExternalFunctions.add(EXTERNAL_FUNCTIONS.ASSERT);
}
-
-
+
+
ExprNode[] in = n.getBdedQuantBounds();
for (ExprNode exprNode : in) {
visitExprNode(exprNode);
diff --git a/src/main/java/de/tla2b/config/ConfigfileEvaluator.java b/src/main/java/de/tla2b/config/ConfigfileEvaluator.java
index c01d402..ab7bce5 100644
--- a/src/main/java/de/tla2b/config/ConfigfileEvaluator.java
+++ b/src/main/java/de/tla2b/config/ConfigfileEvaluator.java
@@ -1,20 +1,9 @@
package de.tla2b.config;
-import java.util.ArrayList;
-import java.util.Enumeration;
-import java.util.HashSet;
-import java.util.Hashtable;
-import java.util.LinkedHashMap;
-import java.util.Map;
-
import de.tla2b.exceptions.ConfigFileErrorException;
import de.tla2b.exceptions.UnificationException;
import de.tla2b.types.*;
-import tla2sany.semantic.InstanceNode;
-import tla2sany.semantic.ModuleNode;
-import tla2sany.semantic.OpDeclNode;
-import tla2sany.semantic.OpDefNode;
-import tla2sany.semantic.OpDefOrDeclNode;
+import tla2sany.semantic.*;
import tlc2.tool.ModelConfig;
import tlc2.util.Vect;
import tlc2.value.IntValue;
@@ -22,6 +11,8 @@ import tlc2.value.ModelValue;
import tlc2.value.SetEnumValue;
import tlc2.value.Value;
+import java.util.*;
+
/**
* This class evaluates the configfile and collects all necessary information of
* the configfile. All used identifier in the configfile are checked to be valid
@@ -106,10 +97,10 @@ public class ConfigfileEvaluator {
evalSpec(); // check if SPECIFICATION declaration is a valid definition
if (moduleNode.getVariableDecls().length > 0 && this.initNode == null
- && this.specNode == null) {
+ && this.specNode == null) {
throw new ConfigFileErrorException(
- "The module contains variables."
- + " Hence there must be either a SPECIFICATION or INIT declaration.");
+ "The module contains variables."
+ + " Hence there must be either a SPECIFICATION or INIT declaration.");
}
evalInvariants();
@@ -133,9 +124,9 @@ public class ConfigfileEvaluator {
this.nextNode = definitions.get(next);
} else {
throw new ConfigFileErrorException(
- "Invalid declaration of the next state predicate."
- + " Module does not contain the defintion '"
- + next + "'");
+ "Invalid declaration of the next state predicate."
+ + " Module does not contain the defintion '"
+ + next + "'");
}
} else
next = null;
@@ -149,9 +140,9 @@ public class ConfigfileEvaluator {
this.initNode = definitions.get(init);
} else {
throw new ConfigFileErrorException(
- "Invalid declaration of the initialisation predicate."
- + " Module does not contain the defintion '"
- + init + "'");
+ "Invalid declaration of the initialisation predicate."
+ + " Module does not contain the defintion '"
+ + init + "'");
}
} else {
init = null;
@@ -166,9 +157,9 @@ public class ConfigfileEvaluator {
this.specNode = definitions.get(spec);
} else {
throw new ConfigFileErrorException(
- "Invalid declaration of the specification predicate."
- + "Module does not contain the defintion '"
- + spec + "'");
+ "Invalid declaration of the specification predicate."
+ + "Module does not contain the defintion '"
+ + spec + "'");
}
} else
spec = null;
@@ -183,8 +174,8 @@ public class ConfigfileEvaluator {
String inv = (String) v.elementAt(i);
if (!definitions.containsKey(inv)) {
throw new ConfigFileErrorException(
- "Invalid invariant declaration. Module does not contain definition '"
- + inv + "'");
+ "Invalid invariant declaration. Module does not contain definition '"
+ + inv + "'");
}
invariantNodeList.add(definitions.get(inv));
}
@@ -247,7 +238,7 @@ public class ConfigfileEvaluator {
}
private void evalConstantOrOperatorAssignments()
- throws ConfigFileErrorException {
+ throws ConfigFileErrorException {
Vect configCons = configAst.getConstants();
// iterate over all constant or operator assignments in the config file
// k = 1 or def = 1
@@ -267,7 +258,7 @@ public class ConfigfileEvaluator {
* in the resulting B machine disappears
**/
if (symbolType instanceof EnumType
- && symbolName.equals(symbolValue.toString())) {
+ && symbolName.equals(symbolValue.toString())) {
bConstantList.remove(c);
}
} else if (definitions.containsKey(symbolName)) {
@@ -288,7 +279,7 @@ public class ConfigfileEvaluator {
// appear in the TLA+
// module
throw new ConfigFileErrorException(
- "Module does not contain the symbol: " + symbolName);
+ "Module does not contain the symbol: " + symbolName);
}
}
@@ -306,7 +297,7 @@ public class ConfigfileEvaluator {
for (int i = 0; i < assignments.size(); i++) {
Vect assigment = (Vect) assignments.elementAt(i);
OpDefOrDeclNode opDefOrDeclNode = searchDefinitionOrConstant(
- mNode, (String) assigment.elementAt(0));
+ mNode, (String) assigment.elementAt(0));
String symbolName = opDefOrDeclNode.getName().toString();
Value symbolValue = (Value) assigment.elementAt(1);
TLAType symbolType = conGetType(assigment.elementAt(1));
@@ -349,7 +340,7 @@ public class ConfigfileEvaluator {
// foo <- [Counter] bar or k <- [Counter] bar
@SuppressWarnings("unchecked")
Hashtable<String, Hashtable<String, String>> configCons = configAst
- .getModOverrides();
+ .getModOverrides();
Enumeration<String> moduleNames = configCons.keys();
while (moduleNames.hasMoreElements()) {
String moduleName = moduleNames.nextElement();
@@ -416,7 +407,7 @@ public class ConfigfileEvaluator {
}
public ModuleNode searchModule(String moduleName)
- throws ConfigFileErrorException {
+ throws ConfigFileErrorException {
/*
* Search module in extended modules
*/
@@ -446,13 +437,13 @@ public class ConfigfileEvaluator {
}
}
throw new ConfigFileErrorException(
- String.format(
- "Module '%s' is not included in the specification.",
- moduleName));
+ String.format(
+ "Module '%s' is not included in the specification.",
+ moduleName));
}
public OpDefOrDeclNode searchDefinitionOrConstant(ModuleNode n,
- String defOrConName) throws ConfigFileErrorException {
+ String defOrConName) throws ConfigFileErrorException {
for (int i = 0; i < n.getOpDefs().length; i++) {
if (n.getOpDefs()[i].getName().toString().equals(defOrConName)) {
return n.getOpDefs()[i];
@@ -460,12 +451,12 @@ public class ConfigfileEvaluator {
}
for (int i = 0; i < n.getConstantDecls().length; i++) {
if (n.getConstantDecls()[i].getName().toString()
- .equals(defOrConName)) {
+ .equals(defOrConName)) {
return n.getConstantDecls()[i];
}
}
throw new ConfigFileErrorException(
- "Module does not contain the symbol: " + defOrConName);
+ "Module does not contain the symbol: " + defOrConName);
}
private TLAType conGetType(Object o) throws ConfigFileErrorException {
@@ -478,16 +469,16 @@ public class ConfigfileEvaluator {
SetType t = new SetType(new UntypedType());
if (set.isEmpty()) {
throw new ConfigFileErrorException(
- "empty set is not permitted!");
+ "empty set is not permitted!");
}
TLAType elemType;
if (set.elems.elementAt(0).getClass().getName()
- .equals("tlc2.value.ModelValue")) {
+ .equals("tlc2.value.ModelValue")) {
EnumType e = new EnumType(new ArrayList<>());
for (int i = 0; i < set.size(); i++) {
if (set.elems.elementAt(i).getClass().getName()
- .equals("tlc2.value.ModelValue")) {
+ .equals("tlc2.value.ModelValue")) {
String mv = set.elems.elementAt(i).toString();
if (!enumeratedSet.contains(mv)) {
enumeratedSet.add(mv);
@@ -503,8 +494,8 @@ public class ConfigfileEvaluator {
} else {
throw new ConfigFileErrorException(
- "Elements of the set must have the same type: "
- + o);
+ "Elements of the set must have the same type: "
+ + o);
}
}
for (String s : e.modelvalues) {
@@ -518,8 +509,8 @@ public class ConfigfileEvaluator {
// all Elements have the same Type?
if (!t.getSubType().compare(elemType)) {
throw new ConfigFileErrorException(
- "Elements of the set must have the same type: "
- + o);
+ "Elements of the set must have the same type: "
+ + o);
}
}
}
@@ -545,7 +536,7 @@ public class ConfigfileEvaluator {
return BoolType.getInstance();
} else {
throw new ConfigFileErrorException("Unkown ConstantType: " + o
- + " " + o.getClass());
+ + " " + o.getClass());
}
}
diff --git a/src/main/java/de/tla2b/config/ModuleOverrider.java b/src/main/java/de/tla2b/config/ModuleOverrider.java
index 6a52605..f6c4080 100644
--- a/src/main/java/de/tla2b/config/ModuleOverrider.java
+++ b/src/main/java/de/tla2b/config/ModuleOverrider.java
@@ -1,20 +1,10 @@
package de.tla2b.config;
-import java.util.Hashtable;
-
-import tla2sany.semantic.ASTConstants;
-import tla2sany.semantic.AbortException;
-import tla2sany.semantic.AssumeNode;
-import tla2sany.semantic.ExprNode;
-import tla2sany.semantic.ExprOrOpArgNode;
-import tla2sany.semantic.LetInNode;
-import tla2sany.semantic.ModuleNode;
-import tla2sany.semantic.OpApplNode;
-import tla2sany.semantic.OpDeclNode;
-import tla2sany.semantic.OpDefNode;
-import tla2sany.semantic.SymbolNode;
+import tla2sany.semantic.*;
import tlc2.tool.BuiltInOPs;
+import java.util.Hashtable;
+
public class ModuleOverrider extends BuiltInOPs implements ASTConstants {
private final ModuleNode moduleNode;
@@ -23,9 +13,9 @@ public class ModuleOverrider extends BuiltInOPs implements ASTConstants {
private final Hashtable<OpDefNode, ValueObj> operatorAssignments;
public ModuleOverrider(ModuleNode moduleNode,
- Hashtable<OpDeclNode, OpDefNode> constantOverrideTable,
- Hashtable<OpDefNode, OpDefNode> operatorOverrideTable,
- Hashtable<OpDefNode, ValueObj> operatorAssignments) {
+ Hashtable<OpDeclNode, OpDefNode> constantOverrideTable,
+ Hashtable<OpDefNode, OpDefNode> operatorOverrideTable,
+ Hashtable<OpDefNode, ValueObj> operatorAssignments) {
this.moduleNode = moduleNode;
this.constantOverrideTable = constantOverrideTable;
this.operatorOverrideTable = operatorOverrideTable;
@@ -81,7 +71,7 @@ public class ModuleOverrider extends BuiltInOPs implements ASTConstants {
if (res != null) {
AssumeNode newAssume = new AssumeNode(assume.stn, res, null,
- null);
+ null);
assumes[i] = newAssume;
}
}
@@ -99,28 +89,28 @@ public class ModuleOverrider extends BuiltInOPs implements ASTConstants {
private OpApplNode visitExprNode(ExprNode n) {
switch (n.getKind()) {
- case OpApplKind:
- return visitOpApplNode((OpApplNode) n);
-
- case StringKind:
- case AtNodeKind: // @
- case NumeralKind:
- case DecimalKind: {
- return null;
- }
-
- case LetInKind: {
- LetInNode l = (LetInNode) n;
- for (int i = 0; i < l.getLets().length; i++) {
- visitExprNode(l.getLets()[i].getBody());
+ case OpApplKind:
+ return visitOpApplNode((OpApplNode) n);
+
+ case StringKind:
+ case AtNodeKind: // @
+ case NumeralKind:
+ case DecimalKind: {
+ return null;
}
- OpApplNode res = visitExprNode(l.getBody());
- if (res != null) {
- throw new RuntimeException();
+ case LetInKind: {
+ LetInNode l = (LetInNode) n;
+ for (int i = 0; i < l.getLets().length; i++) {
+ visitExprNode(l.getLets()[i].getBody());
+ }
+
+ OpApplNode res = visitExprNode(l.getBody());
+ if (res != null) {
+ throw new RuntimeException();
+ }
+ return null;
}
- return null;
- }
}
return null;
}
@@ -128,84 +118,84 @@ public class ModuleOverrider extends BuiltInOPs implements ASTConstants {
private OpApplNode visitOpApplNode(OpApplNode n) {
SymbolNode s = n.getOperator();
switch (s.getKind()) {
- case ConstantDeclKind: {
- if (constantOverrideTable.containsKey(s) && s.getArity() > 0) {
- SymbolNode newOperator = constantOverrideTable.get(s);
- OpApplNode newNode = null;
- try {
- newNode = new OpApplNode(newOperator, n.getArgs(),
+ case ConstantDeclKind: {
+ if (constantOverrideTable.containsKey(s) && s.getArity() > 0) {
+ SymbolNode newOperator = constantOverrideTable.get(s);
+ OpApplNode newNode = null;
+ try {
+ newNode = new OpApplNode(newOperator, n.getArgs(),
n.getTreeNode(), null);
- } catch (AbortException e) {
- throw new RuntimeException();
- }
- for (int i = 0; i < n.getArgs().length; i++) {
- if (n.getArgs()[i] != null) {
- OpApplNode res = visitExprOrOpArgNode(n.getArgs()[i]);
- if (res != null) {
- n.getArgs()[i] = res;
+ } catch (AbortException e) {
+ throw new RuntimeException();
+ }
+ for (int i = 0; i < n.getArgs().length; i++) {
+ if (n.getArgs()[i] != null) {
+ OpApplNode res = visitExprOrOpArgNode(n.getArgs()[i]);
+ if (res != null) {
+ n.getArgs()[i] = res;
+ }
}
}
+ // n.setOperator(constantOverrideTable.get(s));
+ return newNode;
}
- // n.setOperator(constantOverrideTable.get(s));
- return newNode;
- }
- break;
+ break;
- }
- case FormalParamKind: // Params are not global in the module
- case VariableDeclKind: // TODO try to override variable
- break;
+ }
+ case FormalParamKind: // Params are not global in the module
+ case VariableDeclKind: // TODO try to override variable
+ break;
- case BuiltInKind:// Buildin operator can not be overridden by in the
- // configuration file
- ExprNode[] ins = n.getBdedQuantBounds();
- if (ins != null) {
- for (int i = 0; i < ins.length; i++) {
+ case BuiltInKind:// Buildin operator can not be overridden by in the
+ // configuration file
+ ExprNode[] ins = n.getBdedQuantBounds();
+ if (ins != null) {
+ for (int i = 0; i < ins.length; i++) {
- OpApplNode res = visitExprOrOpArgNode(ins[i]);
- if (res != null) {
- ins[i] = res;
+ OpApplNode res = visitExprOrOpArgNode(ins[i]);
+ if (res != null) {
+ ins[i] = res;
+ }
}
}
- }
-
- break;
- case UserDefinedOpKind: {
- OpDefNode operator = (OpDefNode) n.getOperator();
- if (!operatorOverrideTable.containsKey(operator.getSource())
- && !operatorOverrideTable.containsKey(operator))
break;
- SymbolNode newOperator = null;
- // IF there are two override statements in the configuration file
- //(a: Add <- (Rule) Add2, b: R1!Add <- Add3)
- // TLC uses variant a) overriding the source definition
- if (operatorOverrideTable.containsKey(operator.getSource())) {
- newOperator = operatorOverrideTable.get(operator.getSource());
- } else {
- newOperator = operatorOverrideTable.get(operator);
- }
- OpApplNode newNode = null;
- OpDefNode def = (OpDefNode) n.getOperator();
- try {
- newNode = new OpApplNode(newOperator, n.getArgs(),
+ case UserDefinedOpKind: {
+ OpDefNode operator = (OpDefNode) n.getOperator();
+ if (!operatorOverrideTable.containsKey(operator.getSource())
+ && !operatorOverrideTable.containsKey(operator))
+ break;
+
+ SymbolNode newOperator = null;
+ // IF there are two override statements in the configuration file
+ //(a: Add <- (Rule) Add2, b: R1!Add <- Add3)
+ // TLC uses variant a) overriding the source definition
+ if (operatorOverrideTable.containsKey(operator.getSource())) {
+ newOperator = operatorOverrideTable.get(operator.getSource());
+ } else {
+ newOperator = operatorOverrideTable.get(operator);
+ }
+ OpApplNode newNode = null;
+ OpDefNode def = (OpDefNode) n.getOperator();
+ try {
+ newNode = new OpApplNode(newOperator, n.getArgs(),
n.getTreeNode(), def.getOriginallyDefinedInModuleNode());
- } catch (AbortException e) {
- e.printStackTrace();
- }
- for (int i = 0; i < n.getArgs().length; i++) {
- if (n.getArgs()[i] != null) {
- OpApplNode res = visitExprOrOpArgNode(n.getArgs()[i]);
- if (res != null) {
- n.getArgs()[i] = res;
- }
+ } catch (AbortException e) {
+ e.printStackTrace();
}
+ for (int i = 0; i < n.getArgs().length; i++) {
+ if (n.getArgs()[i] != null) {
+ OpApplNode res = visitExprOrOpArgNode(n.getArgs()[i]);
+ if (res != null) {
+ n.getArgs()[i] = res;
+ }
+ }
+ }
+ // n.setOperator(constantOverrideTable.get(s));
+ return newNode;
}
- // n.setOperator(constantOverrideTable.get(s));
- return newNode;
- }
}
for (int i = 0; i < n.getArgs().length; i++) {
diff --git a/src/main/java/de/tla2b/config/TLCValueNode.java b/src/main/java/de/tla2b/config/TLCValueNode.java
index 45e0686..e5cc7a6 100644
--- a/src/main/java/de/tla2b/config/TLCValueNode.java
+++ b/src/main/java/de/tla2b/config/TLCValueNode.java
@@ -20,8 +20,8 @@ public class TLCValueNode extends NumeralNode implements TranslationGlobals {
public String toString2() {
return "\n*TLCValueNode: Value: '"
- + value.toString() + "'";
-
+ + value.toString() + "'";
+
}
public TLAType getType() {
diff --git a/src/main/java/de/tla2b/config/ValueObj.java b/src/main/java/de/tla2b/config/ValueObj.java
index e239c56..b4f2605 100644
--- a/src/main/java/de/tla2b/config/ValueObj.java
+++ b/src/main/java/de/tla2b/config/ValueObj.java
@@ -23,9 +23,9 @@ public class ValueObj {
public void setType(TLAType type) {
this.type = type;
}
-
- public TLAType getType(){
+
+ public TLAType getType() {
return type;
}
-
+
}
diff --git a/src/main/java/de/tla2b/exceptions/ConfigFileErrorException.java b/src/main/java/de/tla2b/exceptions/ConfigFileErrorException.java
index bbe66b1..dc55f68 100644
--- a/src/main/java/de/tla2b/exceptions/ConfigFileErrorException.java
+++ b/src/main/java/de/tla2b/exceptions/ConfigFileErrorException.java
@@ -2,7 +2,7 @@ package de.tla2b.exceptions;
@SuppressWarnings("serial")
-public class ConfigFileErrorException extends TLA2BException{
+public class ConfigFileErrorException extends TLA2BException {
public ConfigFileErrorException(String s) {
super(s);
diff --git a/src/main/java/de/tla2b/exceptions/FrontEndException.java b/src/main/java/de/tla2b/exceptions/FrontEndException.java
index 9d6f9ed..e2588b9 100644
--- a/src/main/java/de/tla2b/exceptions/FrontEndException.java
+++ b/src/main/java/de/tla2b/exceptions/FrontEndException.java
@@ -3,10 +3,11 @@ package de.tla2b.exceptions;
import tla2sany.modanalyzer.SpecObj;
@SuppressWarnings("serial")
-public class FrontEndException extends TLA2BException{
+public class FrontEndException extends TLA2BException {
public SpecObj spec;
- public FrontEndException(String e){
+
+ public FrontEndException(String e) {
super(e);
}
diff --git a/src/main/java/de/tla2b/exceptions/ModuleErrorException.java b/src/main/java/de/tla2b/exceptions/ModuleErrorException.java
index 07c8da5..7e8be40 100644
--- a/src/main/java/de/tla2b/exceptions/ModuleErrorException.java
+++ b/src/main/java/de/tla2b/exceptions/ModuleErrorException.java
@@ -2,8 +2,8 @@ package de.tla2b.exceptions;
@SuppressWarnings("serial")
-public class ModuleErrorException extends TLA2BException{
- public ModuleErrorException(String e){
+public class ModuleErrorException extends TLA2BException {
+ public ModuleErrorException(String e) {
super(e);
}
diff --git a/src/main/java/de/tla2b/exceptions/NotImplementedException.java b/src/main/java/de/tla2b/exceptions/NotImplementedException.java
index 7d1367c..1ef2526 100644
--- a/src/main/java/de/tla2b/exceptions/NotImplementedException.java
+++ b/src/main/java/de/tla2b/exceptions/NotImplementedException.java
@@ -3,7 +3,7 @@ package de.tla2b.exceptions;
@SuppressWarnings("serial")
public class NotImplementedException extends RuntimeException {
- public NotImplementedException(String e){
+ public NotImplementedException(String e) {
super(e);
}
diff --git a/src/main/java/de/tla2b/exceptions/SemanticErrorException.java b/src/main/java/de/tla2b/exceptions/SemanticErrorException.java
index 72c3f61..169718d 100644
--- a/src/main/java/de/tla2b/exceptions/SemanticErrorException.java
+++ b/src/main/java/de/tla2b/exceptions/SemanticErrorException.java
@@ -2,8 +2,8 @@ package de.tla2b.exceptions;
@SuppressWarnings("serial")
public class SemanticErrorException extends TLA2BException {
-
- public SemanticErrorException(String e){
+
+ public SemanticErrorException(String e) {
super(e);
}
diff --git a/src/main/java/de/tla2b/exceptions/TLA2BException.java b/src/main/java/de/tla2b/exceptions/TLA2BException.java
index c86ebf7..42148cc 100644
--- a/src/main/java/de/tla2b/exceptions/TLA2BException.java
+++ b/src/main/java/de/tla2b/exceptions/TLA2BException.java
@@ -1,9 +1,9 @@
package de.tla2b.exceptions;
@SuppressWarnings("serial")
-public abstract class TLA2BException extends Exception{
+public abstract class TLA2BException extends Exception {
- public TLA2BException(String e){
+ public TLA2BException(String e) {
super(e);
}
}
diff --git a/src/main/java/de/tla2b/exceptions/TLA2BIOException.java b/src/main/java/de/tla2b/exceptions/TLA2BIOException.java
index 15595fa..583859d 100644
--- a/src/main/java/de/tla2b/exceptions/TLA2BIOException.java
+++ b/src/main/java/de/tla2b/exceptions/TLA2BIOException.java
@@ -3,8 +3,8 @@ package de.tla2b.exceptions;
@SuppressWarnings("serial")
public class TLA2BIOException extends TLA2BException {
-
- public TLA2BIOException(String e){
+
+ public TLA2BIOException(String e) {
super(e);
}
}
diff --git a/src/main/java/de/tla2b/exceptions/UnificationException.java b/src/main/java/de/tla2b/exceptions/UnificationException.java
index 1bd35e7..74b01bf 100644
--- a/src/main/java/de/tla2b/exceptions/UnificationException.java
+++ b/src/main/java/de/tla2b/exceptions/UnificationException.java
@@ -1,6 +1,7 @@
package de.tla2b.exceptions;
+
@SuppressWarnings("serial")
-public class UnificationException extends TLA2BException{
+public class UnificationException extends TLA2BException {
public UnificationException() {
super(null);
diff --git a/src/main/java/de/tla2b/global/BBuildIns.java b/src/main/java/de/tla2b/global/BBuildIns.java
index a36e425..f9252a4 100644
--- a/src/main/java/de/tla2b/global/BBuildIns.java
+++ b/src/main/java/de/tla2b/global/BBuildIns.java
@@ -4,91 +4,91 @@ import util.UniqueString;
public interface BBuildIns {
UniqueString OP_dotdot = UniqueString
- .uniqueStringOf("..");
+ .uniqueStringOf("..");
UniqueString OP_plus = UniqueString.uniqueStringOf("+");
UniqueString OP_minus = UniqueString
- .uniqueStringOf("-");
+ .uniqueStringOf("-");
UniqueString OP_times = UniqueString
- .uniqueStringOf("*");
+ .uniqueStringOf("*");
UniqueString OP_div = UniqueString
- .uniqueStringOf("\\div");
+ .uniqueStringOf("\\div");
UniqueString OP_realdiv = UniqueString
.uniqueStringOf("/");
UniqueString OP_mod = UniqueString.uniqueStringOf("%");
UniqueString OP_exp = UniqueString.uniqueStringOf("^");
UniqueString OP_uminus = UniqueString
- .uniqueStringOf("-.");
+ .uniqueStringOf("-.");
UniqueString OP_lt = UniqueString.uniqueStringOf("<");
UniqueString OP_leq = UniqueString
- .uniqueStringOf("\\leq");
+ .uniqueStringOf("\\leq");
UniqueString OP_gt = UniqueString.uniqueStringOf(">");
UniqueString OP_geq = UniqueString
- .uniqueStringOf("\\geq");
+ .uniqueStringOf("\\geq");
UniqueString OP_nat = UniqueString
- .uniqueStringOf("Nat");
+ .uniqueStringOf("Nat");
UniqueString OP_int = UniqueString
- .uniqueStringOf("Int");
+ .uniqueStringOf("Int");
UniqueString OP_real = UniqueString
- .uniqueStringOf("Real");
+ .uniqueStringOf("Real");
UniqueString OP_bool = UniqueString
- .uniqueStringOf("BOOLEAN");
+ .uniqueStringOf("BOOLEAN");
UniqueString OP_true = UniqueString
- .uniqueStringOf("TRUE");
+ .uniqueStringOf("TRUE");
UniqueString OP_false = UniqueString
- .uniqueStringOf("FALSE");
+ .uniqueStringOf("FALSE");
UniqueString OP_string = UniqueString
- .uniqueStringOf("STRING");
+ .uniqueStringOf("STRING");
// Sets
UniqueString OP_card = UniqueString
- .uniqueStringOf("Cardinality");
+ .uniqueStringOf("Cardinality");
UniqueString OP_finite = UniqueString
- .uniqueStringOf("IsFiniteSet");
+ .uniqueStringOf("IsFiniteSet");
// Sequences
UniqueString OP_len = UniqueString
- .uniqueStringOf("Len");
+ .uniqueStringOf("Len");
UniqueString OP_append = UniqueString
- .uniqueStringOf("Append");
+ .uniqueStringOf("Append");
UniqueString OP_seq = UniqueString
- .uniqueStringOf("Seq");
+ .uniqueStringOf("Seq");
UniqueString OP_head = UniqueString
- .uniqueStringOf("Head");
+ .uniqueStringOf("Head");
UniqueString OP_tail = UniqueString
- .uniqueStringOf("Tail");
+ .uniqueStringOf("Tail");
UniqueString OP_subseq = UniqueString
- .uniqueStringOf("SubSeq");
+ .uniqueStringOf("SubSeq");
UniqueString OP_conc = UniqueString
- .uniqueStringOf("\\o");
-
+ .uniqueStringOf("\\o");
+
//TLA2B
UniqueString OP_min = UniqueString
- .uniqueStringOf("MinOfSet");
+ .uniqueStringOf("MinOfSet");
UniqueString OP_max = UniqueString
- .uniqueStringOf("MaxOfSet");
+ .uniqueStringOf("MaxOfSet");
UniqueString OP_setprod = UniqueString
- .uniqueStringOf("SetProduct");
+ .uniqueStringOf("SetProduct");
UniqueString OP_setsum = UniqueString
- .uniqueStringOf("SetSummation");
+ .uniqueStringOf("SetSummation");
UniqueString OP_permseq = UniqueString
- .uniqueStringOf("PermutedSequences");
+ .uniqueStringOf("PermutedSequences");
//BBuildIns
UniqueString OP_pow1 = UniqueString
- .uniqueStringOf("POW1");
-
-
+ .uniqueStringOf("POW1");
+
+
//Relations
UniqueString OP_rel_inverse = UniqueString
- .uniqueStringOf("rel_inverse");
-
+ .uniqueStringOf("rel_inverse");
+
//TLC
UniqueString OP_assert = UniqueString
- .uniqueStringOf("Assert");
-
+ .uniqueStringOf("Assert");
+
int B_OPCODE_dotdot = 1;
int B_OPCODE_plus = 2;
int B_OPCODE_minus = 3;
@@ -126,12 +126,12 @@ public interface BBuildIns {
int B_OPCODE_setprod = B_OPCODE_conc + 3;
int B_OPCODE_setsum = B_OPCODE_conc + 4;
int B_OPCODE_permseq = B_OPCODE_conc + 5;
-
+
int B_OPCODE_pow1 = B_OPCODE_permseq + 1;
-
-
+
+
int B_OPCODE_rel_inverse = B_OPCODE_pow1 + 1;
-
+
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 abaad12..d82c68f 100644
--- a/src/main/java/de/tla2b/global/BBuiltInOPs.java
+++ b/src/main/java/de/tla2b/global/BBuiltInOPs.java
@@ -1,11 +1,12 @@
package de.tla2b.global;
-import java.util.Hashtable;
-
import util.UniqueString;
-public class BBuiltInOPs implements BBuildIns{
+import java.util.Hashtable;
+
+public class BBuiltInOPs implements BBuildIns {
private static final Hashtable<UniqueString, Integer> B_Opcode_Table;
+
static {
B_Opcode_Table = new Hashtable<>();
B_Opcode_Table.put(OP_dotdot, B_OPCODE_dotdot);
@@ -17,7 +18,7 @@ public class BBuiltInOPs implements BBuildIns{
B_Opcode_Table.put(OP_mod, B_OPCODE_mod);
B_Opcode_Table.put(OP_exp, B_OPCODE_exp);
B_Opcode_Table.put(OP_uminus, B_OPCODE_uminus);
-
+
B_Opcode_Table.put(OP_lt, B_OPCODE_lt);
B_Opcode_Table.put(OP_leq, B_OPCODE_leq);
B_Opcode_Table.put(OP_gt, B_OPCODE_gt);
@@ -29,10 +30,10 @@ public class BBuiltInOPs implements BBuildIns{
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);
B_Opcode_Table.put(OP_card, B_OPCODE_card);
-
+
B_Opcode_Table.put(OP_len, B_OPCODE_len);
B_Opcode_Table.put(OP_append, B_OPCODE_append);
B_Opcode_Table.put(OP_seq, B_OPCODE_seq);
@@ -40,26 +41,26 @@ public class BBuiltInOPs implements BBuildIns{
B_Opcode_Table.put(OP_tail, B_OPCODE_tail);
B_Opcode_Table.put(OP_subseq, B_OPCODE_subseq);
B_Opcode_Table.put(OP_conc, B_OPCODE_conc);
-
+
B_Opcode_Table.put(OP_min, B_OPCODE_min);
B_Opcode_Table.put(OP_max, B_OPCODE_max);
B_Opcode_Table.put(OP_setprod, B_OPCODE_setprod);
B_Opcode_Table.put(OP_setsum, B_OPCODE_setsum);
B_Opcode_Table.put(OP_permseq, B_OPCODE_permseq);
-
+
B_Opcode_Table.put(OP_pow1, B_OPCODE_pow1);
-
+
//relations
B_Opcode_Table.put(OP_rel_inverse, B_OPCODE_rel_inverse);
-
+
B_Opcode_Table.put(OP_assert, B_OPCODE_assert);
}
-
- public static boolean contains(UniqueString s){
+
+ public static boolean contains(UniqueString s) {
return B_Opcode_Table.containsKey(s);
}
-
- public static int getOpcode(UniqueString s){
+
+ public static int getOpcode(UniqueString s) {
return B_Opcode_Table.get(s);
}
}
diff --git a/src/main/java/de/tla2b/global/OperatorTypes.java b/src/main/java/de/tla2b/global/OperatorTypes.java
index e864f01..619a5c0 100644
--- a/src/main/java/de/tla2b/global/OperatorTypes.java
+++ b/src/main/java/de/tla2b/global/OperatorTypes.java
@@ -1,11 +1,13 @@
package de.tla2b.global;
-import java.util.HashSet;
import tlc2.tool.ToolGlobals;
+import java.util.HashSet;
+
public class OperatorTypes implements ToolGlobals, BBuildIns {
private static final HashSet<Integer> TLA_Predicate_Operators;
private static final HashSet<Integer> BBuiltIn_Predicate_Operators;
+
static {
TLA_Predicate_Operators = new HashSet<>();
TLA_Predicate_Operators.add(OPCODE_eq);
diff --git a/src/main/java/de/tla2b/global/Priorities.java b/src/main/java/de/tla2b/global/Priorities.java
index 071f11d..92afc9c 100644
--- a/src/main/java/de/tla2b/global/Priorities.java
+++ b/src/main/java/de/tla2b/global/Priorities.java
@@ -2,75 +2,61 @@ package de.tla2b.global;
public interface Priorities {
int P_max = 300;
-
+
int P_record_acc = 250;
int P_uminus = 210;
int P_exp = 200;
-
+
int P_times = 190;
int P_div = 190;
int P_mod = 190;
-
-
-
+
+
int P_plus = 180;
int P_minus = 180;
int P_setdiff = 180;
-
+
int P_dotdot = 170;
-
+
int P_maplet = 160;
-
+
int P_take_first = 160;
int P_drop_last = 160;
int P_conc = 160;
-
+
int P_intersect = 140;
int P_union = 140;
-
-
+
+
int P_append = 130;
-
+
int P_total_f = 125;
-
+
int P_comma = 115;
-
-
+
int P_rel_overriding = 90;
-
+
int P_in = 60;
int P_notin = 60;
int P_subseteq = 60;
-
+
int P_equals = 50;
int P_noteq = 50;
int P_gt = 50;
int P_lt = 50;
int P_leq = 50;
int P_geq = 50;
-
+
int P_equiv = 60;
-
+
int P_and = 40;
int P_or = 40;
-
+
int P_implies = 30;
-
+
int P_min = 0;
-
-
-
-
-
-
-
-
-
-
-
-
-
-
+
+
}
diff --git a/src/main/java/de/tla2b/global/TranslationGlobals.java b/src/main/java/de/tla2b/global/TranslationGlobals.java
index 9a4ce27..fe94b0e 100644
--- a/src/main/java/de/tla2b/global/TranslationGlobals.java
+++ b/src/main/java/de/tla2b/global/TranslationGlobals.java
@@ -1,10 +1,10 @@
package de.tla2b.global;
+import tla2sany.semantic.FrontEnd;
+
import java.util.ArrayList;
import java.util.Arrays;
-import tla2sany.semantic.FrontEnd;
-
public interface TranslationGlobals {
String VERSION_NUMBER = VersionHelper.VERSION;
@@ -19,7 +19,7 @@ public interface TranslationGlobals {
int EXCEPT_BASE = 6;
int LET_PARAMS_ID = 13;
int NEW_NAME = 20;
-
+
int SUBSTITUTE_PARAM = 29;
int TUPLE = 30;
@@ -27,6 +27,6 @@ public interface TranslationGlobals {
String IF_THEN_ELSE = " IF_THEN_ELSE(P, a, b) == (%t_.(t_ = TRUE & P = TRUE | a )\\/%t_.(t_= TRUE & not(P= TRUE) | b ))(TRUE)";
ArrayList<String> STANDARD_MODULES = new ArrayList<>(
- Arrays.asList("Naturals", "FiniteSets", "Integers", "Reals",
- "Sequences", "TLC", "Relations", "TLA2B", "BBuildIns"));
+ Arrays.asList("Naturals", "FiniteSets", "Integers", "Reals",
+ "Sequences", "TLC", "Relations", "TLA2B", "BBuildIns"));
}
diff --git a/src/main/java/de/tla2b/global/VersionHelper.java b/src/main/java/de/tla2b/global/VersionHelper.java
index 5ff99e4..26459cd 100644
--- a/src/main/java/de/tla2b/global/VersionHelper.java
+++ b/src/main/java/de/tla2b/global/VersionHelper.java
@@ -11,8 +11,9 @@ final class VersionHelper {
private VersionHelper() {
throw new AssertionError("Utility class");
}
-
+
static final String VERSION;
+
static {
final Properties buildProperties = new Properties();
final InputStream is = VersionHelper.class.getResourceAsStream("/de/tla2b/build.properties");
diff --git a/src/main/java/de/tla2b/output/Indentation.java b/src/main/java/de/tla2b/output/Indentation.java
index e2a1e5a..62e61df 100644
--- a/src/main/java/de/tla2b/output/Indentation.java
+++ b/src/main/java/de/tla2b/output/Indentation.java
@@ -1,24 +1,13 @@
package de.tla2b.output;
+import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
+import de.be4.classicalb.core.parser.node.*;
+
import java.util.ArrayList;
import java.util.HashSet;
import java.util.Hashtable;
import java.util.List;
-import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
-import de.be4.classicalb.core.parser.node.AConjunctPredicate;
-import de.be4.classicalb.core.parser.node.AConstantsMachineClause;
-import de.be4.classicalb.core.parser.node.AExistsPredicate;
-import de.be4.classicalb.core.parser.node.AForallPredicate;
-import de.be4.classicalb.core.parser.node.AImplicationPredicate;
-import de.be4.classicalb.core.parser.node.APredicateDefinitionDefinition;
-import de.be4.classicalb.core.parser.node.APropertiesMachineClause;
-import de.be4.classicalb.core.parser.node.ASetsMachineClause;
-import de.be4.classicalb.core.parser.node.Node;
-import de.be4.classicalb.core.parser.node.PExpression;
-import de.be4.classicalb.core.parser.node.PSet;
-import de.be4.classicalb.core.parser.node.Start;
-
public class Indentation extends DepthFirstAdapter {
private final Hashtable<Node, Integer> indentation = new Hashtable<>();
@@ -100,7 +89,7 @@ public class Indentation extends DepthFirstAdapter {
}
public void inAPredicateDefinitionDefinition(
- APredicateDefinitionDefinition node) {
+ APredicateDefinitionDefinition node) {
indentation.put(node.getRhs(), 0);
}
diff --git a/src/main/java/de/tla2b/output/PrologPrinter.java b/src/main/java/de/tla2b/output/PrologPrinter.java
index 0bc44ca..b26fd25 100644
--- a/src/main/java/de/tla2b/output/PrologPrinter.java
+++ b/src/main/java/de/tla2b/output/PrologPrinter.java
@@ -1,14 +1,5 @@
package de.tla2b.output;
-import java.io.File;
-import java.io.IOException;
-import java.io.PrintWriter;
-import java.util.ArrayList;
-import java.util.HashSet;
-import java.util.Hashtable;
-import java.util.List;
-import java.util.Map;
-
import de.be4.classicalb.core.parser.BParser;
import de.be4.classicalb.core.parser.analysis.prolog.ASTProlog;
import de.be4.classicalb.core.parser.analysis.prolog.RecursiveMachineLoader;
@@ -19,6 +10,11 @@ import de.prob.prolog.output.IPrologTermOutput;
import de.prob.prolog.output.PrologTermOutput;
import de.tla2b.types.TLAType;
+import java.io.File;
+import java.io.IOException;
+import java.io.PrintWriter;
+import java.util.*;
+
public class PrologPrinter {
final RecursiveMachineLoader rml;
final BParser bParser;
@@ -30,7 +26,7 @@ public class PrologPrinter {
private final Hashtable<Node, TLAType> typeTable;
public PrologPrinter(RecursiveMachineLoader rml, BParser bParser,
- File mainFile, String moduleName, Hashtable<Node, TLAType> typeTable) {
+ File mainFile, String moduleName, Hashtable<Node, TLAType> typeTable) {
this.rml = rml;
this.bParser = bParser;
this.moduleName = moduleName;
@@ -38,7 +34,7 @@ public class PrologPrinter {
files.add(mainFile);
}
- public void setPositions( HashSet<PositionedNode> sourcePositions) {
+ public void setPositions(HashSet<PositionedNode> sourcePositions) {
positions = sourcePositions;
}
@@ -53,9 +49,9 @@ public class PrologPrinter {
// rml.getNodeIdMapping());
final TlaTypePrinter pprinter = new TlaTypePrinter(
- rml.getNodeIdMapping(), typeTable);
+ rml.getNodeIdMapping(), typeTable);
pprinter.setSourcePositions(positions);
-
+
final ASTProlog prolog = new ASTProlog(pout, pprinter);
// parser version
@@ -79,7 +75,7 @@ public class PrologPrinter {
pout.closeTerm();
pout.fullstop();
for (final Map.Entry<String, Start> entry : rml.getParsedMachines()
- .entrySet()) {
+ .entrySet()) {
pout.openTerm("machine");
//final SourcePositions src = positions.get(entry.getKey());
//pprinter.setSourcePositions(src);
diff --git a/src/main/java/de/tla2b/output/TlaTypePrinter.java b/src/main/java/de/tla2b/output/TlaTypePrinter.java
index 94e2ffe..afc200b 100644
--- a/src/main/java/de/tla2b/output/TlaTypePrinter.java
+++ b/src/main/java/de/tla2b/output/TlaTypePrinter.java
@@ -1,9 +1,5 @@
package de.tla2b.output;
-import java.util.ArrayList;
-import java.util.HashSet;
-import java.util.Hashtable;
-
import de.be4.classicalb.core.parser.analysis.prolog.INodeIds;
import de.be4.classicalb.core.parser.analysis.prolog.PositionPrinter;
import de.be4.classicalb.core.parser.node.Node;
@@ -12,6 +8,10 @@ import de.prob.prolog.output.IPrologTermOutput;
import de.tla2b.exceptions.NotImplementedException;
import de.tla2b.types.*;
+import java.util.ArrayList;
+import java.util.HashSet;
+import java.util.Hashtable;
+
public class TlaTypePrinter implements PositionPrinter, TypeVisitorInterface {
private IPrologTermOutput pout;
@@ -23,7 +23,7 @@ public class TlaTypePrinter implements PositionPrinter, TypeVisitorInterface {
private HashSet<PositionedNode> positions;
public TlaTypePrinter(INodeIds nodeIds,
- Hashtable<Node, TLAType> typeTable) {
+ Hashtable<Node, TLAType> typeTable) {
this.nodeIds = nodeIds;
this.typeTable = typeTable;
}
diff --git a/src/main/java/de/tla2b/output/TypeVisitorInterface.java b/src/main/java/de/tla2b/output/TypeVisitorInterface.java
index 2edd346..01ad7af 100644
--- a/src/main/java/de/tla2b/output/TypeVisitorInterface.java
+++ b/src/main/java/de/tla2b/output/TypeVisitorInterface.java
@@ -4,18 +4,30 @@ import de.tla2b.types.*;
public interface TypeVisitorInterface {
-
+
void caseIntegerType(IntType type);
+
void caseBoolType(BoolType type);
+
void caseEnumType(EnumType type);
+
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);
+
void caseStructType(StructType type);
+
void caseTupleType(TupleType type);
+
void caseUntyped(UntypedType type);
}
diff --git a/src/main/java/de/tla2b/translation/BDefinitionsFinder.java b/src/main/java/de/tla2b/translation/BDefinitionsFinder.java
index 73eef83..a68e52f 100644
--- a/src/main/java/de/tla2b/translation/BDefinitionsFinder.java
+++ b/src/main/java/de/tla2b/translation/BDefinitionsFinder.java
@@ -1,24 +1,17 @@
package de.tla2b.translation;
-import java.util.ArrayList;
-import java.util.HashSet;
-import java.util.Set;
-
import de.be4.classicalb.core.parser.util.Utils;
import de.tla2b.analysis.AbstractASTVisitor;
import de.tla2b.analysis.BOperation;
import de.tla2b.analysis.SpecAnalyser;
import de.tla2b.global.TranslationGlobals;
-
-import tla2sany.semantic.ASTConstants;
-import tla2sany.semantic.AssumeNode;
-import tla2sany.semantic.ExprNode;
-import tla2sany.semantic.ExprOrOpArgNode;
-import tla2sany.semantic.OpApplNode;
-import tla2sany.semantic.OpDefNode;
-
+import tla2sany.semantic.*;
import tlc2.tool.ToolGlobals;
+import java.util.ArrayList;
+import java.util.HashSet;
+import java.util.Set;
+
public class BDefinitionsFinder extends AbstractASTVisitor implements ASTConstants, ToolGlobals, TranslationGlobals {
private final HashSet<OpDefNode> bDefinitionsSet = new HashSet<>();
diff --git a/src/main/java/de/tla2b/translation/BMacroHandler.java b/src/main/java/de/tla2b/translation/BMacroHandler.java
index 5cf5e02..bcc5292 100644
--- a/src/main/java/de/tla2b/translation/BMacroHandler.java
+++ b/src/main/java/de/tla2b/translation/BMacroHandler.java
@@ -1,18 +1,11 @@
package de.tla2b.translation;
-import java.util.*;
-
-import tla2sany.semantic.AssumeNode;
-import tla2sany.semantic.ExprNode;
-import tla2sany.semantic.ExprOrOpArgNode;
-import tla2sany.semantic.FormalParamNode;
-import tla2sany.semantic.ModuleNode;
-import tla2sany.semantic.OpApplNode;
-import tla2sany.semantic.OpDefNode;
-import tla2sany.semantic.SymbolNode;
import de.tla2b.analysis.AbstractASTVisitor;
import de.tla2b.analysis.SpecAnalyser;
import de.tla2b.config.ConfigfileEvaluator;
+import tla2sany.semantic.*;
+
+import java.util.*;
public class BMacroHandler extends AbstractASTVisitor {
@@ -25,8 +18,8 @@ public class BMacroHandler extends AbstractASTVisitor {
OpDefNode def = moduleNode.getOpDefs()[i];
if (specAnalyser.getUsedDefinitions().contains(def)) {
if (conEval != null
- && conEval.getConstantOverrideTable()
- .containsValue(def)) {
+ && conEval.getConstantOverrideTable()
+ .containsValue(def)) {
continue;
}
bDefs.add(def);
@@ -77,36 +70,36 @@ public class BMacroHandler extends AbstractASTVisitor {
@Override
public void visitBuiltInNode(OpApplNode n) {
switch (getOpCode(n.getOperator().getName())) {
- case OPCODE_rfs:
- case OPCODE_nrfs:
- case OPCODE_fc: // Represents [x \in S |-> e]
- case OPCODE_be: // \E x \in S : P
- case OPCODE_bf: // \A x \in S : P
- case OPCODE_bc: // CHOOSE x \in S: P
- case OPCODE_sso: // $SubsetOf Represents {x \in S : P}
- case OPCODE_soa: // $SetOfAll Represents {e : p1 \in S, p2,p3 \in S2}
- {
-
- FormalParamNode[][] params = n.getBdedQuantSymbolLists();
- HashSet<FormalParamNode> set = new HashSet<>();
- for (FormalParamNode[] param : params) {
- Collections.addAll(set, param);
- }
- localVariables.addAll(set);
- ExprNode[] in = n.getBdedQuantBounds();
- for (ExprNode exprNode : in) {
- visitExprNode(exprNode);
+ case OPCODE_rfs:
+ case OPCODE_nrfs:
+ case OPCODE_fc: // Represents [x \in S |-> e]
+ case OPCODE_be: // \E x \in S : P
+ case OPCODE_bf: // \A x \in S : P
+ case OPCODE_bc: // CHOOSE x \in S: P
+ case OPCODE_sso: // $SubsetOf Represents {x \in S : P}
+ case OPCODE_soa: // $SetOfAll Represents {e : p1 \in S, p2,p3 \in S2}
+ {
+
+ FormalParamNode[][] params = n.getBdedQuantSymbolLists();
+ HashSet<FormalParamNode> set = new HashSet<>();
+ for (FormalParamNode[] param : params) {
+ Collections.addAll(set, param);
+ }
+ localVariables.addAll(set);
+ ExprNode[] in = n.getBdedQuantBounds();
+ for (ExprNode exprNode : in) {
+ visitExprNode(exprNode);
+ }
+ ExprOrOpArgNode[] arguments = n.getArgs();
+ for (ExprOrOpArgNode exprOrOpArgNode : arguments) {
+ visitExprOrOpArgNode(exprOrOpArgNode);
+ }
+ localVariables.removeAll(set);
+ return;
}
- ExprOrOpArgNode[] arguments = n.getArgs();
- for (ExprOrOpArgNode exprOrOpArgNode : arguments) {
- visitExprOrOpArgNode(exprOrOpArgNode);
+ default: {
+ super.visitBuiltInNode(n);
}
- localVariables.removeAll(set);
- return;
- }
- default: {
- super.visitBuiltInNode(n);
- }
}
diff --git a/src/main/java/de/tla2b/translation/OperationsFinder.java b/src/main/java/de/tla2b/translation/OperationsFinder.java
index 4ecec30..6492669 100644
--- a/src/main/java/de/tla2b/translation/OperationsFinder.java
+++ b/src/main/java/de/tla2b/translation/OperationsFinder.java
@@ -1,25 +1,20 @@
package de.tla2b.translation;
-import java.util.ArrayList;
-import util.UniqueString;
-
-import tla2sany.semantic.ASTConstants;
-import tla2sany.semantic.ExprNode;
-import tla2sany.semantic.FormalParamNode;
-import tla2sany.semantic.LetInNode;
-import tla2sany.semantic.OpApplNode;
-import tla2sany.semantic.OpDefNode;
-import tlc2.tool.BuiltInOPs;
-import tlc2.tool.ToolGlobals;
import de.tla2b.analysis.AbstractASTVisitor;
import de.tla2b.analysis.BOperation;
import de.tla2b.analysis.SpecAnalyser;
-import de.tla2b.global.BBuiltInOPs;
import de.tla2b.global.BBuildIns;
+import de.tla2b.global.BBuiltInOPs;
import de.tla2b.global.TranslationGlobals;
+import tla2sany.semantic.*;
+import tlc2.tool.BuiltInOPs;
+import tlc2.tool.ToolGlobals;
+import util.UniqueString;
+
+import java.util.ArrayList;
public class OperationsFinder extends AbstractASTVisitor implements
- ASTConstants, ToolGlobals, TranslationGlobals {
+ ASTConstants, ToolGlobals, TranslationGlobals {
private final SpecAnalyser specAnalyser;
private String currentName;
@@ -40,42 +35,42 @@ public class OperationsFinder extends AbstractASTVisitor implements
}
}
-
+
public void visitExprNode(ExprNode n) {
switch (n.getKind()) {
- case OpApplKind: {
- visitOpApplNode((OpApplNode) n);
- return;
- }
- case NumeralKind:
- case DecimalKind: {
- throw new RuntimeException(String.format(
+ case OpApplKind: {
+ visitOpApplNode((OpApplNode) n);
+ return;
+ }
+ case NumeralKind:
+ case DecimalKind: {
+ throw new RuntimeException(String.format(
"Expected an action (instead of a number).%n%s", n.getLocation().toString()));
- }
- case StringKind: {
- throw new RuntimeException(String.format(
+ }
+ case StringKind: {
+ throw new RuntimeException(String.format(
"Expected an action (instead of a string).%n%s", n.getLocation().toString()));
- }
- case SubstInKind: {
- throw new RuntimeException(String.format(
+ }
+ case SubstInKind: {
+ throw new RuntimeException(String.format(
"Expected an action.%n%s", n.getLocation().toString()));
- }
- case AtNodeKind: { // @
- throw new RuntimeException(String.format(
+ }
+ case AtNodeKind: { // @
+ throw new RuntimeException(String.format(
"Expected an action.%n%s", n.getLocation().toString()));
- }
- case LetInKind: {
- // we do not visit the local definitions
- visitExprNode(((LetInNode) n).getBody());
- }
+ }
+ case LetInKind: {
+ // we do not visit the local definitions
+ visitExprNode(((LetInNode) n).getBody());
+ }
}
}
-
+
public void visitUserDefinedNode(OpApplNode n) {
OpDefNode def = (OpDefNode) n.getOperator();
if (BBuiltInOPs.contains(def.getName())) {
BOperation op = new BOperation(def.getName().toString(), n, exists,
- specAnalyser);
+ specAnalyser);
bOperations.add(op);
return;
}
@@ -90,76 +85,76 @@ public class OperationsFinder extends AbstractASTVisitor implements
@Override
public void visitBuiltInNode(OpApplNode n) {
- UniqueString opname = n.getOperator().getName();
+ UniqueString opname = n.getOperator().getName();
int opcode = BuiltInOPs.getOpCode(opname);
switch (opcode) {
- case OPCODE_dl: // DisjList: split action further
- {
- if (n.getArgs().length == 1) {
- visitExprOrOpArgNode(n.getArgs()[0]);
- } else {
+ case OPCODE_dl: // DisjList: split action further
+ {
+ if (n.getArgs().length == 1) {
+ visitExprOrOpArgNode(n.getArgs()[0]);
+ } else {
+ String oldName = currentName;
+ ArrayList<OpApplNode> oldExists = new ArrayList<>(
+ exists);
+
+ for (int i = 0; i < n.getArgs().length; i++) {
+ exists = new ArrayList<>(oldExists);
+ currentName = oldName + i;
+ visitExprOrOpArgNode(n.getArgs()[i]);
+ }
+ }
+ return;
+ }
+ case OPCODE_lor: { // logical or: split action further
String oldName = currentName;
- ArrayList<OpApplNode> oldExists = new ArrayList<>(
- exists);
+ ArrayList<OpApplNode> oldExists = new ArrayList<>(exists);
for (int i = 0; i < n.getArgs().length; i++) {
exists = new ArrayList<>(oldExists);
currentName = oldName + i;
visitExprOrOpArgNode(n.getArgs()[i]);
}
+ return;
}
- return;
- }
- case OPCODE_lor: { // logical or: split action further
- String oldName = currentName;
- ArrayList<OpApplNode> oldExists = new ArrayList<>(exists);
-
- for (int i = 0; i < n.getArgs().length; i++) {
- exists = new ArrayList<>(oldExists);
- currentName = oldName+ i;
- visitExprOrOpArgNode(n.getArgs()[i]);
+ case OPCODE_be: { // BoundedExists
+ exists.add(n);
+ visitExprOrOpArgNode(n.getArgs()[0]);
+ return;
}
- return;
- }
- case OPCODE_be: { // BoundedExists
- exists.add(n);
- visitExprOrOpArgNode(n.getArgs()[0]);
- return;
- }
- case OPCODE_unchanged:
- case OPCODE_eq: // =
- case OPCODE_noteq: // /=, #
- case OPCODE_neg: // Negation
- case OPCODE_lnot: // Negation
- case OPCODE_cl: // $ConjList
- case OPCODE_land: // \land
- case OPCODE_equiv: // \equiv
- case OPCODE_implies: // =>
- case OPCODE_bf: // \A x \in S : P
- case OPCODE_in: // \in
- case OPCODE_notin: // \notin
- case OPCODE_subseteq: // \subseteq - subset or equal
- case OPCODE_fa: // $FcnApply f[1]
- case OPCODE_ite: // IF THEN ELSE
- case OPCODE_case: {
- // no further decomposing: create a B operation
- BOperation op = new BOperation(currentName, n, exists, specAnalyser);
- bOperations.add(op);
- return;
- }
+ case OPCODE_unchanged:
+ case OPCODE_eq: // =
+ case OPCODE_noteq: // /=, #
+ case OPCODE_neg: // Negation
+ case OPCODE_lnot: // Negation
+ case OPCODE_cl: // $ConjList
+ case OPCODE_land: // \land
+ case OPCODE_equiv: // \equiv
+ case OPCODE_implies: // =>
+ case OPCODE_bf: // \A x \in S : P
+ case OPCODE_in: // \in
+ case OPCODE_notin: // \notin
+ case OPCODE_subseteq: // \subseteq - subset or equal
+ case OPCODE_fa: // $FcnApply f[1]
+ case OPCODE_ite: // IF THEN ELSE
+ case OPCODE_case: {
+ // no further decomposing: create a B operation
+ BOperation op = new BOperation(currentName, n, exists, specAnalyser);
+ bOperations.add(op);
+ return;
+ }
}
//System.out.println("OPCODE of " + opname + " = "+ opcode);
-
+
if (opname == BBuildIns.OP_false || // FALSE: always disabled
- opname == BBuildIns.OP_true) { // TRUE: CHAOS
+ opname == BBuildIns.OP_true) { // TRUE: CHAOS
BOperation op = new BOperation(currentName, n, exists, specAnalyser);
bOperations.add(op);
return;
}
throw new RuntimeException(String.format(
- "Expected an action at '%s' :%n%s", n.getOperator().getName(), n.getLocation().toString()));
+ "Expected an action at '%s' :%n%s", n.getOperator().getName(), n.getLocation().toString()));
}
diff --git a/src/main/java/de/tla2b/translation/RecursiveFunctionHandler.java b/src/main/java/de/tla2b/translation/RecursiveFunctionHandler.java
index 9e99ac9..d659417 100644
--- a/src/main/java/de/tla2b/translation/RecursiveFunctionHandler.java
+++ b/src/main/java/de/tla2b/translation/RecursiveFunctionHandler.java
@@ -1,20 +1,14 @@
package de.tla2b.translation;
+import de.tla2b.analysis.AbstractASTVisitor;
+import de.tla2b.analysis.SpecAnalyser;
+import tla2sany.semantic.*;
+
import java.util.ArrayList;
import java.util.Collections;
import java.util.HashSet;
import java.util.Hashtable;
-import tla2sany.semantic.ExprNode;
-import tla2sany.semantic.ExprOrOpArgNode;
-import tla2sany.semantic.FormalParamNode;
-import tla2sany.semantic.OpApplNode;
-import tla2sany.semantic.OpDefNode;
-import tla2sany.semantic.SemanticNode;
-import tla2sany.semantic.SymbolNode;
-import de.tla2b.analysis.AbstractASTVisitor;
-import de.tla2b.analysis.SpecAnalyser;
-
public class RecursiveFunctionHandler extends AbstractASTVisitor {
private ArrayList<FormalParamNode> paramList;
@@ -68,34 +62,34 @@ public class RecursiveFunctionHandler extends AbstractASTVisitor {
@Override
public void visitBuiltInNode(OpApplNode n) {
switch (getOpCode(n.getOperator().getName())) {
- case OPCODE_rfs:
- case OPCODE_nrfs:
- case OPCODE_fc: // Represents [x \in S |-> e]
- case OPCODE_be: // \E x \in S : P
- case OPCODE_bf: // \A x \in S : P
- case OPCODE_bc: // CHOOSE x \in S: P
- case OPCODE_sso: // $SubsetOf Represents {x \in S : P}
- case OPCODE_soa: // $SetOfAll Represents {e : p1 \in S, p2,p3 \in S2}
- {
- FormalParamNode[][] params = n.getBdedQuantSymbolLists();
- HashSet<FormalParamNode> set = new HashSet<>();
- for (FormalParamNode[] param : params) {
- Collections.addAll(set, param);
- }
- ignoreParamList.addAll(set);
- ExprNode[] in = n.getBdedQuantBounds();
- for (ExprNode exprNode : in) {
- visitExprNode(exprNode);
+ case OPCODE_rfs:
+ case OPCODE_nrfs:
+ case OPCODE_fc: // Represents [x \in S |-> e]
+ case OPCODE_be: // \E x \in S : P
+ case OPCODE_bf: // \A x \in S : P
+ case OPCODE_bc: // CHOOSE x \in S: P
+ case OPCODE_sso: // $SubsetOf Represents {x \in S : P}
+ case OPCODE_soa: // $SetOfAll Represents {e : p1 \in S, p2,p3 \in S2}
+ {
+ FormalParamNode[][] params = n.getBdedQuantSymbolLists();
+ HashSet<FormalParamNode> set = new HashSet<>();
+ for (FormalParamNode[] param : params) {
+ Collections.addAll(set, param);
+ }
+ ignoreParamList.addAll(set);
+ ExprNode[] in = n.getBdedQuantBounds();
+ for (ExprNode exprNode : in) {
+ visitExprNode(exprNode);
+ }
+ ExprOrOpArgNode[] arguments = n.getArgs();
+ for (ExprOrOpArgNode exprOrOpArgNode : arguments) {
+ visitExprOrOpArgNode(exprOrOpArgNode);
+ }
+ return;
}
- ExprOrOpArgNode[] arguments = n.getArgs();
- for (ExprOrOpArgNode exprOrOpArgNode : arguments) {
- visitExprOrOpArgNode(exprOrOpArgNode);
+ default: {
+ super.visitBuiltInNode(n);
}
- return;
- }
- default: {
- super.visitBuiltInNode(n);
- }
}
diff --git a/src/main/java/de/tla2b/translation/UsedDefinitionsFinder.java b/src/main/java/de/tla2b/translation/UsedDefinitionsFinder.java
index b947fcc..61609f6 100644
--- a/src/main/java/de/tla2b/translation/UsedDefinitionsFinder.java
+++ b/src/main/java/de/tla2b/translation/UsedDefinitionsFinder.java
@@ -1,21 +1,19 @@
package de.tla2b.translation;
-import java.util.Collection;
-import java.util.HashSet;
-
import de.be4.classicalb.core.parser.util.Utils;
import de.tla2b.analysis.AbstractASTVisitor;
import de.tla2b.analysis.SpecAnalyser;
import de.tla2b.global.BBuiltInOPs;
import de.tla2b.global.TranslationGlobals;
-
import tla2sany.semantic.ASTConstants;
import tla2sany.semantic.ModuleNode;
import tla2sany.semantic.OpApplNode;
import tla2sany.semantic.OpDefNode;
-
import tlc2.tool.ToolGlobals;
+import java.util.Collection;
+import java.util.HashSet;
+
public class UsedDefinitionsFinder extends AbstractASTVisitor implements ASTConstants, ToolGlobals, TranslationGlobals {
private final HashSet<OpDefNode> usedDefinitions = new HashSet<>();
@@ -82,7 +80,7 @@ public class UsedDefinitionsFinder extends AbstractASTVisitor implements ASTCons
return;
}
if (BBuiltInOPs.contains(def.getName())
- && STANDARD_MODULES.contains(def.getSource().getOriginallyDefinedInModuleNode().getName().toString())) {
+ && STANDARD_MODULES.contains(def.getSource().getOriginallyDefinedInModuleNode().getName().toString())) {
return;
}
if (usedDefinitions.add(def)) {
diff --git a/src/main/java/de/tla2b/types/AbstractHasFollowers.java b/src/main/java/de/tla2b/types/AbstractHasFollowers.java
index 2df1196..ef6e146 100644
--- a/src/main/java/de/tla2b/types/AbstractHasFollowers.java
+++ b/src/main/java/de/tla2b/types/AbstractHasFollowers.java
@@ -1,10 +1,9 @@
package de.tla2b.types;
-import java.util.ArrayList;
-import java.util.List;
-
import tla2sany.semantic.SemanticNode;
+import java.util.ArrayList;
+
public abstract class AbstractHasFollowers extends TLAType {
public ArrayList<Object> followers;
diff --git a/src/main/java/de/tla2b/types/AbstractSymbol.java b/src/main/java/de/tla2b/types/AbstractSymbol.java
index 35da7fc..8b9e3bf 100644
--- a/src/main/java/de/tla2b/types/AbstractSymbol.java
+++ b/src/main/java/de/tla2b/types/AbstractSymbol.java
@@ -3,11 +3,11 @@ package de.tla2b.types;
public abstract class AbstractSymbol {
private TLAType type;
-
- public AbstractSymbol(TLAType t){
+
+ public AbstractSymbol(TLAType t) {
setType(t);
}
-
+
public TLAType getType() {
return type;
}
diff --git a/src/main/java/de/tla2b/types/BoolType.java b/src/main/java/de/tla2b/types/BoolType.java
index f901cd0..1a9175b 100644
--- a/src/main/java/de/tla2b/types/BoolType.java
+++ b/src/main/java/de/tla2b/types/BoolType.java
@@ -31,7 +31,7 @@ public class BoolType extends TLAType {
public boolean compare(TLAType o) {
return o.getKind() == UNTYPED || o.getKind() == BOOL;
}
-
+
@Override
public BoolType unify(TLAType o) throws UnificationException {
if (o.getKind() == BOOL) {
@@ -47,7 +47,7 @@ public class BoolType extends TLAType {
public BoolType cloneTLAType() {
return this;
}
-
+
@Override
public boolean contains(TLAType o) {
return false;
diff --git a/src/main/java/de/tla2b/types/EnumType.java b/src/main/java/de/tla2b/types/EnumType.java
index 36c57cb..08dd486 100644
--- a/src/main/java/de/tla2b/types/EnumType.java
+++ b/src/main/java/de/tla2b/types/EnumType.java
@@ -1,13 +1,13 @@
package de.tla2b.types;
-import java.util.ArrayList;
-import java.util.LinkedHashSet;
-
import de.be4.classicalb.core.parser.node.PExpression;
import de.tla2b.exceptions.UnificationException;
import de.tla2b.output.TypeVisitorInterface;
import de.tla2bAst.BAstCreator;
+import java.util.ArrayList;
+import java.util.LinkedHashSet;
+
public class EnumType extends AbstractHasFollowers {
public final LinkedHashSet<String> modelvalues;
public int id;
@@ -59,7 +59,7 @@ public class EnumType extends AbstractHasFollowers {
public EnumType cloneTLAType() {
return this;
}
-
+
@Override
public boolean contains(TLAType o) {
//TODO is this really false
@@ -70,7 +70,7 @@ public class EnumType extends AbstractHasFollowers {
public String toString() {
return "ENUM" + id;
}
-
+
@Override
public PExpression getBNode() {
return BAstCreator.createIdentifierNode("ENUM" + id);
diff --git a/src/main/java/de/tla2b/types/FunctionType.java b/src/main/java/de/tla2b/types/FunctionType.java
index b061b51..64636da 100644
--- a/src/main/java/de/tla2b/types/FunctionType.java
+++ b/src/main/java/de/tla2b/types/FunctionType.java
@@ -39,8 +39,8 @@ public class FunctionType extends AbstractHasFollowers {
if (other.getKind() == UNTYPED)
return true;
if (other instanceof StringType
- && domain.compare(IntType.getInstance())
- && range instanceof UntypedType) {
+ && domain.compare(IntType.getInstance())
+ && range instanceof UntypedType) {
return true;
}
if (other instanceof FunctionType) {
@@ -59,7 +59,7 @@ public class FunctionType extends AbstractHasFollowers {
@Override
public boolean contains(TLAType o) {
return domain.equals(o) || domain.contains(o) || range.equals(o)
- || range.contains(o);
+ || range.contains(o);
}
@Override
@@ -139,7 +139,7 @@ public class FunctionType extends AbstractHasFollowers {
@Override
public PExpression getBNode() {
return new APartialFunctionExpression(domain.getBNode(),
- range.getBNode());
+ range.getBNode());
}
public void apply(TypeVisitorInterface vistor) {
diff --git a/src/main/java/de/tla2b/types/IType.java b/src/main/java/de/tla2b/types/IType.java
index 2f1f877..b394c0d 100644
--- a/src/main/java/de/tla2b/types/IType.java
+++ b/src/main/java/de/tla2b/types/IType.java
@@ -11,13 +11,13 @@ public interface IType {
int POW = 5;
int PAIR = 6;
int STRUCT = 7;
- int TUPLEORSEQ = 8;
+ 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/ModelValueType.java b/src/main/java/de/tla2b/types/ModelValueType.java
index 9607031..78eaaec 100644
--- a/src/main/java/de/tla2b/types/ModelValueType.java
+++ b/src/main/java/de/tla2b/types/ModelValueType.java
@@ -26,12 +26,12 @@ public class ModelValueType extends TLAType {
public boolean isUntyped() {
return false;
}
-
+
@Override
public boolean compare(TLAType o) {
return o.getKind() == UNTYPED || o.getKind() == MODELVALUE;
}
-
+
@Override
public ModelValueType unify(TLAType o) throws UnificationException {
if (o.getKind() == MODELVALUE) {
@@ -47,7 +47,7 @@ public class ModelValueType extends TLAType {
public ModelValueType cloneTLAType() {
return this;
}
-
+
@Override
public boolean contains(TLAType o) {
return false;
diff --git a/src/main/java/de/tla2b/types/PairType.java b/src/main/java/de/tla2b/types/PairType.java
index b98dfe4..316d36b 100644
--- a/src/main/java/de/tla2b/types/PairType.java
+++ b/src/main/java/de/tla2b/types/PairType.java
@@ -108,13 +108,13 @@ public class PairType extends AbstractHasFollowers {
@Override
public PairType cloneTLAType() {
return new PairType(this.first.cloneTLAType(),
- this.second.cloneTLAType());
+ this.second.cloneTLAType());
}
@Override
public boolean contains(TLAType o) {
return first.equals(o) || first.contains(o) || second.equals(o)
- || second.contains(o);
+ || second.contains(o);
}
@Override
diff --git a/src/main/java/de/tla2b/types/SetType.java b/src/main/java/de/tla2b/types/SetType.java
index 0460b96..4b93977 100644
--- a/src/main/java/de/tla2b/types/SetType.java
+++ b/src/main/java/de/tla2b/types/SetType.java
@@ -37,16 +37,16 @@ public class SetType extends AbstractHasFollowers {
}
public SetType unify(TLAType o) throws UnificationException {
- if (!this.compare(o)|| this.contains(o)) {
+ if (!this.compare(o) || this.contains(o)) {
throw new UnificationException();
}
// if o has followers than switch pointer to this
if (o instanceof AbstractHasFollowers) {
((AbstractHasFollowers) o).setFollowersTo(this);
}
-
- if (o instanceof StructOrFunctionType){
- return (SetType)o.unify(this);
+
+ if (o instanceof StructOrFunctionType) {
+ return (SetType) o.unify(this);
}
if (o instanceof SetType) {
SetType p = (SetType) o;
@@ -61,12 +61,12 @@ public class SetType extends AbstractHasFollowers {
@Override
public boolean compare(TLAType o) {
- if(this.contains(o))
+ if (this.contains(o))
return false;
-
+
if (o.getKind() == UNTYPED)
return true;
-
+
if (o instanceof SetType) {
SetType p = (SetType) o;
// test sub types compatibility
diff --git a/src/main/java/de/tla2b/types/StructOrFunctionType.java b/src/main/java/de/tla2b/types/StructOrFunctionType.java
index eb559b0..56af36e 100644
--- a/src/main/java/de/tla2b/types/StructOrFunctionType.java
+++ b/src/main/java/de/tla2b/types/StructOrFunctionType.java
@@ -1,14 +1,14 @@
package de.tla2b.types;
-import java.util.Iterator;
-import java.util.LinkedHashMap;
-import java.util.Set;
-import java.util.Map.Entry;
-
import de.be4.classicalb.core.parser.node.PExpression;
import de.tla2b.exceptions.UnificationException;
import de.tla2b.output.TypeVisitorInterface;
+import java.util.Iterator;
+import java.util.LinkedHashMap;
+import java.util.Map.Entry;
+import java.util.Set;
+
public class StructOrFunctionType extends AbstractHasFollowers {
private final LinkedHashMap<String, TLAType> types;
@@ -43,7 +43,7 @@ public class StructOrFunctionType extends AbstractHasFollowers {
public String toString() {
StringBuilder sb = new StringBuilder();
sb.append("StructOrFunction(");
- for (Iterator<String> keys = types.keySet().iterator(); keys.hasNext();) {
+ for (Iterator<String> keys = types.keySet().iterator(); keys.hasNext(); ) {
String key = keys.next();
sb.append("\"").append(key).append("\"");
sb.append(" : ").append(types.get(key));
@@ -130,7 +130,7 @@ public class StructOrFunctionType extends AbstractHasFollowers {
temp = temp.unify(itr.next());
}
SetType found = new SetType(new PairType(StringType.getInstance(),
- temp));
+ temp));
return found.unify(o);
}
if (o instanceof StructType) {
diff --git a/src/main/java/de/tla2b/types/StructType.java b/src/main/java/de/tla2b/types/StructType.java
index 51120ae..f11cf84 100644
--- a/src/main/java/de/tla2b/types/StructType.java
+++ b/src/main/java/de/tla2b/types/StructType.java
@@ -1,23 +1,13 @@
package de.tla2b.types;
-import java.util.ArrayList;
-import java.util.Iterator;
-import java.util.LinkedHashMap;
-import java.util.List;
-import java.util.Map.Entry;
-import java.util.Set;
-
-import de.be4.classicalb.core.parser.node.ABoolSetExpression;
-import de.be4.classicalb.core.parser.node.AMultOrCartExpression;
-import de.be4.classicalb.core.parser.node.APowSubsetExpression;
-import de.be4.classicalb.core.parser.node.ARecEntry;
-import de.be4.classicalb.core.parser.node.AStructExpression;
-import de.be4.classicalb.core.parser.node.PExpression;
-import de.be4.classicalb.core.parser.node.PRecEntry;
+import de.be4.classicalb.core.parser.node.*;
import de.tla2b.exceptions.UnificationException;
import de.tla2b.output.TypeVisitorInterface;
import de.tla2bAst.BAstCreator;
+import java.util.*;
+import java.util.Map.Entry;
+
public class StructType extends AbstractHasFollowers {
private final LinkedHashMap<String, TLAType> types;
private boolean extensible;
diff --git a/src/main/java/de/tla2b/types/TLAType.java b/src/main/java/de/tla2b/types/TLAType.java
index c511568..facb86c 100644
--- a/src/main/java/de/tla2b/types/TLAType.java
+++ b/src/main/java/de/tla2b/types/TLAType.java
@@ -15,20 +15,20 @@ public abstract class TLAType implements IType {
}
public abstract String toString();
-
+
public abstract PExpression getBNode();
public abstract boolean compare(TLAType o);
-
+
public abstract boolean contains(TLAType o);
-
+
public abstract boolean isUntyped();
-
+
public abstract TLAType cloneTLAType();
public abstract TLAType unify(TLAType o) throws UnificationException;
-
- public TLAType unityAll(TLAType[] types) throws UnificationException{
+
+ public TLAType unityAll(TLAType[] types) throws UnificationException {
TLAType current = this;
for (TLAType type : types) {
current = current.unify(type);
diff --git a/src/main/java/de/tla2b/types/TupleOrFunction.java b/src/main/java/de/tla2b/types/TupleOrFunction.java
index f2fa7a5..a898ac6 100644
--- a/src/main/java/de/tla2b/types/TupleOrFunction.java
+++ b/src/main/java/de/tla2b/types/TupleOrFunction.java
@@ -1,15 +1,15 @@
package de.tla2b.types;
+import de.be4.classicalb.core.parser.node.PExpression;
+import de.tla2b.exceptions.UnificationException;
+import de.tla2b.output.TypeVisitorInterface;
+
import java.util.ArrayList;
import java.util.Iterator;
import java.util.LinkedHashMap;
import java.util.List;
import java.util.Map.Entry;
-import de.be4.classicalb.core.parser.node.PExpression;
-import de.tla2b.exceptions.UnificationException;
-import de.tla2b.output.TypeVisitorInterface;
-
public class TupleOrFunction extends AbstractHasFollowers {
private final LinkedHashMap<Integer, TLAType> types = new LinkedHashMap<>();
@@ -51,7 +51,7 @@ public class TupleOrFunction extends AbstractHasFollowers {
StringBuilder sb = new StringBuilder();
sb.append("TupleOrFunction");
sb.append("(");
- for (Iterator<Integer> keys = types.keySet().iterator(); keys.hasNext();) {
+ for (Iterator<Integer> keys = types.keySet().iterator(); keys.hasNext(); ) {
Integer key = keys.next();
sb.append(key);
sb.append(" : ").append(types.get(key));
@@ -91,7 +91,7 @@ public class TupleOrFunction extends AbstractHasFollowers {
StringBuilder sb = new StringBuilder();
sb.append("(");
for (Iterator<Integer> keys = types.keySet().iterator(); keys
- .hasNext();) {
+ .hasNext(); ) {
Integer key = keys.next();
sb.append(key);
sb.append(" : ").append(types.get(key));
@@ -130,9 +130,9 @@ public class TupleOrFunction extends AbstractHasFollowers {
TupleType tupleType = (TupleType) o;
for (Integer index : this.types.keySet()) {
if (index >= 1
- && index <= tupleType.getTypes().size()
- && this.types.get(index).compare(
- tupleType.getTypes().get(index - 1))) {
+ && index <= tupleType.getTypes().size()
+ && this.types.get(index).compare(
+ tupleType.getTypes().get(index - 1))) {
} else {
return false;
}
@@ -163,7 +163,7 @@ public class TupleOrFunction extends AbstractHasFollowers {
}
private static boolean isTupleOrFunction(TupleOrFunction t1,
- TupleOrFunction t2) {
+ TupleOrFunction t2) {
List<TLAType> typeList = new ArrayList<>();
typeList.addAll(t1.types.values());
typeList.addAll(t2.types.values());
@@ -199,8 +199,8 @@ public class TupleOrFunction extends AbstractHasFollowers {
public TLAType cloneTLAType() {
TupleOrFunction res = new TupleOrFunction();
for (Entry<Integer, TLAType> entry : this.types.entrySet()) {
- res.types.put(entry.getKey().intValue(), entry
- .getValue().cloneTLAType());
+ res.types.put(entry.getKey(), entry
+ .getValue().cloneTLAType());
}
return res;
}
@@ -231,7 +231,7 @@ public class TupleOrFunction extends AbstractHasFollowers {
for (int i = 0; i < tupleType.getTypes().size(); i++) {
if (this.types.containsKey(i + 1)) {
TLAType res = tupleType.getTypes().get(i)
- .unify(this.types.get(i + 1));
+ .unify(this.types.get(i + 1));
typeList.add(res);
} else {
typeList.add(tupleType.getTypes().get(i));
@@ -322,7 +322,7 @@ public class TupleOrFunction extends AbstractHasFollowers {
if (comparable(list)) {
FunctionType func = new FunctionType(IntType.getInstance(),
- new UntypedType());
+ new UntypedType());
try {
func = (FunctionType) func.unify(this);
this.setFollowersTo(func);
diff --git a/src/main/java/de/tla2b/types/TupleType.java b/src/main/java/de/tla2b/types/TupleType.java
index a5b6ae2..b28632a 100644
--- a/src/main/java/de/tla2b/types/TupleType.java
+++ b/src/main/java/de/tla2b/types/TupleType.java
@@ -1,13 +1,13 @@
package de.tla2b.types;
-import java.util.ArrayList;
-import java.util.List;
-
import de.be4.classicalb.core.parser.node.AMultOrCartExpression;
import de.be4.classicalb.core.parser.node.PExpression;
import de.tla2b.exceptions.UnificationException;
import de.tla2b.output.TypeVisitorInterface;
+import java.util.ArrayList;
+import java.util.List;
+
public class TupleType extends AbstractHasFollowers {
private List<TLAType> types;
diff --git a/src/main/java/de/tla2b/types/UntypedType.java b/src/main/java/de/tla2b/types/UntypedType.java
index 56dc71d..54e9c3f 100644
--- a/src/main/java/de/tla2b/types/UntypedType.java
+++ b/src/main/java/de/tla2b/types/UntypedType.java
@@ -19,20 +19,20 @@ public class UntypedType extends AbstractHasFollowers {
//this.deleteFollowers();
return o;
}
-
+
@Override
- public boolean compare(TLAType o){
+ public boolean compare(TLAType o) {
return !o.contains(this);
}
-
+
@Override
- public boolean contains(TLAType o){
+ public boolean contains(TLAType o) {
return false;
}
@Override
public String toString() {
- return "UNTYPED_"+hashCode();
+ return "UNTYPED_" + hashCode();
}
@Override
diff --git a/src/main/java/de/tla2b/util/FileUtils.java b/src/main/java/de/tla2b/util/FileUtils.java
index e0c3525..88adbe2 100644
--- a/src/main/java/de/tla2b/util/FileUtils.java
+++ b/src/main/java/de/tla2b/util/FileUtils.java
@@ -25,11 +25,11 @@ public class FileUtils {
} else {
// Remove the last period and everything after it
File renamed = new File(f.getParent(), name.substring(0,
- lastPeriodPos));
+ lastPeriodPos));
return renamed.getPath();
}
}
-
+
public static String fileToString(String fileName) throws IOException {
StringBuilder res = new StringBuilder();
BufferedReader in = new BufferedReader(new FileReader(fileName));
@@ -40,7 +40,6 @@ public class FileUtils {
in.close();
return res.toString();
}
-
-
-
+
+
}
diff --git a/src/main/java/de/tla2bAst/ExpressionTranslator.java b/src/main/java/de/tla2bAst/ExpressionTranslator.java
index 5e69ae4..4cd3cc7 100644
--- a/src/main/java/de/tla2bAst/ExpressionTranslator.java
+++ b/src/main/java/de/tla2bAst/ExpressionTranslator.java
@@ -1,12 +1,11 @@
package de.tla2bAst;
-import java.io.File;
-import java.io.FileWriter;
-import java.io.IOException;
-import java.util.ArrayList;
-import java.util.HashSet;
-import java.util.Set;
-
+import de.be4.classicalb.core.parser.node.Start;
+import de.tla2b.analysis.SpecAnalyser;
+import de.tla2b.analysis.SymbolRenamer;
+import de.tla2b.analysis.TypeChecker;
+import de.tla2b.exceptions.ExpressionTranslationException;
+import de.tla2b.exceptions.TLA2BException;
import tla2sany.drivers.FrontEndException;
import tla2sany.drivers.InitException;
import tla2sany.drivers.SANY;
@@ -17,12 +16,13 @@ import tla2sany.semantic.ModuleNode;
import tla2sany.st.SyntaxTreeConstants;
import tla2sany.st.TreeNode;
import util.ToolIO;
-import de.be4.classicalb.core.parser.node.Start;
-import de.tla2b.analysis.SpecAnalyser;
-import de.tla2b.analysis.SymbolRenamer;
-import de.tla2b.analysis.TypeChecker;
-import de.tla2b.exceptions.ExpressionTranslationException;
-import de.tla2b.exceptions.TLA2BException;
+
+import java.io.File;
+import java.io.FileWriter;
+import java.io.IOException;
+import java.util.ArrayList;
+import java.util.HashSet;
+import java.util.Set;
public class ExpressionTranslator implements SyntaxTreeConstants {
@@ -58,17 +58,17 @@ public class ExpressionTranslator implements SyntaxTreeConstants {
tempFile = File.createTempFile("Testing", ".tla");
moduleName = tempFile.getName().substring(0,
- tempFile.getName().indexOf("."));
+ tempFile.getName().indexOf("."));
module = "----MODULE " + moduleName + " ----\n" + "Expression == "
- + tlaExpression + "\n====";
+ + tlaExpression + "\n====";
FileWriter fw = new FileWriter(tempFile);
fw.write(module);
fw.close();
} catch (IOException e) {
throw new ExpressionTranslationException(
- "Can not create temporary file in directory '" + dir + "'");
+ "Can not create temporary file in directory '" + dir + "'");
}
SpecObj spec = parseModuleWithoutSemanticAnalyse(moduleName, module);
@@ -114,7 +114,7 @@ public class ExpressionTranslator implements SyntaxTreeConstants {
public Start translateIncludingModel() throws TLA2BException {
SpecAnalyser specAnalyser = SpecAnalyser
- .createSpecAnalyserForTlaExpression(moduleNode);
+ .createSpecAnalyserForTlaExpression(moduleNode);
TypeChecker tc = translator.getTypeChecker();
tc.visitOpDefNode(specAnalyser.getExpressionOpdefNode());
@@ -128,13 +128,13 @@ public class ExpressionTranslator implements SyntaxTreeConstants {
public Start translate() {
SpecAnalyser specAnalyser = SpecAnalyser
- .createSpecAnalyserForTlaExpression(moduleNode);
+ .createSpecAnalyserForTlaExpression(moduleNode);
TypeChecker tc = new TypeChecker(moduleNode, specAnalyser);
try {
tc.start();
} catch (TLA2BException e) {
String message = "****TypeError****\n" + e.getLocalizedMessage()
- + "\n" + expr + "\n";
+ + "\n" + expr + "\n";
throw new ExpressionTranslationException(message);
}
SymbolRenamer symRenamer = new SymbolRenamer(moduleNode, specAnalyser);
@@ -146,14 +146,14 @@ public class ExpressionTranslator implements SyntaxTreeConstants {
}
public static ModuleNode parseModule(String moduleName, String module)
- throws de.tla2b.exceptions.FrontEndException {
+ throws de.tla2b.exceptions.FrontEndException {
SpecObj spec = new SpecObj(moduleName, null);
try {
SANY.frontEndMain(spec, moduleName, ToolIO.out);
} catch (FrontEndException e) {
// Error in Frontend, should never happens
throw new de.tla2b.exceptions.FrontEndException(
- "Frontend error! This should never happen.", spec);
+ "Frontend error! This should never happen.", spec);
}
if (spec.parseErrors.isFailure()) {
@@ -174,19 +174,19 @@ public class ExpressionTranslator implements SyntaxTreeConstants {
System.err.println(spec.getInitErrors());
throw new de.tla2b.exceptions.FrontEndException(
- allMessagesToString(ToolIO.getAllMessages()), spec);
+ allMessagesToString(ToolIO.getAllMessages()), spec);
}
if (n == null) { // Parse Error
// System.out.println("Rootmodule null");
throw new de.tla2b.exceptions.FrontEndException(
- allMessagesToString(ToolIO.getAllMessages()), spec);
+ allMessagesToString(ToolIO.getAllMessages()), spec);
}
return n;
}
private SpecObj parseModuleWithoutSemanticAnalyse(String moduleFileName,
- String module) {
+ String module) {
SpecObj spec = new SpecObj(moduleFileName, null);
try {
@@ -212,9 +212,9 @@ public class ExpressionTranslator implements SyntaxTreeConstants {
TreeNode n_operatorDefintion = n_body.heirs()[0];
TreeNode expr = n_operatorDefintion.heirs()[2];
searchVarInSyntaxTree(expr);
-
- // this code seems to assume that there is no variable clash between outer and nested variables
- // I guess the parser will then generate "Multiply-defined symbol ..." errors
+
+ // this code seems to assume that there is no variable clash between outer and nested variables
+ // I guess the parser will then generate "Multiply-defined symbol ..." errors
for (String noVariable : noVariables) {
variables.remove(noVariable);
}
@@ -222,6 +222,7 @@ public class ExpressionTranslator implements SyntaxTreeConstants {
}
private final static Set<String> KEYWORDS = new HashSet<>();
+
static {
KEYWORDS.add("BOOLEAN");
KEYWORDS.add("TRUE");
@@ -247,76 +248,77 @@ public class ExpressionTranslator implements SyntaxTreeConstants {
}
/**
- *
+ *
*/
private void searchVarInSyntaxTree(TreeNode treeNode) {
// System.out.println(treeNode.getKind() + " " + treeNode.getImage());
switch (treeNode.getKind()) {
- case N_GeneralId: {
- String con = treeNode.heirs()[1].getImage();
- if (!variables.contains(con) && !KEYWORDS.contains(con)) {
- variables.add(con);
+ case N_GeneralId: {
+ String con = treeNode.heirs()[1].getImage();
+ if (!variables.contains(con) && !KEYWORDS.contains(con)) {
+ variables.add(con);
+ }
+ break;
}
- break;
- }
- case N_IdentLHS: { // left side of a definition
- TreeNode[] children = treeNode.heirs();
- noVariables.add(children[0].getImage());
- break;
- }
- case N_IdentDecl: { // parameter of a LET definition
- // e.g. x in LET foo(x) == e
- noVariables.add(treeNode.heirs()[0].getImage());
- break;
- }
- case N_FunctionDefinition: {
- // the first child is the function name
- noVariables.add(treeNode.heirs()[0].getImage());
- break;
- }
- case N_UnboundQuant: { // TOOD: check: is this an unbounded quantifier with infinite domain or a quantifier that does not hide the quantified variables?
- TreeNode[] children = treeNode.heirs();
- for (int i = 1; i < children.length - 2; i = i + 2) {
- // System.out.println("N_UnboundQuant: "+children[i].getImage());
+ case N_IdentLHS: { // left side of a definition
+ TreeNode[] children = treeNode.heirs();
+ noVariables.add(children[0].getImage());
+ break;
}
- searchVarInSyntaxTree(treeNode.heirs()[children.length - 1]);
- break;
- }
- case N_UnboundOrBoundChoose: { // not sure the format is the same as N_QuantBound
- TreeNode[] children = treeNode.heirs();
- for (int i = 1; i < children.length - 2; i = i + 2) {
- String boundedVar = children[i].getImage();
- // typically children[i+1] is N_MaybeBound
- if (!noVariables.contains(boundedVar)) {
- noVariables.add(boundedVar);
- //System.out.println("CHOOSE quantified variable: " + boundedVar);
+ case N_IdentDecl: { // parameter of a LET definition
+ // e.g. x in LET foo(x) == e
+ noVariables.add(treeNode.heirs()[0].getImage());
+ break;
+ }
+ case N_FunctionDefinition: {
+ // the first child is the function name
+ noVariables.add(treeNode.heirs()[0].getImage());
+ break;
+ }
+ case
+ N_UnboundQuant: { // TOOD: check: is this an unbounded quantifier with infinite domain or a quantifier that does not hide the quantified variables?
+ TreeNode[] children = treeNode.heirs();
+ for (int i = 1; i < children.length - 2; i = i + 2) {
+ // System.out.println("N_UnboundQuant: "+children[i].getImage());
}
+ searchVarInSyntaxTree(treeNode.heirs()[children.length - 1]);
+ break;
}
- searchVarInSyntaxTree(treeNode.heirs()[children.length - 1]);
- break;
- }
- case N_QuantBound: {
- TreeNode[] children = treeNode.heirs();
- for (int i = 0; i < children.length - 2; i = i + 2) {
- String boundedVar = children[i].getImage();
+ case N_UnboundOrBoundChoose: { // not sure the format is the same as N_QuantBound
+ TreeNode[] children = treeNode.heirs();
+ for (int i = 1; i < children.length - 2; i = i + 2) {
+ String boundedVar = children[i].getImage();
+ // typically children[i+1] is N_MaybeBound
+ if (!noVariables.contains(boundedVar)) {
+ noVariables.add(boundedVar);
+ //System.out.println("CHOOSE quantified variable: " + boundedVar);
+ }
+ }
+ searchVarInSyntaxTree(treeNode.heirs()[children.length - 1]);
+ break;
+ }
+ case N_QuantBound: {
+ TreeNode[] children = treeNode.heirs();
+ for (int i = 0; i < children.length - 2; i = i + 2) {
+ String boundedVar = children[i].getImage();
+ if (!noVariables.contains(boundedVar)) {
+ noVariables.add(boundedVar);
+ // System.out.println("N_QuantBound: locally quantified variable" + boundedVar);
+ }
+ }
+ searchVarInSyntaxTree(treeNode.heirs()[children.length - 1]);
+ break;
+ }
+ case N_SubsetOf: { // { x \in S : e }
+ TreeNode[] children = treeNode.heirs();
+ String boundedVar = children[1].getImage(); // x
if (!noVariables.contains(boundedVar)) {
noVariables.add(boundedVar);
- // System.out.println("N_QuantBound: locally quantified variable" + boundedVar);
}
+ searchVarInSyntaxTree(treeNode.heirs()[3]); // S
+ searchVarInSyntaxTree(treeNode.heirs()[5]); // e
+ break;
}
- searchVarInSyntaxTree(treeNode.heirs()[children.length - 1]);
- break;
- }
- case N_SubsetOf: { // { x \in S : e }
- TreeNode[] children = treeNode.heirs();
- String boundedVar = children[1].getImage(); // x
- if (!noVariables.contains(boundedVar)) {
- noVariables.add(boundedVar);
- }
- searchVarInSyntaxTree(treeNode.heirs()[3]); // S
- searchVarInSyntaxTree(treeNode.heirs()[5]); // e
- break;
- }
}
diff --git a/src/main/java/de/tla2bAst/SimpleResolver.java b/src/main/java/de/tla2bAst/SimpleResolver.java
index c91f186..b69f723 100644
--- a/src/main/java/de/tla2bAst/SimpleResolver.java
+++ b/src/main/java/de/tla2bAst/SimpleResolver.java
@@ -1,11 +1,11 @@
package de.tla2bAst;
-import java.io.File;
-
import util.FilenameToStream;
+import java.io.File;
+
public class SimpleResolver implements FilenameToStream {
-
+
private File file;
public boolean isStandardModule(String arg0) {
@@ -22,4 +22,4 @@ public class SimpleResolver implements FilenameToStream {
return file.getAbsolutePath();
}
-}
\ No newline at end of file
+}
diff --git a/src/main/java/de/tla2bAst/Translator.java b/src/main/java/de/tla2bAst/Translator.java
index 2c85ea8..3a6b4c4 100644
--- a/src/main/java/de/tla2bAst/Translator.java
+++ b/src/main/java/de/tla2bAst/Translator.java
@@ -1,18 +1,5 @@
package de.tla2bAst;
-import java.io.BufferedReader;
-import java.io.BufferedWriter;
-import java.io.File;
-import java.io.FileNotFoundException;
-import java.io.FileReader;
-import java.io.IOException;
-import java.io.OutputStreamWriter;
-import java.io.PrintWriter;
-import java.io.UnsupportedEncodingException;
-import java.nio.charset.StandardCharsets;
-import java.nio.file.Files;
-import java.util.Hashtable;
-
import de.be4.classicalb.core.parser.BParser;
import de.be4.classicalb.core.parser.Definitions;
import de.be4.classicalb.core.parser.analysis.prolog.RecursiveMachineLoader;
@@ -22,13 +9,7 @@ import de.be4.classicalb.core.parser.node.Node;
import de.be4.classicalb.core.parser.node.Start;
import de.be4.classicalb.core.parser.util.PrettyPrinter;
import de.be4.classicalb.core.parser.util.SuffixIdentifierRenaming;
-import de.tla2b.analysis.InstanceTransformation;
-import de.tla2b.analysis.PredicateVsExpression;
-import de.tla2b.analysis.SpecAnalyser;
-import de.tla2b.analysis.SymbolRenamer;
-import de.tla2b.analysis.SymbolSorter;
-import de.tla2b.analysis.TypeChecker;
-import de.tla2b.analysis.UsedExternalFunctions;
+import de.tla2b.analysis.*;
import de.tla2b.config.ConfigfileEvaluator;
import de.tla2b.config.ModuleOverrider;
import de.tla2b.exceptions.FrontEndException;
@@ -39,15 +20,17 @@ import de.tla2b.translation.BMacroHandler;
import de.tla2b.translation.RecursiveFunctionHandler;
import de.tla2b.types.TLAType;
import de.tla2b.util.FileUtils;
-
import tla2sany.drivers.SANY;
import tla2sany.modanalyzer.SpecObj;
import tla2sany.semantic.ModuleNode;
-
import tlc2.tool.ModelConfig;
-
import util.ToolIO;
+import java.io.*;
+import java.nio.charset.StandardCharsets;
+import java.nio.file.Files;
+import java.util.Hashtable;
+
public class Translator implements TranslationGlobals {
private String moduleFileName;
private File moduleFile;
@@ -100,7 +83,7 @@ public class Translator implements TranslationGlobals {
* External interface
*/
public static String translateModuleString(String moduleName, String moduleString, String configString)
- throws TLA2BException {
+ throws TLA2BException {
Translator translator = new Translator(moduleName, moduleString, configString);
Start bAST = translator.getBAST();
PrettyPrinter pp = new PrettyPrinter();
@@ -171,13 +154,13 @@ public class Translator implements TranslationGlobals {
if (spec.parseErrors.isFailure()) {
throw new de.tla2b.exceptions.FrontEndException(
- allMessagesToString(ToolIO.getAllMessages()) + spec.parseErrors, spec);
+ allMessagesToString(ToolIO.getAllMessages()) + spec.parseErrors, spec);
}
if (spec.semanticErrors.isFailure()) {
throw new de.tla2b.exceptions.FrontEndException(
- // allMessagesToString(ToolIO.getAllMessages())
- "" + spec.semanticErrors, spec);
+ // allMessagesToString(ToolIO.getAllMessages())
+ "" + spec.semanticErrors, spec);
}
// RootModule
@@ -243,7 +226,7 @@ public class Translator implements TranslationGlobals {
RecursiveFunctionHandler recursiveFunctionHandler = new RecursiveFunctionHandler(specAnalyser);
BMacroHandler bMacroHandler = new BMacroHandler(specAnalyser, conEval);
bAstCreator = new BAstCreator(moduleNode, conEval, specAnalyser, usedExternalFunctions, predicateVsExpression,
- bMacroHandler, recursiveFunctionHandler);
+ bMacroHandler, recursiveFunctionHandler);
this.BAst = bAstCreator.getStartNode();
this.typeTable = bAstCreator.getTypeTable();
@@ -298,7 +281,7 @@ public class Translator implements TranslationGlobals {
in.close();
if (firstLine != null && !firstLine.startsWith("/*@ generated by TLA2B ")) {
System.err.println("Error: File " + machineFile.getName() + " already exists"
- + " and was not generated by TLA2B.\n" + "Delete or move this file.");
+ + " and was not generated by TLA2B.\n" + "Delete or move this file.");
System.exit(-1);
}
} catch (IOException e) {
@@ -332,7 +315,7 @@ public class Translator implements TranslationGlobals {
}
public static RecursiveMachineLoader parseAllMachines(final Start ast, final File f, final BParser bparser)
- throws BCompoundException {
+ throws BCompoundException {
final RecursiveMachineLoader rml = new RecursiveMachineLoader(f.getParent(), bparser.getContentProvider());
rml.loadAllMachines(f, ast, bparser.getDefinitions());
return rml;
--
GitLab