package inference.axioms;

import java.util.HashSet;
import java.util.List;
import java.util.Map;
import java.util.Set;

import exceptions.SubstituteFailedException;
import inference.EquationAxiom;
import models.algebra.Variable;
import models.formulas.EquationFormula;
import models.formulas.Formula;
import models.formulas.meta.MetaEquationFormula;
import models.terms.EvaluatableTerm;
import models.terms.meta.MatchConstraint;
import models.terms.meta.MetaDynamicDependencyTerm;
import models.terms.meta.MetaEvaluatableTermVariable;
import models.terms.meta.MetaRDLTerm;
import models.terms.meta.MetaTermGenerator;

public class LeftSubstitution extends EquationAxiom {

	public LeftSubstitution() {
		super("Left Substitution");
		assumptions.add(new MetaEquationFormula(
				new MetaEvaluatableTermVariable(new Variable("se")),
				new MetaEvaluatableTermVariable(new Variable("te"))
		));
		conclusion = new MetaEquationFormula(
				new MetaDynamicDependencyTerm(
						new MetaTermGenerator() {
							@Override
							public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth,  Map<String, Object> context) {
								curIndex -= 1;
								if (curIndex % 2 == 0) {
									return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex / 2));
								}
								return new MetaEvaluatableTermVariable(new Variable("ve" + curIndex / 2));
							}
						},
						new MetaEvaluatableTermVariable(new Variable("se"))		
				),
				new MetaDynamicDependencyTerm(
						new MetaTermGenerator() {
							@Override
							public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth,  Map<String, Object> context) {
								curIndex -= 1;
								if (curIndex % 2 == 0) {
									return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex / 2));
								}
								return new MetaEvaluatableTermVariable(new Variable("ve" + curIndex / 2));
							}
						},
						new MetaEvaluatableTermVariable(new Variable("te"))		
				)
		);
	}
	
	@Override
	public Set<EvaluatableTerm> apply(List<Formula>assumptions,  EvaluatableTerm term) {
		Set<EvaluatableTerm> result = new HashSet<>();
		boolean isLeft = true;
		if (assumptions.size() < this.assumptions.size()) {
			return new HashSet<>();
		}
		Set<MatchConstraint> matchResult = assumptionMatch(assumptions);
		
		MetaEquationFormula metaConclusion = (MetaEquationFormula) this.conclusion;
		Set<MatchConstraint> conclusionMatchResult = conclusionLeftSideHandMatch(term, matchResult);
		if (conclusionMatchResult.isEmpty()) {
			isLeft = false;
			conclusionMatchResult = conclusionRightSideHandMatch(term, matchResult);
			if (conclusionMatchResult.isEmpty()) {
				return new HashSet<>();
			}
		}
		for (MatchConstraint matchRes: conclusionMatchResult) {
			matchRes.getContext().put("maxIndex", term.getMaxIndex());
			matchRes.getContext().put("maxDepth", term.getMaxDepth());
			try {
				EquationFormula eq = metaConclusion.substitution(matchRes.getBinding(), matchRes.getContext());
				if (isLeft) {
					result.add(eq.getRightSideHand());
				} else {
					result.add(eq.getLeftSideHand());
				}
			} catch (SubstituteFailedException e) {
				continue;
			}
		}
		return result;
	}

}