PredicateVsExpression.java

package de.tla2b.analysis;

import de.tla2b.global.BBuildIns;
import de.tla2b.global.BBuiltInOPs;
import de.tla2b.global.TranslationGlobals;
import tla2sany.semantic.*;
import tlc2.tool.BuiltInOPs;

import java.util.HashMap;

public class PredicateVsExpression extends BuiltInOPs implements ASTConstants,
	BBuildIns, TranslationGlobals {

	private final HashMap<OpDefNode, DefinitionType> definitionsTypeMap;

	public enum DefinitionType {
		PREDICATE, EXPRESSION
	}

	public DefinitionType getDefinitionType(OpDefNode def) {
		return definitionsTypeMap.get(def);
	}

	public PredicateVsExpression(ModuleNode moduleNode) {
		this.definitionsTypeMap = new HashMap<>();
		OpDefNode[] defs = moduleNode.getOpDefs();

		for (OpDefNode def : defs) {
			DefinitionType type = visitSemanticNode(def.getBody());
			definitionsTypeMap.put(def, type);
		}

	}

	private DefinitionType visitSemanticNode(SemanticNode s) {
		switch (s.getKind()) {
			case OpApplKind: {
				return visitOppApplNode((OpApplNode) s);
			}

			case LetInKind: {
				LetInNode letInNode = (LetInNode) s;
				return visitSemanticNode(letInNode.getBody());
			}

		}

		return DefinitionType.EXPRESSION;
	}

	private DefinitionType visitOppApplNode(OpApplNode opApplNode) {
		int kind = opApplNode.getOperator().getKind();

		if (kind == BuiltInKind) {
			switch (getOpCode(opApplNode.getOperator().getName())) {
				case OPCODE_eq: // =
				case OPCODE_noteq: // /=
				case OPCODE_cl: // $ConjList
				case OPCODE_land: // \land
				case OPCODE_dl: // $DisjList
				case OPCODE_lor: // \/
				case OPCODE_equiv: // \equiv
				case OPCODE_implies: // =>
				case OPCODE_lnot: // \lnot
				case OPCODE_be: // \E x \in S : P
				case OPCODE_bf: // \A x \in S : P
				case OPCODE_in: // \in
				case OPCODE_subseteq: // \subseteq {1,2} <: {1,2,3}
				case OPCODE_unchanged: {
					return DefinitionType.PREDICATE;