Skip to content
Snippets Groups Projects
Commit 6ad55775 authored by Jan Gruteser's avatar Jan Gruteser
Browse files

minor simplifications

parent 7ce92491
No related branches found
No related tags found
No related merge requests found
Pipeline #148720 passed
...@@ -65,10 +65,6 @@ public class PredicateVsExpression extends BuiltInOPs implements BBuildIns { ...@@ -65,10 +65,6 @@ public class PredicateVsExpression extends BuiltInOPs implements BBuildIns {
OpApplNode pair = (OpApplNode) opApplNode.getArgs()[0]; OpApplNode pair = (OpApplNode) opApplNode.getArgs()[0];
return visitSemanticNode(pair.getArgs()[1]); return visitSemanticNode(pair.getArgs()[1]);
} }
default: {
return DefinitionType.EXPRESSION;
}
} }
} else if (kind == UserDefinedOpKind) { } else if (kind == UserDefinedOpKind) {
return visitUserdefinedOp(opApplNode); return visitUserdefinedOp(opApplNode);
......
package de.tla2b.analysis; package de.tla2b.analysis;
import de.tla2b.global.BBuiltInOPs; import de.tla2b.global.BBuiltInOPs;
import de.tla2b.global.TranslationGlobals;
import tla2sany.semantic.*; import tla2sany.semantic.*;
import tlc2.tool.BuiltInOPs; import tlc2.tool.BuiltInOPs;
...@@ -10,7 +9,9 @@ import java.util.HashSet; ...@@ -10,7 +9,9 @@ import java.util.HashSet;
import java.util.Map; import java.util.Map;
import java.util.Set; import java.util.Set;
public class SymbolRenamer extends BuiltInOPs implements TranslationGlobals { import static de.tla2b.global.TranslationGlobals.NEW_NAME;
public class SymbolRenamer extends BuiltInOPs {
private final static Set<String> KEYWORDS = new HashSet<>(); private final static Set<String> KEYWORDS = new HashSet<>();
...@@ -286,7 +287,7 @@ public class SymbolRenamer extends BuiltInOPs implements TranslationGlobals { ...@@ -286,7 +287,7 @@ public class SymbolRenamer extends BuiltInOPs implements TranslationGlobals {
if (BBUILTIN_OPERATOR.containsKey(newName)) { if (BBUILTIN_OPERATOR.containsKey(newName)) {
// a B built-in operator is defined outside a standard module // a B built-in operator is defined outside a standard module
if (!STANDARD_MODULES.contains(def.getSource().getOriginallyDefinedInModuleNode().getName().toString())) { if (!BBuiltInOPs.isBBuiltInOp(def)) {
return incName(BBUILTIN_OPERATOR.get(newName)); return incName(BBUILTIN_OPERATOR.get(newName));
} }
} }
......
...@@ -89,8 +89,8 @@ public class TypeChecker extends BuiltInOPs implements BBuildIns, TranslationGlo ...@@ -89,8 +89,8 @@ public class TypeChecker extends BuiltInOPs implements BBuildIns, TranslationGlo
if (!bConstList.contains(con)) if (!bConstList.contains(con))
continue; continue;
TLAType defType = (TLAType) entry.getValue().getToolObject(TYPE_ID); TLAType defType = getType(entry.getValue());
TLAType conType = (TLAType) con.getToolObject(TYPE_ID); TLAType conType = getType(con);
try { try {
setType(con, defType.unify(conType)); setType(con, defType.unify(conType));
} catch (UnificationException e) { } catch (UnificationException e) {
......
package de.tla2b.config; package de.tla2b.config;
import de.tla2b.global.TranslationGlobals;
import de.tla2b.types.TLAType; import de.tla2b.types.TLAType;
import tla2sany.semantic.AbortException; import tla2sany.semantic.AbortException;
import tla2sany.semantic.NumeralNode; import tla2sany.semantic.NumeralNode;
import tla2sany.st.TreeNode; import tla2sany.st.TreeNode;
import tlc2.value.impl.Value; import tlc2.value.impl.Value;
public class TLCValueNode extends NumeralNode implements TranslationGlobals { public class TLCValueNode extends NumeralNode {
private final Value value; private final Value value;
private final TLAType type; private final TLAType type;
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment