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.Variable;
import models.formulas.DependencyFormula;
import models.formulas.Formula;
import models.formulas.meta.MetaDependencyFormula;
import models.formulas.meta.MetaFormula;
import models.terms.meta.MatchConstraint;
import models.terms.meta.MetaDynamicDependency;
import models.terms.meta.MetaEvaluatableTermVariable;
import models.terms.meta.MetaRDLTerm;
import models.terms.meta.MetaRDLTermVariable;
import models.terms.meta.MetaTermGenerator;

public class RedundancyElimination extends InferenceRule {

	public RedundancyElimination() {
		super("Redundancy Elimination");
		assumptions.add(
				new MetaDependencyFormula(
						new MetaDynamicDependency(
								new MetaTermGenerator() {
									@Override
									public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<String, Object> context) {
										curIndex -= 1;
										context.put("firstAssumptionIndex", curIndex + 1);
										return new MetaEvaluatableTermVariable(new Variable("v" + curIndex));
									}
								},
								new MetaEvaluatableTermVariable(new Variable("u"))
						)
				)
		);
		assumptions.add(
				new MetaDependencyFormula(
						new MetaDynamicDependency(
								(ci, cd, mi, md, context) -> new MetaEvaluatableTermVariable(new Variable("v" + (ci - 2))),
								new MetaRDLTermVariable(new Variable("s")),
								new MetaEvaluatableTermVariable(new Variable("u"))
						)
				)
		);
		conclusion = new MetaDependencyFormula(
				new MetaDynamicDependency(
						new MetaTermGenerator() {
							@Override
							public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<String, Object> context) {
								curIndex -= 2;
								int firstAssumptionIndex = (Integer) context.get("firstAssumptionIndex");
								return new MetaEvaluatableTermVariable(new Variable("v" + (curIndex + firstAssumptionIndex)));
							}},
						new MetaRDLTermVariable(new Variable("s")),
						new MetaEvaluatableTermVariable(new Variable("u"))
				)
		);
		this.conclusionMaxIndexCalculator = (assumptions) -> ((DependencyFormula) assumptions.get(1)).getDependency().getMaxIndex() - ((DependencyFormula) assumptions.get(0)).getDependency().getMaxIndex() + 1;
	}
	
	protected Set<Formula> apply(List<Formula> assumptions, MatchConstraint constraint) {
		Map<String, Object> context = new HashMap<>();
		if (assumptions.size() < getAssumptionSize()) {
			return new HashSet<>();
		}
		if (((DependencyFormula) assumptions.get(0)).getDependency().getMaxIndex() >= ((DependencyFormula) assumptions.get(1)).getDependency().getMaxIndex()) {
			return new HashSet<>();
		}
		
		Set<MatchConstraint> result = new HashSet<>();
		result.add(constraint);
		for (int i = 0; i < getAssumptionSize(); i++) {
			result = this.assumptions.get(i).isMatchedBy(assumptions.get(i), result);
			if (result.isEmpty()) {
				return new HashSet<>();
			}
		}
		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) : 0;
				int maxDepth = conclusionMaxDepthCalculator != null ? conclusionMaxDepthCalculator.calculate(assumptions) : 1;
				context.put("maxIndex", maxIndex);
				context.put("maxDepth", maxDepth);
				subRes.add(conclusion.substitution(con.getBinding(), context));
			} catch (SubstituteFailedException e) {
				continue;
			}
		}
		return subRes;
	}
	
}