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.EquationAxiom;
import models.algebra.Variable;
import models.formulas.Formula;
import models.formulas.meta.MetaDependencyFormula;
import models.formulas.meta.MetaEquationFormula;
import models.terms.meta.MatchConstraint;
import models.terms.meta.MetaDependencyTerm;
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;

public class MapComposition extends EquationAxiom {

	public MapComposition() {
		super("Map Composition");
		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("t"))
						)
				)
		);
		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 -= 2;
										context.put("secondAssumptionIndex", curIndex + 1);
										return new MetaEvaluatableTermVariable(new Variable("u" + curIndex));
									}
									
								},
								new MetaEvaluatableTermVariable(new Variable("s")),
								new MetaEvaluatableTermVariable(new Variable("t"))
						)
				)
		);
		this.conclusion = new MetaEquationFormula(
				new MetaDynamicDependencyTerm(
						new MetaTermGenerator() {
							@Override
							public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<String, Object> context) {
								curIndex -= 3;
								int secondAssumptionIndex = (Integer)context.get("secondAssumptionIndex");
								if (curIndex >= secondAssumptionIndex * 2) {
									return null;
								}
								if (curIndex % 2 == 0) {
									return new MetaEvaluatableTermVariable(new Variable("u" + curIndex / 2));
								}
								return new MetaEvaluatableTermVariable(new Variable("y" + curIndex / 2));
							}
						},
						new MetaEvaluatableTermVariable(new Variable("s")),
						new MetaEvaluatableTermVariable(new Variable("t")),
						new MetaDynamicDependencyTerm(
								new MetaTermGenerator() {
									@Override
									public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<String, Object> context) {
										curIndex -= 1;
										int firstAssumptionIndex = (Integer)context.get("firstAssumptionIndex");
										if (curIndex >= firstAssumptionIndex * 2) {
											return null;
										}
										if (curIndex % 2 == 0) {
											return new MetaEvaluatableTermVariable(new Variable("v" + curIndex / 2)); 
										}
										return new MetaEvaluatableTermVariable(new Variable("x" + curIndex / 2));
									}},
								new MetaEvaluatableTermVariable(new Variable("t"))
						)
				),
				new MetaDynamicDependencyTerm(
						new MetaTermGenerator() {
							@Override
							public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<String, Object> context) {
								curIndex -= 1;
								int firstAssumptionIndex = (Integer)context.get("firstAssumptionIndex");
								int secondAssumptionIndex = (Integer)context.get("secondAssumptionIndex");
								if (curIndex >= firstAssumptionIndex * 2 + secondAssumptionIndex * 2) {
									return null;
								}
								if (curIndex < firstAssumptionIndex * 2) {
									if (curIndex % 2 == 0) {
										return new MetaEvaluatableTermVariable(new Variable("v" + curIndex / 2)); 
									}
									return new MetaEvaluatableTermVariable(new Variable("x" + curIndex / 2));
								}
								curIndex -= firstAssumptionIndex * 2;
								if (curIndex % 2 == 0) {
									return new MetaEvaluatableTermVariable(new Variable("u" + curIndex / 2));
								}
								return new MetaEvaluatableTermVariable(new Variable("y" + curIndex / 2));
							}},
						new MetaEvaluatableTermVariable(new Variable("s"))
				)
		);
	}

	@Override
	protected Set<Formula> apply(List<Formula> assumptions, MatchConstraint constraint) {
		Map<String, Object> context = new HashMap<>();
		Set<MatchConstraint> matchResult = new HashSet<>();
		matchResult.add(constraint);
		if (assumptions.size() < 2) {
			return new HashSet<>();
		}
		for (int i = 0; i < 2; i++) {
			matchResult = this.assumptions.get(i).isMatchedBy(assumptions.get(i), matchResult, context);
			if (matchResult.isEmpty()) {
				return new HashSet<>();
			}
		}
		int firstAssumptionIndex = (Integer)context.get("firstAssumptionIndex");
		int secondAssumptionIndex = (Integer)context.get("secondAssumptionIndex");
		if (assumptions.size() < 2 + firstAssumptionIndex + secondAssumptionIndex) {
			return new HashSet<>();
		}
		for (int i = 0; i < firstAssumptionIndex; i++) {
			Formula assumption = assumptions.get(i + 2);
			MetaDependencyTerm mdt = new MetaDependencyTerm(
					new MetaEvaluatableTermVariable(new Variable("v" + i)),
					new MetaEvaluatableTermVariable(new Variable("xxx" + i)),
					new MetaEvaluatableTermVariable(new Variable("yyy" + i))
			);
			MetaEquationFormula mef = new MetaEquationFormula(mdt, new MetaEvaluatableTermVariable(new Variable("x" + i)));
			matchResult = mef.isMatchedBy(assumption, matchResult);
			if (matchResult.isEmpty()) {
				return new HashSet<>();
			}
		}
		for (int i = 0; i < secondAssumptionIndex; i++) {
			Formula assumption = assumptions.get(i + 2 + firstAssumptionIndex);
			MetaDependencyTerm mdt = new MetaDependencyTerm(
					new MetaEvaluatableTermVariable(new Variable("u" + i)),
					new MetaEvaluatableTermVariable(new Variable("xxxx" + i)),
					new MetaEvaluatableTermVariable(new Variable("yyyy" + i))
			);
			MetaEquationFormula mef = new MetaEquationFormula(mdt, new MetaEvaluatableTermVariable(new Variable("y" + i)));
			matchResult = mef.isMatchedBy(assumption, matchResult);
			if (matchResult.isEmpty()) {
				return new HashSet<>();
			}
		}
		Set<Formula> subRes = new HashSet<>();
		for (MatchConstraint con: matchResult) {
			try {
				int maxIndex = 10000;
				int maxDepth = 1;
				context.put("maxIndex", maxIndex);
				context.put("maxDepth", maxDepth);
				subRes.add(conclusion.substitution(con.getBinding(), context));
			} catch (SubstituteFailedException e) {
				continue;
			}
		}
		return subRes;
	}

	
	
}