BAstCreator.java

package de.tla2bAst;

import de.be4.classicalb.core.parser.Definitions;
import de.be4.classicalb.core.parser.analysis.prolog.NodeFileNumbers;
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;
import java.util.stream.Collectors;

public class BAstCreator extends BuiltInOPs implements TranslationGlobals, BBuildIns, ValueConstants {

	private List<PMachineClause> machineClauseList;
	private ConfigfileEvaluator conEval;
	private 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 final Start start;
	private final Map<Node, TLAType> types = new HashMap<>();
	private final Set<PositionedNode> sourcePosition = new HashSet<>();
	private final NodeFileNumbers nodeFileNumbers = new NodeFileNumbers();
	private final List<String> filesOrderedById = new ArrayList<>();
	private List<String> toplevelUnchangedVariableNames = new ArrayList<>();

	/**
	 * 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)) {
			start = new Start(new APredicateParseUnit(visitExprNodePredicate(expr)), new EOF());
		} else {
			start = new Start(new AExpressionParseUnit(visitExprNodeExpression(expr)), new EOF());
		}
	}

	private boolean expressionIsAPredicate(ExprNode expr) {