package inference.axioms;

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

import exceptions.SubstituteFailedException;
import inference.InferenceRule;
import models.Position;
import models.algebra.Variable;
import models.formulas.Formula;
import models.formulas.meta.MetaDependencyFormula;
import models.terms.meta.MatchConstraint;
import models.terms.meta.MetaDependencyTerm;
import models.terms.meta.MetaDynamicDependency;
import models.terms.meta.MetaEvaluatableTermVariable;
import models.terms.meta.MetaRDLTerm;
import models.terms.meta.MetaTermGenerator;
import utils.ExpressionUtils;

public class UncurriedMapping extends InferenceRule{

	public UncurriedMapping() {
		super("Uncurried Mapping");
		assumptions.add(new MetaDependencyFormula(
				new MetaDynamicDependency(
						new MetaTermGenerator() {
							@Override
							public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<Object, Object> context) {
								int i = maxDepth - curDepth;
								context.put("i", Math.max(i, (Integer) context.getOrDefault("i", 0)));
								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"));
									}
									curIndex -= 1;
								} else if (curIndex == 0) {
									return new MetaDynamicDependency(this);
								}
								curIndex -= 1;
								return new MetaEvaluatableTermVariable(new Variable("te" + curDepth + "_" + curIndex), ExpressionUtils.parse("n-" + i));
							}
						}
				)
		));
		
		conclusion = new MetaDependencyFormula(
				new MetaDynamicDependency(
						new MetaTermGenerator() {
							@Override
							public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<Object, Object> context) {
								int i = (Integer) context.get("i");
								if (curDepth == maxDepth - 1 && curIndex == 0) {
									return new MetaDependencyTerm(
											new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")), 
											new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")), 
											new MetaEvaluatableTermVariable(new Variable("ve"), ExpressionUtils.parse("n-" + i)) 
									);
								} else if (curIndex == 0) {
									return new MetaDynamicDependency(this);
								} if (curDepth == 1) {
									if (curIndex == 1) {
										return new MetaEvaluatableTermVariable(new Variable("ve"), ExpressionUtils.parse("n-" + i)); 
									}
									curIndex -= 1;
								}
								curIndex -= 1;
								return new MetaEvaluatableTermVariable(new Variable("te" + curDepth + "_" + curIndex), ExpressionUtils.parse("n-" + i));
							}
						}
				)
		);
		
	}
	
	@Override
	public Set<Formula> derive(List<Formula> assumptions, MatchConstraint constraint) {
		Set<Formula> result = new HashSet<>();
		if (this.assumptions.size() != assumptions.size()) {
			return new HashSet<>();
		}
		Set<MatchConstraint> matchResult = assumptionMatch(assumptions, constraint);
		
		for (MatchConstraint res: matchResult) {
			try {
				int maxDepth = (Integer) res.getContext().get("maxDepth");
				res.getContext().put(new Position(), (Integer) res.getContext().get(new Position()) + 1);
				result.add(this.conclusion.substitution(res.getBinding(), res.getContext()));
			} catch (SubstituteFailedException e) {
				continue;
			}
		}
		return result;
	}
	
}