ModelFactory.java

package edu.udel.cis.vsl.tass.model.impl;

import java.util.LinkedHashMap;
import java.util.Map;
import java.util.Vector;

import edu.udel.cis.vsl.tass.config.RunConfiguration;
import edu.udel.cis.vsl.tass.model.IF.AbstractFunctionIF;
import edu.udel.cis.vsl.tass.model.IF.ModelFactoryIF;
import edu.udel.cis.vsl.tass.model.IF.ModelIF;
import edu.udel.cis.vsl.tass.model.IF.ModelTransformerLoaderIF;
import edu.udel.cis.vsl.tass.model.IF.SyntaxException;
import edu.udel.cis.vsl.tass.model.IF.SystemFunctionIF;
import edu.udel.cis.vsl.tass.model.IF.expression.BinaryExpressionIF;
import edu.udel.cis.vsl.tass.model.IF.expression.BoundExpressionIF.Quantifier;
import edu.udel.cis.vsl.tass.model.IF.expression.DereferenceExpressionIF;
import edu.udel.cis.vsl.tass.model.IF.expression.EvaluatedFunctionExpressionIF;
import edu.udel.cis.vsl.tass.model.IF.expression.ExpressionIF;
import edu.udel.cis.vsl.tass.model.IF.expression.IfThenElseExpressionIF;
import edu.udel.cis.vsl.tass.model.IF.expression.LHSExpressionIF;
import edu.udel.cis.vsl.tass.model.IF.expression.LiteralExpressionIF;
import edu.udel.cis.vsl.tass.model.IF.expression.NamedLiteralExpressionIF;
import edu.udel.cis.vsl.tass.model.IF.expression.NamedObjectLiteralExpressionIF;
import edu.udel.cis.vsl.tass.model.IF.expression.NotEmptyExpressionIF;
import edu.udel.cis.vsl.tass.model.IF.expression.NotFullExpressionIF;
import edu.udel.cis.vsl.tass.model.IF.expression.ObjectLiteralExpressionIF;
import edu.udel.cis.vsl.tass.model.IF.expression.ProcessReferenceExpressionIF;
import edu.udel.cis.vsl.tass.model.IF.expression.RecordNavigationExpressionIF;
import edu.udel.cis.vsl.tass.model.IF.expression.SizeOfExpressionIF;
import edu.udel.cis.vsl.tass.model.IF.expression.SubscriptExpressionIF;
import edu.udel.cis.vsl.tass.model.IF.expression.UnaryExpressionIF;
import edu.udel.cis.vsl.tass.model.IF.expression.VariableExpressionIF;
import edu.udel.cis.vsl.tass.model.IF.scope.BoundScopeIF;
import edu.udel.cis.vsl.tass.model.IF.scope.ScopeIF;
import edu.udel.cis.vsl.tass.model.IF.scope.ScopeIF.ScopeKind;
import edu.udel.cis.vsl.tass.model.IF.type.ArrayTypeIF;
import edu.udel.cis.vsl.tass.model.IF.type.FunctionTypeIF;
import edu.udel.cis.vsl.tass.model.IF.type.PointerTypeIF;
import edu.udel.cis.vsl.tass.model.IF.type.RecordTypeIF;
import edu.udel.cis.vsl.tass.model.IF.type.TypeIF;
import edu.udel.cis.vsl.tass.model.IF.type.TypeIF.TypeKind;
import edu.udel.cis.vsl.tass.model.IF.type.VectorTypeIF;
import edu.udel.cis.vsl.tass.model.IF.variable.BoundVariableIF;
import edu.udel.cis.vsl.tass.model.IF.variable.FormalVariableIF;
import edu.udel.cis.vsl.tass.model.IF.variable.VariableIF;
import edu.udel.cis.vsl.tass.model.impl.expression.AddExpression;
import edu.udel.cis.vsl.tass.model.impl.expression.AddressOfExpression;
import edu.udel.cis.vsl.tass.model.impl.expression.AndExpression;
import edu.udel.cis.vsl.tass.model.impl.expression.AnyExpression;
import edu.udel.cis.vsl.tass.model.impl.expression.ArrayLambdaExpression;
import edu.udel.cis.vsl.tass.model.impl.expression.BoundExpression;
import edu.udel.cis.vsl.tass.model.impl.expression.CastExpression;
import edu.udel.cis.vsl.tass.model.impl.expression.DereferenceExpression;
import edu.udel.cis.vsl.tass.model.impl.expression.DivideExpression;
import edu.udel.cis.vsl.tass.model.impl.expression.EqualsExpression;
import edu.udel.cis.vsl.tass.model.impl.expression.EvaluatedFunctionExpression;
import edu.udel.cis.vsl.tass.model.impl.expression.Expression;
import edu.udel.cis.vsl.tass.model.impl.expression.IfThenElseExpression;
import edu.udel.cis.vsl.tass.model.impl.expression.LengthExpression;
import edu.udel.cis.vsl.tass.model.impl.expression.LessThanExpression;
import edu.udel.cis.vsl.tass.model.impl.expression.LessThanOrEqualsExpression;
import edu.udel.cis.vsl.tass.model.impl.expression.ModuloExpression;
import edu.udel.cis.vsl.tass.model.impl.expression.MultiplyExpression;
import edu.udel.cis.vsl.tass.model.impl.expression.NegativeExpression;
import edu.udel.cis.vsl.tass.model.impl.expression.NotEmptyExpression;
import edu.udel.cis.vsl.tass.model.impl.expression.NotExpression;
import edu.udel.cis.vsl.tass.model.impl.expression.NotFullExpression;
import edu.udel.cis.vsl.tass.model.impl.expression.OrExpression;
import edu.udel.cis.vsl.tass.model.impl.expression.PointerAddExpression;
import edu.udel.cis.vsl.tass.model.impl.expression.ProcessReferenceExpression;
import edu.udel.cis.vsl.tass.model.impl.expression.RecordNavigationExpression;
import edu.udel.cis.vsl.tass.model.impl.expression.SizeOfExpression;
import edu.udel.cis.vsl.tass.model.impl.expression.SubscriptExpression;
import edu.udel.cis.vsl.tass.model.impl.expression.SubtractExpression;
import edu.udel.cis.vsl.tass.model.impl.expression.VariableExpression;
import edu.udel.cis.vsl.tass.model.impl.expression.literal.LiteralExpression;
import edu.udel.cis.vsl.tass.model.impl.expression.literal.NamedLiteralExpression;
import edu.udel.cis.vsl.tass.model.impl.expression.literal.NamedObjectLiteralExpression;
import edu.udel.cis.vsl.tass.model.impl.expression.literal.ObjectLiteralExpression;
import edu.udel.cis.vsl.tass.model.impl.scope.BoundScope;
import edu.udel.cis.vsl.tass.model.impl.scope.LocalScope;
import edu.udel.cis.vsl.tass.model.impl.scope.Scope;
import edu.udel.cis.vsl.tass.model.impl.type.TypeFactory;
import edu.udel.cis.vsl.tass.model.impl.variable.BoundVariable;
import edu.udel.cis.vsl.tass.model.impl.variable.FormalVariable;
import edu.udel.cis.vsl.tass.model.impl.variable.Variable;
import edu.udel.cis.vsl.tass.number.Numbers;
import edu.udel.cis.vsl.tass.number.IF.NumberFactoryIF;

/**
 * An implementation of ModelFactoryIF.
 * 
 * @author siegel
 * 
 */
public class ModelFactory implements ModelFactoryIF {

	/** The number of bound variables instantiated by this model factory */
	private int boundVariableCount = 0;

	/**
	 * Map of library names to LibraryInfo objects.
	 */
	private Map<String, LibraryInfo> libraryInfoMap = new LinkedHashMap<String, LibraryInfo>();

	/**
	 * List of library names indexed by library id.
	 */
	private Vector<LibraryInfo> libraryInfoVector = new Vector<LibraryInfo>();

	private int literalCount = 0;

	private ModelTransformerLoaderIF loader;

	private Vector<ModelIF> models = new Vector<ModelIF>();

	private NumberFactoryIF numberFactory = Numbers.REAL_FACTORY;

	private int objectLiteralCount = 0;

	private AbstractFunctionIF sizeOfType;

	private Scope systemScope;

	private TypeFactory typeFactory;

	private RunConfiguration configuration;

	public ModelFactory(RunConfiguration configuration) {
		this.configuration = configuration;
		systemScope = new Scope(null, ScopeKind.SYSTEM, null, "system scope");
		typeFactory = new TypeFactory();
		try {
			sizeOfType = newAbstractFunction("SIZEOF_TYPE", integerType(), 1);
		} catch (SyntaxException e) {
			throw new RuntimeException("Should not happen");
		}
	}

	@Override
	public RunConfiguration configuration() {
		return configuration;
	}

	@Override
	public BinaryExpressionIF addExpression(ExpressionIF left,
			ExpressionIF right) throws SyntaxException {
		Expression arg0 = (Expression) left;
		Expression arg1 = (Expression) right;

		if (left.type().kind() == TypeKind.INTEGER
				&& right.type().kind() == TypeKind.RATIONAL) {
			arg0 = (Expression) castExpression(right.type(), left);
		} else if (left.type().kind() == TypeKind.RATIONAL
				&& right.type().kind() == TypeKind.INTEGER) {
			arg1 = (Expression) castExpression(left.type(), right);
		}
		return new AddExpression(this, arg0, arg1);
	}

	@Override
	public UnaryExpressionIF addressOfExpression(LHSExpressionIF argument) {
		return new AddressOfExpression(this, argument);
	}

	@Override
	public BinaryExpressionIF andExpression(ExpressionIF left,
			ExpressionIF right) throws SyntaxException {
		return new AndExpression(this, (Expression) left, (Expression) right);

	}

	@Override
	public UnaryExpressionIF anyExpression(LHSExpressionIF expr)
			throws SyntaxException {
		return new AnyExpression(this, expr);
	}

	@Override
	public BinaryExpressionIF arrayLambdaExpression(ExpressionIF extent,
			ExpressionIF function) throws SyntaxException {
		return new ArrayLambdaExpression(this, (Expression) extent,
				(Expression) function);
	}

	// A literal array may contain null values. It may also have length of 0.
	@Override
	public ObjectLiteralExpressionIF arrayLiteralExpression(ArrayTypeIF type,
			ExpressionIF[] values) throws SyntaxException {
		return new ObjectLiteralExpression(this, values, type, literalCount++,
				objectLiteralCount++);
	}

	@Override
	public ArrayTypeIF arrayType(TypeIF elementType) {
		return typeFactory.arrayType(elementType);
	}

	@Override
	public ArrayTypeIF arrayType(TypeIF baseType, int dimension) {
		ArrayTypeIF type = arrayType(baseType);

		if (dimension < 1)
			throw new IllegalArgumentException(
					"Array must have dimension at least 1: " + dimension);
		for (int i = 1; i < dimension; i++) {
			type = arrayType(type);
		}
		return type;
	}

	@Override
	public LiteralExpressionIF booleanLiteralExpression(boolean value) {
		return new LiteralExpression(this, value, literalCount++);
	}

	@Override
	public TypeIF booleanType() {
		return typeFactory.booleanType();
	}

	private BoundExpression boundExpression(Quantifier quantifier,
			BoundVariableIF boundVariable, ExpressionIF restriction,
			ExpressionIF expression) throws SyntaxException {
		BoundExpression result = new BoundExpression(this, quantifier,
				boundVariable, restriction, expression);

		// was: orExpression(notExpression(restriction),expression)

		BoundScope boundScope = (BoundScope) boundVariable.scope();
		boundScope.setExpression(result);
		// need to check that the expression and the restriction are in scope.
		// for collective assertions, can have variables in expression
		// from other scopes.
		// really only concerned that the BoundVariables
		// that occur here are in scope. Don't care about the other variables.
		// Their scope will get checked when expression is attached to model.
		for (VariableIF variable : restriction.freeVariables())
			if (variable.scope().kind() == ScopeKind.BOUND)
				checkScope(variable, boundScope, restriction);
		for (VariableIF variable : expression.freeVariables())
			if (variable.scope().kind() == ScopeKind.BOUND)
				checkScope(variable, boundScope, restriction);
		return result;
	}

	@Override
	public UnaryExpressionIF castExpression(TypeIF newType,
			ExpressionIF expression) throws SyntaxException {
		return new CastExpression(this, newType, (Expression) expression);
	}

	@Override
	public LiteralExpressionIF characterLiteralExpression(char value) {
		return new LiteralExpression(this, value, literalCount++);
	}

	@Override
	public TypeIF characterType() {
		return typeFactory.characterType();
	}

	@Override
	public void checkScope(ExpressionIF expression, ScopeIF scope)
			throws SyntaxException {
		for (VariableIF variable : expression.freeVariables())
			checkScope(variable, scope, expression);
	}

	/**
	 * Checks that isInScope(variable, scope) holds. If not, a SyntaxException
	 * is thrown with meaningful readable message. The expression is only used
	 * to form the message.
	 */
	void checkScope(VariableIF variable, ScopeIF scope, ExpressionIF expression)
			throws SyntaxException {
		if (!isInScope(variable, scope))
			throw new SyntaxException(expression, " variable " + variable
					+ " cannot be used in expression:"
					+ "\nScope of variable: " + variable.scope()
					+ "\nScope of expression: " + scope);
	}

	@Override
	public DereferenceExpressionIF dereferenceExpression(ExpressionIF argument)
			throws SyntaxException {
		return new DereferenceExpression(this, (Expression) argument);
	}

	@Override
	public BinaryExpressionIF divideExpression(ExpressionIF left,
			ExpressionIF right) throws SyntaxException {
		Expression arg0 = (Expression) left;
		Expression arg1 = (Expression) right;

		if (left.type().kind() == TypeKind.INTEGER
				&& right.type().kind() == TypeKind.RATIONAL) {
			arg0 = (Expression) castExpression(right.type(), left);
		} else if (left.type().kind() == TypeKind.RATIONAL
				&& right.type().kind() == TypeKind.INTEGER) {
			arg1 = (Expression) castExpression(left.type(), right);
		}
		return new DivideExpression(this, arg0, arg1);
	}

	@Override
	public BinaryExpressionIF equalsExpression(ExpressionIF left,
			ExpressionIF right) throws SyntaxException {
		Expression arg0 = (Expression) left;
		Expression arg1 = (Expression) right;

		if (left.type().kind() == TypeKind.INTEGER
				&& right.type().kind() == TypeKind.RATIONAL) {
			arg0 = (Expression) castExpression(right.type(), left);
		} else if (left.type().kind() == TypeKind.RATIONAL
				&& right.type().kind() == TypeKind.INTEGER) {
			arg1 = (Expression) castExpression(left.type(), right);
		}
		return new EqualsExpression(this, arg0, arg1);
	}

	@Override
	public EvaluatedFunctionExpressionIF evaluatedFunctionExpression(
			AbstractFunctionIF function, ExpressionIF[] arguments) {
		return new EvaluatedFunctionExpression(this,
				(AbstractFunction) function, arguments);
	}

	@Override
	public BoundExpression existsExpression(BoundVariableIF boundVariable,
			ExpressionIF restriction, ExpressionIF expression)
			throws SyntaxException {
		return boundExpression(Quantifier.EXISTS, boundVariable, restriction,
				expression);

	}

	@Override
	public BoundExpression forallExpression(BoundVariableIF boundVariable,
			ExpressionIF restriction, ExpressionIF expression)
			throws SyntaxException {
		return boundExpression(Quantifier.FORALL, boundVariable, restriction,
				expression);
	}

	public EvaluatedFunctionExpressionIF functionExpression(
			AbstractFunctionIF function, ExpressionIF[] coordinates) {
		return new EvaluatedFunctionExpression(this, function, coordinates);
	}

	@Override
	public FunctionTypeIF functionType(TypeIF[] inputTypes, TypeIF outputType) {
		return typeFactory.functionType(inputTypes, outputType);
	}

	@Override
	public ModelIF getModel(int modelId) {
		return models.get(modelId);
	}

	@Override
	public RecordTypeIF getRecordType(String name) {
		return typeFactory.getRecordType(name);
	}

	@Override
	public IfThenElseExpressionIF ifThenElseExpression(ExpressionIF condition,
			ExpressionIF trueValue, ExpressionIF falseValue)
			throws SyntaxException {
		return new IfThenElseExpression(this, condition, trueValue, falseValue);
	}

	@Override
	public LiteralExpressionIF integerLiteralExpression(int value) {
		return new LiteralExpression(this, value, literalCount++);
	}

	@Override
	public LiteralExpressionIF integerLiteralExpression(String string) {
		return new LiteralExpression(this, numberFactory.integer(string),
				literalCount++);
	}

	@Override
	public TypeIF integerType() {
		return typeFactory.integerType();
	}

	@Override
	public boolean isDescendantOf(ScopeIF scope1, ScopeIF scope2) {
		while (scope1 != null) {
			if (scope1.equals(scope2))
				return true;
			scope1 = scope1.parent();
		}
		return false;
	}

	@Override
	public boolean isInScope(VariableIF variable, ScopeIF scope) {
		return isDescendantOf(scope, variable.scope());
	}

	// TODO: this could be improved by keeping track of ancestors
	// of scopes.
	@Override
	public ScopeIF join(ScopeIF scope1, ScopeIF scope2) {
		for (ScopeIF scope1a = scope1; scope1a != null; scope1a = scope1a
				.parent())
			for (ScopeIF scope2a = scope2; scope2a != null; scope2a = scope2a
					.parent())
				if (scope1a.equals(scope2a))
					return scope2a;
		return null;
	}

	@Override
	public BoundExpression lambdaExpression(BoundVariableIF boundVariable,
			ExpressionIF restriction, ExpressionIF expression)
			throws SyntaxException {
		return boundExpression(Quantifier.LAMBDA, boundVariable, restriction,
				expression);
	}

	@Override
	public UnaryExpressionIF lengthExpression(ExpressionIF array)
			throws SyntaxException {
		return new LengthExpression(this, (Expression) array);
	}

	@Override
	public BinaryExpressionIF lessThanExpression(ExpressionIF left,
			ExpressionIF right) throws SyntaxException {
		Expression arg0 = (Expression) left;
		Expression arg1 = (Expression) right;

		if (left.type().kind() == TypeKind.INTEGER
				&& right.type().kind() == TypeKind.RATIONAL) {
			arg0 = (Expression) castExpression(right.type(), left);
		} else if (left.type().kind() == TypeKind.RATIONAL
				&& right.type().kind() == TypeKind.INTEGER) {
			arg1 = (Expression) castExpression(left.type(), right);
		}
		return new LessThanExpression(this, arg0, arg1);
	}

	@Override
	public BinaryExpressionIF lessThanOrEqualsExpression(ExpressionIF left,
			ExpressionIF right) throws SyntaxException {
		Expression arg0 = (Expression) left;
		Expression arg1 = (Expression) right;

		if (left.type().kind() == TypeKind.INTEGER
				&& right.type().kind() == TypeKind.RATIONAL) {
			arg0 = (Expression) castExpression(right.type(), left);
		} else if (left.type().kind() == TypeKind.RATIONAL
				&& right.type().kind() == TypeKind.INTEGER) {
			arg1 = (Expression) castExpression(left.type(), right);
		}
		return new LessThanOrEqualsExpression(this, arg0, arg1);
	}

	@Override
	public int libraryId(String libraryName) {
		LibraryInfo info = this.libraryInfoMap.get(libraryName);

		if (info == null)
			return -1;
		else
			return info.libraryId();
	}

	@Override
	public String libraryName(int libraryId) {
		if (libraryId >= 0 && libraryId < libraryInfoVector.size())
			return libraryInfoVector.get(libraryId).libraryName();
		return null;
	}

	@Override
	public LiteralExpressionIF literalExpression(String string) {
		return new LiteralExpression(this, string, literalCount++);
	}

	@Override
	public ModelTransformerLoaderIF modelTransformerLoader() {
		return loader;
	}

	@Override
	public BinaryExpressionIF moduloExpression(ExpressionIF left,
			ExpressionIF right) throws SyntaxException {
		return new ModuloExpression(this, (Expression) left, (Expression) right);
	}

	@Override
	public BinaryExpressionIF multiplyExpression(ExpressionIF left,
			ExpressionIF right) throws SyntaxException {
		Expression arg0 = (Expression) left;
		Expression arg1 = (Expression) right;

		if (left.type().kind() == TypeKind.INTEGER
				&& right.type().kind() == TypeKind.RATIONAL) {
			arg0 = (Expression) castExpression(right.type(), left);
		} else if (left.type().kind() == TypeKind.RATIONAL
				&& right.type().kind() == TypeKind.INTEGER) {
			arg1 = (Expression) castExpression(left.type(), right);
		}
		return new MultiplyExpression(this, arg0, arg1);
	}

	@Override
	public NamedObjectLiteralExpressionIF namedArrayLiteralExpression(
			ArrayTypeIF type, LiteralExpressionIF[] literalArray, String name) {
		return new NamedObjectLiteralExpression(this, literalArray, type, name,
				literalCount++, objectLiteralCount++);
	}

	@Override
	public NamedLiteralExpressionIF namedBooleanLiteralExpression(
			boolean value, String name) {
		return new NamedLiteralExpression(this, value, name, literalCount++);
	}

	@Override
	public NamedLiteralExpressionIF namedCharacterLiteralExpression(char value,
			String name) {
		return new NamedLiteralExpression(this, value, name, literalCount++);
	}

	@Override
	public NamedLiteralExpressionIF namedIntegerLiteralExpression(int value,
			String name) {
		return new NamedLiteralExpression(this, value, name, literalCount++);
	}

	@Override
	public NamedLiteralExpressionIF namedIntegerLiteralExpression(
			String string, String name) {
		return new NamedLiteralExpression(this, numberFactory.integer(string),
				name, literalCount++);
	}

	@Override
	public NamedLiteralExpressionIF namedLiteralExpression(String string,
			String name) {
		return new NamedLiteralExpression(this, string, name, literalCount++);
	}

	@Override
	public NamedLiteralExpressionIF namedNullExpression(String name) {
		return new NamedLiteralExpression(this, typeFactory.voidPointerType(),
				name, literalCount++);
	}

	@Override
	public NamedLiteralExpressionIF namedRealLiteralExpression(String string,
			String name) {
		return new NamedLiteralExpression(this, numberFactory.rational(string),
				name, literalCount++);
	}

	@Override
	public NamedObjectLiteralExpressionIF namedRecordLiteralExpression(
			RecordTypeIF type, LiteralExpressionIF[] components, String name) {
		return new NamedObjectLiteralExpression(this, components, type, name,
				literalCount++, objectLiteralCount++);
	}

	@Override
	public UnaryExpressionIF negativeExpression(ExpressionIF expr)
			throws SyntaxException {
		return new NegativeExpression(this, (Expression) expr);
	}

	@Override
	public AbstractFunction newAbstractFunction(String name, TypeIF returnType,
			int numFormals) throws SyntaxException {
		AbstractFunction result = new AbstractFunction(systemScope, name,
				returnType, numFormals);

		systemScope.addFunction(result);
		return result;
	}

	/**
	 * This method creates a new bound scope and returns it. The expression
	 * associated to the new scope is null. User should use the new bound scope
	 * to create one or more bound variables using method newBoundVariable.
	 * These can then be used to create an expression e. Later, when the
	 * variable is used to create a bound expression (forall, exists, lambda,
	 * ...), the scope will be completed.
	 */
	public BoundScopeIF newBoundScope(ScopeIF parent) {
		return new BoundScope(parent);
	}

	/**
	 * A bound variable is bound in the sense of first order logic; it is a
	 * variable used in a quantified expression (forall, exists, lambda). Each
	 * bound variable has a unique ID number. This method creates a new bound
	 * variable and returns it. Scope is null, until it is completed during
	 * creation of bound expression (forall, exists, ...).
	 */
	@Override
	public BoundVariable newBoundVariable(String name, TypeIF type,
			BoundScopeIF boundScope) throws SyntaxException {
		BoundVariable variable = new BoundVariable(name, type,
				(BoundScope) boundScope, boundVariableCount);

		boundVariableCount++;
		((BoundScope) boundScope).addBoundVariable(variable);
		return variable;
	}

	@Override
	public FormalVariableIF newFormalVariable(AbstractFunctionIF function,
			TypeIF type, String name, int index) throws SyntaxException {
		FormalVariable result = new FormalVariable(name, type,
				(LocalScope) function.outermostScope(), index);

		((Function) function).setFormal(result);
		return result;
	}

	@Override
	public ModelIF newModel(String name, int numProcs) {
		int modelCount = models.size();
		ModelIF result = new Model(modelCount, name, numProcs, this);

		models.add(result);
		return result;
	}

	@Override
	public PointerTypeIF newPointerType() {
		return typeFactory.newPointerType();
	}

	@Override
	public NotEmptyExpressionIF notEmptyExpression(ModelIF model,
			ExpressionIF source, ExpressionIF destination, ExpressionIF tag) {
		return new NotEmptyExpression(this, model, (Expression) source,
				(Expression) destination, (Expression) tag);
	}

	@Override
	public UnaryExpressionIF notExpression(ExpressionIF expr)
			throws SyntaxException {
		return new NotExpression(this, (Expression) expr);
	}

	@Override
	public NotFullExpressionIF notFullExpression(ModelIF model,
			ExpressionIF source, ExpressionIF destination, ExpressionIF tag) {
		return new NotFullExpression(this, model, (Expression) source,
				(Expression) destination, (Expression) tag);
	}

	@Override
	public LiteralExpressionIF nullExpression() {
		return new LiteralExpression(this, typeFactory.voidPointerType(),
				literalCount++);
	}

	@Override
	public NumberFactoryIF numberFactory() {
		return numberFactory;
	}

	@Override
	public int numLibraries() {
		return libraryInfoVector.size();
	}

	@Override
	public int numModels() {
		return models.size();
	}

	@Override
	public int numTypes() {
		return typeFactory.numTypes();
	}

	@Override
	public BinaryExpressionIF orExpression(ExpressionIF left, ExpressionIF right)
			throws SyntaxException {
		return new OrExpression(this, (Expression) left, (Expression) right);
	}

	@Override
	public BinaryExpressionIF pointerAddExpression(
			ExpressionIF pointerExpression, ExpressionIF integerExpression) {
		return new PointerAddExpression(this, (Expression) pointerExpression,
				(Expression) integerExpression);
	}

	@Override
	public PointerTypeIF pointerType(TypeIF baseType) {
		return typeFactory.pointerType(baseType);
	}

	@Override
	public ProcessReferenceExpressionIF processReferenceExpression(
			ModelIF model, ExpressionIF pid, String variableName) {
		return new ProcessReferenceExpression(this, model, pid, variableName);
	}

	@Override
	public TypeIF rationalType() {
		return typeFactory.rationalType();
	}

	@Override
	public LiteralExpressionIF realLiteralExpression(String string) {
		return new LiteralExpression(this, numberFactory.rational(string),
				literalCount++);
	}

	@Override
	public ObjectLiteralExpressionIF recordLiteralExpression(RecordTypeIF type,
			ExpressionIF[] components) {
		return new ObjectLiteralExpression(this, components, type,
				literalCount++, objectLiteralCount++);
	}

	private RecordNavigationExpressionIF recordNavigationExpression(
			LHSExpressionIF recordExpression, int fieldIndex) {
		return new RecordNavigationExpression(this, recordExpression,
				fieldIndex);
	}

	@Override
	public RecordNavigationExpressionIF recordNavigationExpression(
			LHSExpressionIF recordExpression, String fieldName)
			throws SyntaxException {
		RecordTypeIF recordType = (RecordTypeIF) recordExpression.type();
		int numFields = recordType.numFields();
		int fieldIndex = -1;

		for (int i = 0; i < numFields; i++) {
			if (recordType.fieldName(i).equals(fieldName)) {
				fieldIndex = i;
				break;
			}
		}
		if (fieldIndex < 0)
			throw new SyntaxException(recordExpression, "Record type "
					+ recordType + " has no field named " + fieldName + "\n"
					+ recordType.longName());
		return recordNavigationExpression(recordExpression, fieldIndex);
	}

	@Override
	public RecordTypeIF recordType(String name, String[] fieldNames,
			TypeIF[] fieldTypes, ExpressionIF[][] dimensionExpressions) {
		return typeFactory.recordType(name, fieldNames, fieldTypes,
				dimensionExpressions);
	}

	/** Sets the libraryInfo and id for the function. */
	public void registerSystemFunction(String libraryName,
			SystemFunctionIF function) throws SyntaxException {
		LibraryInfo libraryInfo = libraryInfoMap.get(libraryName);

		if (libraryInfo == null) {
			libraryInfo = new LibraryInfo(libraryName, libraryInfoVector.size());
			libraryInfoVector.add(libraryInfo);
			libraryInfoMap.put(libraryName, libraryInfo);
		}
		libraryInfo.register(function);
	}

	@Override
	public PointerTypeIF setBaseType(PointerTypeIF pointerType, TypeIF baseType) {
		return typeFactory.setBaseType(pointerType, baseType);
	}

	@Override
	public void setModelTransformerLoader(ModelTransformerLoaderIF loader) {
		this.loader = loader;
	}

	@Override
	public AbstractFunctionIF sizeofAbstractFunction() {
		return sizeOfType;
	}

	@Override
	public SizeOfExpressionIF sizeOfExpression(TypeIF type) {
		SizeOfExpressionIF result = new SizeOfExpression(this, type);

		return result;
	}

	@Override
	public SubscriptExpressionIF subscriptExpression(LHSExpressionIF array,
			ExpressionIF index) throws SyntaxException {
		return new SubscriptExpression(this, array, (Expression) index);
	}

	@Override
	public BinaryExpressionIF subtractExpression(ExpressionIF left,
			ExpressionIF right) throws SyntaxException {
		Expression arg0 = (Expression) left;
		Expression arg1 = (Expression) right;

		if (left.type().kind() == TypeKind.INTEGER
				&& right.type().kind() == TypeKind.RATIONAL) {
			arg0 = (Expression) castExpression(right.type(), left);
		} else if (left.type().kind() == TypeKind.RATIONAL
				&& right.type().kind() == TypeKind.INTEGER) {
			arg1 = (Expression) castExpression(left.type(), right);
		}
		return new SubtractExpression(this, arg0, arg1);
	}

	@Override
	public ScopeIF systemScope() {
		return systemScope;
	}

	@Override
	public TypeIF type(int id) {
		return typeFactory.type(id);
	}

	@Override
	public VariableExpressionIF variableExpression(VariableIF variable) {
		return new VariableExpression(this, (Variable) variable);
	}

	@Override
	public VectorTypeIF vectorType(TypeIF elementType) {
		return typeFactory.vectorType(elementType);
	}

	@Override
	public TypeIF voidType() {
		return typeFactory.voidType();
	}

}