package inference.axioms;

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

import exceptions.SubstituteFailedException;
import inference.InferenceRule;
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.formulas.meta.MetaFormula;
import models.terms.Dependency;
import models.terms.RDLTerm;
import models.terms.Resource;
import models.terms.meta.MatchConstraint;
import models.terms.meta.MetaDependency;
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;

public class UncurriedMapping extends InferenceRule {
	
	public UncurriedMapping() {
		super("Uncurried Mapping");
		this.assumptions.add(
				new MetaDependencyFormula(
						new MetaDynamicDependency(new MetaTermGenerator() {
							@Override
							public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<String, Object> context) {
								int maxOrder = (Integer) context.get("maxOrder");
								context.put("" + curDepth, curIndex + 1);
								context.put("maxDepth", Math.max((Integer) context.getOrDefault("maxDepth", 0), curDepth + 1));
								if (curIndex == 0 && curDepth == maxDepth - 1) {
									return new MetaDependency(
											new MetaEvaluatableTermVariable(new Variable("se")),
											new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n"))
									);
								}
								if (curDepth < maxDepth && curIndex == 0) {
									return new MetaDynamicDependency(this);
								}
								return new MetaEvaluatableTermVariable(new Variable("v" + curDepth), new Constant("" + (maxOrder - (maxDepth - curDepth))));
							}
						})
				)
		);
		this.assumptions.add(new MetaEquationFormula(
				new MetaDependencyTerm(
						new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")),
						new MetaEvaluatableTermVariable(new Variable("xxx")),
						new MetaEvaluatableTermVariable(new Variable("yyy"))
				),
				new MetaEvaluatableTermVariable(new Variable("ue"), new Variable("m"))
		));
		this.conclusion = new MetaDependencyFormula(
				new MetaDynamicDependency(new MetaTermGenerator() {
					@Override
					public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<String, Object> context) {
						int maxOrder = (Integer) context.get("maxOrder");
						int uOrder = (Integer) context.get("uOrder");
						int maxIdx = (Integer) context.get("" + curDepth);
						if (curIndex >= maxIdx) {
							return null;
						}
						if (curIndex == 0 && curDepth == maxDepth - 1) {
							return new MetaDependencyTerm(
									new MetaEvaluatableTermVariable(new Variable("se")),
									new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")),
									new MetaEvaluatableTermVariable(new Variable("ue"), new Variable("m"))
							);
						}
						if (curDepth < maxDepth - 1 && curIndex == 0) {
							return new MetaDynamicDependency(this);
						}
						if (curDepth == uOrder && curIndex == 1) {
							return new MetaEvaluatableTermVariable(new Variable("ue"), new Variable("m"));
						}
						return new MetaEvaluatableTermVariable(new Variable("v" + curDepth), new Constant("" + (maxOrder - (maxDepth - curDepth))));
					}
				})
		);
	}

	
	protected Set<Formula> apply(List<Formula> assumptions, MatchConstraint constraint) {
		Map<String, Object> context = new HashMap<>();
		if (assumptions.size() < getAssumptionSize()) {
			return new HashSet<>();
		}
		
		Set<MatchConstraint> result = new HashSet<>();
		result.add(constraint);
		if (! (assumptions.get(0) instanceof DependencyFormula)) {
			return new HashSet<>();
		}
		Dependency dep = ((DependencyFormula)assumptions.get(0)).getDependency();
		int maxOrder = 0;
		while (true) {
			RDLTerm d2 = dep.getDependingTerm();
			if (d2 instanceof Resource) {
				maxOrder = dep.getDependedTerms().iterator().next().getOrder();
				break;
			}
			dep = (Dependency) d2;
		}
		
		for (int i = 0; i < getAssumptionSize(); i++) {
			context.put("maxOrder", maxOrder);
			result = this.assumptions.get(i).isMatchedBy(assumptions.get(i), result);
			if (result.isEmpty()) {
				return new HashSet<>();
			}
		}
		
		Set<MatchConstraint> ng = new HashSet<>();
		int m = 0;
		for (MatchConstraint matchConstraint : result) {
			int n = matchConstraint.getOrderConstraint().get(new Variable("n")).getOrder();
			m = matchConstraint.getOrderConstraint().get(new Variable("m")).getOrder();
			if (n != maxOrder) {
				ng.add(matchConstraint);
				continue;
			}
		}
		context.put("" + m, (Integer) context.get("" + m) + 1);
		
		if (this.repetitionAssumptions.size() != 0 && (assumptions.size() - this.assumptions.size()) % this.repetitionAssumptions.size() != 0) {
			return new HashSet<>();
		}
		if (this.repetitionAssumptions.size() != 0) {
			for (int i = 0; i < (assumptions.size() - this.assumptions.size()) / this.repetitionAssumptions.size(); i++) {
				List<MetaFormula> metaAssumptions = repetitionAssumptionGenerate(i);
				for (int j = 0; j < this.repetitionAssumptions.size(); j++) {
					Formula assumption = assumptions.get(this.assumptions.size() + i * this.repetitionAssumptions.size() + j);
					MetaFormula metaAssumption = metaAssumptions.get(j);
					result = metaAssumption.isMatchedBy(assumption, result);
					if (result.isEmpty()) {
						return new HashSet<>();
					}
				}
			}
		}
		Set<Formula> subRes = new HashSet<>();
		for (MatchConstraint con: result) {
			try {
				int maxIndex = conclusionMaxIndexCalculator != null ? conclusionMaxIndexCalculator.calculate(assumptions) : 10000;
				int uOrder = con.getBinding().get(new Variable("ue")).getOrder();
				context.put("maxIndex", maxIndex);
				context.put("uOrder", uOrder);
				subRes.add(conclusion.substitution(con.getBinding(), context));
			} catch (SubstituteFailedException e) {
				continue;
			}
		}
		return subRes;
	}
	
}