package in.sivareddy.lambda;

import java.util.List;
import java.util.Set;

import com.google.common.base.Preconditions;
import com.google.common.collect.ImmutableList;

public class QuantifierExpression extends AbstractExpression {
  private static final long serialVersionUID = 1L;

  private final String quantifierName;
  private final List<ConstantExpression> boundVariables;
  private final Expression body;

  public QuantifierExpression(String quantifierName,
      List<ConstantExpression> boundVariables, Expression body) {
    this.quantifierName = quantifierName;
    this.boundVariables = ImmutableList.copyOf(boundVariables);
    this.body = Preconditions.checkNotNull(body);
  }

  public String getQuantifierName() {
    return quantifierName;
  }

  /**
   * Returns the body of the statement, i.e., the portion of the statement over
   * which the quantifier the quantifier has scope.
   *
   * @return
   */
  public Expression getBody() {
    return body;
  }

  /**
   * Gets the variables which are bound by this quantifier.
   *
   * @return
   */
  public List<ConstantExpression> getBoundVariables() {
    return boundVariables;
  }

  @Override
  public void getFreeVariables(Set<Expression> accumulator) {
    body.getFreeVariables(accumulator);
    accumulator.removeAll(boundVariables);
  }

  @Override
  public Expression substitute(Expression constant, Expression replacement) {
    if (!boundVariables.contains(constant)) {
      Expression substitution = body.substitute(constant, replacement);
      return new QuantifierExpression(quantifierName, boundVariables,
          substitution);
    } else {
      return this;
    }
  }

  @Override
  public Expression simplify() {
    Expression simplifiedBody = body.simplify();
    return new QuantifierExpression(quantifierName, boundVariables,
        simplifiedBody);
  }

  @Override
  public String toString() {
    StringBuilder sb = new StringBuilder();
    sb.append("(");
    sb.append(quantifierName);
    for (Expression argument : boundVariables) {
      sb.append(" ");
      sb.append(argument.toString());
    }

    sb.append(" ");
    sb.append(body.toString());
    sb.append(")");
    return sb.toString();
  }

  @Override
  public int hashCode() {
    final int prime = 31;
    int result = 1;
    result = prime * result + ((body == null) ? 0 : body.hashCode());
    result =
        prime * result
            + ((boundVariables == null) ? 0 : boundVariables.hashCode());
    result =
        prime * result
            + ((quantifierName == null) ? 0 : quantifierName.hashCode());
    return result;
  }

  @Override
  public boolean equals(Object obj) {
    if (this == obj) {
      return true;
    }
    if (obj == null) {
      return false;
    }
    if (getClass() != obj.getClass()) {
      return false;
    }
    QuantifierExpression other = (QuantifierExpression) obj;
    if (body == null) {
      if (other.body != null) {
        return false;
      }
    } else if (!body.equals(other.body)) {
      return false;
    }
    if (boundVariables == null) {
      if (other.boundVariables != null) {
        return false;
      }
    } else if (!boundVariables.equals(other.boundVariables)) {
      return false;
    }
    if (quantifierName == null) {
      if (other.quantifierName != null) {
        return false;
      }
    } else if (!quantifierName.equals(other.quantifierName)) {
      return false;
    }
    return true;
  }
}
