BoundExpression.java

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

import static edu.udel.cis.vsl.tass.model.IF.expression.BoundExpressionIF.Quantifier.EXISTS;
import static edu.udel.cis.vsl.tass.model.IF.expression.BoundExpressionIF.Quantifier.FORALL;
import static edu.udel.cis.vsl.tass.model.IF.expression.BoundExpressionIF.Quantifier.LAMBDA;
import edu.udel.cis.vsl.tass.model.IF.ModelFactoryIF;
import edu.udel.cis.vsl.tass.model.IF.expression.BoundExpressionIF;
import edu.udel.cis.vsl.tass.model.IF.expression.ExpressionIF;
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.variable.BoundVariableIF;

public class BoundExpression extends Expression implements BoundExpressionIF {

	private Quantifier quantifier;

	private BoundVariableIF boundVariable;

	private ExpressionIF boundRestriction;

	private ExpressionIF expression;

	/**
	 * Create new BoundExpression with given data. After this constructor is
	 * called, the caller should set the expression in the bound scope to this
	 * expression.
	 */
	public BoundExpression(ModelFactoryIF factory, Quantifier quantifier,
			BoundVariableIF boundVariable, ExpressionIF boundRestriction,
			ExpressionIF expression) {
		super(factory,
				(quantifier == EXISTS ? ExpressionKind.EXISTS
						: (quantifier == FORALL ? ExpressionKind.FORALL
								: (quantifier == LAMBDA ? ExpressionKind.LAMBDA
										: null))));
		if (quantifier == EXISTS || quantifier == FORALL) {
			type = factory.booleanType();
		} else {
			type = factory.functionType(new TypeIF[] { boundVariable.type() },
					expression.type());
		}
		assert boundRestriction.type().kind() == TypeKind.BOOLEAN;
		this.quantifier = quantifier;
		this.boundVariable = boundVariable;
		this.boundRestriction = boundRestriction;
		this.expression = expression;
		freeVariables.addAll(this.expression.freeVariables());
		freeVariables.addAll(this.boundRestriction.freeVariables());
		freeVariables.remove(boundVariable);
	}

	public BoundExpression(ModelFactoryIF factory, Quantifier quantifier,
			BoundVariableIF boundVariable, ExpressionIF expression) {
		this(factory, quantifier, boundVariable, factory
				.booleanLiteralExpression(true), expression);
	}

	public BoundVariableIF boundVariable() {
		return boundVariable;
	}

	public ExpressionIF boundRestriction() {
		return boundRestriction;
	}

	public ExpressionIF expression() {
		return expression;
	}

	public String toString() {
		return quantifier + " { " + boundVariable.type() + " " + boundVariable
				+ " | " + boundRestriction + "}" + expression.atomString();
	}

	public String atomString() {
		return "(" + toString() + ")";
	}

	@Override
	public Quantifier operator() {
		return quantifier;
	}

}