package inference.axioms;

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

import inference.EquationAxiom;
import inference.InferenceOrderConstraint;
import models.algebra.Constant;
import models.algebra.Variable;
import models.formulas.DependencyFormula;
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;
import models.terms.meta.OrderConstraint;

public class PseudoConstantness extends EquationAxiom {

	public PseudoConstantness() {
		super("Pseudo-Constantness");
		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 -= 1;
								return new MetaEvaluatableTermVariable(new Variable("te" + curIndex), new Variable("n"));
							}
						},
						new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n"))
				)
		));
		defaultOrderConstraint = new InferenceOrderConstraint(new Variable("n"), OrderConstraint.GT, new Constant("0"));
		
		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;
								return new MetaEvaluatableTermVariable(new Variable("te" + curIndex / 2), new Variable("n"));
							}
						},
						new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n"))
				),
				new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n"))
		);
	}
	
	@Override
	public Set<EvaluatableTerm> apply(List<Formula> assumptions, EvaluatableTerm term, MatchConstraint constraint) {
		constraint.getContext().put("maxIndex", ((DependencyFormula) assumptions.get(0)).getDependency().getMaxIndex() * 2 - 1);
		constraint.getContext().put("maxDepth", 1);
		return super.apply(assumptions, term, constraint);
	}
	
}