ASTQuantifierExpression.java

package edu.udel.cis.vsl.tass.front.minimp.ast.expression;

import edu.udel.cis.vsl.tass.front.minimp.ast.type.ASTBoolType;
import edu.udel.cis.vsl.tass.model.IF.SyntaxException;

public class ASTQuantifierExpression extends ASTExpression {
	public enum QuantifierKind {
		FORALL, EXISTS
	};

	private QuantifierKind kind;

	private ASTExpressionIF variable;
	private ASTExpressionIF expr;
	private ASTExpressionIF boundExpression;

	public ASTQuantifierExpression(QuantifierKind kind, ASTExpressionIF var,
			ASTExpressionIF boundExpression, ASTExpressionIF expression)
			throws SyntaxException {
		super(new ASTBoolType());
		this.kind = kind;
		if (boundExpression != null
				&& !(boundExpression.getType() instanceof ASTBoolType)) {
			throw new SyntaxException(this,
					"Bounds expression must have boolean type instead of "
							+ boundExpression.getType());
		}

		if (!(expression.getType() instanceof ASTBoolType)) {
			throw new SyntaxException(
					"Quantifier expression must have boolean type instead of "
							+ expression.getType());
		}

		this.expr = expression;
		this.variable = var;
		this.boundExpression = boundExpression;
	}

	public ASTExpressionIF getBoundExpression() {
		return boundExpression;
	}

	public QuantifierKind getQuantifierKind() {
		return this.kind;
	}

	public ASTExpressionIF getExpr() {
		return this.expr;
	}

	public String toString() {
		String result;
		if (this.kind == QuantifierKind.FORALL) {
			result = "(forall ";
		} else {
			result = "(exists ";
		}
		result += this.variable + "" + this.expr + ")";
		return result;
	}

	public ASTExpressionIF getVariable() {
		return variable;
	}
}