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

support free variables in expressions including module

parent a3b3fb00
No related branches found
No related tags found
No related merge requests found
Pipeline #142681 passed
......@@ -74,18 +74,24 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
((AbstractHasFollowers) t).addFollower(con);
}
} else {
// if constant already has a type: keep type; otherwise add an untyped type
if (con.getToolObject(TYPE_ID) == null) {
UntypedType u = new UntypedType();
con.setToolObject(TYPE_ID, u);
u.addFollower(con);
}
}
}
OpDeclNode[] vars = moduleNode.getVariableDecls();
for (OpDeclNode var : vars) {
// if variable already has a type: keep type; otherwise add an untyped type
if (var.getToolObject(TYPE_ID) == null) {
UntypedType u = new UntypedType();
var.setToolObject(TYPE_ID, u);
u.addFollower(var);
}
}
evalDefinitions(moduleNode.getOpDefs());
......@@ -312,7 +318,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
TLAType c = (TLAType) con.getToolObject(TYPE_ID);
if (c == null) {
throw new RuntimeException(con.getName() + " has no type yet!");
throw new TypeErrorException(con.getName() + " has no type yet!");
}
try {
TLAType result = expected.unify(c);
......@@ -335,7 +341,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
// 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!");
throw new TypeErrorException(vName + " has no type yet!");
}
}
try {
......
......@@ -6,6 +6,7 @@ import de.tla2b.analysis.SymbolRenamer;
import de.tla2b.analysis.TypeChecker;
import de.tla2b.exceptions.ExpressionTranslationException;
import de.tla2b.exceptions.TLA2BException;
import de.tla2b.exceptions.TypeErrorException;
import tla2sany.drivers.FrontEndException;
import tla2sany.drivers.InitException;
import tla2sany.drivers.SANY;
......@@ -56,9 +57,7 @@ public class ExpressionTranslator implements SyntaxTreeConstants {
String module;
try {
tempFile = File.createTempFile("Testing", ".tla");
moduleName = tempFile.getName().substring(0,
tempFile.getName().indexOf("."));
moduleName = tempFile.getName().substring(0,tempFile.getName().indexOf("."));
module = "----MODULE " + moduleName + " ----\n" + "Expression == "
+ tlaExpression + "\n====";
......@@ -113,11 +112,26 @@ public class ExpressionTranslator implements SyntaxTreeConstants {
}
public Start translateIncludingModel() throws TLA2BException {
SpecAnalyser specAnalyser = SpecAnalyser
.createSpecAnalyserForTlaExpression(moduleNode);
SpecAnalyser specAnalyser = SpecAnalyser.createSpecAnalyserForTlaExpression(moduleNode);
TypeChecker tc = translator.getTypeChecker();
try {
// here we add typing for known identifiers from the module
tc.visitOpDefNode(specAnalyser.getExpressionOpdefNode());
} catch (TypeErrorException e) {
// ignore type errors; new free variables will always throw an exception here
// (they have no type, which is correct as they are not part of the module);
// real type errors are checked below
}
TypeChecker tc2 = new TypeChecker(moduleNode, specAnalyser);
try {
// here we add the typing for new variables
// the types of module variables are also checked
tc2.start();
} catch (TypeErrorException e) {
String message = "****TypeError****\n" + e.getLocalizedMessage() + "\n" + expr + "\n";
throw new ExpressionTranslationException(message);
}
SymbolRenamer symRenamer = new SymbolRenamer(moduleNode, specAnalyser);
symRenamer.start();
BAstCreator bASTCreator = new BAstCreator(moduleNode, specAnalyser);
......
package de.tla2b.expression;
import de.tla2b.exceptions.TypeErrorException;
import de.tla2b.exceptions.ExpressionTranslationException;
import org.junit.Test;
import static de.tla2b.util.TestUtil.compareExprIncludingModel;
......@@ -16,7 +16,7 @@ public class ModuleAndExpressionTest {
compareExprIncludingModel("k = 1", "k = 1", module);
}
@Test(expected = TypeErrorException.class)
@Test(expected = ExpressionTranslationException.class)
public void testTypeError() throws Exception {
String module = "---- MODULE Testing ----\n"
+ "CONSTANTS k \n"
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment