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;
import utils.ExpressionUtils;

public class Uncurrying extends EquationAxiom {

	public Uncurrying() {
		super("Uncurrying");
		
		assumptions.add(new MetaDependencyFormula(
				new MetaDynamicDependency(
						new MetaTermGenerator() {
							@Override
							public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<String, Object> context) {
								context.put("" + curDepth, maxIndex + 1);
								context.put("i", Math.max(maxDepth - curDepth, (Integer) context.getOrDefault("i", 0)));
								if (curDepth == maxDepth && curIndex == 0) {
									return new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n"));
								} else if (curDepth == maxDepth && curIndex == 1) {
									return new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n"));
								} else if (curIndex == 0) {
									return new MetaDynamicDependency(this);
								}
								return new MetaEvaluatableTermVariable(new Variable("te" + curDepth + "_" + curIndex), ExpressionUtils.parse("n-" + (maxDepth - curDepth)));
							}
						}
				)
		));
		
		conclusion = new MetaEquationFormula(
				new MetaDynamicDependencyTerm(
						new MetaTermGenerator() {
							@Override
							public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<String, Object> context) {
								maxIndex = (Integer) context.get(""+curDepth);
								int i = (Integer) context.get("i");
								if (curDepth == maxDepth) {
									if (curIndex == 0) {
										return new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n"));
									} else if (curIndex == 1) {
										return new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n"));
									} else if (curIndex == 2) {
										return new MetaEvaluatableTermVariable(new Variable("ve"), ExpressionUtils.parse("n-" + i));
									}
								} else if (curIndex == 0) {
									return new MetaDynamicDependencyTerm(this);
								}
								curIndex -= 1;
								if (curIndex >= maxIndex * 2) {
									if (i == maxDepth - curDepth && curIndex == maxIndex * 2) {
										return new MetaEvaluatableTermVariable(new Variable("ve"), ExpressionUtils.parse("n-" + i));
									} else if (i == maxDepth - curDepth && curIndex == maxIndex * 2 + 1) {
										return new MetaEvaluatableTermVariable(new Variable("we"));
									}
									return null;
								}
								if (curIndex % 2 == 0) {
									return new MetaEvaluatableTermVariable(new Variable("te" + curDepth + "_" + curIndex / 2), ExpressionUtils.parse("n-" + (maxDepth - curDepth))); 
								}
								return new MetaEvaluatableTermVariable(new Variable("ue" + curDepth + "_" + curIndex / 2));
							}
						}
				),
				new MetaDynamicDependencyTerm(
						new MetaTermGenerator() {
							@Override
							public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<String, Object> context) {
								maxIndex = (Integer) context.get(""+curDepth);
								if (curDepth == maxDepth) {
									if (curIndex == 0) {
										return new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n"));
									} else if (curIndex == 1) {
										return new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n"));
									} else if (curIndex == 2) {
										return new MetaEvaluatableTermVariable(new Variable("we"));
									}
								} else if (curIndex == 0) {
									return new MetaDynamicDependencyTerm(this);
								}
								curIndex -= 1;
								if (curIndex >= maxIndex * 2) {
									return null;
								}
								if (curIndex % 2 == 0) {
									return new MetaEvaluatableTermVariable(new Variable("te" + curDepth + "_" + curIndex / 2), ExpressionUtils.parse("n-" + (maxDepth - curDepth))); 
								}
								return new MetaEvaluatableTermVariable(new Variable("ue" + curDepth + "_" + curIndex / 2));
							}
						}
				)
		);
	}

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