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.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.MetaTermGenerator;

public class CompositeMapping extends InferenceRule {
	
	public CompositeMapping() {
		super("Compsite Mapping");
		this.assumptions.add(
			new MetaDependencyFormula(
				new MetaDynamicDependency(
						(ci, cd, mi, md, context) -> new MetaEvaluatableTermVariable(new Variable("te" + (ci - 2))),
						new MetaEvaluatableTermVariable(new Variable("se")),
						new MetaEvaluatableTermVariable(new Variable("te"))
				)
			)
		);
		this.assumptions.add(
			new MetaDependencyFormula(
				new MetaDynamicDependency(
						(ci, cd, mi, md, context) -> new MetaEvaluatableTermVariable(new Variable("ue" + (ci - 1))),
						new MetaEvaluatableTermVariable(new Variable("te"))
				)
			)
		);
		this.conclusion = new MetaDependencyFormula(
				new MetaDynamicDependency(
						new MetaTermGenerator() {
							@Override
							public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth,Map<String, Object> context) {
								curIndex -= 1;
								int firstAssumptionSize = (Integer) context.get("firstAssumptionSize") - 2;
								if (curIndex < firstAssumptionSize) {
									return new MetaEvaluatableTermVariable(new Variable("te" + (curIndex)));
								}
								return new MetaEvaluatableTermVariable(new Variable("ue" + (curIndex - firstAssumptionSize)));
							}
							
						},
						new MetaEvaluatableTermVariable(new Variable("se"))
				)
			);
		conclusionMaxIndexCalculator = (assumptions) -> ((DependencyFormula) assumptions.get(0)).getDependency().getMaxIndex() - 2 + ((DependencyFormula) assumptions.get(1)).getDependency().getMaxIndex() - 1 + 1;
	}
	
	protected Set<Formula> apply(List<Formula> assumptions, MatchConstraint constraint) {
		if (assumptions.size() < getAssumptionSize()) {
			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;
				int firstAssumptionSize = ((DependencyFormula) assumptions.get(0)).getDependency().getMaxIndex();
				subRes.add(conclusion.substitution(con.getBinding(), Map.of("maxIndex", maxIndex, "maxDepth", maxDepth, "firstAssumptionSize", firstAssumptionSize)));
			} catch (SubstituteFailedException e) {
				continue;
			}
		}
		return subRes;
	}
	
}