package inference.axioms;

import java.util.Map;

import inference.InferenceOrderConstraint;
import inference.InferenceRule;
import models.algebra.Variable;
import models.formulas.meta.MetaDependencyFormula;
import models.terms.meta.MetaDynamicDependency;
import models.terms.meta.MetaEvaluatableTermVariable;
import models.terms.meta.MetaRDLTerm;
import models.terms.meta.MetaTermGenerator;
import models.terms.meta.OrderConstraint;

public class ConstantMapping extends InferenceRule {

	public ConstantMapping() {
		super("Constant Mapping");
		defaultOrderConstraint = new InferenceOrderConstraint(new Variable("n"), OrderConstraint.LT, new Variable("m"));
		conclusion = new MetaDependencyFormula(
				new MetaDynamicDependency(
						new MetaTermGenerator() {
							@Override
							public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<Object, Object> context) {
								curIndex -= 1;
								return new MetaEvaluatableTermVariable(new Variable("te" + curIndex), new Variable("m"));
							}
						},
						new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n"))
				)
		);
	}
	
}