package models.formulas.meta;

import java.util.Map;

import exceptions.IllegalTypeException;
import lombok.Getter;
import models.algebra.Variable;
import models.formulas.Formula;
import models.formulas.InFormula;
import models.terms.EvaluatableTerm;
import models.terms.RDLTerm;
import models.terms.meta.MetaRDLTerm;
import models.terms.meta.OrderVariableConstraint;

@Getter
public class MetaInFormula extends MetaFormula {

	private MetaRDLTerm leftSideHand;
	private MetaRDLTerm rightSideHand;
	
	public MetaInFormula(MetaRDLTerm leftSideHand, MetaRDLTerm rightSideHand) {
		if (! leftSideHand.isEvaluatableTerm()) {
			throw new IllegalTypeException();
		}
		if(! rightSideHand.isEvaluatableTerm()) {
			throw new IllegalTypeException();
		}
		this.leftSideHand = leftSideHand;
		this.rightSideHand = rightSideHand;
	}
	
	@Override
	public boolean isMatchedBy(Formula formula, Map<Variable, RDLTerm> binding,
			Map<Variable, OrderVariableConstraint> orderConstraint) {
		if (! (formula instanceof InFormula)) {
			return false;
		}
		InFormula inFormula = (InFormula) formula;
		return leftSideHand.isMatchedBy(inFormula.getLeftSideHand(), binding, orderConstraint) 
				&& rightSideHand.isMatchedBy(inFormula.getRightSideHand(), binding, orderConstraint);
	}
	
	@Override
	public InFormula substitution(Map<Variable, RDLTerm> binding) {
		return new InFormula((EvaluatableTerm) leftSideHand.substitute(binding), (EvaluatableTerm) rightSideHand.substitute(binding));
	}
	

	@Override
	public String toString() {
		return leftSideHand.toString() + " in " + rightSideHand.toString();
	}

	@Override
	public boolean equals(Object anohter) {
		if (! (anohter instanceof MetaInFormula)) {
			return false;
		}
		MetaInFormula formula = (MetaInFormula) anohter;
		return leftSideHand.equals(formula.getLeftSideHand()) && rightSideHand.equals(formula.getRightSideHand());
	}

	@Override
	public int hashCode() {
		return toString().hashCode();
	}

}