Select Git revision
BAstCreator.java
-
Jan Gruteser authoredJan Gruteser authored
Code owners
Assign users and groups as approvers for specific file changes. Learn more.
BAstCreator.java 86.33 KiB
package de.tla2bAst;
import de.be4.classicalb.core.parser.Definitions;
import de.be4.classicalb.core.parser.node.*;
import de.hhu.stups.sablecc.patch.PositionedNode;
import de.hhu.stups.sablecc.patch.SourcePosition;
import de.tla2b.analysis.*;
import de.tla2b.analysis.PredicateVsExpression.DefinitionType;
import de.tla2b.analysis.UsedExternalFunctions.EXTERNAL_FUNCTIONS;
import de.tla2b.config.ConfigfileEvaluator;
import de.tla2b.config.ValueObj;
import de.tla2b.exceptions.NotImplementedException;
import de.tla2b.global.*;
import de.tla2b.translation.BMacroHandler;
import de.tla2b.translation.RecursiveFunctionHandler;
import de.tla2b.types.*;
import de.tla2b.util.DebugUtils;
import tla2sany.semantic.*;
import tla2sany.st.Location;
import tlc2.tool.BuiltInOPs;
import tlc2.value.ValueConstants;
import tlc2.value.impl.*;
import java.util.*;
import java.util.Map.Entry;
public class BAstCreator extends BuiltInOPs
implements TranslationGlobals, ASTConstants, BBuildIns, Priorities, ValueConstants {
List<PMachineClause> machineClauseList;
ConfigfileEvaluator conEval;
final SpecAnalyser specAnalyser;
private final PredicateVsExpression predicateVsExpression;
private final BMacroHandler bMacroHandler;
private final RecursiveFunctionHandler recursiveFunctionHandler;
private List<OpDeclNode> bConstants;
private final ModuleNode moduleNode;
private UsedExternalFunctions usedExternalFunctions;
private final Definitions bDefinitions = new Definitions();
private Start start;
private final Hashtable<Node, TLAType> typeTable = new Hashtable<>();
private final HashSet<PositionedNode> sourcePosition = new HashSet<>();
private List<String> toplevelUnchangedVariableNames = new ArrayList<>();
public Start expressionStart;
/**
* Creates a B AST node for a TLA expression
*/
public BAstCreator(ModuleNode moduleNode, SpecAnalyser specAnalyser) {
this.moduleNode = moduleNode;
this.specAnalyser = specAnalyser;
this.bMacroHandler = new BMacroHandler();
this.predicateVsExpression = new PredicateVsExpression(moduleNode);
this.recursiveFunctionHandler = new RecursiveFunctionHandler(specAnalyser);
ExprNode expr = moduleNode.getOpDefs()[moduleNode.getOpDefs().length - 1].getBody();
if (expressionIsAPredicate(expr)) {
APredicateParseUnit predicateParseUnit = new APredicateParseUnit();
predicateParseUnit.setPredicate(visitExprNodePredicate(expr));
expressionStart = new Start(predicateParseUnit, new EOF());
} else {
AExpressionParseUnit expressionParseUnit = new AExpressionParseUnit();
expressionParseUnit.setExpression(visitExprNodeExpression(expr));
expressionStart = new Start(expressionParseUnit, new EOF());
}