org.eclipse.viatra2.loaders.vtcl_lpgparser/src/org/eclipse/viatra2/lpgparser/typechecker/VTCLTypeChecker.java

/**
 * Copyright (c) 2008 OptXware Research and Development LLC.
 * All rights reserved.   This program and the accompanying materials
 * are made available under the terms of the Eclipse Public License v1.0
 * which accompanies this distribution, and is available at
 * http://www.eclipse.org/legal/epl-v10.html
 *
 * Contributors:
 *   Daniel Varro - Initial API and implementation
 */
package org.eclipse.viatra2.lpgparser.typechecker;

import java.io.File;
import java.io.IOException;
import java.util.ArrayList;
import java.util.HashMap;
import java.util.List;
import java.util.Map;

import org.eclipse.emf.ecore.EObject;
import org.eclipse.emf.ecore.resource.Resource;
import org.eclipse.emf.ecore.resource.ResourceSet;
import org.eclipse.emf.ecore.resource.impl.ResourceSetImpl;
import org.eclipse.emf.ecore.xmi.XMIResource;
import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl;
import org.eclipse.emf.ecore.xmi.impl.XMIResourceImpl;
import org.eclipse.viatra2.core.IModelElement;
import org.eclipse.viatra2.core.IModelManager;
import org.eclipse.viatra2.core.IModelSpace;
import org.eclipse.viatra2.errors.VPMRuntimeException;
import org.eclipse.viatra2.errors.info.ErrorInformation;
import org.eclipse.viatra2.errors.info.ErrorInformation.ErrorKind;
import org.eclipse.viatra2.errors.info.ErrorInformation.ErrorSeverity;
import org.eclipse.viatra2.errors.info.Location;
import org.eclipse.viatra2.framework.FrameworkManager;
import org.eclipse.viatra2.gtasm.typerules.BinaryTypeJudgement;
import org.eclipse.viatra2.gtasm.typerules.CustomTypeJudgement;
import org.eclipse.viatra2.gtasm.typerules.RuleSet;
import org.eclipse.viatra2.gtasm.typerules.TypeJudgement;
import org.eclipse.viatra2.gtasm.typerules.TypeRule;
import org.eclipse.viatra2.gtasm.typerules.TyperulesPackage;
import org.eclipse.viatra2.gtasm.typerules.UnaryTypeJudgement;
import org.eclipse.viatra2.gtasmmodel.gtasm.metamodel.asm.core.AnnotatedElement;
import org.eclipse.viatra2.gtasmmodel.gtasm.metamodel.asm.core.Annotation;
import org.eclipse.viatra2.gtasmmodel.gtasm.metamodel.asm.definitions.ASMFunction;
import org.eclipse.viatra2.gtasmmodel.gtasm.metamodel.asm.definitions.DefinitionsFactory;
import org.eclipse.viatra2.gtasmmodel.gtasm.metamodel.asm.definitions.InitialValue;
import org.eclipse.viatra2.gtasmmodel.gtasm.metamodel.asm.definitions.Rule;
import org.eclipse.viatra2.gtasmmodel.gtasm.metamodel.asm.definitions.SymbolicRuleParameter;
import org.eclipse.viatra2.gtasmmodel.gtasm.metamodel.asm.definitions.TypeConstant;
import org.eclipse.viatra2.gtasmmodel.gtasm.metamodel.asm.definitions.Variable;
import org.eclipse.viatra2.gtasmmodel.gtasm.metamodel.asm.definitions.VariableDefinition;
import org.eclipse.viatra2.gtasmmodel.gtasm.metamodel.asm.enums.ValueKind;
import org.eclipse.viatra2.gtasmmodel.gtasm.metamodel.asm.simpleRules.CallRule;
import org.eclipse.viatra2.gtasmmodel.gtasm.metamodel.asm.simpleRules.GTRuleInvocation;
import org.eclipse.viatra2.gtasmmodel.gtasm.metamodel.asm.simpleRules.RuleUpdate;
import org.eclipse.viatra2.gtasmmodel.gtasm.metamodel.asm.simpleRules.RuleUpdateASMFunction;
import org.eclipse.viatra2.gtasmmodel.gtasm.metamodel.asm.simpleRules.RuleUpdateVariable;
import org.eclipse.viatra2.gtasmmodel.gtasm.metamodel.asm.terms.ASMFunctionInvocation;
import org.eclipse.viatra2.gtasmmodel.gtasm.metamodel.asm.terms.FunctionInvocation;
import org.eclipse.viatra2.gtasmmodel.gtasm.metamodel.asm.terms.GTPatternCall;
import org.eclipse.viatra2.gtasmmodel.gtasm.metamodel.asm.terms.ModelElementQuery;
import org.eclipse.viatra2.gtasmmodel.gtasm.metamodel.asm.terms.NativeFunctionInvocation;
import org.eclipse.viatra2.gtasmmodel.gtasm.metamodel.asm.terms.Term;
import org.eclipse.viatra2.gtasmmodel.gtasm.metamodel.asm.terms.VariableReference;
import org.eclipse.viatra2.gtasmmodel.gtasm.metamodel.asm.terms.builtInFunctions.ArithmeticOperation;
import org.eclipse.viatra2.gtasmmodel.gtasm.metamodel.asm.terms.builtInFunctions.ConversionOperation;
import org.eclipse.viatra2.gtasmmodel.gtasm.metamodel.asm.terms.builtInFunctions.RelationalOperation;
import org.eclipse.viatra2.gtasmmodel.gtasm.metamodel.gt.GTPattern;
import org.eclipse.viatra2.gtasmmodel.gtasm.metamodel.gt.GTPatternBody;
import org.eclipse.viatra2.gtasmmodel.gtasm.metamodel.gt.GTRule;
import org.eclipse.viatra2.gtasmmodel.gtasm.metamodel.gt.PatternVariable;
import org.eclipse.viatra2.gtasmmodel.gtasm.metamodel.gt.PatternVariableAssignment;
import org.eclipse.viatra2.gtasmmodel.vpm.editmodel.Entity;
import org.eclipse.viatra2.gtasmmodel.vpm.editmodel.ModelElement;
import org.eclipse.viatra2.gtasmmodel.vpm.editmodel.Relation;
import org.eclipse.viatra2.gtasmmodel.vpm.editmodel.Relationship;
import org.eclipse.viatra2.lpgparser.loader.VTCLMessages;
import org.eclipse.viatra2.lpgparser.modelbuilder.ModelBuilderHelper;

/**
 * This class is responsible for type checking of VTCL programs.
 * @author Daniel Varro
 */
public class VTCLTypeChecker {
	private static final String PARSER_MARKER = "org.eclipse.viatra2.loaders.vtclparsermarker";

	private IModelSpace modelSpace;
	private IModelManager modelManager;
	private TypeResolver typeResolver = new TypeResolver();
	// private TypeAssignments typeAssignments = new TypeAssignments();
	private RuleSet typeRuleSet = null;
	private Map<String, List<CustomTypeJudgement>> customTypeRuleMap = null;
	private Map<StringTriple, BinaryTypeJudgement> binaryTypeRuleMap = null;
	private Map<StringPair, UnaryTypeJudgement> unaryTypeRuleMap = null;

	private List<Term> termsToCheck = new ArrayList<Term>();
	private List<GTRuleInvocation> gtRuleInvocsToCheck = new ArrayList<GTRuleInvocation>();
	private List<CallRule> asmCallRuleToCheck = new ArrayList<CallRule>();
	private List<ASMFunctionInvocation> asmFunInvocsToCheck = new ArrayList<ASMFunctionInvocation>();
	private List<NativeFunctionInvocation> nativeFunInvocsToCheck = new ArrayList<NativeFunctionInvocation>();
	private List<GTPatternCall> patternCallToCheck = new ArrayList<GTPatternCall>();
	private List<RuleUpdate> updateRulesToCheck = new ArrayList<RuleUpdate>();
	private List<InitialValue> initValuesToCheck = new ArrayList<InitialValue>();
	private List<VariableDefinition> varDefsToCheck = new ArrayList<VariableDefinition>();
	private List<GTPattern> gtPatternDefToCheck = new ArrayList<GTPattern>();

	protected enum AbstractionKind {
		FIRST, SECOND, BOTH
	};

	public VTCLTypeChecker(IModelSpace aModelSpace) {
		modelSpace = aModelSpace;
		modelSpace = aModelSpace;
		modelSpace = aModelSpace;
		modelSpace = aModelSpace;
		modelSpace = aModelSpace;
		modelSpace = aModelSpace;
		modelSpace = aModelSpace;
		modelSpace = aModelSpace;
		modelManager = modelSpace.getModelManager();
		typeRuleSet = null;
		try {
			initializeTypeRuleSet();
		} catch (VPMRuntimeException e) {
			// This exception should never be thrown
			e.printStackTrace();
		}
	}

	public TypeResolver getTypeResolver() {
		return typeResolver;
	}

	/**
	 * Returns the type assignment repository
	 * @return the type assignment repository
	 */
	/*
	 * public TypeAssignments getTypeAssignments() { return typeAssignments; }
	 */

	public List<Term> getTermsToCheck() {
		return termsToCheck;
	}

	public List<ASMFunctionInvocation> getAsmFunInvocsToCheck() {
		return asmFunInvocsToCheck;
	}

	public List<NativeFunctionInvocation> getNativeFunInvocsToCheck() {
		return nativeFunInvocsToCheck;
	}

	public List<GTRuleInvocation> getGtRuleInvocsToCheck() {
		return gtRuleInvocsToCheck;
	}

	public List<CallRule> getAsmCallRuleToCheck() {
		return asmCallRuleToCheck;
	}

	public List<GTPatternCall> getPatternCallToCheck() {
		return patternCallToCheck;
	}

	public List<RuleUpdate> getUpdateRulesToCheck() {
		return updateRulesToCheck;
	}

	public List<InitialValue> getInitValuesToCheck() {
		return initValuesToCheck;
	}

	public List<VariableDefinition> getVarDefsToCheck() {
		return varDefsToCheck;
	}

	public List<GTPattern> getPatternDefToCheck() {
		return gtPatternDefToCheck;
	}

	private List<ErrorInformation> typeErrorInfos = new ArrayList<ErrorInformation>();

	public List<ErrorInformation> getAllTypeErrorInfos() {
		return typeErrorInfos;
	}

	public void clearAllTypeErrors() {
		typeErrorInfos.clear();
	}

	/**
	 * Creates an ErrorInformation
	 * @param annotations
	 *            : location information of the error
	 * @param errorString
	 *            : textual representation of the error (VTCLMessages should be
	 *            used)
	 * @param errorSeverity
	 *            : severity of the error
	 * @param context
	 *            : list of contextual information
	 */
	public void addTypeError(List<Annotation> annotations, String errorString,
			ErrorSeverity errorSeverity, String[] context) {
		Location location = ModelBuilderHelper.createLocationInfo(annotations);
		ErrorInformation errorInfo = new ErrorInformation(errorString,
				PARSER_MARKER, ErrorKind.VALIDATION_ERROR, location,
				errorSeverity);
		// Bind contextual parameters of error strings
		errorInfo.bind(context);
		typeErrorInfos.add(errorInfo);
	}

	public void loadTypeRules(File file) throws VPMRuntimeException {
		// Create a resource set.
		ResourceSet resourceSet = new ResourceSetImpl();
		resourceSet.getPackageRegistry().put(TyperulesPackage.eNS_URI,
				TyperulesPackage.eINSTANCE);
		Resource res = resourceSet.getResource(org.eclipse.emf.common.util.URI
				.createFileURI(file.getAbsolutePath()), true);
		try {
			res.load(null);
		} catch (IOException e) {
			throw new VPMRuntimeException("Type rules cannot be loaded");
		}
		if (res.getContents().get(0) instanceof RuleSet) {
			RuleSet rs = (RuleSet) res.getContents().get(0);
			// The new rule set extends the existing one
			rs.setExtends(typeRuleSet);
			// Save the new rule set
			typeRuleSet = rs;
		}
		// TODO: Filter deactivated rules
		// filterDeactivatedTypeRules();
	}

	public void initializeTypeChecker() {
		clearAllTypeErrors();
		clearLists();
	}

	/**
	 * Empties to lists containing various task elements
	 */
	private void clearLists() {
		termsToCheck.clear();
		asmCallRuleToCheck.clear();
		gtRuleInvocsToCheck.clear();
		asmFunInvocsToCheck.clear();
		nativeFunInvocsToCheck.clear();
		patternCallToCheck.clear();
		updateRulesToCheck.clear();
		initValuesToCheck.clear();
		varDefsToCheck.clear();
		gtPatternDefToCheck.clear();
	}

	/**
	 * This method initiates type checking for all - Terms collected in
	 * termsToCheck - CallRules collected in asmCallRuleToCheck -
	 * GTRuleInvocations collected in gtRuleInvocsToCheck -
	 * ASMFunctionInvocations collected in asmFunInvocsToCheck -
	 * NativeFunctionInvocations collected in nativeFunInvocsToCheck -
	 * GTPatternCalls (from pattern composition) collected in patternCallToCheck
	 */
	public void doTypeChecking() {
		try {
			assert (typeErrorInfos.isEmpty()) : "Type error list is not empty";
			// Infer types for pattern variable references
			for (GTPattern patternDef : gtPatternDefToCheck) {
				typeCheckPatternDefinition(patternDef);
			}
			for (Term term : termsToCheck) {
				typeCheckTerm(term);
			}
			for (CallRule callRule : asmCallRuleToCheck) {
				typeCheckCallRule(callRule);
			}
			for (GTRuleInvocation gtRuleInvoc : gtRuleInvocsToCheck) {
				typeCheckGTRuleCall(gtRuleInvoc);
			}
			for (ASMFunctionInvocation asmFunInvoc : asmFunInvocsToCheck) {
				typeCheckAsmFunctionInvocation(asmFunInvoc);
			}
			for (NativeFunctionInvocation nativeFunInvoc : nativeFunInvocsToCheck) {
				typeCheckNativeFunctionInvocation(nativeFunInvoc);
			}
			for (GTPatternCall patternCall : patternCallToCheck) {
				typeCheckPatternCall(patternCall);
			}
			for (RuleUpdate updateRule : updateRulesToCheck) {
				typeCheckUpdateRule(updateRule);
			}
			for (InitialValue initValue : initValuesToCheck) {
				typeCheckInitialValue(initValue);
			}
			for (VariableDefinition varDef : varDefsToCheck) {
				typeCheckVariableDefinition(varDef);
			}
		} finally {
			clearLists();
		}
	}

	protected void initializeTypeRuleSet() throws VPMRuntimeException {
		String bundleStr = "org.eclipse.viatra2.gtasm.typing.model";
		String fileName = "/model/VTCLCore.typerules";
		File file = FrameworkManager.getFileFromBundle(bundleStr, fileName);
		if (file == null) {
			throw new VPMRuntimeException("Type rule file cannot be found");
		}
		// Create a resource set.

		// added by Istvan to make it work in headless mode
		Resource.Factory.Registry.INSTANCE.getExtensionToFactoryMap().put
	       ("typerules",
	        new XMIResourceFactoryImpl()
	        {
	          public Resource createResource(org.eclipse.emf.common.util.URI uri)
	          {
	            XMIResource xmiResource = new XMIResourceImpl(uri);
	            return xmiResource;
	          }
	        });


		ResourceSet resourceSet = new ResourceSetImpl();
		resourceSet.getPackageRegistry().put(TyperulesPackage.eNS_URI,
				TyperulesPackage.eINSTANCE);
		Resource res = resourceSet.getResource(org.eclipse.emf.common.util.URI
				.createFileURI(file.getAbsolutePath()), true);
		try {
			res.load(null);
		} catch (IOException e) {
			throw new VPMRuntimeException("Type rules cannot be loaded");
		}
		if (res.getContents().get(0) instanceof RuleSet) {
			typeRuleSet = (RuleSet) res.getContents().get(0);
		}

		if (typeRuleSet != null) {
			binaryTypeRuleMap = new HashMap<StringTriple, BinaryTypeJudgement>();
			unaryTypeRuleMap = new HashMap<StringPair, UnaryTypeJudgement>();
			customTypeRuleMap = new HashMap<String, List<CustomTypeJudgement>>();
			for (TypeRule typeRule : typeRuleSet.getTyperules()) {
				List<CustomTypeJudgement> customList = null;
				for (TypeJudgement judgement : typeRule.getJudgements()) {
					if (judgement instanceof BinaryTypeJudgement) {
						BinaryTypeJudgement binaryJudge = (BinaryTypeJudgement) judgement;
						StringTriple triple = new StringTriple(typeRule
								.getOperator(), binaryJudge.getFirstOperand(),
								binaryJudge.getSecondOperand());
						binaryTypeRuleMap.put(triple, binaryJudge);
					} else if (judgement instanceof UnaryTypeJudgement) {
						UnaryTypeJudgement unaryJudge = (UnaryTypeJudgement) judgement;
						StringPair pair = new StringPair(
								typeRule.getOperator(), unaryJudge.getOperand());
						unaryTypeRuleMap.put(pair, unaryJudge);

					} else if (judgement instanceof CustomTypeJudgement) {
						CustomTypeJudgement customJudge = (CustomTypeJudgement) judgement;
						customList = customTypeRuleMap.get(typeRule
								.getOperator());
						if (customList == null) {
							customList = new ArrayList<CustomTypeJudgement>();
						}
						customList.add(customJudge);

					}
				}
				customTypeRuleMap.put(typeRule.getOperator(), customList);
			}
		}
	}

	protected void typeCheckPatternDefinition(GTPattern patternDef) {
		// Process pattern parameters
		for (PatternVariable patternVar : patternDef.getSymParameters()) {
			TypeConstant typeConst = DefinitionsFactory.eINSTANCE
					.createTypeConstant();
			typeConst.setKind(ValueKind.UNDEF_LITERAL);
			typeConst.setFqn(VTCLTypeNameConstants.TOP);
			// Infer types for all references
			for (Object varRefObj : patternVar.getReferences()) {
				VariableReference varRef = (VariableReference) varRefObj;
				typeConst = inferTypeForPatternVariableRef(varRef, typeConst);
			}
			inferTypeForPatternVariableDef(patternVar, typeConst);
		}
		// Process all bodies
		for (GTPatternBody body : patternDef.getPatternBodies()) {
			// Process local pattern variables
			for (PatternVariable patternVar : body.getLocalVariables()) {
				TypeConstant typeConst = DefinitionsFactory.eINSTANCE
						.createTypeConstant();
				typeConst.setKind(ValueKind.UNDEF_LITERAL);
				typeConst.setFqn(VTCLTypeNameConstants.TOP);
				for (Object varRefObj : patternVar.getReferences()) {
					VariableReference varRef = (VariableReference) varRefObj;
					typeConst = inferTypeForPatternVariableRef(varRef,
							typeConst);
				}
				inferTypeForPatternVariableDef(patternVar, typeConst);
			}
		}
	}

	/**
	 * @param varRef
	 * @param prevTypeConst
	 * @return
	 */
	protected TypeConstant inferTypeForPatternVariableRef(
			VariableReference varRef, TypeConstant prevTypeConst) {
		EObject parent = varRef.eContainer();
		String typeStr = null;
		ValueKind kind;
		// Handling model elements (entity, relation) in pattern body
		if (parent instanceof ModelElement) {
			ModelElement element = (ModelElement) parent;
			// If it is the first variable reference of an entity/relation
			if (varRef.equals(element.getVariableReferences().get(0))
					|| prevTypeConst == null) {
				// Check if type is defined
				if (!element.getType().isEmpty()) {
					ModelElement type = element.getType().get(0);
					typeStr = type.getName();
				} else {
					if (parent instanceof Entity) {
						typeStr = VTCLTypeNameConstants.ENTITY;
					} else if (parent instanceof Relation) {
						typeStr = VTCLTypeNameConstants.RELATION;
					} else {
						typeStr = VTCLTypeNameConstants.MODELELEMENT;
					}
				}
				// Determine the LUB of variable reference types
				if (prevTypeConst != null
						&& !prevTypeConst.getKind().equals(
								ValueKind.UNDEF_LITERAL)) {
					// TODO: Distinguish between variables in OR patterns and
					// within the same body
					typeStr = typeResolver.leastUpperBound(modelManager,
							typeStr, prevTypeConst.getFqn());
				}
			}
			// If variable reference is not the first
			else {
				typeStr = typeResolver.greatestLowerBound(modelManager,
						VTCLTypeNameConstants.MODELELEMENT, prevTypeConst
								.getFqn());
			}
			kind = ValueKind.MODELELEMENT_LITERAL;
			// Schedule variable reference for type checking
			termsToCheck.add(varRef);
		}
		// Relationship definition
		else if (parent instanceof Relationship) {
			typeStr = VTCLTypeNameConstants.MODELELEMENT;
			kind = ValueKind.MODELELEMENT_LITERAL;
			// Schedule variable reference for type checking
			termsToCheck.add(varRef);
			// Determine the GLB of variable reference types
			if (prevTypeConst != null) {
				typeStr = typeResolver.greatestLowerBound(modelManager,
						typeStr, prevTypeConst.getFqn());
			}
		}
		// Pattern Variable Assignment
		else if (parent instanceof PatternVariableAssignment) {
			typeStr = VTCLTypeNameConstants.MODELELEMENT;
			kind = ValueKind.MODELELEMENT_LITERAL;
			// Schedule variable reference for type checking
			termsToCheck.add(varRef);
			// Determine the GLB of variable reference types
			if (prevTypeConst != null) {
				typeStr = typeResolver.greatestLowerBound(modelManager,
						typeStr, prevTypeConst.getFqn());
			}
		}
		// All other cases (should be checked separately)
		else {
			if (prevTypeConst != null) {
				typeStr = prevTypeConst.getFqn();
				kind = prevTypeConst.getKind();
			} else {
				typeStr = VTCLTypeNameConstants.TOP;
				kind = ValueKind.MODELELEMENT_LITERAL;
			}
		}
		varRef.setType(typeStr);
		varRef.setKind(kind);

		/*if (typeStr.contentEquals(VTCLTypeNameConstants.MODELELEMENT)
				|| typeStr.contentEquals(VTCLTypeNameConstants.ENTITY)
				|| typeStr.contentEquals(VTCLTypeNameConstants.RELATION)) {
			return null;
		}*/
		TypeConstant resultTypeConst = DefinitionsFactory.eINSTANCE
				.createTypeConstant();
		// Set result type constant
		resultTypeConst.setFqn(typeStr);
		resultTypeConst.setKind(kind);

		return resultTypeConst;
	}

	protected void inferTypeForPatternVariableDef(PatternVariable varDef,
			TypeConstant typeConst) {
		// Type inference is only required when the type of varDef is not
		// explicitly defined
		if (varDef.getVariableType() == null && typeConst != null) {
			varDef.setVariableType(typeConst);
		}
	}

	protected void typecheckPatternBody(GTPatternBody body) {
		// For each pattern variable definition below body
		for (Object paramObject : body.getHeader().getSymParameters()) {
			PatternVariable param = (PatternVariable) paramObject;
			// For each variable reference
			for (Object varRefObj : param.getReferences()) {
				VariableReference varRef = (VariableReference) varRefObj;
				// Get the parent of the variable reference
				EObject parent = varRef.eContainer();
				if (parent instanceof ModelElement) {
					ModelElement element = (ModelElement) parent;
					if (!element.getType().isEmpty()) {
						ModelElement type = element.getType().get(0);
						String typeStr = type.getName();
						varRef.setType(typeStr);
					} else {
						if (parent instanceof Entity) {
							varRef.setType(VTCLTypeNameConstants.ENTITY);
						} else if (parent instanceof Relation) {
							varRef.setType(VTCLTypeNameConstants.RELATION);
						} else {
							varRef.setType(VTCLTypeNameConstants.MODELELEMENT);
						}
					}
					varRef.setKind(ValueKind.MODELELEMENT_LITERAL);
				}
				// GTPatternCalls are already handled
				else if (parent instanceof PatternVariableAssignment) {
					// TODO Check if the LHS and RHS are compatible
					// PatternVariableAssignment pva =
					// (PatternVariableAssignment) parent;
				}

			}
		}
		// Register its type
		// Allocate type for its variable definition
	}

	/**
	 * Recursive traversal of the term
	 * @param term
	 */
	protected void typeCheckTerm(Term term) {
		if (term instanceof RelationalOperation
				|| term instanceof ArithmeticOperation
				|| term instanceof ConversionOperation) {
			FunctionInvocation funInvoc = (FunctionInvocation) term;
			if (funInvoc.getActualParameters().size() == 1) {
				Term operand = funInvoc.getActualParameters().get(0);
				if (operand.getType() == null) {
					// Typecheck operand (if needed)
					typeCheckTerm(operand);
				}
				// Typecheck the current term
				typeCheckUnaryTerm(term, operand);

			} else if (funInvoc.getActualParameters().size() == 2) {
				// Typecheck left operand (when needed)
				Term leftOperand = funInvoc.getActualParameters().get(0);
				if (leftOperand.getType() == null) {
					typeCheckTerm(leftOperand);
				}
				// Typecheck right operand (if needed)
				Term rightOperand = funInvoc.getActualParameters().get(1);
				if (rightOperand.getType() == null) {
					typeCheckTerm(rightOperand);
				}
				// Typecheck the current term
				typeCheckBinaryTerm(term, leftOperand, rightOperand);
			}
		} else if (term instanceof ASMFunctionInvocation) {
			ASMFunctionInvocation asmFunInvoc = (ASMFunctionInvocation) term;
			for (Object param : asmFunInvoc.getActualParameters()) {
				Term actualParam = (Term) param;
				if (actualParam.getType() == null) {
					typeCheckTerm(actualParam);
				}
			}
			ASMFunction asmFunDef = asmFunInvoc.getCalledFunction();
			// All GT rule invocations should be resolved prior to type checking
			assert (asmFunDef != null) : "ASM function definition is not resolved for "
					+ asmFunInvoc.getFqn();
			if (asmFunDef.getReturnType() != null) {
				TypeConstant type = asmFunDef.getReturnType();
				asmFunInvoc.setType(type.getFqn());
				asmFunInvoc.setKind(type.getKind());
			} else {
				asmFunInvoc.setType(VTCLTypeNameConstants.TOP);
				asmFunInvoc.setKind(ValueKind.UNDEF_LITERAL);
			}
			// typeCheckAsmFunctionInvocation(asmFunInvoc);
		} else if (term instanceof NativeFunctionInvocation) {
			NativeFunctionInvocation nativeFunInvoc = (NativeFunctionInvocation) term;
			for (Object param : nativeFunInvoc.getActualParameters()) {
				Term actualParam = (Term) param;
				if (actualParam.getType() == null) {
					typeCheckTerm(actualParam);
				}
			}
			// TODO: Provide better return type if possible
			nativeFunInvoc.setType(VTCLTypeNameConstants.TOP);
			nativeFunInvoc.setKind(ValueKind.UNDEF_LITERAL);
			// typeCheckNativeFunctionInvocation(nativeFunInvoc);

		} else if (term instanceof ModelElementQuery) {
			ModelElementQuery meQuery = (ModelElementQuery) term;
			Term argument = meQuery.getArgument();
			if (argument.getType() == null) {
				typeCheckTerm(argument);
			}
			typeCheckUnaryTerm(term, argument);
		} else if (term instanceof GTPatternCall) {
			GTPatternCall patternCall = (GTPatternCall) term;
			for (Object param : patternCall.getActualParameters()) {
				Term actualParam = (Term) param;
				if (actualParam.getType() == null) {
					typeCheckTerm(actualParam);
				}
			}
			// Set the type information for pattern call (used as a term)
			patternCall.setKind(ValueKind.BOOLEAN_LITERAL);
			patternCall.setType("datatypes.Boolean");
			// typeCheckPatternCall(patternCall);
		} else if (term instanceof VariableReference) {
			VariableReference varRef = (VariableReference) term;
			typeCheckVariableReference(varRef);
		} else {
			// assert false;
		}
	}

	/**
	 * Provides type checking for a {@link VariableReference}: it looks up the
	 * type of its corresponding {@link Variable} definition
	 * @param varRef
	 *            : the {@link VariableReference} to be checked
	 */
	protected void typeCheckVariableReference(VariableReference varRef) {
		Variable varDef = varRef.getVariable();
		if (varDef == null) {
			varRef.setType(VTCLTypeNameConstants.TOP);
			varRef.setKind(ValueKind.UNDEF_LITERAL);
			return;
		}
		if (varDef.getVariableType() != null) {
			TypeConstant typeConstant = varDef.getVariableType();
			String typeStr = typeConstant.getFqn();
			ValueKind kind = typeConstant.getKind();
			// Set type for variable reference
			if (typeStr != null && !typeStr.equals("")) {
				assert (kind != null) : "Kind of type constant is not yet set";
				// If the type of the variable reference is not yet set
				// assign it according to the type of the variable definition
				if (varRef.getType() == null) {
					varRef.setType(typeStr);
					varRef.setKind(kind);
				}
				// Check type compatibility if both values are set
				else {
					if (!typeResolver.isSupertype(modelManager, typeStr, varRef
							.getType())) {
						// If inconsistent, report error
						String[] context = new String[] { varRef.getType(),
								typeStr };
						addTypeError(
								varRef.getAnnotations(),
								VTCLMessages.VTCLValidationErrorCodes_INCOMPATIBLE_VARIABLEREF_TYPE,
								ErrorSeverity.WARNING, context);
					}
				}
			} else {
				if (varRef.getType() == null) {
					varRef.setType(VTCLTypeNameConstants.TOP);
					varRef.setKind(ValueKind.UNDEF_LITERAL);
				}
			}
		} else {
			if (varRef.getType() == null) {
				varRef.setType(VTCLTypeNameConstants.TOP);
				varRef.setKind(ValueKind.UNDEF_LITERAL);
			}
		}
	}

	/**
	 * Provides type checking for the actual parameters of a
	 * {@link GTRuleInvocation}
	 * @param gtRuleInvoc
	 *            : the {@link GTRuleInvocation} to be checked
	 */
	protected void typeCheckGTRuleCall(GTRuleInvocation gtRuleInvoc) {
		GTRule gtRuleDef = gtRuleInvoc.getRule();
		// All GT rule invocations should be resolved prior to type checking
		assert (gtRuleDef != null) : "GT rule is not resolved for "
				+ gtRuleInvoc.getFqn();
		assert (gtRuleDef.getSymParameters().size() == gtRuleInvoc
				.getActualParameters().size()) : "Parameter mismatch in GT rule invocation";
		for (int i = 0; i < gtRuleDef.getSymParameters().size(); i++) {
			SymbolicRuleParameter symParam = gtRuleDef.getSymParameters()
					.get(i);
			Variable varDef = symParam.getVariable();
			assert (varDef != null) : "Variable is not resolved for Symbolic parameter";
			Term actualParam = gtRuleInvoc.getActualParameters().get(i);
			if (varDef.getVariableType() != null) {
				TypeConstant type = varDef.getVariableType();
				// Check consistency of types
				if (!typeResolver.isSupertype(modelManager, type.getFqn(),
						actualParam.getType())) {
					// If inconsistent, report error
					String[] context = new String[] { actualParam.getType(),
							type.getFqn(), varDef.getName(),
							gtRuleInvoc.getFqn() };
					addTypeError(
							actualParam.getAnnotations(),
							VTCLMessages.VTCLValidationErrorCodes_INCOMPATIBLE_ACTUALPARAM_TYPE,
							ErrorSeverity.WARNING, context);
				}
			}
		}

	}

	/**
	 * Provides type checking for the actual parameters of a
	 * {@link GTPatternCall}
	 * @param patternCall
	 *            : the {@link GTPatternCall} to be checked
	 */
	protected void typeCheckPatternCall(GTPatternCall patternCall) {
		GTPattern patternDef = patternCall.getCalledPattern();
		// All pattern calls should be resolved prior to type checking
		assert (patternDef != null) : "Pattern definition is not resolved";
		assert (patternDef.getSymParameters().size() == patternCall
				.getActualParameters().size()) : "Parameter mismatch in pattern call";
		for (int i = 0; i < patternDef.getSymParameters().size(); i++) {
			PatternVariable symParam = patternDef.getSymParameters().get(i);
			Term actualParam = patternCall.getActualParameters().get(i);
			if (symParam.getVariableType() != null) {
				TypeConstant type = symParam.getVariableType();
				// Check consistency of types
				// TODO this is a workaround for a nullpointer e
				String actualParamType = actualParam.getType();
				String paramType = type.getFqn();
				if (!typeResolver.isSupertype(modelManager, paramType,
						actualParamType)
						&& !typeResolver.isSupertype(modelManager,
								actualParamType, paramType)) {
					// If inconsistent, report a warning, as a subpattern can
					// strengthen a precondition
					String[] context = new String[] { actualParamType,
							paramType, symParam.getName(), patternCall.getFqn() };
					addTypeError(
							actualParam.getAnnotations(),
							VTCLMessages.VTCLValidationErrorCodes_INCOMPATIBLE_ACTUALPARAM_TYPE,
							ErrorSeverity.WARNING, context);
				}
			}
		}

	}

	/**
	 * Provides type compatibility checking for the actual parameters of a
	 * {@link CallRule}
	 * @param callRule
	 *            : the {@link CallRule} to be checked
	 */
	protected void typeCheckCallRule(CallRule callRule) {
		Rule ruleDef = callRule.getRule();
		// All pattern calls should be resolved prior to type checking
		assert (ruleDef != null) : "ASM rule is not resolved";
		assert (ruleDef.getSymParameters().size() == callRule
				.getActualParameters().size()) : "Parameter mismatch in call rule";
		for (int i = 0; i < ruleDef.getSymParameters().size(); i++) {
			SymbolicRuleParameter symParam = ruleDef.getSymParameters().get(i);
			Variable varDef = symParam.getVariable();
			assert (varDef != null) : "Variable cannot be resolved for Symbolic rule parameter";
			Term actualParam = callRule.getActualParameters().get(i);
			if (varDef.getVariableType() != null) {
				TypeConstant type = varDef.getVariableType();
				// Check consistency of types
				if (!typeResolver.isSupertype(modelManager, type.getFqn(),
						actualParam.getType())) {
					// If inconsistent, report error
					String[] context = new String[] { actualParam.getType(),
							type.getFqn(), varDef.getName(), callRule.getFqn() };
					addTypeError(
							actualParam.getAnnotations(),
							VTCLMessages.VTCLValidationErrorCodes_INCOMPATIBLE_ACTUALPARAM_TYPE,
							ErrorSeverity.WARNING, context);
				}
			}
		}

	}

	/**
	 * Provides type compatibility checking for the left and right values of a
	 * {@link RuleUpdate}
	 * @param updateRule
	 *            : the {@link RuleUpdate} to be checked
	 */
	protected void typeCheckUpdateRule(RuleUpdate updateRule) {
		// Determine the type of its left value
		String leftValueType = "";
		if (updateRule instanceof RuleUpdateVariable) {
			RuleUpdateVariable varUpdateRule = (RuleUpdateVariable) updateRule;
			VariableReference varRef = varUpdateRule.getVariable();
			assert (varRef != null);
			// We assume that the type of varRef is already resolved
			leftValueType = varRef.getType();
		} else if (updateRule instanceof RuleUpdateASMFunction) {
			RuleUpdateASMFunction asmFunUpdateRule = (RuleUpdateASMFunction) updateRule;
			ASMFunction asmFunDef = asmFunUpdateRule.getFunction();
			assert (asmFunDef != null);
			TypeConstant typeConst = asmFunDef.getReturnType();
			if (typeConst != null) {
				leftValueType = typeConst.getFqn();
			} else {
				leftValueType = VTCLTypeNameConstants.TOP;
			}
			// Check type consistency of locations
			if (!asmFunDef.getArgumentTypes().isEmpty()) {
				for (int i = 0; i < asmFunUpdateRule.getLocations().size(); i++) {
					Term term = asmFunUpdateRule.getLocations().get(i);
					TypeConstant typeConstArg = asmFunDef.getArgumentTypes()
							.get(i);
					typeCheckCompatibility(term, typeConstArg.getFqn(), term
							.getType());
				}

			}
		}
		// Determine the type of its right value
		Term value = updateRule.getValue();
		assert (value != null);
		String rightValueType = value.getType();
		// Issue an error message if the type of left value is not a supertype
		// of the right value
		if (!typeResolver.isSupertype(modelManager, leftValueType,
				rightValueType)) {
			String[] context = new String[] { leftValueType, rightValueType };
			addTypeError(
					updateRule.getAnnotations(),
					VTCLMessages.VTCLValidationErrorCodes_INCOMPATIBLE_TYPE_IN_UPDATE,
					ErrorSeverity.WARNING, context);
		}
	}

	protected void typeCheckNativeFunctionInvocation(
			NativeFunctionInvocation nativeFunInvoc) {
		// FIXME To be completed later

	}

	protected void typeCheckAsmFunctionInvocation(
			ASMFunctionInvocation asmFunInvoc) {
		ASMFunction asmFun = asmFunInvoc.getCalledFunction();
		assert (asmFun != null);
		if (!asmFun.getArgumentTypes().isEmpty()) {
			for (int i = 0; i < asmFunInvoc.getActualParameters().size(); i++) {
				Term term = asmFunInvoc.getActualParameters().get(i);
				TypeConstant typeConst = asmFun.getArgumentTypes().get(i);
				typeCheckCompatibility(term, typeConst.getFqn(), term.getType());
			}
		}
	}

	protected void typeCheckInitialValue(InitialValue initValue) {
		ASMFunction asmFun = (ASMFunction) initValue.eContainer();
		// Check if initial value is consistent with type
		if (!asmFun.getArgumentTypes().isEmpty()) {
			for (int i = 0; i < initValue.getLocations().size(); i++) {
				Term term = initValue.getLocations().get(i);
				TypeConstant typeConst = asmFun.getArgumentTypes().get(i);
				typeCheckCompatibility(term, typeConst.getFqn(), term.getType());
			}
		}
		// Check if value is consistent with return type
		if (asmFun.getReturnType() != null) {
			Term term = initValue.getValue();
			TypeConstant typeConst = asmFun.getReturnType();
			typeCheckCompatibility(term, typeConst.getFqn(), term.getType());
		}
	}

	protected void typeCheckVariableDefinition(VariableDefinition varDefine) {
		// Check if initial value of a variable is consistent with its type
		Variable var = varDefine.getVariable();
		TypeConstant typeConst = var.getVariableType();
		if (typeConst != null) {
			Term initValue = varDefine.getValue();
			typeCheckCompatibility(varDefine, typeConst.getFqn(), initValue
					.getType());
		}
	}

	protected void typeCheckCompatibility(AnnotatedElement element,
			String supertypeStr, String subtypeStr) {
		if (!typeResolver.isSupertype(modelManager, supertypeStr, subtypeStr)) {
			// If inconsistent, report error
			String[] context = new String[] { supertypeStr, subtypeStr };
			addTypeError(
					element.getAnnotations(),
					VTCLMessages.VTCLValidationErrorCodes_INCOMPATIBLE_INITIALVALUE_TYPE,
					ErrorSeverity.WARNING, context);
		}
	}

	protected void typeCheckBinaryTerm(Term term, Term leftOperand,
			Term rightOperand) {
		// // Type checking
		// TODO: Enable the following code if needed for double-checking
		ValueKind resultKind = TermTypeChecker.typeCheck(term, leftOperand
				.getKind(), rightOperand.getKind());
		term.setKind(resultKind);
		// // Report type error
		// if (resultKind.getValue() == ValueKind.ERROR) {
		// String[] context = new String[]{
		// TermTypeChecker.getOperationString(term),
		// leftOperand.getKind().getName(), rightOperand.getKind().getName()};
		// addTypeError(
		// term.getAnnotations(),
		// VTCLMessages.VTCLValidationErrorCodes_BINARY_INCOMPATIBLE_TYPES,
		// ErrorSeverity.WARNING,
		// context);
		// }
		// String based Type checking
		String resultType = typeCheckBinaryTerm(term.eClass().getName(),
				leftOperand, rightOperand);
		term.setType(resultType);
		// Report type error
		if (resultType.equals(VTCLTypeNameConstants.BOTTOM)) {
			String[] context = new String[] {
					TermTypeChecker.getOperationString(term),
					leftOperand.getType(), rightOperand.getType() };
			addTypeError(
					term.getAnnotations(),
					VTCLMessages.VTCLValidationErrorCodes_BINARY_INCOMPATIBLE_TYPES,
					ErrorSeverity.WARNING, context);
		}
	}

	protected void typeCheckUnaryTerm(Term term, Term operand) {
		ValueKind resultKind = TermTypeChecker.typeCheck(term, operand
				.getKind());
		term.setKind(resultKind);
		// // Report type error
		// if (resultKind.getValue() == ValueKind.ERROR) {
		// String[] context = new String[]{
		// TermTypeChecker.getOperationString(term),
		// operand.getKind().getName(), };
		// addTypeError(
		// term.getAnnotations(),
		// VTCLMessages.VTCLValidationErrorCodes_UNARY_INCOMPATIBLE_TYPES,
		// ErrorSeverity.WARNING,
		// context);
		// }
		// String based Type checking
		String resultType = typeCheckUnaryTerm(term.eClass().getName(), operand);
		term.setType(resultType);
		// Report type error
		// TODO resultType nullcheck shouldn't be needed
		if (resultType.equals(VTCLTypeNameConstants.BOTTOM)) {
			String[] context = new String[] {
					TermTypeChecker.getOperationString(term), operand.getType() };
			addTypeError(
					term.getAnnotations(),
					VTCLMessages.VTCLValidationErrorCodes_UNARY_INCOMPATIBLE_TYPES,
					ErrorSeverity.WARNING, context);
		}

	}

	protected final String[] longTypeCheckList = {
			VTCLTypeNameConstants.MYSELF, VTCLTypeNameConstants.STAR,
			VTCLTypeNameConstants.SUPERTYPE, VTCLTypeNameConstants.ENTITY,
			VTCLTypeNameConstants.RELATION, VTCLTypeNameConstants.MODELELEMENT };
	protected final String[] builtInTypeCheckList = {
			VTCLTypeNameConstants.MYSELF, VTCLTypeNameConstants.STAR };
	protected final String[] topTypeCheckList = { VTCLTypeNameConstants.TOP,
			VTCLTypeNameConstants.STAR };
	protected final String[] bottomTypeCheckList = { VTCLTypeNameConstants.BOTTOM };

	protected String nextTypeToCheck(String typeCode, String operand) {
		if (typeCode.equals(String.valueOf(VTCLTypeNameConstants.MYSELF))) {
			return operand;
		} else if (typeCode.equals(String.valueOf(VTCLTypeNameConstants.STAR))) {
			return String.valueOf("*");
		} else if (typeCode.equals(String
				.valueOf(VTCLTypeNameConstants.SUPERTYPE))) {
			// TODO: Handle this case properly
			return String.valueOf(VTCLTypeNameConstants.SUPERTYPE);
		} else {
			return typeCode;
		}
	}

	private String[] createTypeCheckList(ValueKind kind, String type) {
		if (kind.equals(ValueKind.MODELELEMENT_LITERAL)) {
			IModelElement element = modelManager.getElementByName(type);
			if (element != null) {
				if (element.isEntity()) {
					String[] resultList = { VTCLTypeNameConstants.MYSELF,
							VTCLTypeNameConstants.STAR,
							VTCLTypeNameConstants.SUPERTYPE,
							VTCLTypeNameConstants.ENTITY,
							VTCLTypeNameConstants.MODELELEMENT };
					return resultList;
				} else if (element.isRelation()) {
					String[] resultList = { VTCLTypeNameConstants.MYSELF,
							VTCLTypeNameConstants.STAR,
							VTCLTypeNameConstants.SUPERTYPE,
							VTCLTypeNameConstants.RELATION,
							VTCLTypeNameConstants.MODELELEMENT };
					return resultList;
				} else {
					// This case should never happen
					String[] resultList = { VTCLTypeNameConstants.MYSELF,
							VTCLTypeNameConstants.STAR,
							VTCLTypeNameConstants.SUPERTYPE,
							VTCLTypeNameConstants.MODELELEMENT };
					return resultList;
				}
			}
			// TODO: Handle case when type cannot be resolved in the model space
			else {
				if (type.equals(VTCLTypeNameConstants.ENTITY)
						|| type.equals("entity")) {
					String[] resultList = { VTCLTypeNameConstants.STAR,
							VTCLTypeNameConstants.ENTITY,
							VTCLTypeNameConstants.MODELELEMENT };
					return resultList;
				} else if (type.equals(VTCLTypeNameConstants.RELATION)
						|| type.equals("relation")) {
					String[] resultList = { VTCLTypeNameConstants.STAR,
							VTCLTypeNameConstants.RELATION,
							VTCLTypeNameConstants.MODELELEMENT };
					return resultList;
				} else {
					String[] resultList = { VTCLTypeNameConstants.STAR,
							VTCLTypeNameConstants.MODELELEMENT };
					return resultList;
				}

			}
		} else if (kind.equals(ValueKind.UNDEF_LITERAL)) {
			return topTypeCheckList;
		} else if (kind.equals(ValueKind.ERROR_LITERAL)) {
			return bottomTypeCheckList;
		} else {
			return builtInTypeCheckList;
		}
	}

	protected String typeCheckBinaryTerm(String termClassName,
			Term leftOperandTerm, Term rightOperandTerm) {
		String leftOperand = leftOperandTerm.getType();
		String rightOperand = rightOperandTerm.getType();
		String[] leftCheckList;
		String[] rightCheckList;
		ValueKind leftKind = leftOperandTerm.getKind(); // typeResolver.getValueKind(leftOperand);
		ValueKind rightKind = rightOperandTerm.getKind(); // typeResolver.getValueKind(rightOperand);
		leftCheckList = createTypeCheckList(leftKind, leftOperand);
		rightCheckList = createTypeCheckList(rightKind, rightOperand);

		for (String leftType : leftCheckList) {
			String leftCheck = nextTypeToCheck(leftType, leftOperand);
			for (String rightType : rightCheckList) {
				String rightCheck = nextTypeToCheck(rightType, rightOperand);
				StringTriple triple = new StringTriple(termClassName,
						leftCheck, rightCheck);
				BinaryTypeJudgement judgement = binaryTypeRuleMap.get(triple);
				if (judgement != null) {
					return judgement.getResult();
				}
			}
		}

		// // GivenType x GivenType
		// StringTriple triple = new StringTriple(termClassName, leftOperand,
		// rightOperand);
		// BinaryTypeJudgement judgement = binaryTypeRuleMap.get(triple);
		// if (judgement != null) {
		// return judgement.getResult();
		// }
		// IModelElement leftElement =
		// modelManager.getElementByName(leftOperand);
		// IModelElement rightElement =
		// modelManager.getElementByName(rightOperand);
		// if (leftElement != null) {
		// // ENTITY x GivenType
		// if (leftElement.isEntity()) {
		// triple = new StringTriple(termClassName, "ENTITY", rightOperand);
		// judgement = binaryTypeRuleMap.get(triple);
		// if (judgement != null) {
		// return judgement.getResult();
		// }
		// if (rightElement != null) {
		// // ENTITY x ENTITY
		// if (rightElement.isEntity()) {
		// triple = new StringTriple(termClassName, "ENTITY", "ENTITY");
		// }
		// // ENTITY x RELATION
		// else if (rightElement.isRelation()) {
		// triple = new StringTriple(termClassName, "ENTITY", "RELATION");
		// }
		// // ENTITY x MODELELEMENT
		// else {
		// triple = new StringTriple(termClassName, "ENTITY", "MODELELEMENT");
		// }
		// judgement = binaryTypeRuleMap.get(triple);
		// if (judgement != null) {
		// return judgement.getResult();
		// }
		// }
		// // rightOperand cannot be resolved to a model element
		// // else {
		// // ENTITY x TOP
		// triple = new StringTriple(termClassName, "ENTITY", "TOP");
		// judgement = binaryTypeRuleMap.get(triple);
		// if (judgement != null) {
		// return judgement.getResult();
		// }
		// // ENTITY x *
		// triple = new StringTriple(termClassName, "ENTITY", "*");
		// judgement = binaryTypeRuleMap.get(triple);
		// if (judgement != null) {
		// return judgement.getResult();
		// }
		// // }
		// }
		// // RELATION x GivenType
		// else if (leftElement.isRelation()) {
		// triple = new StringTriple(termClassName, "RELATION", rightOperand);
		// judgement = binaryTypeRuleMap.get(triple);
		// if (judgement != null) {
		// return judgement.getResult();
		// }
		// if (rightElement != null) {
		// // RELATION x ENTITY
		// if (rightElement.isEntity()) {
		// triple = new StringTriple(termClassName, "RELATION", "ENTITY");
		// }
		// // RELATION x RELATION
		// else if (rightElement.isRelation()) {
		// triple = new StringTriple(termClassName, "RELATION", "RELATION");
		// }
		// // RELATION x MODELELEMENT
		// else {
		// triple = new StringTriple(termClassName, "RELATION", "MODELELEMENT");
		// }
		// judgement = binaryTypeRuleMap.get(triple);
		// if (judgement != null) {
		// return judgement.getResult();
		// }
		// }
		// // rightOperand cannot be resolved to a model element
		// // else {
		// // RELATION x TOP
		// triple = new StringTriple(termClassName, "RELATION", "TOP");
		// judgement = binaryTypeRuleMap.get(triple);
		// if (judgement != null) {
		// return judgement.getResult();
		// }
		// // RELATION x *
		// triple = new StringTriple(termClassName, "RELATION", "*");
		// judgement = binaryTypeRuleMap.get(triple);
		// if (judgement != null) {
		// return judgement.getResult();
		// }
		// // }
		// }
		// // MODELELEMENT x GivenType
		// else {
		// triple = new StringTriple(termClassName, "MODELELEMENT",
		// rightOperand);
		// judgement = binaryTypeRuleMap.get(triple);
		// if (judgement != null) {
		// return judgement.getResult();
		// }
		// if (rightElement != null) {
		// // MODELELEMENT x ENTITY
		// if (rightElement.isEntity()) {
		// triple = new StringTriple(termClassName, "MODELELEMENT", "ENTITY");
		// }
		// // MODELELEMENT x RELATION
		// else if (rightElement.isRelation()) {
		// triple = new StringTriple(termClassName, "MODELELEMENT", "RELATION");
		// }
		// // MODELELEMENT x MODELELEMENT
		// else {
		// triple = new StringTriple(termClassName, "MODELELEMENT",
		// "MODELELEMENT");
		// }
		// judgement = binaryTypeRuleMap.get(triple);
		// if (judgement != null) {
		// return judgement.getResult();
		// }
		// }
		// // rightOperand cannot be resolved to a model element
		// // else {
		// // MODELELEMENT x TOP
		// triple = new StringTriple(termClassName, "MODELELEMENT", "TOP");
		// judgement = binaryTypeRuleMap.get(triple);
		// if (judgement != null) {
		// return judgement.getResult();
		// }
		// // ENTITY x *
		// triple = new StringTriple(termClassName, "MODELELEMENT", "*");
		// judgement = binaryTypeRuleMap.get(triple);
		// if (judgement != null) {
		// return judgement.getResult();
		// }
		// // }
		// }
		// }
		// // leftOperand cannot be resolved to a model element
		// // else {
		// // TOP X GivenType
		// triple = new StringTriple(termClassName, "TOP", rightOperand);
		// judgement = binaryTypeRuleMap.get(triple);
		// if (judgement != null) {
		// return judgement.getResult();
		// }
		// if (rightElement != null) {
		// // TOP x ENTITY
		// if (rightElement.isEntity()) {
		// triple = new StringTriple(termClassName, "TOP", "ENTITY");
		// }
		// // TOP x RELATION
		// else if (rightElement.isRelation()) {
		// triple = new StringTriple(termClassName, "TOP", "RELATION");
		// }
		// // TOP x MODELELEMENT
		// else {
		// triple = new StringTriple(termClassName, "TOP", "MODELELEMENT");
		// }
		// judgement = binaryTypeRuleMap.get(triple);
		// if (judgement != null) {
		// return judgement.getResult();
		// }
		// }
		// // rightOperand cannot be resolved to a model element
		// // else {
		// // TOP x TOP
		// triple = new StringTriple(termClassName, "TOP", "TOP");
		// judgement = binaryTypeRuleMap.get(triple);
		// if (judgement != null) {
		// return judgement.getResult();
		// }
		// // TOP x *
		// triple = new StringTriple(termClassName, "TOP", "*");
		// judgement = binaryTypeRuleMap.get(triple);
		// if (judgement != null) {
		// return judgement.getResult();
		// }
		// // }
		//
		// // * X GivenType
		// triple = new StringTriple(termClassName, "*", rightOperand);
		// judgement = binaryTypeRuleMap.get(triple);
		// if (judgement != null) {
		// return judgement.getResult();
		// }
		// if (rightElement != null) {
		// // * x ENTITY
		// if (rightElement.isEntity()) {
		// triple = new StringTriple(termClassName, "*", "ENTITY");
		// }
		// // * x RELATION
		// else if (rightElement.isRelation()) {
		// triple = new StringTriple(termClassName, "*", "RELATION");
		// }
		// // * x MODELELEMENT
		// else {
		// triple = new StringTriple(termClassName, "*", "MODELELEMENT");
		// }
		// judgement = binaryTypeRuleMap.get(triple);
		// if (judgement != null) {
		// return judgement.getResult();
		// }
		// }
		// // rightOperand cannot be resolved to a model element
		// // else {
		// // * x TOP
		// triple = new StringTriple(termClassName, "*", "TOP");
		// judgement = binaryTypeRuleMap.get(triple);
		// if (judgement != null) {
		// return judgement.getResult();
		// }
		// // * x *
		// triple = new StringTriple(termClassName, "*", "*");
		// judgement = binaryTypeRuleMap.get(triple);
		// if (judgement != null) {
		// return judgement.getResult();
		// }
		// // }
		// // }
		return VTCLTypeNameConstants.BOTTOM;
	}

	protected String typeCheckUnaryTerm(String termClassName, Term operand) {
		String operandStr = operand.getType();
		String resultType = VTCLTypeNameConstants.BOTTOM;
		// XXX when multiple custom judgements are available, the result might
		// vary
		// Handle custom type judgment
		List<CustomTypeJudgement> customList = customTypeRuleMap
				.get(termClassName);
		if (customList != null) {
			for (CustomTypeJudgement customJudgement : customList) {
				if (customJudgement.getName().equals("typeSource")) {
					resultType = CustomTypeJudgementCheck.typeSource(
							modelManager, operandStr);
				} else if (customJudgement.getName().equals("typeTarget")) {
					resultType = CustomTypeJudgementCheck.typeTarget(
							modelManager, operandStr);
				} else if (customJudgement.getName().equals("typeInverse")) {
					resultType = CustomTypeJudgementCheck.typeInverse(
							modelManager, operandStr);
				} else if (customJudgement.getName().equals(
						"typeElementReference")) {
					resultType = CustomTypeJudgementCheck.typeElementReference(
							modelManager, operand);
				}
			}
		}
		// If Custom judgement was successful, return its result
		if (resultType != VTCLTypeNameConstants.BOTTOM) {
			return resultType;
		}
		String[] leftCheckList;
		ValueKind leftKind = operand.getKind();// typeResolver.getValueKind(operandStr);
		leftCheckList = createTypeCheckList(leftKind, operandStr);
		// XXX in case of multiple matching unary type rules the result may vary
		for (String leftType : leftCheckList) {
			String leftCheck = nextTypeToCheck(leftType, operandStr);
			StringPair pair = new StringPair(termClassName, leftCheck);
			UnaryTypeJudgement judgement = unaryTypeRuleMap.get(pair);
			if (judgement != null) {
				return judgement.getResult();
			}
		}

		//
		// // Handle unary type judgment: with given operand
		// StringPair pair = new StringPair(termClassName, operand);
		// UnaryTypeJudgement unaryJudgement = unaryTypeRuleMap.get(pair);
		// if (unaryJudgement != null) {
		// return unaryJudgement.getResult();
		// }
		// IModelElement element = modelManager.getElementByName(operand);
		// // Handle unary type judgment: with ENTITY or RELATION
		// if (element != null) {
		// if (element.isEntity()) {
		// pair = new StringPair(termClassName, "ENTITY");
		// }
		// else if (element.isRelation()) {
		// pair = new StringPair(termClassName, "RELATION");
		//
		// }
		// // Handle unary type judgment: with MODELELEMENT
		// else {
		// pair = new StringPair(termClassName, "MODELELEMENT");
		// }
		// unaryJudgement = unaryTypeRuleMap.get(pair);
		// if (unaryJudgement != null) {
		// return unaryJudgement.getResult();
		// }
		// }
		// // else {
		// // Handle unary type judgment: with TOP
		// pair = new StringPair(termClassName, "TOP");
		// unaryJudgement = unaryTypeRuleMap.get(pair);
		// if (unaryJudgement != null) {
		// return unaryJudgement.getResult();
		// }
		// // Handle unary type judgment: with *
		// pair = new StringPair(termClassName, "*");
		// unaryJudgement = unaryTypeRuleMap.get(pair);
		// if (unaryJudgement != null) {
		// return unaryJudgement.getResult();
		// }
		// // }
		return resultType;
	}

}