package inference.axioms;

import java.util.Map;

import inference.EquationAxiom;
import inference.InferenceOrderConstraint;
import models.algebra.Variable;
import models.formulas.meta.MetaEquationFormula;
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;
import utils.ExpressionUtils;

public class Constantness extends EquationAxiom{

	public Constantness() {
		super("Constantness");
		defaultOrderConstraint = new InferenceOrderConstraint(new Variable("n"), OrderConstraint.LT, new Variable("m"));
		
		conclusion = new MetaEquationFormula(
				new MetaDynamicDependencyTerm(
						new MetaTermGenerator() {
							@Override
							public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<Object, Object> context) {
								if (curDepth == maxDepth && curIndex == 0) {
									return new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n"));
								} else if (curIndex == 0) {
									return new MetaDynamicDependencyTerm(this);
								}
								curIndex -= 1;
								if (curIndex % 2 == 0) {
									return new MetaEvaluatableTermVariable(new Variable("te" + curDepth + "_" + curIndex / 2), ExpressionUtils.parse("m-" + (maxDepth - curDepth)));
								}
								return new MetaEvaluatableTermVariable(new Variable("ue" + curDepth + "_" + curIndex / 2));
							}
						}
				),
				new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n"))
		);
	}
	
}