Skip to content
Snippets Groups Projects
Select Git revision
  • 1633b33ad96db284ef334865744525727e242657
  • main default protected
2 results

iterate_iqtree.py

Blame
  • 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());
    		}