InstanceTransformation.java

package de.tla2b.analysis;

import de.tla2b.global.BBuiltInOPs;
import tla2sany.semantic.*;
import tlc2.tool.BuiltInOPs;
import util.UniqueString;

import java.util.Hashtable;

public class InstanceTransformation extends BuiltInOPs implements ASTConstants {

	final OpDefNode[] defs;
	final Hashtable<String, OpDefNode> defsHash;
	private final int substitutionId = 11;


	public InstanceTransformation(ModuleNode moduleNode) {
		defs = moduleNode.getOpDefs();
		defsHash = new Hashtable<>();
		for (OpDefNode def : defs) {
			defsHash.put(def.getName().toString(), def);
		}
	}

	public void start() {
		for (OpDefNode def : defs) {
			if (def.getSource() != def
				&& !BBuiltInOPs.contains(def.getSource().getName())) {
				// instance
				String defName = def.getName().toString();

				if (def.getBody() instanceof SubstInNode) {
					String prefix = defName.substring(0,
						defName.lastIndexOf('!') + 1);
					def.setParams(generateNewParams(def.getParams()));
					ExprNode body;
					try {
						body = generateNewExprNode(def.getBody(), prefix);
					} catch (AbortException e) {
						throw new RuntimeException();
					}
					def.setBody(body);
				}
			}
		}
	}

	private ExprOrOpArgNode generateNewExprOrOpArgNode(ExprOrOpArgNode n,
	                                                   String prefix) throws AbortException {
		if (n instanceof ExprNode) {
			return generateNewExprNode((ExprNode) n, prefix);
		} else {
			throw new RuntimeException("OpArgNode not implemented jet");
		}
	}

	private ExprNode generateNewExprNode(ExprNode n, String prefix)
		throws AbortException {
		switch (n.getKind()) {
			case OpApplKind: {
				return generateNewOpApplNode((OpApplNode) n, prefix);
			}

			case NumeralKind: {
				NumeralNode num = (NumeralNode) n;
				return new NumeralNode(num.toString(), n.getTreeNode());
			}

			case DecimalKind: {
				String[] image = n.toString().split("\\.");