package inference.axioms;

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

import inference.EquationAxiom;
import models.algebra.Variable;
import models.formulas.Formula;
import models.formulas.meta.MetaDependencyFormula;
import models.formulas.meta.MetaEquationFormula;
import models.terms.EvaluatableTerm;
import models.terms.meta.MatchConstraint;
import models.terms.meta.MetaDynamicDependency;
import models.terms.meta.MetaDynamicDependencyTerm;
import models.terms.meta.MetaEvaluatableTermVariable;
import models.terms.meta.MetaRDLTerm;
import models.terms.meta.MetaTermGenerator;

public class RightSubstitution extends EquationAxiom {
	
	public RightSubstitution() {
		super("Right Substitution");
		assumptions.add(new MetaEquationFormula(
				new MetaEvaluatableTermVariable(new Variable("ue")),
				new MetaEvaluatableTermVariable(new Variable("ve"))
		));
		assumptions.add(new MetaDependencyFormula(
				new MetaDynamicDependency(
						new MetaTermGenerator() {
							@Override
							public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<String, Object> context) {
								curIndex -= 2;
								return new MetaEvaluatableTermVariable(new Variable("xe" + curIndex));
							}
							
						},
						new MetaEvaluatableTermVariable(new Variable("se")),
						new MetaEvaluatableTermVariable(new Variable("te"))
				)
		));
		this.conclusion = new MetaEquationFormula(
				new MetaDynamicDependencyTerm(
						new MetaTermGenerator() {
							@Override
							public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<String, Object> context) {
								curIndex -= 3;
								if (curIndex % 2 == 0) {
									return new MetaEvaluatableTermVariable(new Variable("xe" + curIndex / 2));
								}
								return new MetaEvaluatableTermVariable(new Variable("x" + curIndex / 2));
							}
						},
						new MetaEvaluatableTermVariable(new Variable("se")),
						new MetaEvaluatableTermVariable(new Variable("te")),
						new MetaEvaluatableTermVariable(new Variable("ue"))
				),
				new MetaDynamicDependencyTerm(
						new MetaTermGenerator() {
							@Override
							public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<String, Object> context) {
								curIndex -= 3;
								if (curIndex % 2 == 0) {
									return new MetaEvaluatableTermVariable(new Variable("xe" + curIndex / 2));
								}
								return new MetaEvaluatableTermVariable(new Variable("x" + curIndex / 2));
							}
						},
						new MetaEvaluatableTermVariable(new Variable("se")),
						new MetaEvaluatableTermVariable(new Variable("te")),
						new MetaEvaluatableTermVariable(new Variable("ve"))
				)
		);
	}

	
	@Override
	public Set<EvaluatableTerm> apply(List<Formula>assumptions,  EvaluatableTerm term) {
		MatchConstraint constraint = MatchConstraint.createDefault();
		constraint.getContext().put("maxIndex", term.getMaxIndex());
		constraint.getContext().put("maxDepth", term.getMaxDepth());
		return apply(assumptions, term, constraint);
	}
	
}